From d0257b0a47ad998e01715e9bc6ba612b834765f1 Mon Sep 17 00:00:00 2001
From: James Pollard <james@pollard.dev>
Date: Thu, 11 Jun 2020 14:47:52 +0100
Subject: Working on proof.

---
 src/translation/HTLgen.v      |   7 +-
 src/translation/HTLgenproof.v | 152 ++++++++++++++++++++++++++++++++----------
 src/translation/HTLgenspec.v  |  18 ++++-
 3 files changed, 136 insertions(+), 41 deletions(-)

(limited to 'src/translation')

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.
-- 
cgit 


From 088a554043e3d4b8b8b424dbda9a136e3f4571e5 Mon Sep 17 00:00:00 2001
From: James Pollard <james@pollard.dev>
Date: Thu, 11 Jun 2020 22:50:01 +0100
Subject: Rough outline of stack address proof

---
 src/translation/HTLgen.v      |  12 ++---
 src/translation/HTLgenproof.v | 123 +++++++++++++++++++++++++++++++++---------
 2 files changed, 105 insertions(+), 30 deletions(-)

(limited to 'src/translation')

diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v
index d5a8af2..cba2940 100644
--- a/src/translation/HTLgen.v
+++ b/src/translation/HTLgen.v
@@ -314,21 +314,21 @@ Definition add_branch_instr (e: expr) (n n1 n2: node) : mon unit :=
 
 Definition translate_arr_access (mem : AST.memory_chunk) (addr : Op.addressing)
            (args : list reg) (stack : reg) : mon expr :=
-  match addr, args with (* TODO: We should be more methodical here; what are the possibilities?*)
-  | Op.Aindexed off, r1::nil => ret (Vvari stack (boplitz Vadd r1 off)) (* FIXME: Cannot guarantee alignment *)
-  | Op.Ascaled scale offset, r1::nil =>
+  match mem, addr, args with (* TODO: We should be more methodical here; what are the possibilities?*)
+  | Mint32, Op.Aindexed off, r1::nil => ret (Vvari stack (boplitz Vadd r1 off)) (* FIXME: Cannot guarantee alignment *)
+  | Mint32, Op.Ascaled scale offset, r1::nil =>
     if ((Z.eqb (Z.modulo scale 4) 0) && (Z.eqb (Z.modulo offset 4) 0))
     then ret (Vvari stack (Vbinop Vadd (boplitz Vmul r1 (scale / 4)) (Vlit (ZToValue 32 (offset / 4)))))
     else error (Errors.msg "Veriloggen: translate_arr_access address misaligned")
-  | Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *)
+  | Mint32, Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *)
     if ((Z.eqb (Z.modulo scale 4) 0) && (Z.eqb (Z.modulo offset 4) 0))
     then ret (Vvari stack (Vbinop Vadd (boplitz Vadd r1 (offset / 4)) (boplitz Vmul r2 (scale / 4))))
     else error (Errors.msg "Veriloggen: translate_arr_access address misaligned")
-  | Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *)
+  | Mint32, Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *)
     let a := Integers.Ptrofs.unsigned a in (* FIXME: Assuming stack offsets are +ve; is this ok? *)
     if (Z.eq_dec (Z.modulo a 4) 0) then ret (Vvari stack (Vlit (ZToValue 32 (a / 4))))
     else error (Errors.msg "Veriloggen: eff_addressing misaligned stack offset")
-  | _, _ => error (Errors.msg "Veriloggen: translate_arr_access unsuported addressing")
+  | _, _, _ => error (Errors.msg "Veriloggen: translate_arr_access unsuported addressing")
   end.
 
 Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon unit :=
diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v
index 1f9e368..34fa8ec 100644
--- a/src/translation/HTLgenproof.v
+++ b/src/translation/HTLgenproof.v
@@ -51,7 +51,7 @@ Inductive match_arrs (m : HTL.module) (f : RTL.function) (sp : Values.val) (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)))
-                              (nth (Z.to_nat ptr) stack (ZToValue 32 0))) ->
+                              (nth (Z.to_nat ptr / 4) stack (ZToValue 32 0))) ->
     match_arrs m f sp mem asa.
 
 Inductive match_stacks (mem : mem) : list RTL.stackframe -> list HTL.stackframe -> Prop :=
@@ -425,38 +425,113 @@ Section CORRECTNESS.
         | [ H: Values.Vptr _ _ = Values.Vptr _ _ |- _]  => invert H
         end.
 
-    - destruct c, addr, args; simplify; rt; t; simplify.
+      Opaque Nat.div.
+
+    - destruct c, chunk, addr, args; simplify; rt; simplify.
 
       + admit. (* FIXME: Alignment *)
+      + admit.
+      + admit.
 
+      + invert MARR. simplify.
 
-      + unfold Op.eval_addressing in *.
-        (* destruct (Archi.ptr64); simplify; *)
-        (*   destruct (Registers.Regmap.get r0 rs); simplify. *)
-        admit.
+        unfold Op.eval_addressing in H0.
+        destruct (Archi.ptr64) eqn:ARCHI; simplify.
+        rewrite ARCHI in H0. simplify.
 
-        (* 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. *)
+        (* Out of bounds reads are undefined behaviour. *)
+        assert (forall ptr v, f.(RTL.fn_stacksize) <= ptr ->
+                         Mem.loadv AST.Mint32 m (Values.Val.offset_ptr sp (Integers.Ptrofs.repr ptr)) = Some v ->
+                         v = Values.Vundef) as INVALID_READ by admit.
 
-        (* inversion MARR; subst; clear MARR. simpl in *. *)
-        (* unfold Verilog.arr_assocmap_lookup. *)
-        (* rewrite H3. *)
+        (* Case split on whether read is out of bounds. *)
+        destruct (RTL.fn_stacksize f <=? Integers.Ptrofs.unsigned i0) eqn:BOUND.
+        * assert (RTL.fn_stacksize f <= Integers.Ptrofs.unsigned i0) as OUT_OF_BOUNDS. {
+            apply Zle_bool_imp_le. assumption.
+          }
+          eapply INVALID_READ in OUT_OF_BOUNDS.
+          2: { rewrite Integers.Ptrofs.repr_unsigned. eassumption. }
 
-        (* admit. *)
+          eexists. split.
+          eapply Smallstep.plus_one.
+          eapply HTL.step_module; eauto.
+          econstructor. econstructor. econstructor. simplify.
+          econstructor. econstructor. econstructor. econstructor. simplify.
 
-      + 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.
+          unfold Verilog.arr_assocmap_lookup. rewrite H3.
+          reflexivity.
 
-      + admit.
+          simplify. unfold_merge. apply AssocMap.gss.
+
+          simplify. rewrite assumption_32bit.
+          constructor.
+
+          unfold_merge.
+          apply regs_lessdef_add_greater.
+          apply greater_than_max_func.
+
+          apply regs_lessdef_add_match.
+          rewrite OUT_OF_BOUNDS.
+          constructor. assumption.
+
+          assumption.
+
+          unfold state_st_wf. inversion 1. simplify.
+          unfold_merge. apply AssocMap.gss.
+
+          assumption.
+
+          econstructor; simplify; try reflexivity; eassumption.
+
+        * assert (Integers.Ptrofs.unsigned i0 < f.(RTL.fn_stacksize)) as IN_BOUNDS. {
+            rewrite Z.leb_antisym in BOUND.
+            rewrite negb_false_iff in BOUND.
+            apply Zlt_is_lt_bool. assumption.
+          }
+
+          eexists. split.
+          eapply Smallstep.plus_one.
+          eapply HTL.step_module; eauto.
+          econstructor. econstructor. econstructor. simplify.
+          econstructor. econstructor. econstructor. econstructor. simplify.
+
+          unfold Verilog.arr_assocmap_lookup. rewrite H3.
+          reflexivity.
+
+          simplify. unfold_merge. apply AssocMap.gss.
+
+          simplify. rewrite assumption_32bit.
+          constructor.
+
+          unfold_merge.
+          apply regs_lessdef_add_greater.
+          apply greater_than_max_func.
+
+          apply regs_lessdef_add_match.
+
+          assert (exists ptr, (Z.to_nat ptr / 4)%nat = (valueToNat (ZToValue 32 (Integers.Ptrofs.unsigned i0 / 4))))
+                 by admit.
+          simplify. rewrite <- H5.
+          specialize (H4 x).
+          assert (0 <= x < Z.of_nat (Z.to_nat (RTL.fn_stacksize f / 4))) by admit.
+          apply H4 in H0.
+          invert H0.
+          assert (Integers.Ptrofs.repr x = i0) by admit.
+          rewrite H0 in H6.
+          rewrite H1 in H6.
+          invert H6.
+          assumption.
+
+          assumption.
+
+          assumption.
+
+          unfold state_st_wf. inversion 1. simplify.
+          unfold_merge. apply AssocMap.gss.
+
+          assumption.
+
+          econstructor; simplify; try reflexivity; eassumption.
 
     - admit.
 
-- 
cgit 


From 9acb804500b590edbff66cd802216f58dde169cd Mon Sep 17 00:00:00 2001
From: James Pollard <james@pollard.dev>
Date: Fri, 12 Jun 2020 16:54:28 +0100
Subject: Some work on store proof.

---
 src/translation/HTLgenproof.v | 49 +++++++++++++++++++++++++++++++++----------
 1 file changed, 38 insertions(+), 11 deletions(-)

(limited to 'src/translation')

diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v
index 34fa8ec..6dc4c21 100644
--- a/src/translation/HTLgenproof.v
+++ b/src/translation/HTLgenproof.v
@@ -415,16 +415,6 @@ Section CORRECTNESS.
         | [ _ : 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.
-
       Opaque Nat.div.
 
     - destruct c, chunk, addr, args; simplify; rt; simplify.
@@ -522,6 +512,11 @@ Section CORRECTNESS.
           invert H6.
           assumption.
 
+          assert (Integers.Ptrofs.repr x = i0) by admit.
+          rewrite H0 in H7.
+          rewrite H1 in H7.
+          discriminate.
+
           assumption.
 
           assumption.
@@ -533,7 +528,39 @@ Section CORRECTNESS.
 
           econstructor; simplify; try reflexivity; eassumption.
 
-    - admit.
+    - destruct c, chunk, addr, args; simplify; rt; simplify.
+      + admit.
+      + admit.
+      + admit.
+
+      + eexists. split.
+        eapply Smallstep.plus_one.
+        eapply HTL.step_module; eauto.
+        econstructor. econstructor. econstructor. simplify.
+        eapply Verilog.stmnt_runp_Vblock_arr. simplify.
+        econstructor. econstructor. econstructor. simplify.
+
+        reflexivity.
+
+        unfold_merge. apply AssocMap.gss.
+
+        simplify. rewrite assumption_32bit. econstructor.
+
+        unfold_merge.
+        apply regs_lessdef_add_greater.
+        apply greater_than_max_func.
+        assumption.
+
+        assumption.
+
+        unfold state_st_wf. inversion 1. simplify.
+        unfold_merge. apply AssocMap.gss.
+
+        admit.
+
+        econstructor; simplify; try reflexivity.
+        admit.
+
 
     - eexists. split. apply Smallstep.plus_one.
       eapply HTL.step_module; eauto.
-- 
cgit 


From eacdec2dd13611f94fe12a41cf04cf38dc389092 Mon Sep 17 00:00:00 2001
From: James Pollard <james@pollard.dev>
Date: Fri, 12 Jun 2020 18:13:52 +0100
Subject: Fix broken proof.

---
 src/translation/HTLgenspec.v | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'src/translation')

diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v
index 57d2d87..57d7d62 100644
--- a/src/translation/HTLgenspec.v
+++ b/src/translation/HTLgenspec.v
@@ -433,8 +433,8 @@ 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.
+Lemma create_arr_inv : forall w x y z a b c d,
+    create_arr w x y z = OK (a, b) c d -> y = b.
 Proof.
   inversion 1. reflexivity.
 Qed.
@@ -454,14 +454,14 @@ Proof.
   monadInv Heqr.
 
   (* TODO: We should be able to fold this into the automation. *)
-  pose proof (create_arr_inv _ _ _ _ _ _ _ EQ0) as STK_LEN.
+  pose proof (create_arr_inv _ _ _ _ _ _ _ _ EQ0) as STK_LEN.
   rewrite <- STK_LEN.
 
   econstructor; simpl; trivial.
   intros.
   inv_incr.
   assert (EQ3D := EQ3).
-  destruct x3.
+  destruct x4.
   apply collect_declare_datapath_trans in EQ3.
   apply collect_declare_controllogic_trans in EQ3D.
   assert (STC: st_controllogic s10 = st_controllogic s3) by congruence.
-- 
cgit 


From 044a68b1b215125e2651c637f28c794536d27ba5 Mon Sep 17 00:00:00 2001
From: James Pollard <james@pollard.dev>
Date: Sun, 14 Jun 2020 16:41:27 +0100
Subject: Array semantics now uses dependent Array type.

---
 src/translation/HTLgen.v     | 14 +++++++-------
 src/translation/Veriloggen.v |  5 +++--
 2 files changed, 10 insertions(+), 9 deletions(-)

(limited to 'src/translation')

diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v
index d35a296..1c67fe7 100644
--- a/src/translation/HTLgen.v
+++ b/src/translation/HTLgen.v
@@ -131,7 +131,7 @@ Lemma declare_reg_state_incr :
        s.(st_st)
        s.(st_freshreg)
        s.(st_freshstate)
-       (AssocMap.set r (i, Scalar sz) s.(st_scldecls))
+       (AssocMap.set r (i, VScalar sz) s.(st_scldecls))
        s.(st_arrdecls)
        s.(st_datapath)
        s.(st_controllogic)).
@@ -142,7 +142,7 @@ Definition declare_reg (i : option io) (r : reg) (sz : nat) : mon unit :=
                 s.(st_st)
                 s.(st_freshreg)
                 s.(st_freshstate)
-                (AssocMap.set r (i, Scalar sz) s.(st_scldecls))
+                (AssocMap.set r (i, VScalar sz) s.(st_scldecls))
                 s.(st_arrdecls)
                 s.(st_datapath)
                 s.(st_controllogic))
@@ -393,7 +393,7 @@ Lemma create_reg_state_incr:
          s.(st_st)
          (Pos.succ (st_freshreg s))
          (st_freshstate s)
-         (AssocMap.set s.(st_freshreg) (i, Scalar sz) s.(st_scldecls))
+         (AssocMap.set s.(st_freshreg) (i, VScalar sz) s.(st_scldecls))
          s.(st_arrdecls)
          (st_datapath s)
          (st_controllogic s)).
@@ -405,7 +405,7 @@ Definition create_reg (i : option io) (sz : nat) : mon reg :=
                    s.(st_st)
                    (Pos.succ r)
                    (st_freshstate s)
-                   (AssocMap.set s.(st_freshreg) (i, Scalar sz) s.(st_scldecls))
+                   (AssocMap.set s.(st_freshreg) (i, VScalar sz) s.(st_scldecls))
                    (st_arrdecls s)
                    (st_datapath s)
                    (st_controllogic s))
@@ -418,7 +418,7 @@ Lemma create_arr_state_incr:
          (Pos.succ (st_freshreg s))
          (st_freshstate s)
          s.(st_scldecls)
-         (AssocMap.set s.(st_freshreg) (i, Array sz ln) s.(st_arrdecls))
+         (AssocMap.set s.(st_freshreg) (i, VArray sz ln) s.(st_arrdecls))
          (st_datapath s)
          (st_controllogic s)).
 Proof. constructor; simpl; auto with htlh. Qed.
@@ -430,7 +430,7 @@ Definition create_arr (i : option io) (sz : nat) (ln : nat) : mon (reg * nat) :=
                    (Pos.succ r)
                    (st_freshstate s)
                    s.(st_scldecls)
-                   (AssocMap.set s.(st_freshreg) (i, Array sz ln) s.(st_arrdecls))
+                   (AssocMap.set s.(st_freshreg) (i, VArray sz ln) s.(st_arrdecls))
                    (st_datapath s)
                    (st_controllogic s))
               (create_arr_state_incr s sz ln i).
@@ -466,7 +466,7 @@ Definition max_state (f: function) : state :=
   mkstate st
           (Pos.succ st)
           (Pos.succ (max_pc_function f))
-          (AssocMap.set st (None, Scalar 32) (st_scldecls (init_state st)))
+          (AssocMap.set st (None, VScalar 32) (st_scldecls (init_state st)))
           (st_arrdecls (init_state st))
           (st_datapath (init_state st))
           (st_controllogic (init_state st)).
diff --git a/src/translation/Veriloggen.v b/src/translation/Veriloggen.v
index efe3565..2b9974b 100644
--- a/src/translation/Veriloggen.v
+++ b/src/translation/Veriloggen.v
@@ -29,13 +29,13 @@ Fixpoint transl_list (st : list (node * Verilog.stmnt)) {struct st} : list (expr
 
 Fixpoint scl_to_Vdecl (scldecl : list (reg * (option io * scl_decl))) {struct scldecl} : list module_item :=
   match scldecl with
-  | (r, (io, Scalar sz))::scldecl' => Vdeclaration (Vdecl io r sz) :: scl_to_Vdecl scldecl'
+  | (r, (io, VScalar sz))::scldecl' => Vdeclaration (Vdecl io r sz) :: scl_to_Vdecl scldecl'
   | nil => nil
   end.
 
 Fixpoint arr_to_Vdeclarr (arrdecl : list (reg * (option io * arr_decl))) {struct arrdecl} : list module_item :=
   match arrdecl with
-  | (r, (io, Array sz l))::arrdecl' => Vdeclaration (Vdeclarr io r sz l) :: arr_to_Vdeclarr arrdecl'
+  | (r, (io, VArray sz l))::arrdecl' => Vdeclaration (Vdeclarr io r sz l) :: arr_to_Vdeclarr arrdecl'
   | nil => nil
   end.
 
@@ -56,6 +56,7 @@ Definition transl_module (m : HTL.module) : Verilog.module :=
                    m.(mod_return)
                    m.(mod_st)
                    m.(mod_stk)
+                   m.(mod_stk_len)
                    m.(mod_params)
                    body
                    m.(mod_entrypoint).
-- 
cgit 


From 58f0022a8b5f9ab42e1a8515a77820a9d086ba76 Mon Sep 17 00:00:00 2001
From: James Pollard <james@pollard.dev>
Date: Wed, 17 Jun 2020 20:05:05 +0100
Subject: Use NBAs for loads and stores.

---
 src/translation/HTLgen.v     | 4 ++--
 src/translation/HTLgenspec.v | 4 ++--
 2 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'src/translation')

diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v
index 1c67fe7..73f2b63 100644
--- a/src/translation/HTLgen.v
+++ b/src/translation/HTLgen.v
@@ -366,10 +366,10 @@ Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon uni
     | Iload mem addr args dst n' =>
       do src <- translate_arr_access mem addr args stack;
       do _ <- declare_reg None dst 32;
-      add_instr n n' (block dst src)
+      add_instr n n' (nonblock dst src)
     | Istore mem addr args src n' =>
       do dst <- translate_arr_access mem addr args stack;
-      add_instr n n' (Vblock dst (Vvar src)) (* TODO: Could juse use add_instr? reg exists. *)
+      add_instr n n' (Vnonblock dst (Vvar src)) (* TODO: Could juse use add_instr? reg exists. *)
     | Icall _ _ _ _ _ => error (Errors.msg "Calls are not implemented.")
     | Itailcall _ _ _ => error (Errors.msg "Tailcalls are not implemented.")
     | Ibuiltin _ _ _ _ => error (Errors.msg "Builtin functions not implemented.")
diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v
index 57d7d62..1a9144c 100644
--- a/src/translation/HTLgenspec.v
+++ b/src/translation/HTLgenspec.v
@@ -163,11 +163,11 @@ Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> stmnt -> stmnt -
 | tr_instr_Iload :
     forall mem addr args s s' i c dst n,
       translate_arr_access mem addr args stk s = OK c s' i ->
-      tr_instr fin rtrn st stk (RTL.Iload mem addr args dst n) (block dst c) (state_goto st n)
+      tr_instr fin rtrn st stk (RTL.Iload mem addr args dst n) (nonblock dst c) (state_goto st n)
 | tr_instr_Istore :
     forall mem addr args s s' i c src n,
       translate_arr_access mem addr args stk s = OK c s' i ->
-      tr_instr fin rtrn st stk (RTL.Istore mem addr args src n) (Vblock c (Vvar src))
+      tr_instr fin rtrn st stk (RTL.Istore mem addr args src n) (Vnonblock c (Vvar src))
                (state_goto st n).
 Hint Constructors tr_instr : htlspec.
 
-- 
cgit 


From 00c579e603478d452959dde0ec61672d7b5d27a4 Mon Sep 17 00:00:00 2001
From: James Pollard <james@pollard.dev>
Date: Wed, 17 Jun 2020 23:08:32 +0100
Subject: Some (very) useful lemmas about arrays.

---
 src/translation/HTLgenproof.v | 36 ++++++++++++++++++++++++++++++++----
 1 file changed, 32 insertions(+), 4 deletions(-)

(limited to 'src/translation')

diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v
index 773497b..1356f08 100644
--- a/src/translation/HTLgenproof.v
+++ b/src/translation/HTLgenproof.v
@@ -43,15 +43,16 @@ Definition state_st_wf (m : HTL.module) (s : HTL.state) :=
 Hint Unfold state_st_wf : htlproof.
 
 Inductive match_arrs (m : HTL.module) (f : RTL.function) (sp : Values.val) (mem : mem) :
-  AssocMap.t (list value) -> Prop :=
+  Verilog.assocmap_arr -> 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 ->
+    asa ! (m.(HTL.mod_stk)) = Some stack /\
+    stack.(arr_length) = Z.to_nat (f.(RTL.fn_stacksize) / 4) /\
     (forall ptr,
         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)))
-                              (nth (Z.to_nat ptr / 4) stack (ZToValue 32 0))) ->
+                              (Option.default (NToValue 32 0)
+                                 (Option.join (array_get_error (Z.to_nat ptr / 4) stack)))) ->
     match_arrs m f sp mem asa.
 
 Inductive match_stacks (mem : mem) : list RTL.stackframe -> list HTL.stackframe -> Prop :=
@@ -130,6 +131,33 @@ Proof.
 Qed.
 Hint Resolve regs_lessdef_add_match : htlproof.
 
+Lemma list_combine_none :
+  forall n l,
+    length l = n ->
+    list_combine Verilog.merge_cell (list_repeat None n) l = l.
+Proof.
+  induction n; intros; simplify.
+  - symmetry. apply length_zero_iff_nil. auto.
+  - destruct l; simplify.
+    rewrite list_repeat_cons.
+    simplify. f_equal.
+    eauto.
+Qed.
+
+Lemma combine_none :
+  forall n a,
+    a.(arr_length) = n ->
+    arr_contents (combine Verilog.merge_cell (arr_repeat None n) a) = arr_contents a.
+Proof.
+  intros.
+  unfold combine.
+  simplify.
+
+  rewrite <- (arr_wf a) in H.
+  apply list_combine_none.
+  assumption.
+Qed.
+
 (* Need to eventually move posToValue 32 to posToValueAuto, as that has this proof. *)
 Lemma assumption_32bit :
   forall v,
-- 
cgit 


From 9a65ca2731adf234f5ce946503314267ced62a44 Mon Sep 17 00:00:00 2001
From: James Pollard <james@pollard.dev>
Date: Wed, 17 Jun 2020 23:19:48 +0100
Subject: Fix Inop proof to work with new array semantics.

---
 src/translation/HTLgenproof.v | 43 ++++++++++++++++++++++++++++++++++++-------
 1 file changed, 36 insertions(+), 7 deletions(-)

(limited to 'src/translation')

diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v
index 1356f08..80d936f 100644
--- a/src/translation/HTLgenproof.v
+++ b/src/translation/HTLgenproof.v
@@ -18,7 +18,7 @@
 
 From compcert Require RTL Registers AST Integers.
 From compcert Require Import Globalenvs Memory.
-From coqup Require Import Coquplib HTLgenspec HTLgen Value AssocMap.
+From coqup Require Import Coquplib HTLgenspec HTLgen Value AssocMap Array.
 From coqup Require HTL Verilog.
 
 Local Open Scope assocmap.
@@ -326,21 +326,51 @@ Section CORRECTNESS.
       eapply HTL.step_module; eauto.
       (* processing of state *)
       econstructor.
-      simpl. trivial.
+      simplify.
       econstructor.
       econstructor.
       econstructor.
+      simplify.
 
-      (* prove stval *)
-      unfold merge_assocmap.
-      unfold_merge. simpl. apply AssocMap.gss.
+      unfold Verilog.merge_regs.
+      unfold_merge. apply AssocMap.gss.
 
       (* prove match_state *)
       rewrite assumption_32bit.
-      constructor; auto.
+      constructor; auto; simplify.
+
+      unfold Verilog.merge_regs.
       unfold_merge. simpl. apply regs_lessdef_add_greater. apply greater_than_max_func.
       assumption.
+      unfold Verilog.merge_regs.
       unfold state_st_wf. inversion 1. subst. unfold_merge. apply AssocMap.gss.
+
+      (* prove match_arrs *)
+      invert MARR. simplify.
+      unfold HTL.empty_stack. simplify. unfold Verilog.merge_arrs.
+      econstructor.
+      simplify. repeat split.
+
+      rewrite AssocMap.gcombine.
+      2: { reflexivity. }
+      rewrite AssocMap.gss.
+      unfold Verilog.merge_arr.
+      setoid_rewrite H1.
+      reflexivity.
+
+      rewrite combine_length.
+      unfold arr_repeat. simplify.
+      rewrite list_repeat_len.
+      reflexivity.
+
+      unfold arr_repeat. simplify.
+      rewrite list_repeat_len; auto.
+      intros.
+      erewrite array_get_error_equal.
+      eauto. apply combine_none.
+
+      assumption.
+
     - (* Iop *)
       (* destruct v eqn:?; *)
       (*          try ( *)
@@ -443,7 +473,6 @@ Section CORRECTNESS.
         | [ _ : context[match ?x with | _ => _ end] |- _ ] => destruct x
         end.
 
-      Opaque Nat.div.
 
     - destruct c, chunk, addr, args; simplify; rt; simplify.
 
-- 
cgit 


From 39c336a3e507b9264cd80d1721b724dc5606de6d Mon Sep 17 00:00:00 2001
From: James Pollard <james@pollard.dev>
Date: Thu, 18 Jun 2020 00:47:29 +0100
Subject: Fix up ILoad proof.

---
 src/translation/HTLgenproof.v | 153 ++++++++++++++++--------------------------
 1 file changed, 58 insertions(+), 95 deletions(-)

(limited to 'src/translation')

diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v
index 80d936f..8a246f3 100644
--- a/src/translation/HTLgenproof.v
+++ b/src/translation/HTLgenproof.v
@@ -21,6 +21,8 @@ From compcert Require Import Globalenvs Memory.
 From coqup Require Import Coquplib HTLgenspec HTLgen Value AssocMap Array.
 From coqup Require HTL Verilog.
 
+Require Import Lia.
+
 Local Open Scope assocmap.
 
 Hint Resolve Smallstep.forward_simulation_plus : htlproof.
@@ -449,16 +451,6 @@ Section CORRECTNESS.
       (* assumption. *)
       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
@@ -473,8 +465,8 @@ Section CORRECTNESS.
         | [ _ : context[match ?x with | _ => _ end] |- _ ] => destruct x
         end.
 
-
-    - destruct c, chunk, addr, args; simplify; rt; simplify.
+    - (* FIXME: Should be able to use the spec to avoid destructing here. *)
+      destruct c, chunk, addr, args; simplify; rt; simplify.
 
       + admit. (* FIXME: Alignment *)
       + admit.
@@ -486,104 +478,75 @@ Section CORRECTNESS.
         destruct (Archi.ptr64) eqn:ARCHI; simplify.
         rewrite ARCHI in H0. simplify.
 
-        (* Out of bounds reads are undefined behaviour. *)
-        assert (forall ptr v, f.(RTL.fn_stacksize) <= ptr ->
-                         Mem.loadv AST.Mint32 m (Values.Val.offset_ptr sp (Integers.Ptrofs.repr ptr)) = Some v ->
-                         v = Values.Vundef) as INVALID_READ by admit.
-
-        (* Case split on whether read is out of bounds. *)
-        destruct (RTL.fn_stacksize f <=? Integers.Ptrofs.unsigned i0) eqn:BOUND.
-        * assert (RTL.fn_stacksize f <= Integers.Ptrofs.unsigned i0) as OUT_OF_BOUNDS. {
-            apply Zle_bool_imp_le. assumption.
-          }
-          eapply INVALID_READ in OUT_OF_BOUNDS.
-          2: { rewrite Integers.Ptrofs.repr_unsigned. eassumption. }
-
-          eexists. split.
-          eapply Smallstep.plus_one.
-          eapply HTL.step_module; eauto.
-          econstructor. econstructor. econstructor. simplify.
-          econstructor. econstructor. econstructor. econstructor. simplify.
-
-          unfold Verilog.arr_assocmap_lookup. rewrite H3.
-          reflexivity.
-
-          simplify. unfold_merge. apply AssocMap.gss.
-
-          simplify. rewrite assumption_32bit.
-          constructor.
-
-          unfold_merge.
-          apply regs_lessdef_add_greater.
-          apply greater_than_max_func.
-
-          apply regs_lessdef_add_match.
-          rewrite OUT_OF_BOUNDS.
-          constructor. assumption.
 
-          assumption.
+        (** Here we are assuming that any stack read will be within the bounds
+            of the activation record. *)
+        assert (0 <= Integers.Ptrofs.unsigned i0) as READ_BOUND_LOW by admit.
+        assert (Integers.Ptrofs.unsigned i0 < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH by admit.
 
-          unfold state_st_wf. inversion 1. simplify.
-          unfold_merge. apply AssocMap.gss.
-
-          assumption.
-
-          econstructor; simplify; try reflexivity; eassumption.
-
-        * assert (Integers.Ptrofs.unsigned i0 < f.(RTL.fn_stacksize)) as IN_BOUNDS. {
-            rewrite Z.leb_antisym in BOUND.
-            rewrite negb_false_iff in BOUND.
-            apply Zlt_is_lt_bool. assumption.
-          }
+        eexists. split.
+        eapply Smallstep.plus_one.
+        eapply HTL.step_module; eauto.
+        econstructor. econstructor. econstructor. simplify.
+        econstructor. econstructor. econstructor. econstructor. simplify.
 
-          eexists. split.
-          eapply Smallstep.plus_one.
-          eapply HTL.step_module; eauto.
-          econstructor. econstructor. econstructor. simplify.
-          econstructor. econstructor. econstructor. econstructor. simplify.
+        unfold Verilog.arr_assocmap_lookup. setoid_rewrite H3.
+        f_equal.
 
-          unfold Verilog.arr_assocmap_lookup. rewrite H3.
-          reflexivity.
+        simplify. unfold Verilog.merge_regs.
+        unfold_merge.
+        rewrite AssocMap.gso.
+        apply AssocMap.gss.
+        apply st_greater_than_res.
 
-          simplify. unfold_merge. apply AssocMap.gss.
+        simplify. rewrite assumption_32bit.
+        constructor.
 
-          simplify. rewrite assumption_32bit.
-          constructor.
+        unfold Verilog.merge_regs. unfold_merge.
+        apply regs_lessdef_add_match.
 
-          unfold_merge.
-          apply regs_lessdef_add_greater.
-          apply greater_than_max_func.
+        (** Equality proof *)
+        admit.
 
-          apply regs_lessdef_add_match.
+        apply regs_lessdef_add_greater.
+        apply greater_than_max_func.
+        assumption. assumption.
 
-          assert (exists ptr, (Z.to_nat ptr / 4)%nat = (valueToNat (ZToValue 32 (Integers.Ptrofs.unsigned i0 / 4))))
-                 by admit.
-          simplify. rewrite <- H5.
-          specialize (H4 x).
-          assert (0 <= x < Z.of_nat (Z.to_nat (RTL.fn_stacksize f / 4))) by admit.
-          apply H4 in H0.
-          invert H0.
-          assert (Integers.Ptrofs.repr x = i0) by admit.
-          rewrite H0 in H6.
-          rewrite H1 in H6.
-          invert H6.
-          assumption.
+        unfold state_st_wf. inversion 1. simplify.
+        unfold Verilog.merge_regs.
+        unfold_merge. rewrite AssocMap.gso.
+        apply AssocMap.gss.
+        apply st_greater_than_res.
 
-          assert (Integers.Ptrofs.repr x = i0) by admit.
-          rewrite H0 in H7.
-          rewrite H1 in H7.
-          discriminate.
+        assumption.
 
-          assumption.
+        econstructor.
+        repeat split; simplify.
+        unfold HTL.empty_stack.
+        simplify.
+        unfold Verilog.merge_arrs.
+
+        rewrite AssocMap.gcombine.
+        2: { reflexivity. }
+        rewrite AssocMap.gss.
+        unfold Verilog.merge_arr.
+        setoid_rewrite H3.
+        reflexivity.
 
-          assumption.
+        rewrite combine_length.
+        unfold arr_repeat. simplify.
+        rewrite list_repeat_len.
+        reflexivity.
 
-          unfold state_st_wf. inversion 1. simplify.
-          unfold_merge. apply AssocMap.gss.
+        unfold arr_repeat. simplify.
+        rewrite list_repeat_len.
+        congruence.
 
-          assumption.
+        intros.
+        erewrite array_get_error_equal.
+        eauto. apply combine_none.
 
-          econstructor; simplify; try reflexivity; eassumption.
+        assumption.
 
     - destruct c, chunk, addr, args; simplify; rt; simplify.
       + admit.
-- 
cgit 


From f5172e5c66ab7175d5e90acee69e88ac214f4b0f Mon Sep 17 00:00:00 2001
From: James Pollard <james@pollard.dev>
Date: Thu, 18 Jun 2020 01:34:49 +0100
Subject: Finish AInStack proof with minor assertions.

---
 src/translation/HTLgenproof.v | 53 +++++++++++++++++--------------------------
 1 file changed, 21 insertions(+), 32 deletions(-)

(limited to 'src/translation')

diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v
index 8a246f3..f37fc8d 100644
--- a/src/translation/HTLgenproof.v
+++ b/src/translation/HTLgenproof.v
@@ -52,9 +52,9 @@ Inductive match_arrs (m : HTL.module) (f : RTL.function) (sp : Values.val) (mem
     (forall ptr,
         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)))
+                                         (Values.Val.offset_ptr sp (Integers.Ptrofs.repr (4 * ptr))))
                               (Option.default (NToValue 32 0)
-                                 (Option.join (array_get_error (Z.to_nat ptr / 4) stack)))) ->
+                                 (Option.join (array_get_error (Z.to_nat ptr) stack)))) ->
     match_arrs m f sp mem asa.
 
 Inductive match_stacks (mem : mem) : list RTL.stackframe -> list HTL.stackframe -> Prop :=
@@ -465,6 +465,8 @@ Section CORRECTNESS.
         | [ _ : context[match ?x with | _ => _ end] |- _ ] => destruct x
         end.
 
+      Opaque Z.mul.
+
     - (* FIXME: Should be able to use the spec to avoid destructing here. *)
       destruct c, chunk, addr, args; simplify; rt; simplify.
 
@@ -478,7 +480,6 @@ Section CORRECTNESS.
         destruct (Archi.ptr64) eqn:ARCHI; simplify.
         rewrite ARCHI in H0. simplify.
 
-
         (** Here we are assuming that any stack read will be within the bounds
             of the activation record. *)
         assert (0 <= Integers.Ptrofs.unsigned i0) as READ_BOUND_LOW by admit.
@@ -506,7 +507,18 @@ Section CORRECTNESS.
         apply regs_lessdef_add_match.
 
         (** Equality proof *)
-        admit.
+        assert (forall x, valueToNat (ZToValue 32 x) = Z.to_nat x) by admit. (* FIXME: 32-bit issue. *)
+        (* Modular arithmetic facts. *)
+        assert (0 <= Integers.Ptrofs.unsigned i0 / 4 < RTL.fn_stacksize f / 4) by admit.
+        assert (4 * (Integers.Ptrofs.unsigned i0 / 4) = Integers.Ptrofs.unsigned i0) by admit.
+        rewrite H0.
+        specialize (H5 (Integers.Ptrofs.unsigned i0 / 4)).
+        rewrite Z2Nat.id in H5; try lia.
+        apply H5 in H4.
+        rewrite H6 in H4.
+        rewrite Integers.Ptrofs.repr_unsigned in H4.
+        rewrite H1 in H4.
+        invert H4. assumption.
 
         apply regs_lessdef_add_greater.
         apply greater_than_max_func.
@@ -553,34 +565,11 @@ Section CORRECTNESS.
       + admit.
       + admit.
 
-      + eexists. split.
-        eapply Smallstep.plus_one.
-        eapply HTL.step_module; eauto.
-        econstructor. econstructor. econstructor. simplify.
-        eapply Verilog.stmnt_runp_Vblock_arr. simplify.
-        econstructor. econstructor. econstructor. simplify.
-
-        reflexivity.
-
-        unfold_merge. apply AssocMap.gss.
-
-        simplify. rewrite assumption_32bit. econstructor.
-
-        unfold_merge.
-        apply regs_lessdef_add_greater.
-        apply greater_than_max_func.
-        assumption.
-
-        assumption.
-
-        unfold state_st_wf. inversion 1. simplify.
-        unfold_merge. apply AssocMap.gss.
-
-        admit.
-
-        econstructor; simplify; try reflexivity.
-        admit.
-
+      (* + eexists. split. *)
+      (*   eapply Smallstep.plus_one. *)
+      (*   eapply HTL.step_module; eauto. *)
+      (*   econstructor. econstructor. econstructor. simplify. *)
+      + admit.
 
     - eexists. split. apply Smallstep.plus_one.
       eapply HTL.step_module; eauto.
-- 
cgit 


From 6b20fbbeaad23724ca7fbcc10c9445f5cb94b699 Mon Sep 17 00:00:00 2001
From: James Pollard <james@pollard.dev>
Date: Thu, 18 Jun 2020 17:12:20 +0100
Subject: Tidy up proof.

---
 src/translation/HTLgenproof.v | 27 +++++++++++++++------------
 1 file changed, 15 insertions(+), 12 deletions(-)

(limited to 'src/translation')

diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v
index f37fc8d..a5396af 100644
--- a/src/translation/HTLgenproof.v
+++ b/src/translation/HTLgenproof.v
@@ -482,8 +482,8 @@ Section CORRECTNESS.
 
         (** Here we are assuming that any stack read will be within the bounds
             of the activation record. *)
-        assert (0 <= Integers.Ptrofs.unsigned i0) as READ_BOUND_LOW by admit.
-        assert (Integers.Ptrofs.unsigned i0 < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH by admit.
+        assert (0 <= Integers.Ptrofs.unsigned i0 / 4) as READ_BOUND_LOW by admit.
+        assert (Integers.Ptrofs.unsigned i0 / 4 < f.(RTL.fn_stacksize) / 4) as READ_BOUND_HIGH by admit.
 
         eexists. split.
         eapply Smallstep.plus_one.
@@ -507,18 +507,21 @@ Section CORRECTNESS.
         apply regs_lessdef_add_match.
 
         (** Equality proof *)
-        assert (forall x, valueToNat (ZToValue 32 x) = Z.to_nat x) by admit. (* FIXME: 32-bit issue. *)
-        (* Modular arithmetic facts. *)
-        assert (0 <= Integers.Ptrofs.unsigned i0 / 4 < RTL.fn_stacksize f / 4) by admit.
-        assert (4 * (Integers.Ptrofs.unsigned i0 / 4) = Integers.Ptrofs.unsigned i0) by admit.
-        rewrite H0.
+        (* FIXME: 32-bit issue. *)
+        assert (forall x, valueToNat (ZToValue 32 x) = Z.to_nat x) as VALUE_IDENTITY by admit.
+        assert (4 * (Integers.Ptrofs.unsigned i0 / 4) = Integers.Ptrofs.unsigned i0) as MOD_IDENTITY.
+        {
+          rewrite Z.mul_comm.
+          rewrite ZLib.div_mul_undo; lia.
+        }
+        rewrite VALUE_IDENTITY.
         specialize (H5 (Integers.Ptrofs.unsigned i0 / 4)).
         rewrite Z2Nat.id in H5; try lia.
-        apply H5 in H4.
-        rewrite H6 in H4.
-        rewrite Integers.Ptrofs.repr_unsigned in H4.
-        rewrite H1 in H4.
-        invert H4. assumption.
+        exploit H5; auto; intros.
+        rewrite MOD_IDENTITY in H0.
+        rewrite Integers.Ptrofs.repr_unsigned in H0.
+        rewrite H1 in H0.
+        invert H0. assumption.
 
         apply regs_lessdef_add_greater.
         apply greater_than_max_func.
-- 
cgit 


From b59a2e2913aa7ad010c0652e909ae790c07c7281 Mon Sep 17 00:00:00 2001
From: James Pollard <james@pollard.dev>
Date: Thu, 18 Jun 2020 17:47:21 +0100
Subject: Enforce stack size alignment to fix proof.

---
 src/translation/HTLgen.v      |  4 +++-
 src/translation/HTLgenproof.v | 25 +++++++++++++++++--------
 src/translation/HTLgenspec.v  |  3 ++-
 3 files changed, 22 insertions(+), 10 deletions(-)

(limited to 'src/translation')

diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v
index 73f2b63..f661aa6 100644
--- a/src/translation/HTLgen.v
+++ b/src/translation/HTLgen.v
@@ -436,6 +436,7 @@ Definition create_arr (i : option io) (sz : nat) (ln : nat) : mon (reg * nat) :=
               (create_arr_state_incr s sz ln i).
 
 Definition transf_module (f: function) : mon module :=
+  if (Z.eq_dec (Z.modulo f.(fn_stacksize) 4) 0) then
   do fin <- create_reg (Some Voutput) 1;
   do rtrn <- create_reg (Some Voutput) 32;
   do (stack, stack_len) <- create_arr None 32 (Z.to_nat (f.(fn_stacksize) / 4));
@@ -459,7 +460,8 @@ Definition transf_module (f: function) : mon module :=
          rst
          clk
          current_state.(st_scldecls)
-         current_state.(st_arrdecls)).
+         current_state.(st_arrdecls))
+  else error (Errors.msg "Stack size misalignment.").
 
 Definition max_state (f: function) : state :=
   let st := Pos.succ (max_reg_function f) in
diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v
index a5396af..77a11dc 100644
--- a/src/translation/HTLgenproof.v
+++ b/src/translation/HTLgenproof.v
@@ -482,8 +482,8 @@ Section CORRECTNESS.
 
         (** Here we are assuming that any stack read will be within the bounds
             of the activation record. *)
-        assert (0 <= Integers.Ptrofs.unsigned i0 / 4) as READ_BOUND_LOW by admit.
-        assert (Integers.Ptrofs.unsigned i0 / 4 < f.(RTL.fn_stacksize) / 4) as READ_BOUND_HIGH by admit.
+        assert (0 <= Integers.Ptrofs.unsigned i0) as READ_BOUND_LOW by admit.
+        assert (Integers.Ptrofs.unsigned i0 < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH by admit.
 
         eexists. split.
         eapply Smallstep.plus_one.
@@ -509,16 +509,25 @@ Section CORRECTNESS.
         (** Equality proof *)
         (* FIXME: 32-bit issue. *)
         assert (forall x, valueToNat (ZToValue 32 x) = Z.to_nat x) as VALUE_IDENTITY by admit.
-        assert (4 * (Integers.Ptrofs.unsigned i0 / 4) = Integers.Ptrofs.unsigned i0) as MOD_IDENTITY.
-        {
-          rewrite Z.mul_comm.
-          rewrite ZLib.div_mul_undo; lia.
-        }
         rewrite VALUE_IDENTITY.
         specialize (H5 (Integers.Ptrofs.unsigned i0 / 4)).
         rewrite Z2Nat.id in H5; try lia.
         exploit H5; auto; intros.
-        rewrite MOD_IDENTITY in H0.
+        1: {
+          split.
+          - apply Z.div_pos; lia.
+          - apply Zmult_lt_reg_r with (p := 4); try lia.
+            repeat rewrite ZLib.div_mul_undo; lia.
+        }
+        2: {
+          assert (0 < RTL.fn_stacksize f) by lia.
+          apply Z.div_pos; lia.
+        }
+        replace (4 * (Integers.Ptrofs.unsigned i0 / 4)) with (Integers.Ptrofs.unsigned i0) in H0.
+        2: {
+          rewrite Z.mul_comm.
+          rewrite ZLib.div_mul_undo; lia.
+        }
         rewrite Integers.Ptrofs.repr_unsigned in H0.
         rewrite H1 in H0.
         invert H0. assumption.
diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v
index 1a9144c..a916cb5 100644
--- a/src/translation/HTLgenspec.v
+++ b/src/translation/HTLgenspec.v
@@ -188,6 +188,7 @@ Inductive tr_module (f : RTL.function) : module -> Prop :=
       (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) ->
       stk_len = Z.to_nat (f.(RTL.fn_stacksize) / 4) ->
+      Z.modulo (f.(RTL.fn_stacksize)) 4 = 0 ->
       m = (mkmodule f.(RTL.fn_params)
                         data
                         control
@@ -451,7 +452,7 @@ Proof.
   inversion s; subst.
 
   unfold transf_module in *.
-  monadInv Heqr.
+  destruct (Z.eq_dec (RTL.fn_stacksize f mod 4) 0); monadInv Heqr.
 
   (* TODO: We should be able to fold this into the automation. *)
   pose proof (create_arr_inv _ _ _ _ _ _ _ _ EQ0) as STK_LEN.
-- 
cgit 


From d216c3b6dfbd80f49296b47ba46d18603c723804 Mon Sep 17 00:00:00 2001
From: James Pollard <james@pollard.dev>
Date: Fri, 19 Jun 2020 00:35:41 +0100
Subject: Working on proof.

---
 src/translation/HTLgenproof.v | 96 ++++++++++++++++++++++++++++++++++++++-----
 1 file changed, 86 insertions(+), 10 deletions(-)

(limited to 'src/translation')

diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v
index 77a11dc..046ae06 100644
--- a/src/translation/HTLgenproof.v
+++ b/src/translation/HTLgenproof.v
@@ -69,13 +69,31 @@ Inductive match_stacks (mem : mem) : list RTL.stackframe -> list HTL.stackframe
       match_stacks mem (RTL.Stackframe r f sp pc rs :: cs)
                        (HTL.Stackframe r m pc asr asa :: lr).
 
+Definition reg_stack_based_pointers (sp : Values.block) (rs : Registers.Regmap.t Values.val) : Prop :=
+  forall r, match Registers.Regmap.get r rs with
+        | Values.Vptr sp' off => sp' = sp
+        | _ => True
+        end.
+
+Definition arr_stack_based_pointers (spb : Values.block) (m : mem) (stack_length : Z)
+  (sp : Values.val) : Prop :=
+  forall ptr,
+    0 <= ptr < (stack_length / 4) ->
+    match Mem.loadv AST.Mint32 m (Values.Val.offset_ptr sp (Integers.Ptrofs.repr (4 * ptr))) with
+    | Some (Values.Vptr sp' off) => sp' = spb
+    | _ => True
+    end.
+
 Inductive match_states : RTL.state -> HTL.state -> Prop :=
-| match_state : forall asa asr sf f sp rs mem m st res
+| match_state : forall asa asr sf f sp 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 mem sf res)
-    (MARR : match_arrs m f sp mem asa),
+    (MARR : match_arrs m f sp mem asa)
+    (SP : sp = Values.Vptr sp' (Integers.Ptrofs.repr 0))
+    (RSBP: reg_stack_based_pointers sp' rs)
+    (ASBP: arr_stack_based_pointers sp' mem (f.(RTL.fn_stacksize)) sp),
     match_states (RTL.State sf f sp st rs mem)
                  (HTL.State res m st asr asa)
 | match_returnstate :
@@ -339,7 +357,7 @@ Section CORRECTNESS.
 
       (* prove match_state *)
       rewrite assumption_32bit.
-      constructor; auto; simplify.
+      econstructor; simplify; eauto.
 
       unfold Verilog.merge_regs.
       unfold_merge. simpl. apply regs_lessdef_add_greater. apply greater_than_max_func.
@@ -471,8 +489,67 @@ Section CORRECTNESS.
       destruct c, chunk, addr, args; simplify; rt; simplify.
 
       + admit. (* FIXME: Alignment *)
-      + admit.
-      + admit.
+
+      + (* FIXME: Why is this degenerate? Should we support this mode? *)
+        unfold Op.eval_addressing in H0.
+        destruct (Archi.ptr64) eqn:ARCHI; simplify.
+        destruct (Registers.Regmap.get r0 rs) eqn:EQr0; discriminate.
+
+      + invert MARR. simplify.
+
+        unfold Op.eval_addressing in H0.
+        destruct (Archi.ptr64) eqn:ARCHI; simplify.
+
+        unfold reg_stack_based_pointers in RSBP.
+        pose proof (RSBP r0) as RSBPr0.
+        pose proof (RSBP r1) as RSBPr1.
+
+        destruct (Registers.Regmap.get r0 rs) eqn:EQr0;
+        destruct (Registers.Regmap.get r1 rs) eqn:EQr1; simplify.
+
+        rewrite ARCHI in H1. simplify.
+        subst.
+
+        eexists. split.
+        eapply Smallstep.plus_one.
+        eapply HTL.step_module; eauto.
+        econstructor. econstructor. econstructor. simplify.
+        econstructor. econstructor. econstructor. econstructor. simplify.
+        econstructor.
+        econstructor.
+        econstructor.
+        econstructor.
+        econstructor.
+        econstructor.
+        econstructor.
+        econstructor.
+        econstructor.
+        econstructor.
+        econstructor.
+        econstructor.
+        econstructor.
+        econstructor.
+        econstructor.
+        econstructor.
+        econstructor.
+        econstructor. (* FIXME: Oh dear. *)
+
+        unfold Verilog.arr_assocmap_lookup. simplify. setoid_rewrite H3.
+        f_equal.
+
+        simplify. unfold Verilog.merge_regs.
+        unfold_merge.
+        rewrite AssocMap.gso.
+        apply AssocMap.gss.
+        apply st_greater_than_res.
+
+        simplify. rewrite assumption_32bit.
+        econstructor; simplify; eauto.
+
+        unfold Verilog.merge_regs. unfold_merge.
+        apply regs_lessdef_add_match.
+
+        all: admit.
 
       + invert MARR. simplify.
 
@@ -501,7 +578,7 @@ Section CORRECTNESS.
         apply st_greater_than_res.
 
         simplify. rewrite assumption_32bit.
-        constructor.
+        econstructor; simplify; eauto.
 
         unfold Verilog.merge_regs. unfold_merge.
         apply regs_lessdef_add_match.
@@ -534,7 +611,7 @@ Section CORRECTNESS.
 
         apply regs_lessdef_add_greater.
         apply greater_than_max_func.
-        assumption. assumption.
+        assumption.
 
         unfold state_st_wf. inversion 1. simplify.
         unfold Verilog.merge_regs.
@@ -542,8 +619,6 @@ Section CORRECTNESS.
         apply AssocMap.gss.
         apply st_greater_than_res.
 
-        assumption.
-
         econstructor.
         repeat split; simplify.
         unfold HTL.empty_stack.
@@ -569,9 +644,10 @@ Section CORRECTNESS.
         intros.
         erewrite array_get_error_equal.
         eauto. apply combine_none.
-
         assumption.
 
+        (* FIXME: RSBP Proof. *)
+
     - destruct c, chunk, addr, args; simplify; rt; simplify.
       + admit.
       + admit.
-- 
cgit