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 +++++++++++++++++++++++++++++++++++------- src/translation/HTLgenspec.v | 2 +- src/verilog/AssocMap.v | 17 ++-- 3 files changed, 161 insertions(+), 35 deletions(-) (limited to 'src') 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. diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v index e2d788c..a7d65fc 100644 --- a/src/translation/HTLgenspec.v +++ b/src/translation/HTLgenspec.v @@ -64,7 +64,7 @@ Inductive tr_instr (fin rtrn st : reg) : RTL.instruction -> stmnt -> stmnt -> Pr translate_condition cond args s = OK c s' i -> tr_instr fin rtrn st (RTL.Icond cond args n1 n2) Vskip (state_cond st c n1 n2) | tr_instr_Ireturn_None : - tr_instr fin rtrn st (RTL.Ireturn None) (block fin (Vlit (ZToValue 1%nat 1%Z))) Vskip + tr_instr fin rtrn st (RTL.Ireturn None) (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z))) (block rtrn (Vlit (ZToValue 1%nat 0%Z)))) Vskip | tr_instr_Ireturn_Some : forall r, tr_instr fin rtrn st (RTL.Ireturn (Some r)) diff --git a/src/verilog/AssocMap.v b/src/verilog/AssocMap.v index bd61c8e..9caa2d1 100644 --- a/src/verilog/AssocMap.v +++ b/src/verilog/AssocMap.v @@ -36,12 +36,17 @@ Module AssocMapExt. | Some v => v end. - Definition merge : t elt -> t elt -> t elt := fold (@add elt). - - Lemma merge_add_assoc : - forall am am' r v x, - find x (merge (add r v am) am') = find x (add r v (merge am am')). - Admitted. + Definition merge (m1 m2 : t elt) : t elt := + fold_right (fun el m => match el with (k, v) => add k v m end) m2 (elements m1). + + Lemma merge_add_assoc2 : + forall am am' r v, + merge (add r v am) am' = add r v (merge am am'). + Proof. + intros. + unfold merge. + Search fold_right. + apply SetoidList.fold_right_add2. Lemma merge_base : forall am, -- cgit