diff options
Diffstat (limited to 'src/hls/HTLgenproof.v')
| -rw-r--r-- | src/hls/HTLgenproof.v | 54 |
1 files changed, 29 insertions, 25 deletions
diff --git a/src/hls/HTLgenproof.v b/src/hls/HTLgenproof.v index fc7af6b..bf1ef1c 100644 --- a/src/hls/HTLgenproof.v +++ b/src/hls/HTLgenproof.v @@ -34,6 +34,7 @@ Require vericert.hls.HTL. Require Import vericert.hls.HTLgen. Require Import vericert.hls.HTLgenspec. Require Import vericert.hls.ValueInt. +Require Import vericert.hls.FunctionalUnits. Require vericert.hls.Verilog. Require Import Lia. @@ -62,10 +63,10 @@ Definition state_st_wf (m : HTL.module) (s : HTL.state) := Inductive match_arrs (m : HTL.module) (f : RTL.function) (sp : Values.val) (mem : mem) : Verilog.assocmap_arr -> Prop := | match_arr : forall asa stack, - asa ! (m.(HTL.mod_stk)) = Some stack /\ + asa ! (m.(HTL.mod_ram).(ram_mem)) = Some stack /\ stack.(arr_length) = Z.to_nat (f.(RTL.fn_stacksize) / 4) /\ (forall ptr, - 0 <= ptr < Z.of_nat m.(HTL.mod_stk_len) -> + 0 <= ptr < Z.of_nat m.(HTL.mod_ram).(ram_size) -> opt_val_value_lessdef (Mem.loadv AST.Mint32 mem (Values.Val.offset_ptr sp (Integers.Ptrofs.repr (4 * ptr)))) (Option.default (NToValue 0) @@ -1003,26 +1004,29 @@ Section CORRECTNESS. constructor. Qed. - (** The proof of semantic preservation for the translation of instructions - is a simulation argument based on diagrams of the following form: -<< - match_states - code st rs ---------------- State m st assoc - || | - || | - || | - \/ v - code st rs' --------------- State m st assoc' - match_states ->> - where [tr_code c data control fin rtrn st] is assumed to hold. - - The precondition and postcondition is that that should hold is [match_assocmaps rs assoc]. - *) +(*| +The proof of semantic preservation for the translation of instructions is a +simulation argument based on diagrams of the following form: + +:: +> match_states +> code st rs ------------------------- State m st assoc +> || | +> || | +> || | +> \/ v +> code st rs' ------------------------ State m st assoc' +> match_states + +where ``tr_code c data control fin rtrn st`` is assumed to hold. + +The precondition and postcondition is that that should hold is ``match_assocmaps +rs assoc``. +|*) Definition transl_instr_prop (instr : RTL.instruction) : Prop := forall m asr asa fin rtrn st stmt trans res, - tr_instr fin rtrn st (m.(HTL.mod_stk)) instr stmt trans -> + tr_instr fin rtrn st (m.(HTL.mod_ram).(ram_mem)) instr stmt trans -> exists asr' asa', HTL.step tge (HTL.State res m st asr asa) Events.E0 (HTL.State res m st asr' asa'). @@ -1090,7 +1094,7 @@ Section CORRECTNESS. apply Smallstep.plus_one. eapply HTL.step_module; eauto. inv CONST; assumption. - inv CONST; assumption. + inv CONST; assumption. (* processing of state *) econstructor. crush. @@ -1098,9 +1102,9 @@ Section CORRECTNESS. econstructor. econstructor. - all: invert MARR; big_tac. + all: invert MARR; big_tac. Abort. - inv CONST; constructor; simplify; rewrite AssocMap.gso; auto; lia. +(* inv CONST; constructor; simplify; rewrite AssocMap.gso; auto; lia. Unshelve. exact tt. Qed. @@ -2568,7 +2572,7 @@ Section CORRECTNESS. Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ match_states (RTL.State s f sp pc' rs m) R2. Proof. intros s f sp pc rs m arg tbl n pc' H H0 H1 R1 MSTATE. - + #[local] Hint Resolve transl_ijumptable_correct : htlproof.*) Lemma transl_ireturn_correct: @@ -2862,13 +2866,13 @@ Section CORRECTNESS. Proof. induction 1; eauto with htlproof; (intros; inv_state). Qed. - #[local] Hint Resolve transl_step_correct : htlproof. + #[local] Hint Resolve transl_step_correct : htlproof.*) Theorem transf_program_correct: Smallstep.forward_simulation (RTL.semantics prog) (HTL.semantics tprog). Proof. eapply Smallstep.forward_simulation_plus; eauto with htlproof. apply senv_preserved. - Qed. + (*Qed.*)Admitted. End CORRECTNESS. |