diff options
author | Michalis Pardalos <m.pardalos@gmail.com> | 2021-06-10 22:01:26 +0100 |
---|---|---|
committer | Michalis Pardalos <m.pardalos@gmail.com> | 2021-06-10 22:01:26 +0100 |
commit | f7616136f1a2f3561500b1c28219ae725c4cda17 (patch) | |
tree | fed32ce1b6ff600883d5735891de7d2119f38b7a /src/hls | |
parent | 6957832da6522c7099b9554bfc68b67e0fb39444 (diff) | |
download | vericert-f7616136f1a2f3561500b1c28219ae725c4cda17.tar.gz vericert-f7616136f1a2f3561500b1c28219ae725c4cda17.zip |
Remove all Admitted from top-level Compiler.v
Diffstat (limited to 'src/hls')
-rw-r--r-- | src/hls/ApplyExternctrl.v | 16 | ||||
-rw-r--r-- | src/hls/HTLgenproof.v | 222 | ||||
-rw-r--r-- | src/hls/Renaming.v | 13 | ||||
-rw-r--r-- | src/hls/Veriloggen.v | 8 | ||||
-rw-r--r-- | src/hls/Veriloggenproof.v | 712 |
5 files changed, 588 insertions, 383 deletions
diff --git a/src/hls/ApplyExternctrl.v b/src/hls/ApplyExternctrl.v index 44c6b83..5ddbd4a 100644 --- a/src/hls/ApplyExternctrl.v +++ b/src/hls/ApplyExternctrl.v @@ -178,3 +178,19 @@ End APPLY_EXTERNCTRL. Definition transf_fundef (prog : HTL.program) := transf_partial_fundef (module_apply_externctrl prog). Definition transf_program (prog : HTL.program) := transform_partial_program (transf_fundef prog) prog. + +(* Semantics *) + +Definition match_prog : HTL.program -> HTL.program -> Prop := + Linking.match_program (fun ctx f tf => ApplyExternctrl.transf_fundef ctx f = OK tf) eq. + +Lemma transf_program_match : forall p tp, + ApplyExternctrl.transf_program p = OK tp -> match_prog p tp. +Admitted. + +Lemma transf_program_correct : forall p tp, + match_prog p tp -> Smallstep.forward_simulation (HTL.semantics p) (HTL.semantics tp). +Admitted. + +Instance TransfLink : Linking.TransfLink match_prog. +Admitted. diff --git a/src/hls/HTLgenproof.v b/src/hls/HTLgenproof.v index 0513066..cba21b0 100644 --- a/src/hls/HTLgenproof.v +++ b/src/hls/HTLgenproof.v @@ -171,6 +171,7 @@ Inductive match_states (ge : RTL.genv) : RTL.state -> HTL.state -> Prop := forall f m rtl_args htl_args mid mem rtl_stk htl_stk (TF : tr_module ge f m) (MF : match_frames ge mid mem rtl_stk htl_stk) + (NP : Forall not_pointer rtl_args) (MARGS : list_forall2 val_value_lessdef rtl_args htl_args), match_states ge (RTL.Callstate rtl_stk (AST.Internal f) rtl_args mem) @@ -1256,6 +1257,39 @@ Section CORRECTNESS. - destruct params; eauto using regs_lessdef_add_match with htlproof. Qed. + Lemma stack_based_set : forall sp r v rs, + stack_based v sp -> + reg_stack_based_pointers sp rs -> + reg_stack_based_pointers sp (Registers.Regmap.set r v rs). + Proof. + unfold reg_stack_based_pointers, Registers.Regmap.set, "_ !! _". + intros * ? ? r0. + simpl. + destruct (peq r r0); subst. + - rewrite AssocMap.gss; auto. + - rewrite AssocMap.gso; auto. + Qed. + + Lemma stack_based_non_pointers : forall args params stk, + Forall not_pointer args -> + reg_stack_based_pointers stk (RTL.init_regs args params). + Proof. + unfold reg_stack_based_pointers. + induction args; intros * NP *. + + destruct params; + simpl; + unfold "_ !! _"; + rewrite PTree.gempty; + crush. + + destruct params; simpl. + * unfold "_ !! _". rewrite PTree.gempty. crush. + * inv NP. + apply stack_based_set; + [ destruct a; crush + | unfold reg_stack_based_pointers; auto + ]. + Qed. + Lemma transl_callstate_correct: forall (s : list RTL.stackframe) (f : RTL.function) (args : list Values.val) (m : mem) (m' : Mem.mem') (stk : Values.block), @@ -1280,17 +1314,15 @@ Section CORRECTNESS. - repeat apply regs_lessdef_add_greater; try not_control_reg. eauto using match_args. - edestruct no_stack_calls; eauto. - + replace (RTL.fn_stacksize f) in *. - replace m' with m by - (destruct (mem_alloc_zero m); crush). - subst. + + replace (RTL.fn_stacksize f) with 0 in * + by assumption. + replace m' with m + by (destruct (mem_alloc_zero m); crush). assumption. + subst. inv MF. constructor. - - (* Stack pointer *) - admit. - - (* Stack based args *) - unfold reg_stack_based_pointers; intros. + - big_tac. admit. + - eauto using stack_based_non_pointers. - (* Stack based stack pointer *) unfold arr_stack_based_pointers; intros. admit. @@ -1315,7 +1347,76 @@ Section CORRECTNESS. exists x. crush. Qed. - Require Import Registers. + Fixpoint assign_all acc (rs : list reg) (vals : list value) := + match rs, vals with + | r::rs', val::vals' => assign_all (acc # r <- val) rs' vals' + | _, _ => acc + end. + + Notation "a ## b '<-' c" := (assign_all a b c) (at level 1, b at next level) : assocmap. + + Lemma assign_all_nil : forall a rs, a ## rs <- nil = a. + Proof. destruct rs; crush. Qed. + + Lemma assign_all_out : forall rs vs a r, (forall v, ~ In (r, v) (List.combine rs vs)) -> (a ## rs <- vs) ! r = a ! r. + Proof. + induction rs; intros * H. + - trivial. + - destruct vs. + + rewrite assign_all_nil. + trivial. + + simpl. + rewrite IHrs. + rewrite AssocMap.gso. + crush. + * simpl (List.combine _ _) in *. + specialize (H v). + rewrite not_in_cons in H. + inv H. + crush. + * intros v0. + specialize (H v0). + simpl (List.combine _ _) in *. + rewrite not_in_cons in H. + crush. + Qed. + + Lemma nonblock_all_exec : forall from_regs to_regs f basr nasr basa nasa, + Verilog.stmnt_runp + f + {| Verilog.assoc_blocking := basr; Verilog.assoc_nonblocking := nasr |} + {| Verilog.assoc_blocking := basa; Verilog.assoc_nonblocking := nasa |} + (nonblock_all (List.combine to_regs from_regs)) + {| Verilog.assoc_blocking := basr; Verilog.assoc_nonblocking := nasr ## to_regs <- (basr##from_regs) |} + {| Verilog.assoc_blocking := basa; Verilog.assoc_nonblocking := nasa |}. + Proof. + induction from_regs; intros. + - rewrite combine_nil, assign_all_nil. + constructor. + - destruct to_regs; try solve [ constructor ]. + simpl. + econstructor. + + repeat econstructor. + + eapply IHfrom_regs. + Qed. + + Lemma fork_exec : forall f basr nasr basa nasa rst to_regs from_regs, + Verilog.stmnt_runp + f + {| Verilog.assoc_blocking := basr; Verilog.assoc_nonblocking := nasr |} + {| Verilog.assoc_blocking := basa; Verilog.assoc_nonblocking := nasa |} + (fork rst (List.combine to_regs from_regs)) + {| Verilog.assoc_blocking := basr; Verilog.assoc_nonblocking := (nasr # rst <- (ZToValue 1)) ## to_regs <- (basr##from_regs) |} + {| Verilog.assoc_blocking := basa; Verilog.assoc_nonblocking := nasa |}. + Proof. + intros. + unfold fork. + econstructor. + - repeat econstructor. + - unfold Verilog.nonblock_reg; simpl. + eapply nonblock_all_exec. + Qed. + Lemma transl_icall_correct: forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive) (rs : RTL.regset) (m : mem) sig fn fd args dst pc', @@ -1325,8 +1426,96 @@ Section CORRECTNESS. match_states ge (RTL.State s f sp pc rs m) R1 -> exists R2 : HTL.state, Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ - match_states ge (RTL.Callstate (RTL.Stackframe dst f sp pc' rs :: s) fd rs##args m) R2. + match_states ge (RTL.Callstate (RTL.Stackframe dst f sp pc' rs :: s) fd + (List.map (fun r => Registers.Regmap.get r rs) args) m) + R2. Proof. + intros * H Hfunc * MSTATE. + inv_state. + edestruct (only_internal_calls fd); eauto; subst fd. + simpl in *. + eexists. split. + - inv CONST. + simplify. + eapply Smallstep.plus_three; simpl in *. + + eapply HTL.step_module; simpl. + * repeat econstructor; auto. + * repeat econstructor; auto. + * repeat econstructor; eauto. + * repeat econstructor; eauto. + * repeat econstructor; eauto. + * repeat econstructor; auto. + * repeat econstructor; eauto. + * eapply fork_exec. + * trivial. + * trivial. + * eapply AssocMapExt.merge_correct_1. + rewrite assign_all_out. + big_tac. + -- not_control_reg. + -- simpl. + insterU H6. + simplify. + admit. + * admit. + + eapply HTL.step_module; trivial. + * simpl. + apply AssocMapExt.merge_correct_2; auto. + rewrite assign_all_out by admit. + rewrite AssocMap.gso by not_control_reg. + rewrite AssocMap.gso by lia. + apply AssocMap.gempty. + * simpl. + apply AssocMapExt.merge_correct_2; auto. + rewrite assign_all_out by admit. + rewrite AssocMap.gso by not_control_reg. + rewrite AssocMap.gso by lia. + apply AssocMap.gempty. + * simpl. + apply AssocMapExt.merge_correct_1; auto. + rewrite assign_all_out by admit. + rewrite AssocMap.gso by not_control_reg. + apply AssocMap.gss. + * eauto. + * eauto. + * unfold state_wait. + eapply Verilog.stmnt_runp_Vcond_false. + -- simpl. econstructor; econstructor; simpl. + replace (Verilog.merge_regs ((empty_assocmap # st1 <- (posToValue x0)) # x1 <- (ZToValue 1)) ## x4 <- (asr ## args) asr) # x3 + with (ZToValue 0) by admit. + trivial. + -- auto. + -- econstructor. + * simpl. + apply AssocMapExt.merge_correct_1; auto. + rewrite assign_all_out by admit. + rewrite AssocMap.gso by not_control_reg. + apply AssocMap.gss. + * repeat econstructor. + * simpl. + apply AssocMapExt.merge_correct_2. + big_tac. + apply AssocMap.gempty. + not_control_reg. + assert (Ple dst (RTL.max_reg_function f)) + by eauto using RTL.max_reg_function_def. + xomega. + apply AssocMapExt.merge_correct_1. + rewrite assign_all_out by admit. + rewrite AssocMap.gso by not_control_reg. + apply AssocMap.gss. + * admit. + + eapply HTL.step_initcall. + * (* find called module *) admit. + * (* callee reset mapped *) admit. + * (* params mapped *) admit. + * (* callee reset unset *) admit. + * (* params set *) admit. + + eauto with htlproof. + - econstructor; try solve [repeat econstructor; eauto with htlproof ]. + + (* Called module is translated *) admit. + + (* Match stackframes *) admit. + + (* Argument values match *) admit. Admitted. Hint Resolve transl_icall_correct : htlproof. Close Scope rtl. @@ -1392,19 +1581,6 @@ Section CORRECTNESS. Qed. Hint Resolve transl_ireturn_correct : htlproof. - Lemma stack_based_set : forall sp r v rs, - stack_based v sp -> - reg_stack_based_pointers sp rs -> - reg_stack_based_pointers sp (Registers.Regmap.set r v rs). - Proof. - unfold reg_stack_based_pointers, Registers.Regmap.set, "_ !! _". - intros * ? ? r0. - simpl. - destruct (Pos.eq_dec r r0); subst. - - rewrite AssocMap.gss; auto. - - rewrite AssocMap.gso; auto. - Qed. - Lemma transl_returnstate_correct: forall (res0 : Registers.reg) (f : RTL.function) (sp : Values.val) (pc : RTL.node) (rs : RTL.regset) (s : list RTL.stackframe) (vres : Values.val) (m : mem) diff --git a/src/hls/Renaming.v b/src/hls/Renaming.v index 3efc20f..b9fbcaa 100644 --- a/src/hls/Renaming.v +++ b/src/hls/Renaming.v @@ -216,3 +216,16 @@ Definition transf_program (p : HTL.program) : Errors.res HTL.program := (fun _ f => renumber_fundef f) (mk_renumber_state 1%positive (PTree.empty reg)) p. + +Definition match_prog : HTL.program -> HTL.program -> Prop := fun _ _ => True. + +Instance TransfRenamingLink : Linking.TransfLink match_prog. +Admitted. + +Lemma transf_program_match : forall p tp, + Renaming.transf_program p = Errors.OK tp -> match_prog p tp. +Admitted. + +Lemma transf_program_correct : forall p tp, + match_prog p tp -> Smallstep.forward_simulation (HTL.semantics p) (HTL.semantics tp). +Admitted. diff --git a/src/hls/Veriloggen.v b/src/hls/Veriloggen.v index 1f0938b..7ace6be 100644 --- a/src/hls/Veriloggen.v +++ b/src/hls/Veriloggen.v @@ -63,9 +63,9 @@ Section TRANSLATE. end. (* FIXME Remove the fuel parameter (recursion limit)*) - Fixpoint transf_module (fuel : nat) (prog : HTL.program) (externclk : option reg) (m : HTL.module) : res Verilog.module := + Fixpoint transl_module (fuel : nat) (prog : HTL.program) (externclk : option reg) (m : HTL.module) : res Verilog.module := match fuel with - | O => Error (msg "Veriloggen: transf_module recursion too deep") + | O => Error (msg "Veriloggen: transl_module recursion too deep") | S fuel' => let clk := match externclk with | None => HTL.mod_clk m @@ -77,7 +77,7 @@ Section TRANSLATE. let htl_modules := PTree.filter (fun m _ => List.existsb (Pos.eqb m) inline_names) modmap in - do translated_modules <- PTree.traverse (fun _ => transf_module fuel' prog (Some clk)) htl_modules; + do translated_modules <- PTree.traverse (fun _ => transl_module fuel' prog (Some clk)) htl_modules; let cleaned_modules := PTree.map1 (map_body (Option.map_option (clean_up_decl clk))) translated_modules in @@ -125,7 +125,7 @@ Section TRANSLATE. (HTL.mod_entrypoint m)) end. - Definition transl_fundef (prog : HTL.program) := transf_partial_fundef (transf_module 10 prog None). + Definition transl_fundef (prog : HTL.program) := transf_partial_fundef (transl_module 10 prog None). Definition transl_program (prog : HTL.program) := transform_partial_program (transl_fundef prog) prog. End TRANSLATE. diff --git a/src/hls/Veriloggenproof.v b/src/hls/Veriloggenproof.v index 59267f7..ccb315e 100644 --- a/src/hls/Veriloggenproof.v +++ b/src/hls/Veriloggenproof.v @@ -22,247 +22,247 @@ From vericert Require HTL. From vericert Require Import Vericertlib Veriloggen Verilog ValueInt AssocMap. Require Import Lia. - Local Open Scope assocmap. Definition match_prog (prog : HTL.program) (tprog : Verilog.program) := match_program (fun cu f tf => Errors.OK tf = transl_fundef prog f) eq prog tprog. -(* - Lemma transf_program_match: - forall prog, match_prog prog (transl_program prog). -Proof. - intros. eapply match_transform_program_contextual. auto. -Qed. - -Inductive match_stacks : list HTL.stackframe -> list stackframe -> Prop := -| match_stack : - forall res m pc reg_assoc arr_assoc hstk vstk, - match_stacks hstk vstk -> - match_stacks (HTL.Stackframe res m pc reg_assoc arr_assoc :: hstk) - (Stackframe res (transl_module m) pc - reg_assoc arr_assoc :: vstk) -| match_stack_nil : match_stacks nil nil. - -Inductive match_states : HTL.state -> state -> Prop := -| match_state : - forall m st reg_assoc arr_assoc hstk vstk, - match_stacks hstk vstk -> - match_states (HTL.State hstk m st reg_assoc arr_assoc) - (State vstk (transl_module m) st reg_assoc arr_assoc) -| match_returnstate : - forall v hstk vstk, - match_stacks hstk vstk -> - match_states (HTL.Returnstate hstk v) (Returnstate vstk v) -| match_initial_call : - forall m, - match_states (HTL.Callstate nil m nil) (Callstate nil (transl_module m) nil). - -Lemma Vlit_inj : - forall a b, Vlit a = Vlit b -> a = b. -Proof. inversion 1. trivial. Qed. - -Lemma posToValue_inj : - forall a b, - 0 <= Z.pos a <= Int.max_unsigned -> - 0 <= Z.pos b <= Int.max_unsigned -> - posToValue a = posToValue b -> - a = b. -Proof. - intros. rewrite <- Pos2Z.id at 1. rewrite <- Pos2Z.id. - rewrite <- Int.unsigned_repr at 1; try assumption. - symmetry. - rewrite <- Int.unsigned_repr at 1; try assumption. - unfold posToValue in *. rewrite H1; auto. -Qed. - -Lemma valueToPos_inj : - forall a b, - 0 < Int.unsigned a -> - 0 < Int.unsigned b -> - valueToPos a = valueToPos b -> - a = b. -Proof. - intros. unfold valueToPos in *. - rewrite <- Int.repr_unsigned at 1. - rewrite <- Int.repr_unsigned. - apply Pos2Z.inj_iff in H1. - rewrite Z2Pos.id in H1; auto. - rewrite Z2Pos.id in H1; auto. - rewrite H1. auto. -Qed. - -Lemma unsigned_posToValue_le : - forall p, - Z.pos p <= Int.max_unsigned -> - 0 < Int.unsigned (posToValue p). -Proof. - intros. unfold posToValue. rewrite Int.unsigned_repr; lia. -Qed. - -Lemma transl_ctrl_fun_fst : - forall p1 p2 a b, - 0 <= Z.pos p1 <= Int.max_unsigned -> - 0 <= Z.pos p2 <= Int.max_unsigned -> - transl_ctrl_fun (p1, a) = transl_ctrl_fun (p2, b) -> - (p1, a) = (p2, b). -Proof. - intros. unfold transl_ctrl_fun in H1. apply pair_equal_spec in H1. - destruct H1. rewrite H2. apply Vlit_inj in H1. - apply posToValue_inj in H1; try assumption. - rewrite H1; auto. -Qed. - -Lemma transl_data_fun_fst : - forall p1 p2 a b, - 0 <= Z.pos p1 <= Int.max_unsigned -> - 0 <= Z.pos p2 <= Int.max_unsigned -> - transl_datapath_fun (p1, a) = transl_datapath_fun (p2, b) -> - p1 = p2. -Proof. - intros. - unfold transl_datapath_fun in H1. apply pair_equal_spec in H1. destruct H1. - apply Vlit_inj in H1. apply posToValue_inj in H1; assumption. -Qed. - -Lemma Zle_relax : - forall p q r, - p < q <= r -> - p <= q <= r. -Proof. lia. Qed. -Hint Resolve Zle_relax : verilogproof. - -Lemma transl_in : - forall l p, - 0 <= Z.pos p <= Int.max_unsigned -> - (forall p0, In p0 (List.map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> - In (Vlit (posToValue p)) (map fst (map transl_ctrl_fun l)) -> - In p (map fst l). -Proof. - induction l. - - simplify. auto. - - intros. destruct a. simplify. destruct (peq p0 p); auto. - right. inv H1. apply Vlit_inj in H. apply posToValue_inj in H; auto. contradiction. - auto with verilogproof. - apply IHl; auto. -Qed. - -Lemma transl_notin : - forall l p, - 0 <= Z.pos p <= Int.max_unsigned -> - (forall p0, In p0 (List.map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> - ~ In p (List.map fst l) -> ~ In (Vlit (posToValue p)) (List.map fst (transl_ctrl l)). -Proof. - induction l; auto. intros. destruct a. unfold not in *. intros. - simplify. - destruct (peq p0 p). apply H1. auto. apply H1. - unfold transl_ctrl in *. inv H2. apply Vlit_inj in H. apply posToValue_inj in H. - contradiction. - auto with verilogproof. auto. - right. apply transl_in; auto. -Qed. - -Lemma transl_norepet : - forall l, - (forall p0, In p0 (List.map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> - list_norepet (List.map fst l) -> list_norepet (List.map fst (transl_ctrl l)). + forall prog tprog, transl_program prog = Errors.OK tprog -> match_prog prog tprog. Proof. - induction l. - - intros. simpl. apply list_norepet_nil. - - destruct a. intros. simpl. apply list_norepet_cons. - inv H0. apply transl_notin. apply Zle_relax. apply H. simplify; auto. - intros. apply H. destruct (peq p0 p); subst; simplify; auto. - assumption. apply IHl. intros. apply H. destruct (peq p0 p); subst; simplify; auto. - simplify. inv H0. assumption. + intros. unfold transl_program in *. eapply match_transform_partial_program_contextual; eauto. Qed. -Lemma transl_ctrl_correct : - forall l v ev f asr asa asrn asan asr' asa' asrn' asan', - (forall p0, In p0 (List.map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> - list_norepet (List.map fst l) -> - asr!ev = Some v -> - (forall p s, - In (p, s) l -> - v = posToValue p -> - stmnt_runp f - {| assoc_blocking := asr; assoc_nonblocking := asrn |} - {| assoc_blocking := asa; assoc_nonblocking := asan |} - s - {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} - {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> - stmnt_runp f - {| assoc_blocking := asr; assoc_nonblocking := asrn |} - {| assoc_blocking := asa; assoc_nonblocking := asan |} - (Vcase (Vvar ev) (transl_ctrl l) (Some Vskip)) - {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} - {| assoc_blocking := asa'; assoc_nonblocking := asan' |}). -Proof. - induction l as [| a l IHl]. - - contradiction. - - intros v ev f asr asa asrn asan asr' asa' asrn' asan' BOUND NOREP ASSOC p s IN EQ SRUN. - destruct a as [p' s']. simplify. - destruct (peq p p'); subst. eapply stmnt_runp_Vcase_match. - constructor. simplify. unfold AssocMap.find_assocmap, AssocMapExt.get_default. - rewrite ASSOC. trivial. constructor. auto. - inversion IN as [INV | INV]. inversion INV as [INV2]; subst. assumption. - inv NOREP. eapply in_map with (f := fst) in INV. contradiction. - - eapply stmnt_runp_Vcase_nomatch. constructor. simplify. - unfold AssocMap.find_assocmap, AssocMapExt.get_default. rewrite ASSOC. - trivial. constructor. unfold not. intros. apply n. apply posToValue_inj. - apply Zle_relax. apply BOUND. right. inv IN. inv H0; contradiction. - eapply in_map with (f := fst) in H0. auto. - apply Zle_relax. apply BOUND; auto. auto. - - eapply IHl. auto. inv NOREP. auto. eassumption. inv IN. inv H. contradiction. apply H. - trivial. assumption. -Qed. -Hint Resolve transl_ctrl_correct : verilogproof. - -(* FIXME Probably wrong we probably need some statemnt about datapath_statement_runp *) -Lemma transl_datapath_correct : - forall l v ev f asr asa asrn asan asr' asa' asrn' asan', - (forall p0, In p0 (List.map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> - list_norepet (List.map fst l) -> - asr!ev = Some v -> - (forall p s, - In (p, s) l -> - v = posToValue p -> - stmnt_runp f - {| assoc_blocking := asr; assoc_nonblocking := asrn |} - {| assoc_blocking := asa; assoc_nonblocking := asan |} - s - {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} - {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> - stmnt_runp f - {| assoc_blocking := asr; assoc_nonblocking := asrn |} - {| assoc_blocking := asa; assoc_nonblocking := asan |} - (Vcase (Vvar ev) (transl_ctrl l) (Some Vskip)) - {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} - {| assoc_blocking := asa'; assoc_nonblocking := asan' |}). -Proof. Admitted. - -Lemma pc_wf : - forall A m p v, - (forall p0, In p0 (List.map fst (@AssocMap.elements A m)) -> 0 < Z.pos p0 <= Int.max_unsigned) -> - m!p = Some v -> - 0 <= Z.pos p <= Int.max_unsigned. -Proof. - intros A m p v LT S. apply Zle_relax. apply LT. - apply AssocMap.elements_correct in S. remember (p, v) as x. - exploit in_map. apply S. instantiate (1 := fst). subst. simplify. auto. -Qed. - -Lemma mis_stepp_decl : - forall l asr asa f, - mis_stepp f asr asa (map Vdeclaration l) asr asa. -Proof. - induction l. - - intros. constructor. - - intros. simplify. econstructor. constructor. auto. -Qed. -Hint Resolve mis_stepp_decl : verilogproof. +Instance TransfVerilogLink : TransfLink Veriloggenproof.match_prog. +Admitted. + +(* Inductive match_stacks : list HTL.stackframe -> list stackframe -> Prop := *) +(* | match_stack : *) +(* forall res m pc reg_assoc arr_assoc hstk vstk, *) +(* match_stacks hstk vstk -> *) +(* match_stacks (HTL.Stackframe res m pc reg_assoc arr_assoc :: hstk) *) +(* (Stackframe res (transl_module m) pc *) +(* reg_assoc arr_assoc :: vstk) *) +(* | match_stack_nil : match_stacks nil nil. *) + +(* Inductive match_states : HTL.state -> state -> Prop := *) +(* | match_state : *) +(* forall m st reg_assoc arr_assoc hstk vstk, *) +(* match_stacks hstk vstk -> *) +(* match_states (HTL.State hstk m st reg_assoc arr_assoc) *) +(* (State vstk (transl_module m) st reg_assoc arr_assoc) *) +(* | match_returnstate : *) +(* forall v hstk vstk, *) +(* match_stacks hstk vstk -> *) +(* match_states (HTL.Returnstate hstk v) (Returnstate vstk v) *) +(* | match_initial_call : *) +(* forall m, *) +(* match_states (HTL.Callstate nil m nil) (Callstate nil (transl_module m) nil). *) + +(* Lemma Vlit_inj : *) +(* forall a b, Vlit a = Vlit b -> a = b. *) +(* Proof. inversion 1. trivial. Qed. *) + +(* Lemma posToValue_inj : *) +(* forall a b, *) +(* 0 <= Z.pos a <= Int.max_unsigned -> *) +(* 0 <= Z.pos b <= Int.max_unsigned -> *) +(* posToValue a = posToValue b -> *) +(* a = b. *) +(* Proof. *) +(* intros. rewrite <- Pos2Z.id at 1. rewrite <- Pos2Z.id. *) +(* rewrite <- Int.unsigned_repr at 1; try assumption. *) +(* symmetry. *) +(* rewrite <- Int.unsigned_repr at 1; try assumption. *) +(* unfold posToValue in *. rewrite H1; auto. *) +(* Qed. *) + +(* Lemma valueToPos_inj : *) +(* forall a b, *) +(* 0 < Int.unsigned a -> *) +(* 0 < Int.unsigned b -> *) +(* valueToPos a = valueToPos b -> *) +(* a = b. *) +(* Proof. *) +(* intros. unfold valueToPos in *. *) +(* rewrite <- Int.repr_unsigned at 1. *) +(* rewrite <- Int.repr_unsigned. *) +(* apply Pos2Z.inj_iff in H1. *) +(* rewrite Z2Pos.id in H1; auto. *) +(* rewrite Z2Pos.id in H1; auto. *) +(* rewrite H1. auto. *) +(* Qed. *) + +(* Lemma unsigned_posToValue_le : *) +(* forall p, *) +(* Z.pos p <= Int.max_unsigned -> *) +(* 0 < Int.unsigned (posToValue p). *) +(* Proof. *) +(* intros. unfold posToValue. rewrite Int.unsigned_repr; lia. *) +(* Qed. *) + +(* Lemma transl_ctrl_fun_fst : *) +(* forall p1 p2 a b, *) +(* 0 <= Z.pos p1 <= Int.max_unsigned -> *) +(* 0 <= Z.pos p2 <= Int.max_unsigned -> *) +(* transl_ctrl_fun (p1, a) = transl_ctrl_fun (p2, b) -> *) +(* (p1, a) = (p2, b). *) +(* Proof. *) +(* intros. unfold transl_ctrl_fun in H1. apply pair_equal_spec in H1. *) +(* destruct H1. rewrite H2. apply Vlit_inj in H1. *) +(* apply posToValue_inj in H1; try assumption. *) +(* rewrite H1; auto. *) +(* Qed. *) + +(* Lemma transl_data_fun_fst : *) +(* forall p1 p2 a b, *) +(* 0 <= Z.pos p1 <= Int.max_unsigned -> *) +(* 0 <= Z.pos p2 <= Int.max_unsigned -> *) +(* transl_datapath_fun (p1, a) = transl_datapath_fun (p2, b) -> *) +(* p1 = p2. *) +(* Proof. *) +(* intros. *) +(* unfold transl_datapath_fun in H1. apply pair_equal_spec in H1. destruct H1. *) +(* apply Vlit_inj in H1. apply posToValue_inj in H1; assumption. *) +(* Qed. *) + +(* Lemma Zle_relax : *) +(* forall p q r, *) +(* p < q <= r -> *) +(* p <= q <= r. *) +(* Proof. lia. Qed. *) +(* Hint Resolve Zle_relax : verilogproof. *) + +(* Lemma transl_in : *) +(* forall l p, *) +(* 0 <= Z.pos p <= Int.max_unsigned -> *) +(* (forall p0, In p0 (List.map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> *) +(* In (Vlit (posToValue p)) (map fst (map transl_ctrl_fun l)) -> *) +(* In p (map fst l). *) +(* Proof. *) +(* induction l. *) +(* - simplify. auto. *) +(* - intros. destruct a. simplify. destruct (peq p0 p); auto. *) +(* right. inv H1. apply Vlit_inj in H. apply posToValue_inj in H; auto. contradiction. *) +(* auto with verilogproof. *) +(* apply IHl; auto. *) +(* Qed. *) + +(* Lemma transl_notin : *) +(* forall l p, *) +(* 0 <= Z.pos p <= Int.max_unsigned -> *) +(* (forall p0, In p0 (List.map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> *) +(* ~ In p (List.map fst l) -> ~ In (Vlit (posToValue p)) (List.map fst (transl_ctrl l)). *) +(* Proof. *) +(* induction l; auto. intros. destruct a. unfold not in *. intros. *) +(* simplify. *) +(* destruct (peq p0 p). apply H1. auto. apply H1. *) +(* unfold transl_ctrl in *. inv H2. apply Vlit_inj in H. apply posToValue_inj in H. *) +(* contradiction. *) +(* auto with verilogproof. auto. *) +(* right. apply transl_in; auto. *) +(* Qed. *) + +(* Lemma transl_norepet : *) +(* forall l, *) +(* (forall p0, In p0 (List.map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> *) +(* list_norepet (List.map fst l) -> list_norepet (List.map fst (transl_ctrl l)). *) +(* Proof. *) +(* induction l. *) +(* - intros. simpl. apply list_norepet_nil. *) +(* - destruct a. intros. simpl. apply list_norepet_cons. *) +(* inv H0. apply transl_notin. apply Zle_relax. apply H. simplify; auto. *) +(* intros. apply H. destruct (peq p0 p); subst; simplify; auto. *) +(* assumption. apply IHl. intros. apply H. destruct (peq p0 p); subst; simplify; auto. *) +(* simplify. inv H0. assumption. *) +(* Qed. *) + +(* Lemma transl_ctrl_correct : *) +(* forall l v ev f asr asa asrn asan asr' asa' asrn' asan', *) +(* (forall p0, In p0 (List.map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> *) +(* list_norepet (List.map fst l) -> *) +(* asr!ev = Some v -> *) +(* (forall p s, *) +(* In (p, s) l -> *) +(* v = posToValue p -> *) +(* stmnt_runp f *) +(* {| assoc_blocking := asr; assoc_nonblocking := asrn |} *) +(* {| assoc_blocking := asa; assoc_nonblocking := asan |} *) +(* s *) +(* {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} *) +(* {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> *) +(* stmnt_runp f *) +(* {| assoc_blocking := asr; assoc_nonblocking := asrn |} *) +(* {| assoc_blocking := asa; assoc_nonblocking := asan |} *) +(* (Vcase (Vvar ev) (transl_ctrl l) (Some Vskip)) *) +(* {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} *) +(* {| assoc_blocking := asa'; assoc_nonblocking := asan' |}). *) +(* Proof. *) +(* induction l as [| a l IHl]. *) +(* - contradiction. *) +(* - intros v ev f asr asa asrn asan asr' asa' asrn' asan' BOUND NOREP ASSOC p s IN EQ SRUN. *) +(* destruct a as [p' s']. simplify. *) +(* destruct (peq p p'); subst. eapply stmnt_runp_Vcase_match. *) +(* constructor. simplify. unfold AssocMap.find_assocmap, AssocMapExt.get_default. *) +(* rewrite ASSOC. trivial. constructor. auto. *) +(* inversion IN as [INV | INV]. inversion INV as [INV2]; subst. assumption. *) +(* inv NOREP. eapply in_map with (f := fst) in INV. contradiction. *) + +(* eapply stmnt_runp_Vcase_nomatch. constructor. simplify. *) +(* unfold AssocMap.find_assocmap, AssocMapExt.get_default. rewrite ASSOC. *) +(* trivial. constructor. unfold not. intros. apply n. apply posToValue_inj. *) +(* apply Zle_relax. apply BOUND. right. inv IN. inv H0; contradiction. *) +(* eapply in_map with (f := fst) in H0. auto. *) +(* apply Zle_relax. apply BOUND; auto. auto. *) + +(* eapply IHl. auto. inv NOREP. auto. eassumption. inv IN. inv H. contradiction. apply H. *) +(* trivial. assumption. *) +(* Qed. *) +(* Hint Resolve transl_ctrl_correct : verilogproof. *) + +(* (* FIXME Probably wrong we probably need some statemnt about datapath_statement_runp *) *) +(* Lemma transl_datapath_correct : *) +(* forall l v ev f asr asa asrn asan asr' asa' asrn' asan', *) +(* (forall p0, In p0 (List.map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> *) +(* list_norepet (List.map fst l) -> *) +(* asr!ev = Some v -> *) +(* (forall p s, *) +(* In (p, s) l -> *) +(* v = posToValue p -> *) +(* stmnt_runp f *) +(* {| assoc_blocking := asr; assoc_nonblocking := asrn |} *) +(* {| assoc_blocking := asa; assoc_nonblocking := asan |} *) +(* s *) +(* {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} *) +(* {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> *) +(* stmnt_runp f *) +(* {| assoc_blocking := asr; assoc_nonblocking := asrn |} *) +(* {| assoc_blocking := asa; assoc_nonblocking := asan |} *) +(* (Vcase (Vvar ev) (transl_ctrl l) (Some Vskip)) *) +(* {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} *) +(* {| assoc_blocking := asa'; assoc_nonblocking := asan' |}). *) +(* Proof. Admitted. *) + +(* Lemma pc_wf : *) +(* forall A m p v, *) +(* (forall p0, In p0 (List.map fst (@AssocMap.elements A m)) -> 0 < Z.pos p0 <= Int.max_unsigned) -> *) +(* m!p = Some v -> *) +(* 0 <= Z.pos p <= Int.max_unsigned. *) +(* Proof. *) +(* intros A m p v LT S. apply Zle_relax. apply LT. *) +(* apply AssocMap.elements_correct in S. remember (p, v) as x. *) +(* exploit in_map. apply S. instantiate (1 := fst). subst. simplify. auto. *) +(* Qed. *) + +(* Lemma mis_stepp_decl : *) +(* forall l asr asa f, *) +(* mis_stepp f asr asa (map Vdeclaration l) asr asa. *) +(* Proof. *) +(* induction l. *) +(* - intros. constructor. *) +(* - intros. simplify. econstructor. constructor. auto. *) +(* Qed. *) +(* Hint Resolve mis_stepp_decl : verilogproof. *) Section CORRECTNESS. @@ -279,133 +279,133 @@ Section CORRECTNESS. Proof. intros. eapply (Genv.find_symbol_match TRANSL). Qed. Hint Resolve symbols_preserved : verilogproof. - Lemma function_ptr_translated: - forall (b: Values.block) (f: HTL.fundef), - Genv.find_funct_ptr ge b = Some f -> - exists tf, - Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = tf. - Proof. - intros. exploit (Genv.find_funct_ptr_match TRANSL); eauto. - intros (cu & tf & P & Q & R); exists tf; auto. - Qed. - Hint Resolve function_ptr_translated : verilogproof. - - Lemma functions_translated: - forall (v: Values.val) (f: HTL.fundef), - Genv.find_funct ge v = Some f -> - exists tf, - Genv.find_funct tge v = Some tf /\ transl_fundef f = tf. - Proof. - intros. exploit (Genv.find_funct_match TRANSL); eauto. - intros (cu & tf & P & Q & R); exists tf; auto. - Qed. - Hint Resolve functions_translated : verilogproof. - - Lemma senv_preserved: - Senv.equiv (Genv.to_senv ge) (Genv.to_senv tge). - Proof. - intros. eapply (Genv.senv_match TRANSL). - Qed. - Hint Resolve senv_preserved : verilogproof. - - Theorem transl_step_correct : - forall (S1 : HTL.state) t S2, - HTL.step ge S1 t S2 -> - forall (R1 : state), - match_states S1 R1 -> - exists R2, Smallstep.plus step tge R1 t R2 /\ match_states S2 R2. - Proof. - induction 1; intros R1 MSTATE; inv MSTATE. - - econstructor; split. apply Smallstep.plus_one. econstructor. - assumption. assumption. eassumption. apply valueToPos_posToValue. - split. lia. - eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _]. - split. lia. apply HP. eassumption. eassumption. - econstructor. econstructor. eapply stmnt_runp_Vcond_false. econstructor. econstructor. - simpl. unfold find_assocmap. unfold AssocMapExt.get_default. - rewrite H. trivial. - - econstructor. simpl. auto. auto. - - eapply transl_ctrl_correct. - intros. split. lia. pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _]. auto. - apply Maps.PTree.elements_keys_norepet. eassumption. - 2: { apply valueToPos_inj. apply unsigned_posToValue_le. - eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _]. - split. lia. apply HP. eassumption. eassumption. - apply unsigned_posToValue_le. eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. - destruct HP as [HP _]. - split. lia. apply HP. eassumption. eassumption. trivial. - } - apply Maps.PTree.elements_correct. eassumption. eassumption. - - econstructor. econstructor. - - { admit. - (* - eapply transl_list_correct. - intros. split. lia. pose proof (HTL.mod_wf m) as HP. destruct HP as [_ HP]. auto. - apply Maps.PTree.elements_keys_norepet. eassumption. - 2: { apply valueToPos_inj. apply unsigned_posToValue_le. - eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _]. - split. lia. apply HP. eassumption. eassumption. - apply unsigned_posToValue_le. eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. - destruct HP as [HP _]. - split. lia. apply HP. eassumption. eassumption. trivial. - } - apply Maps.PTree.elements_correct. eassumption. eassumption. - *) - } - - apply mis_stepp_decl. trivial. trivial. simpl. eassumption. auto. - rewrite valueToPos_posToValue. constructor; assumption. lia. - - econstructor; split. apply Smallstep.plus_one. apply step_finish. assumption. eassumption. - constructor; assumption. - - econstructor; split. apply Smallstep.plus_one. constructor. - - constructor. constructor. - - inv H3. econstructor; split. apply Smallstep.plus_one. constructor. trivial. - - apply match_state. assumption. - Admitted. - Hint Resolve transl_step_correct : verilogproof. - - Lemma transl_initial_states : - forall s1 : Smallstep.state (HTL.semantics prog), - Smallstep.initial_state (HTL.semantics prog) s1 -> - exists s2 : Smallstep.state (Verilog.semantics tprog), - Smallstep.initial_state (Verilog.semantics tprog) s2 /\ match_states s1 s2. - Proof. - induction 1. - econstructor; split. econstructor. - apply (Genv.init_mem_transf TRANSL); eauto. - rewrite symbols_preserved. - replace (AST.prog_main tprog) with (AST.prog_main prog); eauto. - symmetry; eapply Linking.match_program_main; eauto. - exploit function_ptr_translated; eauto. intros [tf [A B]]. - inv B. eauto. - constructor. - Qed. - Hint Resolve transl_initial_states : verilogproof. - - Lemma transl_final_states : - forall (s1 : Smallstep.state (HTL.semantics prog)) - (s2 : Smallstep.state (Verilog.semantics tprog)) - (r : Integers.Int.int), - match_states s1 s2 -> - Smallstep.final_state (HTL.semantics prog) s1 r -> - Smallstep.final_state (Verilog.semantics tprog) s2 r. - Proof. - intros. inv H0. inv H. inv H3. constructor. reflexivity. - Qed. - Hint Resolve transl_final_states : verilogproof. +(* Lemma function_ptr_translated: *) +(* forall (b: Values.block) (f: HTL.fundef), *) +(* Genv.find_funct_ptr ge b = Some f -> *) +(* exists tf, *) +(* Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = tf. *) +(* Proof. *) +(* intros. exploit (Genv.find_funct_ptr_match TRANSL); eauto. *) +(* intros (cu & tf & P & Q & R); exists tf; auto. *) +(* Qed. *) +(* Hint Resolve function_ptr_translated : verilogproof. *) + +(* Lemma functions_translated: *) +(* forall (v: Values.val) (f: HTL.fundef), *) +(* Genv.find_funct ge v = Some f -> *) +(* exists tf, *) +(* Genv.find_funct tge v = Some tf /\ transl_fundef f = tf. *) +(* Proof. *) +(* intros. exploit (Genv.find_funct_match TRANSL); eauto. *) +(* intros (cu & tf & P & Q & R); exists tf; auto. *) +(* Qed. *) +(* Hint Resolve functions_translated : verilogproof. *) + +(* Lemma senv_preserved: *) +(* Senv.equiv (Genv.to_senv ge) (Genv.to_senv tge). *) +(* Proof. *) +(* intros. eapply (Genv.senv_match TRANSL). *) +(* Qed. *) +(* Hint Resolve senv_preserved : verilogproof. *) + +(* Theorem transl_step_correct : *) +(* forall (S1 : HTL.state) t S2, *) +(* HTL.step ge S1 t S2 -> *) +(* forall (R1 : state), *) +(* match_states S1 R1 -> *) +(* exists R2, Smallstep.plus step tge R1 t R2 /\ match_states S2 R2. *) +(* Proof. *) +(* induction 1; intros R1 MSTATE; inv MSTATE. *) +(* - econstructor; split. apply Smallstep.plus_one. econstructor. *) +(* assumption. assumption. eassumption. apply valueToPos_posToValue. *) +(* split. lia. *) +(* eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _]. *) +(* split. lia. apply HP. eassumption. eassumption. *) +(* econstructor. econstructor. eapply stmnt_runp_Vcond_false. econstructor. econstructor. *) +(* simpl. unfold find_assocmap. unfold AssocMapExt.get_default. *) +(* rewrite H. trivial. *) + +(* econstructor. simpl. auto. auto. *) + +(* eapply transl_ctrl_correct. *) +(* intros. split. lia. pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _]. auto. *) +(* apply Maps.PTree.elements_keys_norepet. eassumption. *) +(* 2: { apply valueToPos_inj. apply unsigned_posToValue_le. *) +(* eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _]. *) +(* split. lia. apply HP. eassumption. eassumption. *) +(* apply unsigned_posToValue_le. eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. *) +(* destruct HP as [HP _]. *) +(* split. lia. apply HP. eassumption. eassumption. trivial. *) +(* } *) +(* apply Maps.PTree.elements_correct. eassumption. eassumption. *) + +(* econstructor. econstructor. *) + +(* { admit. *) +(* (* *) *) +(* (* eapply transl_list_correct. *) *) +(* (* intros. split. lia. pose proof (HTL.mod_wf m) as HP. destruct HP as [_ HP]. auto. *) *) +(* (* apply Maps.PTree.elements_keys_norepet. eassumption. *) *) +(* (* 2: { apply valueToPos_inj. apply unsigned_posToValue_le. *) *) +(* (* eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _]. *) *) +(* (* split. lia. apply HP. eassumption. eassumption. *) *) +(* (* apply unsigned_posToValue_le. eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. *) *) +(* (* destruct HP as [HP _]. *) *) +(* (* split. lia. apply HP. eassumption. eassumption. trivial. *) *) +(* (* } *) *) +(* (* apply Maps.PTree.elements_correct. eassumption. eassumption. *) *) +(* (* *) *) +(* } *) + +(* apply mis_stepp_decl. trivial. trivial. simpl. eassumption. auto. *) +(* rewrite valueToPos_posToValue. constructor; assumption. lia. *) +(* - econstructor; split. apply Smallstep.plus_one. apply step_finish. assumption. eassumption. *) +(* constructor; assumption. *) +(* - econstructor; split. apply Smallstep.plus_one. constructor. *) + +(* constructor. constructor. *) +(* - inv H3. econstructor; split. apply Smallstep.plus_one. constructor. trivial. *) + +(* apply match_state. assumption. *) +(* Admitted. *) +(* Hint Resolve transl_step_correct : verilogproof. *) + +(* Lemma transl_initial_states : *) +(* forall s1 : Smallstep.state (HTL.semantics prog), *) +(* Smallstep.initial_state (HTL.semantics prog) s1 -> *) +(* exists s2 : Smallstep.state (Verilog.semantics tprog), *) +(* Smallstep.initial_state (Verilog.semantics tprog) s2 /\ match_states s1 s2. *) +(* Proof. *) +(* induction 1. *) +(* econstructor; split. econstructor. *) +(* apply (Genv.init_mem_transf TRANSL); eauto. *) +(* rewrite symbols_preserved. *) +(* replace (AST.prog_main tprog) with (AST.prog_main prog); eauto. *) +(* symmetry; eapply Linking.match_program_main; eauto. *) +(* exploit function_ptr_translated; eauto. intros [tf [A B]]. *) +(* inv B. eauto. *) +(* constructor. *) +(* Qed. *) +(* Hint Resolve transl_initial_states : verilogproof. *) + +(* Lemma transl_final_states : *) +(* forall (s1 : Smallstep.state (HTL.semantics prog)) *) +(* (s2 : Smallstep.state (Verilog.semantics tprog)) *) +(* (r : Integers.Int.int), *) +(* match_states s1 s2 -> *) +(* Smallstep.final_state (HTL.semantics prog) s1 r -> *) +(* Smallstep.final_state (Verilog.semantics tprog) s2 r. *) +(* Proof. *) +(* intros. inv H0. inv H. inv H3. constructor. reflexivity. *) +(* Qed. *) +(* Hint Resolve transl_final_states : verilogproof. *) Theorem transf_program_correct: forward_simulation (HTL.semantics prog) (Verilog.semantics tprog). Proof. - eapply Smallstep.forward_simulation_plus; eauto with verilogproof. - apply senv_preserved. - Qed. + (* eapply Smallstep.forward_simulation_plus; eauto with verilogproof. *) + (* apply senv_preserved. *) + admit. + Admitted. End CORRECTNESS. -*) |