Add proof of translation correctness

Modified-by: Yann Herklotz <git@yannherklotz.com>

2 files changed, 200 insertions, 17 deletions

diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v
index 7a4ec34..ff7c24d 100644
--- a/src/translation/HTLgenproof.v
+++ b/src/translation/HTLgenproof.v
@@ -23,14 +23,22 @@ From compcert Require RTL Registers Globalenvs AST.
 Import AssocMapNotation.
 
 Inductive match_assocmaps : RTL.regset -> assocmap -> Prop :=
-| match_assocmap : forall r rs am,
-    val_value_lessdef (Registers.Regmap.get r rs) am#r ->
+| match_assocmap : forall rs am,
+    (forall r, val_value_lessdef (Registers.Regmap.get r rs) am#r) ->
     match_assocmaps rs am.
 
+Definition state_st_wf (m : HTL.module) (s : HTL.state) :=
+  forall st assoc,
+  s = HTL.State m st assoc ->
+  assoc!(m.(HTL.mod_st)) = Some (posToValue 32 st).
+
 Inductive match_states : RTL.state -> HTL.state -> Prop :=
-| match_state : forall (rs : RTL.regset) assoc sf f sp rs mem m st,
-    match_assocmaps rs assoc ->
-    tr_module f m ->
+| match_state : forall (rs : RTL.regset) assoc sf f sp rs mem m st
+    (MASSOC : match_assocmaps rs assoc)
+    (TF : tr_module f m)
+    (TC : tr_code f.(RTL.fn_code) st m.(HTL.mod_datapath) m.(HTL.mod_controllogic)
+                  m.(HTL.mod_finish) m.(HTL.mod_return) m.(HTL.mod_st))
+    (WF : state_st_wf m (HTL.State m st assoc)),
     match_states (RTL.State sf f sp st rs mem)
                  (HTL.State m st assoc)
 | match_returnstate : forall v v' stack m,
@@ -46,6 +54,80 @@ Inductive match_program : RTL.program -> HTL.module -> Prop :=
     tr_module f m ->
     match_program p m.
 
+Lemma regs_lessdef_regs :
+  forall rs1 rs2 n v,
+    match_assocmaps rs1 rs2 ->
+    match_assocmaps rs1 (AssocMap.add n v rs2).
+Admitted.
+
+Lemma regs_add_match :
+  forall rs am r v v',
+    match_assocmaps rs am ->
+    val_value_lessdef v v' ->
+    match_assocmaps (Registers.Regmap.set r v rs) (AssocMap.add r v' am).
+Admitted.
+
+Lemma merge_inj :
+  forall am am' r v,
+    merge_assocmap (AssocMap.add r v am) am' = AssocMap.add r v (merge_assocmap am am').
+Admitted.
+
+Lemma valToValue_lessdef :
+  forall v,
+    val_value_lessdef v (valToValue v).
+Admitted.
+
+Lemma assocmap_merge_add :
+  forall k v assoc,
+    AssocMap.add k v assoc = merge_assocmap (AssocMap.add k v empty_assocmap) assoc.
+Admitted.
+
+(* Need to eventually move posToValue 32 to posToValueAuto, as that has this proof. *)
+Lemma assumption_32bit :
+  forall v,
+    valueToPos (posToValue 32 v) = v.
+Admitted.
+
+Lemma regset_assocmap_get :
+  forall r rs am v v',
+    match_assocmaps rs am ->
+    v = Registers.Regmap.get r rs ->
+    v' = am#r ->
+    val_value_lessdef v v'.
+Proof. inversion 1. intros. subst. apply H0. Qed.
+
+Lemma regset_assocmap_wf :
+  forall r rs am i,
+    match_assocmaps rs am ->
+    Values.Vint i <> Registers.Regmap.get r rs ->
+    am!r = None.
+Admitted.
+
+Lemma regset_assocmap_wf2 :
+  forall r rs am i,
+    match_assocmaps rs am ->
+    Values.Vint i = Registers.Regmap.get r rs ->
+    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.
+Admitted.
+
+Ltac subst_eq_hyp :=
+  match goal with
+    H1: ?x = Some ?i, H2: ?x = Some ?j |- _ =>
+    let H := fresh "H" in
+    rewrite H1 in H2; injection H2; intro H; clear H2; subst
+  end.
+
 Section CORRECTNESS.
 
   Variable prog : RTL.program.
@@ -56,22 +138,123 @@ Section CORRECTNESS.
   Let ge : RTL.genv := Globalenvs.Genv.globalenv prog.
   Let tge : HTL.genv := HTL.genv_empty.
 
+  Lemma eval_correct :
+    forall sp op rs args m v e assoc f,
+      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 ->
+      Verilog.expr_runp f assoc e (valToValue v).
+  Admitted.
+
   (** The proof of semantic preservation for the translation of instructions
       is a simulation argument based on diagrams of the following form:
 <<
-                    I /\ P
+                      match_states
     code st rs ---------------- State m st assoc
          ||                             |
          ||                             |
          ||                             |
          \/                             v
     code st rs' --------------- State m st assoc'
-                    I /\ Q
+                      I
 >>
       where [tr_code c data control fin rtrn st] is assumed to hold.
+
+      The precondition and postcondition is that that should hold is [match_assocmaps rs assoc].
    *)
 
-  Definition transl_code_prop : Prop :=
-    HTL.step tge (HTL.State)
+  Definition transl_instr_prop (instr : RTL.instruction) : Prop :=
+    forall m assoc fin rtrn st stmt trans,
+      tr_instr fin rtrn st instr stmt trans ->
+      exists assoc',
+        HTL.step tge (HTL.State m st assoc) Events.E0 (HTL.State m st assoc').
+
+  Theorem transl_step_correct:
+    forall (S1 : RTL.state) t S2,
+      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.
+  Proof.
+    induction 1; intros R1 MSTATE.
+    - (* Inop *)
+      inversion MSTATE. subst.
+      econstructor.
+      split.
+
+      inversion TC.
+      eapply HTL.step_module; subst_eq_hyp; remember (HTL.mod_st m0) as st; inversion H3; subst.
+      apply H2.
+      apply H1.
+      (* processing of state *)
+      econstructor.
+      simpl. trivial.
+      econstructor. trivial.
+      inversion H3. subst.
+      econstructor.
+
+      (* prove merge *)
+      apply assocmap_merge_add.
+
+      (* prove stval *)
+      apply AssocMap.gss.
+      apply assumption_32bit.
+
+      (* prove match_state *)
+      constructor.
+      apply rs.
+      apply regs_lessdef_regs.
+      assumption.
+      inversion TF. simpl. apply H0.
+      assumption.
+      unfold state_st_wf. intros. inversion H0. subst.
+      apply AssocMap.gss.
+    - (* Iop *)
+      inversion MSTATE. subst.
+      econstructor.
+      split.
+
+      inversion TC.
+      eapply HTL.step_module; subst_eq_hyp; remember (HTL.mod_st m0) as st; inversion H4; subst.
+      apply H3.
+      apply H2.
+      econstructor.
+      simpl. trivial.
+      constructor. trivial.
+      econstructor.
+      simpl. trivial.
+      eapply eval_correct. apply H0. apply H10. trivial. trivial.
+      apply access_merge_assocmap. rewrite AssocMap.gso.
+      apply AssocMap.gss.
+      apply st_greater_than_res.
+      trivial.
+
+      (* match_states *)
+      assert (pc' = valueToPos (posToValue 32 pc')). symmetry. apply assumption_32bit.
+      rewrite <- H1.
+      constructor. apply rs0.
+      rewrite merge_inj.
+      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.
+
+      unfold state_st_wf. intros. inversion H2. subst.
+      rewrite merge_inj.
+      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.
+      apply match_state. apply rs0.
+      apply regs_add_match. apply MASSOC. apply valToValue_lessdef.
+      inversion TF. rewrite H3.
 
 End CORRECTNESS.
diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v
index fb1c70d..e2d788c 100644
--- a/src/translation/HTLgenspec.v
+++ b/src/translation/HTLgenspec.v
@@ -70,20 +70,20 @@ Inductive tr_instr (fin rtrn st : reg) : RTL.instruction -> stmnt -> stmnt -> Pr
       tr_instr fin rtrn st (RTL.Ireturn (Some r))
                (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z))) (block rtrn (Vvar r))) Vskip.
 
-Inductive tr_code (c : RTL.code) (stmnts trans : PositiveMap.t stmnt)
+Inductive tr_code (c : RTL.code) (pc : RTL.node) (stmnts trans : PositiveMap.t stmnt)
           (fin rtrn st : reg) : Prop :=
   tr_code_intro :
-    forall i s t n,
-      Maps.PTree.get n c = Some i ->
-      stmnts!n = Some s ->
-      trans!n = Some t ->
+    forall i s t,
+      Maps.PTree.get pc c = Some i ->
+      stmnts!pc = Some s ->
+      trans!pc = Some t ->
       tr_instr fin rtrn st i s t ->
-      tr_code c stmnts trans fin rtrn st.
+      tr_code c pc stmnts trans fin rtrn st.
 
 Inductive tr_module (f : RTL.function) : module -> Prop :=
   tr_module_intro :
-    forall c data control fin rtrn st,
-      tr_code c data control fin rtrn st ->
+    forall data control fin rtrn st,
+      (forall pc, tr_code f.(RTL.fn_code) pc data control fin rtrn st) ->
       tr_module f (mkmodule
                      f.(RTL.fn_params)
                      data