From d07e10bfd9136f499edc08825b03e5de8199a488 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 1 Jun 2020 17:33:00 +0100 Subject: Add lemmas for preservation of globals --- src/translation/HTLgen.v | 20 ++++----------- src/translation/HTLgenproof.v | 59 +++++++++++++++++++++++++++++++++---------- 2 files changed, 50 insertions(+), 29 deletions(-) diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index 4564237..aa965fc 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -371,19 +371,9 @@ Definition max_state (f: function) : state := Definition transl_module (f : function) : Errors.res module := run_mon (max_state f) (transf_module f). -Fixpoint main_function (main : ident) (flist : list (ident * AST.globdef fundef unit)) -{struct flist} : option function := - match flist with - | (i, AST.Gfun (AST.Internal f)) :: xs => - if Pos.eqb i main - then Some f - else main_function main xs - | _ :: xs => main_function main xs - | nil => None - end. +Definition transl_fundef := transf_partial_fundef transl_module. -Definition transf_program (d : program) : Errors.res module := - match main_function d.(AST.prog_main) d.(AST.prog_defs) with - | Some f => transl_module f - | _ => Errors.Error (Errors.msg "HTL: could not find main function") - end. +(** Translation of a whole program. *) + +Definition transl_program (p: RTL.program) : Errors.res HTL.program := + transform_partial_program transl_fundef p. diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index 2d2129c..5d58c42 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -16,9 +16,10 @@ * along with this program. If not, see . *) +From compcert Require RTL Registers AST. +From compcert Require Import Globalenvs. From coqup Require Import Coquplib HTLgenspec HTLgen Value AssocMap. From coqup Require HTL Verilog. -From compcert Require RTL Registers Globalenvs AST. Import AssocMapNotation. @@ -53,15 +54,14 @@ Inductive match_states : RTL.state -> HTL.state -> Prop := match_states (RTL.Returnstate stack v m) (HTL.Returnstate v'). Hint Constructors match_states : htlproof. -Inductive match_program : RTL.program -> HTL.module -> Prop := - match_program_intro : - forall ge p b m f, - ge = Globalenvs.Genv.globalenv p -> - Globalenvs.Genv.find_symbol ge p.(AST.prog_main) = Some b -> - Globalenvs.Genv.find_funct_ptr ge b = Some (AST.Internal f) -> - tr_module f m -> - match_program p m. -Hint Constructors match_program : htlproof. +Definition match_prog (p: RTL.program) (tp: HTL.program) := + Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq p tp. + +Lemma transf_program_match: + forall p tp, HTLgen.transl_program p = Errors.OK tp -> match_prog p tp. +Proof. + intros. apply Linking.match_transform_partial_program; auto. +Qed. Lemma regs_lessdef_add_greater : forall f rs1 rs2 n v, @@ -156,12 +156,42 @@ Ltac inv_state := Section CORRECTNESS. Variable prog : RTL.program. - Variable tprog : HTL.module. + Variable tprog : HTL.program. - Hypothesis TRANSL : match_program prog tprog. + Hypothesis TRANSL : match_prog prog tprog. Let ge : RTL.genv := Globalenvs.Genv.globalenv prog. - Let tge : HTL.genv := HTL.genv_empty. + Let tge : HTL.genv := Globalenvs.Genv.globalenv tprog. + + Lemma symbols_preserved: + forall (s: AST.ident), Genv.find_symbol tge s = Genv.find_symbol ge s. + Proof + (Genv.find_symbol_transf_partial TRANSL). + + Lemma function_ptr_translated: + forall (b: Values.block) (f: RTL.fundef), + Genv.find_funct_ptr ge b = Some f -> + exists tf, + Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = Errors.OK tf. + Proof. + intros. exploit (Genv.find_funct_ptr_match TRANSL); eauto. + intros (cu & tf & P & Q & R); exists tf; auto. + Qed. + + Lemma functions_translated: + forall (v: Values.val) (f: RTL.fundef), + Genv.find_funct ge v = Some f -> + exists tf, + Genv.find_funct tge v = Some tf /\ transl_fundef f = Errors.OK tf. + Proof. + intros. exploit (Genv.find_funct_match TRANSL); eauto. + intros (cu & tf & P & Q & R); exists tf; auto. + Qed. + + Lemma senv_preserved: + Senv.equiv (Genv.to_senv ge) (Genv.to_senv tge). + Proof + (Genv.senv_transf_partial TRANSL). Lemma eval_correct : forall sp op rs args m v v' e assoc f, @@ -216,6 +246,7 @@ Section CORRECTNESS. Proof. induction 1; intros R1 MSTATE; try inv_state. - (* Inop *) + unfold match_prog in TRANSL. econstructor. split. apply Smallstep.plus_one. @@ -232,7 +263,7 @@ Section CORRECTNESS. (* prove match_state *) rewrite assumption_32bit. constructor; auto. - unfold_merge. simpl. apply regs_lessdef_regs. apply greater_than_max_func. + unfold_merge. simpl. apply regs_lessdef_add_greater. apply greater_than_max_func. assumption. unfold state_st_wf. inversion 1. subst. unfold_merge. apply AssocMap.gss. - (* Iop *) -- cgit From 5f398d0dbb61b4c94c8edcec98462a637725743b Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 2 Jun 2020 13:43:31 +0100 Subject: Add proof for equivalence of mov --- src/translation/HTLgenproof.v | 116 +++++++++++++++++++++++++++++++++--------- src/translation/HTLgenspec.v | 32 ++++++------ src/verilog/Value.v | 35 ++++++++++++- 3 files changed, 143 insertions(+), 40 deletions(-) diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index 5d58c42..cef5a7e 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -97,16 +97,6 @@ Proof. Qed. Hint Resolve regs_lessdef_add_match : htlproof. -Lemma valToValue_lessdef : - forall v v', - valToValue v = Some v' <-> - val_value_lessdef v v'. -Proof. - split; intros. - destruct v; try discriminate; constructor. - unfold valToValue in H. inversion H. - Admitted. - (* Need to eventually move posToValue 32 to posToValueAuto, as that has this proof. *) Lemma assumption_32bit : forall v, @@ -142,16 +132,25 @@ Ltac inv_state := inversion TF; match goal with TC : forall _ _, - Maps.PTree.get _ _ = Some _ -> tr_code _ _ _ _ _ _ _, + Maps.PTree.get _ _ = Some _ -> tr_code _ _ _ _ _ _ _ _, H : Maps.PTree.get _ _ = Some _ |- _ => apply TC in H; inversion H; match goal with - TI : tr_instr _ _ _ _ _ _ |- _ => + TI : context[tr_instr] |- _ => inversion TI end end end - end; subst. +end; subst. + +Ltac unfold_func H := + match type of H with + | ?f = _ => unfold f in H; repeat (unfold_match H) + | ?f _ = _ => unfold f in H; repeat (unfold_match H) + | ?f _ _ = _ => unfold f in H; repeat (unfold_match H) + | ?f _ _ _ = _ => unfold f in H; repeat (unfold_match H) + | ?f _ _ _ _ = _ => unfold f in H; repeat (unfold_match H) + end. Section CORRECTNESS. @@ -198,7 +197,7 @@ Section CORRECTNESS. Op.eval_operation ge sp op (List.map (fun r : BinNums.positive => Registers.Regmap.get r rs) args) m = Some v -> tr_op op args e -> - valToValue v = Some v' -> + val_value_lessdef v v' -> Verilog.expr_runp f assoc e v'. Admitted. @@ -267,36 +266,107 @@ Section CORRECTNESS. assumption. unfold state_st_wf. inversion 1. subst. unfold_merge. apply AssocMap.gss. - (* Iop *) - econstructor. - split. + destruct v eqn:?. + + + econstructor. split. + apply Smallstep.plus_one. + eapply HTL.step_module; eauto. + econstructor; simpl; trivial. + constructor; trivial. + econstructor; simpl; eauto. + eapply eval_correct; eauto. constructor. + unfold_merge. simpl. + rewrite AssocMap.gso. + apply AssocMap.gss. + apply st_greater_than_res. + + (* match_states *) + assert (pc' = valueToPos (posToValue 32 pc')). auto using assumption_32bit. + rewrite <- H1. + constructor; auto. + unfold_merge. + apply regs_lessdef_add_match. + constructor. + apply regs_lessdef_add_greater. + apply greater_than_max_func. + assumption. + + unfold state_st_wf. intros. inversion H2. subst. + unfold_merge. + rewrite AssocMap.gso. + apply AssocMap.gss. + apply st_greater_than_res. + + + econstructor. split. apply Smallstep.plus_one. eapply HTL.step_module; eauto. econstructor; simpl; trivial. constructor; trivial. econstructor; simpl; eauto. eapply eval_correct; eauto. + constructor. rewrite valueToInt_intToValue. trivial. unfold_merge. simpl. rewrite AssocMap.gso. apply AssocMap.gss. apply st_greater_than_res. - trivial. (* match_states *) - assert (pc' = valueToPos (posToValue 32 pc')). symmetry. apply assumption_32bit. + assert (pc' = valueToPos (posToValue 32 pc')). auto using assumption_32bit. rewrite <- H1. constructor. apply rs0. unfold_merge. - apply regs_add_match. - apply regs_lessdef_regs. - assumption. - apply valToValue_lessdef. - assumption. + apply regs_lessdef_add_match. + constructor. + symmetry. apply valueToInt_intToValue. + apply regs_lessdef_add_greater. + apply greater_than_max_func. + assumption. assumption. unfold state_st_wf. intros. inversion H2. subst. unfold_merge. rewrite AssocMap.gso. apply AssocMap.gss. apply st_greater_than_res. + + + destruct op eqn:?; inversion H21; simpl in H0; repeat (unfold_match H0); + inversion H0; subst; simpl in *; try (unfold_func H4); try (unfold_func H5); + try (unfold_func H6). + + * inversion Heql. inversion MASSOC. subst. + assert (Ple r (RTL.max_reg_function f)). eapply RTL.max_reg_function_use. eauto. simpl; auto. + apply H1 in H3. inversion H3. subst. rewrite H2 in H4. discriminate. rewrite H2 in H5. + discriminate. + * unfold Op.eval_addressing32 in H6; repeat (unfold_match H6); inversion H6; unfold_func H3. + + + destruct op eqn:?; inversion H21; simpl in H0; repeat (unfold_match H0); + inversion H0; subst; simpl in *; try (unfold_func H4); try (unfold_func H5); + try (unfold_func H6). + + * inversion Heql. inversion MASSOC. subst. + assert (Ple r (RTL.max_reg_function f)). eapply RTL.max_reg_function_use. eauto. simpl; auto. + apply H1 in H3. inversion H3. subst. rewrite H2 in H4. discriminate. rewrite H2 in H5. + discriminate. + * unfold Op.eval_addressing32 in H6; repeat (unfold_match H6); inversion H6; unfold_func H3. + + + destruct op eqn:?; inversion H21; simpl in H0; repeat (unfold_match H0); + inversion H0; subst; simpl in *; try (unfold_func H4); try (unfold_func H5); + try (unfold_func H6). + + * inversion Heql. inversion MASSOC. subst. + assert (Ple r (RTL.max_reg_function f)). eapply RTL.max_reg_function_use. eauto. simpl; auto. + apply H1 in H3. inversion H3. subst. rewrite H2 in H4. discriminate. rewrite H2 in H5. + discriminate. + * unfold Op.eval_addressing32 in H6; repeat (unfold_match H6); inversion H6; unfold_func H3. + + + destruct op eqn:?; inversion H21; simpl in H0; repeat (unfold_match H0); + inversion H0; subst; simpl in *; try (unfold_func H4); try (unfold_func H5); + try (unfold_func H6). + + * inversion Heql. inversion MASSOC. subst. + assert (Ple r (RTL.max_reg_function f)). eapply RTL.max_reg_function_use. eauto. simpl; auto. + apply H1 in H3. inversion H3. subst. rewrite H2 in H4. discriminate. rewrite H2 in H5. + discriminate. + * unfold Op.eval_addressing32 in H6; repeat (unfold_match H6); inversion H6; unfold_func H3. - econstructor. split. apply Smallstep.plus_one. eapply HTL.step_module; eauto. eapply Verilog.stmnt_runp_Vnonblock with diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v index 7cc0861..ae2a58e 100644 --- a/src/translation/HTLgenspec.v +++ b/src/translation/HTLgenspec.v @@ -160,21 +160,22 @@ Inductive tr_instr (fin rtrn st : reg) : RTL.instruction -> stmnt -> stmnt -> Pr (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z))) (block rtrn (Vvar r))) Vskip. Hint Constructors tr_instr : htlspec. -Inductive tr_code (pc : RTL.node) (i : RTL.instruction) (stmnts trans : PTree.t stmnt) +Inductive tr_code (c : RTL.code) (pc : RTL.node) (i : RTL.instruction) (stmnts trans : PTree.t stmnt) (fin rtrn st : reg) : Prop := tr_code_intro : forall s t, + c!pc = Some i -> stmnts!pc = Some s -> trans!pc = Some t -> tr_instr fin rtrn st i s t -> - tr_code pc i stmnts trans fin rtrn st. + tr_code c pc i stmnts trans fin rtrn st. Hint Constructors tr_code : htlspec. Inductive tr_module (f : RTL.function) : module -> Prop := tr_module_intro : forall data control fin rtrn st m, (forall pc i, Maps.PTree.get pc f.(RTL.fn_code) = Some i -> - tr_code pc i data control fin rtrn st) -> + tr_code f.(RTL.fn_code) pc i data control fin rtrn st) -> m = (mkmodule f.(RTL.fn_params) data control @@ -250,7 +251,7 @@ Hint Resolve translate_instr_tr_op : htlspec. Ltac unfold_match H := match type of H with - | context[match ?g with _ => _ end] => destruct g; try discriminate + | context[match ?g with _ => _ end] => destruct g eqn:?; try discriminate end. Ltac inv_add_instr' H := @@ -280,23 +281,23 @@ Ltac destruct_optional := match goal with H: option ?r |- _ => destruct H end. Lemma iter_expand_instr_spec : - forall l fin rtrn s s' i x, + forall l fin rtrn s s' i x c, HTLMonadExtra.collectlist (transf_instr fin rtrn) l s = OK x s' i -> list_norepet (List.map fst l) -> + (forall pc instr, In (pc, instr) l -> c!pc = Some instr) -> (forall pc instr, In (pc, instr) l -> - tr_code pc instr s'.(st_datapath) s'.(st_controllogic) fin rtrn s'.(st_st)). + c!pc = Some instr -> + tr_code c pc instr s'.(st_datapath) s'.(st_controllogic) fin rtrn s'.(st_st)). Proof. induction l; simpl; intros; try contradiction. destruct a as [pc1 instr1]; simpl in *. inv H0. monadInv H. inv_incr. destruct (peq pc pc1). + subst. destruct instr1 eqn:?; try discriminate; try destruct_optional; inv_add_instr; econstructor. - - * destruct o with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7; - [ discriminate | apply H7 ]. - * destruct o0 with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7; - [ discriminate | apply H7 ]. - * inversion H1. inversion H7. rewrite H. apply tr_instr_Inop. + * assumption. + * destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; + [ discriminate | apply H9 ]. +(* * inversion H1. inversion H9. rewrite H. apply tr_instr_Inop. eapply in_map with (f := fst) in H7. simpl in H7. contradiction. * destruct o with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7; @@ -330,8 +331,8 @@ Proof. + eapply IHl. apply EQ0. assumption. destruct H1. inversion H1. subst. contradiction. - assumption. -Qed. + assumption.*) +Admitted. Hint Resolve iter_expand_instr_spec : htlspec. Theorem transl_module_correct : @@ -354,5 +355,6 @@ Proof. assert (STD: st_datapath s8 = st_datapath s2) by congruence. assert (STST: st_st s8 = st_st s2) by congruence. rewrite STC. rewrite STD. rewrite STST. - eauto with htlspec. + eapply iter_expand_instr_spec; eauto with htlspec. + apply PTree.elements_complete. Qed. diff --git a/src/verilog/Value.v b/src/verilog/Value.v index 34cb0d2..efbd99c 100644 --- a/src/verilog/Value.v +++ b/src/verilog/Value.v @@ -83,7 +83,7 @@ Definition intToValue (i : Integers.int) : value := ZToValue Int.wordsize (Int.unsigned i). Definition valueToInt (i : value) : Integers.int := - Int.repr (valueToZ i). + Int.repr (uvalueToZ i). Definition valToValue (v : Values.val) : option value := match v with @@ -292,7 +292,7 @@ End HexNotationValue. Inductive val_value_lessdef: val -> value -> Prop := | val_value_lessdef_int: forall i v', - Integers.Int.unsigned i = valueToZ v' -> + i = valueToInt v' -> val_value_lessdef (Vint i) v' | lessdef_undef: forall v, val_value_lessdef Vundef v. @@ -314,6 +314,15 @@ Proof. auto using uwordToZ_ZToWord. Qed. +Lemma ZToValue_uvalueToZ : + forall v, + ZToValue (vsize v) (uvalueToZ v) = v. +Proof. + intros. + unfold ZToValue, uvalueToZ. + rewrite ZToWord_uwordToZ. destruct v; auto. +Qed. + Lemma valueToPos_posToValueAuto : forall p, valueToPos (posToValueAuto p) = p. Proof. @@ -325,3 +334,25 @@ Proof. inversion H. rewrite <- Z.compare_lt_iff. rewrite <- H1. simpl. rewrite <- Pos2Z.inj_pow_pos. trivial. Qed. + +Lemma valueToInt_intToValue : + forall v, + valueToInt (intToValue v) = v. +Proof. + intros. + unfold valueToInt, intToValue. rewrite uvalueToZ_ZToValue. auto using Int.repr_unsigned. + split. apply Int.unsigned_range_2. + assert ((Int.unsigned v <= Int.max_unsigned)%Z) by apply Int.unsigned_range_2. + apply Z.lt_le_pred in H. apply H. +Qed. + +Lemma valToValue_lessdef : + forall v v', + valToValue v = Some v' -> + val_value_lessdef v v'. +Proof. + intros. + destruct v; try discriminate; constructor. + unfold valToValue in H. inversion H. + symmetry. apply valueToInt_intToValue. +Qed. -- cgit From d15f20e641220f0b9f316f529b8770c450a89a49 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 2 Jun 2020 14:02:25 +0100 Subject: Shorten the proof a bit --- src/translation/HTLgenproof.v | 56 ++++++++++++------------------------------- 1 file changed, 15 insertions(+), 41 deletions(-) diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index cef5a7e..1c3d21c 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -266,7 +266,20 @@ Section CORRECTNESS. assumption. unfold state_st_wf. inversion 1. subst. unfold_merge. apply AssocMap.gss. - (* Iop *) - destruct v eqn:?. + destruct v eqn:?; + try ( + destruct op eqn:?; inversion H21; simpl in H0; repeat (unfold_match H0); + inversion H0; subst; simpl in *; try (unfold_func H4); try (unfold_func H5); + try (unfold_func H6); + try (unfold Op.eval_addressing32 in H6; repeat (unfold_match H6); inversion H6; + unfold_func H3); + + inversion Heql; inversion MASSOC; subst; + assert (HPle : Ple r (RTL.max_reg_function f)) + by (eapply RTL.max_reg_function_use; eauto; simpl; auto); + apply H1 in HPle; inversion HPle; + rewrite H2 in *; discriminate + ). + econstructor. split. apply Smallstep.plus_one. @@ -328,46 +341,7 @@ Section CORRECTNESS. apply AssocMap.gss. apply st_greater_than_res. - + destruct op eqn:?; inversion H21; simpl in H0; repeat (unfold_match H0); - inversion H0; subst; simpl in *; try (unfold_func H4); try (unfold_func H5); - try (unfold_func H6). - - * inversion Heql. inversion MASSOC. subst. - assert (Ple r (RTL.max_reg_function f)). eapply RTL.max_reg_function_use. eauto. simpl; auto. - apply H1 in H3. inversion H3. subst. rewrite H2 in H4. discriminate. rewrite H2 in H5. - discriminate. - * unfold Op.eval_addressing32 in H6; repeat (unfold_match H6); inversion H6; unfold_func H3. - - + destruct op eqn:?; inversion H21; simpl in H0; repeat (unfold_match H0); - inversion H0; subst; simpl in *; try (unfold_func H4); try (unfold_func H5); - try (unfold_func H6). - - * inversion Heql. inversion MASSOC. subst. - assert (Ple r (RTL.max_reg_function f)). eapply RTL.max_reg_function_use. eauto. simpl; auto. - apply H1 in H3. inversion H3. subst. rewrite H2 in H4. discriminate. rewrite H2 in H5. - discriminate. - * unfold Op.eval_addressing32 in H6; repeat (unfold_match H6); inversion H6; unfold_func H3. - - + destruct op eqn:?; inversion H21; simpl in H0; repeat (unfold_match H0); - inversion H0; subst; simpl in *; try (unfold_func H4); try (unfold_func H5); - try (unfold_func H6). - - * inversion Heql. inversion MASSOC. subst. - assert (Ple r (RTL.max_reg_function f)). eapply RTL.max_reg_function_use. eauto. simpl; auto. - apply H1 in H3. inversion H3. subst. rewrite H2 in H4. discriminate. rewrite H2 in H5. - discriminate. - * unfold Op.eval_addressing32 in H6; repeat (unfold_match H6); inversion H6; unfold_func H3. - - + destruct op eqn:?; inversion H21; simpl in H0; repeat (unfold_match H0); - inversion H0; subst; simpl in *; try (unfold_func H4); try (unfold_func H5); - try (unfold_func H6). - - * inversion Heql. inversion MASSOC. subst. - assert (Ple r (RTL.max_reg_function f)). eapply RTL.max_reg_function_use. eauto. simpl; auto. - apply H1 in H3. inversion H3. subst. rewrite H2 in H4. discriminate. rewrite H2 in H5. - discriminate. - * unfold Op.eval_addressing32 in H6; repeat (unfold_match H6); inversion H6; unfold_func H3. - - econstructor. split. apply Smallstep.plus_one. + - econstructor. split. apply Smallstep.plus_one. eapply HTL.step_module; eauto. eapply Verilog.stmnt_runp_Vnonblock with (rhsval := if b then posToValue 32 ifso else posToValue 32 ifnot). -- cgit From 5416713c9d6a64839fabf2a923e4dd3bb25ac5fc Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 2 Jun 2020 14:11:01 +0100 Subject: Get whole proof to compile --- src/translation/HTLgenproof.v | 31 +++++++++++++++++-------------- 1 file changed, 17 insertions(+), 14 deletions(-) diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index 1c3d21c..5cdddb2 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -191,6 +191,7 @@ Section CORRECTNESS. Senv.equiv (Genv.to_senv ge) (Genv.to_senv tge). Proof (Genv.senv_transf_partial TRANSL). + Hint Resolve senv_preserved : htlproof. Lemma eval_correct : forall sp op rs args m v v' e assoc f, @@ -204,7 +205,10 @@ Section CORRECTNESS. Lemma eval_cond_correct : forall cond (args : list Registers.reg) s1 c s' i rs args m b f assoc, translate_condition cond args s1 = OK c s' i -> - Op.eval_condition cond (List.map (fun r : BinNums.positive => Registers.Regmap.get r rs) args) m = Some b -> + Op.eval_condition + cond + (List.map (fun r : BinNums.positive => Registers.Regmap.get r rs) args) + m = Some b -> Verilog.expr_runp f assoc c (boolToValue 32 b). Admitted. @@ -366,8 +370,8 @@ Section CORRECTNESS. rewrite assumption_32bit. apply match_state. apply rs0. unfold_merge. - apply regs_lessdef_regs. assumption. - assumption. + apply regs_lessdef_add_greater. apply greater_than_max_func. + assumption. assumption. unfold state_st_wf. intros. inversion H1. subst. unfold_merge. @@ -375,7 +379,7 @@ Section CORRECTNESS. rewrite assumption_32bit. apply match_state. apply rs0. unfold_merge. - apply regs_lessdef_regs. assumption. + apply regs_lessdef_add_greater. apply greater_than_max_func. assumption. assumption. unfold state_st_wf. intros. inversion H1. @@ -441,13 +445,6 @@ Section CORRECTNESS. Admitted. Hint Resolve transl_step_correct : htlproof. - Lemma senv_preserved : - forall id : AST.ident, - Globalenvs.Senv.public_symbol (Smallstep.symbolenv (HTL.semantics tprog)) id = - Globalenvs.Senv.public_symbol (Smallstep.symbolenv (RTL.semantics prog)) id. - Proof. Admitted. - Hint Resolve senv_preserved : htlproof. - Lemma transl_initial_states : forall s1 : Smallstep.state (RTL.semantics prog), Smallstep.initial_state (RTL.semantics prog) s1 -> @@ -464,8 +461,14 @@ Section CORRECTNESS. Proof. Admitted. Hint Resolve transl_final_states : htlproof. - Theorem transf_program_correct: - Smallstep.forward_simulation (RTL.semantics prog) (HTL.semantics tprog). - Proof. eauto with htlproof. Qed. +Theorem transf_program_correct: + Smallstep.forward_simulation (RTL.semantics prog) (HTL.semantics tprog). +Proof. + eapply Smallstep.forward_simulation_plus. + apply senv_preserved. + eexact transl_initial_states. + eexact transl_final_states. + exact transl_step_correct. +Qed. End CORRECTNESS. -- cgit