From 39a4348657c2f3efb3feafe9cf65b0f2a1a263c2 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 21 May 2020 23:10:45 +0100 Subject: Finish the proof with most assumptions --- src/translation/HTLgenproof.v | 177 +++++++++++++++++++++++++++++++++++------- 1 file changed, 149 insertions(+), 28 deletions(-) (limited to 'src/translation/HTLgenproof.v') diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index ff7c24d..cb621a8 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -88,6 +88,11 @@ Lemma assumption_32bit : valueToPos (posToValue 32 v) = v. Admitted. +Lemma assumption_32bit_bool : + forall b, + valueToBool (boolToValue 32 b) = b. +Admitted. + Lemma regset_assocmap_get : forall r rs am v v', match_assocmaps rs am -> @@ -110,15 +115,19 @@ Lemma regset_assocmap_wf2 : am!r = Some (intToValue i). Admitted. -Lemma access_merge_assocmap : - forall nb r v am, - nb!r = Some v -> - (merge_assocmap nb am) ! r = Some v. -Admitted. - Lemma st_greater_than_res : forall m res, - (HTL.mod_st m) <> res. + HTL.mod_st m <> res. +Admitted. + +Lemma finish_not_return : + forall m, + HTL.mod_finish m <> HTL.mod_return m. +Admitted. + +Lemma finish_not_res : + forall m r, + HTL.mod_finish m <> r. Admitted. Ltac subst_eq_hyp := @@ -128,6 +137,9 @@ Ltac subst_eq_hyp := rewrite H1 in H2; injection H2; intro H; clear H2; subst end. +Ltac unfold_merge := + try (repeat (rewrite merge_inj)); unfold merge_assocmap; rewrite AssocMapExt.merge_base. + Section CORRECTNESS. Variable prog : RTL.program. @@ -146,6 +158,13 @@ Section CORRECTNESS. Verilog.expr_runp f assoc e (valToValue v). Admitted. + Lemma eval_cond_correct : + forall cond (args : list Registers.reg) s1 c s' i rs args m b f assoc, + Veriloggen.translate_condition cond args s1 = Veriloggen.OK c s' i -> + 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. + (** The proof of semantic preservation for the translation of instructions is a simulation argument based on diagrams of the following form: << @@ -156,7 +175,7 @@ Section CORRECTNESS. || | \/ v code st rs' --------------- State m st assoc' - I + match_states >> where [tr_code c data control fin rtrn st] is assumed to hold. @@ -174,16 +193,17 @@ Section CORRECTNESS. RTL.step ge S1 t S2 -> forall (R1 : HTL.state), match_states S1 R1 -> - exists R2, HTL.step tge R1 t R2 /\ match_states S2 R2. + exists R2, Smallstep.plus HTL.step tge R1 t R2 /\ match_states S2 R2. Proof. - induction 1; intros R1 MSTATE. + induction 1; intros R1 MSTATE; + try (inversion MSTATE; inversion TC; inversion H12; subst_eq_hyp; discriminate). - (* Inop *) inversion MSTATE. subst. econstructor. split. - + apply Smallstep.plus_one. inversion TC. - eapply HTL.step_module; subst_eq_hyp; remember (HTL.mod_st m0) as st; inversion H3; subst. + eapply HTL.step_module; subst_eq_hyp; inversion H3; subst. apply H2. apply H1. (* processing of state *) @@ -205,17 +225,17 @@ Section CORRECTNESS. apply rs. apply regs_lessdef_regs. assumption. - inversion TF. simpl. apply H0. assumption. + inversion TF. simpl. apply H0. unfold state_st_wf. intros. inversion H0. subst. apply AssocMap.gss. - (* Iop *) inversion MSTATE. subst. econstructor. split. - + apply Smallstep.plus_one. inversion TC. - eapply HTL.step_module; subst_eq_hyp; remember (HTL.mod_st m0) as st; inversion H4; subst. + eapply HTL.step_module; subst_eq_hyp; inversion H4; subst. apply H3. apply H2. econstructor. @@ -224,7 +244,8 @@ Section CORRECTNESS. econstructor. simpl. trivial. eapply eval_correct. apply H0. apply H10. trivial. trivial. - apply access_merge_assocmap. rewrite AssocMap.gso. + unfold_merge. + rewrite AssocMap.gso. apply AssocMap.gss. apply st_greater_than_res. trivial. @@ -233,28 +254,128 @@ Section CORRECTNESS. assert (pc' = valueToPos (posToValue 32 pc')). symmetry. apply assumption_32bit. rewrite <- H1. constructor. apply rs0. - rewrite merge_inj. + unfold_merge. apply regs_add_match. - rewrite merge_inj. - unfold merge_assocmap. rewrite AssocMapExt.merge_base. apply regs_lessdef_regs. assumption. apply valToValue_lessdef. - - inversion TF. simpl. apply H2. assumption. + inversion TF. simpl. apply H2. unfold state_st_wf. intros. inversion H2. subst. - rewrite merge_inj. + unfold_merge. rewrite AssocMap.gso. - rewrite merge_inj. apply AssocMap.gss. apply st_greater_than_res. - - inversion MSTATE. inversion TC. subst. - econstructor. constructor. - inversion H12; subst_eq_hyp; discriminate. + - inversion MSTATE; inversion TC; + inversion H12; subst_eq_hyp; inversion H13. + - inversion MSTATE. inversion TC. subst_eq_hyp. inversion H12. subst. + econstructor. split. apply Smallstep.plus_one. + eapply HTL.step_module. subst. apply H11. apply H10. + eapply Verilog.stmnt_runp_Vnonblock with + (rhsval := if b then posToValue 32 ifso else posToValue 32 ifnot). + simpl. trivial. + destruct b. + eapply Verilog.erun_Vternary_true. + eapply eval_cond_correct. apply args. + apply H7. apply H0. + constructor. + apply assumption_32bit_bool. + eapply Verilog.erun_Vternary_false. + eapply eval_cond_correct. apply args. + apply H7. apply H0. + constructor. + apply assumption_32bit_bool. + trivial. + constructor. + trivial. + unfold_merge. + apply AssocMap.gss. + trivial. + + destruct b. + rewrite assumption_32bit. + apply match_state. apply rs0. + unfold_merge. + apply regs_lessdef_regs. assumption. + assumption. + + inversion TF. simpl. apply H1. + + unfold state_st_wf. intros. inversion H1. + subst. unfold_merge. + apply AssocMap.gss. + rewrite assumption_32bit. apply match_state. apply rs0. - apply regs_add_match. apply MASSOC. apply valToValue_lessdef. - inversion TF. rewrite H3. + unfold_merge. + apply regs_lessdef_regs. assumption. + assumption. + + inversion TF. simpl. apply H1. + + unfold state_st_wf. intros. inversion H1. + subst. unfold_merge. + apply AssocMap.gss. + + - (* Return *) + inversion MSTATE. inversion TC. subst_eq_hyp. + inversion H11. subst. + econstructor. split. + eapply Smallstep.plus_two. + + eapply HTL.step_module. + apply H10. + apply H9. + constructor. + econstructor; simpl; trivial. + econstructor; simpl; trivial. + constructor. + econstructor; simpl; trivial. + constructor. + unfold_merge. + trivial. + rewrite AssocMap.gso. + rewrite AssocMap.gso. + unfold state_st_wf in WF. apply WF. trivial. + apply st_greater_than_res. apply st_greater_than_res. trivial. + + apply HTL.step_finish. + rewrite AssocMap.gso. + apply AssocMap.gss. + apply finish_not_return. + apply AssocMap.gss. + rewrite Events.E0_left. trivial. + + constructor. constructor. + destruct (assoc!r) eqn:?. + inversion H11. subst. + econstructor. split. + eapply Smallstep.plus_two. + eapply HTL.step_module. + apply H10. + apply H9. + constructor. + econstructor; simpl; trivial. + econstructor; simpl; trivial. + constructor. + econstructor; simpl; trivial. + apply Verilog.erun_Vvar. + rewrite AssocMap.gso. + apply Heqo. apply not_eq_sym. apply finish_not_res. + unfold_merge. + trivial. + rewrite AssocMap.gso. + rewrite AssocMap.gso. + unfold state_st_wf in WF. apply WF. trivial. + apply st_greater_than_res. apply st_greater_than_res. trivial. + + apply HTL.step_finish. + rewrite AssocMap.gso. + apply AssocMap.gss. + apply finish_not_return. + apply AssocMap.gss. + rewrite Events.E0_left. trivial. + + constructor. simpl. Search Registers.Regmap.get. End CORRECTNESS. -- cgit