Working on proof.

5 files changed, 156 insertions, 47 deletions

diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v
index b573b06..d5a8af2 100644
--- a/src/translation/HTLgen.v
+++ b/src/translation/HTLgen.v
@@ -398,9 +398,9 @@ Lemma create_arr_state_incr:
          (st_controllogic s)).
 Proof. constructor; simpl; auto with htlh. Qed.
 
-Definition create_arr (sz : nat) (ln : nat) : mon reg :=
+Definition create_arr (sz : nat) (ln : nat) : mon (reg * nat) :=
   fun s => let r := s.(st_freshreg) in
-           OK r (mkstate
+           OK (r, ln) (mkstate
                    s.(st_st)
                    (Pos.succ r)
                    (st_freshstate s)
@@ -413,7 +413,7 @@ Definition create_arr (sz : nat) (ln : nat) : mon reg :=
 Definition transf_module (f: function) : mon module :=
   do fin <- create_reg 1;
   do rtrn <- create_reg 32;
-  do stack <- create_arr 32 (Z.to_nat (f.(fn_stacksize) / 4));
+  do (stack, stack_len) <- create_arr 32 (Z.to_nat (f.(fn_stacksize) / 4));
   do _ <- collectlist (transf_instr fin rtrn stack) (Maps.PTree.elements f.(RTL.fn_code));
   do start <- create_reg 1;
   do rst <- create_reg 1;
@@ -426,6 +426,7 @@ Definition transf_module (f: function) : mon module :=
          f.(fn_entrypoint)
          current_state.(st_st)
          stack
+         stack_len
          fin
          rtrn).
 
diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v
index 523c86c..1f9e368 100644
--- a/src/translation/HTLgenproof.v
+++ b/src/translation/HTLgenproof.v
@@ -42,44 +42,45 @@ Definition state_st_wf (m : HTL.module) (s : HTL.state) :=
   asa!(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_arrs (m : HTL.module) : RTL.function -> mem ->  AssocMap.t (list value) -> Prop :=
-| match_arr : forall mem asa stack sp f sz,
-    sz = f.(RTL.fn_stacksize) ->
+Inductive match_arrs (m : HTL.module) (f : RTL.function) (sp : Values.val) (mem : mem) :
+  AssocMap.t (list value) -> Prop :=
+| match_arr : forall asa stack,
+    m.(HTL.mod_stk_len) = Z.to_nat (f.(RTL.fn_stacksize) / 4) ->
     asa ! (m.(HTL.mod_stk)) = Some stack ->
     (forall ptr,
-        0 <= ptr < sz ->
-        nth_error stack (Z.to_nat ptr) =
-        (Coquplib.Option.bind (Mem.loadv AST.Mint32 mem
+        0 <= ptr < Z.of_nat m.(HTL.mod_stk_len) ->
+        opt_val_value_lessdef (Mem.loadv AST.Mint32 mem
                                          (Values.Val.offset_ptr sp (Integers.Ptrofs.repr ptr)))
-         valToValue)) ->
-    match_arrs m f mem asa.
+                              (nth (Z.to_nat ptr) stack (ZToValue 32 0))) ->
+    match_arrs m f sp mem asa.
+
+Inductive match_stacks (mem : mem) : list RTL.stackframe -> list HTL.stackframe -> Prop :=
+| match_stacks_nil :
+    match_stacks mem nil nil
+| match_stacks_cons :
+    forall cs lr r f sp pc rs m asr asa
+           (TF : tr_module f m)
+           (ST: match_stacks mem cs lr)
+           (MA: match_assocmaps f rs asr)
+           (MARR : match_arrs m f sp mem asa),
+      match_stacks mem (RTL.Stackframe r f sp pc rs :: cs)
+                       (HTL.Stackframe r m pc asr asa :: lr).
 
 Inductive match_states : RTL.state -> HTL.state -> Prop :=
 | match_state : forall asa asr sf f sp rs mem m st res
     (MASSOC : match_assocmaps f rs asr)
     (TF : tr_module f m)
     (WF : state_st_wf m (HTL.State res m st asr asa))
-    (MS : match_stacks sf res)
-    (MA : match_arrs m f mem asa),
+    (MS : match_stacks mem sf res)
+    (MARR : match_arrs m f sp mem asa),
     match_states (RTL.State sf f sp st rs mem)
                  (HTL.State res m st asr asa)
 | match_returnstate :
     forall
-      v v' stack m res
-      (MS : match_stacks stack res),
+      v v' stack mem res
+      (MS : match_stacks mem stack res),
       val_value_lessdef v v' ->
-      match_states (RTL.Returnstate stack v m) (HTL.Returnstate res v')
+      match_states (RTL.Returnstate stack v mem) (HTL.Returnstate res v')
 | match_initial_call :
     forall f m m0
     (TF : tr_module f m),
@@ -390,7 +391,73 @@ Section CORRECTNESS.
       (* assumption. *)
       admit.
 
-    - admit.
+      Ltac invert x := inversion x; subst; clear x.
+
+      Ltac clear_obvious :=
+        repeat match goal with
+        | [ H : ex _ |- _ ] => invert H
+        | [ H : Some _ = Some _ |- _ ] => invert H
+        end.
+
+      Ltac simplify := simpl in *; clear_obvious; simpl in *; try discriminate.
+
+      Ltac rt :=
+        repeat match goal with
+        | [ _ : error _ _ = OK _ _ _ |- _ ] => discriminate
+        | [ _ : context[if (?x && ?y) then _ else _] |- _ ] =>
+          let EQ1 := fresh "EQ" in
+          let EQ2 := fresh "EQ" in
+          destruct x eqn:EQ1; destruct y eqn:EQ2; simpl in *
+        | [ _ : context[if ?x then _ else _] |- _ ] =>
+          let EQ := fresh "EQ" in
+          destruct x eqn:EQ; simpl in *
+        | [ H : ret _ _ = _  |- _ ] => invert H
+        | [ _ : context[match ?x with | _ => _ end] |- _ ] => destruct x
+        end.
+
+      Ltac t :=
+        match goal with
+        | [ _ : Mem.loadv _ _ ?a = Some _ |- _ ] =>
+          let PTR := fresh "PTR" in
+          assert (exists b ofs, a = Values.Vptr b ofs) as PTR;
+          [> destruct a; simpl in *; try discriminate;
+          repeat eexists |]
+        | [ H: Values.Vptr _ _ = Values.Vptr _ _ |- _]  => invert H
+        end.
+
+    - destruct c, addr, args; simplify; rt; t; simplify.
+
+      + admit. (* FIXME: Alignment *)
+
+
+      + unfold Op.eval_addressing in *.
+        (* destruct (Archi.ptr64); simplify; *)
+        (*   destruct (Registers.Regmap.get r0 rs); simplify. *)
+        admit.
+
+        (* eexists. split. *)
+        (* eapply Smallstep.plus_one. *)
+        (* eapply HTL.step_module; eauto. *)
+        (* econstructor. econstructor. econstructor. simpl. *)
+        (* econstructor. econstructor. econstructor. econstructor. econstructor. *)
+        (* econstructor. econstructor. econstructor. econstructor. econstructor. *)
+        (* econstructor. econstructor. econstructor. simpl. *)
+
+        (* inversion MARR; subst; clear MARR. simpl in *. *)
+        (* unfold Verilog.arr_assocmap_lookup. *)
+        (* rewrite H3. *)
+
+        (* admit. *)
+
+      + unfold Op.eval_addressing in *.
+        (* destruct (Archi.ptr64); simplify; *)
+        (* destruct (Registers.Regmap.get r0 rs); *)
+        (*   destruct (Registers.Regmap.get r1 rs); simplify; *)
+        (*     destruct (Archi.ptr64); simplify. *)
+        admit.
+
+      + admit.
+
     - admit.
 
     - eexists. split. apply Smallstep.plus_one.
@@ -453,8 +520,7 @@ Section CORRECTNESS.
       econstructor; simpl; trivial.
       constructor.
 
-      constructor.
-      constructor.
+      constructor. constructor.
 
       unfold_merge. simpl.
       rewrite AssocMap.gso.
@@ -470,7 +536,8 @@ Section CORRECTNESS.
       apply AssocMap.gss.
       rewrite Events.E0_left. reflexivity.
       constructor.
-      assumption.
+
+      admit.
       constructor.
 
     - econstructor. split.
@@ -499,21 +566,38 @@ Section CORRECTNESS.
       apply AssocMap.gss.
       rewrite Events.E0_left. trivial.
 
-      constructor. assumption. simpl. inversion MASSOC. subst.
+      constructor.
+      admit.
+
+      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.
+      eapply HTL.step_call. simpl.
 
       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.
 
-      admit.
+      econstructor; simpl.
+      reflexivity.
+      rewrite AssocMap.gss. reflexivity.
+      intros.
+      destruct (Mem.load AST.Mint32 m' stk
+                         (Integers.Ptrofs.unsigned (Integers.Ptrofs.add
+                                                      Integers.Ptrofs.zero
+                                                      (Integers.Ptrofs.repr ptr)))) eqn:LOAD.
+      pose proof Mem.load_alloc_same as LOAD_ALLOC.
+      pose proof H as ALLOC.
+      eapply LOAD_ALLOC in ALLOC.
+      2: { exact LOAD. }
+      rewrite ALLOC.
+      repeat constructor.
+      constructor.
 
     - inversion MSTATE; subst. inversion MS; subst. econstructor.
       split. apply Smallstep.plus_one.
@@ -525,13 +609,11 @@ Section CORRECTNESS.
       unfold state_st_wf. intros. inv H. rewrite AssocMap.gso.
       rewrite AssocMap.gss. trivial. apply st_greater_than_res.
 
-      admit.
-
       Unshelve.
       exact (AssocMap.empty value).
       exact (AssocMap.empty value).
-      admit.
-      admit.
+      exact (AssocMap.empty value).
+      exact (AssocMap.empty value).
       (* exact (ZToValue 32 0). *)
       (* exact (AssocMap.empty value). *)
       (* exact (AssocMap.empty value). *)
diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v
index 4bf3843..89b79ac 100644
--- a/src/translation/HTLgenspec.v
+++ b/src/translation/HTLgenspec.v
@@ -184,14 +184,15 @@ Hint Constructors tr_code : htlspec.
 
 Inductive tr_module (f : RTL.function) : module -> Prop :=
   tr_module_intro :
-    forall data control fin rtrn st stk m,
+    forall data control fin rtrn st stk stk_len m,
       (forall pc i, Maps.PTree.get pc f.(RTL.fn_code) = Some i ->
-                    tr_code f.(RTL.fn_code) pc i data control fin rtrn st stk) ->
+               tr_code f.(RTL.fn_code) pc i data control fin rtrn st stk) ->
+      stk_len = Z.to_nat (f.(RTL.fn_stacksize) / 4) ->
       m = (mkmodule f.(RTL.fn_params)
                         data
                         control
                         f.(RTL.fn_entrypoint)
-                            st stk fin rtrn) ->
+                            st stk stk_len fin rtrn) ->
       tr_module f m.
 Hint Constructors tr_module : htlspec.
 
@@ -379,6 +380,12 @@ Proof.
 Qed.
 Hint Resolve iter_expand_instr_spec : htlspec.
 
+Lemma create_arr_inv : forall x y z a b c d,
+    create_arr x y z = OK (a, b) c d -> y = b.
+Proof.
+  inversion 1. reflexivity.
+Qed.
+
 Theorem transl_module_correct :
   forall f m,
     transl_module f = Errors.OK m -> tr_module f m.
@@ -392,6 +399,11 @@ Proof.
 
   unfold transf_module in *.
   monadInv Heqr.
+
+  (* TODO: We should be able to fold this into the automation. *)
+  pose proof (create_arr_inv _ _ _ _ _ _ _ EQ0) as STK_LEN.
+  rewrite <- STK_LEN.
+
   econstructor; simpl; trivial.
   intros.
   inv_incr.
diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v
index 2e4ef1a..82aac41 100644
--- a/src/verilog/HTL.v
+++ b/src/verilog/HTL.v
@@ -46,6 +46,7 @@ Record module: Type :=
     mod_entrypoint : node;
     mod_st : reg;
     mod_stk : reg;
+    mod_stk_len : nat;
     mod_finish : reg;
     mod_return : reg
   }.
@@ -60,6 +61,14 @@ Fixpoint init_regs (vl : list value) (rl : list reg) {struct rl} :=
   | _, _ => empty_assocmap
   end.
 
+Fixpoint zeroes' (acc : list value) (n : nat) : list value :=
+  match n with
+  | O => acc
+  | S n => zeroes' ((NToValue 32 0)::acc) n
+  end.
+
+Definition zeroes : nat -> list value := zeroes' nil.
+
 (** * Operational Semantics *)
 
 Definition genv := Globalenvs.Genv.t fundef unit.
@@ -69,7 +78,8 @@ Inductive stackframe : Type :=
     forall  (res : reg)
             (m : module)
             (pc : node)
-            (assoc : assocmap),
+            (reg_assoc : assocmap)
+            (arr_assoc : AssocMap.t (list value)),
       stackframe.
 
 Inductive state : Type :=
@@ -125,13 +135,12 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop :=
            (State res m m.(mod_entrypoint)
              (AssocMap.set (mod_st m) (posToValue 32 m.(mod_entrypoint))
                            (init_regs args m.(mod_params)))
-              (AssocMap.empty (list value)))
+              (AssocMap.set m.(mod_stk) (zeroes m.(mod_stk_len)) (AssocMap.empty (list value))))
 | step_return :
-    forall g m asr i r sf pc mst,
+    forall g m asr asa i r sf pc mst,
       mst = mod_st m ->
-      step g (Returnstate (Stackframe r m pc asr :: sf) i) Events.E0
-           (State sf m pc ((asr # mst <- (posToValue 32 pc)) # r <- i)
-                  (AssocMap.empty (list value))).
+      step g (Returnstate (Stackframe r m pc asr asa :: sf) i) Events.E0
+           (State sf m pc ((asr # mst <- (posToValue 32 pc)) # r <- i) asa).
 Hint Constructors step : htl.
 
 Inductive initial_state (p: program): state -> Prop :=
diff --git a/src/verilog/Value.v b/src/verilog/Value.v
index d527b15..b1ee353 100644
--- a/src/verilog/Value.v
+++ b/src/verilog/Value.v
@@ -296,6 +296,11 @@ Inductive val_value_lessdef: val -> value -> Prop :=
     val_value_lessdef (Vint i) v'
 | lessdef_undef: forall v, val_value_lessdef Vundef v.
 
+Inductive opt_val_value_lessdef: option val -> value -> Prop :=
+| opt_lessdef_some:
+    forall v v', val_value_lessdef v v' -> opt_val_value_lessdef (Some v) v'
+| opt_lessdef_none: forall v, opt_val_value_lessdef None v.
+
 Lemma valueToZ_ZToValue :
   forall n z,
   (- Z.of_nat (2 ^ n) <= z < Z.of_nat (2 ^ n))%Z ->