Finished main proof with small assumptions

5 files changed, 157 insertions, 59 deletions

diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v
index e719070..204451c 100644
--- a/src/translation/HTLgenproof.v
+++ b/src/translation/HTLgenproof.v
@@ -21,7 +21,7 @@ From compcert Require Import Globalenvs.
 From coqup Require Import Coquplib HTLgenspec HTLgen Value AssocMap.
 From coqup Require HTL Verilog.
 
-Import AssocMapNotation.
+Local Open Scope assocmap.
 
 Hint Resolve Smallstep.forward_simulation_plus : htlproof.
 Hint Resolve AssocMap.gss : htlproof.
@@ -37,25 +37,40 @@ Inductive match_assocmaps : RTL.function -> RTL.regset -> assocmap -> Prop :=
 Hint Constructors match_assocmaps : htlproof.
 
 Definition state_st_wf (m : HTL.module) (s : HTL.state) :=
-  forall st assoc,
-  s = HTL.State m st assoc ->
+  forall st assoc res,
+  s = HTL.State res m st assoc ->
   assoc!(m.(HTL.mod_st)) = Some (posToValue 32 st).
 Hint Unfold state_st_wf : htlproof.
 
+Inductive match_stacks : list RTL.stackframe -> list HTL.stackframe -> Prop :=
+| match_stacks_nil :
+    match_stacks nil nil
+| match_stacks_cons :
+    forall cs lr r f sp pc rs m assoc
+           (TF : tr_module f m)
+           (ST: match_stacks cs lr)
+           (MA: match_assocmaps f rs assoc),
+      match_stacks (RTL.Stackframe r f sp pc rs :: cs)
+                   (HTL.Stackframe r m pc assoc :: lr).
+
 Inductive match_states : RTL.state -> HTL.state -> Prop :=
-| match_state : forall (rs : RTL.regset) assoc sf f sp rs mem m st
+| match_state : forall assoc sf f sp rs mem m st res
     (MASSOC : match_assocmaps f rs assoc)
     (TF : tr_module f m)
-    (WF : state_st_wf m (HTL.State m st assoc)),
+    (WF : state_st_wf m (HTL.State res m st assoc))
+    (MS : match_stacks sf res),
     match_states (RTL.State sf f sp st rs mem)
-                 (HTL.State m st assoc)
-| match_returnstate : forall v v' stack m,
-    val_value_lessdef v v' ->
-    match_states (RTL.Returnstate stack v m) (HTL.Returnstate v')
+                 (HTL.State res m st assoc)
+| match_returnstate :
+    forall
+      v v' stack m res
+      (MS : match_stacks stack res),
+      val_value_lessdef v v' ->
+      match_states (RTL.Returnstate stack v m) (HTL.Returnstate res v')
 | match_initial_call :
-    forall f m m0 st
+    forall f m m0
     (TF : tr_module f m),
-      match_states (RTL.Callstate nil (AST.Internal f) nil m0) (HTL.State m st empty_assocmap).
+      match_states (RTL.Callstate nil (AST.Internal f) nil m0) (HTL.Callstate nil m nil).
 Hint Constructors match_states : htlproof.
 
 Definition match_prog (p: RTL.program) (tp: HTL.program) :=
@@ -156,6 +171,20 @@ Ltac unfold_func H :=
   | ?f _ _ _ _ = _ => unfold f in H; repeat (unfold_match H)
   end.
 
+Lemma init_reg_assoc_empty :
+  forall f l,
+    match_assocmaps f (RTL.init_regs nil l) (HTL.init_regs nil l).
+Proof.
+  induction l; simpl; constructor; intros.
+  - rewrite Registers.Regmap.gi. unfold find_assocmap.
+    unfold AssocMapExt.get_default. rewrite AssocMap.gempty.
+    constructor.
+
+  - rewrite Registers.Regmap.gi. unfold find_assocmap.
+    unfold AssocMapExt.get_default. rewrite AssocMap.gempty.
+    constructor.
+Qed.
+
 Section CORRECTNESS.
 
   Variable prog : RTL.program.
@@ -234,10 +263,10 @@ Section CORRECTNESS.
    *)
 
   Definition transl_instr_prop (instr : RTL.instruction) : Prop :=
-    forall m assoc fin rtrn st stmt trans,
+    forall m assoc fin rtrn st stmt trans res,
       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').
+        HTL.step tge (HTL.State res m st assoc) Events.E0 (HTL.State res m st assoc').
 
   Theorem transl_step_correct:
     forall (S1 : RTL.state) t S2,
@@ -329,7 +358,7 @@ Section CORRECTNESS.
       (* match_states *)
       assert (pc' = valueToPos (posToValue 32 pc')). auto using assumption_32bit.
       rewrite <- H1.
-      constructor. apply rs0.
+      constructor.
       unfold_merge.
       apply regs_lessdef_add_match.
       constructor.
@@ -343,6 +372,7 @@ Section CORRECTNESS.
       rewrite AssocMap.gso.
       apply AssocMap.gss.
       apply st_greater_than_res.
+      assumption.
 
       - econstructor. split. apply Smallstep.plus_one.
       eapply HTL.step_module; eauto.
@@ -367,7 +397,7 @@ Section CORRECTNESS.
 
       destruct b.
       rewrite assumption_32bit.
-      apply match_state. apply rs0.
+      apply match_state.
       unfold_merge.
       apply regs_lessdef_add_greater. apply greater_than_max_func.
       assumption. assumption.
@@ -375,8 +405,9 @@ Section CORRECTNESS.
       unfold state_st_wf. intros. inversion H1.
       subst. unfold_merge.
       apply AssocMap.gss.
+      assumption.
       rewrite assumption_32bit.
-      apply match_state. apply rs0.
+      apply match_state.
       unfold_merge.
       apply regs_lessdef_add_greater. apply greater_than_max_func. assumption.
       assumption.
@@ -384,6 +415,7 @@ Section CORRECTNESS.
       unfold state_st_wf. intros. inversion H1.
       subst. unfold_merge.
       apply AssocMap.gss.
+      assumption.
 
     - (* Return *)
       econstructor. split.
@@ -400,7 +432,7 @@ Section CORRECTNESS.
       trivial.
       rewrite AssocMap.gso.
       rewrite AssocMap.gso.
-      unfold state_st_wf in WF. apply WF. trivial.
+      unfold state_st_wf in WF. eapply WF. trivial.
       apply st_greater_than_res. apply st_greater_than_res. trivial.
 
       apply HTL.step_finish.
@@ -410,10 +442,10 @@ Section CORRECTNESS.
       apply finish_not_return.
       apply AssocMap.gss.
       rewrite Events.E0_left. trivial.
-
-      constructor. constructor.
-    - destruct (assoc!r) eqn:?.
-      inversion H11. subst.
+      constructor.
+      assumption.
+      constructor.
+    - inversion H11. subst.
       econstructor. split.
       eapply Smallstep.plus_two.
       eapply HTL.step_module; eauto.
@@ -422,14 +454,11 @@ Section CORRECTNESS.
       econstructor; simpl; trivial.
       constructor.
       econstructor; simpl; trivial.
-      apply Verilog.erun_Vvar.
-      rewrite AssocMap.gso.
-      apply Heqo. apply not_eq_sym. apply finish_not_res.
+      apply Verilog.erun_Vvar. trivial.
       unfold_merge.
-      trivial.
       rewrite AssocMap.gso.
       rewrite AssocMap.gso.
-      unfold state_st_wf in WF. apply WF. trivial.
+      unfold state_st_wf in WF. eapply WF. trivial.
       apply st_greater_than_res. apply st_greater_than_res. trivial.
 
       apply HTL.step_finish.
@@ -440,8 +469,38 @@ Section CORRECTNESS.
       apply AssocMap.gss.
       rewrite Events.E0_left. trivial.
 
-      constructor. simpl.
-      Admitted.
+      constructor. assumption. simpl. inversion MASSOC. subst.
+      unfold find_assocmap, AssocMapExt.get_default. rewrite AssocMap.gso.
+      apply H1. eapply RTL.max_reg_function_use. eauto. simpl; tauto.
+      apply st_greater_than_res.
+
+    - inversion MSTATE; subst. inversion TF; subst.
+      econstructor. split. apply Smallstep.plus_one.
+      eapply HTL.step_call.
+
+      constructor. apply regs_lessdef_add_greater.
+      apply greater_than_max_func.
+      apply init_reg_assoc_empty. assumption. unfold state_st_wf.
+      intros. inv H1. apply AssocMap.gss. constructor.
+    - inversion MSTATE; subst. inversion MS; subst. econstructor.
+      split. apply Smallstep.plus_one.
+      constructor.
+
+      constructor; auto. constructor; auto. apply regs_lessdef_add_match; auto.
+      apply regs_lessdef_add_greater. apply greater_than_max_func. auto.
+
+      unfold state_st_wf. intros. inv H. rewrite AssocMap.gso.
+      rewrite AssocMap.gss. trivial. apply st_greater_than_res.
+
+      Unshelve.
+      exact (AssocMap.empty value).
+      exact (AssocMap.empty value).
+      exact (ZToValue 32 0).
+      exact (AssocMap.empty value).
+      exact (AssocMap.empty value).
+      exact (AssocMap.empty value).
+      exact (AssocMap.empty value).
+  Qed.
   Hint Resolve transl_step_correct : htlproof.
 
   Lemma transl_initial_states :
@@ -467,12 +526,14 @@ Section CORRECTNESS.
   Hint Resolve transl_initial_states : htlproof.
 
   Lemma transl_final_states :
-    forall (s1 : Smallstep.state (RTL.semantics prog)) (s2 : Smallstep.state (HTL.semantics tprog))
+    forall (s1 : Smallstep.state (RTL.semantics prog))
+           (s2 : Smallstep.state (HTL.semantics tprog))
            (r : Integers.Int.int),
       match_states s1 s2 ->
-      Smallstep.final_state (RTL.semantics prog) s1 r -> Smallstep.final_state (HTL.semantics tprog) s2 r.
+      Smallstep.final_state (RTL.semantics prog) s1 r ->
+      Smallstep.final_state (HTL.semantics tprog) s2 r.
   Proof.
-    intros. inv H0. inv H. inv H4. constructor. trivial.
+    intros. inv H0. inv H. inv H4. inv MS. constructor. trivial.
   Qed.
   Hint Resolve transl_final_states : htlproof.
 
diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v
index ca069c1..afc6f72 100644
--- a/src/translation/HTLgenspec.v
+++ b/src/translation/HTLgenspec.v
@@ -300,15 +300,14 @@ Proof.
     * destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9;
         [ discriminate | apply H9 ].
     * inversion H2. inversion H9. rewrite H. apply tr_instr_Inop.
-      eapply in_map with (f := fst) in H9. contradiction.
+      eapply in_map with (f := fst) in H9; contradiction.
 
     * destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9;
         [ discriminate | apply H9 ].
     * destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9;
         [ discriminate | apply H9 ].
     * inversion H2. inversion H9. unfold nonblock. rewrite <- e2. rewrite H. constructor.
-      eapply translate_instr_tr_op. apply EQ1.
-      eapply in_map with (f := fst) in H9. contradiction.
+      eapply translate_instr_tr_op. apply EQ1. eapply in_map with (f := fst) in H9. contradiction.
 
     * destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9;
         [ discriminate | apply H9 ].
diff --git a/src/verilog/AssocMap.v b/src/verilog/AssocMap.v
index 88b13a6..5d531d5 100644
--- a/src/verilog/AssocMap.v
+++ b/src/verilog/AssocMap.v
@@ -202,9 +202,16 @@ Ltac unfold_merge :=
   unfold merge_assocmap; try (repeat (rewrite merge_add_assoc));
   rewrite AssocMapExt.merge_base_1.
 
-Module AssocMapNotation.
-  Notation "a ! b" := (AssocMap.get b a) (at level 1).
-  Notation "a # ( b , c )" := (find_assocmap c b a) (at level 1).
-  Notation "a # b" := (find_assocmap 32 b a) (at level 1).
-  Notation "a ## b" := (List.map (fun c => find_assocmap 32 c a) b) (at level 1).
-End AssocMapNotation.
+Declare Scope assocmap.
+Notation "a ! b" := (AssocMap.get b a) (at level 1) : assocmap.
+Notation "a # ( b , c )" := (find_assocmap c b a) (at level 1) : assocmap.
+Notation "a # b" := (find_assocmap 32 b a) (at level 1) : assocmap.
+Notation "a ## b" := (List.map (fun c => find_assocmap 32 c a) b) (at level 1) : assocmap.
+Notation "a # b '<-' c" := (AssocMap.set b c a) (at level 1, b at next level) : assocmap.
+
+Local Open Scope assocmap.
+Lemma find_get_assocmap :
+  forall assoc r v,
+  assoc ! r = Some v ->
+  assoc # r = v.
+Proof. intros. unfold find_assocmap, AssocMapExt.get_default. rewrite H. trivial. Qed.
diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v
index bf38b29..82378b3 100644
--- a/src/verilog/HTL.v
+++ b/src/verilog/HTL.v
@@ -30,6 +30,8 @@ hardware-like layout that is still similar to the register transfer language
 instantiations and that we now describe a state machine instead of a
 control-flow graph. *)
 
+Local Open Scope assocmap.
+
 Definition reg := positive.
 Definition node := positive.
 
@@ -51,21 +53,42 @@ Definition fundef := AST.fundef module.
 
 Definition program := AST.program fundef unit.
 
+Fixpoint init_regs (vl : list value) (rl : list reg) {struct rl} :=
+  match rl, vl with
+  | r :: rl', v :: vl' => AssocMap.set r v (init_regs vl' rl')
+  | _, _ => empty_assocmap
+  end.
+
 (** * Operational Semantics *)
 
 Definition genv := Globalenvs.Genv.t fundef unit.
 
+Inductive stackframe : Type :=
+  Stackframe :
+    forall  (res : reg)
+            (m : module)
+            (pc : node)
+            (assoc : assocmap),
+      stackframe.
+
 Inductive state : Type :=
 | State :
-    forall (m : module)
+    forall (stack : list stackframe)
+           (m : module)
            (st : node)
-           (assoc : assocmap),
-  state
-| Returnstate : forall v : value, state.
+           (assoc : assocmap), state
+| Returnstate :
+    forall (res : list stackframe)
+           (v : value), state
+| Callstate :
+    forall (stack : list stackframe)
+           (m : module)
+           (args : list value), state.
 
 Inductive step : genv -> state -> Events.trace -> state -> Prop :=
 | step_module :
-    forall g t m st ctrl data assoc0 assoc1 assoc2 assoc3 nbassoc0 nbassoc1 f stval pstval,
+    forall g m st ctrl data assoc0 assoc1 assoc2
+           assoc3 nbassoc0 nbassoc1 f stval pstval sf,
       m.(mod_controllogic)!st = Some ctrl ->
       m.(mod_datapath)!st = Some data ->
       Verilog.stmnt_runp f
@@ -79,27 +102,38 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop :=
       assoc3 = merge_assocmap nbassoc1 assoc2 ->
       assoc3!(m.(mod_st)) = Some stval ->
       valueToPos stval = pstval ->
-      step g (State m st assoc0) t (State m pstval assoc3)
+      step g (State sf m st assoc0) Events.E0 (State sf m pstval assoc3)
 | step_finish :
-    forall g t m st assoc retval,
+    forall g m st assoc retval sf,
     assoc!(m.(mod_finish)) = Some (1'h"1") ->
     assoc!(m.(mod_return)) = Some retval ->
-    step g (State m st assoc) t (Returnstate retval).
+    step g (State sf m st assoc) Events.E0 (Returnstate sf retval)
+| step_call :
+    forall g m args res,
+      step g (Callstate res m args) Events.E0
+           (State res m m.(mod_entrypoint)
+             (AssocMap.set (mod_st m) (posToValue 32 m.(mod_entrypoint))
+               (init_regs args m.(mod_params))))
+| step_return :
+    forall g m assoc i r sf pc mst,
+      mst = mod_st m ->
+      step g (Returnstate (Stackframe r m pc assoc :: sf) i) Events.E0
+           (State sf m pc ((assoc # mst <- (posToValue 32 pc)) # r <- i)).
 Hint Constructors step : htl.
 
 Inductive initial_state (p: program): state -> Prop :=
-  | initial_state_intro: forall b m0 st m,
+  | initial_state_intro: forall b m0 m,
       let ge := Globalenvs.Genv.globalenv p in
       Globalenvs.Genv.init_mem p = Some m0 ->
       Globalenvs.Genv.find_symbol ge p.(AST.prog_main) = Some b ->
       Globalenvs.Genv.find_funct_ptr ge b = Some (AST.Internal m) ->
-      st = m.(mod_entrypoint) ->
-      initial_state p (State m st empty_assocmap).
+      initial_state p (Callstate nil m nil).
 
 Inductive final_state : state -> Integers.int -> Prop :=
 | final_state_intro : forall retval retvali,
     retvali = valueToInt retval ->
-    final_state (Returnstate retval) retvali.
+    final_state (Returnstate nil retval) retvali.
 
 Definition semantics (m : program) :=
-  Smallstep.Semantics step (initial_state m) final_state (Globalenvs.Genv.globalenv m).
+  Smallstep.Semantics step (initial_state m) final_state
+                      (Globalenvs.Genv.globalenv m).
diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v
index ce7ddd9..cccdf9a 100644
--- a/src/verilog/Verilog.v
+++ b/src/verilog/Verilog.v
@@ -32,7 +32,8 @@ From compcert Require Integers Events.
 From compcert Require Import Errors Smallstep Globalenvs.
 
 Import HexNotationValue.
-Import AssocMapNotation.
+
+Local Open Scope assocmap.
 
 Definition reg : Type := positive.
 Definition node : Type := positive.
@@ -246,12 +247,8 @@ Inductive expr_runp : fext -> assocmap -> expr -> value -> Prop :=
       expr_runp fext assoc (Vlit v) v
   | erun_Vvar :
       forall fext assoc v r,
-      assoc!r = Some v ->
+      assoc#r = v ->
       expr_runp fext assoc (Vvar r) v
-  | erun_Vvar_empty :
-      forall fext assoc r sz,
-      assoc!r = None ->
-      expr_runp fext assoc (Vvar r) (ZToValue sz 0)
   | erun_Vinputvar :
       forall fext assoc r v,
       fext!r = Some v ->