Finish the proof with most assumptions

2 files changed, 150 insertions, 29 deletions

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))