Merge branch 'dev-nadesh-merge' into dev-nadeshdev-nadesh

24 files changed, 3075 insertions, 423 deletions

diff --git a/Makefile b/Makefile
index 0167a78..1303b13 100644
--- a/Makefile
+++ b/Makefile
@@ -28,7 +28,7 @@ all: lib/COMPCERTSTAMP
 	$(MAKE) compile
 
 lib/COMPCERTSTAMP:
-	(cd lib/CompCert && ./configure $(ARCH))
+	(cd lib/CompCert && ./configure --ignore-coq-version $(ARCH))
 	$(MAKE) -C lib/CompCert
 	touch $@
 
@@ -67,3 +67,4 @@ clean:: Makefile.coq
 
 clean::
 	rm -f */*.v.d */*.glob */*.vo */*~ *~
+	rm -f src/extraction/*.ml src/extraction/*.mli
diff --git a/driver/CoqupDriver.ml b/driver/CoqupDriver.ml
index 2932a50..0b64f48 100644
--- a/driver/CoqupDriver.ml
+++ b/driver/CoqupDriver.ml
@@ -36,11 +36,7 @@ open Coqup.Frontend
 open Coqup.Assembler
 open Coqup.Linker
 open Coqup.Diagnostics
-
-(* Coqup flags *)
-let option_simulate = ref false
-let option_hls = ref true
-let option_debug_hls = ref false
+open Coqup.CoqupClflags
 
 (* Name used for version string etc. *)
 let tool_name = "C verified high-level synthesis"
@@ -69,6 +65,7 @@ let compile_c_file sourcename ifile ofile =
   set_dest Coqup.PrintClight.destination option_dclight ".light.c";
   set_dest Coqup.PrintCminor.destination option_dcminor ".cm";
   set_dest Coqup.PrintRTL.destination option_drtl ".rtl";
+  set_dest Coqup.PrintHTL.destination option_dhtl ".htl";
   set_dest Coqup.Regalloc.destination_alloctrace option_dalloctrace ".alloctrace";
   set_dest Coqup.PrintLTL.destination option_dltl ".ltl";
   set_dest Coqup.PrintMach.destination option_dmach ".mach";
@@ -215,6 +212,7 @@ Processing options:
   --no-hls       Do not use HLS and generate standard flow.
   --simulate     Simulate the result with the Verilog semantics.
   --debug-hls    Add debug logic to the Verilog.
+  --initialise-stack initialise the stack to all 0s.
 |} ^
   prepro_help ^
   language_support_help ^
@@ -256,6 +254,7 @@ Code generation options: (use -fno-<opt> to turn off -f<opt>)
   -dclight       Save generated Clight in <file>.light.c
   -dcminor       Save generated Cminor in <file>.cm
   -drtl          Save RTL at various optimization points in <file>.rtl.<n>
+  -dhtl          Save HTL before Verilog generation <file>.htl
   -dltl          Save LTL after register allocation in <file>.ltl
   -dmach         Save generated Mach code in <file>.mach
   -dasm          Save generated assembly in <file>.s
@@ -316,6 +315,7 @@ let cmdline_actions =
   [Exact "--no-hls", Unset option_hls;
    Exact "--simulate", Set option_simulate;
    Exact "--debug-hls", Set option_debug_hls;
+   Exact "--initialise-stack", Set option_initial;
   ]
 (* Getting version info *)
   @ version_options tool_name @
@@ -379,6 +379,7 @@ let cmdline_actions =
   Exact "-dclight", Set option_dclight;
   Exact "-dcminor", Set option_dcminor;
   Exact "-drtl", Set option_drtl;
+  Exact "-dhtl", Set option_dhtl;
   Exact "-dltl", Set option_dltl;
   Exact "-dalloctrace", Set option_dalloctrace;
   Exact "-dmach", Set option_dmach;
@@ -390,6 +391,7 @@ let cmdline_actions =
     option_dclight := true;
     option_dcminor := true;
     option_drtl := true;
+    option_dhtl := true;
     option_dltl := true;
     option_dalloctrace := true;
     option_dmach := true;
diff --git a/shell.nix b/shell.nix
index f81ded1..3906659 100644
--- a/shell.nix
+++ b/shell.nix
@@ -1,5 +1,5 @@
 with import <nixpkgs> {};
 
 mkShell {
-  buildInputs = (import ./.).buildInputs ++ [ocamlPackages.ocp-indent verilog];
+  buildInputs = (import ./.).buildInputs ++ [ocamlPackages.ocp-indent verilog yosys];
 }
diff --git a/src/Compiler.v b/src/Compiler.v
index f9fe686..513b5fa 100644
--- a/src/Compiler.v
+++ b/src/Compiler.v
@@ -51,6 +51,7 @@ From coqup Require
      HTLgen.
 
 Parameter print_RTL: Z -> RTL.program -> unit.
+Parameter print_HTL: HTL.program -> unit.
 
 Definition print {A: Type} (printer: A -> unit) (prog: A) : A :=
   let unused := printer prog in prog.
@@ -86,6 +87,7 @@ Definition transf_backend (r : RTL.program) : res Verilog.program :=
   @@@ Unusedglob.transform_program
   @@ print (print_RTL 1)
   @@@ HTLgen.transl_program
+  @@ print print_HTL
   @@ Veriloggen.transl_program.
 
 (* Unoptimised below: *)
diff --git a/src/CoqupClflags.ml b/src/CoqupClflags.ml
new file mode 100644
index 0000000..5b40ce6
--- /dev/null
+++ b/src/CoqupClflags.ml
@@ -0,0 +1,6 @@
+(* Coqup flags *)
+let option_simulate = ref false
+let option_hls = ref true
+let option_debug_hls = ref false
+let option_initial = ref false
+let option_dhtl = ref false
diff --git a/src/common/Coquplib.v b/src/common/Coquplib.v
index 47360d6..c9361c2 100644
--- a/src/common/Coquplib.v
+++ b/src/common/Coquplib.v
@@ -23,11 +23,14 @@ From Coq Require Export
      List
      Bool.
 
+Require Import Lia.
+
 From coqup Require Import Show.
 
 (* Depend on CompCert for the basic library, as they declare and prove some
    useful theorems. *)
 From compcert.lib Require Export Coqlib.
+From compcert Require Import Integers.
 
 Ltac unfold_rec c := unfold c; fold c.
 
@@ -41,6 +44,101 @@ Ltac solve_by_inverts n :=
 
 Ltac solve_by_invert := solve_by_inverts 1.
 
+Ltac invert x := inversion x; subst; clear x.
+
+Ltac destruct_match :=
+  match goal with | [ |- context[match ?x with | _ => _ end ] ] => destruct x end.
+
+Ltac clear_obvious :=
+  repeat match goal with
+         | [ H : ex _ |- _ ] => invert H
+         | [ H : Some _ = Some _ |- _ ] => invert H
+         | [ H : _ /\ _ |- _ ] => invert H
+         end.
+
+Ltac nicify_goals :=
+  repeat match goal with
+         | [ |- _ /\ _ ] => split
+         | [ |- Some _ = Some _ ] => f_equal
+         | [ |- S _ = S _ ] => f_equal
+         end.
+
+Ltac kill_bools :=
+  repeat match goal with
+         | [ H : _ && _ = true |- _ ] => apply andb_prop in H
+         | [ H : _ || _ = false |- _ ] => apply orb_false_elim in H
+
+         | [ H : _ <=? _ = true |- _ ] => apply Z.leb_le in H
+         | [ H : _ <=? _ = false |- _ ] => apply Z.leb_gt in H
+         | [ H : _ <? _ = true |- _ ] => apply Z.ltb_lt in H
+         | [ H : _ <? _ = false |- _ ] => apply Z.ltb_ge in H
+         | [ H : _ >=? _ = _ |- _ ] => rewrite Z.geb_leb in H
+         | [ H : _ >? _ = _ |- _ ] => rewrite Z.gtb_ltb in H
+
+         | [ H : _ =? _ = true |- _ ] => apply Z.eqb_eq in H
+         | [ H : _ =? _ = false |- _ ] => apply Z.eqb_neq in H
+         end.
+
+Ltac unfold_constants :=
+  repeat match goal with
+         | [ |- 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] ] =>
+           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] ] =>
+           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] ] =>
+           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] ] =>
+           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] ] =>
+           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] ] =>
+           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] ] =>
+           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 crush := intros; unfold_constants; simpl in *;
+              repeat (clear_obvious; nicify_goals; kill_bools);
+              simpl in *; try discriminate; try congruence; try lia; try assumption.
+
+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). *)
@@ -71,6 +169,12 @@ Definition bind {A B : Type} (f : option A) (g : A -> option B) : option B :=
   | _ => None
   end.
 
+Definition join {A : Type} (a : option (option A)) : option A :=
+  match a with
+  | None => None
+  | Some a' => a'
+  end.
+
 Module Notation.
 Notation "'do' X <- A ; B" := (bind A (fun X => B))
    (at level 200, X ident, A at level 100, B at level 200).
diff --git a/src/common/IntegerExtra.v b/src/common/IntegerExtra.v
new file mode 100644
index 0000000..6bac18d
--- /dev/null
+++ b/src/common/IntegerExtra.v
@@ -0,0 +1,283 @@
+Require Import BinInt.
+Require Import Lia.
+Require Import ZBinary.
+
+From bbv Require Import ZLib.
+From compcert Require Import Integers Coqlib.
+
+Require Import Coquplib.
+
+Local Open Scope Z_scope.
+
+Module PtrofsExtra.
+
+  Ltac ptrofs_mod_match m :=
+    match goal with
+    | [ H : ?x = 0 |- context[?x] ] => rewrite H
+    | [ _ : _ |- context[_ - 0] ] => rewrite Z.sub_0_r
+    | [ _ : _ |- context[0 + _] ] => rewrite Z.add_0_l
+    | [ _ : _ |- context[_ + 0] ] => rewrite Z.add_0_r
+    | [ _ : _ |- context[0 * _] ] => rewrite Z.mul_0_l
+    | [ _ : _ |- context[_ * 0] ] => rewrite Z.mul_0_r
+    | [ _ : _ |- context[?m mod ?m] ] =>
+      rewrite Z_mod_same_full with (a := m)
+    | [ _ : _ |- context[0 mod _] ] =>
+      rewrite Z.mod_0_l
+    | [ _ : _ |- context[(_ mod ?m) mod ?m] ] =>
+      rewrite Zmod_mod
+    | [ _ : _ |- context[(_ mod Ptrofs.modulus) mod m ] ] =>
+      rewrite <- Zmod_div_mod;
+      try (crush; lia || assumption)
+
+    | [ _ : _ |- context[Ptrofs.modulus mod m] ] =>
+      rewrite Zdivide_mod with (a := Ptrofs.modulus);
+      try (lia || assumption)
+
+    | [ _ : _ |- context[Ptrofs.signed ?a mod Ptrofs.modulus] ] =>
+      rewrite Z.mod_small with (a := Ptrofs.signed a) (b := Ptrofs.modulus)
+
+    | [ _ : _ |- context[(?x - ?y) mod ?m] ] =>
+      rewrite Zminus_mod with (a := x) (b := y) (n := m)
+
+    | [ _ : _ |- context[((?x + ?y) mod ?m) + _] ] =>
+      rewrite Zplus_mod with (a := x) (b := y) (n := m)
+    | [ _ : _ |- context[(?x + ?y) mod ?m] ] =>
+      rewrite Zplus_mod with (a := x) (b := y) (n := m)
+
+    | [ _ : _ |- context[(?x * ?y) mod ?m] ] =>
+      rewrite Zmult_mod with (a := x) (b := y) (n := m)
+    end.
+
+  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 crush; ptrofs_mod_tac m.
+  Qed.
+
+  Lemma of_int_mod :
+    forall x m,
+      Int.signed x mod m = 0 ->
+      Ptrofs.signed (Ptrofs.of_int x) mod m = 0.
+  Proof.
+    intros.
+    pose proof (Integers.Ptrofs.agree32_of_int eq_refl x) as A.
+    pose proof Ptrofs.agree32_signed.
+    apply H0 in A; try reflexivity.
+    rewrite A. assumption.
+  Qed.
+
+  Lemma mul_mod :
+    forall x y m,
+      0 < m ->
+      (m | Ptrofs.modulus) ->
+      Ptrofs.signed x mod m = 0 ->
+      Ptrofs.signed y mod m = 0 ->
+      (Ptrofs.signed (Ptrofs.mul x y)) mod m = 0.
+  Proof.
+    intros. unfold Ptrofs.mul.
+    rewrite Ptrofs.signed_repr_eq.
+
+    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(crush; lia); ptrofs_mod_tac m.
+  Qed.
+
+  Lemma add_mod :
+    forall x y m,
+      0 < m ->
+      (m | Ptrofs.modulus) ->
+      Ptrofs.signed x mod m = 0 ->
+      Ptrofs.signed y mod m = 0 ->
+      (Ptrofs.unsigned (Ptrofs.add x y)) mod m = 0.
+  Proof.
+    intros. unfold Ptrofs.add.
+    rewrite Ptrofs.unsigned_repr_eq.
+
+    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 (crush; lia); ptrofs_mod_tac m.
+  Qed.
+
+  Lemma mul_divu :
+    forall 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.
+
+    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.
+    exact H0.
+    rewrite Z.mul_comm.
+    apply Z.le_mul_diag_r; crush.
+  Qed.
+
+  Lemma mul_unsigned :
+    forall x y,
+      Ptrofs.mul x y =
+      Ptrofs.repr (Ptrofs.unsigned x * Ptrofs.unsigned y).
+  Proof.
+    intros; unfold Ptrofs.mul.
+    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.
+
+Ltac ptrofs :=
+  repeat match goal with
+         | [ |- context[Ptrofs.add (Ptrofs.zero) _] ] => setoid_rewrite Ptrofs.add_zero_l
+         | [ H : context[Ptrofs.add (Ptrofs.zero) _] |- _ ] => setoid_rewrite Ptrofs.add_zero_l in H
+
+         | [ |- context[Ptrofs.repr 0] ] => replace (Ptrofs.repr 0) with Ptrofs.zero by reflexivity
+         | [ H : context[Ptrofs.repr 0] |- _ ] =>
+           replace (Ptrofs.repr 0) with Ptrofs.zero in H by reflexivity
+
+         | [ H: context[Ptrofs.unsigned (Ptrofs.repr (Ptrofs.unsigned _))] |- _ ] =>
+           setoid_rewrite Ptrofs.unsigned_repr in H; [>| apply Ptrofs.unsigned_range_2]
+         | [ |- context[Ptrofs.unsigned (Ptrofs.repr (Ptrofs.unsigned _))] ] =>
+           rewrite Ptrofs.unsigned_repr; [>| apply Ptrofs.unsigned_range_2]
+
+         | [ |- context[0 <= Ptrofs.unsigned _] ] => apply Ptrofs.unsigned_range_2
+         end.
+
+Module IntExtra.
+
+  Ltac int_mod_match m :=
+    match goal with
+    | [ H : ?x = 0 |- context[?x] ] => rewrite H
+    | [ _ : _ |- context[_ - 0] ] => rewrite Z.sub_0_r
+    | [ _ : _ |- context[0 + _] ] => rewrite Z.add_0_l
+    | [ _ : _ |- context[_ + 0] ] => rewrite Z.add_0_r
+    | [ _ : _ |- context[0 * _] ] => rewrite Z.mul_0_l
+    | [ _ : _ |- context[_ * 0] ] => rewrite Z.mul_0_r
+    | [ _ : _ |- context[?m mod ?m] ] =>
+      rewrite Z_mod_same_full with (a := m)
+    | [ _ : _ |- context[0 mod _] ] =>
+      rewrite Z.mod_0_l
+    | [ _ : _ |- context[(_ mod ?m) mod ?m] ] =>
+      rewrite Zmod_mod
+    | [ _ : _ |- context[(_ mod Int.modulus) mod m ] ] =>
+      rewrite <- Zmod_div_mod;
+      try (crush; lia || assumption)
+
+    | [ _ : _ |- context[Int.modulus mod m] ] =>
+      rewrite Zdivide_mod with (a := Int.modulus);
+      try (lia || assumption)
+
+    | [ _ : _ |- context[Int.signed ?a mod Int.modulus] ] =>
+      rewrite Z.mod_small with (a := Int.signed a) (b := Int.modulus)
+
+    | [ _ : _ |- context[(?x - ?y) mod ?m] ] =>
+      rewrite Zminus_mod with (a := x) (b := y) (n := m)
+
+    | [ _ : _ |- context[((?x + ?y) mod ?m) + _] ] =>
+      rewrite Zplus_mod with (a := x) (b := y) (n := m)
+    | [ _ : _ |- context[(?x + ?y) mod ?m] ] =>
+      rewrite Zplus_mod with (a := x) (b := y) (n := m)
+
+    | [ _ : _ |- context[(?x * ?y) mod ?m] ] =>
+      rewrite Zmult_mod with (a := x) (b := y) (n := m)
+    end.
+
+  Ltac int_mod_tac m :=
+    repeat (int_mod_match m); lia.
+
+  Lemma mul_mod :
+    forall x y m,
+      0 < m ->
+      (m | Int.modulus) ->
+      Int.signed x mod m = 0 ->
+      Int.signed y mod m = 0 ->
+      (Int.signed (Int.mul x y)) mod m = 0.
+  Proof.
+    intros. unfold Int.mul.
+    rewrite Int.signed_repr_eq.
+
+    repeat match goal with
+           | [ _ : _ |- context[if ?x then _ else _] ] => destruct x
+           | [ _ : _ |- context[_ mod Int.modulus mod m] ] =>
+             rewrite <- Zmod_div_mod; try lia; try assumption
+           | [ _ : _ |- context[Int.unsigned _] ] => rewrite Int.unsigned_signed
+           end; try (crush; lia); int_mod_tac m.
+  Qed.
+
+  Lemma add_mod :
+    forall x y m,
+      0 < m ->
+      (m | Int.modulus) ->
+      Int.signed x mod m = 0 ->
+      Int.signed y mod m = 0 ->
+      (Int.signed (Int.add x y)) mod m = 0.
+  Proof.
+    intros. unfold Int.add.
+    rewrite Int.signed_repr_eq.
+
+    repeat match goal with
+           | [ _ : _ |- context[if ?x then _ else _] ] => destruct x
+           | [ _ : _ |- context[_ mod Int.modulus mod m] ] =>
+             rewrite <- Zmod_div_mod; try lia; try assumption
+           | [ _ : _ |- context[Int.unsigned _] ] => rewrite Int.unsigned_signed
+           end; try (crush; lia); int_mod_tac m.
+  Qed.
+End IntExtra.
diff --git a/src/common/ZExtra.v b/src/common/ZExtra.v
new file mode 100644
index 0000000..a0dd717
--- /dev/null
+++ b/src/common/ZExtra.v
@@ -0,0 +1,34 @@
+Require Import ZArith.
+Require Import Lia.
+
+Local Open Scope Z_scope.
+
+Module ZExtra.
+
+  Lemma mod_0_bounds :
+    forall x y m,
+      0 < m ->
+      x mod m = 0 ->
+      y mod m = 0 ->
+      x <> y ->
+      x + m > y ->
+      y + m <= x.
+  Proof.
+    intros x y m.
+    intros POS XMOD YMOD NEQ H.
+    destruct (Z_le_gt_dec (y + m) x); eauto.
+
+    apply Znumtheory.Zmod_divide in YMOD; try lia.
+    apply Znumtheory.Zmod_divide in XMOD; try lia.
+    inversion XMOD as [x']; subst; clear XMOD.
+    inversion YMOD as [y']; subst; clear YMOD.
+
+    assert (x' <> y') as NEQ' by lia; clear NEQ.
+
+    rewrite <- Z.mul_succ_l in H.
+    rewrite <- Z.mul_succ_l in g.
+    apply Zmult_gt_reg_r in H;
+      apply Zmult_gt_reg_r in g; lia.
+  Qed.
+
+End ZExtra.
diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v
index ba87af6..df21dc4 100644
--- a/src/extraction/Extraction.v
+++ b/src/extraction/Extraction.v
@@ -128,6 +128,7 @@ Extract Constant Compiler.print_Clight => "PrintClight.print_if".
 Extract Constant Compiler.print_Cminor => "PrintCminor.print_if".
 Extract Constant driver.Compiler.print_RTL => "PrintRTL.print_if".
 Extract Constant Compiler.print_RTL => "PrintRTL.print_if".
+Extract Constant Compiler.print_HTL => "PrintHTL.print_if".
 Extract Constant Compiler.print_LTL => "PrintLTL.print_if".
 Extract Constant Compiler.print_Mach => "PrintMach.print_if".
 Extract Constant Compiler.print => "fun (f: 'a -> unit) (x: 'a) -> f x; x".
diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v
index c96d4c7..4cde0c8 100644
--- a/src/translation/HTLgen.v
+++ b/src/translation/HTLgen.v
@@ -17,7 +17,7 @@
  *)
 
 From compcert Require Import Maps.
-From compcert Require Errors Globalenvs.
+From compcert Require Errors Globalenvs Integers.
 From compcert Require Import AST RTL.
 From coqup Require Import Verilog HTL Coquplib AssocMap Value Statemonad.
 
@@ -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))
@@ -280,19 +280,39 @@ 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_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
-  | Op.Aindexed off, r1::nil => ret (boplitz Vadd r1 off)
-  | Op.Aindexed2 off, r1::r2::nil => ret (Vbinop Vadd (Vvar r1) (boplitz Vadd r2 off))
+  match a, args with (* TODO: We should be more methodical here; what are the possibilities?*)
+  | Op.Aindexed off, r1::nil =>
+    if (check_address_parameter_signed off)
+    then ret (boplitz Vadd r1 off)
+    else error (Errors.msg "Veriloggen: translate_eff_addressing (Aindexed): address misaligned")
   | Op.Ascaled scale offset, r1::nil =>
-    ret (Vbinop Vadd (boplitz Vmul r1 scale) (Vlit (ZToValue 32 offset)))
-  | Op.Aindexed2scaled scale offset, r1::r2::nil =>
-    ret (Vbinop Vadd (boplitz Vadd r1 offset) (boplitz Vmul r2 scale))
-  (* Stack arrays/referenced variables *)
+    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 (Ascaled): address misaligned")
+  | Op.Aindexed2 offset, r1::r2::nil =>
+    if (check_address_parameter_signed offset)
+    then ret (Vbinop Vadd (Vvar r1) (boplitz Vadd r2 offset))
+    else error (Errors.msg "Veriloggen: translate_eff_addressing (Aindexed2): address misaligned")
+  | Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *)
+    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 (Aindexed2scaled): address misaligned")
   | 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? *)
-    ret (Vlit (ZToValue 32 a))
-  | _, _ => error (Errors.msg "Htlgen: eff_addressing instruction not implemented: other")
+    let a := Integers.Ptrofs.unsigned a in
+    if (check_address_parameter_unsigned a)
+    then ret (Vlit (ZToValue 32 a))
+    else error (Errors.msg "Veriloggen: translate_eff_addressing (Ainstack): address misaligned")
+  | _, _ => error (Errors.msg "Veriloggen: translate_eff_addressing unsuported addressing")
   end.
 
 (** Translate an instruction to a statement. FIX mulhs mulhu *)
@@ -374,24 +394,24 @@ 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 => (* FIXME: Cannot guarantee alignment *)
-    ret (Vvari stack (Vbinop Vadd (boplitz Vdiv r1 4) (Vlit (ZToValue 32 (off / 4)))))
-  | 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 "Htlgen: translate_arr_access address misaligned")
-  | 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))
+  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_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_signed scale) && (check_address_parameter_signed offset)
     then ret (Vvari stack
-                    (Vbinop Vadd (Vbinop Vadd (boplitz Vdiv r1 4) (Vlit (ZToValue 32 (offset / 4))))
-                                 (boplitz Vmul r2 (scale / 4))))
-    else error (Errors.msg "Htlgen: translate_arr_access address misaligned")
-  | 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 "Htlgen: eff_addressing misaligned stack offset")
-  | _, _ => error (Errors.msg "Htlgen: translate_arr_access unsupported addressing")
+                    (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.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")
   end.
 
 Fixpoint enumerate (i : nat) (ns : list node) {struct ns} : list (nat * node) :=
@@ -418,10 +438,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.")
@@ -447,7 +467,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)).
@@ -459,7 +479,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))
@@ -472,27 +492,31 @@ 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.
 
-Definition create_arr (i : option io) (sz : nat) (ln : nat) : mon reg :=
+Definition create_arr (i : option io) (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)
                    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).
 
+Definition stack_correct (sz : Z) : bool :=
+  (0 <=? sz) && (sz <? Integers.Ptrofs.modulus) && (Z.modulo sz 4 =? 0).
+
 Definition transf_module (f: function) : mon module :=
+  if stack_correct f.(fn_stacksize) then
   do fin <- create_reg (Some Voutput) 1;
   do rtrn <- create_reg (Some Voutput) 32;
-  do stack <- create_arr None 32 (Z.to_nat (f.(fn_stacksize) / 4));
+  do (stack, stack_len) <- create_arr None 32 (Z.to_nat (f.(fn_stacksize) / 4));
   do _ <- collectlist (transf_instr fin rtrn stack) (Maps.PTree.elements f.(RTL.fn_code));
   do _ <- collectlist (fun r => declare_reg (Some Vinput) r 32) f.(RTL.fn_params);
   do start <- create_reg (Some Vinput) 1;
@@ -506,20 +530,22 @@ Definition transf_module (f: function) : mon module :=
          f.(fn_entrypoint)
          current_state.(st_st)
          stack
+         stack_len
          fin
          rtrn
          start
          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
   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)).
@@ -529,7 +555,7 @@ Definition transl_module (f : function) : Errors.res module :=
 
 Definition transl_fundef := transf_partial_fundef transl_module.
 
-Definition transl_program (p : RTL.program) := transform_partial_program transl_fundef p.
+(* Definition transl_program (p : RTL.program) := transform_partial_program transl_fundef p. *)
 
 (*Definition transl_main_fundef f : Errors.res HTL.fundef :=
   match f with
@@ -546,11 +572,18 @@ Definition transl_program (p: RTL.program) : Errors.res HTL.program :=
                              (fun i v => Errors.OK v) p.
 *)
 
-(*Definition main_is_internal (p : RTL.program): Prop :=
+Definition main_is_internal (p : RTL.program) : bool :=
   let ge := Globalenvs.Genv.globalenv p in
-  forall b m,
-  Globalenvs.Genv.find_symbol ge p.(AST.prog_main) = Some b ->
-  Globalenvs.Genv.find_funct_ptr ge b = Some (AST.Internal m).
+  match Globalenvs.Genv.find_symbol ge p.(AST.prog_main) with
+  | Some b =>
+    match Globalenvs.Genv.find_funct_ptr ge b with
+    | Some (AST.Internal _) => true
+    | _ => false
+    end
+  | _ => false
+  end.
 
-Definition tranls_program_with_proof (p : RTL.program) : Errors.res { p' : HTL.program | main_is_internal p }.
-*)
+Definition transl_program (p : RTL.program) : Errors.res HTL.program :=
+  if main_is_internal p
+  then transform_partial_program transl_fundef p
+  else Errors.Error (Errors.msg "Main function is not Internal.").
diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v
index 9786d23..6e470d5 100644
--- a/src/translation/HTLgenproof.v
+++ b/src/translation/HTLgenproof.v
@@ -18,9 +18,11 @@
 
 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 IntegerExtra ZExtra.
 From coqup Require HTL Verilog.
 
+Require Import Lia.
+
 Local Open Scope assocmap.
 
 Hint Resolve Smallstep.forward_simulation_plus : htlproof.
@@ -42,44 +44,80 @@ 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) ->
-    asa ! (m.(HTL.mod_stk)) = Some stack ->
+Inductive match_arrs (m : HTL.module) (f : RTL.function) (sp : Values.val) (mem : mem) :
+  Verilog.assocmap_arr -> Prop :=
+| match_arr : forall asa stack,
+    asa ! (m.(HTL.mod_stk)) = Some stack /\
+    stack.(arr_length) = Z.to_nat (f.(RTL.fn_stacksize) / 4) /\
     (forall ptr,
-        0 <= ptr < sz ->
-        nth_error stack (Z.to_nat ptr) =
-        (Coquplib.Option.bind (Mem.loadv AST.Mint32 mem
-                                         (Values.Val.offset_ptr sp (Integers.Ptrofs.repr ptr)))
-         valToValue)) ->
-    match_arrs m f mem asa.
+        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 (4 * ptr))))
+                              (Option.default (NToValue 32 0)
+                                 (Option.join (array_get_error (Z.to_nat ptr) stack)))) ->
+    match_arrs m f sp mem asa.
+
+Definition stack_based (v : Values.val) (sp : Values.block) : Prop :=
+   match v with
+   | Values.Vptr sp' off => sp' = sp
+   | _ => True
+   end.
+
+Definition reg_stack_based_pointers (sp : Values.block) (rs : Registers.Regmap.t Values.val) : Prop :=
+  forall r, stack_based (Registers.Regmap.get r rs) sp.
+
+Definition arr_stack_based_pointers (spb : Values.block) (m : mem) (stack_length : Z)
+  (sp : Values.val) : Prop :=
+  forall ptr,
+    0 <= ptr < (stack_length / 4) ->
+    stack_based (Option.default
+                   Values.Vundef
+                   (Mem.loadv AST.Mint32 m
+                              (Values.Val.offset_ptr sp (Integers.Ptrofs.repr (4 * ptr)))))
+                spb.
+
+Definition stack_bounds (sp : Values.val) (hi : Z) (m : mem) : Prop :=
+  forall ptr v,
+    hi <= ptr <= Integers.Ptrofs.max_unsigned ->
+    Z.modulo ptr 4 = 0 ->
+    Mem.loadv AST.Mint32 m (Values.Val.offset_ptr sp (Integers.Ptrofs.repr ptr )) = None /\
+    Mem.storev AST.Mint32 m (Values.Val.offset_ptr sp (Integers.Ptrofs.repr ptr )) v = None.
+
+Inductive match_frames : list RTL.stackframe -> list HTL.stackframe -> Prop :=
+| match_frames_nil :
+    match_frames nil nil.
+(* | match_frames_cons : *)
+(*     forall cs lr r f sp sp' pc rs m asr asa *)
+(*            (TF : tr_module f m) *)
+(*            (ST: match_frames mem cs lr) *)
+(*            (MA: match_assocmaps f rs asr) *)
+(*            (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) *)
+(*            (BOUNDS : stack_bounds sp (f.(RTL.fn_stacksize)) mem), *)
+(*       match_frames 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
+| 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 sf res)
-    (MA : match_arrs m f mem asa),
+    (MF : match_frames sf res)
+    (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)
+    (BOUNDS : stack_bounds sp (f.(RTL.fn_stacksize)) mem),
     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
+      (MF : match_frames 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),
@@ -87,12 +125,23 @@ Inductive match_states : RTL.state -> HTL.state -> Prop :=
 Hint Constructors match_states : htlproof.
 
 Definition match_prog (p: RTL.program) (tp: HTL.program) :=
-  Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq p tp.
+  Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq p tp /\
+  main_is_internal p = true.
+
+Definition match_prog_matches :
+  forall p tp,
+    match_prog p tp ->
+    Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq p tp.
+  Proof. intros. unfold match_prog in H. tauto. Qed.
 
 Lemma transf_program_match:
   forall p tp, HTLgen.transl_program p = Errors.OK tp -> match_prog p tp.
 Proof.
-  intros. apply Linking.match_transform_partial_program; auto.
+  intros. unfold transl_program in H.
+  destruct (main_is_internal p) eqn:?; try discriminate.
+  unfold match_prog. split.
+  apply Linking.match_transform_partial_program; auto.
+  assumption.
 Qed.
 
 Lemma regs_lessdef_add_greater :
@@ -129,6 +178,94 @@ 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; crush.
+  - symmetry. apply length_zero_iff_nil. auto.
+  - destruct l; crush.
+    rewrite list_repeat_cons.
+    crush. 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.
+  crush.
+
+  rewrite <- (arr_wf a) in H.
+  apply list_combine_none.
+  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; crush.
+
+  rewrite nth_error_nil in H0.
+  discriminate.
+
+  destruct l2 eqn:EQl2. crush.
+  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; crush; auto.
+
+  destruct l2 eqn:EQl2. crush.
+  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,
@@ -198,6 +335,17 @@ Proof.
     constructor.
 Qed.
 
+Lemma arr_lookup_some:
+  forall (z : Z) (r0 : Registers.reg) (r : Verilog.reg) (asr : assocmap) (asa : Verilog.assocmap_arr)
+    (stack : Array (option value)) (H5 : asa ! r = Some stack) n,
+    exists x, Verilog.arr_assocmap_lookup asa r n = Some x.
+Proof.
+  intros z r0 r asr asa stack H5 n.
+  eexists.
+  unfold Verilog.arr_assocmap_lookup. rewrite H5. reflexivity.
+Qed.
+Hint Resolve arr_lookup_some : htlproof.
+
 Section CORRECTNESS.
 
   Variable prog : RTL.program.
@@ -205,13 +353,16 @@ Section CORRECTNESS.
 
   Hypothesis TRANSL : match_prog prog tprog.
 
-(*  Let ge : RTL.genv := Globalenvs.Genv.globalenv prog.
+  Lemma TRANSL' :
+    Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq prog tprog.
+  Proof. intros; apply match_prog_matches; assumption. Qed.
+
+  Let ge : RTL.genv := Globalenvs.Genv.globalenv prog.
   Let tge : HTL.genv := Globalenvs.Genv.globalenv tprog.
 
   Lemma symbols_preserved:
     forall (s: AST.ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
-  Proof
-    (Genv.find_symbol_transf_partial TRANSL).
+  Proof. intros. eapply (Genv.find_symbol_match TRANSL'). Qed.
 
   Lemma function_ptr_translated:
     forall (b: Values.block) (f: RTL.fundef),
@@ -219,7 +370,7 @@ Section CORRECTNESS.
       exists tf,
         Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = Errors.OK tf.
   Proof.
-    intros. exploit (Genv.find_funct_ptr_match TRANSL); eauto.
+    intros. exploit (Genv.find_funct_ptr_match TRANSL'); eauto.
     intros (cu & tf & P & Q & R); exists tf; auto.
   Qed.
 
@@ -229,21 +380,21 @@ Section CORRECTNESS.
       exists tf,
         Genv.find_funct tge v = Some tf /\ transl_fundef f = Errors.OK tf.
   Proof.
-    intros. exploit (Genv.find_funct_match TRANSL); eauto.
+    intros. exploit (Genv.find_funct_match TRANSL'); eauto.
     intros (cu & tf & P & Q & R); exists tf; auto.
   Qed.
 
   Lemma senv_preserved:
     Senv.equiv (Genv.to_senv ge) (Genv.to_senv tge).
   Proof
-    (Genv.senv_transf_partial TRANSL).
+    (Genv.senv_transf_partial TRANSL').
   Hint Resolve senv_preserved : htlproof.
 
   Lemma eval_correct :
-    forall sp op rs args m v v' e asr asa f,
+    forall sp op rs args m v v' e asr asa f s s' i,
       Op.eval_operation ge sp op
 (List.map (fun r : BinNums.positive => Registers.Regmap.get r rs) args) m = Some v ->
-      tr_op op args e ->
+      translate_instr op args s = OK e s' i ->
       val_value_lessdef v v' ->
       Verilog.expr_runp f asr asa e v'.
   Admitted.
@@ -281,171 +432,1470 @@ Section CORRECTNESS.
       exists asr' asa',
         HTL.step tge (HTL.State res m st asr asa) Events.E0 (HTL.State res m st asr' asa').
 
-  Theorem transl_step_correct:
-    forall (S1 : RTL.state) t S2,
-      RTL.step ge S1 t S2 ->
-      forall (R1 : HTL.state),
-        match_states S1 R1 ->
-        exists R2, Smallstep.plus HTL.step tge R1 t R2 /\ match_states S2 R2.
+  Opaque combine.
+
+  Ltac tac0 :=
+    match goal with
+    | [ |- context[valueToPos (posToValue 32 _)] ] => rewrite assumption_32bit
+
+    | [ |- context[Verilog.merge_arrs _ _] ] => unfold Verilog.merge_arrs
+    | [ |- context[Verilog.merge_arr] ] => unfold Verilog.merge_arr
+    | [ |- context[Verilog.merge_regs _ _] ] => unfold Verilog.merge_regs; crush; unfold_merge
+    | [ |- context[reg_stack_based_pointers] ] => unfold reg_stack_based_pointers; intros
+    | [ |- context[Verilog.arr_assocmap_set _ _ _ _] ] => unfold Verilog.arr_assocmap_set
+
+    | [ |- context[HTL.empty_stack] ] => unfold HTL.empty_stack
+
+    | [ |- context[_ # ?d <- _ ! ?d] ] => rewrite AssocMap.gss
+    | [ |- context[_ # ?d <- _ ! ?s] ] => rewrite AssocMap.gso
+    | [ |- context[(AssocMap.empty _) ! _] ] => rewrite AssocMap.gempty
+
+    | [ |- context[array_get_error _ (combine Verilog.merge_cell (arr_repeat None _) _)] ] =>
+      rewrite combine_lookup_first
+
+    | [ |- state_st_wf _ _ ] => unfold state_st_wf; inversion 1
+    | [ |- context[match_states _ _] ] => econstructor; auto
+    | [ |- match_arrs _ _ _ _ _ ] => econstructor; auto
+    | [ |- match_assocmaps _ _ _ # _ <- (posToValue 32 _) ] =>
+      apply regs_lessdef_add_greater; [> apply greater_than_max_func | assumption]
+
+    | [ H : ?asa ! ?r = Some _ |- Verilog.arr_assocmap_lookup ?asa ?r _ = Some _ ] =>
+      unfold Verilog.arr_assocmap_lookup; setoid_rewrite H; f_equal
+    | [ |- context[(AssocMap.combine _ _ _) ! _] ] =>
+      try (rewrite AssocMap.gcombine; [> | reflexivity])
+
+    | [ |- context[Registers.Regmap.get ?d (Registers.Regmap.set ?d _ _)] ] =>
+      rewrite Registers.Regmap.gss
+    | [ |- context[Registers.Regmap.get ?s (Registers.Regmap.set ?d _ _)] ] =>
+      destruct (Pos.eq_dec s d) as [EQ|EQ];
+      [> rewrite EQ | rewrite Registers.Regmap.gso; auto]
+
+    | [ H : opt_val_value_lessdef _ _ |- _ ] => invert H
+    | [ H : context[Z.of_nat (Z.to_nat _)] |- _ ] => rewrite Z2Nat.id in H; [> solve crush |]
+    | [ H : _ ! _ = Some _ |- _] => setoid_rewrite H
+    end.
+
+  Ltac small_tac := repeat (crush; try array; try ptrofs); crush; auto.
+  Ltac big_tac := repeat (crush; try array; try ptrofs; try tac0); crush; auto.
+
+  Lemma transl_inop_correct:
+    forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive)
+      (rs : RTL.regset) (m : mem) (pc' : RTL.node),
+      (RTL.fn_code f) ! pc = Some (RTL.Inop pc') ->
+      forall R1 : HTL.state,
+        match_states (RTL.State s f sp pc rs m) R1 ->
+        exists R2 : HTL.state,
+          Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ match_states (RTL.State s f sp pc' rs m) R2.
   Proof.
-    induction 1; intros R1 MSTATE; try inv_state.
-    - (* Inop *)
-      unfold match_prog in TRANSL.
-      econstructor.
-      split.
-      apply Smallstep.plus_one.
+    intros s f sp pc rs m pc' H R1 MSTATE.
+    inv_state.
+
+    unfold match_prog in TRANSL.
+    econstructor.
+    split.
+    apply Smallstep.plus_one.
+    eapply HTL.step_module; eauto.
+    apply assumption_32bit.
+    (* processing of state *)
+    econstructor.
+    crush.
+    econstructor.
+    econstructor.
+    econstructor.
+
+    all: invert MARR; big_tac.
+    Unshelve.
+    constructor.
+  Qed.
+  Hint Resolve transl_inop_correct : htlproof.
+
+  Lemma transl_iop_correct:
+    forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive)
+      (rs : Registers.Regmap.t Values.val) (m : mem) (op : Op.operation) (args : list Registers.reg)
+      (res0 : Registers.reg) (pc' : RTL.node) (v : Values.val),
+      (RTL.fn_code f) ! pc = Some (RTL.Iop op args res0 pc') ->
+      Op.eval_operation ge sp op (map (fun r : positive => Registers.Regmap.get r rs) args) m = Some v ->
+      forall R1 : HTL.state,
+        match_states (RTL.State s f sp pc rs m) R1 ->
+        exists R2 : HTL.state,
+          Smallstep.plus HTL.step tge R1 Events.E0 R2 /\
+          match_states (RTL.State s f sp pc' (Registers.Regmap.set res0 v rs) m) R2.
+  Proof.
+    intros s f sp pc rs m op args res0 pc' v H H0.
+
+    (* Iop *)
+    (* destruct v eqn:?; *)
+    (*          try ( *)
+    (*            destruct op eqn:?; inversion H21; simpl in H0; repeat (unfold_match H0); *)
+    (*            inversion H0; subst; simpl in *; try (unfold_func H4); try (unfold_func H5); *)
+    (*            try (unfold_func H6); *)
+    (*            try (unfold Op.eval_addressing32 in H6; repeat (unfold_match H6); inversion H6; *)
+    (*                 unfold_func H3); *)
+
+    (*            inversion Heql; inversion MASSOC; subst; *)
+    (*            assert (HPle : Ple r (RTL.max_reg_function f)) *)
+    (*              by (eapply RTL.max_reg_function_use; eauto; simpl; auto); *)
+    (*            apply H1 in HPle; inversion HPle; *)
+    (*            rewrite H2 in *; discriminate *)
+    (*          ). *)
+
+    (* + econstructor. split. *)
+    (* apply Smallstep.plus_one. *)
+    (* eapply HTL.step_module; eauto. *)
+    (* econstructor; simpl; trivial. *)
+    (* constructor; trivial. *)
+    (* econstructor; simpl; eauto. *)
+    (* eapply eval_correct; eauto. constructor. *)
+    (* unfold_merge. simpl. *)
+    (* rewrite AssocMap.gso. *)
+    (* apply AssocMap.gss. *)
+    (* apply st_greater_than_res. *)
+
+    (* (* match_states *) *)
+    (* assert (pc' = valueToPos (posToValue 32 pc')). auto using assumption_32bit. *)
+    (* rewrite <- H1. *)
+    (* constructor; auto. *)
+    (* unfold_merge. *)
+    (* apply regs_lessdef_add_match. *)
+    (* constructor. *)
+    (* apply regs_lessdef_add_greater. *)
+    (* apply greater_than_max_func. *)
+    (* assumption. *)
+
+    (* unfold state_st_wf. intros. inversion H2. subst. *)
+    (* unfold_merge. *)
+    (* rewrite AssocMap.gso. *)
+    (* apply AssocMap.gss. *)
+    (* apply st_greater_than_res. *)
+
+    (* + econstructor. split. *)
+    (* apply Smallstep.plus_one. *)
+    (* eapply HTL.step_module; eauto. *)
+    (* econstructor; simpl; trivial. *)
+    (* constructor; trivial. *)
+    (* econstructor; simpl; eauto. *)
+    (* eapply eval_correct; eauto. *)
+    (* constructor. rewrite valueToInt_intToValue. trivial. *)
+    (* unfold_merge. simpl. *)
+    (* rewrite AssocMap.gso. *)
+    (* apply AssocMap.gss. *)
+    (* apply st_greater_than_res. *)
+
+    (* (* match_states *) *)
+    (* assert (pc' = valueToPos (posToValue 32 pc')). auto using assumption_32bit. *)
+    (* rewrite <- H1. *)
+    (* constructor. *)
+    (* unfold_merge. *)
+    (* apply regs_lessdef_add_match. *)
+    (* constructor. *)
+    (* symmetry. apply valueToInt_intToValue. *)
+    (* apply regs_lessdef_add_greater. *)
+    (* apply greater_than_max_func. *)
+    (* assumption. assumption. *)
+
+    (* unfold state_st_wf. intros. inversion H2. subst. *)
+    (* unfold_merge. *)
+    (* rewrite AssocMap.gso. *)
+    (* apply AssocMap.gss. *)
+    (* apply st_greater_than_res. *)
+    (* assumption. *)
+  Admitted.
+  Hint Resolve transl_iop_correct : htlproof.
+
+  Ltac tac :=
+    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 inv_arr_access :=
+    match goal with
+    | [ _ : translate_arr_access ?chunk ?addr ?args _ _ = OK ?c _ _ |- _] =>
+      destruct c, chunk, addr, args; crush; tac; crush
+    end.
+
+  Lemma transl_iload_correct:
+    forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive)
+      (rs : Registers.Regmap.t Values.val) (m : mem) (chunk : AST.memory_chunk)
+      (addr : Op.addressing) (args : list Registers.reg) (dst : Registers.reg)
+      (pc' : RTL.node) (a v : Values.val),
+      (RTL.fn_code f) ! pc = Some (RTL.Iload chunk addr args dst pc') ->
+      Op.eval_addressing ge sp addr (map (fun r : positive => Registers.Regmap.get r rs) args) = Some a ->
+      Mem.loadv chunk m a = Some v ->
+      forall R1 : HTL.state,
+        match_states (RTL.State s f sp pc rs m) R1 ->
+        exists R2 : HTL.state,
+          Smallstep.plus HTL.step tge R1 Events.E0 R2 /\
+          match_states (RTL.State s f sp pc' (Registers.Regmap.set dst v rs) m) R2.
+  Proof.
+    intros s f sp pc rs m chunk addr args dst pc' a v H H0 H1 R1 MSTATE.
+    inv_state. inv_arr_access.
+
+    + (** Preamble *)
+      invert MARR. crush.
+
+      unfold Op.eval_addressing in H0.
+      destruct (Archi.ptr64) eqn:ARCHI; crush.
+
+      unfold reg_stack_based_pointers in RSBP.
+      pose proof (RSBP r0) as RSBPr0.
+
+      destruct (Registers.Regmap.get r0 rs) eqn:EQr0; crush.
+
+      rewrite ARCHI in H1. crush.
+      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; crush; eauto).
+      apply H6 in HPler0.
+      invert HPler0; try congruence.
+      rewrite EQr0 in H8.
+      invert H8.
+      clear H0. clear H6.
+
+      unfold check_address_parameter_signed in *;
+      unfold check_address_parameter_unsigned in *; crush.
+
+      remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (valueToZ asr # r0))
+                                    (Integers.Ptrofs.of_int (Integers.Int.repr z))) as OFFSET.
+
+      (** Modular preservation proof *)
+      assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE.
+      { rewrite HeqOFFSET.
+        apply PtrofsExtra.add_mod; crush; 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; crush. }
+
+      (** Read bounds proof *)
+      assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH.
+      { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; crush; auto.
+        unfold stack_bounds in BOUNDS.
+        exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET)); auto.
+        split; try lia; apply Integers.Ptrofs.unsigned_range_2.
+        small_tac. }
+
+      (** Normalisation proof *)
+      assert (Integers.Ptrofs.repr
+                (4 * Integers.Ptrofs.unsigned
+                       (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_divu; crush; auto. }
+
+      (** Normalised bounds proof *)
+      assert (0 <=
+              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.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; crush.
+        apply Zmult_lt_reg_r with (p := 4); try lia.
+        repeat rewrite ZLib.div_mul_undo; try lia.
+        apply Z.div_pos; small_tac.
+        apply Z.div_le_upper_bound; small_tac. }
+
+      inversion NORMALISE_BOUND as [ NORMALISE_BOUND_LOW NORMALISE_BOUND_HIGH ];
+      clear NORMALISE_BOUND.
+
+      (** Start of proof proper *)
+      eexists. split.
+      eapply Smallstep.plus_one.
       eapply HTL.step_module; eauto.
-      (* processing of state *)
+      apply assumption_32bit.
+      econstructor. econstructor. econstructor. crush.
+      econstructor. econstructor. econstructor. crush.
+      econstructor. econstructor.
+      econstructor. econstructor. econstructor. econstructor.
+      econstructor. econstructor. econstructor. econstructor.
+
+      all: big_tac.
+
+      1: { apply st_greater_than_res. }
+      2: { apply st_greater_than_res. }
+
+      (** Match assocmaps *)
+      apply regs_lessdef_add_match; big_tac.
+
+      (** Equality proof *)
+      match goal with
+      | [ |- context [valueToNat ?x] ] =>
+        assert (Z.to_nat
+                  (Integers.Ptrofs.unsigned
+                     (Integers.Ptrofs.divu
+                        OFFSET
+                        (Integers.Ptrofs.repr 4)))
+                =
+                valueToNat x)
+          as EXPR_OK by admit
+      end.
+      rewrite <- EXPR_OK.
+
+      specialize (H7 (Integers.Ptrofs.unsigned
+                        (Integers.Ptrofs.divu
+                           OFFSET
+                           (Integers.Ptrofs.repr 4)))).
+      exploit H7; big_tac.
+
+      (** RSBP preservation *)
+      unfold arr_stack_based_pointers in ASBP.
+      specialize (ASBP (Integers.Ptrofs.unsigned
+                          (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)))).
+      exploit ASBP; big_tac.
+      rewrite NORMALISE in H0. rewrite H1 in H0. assumption.
+
+    + (** Preamble *)
+      invert MARR. crush.
+
+      unfold Op.eval_addressing in H0.
+      destruct (Archi.ptr64) eqn:ARCHI; crush.
+
+      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; crush.
+
+      rewrite ARCHI in H1. crush.
+      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; crush; 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 *; crush.
+
+      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.
+
+      (** Modular preservation proof *)
+      assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE.
+      { rewrite HeqOFFSET.
+        apply PtrofsExtra.add_mod; crush; 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; crush; try lia.
+        exists 1073741824. reflexivity. (* FIXME: This is sadness inducing. *)
+        apply IntExtra.mul_mod; crush; try lia.
+        exists 1073741824. reflexivity. (* FIXME: This is sadness inducing. *)
+        admit. (* FIXME: Register bounds. *)
+        rewrite Integers.Int.signed_repr; crush.
+        rewrite Integers.Int.signed_repr; crush. }
+
+      (** Read bounds proof *)
+      assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH.
+      { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; crush; auto.
+        unfold stack_bounds in BOUNDS.
+        exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET)); auto.
+        split; try lia; apply Integers.Ptrofs.unsigned_range_2.
+        small_tac. }
+
+      (** Normalisation proof *)
+      assert (Integers.Ptrofs.repr
+                (4 * Integers.Ptrofs.unsigned
+                       (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_divu; crush. }
+
+      (** Normalised bounds proof *)
+      assert (0 <=
+              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.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; crush.
+        apply Zmult_lt_reg_r with (p := 4); try lia.
+        repeat rewrite ZLib.div_mul_undo; try lia.
+        apply Z.div_pos; small_tac.
+        apply Z.div_le_upper_bound; lia. }
+
+      inversion NORMALISE_BOUND as [ NORMALISE_BOUND_LOW NORMALISE_BOUND_HIGH ];
+      clear NORMALISE_BOUND.
+
+      (** Start of proof proper *)
+      eexists. split.
+      eapply Smallstep.plus_one.
+      eapply HTL.step_module; eauto.
+      apply assumption_32bit.
+      econstructor. econstructor. econstructor. crush.
+      econstructor. econstructor. econstructor. crush.
+      econstructor. econstructor. econstructor.
+      econstructor. econstructor. econstructor. econstructor.
       econstructor.
-      simpl. trivial.
+      eapply Verilog.erun_Vbinop with (EQ := ?[EQ6]).
+      econstructor. econstructor. econstructor. econstructor.
+      econstructor. econstructor. econstructor. econstructor.
+      econstructor. econstructor.
+
+      all: big_tac.
+
+      1: { apply st_greater_than_res. }
+      2: { apply st_greater_than_res. }
+
+      (** Match assocmaps *)
+      apply regs_lessdef_add_match; big_tac.
+
+      (** Equality proof *)
+      match goal with
+      | [ |- context [valueToNat ?x] ] =>
+        assert (Z.to_nat
+                  (Integers.Ptrofs.unsigned
+                     (Integers.Ptrofs.divu
+                        OFFSET
+                        (Integers.Ptrofs.repr 4)))
+                =
+                valueToNat x)
+          as EXPR_OK by admit
+      end.
+      rewrite <- EXPR_OK.
+
+      specialize (H7 (Integers.Ptrofs.unsigned
+                        (Integers.Ptrofs.divu
+                           OFFSET
+                           (Integers.Ptrofs.repr 4)))).
+      exploit H7; big_tac.
+
+      (** RSBP preservation *)
+      unfold arr_stack_based_pointers in ASBP.
+      specialize (ASBP (Integers.Ptrofs.unsigned
+                          (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)))).
+      exploit ASBP; big_tac.
+      rewrite NORMALISE in H0. rewrite H1 in H0. assumption.
+
+    + invert MARR. crush.
+
+      unfold Op.eval_addressing in H0.
+      destruct (Archi.ptr64) eqn:ARCHI; crush.
+      rewrite ARCHI in H0. crush.
+
+      unfold check_address_parameter_unsigned in *;
+      unfold check_address_parameter_signed in *; crush.
+
+      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.
+
+      (** Modular preservation proof *)
+      rename H0 into MOD_PRESERVE.
+
+      (** Read bounds proof *)
+      assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH.
+      { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; crush; auto.
+        unfold stack_bounds in BOUNDS.
+        exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET)); big_tac. }
+
+      (** Normalisation proof *)
+      assert (Integers.Ptrofs.repr
+                (4 * Integers.Ptrofs.unsigned
+                       (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_divu; crush. }
+
+      (** Normalised bounds proof *)
+      assert (0 <=
+              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.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; crush.
+        apply Zmult_lt_reg_r with (p := 4); try lia.
+        repeat rewrite ZLib.div_mul_undo; try lia.
+        apply Z.div_pos; small_tac.
+        apply Z.div_le_upper_bound; lia. }
+
+      inversion NORMALISE_BOUND as [ NORMALISE_BOUND_LOW NORMALISE_BOUND_HIGH ];
+      clear NORMALISE_BOUND.
+
+      (** Start of proof proper *)
+      eexists. split.
+      eapply Smallstep.plus_one.
+      eapply HTL.step_module; eauto.
+      apply assumption_32bit.
+      econstructor. econstructor. econstructor. crush.
+      econstructor. econstructor. econstructor. econstructor. crush.
+
+      all: big_tac.
+
+      1: { apply st_greater_than_res. }
+      2: { apply st_greater_than_res. }
+
+      (** Match assocmaps *)
+      apply regs_lessdef_add_match; big_tac.
+
+      (** Equality proof *)
+      match goal with
+      | [ |- context [valueToNat ?x] ] =>
+        assert (Z.to_nat
+                  (Integers.Ptrofs.unsigned
+                     (Integers.Ptrofs.divu
+                        OFFSET
+                        (Integers.Ptrofs.repr 4)))
+                =
+                valueToNat x)
+          as EXPR_OK by admit
+      end.
+      rewrite <- EXPR_OK.
+
+      specialize (H7 (Integers.Ptrofs.unsigned
+                        (Integers.Ptrofs.divu
+                           OFFSET
+                           (Integers.Ptrofs.repr 4)))).
+      exploit H7; big_tac.
+
+      (** RSBP preservation *)
+      unfold arr_stack_based_pointers in ASBP.
+      specialize (ASBP (Integers.Ptrofs.unsigned
+                          (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)))).
+      exploit ASBP; big_tac.
+      rewrite NORMALISE in H0. rewrite H1 in H0. assumption.
+  Admitted.
+  Hint Resolve transl_iload_correct : htlproof.
+
+  Lemma transl_istore_correct:
+    forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive)
+      (rs : Registers.Regmap.t Values.val) (m : mem) (chunk : AST.memory_chunk)
+      (addr : Op.addressing) (args : list Registers.reg) (src : Registers.reg)
+      (pc' : RTL.node) (a : Values.val) (m' : mem),
+      (RTL.fn_code f) ! pc = Some (RTL.Istore chunk addr args src pc') ->
+      Op.eval_addressing ge sp addr (map (fun r : positive => Registers.Regmap.get r rs) args) = Some a ->
+      Mem.storev chunk m a (Registers.Regmap.get src rs) = Some m' ->
+      forall R1 : HTL.state,
+        match_states (RTL.State s f sp pc rs m) R1 ->
+        exists R2 : HTL.state,
+          Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ match_states (RTL.State s f sp pc' rs m') R2.
+  Proof.
+    intros s f sp pc rs m chunk addr args src pc' a m' H H0 H1 R1 MSTATES.
+    inv_state. inv_arr_access.
+
+    + (** Preamble *)
+      invert MARR. crush.
+
+      unfold Op.eval_addressing in H0.
+      destruct (Archi.ptr64) eqn:ARCHI; crush.
+
+      unfold reg_stack_based_pointers in RSBP.
+      pose proof (RSBP r0) as RSBPr0.
+
+      destruct (Registers.Regmap.get r0 rs) eqn:EQr0; crush.
+
+      rewrite ARCHI in H1. crush.
+      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; crush; 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 *; crush.
+
+      remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (valueToZ asr # r0))
+                                    (Integers.Ptrofs.of_int (Integers.Int.repr z))) as OFFSET.
+
+      (** Modular preservation proof *)
+      assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE.
+      { rewrite HeqOFFSET.
+        apply PtrofsExtra.add_mod; crush; 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; crush. }
+
+      (** Write bounds proof *)
+      assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as WRITE_BOUND_HIGH.
+      { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; crush; auto.
+        unfold stack_bounds in BOUNDS.
+        exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET) (Registers.Regmap.get src rs)); big_tac.
+        apply Integers.Ptrofs.unsigned_range_2. }
+
+      (** Start of proof proper *)
+      eexists. split.
+      eapply Smallstep.plus_one.
+      eapply HTL.step_module; eauto.
+      apply assumption_32bit.
+      econstructor. econstructor. econstructor.
+      eapply Verilog.stmnt_runp_Vnonblock_arr. crush.
       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.
 
-      (* prove stval *)
-      unfold merge_assocmap.
-      unfold_merge. simpl. apply AssocMap.gss.
+      all: crush.
 
-      (* prove match_state *)
+      (** State Lookup *)
+      unfold Verilog.merge_regs.
+      crush.
+      unfold_merge.
+      apply AssocMap.gss.
+
+      (** Match states *)
       rewrite assumption_32bit.
-      constructor; auto.
-      unfold_merge. simpl. apply regs_lessdef_add_greater. apply greater_than_max_func.
+      econstructor; eauto.
+
+      (** Match assocmaps *)
+      unfold Verilog.merge_regs. crush. unfold_merge.
+      apply regs_lessdef_add_greater. apply greater_than_max_func.
       assumption.
-      unfold state_st_wf. inversion 1. subst. unfold_merge. apply AssocMap.gss.
-    - (* Iop *)
-      (* destruct v eqn:?; *)
-      (*          try ( *)
-      (*            destruct op eqn:?; inversion H21; simpl in H0; repeat (unfold_match H0); *)
-      (*            inversion H0; subst; simpl in *; try (unfold_func H4); try (unfold_func H5); *)
-      (*            try (unfold_func H6); *)
-      (*            try (unfold Op.eval_addressing32 in H6; repeat (unfold_match H6); inversion H6; *)
-      (*                 unfold_func H3); *)
-
-      (*            inversion Heql; inversion MASSOC; subst; *)
-      (*            assert (HPle : Ple r (RTL.max_reg_function f)) *)
-      (*              by (eapply RTL.max_reg_function_use; eauto; simpl; auto); *)
-      (*            apply H1 in HPle; inversion HPle; *)
-      (*            rewrite H2 in *; discriminate *)
-      (*          ). *)
-
-      (* + econstructor. split. *)
-      (* apply Smallstep.plus_one. *)
-      (* eapply HTL.step_module; eauto. *)
-      (* econstructor; simpl; trivial. *)
-      (* constructor; trivial. *)
-      (* econstructor; simpl; eauto. *)
-      (* eapply eval_correct; eauto. constructor. *)
-      (* unfold_merge. simpl. *)
-      (* rewrite AssocMap.gso. *)
-      (* apply AssocMap.gss. *)
-      (* apply st_greater_than_res. *)
-
-      (* (* match_states *) *)
-      (* assert (pc' = valueToPos (posToValue 32 pc')). auto using assumption_32bit. *)
-      (* rewrite <- H1. *)
-      (* constructor; auto. *)
-      (* unfold_merge. *)
-      (* apply regs_lessdef_add_match. *)
-      (* constructor. *)
-      (* apply regs_lessdef_add_greater. *)
-      (* apply greater_than_max_func. *)
-      (* assumption. *)
-
-      (* unfold state_st_wf. intros. inversion H2. subst. *)
-      (* unfold_merge. *)
-      (* rewrite AssocMap.gso. *)
-      (* apply AssocMap.gss. *)
-      (* apply st_greater_than_res. *)
-
-      (* + econstructor. split. *)
-      (* apply Smallstep.plus_one. *)
-      (* eapply HTL.step_module; eauto. *)
-      (* econstructor; simpl; trivial. *)
-      (* constructor; trivial. *)
-      (* econstructor; simpl; eauto. *)
-      (* eapply eval_correct; eauto. *)
-      (* constructor. rewrite valueToInt_intToValue. trivial. *)
-      (* unfold_merge. simpl. *)
-      (* rewrite AssocMap.gso. *)
-      (* apply AssocMap.gss. *)
-      (* apply st_greater_than_res. *)
-
-      (* (* match_states *) *)
-      (* assert (pc' = valueToPos (posToValue 32 pc')). auto using assumption_32bit. *)
-      (* rewrite <- H1. *)
-      (* constructor. *)
-      (* unfold_merge. *)
-      (* apply regs_lessdef_add_match. *)
-      (* constructor. *)
-      (* symmetry. apply valueToInt_intToValue. *)
-      (* apply regs_lessdef_add_greater. *)
-      (* apply greater_than_max_func. *)
-      (* assumption. assumption. *)
-
-      (* unfold state_st_wf. intros. inversion H2. subst. *)
-      (* unfold_merge. *)
-      (* rewrite AssocMap.gso. *)
-      (* apply AssocMap.gss. *)
-      (* apply st_greater_than_res. *)
-      (* assumption. *)
-      admit.
-
-    - admit.
-    - admit.
-
-    - eexists. split. apply Smallstep.plus_one.
-      eapply HTL.step_module; eauto.
-      eapply Verilog.stmnt_runp_Vnonblock_reg with
-          (rhsval := if b then posToValue 32 ifso else posToValue 32 ifnot).
 
+      (** States well formed *)
+      unfold state_st_wf. inversion 1. crush.
+      unfold Verilog.merge_regs.
+      unfold_merge.
+      apply AssocMap.gss.
+
+      (** Equality proof *)
+      match goal with
+      | [ |- context [valueToNat ?x] ] =>
+        assert (Z.to_nat
+                  (Integers.Ptrofs.unsigned
+                     (Integers.Ptrofs.divu
+                        OFFSET
+                        (Integers.Ptrofs.repr 4)))
+                =
+                valueToNat x)
+          as EXPR_OK by admit
+      end.
+
+      assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
+      inversion MASSOC; revert HeqOFFSET; subst; clear MASSOC; intros HeqOFFSET.
+
+      econstructor.
+      repeat split; crush.
+      unfold HTL.empty_stack.
+      crush.
+      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. crush.
+      apply list_repeat_len.
+
+      rewrite <- array_set_len.
+      unfold arr_repeat. crush.
+      rewrite list_repeat_len.
+      rewrite H4. reflexivity.
+
+      remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (valueToZ asr # r0))
+                                    (Integers.Ptrofs.of_int (Integers.Int.repr z))) as OFFSET.
+
+      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 H13.
+      destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; invert H13; eauto.
+
+      rewrite <- array_set_len.
+      unfold arr_repeat. crush.
+      rewrite list_repeat_len. auto.
+
+      assert (4 * ptr / 4 = Integers.Ptrofs.unsigned OFFSET / 4) by (f_equal; assumption).
+      rewrite Z.mul_comm in H13.
+      rewrite Z_div_mult in H13; try lia.
+      replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) in H13 by reflexivity.
+      rewrite <- PtrofsExtra.divu_unsigned in H13; unfold_constants; try lia.
+      rewrite H13. 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'.
+           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); crush; 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. crush.
+      rewrite list_repeat_len. auto.
+      rewrite array_gso.
+      unfold array_get_error.
+      unfold arr_repeat.
+      crush.
+      apply list_repeat_lookup.
+      lia.
+      unfold_constants.
+      intro.
+      apply Z2Nat.inj_iff in H13; 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).
+
+      crush.
+      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. }
+      crush.
+      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.
-      destruct b.
-      eapply Verilog.erun_Vternary_true.
-      eapply eval_cond_correct; eauto.
-      constructor.
-      apply boolToValue_ValueToBool.
-      eapply Verilog.erun_Vternary_false.
-      eapply eval_cond_correct; eauto.
-      constructor.
-      apply boolToValue_ValueToBool.
-      constructor.
+      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); crush; lia.
+      }
+      apply ASBP; assumption.
+
+      unfold stack_bounds in *. intros.
+      simpl.
+      assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
+      erewrite Mem.load_store_other with (m1 := m).
+      2: { exact H1. }
+      2: { right. right. simpl.
+           rewrite ZERO.
+           rewrite Integers.Ptrofs.add_zero_l.
+           rewrite Integers.Ptrofs.unsigned_repr; crush; try lia.
+           apply ZExtra.mod_0_bounds; crush; try lia. }
+      crush.
+      exploit (BOUNDS ptr); try lia. intros. crush.
+      exploit (BOUNDS ptr v); try lia. intros.
+      invert H0.
+      match goal with | |- ?x = _ => destruct x eqn:EQ end; try reflexivity.
+      assert (Mem.valid_access m AST.Mint32 sp'
+                               (Integers.Ptrofs.unsigned
+                                  (Integers.Ptrofs.add (Integers.Ptrofs.repr 0)
+                                                       (Integers.Ptrofs.repr ptr))) Writable).
+      { pose proof H1. eapply Mem.store_valid_access_2 in H0.
+        exact H0. eapply Mem.store_valid_access_3. eassumption. }
+      pose proof (Mem.valid_access_store m AST.Mint32 sp'
+                                         (Integers.Ptrofs.unsigned
+                                            (Integers.Ptrofs.add (Integers.Ptrofs.repr 0)
+                                                                 (Integers.Ptrofs.repr ptr))) v).
+      apply X in H0. invert H0. congruence.
+
+    + (** Preamble *)
+      invert MARR. crush.
+
+      unfold Op.eval_addressing in H0.
+      destruct (Archi.ptr64) eqn:ARCHI; crush.
+
+      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; crush.
+
+      rewrite ARCHI in H1. crush.
+      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; crush; 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 *; crush.
+
+      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.
+
+      (** Modular preservation proof *)
+      assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE.
+      { rewrite HeqOFFSET.
+        apply PtrofsExtra.add_mod; crush; 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; crush; try lia.
+        exists 1073741824. reflexivity. (* FIXME: This is sadness inducing. *)
+        apply IntExtra.mul_mod; crush; try lia.
+        exists 1073741824. reflexivity. (* FIXME: This is sadness inducing. *)
+        admit. (* FIXME: Register bounds. *)
+        rewrite Integers.Int.signed_repr; crush; try split; try assumption.
+        rewrite Integers.Int.signed_repr; crush; try split; try assumption.
+      }
+
+      (** Write bounds proof *)
+      assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as WRITE_BOUND_HIGH.
+      { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; crush; auto.
+        unfold stack_bounds in BOUNDS.
+        exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET) (Registers.Regmap.get src rs)); auto.
+        split; try lia; apply Integers.Ptrofs.unsigned_range_2.
+        small_tac. }
+
+      (** Start of proof proper *)
+      eexists. split.
+      eapply Smallstep.plus_one.
+      eapply HTL.step_module; eauto.
+      apply assumption_32bit.
+      econstructor. econstructor. econstructor.
+      eapply Verilog.stmnt_runp_Vnonblock_arr. crush.
+      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: crush.
+
+      (** State Lookup *)
+      unfold Verilog.merge_regs.
+      crush.
       unfold_merge.
       apply AssocMap.gss.
 
-      destruct b.
+      (** Match states *)
       rewrite assumption_32bit.
-      apply match_state.
-      unfold_merge.
+      econstructor; eauto.
+
+      (** Match assocmaps *)
+      unfold Verilog.merge_regs. crush. unfold_merge.
       apply regs_lessdef_add_greater. apply greater_than_max_func.
-      assumption. assumption.
+      assumption.
 
-      unfold state_st_wf. intros. inversion H1.
-      subst. unfold_merge.
+      (** States well formed *)
+      unfold state_st_wf. inversion 1. crush.
+      unfold Verilog.merge_regs.
+      unfold_merge.
       apply AssocMap.gss.
-      assumption.
 
+      (** 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; crush.
+      unfold HTL.empty_stack.
+      crush.
+      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. crush.
+      apply list_repeat_len.
+
+      rewrite <- array_set_len.
+      unfold arr_repeat. crush.
+      rewrite list_repeat_len.
+      rewrite H4. reflexivity.
+
+      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.
+      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 H20.
+      destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; invert H20; eauto.
+
+      rewrite <- array_set_len.
+      unfold arr_repeat. crush.
+      rewrite list_repeat_len. auto.
+
+      assert (4 * ptr / 4 = Integers.Ptrofs.unsigned OFFSET / 4) by (f_equal; assumption).
+      rewrite Z.mul_comm in H20.
+      rewrite Z_div_mult in H20; try lia.
+      replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) in H20 by reflexivity.
+      rewrite <- PtrofsExtra.divu_unsigned in H20; unfold_constants; try lia.
+      rewrite H20. 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'.
+           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); crush; 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. crush.
+      rewrite list_repeat_len. auto.
+      rewrite array_gso.
+      unfold array_get_error.
+      unfold arr_repeat.
+      crush.
+      apply list_repeat_lookup.
+      lia.
+      unfold_constants.
+      intro.
+      apply Z2Nat.inj_iff in H20; 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).
+
+      crush.
+      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. }
+      crush.
+      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.
 
-      rewrite assumption_32bit.
-      apply match_state.
+      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); crush; lia.
+      }
+      apply ASBP; assumption.
+
+      unfold stack_bounds in *. intros.
+      simpl.
+      assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
+      erewrite Mem.load_store_other with (m1 := m).
+      2: { exact H1. }
+      2: { right. right. simpl.
+           rewrite ZERO.
+           rewrite Integers.Ptrofs.add_zero_l.
+           rewrite Integers.Ptrofs.unsigned_repr; crush; try lia.
+           apply ZExtra.mod_0_bounds; crush; try lia. }
+      crush.
+      exploit (BOUNDS ptr); try lia. intros. crush.
+      exploit (BOUNDS ptr v); try lia. intros.
+      invert H0.
+      match goal with | |- ?x = _ => destruct x eqn:EQ end; try reflexivity.
+      assert (Mem.valid_access m AST.Mint32 sp'
+                               (Integers.Ptrofs.unsigned
+                                  (Integers.Ptrofs.add (Integers.Ptrofs.repr 0)
+                                                       (Integers.Ptrofs.repr ptr))) Writable).
+      { pose proof H1. eapply Mem.store_valid_access_2 in H0.
+        exact H0. eapply Mem.store_valid_access_3. eassumption. }
+      pose proof (Mem.valid_access_store m AST.Mint32 sp'
+                                         (Integers.Ptrofs.unsigned
+                                            (Integers.Ptrofs.add (Integers.Ptrofs.repr 0)
+                                                                 (Integers.Ptrofs.repr ptr))) v).
+      apply X in H0. invert H0. congruence.
+
+    + invert MARR. crush.
+
+      unfold Op.eval_addressing in H0.
+      destruct (Archi.ptr64) eqn:ARCHI; crush.
+      rewrite ARCHI in H0. crush.
+
+      unfold check_address_parameter_unsigned in *;
+      unfold check_address_parameter_signed in *; crush.
+
+      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.
+
+      (** Modular preservation proof *)
+      rename H0 into MOD_PRESERVE.
+
+      (** Write bounds proof *)
+      assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as WRITE_BOUND_HIGH.
+      { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; crush; auto.
+        unfold stack_bounds in BOUNDS.
+        exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET) (Registers.Regmap.get src rs)); auto.
+        crush.
+        replace (Integers.Ptrofs.repr 0) with (Integers.Ptrofs.zero) by reflexivity.
+        small_tac. }
+
+      (** Start of proof proper *)
+      eexists. split.
+      eapply Smallstep.plus_one.
+      eapply HTL.step_module; eauto.
+      apply assumption_32bit.
+      econstructor. econstructor. econstructor.
+      eapply Verilog.stmnt_runp_Vnonblock_arr. crush.
+      econstructor. econstructor. econstructor. econstructor.
+
+      all: crush.
+
+      (** State Lookup *)
+      unfold Verilog.merge_regs.
+      crush.
       unfold_merge.
-      apply regs_lessdef_add_greater. apply greater_than_max_func. assumption.
+      apply AssocMap.gss.
+
+      (** Match states *)
+      rewrite assumption_32bit.
+      econstructor; eauto.
+
+      (** Match assocmaps *)
+      unfold Verilog.merge_regs. crush. unfold_merge.
+      apply regs_lessdef_add_greater. apply greater_than_max_func.
       assumption.
 
-      unfold state_st_wf. intros. inversion H1.
-      subst. unfold_merge.
+      (** States well formed *)
+      unfold state_st_wf. inversion 1. crush.
+      unfold Verilog.merge_regs.
+      unfold_merge.
       apply AssocMap.gss.
-      assumption.
 
+      (** 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; crush.
+      unfold HTL.empty_stack.
+      crush.
+      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. crush.
+      apply list_repeat_len.
+
+      rewrite <- array_set_len.
+      unfold arr_repeat. crush.
+      rewrite list_repeat_len.
+      rewrite H4. reflexivity.
+
+      remember i0 as OFFSET.
+      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 H8.
+      destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; invert H8; eauto.
+
+      rewrite <- array_set_len.
+      unfold arr_repeat. crush.
+      rewrite list_repeat_len. auto.
+
+      assert (4 * ptr / 4 = Integers.Ptrofs.unsigned OFFSET / 4) by (f_equal; assumption).
+      rewrite Z.mul_comm in H8.
+      rewrite Z_div_mult in H8; try lia.
+      replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) in H8 by reflexivity.
+      rewrite <- PtrofsExtra.divu_unsigned in H8; unfold_constants; try lia.
+      rewrite H8. 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'.
+           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); crush; 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. crush.
+      rewrite list_repeat_len. auto.
+      rewrite array_gso.
+      unfold array_get_error.
+      unfold arr_repeat.
+      crush.
+      apply list_repeat_lookup.
+      lia.
+      unfold_constants.
+      intro.
+      apply Z2Nat.inj_iff in H8; 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).
+
+      crush.
+      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. }
+      crush.
+      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.
 
-    - (* Return *)
-      econstructor. split.
+      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); crush; lia.
+      }
+      apply ASBP; assumption.
+
+      unfold stack_bounds in *. intros.
+      simpl.
+      assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
+      erewrite Mem.load_store_other with (m1 := m).
+      2: { exact H1. }
+      2: { right. right. simpl.
+           rewrite ZERO.
+           rewrite Integers.Ptrofs.add_zero_l.
+           rewrite Integers.Ptrofs.unsigned_repr; crush; try lia.
+           apply ZExtra.mod_0_bounds; crush; try lia. }
+      crush.
+      exploit (BOUNDS ptr); try lia. intros. crush.
+      exploit (BOUNDS ptr v); try lia. intros.
+      invert H0.
+      match goal with | |- ?x = _ => destruct x eqn:EQ end; try reflexivity.
+      assert (Mem.valid_access m AST.Mint32 sp'
+                               (Integers.Ptrofs.unsigned
+                                  (Integers.Ptrofs.add (Integers.Ptrofs.repr 0)
+                                                       (Integers.Ptrofs.repr ptr))) Writable).
+      { pose proof H1. eapply Mem.store_valid_access_2 in H0.
+        exact H0. eapply Mem.store_valid_access_3. eassumption. }
+      pose proof (Mem.valid_access_store m AST.Mint32 sp'
+                                         (Integers.Ptrofs.unsigned
+                                            (Integers.Ptrofs.add (Integers.Ptrofs.repr 0)
+                                                                 (Integers.Ptrofs.repr ptr))) v).
+      apply X in H0. invert H0. congruence.
+  Admitted.
+  Hint Resolve transl_istore_correct : htlproof.
+
+  Lemma transl_icond_correct:
+    forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive)
+      (rs : Registers.Regmap.t Values.val) (m : mem) (cond : Op.condition) (args : list Registers.reg)
+      (ifso ifnot : RTL.node) (b : bool) (pc' : RTL.node),
+      (RTL.fn_code f) ! pc = Some (RTL.Icond cond args ifso ifnot) ->
+      Op.eval_condition cond (map (fun r : positive => Registers.Regmap.get r rs) args) m = Some b ->
+      pc' = (if b then ifso else ifnot) ->
+      forall R1 : HTL.state,
+        match_states (RTL.State s f sp pc rs m) R1 ->
+        exists R2 : HTL.state,
+          Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ match_states (RTL.State s f sp pc' rs m) R2.
+  Proof.
+    intros s f sp pc rs m cond args ifso ifnot b pc' H H0 H1 R1 MSTATE.
+    inv_state.
+
+    eexists. split. apply Smallstep.plus_one.
+    eapply HTL.step_module; eauto.
+    apply assumption_32bit.
+    eapply Verilog.stmnt_runp_Vnonblock_reg with
+        (rhsval := if b then posToValue 32 ifso else posToValue 32 ifnot).
+    constructor.
+
+    simpl.
+    destruct b.
+    eapply Verilog.erun_Vternary_true.
+    eapply eval_cond_correct; eauto.
+    constructor.
+    apply boolToValue_ValueToBool.
+    eapply Verilog.erun_Vternary_false.
+    eapply eval_cond_correct; eauto.
+    constructor.
+    apply boolToValue_ValueToBool.
+    constructor.
+
+    big_tac.
+
+    invert MARR.
+    destruct b; rewrite assumption_32bit; big_tac.
+
+    Unshelve.
+    constructor.
+  Qed.
+  Hint Resolve transl_icond_correct : htlproof.
+
+  Lemma transl_ijumptable_correct:
+    forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive)
+      (rs : Registers.Regmap.t Values.val) (m : mem) (arg : Registers.reg) (tbl : list RTL.node)
+      (n : Integers.Int.int) (pc' : RTL.node),
+      (RTL.fn_code f) ! pc = Some (RTL.Ijumptable arg tbl) ->
+      Registers.Regmap.get arg rs = Values.Vint n ->
+      list_nth_z tbl (Integers.Int.unsigned n) = Some pc' ->
+      forall R1 : HTL.state,
+        match_states (RTL.State s f sp pc rs m) R1 ->
+        exists R2 : HTL.state,
+          Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ match_states (RTL.State s f sp pc' rs m) R2.
+  Proof.
+    intros s f sp pc rs m arg tbl n pc' H H0 H1 R1 MSTATE.
+  Admitted.
+  Hint Resolve transl_ijumptable_correct : htlproof.
+
+  Lemma transl_ireturn_correct:
+    forall (s : list RTL.stackframe) (f : RTL.function) (stk : Values.block)
+      (pc : positive) (rs : RTL.regset) (m : mem) (or : option Registers.reg)
+      (m' : mem),
+      (RTL.fn_code f) ! pc = Some (RTL.Ireturn or) ->
+      Mem.free m stk 0 (RTL.fn_stacksize f) = Some m' ->
+      forall R1 : HTL.state,
+        match_states (RTL.State s f (Values.Vptr stk Integers.Ptrofs.zero) pc rs m) R1 ->
+        exists R2 : HTL.state,
+          Smallstep.plus HTL.step tge R1 Events.E0 R2 /\
+          match_states (RTL.Returnstate s (Registers.regmap_optget or Values.Vundef rs) m') R2.
+  Proof.
+    intros s f stk pc rs m or m' H H0 R1 MSTATE.
+    inv_state.
+
+    - econstructor. split.
       eapply Smallstep.plus_two.
-      
+
       eapply HTL.step_module; eauto.
+      apply assumption_32bit.
       constructor.
       econstructor; simpl; trivial.
       econstructor; simpl; trivial.
@@ -453,45 +1903,41 @@ Section CORRECTNESS.
       econstructor; simpl; trivial.
       constructor.
 
-      constructor.
-      constructor.
+      constructor. constructor.
 
-      unfold_merge. simpl.
-      rewrite AssocMap.gso.
-      rewrite AssocMap.gso.
-      unfold state_st_wf in WF. eapply WF. reflexivity.
-      apply st_greater_than_res. apply st_greater_than_res.
+      unfold state_st_wf in WF; big_tac; eauto.
+      apply st_greater_than_res.
+      apply st_greater_than_res.
 
       apply HTL.step_finish.
+      unfold Verilog.merge_regs.
       unfold_merge; simpl.
       rewrite AssocMap.gso.
       apply AssocMap.gss.
       apply finish_not_return.
       apply AssocMap.gss.
       rewrite Events.E0_left. reflexivity.
-      constructor.
-      assumption.
+
+      constructor; auto.
       constructor.
 
+    (* FIXME: Duplication *)
     - econstructor. split.
       eapply Smallstep.plus_two.
       eapply HTL.step_module; eauto.
+      apply assumption_32bit.
       constructor.
       econstructor; simpl; trivial.
       econstructor; simpl; trivial.
+      constructor. constructor. constructor.
+      constructor. constructor. constructor.
 
-      constructor. constructor.
-
-      constructor.
-      econstructor; simpl; trivial.
-      apply Verilog.erun_Vvar. trivial.
-      unfold_merge. simpl.
-      rewrite AssocMap.gso.
-      rewrite AssocMap.gso.
-      unfold state_st_wf in WF. eapply WF. trivial.
-      apply st_greater_than_res. apply st_greater_than_res. trivial.
+      unfold state_st_wf in WF; big_tac; eauto.
+      apply st_greater_than_res.
+      apply st_greater_than_res.
 
       apply HTL.step_finish.
+      unfold Verilog.merge_regs.
       unfold_merge.
       rewrite AssocMap.gso.
       apply AssocMap.gss.
@@ -499,46 +1945,158 @@ Section CORRECTNESS.
       apply AssocMap.gss.
       rewrite Events.E0_left. trivial.
 
-      constructor. assumption. simpl. inversion MASSOC. subst.
+      constructor; auto.
+
+      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.
+      Unshelve.
+      all: constructor.
+  Qed.
+  Hint Resolve transl_ireturn_correct : htlproof.
+
+  Lemma transl_callstate_correct:
+    forall (s : list RTL.stackframe) (f : RTL.function) (args : list Values.val)
+      (m : mem) (m' : Mem.mem') (stk : Values.block),
+      Mem.alloc m 0 (RTL.fn_stacksize f) = (m', stk) ->
+      forall R1 : HTL.state,
+        match_states (RTL.Callstate s (AST.Internal f) args m) R1 ->
+        exists R2 : HTL.state,
+          Smallstep.plus HTL.step tge R1 Events.E0 R2 /\
+          match_states
+            (RTL.State s f (Values.Vptr stk Integers.Ptrofs.zero) (RTL.fn_entrypoint f)
+                       (RTL.init_regs args (RTL.fn_params f)) m') R2.
+  Proof.
+    intros s f args m m' stk H R1 MSTATE.
 
-      constructor. apply regs_lessdef_add_greater.
-      apply greater_than_max_func.
-      apply init_reg_assoc_empty. assumption. unfold state_st_wf.
-      intros. inv H1. apply AssocMap.gss. constructor.
+    inversion MSTATE; subst. inversion TF; subst.
+    econstructor. split. apply Smallstep.plus_one.
+    eapply HTL.step_call. crush.
 
-      admit.
+    apply match_state with (sp' := stk); eauto.
 
-    - inversion MSTATE; subst. inversion MS; subst. econstructor.
-      split. apply Smallstep.plus_one.
-      constructor.
+    all: big_tac.
 
-      constructor; auto. constructor; auto. apply regs_lessdef_add_match; auto.
-      apply regs_lessdef_add_greater. apply greater_than_max_func. auto.
+    apply regs_lessdef_add_greater.
+    apply greater_than_max_func.
+    apply init_reg_assoc_empty.
 
-      unfold state_st_wf. intros. inv H. rewrite AssocMap.gso.
-      rewrite AssocMap.gss. trivial. apply st_greater_than_res.
+    constructor.
 
-      admit.
+    destruct (Mem.load AST.Mint32 m' stk
+                       (Integers.Ptrofs.unsigned (Integers.Ptrofs.add
+                                                    Integers.Ptrofs.zero
+                                                    (Integers.Ptrofs.repr (4 * 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. }
+    ptrofs. rewrite LOAD.
+    rewrite ALLOC.
+    repeat constructor.
+
+    ptrofs. rewrite LOAD.
+    repeat constructor.
+
+    unfold reg_stack_based_pointers. intros.
+    unfold RTL.init_regs; crush.
+    destruct (RTL.fn_params f);
+    rewrite Registers.Regmap.gi; constructor.
+
+    unfold arr_stack_based_pointers. intros.
+    crush.
+    destruct (Mem.load AST.Mint32 m' stk
+                       (Integers.Ptrofs.unsigned (Integers.Ptrofs.add
+                                                    Integers.Ptrofs.zero
+                                                    (Integers.Ptrofs.repr (4 * 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.
 
-      Unshelve.
-      exact (AssocMap.empty value).
-      exact (AssocMap.empty value).
-      admit.
-      admit.
-      (* exact (ZToValue 32 0). *)
-      (* exact (AssocMap.empty value). *)
-      (* exact (AssocMap.empty value). *)
-      (* exact (AssocMap.empty value). *)
-      (* exact (AssocMap.empty value). *)
-  Admitted.
-  Hint Resolve transl_step_correct : htlproof.
+    Transparent Mem.alloc. (* TODO: Since there are opaque there's probably a lemma. *)
+    Transparent Mem.load.
+    Transparent Mem.store.
+    unfold stack_bounds.
+    split.
+
+    unfold Mem.alloc in H.
+    invert H.
+    crush.
+    unfold Mem.load.
+    intros.
+    match goal with | |- context[if ?x then _ else _] => destruct x end; try congruence.
+    invert v0. unfold Mem.range_perm in H3.
+    unfold Mem.perm in H3. crush.
+    unfold Mem.perm_order' in H3.
+    small_tac.
+    exploit (H3 ptr). rewrite Integers.Ptrofs.unsigned_repr; small_tac. intros.
+    rewrite Maps.PMap.gss in H8.
+    match goal with | H8 : context[if ?x then _ else _] |- _ => destruct x eqn:EQ end; try contradiction.
+    crush.
+    apply proj_sumbool_true in H10. lia.
+
+    unfold Mem.alloc in H.
+    invert H.
+    crush.
+    unfold Mem.store.
+    intros.
+    match goal with | |- context[if ?x then _ else _] => destruct x end; try congruence.
+    invert v0. unfold Mem.range_perm in H3.
+    unfold Mem.perm in H3. crush.
+    unfold Mem.perm_order' in H3.
+    small_tac.
+    exploit (H3 ptr). rewrite Integers.Ptrofs.unsigned_repr; small_tac. intros.
+    rewrite Maps.PMap.gss in H8.
+    match goal with | H8 : context[if ?x then _ else _] |- _ => destruct x eqn:EQ end; try contradiction.
+    crush.
+    apply proj_sumbool_true in H10. lia.
+    Opaque Mem.alloc.
+    Opaque Mem.load.
+    Opaque Mem.store.
+  Qed.
+  Hint Resolve transl_callstate_correct : htlproof.
+
+  Lemma transl_returnstate_correct:
+    forall (res0 : Registers.reg) (f : RTL.function) (sp : Values.val) (pc : RTL.node)
+      (rs : RTL.regset) (s : list RTL.stackframe) (vres : Values.val) (m : mem)
+      (R1 : HTL.state),
+      match_states (RTL.Returnstate (RTL.Stackframe res0 f sp pc rs :: s) vres m) R1 ->
+      exists R2 : HTL.state,
+        Smallstep.plus HTL.step tge R1 Events.E0 R2 /\
+        match_states (RTL.State s f sp pc (Registers.Regmap.set res0 vres rs) m) R2.
+  Proof.
+    intros res0 f sp pc rs s vres m R1 MSTATE.
+    inversion MSTATE. inversion MF.
+  Qed.
+  Hint Resolve transl_returnstate_correct : htlproof.
+
+  Lemma option_inv :
+    forall A x y,
+      @Some A x = Some y -> x = y.
+  Proof. intros. inversion H. trivial. Qed.
+
+  Lemma main_tprog_internal :
+    forall b,
+      Globalenvs.Genv.find_symbol tge tprog.(AST.prog_main) = Some b ->
+      exists f, Genv.find_funct_ptr (Genv.globalenv tprog) b = Some (AST.Internal f).
+  Proof.
+    intros.
+    destruct TRANSL. unfold main_is_internal in H1.
+    repeat (unfold_match H1). replace b with b0.
+    exploit function_ptr_translated; eauto. intros [tf [A B]].
+    unfold transl_fundef, AST.transf_partial_fundef, Errors.bind in B.
+    unfold_match B. inv B. econstructor. apply A.
+
+    apply option_inv. rewrite <- Heqo. rewrite <- H.
+    rewrite symbols_preserved. replace (AST.prog_main tprog) with (AST.prog_main prog).
+    trivial. symmetry; eapply Linking.match_program_main; eauto.
+  Qed.
 
   (* Had to admit proof because currently there is no way to force main to be Internal. *)
   Lemma transl_initial_states :
@@ -548,20 +2106,35 @@ Section CORRECTNESS.
         Smallstep.initial_state (HTL.semantics tprog) s2 /\ match_states s1 s2.
   Proof.
     induction 1.
+    destruct TRANSL. unfold main_is_internal in H4.
+    repeat (unfold_match H4).
+    assert (f = AST.Internal f1). apply option_inv.
+    rewrite <- Heqo0. rewrite <- H1. replace b with b0.
+    auto. apply option_inv. rewrite <- H0. rewrite <- Heqo.
+    trivial.
     exploit function_ptr_translated; eauto.
     intros [tf [A B]].
     unfold transl_fundef, Errors.bind in B.
+    unfold AST.transf_partial_fundef, Errors.bind in B.
     repeat (unfold_match B). inversion B. subst.
+    exploit main_tprog_internal; eauto; intros.
+    rewrite symbols_preserved. replace (AST.prog_main tprog) with (AST.prog_main prog).
+    apply Heqo. symmetry; eapply Linking.match_program_main; eauto.
+    inversion H5.
     econstructor; split. econstructor.
-    apply (Genv.init_mem_transf_partial TRANSL); eauto.
+    apply (Genv.init_mem_transf_partial TRANSL'); eauto.
     replace (AST.prog_main tprog) with (AST.prog_main prog).
     rewrite symbols_preserved; eauto.
     symmetry; eapply Linking.match_program_main; eauto.
-    Admitted.
-    (*eexact A. trivial.
+    apply H6.
+
     constructor.
-    apply transl_module_correct. auto.
-  Qed.*)
+    apply transl_module_correct.
+    assert (Some (AST.Internal x) = Some (AST.Internal m)).
+    replace (AST.fundef HTL.module) with (HTL.fundef).
+    rewrite <- H6. setoid_rewrite <- A. trivial.
+    trivial. inv H7. assumption.
+  Qed.
   Hint Resolve transl_initial_states : htlproof.
 
   Lemma transl_final_states :
@@ -572,18 +2145,26 @@ Section CORRECTNESS.
       Smallstep.final_state (RTL.semantics prog) s1 r ->
       Smallstep.final_state (HTL.semantics tprog) s2 r.
   Proof.
-    intros. inv H0. inv H. inv H4. inv MS. constructor. trivial.
+    intros. inv H0. inv H. inv H4. invert MF. constructor. reflexivity.
   Qed.
-  Hint Resolve transl_final_states : htlproof.*)
+  Hint Resolve transl_final_states : htlproof.
 
-Theorem transf_program_correct:
-  Smallstep.forward_simulation (RTL.semantics prog) (HTL.semantics tprog).
-Proof.
-(*  eapply Smallstep.forward_simulation_plus.
-  apply senv_preserved.
-  eexact transl_initial_states.
-  eexact transl_final_states.
-  exact transl_step_correct.*)
-Admitted.
+  Theorem transl_step_correct:
+    forall (S1 : RTL.state) t S2,
+      RTL.step ge S1 t S2 ->
+      forall (R1 : HTL.state),
+        match_states S1 R1 ->
+        exists R2, Smallstep.plus HTL.step tge R1 t R2 /\ match_states S2 R2.
+  Proof.
+    induction 1; eauto with htlproof; (intros; inv_state).
+  Qed.
+  Hint Resolve transl_step_correct : htlproof.
+
+  Theorem transf_program_correct:
+    Smallstep.forward_simulation (RTL.semantics prog) (HTL.semantics tprog).
+  Proof.
+    eapply Smallstep.forward_simulation_plus; eauto with htlproof.
+    apply senv_preserved.
+  Qed.
 
 End CORRECTNESS.
diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v
index 887a696..0cdecba 100644
--- a/src/translation/HTLgenspec.v
+++ b/src/translation/HTLgenspec.v
@@ -113,41 +113,13 @@ Ltac monadInv H :=
 statemachine that is created by the translation contains the correct
 translations for each of the elements *)
 
-Inductive tr_op : Op.operation -> list reg -> expr -> Prop :=
-| tr_op_Omove : forall r, tr_op Op.Omove (r::nil) (Vvar r)
-| tr_op_Ointconst : forall n l, tr_op (Op.Ointconst n) l (Vlit (intToValue n))
-| tr_op_Oneg : forall r, tr_op Op.Oneg (r::nil) (Vunop Vneg (Vvar r))
-| tr_op_Osub : forall r1 r2, tr_op Op.Osub (r1::r2::nil) (bop Vsub r1 r2)
-| tr_op_Omul : forall r1 r2, tr_op Op.Omul (r1::r2::nil) (bop Vmul r1 r2)
-| tr_op_Omulimm : forall r n, tr_op (Op.Omulimm n) (r::nil) (boplit Vmul r n)
-| tr_op_Odiv : forall r1 r2, tr_op Op.Odiv (r1::r2::nil) (bop Vdiv r1 r2)
-| tr_op_Odivu : forall r1 r2, tr_op Op.Odivu (r1::r2::nil) (bop Vdivu r1 r2)
-| tr_op_Omod : forall r1 r2, tr_op Op.Omod (r1::r2::nil) (bop Vmod r1 r2)
-| tr_op_Omodu : forall r1 r2, tr_op Op.Omodu (r1::r2::nil) (bop Vmodu r1 r2)
-| tr_op_Oand : forall r1 r2, tr_op Op.Oand (r1::r2::nil) (bop Vand r1 r2)
-| tr_op_Oandimm : forall n r, tr_op (Op.Oandimm n) (r::nil) (boplit Vand r n)
-| tr_op_Oor : forall r1 r2, tr_op Op.Oor (r1::r2::nil) (bop Vor r1 r2)
-| tr_op_Oorimm : forall n r, tr_op (Op.Oorimm n) (r::nil) (boplit Vor r n)
-| tr_op_Oxor : forall r1 r2, tr_op Op.Oxor (r1::r2::nil) (bop Vxor r1 r2)
-| tr_op_Oxorimm : forall n r, tr_op (Op.Oxorimm n) (r::nil) (boplit Vxor r n)
-| tr_op_Onot : forall r, tr_op Op.Onot (r::nil) (Vunop Vnot (Vvar r))
-| tr_op_Oshl : forall r1 r2, tr_op Op.Oshl (r1::r2::nil) (bop Vshl r1 r2)
-| tr_op_Oshlimm : forall n r, tr_op (Op.Oshlimm n) (r::nil) (boplit Vshl r n)
-| tr_op_Oshr : forall r1 r2, tr_op Op.Oshr (r1::r2::nil) (bop Vshr r1 r2)
-| tr_op_Oshrimm : forall n r, tr_op (Op.Oshrimm n) (r::nil) (boplit Vshr r n)
-| tr_op_Ocmp : forall c l e s s' i, translate_condition c l s = OK e s' i -> tr_op (Op.Ocmp c) l e
-| tr_op_Olea : forall a l e s s' i, translate_eff_addressing a l s = OK e s' i -> tr_op (Op.Olea a) l e
-| tr_op_Oleal : forall a l e s s' i, translate_eff_addressing a l s = OK e s' i -> tr_op (Op.Oleal a) l e
-| tr_op_Ocast32signed : forall r, tr_op (Op.Ocast32signed) (r::nil) (Vvar r).
-Hint Constructors tr_op : htlspec.
-
 Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> stmnt -> stmnt -> Prop :=
 | tr_instr_Inop :
     forall n,
       tr_instr fin rtrn st stk (RTL.Inop n) Vskip (state_goto st n)
 | tr_instr_Iop :
-    forall n op args e dst,
-      tr_op op args e ->
+    forall n op args dst s s' e i,
+      translate_instr op args s = OK e s' i ->
       tr_instr fin rtrn st stk (RTL.Iop op args dst n) (Vnonblock (Vvar dst) e) (state_goto st n)
 | tr_instr_Icond :
     forall n1 n2 cond args s s' i c,
@@ -163,12 +135,16 @@ 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))
-               (state_goto st n).
+      tr_instr fin rtrn st stk (RTL.Istore mem addr args src n) (Vnonblock c (Vvar src))
+               (state_goto st n)
+| tr_instr_Ijumptable :
+    forall cexpr tbl r,
+    cexpr = tbl_to_case_expr st tbl ->
+    tr_instr fin rtrn st stk (RTL.Ijumptable r tbl) (Vskip) (Vcase (Vvar r) cexpr (Some Vskip)).
 Hint Constructors tr_instr : htlspec.
 
 Inductive tr_code (c : RTL.code) (pc : RTL.node) (i : RTL.instruction) (stmnts trans : PTree.t stmnt)
@@ -184,14 +160,17 @@ Hint Constructors tr_code : htlspec.
 
 Inductive tr_module (f : RTL.function) : module -> Prop :=
   tr_module_intro :
-    forall data control fin rtrn st stk m start rst clk scldecls arrdecls,
+    forall data control fin rtrn st stk stk_len m start rst clk scldecls arrdecls,
       (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) ->
+      Z.modulo (f.(RTL.fn_stacksize)) 4 = 0 ->
+      0 <= f.(RTL.fn_stacksize) < Integers.Ptrofs.modulus ->
       m = (mkmodule f.(RTL.fn_params)
                         data
                         control
                         f.(RTL.fn_entrypoint)
-                        st stk fin rtrn start rst clk scldecls arrdecls) ->
+                        st stk stk_len fin rtrn start rst clk scldecls arrdecls) ->
       tr_module f m.
 Hint Constructors tr_module : htlspec.
 
@@ -315,21 +294,6 @@ Ltac rewrite_states :=
     remember (?x ?s) as c1; remember (?x ?s') as c2; try subst
   end.
 
-Lemma translate_instr_tr_op :
-  forall op args s s' e i,
-    translate_instr op args s = OK e s' i ->
-    tr_op op args e.
-Proof.
-(*  intros.
-  destruct op eqn:?; eauto with htlspec; try discriminate; simpl in *;
-    try (match goal with
-           [ H: match ?args with _ => _ end _ = _ _ _ |- _ ] =>
-           repeat (destruct args; try discriminate)
-         end);
-    monadInv H; constructor.
-Qed.*) Admitted. (* FIXME: Currently admitted because added Osel *)
-Hint Resolve translate_instr_tr_op : htlspec.
-
 Ltac unfold_match H :=
   match type of H with
   | context[match ?g with _ => _ end] => destruct g eqn:?; try discriminate
@@ -343,7 +307,7 @@ Ltac inv_add_instr' H :=
   end; repeat unfold_match H; inversion H.
 
 Ltac inv_add_instr :=
-  match goal with
+  lazymatch goal with
   | H: context[add_instr_skip _ _ _] |- _ =>
     inv_add_instr' H
   | H: context[add_instr_skip _ _] |- _ =>
@@ -356,6 +320,10 @@ Ltac inv_add_instr :=
     inv_add_instr' H
   | H: context[add_branch_instr _ _ _ _] |- _ =>
     monadInv H; inv_incr; inv_add_instr
+  | H: context[add_node_skip _ _ _] |- _ =>
+    inv_add_instr' H
+  | H: context[add_node_skip _ _] |- _ =>
+    monadInv H; inv_incr; inv_add_instr
   end.
 
 Ltac destruct_optional :=
@@ -370,7 +338,7 @@ Lemma iter_expand_instr_spec :
                       c!pc = Some instr ->
                       tr_code c pc instr s'.(st_datapath) s'.(st_controllogic) fin rtrn s'.(st_st) stack).
 Proof.
-(*  induction l; simpl; intros; try contradiction.
+  induction l; simpl; intros; try contradiction.
   destruct a as [pc1 instr1]; simpl in *. inv H0. monadInv H. inv_incr.
   destruct (peq pc pc1).
   - subst.
@@ -383,15 +351,13 @@ Proof.
 
     + destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence.
     + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence.
-    + inversion H2. inversion H14. unfold nonblock. assert (HST: st_st s4 = st_st s2) by congruence. rewrite HST.
-      constructor. eapply translate_instr_tr_op. apply EQ1.
-      eapply in_map with (f := fst) in H14. contradiction.
+    + inversion H2. inversion H14. unfold nonblock. replace (st_st s4) with (st_st s2) by congruence.
+      econstructor. apply EQ1. eapply in_map with (f := fst) in H14. contradiction.
 
     + destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence.
     + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence.
-    + inversion H2. inversion H14. rewrite <- e2. assert (HST: st_st s2 = st_st s0) by congruence.
-      rewrite HST. econstructor. apply EQ1.
-      eapply in_map with (f := fst) in H14. contradiction.
+    + inversion H2. inversion H14. rewrite <- e2. replace (st_st s2) with (st_st s0) by congruence.
+      econstructor. apply EQ1. eapply in_map with (f := fst) in H14. contradiction.
 
     + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence.
     + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence.
@@ -409,6 +375,12 @@ Proof.
         eauto with htlspec.
       * apply in_map with (f := fst) in H2. contradiction.
 
+    + destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence.
+    + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence.
+    + inversion H2.
+      * inversion H14. constructor. congruence.
+      * apply in_map with (f := fst) in H14. contradiction.
+
     + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence.
     + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence.
     + inversion H2.
@@ -428,10 +400,16 @@ Proof.
   - eapply IHl. apply EQ0. assumption.
     destruct H2. inversion H2. subst. contradiction.
     intros. specialize H1 with pc0 instr0. destruct H1. tauto. trivial.
-    destruct H2. inv H2. contradiction. assumption. assumption.*)
-Admitted.
+    destruct H2. inv H2. contradiction. assumption. assumption.
+Qed.
 Hint Resolve iter_expand_instr_spec : htlspec.
 
+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.
+
 Theorem transl_module_correct :
   forall f m,
     transl_module f = Errors.OK m -> tr_module f m.
@@ -444,12 +422,22 @@ Proof.
   inversion s; subst.
 
   unfold transf_module in *.
-  monadInv Heqr.
-  econstructor; simpl; trivial.
+  unfold stack_correct in *.
+  destruct (0 <=? RTL.fn_stacksize f) eqn:STACK_BOUND_LOW;
+    destruct (RTL.fn_stacksize f <? Integers.Ptrofs.modulus) eqn:STACK_BOUND_HIGH;
+    destruct (RTL.fn_stacksize f mod 4 =? 0) eqn:STACK_ALIGN;
+    crush;
+    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; auto.
   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.
diff --git a/src/translation/Veriloggen.v b/src/translation/Veriloggen.v
index efe3565..b550ff9 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.
 
@@ -43,10 +43,10 @@ Definition transl_module (m : HTL.module) : Verilog.module :=
   let case_el_ctrl := transl_list (PTree.elements m.(mod_controllogic)) in
   let case_el_data := transl_list (PTree.elements m.(mod_datapath)) in
   let body :=
-      Valways (Vposedge m.(mod_clk)) (Vcase (Vvar m.(mod_st)) case_el_data (Some Vskip))
-      :: Valways (Vposedge m.(mod_clk)) (Vcond (Vbinop Veq (Vvar m.(mod_reset)) (ZToValue 1 1))
+      Valways (Vposedge m.(mod_clk)) (Vcond (Vbinop Veq (Vvar m.(mod_reset)) (ZToValue 1 1))
                                                (Vnonblock (Vvar m.(mod_st)) (posToValue 32 m.(mod_entrypoint)))
                                                (Vcase (Vvar m.(mod_st)) case_el_ctrl (Some Vskip)))
+      :: Valways (Vposedge m.(mod_clk)) (Vcase (Vvar m.(mod_st)) case_el_data (Some Vskip))
       :: (arr_to_Vdeclarr (AssocMap.elements m.(mod_arrdecls))
                           ++ scl_to_Vdecl (AssocMap.elements m.(mod_scldecls))) in
   Verilog.mkmodule m.(mod_start)
@@ -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).
diff --git a/src/translation/Veriloggenproof.v b/src/translation/Veriloggenproof.v
index 6c58c56..ca4ecab 100644
--- a/src/translation/Veriloggenproof.v
+++ b/src/translation/Veriloggenproof.v
@@ -16,16 +16,68 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-From compcert Require Import Smallstep.
-From coqup Require HTL Verilog.
+From compcert Require Import Smallstep Linking.
+From coqup Require HTL.
+From coqup Require Import Coquplib Veriloggen Verilog.
+
+Definition match_prog (prog : HTL.program) (tprog : Verilog.program) :=
+  match_program (fun cu f tf => tf = transl_fundef f) eq prog tprog.
+
+Lemma transf_program_match:
+  forall prog, match_prog prog (transl_program prog).
+Proof.
+  intros. eapply match_transform_program_contextual. auto.
+Qed.
+
+Inductive match_stacks : list HTL.stackframe -> list stackframe -> Prop :=
+| match_stack :
+    forall res m pc reg_assoc arr_assoc hstk vstk,
+      match_stacks hstk vstk ->
+      match_stacks (HTL.Stackframe res m pc reg_assoc arr_assoc :: hstk)
+                   (Stackframe res (transl_module m) pc
+                                       reg_assoc arr_assoc :: vstk)
+| match_stack_nil : match_stacks nil nil.
+
+Inductive match_states : HTL.state -> state -> Prop :=
+| match_state :
+    forall m st reg_assoc arr_assoc hstk vstk,
+      match_stacks hstk vstk ->
+      match_states (HTL.State hstk m st reg_assoc arr_assoc)
+                   (State vstk (transl_module m) st reg_assoc arr_assoc)
+| match_returnstate :
+    forall v hstk vstk,
+      match_stacks hstk vstk ->
+      match_states (HTL.Returnstate hstk v) (Returnstate vstk v)
+| match_initial_call :
+    forall m,
+      match_states (HTL.Callstate nil m nil) (Callstate nil (transl_module m) nil).
 
 Section CORRECTNESS.
 
   Variable prog: HTL.program.
-  Variable tprog: Verilog.program.
+  Variable tprog: program.
+
+  Hypothesis TRANSL : match_prog prog tprog.
+
+  Let ge : HTL.genv := Globalenvs.Genv.globalenv prog.
+  Let tge : genv := Globalenvs.Genv.globalenv tprog.
+
+  Theorem transl_step_correct :
+    forall (S1 : HTL.state) t S2,
+      HTL.step ge S1 t S2 ->
+      forall (R1 : state),
+        match_states S1 R1 ->
+        exists R2, Smallstep.plus step tge R1 t R2 /\ match_states S2 R2.
+  Proof.
+(*    induction 1; intros R1 MSTATE; inv MSTATE; econstructor; split.
+    - apply Smallstep.plus_one. econstructor. eassumption. trivial.
+      * econstructor. econstructor.*)
+    Admitted.
 
   Theorem transf_program_correct:
     forward_simulation (HTL.semantics prog) (Verilog.semantics tprog).
-  Admitted.
+    Admitted.
+
 
 End CORRECTNESS.
+
diff --git a/src/verilog/Array.v b/src/verilog/Array.v
new file mode 100644
index 0000000..be06541
--- /dev/null
+++ b/src/verilog/Array.v
@@ -0,0 +1,337 @@
+Set Implicit Arguments.
+
+Require Import Lia.
+Require Import Coquplib.
+From Coq Require Import Lists.List Datatypes.
+
+Import ListNotations.
+
+Local Open Scope nat_scope.
+
+Record Array (A : Type) : Type :=
+  mk_array
+    { arr_contents : list A
+    ; arr_length : nat
+    ; arr_wf : length arr_contents = arr_length
+    }.
+
+Definition make_array {A : Type} (l : list A) : Array A :=
+  @mk_array A l (length l) eq_refl.
+
+Fixpoint list_set {A : Type} (i : nat) (x : A) (l : list A) {struct l} : list A :=
+  match i, l with
+  | _, nil => nil
+  | S n, h :: t => h :: list_set n x t
+  | O, h :: t => x :: t
+  end.
+
+Lemma list_set_spec1 {A : Type} :
+  forall l i (x : A),
+    i < length l -> nth_error (list_set i x l) i = Some x.
+Proof.
+  induction l; intros; destruct i; crush; firstorder.
+Qed.
+Hint Resolve list_set_spec1 : array.
+
+Lemma list_set_spec2 {A : Type} :
+  forall l i (x : A) d,
+    i < length l -> nth i (list_set i x l) d = x.
+Proof.
+  induction l; intros; destruct i; crush; firstorder.
+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; crush; 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.
+Proof.
+  induction l; intros; destruct i; auto.
+
+  invert H; crush; auto.
+Qed.
+
+Definition array_set {A : Type} (i : nat) (x : A) (a : Array A) :=
+  let l := a.(arr_contents) in
+  let ln := a.(arr_length) in
+  let WF := a.(arr_wf) in
+  @mk_array A (list_set i x l) ln (@array_set_wf A l ln i x WF).
+
+Lemma array_set_spec1 {A : Type} :
+  forall a i (x : A),
+    i < a.(arr_length) -> nth_error ((array_set i x a).(arr_contents)) i = Some x.
+Proof.
+  intros.
+
+  rewrite <- a.(arr_wf) in H.
+  unfold array_set. crush.
+  eauto with array.
+Qed.
+Hint Resolve array_set_spec1 : array.
+
+Lemma array_set_spec2 {A : Type} :
+  forall a i (x : A) d,
+    i < a.(arr_length) -> nth i ((array_set i x a).(arr_contents)) d = x.
+Proof.
+  intros.
+
+  rewrite <- a.(arr_wf) in H.
+  unfold array_set. crush.
+  eauto with array.
+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. crush.
+Qed.
+
+Definition array_get_error {A : Type} (i : nat) (a : Array A) : option A :=
+  nth_error a.(arr_contents) i.
+
+Lemma array_get_error_equal {A : Type} :
+  forall (a b : Array A) i,
+    a.(arr_contents) = b.(arr_contents) ->
+    array_get_error i a = array_get_error i b.
+Proof.
+  unfold array_get_error. crush.
+Qed.
+
+Lemma array_get_error_bound {A : Type} :
+  forall (a : Array A) i,
+    i < a.(arr_length) -> exists x, array_get_error i a = Some x.
+Proof.
+  intros.
+
+  rewrite <- a.(arr_wf) in H.
+  assert (~ length (arr_contents a) <= i) by lia.
+
+  pose proof (nth_error_None a.(arr_contents) i).
+  apply not_iff_compat in H1.
+  apply <- H1 in H0.
+
+  destruct (nth_error (arr_contents a) i) eqn:EQ; try contradiction; eauto.
+Qed.
+
+Lemma array_get_error_set_bound {A : Type} :
+  forall (a : Array A) i x,
+    i < a.(arr_length) -> array_get_error i (array_set i x a) = Some x.
+Proof.
+  intros.
+
+  unfold array_get_error.
+  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.
+  crush.
+  eauto with array.
+Qed.
+
+Definition array_get {A : Type} (i : nat) (x : A) (a : Array A) : A :=
+  nth i a.(arr_contents) x.
+
+Lemma array_get_set_bound {A : Type} :
+  forall (a : Array A) i x d,
+    i < a.(arr_length) -> array_get i d (array_set i x a) = x.
+Proof.
+  intros.
+
+  unfold array_get.
+  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
+  | O => acc
+  | S n => list_repeat' (a::acc) a n
+  end.
+
+Lemma list_repeat'_len {A : Type} : forall (a : A) n l,
+    length (list_repeat' l a n) = (n + Datatypes.length l)%nat.
+Proof.
+  induction n; intros; crush; try reflexivity.
+
+  specialize (IHn (a :: l)).
+  rewrite IHn.
+  crush.
+Qed.
+
+Lemma list_repeat'_app {A : Type} : forall (a : A) n l,
+    list_repeat' l a n = list_repeat' [] a n ++ l.
+Proof.
+  induction n; intros; crush; try reflexivity.
+
+  pose proof IHn.
+  specialize (H (a :: l)).
+  rewrite H. clear H.
+  specialize (IHn (a :: nil)).
+  rewrite IHn. clear IHn.
+  remember (list_repeat' [] a n) as l0.
+
+  rewrite <- app_assoc.
+  f_equal.
+Qed.
+
+Lemma list_repeat'_head_tail {A : Type} : forall n (a : A),
+  a :: list_repeat' [] a n = list_repeat' [] a n ++ [a].
+Proof.
+  induction n; intros; crush; try reflexivity.
+  rewrite list_repeat'_app.
+
+  replace (a :: list_repeat' [] a n ++ [a]) with (list_repeat' [] a n ++ [a] ++ [a]).
+  2: { rewrite app_comm_cons. rewrite IHn; auto.
+       rewrite app_assoc. reflexivity. }
+  rewrite app_assoc. reflexivity.
+Qed.
+
+Lemma list_repeat'_cons {A : Type} : forall (a : A) n,
+    list_repeat' [a] a n = a :: list_repeat' [] a n.
+Proof.
+  intros.
+
+  rewrite list_repeat'_head_tail; auto.
+  apply list_repeat'_app.
+Qed.
+
+Definition list_repeat {A : Type} : A -> nat -> list A := list_repeat' nil.
+
+Lemma list_repeat_len {A : Type} : forall n (a : A), length (list_repeat a n) = n.
+Proof.
+  intros.
+  unfold list_repeat.
+  rewrite list_repeat'_len.
+  crush.
+Qed.
+
+Lemma dec_list_repeat_spec {A : Type} : forall n (a : A) a',
+    (forall x x' : A, {x' = x} + {~ x' = x}) ->
+    In a' (list_repeat a n) -> a' = a.
+Proof.
+  induction n; intros; crush.
+
+  unfold list_repeat in *.
+  crush.
+
+  rewrite list_repeat'_app in H.
+  pose proof (X a a').
+  destruct H0; auto.
+
+  (* This is actually a degenerate case, not an unprovable goal. *)
+  pose proof (in_app_or (list_repeat' [] a n) ([a])).
+  apply H0 in H. invert H.
+
+  - eapply IHn in X; eassumption.
+  - invert H1; contradiction.
+Qed.
+
+Lemma list_repeat_head_tail {A : Type} : forall n (a : A),
+    a :: list_repeat a n = list_repeat a n ++ [a].
+Proof.
+  unfold list_repeat. apply list_repeat'_head_tail.
+Qed.
+
+Lemma list_repeat_cons {A : Type} : forall n (a : A),
+    list_repeat a (S n) = a :: list_repeat a n.
+Proof.
+  intros.
+
+  unfold list_repeat.
+  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; crush.
+
+  rewrite list_repeat_cons.
+  destruct i; crush; firstorder.
+Qed.
+
+Definition arr_repeat {A : Type} (a : A) (n : nat) : Array A := make_array (list_repeat a n).
+
+Lemma arr_repeat_length {A : Type} : forall n (a : A), arr_length (arr_repeat a n) = n.
+Proof.
+  unfold list_repeat. crush. apply list_repeat_len.
+Qed.
+
+Fixpoint list_combine {A B C : Type} (f : A -> B -> C) (x : list A) (y : list B) : list C :=
+  match x, y with
+  | a :: t, b :: t' => f a b :: list_combine f t t'
+  | _, _ => nil
+  end.
+
+Lemma list_combine_length {A B C : Type} (f : A -> B -> C) : forall (x : list A) (y : list B),
+    length (list_combine f x y) = min (length x) (length y).
+Proof.
+  induction x; intros; crush.
+
+  destruct y; crush; auto.
+Qed.
+
+Definition combine {A B C : Type} (f : A -> B -> C) (x : Array A) (y : Array B) : Array C :=
+  make_array (list_combine f x.(arr_contents) y.(arr_contents)).
+
+Lemma combine_length {A B C: Type} : forall x y (f : A -> B -> C),
+    x.(arr_length) = y.(arr_length) -> arr_length (combine f x y) = x.(arr_length).
+Proof.
+  intros.
+
+  unfold combine.
+  unfold make_array.
+  crush.
+
+  rewrite <- (arr_wf x) in *.
+  rewrite <- (arr_wf y) in *.
+
+  destruct (arr_contents x); destruct (arr_contents y); crush.
+  rewrite list_combine_length.
+  destruct (Min.min_dec (length l) (length l0)); congruence.
+Qed.
+
+Ltac array :=
+  try match goal with
+      | [ |- context[arr_length (combine _ _ _)] ] =>
+        rewrite combine_length
+      | [ |- context[length (list_repeat _ _)] ] =>
+        rewrite list_repeat_len
+      | |- context[array_get_error _ (arr_repeat ?x _) = Some ?x] =>
+        unfold array_get_error, arr_repeat
+      | |- context[nth_error (list_repeat ?x _) _ = Some ?x] =>
+        apply list_repeat_lookup
+      end.
diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v
index c07d672..a3623f0 100644
--- a/src/verilog/HTL.v
+++ b/src/verilog/HTL.v
@@ -17,7 +17,7 @@
  *)
 
 From Coq Require Import FSets.FMapPositive.
-From coqup Require Import Coquplib Value AssocMap.
+From coqup Require Import Coquplib Value AssocMap Array.
 From coqup Require Verilog.
 From compcert Require Events Globalenvs Smallstep Integers Values.
 From compcert Require Import Maps.
@@ -46,6 +46,7 @@ Record module: Type :=
     mod_entrypoint : node;
     mod_st : reg;
     mod_stk : reg;
+    mod_stk_len : nat;
     mod_finish : reg;
     mod_return : reg;
     mod_start : reg;
@@ -65,6 +66,9 @@ Fixpoint init_regs (vl : list value) (rl : list reg) {struct rl} :=
   | _, _ => empty_assocmap
   end.
 
+Definition empty_stack (m : module) : Verilog.assocmap_arr :=
+  (AssocMap.set m.(mod_stk) (Array.arr_repeat None m.(mod_stk_len)) (AssocMap.empty Verilog.arr)).
+
 (** * Operational Semantics *)
 
 Definition genv := Globalenvs.Genv.t fundef unit.
@@ -74,7 +78,8 @@ Inductive stackframe : Type :=
     forall  (res : reg)
             (m : module)
             (pc : node)
-            (assoc : assocmap),
+            (reg_assoc : Verilog.assocmap_reg)
+            (arr_assoc : Verilog.assocmap_arr),
       stackframe.
 
 Inductive state : Type :=
@@ -82,8 +87,8 @@ Inductive state : Type :=
     forall (stack : list stackframe)
            (m : module)
            (st : node)
-           (reg_assoc : assocmap)
-           (arr_assoc : AssocMap.t (list value)), state
+           (reg_assoc : Verilog.assocmap_reg)
+           (arr_assoc : Verilog.assocmap_arr), state
 | Returnstate :
     forall (res : list stackframe)
            (v : value), state
@@ -94,17 +99,19 @@ Inductive state : Type :=
 
 Inductive step : genv -> state -> Events.trace -> state -> Prop :=
 | step_module :
-    forall g m st sf ctrl data
+    forall g m st sf ctrl data ist
       asr asa
       basr1 basa1 nasr1 nasa1
       basr2 basa2 nasr2 nasa2
       asr' asa'
       f stval pstval,
+      asr!(m.(mod_st)) = Some ist ->
+      valueToPos ist = st ->
       m.(mod_controllogic)!st = Some ctrl ->
       m.(mod_datapath)!st = Some data ->
       Verilog.stmnt_runp f
         (Verilog.mkassociations asr empty_assocmap)
-        (Verilog.mkassociations asa (AssocMap.empty (list value)))
+        (Verilog.mkassociations asa (empty_stack m))
         ctrl
         (Verilog.mkassociations basr1 nasr1)
         (Verilog.mkassociations basa1 nasa1) ->
@@ -114,8 +121,8 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop :=
         data
         (Verilog.mkassociations basr2 nasr2)
         (Verilog.mkassociations basa2 nasa2) ->
-      asr' = merge_assocmap nasr2 basr2 ->
-      asa' = AssocMapExt.merge (list value) nasa2 basa2 ->
+      asr' = Verilog.merge_regs nasr2 basr2 ->
+      asa' = Verilog.merge_arrs nasa2 basa2 ->
       asr'!(m.(mod_st)) = Some stval ->
       valueToPos stval = pstval ->
       step g (State sf m st asr asa) Events.E0 (State sf m pstval asr' asa')
@@ -130,13 +137,12 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop :=
            (State res m m.(mod_entrypoint)
              (AssocMap.set (mod_st m) (posToValue 32 m.(mod_entrypoint))
                            (init_regs args m.(mod_params)))
-              (AssocMap.empty (list value)))
+             (empty_stack m))
 | step_return :
-    forall g m asr i r sf pc mst,
+    forall g m asr asa i r sf pc mst,
       mst = mod_st m ->
-      step g (Returnstate (Stackframe r m pc asr :: sf) i) Events.E0
-           (State sf m pc ((asr # mst <- (posToValue 32 pc)) # r <- i)
-                  (AssocMap.empty (list value))).
+      step g (Returnstate (Stackframe r m pc asr asa :: sf) i) Events.E0
+           (State sf m pc ((asr # mst <- (posToValue 32 pc)) # r <- i) asa).
 Hint Constructors step : htl.
 
 Inductive initial_state (p: program): state -> Prop :=
diff --git a/src/verilog/PrintHTL.ml b/src/verilog/PrintHTL.ml
new file mode 100644
index 0000000..0bdba51
--- /dev/null
+++ b/src/verilog/PrintHTL.ml
@@ -0,0 +1,81 @@
+(* -*- mode: tuareg -*-
+ * CoqUp: Verified high-level synthesis.
+ * Copyright (C) 2019-2020 Yann Herklotz <yann@yannherklotz.com>
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <https://www.gnu.org/licenses/>.
+ *)
+
+open Value
+open Datatypes
+open Camlcoq
+open AST
+open Clflags
+open Printf
+open Maps
+open AST
+open HTL
+open PrintAST
+open PrintVerilog
+open CoqupClflags
+
+let pstr pp = fprintf pp "%s"
+
+let reg pp r =
+  fprintf pp "x%d" (P.to_int r)
+
+let rec regs pp = function
+  | [] -> ()
+  | [r] -> reg pp r
+  | r1::rl -> fprintf pp "%a, %a" reg r1 regs rl
+
+let print_instruction pp (pc, i) =
+  fprintf pp "%5d:\t%s" pc (pprint_stmnt 0 i)
+
+let print_module pp id f =
+  fprintf pp "%s(%a) {\n" (extern_atom id) regs f.mod_params;
+  let datapath =
+    List.sort
+      (fun (pc1, _) (pc2, _) -> compare pc2 pc1)
+      (List.rev_map
+        (fun (pc, i) -> (P.to_int pc, i))
+        (PTree.elements f.mod_datapath)) in
+  let controllogic =
+    List.sort
+      (fun (pc1, _) (pc2, _) -> compare pc2 pc1)
+      (List.rev_map
+        (fun (pc, i) -> (P.to_int pc, i))
+        (PTree.elements f.mod_controllogic)) in
+  fprintf pp "  datapath {\n";
+  List.iter (print_instruction pp) datapath;
+  fprintf pp "  }\n\n  controllogic {\n";
+  List.iter (print_instruction pp) controllogic;
+  fprintf pp "  }\n}\n\n"
+
+let print_globdef pp (id, gd) =
+  match gd with
+  | Gfun(Internal f) -> print_module pp id f
+  | _ -> ()
+
+let print_program pp prog =
+  List.iter (print_globdef pp) prog.prog_defs
+
+let destination : string option ref = ref None
+
+let print_if prog =
+  match !destination with
+  | None -> ()
+  | Some f ->
+    let oc = open_out f in
+    print_program oc prog;
+    close_out oc
diff --git a/src/verilog/PrintVerilog.ml b/src/verilog/PrintVerilog.ml
index 5dc0386..5265c97 100644
--- a/src/verilog/PrintVerilog.ml
+++ b/src/verilog/PrintVerilog.ml
@@ -22,9 +22,12 @@ open Datatypes
 
 open Camlcoq
 open AST
+open Clflags
 
 open Printf
 
+open CoqupClflags
+
 let concat = String.concat ""
 
 let indent i = String.make (2 * i) ' '
@@ -75,7 +78,7 @@ let rec pprint_expr = function
   | Vvari (s, i) -> concat [register s; "["; pprint_expr i; "]"]
   | Vinputvar s -> register s
   | Vunop (u, e) -> concat ["("; unop u; pprint_expr e; ")"]
-  | Vbinop (op, a, b) -> concat ["("; pprint_binop (pprint_expr a) (pprint_expr b) op; ")"]
+  | Vbinop (op, a, b) -> concat [pprint_binop (pprint_expr a) (pprint_expr b) op]
   | Vternary (c, t, f) -> concat ["("; pprint_expr c; " ? "; pprint_expr t; " : "; pprint_expr f; ")"]
 
 let rec pprint_stmnt i =
@@ -187,6 +190,12 @@ let debug_always i clk state = concat [
     indent i; "end\n"
   ]
 
+let print_initial i n stk = concat [
+    indent i; "integer i;\n";
+    indent i; "initial for(i = 0; i < "; sprintf "%d" n; "; i++)\n";
+    indent (i+1); register stk; "[i] = 0;\n"
+  ]
+
 let pprint_module debug i n m =
   if (extern_atom n) = "main" then
     let inputs = m.mod_start :: m.mod_reset :: m.mod_clk :: m.mod_args in
@@ -194,6 +203,7 @@ let pprint_module debug i n m =
     concat [ indent i; "module "; (extern_atom n);
              "("; concat (intersperse ", " (List.map register (inputs @ outputs))); ");\n";
              fold_map (pprint_module_item (i+1)) m.mod_body;
+             if !option_initial then print_initial i (Nat.to_int m.mod_stk_len) m.mod_stk else "";
              if debug then debug_always i m.mod_clk m.mod_st else "";
              indent i; "endmodule\n\n"
            ]
diff --git a/src/verilog/PrintVerilog.mli b/src/verilog/PrintVerilog.mli
index 6544e52..62bf63f 100644
--- a/src/verilog/PrintVerilog.mli
+++ b/src/verilog/PrintVerilog.mli
@@ -16,6 +16,8 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
+val pprint_stmnt : int -> Verilog.stmnt -> string
+
 val print_value : out_channel -> Value.value -> unit
 
 val print_program : bool -> out_channel -> Verilog.program -> unit
diff --git a/src/verilog/Value.v b/src/verilog/Value.v
index d527b15..8ba5138 100644
--- a/src/verilog/Value.v
+++ b/src/verilog/Value.v
@@ -19,7 +19,7 @@
 (* begin hide *)
 From bbv Require Import Word.
 From bbv Require HexNotation WordScope.
-From Coq Require Import ZArith.ZArith FSets.FMapPositive.
+From Coq Require Import ZArith.ZArith FSets.FMapPositive Lia.
 From compcert Require Import lib.Integers common.Values.
 (* end hide *)
 
@@ -108,6 +108,11 @@ Definition boolToValue (sz : nat) (b : bool) : value :=
 Definition unify_word (sz1 sz2 : nat) (w1 : word sz2): sz1 = sz2 -> word sz1.
 intros; subst; assumption. Defined.
 
+Lemma unify_word_unfold :
+  forall sz w,
+  unify_word sz sz w eq_refl = w.
+Proof. auto. Qed.
+
 Definition value_eq_size:
   forall v1 v2 : value, { vsize v1 = vsize v2 } + { True }.
 Proof.
@@ -294,8 +299,18 @@ Inductive val_value_lessdef: val -> value -> Prop :=
     forall i v',
     i = valueToInt v' ->
     val_value_lessdef (Vint i) v'
+| val_value_lessdef_ptr:
+    forall b off v',
+    off = Ptrofs.repr (valueToZ v') ->
+    (Z.modulo (valueToZ v') 4) = 0%Z ->
+    val_value_lessdef (Vptr b off) v'
 | lessdef_undef: forall v, val_value_lessdef Vundef v.
 
+Inductive opt_val_value_lessdef: option val -> value -> Prop :=
+| opt_lessdef_some:
+    forall v v', val_value_lessdef v v' -> opt_val_value_lessdef (Some v) v'
+| opt_lessdef_none: forall v, opt_val_value_lessdef None v.
+
 Lemma valueToZ_ZToValue :
   forall n z,
   (- Z.of_nat (2 ^ n) <= z < Z.of_nat (2 ^ n))%Z ->
@@ -314,6 +329,12 @@ Proof.
   auto using uwordToZ_ZToWord.
 Qed.
 
+Lemma uvalueToZ_ZToValue_full :
+  forall sz : nat,
+  (0 < sz)%nat ->
+  forall z : Z, uvalueToZ (ZToValue sz z) = (z mod 2 ^ Z.of_nat sz)%Z.
+Proof. unfold uvalueToZ, ZToValue. simpl. auto using uwordToZ_ZToWord_full. Qed.
+
 Lemma ZToValue_uvalueToZ :
   forall v,
   ZToValue (vsize v) (uvalueToZ v) = v.
@@ -330,7 +351,19 @@ Proof.
   rewrite uvalueToZ_ZToValue. auto. rewrite positive_nat_Z.
   split. apply Zle_0_pos.
 
-  assert (p < 2 ^ (Pos.size p))%positive. apply Pos.size_gt.
+  assert (p < 2 ^ (Pos.size p))%positive by apply Pos.size_gt.
+  inversion H. rewrite <- Z.compare_lt_iff. rewrite <- H1.
+  simpl. rewrite <- Pos2Z.inj_pow_pos. trivial.
+Qed.
+
+Lemma valueToPos_posToValue :
+  forall p, valueToPos (posToValueAuto p) = p.
+Proof.
+  intros. unfold valueToPos, posToValueAuto.
+  rewrite uvalueToZ_ZToValue. auto. rewrite positive_nat_Z.
+  split. apply Zle_0_pos.
+
+  assert (p < 2 ^ (Pos.size p))%positive by apply Pos.size_gt.
   inversion H. rewrite <- Z.compare_lt_iff. rewrite <- H1.
   simpl. rewrite <- Pos2Z.inj_pow_pos. trivial.
 Qed.
@@ -360,4 +393,76 @@ Qed.
 Lemma boolToValue_ValueToBool :
   forall b,
   valueToBool (boolToValue 32 b) = b.
-Proof. destruct b; unfold valueToBool, boolToValue; simpl; trivial. Qed.
+Proof. destruct b; auto. Qed.
+
+Local Open Scope Z.
+
+Ltac word_op_value H :=
+  intros; unfold uvalueToZ, ZToValue; simpl; rewrite unify_word_unfold;
+  rewrite <- H; rewrite uwordToZ_ZToWord_full; auto; omega.
+
+Lemma zadd_vplus :
+  forall sz z1 z2,
+  (sz > 0)%nat ->
+  uvalueToZ (vplus (ZToValue sz z1) (ZToValue sz z2) eq_refl) = (z1 + z2) mod 2 ^ Z.of_nat sz.
+Proof. word_op_value ZToWord_plus. Qed.
+
+Lemma zadd_vplus2 :
+  forall z1 z2,
+  vplus (ZToValue 32 z1) (ZToValue 32 z2) eq_refl = ZToValue 32 (z1 + z2).
+Proof.
+  intros. unfold vplus, ZToValue, map_word2. rewrite unify_word_unfold. simpl.
+  rewrite ZToWord_plus; auto.
+Qed.
+
+Lemma wordsize_32 :
+  Int.wordsize = 32%nat.
+Proof. auto. Qed.
+
+Lemma intadd_vplus :
+  forall i1 i2,
+  valueToInt (vplus (intToValue i1) (intToValue i2) eq_refl) = Int.add i1 i2.
+Proof.
+  intros. unfold Int.add, valueToInt, intToValue. rewrite zadd_vplus.
+  rewrite <- Int.unsigned_repr_eq.
+  rewrite Int.repr_unsigned. auto. rewrite wordsize_32. omega.
+Qed.
+
+Lemma zsub_vminus :
+  forall sz z1 z2,
+  (sz > 0)%nat ->
+  uvalueToZ (vminus (ZToValue sz z1) (ZToValue sz z2) eq_refl) = (z1 - z2) mod 2 ^ Z.of_nat sz.
+Proof. word_op_value ZToWord_minus. Qed.
+
+Lemma zmul_vmul :
+  forall sz z1 z2,
+  (sz > 0)%nat ->
+  uvalueToZ (vmul (ZToValue sz z1) (ZToValue sz z2) eq_refl) = (z1 * z2) mod 2 ^ Z.of_nat sz.
+Proof. word_op_value ZToWord_mult. Qed.
+
+Local Open Scope N.
+Lemma zdiv_vdiv :
+  forall n1 n2,
+  n1 < 2 ^ 32 ->
+  n2 < 2 ^ 32 ->
+  n1 / n2 < 2 ^ 32 ->
+  valueToN (vdiv (NToValue 32 n1) (NToValue 32 n2) eq_refl) = n1 / n2.
+Proof.
+  intros; unfold valueToN, NToValue; simpl; rewrite unify_word_unfold. unfold wdiv.
+  unfold wordBin. repeat (rewrite wordToN_NToWord_2); auto.
+Qed.
+
+(*Lemma ZToValue_valueToNat :
+  forall x sz,
+  sz > 0 ->
+  (x < 2^(Z.of_nat sz))%Z ->
+  valueToNat (ZToValue sz x) = Z.to_nat x.
+Proof.
+  destruct x; intros; unfold ZToValue, valueToNat; simpl.
+  - rewrite wzero'_def. apply wordToNat_wzero.
+  - rewrite posToWord_nat. rewrite wordToNat_natToWord_2. trivial.
+    unfold Z.of_nat in *. destruct sz eqn:?. omega. simpl in H0.
+    rewrite <- Pos2Z.inj_pow_pos in H0. Search (Z.pos _ < Z.pos _)%Z.
+    Search Pos.to_nat (_ < _). (* Pos2Nat.inj_lt *)
+    Search "inj" positive nat.
+*)
diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v
index b80678e..555ddbd 100644
--- a/src/verilog/Verilog.v
+++ b/src/verilog/Verilog.v
@@ -25,9 +25,11 @@ From Coq Require Import
   Lists.List
   Program.
 
+Require Import Lia.
+
 Import ListNotations.
 
-From coqup Require Import common.Coquplib common.Show verilog.Value AssocMap.
+From coqup Require Import common.Coquplib common.Show verilog.Value AssocMap Array.
 From compcert Require Integers Events.
 From compcert Require Import Errors Smallstep Globalenvs.
 
@@ -47,39 +49,51 @@ Record associations (A : Type) : Type :=
     assoc_nonblocking : AssocMap.t A
   }.
 
+Definition arr := (Array (option value)).
+
 Definition reg_associations := associations value.
-Definition arr_associations := associations (list value).
+Definition arr_associations := associations arr.
 
-Definition assocmap_arr := AssocMap.t (list value).
+Definition assocmap_reg := AssocMap.t value.
+Definition assocmap_arr := AssocMap.t arr.
 
-Definition merge_associations {A : Type} (assoc : associations A) :=
-  mkassociations (AssocMapExt.merge A assoc.(assoc_nonblocking) assoc.(assoc_blocking))
-                 (AssocMap.empty A).
+Definition merge_regs (new : assocmap_reg) (old : assocmap_reg) : assocmap_reg :=
+  AssocMapExt.merge value new old.
+
+Definition merge_cell (new : option value) (old : option value) : option value :=
+  match new, old with
+  | Some _, _ => new
+  | _, _ => old
+  end.
+
+Definition merge_arr (new : option arr) (old : option arr) : option arr :=
+  match new, old with
+  | Some new', Some old' => Some (combine merge_cell new' old')
+  | Some new', None => Some new'
+  | None, Some old' => Some old'
+  | None, None => None
+  end.
+
+Definition merge_arrs (new : assocmap_arr) (old : assocmap_arr) : assocmap_arr :=
+  AssocMap.combine merge_arr new old.
 
 Definition arr_assocmap_lookup (a : assocmap_arr) (r : reg) (i : nat) : option value :=
   match a ! r with
   | None => None
-  | Some arr => nth_error arr i
-  end.
-
-Fixpoint list_set {A : Type} (i : nat) (x : A) (l : list A) : list A :=
-  match i, l with
-  | _, nil => nil
-  | S n, h :: t => h :: list_set n x t
-  | O, h :: t => x :: t
+  | Some arr => Some (Option.default (NToValue 32 0) (Option.join (array_get_error i arr)))
   end.
 
-Definition assocmap_l_set (r : reg) (i : nat) (v : value) (a : assocmap_arr) : assocmap_arr :=
+Definition arr_assocmap_set (r : reg) (i : nat) (v : value) (a : assocmap_arr) : assocmap_arr :=
   match a ! r with
   | None => a
-  | Some arr => AssocMap.set r (list_set i v arr) a
+  | Some arr => a # r <- (array_set i (Some v) arr)
   end.
 
 Definition block_arr (r : reg) (i : nat) (asa : arr_associations) (v : value) : arr_associations :=
-  mkassociations (assocmap_l_set r i v asa.(assoc_blocking)) asa.(assoc_nonblocking).
+  mkassociations (arr_assocmap_set r i v asa.(assoc_blocking)) asa.(assoc_nonblocking).
 
 Definition nonblock_arr (r : reg) (i : nat) (asa : arr_associations) (v : value) : arr_associations :=
-  mkassociations asa.(assoc_blocking) (assocmap_l_set r i v asa.(assoc_nonblocking)).
+  mkassociations asa.(assoc_blocking) (arr_assocmap_set r i v asa.(assoc_nonblocking)).
 
 Definition block_reg (r : reg) (asr : reg_associations) (v : value) :=
   mkassociations (AssocMap.set r v asr.(assoc_blocking)) asr.(assoc_nonblocking).
@@ -87,8 +101,8 @@ Definition block_reg (r : reg) (asr : reg_associations) (v : value) :=
 Definition nonblock_reg (r : reg) (asr : reg_associations) (v : value) :=
   mkassociations asr.(assoc_blocking) (AssocMap.set r v asr.(assoc_nonblocking)).
 
-Inductive scl_decl : Type := Scalar (sz : nat).
-Inductive arr_decl : Type := Array (sz : nat) (ln : nat).
+Inductive scl_decl : Type := VScalar (sz : nat).
+Inductive arr_decl : Type := VArray (sz : nat) (ln : nat).
 
 (** * Verilog AST
 
@@ -218,6 +232,7 @@ Record module : Type := mkmodule {
   mod_return : reg;
   mod_st : reg; (**r Variable that defines the current state, it should be internal. *)
   mod_stk : reg;
+  mod_stk_len : nat;
   mod_args : list reg;
   mod_body : list module_item;
   mod_entrypoint : node;
@@ -235,7 +250,7 @@ Definition posToLit (p : positive) : expr :=
 Coercion Vlit : value >-> expr.
 Coercion Vvar : reg >-> expr.
 
-Definition fext := AssocMap.t value.
+Definition fext := assocmap.
 Definition fextclk := nat -> fext.
 
 (** ** State
@@ -264,7 +279,8 @@ Inductive stackframe : Type :=
     forall  (res : reg)
             (m : module)
             (pc : node)
-            (assoc : assocmap),
+            (reg_assoc : assocmap_reg)
+            (arr_assoc : assocmap_arr),
       stackframe.
 
 Inductive state : Type :=
@@ -272,8 +288,8 @@ Inductive state : Type :=
     forall (stack : list stackframe)
            (m : module)
            (st : node)
-           (reg_assoc : assocmap)
-           (arr_assoc : AssocMap.t (list value)), state
+           (reg_assoc : assocmap_reg)
+           (arr_assoc : assocmap_arr), state
 | Returnstate :
     forall (res : list stackframe)
            (v : value), state
@@ -691,17 +707,21 @@ Fixpoint init_params (vl : list value) (rl : list reg) {struct rl} :=
   end.
 
 Definition genv := Globalenvs.Genv.t fundef unit.
+Definition empty_stack (m : module) : assocmap_arr :=
+  (AssocMap.set m.(mod_stk) (Array.arr_repeat None m.(mod_stk_len)) (AssocMap.empty arr)).
 
 Inductive step : genv -> state -> Events.trace -> state -> Prop :=
   | step_module :
-      forall asr asa asr' asa' basr1 nasr1 basa1 nasa1 f stval pstval m sf st g,
+      forall asr asa asr' asa' basr1 nasr1 basa1 nasa1 f stval pstval m sf st g ist,
+      asr!(m.(mod_st)) = Some ist ->
+      valueToPos ist = st ->
       mis_stepp f (mkassociations asr empty_assocmap)
-                  (mkassociations asa (AssocMap.empty (list value)))
+                  (mkassociations asa (empty_stack m))
                   m.(mod_body)
                   (mkassociations basr1 nasr1)
                   (mkassociations basa1 nasa1)->
-      asr' = merge_assocmap nasr1 basr1 ->
-      asa' = AssocMapExt.merge (list value) nasa1 basa1 ->
+      asr' = merge_regs nasr1 basr1 ->
+      asa' = merge_arrs nasa1 basa1 ->
       asr'!(m.(mod_st)) = Some stval ->
       valueToPos stval = pstval ->
       step g (State sf m st asr asa) Events.E0 (State sf m pstval asr' asa')
@@ -716,13 +736,13 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop :=
          (State res m m.(mod_entrypoint)
           (AssocMap.set m.(mod_st) (posToValue 32 m.(mod_entrypoint))
            (init_params args m.(mod_args)))
-          (AssocMap.empty (list value)))
+          (empty_stack m))
 | step_return :
-    forall g m asr i r sf pc mst,
+    forall g m asr i r sf pc mst asa,
     mst = mod_st m ->
-    step g (Returnstate (Stackframe r m pc asr :: sf) i) Events.E0
+    step g (Returnstate (Stackframe r m pc asr asa :: sf) i) Events.E0
          (State sf m pc ((asr # mst <- (posToValue 32 pc)) # r <- i)
-                (AssocMap.empty (list value))).
+                (empty_stack m)).
 Hint Constructors step : verilog.
 
 Inductive initial_state (p: program): state -> Prop :=
diff --git a/test/array.c b/test/array.c
index e33d47b..7d78a61 100644
--- a/test/array.c
+++ b/test/array.c
@@ -1,4 +1,7 @@
 int main() {
-        int x[5] = {1, 2, 3, 4, 5};
-        return x[2];
+    int x[3] = {1, 2, 3};
+    int sum = 0, incr = 1;
+    for (int i = 0; i < 3; i=i+incr)
+        sum += x[i];
+    return sum;
 }
diff --git a/test/loop.c b/test/loop.c
index b459e3a..52e4fe9 100644
--- a/test/loop.c
+++ b/test/loop.c
@@ -1,10 +1,12 @@
 int main() {
     int max = 5;
     int acc = 0;
+    int b = 1;
+    int c = 2;
     
-    for (int i = 0; i < max; i++) {
+    for (int i = 0; i < max; i = i + b) {
         acc += i;
     }
 
-    return acc + 2;
+    return acc + c;
 }
diff --git a/test/matrix.c b/test/matrix.c
index 2bb17e7..daa00ae 100644
--- a/test/matrix.c
+++ b/test/matrix.c
@@ -1,10 +1,8 @@
-#define N 4
-
-void matrix_multiply(int first[N][N], int second[N][N], int multiply[N][N]) {
+void matrix_multiply(int first[2][2], int second[2][2], int multiply[2][2]) {
     int sum = 0;
-    for (int c = 0; c < N; c++) {
-        for (int d = 0; d < N; d++) {
-            for (int k = 0; k < N; k++) {
+    for (int c = 0; c < 2; c++) {
+        for (int d = 0; d < 2; d++) {
+            for (int k = 0; k < 2; k++) {
                 sum = sum + first[c][k]*second[k][d];
             }
             multiply[c][d] = sum;
@@ -14,9 +12,9 @@ void matrix_multiply(int first[N][N], int second[N][N], int multiply[N][N]) {
 }
 
 int main() {
-    int f[N][N] = {{1, 2, 3, 4}, {1, 2, 3, 4}, {1, 2, 3, 4}, {1, 2, 3, 4}};
-    int s[N][N] = {{5, 6, 7, 8}, {5, 6, 7, 8}, {5, 6, 7, 8}, {5, 6, 7, 8}};
-    int m[N][N] = {{0, 0, 0, 0}, {0, 0, 0, 0}, {0, 0, 0, 0}, {0, 0, 0, 0}};
+    int f[2][2] = {{1, 2}, {3, 4}};
+    int s[2][2] = {{5, 6}, {7, 8}};
+    int m[2][2] = {{0, 0}, {0, 0}};
 
     matrix_multiply(f, s, m);
     return m[1][1];