Merge remote-tracking branch 'james/arrays-proof' into develop

5 files changed, 961 insertions, 101 deletions

diff --git a/src/common/Coquplib.v b/src/common/Coquplib.v
index b4ca906..5de1e7c 100644
--- a/src/common/Coquplib.v
+++ b/src/common/Coquplib.v
@@ -69,45 +69,52 @@ Ltac kill_bools :=
 
 Ltac unfold_constants :=
   repeat match goal with
-         | [ _ : _ |- context[Integers.Ptrofs.modulus] ] =>
+         | [ |- context[Integers.Ptrofs.modulus] ] =>
            replace Integers.Ptrofs.modulus with 4294967296 by reflexivity
          | [ H : context[Integers.Ptrofs.modulus] |- _ ] =>
            replace Integers.Ptrofs.modulus with 4294967296 in H by reflexivity
 
-         | [ _ : _ |- context[Integers.Ptrofs.min_signed] ] =>
+         | [ |- context[Integers.Ptrofs.min_signed] ] =>
            replace Integers.Ptrofs.min_signed with (-2147483648) by reflexivity
          | [ H : context[Integers.Ptrofs.min_signed] |- _ ] =>
            replace Integers.Ptrofs.min_signed with (-2147483648) in H by reflexivity
 
-         | [ _ : _ |- context[Integers.Ptrofs.max_signed] ] =>
+         | [ |- context[Integers.Ptrofs.max_signed] ] =>
            replace Integers.Ptrofs.max_signed with 2147483647 by reflexivity
          | [ H : context[Integers.Ptrofs.max_signed] |- _ ] =>
            replace Integers.Ptrofs.max_signed with 2147483647 in H by reflexivity
 
-         | [ _ : _ |- context[Integers.Ptrofs.max_unsigned] ] =>
+         | [ |- context[Integers.Ptrofs.max_unsigned] ] =>
            replace Integers.Ptrofs.max_unsigned with 4294967295 by reflexivity
          | [ H : context[Integers.Ptrofs.max_unsigned] |- _ ] =>
            replace Integers.Ptrofs.max_unsigned with 4294967295 in H by reflexivity
 
-         | [ _ : _ |- context[Integers.Int.modulus] ] =>
+         | [ |- context[Integers.Int.modulus] ] =>
            replace Integers.Int.modulus with 4294967296 by reflexivity
          | [ H : context[Integers.Int.modulus] |- _ ] =>
            replace Integers.Int.modulus with 4294967296 in H by reflexivity
 
-         | [ _ : _ |- context[Integers.Int.min_signed] ] =>
+         | [ |- context[Integers.Int.min_signed] ] =>
            replace Integers.Int.min_signed with (-2147483648) by reflexivity
          | [ H : context[Integers.Int.min_signed] |- _ ] =>
            replace Integers.Int.min_signed with (-2147483648) in H by reflexivity
 
-         | [ _ : _ |- context[Integers.Int.max_signed] ] =>
+         | [ |- context[Integers.Int.max_signed] ] =>
            replace Integers.Int.max_signed with 2147483647 by reflexivity
          | [ H : context[Integers.Int.max_signed] |- _ ] =>
            replace Integers.Int.max_signed with 2147483647 in H by reflexivity
 
-         | [ _ : _ |- context[Integers.Int.max_unsigned] ] =>
+         | [ |- context[Integers.Int.max_unsigned] ] =>
            replace Integers.Int.max_unsigned with 4294967295 by reflexivity
          | [ H : context[Integers.Int.max_unsigned] |- _ ] =>
            replace Integers.Int.max_unsigned with 4294967295 in H by reflexivity
+
+         | [ |- context[Integers.Ptrofs.unsigned (Integers.Ptrofs.repr ?x) ] ] =>
+           match (eval compute in (0 <=? x)) with
+           | true => replace (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr x))
+                    with x by reflexivity
+           | false => idtac
+           end
          end.
 
 Ltac simplify := unfold_constants; simpl in *;
@@ -117,6 +124,9 @@ Ltac simplify := unfold_constants; simpl in *;
 Global Opaque Nat.div.
 Global Opaque Z.mul.
 
+Infix "==nat" := eq_nat_dec (no associativity, at level 50).
+Infix "==Z" := Z.eq_dec (no associativity, at level 50).
+
 (* Definition const (A B : Type) (a : A) (b : B) : A := a.
 
 Definition compose (A B C : Type) (f : B -> C) (g : A -> B) (x : A) : C := f (g x). *)
diff --git a/src/common/IntegerExtra.v b/src/common/IntegerExtra.v
index 2f9aae6..8df70d9 100644
--- a/src/common/IntegerExtra.v
+++ b/src/common/IntegerExtra.v
@@ -51,6 +51,23 @@ Module PtrofsExtra.
   Ltac ptrofs_mod_tac m :=
     repeat (ptrofs_mod_match m); lia.
 
+  Lemma signed_mod_unsigned_mod :
+    forall x m,
+      0 < m ->
+      Ptrofs.modulus mod m = 0 ->
+      Ptrofs.signed x mod m = 0 ->
+      Ptrofs.unsigned x mod m = 0.
+  Proof.
+    intros.
+
+    repeat match goal with
+           | [ _ : _ |- context[if ?x then _ else _] ] => destruct x
+           | [ _ : _ |- context[_ mod Ptrofs.modulus mod m] ] =>
+             rewrite <- Zmod_div_mod; try lia; try assumption
+           | [ _ : _ |- context[Ptrofs.unsigned _] ] => rewrite Ptrofs.unsigned_signed
+           end; try (simplify; lia); ptrofs_mod_tac m.
+  Qed.
+
   Lemma of_int_mod :
     forall x m,
       Int.signed x mod m = 0 ->
@@ -88,10 +105,10 @@ Module PtrofsExtra.
       (m | Ptrofs.modulus) ->
       Ptrofs.signed x mod m = 0 ->
       Ptrofs.signed y mod m = 0 ->
-      (Ptrofs.signed (Ptrofs.add x y)) mod m = 0.
+      (Ptrofs.unsigned (Ptrofs.add x y)) mod m = 0.
   Proof.
     intros. unfold Ptrofs.add.
-    rewrite Ptrofs.signed_repr_eq.
+    rewrite Ptrofs.unsigned_repr_eq.
 
     repeat match goal with
            | [ _ : _ |- context[if ?x then _ else _] ] => destruct x
@@ -101,26 +118,47 @@ Module PtrofsExtra.
            end; try (simplify; lia); ptrofs_mod_tac m.
   Qed.
 
-  Lemma mul_divs :
+  Lemma mul_divu :
     forall x y,
-      0 <= Ptrofs.signed y ->
-      0 < Ptrofs.signed x ->
-      Ptrofs.signed y mod Ptrofs.signed x = 0 ->
-      (Integers.Ptrofs.mul x (Integers.Ptrofs.divs y x)) = y.
+      0 < Ptrofs.unsigned x ->
+      Ptrofs.unsigned y mod Ptrofs.unsigned x = 0 ->
+      (Integers.Ptrofs.mul x (Integers.Ptrofs.divu y x)) = y.
   Proof.
     intros.
 
-    pose proof (Ptrofs.mods_divs_Euclid y x).
-    pose proof (Zquot.Zrem_Zmod_zero (Ptrofs.signed y) (Ptrofs.signed x)).
-    apply <- H3 in H1; try lia; clear H3.
-    unfold Ptrofs.mods in H2.
-    rewrite H1 in H2.
-    replace (Ptrofs.repr 0) with (Ptrofs.zero) in H2 by reflexivity.
+    assert (x <> Ptrofs.zero).
+    { intro.
+      rewrite H1 in H.
+      replace (Ptrofs.unsigned Ptrofs.zero) with 0 in H by reflexivity.
+      lia. }
+
+    exploit (Ptrofs.modu_divu_Euclid y x); auto; intros.
+    unfold Ptrofs.modu in H2. rewrite H0 in H2.
+    replace (Ptrofs.repr 0) with Ptrofs.zero in H2 by reflexivity.
     rewrite Ptrofs.add_zero in H2.
     rewrite Ptrofs.mul_commut.
     congruence.
   Qed.
 
+  Lemma divu_unsigned :
+    forall x y,
+      0 < Ptrofs.unsigned y ->
+      Ptrofs.unsigned x < Ptrofs.max_unsigned ->
+      Ptrofs.unsigned (Ptrofs.divu x y) = Ptrofs.unsigned x / Ptrofs.unsigned y.
+  Proof.
+    intros.
+    unfold Ptrofs.divu.
+    rewrite Ptrofs.unsigned_repr; auto.
+    split.
+    apply Z.div_pos; auto.
+    apply Ptrofs.unsigned_range.
+    apply Z.div_le_upper_bound; auto.
+    eapply Z.le_trans.
+    apply Z.lt_le_incl. exact H0.
+    rewrite Z.mul_comm.
+    apply Z.le_mul_diag_r; simplify; lia.
+  Qed.
+
   Lemma mul_unsigned :
     forall x y,
       Ptrofs.mul x y =
@@ -130,6 +168,20 @@ Module PtrofsExtra.
     apply Ptrofs.eqm_samerepr.
     apply Ptrofs.eqm_mult; exists 0; lia.
   Qed.
+
+  Lemma pos_signed_unsigned :
+    forall x,
+      0 <= Ptrofs.signed x ->
+      Ptrofs.signed x = Ptrofs.unsigned x.
+  Proof.
+    intros.
+    rewrite Ptrofs.unsigned_signed.
+    destruct (Ptrofs.lt x Ptrofs.zero) eqn:EQ.
+    unfold Ptrofs.lt in EQ.
+    destruct (zlt (Ptrofs.signed x) (Ptrofs.signed Ptrofs.zero)); try discriminate.
+    replace (Ptrofs.signed (Ptrofs.zero)) with 0 in l by reflexivity. lia.
+    reflexivity.
+  Qed.
 End PtrofsExtra.
 
 Module IntExtra.
diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v
index 54ad77a..59fb70a 100644
--- a/src/translation/HTLgen.v
+++ b/src/translation/HTLgen.v
@@ -280,32 +280,36 @@ Definition translate_condition (c : Op.condition) (args : list reg) : mon expr :
   | _, _ => error (Errors.msg "Htlgen: condition instruction not implemented: other")
   end.
 
-Definition check_address_parameter (p : Z) : bool :=
+Definition check_address_parameter_signed (p : Z) : bool :=
   Z.eqb (Z.modulo p 4) 0
   && Z.leb Integers.Ptrofs.min_signed p
   && Z.leb p Integers.Ptrofs.max_signed.
 
+Definition check_address_parameter_unsigned (p : Z) : bool :=
+  Z.eqb (Z.modulo p 4) 0
+  && Z.leb p Integers.Ptrofs.max_unsigned.
+
 Definition translate_eff_addressing (a: Op.addressing) (args: list reg) : mon expr :=
   match a, args with (* TODO: We should be more methodical here; what are the possibilities?*)
   | Op.Aindexed off, r1::nil =>
-    if (check_address_parameter off)
+    if (check_address_parameter_signed off)
     then ret (boplitz Vadd r1 off)
     else error (Errors.msg "Veriloggen: translate_eff_addressing address misaligned")
   | Op.Ascaled scale offset, r1::nil =>
-    if (check_address_parameter scale) && (check_address_parameter offset)
+    if (check_address_parameter_signed scale) && (check_address_parameter_signed offset)
     then ret (Vbinop Vadd (boplitz Vmul r1 scale) (Vlit (ZToValue 32 offset)))
     else error (Errors.msg "Veriloggen: translate_eff_addressing address misaligned")
   | Op.Aindexed2 offset, r1::r2::nil =>
-    if (check_address_parameter offset)
+    if (check_address_parameter_signed offset)
     then ret (Vbinop Vadd (Vvar r1) (boplitz Vadd r2 offset))
     else error (Errors.msg "Veriloggen: translate_eff_addressing address misaligned")
   | Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *)
-    if (check_address_parameter scale) && (check_address_parameter offset)
+    if (check_address_parameter_signed scale) && (check_address_parameter_signed offset)
     then ret (Vbinop Vadd (boplitz Vadd r1 offset) (boplitz Vmul r2 scale))
     else error (Errors.msg "Veriloggen: translate_eff_addressing address misaligned")
   | Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *)
     let a := Integers.Ptrofs.unsigned a in
-    if (check_address_parameter a)
+    if (check_address_parameter_unsigned a)
     then ret (Vlit (ZToValue 32 a))
     else error (Errors.msg "Veriloggen: translate_eff_addressing address misaligned")
   | _, _ => error (Errors.msg "Veriloggen: translate_eff_addressing unsuported addressing")
@@ -392,19 +396,19 @@ Definition translate_arr_access (mem : AST.memory_chunk) (addr : Op.addressing)
            (args : list reg) (stack : reg) : mon expr :=
   match mem, addr, args with (* TODO: We should be more methodical here; what are the possibilities?*)
   | Mint32, Op.Aindexed off, r1::nil =>
-    if (check_address_parameter off)
-    then ret (Vvari stack (Vbinop Vdiv (boplitz Vadd r1 off) (Vlit (ZToValue 32 4))))
+    if (check_address_parameter_signed off)
+    then ret (Vvari stack (Vbinop Vdivu (boplitz Vadd r1 off) (Vlit (ZToValue 32 4))))
     else error (Errors.msg "HTLgen: translate_arr_access address misaligned")
   | Mint32, Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *)
-    if (check_address_parameter scale) && (check_address_parameter offset)
+    if (check_address_parameter_signed scale) && (check_address_parameter_signed offset)
     then ret (Vvari stack
-                    (Vbinop Vdiv
+                    (Vbinop Vdivu
                             (Vbinop Vadd (boplitz Vadd r1 offset) (boplitz Vmul r2 scale))
                             (ZToValue 32 4)))
     else error (Errors.msg "HTLgen: translate_arr_access address misaligned")
   | Mint32, Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *)
-    let a := Integers.Ptrofs.signed a in
-    if (check_address_parameter a)
+    let a := Integers.Ptrofs.unsigned a in
+    if (check_address_parameter_unsigned a)
     then ret (Vvari stack (Vlit (ZToValue 32 (a / 4))))
     else error (Errors.msg "HTLgen: eff_addressing misaligned stack offset")
   | _, _, _ => error (Errors.msg "HTLgen: translate_arr_access unsuported addressing")
diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v
index 77bd4ef..753dccf 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 Array IntegerExtra.
+From coqup Require Import Coquplib HTLgenspec HTLgen Value AssocMap Array IntegerExtra ZExtra.
 From coqup Require HTL Verilog.
 
 Require Import Lia.
@@ -196,6 +196,67 @@ Proof.
   assumption.
 Qed.
 
+Lemma list_combine_lookup_first :
+  forall l1 l2 n,
+    length l1 = length l2 ->
+    nth_error l1 n = Some None ->
+    nth_error (list_combine Verilog.merge_cell l1 l2) n = nth_error l2 n.
+Proof.
+  induction l1; intros; simplify.
+
+  rewrite nth_error_nil in H0.
+  discriminate.
+
+  destruct l2 eqn:EQl2. simplify.
+  simpl in H. invert H.
+  destruct n; simpl in *.
+  invert H0. simpl. reflexivity.
+  eauto.
+Qed.
+
+Lemma combine_lookup_first :
+  forall a1 a2 n,
+    a1.(arr_length) = a2.(arr_length) ->
+    array_get_error n a1 = Some None ->
+    array_get_error n (combine Verilog.merge_cell a1 a2) = array_get_error n a2.
+Proof.
+  intros.
+
+  unfold array_get_error in *.
+  apply list_combine_lookup_first; eauto.
+  rewrite a1.(arr_wf). rewrite a2.(arr_wf).
+  assumption.
+Qed.
+
+Lemma list_combine_lookup_second :
+  forall l1 l2 n x,
+    length l1 = length l2 ->
+    nth_error l1 n = Some (Some x) ->
+    nth_error (list_combine Verilog.merge_cell l1 l2) n = Some (Some x).
+Proof.
+  induction l1; intros; simplify; auto.
+
+  destruct l2 eqn:EQl2. simplify.
+  simpl in H. invert H.
+  destruct n; simpl in *.
+  invert H0. simpl. reflexivity.
+  eauto.
+Qed.
+
+Lemma combine_lookup_second :
+  forall a1 a2 n x,
+    a1.(arr_length) = a2.(arr_length) ->
+    array_get_error n a1 = Some (Some x) ->
+    array_get_error n (combine Verilog.merge_cell a1 a2) = Some (Some x).
+Proof.
+  intros.
+
+  unfold array_get_error in *.
+  apply list_combine_lookup_second; eauto.
+  rewrite a1.(arr_wf). rewrite a2.(arr_wf).
+  assumption.
+Qed.
+
 (* Need to eventually move posToValue 32 to posToValueAuto, as that has this proof. *)
 Lemma assumption_32bit :
   forall v,
@@ -533,17 +594,17 @@ Section CORRECTNESS.
         invert H8.
         clear H0. clear H6.
 
-        unfold check_address_parameter in *. simplify.
+        unfold check_address_parameter_signed in *;
+        unfold check_address_parameter_unsigned in *; simplify.
 
         remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (valueToZ asr # r0))
                                       (Integers.Ptrofs.of_int (Integers.Int.repr z))) as OFFSET.
 
         (** Read bounds assumption *)
-        assert (0 <= Integers.Ptrofs.signed OFFSET) as READ_BOUND_LOW by admit.
-        assert (Integers.Ptrofs.signed OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH by admit.
+        assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH by admit.
 
         (** Modular preservation proof *)
-        assert (Integers.Ptrofs.signed OFFSET mod 4 = 0) as MOD_PRESERVE.
+        assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE.
         { rewrite HeqOFFSET.
           apply PtrofsExtra.add_mod; simplify; try lia.
           exists 1073741824. reflexivity. (* FIXME: This is sadness inducing. *)
@@ -556,34 +617,28 @@ Section CORRECTNESS.
         (** Normalisation proof *)
         assert (Integers.Ptrofs.repr
                   (4 * Integers.Ptrofs.unsigned
-                         (Integers.Ptrofs.divs OFFSET (Integers.Ptrofs.repr 4))) = OFFSET)
+                         (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4))) = OFFSET)
           as NORMALISE.
         { replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) at 1 by reflexivity.
           rewrite <- PtrofsExtra.mul_unsigned.
-          apply PtrofsExtra.mul_divs; auto.
-          rewrite Integers.Ptrofs.signed_repr; simplify; lia. }
+          apply PtrofsExtra.mul_divu; simplify; auto; lia. }
 
         (** Normalised bounds proof *)
         assert (0 <=
-                Integers.Ptrofs.unsigned (Integers.Ptrofs.divs OFFSET (Integers.Ptrofs.repr 4))
+                Integers.Ptrofs.unsigned (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4))
                 < (RTL.fn_stacksize f / 4))
         as NORMALISE_BOUND.
         { split.
           apply Integers.Ptrofs.unsigned_range_2.
-          assert (forall x y, Integers.Ptrofs.divs x y = Integers.Ptrofs.divs x y ) by reflexivity.
-          unfold Integers.Ptrofs.divs at 2 in H0.
+          assert (forall x y, Integers.Ptrofs.divu x y = Integers.Ptrofs.divu x y ) by reflexivity.
+          unfold Integers.Ptrofs.divu at 2 in H0.
           rewrite H0. clear H0.
           rewrite Integers.Ptrofs.unsigned_repr; simplify.
-          rewrite Integers.Ptrofs.signed_repr; simplify; try lia.
-          rewrite Z.quot_div_nonneg; try (rewrite <- HeqOFFSET; assumption); try lia.
           apply Zmult_lt_reg_r with (p := 4); try lia.
           repeat rewrite ZLib.div_mul_undo; try lia.
-          rewrite Integers.Ptrofs.signed_repr.
-          rewrite Z.quot_div_nonneg; try (rewrite <- HeqOFFSET; assumption); try lia.
           split.
-          apply Z.div_pos; try (rewrite <- HeqOFFSET; assumption); try lia.
-          apply Z.div_le_upper_bound; simplify; try (rewrite <- HeqOFFSET; lia); try lia.
-          simplify; lia. }
+          apply Z.div_pos; try lia; apply Integers.Ptrofs.unsigned_range_2.
+          apply Z.div_le_upper_bound; lia. }
 
         inversion NORMALISE_BOUND as [ NORMALISE_BOUND_LOW NORMALISE_BOUND_HIGH ];
         clear NORMALISE_BOUND.
@@ -626,7 +681,7 @@ Section CORRECTNESS.
         setoid_rewrite Integers.Ptrofs.add_zero_l in H7.
 
         specialize (H7 (Integers.Ptrofs.unsigned
-                          (Integers.Ptrofs.divs
+                          (Integers.Ptrofs.divu
                              OFFSET
                              (Integers.Ptrofs.repr 4)))).
 
@@ -638,11 +693,11 @@ Section CORRECTNESS.
 
         assert (Z.to_nat
                   (Integers.Ptrofs.unsigned
-                     (Integers.Ptrofs.divs
+                     (Integers.Ptrofs.divu
                         OFFSET
                         (Integers.Ptrofs.repr 4)))
                 =
-                valueToNat (vdivs (vplus asr # r0 (ZToValue 32 z) ?EQ2) (ZToValue 32 4) ?EQ1))
+                valueToNat (vdiv (vplus asr # r0 (ZToValue 32 z) ?EQ2) (ZToValue 32 4) ?EQ1))
           as EXPR_OK by admit.
         rewrite <- EXPR_OK.
         rewrite NORMALISE in I.
@@ -696,7 +751,7 @@ Section CORRECTNESS.
         rewrite Registers.Regmap.gss.
         unfold arr_stack_based_pointers in ASBP.
         specialize (ASBP (Integers.Ptrofs.unsigned
-                            (Integers.Ptrofs.divs OFFSET (Integers.Ptrofs.repr 4)))).
+                            (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)))).
         exploit ASBP; auto; intros I.
 
         rewrite NORMALISE in I.
@@ -743,7 +798,8 @@ Section CORRECTNESS.
         invert H10. invert H12.
         clear H0. clear H6. clear H8.
 
-        unfold check_address_parameter in *. simplify.
+        unfold check_address_parameter_signed in *;
+        unfold check_address_parameter_unsigned in *; simplify.
 
         remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (valueToZ asr # r0))
                                       (Integers.Ptrofs.of_int
@@ -751,11 +807,10 @@ Section CORRECTNESS.
                                                            (Integers.Int.repr z0)))) as OFFSET.
 
         (** Read bounds assumption *)
-        assert (0 <= Integers.Ptrofs.signed OFFSET) as READ_BOUND_LOW by admit.
-        assert (Integers.Ptrofs.signed OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH by admit.
+        assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH by admit.
 
         (** Modular preservation proof *)
-        assert (Integers.Ptrofs.signed OFFSET mod 4 = 0) as MOD_PRESERVE.
+        assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE.
         { rewrite HeqOFFSET.
           apply PtrofsExtra.add_mod; simplify; try lia.
           exists 1073741824. reflexivity. (* FIXME: This is sadness inducing. *)
@@ -774,34 +829,28 @@ Section CORRECTNESS.
         (** Normalisation proof *)
         assert (Integers.Ptrofs.repr
                   (4 * Integers.Ptrofs.unsigned
-                         (Integers.Ptrofs.divs OFFSET (Integers.Ptrofs.repr 4))) = OFFSET)
+                         (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4))) = OFFSET)
           as NORMALISE.
         { replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) at 1 by reflexivity.
           rewrite <- PtrofsExtra.mul_unsigned.
-          apply PtrofsExtra.mul_divs; auto.
-          rewrite Integers.Ptrofs.signed_repr; simplify; lia. }
+          apply PtrofsExtra.mul_divu; simplify; auto; lia. }
 
         (** Normalised bounds proof *)
         assert (0 <=
-                Integers.Ptrofs.unsigned (Integers.Ptrofs.divs OFFSET (Integers.Ptrofs.repr 4))
+                Integers.Ptrofs.unsigned (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4))
                 < (RTL.fn_stacksize f / 4))
         as NORMALISE_BOUND.
         { split.
           apply Integers.Ptrofs.unsigned_range_2.
-          assert (forall x y, Integers.Ptrofs.divs x y = Integers.Ptrofs.divs x y ) by reflexivity.
-          unfold Integers.Ptrofs.divs at 2 in H0.
+          assert (forall x y, Integers.Ptrofs.divu x y = Integers.Ptrofs.divu x y ) by reflexivity.
+          unfold Integers.Ptrofs.divu at 2 in H0.
           rewrite H0. clear H0.
           rewrite Integers.Ptrofs.unsigned_repr; simplify.
-          rewrite Integers.Ptrofs.signed_repr; simplify; try lia.
-          rewrite Z.quot_div_nonneg; try (rewrite <- HeqOFFSET; assumption); try lia.
           apply Zmult_lt_reg_r with (p := 4); try lia.
           repeat rewrite ZLib.div_mul_undo; try lia.
-          rewrite Integers.Ptrofs.signed_repr.
-          rewrite Z.quot_div_nonneg; try (rewrite <- HeqOFFSET; assumption); try lia.
           split.
-          apply Z.div_pos; try (rewrite <- HeqOFFSET; assumption); try lia.
-          apply Z.div_le_upper_bound; simplify; try (rewrite <- HeqOFFSET; lia); try lia.
-          simplify; lia. }
+          apply Z.div_pos; try lia; apply Integers.Ptrofs.unsigned_range_2.
+          apply Z.div_le_upper_bound; lia. }
 
         inversion NORMALISE_BOUND as [ NORMALISE_BOUND_LOW NORMALISE_BOUND_HIGH ];
         clear NORMALISE_BOUND.
@@ -850,7 +899,7 @@ Section CORRECTNESS.
         setoid_rewrite Integers.Ptrofs.add_zero_l in H7.
 
         specialize (H7 (Integers.Ptrofs.unsigned
-                          (Integers.Ptrofs.divs
+                          (Integers.Ptrofs.divu
                              OFFSET
                              (Integers.Ptrofs.repr 4)))).
 
@@ -861,12 +910,12 @@ Section CORRECTNESS.
         intros I.
         assert (Z.to_nat
                   (Integers.Ptrofs.unsigned
-                     (Integers.Ptrofs.divs
+                     (Integers.Ptrofs.divu
                         OFFSET
                         (Integers.Ptrofs.repr 4)))
                 = valueToNat
-                    (vdivs (vplus (vplus asr # r0 (ZToValue 32 z0) ?EQ5)
-                                  (vmul asr # r1 (ZToValue 32 z) ?EQ6) ?EQ4) (ZToValue 32 4) ?EQ3))
+                    (vdiv (vplus (vplus asr # r0 (ZToValue 32 z0) ?EQ5)
+                                 (vmul asr # r1 (ZToValue 32 z) ?EQ6) ?EQ4) (ZToValue 32 4) ?EQ3))
           as EXPR_OK by admit.
         rewrite <- EXPR_OK.
         rewrite NORMALISE in I.
@@ -920,7 +969,7 @@ Section CORRECTNESS.
         rewrite Registers.Regmap.gss.
         unfold arr_stack_based_pointers in ASBP.
         specialize (ASBP (Integers.Ptrofs.unsigned
-                            (Integers.Ptrofs.divs OFFSET (Integers.Ptrofs.repr 4)))).
+                            (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)))).
         exploit ASBP; auto; intros I.
 
         rewrite NORMALISE in I.
@@ -940,7 +989,8 @@ Section CORRECTNESS.
         destruct (Archi.ptr64) eqn:ARCHI; simplify.
         rewrite ARCHI in H0. simplify.
 
-        unfold check_address_parameter in EQ; simplify.
+        unfold check_address_parameter_unsigned in *;
+        unfold check_address_parameter_signed in *; simplify.
 
         assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
         rewrite ZERO in H1. clear ZERO.
@@ -949,43 +999,36 @@ Section CORRECTNESS.
         remember i0 as OFFSET.
 
         (** Read bounds assumption *)
-        assert (0 <= Integers.Ptrofs.signed OFFSET) as READ_BOUND_LOW by admit.
-        assert (Integers.Ptrofs.signed OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH by admit.
+        assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH by admit.
 
         (** Modular preservation proof *)
-        rename H8 into MOD_PRESERVE.
+        rename H0 into MOD_PRESERVE.
 
         (** Normalisation proof *)
         assert (Integers.Ptrofs.repr
                   (4 * Integers.Ptrofs.unsigned
-                         (Integers.Ptrofs.divs OFFSET (Integers.Ptrofs.repr 4))) = OFFSET)
+                         (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4))) = OFFSET)
           as NORMALISE.
         { replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) at 1 by reflexivity.
           rewrite <- PtrofsExtra.mul_unsigned.
-          apply PtrofsExtra.mul_divs; auto.
-          rewrite Integers.Ptrofs.signed_repr; simplify; lia. }
+          apply PtrofsExtra.mul_divu; simplify; auto; try lia. }
 
         (** Normalised bounds proof *)
         assert (0 <=
-                Integers.Ptrofs.unsigned (Integers.Ptrofs.divs OFFSET (Integers.Ptrofs.repr 4))
+                Integers.Ptrofs.unsigned (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4))
                 < (RTL.fn_stacksize f / 4))
         as NORMALISE_BOUND.
         { split.
           apply Integers.Ptrofs.unsigned_range_2.
-          assert (forall x y, Integers.Ptrofs.divs x y = Integers.Ptrofs.divs x y ) by reflexivity.
-          unfold Integers.Ptrofs.divs at 2 in H0.
+          assert (forall x y, Integers.Ptrofs.divu x y = Integers.Ptrofs.divu x y ) by reflexivity.
+          unfold Integers.Ptrofs.divu at 2 in H0.
           rewrite H0. clear H0.
           rewrite Integers.Ptrofs.unsigned_repr; simplify.
-          rewrite Integers.Ptrofs.signed_repr; simplify; try lia.
-          rewrite Z.quot_div_nonneg; try (rewrite <- HeqOFFSET; assumption); try lia.
           apply Zmult_lt_reg_r with (p := 4); try lia.
           repeat rewrite ZLib.div_mul_undo; try lia.
-          rewrite Integers.Ptrofs.signed_repr.
-          rewrite Z.quot_div_nonneg; try (rewrite <- HeqOFFSET; assumption); try lia.
           split.
-          apply Z.div_pos; try (rewrite <- HeqOFFSET; assumption); try lia.
-          apply Z.div_le_upper_bound; simplify; try (rewrite <- HeqOFFSET; lia); try lia.
-          simplify; lia. }
+          apply Z.div_pos; try lia; apply Integers.Ptrofs.unsigned_range_2.
+          apply Z.div_le_upper_bound; lia. }
 
         inversion NORMALISE_BOUND as [ NORMALISE_BOUND_LOW NORMALISE_BOUND_HIGH ];
         clear NORMALISE_BOUND.
@@ -1025,7 +1068,7 @@ Section CORRECTNESS.
         setoid_rewrite Integers.Ptrofs.add_zero_l in H7.
 
         specialize (H7 (Integers.Ptrofs.unsigned
-                          (Integers.Ptrofs.divs
+                          (Integers.Ptrofs.divu
                              OFFSET
                              (Integers.Ptrofs.repr 4)))).
 
@@ -1036,11 +1079,11 @@ Section CORRECTNESS.
         intros I.
         assert (Z.to_nat
                   (Integers.Ptrofs.unsigned
-                     (Integers.Ptrofs.divs
+                     (Integers.Ptrofs.divu
                         OFFSET
                         (Integers.Ptrofs.repr 4)))
                   =
-                  valueToNat (ZToValue 32 (Integers.Ptrofs.signed OFFSET / 4)))
+                  valueToNat (ZToValue 32 (Integers.Ptrofs.unsigned OFFSET / 4)))
           as EXPR_OK by admit.
         rewrite <- EXPR_OK.
         rewrite NORMALISE in I.
@@ -1094,7 +1137,7 @@ Section CORRECTNESS.
         rewrite Registers.Regmap.gss.
         unfold arr_stack_based_pointers in ASBP.
         specialize (ASBP (Integers.Ptrofs.unsigned
-                            (Integers.Ptrofs.divs OFFSET (Integers.Ptrofs.repr 4)))).
+                            (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)))).
         exploit ASBP; auto; intros I.
 
         rewrite NORMALISE in I.
@@ -1109,9 +1152,707 @@ Section CORRECTNESS.
         rewrite Registers.Regmap.gso; auto.
 
     - destruct c, chunk, addr, args; simplify; rt; simplify.
-      + admit.
-      + admit.
-      + admit.
+      + (** Preamble *)
+        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.
+
+        destruct (Registers.Regmap.get r0 rs) eqn:EQr0; simplify.
+
+        rewrite ARCHI in H1. simplify.
+        subst.
+
+        pose proof MASSOC as MASSOC'.
+        invert MASSOC'.
+        pose proof (H0 r0).
+        assert (HPler0 : Ple r0 (RTL.max_reg_function f))
+          by (eapply RTL.max_reg_function_use; eauto; simplify; eauto).
+        apply H6 in HPler0.
+        invert HPler0; try congruence.
+        rewrite EQr0 in H8.
+        invert H8.
+        clear H0. clear H6.
+
+        unfold check_address_parameter_unsigned in *;
+        unfold check_address_parameter_signed in *; simplify.
+
+        remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (valueToZ asr # r0))
+                                      (Integers.Ptrofs.of_int (Integers.Int.repr z))) as OFFSET.
+
+        (** Read bounds assumption *)
+        assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as WRITE_BOUND_HIGH by admit.
+
+        (** Modular preservation proof *)
+        assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE.
+        { rewrite HeqOFFSET.
+          apply PtrofsExtra.add_mod; simplify; try lia.
+          exists 1073741824. reflexivity. (* FIXME: This is sadness inducing. *)
+          rewrite Integers.Ptrofs.signed_repr; try assumption.
+          admit. (* FIXME: Register bounds. *)
+          apply PtrofsExtra.of_int_mod.
+          rewrite Integers.Int.signed_repr; simplify; try split; try assumption.
+        }
+
+        (** Start of proof proper *)
+        eexists. split.
+        eapply Smallstep.plus_one.
+        eapply HTL.step_module; eauto.
+        econstructor. econstructor. econstructor.
+        eapply Verilog.stmnt_runp_Vnonblock_arr. simplify.
+        econstructor.
+        eapply Verilog.erun_Vbinop with (EQ := ?[EQ7]).
+        eapply Verilog.erun_Vbinop with (EQ := ?[EQ8]).
+        econstructor.
+        econstructor.
+        econstructor. econstructor. econstructor. econstructor.
+        econstructor. econstructor. econstructor. econstructor.
+
+        all: simplify.
+
+        (** State Lookup *)
+        unfold Verilog.merge_regs.
+        simplify.
+        unfold_merge.
+        apply AssocMap.gss.
+
+        (** Match states *)
+        rewrite assumption_32bit.
+        econstructor; eauto.
+
+        (** Match assocmaps *)
+        unfold Verilog.merge_regs. simplify. unfold_merge.
+        apply regs_lessdef_add_greater. apply greater_than_max_func.
+        assumption.
+
+        (** States well formed *)
+        unfold state_st_wf. inversion 1. simplify.
+        unfold Verilog.merge_regs.
+        unfold_merge.
+        apply AssocMap.gss.
+
+        (** Match stacks *)
+        admit.
+
+        (** Equality proof *)
+        assert (Z.to_nat
+                  (Integers.Ptrofs.unsigned
+                     (Integers.Ptrofs.divu
+                        OFFSET
+                        (Integers.Ptrofs.repr 4)))
+                =
+                valueToNat (vdiv (vplus asr # r0 (ZToValue 32 z) ?EQ8) (ZToValue 32 4) ?EQ7))
+          as EXPR_OK by admit.
+
+        assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
+        inversion MASSOC; revert HeqOFFSET; subst; clear MASSOC; intros HeqOFFSET.
+
+        econstructor.
+        repeat split; simplify.
+        unfold HTL.empty_stack.
+        simplify.
+        unfold Verilog.merge_arrs.
+
+        rewrite AssocMap.gcombine.
+        2: { reflexivity. }
+        unfold Verilog.arr_assocmap_set.
+        rewrite AssocMap.gss.
+        unfold Verilog.merge_arr.
+        rewrite AssocMap.gss.
+        setoid_rewrite H5.
+        reflexivity.
+
+        rewrite combine_length.
+        rewrite <- array_set_len.
+        unfold arr_repeat. simplify.
+        apply list_repeat_len.
+
+        rewrite <- array_set_len.
+        unfold arr_repeat. simplify.
+        rewrite list_repeat_len.
+        rewrite H4. reflexivity.
+
+        intros.
+        destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET).
+
+        erewrite Mem.load_store_same.
+        2: { rewrite ZERO.
+             rewrite Integers.Ptrofs.add_zero_l.
+             rewrite e.
+             rewrite Integers.Ptrofs.unsigned_repr.
+             exact H1.
+             apply Integers.Ptrofs.unsigned_range_2. }
+        constructor.
+        erewrite combine_lookup_second.
+        simpl.
+        assert (Ple src (RTL.max_reg_function f))
+          by (eapply RTL.max_reg_function_use; eauto; simpl; auto);
+        apply H0 in H14.
+        destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; invert H14; eauto.
+
+        rewrite <- array_set_len.
+        unfold arr_repeat. simplify.
+        rewrite list_repeat_len. auto.
+
+        assert (4 * ptr / 4 = Integers.Ptrofs.unsigned OFFSET / 4) by (f_equal; assumption).
+        rewrite Z.mul_comm in H14.
+        rewrite Z_div_mult in H14; try lia.
+        replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) in H14 by reflexivity.
+        rewrite <- PtrofsExtra.divu_unsigned in H14; unfold_constants; try lia.
+        rewrite H14. rewrite EXPR_OK.
+        rewrite array_get_error_set_bound.
+        reflexivity.
+        unfold arr_length, arr_repeat. simpl.
+        rewrite list_repeat_len. lia.
+
+        erewrite Mem.load_store_other with (m1 := m).
+        2: { exact H1. }
+        2: { right.
+             rewrite ZERO.
+             rewrite Integers.Ptrofs.add_zero_l.
+             rewrite Integers.Ptrofs.unsigned_repr.
+             simpl.
+             destruct (Z_le_gt_dec (4 * ptr + 4) (Integers.Ptrofs.unsigned OFFSET)); eauto.
+             right.
+             apply ZExtra.mod_0_bounds; try lia.
+             apply ZLib.Z_mod_mult'.
+             invert H13.
+             rewrite Z2Nat.id in H19; try lia.
+             apply Zmult_lt_compat_r with (p := 4) in H19; try lia.
+             rewrite ZLib.div_mul_undo in H19; try lia.
+             split; try lia.
+             apply Z.le_trans with (m := RTL.fn_stacksize f); simplify; lia.
+        }
+
+        rewrite <- EXPR_OK.
+        rewrite PtrofsExtra.divu_unsigned; auto; try (unfold_constants; lia).
+        destruct (ptr ==Z Integers.Ptrofs.unsigned OFFSET / 4).
+        apply Z.mul_cancel_r with (p := 4) in e; try lia.
+        rewrite ZLib.div_mul_undo in e; try lia.
+        rewrite combine_lookup_first.
+        eapply H7; eauto.
+
+        rewrite <- array_set_len.
+        unfold arr_repeat. simplify.
+        rewrite list_repeat_len. auto.
+        rewrite array_gso.
+        unfold array_get_error.
+        unfold arr_repeat.
+        simplify.
+        apply list_repeat_lookup.
+        lia.
+        unfold_constants.
+        intro.
+        apply Z2Nat.inj_iff in H14; try lia.
+        apply Z.div_pos; try lia.
+        apply Integers.Ptrofs.unsigned_range.
+
+        assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
+        unfold arr_stack_based_pointers.
+        intros.
+        destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET).
+
+        simplify.
+        erewrite Mem.load_store_same.
+        2: { rewrite ZERO.
+             rewrite Integers.Ptrofs.add_zero_l.
+             rewrite e.
+             rewrite Integers.Ptrofs.unsigned_repr.
+             exact H1.
+             apply Integers.Ptrofs.unsigned_range_2. }
+        simplify.
+        destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; try constructor.
+        destruct (Archi.ptr64); try discriminate.
+        pose proof (RSBP src). rewrite EQ_SRC in H0.
+        assumption.
+
+        simpl.
+        erewrite Mem.load_store_other with (m1 := m).
+        2: { exact H1. }
+        2: { right.
+             rewrite ZERO.
+             rewrite Integers.Ptrofs.add_zero_l.
+             rewrite Integers.Ptrofs.unsigned_repr.
+             simpl.
+             destruct (Z_le_gt_dec (4 * ptr + 4) (Integers.Ptrofs.unsigned OFFSET)); eauto.
+             right.
+             apply ZExtra.mod_0_bounds; try lia.
+             apply ZLib.Z_mod_mult'.
+             invert H0.
+             apply Zmult_lt_compat_r with (p := 4) in H14; try lia.
+             rewrite ZLib.div_mul_undo in H14; try lia.
+             split; try lia.
+             apply Z.le_trans with (m := RTL.fn_stacksize f); simplify; lia.
+        }
+        apply ASBP; assumption.
+
+      + (** Preamble *)
+        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.
+        clear RSBPr1.
+
+        pose proof MASSOC as MASSOC'.
+        invert MASSOC'.
+        pose proof (H0 r0).
+        pose proof (H0 r1).
+        assert (HPler0 : Ple r0 (RTL.max_reg_function f))
+          by (eapply RTL.max_reg_function_use; eauto; simplify; eauto).
+        assert (HPler1 : Ple r1 (RTL.max_reg_function f))
+          by (eapply RTL.max_reg_function_use; eauto; simpl; auto).
+        apply H6 in HPler0.
+        apply H8 in HPler1.
+        invert HPler0; invert HPler1; try congruence.
+        rewrite EQr0 in H10.
+        rewrite EQr1 in H12.
+        invert H10. invert H12.
+        clear H0. clear H6. clear H8.
+
+        unfold check_address_parameter_signed in *;
+        unfold check_address_parameter_unsigned in *; simplify.
+
+        remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (valueToZ asr # r0))
+                                      (Integers.Ptrofs.of_int
+                                         (Integers.Int.add (Integers.Int.mul (valueToInt asr # r1) (Integers.Int.repr z))
+                                                           (Integers.Int.repr z0)))) as OFFSET.
+
+        (** Read bounds assumption *)
+        assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH by admit.
+
+        (** Modular preservation proof *)
+        assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE.
+        { rewrite HeqOFFSET.
+          apply PtrofsExtra.add_mod; simplify; try lia.
+          exists 1073741824. reflexivity. (* FIXME: This is sadness inducing. *)
+          rewrite Integers.Ptrofs.signed_repr; try assumption.
+          admit. (* FIXME: Register bounds. *)
+          apply PtrofsExtra.of_int_mod.
+          apply IntExtra.add_mod; simplify; try lia.
+          exists 1073741824. reflexivity. (* FIXME: This is sadness inducing. *)
+          apply IntExtra.mul_mod; simplify; try lia.
+          exists 1073741824. reflexivity. (* FIXME: This is sadness inducing. *)
+          admit. (* FIXME: Register bounds. *)
+          rewrite Integers.Int.signed_repr; simplify; try split; try assumption.
+          rewrite Integers.Int.signed_repr; simplify; try split; try assumption.
+        }
+
+        (** Start of proof proper *)
+        eexists. split.
+        eapply Smallstep.plus_one.
+        eapply HTL.step_module; eauto.
+        econstructor. econstructor. econstructor.
+        eapply Verilog.stmnt_runp_Vnonblock_arr. simplify.
+        econstructor.
+        eapply Verilog.erun_Vbinop with (EQ := ?[EQ9]).
+        eapply Verilog.erun_Vbinop with (EQ := ?[EQ10]).
+        eapply Verilog.erun_Vbinop with (EQ := ?[EQ11]).
+        econstructor. econstructor. econstructor. econstructor.
+        econstructor.
+        eapply Verilog.erun_Vbinop with (EQ := ?[EQ12]).
+        econstructor. econstructor. econstructor. econstructor.
+        econstructor. econstructor. econstructor. econstructor.
+        econstructor. econstructor. econstructor. econstructor.
+
+        all: simplify.
+
+        (** State Lookup *)
+        unfold Verilog.merge_regs.
+        simplify.
+        unfold_merge.
+        apply AssocMap.gss.
+
+        (** Match states *)
+        rewrite assumption_32bit.
+        econstructor; eauto.
+
+        (** Match assocmaps *)
+        unfold Verilog.merge_regs. simplify. unfold_merge.
+        apply regs_lessdef_add_greater. apply greater_than_max_func.
+        assumption.
+
+        (** States well formed *)
+        unfold state_st_wf. inversion 1. simplify.
+        unfold Verilog.merge_regs.
+        unfold_merge.
+        apply AssocMap.gss.
+
+        (** Match stacks *)
+        admit.
+
+        (** Equality proof *)
+        assert (Z.to_nat
+                  (Integers.Ptrofs.unsigned
+                     (Integers.Ptrofs.divu
+                        OFFSET
+                        (Integers.Ptrofs.repr 4)))
+                =
+                valueToNat (vdiv
+                              (vplus (vplus asr # r0 (ZToValue 32 z0) ?EQ11) (vmul asr # r1 (ZToValue 32 z) ?EQ12)
+                                     ?EQ10) (ZToValue 32 4) ?EQ9))
+          as EXPR_OK by admit.
+
+        assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
+        inversion MASSOC; revert HeqOFFSET; subst; clear MASSOC; intros HeqOFFSET.
+
+        econstructor.
+        repeat split; simplify.
+        unfold HTL.empty_stack.
+        simplify.
+        unfold Verilog.merge_arrs.
+
+        rewrite AssocMap.gcombine.
+        2: { reflexivity. }
+        unfold Verilog.arr_assocmap_set.
+        rewrite AssocMap.gss.
+        unfold Verilog.merge_arr.
+        rewrite AssocMap.gss.
+        setoid_rewrite H5.
+        reflexivity.
+
+        rewrite combine_length.
+        rewrite <- array_set_len.
+        unfold arr_repeat. simplify.
+        apply list_repeat_len.
+
+        rewrite <- array_set_len.
+        unfold arr_repeat. simplify.
+        rewrite list_repeat_len.
+        rewrite H4. reflexivity.
+
+        intros.
+        destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET).
+
+        erewrite Mem.load_store_same.
+        2: { rewrite ZERO.
+             rewrite Integers.Ptrofs.add_zero_l.
+             rewrite e.
+             rewrite Integers.Ptrofs.unsigned_repr.
+             exact H1.
+             apply Integers.Ptrofs.unsigned_range_2. }
+        constructor.
+        erewrite combine_lookup_second.
+        simpl.
+        assert (Ple src (RTL.max_reg_function f))
+          by (eapply RTL.max_reg_function_use; eauto; simpl; auto);
+        apply H0 in H21.
+        destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; invert H21; eauto.
+
+        rewrite <- array_set_len.
+        unfold arr_repeat. simplify.
+        rewrite list_repeat_len. auto.
+
+        assert (4 * ptr / 4 = Integers.Ptrofs.unsigned OFFSET / 4) by (f_equal; assumption).
+        rewrite Z.mul_comm in H21.
+        rewrite Z_div_mult in H21; try lia.
+        replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) in H21 by reflexivity.
+        rewrite <- PtrofsExtra.divu_unsigned in H21; unfold_constants; try lia.
+        rewrite H21. rewrite EXPR_OK.
+        rewrite array_get_error_set_bound.
+        reflexivity.
+        unfold arr_length, arr_repeat. simpl.
+        rewrite list_repeat_len. lia.
+
+        erewrite Mem.load_store_other with (m1 := m).
+        2: { exact H1. }
+        2: { right.
+             rewrite ZERO.
+             rewrite Integers.Ptrofs.add_zero_l.
+             rewrite Integers.Ptrofs.unsigned_repr.
+             simpl.
+             destruct (Z_le_gt_dec (4 * ptr + 4) (Integers.Ptrofs.unsigned OFFSET)); eauto.
+             right.
+             apply ZExtra.mod_0_bounds; try lia.
+             apply ZLib.Z_mod_mult'.
+             invert H20.
+             rewrite Z2Nat.id in H22; try lia.
+             apply Zmult_lt_compat_r with (p := 4) in H22; try lia.
+             rewrite ZLib.div_mul_undo in H22; try lia.
+             split; try lia.
+             apply Z.le_trans with (m := RTL.fn_stacksize f); simplify; lia.
+        }
+
+        rewrite <- EXPR_OK.
+        rewrite PtrofsExtra.divu_unsigned; auto; try (unfold_constants; lia).
+        destruct (ptr ==Z Integers.Ptrofs.unsigned OFFSET / 4).
+        apply Z.mul_cancel_r with (p := 4) in e; try lia.
+        rewrite ZLib.div_mul_undo in e; try lia.
+        rewrite combine_lookup_first.
+        eapply H7; eauto.
+
+        rewrite <- array_set_len.
+        unfold arr_repeat. simplify.
+        rewrite list_repeat_len. auto.
+        rewrite array_gso.
+        unfold array_get_error.
+        unfold arr_repeat.
+        simplify.
+        apply list_repeat_lookup.
+        lia.
+        unfold_constants.
+        intro.
+        apply Z2Nat.inj_iff in H21; try lia.
+        apply Z.div_pos; try lia.
+        apply Integers.Ptrofs.unsigned_range.
+
+        assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
+        unfold arr_stack_based_pointers.
+        intros.
+        destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET).
+
+        simplify.
+        erewrite Mem.load_store_same.
+        2: { rewrite ZERO.
+             rewrite Integers.Ptrofs.add_zero_l.
+             rewrite e.
+             rewrite Integers.Ptrofs.unsigned_repr.
+             exact H1.
+             apply Integers.Ptrofs.unsigned_range_2. }
+        simplify.
+        destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; try constructor.
+        destruct (Archi.ptr64); try discriminate.
+        pose proof (RSBP src). rewrite EQ_SRC in H0.
+        assumption.
+
+        simpl.
+        erewrite Mem.load_store_other with (m1 := m).
+        2: { exact H1. }
+        2: { right.
+             rewrite ZERO.
+             rewrite Integers.Ptrofs.add_zero_l.
+             rewrite Integers.Ptrofs.unsigned_repr.
+             simpl.
+             destruct (Z_le_gt_dec (4 * ptr + 4) (Integers.Ptrofs.unsigned OFFSET)); eauto.
+             right.
+             apply ZExtra.mod_0_bounds; try lia.
+             apply ZLib.Z_mod_mult'.
+             invert H0.
+             apply Zmult_lt_compat_r with (p := 4) in H21; try lia.
+             rewrite ZLib.div_mul_undo in H21; try lia.
+             split; try lia.
+             apply Z.le_trans with (m := RTL.fn_stacksize f); simplify; lia.
+        }
+        apply ASBP; assumption.
+
+      + invert MARR. simplify.
+
+        unfold Op.eval_addressing in H0.
+        destruct (Archi.ptr64) eqn:ARCHI; simplify.
+        rewrite ARCHI in H0. simplify.
+
+        unfold check_address_parameter_unsigned in *;
+        unfold check_address_parameter_signed in *; simplify.
+
+        assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
+        rewrite ZERO in H1. clear ZERO.
+        rewrite Integers.Ptrofs.add_zero_l in H1.
+
+        remember i0 as OFFSET.
+
+        (** Read bounds assumption *)
+        assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH by admit.
+
+        (** Modular preservation proof *)
+        rename H0 into MOD_PRESERVE.
+
+        (** Start of proof proper *)
+        eexists. split.
+        eapply Smallstep.plus_one.
+        eapply HTL.step_module; eauto.
+        econstructor. econstructor. econstructor.
+        eapply Verilog.stmnt_runp_Vnonblock_arr. simplify.
+        econstructor. econstructor. econstructor. econstructor.
+
+        all: simplify.
+
+        (** State Lookup *)
+        unfold Verilog.merge_regs.
+        simplify.
+        unfold_merge.
+        apply AssocMap.gss.
+
+        (** Match states *)
+        rewrite assumption_32bit.
+        econstructor; eauto.
+
+        (** Match assocmaps *)
+        unfold Verilog.merge_regs. simplify. unfold_merge.
+        apply regs_lessdef_add_greater. apply greater_than_max_func.
+        assumption.
+
+        (** States well formed *)
+        unfold state_st_wf. inversion 1. simplify.
+        unfold Verilog.merge_regs.
+        unfold_merge.
+        apply AssocMap.gss.
+
+        (** Match stacks *)
+        admit.
+
+        (** Equality proof *)
+        assert (Z.to_nat
+                  (Integers.Ptrofs.unsigned
+                     (Integers.Ptrofs.divu
+                        OFFSET
+                        (Integers.Ptrofs.repr 4)))
+                =
+                valueToNat (ZToValue 32 (Integers.Ptrofs.unsigned OFFSET / 4)))
+          as EXPR_OK by admit.
+
+        assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
+        inversion MASSOC; revert HeqOFFSET; subst; clear MASSOC; intros HeqOFFSET.
+
+        econstructor.
+        repeat split; simplify.
+        unfold HTL.empty_stack.
+        simplify.
+        unfold Verilog.merge_arrs.
+
+        rewrite AssocMap.gcombine.
+        2: { reflexivity. }
+        unfold Verilog.arr_assocmap_set.
+        rewrite AssocMap.gss.
+        unfold Verilog.merge_arr.
+        rewrite AssocMap.gss.
+        setoid_rewrite H5.
+        reflexivity.
+
+        rewrite combine_length.
+        rewrite <- array_set_len.
+        unfold arr_repeat. simplify.
+        apply list_repeat_len.
+
+        rewrite <- array_set_len.
+        unfold arr_repeat. simplify.
+        rewrite list_repeat_len.
+        rewrite H4. reflexivity.
+
+        intros.
+        destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET).
+
+        erewrite Mem.load_store_same.
+        2: { rewrite ZERO.
+             rewrite Integers.Ptrofs.add_zero_l.
+             rewrite e.
+             rewrite Integers.Ptrofs.unsigned_repr.
+             exact H1.
+             apply Integers.Ptrofs.unsigned_range_2. }
+        constructor.
+        erewrite combine_lookup_second.
+        simpl.
+        assert (Ple src (RTL.max_reg_function f))
+          by (eapply RTL.max_reg_function_use; eauto; simpl; auto);
+        apply H0 in H10.
+        destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; invert H10; eauto.
+
+        rewrite <- array_set_len.
+        unfold arr_repeat. simplify.
+        rewrite list_repeat_len. auto.
+
+        assert (4 * ptr / 4 = Integers.Ptrofs.unsigned OFFSET / 4) by (f_equal; assumption).
+        rewrite Z.mul_comm in H10.
+        rewrite Z_div_mult in H10; try lia.
+        replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) in H10 by reflexivity.
+        rewrite <- PtrofsExtra.divu_unsigned in H10; unfold_constants; try lia.
+        rewrite H10. rewrite EXPR_OK.
+        rewrite array_get_error_set_bound.
+        reflexivity.
+        unfold arr_length, arr_repeat. simpl.
+        rewrite list_repeat_len. lia.
+
+        erewrite Mem.load_store_other with (m1 := m).
+        2: { exact H1. }
+        2: { right.
+             rewrite ZERO.
+             rewrite Integers.Ptrofs.add_zero_l.
+             rewrite Integers.Ptrofs.unsigned_repr.
+             simpl.
+             destruct (Z_le_gt_dec (4 * ptr + 4) (Integers.Ptrofs.unsigned OFFSET)); eauto.
+             right.
+             apply ZExtra.mod_0_bounds; try lia.
+             apply ZLib.Z_mod_mult'.
+             invert H8.
+             rewrite Z2Nat.id in H12; try lia.
+             apply Zmult_lt_compat_r with (p := 4) in H12; try lia.
+             rewrite ZLib.div_mul_undo in H12; try lia.
+             split; try lia.
+             apply Z.le_trans with (m := RTL.fn_stacksize f); simplify; lia.
+        }
+
+        rewrite <- EXPR_OK.
+        rewrite PtrofsExtra.divu_unsigned; auto; try (unfold_constants; lia).
+        destruct (ptr ==Z Integers.Ptrofs.unsigned OFFSET / 4).
+        apply Z.mul_cancel_r with (p := 4) in e; try lia.
+        rewrite ZLib.div_mul_undo in e; try lia.
+        rewrite combine_lookup_first.
+        eapply H7; eauto.
+
+        rewrite <- array_set_len.
+        unfold arr_repeat. simplify.
+        rewrite list_repeat_len. auto.
+        rewrite array_gso.
+        unfold array_get_error.
+        unfold arr_repeat.
+        simplify.
+        apply list_repeat_lookup.
+        lia.
+        unfold_constants.
+        intro.
+        apply Z2Nat.inj_iff in H10; try lia.
+        apply Z.div_pos; try lia.
+        apply Integers.Ptrofs.unsigned_range.
+
+        assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
+        unfold arr_stack_based_pointers.
+        intros.
+        destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET).
+
+        simplify.
+        erewrite Mem.load_store_same.
+        2: { rewrite ZERO.
+             rewrite Integers.Ptrofs.add_zero_l.
+             rewrite e.
+             rewrite Integers.Ptrofs.unsigned_repr.
+             exact H1.
+             apply Integers.Ptrofs.unsigned_range_2. }
+        simplify.
+        destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; try constructor.
+        destruct (Archi.ptr64); try discriminate.
+        pose proof (RSBP src). rewrite EQ_SRC in H0.
+        assumption.
+
+        simpl.
+        erewrite Mem.load_store_other with (m1 := m).
+        2: { exact H1. }
+        2: { right.
+             rewrite ZERO.
+             rewrite Integers.Ptrofs.add_zero_l.
+             rewrite Integers.Ptrofs.unsigned_repr.
+             simpl.
+             destruct (Z_le_gt_dec (4 * ptr + 4) (Integers.Ptrofs.unsigned OFFSET)); eauto.
+             right.
+             apply ZExtra.mod_0_bounds; try lia.
+             apply ZLib.Z_mod_mult'.
+             invert H0.
+             apply Zmult_lt_compat_r with (p := 4) in H10; try lia.
+             rewrite ZLib.div_mul_undo in H10; try lia.
+             split; try lia.
+             apply Z.le_trans with (m := RTL.fn_stacksize f); simplify; lia.
+        }
+        apply ASBP; assumption.
 
     - eexists. split. apply Smallstep.plus_one.
       eapply HTL.step_module; eauto.
diff --git a/src/verilog/Array.v b/src/verilog/Array.v
index fc52f04..f3e1cd7 100644
--- a/src/verilog/Array.v
+++ b/src/verilog/Array.v
@@ -41,6 +41,15 @@ Proof.
 Qed.
 Hint Resolve list_set_spec2 : array.
 
+Lemma list_set_spec3 {A : Type} :
+  forall l i1 i2 (x : A),
+    i1 <> i2 ->
+    nth_error (list_set i1 x l) i2 = nth_error l i2.
+Proof.
+  induction l; intros; destruct i1; destruct i2; simplify; try lia; try reflexivity; firstorder.
+Qed.
+Hint Resolve list_set_spec3 : array.
+
 Lemma array_set_wf {A : Type} :
   forall l ln i (x : A),
     length l = ln -> length (list_set i x l) = ln.
@@ -80,6 +89,13 @@ Proof.
 Qed.
 Hint Resolve array_set_spec2 : array.
 
+Lemma array_set_len {A : Type} :
+  forall a i (x : A),
+    a.(arr_length) = (array_set i x a).(arr_length).
+Proof.
+  unfold array_set. simplify. reflexivity.
+Qed.
+
 Definition array_get_error {A : Type} (i : nat) (a : Array A) : option A :=
   nth_error a.(arr_contents) i.
 
@@ -117,6 +133,19 @@ Proof.
   eauto with array.
 Qed.
 
+Lemma array_gso {A : Type} :
+  forall (a : Array A) i1 i2 x,
+    i1 <> i2 ->
+    array_get_error i2 (array_set i1 x a) = array_get_error i2 a.
+Proof.
+  intros.
+
+  unfold array_get_error.
+  unfold array_set.
+  simplify.
+  eauto with array.
+Qed.
+
 Definition array_get {A : Type} (i : nat) (x : A) (a : Array A) : A :=
   nth i a.(arr_contents) x.
 
@@ -130,6 +159,17 @@ Proof.
   info_eauto with array.
 Qed.
 
+Lemma array_get_get_error {A : Type} :
+  forall (a : Array A) i x d,
+    array_get_error i a = Some x ->
+    array_get i d a = x.
+Proof.
+  intros.
+  unfold array_get.
+  unfold array_get_error in H.
+  auto using nth_error_nth.
+Qed.
+
 (** Tail recursive version of standard library function. *)
 Fixpoint list_repeat' {A : Type} (acc : list A) (a : A) (n : nat) : list A :=
   match n with
@@ -231,6 +271,19 @@ Proof.
   apply list_repeat'_cons.
 Qed.
 
+Lemma list_repeat_lookup {A : Type} :
+  forall n i (a : A),
+    i < n ->
+    nth_error (list_repeat a n) i = Some a.
+Proof.
+  induction n; intros.
+
+  destruct i; simplify; lia.
+
+  rewrite list_repeat_cons.
+  destruct i; simplify; firstorder.
+Qed.
+
 Definition arr_repeat {A : Type} (a : A) (n : nat) : Array A := make_array (list_repeat a n).
 
 Fixpoint list_combine {A B C : Type} (f : A -> B -> C) (x : list A) (y : list B) : list C :=