Merge branch 'develop' into dev-nadesh

5 files changed, 1883 insertions, 196 deletions

diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v
index c96d4c7..a75ef5c 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 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 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 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 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 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..2f296f2 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.
 From coqup Require HTL Verilog.
 
+Require Import Lia.
+
 Local Open Scope assocmap.
 
 Hint Resolve Smallstep.forward_simulation_plus : htlproof.
@@ -42,44 +44,71 @@ 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 :=
+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 < 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.
+
+Inductive match_stacks (mem : mem) : list RTL.stackframe -> list HTL.stackframe -> Prop :=
 | match_stacks_nil :
-    match_stacks nil nil
+    match_stacks mem nil nil
 | match_stacks_cons :
-    forall cs lr r f sp pc rs m assoc
+    forall cs lr r f sp sp' pc rs m asr asa
            (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 ->
-    (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.
+           (ST: match_stacks 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),
+      match_stacks mem (RTL.Stackframe r f sp pc rs :: cs)
+                       (HTL.Stackframe r m pc asr asa :: lr).
 
 Inductive match_states : RTL.state -> HTL.state -> Prop :=
-| match_state : forall asa asr sf f sp rs mem m st res
+| 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),
+    (MS : match_stacks mem 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),
     match_states (RTL.State sf f sp st rs mem)
                  (HTL.State res m st asr asa)
 | match_returnstate :
     forall
-      v v' stack m res
-      (MS : match_stacks stack res),
+      v v' stack mem res
+      (MS : match_stacks mem stack res),
       val_value_lessdef v v' ->
-      match_states (RTL.Returnstate stack v m) (HTL.Returnstate res v')
+      match_states (RTL.Returnstate stack v mem) (HTL.Returnstate res v')
 | match_initial_call :
     forall f m m0
     (TF : tr_module f m),
@@ -87,12 +116,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 +169,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; simplify.
+  - symmetry. apply length_zero_iff_nil. auto.
+  - destruct l; simplify.
+    rewrite list_repeat_cons.
+    simplify. f_equal.
+    eauto.
+Qed.
+
+Lemma combine_none :
+  forall n a,
+    a.(arr_length) = n ->
+    arr_contents (combine Verilog.merge_cell (arr_repeat None n) a) = arr_contents a.
+Proof.
+  intros.
+  unfold combine.
+  simplify.
+
+  rewrite <- (arr_wf a) in H.
+  apply list_combine_none.
+  assumption.
+Qed.
+
+Lemma list_combine_lookup_first :
+  forall l1 l2 n,
+    length l1 = length l2 ->
+    nth_error l1 n = Some None ->
+    nth_error (list_combine Verilog.merge_cell l1 l2) n = nth_error l2 n.
+Proof.
+  induction l1; intros; simplify.
+
+  rewrite nth_error_nil in H0.
+  discriminate.
+
+  destruct l2 eqn:EQl2. simplify.
+  simpl in H. invert H.
+  destruct n; simpl in *.
+  invert H0. simpl. reflexivity.
+  eauto.
+Qed.
+
+Lemma combine_lookup_first :
+  forall a1 a2 n,
+    a1.(arr_length) = a2.(arr_length) ->
+    array_get_error n a1 = Some None ->
+    array_get_error n (combine Verilog.merge_cell a1 a2) = array_get_error n a2.
+Proof.
+  intros.
+
+  unfold array_get_error in *.
+  apply list_combine_lookup_first; eauto.
+  rewrite a1.(arr_wf). rewrite a2.(arr_wf).
+  assumption.
+Qed.
+
+Lemma list_combine_lookup_second :
+  forall l1 l2 n x,
+    length l1 = length l2 ->
+    nth_error l1 n = Some (Some x) ->
+    nth_error (list_combine Verilog.merge_cell l1 l2) n = Some (Some x).
+Proof.
+  induction l1; intros; simplify; auto.
+
+  destruct l2 eqn:EQl2. simplify.
+  simpl in H. invert H.
+  destruct n; simpl in *.
+  invert H0. simpl. reflexivity.
+  eauto.
+Qed.
+
+Lemma combine_lookup_second :
+  forall a1 a2 n x,
+    a1.(arr_length) = a2.(arr_length) ->
+    array_get_error n a1 = Some (Some x) ->
+    array_get_error n (combine Verilog.merge_cell a1 a2) = Some (Some x).
+Proof.
+  intros.
+
+  unfold array_get_error in *.
+  apply list_combine_lookup_second; eauto.
+  rewrite a1.(arr_wf). rewrite a2.(arr_wf).
+  assumption.
+Qed.
+
 (* Need to eventually move posToValue 32 to posToValueAuto, as that has this proof. *)
 Lemma assumption_32bit :
   forall v,
@@ -205,13 +333,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 +350,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 +360,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,6 +412,7 @@ 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 ->
@@ -295,23 +427,54 @@ Section CORRECTNESS.
       split.
       apply Smallstep.plus_one.
       eapply HTL.step_module; eauto.
+      apply assumption_32bit.
       (* processing of state *)
       econstructor.
-      simpl. trivial.
+      simplify.
       econstructor.
       econstructor.
       econstructor.
+      simplify.
 
-      (* prove stval *)
-      unfold merge_assocmap.
-      unfold_merge. simpl. apply AssocMap.gss.
+      unfold Verilog.merge_regs.
+      unfold_merge. apply AssocMap.gss.
 
       (* prove match_state *)
       rewrite assumption_32bit.
-      constructor; auto.
+      econstructor; simplify; eauto.
+
+      unfold Verilog.merge_regs.
       unfold_merge. simpl. apply regs_lessdef_add_greater. apply greater_than_max_func.
       assumption.
+      unfold Verilog.merge_regs.
       unfold state_st_wf. inversion 1. subst. unfold_merge. apply AssocMap.gss.
+
+      (* prove match_arrs *)
+      invert MARR. simplify.
+      unfold HTL.empty_stack. simplify. unfold Verilog.merge_arrs.
+      econstructor.
+      simplify. repeat split.
+
+      rewrite AssocMap.gcombine.
+      2: { reflexivity. }
+      rewrite AssocMap.gss.
+      unfold Verilog.merge_arr.
+      setoid_rewrite H5.
+      reflexivity.
+
+      rewrite combine_length.
+      unfold arr_repeat. simplify.
+      rewrite list_repeat_len.
+      reflexivity.
+
+      unfold arr_repeat. simplify.
+      rewrite list_repeat_len; auto.
+      intros.
+      erewrite array_get_error_equal.
+      eauto. apply combine_none.
+
+      assumption.
+
     - (* Iop *)
       (* destruct v eqn:?; *)
       (*          try ( *)
@@ -390,11 +553,1317 @@ Section CORRECTNESS.
       (* assumption. *)
       admit.
 
-    - admit.
-    - admit.
+      Ltac rt :=
+        repeat match goal with
+        | [ _ : error _ _ = OK _ _ _ |- _ ] => discriminate
+        | [ _ : context[if (?x && ?y) then _ else _] |- _ ] =>
+          let EQ1 := fresh "EQ" in
+          let EQ2 := fresh "EQ" in
+          destruct x eqn:EQ1; destruct y eqn:EQ2; simpl in *
+        | [ _ : context[if ?x then _ else _] |- _ ] =>
+          let EQ := fresh "EQ" in
+          destruct x eqn:EQ; simpl in *
+        | [ H : ret _ _ = _  |- _ ] => invert H
+        | [ _ : context[match ?x with | _ => _ end] |- _ ] => destruct x
+        end.
+
+    - (* FIXME: Should be able to use the spec to avoid destructing here? *)
+      destruct c, chunk, addr, args; simplify; rt; simplify.
+
+      + (** Preamble *)
+        invert MARR. simplify.
+
+        unfold Op.eval_addressing in H0.
+        destruct (Archi.ptr64) eqn:ARCHI; simplify.
+
+        unfold reg_stack_based_pointers in RSBP.
+        pose proof (RSBP r0) as RSBPr0.
+
+        destruct (Registers.Regmap.get r0 rs) eqn:EQr0; simplify.
+
+        rewrite ARCHI in H1. simplify.
+        subst.
+
+        pose proof MASSOC as MASSOC'.
+        invert MASSOC'.
+        pose proof (H0 r0).
+        assert (HPler0 : Ple r0 (RTL.max_reg_function f))
+          by (eapply RTL.max_reg_function_use; eauto; simplify; eauto).
+        apply H6 in HPler0.
+        invert HPler0; try congruence.
+        rewrite EQr0 in H8.
+        invert H8.
+        clear H0. clear H6.
+
+        unfold check_address_parameter_signed in *;
+        unfold check_address_parameter_unsigned in *; simplify.
+
+        remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (valueToZ asr # r0))
+                                      (Integers.Ptrofs.of_int (Integers.Int.repr z))) as OFFSET.
+
+        (** Read bounds assumption *)
+        assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH by admit.
+
+        (** Modular preservation proof *)
+        assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE.
+        { rewrite HeqOFFSET.
+          apply PtrofsExtra.add_mod; simplify; try lia.
+          exists 1073741824. reflexivity. (* FIXME: This is sadness inducing. *)
+          rewrite Integers.Ptrofs.signed_repr; try assumption.
+          admit. (* FIXME: Register bounds. *)
+          apply PtrofsExtra.of_int_mod.
+          rewrite Integers.Int.signed_repr; simplify; try split; try assumption.
+        }
+
+        (** 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; simplify; auto; lia. }
+
+        (** 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; simplify.
+          apply Zmult_lt_reg_r with (p := 4); try lia.
+          repeat rewrite ZLib.div_mul_undo; try lia.
+          split.
+          apply Z.div_pos; try lia; apply Integers.Ptrofs.unsigned_range_2.
+          apply Z.div_le_upper_bound; lia. }
+
+        inversion NORMALISE_BOUND as [ NORMALISE_BOUND_LOW NORMALISE_BOUND_HIGH ];
+        clear NORMALISE_BOUND.
+
+        eexists. split.
+        eapply Smallstep.plus_one.
+        eapply HTL.step_module; eauto.
+        apply assumption_32bit.
+        econstructor. econstructor. econstructor. simplify.
+        econstructor. econstructor. econstructor. simplify.
+        eapply Verilog.erun_Vbinop with (EQ := ?[EQ1]). (* FIXME: These will be shelved and cause sadness. *)
+        eapply Verilog.erun_Vbinop with (EQ := ?[EQ2]).
+        econstructor. econstructor. econstructor. econstructor.
+        econstructor. econstructor. econstructor. econstructor.
+
+        all: simplify.
+
+        (** Verilog array lookup *)
+        unfold Verilog.arr_assocmap_lookup. setoid_rewrite H5.
+        f_equal.
+
+        (** State Lookup *)
+        unfold Verilog.merge_regs.
+        simplify.
+        unfold_merge.
+        rewrite AssocMap.gso.
+        apply AssocMap.gss.
+        apply st_greater_than_res.
+
+        (** Match states *)
+        rewrite assumption_32bit.
+        econstructor; eauto.
+
+        (** Match assocmaps *)
+        unfold Verilog.merge_regs. simplify. unfold_merge.
+        apply regs_lessdef_add_match.
+
+        (** Equality proof *)
+        assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
+        rewrite ZERO in H7. clear ZERO.
+        setoid_rewrite Integers.Ptrofs.add_zero_l in H7.
+
+        specialize (H7 (Integers.Ptrofs.unsigned
+                          (Integers.Ptrofs.divu
+                             OFFSET
+                             (Integers.Ptrofs.repr 4)))).
+
+        exploit H7.
+        rewrite Z2Nat.id; eauto.
+        apply Z.div_pos; lia.
+
+        intros I.
+
+        assert (Z.to_nat
+                  (Integers.Ptrofs.unsigned
+                     (Integers.Ptrofs.divu
+                        OFFSET
+                        (Integers.Ptrofs.repr 4)))
+                =
+                valueToNat (vdiv (vplus asr # r0 (ZToValue 32 z) ?EQ2) (ZToValue 32 4) ?EQ1))
+          as EXPR_OK by admit.
+        rewrite <- EXPR_OK.
+        rewrite NORMALISE in I.
+        rewrite H1 in I.
+        invert I. assumption.
+
+        (** PC match *)
+        apply regs_lessdef_add_greater.
+        apply greater_than_max_func.
+        assumption.
+
+        (** States well formed *)
+        unfold state_st_wf. inversion 1. simplify.
+        unfold Verilog.merge_regs.
+        unfold_merge. rewrite AssocMap.gso.
+        apply AssocMap.gss.
+        apply st_greater_than_res.
+
+        (** Match arrays *)
+        econstructor.
+        repeat split; simplify.
+        unfold HTL.empty_stack.
+        simplify.
+        unfold Verilog.merge_arrs.
+
+        rewrite AssocMap.gcombine.
+        2: { reflexivity. }
+        rewrite AssocMap.gss.
+        unfold Verilog.merge_arr.
+        setoid_rewrite H5.
+        reflexivity.
+
+        rewrite combine_length.
+        unfold arr_repeat. simplify.
+        rewrite list_repeat_len.
+        reflexivity.
+
+        unfold arr_repeat. simplify.
+        rewrite list_repeat_len.
+        congruence.
+
+        intros.
+        erewrite array_get_error_equal.
+        eauto. apply combine_none.
+        assumption.
+
+        (** RSBP preservation *)
+        unfold reg_stack_based_pointers. intros.
+        destruct (Pos.eq_dec r1 dst); try rewrite e. (* FIXME: Prepare this for automation *)
+
+        rewrite Registers.Regmap.gss.
+        unfold arr_stack_based_pointers in ASBP.
+        specialize (ASBP (Integers.Ptrofs.unsigned
+                            (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)))).
+        exploit ASBP; auto; intros I.
+
+        rewrite NORMALISE in I.
+        assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
+        rewrite ZERO in I. clear ZERO.
+        simplify.
+        rewrite Integers.Ptrofs.add_zero_l in I.
+        rewrite H1 in I.
+        assumption.
+        simplify.
+
+        rewrite Registers.Regmap.gso; auto.
+
+      + (** Preamble *)
+        invert MARR. simplify.
+
+        unfold Op.eval_addressing in H0.
+        destruct (Archi.ptr64) eqn:ARCHI; simplify.
+
+        unfold reg_stack_based_pointers in RSBP.
+        pose proof (RSBP r0) as RSBPr0.
+        pose proof (RSBP r1) as RSBPr1.
+
+        destruct (Registers.Regmap.get r0 rs) eqn:EQr0;
+        destruct (Registers.Regmap.get r1 rs) eqn:EQr1; simplify.
+
+        rewrite ARCHI in H1. simplify.
+        subst.
+        clear RSBPr1.
+
+        pose proof MASSOC as MASSOC'.
+        invert MASSOC'.
+        pose proof (H0 r0).
+        pose proof (H0 r1).
+        assert (HPler0 : Ple r0 (RTL.max_reg_function f))
+          by (eapply RTL.max_reg_function_use; eauto; simplify; eauto).
+        assert (HPler1 : Ple r1 (RTL.max_reg_function f))
+          by (eapply RTL.max_reg_function_use; eauto; simpl; auto).
+        apply H6 in HPler0.
+        apply H8 in HPler1.
+        invert HPler0; invert HPler1; try congruence.
+        rewrite EQr0 in H10.
+        rewrite EQr1 in H12.
+        invert H10. invert H12.
+        clear H0. clear H6. clear H8.
+
+        unfold check_address_parameter_signed in *;
+        unfold check_address_parameter_unsigned in *; simplify.
+
+        remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (valueToZ asr # r0))
+                                      (Integers.Ptrofs.of_int
+                                         (Integers.Int.add (Integers.Int.mul (valueToInt asr # r1) (Integers.Int.repr z))
+                                                           (Integers.Int.repr z0)))) as OFFSET.
+
+        (** Read bounds assumption *)
+        assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH by admit.
+
+        (** Modular preservation proof *)
+        assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE.
+        { rewrite HeqOFFSET.
+          apply PtrofsExtra.add_mod; simplify; try lia.
+          exists 1073741824. reflexivity. (* FIXME: This is sadness inducing. *)
+          rewrite Integers.Ptrofs.signed_repr; try assumption.
+          admit. (* FIXME: Register bounds. *)
+          apply PtrofsExtra.of_int_mod.
+          apply IntExtra.add_mod; simplify; try lia.
+          exists 1073741824. reflexivity. (* FIXME: This is sadness inducing. *)
+          apply IntExtra.mul_mod; simplify; try lia.
+          exists 1073741824. reflexivity. (* FIXME: This is sadness inducing. *)
+          admit. (* FIXME: Register bounds. *)
+          rewrite Integers.Int.signed_repr; simplify; try split; try assumption.
+          rewrite Integers.Int.signed_repr; simplify; try split; try assumption.
+        }
+
+        (** 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; simplify; auto; lia. }
+
+        (** 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; simplify.
+          apply Zmult_lt_reg_r with (p := 4); try lia.
+          repeat rewrite ZLib.div_mul_undo; try lia.
+          split.
+          apply Z.div_pos; try lia; apply Integers.Ptrofs.unsigned_range_2.
+          apply Z.div_le_upper_bound; lia. }
+
+        inversion NORMALISE_BOUND as [ NORMALISE_BOUND_LOW NORMALISE_BOUND_HIGH ];
+        clear NORMALISE_BOUND.
+
+        (** Start of proof proper *)
+        eexists. split.
+        eapply Smallstep.plus_one.
+        eapply HTL.step_module; eauto.
+        apply assumption_32bit.
+        econstructor. econstructor. econstructor. simplify.
+        econstructor. econstructor. econstructor. simplify.
+        eapply Verilog.erun_Vbinop with (EQ := ?[EQ3]). (* FIXME: These will be shelved and cause sadness. *)
+        eapply Verilog.erun_Vbinop with (EQ := ?[EQ4]).
+        eapply Verilog.erun_Vbinop with (EQ := ?[EQ5]).
+        econstructor. econstructor. econstructor. econstructor.
+        econstructor.
+        eapply Verilog.erun_Vbinop with (EQ := ?[EQ6]).
+        econstructor. econstructor. econstructor. econstructor.
+        econstructor. econstructor. econstructor. econstructor.
+        econstructor. econstructor.
+
+        all: simplify.
+
+        (** Verilog array lookup *)
+        unfold Verilog.arr_assocmap_lookup. setoid_rewrite H5.
+        f_equal.
+
+        (** State Lookup *)
+        unfold Verilog.merge_regs.
+        simplify.
+        unfold_merge.
+        rewrite AssocMap.gso.
+        apply AssocMap.gss.
+        apply st_greater_than_res.
+
+        (** Match states *)
+        rewrite assumption_32bit.
+        econstructor; eauto.
+
+        (** Match assocmaps *)
+        unfold Verilog.merge_regs. simplify. unfold_merge.
+        apply regs_lessdef_add_match.
+
+        (** Equality proof *)
+        assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
+        rewrite ZERO in H7. clear ZERO.
+        setoid_rewrite Integers.Ptrofs.add_zero_l in H7.
+
+        specialize (H7 (Integers.Ptrofs.unsigned
+                          (Integers.Ptrofs.divu
+                             OFFSET
+                             (Integers.Ptrofs.repr 4)))).
+
+        exploit H7.
+        rewrite Z2Nat.id; eauto.
+        apply Z.div_pos; lia.
+
+        intros I.
+        assert (Z.to_nat
+                  (Integers.Ptrofs.unsigned
+                     (Integers.Ptrofs.divu
+                        OFFSET
+                        (Integers.Ptrofs.repr 4)))
+                = valueToNat
+                    (vdiv (vplus (vplus asr # r0 (ZToValue 32 z0) ?EQ5)
+                                 (vmul asr # r1 (ZToValue 32 z) ?EQ6) ?EQ4) (ZToValue 32 4) ?EQ3))
+          as EXPR_OK by admit.
+        rewrite <- EXPR_OK.
+        rewrite NORMALISE in I.
+        rewrite H1 in I.
+        invert I. assumption.
+
+        (** PC match *)
+        apply regs_lessdef_add_greater.
+        apply greater_than_max_func.
+        assumption.
+
+        (** States well formed *)
+        unfold state_st_wf. inversion 1. simplify.
+        unfold Verilog.merge_regs.
+        unfold_merge. rewrite AssocMap.gso.
+        apply AssocMap.gss.
+        apply st_greater_than_res.
+
+        (** Match arrays *)
+        econstructor.
+        repeat split; simplify.
+        unfold HTL.empty_stack.
+        simplify.
+        unfold Verilog.merge_arrs.
+
+        rewrite AssocMap.gcombine.
+        2: { reflexivity. }
+        rewrite AssocMap.gss.
+        unfold Verilog.merge_arr.
+        setoid_rewrite H5.
+        reflexivity.
+
+        rewrite combine_length.
+        unfold arr_repeat. simplify.
+        rewrite list_repeat_len.
+        reflexivity.
+
+        unfold arr_repeat. simplify.
+        rewrite list_repeat_len.
+        congruence.
+
+        intros.
+        erewrite array_get_error_equal.
+        eauto. apply combine_none.
+        assumption.
+
+        (** RSBP preservation *)
+        unfold reg_stack_based_pointers. intros.
+        destruct (Pos.eq_dec r2 dst); try rewrite e. (* FIXME: Prepare this for automation *)
+
+        rewrite Registers.Regmap.gss.
+        unfold arr_stack_based_pointers in ASBP.
+        specialize (ASBP (Integers.Ptrofs.unsigned
+                            (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)))).
+        exploit ASBP; auto; intros I.
+
+        rewrite NORMALISE in I.
+        assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
+        rewrite ZERO in I. clear ZERO.
+        simplify.
+        rewrite Integers.Ptrofs.add_zero_l in I.
+        rewrite H1 in I.
+        assumption.
+        simplify.
+
+        rewrite Registers.Regmap.gso; auto.
+
+      + invert MARR. simplify.
+
+        unfold Op.eval_addressing in H0.
+        destruct (Archi.ptr64) eqn:ARCHI; simplify.
+        rewrite ARCHI in H0. simplify.
+
+        unfold check_address_parameter_unsigned in *;
+        unfold check_address_parameter_signed in *; simplify.
+
+        assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
+        rewrite ZERO in H1. clear ZERO.
+        rewrite Integers.Ptrofs.add_zero_l in H1.
+
+        remember i0 as OFFSET.
+
+        (** Read bounds assumption *)
+        assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH by admit.
+
+        (** Modular preservation proof *)
+        rename H0 into MOD_PRESERVE.
+
+        (** 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; simplify; auto; try lia. }
+
+        (** 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; simplify.
+          apply Zmult_lt_reg_r with (p := 4); try lia.
+          repeat rewrite ZLib.div_mul_undo; try lia.
+          split.
+          apply Z.div_pos; try lia; apply Integers.Ptrofs.unsigned_range_2.
+          apply Z.div_le_upper_bound; lia. }
+
+        inversion NORMALISE_BOUND as [ NORMALISE_BOUND_LOW NORMALISE_BOUND_HIGH ];
+        clear NORMALISE_BOUND.
+
+        (** Start of proof proper *)
+        eexists. split.
+        eapply Smallstep.plus_one.
+        eapply HTL.step_module; eauto.
+        apply assumption_32bit.
+        econstructor. econstructor. econstructor. simplify.
+        econstructor. econstructor. econstructor. econstructor. simplify.
+
+        all: simplify.
+
+        (** Verilog array lookup *)
+        unfold Verilog.arr_assocmap_lookup. setoid_rewrite H5.
+        f_equal.
+
+        (** State Lookup *)
+        unfold Verilog.merge_regs.
+        simplify.
+        unfold_merge.
+        rewrite AssocMap.gso.
+        apply AssocMap.gss.
+        apply st_greater_than_res.
+
+        (** Match states *)
+        rewrite assumption_32bit.
+        econstructor; eauto.
+
+        (** Match assocmaps *)
+        unfold Verilog.merge_regs. simplify. unfold_merge.
+        apply regs_lessdef_add_match.
+
+        (** Equality proof *)
+        assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
+        rewrite ZERO in H7. clear ZERO.
+        setoid_rewrite Integers.Ptrofs.add_zero_l in H7.
+
+        specialize (H7 (Integers.Ptrofs.unsigned
+                          (Integers.Ptrofs.divu
+                             OFFSET
+                             (Integers.Ptrofs.repr 4)))).
+
+        exploit H7.
+        rewrite Z2Nat.id; eauto.
+        apply Z.div_pos; lia.
+
+        intros I.
+        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.
+        rewrite <- EXPR_OK.
+        rewrite NORMALISE in I.
+        rewrite H1 in I.
+        invert I. assumption.
+
+        (** PC match *)
+        apply regs_lessdef_add_greater.
+        apply greater_than_max_func.
+        assumption.
+
+        (** States well formed *)
+        unfold state_st_wf. inversion 1. simplify.
+        unfold Verilog.merge_regs.
+        unfold_merge. rewrite AssocMap.gso.
+        apply AssocMap.gss.
+        apply st_greater_than_res.
+
+        (** Match arrays *)
+        econstructor.
+        repeat split; simplify.
+        unfold HTL.empty_stack.
+        simplify.
+        unfold Verilog.merge_arrs.
+
+        rewrite AssocMap.gcombine.
+        2: { reflexivity. }
+        rewrite AssocMap.gss.
+        unfold Verilog.merge_arr.
+        setoid_rewrite H5.
+        reflexivity.
+
+        rewrite combine_length.
+        unfold arr_repeat. simplify.
+        rewrite list_repeat_len.
+        reflexivity.
+
+        unfold arr_repeat. simplify.
+        rewrite list_repeat_len.
+        congruence.
+
+        intros.
+        erewrite array_get_error_equal.
+        eauto. apply combine_none.
+        assumption.
+
+        (** RSBP preservation *)
+        unfold reg_stack_based_pointers. intros.
+        destruct (Pos.eq_dec r0 dst); try rewrite e. (* FIXME: Prepare this for automation *)
+
+        rewrite Registers.Regmap.gss.
+        unfold arr_stack_based_pointers in ASBP.
+        specialize (ASBP (Integers.Ptrofs.unsigned
+                            (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)))).
+        exploit ASBP; auto; intros I.
+
+        rewrite NORMALISE in I.
+        assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
+        rewrite ZERO in I. clear ZERO.
+        simplify.
+        rewrite Integers.Ptrofs.add_zero_l in I.
+        rewrite H1 in I.
+        assumption.
+        simplify.
+
+        rewrite Registers.Regmap.gso; auto.
+
+    - destruct c, chunk, addr, args; simplify; rt; simplify.
+      + (** Preamble *)
+        invert MARR. simplify.
+
+        unfold Op.eval_addressing in H0.
+        destruct (Archi.ptr64) eqn:ARCHI; simplify.
+
+        unfold reg_stack_based_pointers in RSBP.
+        pose proof (RSBP r0) as RSBPr0.
+
+        destruct (Registers.Regmap.get r0 rs) eqn:EQr0; simplify.
+
+        rewrite ARCHI in H1. simplify.
+        subst.
+
+        pose proof MASSOC as MASSOC'.
+        invert MASSOC'.
+        pose proof (H0 r0).
+        assert (HPler0 : Ple r0 (RTL.max_reg_function f))
+          by (eapply RTL.max_reg_function_use; eauto; simplify; eauto).
+        apply H6 in HPler0.
+        invert HPler0; try congruence.
+        rewrite EQr0 in H8.
+        invert H8.
+        clear H0. clear H6.
+
+        unfold check_address_parameter_unsigned in *;
+        unfold check_address_parameter_signed in *; simplify.
+
+        remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (valueToZ asr # r0))
+                                      (Integers.Ptrofs.of_int (Integers.Int.repr z))) as OFFSET.
+
+        (** Read bounds assumption *)
+        assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as WRITE_BOUND_HIGH by admit.
+
+        (** Modular preservation proof *)
+        assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE.
+        { rewrite HeqOFFSET.
+          apply PtrofsExtra.add_mod; simplify; try lia.
+          exists 1073741824. reflexivity. (* FIXME: This is sadness inducing. *)
+          rewrite Integers.Ptrofs.signed_repr; try assumption.
+          admit. (* FIXME: Register bounds. *)
+          apply PtrofsExtra.of_int_mod.
+          rewrite Integers.Int.signed_repr; simplify; try split; try assumption.
+        }
+
+        (** Start of proof proper *)
+        eexists. split.
+        eapply Smallstep.plus_one.
+        eapply HTL.step_module; eauto.
+        apply assumption_32bit.
+        econstructor. econstructor. econstructor.
+        eapply Verilog.stmnt_runp_Vnonblock_arr. simplify.
+        econstructor.
+        eapply Verilog.erun_Vbinop with (EQ := ?[EQ7]).
+        eapply Verilog.erun_Vbinop with (EQ := ?[EQ8]).
+        econstructor.
+        econstructor.
+        econstructor. econstructor. econstructor. econstructor.
+        econstructor. econstructor. econstructor. econstructor.
+
+        all: simplify.
+
+        (** State Lookup *)
+        unfold Verilog.merge_regs.
+        simplify.
+        unfold_merge.
+        apply AssocMap.gss.
+
+        (** Match states *)
+        rewrite assumption_32bit.
+        econstructor; eauto.
+
+        (** Match assocmaps *)
+        unfold Verilog.merge_regs. simplify. unfold_merge.
+        apply regs_lessdef_add_greater. apply greater_than_max_func.
+        assumption.
+
+        (** States well formed *)
+        unfold state_st_wf. inversion 1. simplify.
+        unfold Verilog.merge_regs.
+        unfold_merge.
+        apply AssocMap.gss.
+
+        (** Match stacks *)
+        admit.
+
+        (** Equality proof *)
+        assert (Z.to_nat
+                  (Integers.Ptrofs.unsigned
+                     (Integers.Ptrofs.divu
+                        OFFSET
+                        (Integers.Ptrofs.repr 4)))
+                =
+                valueToNat (vdiv (vplus asr # r0 (ZToValue 32 z) ?EQ8) (ZToValue 32 4) ?EQ7))
+          as EXPR_OK by admit.
+
+        assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
+        inversion MASSOC; revert HeqOFFSET; subst; clear MASSOC; intros HeqOFFSET.
+
+        econstructor.
+        repeat split; simplify.
+        unfold HTL.empty_stack.
+        simplify.
+        unfold Verilog.merge_arrs.
+
+        rewrite AssocMap.gcombine.
+        2: { reflexivity. }
+        unfold Verilog.arr_assocmap_set.
+        rewrite AssocMap.gss.
+        unfold Verilog.merge_arr.
+        rewrite AssocMap.gss.
+        setoid_rewrite H5.
+        reflexivity.
+
+        rewrite combine_length.
+        rewrite <- array_set_len.
+        unfold arr_repeat. simplify.
+        apply list_repeat_len.
+
+        rewrite <- array_set_len.
+        unfold arr_repeat. simplify.
+        rewrite list_repeat_len.
+        rewrite H4. reflexivity.
+
+        intros.
+        destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET).
+
+        erewrite Mem.load_store_same.
+        2: { rewrite ZERO.
+             rewrite Integers.Ptrofs.add_zero_l.
+             rewrite e.
+             rewrite Integers.Ptrofs.unsigned_repr.
+             exact H1.
+             apply Integers.Ptrofs.unsigned_range_2. }
+        constructor.
+        erewrite combine_lookup_second.
+        simpl.
+        assert (Ple src (RTL.max_reg_function f))
+          by (eapply RTL.max_reg_function_use; eauto; simpl; auto);
+        apply H0 in H14.
+        destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; invert H14; eauto.
+
+        rewrite <- array_set_len.
+        unfold arr_repeat. simplify.
+        rewrite list_repeat_len. auto.
+
+        assert (4 * ptr / 4 = Integers.Ptrofs.unsigned OFFSET / 4) by (f_equal; assumption).
+        rewrite Z.mul_comm in H14.
+        rewrite Z_div_mult in H14; try lia.
+        replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) in H14 by reflexivity.
+        rewrite <- PtrofsExtra.divu_unsigned in H14; unfold_constants; try lia.
+        rewrite H14. rewrite EXPR_OK.
+        rewrite array_get_error_set_bound.
+        reflexivity.
+        unfold arr_length, arr_repeat. simpl.
+        rewrite list_repeat_len. lia.
+
+        erewrite Mem.load_store_other with (m1 := m).
+        2: { exact H1. }
+        2: { right.
+             rewrite ZERO.
+             rewrite Integers.Ptrofs.add_zero_l.
+             rewrite Integers.Ptrofs.unsigned_repr.
+             simpl.
+             destruct (Z_le_gt_dec (4 * ptr + 4) (Integers.Ptrofs.unsigned OFFSET)); eauto.
+             right.
+             apply ZExtra.mod_0_bounds; try lia.
+             apply ZLib.Z_mod_mult'.
+             invert H13.
+             rewrite Z2Nat.id in H19; try lia.
+             apply Zmult_lt_compat_r with (p := 4) in H19; try lia.
+             rewrite ZLib.div_mul_undo in H19; try lia.
+             split; try lia.
+             apply Z.le_trans with (m := RTL.fn_stacksize f); simplify; lia.
+        }
+
+        rewrite <- EXPR_OK.
+        rewrite PtrofsExtra.divu_unsigned; auto; try (unfold_constants; lia).
+        destruct (ptr ==Z Integers.Ptrofs.unsigned OFFSET / 4).
+        apply Z.mul_cancel_r with (p := 4) in e; try lia.
+        rewrite ZLib.div_mul_undo in e; try lia.
+        rewrite combine_lookup_first.
+        eapply H7; eauto.
+
+        rewrite <- array_set_len.
+        unfold arr_repeat. simplify.
+        rewrite list_repeat_len. auto.
+        rewrite array_gso.
+        unfold array_get_error.
+        unfold arr_repeat.
+        simplify.
+        apply list_repeat_lookup.
+        lia.
+        unfold_constants.
+        intro.
+        apply Z2Nat.inj_iff in H14; try lia.
+        apply Z.div_pos; try lia.
+        apply Integers.Ptrofs.unsigned_range.
+
+        assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
+        unfold arr_stack_based_pointers.
+        intros.
+        destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET).
+
+        simplify.
+        erewrite Mem.load_store_same.
+        2: { rewrite ZERO.
+             rewrite Integers.Ptrofs.add_zero_l.
+             rewrite e.
+             rewrite Integers.Ptrofs.unsigned_repr.
+             exact H1.
+             apply Integers.Ptrofs.unsigned_range_2. }
+        simplify.
+        destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; try constructor.
+        destruct (Archi.ptr64); try discriminate.
+        pose proof (RSBP src). rewrite EQ_SRC in H0.
+        assumption.
+
+        simpl.
+        erewrite Mem.load_store_other with (m1 := m).
+        2: { exact H1. }
+        2: { right.
+             rewrite ZERO.
+             rewrite Integers.Ptrofs.add_zero_l.
+             rewrite Integers.Ptrofs.unsigned_repr.
+             simpl.
+             destruct (Z_le_gt_dec (4 * ptr + 4) (Integers.Ptrofs.unsigned OFFSET)); eauto.
+             right.
+             apply ZExtra.mod_0_bounds; try lia.
+             apply ZLib.Z_mod_mult'.
+             invert H0.
+             apply Zmult_lt_compat_r with (p := 4) in H14; try lia.
+             rewrite ZLib.div_mul_undo in H14; try lia.
+             split; try lia.
+             apply Z.le_trans with (m := RTL.fn_stacksize f); simplify; lia.
+        }
+        apply ASBP; assumption.
+
+      + (** Preamble *)
+        invert MARR. simplify.
+
+        unfold Op.eval_addressing in H0.
+        destruct (Archi.ptr64) eqn:ARCHI; simplify.
+
+        unfold reg_stack_based_pointers in RSBP.
+        pose proof (RSBP r0) as RSBPr0.
+        pose proof (RSBP r1) as RSBPr1.
+
+        destruct (Registers.Regmap.get r0 rs) eqn:EQr0;
+        destruct (Registers.Regmap.get r1 rs) eqn:EQr1; simplify.
+
+        rewrite ARCHI in H1. simplify.
+        subst.
+        clear RSBPr1.
+
+        pose proof MASSOC as MASSOC'.
+        invert MASSOC'.
+        pose proof (H0 r0).
+        pose proof (H0 r1).
+        assert (HPler0 : Ple r0 (RTL.max_reg_function f))
+          by (eapply RTL.max_reg_function_use; eauto; simplify; eauto).
+        assert (HPler1 : Ple r1 (RTL.max_reg_function f))
+          by (eapply RTL.max_reg_function_use; eauto; simpl; auto).
+        apply H6 in HPler0.
+        apply H8 in HPler1.
+        invert HPler0; invert HPler1; try congruence.
+        rewrite EQr0 in H10.
+        rewrite EQr1 in H12.
+        invert H10. invert H12.
+        clear H0. clear H6. clear H8.
+
+        unfold check_address_parameter_signed in *;
+        unfold check_address_parameter_unsigned in *; simplify.
+
+        remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (valueToZ asr # r0))
+                                      (Integers.Ptrofs.of_int
+                                         (Integers.Int.add (Integers.Int.mul (valueToInt asr # r1) (Integers.Int.repr z))
+                                                           (Integers.Int.repr z0)))) as OFFSET.
+
+        (** Read bounds assumption *)
+        assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH by admit.
+
+        (** Modular preservation proof *)
+        assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE.
+        { rewrite HeqOFFSET.
+          apply PtrofsExtra.add_mod; simplify; try lia.
+          exists 1073741824. reflexivity. (* FIXME: This is sadness inducing. *)
+          rewrite Integers.Ptrofs.signed_repr; try assumption.
+          admit. (* FIXME: Register bounds. *)
+          apply PtrofsExtra.of_int_mod.
+          apply IntExtra.add_mod; simplify; try lia.
+          exists 1073741824. reflexivity. (* FIXME: This is sadness inducing. *)
+          apply IntExtra.mul_mod; simplify; try lia.
+          exists 1073741824. reflexivity. (* FIXME: This is sadness inducing. *)
+          admit. (* FIXME: Register bounds. *)
+          rewrite Integers.Int.signed_repr; simplify; try split; try assumption.
+          rewrite Integers.Int.signed_repr; simplify; try split; try assumption.
+        }
+
+        (** Start of proof proper *)
+        eexists. split.
+        eapply Smallstep.plus_one.
+        eapply HTL.step_module; eauto.
+        apply assumption_32bit.
+        econstructor. econstructor. econstructor.
+        eapply Verilog.stmnt_runp_Vnonblock_arr. simplify.
+        econstructor.
+        eapply Verilog.erun_Vbinop with (EQ := ?[EQ9]).
+        eapply Verilog.erun_Vbinop with (EQ := ?[EQ10]).
+        eapply Verilog.erun_Vbinop with (EQ := ?[EQ11]).
+        econstructor. econstructor. econstructor. econstructor.
+        econstructor.
+        eapply Verilog.erun_Vbinop with (EQ := ?[EQ12]).
+        econstructor. econstructor. econstructor. econstructor.
+        econstructor. econstructor. econstructor. econstructor.
+        econstructor. econstructor. econstructor. econstructor.
+
+        all: simplify.
+
+        (** State Lookup *)
+        unfold Verilog.merge_regs.
+        simplify.
+        unfold_merge.
+        apply AssocMap.gss.
+
+        (** Match states *)
+        rewrite assumption_32bit.
+        econstructor; eauto.
+
+        (** Match assocmaps *)
+        unfold Verilog.merge_regs. simplify. unfold_merge.
+        apply regs_lessdef_add_greater. apply greater_than_max_func.
+        assumption.
+
+        (** States well formed *)
+        unfold state_st_wf. inversion 1. simplify.
+        unfold Verilog.merge_regs.
+        unfold_merge.
+        apply AssocMap.gss.
+
+        (** Match stacks *)
+        admit.
+
+        (** Equality proof *)
+        assert (Z.to_nat
+                  (Integers.Ptrofs.unsigned
+                     (Integers.Ptrofs.divu
+                        OFFSET
+                        (Integers.Ptrofs.repr 4)))
+                =
+                valueToNat (vdiv
+                              (vplus (vplus asr # r0 (ZToValue 32 z0) ?EQ11) (vmul asr # r1 (ZToValue 32 z) ?EQ12)
+                                     ?EQ10) (ZToValue 32 4) ?EQ9))
+          as EXPR_OK by admit.
+
+        assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
+        inversion MASSOC; revert HeqOFFSET; subst; clear MASSOC; intros HeqOFFSET.
+
+        econstructor.
+        repeat split; simplify.
+        unfold HTL.empty_stack.
+        simplify.
+        unfold Verilog.merge_arrs.
+
+        rewrite AssocMap.gcombine.
+        2: { reflexivity. }
+        unfold Verilog.arr_assocmap_set.
+        rewrite AssocMap.gss.
+        unfold Verilog.merge_arr.
+        rewrite AssocMap.gss.
+        setoid_rewrite H5.
+        reflexivity.
+
+        rewrite combine_length.
+        rewrite <- array_set_len.
+        unfold arr_repeat. simplify.
+        apply list_repeat_len.
+
+        rewrite <- array_set_len.
+        unfold arr_repeat. simplify.
+        rewrite list_repeat_len.
+        rewrite H4. reflexivity.
+
+        intros.
+        destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET).
+
+        erewrite Mem.load_store_same.
+        2: { rewrite ZERO.
+             rewrite Integers.Ptrofs.add_zero_l.
+             rewrite e.
+             rewrite Integers.Ptrofs.unsigned_repr.
+             exact H1.
+             apply Integers.Ptrofs.unsigned_range_2. }
+        constructor.
+        erewrite combine_lookup_second.
+        simpl.
+        assert (Ple src (RTL.max_reg_function f))
+          by (eapply RTL.max_reg_function_use; eauto; simpl; auto);
+        apply H0 in H21.
+        destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; invert H21; eauto.
+
+        rewrite <- array_set_len.
+        unfold arr_repeat. simplify.
+        rewrite list_repeat_len. auto.
+
+        assert (4 * ptr / 4 = Integers.Ptrofs.unsigned OFFSET / 4) by (f_equal; assumption).
+        rewrite Z.mul_comm in H21.
+        rewrite Z_div_mult in H21; try lia.
+        replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) in H21 by reflexivity.
+        rewrite <- PtrofsExtra.divu_unsigned in H21; unfold_constants; try lia.
+        rewrite H21. rewrite EXPR_OK.
+        rewrite array_get_error_set_bound.
+        reflexivity.
+        unfold arr_length, arr_repeat. simpl.
+        rewrite list_repeat_len. lia.
+
+        erewrite Mem.load_store_other with (m1 := m).
+        2: { exact H1. }
+        2: { right.
+             rewrite ZERO.
+             rewrite Integers.Ptrofs.add_zero_l.
+             rewrite Integers.Ptrofs.unsigned_repr.
+             simpl.
+             destruct (Z_le_gt_dec (4 * ptr + 4) (Integers.Ptrofs.unsigned OFFSET)); eauto.
+             right.
+             apply ZExtra.mod_0_bounds; try lia.
+             apply ZLib.Z_mod_mult'.
+             invert H20.
+             rewrite Z2Nat.id in H22; try lia.
+             apply Zmult_lt_compat_r with (p := 4) in H22; try lia.
+             rewrite ZLib.div_mul_undo in H22; try lia.
+             split; try lia.
+             apply Z.le_trans with (m := RTL.fn_stacksize f); simplify; lia.
+        }
+
+        rewrite <- EXPR_OK.
+        rewrite PtrofsExtra.divu_unsigned; auto; try (unfold_constants; lia).
+        destruct (ptr ==Z Integers.Ptrofs.unsigned OFFSET / 4).
+        apply Z.mul_cancel_r with (p := 4) in e; try lia.
+        rewrite ZLib.div_mul_undo in e; try lia.
+        rewrite combine_lookup_first.
+        eapply H7; eauto.
+
+        rewrite <- array_set_len.
+        unfold arr_repeat. simplify.
+        rewrite list_repeat_len. auto.
+        rewrite array_gso.
+        unfold array_get_error.
+        unfold arr_repeat.
+        simplify.
+        apply list_repeat_lookup.
+        lia.
+        unfold_constants.
+        intro.
+        apply Z2Nat.inj_iff in H21; try lia.
+        apply Z.div_pos; try lia.
+        apply Integers.Ptrofs.unsigned_range.
+
+        assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
+        unfold arr_stack_based_pointers.
+        intros.
+        destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET).
+
+        simplify.
+        erewrite Mem.load_store_same.
+        2: { rewrite ZERO.
+             rewrite Integers.Ptrofs.add_zero_l.
+             rewrite e.
+             rewrite Integers.Ptrofs.unsigned_repr.
+             exact H1.
+             apply Integers.Ptrofs.unsigned_range_2. }
+        simplify.
+        destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; try constructor.
+        destruct (Archi.ptr64); try discriminate.
+        pose proof (RSBP src). rewrite EQ_SRC in H0.
+        assumption.
+
+        simpl.
+        erewrite Mem.load_store_other with (m1 := m).
+        2: { exact H1. }
+        2: { right.
+             rewrite ZERO.
+             rewrite Integers.Ptrofs.add_zero_l.
+             rewrite Integers.Ptrofs.unsigned_repr.
+             simpl.
+             destruct (Z_le_gt_dec (4 * ptr + 4) (Integers.Ptrofs.unsigned OFFSET)); eauto.
+             right.
+             apply ZExtra.mod_0_bounds; try lia.
+             apply ZLib.Z_mod_mult'.
+             invert H0.
+             apply Zmult_lt_compat_r with (p := 4) in H21; try lia.
+             rewrite ZLib.div_mul_undo in H21; try lia.
+             split; try lia.
+             apply Z.le_trans with (m := RTL.fn_stacksize f); simplify; lia.
+        }
+        apply ASBP; assumption.
+
+      + invert MARR. simplify.
+
+        unfold Op.eval_addressing in H0.
+        destruct (Archi.ptr64) eqn:ARCHI; simplify.
+        rewrite ARCHI in H0. simplify.
+
+        unfold check_address_parameter_unsigned in *;
+        unfold check_address_parameter_signed in *; simplify.
+
+        assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
+        rewrite ZERO in H1. clear ZERO.
+        rewrite Integers.Ptrofs.add_zero_l in H1.
+
+        remember i0 as OFFSET.
+
+        (** Read bounds assumption *)
+        assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH by admit.
+
+        (** Modular preservation proof *)
+        rename H0 into MOD_PRESERVE.
+
+        (** Start of proof proper *)
+        eexists. split.
+        eapply Smallstep.plus_one.
+        eapply HTL.step_module; eauto.
+        apply assumption_32bit.
+        econstructor. econstructor. econstructor.
+        eapply Verilog.stmnt_runp_Vnonblock_arr. simplify.
+        econstructor. econstructor. econstructor. econstructor.
+
+        all: simplify.
+
+        (** State Lookup *)
+        unfold Verilog.merge_regs.
+        simplify.
+        unfold_merge.
+        apply AssocMap.gss.
+
+        (** Match states *)
+        rewrite assumption_32bit.
+        econstructor; eauto.
+
+        (** Match assocmaps *)
+        unfold Verilog.merge_regs. simplify. unfold_merge.
+        apply regs_lessdef_add_greater. apply greater_than_max_func.
+        assumption.
+
+        (** States well formed *)
+        unfold state_st_wf. inversion 1. simplify.
+        unfold Verilog.merge_regs.
+        unfold_merge.
+        apply AssocMap.gss.
+
+        (** Match stacks *)
+        admit.
+
+        (** Equality proof *)
+        assert (Z.to_nat
+                  (Integers.Ptrofs.unsigned
+                     (Integers.Ptrofs.divu
+                        OFFSET
+                        (Integers.Ptrofs.repr 4)))
+                =
+                valueToNat (ZToValue 32 (Integers.Ptrofs.unsigned OFFSET / 4)))
+          as EXPR_OK by admit.
+
+        assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
+        inversion MASSOC; revert HeqOFFSET; subst; clear MASSOC; intros HeqOFFSET.
+
+        econstructor.
+        repeat split; simplify.
+        unfold HTL.empty_stack.
+        simplify.
+        unfold Verilog.merge_arrs.
+
+        rewrite AssocMap.gcombine.
+        2: { reflexivity. }
+        unfold Verilog.arr_assocmap_set.
+        rewrite AssocMap.gss.
+        unfold Verilog.merge_arr.
+        rewrite AssocMap.gss.
+        setoid_rewrite H5.
+        reflexivity.
+
+        rewrite combine_length.
+        rewrite <- array_set_len.
+        unfold arr_repeat. simplify.
+        apply list_repeat_len.
+
+        rewrite <- array_set_len.
+        unfold arr_repeat. simplify.
+        rewrite list_repeat_len.
+        rewrite H4. reflexivity.
+
+        intros.
+        destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET).
+
+        erewrite Mem.load_store_same.
+        2: { rewrite ZERO.
+             rewrite Integers.Ptrofs.add_zero_l.
+             rewrite e.
+             rewrite Integers.Ptrofs.unsigned_repr.
+             exact H1.
+             apply Integers.Ptrofs.unsigned_range_2. }
+        constructor.
+        erewrite combine_lookup_second.
+        simpl.
+        assert (Ple src (RTL.max_reg_function f))
+          by (eapply RTL.max_reg_function_use; eauto; simpl; auto);
+        apply H0 in H10.
+        destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; invert H10; eauto.
+
+        rewrite <- array_set_len.
+        unfold arr_repeat. simplify.
+        rewrite list_repeat_len. auto.
+
+        assert (4 * ptr / 4 = Integers.Ptrofs.unsigned OFFSET / 4) by (f_equal; assumption).
+        rewrite Z.mul_comm in H10.
+        rewrite Z_div_mult in H10; try lia.
+        replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) in H10 by reflexivity.
+        rewrite <- PtrofsExtra.divu_unsigned in H10; unfold_constants; try lia.
+        rewrite H10. rewrite EXPR_OK.
+        rewrite array_get_error_set_bound.
+        reflexivity.
+        unfold arr_length, arr_repeat. simpl.
+        rewrite list_repeat_len. lia.
+
+        erewrite Mem.load_store_other with (m1 := m).
+        2: { exact H1. }
+        2: { right.
+             rewrite ZERO.
+             rewrite Integers.Ptrofs.add_zero_l.
+             rewrite Integers.Ptrofs.unsigned_repr.
+             simpl.
+             destruct (Z_le_gt_dec (4 * ptr + 4) (Integers.Ptrofs.unsigned OFFSET)); eauto.
+             right.
+             apply ZExtra.mod_0_bounds; try lia.
+             apply ZLib.Z_mod_mult'.
+             invert H8.
+             rewrite Z2Nat.id in H12; try lia.
+             apply Zmult_lt_compat_r with (p := 4) in H12; try lia.
+             rewrite ZLib.div_mul_undo in H12; try lia.
+             split; try lia.
+             apply Z.le_trans with (m := RTL.fn_stacksize f); simplify; lia.
+        }
+
+        rewrite <- EXPR_OK.
+        rewrite PtrofsExtra.divu_unsigned; auto; try (unfold_constants; lia).
+        destruct (ptr ==Z Integers.Ptrofs.unsigned OFFSET / 4).
+        apply Z.mul_cancel_r with (p := 4) in e; try lia.
+        rewrite ZLib.div_mul_undo in e; try lia.
+        rewrite combine_lookup_first.
+        eapply H7; eauto.
+
+        rewrite <- array_set_len.
+        unfold arr_repeat. simplify.
+        rewrite list_repeat_len. auto.
+        rewrite array_gso.
+        unfold array_get_error.
+        unfold arr_repeat.
+        simplify.
+        apply list_repeat_lookup.
+        lia.
+        unfold_constants.
+        intro.
+        apply Z2Nat.inj_iff in H10; try lia.
+        apply Z.div_pos; try lia.
+        apply Integers.Ptrofs.unsigned_range.
+
+        assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
+        unfold arr_stack_based_pointers.
+        intros.
+        destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET).
+
+        simplify.
+        erewrite Mem.load_store_same.
+        2: { rewrite ZERO.
+             rewrite Integers.Ptrofs.add_zero_l.
+             rewrite e.
+             rewrite Integers.Ptrofs.unsigned_repr.
+             exact H1.
+             apply Integers.Ptrofs.unsigned_range_2. }
+        simplify.
+        destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; try constructor.
+        destruct (Archi.ptr64); try discriminate.
+        pose proof (RSBP src). rewrite EQ_SRC in H0.
+        assumption.
+
+        simpl.
+        erewrite Mem.load_store_other with (m1 := m).
+        2: { exact H1. }
+        2: { right.
+             rewrite ZERO.
+             rewrite Integers.Ptrofs.add_zero_l.
+             rewrite Integers.Ptrofs.unsigned_repr.
+             simpl.
+             destruct (Z_le_gt_dec (4 * ptr + 4) (Integers.Ptrofs.unsigned OFFSET)); eauto.
+             right.
+             apply ZExtra.mod_0_bounds; try lia.
+             apply ZLib.Z_mod_mult'.
+             invert H0.
+             apply Zmult_lt_compat_r with (p := 4) in H10; try lia.
+             rewrite ZLib.div_mul_undo in H10; try lia.
+             split; try lia.
+             apply Z.le_trans with (m := RTL.fn_stacksize f); simplify; lia.
+        }
+        apply ASBP; assumption.
 
     - eexists. split. apply Smallstep.plus_one.
       eapply HTL.step_module; eauto.
+      apply assumption_32bit.
       eapply Verilog.stmnt_runp_Vnonblock_reg with
           (rhsval := if b then posToValue 32 ifso else posToValue 32 ifnot).
 
@@ -411,41 +1880,101 @@ Section CORRECTNESS.
       constructor.
       apply boolToValue_ValueToBool.
       constructor.
+      unfold Verilog.merge_regs.
       unfold_merge.
       apply AssocMap.gss.
 
       destruct b.
       rewrite assumption_32bit.
-      apply match_state.
+      simplify.
+      apply match_state with (sp' := sp'); eauto.
+      unfold Verilog.merge_regs.
       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.
+      unfold state_st_wf. intros.
+      invert H3.
+      unfold Verilog.merge_regs. unfold_merge.
       apply AssocMap.gss.
-      assumption.
 
+      (** Match arrays *)
+      invert MARR. simplify.
+      econstructor.
+      repeat split; simplify.
+      unfold HTL.empty_stack.
+      simplify.
+      unfold Verilog.merge_arrs.
+
+      rewrite AssocMap.gcombine.
+      2: { reflexivity. }
+      rewrite AssocMap.gss.
+      unfold Verilog.merge_arr.
+      setoid_rewrite H4.
+      reflexivity.
+
+      rewrite combine_length.
+      unfold arr_repeat. simplify.
+      rewrite list_repeat_len.
+      reflexivity.
+
+      unfold arr_repeat. simplify.
+      rewrite list_repeat_len.
+      congruence.
+
+      intros.
+      erewrite array_get_error_equal.
+      eauto. apply combine_none.
       assumption.
 
       rewrite assumption_32bit.
-      apply match_state.
-      unfold_merge.
-      apply regs_lessdef_add_greater. apply greater_than_max_func. assumption.
+      apply match_state with (sp' := sp'); eauto.
+      unfold Verilog.merge_regs. unfold_merge.
+      apply regs_lessdef_add_greater. apply greater_than_max_func.
       assumption.
 
-      unfold state_st_wf. intros. inversion H1.
-      subst. unfold_merge.
+      unfold state_st_wf. intros.
+      invert H1.
+      unfold Verilog.merge_regs. unfold_merge.
       apply AssocMap.gss.
-      assumption.
 
+      (** Match arrays *)
+      invert MARR. simplify.
+      econstructor.
+      repeat split; simplify.
+      unfold HTL.empty_stack.
+      simplify.
+      unfold Verilog.merge_arrs.
+
+      rewrite AssocMap.gcombine.
+      2: { reflexivity. }
+      rewrite AssocMap.gss.
+      unfold Verilog.merge_arr.
+      setoid_rewrite H2.
+      reflexivity.
+
+      rewrite combine_length.
+      unfold arr_repeat. simplify.
+      rewrite list_repeat_len.
+      reflexivity.
+
+      unfold arr_repeat. simplify.
+      rewrite list_repeat_len.
+      congruence.
+
+      intros.
+      erewrite array_get_error_equal.
+      eauto. apply combine_none.
       assumption.
 
+    - admit.
+
     - (* Return *)
       econstructor. split.
       eapply Smallstep.plus_two.
       
       eapply HTL.step_module; eauto.
+      apply assumption_32bit.
       constructor.
       econstructor; simpl; trivial.
       econstructor; simpl; trivial.
@@ -453,9 +1982,9 @@ Section CORRECTNESS.
       econstructor; simpl; trivial.
       constructor.
 
-      constructor.
-      constructor.
+      constructor. constructor.
 
+      unfold Verilog.merge_regs.
       unfold_merge. simpl.
       rewrite AssocMap.gso.
       rewrite AssocMap.gso.
@@ -463,6 +1992,7 @@ Section CORRECTNESS.
       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.
@@ -470,12 +2000,14 @@ Section CORRECTNESS.
       apply AssocMap.gss.
       rewrite Events.E0_left. reflexivity.
       constructor.
-      assumption.
+
+      admit.
       constructor.
 
     - econstructor. split.
       eapply Smallstep.plus_two.
       eapply HTL.step_module; eauto.
+      apply assumption_32bit.
       constructor.
       econstructor; simpl; trivial.
       econstructor; simpl; trivial.
@@ -485,6 +2017,7 @@ Section CORRECTNESS.
       constructor.
       econstructor; simpl; trivial.
       apply Verilog.erun_Vvar. trivial.
+      unfold Verilog.merge_regs.
       unfold_merge. simpl.
       rewrite AssocMap.gso.
       rewrite AssocMap.gso.
@@ -492,6 +2025,7 @@ Section CORRECTNESS.
       apply st_greater_than_res. apply st_greater_than_res. trivial.
 
       apply HTL.step_finish.
+      unfold Verilog.merge_regs.
       unfold_merge.
       rewrite AssocMap.gso.
       apply AssocMap.gss.
@@ -499,27 +2033,71 @@ Section CORRECTNESS.
       apply AssocMap.gss.
       rewrite Events.E0_left. trivial.
 
-      constructor. assumption. simpl. inversion MASSOC. subst.
+      constructor.
+      admit.
+
+      simpl. inversion MASSOC. subst.
       unfold find_assocmap, AssocMapExt.get_default. rewrite AssocMap.gso.
       apply H1. eapply RTL.max_reg_function_use. eauto. simpl; tauto.
       apply st_greater_than_res.
 
     - inversion MSTATE; subst. inversion TF; subst.
       econstructor. split. apply Smallstep.plus_one.
-      eapply HTL.step_call.
+      eapply HTL.step_call. simplify.
+
+      apply match_state with (sp' := stk); eauto.
 
-      constructor. apply regs_lessdef_add_greater.
+      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.
+      apply init_reg_assoc_empty.
+      unfold state_st_wf.
+      intros. inv H3. apply AssocMap.gss. constructor.
+
+      econstructor. simplify.
+      repeat split. unfold HTL.empty_stack.
+      simplify. apply AssocMap.gss.
+      unfold arr_repeat. simplify.
+      apply list_repeat_len.
+      intros.
+      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.
 
-      admit.
+      unfold reg_stack_based_pointers. intros.
+      unfold RTL.init_regs; simplify.
+      destruct (RTL.fn_params f);
+      rewrite Registers.Regmap.gi; constructor.
+
+      unfold arr_stack_based_pointers. intros.
+      simplify.
+      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.
 
-    - inversion MSTATE; subst. inversion MS; subst. econstructor.
+    - invert MSTATE. invert MS.
+      econstructor.
       split. apply Smallstep.plus_one.
       constructor.
 
-      constructor; auto. constructor; auto. apply regs_lessdef_add_match; auto.
+      constructor; auto.
+      econstructor; auto.
+      apply regs_lessdef_add_match; auto.
       apply regs_lessdef_add_greater. apply greater_than_max_func. auto.
 
       unfold state_st_wf. intros. inv H. rewrite AssocMap.gso.
@@ -530,8 +2108,6 @@ Section CORRECTNESS.
       Unshelve.
       exact (AssocMap.empty value).
       exact (AssocMap.empty value).
-      admit.
-      admit.
       (* exact (ZToValue 32 0). *)
       (* exact (AssocMap.empty value). *)
       (* exact (AssocMap.empty value). *)
@@ -540,6 +2116,30 @@ Section CORRECTNESS.
   Admitted.
   Hint Resolve transl_step_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 :
     forall s1 : Smallstep.state (RTL.semantics prog),
@@ -548,20 +2148,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 :
@@ -574,16 +2189,16 @@ Section CORRECTNESS.
   Proof.
     intros. inv H0. inv H. inv H4. inv MS. constructor. trivial.
   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.
+  eapply Smallstep.forward_simulation_plus.
   apply senv_preserved.
   eexact transl_initial_states.
   eexact transl_final_states.
-  exact transl_step_correct.*)
-Admitted.
+  exact transl_step_correct.
+Qed.
 
 End CORRECTNESS.
diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v
index 887a696..a78256b 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;
+    simplify;
+    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..db96949 100644
--- a/src/translation/Veriloggenproof.v
+++ b/src/translation/Veriloggenproof.v
@@ -16,16 +16,66 @@
  * 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.
 
   Theorem transf_program_correct:
     forward_simulation (HTL.semantics prog) (Verilog.semantics tprog).
-  Admitted.
+
 
 End CORRECTNESS.
+