Implemented algorithm for new byte-addressed stack.

11 files changed, 2730 insertions, 2682 deletions

diff --git a/src/common/Coquplib.v b/src/common/Coquplib.v
index 2295ff6..469eddc 100644
--- a/src/common/Coquplib.v
+++ b/src/common/Coquplib.v
@@ -235,3 +235,5 @@ Definition debug_show {A B : Type} `{Show A} (a : A) (b : B) : B :=
 
 Definition debug_show_msg {A B : Type} `{Show A} (s : string) (a : A) (b : B) : B :=
   let unused := debug_print (s ++ show a) in b.
+
+Notation "f $ x" := (f x) (at level 60, right associativity, only parsing).
diff --git a/src/common/IntegerExtra.v b/src/common/IntegerExtra.v
index fe7d94f..8e32c2c 100644
--- a/src/common/IntegerExtra.v
+++ b/src/common/IntegerExtra.v
@@ -298,44 +298,48 @@ Module IntExtra.
            (or (shl (repr (Byte.unsigned c)) (repr Byte.zwordsize))
                (repr (Byte.unsigned d)))).
 
-  Definition byte1 (n: int) : byte := Byte.repr (unsigned n).
+  Definition byte0 (n: int) : byte := Byte.repr $ unsigned n.
+  Definition ibyte0 (n: int) : int := Int.repr $ Byte.unsigned $ byte0 n.
 
-  Definition byte2 (n: int) : byte := Byte.repr (unsigned (shru n (repr Byte.zwordsize))).
+  Definition byte1 (n: int) : byte := Byte.repr $ unsigned $ shru n $ repr Byte.zwordsize.
+  Definition ibyte1 (n: int) : int := Int.repr $ Byte.unsigned $ byte1 n.
 
-  Definition byte3 (n: int) : byte := Byte.repr (unsigned (shru n (repr (2 * Byte.zwordsize)))).
+  Definition byte2 (n: int) : byte := Byte.repr $ unsigned $ shru n $ repr (2 * Byte.zwordsize).
+  Definition ibyte2 (n: int) : int := Int.repr $ Byte.unsigned $ byte2 n.
 
-  Definition byte4 (n: int) : byte := Byte.repr (unsigned (shru n (repr (3 * Byte.zwordsize)))).
+  Definition byte3 (n: int) : byte := Byte.repr $ unsigned $ shru n $ repr (3 * Byte.zwordsize).
+  Definition ibyte3 (n: int) : int := Int.repr $ Byte.unsigned $ byte3 n.
 
-  Lemma bits_byte1:
-    forall n i, 0 <= i < Byte.zwordsize -> Byte.testbit (byte1 n) i = testbit n i.
+  Lemma bits_byte0:
+    forall n i, 0 <= i < Byte.zwordsize -> Byte.testbit (byte0 n) i = testbit n i.
   Proof.
-    intros. unfold byte1. rewrite Byte.testbit_repr; auto.
+    intros. unfold byte0. rewrite Byte.testbit_repr; auto.
   Qed.
 
-  Lemma bits_byte2:
-    forall n i, 0 <= i < Byte.zwordsize -> Byte.testbit (byte2 n) i = testbit n (i + Byte.zwordsize).
+  Lemma bits_byte1:
+    forall n i, 0 <= i < Byte.zwordsize -> Byte.testbit (byte1 n) i = testbit n (i + Byte.zwordsize).
   Proof.
-    intros. unfold byte2. rewrite Byte.testbit_repr; auto.
+    intros. unfold byte1. rewrite Byte.testbit_repr; auto.
     assert (zwordsize = 4 * Byte.zwordsize) by reflexivity.
     fold (testbit (shru n (repr Byte.zwordsize)) i). rewrite bits_shru.
     change (unsigned (repr Byte.zwordsize)) with Byte.zwordsize.
     apply zlt_true. omega. omega.
   Qed.
 
-  Lemma bits_byte3:
-    forall n i, 0 <= i < Byte.zwordsize -> Byte.testbit (byte3 n) i = testbit n (i + (2 * Byte.zwordsize)).
+  Lemma bits_byte2:
+    forall n i, 0 <= i < Byte.zwordsize -> Byte.testbit (byte2 n) i = testbit n (i + (2 * Byte.zwordsize)).
   Proof.
-    intros. unfold byte3. rewrite Byte.testbit_repr; auto.
+    intros. unfold byte2. rewrite Byte.testbit_repr; auto.
     assert (zwordsize = 4 * Byte.zwordsize) by reflexivity.
     fold (testbit (shru n (repr (2 * Byte.zwordsize))) i). rewrite bits_shru.
     change (unsigned (repr (2 * Byte.zwordsize))) with (2 * Byte.zwordsize).
     apply zlt_true. omega. omega.
   Qed.
 
-  Lemma bits_byte4:
-    forall n i, 0 <= i < Byte.zwordsize -> Byte.testbit (byte4 n) i = testbit n (i + (3 * Byte.zwordsize)).
+  Lemma bits_byte3:
+    forall n i, 0 <= i < Byte.zwordsize -> Byte.testbit (byte3 n) i = testbit n (i + (3 * Byte.zwordsize)).
   Proof.
-    intros. unfold byte4. rewrite Byte.testbit_repr; auto.
+    intros. unfold byte3. rewrite Byte.testbit_repr; auto.
     assert (zwordsize = 4 * Byte.zwordsize) by reflexivity.
     fold (testbit (shru n (repr (3 * Byte.zwordsize))) i). rewrite bits_shru.
     change (unsigned (repr (3 * Byte.zwordsize))) with (3 * Byte.zwordsize).
diff --git a/src/common/Monad.v b/src/common/Monad.v
index 8517186..628963e 100644
--- a/src/common/Monad.v
+++ b/src/common/Monad.v
@@ -20,6 +20,10 @@ Module MonadExtra(M : Monad).
 
   Module MonadNotation.
 
+    Notation "A ; B" :=
+      (bind A (fun _ => B))
+        (at level 200, B at level 200).
+
     Notation "'do' X <- A ; B" :=
       (bind A (fun X => B))
         (at level 200, X ident, A at level 100, B at level 200).
diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v
index df21dc4..5d10cd7 100644
--- a/src/extraction/Extraction.v
+++ b/src/extraction/Extraction.v
@@ -16,7 +16,7 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-From coqup Require Verilog Value Compiler.
+From coqup Require Verilog ValueInt Compiler.
 
 From Coq Require DecidableClass.
 
@@ -167,7 +167,7 @@ Set Extraction AccessOpaque.
 
 Cd "src/extraction".
 Separate Extraction
-         Verilog.module Value.uvalueToZ coqup.Compiler.transf_hls
+         Verilog.module ValueInt.uvalueToZ coqup.Compiler.transf_hls
 
    Compiler.transf_c_program Compiler.transf_cminor_program
    Cexec.do_initial_state Cexec.do_step Cexec.at_final_state
diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v
index e02d759..995977c 100644
--- a/src/translation/HTLgen.v
+++ b/src/translation/HTLgen.v
@@ -292,26 +292,16 @@ Definition check_address_parameter_unsigned (p : Z) : bool :=
 Definition translate_eff_addressing (a: Op.addressing) (args: list reg) : mon expr :=
   match a, args with (* TODO: We should be more methodical here; what are the possibilities?*)
   | Op.Aindexed off, r1::nil =>
-    if (check_address_parameter_signed off)
-    then ret (boplitz Vadd r1 off)
-    else error (Errors.msg "Veriloggen: translate_eff_addressing (Aindexed): address misaligned")
+    ret (boplitz Vadd r1 off)
   | Op.Ascaled scale offset, r1::nil =>
-    if (check_address_parameter_signed scale) && (check_address_parameter_signed offset)
-    then ret (Vbinop Vadd (boplitz Vmul r1 scale) (Vlit (ZToValue offset)))
-    else error (Errors.msg "Veriloggen: translate_eff_addressing (Ascaled): address misaligned")
+    ret (Vbinop Vadd (boplitz Vmul r1 scale) (Vlit (ZToValue offset)))
   | Op.Aindexed2 offset, r1::r2::nil =>
-    if (check_address_parameter_signed offset)
-    then ret (Vbinop Vadd (Vvar r1) (boplitz Vadd r2 offset))
-    else error (Errors.msg "Veriloggen: translate_eff_addressing (Aindexed2): address misaligned")
+    ret (Vbinop Vadd (Vvar r1) (boplitz Vadd r2 offset))
   | Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *)
-    if (check_address_parameter_signed scale) && (check_address_parameter_signed offset)
-    then ret (Vbinop Vadd (boplitz Vadd r1 offset) (boplitz Vmul r2 scale))
-    else error (Errors.msg "Veriloggen: translate_eff_addressing (Aindexed2scaled): address misaligned")
+    ret (Vbinop Vadd (boplitz Vadd r1 offset) (boplitz Vmul r2 scale))
   | 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 (Vlit (ZToValue a))
-    else error (Errors.msg "Veriloggen: translate_eff_addressing (Ainstack): address misaligned")
+    ret (Vlit (ZToValue a))
   | _, _ => error (Errors.msg "Veriloggen: translate_eff_addressing unsuported addressing")
   end.
 
@@ -390,27 +380,27 @@ Definition add_branch_instr (e: expr) (n n1 n2: node) : mon unit :=
     | _, _ => Error (Errors.msg "Htlgen: add_branch_instr")
     end.
 
-Definition translate_arr_access (mem : AST.memory_chunk) (addr : Op.addressing)
-           (args : list reg) (stack : reg) : mon expr :=
-  match mem, addr, args with (* TODO: We should be more methodical here; what are the possibilities?*)
-  | Mint32, Op.Aindexed off, r1::nil =>
-    if (check_address_parameter_signed off)
-    then ret (Vvari stack (Vbinop Vdivu (boplitz Vadd r1 off) (Vlit (ZToValue 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 Vdivu
-                            (Vbinop Vadd (boplitz Vadd r1 offset) (boplitz Vmul r2 scale))
-                            (Vlit (ZToValue 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 (a / 4))))
-    else error (Errors.msg "HTLgen: eff_addressing misaligned stack offset")
-  | _, _, _ => error (Errors.msg "HTLgen: translate_arr_access unsuported addressing")
-  end.
+(* Definition translate_arr_access (mem : AST.memory_chunk) (addr : Op.addressing) *)
+(*            (args : list reg) (stack : reg) : mon expr := *)
+(*   match mem, addr, args with (* TODO: We should be more methodical here; what are the possibilities?*) *)
+(*   | Mint32, Op.Aindexed off, r1::nil => *)
+(*     if (check_address_parameter_signed off) *)
+(*     then ret (Vvari stack (Vbinop Vdivu (boplitz Vadd r1 off) (Vlit (ZToValue 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 Vdivu *)
+(*                             (Vbinop Vadd (boplitz Vadd r1 offset) (boplitz Vmul r2 scale)) *)
+(*                             (Vlit (ZToValue 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 (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) :=
   match ns with
@@ -424,6 +414,22 @@ Definition tbl_to_case_expr (st : reg) (ns : list node) : list (expr * stmnt) :=
                   end)
            (enumerate 0 ns).
 
+Definition add_single_cycle_load (n n' : node) (stack : reg) (addr : expr) (dst : reg) : mon unit :=
+  let l0   := Vnonblock (Vvarb0 dst) (Vvari stack addr) in
+  let l1   := Vnonblock (Vvarb1 dst) (Vvari stack $ Vbinop Vadd addr (Vlit $ ZToValue 1)) in
+  let l2   := Vnonblock (Vvarb2 dst) (Vvari stack $ Vbinop Vadd addr (Vlit $ ZToValue 2)) in
+  let l3   := Vnonblock (Vvarb3 dst) (Vvari stack $ Vbinop Vadd addr (Vlit $ ZToValue 2)) in
+  let instr := Vseq l0 $ Vseq l1 $ Vseq l2 $ l3
+  in add_instr n n' instr.
+
+Definition add_single_cycle_store (n n' : node) (stack : reg) (addr : expr) (src : reg) : mon unit :=
+  let l0   := Vnonblock (Vvari stack addr) (Vvarb0 src) in
+  let l1   := Vnonblock (Vvari stack $ Vbinop Vadd addr (Vlit $ ZToValue 1)) (Vvarb1 src) in
+  let l2   := Vnonblock (Vvari stack $ Vbinop Vadd addr (Vlit $ ZToValue 2)) (Vvarb2 src) in
+  let l3   := Vnonblock (Vvari stack $ Vbinop Vadd addr (Vlit $ ZToValue 2)) (Vvarb3 src) in
+  let instr := Vseq l0 $ Vseq l1 $ Vseq l2 $ l3
+  in add_instr n n' instr.
+
 Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon unit :=
   match ni with
     (n, i) =>
@@ -434,12 +440,12 @@ Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon uni
       do _ <- declare_reg None dst 32;
       add_instr n n' (nonblock dst instr)
     | Iload mem addr args dst n' =>
-      do src <- translate_arr_access mem addr args stack;
+      do addr' <- translate_eff_addressing addr args;
       do _ <- declare_reg None dst 32;
-      add_instr n n' (nonblock dst src)
+      add_single_cycle_load n n' stack addr' dst
     | Istore mem addr args src n' =>
-      do dst <- translate_arr_access mem addr args stack;
-      add_instr n n' (Vnonblock dst (Vvar src)) (* TODO: Could juse use add_instr? reg exists. *)
+      do addr' <- translate_eff_addressing addr args;
+      add_single_cycle_store n n' stack addr' src
     | Icall _ _ _ _ _ => error (Errors.msg "Calls are not implemented.")
     | Itailcall _ _ _ => error (Errors.msg "Tailcalls are not implemented.")
     | Ibuiltin _ _ _ _ => error (Errors.msg "Builtin functions not implemented.")
@@ -543,7 +549,7 @@ 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, stack_len) <- create_arr None 32 (Z.to_nat (f.(fn_stacksize) / 4));
+    do (stack, stack_len) <- create_arr None 8 (Z.to_nat f.(fn_stacksize));
     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;
diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v
index 305c14f..e404c82 100644
--- a/src/translation/HTLgenproof.v
+++ b/src/translation/HTLgenproof.v
@@ -31,2158 +31,2159 @@ Hint Resolve AssocMap.gso : htlproof.
 
 Hint Unfold find_assocmap AssocMapExt.get_default : htlproof.
 
-Inductive match_assocmaps : RTL.function -> RTL.regset -> assocmap -> Prop :=
-  match_assocmap : forall f rs am,
-    (forall r, Ple r (RTL.max_reg_function f) ->
-               val_value_lessdef (Registers.Regmap.get r rs) am#r) ->
-    match_assocmaps f rs am.
-Hint Constructors match_assocmaps : htlproof.
-
-Definition state_st_wf (m : HTL.module) (s : HTL.state) :=
-  forall st asa asr res,
-  s = HTL.State res m st asa asr ->
-  asa!(m.(HTL.mod_st)) = Some (posToValue st).
-Hint Unfold state_st_wf : htlproof.
-
-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 0)
-                                 (Option.join (array_get_error (Z.to_nat ptr) stack)))) ->
-    match_arrs m f sp mem asa.
-
-Definition stack_based (v : Values.val) (sp : Values.block) : Prop :=
-   match v with
-   | Values.Vptr sp' off => sp' = sp
-   | _ => True
-   end.
-
-Definition reg_stack_based_pointers (sp : Values.block) (rs : Registers.Regmap.t Values.val) : Prop :=
-  forall r, stack_based (Registers.Regmap.get r rs) sp.
-
-Definition arr_stack_based_pointers (spb : Values.block) (m : mem) (stack_length : Z)
-  (sp : Values.val) : Prop :=
-  forall ptr,
-    0 <= ptr < (stack_length / 4) ->
-    stack_based (Option.default
-                   Values.Vundef
-                   (Mem.loadv AST.Mint32 m
-                              (Values.Val.offset_ptr sp (Integers.Ptrofs.repr (4 * ptr)))))
-                spb.
-
-Definition stack_bounds (sp : Values.val) (hi : Z) (m : mem) : Prop :=
-  forall ptr v,
-    hi <= ptr <= Integers.Ptrofs.max_unsigned ->
-    Z.modulo ptr 4 = 0 ->
-    Mem.loadv AST.Mint32 m (Values.Val.offset_ptr sp (Integers.Ptrofs.repr ptr )) = None /\
-    Mem.storev AST.Mint32 m (Values.Val.offset_ptr sp (Integers.Ptrofs.repr ptr )) v = None.
-
-Inductive match_frames : list RTL.stackframe -> list HTL.stackframe -> Prop :=
-| match_frames_nil :
-    match_frames nil nil.
-
-  Lemma assumption_32bit :
-    forall v,
-      valueToPos (posToValue v) = v.
-  Proof.
-  Admitted.
-
-Inductive match_states : RTL.state -> HTL.state -> Prop :=
-| 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))
-    (MF : match_frames sf res)
-    (MARR : match_arrs m f sp mem asa)
-    (SP : sp = Values.Vptr sp' (Integers.Ptrofs.repr 0))
-    (RSBP : reg_stack_based_pointers sp' rs)
-    (ASBP : arr_stack_based_pointers sp' mem (f.(RTL.fn_stacksize)) sp)
-    (BOUNDS : stack_bounds sp (f.(RTL.fn_stacksize)) mem),
-    match_states (RTL.State sf f sp st rs mem)
-                 (HTL.State res m st asr asa)
-| match_returnstate :
-    forall
-      v v' stack mem res
-      (MF : match_frames stack res),
-      val_value_lessdef v v' ->
-      match_states (RTL.Returnstate stack v mem) (HTL.Returnstate res v')
-| match_initial_call :
-    forall f m m0
-    (TF : tr_module f m),
-      match_states (RTL.Callstate nil (AST.Internal f) nil m0) (HTL.Callstate nil m nil).
-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 /\
-  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. 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 :
-  forall f rs1 rs2 n v,
-    Plt (RTL.max_reg_function f) n ->
-    match_assocmaps f rs1 rs2 ->
-    match_assocmaps f rs1 (AssocMap.set n v rs2).
-Proof.
-  inversion 2; subst.
-  intros. constructor.
-  intros. unfold find_assocmap. unfold AssocMapExt.get_default.
-  rewrite AssocMap.gso. eauto.
-  apply Pos.le_lt_trans with _ _ n in H2.
-  unfold not. intros. subst. eapply Pos.lt_irrefl. eassumption. assumption.
-Qed.
-Hint Resolve regs_lessdef_add_greater : htlproof.
-
-Lemma regs_lessdef_add_match :
-  forall f rs am r v v',
-    val_value_lessdef v v' ->
-    match_assocmaps f rs am ->
-    match_assocmaps f (Registers.Regmap.set r v rs) (AssocMap.set r v' am).
-Proof.
-  inversion 2; subst.
-  constructor. intros.
-  destruct (peq r0 r); subst.
-  rewrite Registers.Regmap.gss.
-  unfold find_assocmap. unfold AssocMapExt.get_default.
-  rewrite AssocMap.gss. assumption.
-
-  rewrite Registers.Regmap.gso; try assumption.
-  unfold find_assocmap. unfold AssocMapExt.get_default.
-  rewrite AssocMap.gso; eauto.
-Qed.
-Hint Resolve regs_lessdef_add_match : htlproof.
-
-Lemma list_combine_none :
-  forall n l,
-    length l = n ->
-    list_combine Verilog.merge_cell (list_repeat None n) l = l.
-Proof.
-  induction n; intros; crush.
-  - symmetry. apply length_zero_iff_nil. auto.
-  - destruct l; crush.
-    rewrite list_repeat_cons.
-    crush. f_equal.
-    eauto.
-Qed.
-
-Lemma combine_none :
-  forall n a,
-    a.(arr_length) = n ->
-    arr_contents (combine Verilog.merge_cell (arr_repeat None n) a) = arr_contents a.
-Proof.
-  intros.
-  unfold combine.
-  crush.
-
-  rewrite <- (arr_wf a) in H.
-  apply list_combine_none.
-  assumption.
-Qed.
-
-Lemma list_combine_lookup_first :
-  forall l1 l2 n,
-    length l1 = length l2 ->
-    nth_error l1 n = Some None ->
-    nth_error (list_combine Verilog.merge_cell l1 l2) n = nth_error l2 n.
-Proof.
-  induction l1; intros; crush.
-
-  rewrite nth_error_nil in H0.
-  discriminate.
-
-  destruct l2 eqn:EQl2. crush.
-  simpl in H. invert H.
-  destruct n; simpl in *.
-  invert H0. simpl. reflexivity.
-  eauto.
-Qed.
-
-Lemma combine_lookup_first :
-  forall a1 a2 n,
-    a1.(arr_length) = a2.(arr_length) ->
-    array_get_error n a1 = Some None ->
-    array_get_error n (combine Verilog.merge_cell a1 a2) = array_get_error n a2.
-Proof.
-  intros.
-
-  unfold array_get_error in *.
-  apply list_combine_lookup_first; eauto.
-  rewrite a1.(arr_wf). rewrite a2.(arr_wf).
-  assumption.
-Qed.
-
-Lemma list_combine_lookup_second :
-  forall l1 l2 n x,
-    length l1 = length l2 ->
-    nth_error l1 n = Some (Some x) ->
-    nth_error (list_combine Verilog.merge_cell l1 l2) n = Some (Some x).
-Proof.
-  induction l1; intros; crush; auto.
-
-  destruct l2 eqn:EQl2. crush.
-  simpl in H. invert H.
-  destruct n; simpl in *.
-  invert H0. simpl. reflexivity.
-  eauto.
-Qed.
-
-Lemma combine_lookup_second :
-  forall a1 a2 n x,
-    a1.(arr_length) = a2.(arr_length) ->
-    array_get_error n a1 = Some (Some x) ->
-    array_get_error n (combine Verilog.merge_cell a1 a2) = Some (Some x).
-Proof.
-  intros.
-
-  unfold array_get_error in *.
-  apply list_combine_lookup_second; eauto.
-  rewrite a1.(arr_wf). rewrite a2.(arr_wf).
-  assumption.
-Qed.
-
-Ltac inv_state :=
-  match goal with
-    MSTATE : match_states _ _ |- _ =>
-    inversion MSTATE;
-    match goal with
-      TF : tr_module _ _ |- _ =>
-      inversion TF;
-      match goal with
-        TC : forall _ _,
-          Maps.PTree.get _ _ = Some _ -> tr_code _ _ _ _ _ _ _ _ _,
-        H : Maps.PTree.get _ _ = Some _ |- _ =>
-        apply TC in H; inversion H;
-        match goal with
-          TI : context[tr_instr] |- _ =>
-          inversion TI
-        end
-      end
-    end
-end; subst.
-
-Ltac unfold_func H :=
-  match type of H with
-  | ?f = _ => unfold f in H; repeat (unfold_match H)
-  | ?f _ = _ => unfold f in H; repeat (unfold_match H)
-  | ?f _ _ = _ => unfold f in H; repeat (unfold_match H)
-  | ?f _ _ _ = _ => unfold f in H; repeat (unfold_match H)
-  | ?f _ _ _ _ = _ => unfold f in H; repeat (unfold_match H)
-  end.
-
-Lemma init_reg_assoc_empty :
-  forall f l,
-    match_assocmaps f (RTL.init_regs nil l) (HTL.init_regs nil l).
-Proof.
-  induction l; simpl; constructor; intros.
-  - rewrite Registers.Regmap.gi. unfold find_assocmap.
-    unfold AssocMapExt.get_default. rewrite AssocMap.gempty.
-    constructor.
-
-  - rewrite Registers.Regmap.gi. unfold find_assocmap.
-    unfold AssocMapExt.get_default. rewrite AssocMap.gempty.
-    constructor.
-Qed.
-
-Lemma arr_lookup_some:
-  forall (z : Z) (r0 : Registers.reg) (r : Verilog.reg) (asr : assocmap) (asa : Verilog.assocmap_arr)
-    (stack : Array (option value)) (H5 : asa ! r = Some stack) n,
-    exists x, Verilog.arr_assocmap_lookup asa r n = Some x.
-Proof.
-  intros z r0 r asr asa stack H5 n.
-  eexists.
-  unfold Verilog.arr_assocmap_lookup. rewrite H5. reflexivity.
-Qed.
-Hint Resolve arr_lookup_some : htlproof.
-
-Section CORRECTNESS.
-
-  Variable prog : RTL.program.
-  Variable tprog : HTL.program.
-
-  Hypothesis TRANSL : match_prog prog tprog.
-
-  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. intros. eapply (Genv.find_symbol_match TRANSL'). Qed.
-
-  Lemma function_ptr_translated:
-    forall (b: Values.block) (f: RTL.fundef),
-      Genv.find_funct_ptr ge b = Some f ->
-      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 (cu & tf & P & Q & R); exists tf; auto.
-  Qed.
-
-  Lemma functions_translated:
-    forall (v: Values.val) (f: RTL.fundef),
-      Genv.find_funct ge v = Some f ->
-      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 (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').
-  Hint Resolve senv_preserved : htlproof.
-
-  Lemma ptrofs_inj :
-    forall a b,
-      Ptrofs.unsigned a = Ptrofs.unsigned b -> a = b.
-  Proof.
-    intros. rewrite <- Ptrofs.repr_unsigned. symmetry. rewrite <- Ptrofs.repr_unsigned.
-    rewrite H. auto.
-  Qed.
-
-  Lemma eval_correct :
-    forall s sp op rs m v e asr asa f f' stk s' i pc res0 pc' args res ml st,
-      match_states (RTL.State stk f sp pc rs m) (HTL.State res ml st asr asa) ->
-      (RTL.fn_code f) ! pc = Some (RTL.Iop op args res0 pc') ->
-      Op.eval_operation ge sp op
-                        (List.map (fun r : BinNums.positive => Registers.Regmap.get r rs) args) m = Some v ->
-      translate_instr op args s = OK e s' i ->
-      exists v', Verilog.expr_runp f' asr asa e v' /\ val_value_lessdef v v'.
-  Proof.
-    intros s sp op rs m v e asr asa f f' stk s' i pc pc' res0 args res ml st MSTATE INSTR EVAL TR_INSTR.
-    inv MSTATE. inv MASSOC. unfold translate_instr in TR_INSTR; repeat (unfold_match TR_INSTR); inv TR_INSTR;
-    unfold Op.eval_operation in EVAL; repeat (unfold_match EVAL); simplify.
-    - inv Heql.
-      assert (HPle : Ple r (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto).
-      apply H in HPle. eexists. split; try constructor; eauto.
-    - eexists. split. constructor. constructor. auto.
-    - inv Heql.
-      assert (HPle : Ple r (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto).
-      apply H in HPle.
-      eexists. split. econstructor; eauto. constructor. trivial.
-      unfold Verilog.unop_run. unfold Values.Val.neg. destruct (Registers.Regmap.get r rs) eqn:?; constructor.
-      inv HPle. auto.
-    - inv Heql.
-      assert (HPle : Ple r (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto).
-      assert (HPle0 : Ple r0 (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto).
-      apply H in HPle. apply H in HPle0.
-      eexists. split. econstructor; eauto. constructor. trivial.
-      constructor. trivial. simplify. inv HPle. inv HPle0; constructor; auto.
-      + inv HPle0. constructor. unfold valueToPtr. Search Integers.Ptrofs.sub Integers.int.
-        pose proof Integers.Ptrofs.agree32_sub. unfold Integers.Ptrofs.agree32 in H3.
-        Print Integers.Ptrofs.agree32. unfold Ptrofs.of_int. simpl.
-        apply ptrofs_inj. assert (Archi.ptr64 = false) by auto. eapply H3 in H4.
-        rewrite Ptrofs.unsigned_repr. apply H4. replace Ptrofs.max_unsigned with Int.max_unsigned; auto.
-        apply Int.unsigned_range_2.
-        auto. rewrite Ptrofs.unsigned_repr. replace Ptrofs.max_unsigned with Int.max_unsigned; auto.
-        apply Int.unsigned_range_2. rewrite Ptrofs.unsigned_repr. auto.
-        replace Ptrofs.max_unsigned with Int.max_unsigned; auto.
-        apply Int.unsigned_range_2.
-        Admitted.
-
-  Lemma eval_cond_correct :
-    forall cond (args : list Registers.reg) s1 c s' i rs args m b f asr asa,
-      translate_condition cond args s1 = OK c s' i ->
-      Op.eval_condition
-        cond
-        (List.map (fun r : BinNums.positive => Registers.Regmap.get r rs) args)
-        m = Some b ->
-      Verilog.expr_runp f asr asa c (boolToValue b).
-  Admitted.
-
-  (** The proof of semantic preservation for the translation of instructions
-      is a simulation argument based on diagrams of the following form:
-<<
-                      match_states
-    code st rs ---------------- State m st assoc
-         ||                             |
-         ||                             |
-         ||                             |
-         \/                             v
-    code st rs' --------------- State m st assoc'
-                      match_states
->>
-      where [tr_code c data control fin rtrn st] is assumed to hold.
-
-      The precondition and postcondition is that that should hold is [match_assocmaps rs assoc].
-   *)
-
-  Definition transl_instr_prop (instr : RTL.instruction) : Prop :=
-    forall m asr asa fin rtrn st stmt trans res,
-      tr_instr fin rtrn st (m.(HTL.mod_stk)) instr stmt trans ->
-      exists asr' asa',
-        HTL.step tge (HTL.State res m st asr asa) Events.E0 (HTL.State res m st asr' asa').
-
-  Opaque combine.
-
-  Ltac tac0 :=
-    match goal with
-    | [ |- context[valueToPos (posToValue _)] ] => rewrite assumption_32bit
-
-    | [ |- context[Verilog.merge_arrs _ _] ] => unfold Verilog.merge_arrs
-    | [ |- context[Verilog.merge_arr] ] => unfold Verilog.merge_arr
-    | [ |- context[Verilog.merge_regs _ _] ] => unfold Verilog.merge_regs; crush; unfold_merge
-    | [ |- context[reg_stack_based_pointers] ] => unfold reg_stack_based_pointers; intros
-    | [ |- context[Verilog.arr_assocmap_set _ _ _ _] ] => unfold Verilog.arr_assocmap_set
-
-    | [ |- context[HTL.empty_stack] ] => unfold HTL.empty_stack
-
-    | [ |- context[_ # ?d <- _ ! ?d] ] => rewrite AssocMap.gss
-    | [ |- context[_ # ?d <- _ ! ?s] ] => rewrite AssocMap.gso
-    | [ |- context[(AssocMap.empty _) ! _] ] => rewrite AssocMap.gempty
-
-    | [ |- context[array_get_error _ (combine Verilog.merge_cell (arr_repeat None _) _)] ] =>
-      rewrite combine_lookup_first
-
-    | [ |- state_st_wf _ _ ] => unfold state_st_wf; inversion 1
-    | [ |- context[match_states _ _] ] => econstructor; auto
-    | [ |- match_arrs _ _ _ _ _ ] => econstructor; auto
-    | [ |- match_assocmaps _ _ _ # _ <- (posToValue _) ] =>
-      apply regs_lessdef_add_greater; [> unfold Plt; lia | assumption]
-
-    | [ H : ?asa ! ?r = Some _ |- Verilog.arr_assocmap_lookup ?asa ?r _ = Some _ ] =>
-      unfold Verilog.arr_assocmap_lookup; setoid_rewrite H; f_equal
-    | [ |- context[(AssocMap.combine _ _ _) ! _] ] =>
-      try (rewrite AssocMap.gcombine; [> | reflexivity])
-
-    | [ |- context[Registers.Regmap.get ?d (Registers.Regmap.set ?d _ _)] ] =>
-      rewrite Registers.Regmap.gss
-    | [ |- context[Registers.Regmap.get ?s (Registers.Regmap.set ?d _ _)] ] =>
-      destruct (Pos.eq_dec s d) as [EQ|EQ];
-      [> rewrite EQ | rewrite Registers.Regmap.gso; auto]
-
-    | [ H : opt_val_value_lessdef _ _ |- _ ] => invert H
-    | [ H : context[Z.of_nat (Z.to_nat _)] |- _ ] => rewrite Z2Nat.id in H; [> solve crush |]
-    | [ H : _ ! _ = Some _ |- _] => setoid_rewrite H
-    end.
-
-  Ltac small_tac := repeat (crush; try array; try ptrofs); crush; auto.
-  Ltac big_tac := repeat (crush; try array; try ptrofs; try tac0); crush; auto.
-
-  Lemma transl_inop_correct:
-    forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive)
-      (rs : RTL.regset) (m : mem) (pc' : RTL.node),
-      (RTL.fn_code f) ! pc = Some (RTL.Inop pc') ->
-      forall R1 : HTL.state,
-        match_states (RTL.State s f sp pc rs m) R1 ->
-        exists R2 : HTL.state,
-          Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ match_states (RTL.State s f sp pc' rs m) R2.
-  Proof.
-    intros s f sp pc rs m pc' H R1 MSTATE.
-    inv_state.
-
-    unfold match_prog in TRANSL.
-    econstructor.
-    split.
-    apply Smallstep.plus_one.
-    eapply HTL.step_module; eauto.
-    apply assumption_32bit.
-    (* processing of state *)
-    econstructor.
-    crush.
-    econstructor.
-    econstructor.
-    econstructor.
-
-    all: invert MARR; big_tac.
-    Unshelve.
-    constructor.
-  Qed.
-  Hint Resolve transl_inop_correct : htlproof.
-
-  Lemma transl_iop_correct:
-    forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive)
-      (rs : Registers.Regmap.t Values.val) (m : mem) (op : Op.operation) (args : list Registers.reg)
-      (res0 : Registers.reg) (pc' : RTL.node) (v : Values.val),
-      (RTL.fn_code f) ! pc = Some (RTL.Iop op args res0 pc') ->
-      Op.eval_operation ge sp op (map (fun r : positive => Registers.Regmap.get r rs) args) m = Some v ->
-      forall R1 : HTL.state,
-        match_states (RTL.State s f sp pc rs m) R1 ->
-        exists R2 : HTL.state,
-          Smallstep.plus HTL.step tge R1 Events.E0 R2 /\
-          match_states (RTL.State s f sp pc' (Registers.Regmap.set res0 v rs) m) R2.
-  Proof.
-    intros s f sp pc rs m op args res0 pc' v H H0 R1 MSTATE.
-    inv_state.
-    exploit eval_correct; eauto. intros. inversion H1. inversion H2.
-    econstructor. split.
-    apply Smallstep.plus_one.
-    eapply HTL.step_module; eauto.
-    apply assumption_32bit.
-    econstructor; simpl; trivial.
-    constructor; trivial.
-    econstructor; simpl; eauto.
-    simpl. econstructor. econstructor.
-    apply H3. simplify.
-
-    all: big_tac.
-
-    assert (Ple res0 (RTL.max_reg_function f))
-        by (eapply RTL.max_reg_function_def; eauto; simpl; auto).
-
-    unfold Ple in H10. lia.
-    apply regs_lessdef_add_match. assumption.
-    apply regs_lessdef_add_greater. unfold Plt; lia. assumption.
-    assert (Ple res0 (RTL.max_reg_function f))
-        by (eapply RTL.max_reg_function_def; eauto; simpl; auto).
-    unfold Ple in H12; lia.
-    unfold_merge. simpl.
-    rewrite AssocMap.gso.
-    apply AssocMap.gss.
-    apply st_greater_than_res.
-
-    (*match_states*)
-      assert (pc' = valueToPos (posToValue 32 pc')). auto using assumption_32bit.
-    rewrite <- H1.
-    constructor; auto.
-    unfold_merge.
-    apply regs_lessdef_add_match.
-    constructor.
-    apply regs_lessdef_add_greater.
-    apply greater_than_max_func.
-    assumption.
-
-    unfold state_st_wf. intros. inversion H2. subst.
-    unfold_merge.
-    rewrite AssocMap.gso.
-    apply AssocMap.gss.
-    apply st_greater_than_res.
-
-     + econstructor. split.
-     apply Smallstep.plus_one.
-     eapply HTL.step_module; eauto.
-     econstructor; simpl; trivial.
-     constructor; trivial.
-     econstructor; simpl; eauto.
-     eapply eval_correct; eauto.
-     constructor. rewrite valueToInt_intToValue. trivial.
-     unfold_merge. simpl.
-     rewrite AssocMap.gso.
-     apply AssocMap.gss.
-     apply st_greater_than_res.
-
-      match_states
-     assert (pc' = valueToPos (posToValue 32 pc')). auto using assumption_32bit.
-     rewrite <- H1.
-     constructor.
-     unfold_merge.
-     apply regs_lessdef_add_match.
-     constructor.
-     symmetry. apply valueToInt_intToValue.
-     apply regs_lessdef_add_greater.
-     apply greater_than_max_func.
-     assumption. assumption.
-
-     unfold state_st_wf. intros. inversion H2. subst.
-     unfold_merge.
-     rewrite AssocMap.gso.
-     apply AssocMap.gss.
-     apply st_greater_than_res.
-     assumption.
-  Admitted.
-  Hint Resolve transl_iop_correct : htlproof.
-
-  Ltac tac :=
-    repeat match goal with
-           | [ _ : error _ _ = OK _ _ _ |- _ ] => discriminate
-           | [ _ : context[if (?x && ?y) then _ else _] |- _ ] =>
-             let EQ1 := fresh "EQ" in
-             let EQ2 := fresh "EQ" in
-             destruct x eqn:EQ1; destruct y eqn:EQ2; simpl in *
-           | [ _ : context[if ?x then _ else _] |- _ ] =>
-             let EQ := fresh "EQ" in
-             destruct x eqn:EQ; simpl in *
-           | [ H : ret _ _ = _  |- _ ] => invert H
-           | [ _ : context[match ?x with | _ => _ end] |- _ ] => destruct x
-           end.
-
-  Ltac inv_arr_access :=
-    match goal with
-    | [ _ : translate_arr_access ?chunk ?addr ?args _ _ = OK ?c _ _ |- _] =>
-      destruct c, chunk, addr, args; crush; tac; crush
-    end.
-
-  Lemma transl_iload_correct:
-    forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive)
-      (rs : Registers.Regmap.t Values.val) (m : mem) (chunk : AST.memory_chunk)
-      (addr : Op.addressing) (args : list Registers.reg) (dst : Registers.reg)
-      (pc' : RTL.node) (a v : Values.val),
-      (RTL.fn_code f) ! pc = Some (RTL.Iload chunk addr args dst pc') ->
-      Op.eval_addressing ge sp addr (map (fun r : positive => Registers.Regmap.get r rs) args) = Some a ->
-      Mem.loadv chunk m a = Some v ->
-      forall R1 : HTL.state,
-        match_states (RTL.State s f sp pc rs m) R1 ->
-        exists R2 : HTL.state,
-          Smallstep.plus HTL.step tge R1 Events.E0 R2 /\
-          match_states (RTL.State s f sp pc' (Registers.Regmap.set dst v rs) m) R2.
-  Proof.
-    intros s f sp pc rs m chunk addr args dst pc' a v H H0 H1 R1 MSTATE.
-    inv_state. inv_arr_access.
-
-    + (** Preamble *)
-      invert MARR. crush.
-
-      unfold Op.eval_addressing in H0.
-      destruct (Archi.ptr64) eqn:ARCHI; crush.
-
-      unfold reg_stack_based_pointers in RSBP.
-      pose proof (RSBP r0) as RSBPr0.
-
-      destruct (Registers.Regmap.get r0 rs) eqn:EQr0; crush.
-
-      rewrite ARCHI in H1. crush.
-      subst.
-
-      pose proof MASSOC as MASSOC'.
-      invert MASSOC'.
-      pose proof (H0 r0).
-      assert (HPler0 : Ple r0 (RTL.max_reg_function f))
-        by (eapply RTL.max_reg_function_use; eauto; crush; eauto).
-      apply H6 in HPler0.
-      invert HPler0; try congruence.
-      rewrite EQr0 in H8.
-      invert H8.
-      clear H0. clear H6.
-
-      unfold check_address_parameter_signed in *;
-      unfold check_address_parameter_unsigned in *; crush.
-
-      remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ asr # r0))
-                                    (Integers.Ptrofs.of_int (Integers.Int.repr z))) as OFFSET.
-
-      (** Modular preservation proof *)
-      assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE.
-      { rewrite HeqOFFSET.
-        apply PtrofsExtra.add_mod; crush.
-        rewrite Integers.Ptrofs.unsigned_repr_eq.
-        rewrite <- Zmod_div_mod; crush.
-        apply PtrofsExtra.of_int_mod.
-        rewrite Integers.Int.unsigned_repr_eq.
-        rewrite <- Zmod_div_mod; crush. }
-
-      (** Read bounds proof *)
-      assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH.
-      { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; crush; auto.
-        unfold stack_bounds in BOUNDS.
-        exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET)); auto.
-        split; try lia; apply Integers.Ptrofs.unsigned_range_2.
-        small_tac. }
-
-      (** Normalisation proof *)
-      assert (Integers.Ptrofs.repr
-                (4 * Integers.Ptrofs.unsigned
-                       (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4))) = OFFSET)
-        as NORMALISE.
-      { replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) at 1 by reflexivity.
-        rewrite <- PtrofsExtra.mul_unsigned.
-        apply PtrofsExtra.mul_divu; crush; auto. }
-
-      (** Normalised bounds proof *)
-      assert (0 <=
-              Integers.Ptrofs.unsigned (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4))
-              < (RTL.fn_stacksize f / 4))
-        as NORMALISE_BOUND.
-      { split.
-        apply Integers.Ptrofs.unsigned_range_2.
-        assert (forall x y, Integers.Ptrofs.divu x y = Integers.Ptrofs.divu x y ) by reflexivity.
-        unfold Integers.Ptrofs.divu at 2 in H0.
-        rewrite H0. clear H0.
-        rewrite Integers.Ptrofs.unsigned_repr; crush.
-        apply Zmult_lt_reg_r with (p := 4); try lia.
-        repeat rewrite ZLib.div_mul_undo; try lia.
-        apply Z.div_pos; small_tac.
-        apply Z.div_le_upper_bound; small_tac. }
-
-      inversion NORMALISE_BOUND as [ NORMALISE_BOUND_LOW NORMALISE_BOUND_HIGH ];
-      clear NORMALISE_BOUND.
-
-      (** Start of proof proper *)
-      eexists. split.
-      eapply Smallstep.plus_one.
-      eapply HTL.step_module; eauto.
-      apply assumption_32bit.
-      econstructor. econstructor. econstructor. crush.
-      econstructor. econstructor. econstructor. crush.
-      econstructor. econstructor.
-      econstructor. econstructor. econstructor. econstructor.
-      econstructor. econstructor. econstructor. econstructor.
-
-      all: big_tac.
-
-      1: {
-        assert (HPle : Ple dst (RTL.max_reg_function f)).
-        eapply RTL.max_reg_function_def. eassumption. auto.
-        apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption.
-      }
-
-      2: {
-        assert (HPle : Ple dst (RTL.max_reg_function f)).
-        eapply RTL.max_reg_function_def. eassumption. auto.
-        apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption.
-      }
-
-      (** Match assocmaps *)
-      apply regs_lessdef_add_match; big_tac.
-
-      (** Equality proof *)
-      match goal with
-      | [ |- context [valueToNat ?x] ] =>
-        assert (Z.to_nat
-                  (Integers.Ptrofs.unsigned
-                     (Integers.Ptrofs.divu
-                        OFFSET
-                        (Integers.Ptrofs.repr 4)))
-                =
-                valueToNat x)
-          as EXPR_OK by admit
-      end.
-      rewrite <- EXPR_OK.
-
-      specialize (H7 (Integers.Ptrofs.unsigned
-                        (Integers.Ptrofs.divu
-                           OFFSET
-                           (Integers.Ptrofs.repr 4)))).
-      exploit H7; big_tac.
-
-      (** RSBP preservation *)
-      unfold arr_stack_based_pointers in ASBP.
-      specialize (ASBP (Integers.Ptrofs.unsigned
-                          (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)))).
-      exploit ASBP; big_tac.
-      rewrite NORMALISE in H0. rewrite H1 in H0. assumption.
-
-    + (** Preamble *)
-      invert MARR. crush.
-
-      unfold Op.eval_addressing in H0.
-      destruct (Archi.ptr64) eqn:ARCHI; crush.
-
-      unfold reg_stack_based_pointers in RSBP.
-      pose proof (RSBP r0) as RSBPr0.
-      pose proof (RSBP r1) as RSBPr1.
-
-      destruct (Registers.Regmap.get r0 rs) eqn:EQr0;
-      destruct (Registers.Regmap.get r1 rs) eqn:EQr1; crush.
-
-      rewrite ARCHI in H1. crush.
-      subst.
-      clear RSBPr1.
-
-      pose proof MASSOC as MASSOC'.
-      invert MASSOC'.
-      pose proof (H0 r0).
-      pose proof (H0 r1).
-      assert (HPler0 : Ple r0 (RTL.max_reg_function f))
-        by (eapply RTL.max_reg_function_use; eauto; crush; eauto).
-      assert (HPler1 : Ple r1 (RTL.max_reg_function f))
-        by (eapply RTL.max_reg_function_use; eauto; simpl; auto).
-      apply H6 in HPler0.
-      apply H8 in HPler1.
-      invert HPler0; invert HPler1; try congruence.
-      rewrite EQr0 in H9.
-      rewrite EQr1 in H11.
-      invert H9. invert H11.
-      clear H0. clear H6. clear H8.
-
-      unfold check_address_parameter_signed in *;
-      unfold check_address_parameter_unsigned in *; crush.
-
-      remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ asr # r0))
-                                    (Integers.Ptrofs.of_int
-                                       (Integers.Int.add (Integers.Int.mul (valueToInt asr # r1) (Integers.Int.repr z))
-                                                         (Integers.Int.repr z0)))) as OFFSET.
-
-      (** Modular preservation proof *)
-      assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE.
-      { rewrite HeqOFFSET.
-        apply PtrofsExtra.add_mod; crush; try lia.
-        rewrite Integers.Ptrofs.unsigned_repr_eq.
-        rewrite <- Zmod_div_mod; crush.
-        apply PtrofsExtra.of_int_mod.
-        apply IntExtra.add_mod; crush.
-        apply IntExtra.mul_mod2; crush.
-        rewrite Integers.Int.unsigned_repr_eq.
-        rewrite <- Zmod_div_mod; crush.
-        rewrite Integers.Int.unsigned_repr_eq.
-        rewrite <- Zmod_div_mod; crush. }
-
-      (** Read bounds proof *)
-      assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH.
-      { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; crush; auto.
-        unfold stack_bounds in BOUNDS.
-        exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET)); auto.
-        split; try lia; apply Integers.Ptrofs.unsigned_range_2.
-        small_tac. }
-
-      (** Normalisation proof *)
-      assert (Integers.Ptrofs.repr
-                (4 * Integers.Ptrofs.unsigned
-                       (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4))) = OFFSET)
-        as NORMALISE.
-      { replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) at 1 by reflexivity.
-        rewrite <- PtrofsExtra.mul_unsigned.
-        apply PtrofsExtra.mul_divu; crush. }
-
-      (** Normalised bounds proof *)
-      assert (0 <=
-              Integers.Ptrofs.unsigned (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4))
-              < (RTL.fn_stacksize f / 4))
-        as NORMALISE_BOUND.
-      { split.
-        apply Integers.Ptrofs.unsigned_range_2.
-        assert (forall x y, Integers.Ptrofs.divu x y = Integers.Ptrofs.divu x y ) by reflexivity.
-        unfold Integers.Ptrofs.divu at 2 in H0.
-        rewrite H0. clear H0.
-        rewrite Integers.Ptrofs.unsigned_repr; crush.
-        apply Zmult_lt_reg_r with (p := 4); try lia.
-        repeat rewrite ZLib.div_mul_undo; try lia.
-        apply Z.div_pos; small_tac.
-        apply Z.div_le_upper_bound; lia. }
-
-      inversion NORMALISE_BOUND as [ NORMALISE_BOUND_LOW NORMALISE_BOUND_HIGH ];
-      clear NORMALISE_BOUND.
-
-      (** Start of proof proper *)
-      eexists. split.
-      eapply Smallstep.plus_one.
-      eapply HTL.step_module; eauto.
-      apply assumption_32bit.
-      econstructor. econstructor. econstructor. crush.
-      econstructor. econstructor. econstructor. crush.
-      econstructor. econstructor. econstructor.
-      econstructor. econstructor. econstructor. econstructor.
-      econstructor.
-      eapply Verilog.erun_Vbinop with (EQ := ?[EQ6]).
-      econstructor. econstructor. econstructor. econstructor.
-      econstructor. econstructor. econstructor. econstructor.
-      econstructor. econstructor.
-
-      all: big_tac.
-
-      1: { assert (HPle : Ple dst (RTL.max_reg_function f)).
-           eapply RTL.max_reg_function_def. eassumption. auto.
-           apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. }
-
-      2: { assert (HPle : Ple dst (RTL.max_reg_function f)).
-           eapply RTL.max_reg_function_def. eassumption. auto.
-           apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. }
-
-      (** Match assocmaps *)
-      apply regs_lessdef_add_match; big_tac.
-
-      (** Equality proof *)
-      match goal with
-      | [ |- context [valueToNat ?x] ] =>
-        assert (Z.to_nat
-                  (Integers.Ptrofs.unsigned
-                     (Integers.Ptrofs.divu
-                        OFFSET
-                        (Integers.Ptrofs.repr 4)))
-                =
-                valueToNat x)
-          as EXPR_OK by admit
-      end.
-      rewrite <- EXPR_OK.
-
-      specialize (H7 (Integers.Ptrofs.unsigned
-                        (Integers.Ptrofs.divu
-                           OFFSET
-                           (Integers.Ptrofs.repr 4)))).
-      exploit H7; big_tac.
-
-      (** RSBP preservation *)
-      unfold arr_stack_based_pointers in ASBP.
-      specialize (ASBP (Integers.Ptrofs.unsigned
-                          (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)))).
-      exploit ASBP; big_tac.
-      rewrite NORMALISE in H0. rewrite H1 in H0. assumption.
-
-    + invert MARR. crush.
-
-      unfold Op.eval_addressing in H0.
-      destruct (Archi.ptr64) eqn:ARCHI; crush.
-      rewrite ARCHI in H0. crush.
-
-      unfold check_address_parameter_unsigned in *;
-      unfold check_address_parameter_signed in *; crush.
-
-      assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
-      rewrite ZERO in H1. clear ZERO.
-      rewrite Integers.Ptrofs.add_zero_l in H1.
-
-      remember i0 as OFFSET.
-
-      (** Modular preservation proof *)
-      rename H0 into MOD_PRESERVE.
-
-      (** Read bounds proof *)
-      assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH.
-      { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; crush; auto.
-        unfold stack_bounds in BOUNDS.
-        exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET)); big_tac. }
-
-      (** Normalisation proof *)
-      assert (Integers.Ptrofs.repr
-                (4 * Integers.Ptrofs.unsigned
-                       (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4))) = OFFSET)
-        as NORMALISE.
-      { replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) at 1 by reflexivity.
-        rewrite <- PtrofsExtra.mul_unsigned.
-        apply PtrofsExtra.mul_divu; crush. }
-
-      (** Normalised bounds proof *)
-      assert (0 <=
-              Integers.Ptrofs.unsigned (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4))
-              < (RTL.fn_stacksize f / 4))
-        as NORMALISE_BOUND.
-      { split.
-        apply Integers.Ptrofs.unsigned_range_2.
-        assert (forall x y, Integers.Ptrofs.divu x y = Integers.Ptrofs.divu x y ) by reflexivity.
-        unfold Integers.Ptrofs.divu at 2 in H0.
-        rewrite H0. clear H0.
-        rewrite Integers.Ptrofs.unsigned_repr; crush.
-        apply Zmult_lt_reg_r with (p := 4); try lia.
-        repeat rewrite ZLib.div_mul_undo; try lia.
-        apply Z.div_pos; small_tac.
-        apply Z.div_le_upper_bound; lia. }
-
-      inversion NORMALISE_BOUND as [ NORMALISE_BOUND_LOW NORMALISE_BOUND_HIGH ];
-      clear NORMALISE_BOUND.
-
-      (** Start of proof proper *)
-      eexists. split.
-      eapply Smallstep.plus_one.
-      eapply HTL.step_module; eauto.
-      apply assumption_32bit.
-      econstructor. econstructor. econstructor. crush.
-      econstructor. econstructor. econstructor. econstructor. crush.
-
-      all: big_tac.
-
-      1: { assert (HPle : Ple dst (RTL.max_reg_function f)).
-           eapply RTL.max_reg_function_def. eassumption. auto.
-           apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. }
-
-      2: { assert (HPle : Ple dst (RTL.max_reg_function f)).
-           eapply RTL.max_reg_function_def. eassumption. auto.
-           apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. }
-
-      (** Match assocmaps *)
-      apply regs_lessdef_add_match; big_tac.
-
-      (** Equality proof *)
-      match goal with (* Prevents issues with evars *)
-      | [ |- context [valueToNat ?x] ] =>
-        assert (Z.to_nat
-                  (Integers.Ptrofs.unsigned
-                     (Integers.Ptrofs.divu
-                        OFFSET
-                        (Integers.Ptrofs.repr 4)))
-                =
-                valueToNat x)
-          as EXPR_OK by admit
-      end.
-      rewrite <- EXPR_OK.
-
-      specialize (H7 (Integers.Ptrofs.unsigned
-                        (Integers.Ptrofs.divu
-                           OFFSET
-                           (Integers.Ptrofs.repr 4)))).
-      exploit H7; big_tac.
-
-      (** RSBP preservation *)
-      unfold arr_stack_based_pointers in ASBP.
-      specialize (ASBP (Integers.Ptrofs.unsigned
-                          (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)))).
-      exploit ASBP; big_tac.
-      rewrite NORMALISE in H0. rewrite H1 in H0. assumption.
-  Admitted.
-  Hint Resolve transl_iload_correct : htlproof.
-
-  Lemma transl_istore_correct:
-    forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive)
-      (rs : Registers.Regmap.t Values.val) (m : mem) (chunk : AST.memory_chunk)
-      (addr : Op.addressing) (args : list Registers.reg) (src : Registers.reg)
-      (pc' : RTL.node) (a : Values.val) (m' : mem),
-      (RTL.fn_code f) ! pc = Some (RTL.Istore chunk addr args src pc') ->
-      Op.eval_addressing ge sp addr (map (fun r : positive => Registers.Regmap.get r rs) args) = Some a ->
-      Mem.storev chunk m a (Registers.Regmap.get src rs) = Some m' ->
-      forall R1 : HTL.state,
-        match_states (RTL.State s f sp pc rs m) R1 ->
-        exists R2 : HTL.state,
-          Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ match_states (RTL.State s f sp pc' rs m') R2.
-  Proof.
-    intros s f sp pc rs m chunk addr args src pc' a m' H H0 H1 R1 MSTATES.
-    inv_state. inv_arr_access.
-
-    + (** Preamble *)
-      invert MARR. crush.
-
-      unfold Op.eval_addressing in H0.
-      destruct (Archi.ptr64) eqn:ARCHI; crush.
-
-      unfold reg_stack_based_pointers in RSBP.
-      pose proof (RSBP r0) as RSBPr0.
-
-      destruct (Registers.Regmap.get r0 rs) eqn:EQr0; crush.
-
-      rewrite ARCHI in H1. crush.
-      subst.
-
-      pose proof MASSOC as MASSOC'.
-      invert MASSOC'.
-      pose proof (H0 r0).
-      assert (HPler0 : Ple r0 (RTL.max_reg_function f))
-        by (eapply RTL.max_reg_function_use; eauto; crush; eauto).
-      apply H6 in HPler0.
-      invert HPler0; try congruence.
-      rewrite EQr0 in H8.
-      invert H8.
-      clear H0. clear H6.
-
-      unfold check_address_parameter_unsigned in *;
-      unfold check_address_parameter_signed in *; crush.
-
-      remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ asr # r0))
-                                    (Integers.Ptrofs.of_int (Integers.Int.repr z))) as OFFSET.
-
-      (** Modular preservation proof *)
-      assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE.
-      { rewrite HeqOFFSET.
-        apply PtrofsExtra.add_mod; crush; try lia.
-        rewrite Integers.Ptrofs.unsigned_repr_eq.
-        rewrite <- Zmod_div_mod; crush.
-        apply PtrofsExtra.of_int_mod.
-        rewrite Integers.Int.unsigned_repr_eq.
-        rewrite <- Zmod_div_mod; crush. }
-
-      (** Write bounds proof *)
-      assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as WRITE_BOUND_HIGH.
-      { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; crush; auto.
-        unfold stack_bounds in BOUNDS.
-        exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET) (Registers.Regmap.get src rs)); big_tac.
-        apply Integers.Ptrofs.unsigned_range_2. }
-
-      (** Start of proof proper *)
-      eexists. split.
-      eapply Smallstep.plus_one.
-      eapply HTL.step_module; eauto.
-      apply assumption_32bit.
-      econstructor. econstructor. econstructor.
-      eapply Verilog.stmnt_runp_Vnonblock_arr. crush.
-      econstructor.
-      eapply Verilog.erun_Vbinop with (EQ := ?[EQ7]).
-      eapply Verilog.erun_Vbinop with (EQ := ?[EQ8]).
-      econstructor.
-      econstructor.
-      econstructor. econstructor. econstructor. econstructor.
-      econstructor. econstructor. econstructor. econstructor.
-
-      all: crush.
-
-      (** State Lookup *)
-      unfold Verilog.merge_regs.
-      crush.
-      unfold_merge.
-      apply AssocMap.gss.
-
-      (** Match states *)
-      rewrite assumption_32bit.
-      econstructor; eauto.
-
-      (** Match assocmaps *)
-      unfold Verilog.merge_regs. crush. unfold_merge.
-      apply regs_lessdef_add_greater.
-      unfold Plt; lia.
-      assumption.
-
-      (** States well formed *)
-      unfold state_st_wf. inversion 1. crush.
-      unfold Verilog.merge_regs.
-      unfold_merge.
-      apply AssocMap.gss.
-
-      (** Equality proof *)
-      match goal with
-      | [ |- context [valueToNat ?x] ] =>
-        assert (Z.to_nat
-                  (Integers.Ptrofs.unsigned
-                     (Integers.Ptrofs.divu
-                        OFFSET
-                        (Integers.Ptrofs.repr 4)))
-                =
-                valueToNat x)
-          as EXPR_OK by admit
-      end.
-
-      assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
-      inversion MASSOC; revert HeqOFFSET; subst; clear MASSOC; intros HeqOFFSET.
-
-      econstructor.
-      repeat split; crush.
-      unfold HTL.empty_stack.
-      crush.
-      unfold Verilog.merge_arrs.
-
-      rewrite AssocMap.gcombine.
-      2: { reflexivity. }
-      unfold Verilog.arr_assocmap_set.
-      rewrite AssocMap.gss.
-      unfold Verilog.merge_arr.
-      rewrite AssocMap.gss.
-      setoid_rewrite H5.
-      reflexivity.
-
-      rewrite combine_length.
-      rewrite <- array_set_len.
-      unfold arr_repeat. crush.
-      apply list_repeat_len.
-
-      rewrite <- array_set_len.
-      unfold arr_repeat. crush.
-      rewrite list_repeat_len.
-      rewrite H4. reflexivity.
-
-      remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ asr # r0))
-                                    (Integers.Ptrofs.of_int (Integers.Int.repr z))) as OFFSET.
-
-      destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET).
-
-      erewrite Mem.load_store_same.
-      2: { rewrite ZERO.
-           rewrite Integers.Ptrofs.add_zero_l.
-           rewrite e.
-           rewrite Integers.Ptrofs.unsigned_repr.
-           exact H1.
-           apply Integers.Ptrofs.unsigned_range_2. }
-      constructor.
-      erewrite combine_lookup_second.
-      simpl.
-      assert (Ple src (RTL.max_reg_function f))
-        by (eapply RTL.max_reg_function_use; eauto; simpl; auto);
-      apply H0 in H13.
-      destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; invert H13; eauto.
-
-      rewrite <- array_set_len.
-      unfold arr_repeat. crush.
-      rewrite list_repeat_len. auto.
-
-      assert (4 * ptr / 4 = Integers.Ptrofs.unsigned OFFSET / 4) by (f_equal; assumption).
-      rewrite Z.mul_comm in H13.
-      rewrite Z_div_mult in H13; try lia.
-      replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) in H13 by reflexivity.
-      rewrite <- PtrofsExtra.divu_unsigned in H13; unfold_constants; try lia.
-      rewrite H13. rewrite EXPR_OK.
-      rewrite array_get_error_set_bound.
-      reflexivity.
-      unfold arr_length, arr_repeat. simpl.
-      rewrite list_repeat_len. lia.
-
-      erewrite Mem.load_store_other with (m1 := m).
-      2: { exact H1. }
-      2: { right.
-           rewrite ZERO.
-           rewrite Integers.Ptrofs.add_zero_l.
-           rewrite Integers.Ptrofs.unsigned_repr.
-           simpl.
-           destruct (Z_le_gt_dec (4 * ptr + 4) (Integers.Ptrofs.unsigned OFFSET)); eauto.
-           right.
-           apply ZExtra.mod_0_bounds; try lia.
-           apply ZLib.Z_mod_mult'.
-           rewrite Z2Nat.id in H15; try lia.
-           apply Zmult_lt_compat_r with (p := 4) in H15; try lia.
-           rewrite ZLib.div_mul_undo in H15; try lia.
-           split; try lia.
-           apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia.
-      }
-
-      rewrite <- EXPR_OK.
-      rewrite PtrofsExtra.divu_unsigned; auto; try (unfold_constants; lia).
-      destruct (ptr ==Z Integers.Ptrofs.unsigned OFFSET / 4).
-      apply Z.mul_cancel_r with (p := 4) in e; try lia.
-      rewrite ZLib.div_mul_undo in e; try lia.
-      rewrite combine_lookup_first.
-      eapply H7; eauto.
-
-      rewrite <- array_set_len.
-      unfold arr_repeat. crush.
-      rewrite list_repeat_len. auto.
-      rewrite array_gso.
-      unfold array_get_error.
-      unfold arr_repeat.
-      crush.
-      apply list_repeat_lookup.
-      lia.
-      unfold_constants.
-      intro.
-      apply Z2Nat.inj_iff in H13; try lia.
-      apply Z.div_pos; try lia.
-      apply Integers.Ptrofs.unsigned_range.
-
-      assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
-      unfold arr_stack_based_pointers.
-      intros.
-      destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET).
-
-      crush.
-      erewrite Mem.load_store_same.
-      2: { rewrite ZERO.
-           rewrite Integers.Ptrofs.add_zero_l.
-           rewrite e.
-           rewrite Integers.Ptrofs.unsigned_repr.
-           exact H1.
-           apply Integers.Ptrofs.unsigned_range_2. }
-      crush.
-      destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; try constructor.
-      destruct (Archi.ptr64); try discriminate.
-      pose proof (RSBP src). rewrite EQ_SRC in H0.
-      assumption.
-
-      simpl.
-      erewrite Mem.load_store_other with (m1 := m).
-      2: { exact H1. }
-      2: { right.
-           rewrite ZERO.
-           rewrite Integers.Ptrofs.add_zero_l.
-           rewrite Integers.Ptrofs.unsigned_repr.
-           simpl.
-           destruct (Z_le_gt_dec (4 * ptr + 4) (Integers.Ptrofs.unsigned OFFSET)); eauto.
-           right.
-           apply ZExtra.mod_0_bounds; try lia.
-           apply ZLib.Z_mod_mult'.
-           invert H0.
-           apply Zmult_lt_compat_r with (p := 4) in H14; try lia.
-           rewrite ZLib.div_mul_undo in H14; try lia.
-           split; try lia.
-           apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia.
-      }
-      apply ASBP; assumption.
-
-      unfold stack_bounds in *. intros.
-      simpl.
-      assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
-      erewrite Mem.load_store_other with (m1 := m).
-      2: { exact H1. }
-      2: { right. right. simpl.
-           rewrite ZERO.
-           rewrite Integers.Ptrofs.add_zero_l.
-           rewrite Integers.Ptrofs.unsigned_repr; crush; try lia.
-           apply ZExtra.mod_0_bounds; crush; try lia. }
-      crush.
-      exploit (BOUNDS ptr); try lia. intros. crush.
-      exploit (BOUNDS ptr v); try lia. intros.
-      invert H0.
-      match goal with | |- ?x = _ => destruct x eqn:EQ end; try reflexivity.
-      assert (Mem.valid_access m AST.Mint32 sp'
-                               (Integers.Ptrofs.unsigned
-                                  (Integers.Ptrofs.add (Integers.Ptrofs.repr 0)
-                                                       (Integers.Ptrofs.repr ptr))) Writable).
-      { pose proof H1. eapply Mem.store_valid_access_2 in H0.
-        exact H0. eapply Mem.store_valid_access_3. eassumption. }
-      pose proof (Mem.valid_access_store m AST.Mint32 sp'
-                                         (Integers.Ptrofs.unsigned
-                                            (Integers.Ptrofs.add (Integers.Ptrofs.repr 0)
-                                                                 (Integers.Ptrofs.repr ptr))) v).
-      apply X in H0. invert H0. congruence.
-
-    + (** Preamble *)
-      invert MARR. crush.
-
-      unfold Op.eval_addressing in H0.
-      destruct (Archi.ptr64) eqn:ARCHI; crush.
-
-      unfold reg_stack_based_pointers in RSBP.
-      pose proof (RSBP r0) as RSBPr0.
-      pose proof (RSBP r1) as RSBPr1.
-
-      destruct (Registers.Regmap.get r0 rs) eqn:EQr0;
-      destruct (Registers.Regmap.get r1 rs) eqn:EQr1; crush.
-
-      rewrite ARCHI in H1. crush.
-      subst.
-      clear RSBPr1.
-
-      pose proof MASSOC as MASSOC'.
-      invert MASSOC'.
-      pose proof (H0 r0).
-      pose proof (H0 r1).
-      assert (HPler0 : Ple r0 (RTL.max_reg_function f))
-        by (eapply RTL.max_reg_function_use; eauto; crush; eauto).
-      assert (HPler1 : Ple r1 (RTL.max_reg_function f))
-        by (eapply RTL.max_reg_function_use; eauto; simpl; auto).
-      apply H6 in HPler0.
-      apply H8 in HPler1.
-      invert HPler0; invert HPler1; try congruence.
-      rewrite EQr0 in H9.
-      rewrite EQr1 in H11.
-      invert H9. invert H11.
-      clear H0. clear H6. clear H8.
-
-      unfold check_address_parameter_signed in *;
-      unfold check_address_parameter_unsigned in *; crush.
-
-      remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ asr # r0))
-                                    (Integers.Ptrofs.of_int
-                                       (Integers.Int.add (Integers.Int.mul (valueToInt asr # r1) (Integers.Int.repr z))
-                                                         (Integers.Int.repr z0)))) as OFFSET.
-
-      (** Modular preservation proof *)
-      assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE.
-      { rewrite HeqOFFSET.
-        apply PtrofsExtra.add_mod; crush; try lia.
-        rewrite Integers.Ptrofs.unsigned_repr_eq.
-        rewrite <- Zmod_div_mod; crush.
-        apply PtrofsExtra.of_int_mod.
-        apply IntExtra.add_mod; crush.
-        apply IntExtra.mul_mod2; crush.
-        rewrite Integers.Int.unsigned_repr_eq.
-        rewrite <- Zmod_div_mod; crush.
-        rewrite Integers.Int.unsigned_repr_eq.
-        rewrite <- Zmod_div_mod; crush. }
-
-      (** Write bounds proof *)
-      assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as WRITE_BOUND_HIGH.
-      { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; crush; auto.
-        unfold stack_bounds in BOUNDS.
-        exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET) (Registers.Regmap.get src rs)); auto.
-        split; try lia; apply Integers.Ptrofs.unsigned_range_2.
-        small_tac. }
-
-      (** Start of proof proper *)
-      eexists. split.
-      eapply Smallstep.plus_one.
-      eapply HTL.step_module; eauto.
-      apply assumption_32bit.
-      econstructor. econstructor. econstructor.
-      eapply Verilog.stmnt_runp_Vnonblock_arr. crush.
-      econstructor.
-      eapply Verilog.erun_Vbinop with (EQ := ?[EQ9]).
-      eapply Verilog.erun_Vbinop with (EQ := ?[EQ10]).
-      eapply Verilog.erun_Vbinop with (EQ := ?[EQ11]).
-      econstructor. econstructor. econstructor. econstructor.
-      econstructor.
-      eapply Verilog.erun_Vbinop with (EQ := ?[EQ12]).
-      econstructor. econstructor. econstructor. econstructor.
-      econstructor. econstructor. econstructor. econstructor.
-      econstructor. econstructor. econstructor. econstructor.
-
-      all: crush.
-
-      (** State Lookup *)
-      unfold Verilog.merge_regs.
-      crush.
-      unfold_merge.
-      apply AssocMap.gss.
-
-      (** Match states *)
-      rewrite assumption_32bit.
-      econstructor; eauto.
-
-      (** Match assocmaps *)
-      unfold Verilog.merge_regs. crush. unfold_merge.
-      apply regs_lessdef_add_greater.
-      unfold Plt; lia.
-      assumption.
-
-      (** States well formed *)
-      unfold state_st_wf. inversion 1. crush.
-      unfold Verilog.merge_regs.
-      unfold_merge.
-      apply AssocMap.gss.
-
-      (** Equality proof *)
-      assert (Z.to_nat
-                (Integers.Ptrofs.unsigned
-                   (Integers.Ptrofs.divu
-                      OFFSET
-                      (Integers.Ptrofs.repr 4)))
-              =
-              valueToNat (vdiv
-                            (vplus (vplus asr # r0 (ZToValue 32 z0) ?EQ11) (vmul asr # r1 (ZToValue 32 z) ?EQ12)
-                                   ?EQ10) (ZToValue 32 4) ?EQ9))
-        as EXPR_OK by admit.
-
-      assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
-      inversion MASSOC; revert HeqOFFSET; subst; clear MASSOC; intros HeqOFFSET.
-
-      econstructor.
-      repeat split; crush.
-      unfold HTL.empty_stack.
-      crush.
-      unfold Verilog.merge_arrs.
-
-      rewrite AssocMap.gcombine.
-      2: { reflexivity. }
-      unfold Verilog.arr_assocmap_set.
-      rewrite AssocMap.gss.
-      unfold Verilog.merge_arr.
-      rewrite AssocMap.gss.
-      setoid_rewrite H5.
-      reflexivity.
-
-      rewrite combine_length.
-      rewrite <- array_set_len.
-      unfold arr_repeat. crush.
-      apply list_repeat_len.
-
-      rewrite <- array_set_len.
-      unfold arr_repeat. crush.
-      rewrite list_repeat_len.
-      rewrite H4. reflexivity.
-
-      remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ asr # r0))
-                                    (Integers.Ptrofs.of_int
-                                       (Integers.Int.add (Integers.Int.mul (valueToInt asr # r1) (Integers.Int.repr z))
-                                                         (Integers.Int.repr z0)))) as OFFSET.
-      destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET).
-
-      erewrite Mem.load_store_same.
-      2: { rewrite ZERO.
-           rewrite Integers.Ptrofs.add_zero_l.
-           rewrite e.
-           rewrite Integers.Ptrofs.unsigned_repr.
-           exact H1.
-           apply Integers.Ptrofs.unsigned_range_2. }
-      constructor.
-      erewrite combine_lookup_second.
-      simpl.
-      assert (Ple src (RTL.max_reg_function f))
-        by (eapply RTL.max_reg_function_use; eauto; simpl; auto);
-      apply H0 in H16.
-      destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; invert H16; eauto.
-
-      rewrite <- array_set_len.
-      unfold arr_repeat. crush.
-      rewrite list_repeat_len. auto.
-
-      assert (4 * ptr / 4 = Integers.Ptrofs.unsigned OFFSET / 4) by (f_equal; assumption).
-      rewrite Z.mul_comm in H16.
-      rewrite Z_div_mult in H16; try lia.
-      replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) in H16 by reflexivity.
-      rewrite <- PtrofsExtra.divu_unsigned in H16; unfold_constants; try lia.
-      rewrite H16. rewrite EXPR_OK.
-      rewrite array_get_error_set_bound.
-      reflexivity.
-      unfold arr_length, arr_repeat. simpl.
-      rewrite list_repeat_len. lia.
-
-      erewrite Mem.load_store_other with (m1 := m).
-      2: { exact H1. }
-      2: { right.
-           rewrite ZERO.
-           rewrite Integers.Ptrofs.add_zero_l.
-           rewrite Integers.Ptrofs.unsigned_repr.
-           simpl.
-           destruct (Z_le_gt_dec (4 * ptr + 4) (Integers.Ptrofs.unsigned OFFSET)); eauto.
-           right.
-           apply ZExtra.mod_0_bounds; try lia.
-           apply ZLib.Z_mod_mult'.
-           rewrite Z2Nat.id in H18; try lia.
-           apply Zmult_lt_compat_r with (p := 4) in H18; try lia.
-           rewrite ZLib.div_mul_undo in H18; try lia.
-           split; try lia.
-           apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia.
-      }
-
-      rewrite <- EXPR_OK.
-      rewrite PtrofsExtra.divu_unsigned; auto; try (unfold_constants; lia).
-      destruct (ptr ==Z Integers.Ptrofs.unsigned OFFSET / 4).
-      apply Z.mul_cancel_r with (p := 4) in e; try lia.
-      rewrite ZLib.div_mul_undo in e; try lia.
-      rewrite combine_lookup_first.
-      eapply H7; eauto.
-
-      rewrite <- array_set_len.
-      unfold arr_repeat. crush.
-      rewrite list_repeat_len. auto.
-      rewrite array_gso.
-      unfold array_get_error.
-      unfold arr_repeat.
-      crush.
-      apply list_repeat_lookup.
-      lia.
-      unfold_constants.
-      intro.
-      apply Z2Nat.inj_iff in H16; try lia.
-      apply Z.div_pos; try lia.
-      apply Integers.Ptrofs.unsigned_range.
-
-      assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
-      unfold arr_stack_based_pointers.
-      intros.
-      destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET).
-
-      crush.
-      erewrite Mem.load_store_same.
-      2: { rewrite ZERO.
-           rewrite Integers.Ptrofs.add_zero_l.
-           rewrite e.
-           rewrite Integers.Ptrofs.unsigned_repr.
-           exact H1.
-           apply Integers.Ptrofs.unsigned_range_2. }
-      crush.
-      destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; try constructor.
-      destruct (Archi.ptr64); try discriminate.
-      pose proof (RSBP src). rewrite EQ_SRC in H0.
-      assumption.
-
-      simpl.
-      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 H17; try lia.
-           rewrite ZLib.div_mul_undo in H17; try lia.
-           split; try lia.
-           apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia.
-      }
-      apply ASBP; assumption.
-
-      unfold stack_bounds in *. intros.
-      simpl.
-      assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
-      erewrite Mem.load_store_other with (m1 := m).
-      2: { exact H1. }
-      2: { right. right. simpl.
-           rewrite ZERO.
-           rewrite Integers.Ptrofs.add_zero_l.
-           rewrite Integers.Ptrofs.unsigned_repr; crush; try lia.
-           apply ZExtra.mod_0_bounds; crush; try lia. }
-      crush.
-      exploit (BOUNDS ptr); try lia. intros. crush.
-      exploit (BOUNDS ptr v); try lia. intros.
-      invert H0.
-      match goal with | |- ?x = _ => destruct x eqn:EQ end; try reflexivity.
-      assert (Mem.valid_access m AST.Mint32 sp'
-                               (Integers.Ptrofs.unsigned
-                                  (Integers.Ptrofs.add (Integers.Ptrofs.repr 0)
-                                                       (Integers.Ptrofs.repr ptr))) Writable).
-      { pose proof H1. eapply Mem.store_valid_access_2 in H0.
-        exact H0. eapply Mem.store_valid_access_3. eassumption. }
-      pose proof (Mem.valid_access_store m AST.Mint32 sp'
-                                         (Integers.Ptrofs.unsigned
-                                            (Integers.Ptrofs.add (Integers.Ptrofs.repr 0)
-                                                                 (Integers.Ptrofs.repr ptr))) v).
-      apply X in H0. invert H0. congruence.
-
-    + invert MARR. crush.
-
-      unfold Op.eval_addressing in H0.
-      destruct (Archi.ptr64) eqn:ARCHI; crush.
-      rewrite ARCHI in H0. crush.
-
-      unfold check_address_parameter_unsigned in *;
-      unfold check_address_parameter_signed in *; crush.
-
-      assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
-      rewrite ZERO in H1. clear ZERO.
-      rewrite Integers.Ptrofs.add_zero_l in H1.
-
-      remember i0 as OFFSET.
-
-      (** Modular preservation proof *)
-      rename H0 into MOD_PRESERVE.
-
-      (** Write bounds proof *)
-      assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as WRITE_BOUND_HIGH.
-      { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; crush; auto.
-        unfold stack_bounds in BOUNDS.
-        exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET) (Registers.Regmap.get src rs)); auto.
-        crush.
-        replace (Integers.Ptrofs.repr 0) with (Integers.Ptrofs.zero) by reflexivity.
-        small_tac. }
-
-      (** Start of proof proper *)
-      eexists. split.
-      eapply Smallstep.plus_one.
-      eapply HTL.step_module; eauto.
-      apply assumption_32bit.
-      econstructor. econstructor. econstructor.
-      eapply Verilog.stmnt_runp_Vnonblock_arr. crush.
-      econstructor. econstructor. econstructor. econstructor.
-
-      all: crush.
-
-      (** State Lookup *)
-      unfold Verilog.merge_regs.
-      crush.
-      unfold_merge.
-      apply AssocMap.gss.
-
-      (** Match states *)
-      rewrite assumption_32bit.
-      econstructor; eauto.
-
-      (** Match assocmaps *)
-      unfold Verilog.merge_regs. crush. unfold_merge.
-      apply regs_lessdef_add_greater.
-      unfold Plt; lia.
-      assumption.
-
-      (** States well formed *)
-      unfold state_st_wf. inversion 1. crush.
-      unfold Verilog.merge_regs.
-      unfold_merge.
-      apply AssocMap.gss.
-
-      (** Equality proof *)
-      assert (Z.to_nat
-                (Integers.Ptrofs.unsigned
-                   (Integers.Ptrofs.divu
-                      OFFSET
-                      (Integers.Ptrofs.repr 4)))
-              =
-              valueToNat (ZToValue 32 (Integers.Ptrofs.unsigned OFFSET / 4)))
-        as EXPR_OK by admit.
-
-      assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
-      inversion MASSOC; revert HeqOFFSET; subst; clear MASSOC; intros HeqOFFSET.
-
-      econstructor.
-      repeat split; crush.
-      unfold HTL.empty_stack.
-      crush.
-      unfold Verilog.merge_arrs.
-
-      rewrite AssocMap.gcombine.
-      2: { reflexivity. }
-      unfold Verilog.arr_assocmap_set.
-      rewrite AssocMap.gss.
-      unfold Verilog.merge_arr.
-      rewrite AssocMap.gss.
-      setoid_rewrite H5.
-      reflexivity.
-
-      rewrite combine_length.
-      rewrite <- array_set_len.
-      unfold arr_repeat. crush.
-      apply list_repeat_len.
-
-      rewrite <- array_set_len.
-      unfold arr_repeat. crush.
-      rewrite list_repeat_len.
-      rewrite H4. reflexivity.
-
-      remember i0 as OFFSET.
-      destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET).
-
-      erewrite Mem.load_store_same.
-      2: { rewrite ZERO.
-           rewrite Integers.Ptrofs.add_zero_l.
-           rewrite e.
-           rewrite Integers.Ptrofs.unsigned_repr.
-           exact H1.
-           apply Integers.Ptrofs.unsigned_range_2. }
-      constructor.
-      erewrite combine_lookup_second.
-      simpl.
-      assert (Ple src (RTL.max_reg_function f))
-        by (eapply RTL.max_reg_function_use; eauto; simpl; auto);
-      apply H0 in H8.
-      destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; invert H8; eauto.
-
-      rewrite <- array_set_len.
-      unfold arr_repeat. crush.
-      rewrite list_repeat_len. auto.
-
-      assert (4 * ptr / 4 = Integers.Ptrofs.unsigned OFFSET / 4) by (f_equal; assumption).
-      rewrite Z.mul_comm in H8.
-      rewrite Z_div_mult in H8; try lia.
-      replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) in H8 by reflexivity.
-      rewrite <- PtrofsExtra.divu_unsigned in H8; unfold_constants; try lia.
-      rewrite H8. rewrite EXPR_OK.
-      rewrite array_get_error_set_bound.
-      reflexivity.
-      unfold arr_length, arr_repeat. simpl.
-      rewrite list_repeat_len. lia.
-
-      erewrite Mem.load_store_other with (m1 := m).
-      2: { exact H1. }
-      2: { right.
-           rewrite ZERO.
-           rewrite Integers.Ptrofs.add_zero_l.
-           rewrite Integers.Ptrofs.unsigned_repr.
-           simpl.
-           destruct (Z_le_gt_dec (4 * ptr + 4) (Integers.Ptrofs.unsigned OFFSET)); eauto.
-           right.
-           apply ZExtra.mod_0_bounds; try lia.
-           apply ZLib.Z_mod_mult'.
-           rewrite Z2Nat.id in H11; try lia.
-           apply Zmult_lt_compat_r with (p := 4) in H11; try lia.
-           rewrite ZLib.div_mul_undo in H11; try lia.
-           split; try lia.
-           apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia.
-      }
-
-      rewrite <- EXPR_OK.
-      rewrite PtrofsExtra.divu_unsigned; auto; try (unfold_constants; lia).
-      destruct (ptr ==Z Integers.Ptrofs.unsigned OFFSET / 4).
-      apply Z.mul_cancel_r with (p := 4) in e; try lia.
-      rewrite ZLib.div_mul_undo in e; try lia.
-      rewrite combine_lookup_first.
-      eapply H7; eauto.
-
-      rewrite <- array_set_len.
-      unfold arr_repeat. crush.
-      rewrite list_repeat_len. auto.
-      rewrite array_gso.
-      unfold array_get_error.
-      unfold arr_repeat.
-      crush.
-      apply list_repeat_lookup.
-      lia.
-      unfold_constants.
-      intro.
-      apply Z2Nat.inj_iff in H8; try lia.
-      apply Z.div_pos; try lia.
-      apply Integers.Ptrofs.unsigned_range.
-
-      assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
-      unfold arr_stack_based_pointers.
-      intros.
-      destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET).
-
-      crush.
-      erewrite Mem.load_store_same.
-      2: { rewrite ZERO.
-           rewrite Integers.Ptrofs.add_zero_l.
-           rewrite e.
-           rewrite Integers.Ptrofs.unsigned_repr.
-           exact H1.
-           apply Integers.Ptrofs.unsigned_range_2. }
-      crush.
-      destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; try constructor.
-      destruct (Archi.ptr64); try discriminate.
-      pose proof (RSBP src). rewrite EQ_SRC in H0.
-      assumption.
-
-      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 H9; try lia.
-           rewrite ZLib.div_mul_undo in H9; try lia.
-           split; try lia.
-           apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia.
-      }
-      apply ASBP; assumption.
-
-      unfold stack_bounds in *. intros.
-      simpl.
-      assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
-      erewrite Mem.load_store_other with (m1 := m).
-      2: { exact H1. }
-      2: { right. right. simpl.
-           rewrite ZERO.
-           rewrite Integers.Ptrofs.add_zero_l.
-           rewrite Integers.Ptrofs.unsigned_repr; crush; try lia.
-           apply ZExtra.mod_0_bounds; crush; try lia. }
-      crush.
-      exploit (BOUNDS ptr); try lia. intros. crush.
-      exploit (BOUNDS ptr v); try lia. intros.
-      invert H0.
-      match goal with | |- ?x = _ => destruct x eqn:EQ end; try reflexivity.
-      assert (Mem.valid_access m AST.Mint32 sp'
-                               (Integers.Ptrofs.unsigned
-                                  (Integers.Ptrofs.add (Integers.Ptrofs.repr 0)
-                                                       (Integers.Ptrofs.repr ptr))) Writable).
-      { pose proof H1. eapply Mem.store_valid_access_2 in H0.
-        exact H0. eapply Mem.store_valid_access_3. eassumption. }
-      pose proof (Mem.valid_access_store m AST.Mint32 sp'
-                                         (Integers.Ptrofs.unsigned
-                                            (Integers.Ptrofs.add (Integers.Ptrofs.repr 0)
-                                                                 (Integers.Ptrofs.repr ptr))) v).
-      apply X in H0. invert H0. congruence.
-  Admitted.
-  Hint Resolve transl_istore_correct : htlproof.
-
-  Lemma transl_icond_correct:
-    forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive)
-      (rs : Registers.Regmap.t Values.val) (m : mem) (cond : Op.condition) (args : list Registers.reg)
-      (ifso ifnot : RTL.node) (b : bool) (pc' : RTL.node),
-      (RTL.fn_code f) ! pc = Some (RTL.Icond cond args ifso ifnot) ->
-      Op.eval_condition cond (map (fun r : positive => Registers.Regmap.get r rs) args) m = Some b ->
-      pc' = (if b then ifso else ifnot) ->
-      forall R1 : HTL.state,
-        match_states (RTL.State s f sp pc rs m) R1 ->
-        exists R2 : HTL.state,
-          Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ match_states (RTL.State s f sp pc' rs m) R2.
-  Proof.
-    intros s f sp pc rs m cond args ifso ifnot b pc' H H0 H1 R1 MSTATE.
-    inv_state.
-
-    eexists. split. apply Smallstep.plus_one.
-    eapply HTL.step_module; eauto.
-    apply assumption_32bit.
-    eapply Verilog.stmnt_runp_Vnonblock_reg with
-        (rhsval := if b then posToValue 32 ifso else posToValue 32 ifnot).
-    constructor.
-
-    simpl.
-    destruct b.
-    eapply Verilog.erun_Vternary_true.
-    eapply eval_cond_correct; eauto.
-    constructor.
-    apply boolToValue_ValueToBool.
-    eapply Verilog.erun_Vternary_false.
-    eapply eval_cond_correct; eauto.
-    constructor.
-    apply boolToValue_ValueToBool.
-    constructor.
-
-    big_tac.
-
-    invert MARR.
-    destruct b; rewrite assumption_32bit; big_tac.
-
-    Unshelve.
-    constructor.
-  Qed.
-  Hint Resolve transl_icond_correct : htlproof.
-
-  Lemma transl_ijumptable_correct:
-    forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive)
-      (rs : Registers.Regmap.t Values.val) (m : mem) (arg : Registers.reg) (tbl : list RTL.node)
-      (n : Integers.Int.int) (pc' : RTL.node),
-      (RTL.fn_code f) ! pc = Some (RTL.Ijumptable arg tbl) ->
-      Registers.Regmap.get arg rs = Values.Vint n ->
-      list_nth_z tbl (Integers.Int.unsigned n) = Some pc' ->
-      forall R1 : HTL.state,
-        match_states (RTL.State s f sp pc rs m) R1 ->
-        exists R2 : HTL.state,
-          Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ match_states (RTL.State s f sp pc' rs m) R2.
-  Proof.
-    intros s f sp pc rs m arg tbl n pc' H H0 H1 R1 MSTATE.
-  Admitted.
-  Hint Resolve transl_ijumptable_correct : htlproof.
-
-  Lemma transl_ireturn_correct:
-    forall (s : list RTL.stackframe) (f : RTL.function) (stk : Values.block)
-      (pc : positive) (rs : RTL.regset) (m : mem) (or : option Registers.reg)
-      (m' : mem),
-      (RTL.fn_code f) ! pc = Some (RTL.Ireturn or) ->
-      Mem.free m stk 0 (RTL.fn_stacksize f) = Some m' ->
-      forall R1 : HTL.state,
-        match_states (RTL.State s f (Values.Vptr stk Integers.Ptrofs.zero) pc rs m) R1 ->
-        exists R2 : HTL.state,
-          Smallstep.plus HTL.step tge R1 Events.E0 R2 /\
-          match_states (RTL.Returnstate s (Registers.regmap_optget or Values.Vundef rs) m') R2.
-  Proof.
-    intros s f stk pc rs m or m' H H0 R1 MSTATE.
-    inv_state.
-
-    - econstructor. split.
-      eapply Smallstep.plus_two.
-
-      eapply HTL.step_module; eauto.
-      apply assumption_32bit.
-      constructor.
-      econstructor; simpl; trivial.
-      econstructor; simpl; trivial.
-      constructor.
-      econstructor; simpl; trivial.
-      constructor.
-
-      constructor. constructor.
-
-      unfold state_st_wf in WF; big_tac; eauto.
-
-      apply HTL.step_finish.
-      unfold Verilog.merge_regs.
-      unfold_merge; simpl.
-      rewrite AssocMap.gso.
-      apply AssocMap.gss. lia.
-      apply AssocMap.gss.
-      rewrite Events.E0_left. reflexivity.
-
-      constructor; auto.
-      constructor.
-
-    (* FIXME: Duplication *)
-    - econstructor. split.
-      eapply Smallstep.plus_two.
-      eapply HTL.step_module; eauto.
-      apply assumption_32bit.
-      constructor.
-      econstructor; simpl; trivial.
-      econstructor; simpl; trivial.
-      constructor. constructor. constructor.
-      constructor. constructor. constructor.
-
-      unfold state_st_wf in WF; big_tac; eauto.
-
-      apply HTL.step_finish.
-      unfold Verilog.merge_regs.
-      unfold_merge.
-      rewrite AssocMap.gso.
-      apply AssocMap.gss. simpl; lia.
-      apply AssocMap.gss.
-      rewrite Events.E0_left. trivial.
-
-      constructor; auto.
-
-      simpl. inversion MASSOC. subst.
-      unfold find_assocmap, AssocMapExt.get_default. rewrite AssocMap.gso.
-      apply H1. eapply RTL.max_reg_function_use. eauto. simpl; tauto.
-      assert (HPle : Ple r (RTL.max_reg_function f)).
-      eapply RTL.max_reg_function_use. eassumption. simpl; auto.
-      apply ZExtra.Ple_not_eq. apply ZExtra.Ple_Plt_Succ. assumption.
-
-      Unshelve.
-      all: constructor.
-  Qed.
-  Hint Resolve transl_ireturn_correct : htlproof.
-
-  Lemma transl_callstate_correct:
-    forall (s : list RTL.stackframe) (f : RTL.function) (args : list Values.val)
-      (m : mem) (m' : Mem.mem') (stk : Values.block),
-      Mem.alloc m 0 (RTL.fn_stacksize f) = (m', stk) ->
-      forall R1 : HTL.state,
-        match_states (RTL.Callstate s (AST.Internal f) args m) R1 ->
-        exists R2 : HTL.state,
-          Smallstep.plus HTL.step tge R1 Events.E0 R2 /\
-          match_states
-            (RTL.State s f (Values.Vptr stk Integers.Ptrofs.zero) (RTL.fn_entrypoint f)
-                       (RTL.init_regs args (RTL.fn_params f)) m') R2.
-  Proof.
-    intros s f args m m' stk H R1 MSTATE.
-
-    inversion MSTATE; subst. inversion TF; subst.
-    econstructor. split. apply Smallstep.plus_one.
-    eapply HTL.step_call. crush.
-
-    apply match_state with (sp' := stk); eauto.
-
-    all: big_tac.
-
-    apply regs_lessdef_add_greater.
-    unfold Plt; lia.
-    apply init_reg_assoc_empty.
-
-    constructor.
-
-    destruct (Mem.load AST.Mint32 m' stk
-                       (Integers.Ptrofs.unsigned (Integers.Ptrofs.add
-                                                    Integers.Ptrofs.zero
-                                                    (Integers.Ptrofs.repr (4 * ptr))))) eqn:LOAD.
-    pose proof Mem.load_alloc_same as LOAD_ALLOC.
-    pose proof H as ALLOC.
-    eapply LOAD_ALLOC in ALLOC.
-    2: { exact LOAD. }
-    ptrofs. rewrite LOAD.
-    rewrite ALLOC.
-    repeat constructor.
-
-    ptrofs. rewrite LOAD.
-    repeat constructor.
-
-    unfold reg_stack_based_pointers. intros.
-    unfold RTL.init_regs; crush.
-    destruct (RTL.fn_params f);
-    rewrite Registers.Regmap.gi; constructor.
-
-    unfold arr_stack_based_pointers. intros.
-    crush.
-    destruct (Mem.load AST.Mint32 m' stk
-                       (Integers.Ptrofs.unsigned (Integers.Ptrofs.add
-                                                    Integers.Ptrofs.zero
-                                                    (Integers.Ptrofs.repr (4 * ptr))))) eqn:LOAD.
-    pose proof Mem.load_alloc_same as LOAD_ALLOC.
-    pose proof H as ALLOC.
-    eapply LOAD_ALLOC in ALLOC.
-    2: { exact LOAD. }
-    rewrite ALLOC.
-    repeat constructor.
-    constructor.
-
-    Transparent Mem.alloc. (* TODO: Since there are opaque there's probably a lemma. *)
-    Transparent Mem.load.
-    Transparent Mem.store.
-    unfold stack_bounds.
-    split.
-
-    unfold Mem.alloc in H.
-    invert H.
-    crush.
-    unfold Mem.load.
-    intros.
-    match goal with | |- context[if ?x then _ else _] => destruct x end; try congruence.
-    invert v0. unfold Mem.range_perm in H4.
-    unfold Mem.perm in H4. crush.
-    unfold Mem.perm_order' in H4.
-    small_tac.
-    exploit (H4 ptr). rewrite Integers.Ptrofs.unsigned_repr; small_tac. intros.
-    rewrite Maps.PMap.gss in H8.
-    match goal with | H8 : context[if ?x then _ else _] |- _ => destruct x eqn:EQ end; try contradiction.
-    crush.
-    apply proj_sumbool_true in H10. lia.
-
-    unfold Mem.alloc in H.
-    invert H.
-    crush.
-    unfold Mem.store.
-    intros.
-    match goal with | |- context[if ?x then _ else _] => destruct x end; try congruence.
-    invert v0. unfold Mem.range_perm in H4.
-    unfold Mem.perm in H4. crush.
-    unfold Mem.perm_order' in H4.
-    small_tac.
-    exploit (H4 ptr). rewrite Integers.Ptrofs.unsigned_repr; small_tac. intros.
-    rewrite Maps.PMap.gss in H8.
-    match goal with | H8 : context[if ?x then _ else _] |- _ => destruct x eqn:EQ end; try contradiction.
-    crush.
-    apply proj_sumbool_true in H10. lia.
-    Opaque Mem.alloc.
-    Opaque Mem.load.
-    Opaque Mem.store.
-  Qed.
-  Hint Resolve transl_callstate_correct : htlproof.
-
-  Lemma transl_returnstate_correct:
-    forall (res0 : Registers.reg) (f : RTL.function) (sp : Values.val) (pc : RTL.node)
-      (rs : RTL.regset) (s : list RTL.stackframe) (vres : Values.val) (m : mem)
-      (R1 : HTL.state),
-      match_states (RTL.Returnstate (RTL.Stackframe res0 f sp pc rs :: s) vres m) R1 ->
-      exists R2 : HTL.state,
-        Smallstep.plus HTL.step tge R1 Events.E0 R2 /\
-        match_states (RTL.State s f sp pc (Registers.Regmap.set res0 vres rs) m) R2.
-  Proof.
-    intros res0 f sp pc rs s vres m R1 MSTATE.
-    inversion MSTATE. inversion MF.
-  Qed.
-  Hint Resolve transl_returnstate_correct : htlproof.
-
-  Lemma option_inv :
-    forall A x y,
-      @Some A x = Some y -> x = y.
-  Proof. intros. inversion H. trivial. Qed.
-
-  Lemma main_tprog_internal :
-    forall b,
-      Globalenvs.Genv.find_symbol tge tprog.(AST.prog_main) = Some b ->
-      exists f, Genv.find_funct_ptr (Genv.globalenv tprog) b = Some (AST.Internal f).
-  Proof.
-    intros.
-    destruct TRANSL. unfold main_is_internal in H1.
-    repeat (unfold_match H1). replace b with b0.
-    exploit function_ptr_translated; eauto. intros [tf [A B]].
-    unfold transl_fundef, AST.transf_partial_fundef, Errors.bind in B.
-    unfold_match B. inv B. econstructor. apply A.
-
-    apply option_inv. rewrite <- Heqo. rewrite <- H.
-    rewrite symbols_preserved. replace (AST.prog_main tprog) with (AST.prog_main prog).
-    trivial. symmetry; eapply Linking.match_program_main; eauto.
-  Qed.
-
-  Lemma transl_initial_states :
-    forall s1 : Smallstep.state (RTL.semantics prog),
-      Smallstep.initial_state (RTL.semantics prog) s1 ->
-      exists s2 : Smallstep.state (HTL.semantics tprog),
-        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.
-    replace (AST.prog_main tprog) with (AST.prog_main prog).
-    rewrite symbols_preserved; eauto.
-    symmetry; eapply Linking.match_program_main; eauto.
-    apply H6.
-
-    constructor.
-    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 :
-    forall (s1 : Smallstep.state (RTL.semantics prog))
-           (s2 : Smallstep.state (HTL.semantics tprog))
-           (r : Integers.Int.int),
-      match_states s1 s2 ->
-      Smallstep.final_state (RTL.semantics prog) s1 r ->
-      Smallstep.final_state (HTL.semantics tprog) s2 r.
-  Proof.
-    intros. inv H0. inv H. inv H4. invert MF. constructor. reflexivity.
-  Qed.
-  Hint Resolve transl_final_states : htlproof.
-
-  Theorem transl_step_correct:
-    forall (S1 : RTL.state) t S2,
-      RTL.step ge S1 t S2 ->
-      forall (R1 : HTL.state),
-        match_states S1 R1 ->
-        exists R2, Smallstep.plus HTL.step tge R1 t R2 /\ match_states S2 R2.
-  Proof.
-    induction 1; eauto with htlproof; (intros; inv_state).
-  Qed.
-  Hint Resolve transl_step_correct : htlproof.
-
-  Theorem transf_program_correct:
-    Smallstep.forward_simulation (RTL.semantics prog) (HTL.semantics tprog).
-  Proof.
-    eapply Smallstep.forward_simulation_plus; eauto with htlproof.
-    apply senv_preserved.
-  Qed.
-
-End CORRECTNESS.
+(* Inductive match_assocmaps : RTL.function -> RTL.regset -> assocmap -> Prop := *)
+(*   match_assocmap : forall f rs am, *)
+(*     (forall r, Ple r (RTL.max_reg_function f) -> *)
+(*                val_value_lessdef (Registers.Regmap.get r rs) am#r) -> *)
+(*     match_assocmaps f rs am. *)
+(* Hint Constructors match_assocmaps : htlproof. *)
+
+(* Definition state_st_wf (m : HTL.module) (s : HTL.state) := *)
+(*   forall st asa asr res, *)
+(*   s = HTL.State res m st asa asr -> *)
+(*   asa!(m.(HTL.mod_st)) = Some (posToValue st). *)
+(* Hint Unfold state_st_wf : htlproof. *)
+
+(* 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 0) *)
+(*                                  (Option.join (array_get_error (Z.to_nat ptr) stack)))) -> *)
+(*     match_arrs m f sp mem asa. *)
+
+(* Definition stack_based (v : Values.val) (sp : Values.block) : Prop := *)
+(*    match v with *)
+(*    | Values.Vptr sp' off => sp' = sp *)
+(*    | _ => True *)
+(*    end. *)
+
+(* Definition reg_stack_based_pointers (sp : Values.block) (rs : Registers.Regmap.t Values.val) : Prop := *)
+(*   forall r, stack_based (Registers.Regmap.get r rs) sp. *)
+
+(* Definition arr_stack_based_pointers (spb : Values.block) (m : mem) (stack_length : Z) *)
+(*   (sp : Values.val) : Prop := *)
+(*   forall ptr, *)
+(*     0 <= ptr < (stack_length / 4) -> *)
+(*     stack_based (Option.default *)
+(*                    Values.Vundef *)
+(*                    (Mem.loadv AST.Mint32 m *)
+(*                               (Values.Val.offset_ptr sp (Integers.Ptrofs.repr (4 * ptr))))) *)
+(*                 spb. *)
+
+(* Definition stack_bounds (sp : Values.val) (hi : Z) (m : mem) : Prop := *)
+(*   forall ptr v, *)
+(*     hi <= ptr <= Integers.Ptrofs.max_unsigned -> *)
+(*     Z.modulo ptr 4 = 0 -> *)
+(*     Mem.loadv AST.Mint32 m (Values.Val.offset_ptr sp (Integers.Ptrofs.repr ptr )) = None /\ *)
+(*     Mem.storev AST.Mint32 m (Values.Val.offset_ptr sp (Integers.Ptrofs.repr ptr )) v = None. *)
+
+(* Inductive match_frames : list RTL.stackframe -> list HTL.stackframe -> Prop := *)
+(* | match_frames_nil : *)
+(*     match_frames nil nil. *)
+
+(*   Lemma assumption_32bit : *)
+(*     forall v, *)
+(*       valueToPos (posToValue v) = v. *)
+(*   Proof. *)
+(*   Admitted. *)
+
+(* Inductive match_states : RTL.state -> HTL.state -> Prop := *)
+(* | 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)) *)
+(*     (MF : match_frames sf res) *)
+(*     (MARR : match_arrs m f sp mem asa) *)
+(*     (SP : sp = Values.Vptr sp' (Integers.Ptrofs.repr 0)) *)
+(*     (RSBP : reg_stack_based_pointers sp' rs) *)
+(*     (ASBP : arr_stack_based_pointers sp' mem (f.(RTL.fn_stacksize)) sp) *)
+(*     (BOUNDS : stack_bounds sp (f.(RTL.fn_stacksize)) mem), *)
+(*     match_states (RTL.State sf f sp st rs mem) *)
+(*                  (HTL.State res m st asr asa) *)
+(* | match_returnstate : *)
+(*     forall *)
+(*       v v' stack mem res *)
+(*       (MF : match_frames stack res), *)
+(*       val_value_lessdef v v' -> *)
+(*       match_states (RTL.Returnstate stack v mem) (HTL.Returnstate res v') *)
+(* | match_initial_call : *)
+(*     forall f m m0 *)
+(*     (TF : tr_module f m), *)
+(*       match_states (RTL.Callstate nil (AST.Internal f) nil m0) (HTL.Callstate nil m nil). *)
+(* 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 /\ *)
+(*   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. 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 : *)
+(*   forall f rs1 rs2 n v, *)
+(*     Plt (RTL.max_reg_function f) n -> *)
+(*     match_assocmaps f rs1 rs2 -> *)
+(*     match_assocmaps f rs1 (AssocMap.set n v rs2). *)
+(* Proof. *)
+(*   inversion 2; subst. *)
+(*   intros. constructor. *)
+(*   intros. unfold find_assocmap. unfold AssocMapExt.get_default. *)
+(*   rewrite AssocMap.gso. eauto. *)
+(*   apply Pos.le_lt_trans with _ _ n in H2. *)
+(*   unfold not. intros. subst. eapply Pos.lt_irrefl. eassumption. assumption. *)
+(* Qed. *)
+(* Hint Resolve regs_lessdef_add_greater : htlproof. *)
+
+(* Lemma regs_lessdef_add_match : *)
+(*   forall f rs am r v v', *)
+(*     val_value_lessdef v v' -> *)
+(*     match_assocmaps f rs am -> *)
+(*     match_assocmaps f (Registers.Regmap.set r v rs) (AssocMap.set r v' am). *)
+(* Proof. *)
+(*   inversion 2; subst. *)
+(*   constructor. intros. *)
+(*   destruct (peq r0 r); subst. *)
+(*   rewrite Registers.Regmap.gss. *)
+(*   unfold find_assocmap. unfold AssocMapExt.get_default. *)
+(*   rewrite AssocMap.gss. assumption. *)
+
+(*   rewrite Registers.Regmap.gso; try assumption. *)
+(*   unfold find_assocmap. unfold AssocMapExt.get_default. *)
+(*   rewrite AssocMap.gso; eauto. *)
+(* Qed. *)
+(* Hint Resolve regs_lessdef_add_match : htlproof. *)
+
+(* Lemma list_combine_none : *)
+(*   forall n l, *)
+(*     length l = n -> *)
+(*     list_combine Verilog.merge_cell (list_repeat None n) l = l. *)
+(* Proof. *)
+(*   induction n; intros; crush. *)
+(*   - symmetry. apply length_zero_iff_nil. auto. *)
+(*   - destruct l; crush. *)
+(*     rewrite list_repeat_cons. *)
+(*     crush. f_equal. *)
+(*     eauto. *)
+(* Qed. *)
+
+(* Lemma combine_none : *)
+(*   forall n a, *)
+(*     a.(arr_length) = n -> *)
+(*     arr_contents (combine Verilog.merge_cell (arr_repeat None n) a) = arr_contents a. *)
+(* Proof. *)
+(*   intros. *)
+(*   unfold combine. *)
+(*   crush. *)
+
+(*   rewrite <- (arr_wf a) in H. *)
+(*   apply list_combine_none. *)
+(*   assumption. *)
+(* Qed. *)
+
+(* Lemma list_combine_lookup_first : *)
+(*   forall l1 l2 n, *)
+(*     length l1 = length l2 -> *)
+(*     nth_error l1 n = Some None -> *)
+(*     nth_error (list_combine Verilog.merge_cell l1 l2) n = nth_error l2 n. *)
+(* Proof. *)
+(*   induction l1; intros; crush. *)
+
+(*   rewrite nth_error_nil in H0. *)
+(*   discriminate. *)
+
+(*   destruct l2 eqn:EQl2. crush. *)
+(*   simpl in H. invert H. *)
+(*   destruct n; simpl in *. *)
+(*   invert H0. simpl. reflexivity. *)
+(*   eauto. *)
+(* Qed. *)
+
+(* Lemma combine_lookup_first : *)
+(*   forall a1 a2 n, *)
+(*     a1.(arr_length) = a2.(arr_length) -> *)
+(*     array_get_error n a1 = Some None -> *)
+(*     array_get_error n (combine Verilog.merge_cell a1 a2) = array_get_error n a2. *)
+(* Proof. *)
+(*   intros. *)
+
+(*   unfold array_get_error in *. *)
+(*   apply list_combine_lookup_first; eauto. *)
+(*   rewrite a1.(arr_wf). rewrite a2.(arr_wf). *)
+(*   assumption. *)
+(* Qed. *)
+
+(* Lemma list_combine_lookup_second : *)
+(*   forall l1 l2 n x, *)
+(*     length l1 = length l2 -> *)
+(*     nth_error l1 n = Some (Some x) -> *)
+(*     nth_error (list_combine Verilog.merge_cell l1 l2) n = Some (Some x). *)
+(* Proof. *)
+(*   induction l1; intros; crush; auto. *)
+
+(*   destruct l2 eqn:EQl2. crush. *)
+(*   simpl in H. invert H. *)
+(*   destruct n; simpl in *. *)
+(*   invert H0. simpl. reflexivity. *)
+(*   eauto. *)
+(* Qed. *)
+
+(* Lemma combine_lookup_second : *)
+(*   forall a1 a2 n x, *)
+(*     a1.(arr_length) = a2.(arr_length) -> *)
+(*     array_get_error n a1 = Some (Some x) -> *)
+(*     array_get_error n (combine Verilog.merge_cell a1 a2) = Some (Some x). *)
+(* Proof. *)
+(*   intros. *)
+
+(*   unfold array_get_error in *. *)
+(*   apply list_combine_lookup_second; eauto. *)
+(*   rewrite a1.(arr_wf). rewrite a2.(arr_wf). *)
+(*   assumption. *)
+(* Qed. *)
+
+(* Ltac inv_state := *)
+(*   match goal with *)
+(*     MSTATE : match_states _ _ |- _ => *)
+(*     inversion MSTATE; *)
+(*     match goal with *)
+(*       TF : tr_module _ _ |- _ => *)
+(*       inversion TF; *)
+(*       match goal with *)
+(*         TC : forall _ _, *)
+(*           Maps.PTree.get _ _ = Some _ -> tr_code _ _ _ _ _ _ _ _ _, *)
+(*         H : Maps.PTree.get _ _ = Some _ |- _ => *)
+(*         apply TC in H; inversion H; *)
+(*         match goal with *)
+(*           TI : context[tr_instr] |- _ => *)
+(*           inversion TI *)
+(*         end *)
+(*       end *)
+(*     end *)
+(* end; subst. *)
+
+(* Ltac unfold_func H := *)
+(*   match type of H with *)
+(*   | ?f = _ => unfold f in H; repeat (unfold_match H) *)
+(*   | ?f _ = _ => unfold f in H; repeat (unfold_match H) *)
+(*   | ?f _ _ = _ => unfold f in H; repeat (unfold_match H) *)
+(*   | ?f _ _ _ = _ => unfold f in H; repeat (unfold_match H) *)
+(*   | ?f _ _ _ _ = _ => unfold f in H; repeat (unfold_match H) *)
+(*   end. *)
+
+(* Lemma init_reg_assoc_empty : *)
+(*   forall f l, *)
+(*     match_assocmaps f (RTL.init_regs nil l) (HTL.init_regs nil l). *)
+(* Proof. *)
+(*   induction l; simpl; constructor; intros. *)
+(*   - rewrite Registers.Regmap.gi. unfold find_assocmap. *)
+(*     unfold AssocMapExt.get_default. rewrite AssocMap.gempty. *)
+(*     constructor. *)
+
+(*   - rewrite Registers.Regmap.gi. unfold find_assocmap. *)
+(*     unfold AssocMapExt.get_default. rewrite AssocMap.gempty. *)
+(*     constructor. *)
+(* Qed. *)
+
+(* Lemma arr_lookup_some: *)
+(*   forall (z : Z) (r0 : Registers.reg) (r : Verilog.reg) (asr : assocmap) (asa : Verilog.assocmap_arr) *)
+(*     (stack : Array (option value)) (H5 : asa ! r = Some stack) n, *)
+(*     exists x, Verilog.arr_assocmap_lookup asa r n = Some x. *)
+(* Proof. *)
+(*   intros z r0 r asr asa stack H5 n. *)
+(*   eexists. *)
+(*   unfold Verilog.arr_assocmap_lookup. rewrite H5. reflexivity. *)
+(* Qed. *)
+(* Hint Resolve arr_lookup_some : htlproof. *)
+
+(* Section CORRECTNESS. *)
+
+(*   Variable prog : RTL.program. *)
+(*   Variable tprog : HTL.program. *)
+
+(*   Hypothesis TRANSL : match_prog prog tprog. *)
+
+(*   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. intros. eapply (Genv.find_symbol_match TRANSL'). Qed. *)
+
+(*   Lemma function_ptr_translated: *)
+(*     forall (b: Values.block) (f: RTL.fundef), *)
+(*       Genv.find_funct_ptr ge b = Some f -> *)
+(*       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 (cu & tf & P & Q & R); exists tf; auto. *)
+(*   Qed. *)
+
+(*   Lemma functions_translated: *)
+(*     forall (v: Values.val) (f: RTL.fundef), *)
+(*       Genv.find_funct ge v = Some f -> *)
+(*       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 (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'). *)
+(*   Hint Resolve senv_preserved : htlproof. *)
+
+(*   Lemma ptrofs_inj : *)
+(*     forall a b, *)
+(*       Ptrofs.unsigned a = Ptrofs.unsigned b -> a = b. *)
+(*   Proof. *)
+(*     intros. rewrite <- Ptrofs.repr_unsigned. symmetry. rewrite <- Ptrofs.repr_unsigned. *)
+(*     rewrite H. auto. *)
+(*   Qed. *)
+
+(*   Lemma eval_correct : *)
+(*     forall s sp op rs m v e asr asa f f' stk s' i pc res0 pc' args res ml st, *)
+(*       match_states (RTL.State stk f sp pc rs m) (HTL.State res ml st asr asa) -> *)
+(*       (RTL.fn_code f) ! pc = Some (RTL.Iop op args res0 pc') -> *)
+(*       Op.eval_operation ge sp op *)
+(*                         (List.map (fun r : BinNums.positive => Registers.Regmap.get r rs) args) m = Some v -> *)
+(*       translate_instr op args s = OK e s' i -> *)
+(*       exists v', Verilog.expr_runp f' asr asa e v' /\ val_value_lessdef v v'. *)
+(*   Proof. *)
+(*     intros s sp op rs m v e asr asa f f' stk s' i pc pc' res0 args res ml st MSTATE INSTR EVAL TR_INSTR. *)
+(*     inv MSTATE. inv MASSOC. unfold translate_instr in TR_INSTR; repeat (unfold_match TR_INSTR); inv TR_INSTR; *)
+(*     unfold Op.eval_operation in EVAL; repeat (unfold_match EVAL); simplify. *)
+(*     - inv Heql. *)
+(*       assert (HPle : Ple r (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto). *)
+(*       apply H in HPle. eexists. split; try constructor; eauto. *)
+(*     - eexists. split. constructor. constructor. auto. *)
+(*     - inv Heql. *)
+(*       assert (HPle : Ple r (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto). *)
+(*       apply H in HPle. *)
+(*       eexists. split. econstructor; eauto. constructor. trivial. *)
+(*       unfold Verilog.unop_run. unfold Values.Val.neg. destruct (Registers.Regmap.get r rs) eqn:?; constructor. *)
+(*       inv HPle. auto. *)
+(*     - inv Heql. *)
+(*       assert (HPle : Ple r (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto). *)
+(*       assert (HPle0 : Ple r0 (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto). *)
+(*       apply H in HPle. apply H in HPle0. *)
+(*       eexists. split. econstructor; eauto. constructor. trivial. *)
+(*       constructor. trivial. simplify. inv HPle. inv HPle0; constructor; auto. *)
+(*       + inv HPle0. constructor. unfold valueToPtr. Search Integers.Ptrofs.sub Integers.int. *)
+(*         pose proof Integers.Ptrofs.agree32_sub. unfold Integers.Ptrofs.agree32 in H3. *)
+(*         Print Integers.Ptrofs.agree32. unfold Ptrofs.of_int. simpl. *)
+(*         apply ptrofs_inj. assert (Archi.ptr64 = false) by auto. eapply H3 in H4. *)
+(*         rewrite Ptrofs.unsigned_repr. apply H4. replace Ptrofs.max_unsigned with Int.max_unsigned; auto. *)
+(*         apply Int.unsigned_range_2. *)
+(*         auto. rewrite Ptrofs.unsigned_repr. replace Ptrofs.max_unsigned with Int.max_unsigned; auto. *)
+(*         apply Int.unsigned_range_2. rewrite Ptrofs.unsigned_repr. auto. *)
+(*         replace Ptrofs.max_unsigned with Int.max_unsigned; auto. *)
+(*         apply Int.unsigned_range_2. *)
+(*         Admitted. *)
+
+(*   Lemma eval_cond_correct : *)
+(*     forall cond (args : list Registers.reg) s1 c s' i rs args m b f asr asa, *)
+(*       translate_condition cond args s1 = OK c s' i -> *)
+(*       Op.eval_condition *)
+(*         cond *)
+(*         (List.map (fun r : BinNums.positive => Registers.Regmap.get r rs) args) *)
+(*         m = Some b -> *)
+(*       Verilog.expr_runp f asr asa c (boolToValue b). *)
+(*   Admitted. *)
+
+(*   (** The proof of semantic preservation for the translation of instructions *)
+(*       is a simulation argument based on diagrams of the following form: *)
+(* << *)
+(*                       match_states *)
+(*     code st rs ---------------- State m st assoc *)
+(*          ||                             | *)
+(*          ||                             | *)
+(*          ||                             | *)
+(*          \/                             v *)
+(*     code st rs' --------------- State m st assoc' *)
+(*                       match_states *)
+(* >> *)
+(*       where [tr_code c data control fin rtrn st] is assumed to hold. *)
+
+(*       The precondition and postcondition is that that should hold is [match_assocmaps rs assoc]. *)
+(*    *) *)
+
+(*   Definition transl_instr_prop (instr : RTL.instruction) : Prop := *)
+(*     forall m asr asa fin rtrn st stmt trans res, *)
+(*       tr_instr fin rtrn st (m.(HTL.mod_stk)) instr stmt trans -> *)
+(*       exists asr' asa', *)
+(*         HTL.step tge (HTL.State res m st asr asa) Events.E0 (HTL.State res m st asr' asa'). *)
+
+(*   Opaque combine. *)
+
+(*   Ltac tac0 := *)
+(*     match goal with *)
+(*     | [ |- context[valueToPos (posToValue _)] ] => rewrite assumption_32bit *)
+
+(*     | [ |- context[Verilog.merge_arrs _ _] ] => unfold Verilog.merge_arrs *)
+(*     | [ |- context[Verilog.merge_arr] ] => unfold Verilog.merge_arr *)
+(*     | [ |- context[Verilog.merge_regs _ _] ] => unfold Verilog.merge_regs; crush; unfold_merge *)
+(*     | [ |- context[reg_stack_based_pointers] ] => unfold reg_stack_based_pointers; intros *)
+(*     | [ |- context[Verilog.arr_assocmap_set _ _ _ _] ] => unfold Verilog.arr_assocmap_set *)
+
+(*     | [ |- context[HTL.empty_stack] ] => unfold HTL.empty_stack *)
+
+(*     | [ |- context[_ # ?d <- _ ! ?d] ] => rewrite AssocMap.gss *)
+(*     | [ |- context[_ # ?d <- _ ! ?s] ] => rewrite AssocMap.gso *)
+(*     | [ |- context[(AssocMap.empty _) ! _] ] => rewrite AssocMap.gempty *)
+
+(*     | [ |- context[array_get_error _ (combine Verilog.merge_cell (arr_repeat None _) _)] ] => *)
+(*       rewrite combine_lookup_first *)
+
+(*     | [ |- state_st_wf _ _ ] => unfold state_st_wf; inversion 1 *)
+(*     | [ |- context[match_states _ _] ] => econstructor; auto *)
+(*     | [ |- match_arrs _ _ _ _ _ ] => econstructor; auto *)
+(*     | [ |- match_assocmaps _ _ _ # _ <- (posToValue _) ] => *)
+(*       apply regs_lessdef_add_greater; [> unfold Plt; lia | assumption] *)
+
+(*     | [ H : ?asa ! ?r = Some _ |- Verilog.arr_assocmap_lookup ?asa ?r _ = Some _ ] => *)
+(*       unfold Verilog.arr_assocmap_lookup; setoid_rewrite H; f_equal *)
+(*     | [ |- context[(AssocMap.combine _ _ _) ! _] ] => *)
+(*       try (rewrite AssocMap.gcombine; [> | reflexivity]) *)
+
+(*     | [ |- context[Registers.Regmap.get ?d (Registers.Regmap.set ?d _ _)] ] => *)
+(*       rewrite Registers.Regmap.gss *)
+(*     | [ |- context[Registers.Regmap.get ?s (Registers.Regmap.set ?d _ _)] ] => *)
+(*       destruct (Pos.eq_dec s d) as [EQ|EQ]; *)
+(*       [> rewrite EQ | rewrite Registers.Regmap.gso; auto] *)
+
+(*     | [ H : opt_val_value_lessdef _ _ |- _ ] => invert H *)
+(*     | [ H : context[Z.of_nat (Z.to_nat _)] |- _ ] => rewrite Z2Nat.id in H; [> solve crush |] *)
+(*     | [ H : _ ! _ = Some _ |- _] => setoid_rewrite H *)
+(*     end. *)
+
+(*   Ltac small_tac := repeat (crush; try array; try ptrofs); crush; auto. *)
+(*   Ltac big_tac := repeat (crush; try array; try ptrofs; try tac0); crush; auto. *)
+
+  (* Lemma transl_inop_correct: *)
+  (*   forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive) *)
+  (*     (rs : RTL.regset) (m : mem) (pc' : RTL.node), *)
+  (*     (RTL.fn_code f) ! pc = Some (RTL.Inop pc') -> *)
+  (*     forall R1 : HTL.state, *)
+  (*       match_states (RTL.State s f sp pc rs m) R1 -> *)
+  (*       exists R2 : HTL.state, *)
+  (*         Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ match_states (RTL.State s f sp pc' rs m) R2. *)
+  (* Proof. *)
+  (*   intros s f sp pc rs m pc' H R1 MSTATE. *)
+  (*   inv_state. *)
+
+  (*   unfold match_prog in TRANSL. *)
+  (*   econstructor. *)
+  (*   split. *)
+  (*   apply Smallstep.plus_one. *)
+  (*   eapply HTL.step_module; eauto. *)
+  (*   apply assumption_32bit. *)
+  (*   (* processing of state *) *)
+  (*   econstructor. *)
+  (*   crush. *)
+  (*   econstructor. *)
+  (*   econstructor. *)
+  (*   econstructor. *)
+
+  (*   all: invert MARR; big_tac. *)
+  (*   Unshelve. *)
+  (*   constructor. *)
+  (* Qed. *)
+  (* Hint Resolve transl_inop_correct : htlproof. *)
+
+  (* Lemma transl_iop_correct: *)
+  (*   forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive) *)
+  (*     (rs : Registers.Regmap.t Values.val) (m : mem) (op : Op.operation) (args : list Registers.reg) *)
+  (*     (res0 : Registers.reg) (pc' : RTL.node) (v : Values.val), *)
+  (*     (RTL.fn_code f) ! pc = Some (RTL.Iop op args res0 pc') -> *)
+  (*     Op.eval_operation ge sp op (map (fun r : positive => Registers.Regmap.get r rs) args) m = Some v -> *)
+  (*     forall R1 : HTL.state, *)
+  (*       match_states (RTL.State s f sp pc rs m) R1 -> *)
+  (*       exists R2 : HTL.state, *)
+  (*         Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ *)
+  (*         match_states (RTL.State s f sp pc' (Registers.Regmap.set res0 v rs) m) R2. *)
+  (* Proof. *)
+  (*   intros s f sp pc rs m op args res0 pc' v H H0 R1 MSTATE. *)
+  (*   inv_state. *)
+  (*   exploit eval_correct; eauto. intros. inversion H1. inversion H2. *)
+  (*   econstructor. split. *)
+  (*   apply Smallstep.plus_one. *)
+  (*   eapply HTL.step_module; eauto. *)
+  (*   apply assumption_32bit. *)
+  (*   econstructor; simpl; trivial. *)
+  (*   constructor; trivial. *)
+  (*   econstructor; simpl; eauto. *)
+  (*   simpl. econstructor. econstructor. *)
+  (*   apply H3. simplify. *)
+
+  (*   all: big_tac. *)
+
+  (*   assert (Ple res0 (RTL.max_reg_function f)) *)
+  (*       by (eapply RTL.max_reg_function_def; eauto; simpl; auto). *)
+
+  (*   unfold Ple in H10. lia. *)
+  (*   apply regs_lessdef_add_match. assumption. *)
+  (*   apply regs_lessdef_add_greater. unfold Plt; lia. assumption. *)
+  (*   assert (Ple res0 (RTL.max_reg_function f)) *)
+  (*       by (eapply RTL.max_reg_function_def; eauto; simpl; auto). *)
+  (*   unfold Ple in H12; lia. *)
+  (*   unfold_merge. simpl. *)
+  (*   rewrite AssocMap.gso. *)
+  (*   apply AssocMap.gss. *)
+  (*   apply st_greater_than_res. *)
+
+  (*   (*match_states*) *)
+  (*     assert (pc' = valueToPos (posToValue 32 pc')). auto using assumption_32bit. *)
+  (*   rewrite <- H1. *)
+  (*   constructor; auto. *)
+  (*   unfold_merge. *)
+  (*   apply regs_lessdef_add_match. *)
+  (*   constructor. *)
+  (*   apply regs_lessdef_add_greater. *)
+  (*   apply greater_than_max_func. *)
+  (*   assumption. *)
+
+  (*   unfold state_st_wf. intros. inversion H2. subst. *)
+  (*   unfold_merge. *)
+  (*   rewrite AssocMap.gso. *)
+  (*   apply AssocMap.gss. *)
+  (*   apply st_greater_than_res. *)
+
+  (*    + econstructor. split. *)
+  (*    apply Smallstep.plus_one. *)
+  (*    eapply HTL.step_module; eauto. *)
+  (*    econstructor; simpl; trivial. *)
+  (*    constructor; trivial. *)
+  (*    econstructor; simpl; eauto. *)
+  (*    eapply eval_correct; eauto. *)
+  (*    constructor. rewrite valueToInt_intToValue. trivial. *)
+  (*    unfold_merge. simpl. *)
+  (*    rewrite AssocMap.gso. *)
+  (*    apply AssocMap.gss. *)
+  (*    apply st_greater_than_res. *)
+
+  (*     match_states *)
+  (*    assert (pc' = valueToPos (posToValue 32 pc')). auto using assumption_32bit. *)
+  (*    rewrite <- H1. *)
+  (*    constructor. *)
+  (*    unfold_merge. *)
+  (*    apply regs_lessdef_add_match. *)
+  (*    constructor. *)
+  (*    symmetry. apply valueToInt_intToValue. *)
+  (*    apply regs_lessdef_add_greater. *)
+  (*    apply greater_than_max_func. *)
+  (*    assumption. assumption. *)
+
+  (*    unfold state_st_wf. intros. inversion H2. subst. *)
+  (*    unfold_merge. *)
+  (*    rewrite AssocMap.gso. *)
+  (*    apply AssocMap.gss. *)
+  (*    apply st_greater_than_res. *)
+  (*    assumption. *)
+  (* Admitted. *)
+  (* Hint Resolve transl_iop_correct : htlproof. *)
+
+  (* Ltac tac := *)
+  (*   repeat match goal with *)
+  (*          | [ _ : error _ _ = OK _ _ _ |- _ ] => discriminate *)
+  (*          | [ _ : context[if (?x && ?y) then _ else _] |- _ ] => *)
+  (*            let EQ1 := fresh "EQ" in *)
+  (*            let EQ2 := fresh "EQ" in *)
+  (*            destruct x eqn:EQ1; destruct y eqn:EQ2; simpl in * *)
+  (*          | [ _ : context[if ?x then _ else _] |- _ ] => *)
+  (*            let EQ := fresh "EQ" in *)
+  (*            destruct x eqn:EQ; simpl in * *)
+  (*          | [ H : ret _ _ = _  |- _ ] => invert H *)
+  (*          | [ _ : context[match ?x with | _ => _ end] |- _ ] => destruct x *)
+  (*          end. *)
+
+  (* Ltac inv_arr_access := *)
+  (*   match goal with *)
+  (*   | [ _ : translate_arr_access ?chunk ?addr ?args _ _ = OK ?c _ _ |- _] => *)
+  (*     destruct c, chunk, addr, args; crush; tac; crush *)
+  (*   end. *)
+
+  (* Lemma transl_iload_correct: *)
+  (*   forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive) *)
+  (*     (rs : Registers.Regmap.t Values.val) (m : mem) (chunk : AST.memory_chunk) *)
+  (*     (addr : Op.addressing) (args : list Registers.reg) (dst : Registers.reg) *)
+  (*     (pc' : RTL.node) (a v : Values.val), *)
+  (*     (RTL.fn_code f) ! pc = Some (RTL.Iload chunk addr args dst pc') -> *)
+  (*     Op.eval_addressing ge sp addr (map (fun r : positive => Registers.Regmap.get r rs) args) = Some a -> *)
+  (*     Mem.loadv chunk m a = Some v -> *)
+  (*     forall R1 : HTL.state, *)
+  (*       match_states (RTL.State s f sp pc rs m) R1 -> *)
+  (*       exists R2 : HTL.state, *)
+  (*         Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ *)
+  (*         match_states (RTL.State s f sp pc' (Registers.Regmap.set dst v rs) m) R2. *)
+  (* Proof. *)
+  (*   intros s f sp pc rs m chunk addr args dst pc' a v H H0 H1 R1 MSTATE. *)
+  (*   inv_state. inv_arr_access. *)
+
+  (*   + (** Preamble *) *)
+  (*     invert MARR. crush. *)
+
+  (*     unfold Op.eval_addressing in H0. *)
+  (*     destruct (Archi.ptr64) eqn:ARCHI; crush. *)
+
+  (*     unfold reg_stack_based_pointers in RSBP. *)
+  (*     pose proof (RSBP r0) as RSBPr0. *)
+
+  (*     destruct (Registers.Regmap.get r0 rs) eqn:EQr0; crush. *)
+
+  (*     rewrite ARCHI in H1. crush. *)
+  (*     subst. *)
+
+  (*     pose proof MASSOC as MASSOC'. *)
+  (*     invert MASSOC'. *)
+  (*     pose proof (H0 r0). *)
+  (*     assert (HPler0 : Ple r0 (RTL.max_reg_function f)) *)
+  (*       by (eapply RTL.max_reg_function_use; eauto; crush; eauto). *)
+  (*     apply H6 in HPler0. *)
+  (*     invert HPler0; try congruence. *)
+  (*     rewrite EQr0 in H8. *)
+  (*     invert H8. *)
+  (*     clear H0. clear H6. *)
+
+  (*     unfold check_address_parameter_signed in *; *)
+  (*     unfold check_address_parameter_unsigned in *; crush. *)
+
+  (*     remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ asr # r0)) *)
+  (*                                   (Integers.Ptrofs.of_int (Integers.Int.repr z))) as OFFSET. *)
+
+  (*     (** Modular preservation proof *) *)
+  (*     assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE. *)
+  (*     { rewrite HeqOFFSET. *)
+  (*       apply PtrofsExtra.add_mod; crush. *)
+  (*       rewrite Integers.Ptrofs.unsigned_repr_eq. *)
+  (*       rewrite <- Zmod_div_mod; crush. *)
+  (*       apply PtrofsExtra.of_int_mod. *)
+  (*       rewrite Integers.Int.unsigned_repr_eq. *)
+  (*       rewrite <- Zmod_div_mod; crush. } *)
+
+  (*     (** Read bounds proof *) *)
+  (*     assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH. *)
+  (*     { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; crush; auto. *)
+  (*       unfold stack_bounds in BOUNDS. *)
+  (*       exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET)); auto. *)
+  (*       split; try lia; apply Integers.Ptrofs.unsigned_range_2. *)
+  (*       small_tac. } *)
+
+  (*     (** Normalisation proof *) *)
+  (*     assert (Integers.Ptrofs.repr *)
+  (*               (4 * Integers.Ptrofs.unsigned *)
+  (*                      (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4))) = OFFSET) *)
+  (*       as NORMALISE. *)
+  (*     { replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) at 1 by reflexivity. *)
+  (*       rewrite <- PtrofsExtra.mul_unsigned. *)
+  (*       apply PtrofsExtra.mul_divu; crush; auto. } *)
+
+  (*     (** Normalised bounds proof *) *)
+  (*     assert (0 <= *)
+  (*             Integers.Ptrofs.unsigned (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)) *)
+  (*             < (RTL.fn_stacksize f / 4)) *)
+  (*       as NORMALISE_BOUND. *)
+  (*     { split. *)
+  (*       apply Integers.Ptrofs.unsigned_range_2. *)
+  (*       assert (forall x y, Integers.Ptrofs.divu x y = Integers.Ptrofs.divu x y ) by reflexivity. *)
+  (*       unfold Integers.Ptrofs.divu at 2 in H0. *)
+  (*       rewrite H0. clear H0. *)
+  (*       rewrite Integers.Ptrofs.unsigned_repr; crush. *)
+  (*       apply Zmult_lt_reg_r with (p := 4); try lia. *)
+  (*       repeat rewrite ZLib.div_mul_undo; try lia. *)
+  (*       apply Z.div_pos; small_tac. *)
+  (*       apply Z.div_le_upper_bound; small_tac. } *)
+
+  (*     inversion NORMALISE_BOUND as [ NORMALISE_BOUND_LOW NORMALISE_BOUND_HIGH ]; *)
+  (*     clear NORMALISE_BOUND. *)
+
+  (*     (** Start of proof proper *) *)
+  (*     eexists. split. *)
+  (*     eapply Smallstep.plus_one. *)
+  (*     eapply HTL.step_module; eauto. *)
+  (*     apply assumption_32bit. *)
+  (*     econstructor. econstructor. econstructor. crush. *)
+  (*     econstructor. econstructor. econstructor. crush. *)
+  (*     econstructor. econstructor. *)
+  (*     econstructor. econstructor. econstructor. econstructor. *)
+  (*     econstructor. econstructor. econstructor. econstructor. *)
+
+  (*     all: big_tac. *)
+
+  (*     1: { *)
+  (*       assert (HPle : Ple dst (RTL.max_reg_function f)). *)
+  (*       eapply RTL.max_reg_function_def. eassumption. auto. *)
+  (*       apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. *)
+  (*     } *)
+
+  (*     2: { *)
+  (*       assert (HPle : Ple dst (RTL.max_reg_function f)). *)
+  (*       eapply RTL.max_reg_function_def. eassumption. auto. *)
+  (*       apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. *)
+  (*     } *)
+
+  (*     (** Match assocmaps *) *)
+  (*     apply regs_lessdef_add_match; big_tac. *)
+
+  (*     (** Equality proof *) *)
+  (*     match goal with *)
+  (*     | [ |- context [valueToNat ?x] ] => *)
+  (*       assert (Z.to_nat *)
+  (*                 (Integers.Ptrofs.unsigned *)
+  (*                    (Integers.Ptrofs.divu *)
+  (*                       OFFSET *)
+  (*                       (Integers.Ptrofs.repr 4))) *)
+  (*               = *)
+  (*               valueToNat x) *)
+  (*         as EXPR_OK by admit *)
+  (*     end. *)
+  (*     rewrite <- EXPR_OK. *)
+
+  (*     specialize (H7 (Integers.Ptrofs.unsigned *)
+  (*                       (Integers.Ptrofs.divu *)
+  (*                          OFFSET *)
+  (*                          (Integers.Ptrofs.repr 4)))). *)
+  (*     exploit H7; big_tac. *)
+
+  (*     (** RSBP preservation *) *)
+  (*     unfold arr_stack_based_pointers in ASBP. *)
+  (*     specialize (ASBP (Integers.Ptrofs.unsigned *)
+  (*                         (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)))). *)
+  (*     exploit ASBP; big_tac. *)
+  (*     rewrite NORMALISE in H0. rewrite H1 in H0. assumption. *)
+
+  (*   + (** Preamble *) *)
+  (*     invert MARR. crush. *)
+
+  (*     unfold Op.eval_addressing in H0. *)
+  (*     destruct (Archi.ptr64) eqn:ARCHI; crush. *)
+
+  (*     unfold reg_stack_based_pointers in RSBP. *)
+  (*     pose proof (RSBP r0) as RSBPr0. *)
+  (*     pose proof (RSBP r1) as RSBPr1. *)
+
+  (*     destruct (Registers.Regmap.get r0 rs) eqn:EQr0; *)
+  (*     destruct (Registers.Regmap.get r1 rs) eqn:EQr1; crush. *)
+
+  (*     rewrite ARCHI in H1. crush. *)
+  (*     subst. *)
+  (*     clear RSBPr1. *)
+
+  (*     pose proof MASSOC as MASSOC'. *)
+  (*     invert MASSOC'. *)
+  (*     pose proof (H0 r0). *)
+  (*     pose proof (H0 r1). *)
+  (*     assert (HPler0 : Ple r0 (RTL.max_reg_function f)) *)
+  (*       by (eapply RTL.max_reg_function_use; eauto; crush; eauto). *)
+  (*     assert (HPler1 : Ple r1 (RTL.max_reg_function f)) *)
+  (*       by (eapply RTL.max_reg_function_use; eauto; simpl; auto). *)
+  (*     apply H6 in HPler0. *)
+  (*     apply H8 in HPler1. *)
+  (*     invert HPler0; invert HPler1; try congruence. *)
+  (*     rewrite EQr0 in H9. *)
+  (*     rewrite EQr1 in H11. *)
+  (*     invert H9. invert H11. *)
+  (*     clear H0. clear H6. clear H8. *)
+
+  (*     unfold check_address_parameter_signed in *; *)
+  (*     unfold check_address_parameter_unsigned in *; crush. *)
+
+  (*     remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ asr # r0)) *)
+  (*                                   (Integers.Ptrofs.of_int *)
+  (*                                      (Integers.Int.add (Integers.Int.mul (valueToInt asr # r1) (Integers.Int.repr z)) *)
+  (*                                                        (Integers.Int.repr z0)))) as OFFSET. *)
+
+  (*     (** Modular preservation proof *) *)
+  (*     assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE. *)
+  (*     { rewrite HeqOFFSET. *)
+  (*       apply PtrofsExtra.add_mod; crush; try lia. *)
+  (*       rewrite Integers.Ptrofs.unsigned_repr_eq. *)
+  (*       rewrite <- Zmod_div_mod; crush. *)
+  (*       apply PtrofsExtra.of_int_mod. *)
+  (*       apply IntExtra.add_mod; crush. *)
+  (*       apply IntExtra.mul_mod2; crush. *)
+  (*       rewrite Integers.Int.unsigned_repr_eq. *)
+  (*       rewrite <- Zmod_div_mod; crush. *)
+  (*       rewrite Integers.Int.unsigned_repr_eq. *)
+  (*       rewrite <- Zmod_div_mod; crush. } *)
+
+  (*     (** Read bounds proof *) *)
+  (*     assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH. *)
+  (*     { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; crush; auto. *)
+  (*       unfold stack_bounds in BOUNDS. *)
+  (*       exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET)); auto. *)
+  (*       split; try lia; apply Integers.Ptrofs.unsigned_range_2. *)
+  (*       small_tac. } *)
+
+  (*     (** Normalisation proof *) *)
+  (*     assert (Integers.Ptrofs.repr *)
+  (*               (4 * Integers.Ptrofs.unsigned *)
+  (*                      (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4))) = OFFSET) *)
+  (*       as NORMALISE. *)
+  (*     { replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) at 1 by reflexivity. *)
+  (*       rewrite <- PtrofsExtra.mul_unsigned. *)
+  (*       apply PtrofsExtra.mul_divu; crush. } *)
+
+  (*     (** Normalised bounds proof *) *)
+  (*     assert (0 <= *)
+  (*             Integers.Ptrofs.unsigned (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)) *)
+  (*             < (RTL.fn_stacksize f / 4)) *)
+  (*       as NORMALISE_BOUND. *)
+  (*     { split. *)
+  (*       apply Integers.Ptrofs.unsigned_range_2. *)
+  (*       assert (forall x y, Integers.Ptrofs.divu x y = Integers.Ptrofs.divu x y ) by reflexivity. *)
+  (*       unfold Integers.Ptrofs.divu at 2 in H0. *)
+  (*       rewrite H0. clear H0. *)
+  (*       rewrite Integers.Ptrofs.unsigned_repr; crush. *)
+  (*       apply Zmult_lt_reg_r with (p := 4); try lia. *)
+  (*       repeat rewrite ZLib.div_mul_undo; try lia. *)
+  (*       apply Z.div_pos; small_tac. *)
+  (*       apply Z.div_le_upper_bound; lia. } *)
+
+  (*     inversion NORMALISE_BOUND as [ NORMALISE_BOUND_LOW NORMALISE_BOUND_HIGH ]; *)
+  (*     clear NORMALISE_BOUND. *)
+
+  (*     (** Start of proof proper *) *)
+  (*     eexists. split. *)
+  (*     eapply Smallstep.plus_one. *)
+  (*     eapply HTL.step_module; eauto. *)
+  (*     apply assumption_32bit. *)
+  (*     econstructor. econstructor. econstructor. crush. *)
+  (*     econstructor. econstructor. econstructor. crush. *)
+  (*     econstructor. econstructor. econstructor. *)
+  (*     econstructor. econstructor. econstructor. econstructor. *)
+  (*     econstructor. *)
+  (*     eapply Verilog.erun_Vbinop with (EQ := ?[EQ6]). *)
+  (*     econstructor. econstructor. econstructor. econstructor. *)
+  (*     econstructor. econstructor. econstructor. econstructor. *)
+  (*     econstructor. econstructor. *)
+
+  (*     all: big_tac. *)
+
+  (*     1: { assert (HPle : Ple dst (RTL.max_reg_function f)). *)
+  (*          eapply RTL.max_reg_function_def. eassumption. auto. *)
+  (*          apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. } *)
+
+  (*     2: { assert (HPle : Ple dst (RTL.max_reg_function f)). *)
+  (*          eapply RTL.max_reg_function_def. eassumption. auto. *)
+  (*          apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. } *)
+
+  (*     (** Match assocmaps *) *)
+  (*     apply regs_lessdef_add_match; big_tac. *)
+
+  (*     (** Equality proof *) *)
+  (*     match goal with *)
+  (*     | [ |- context [valueToNat ?x] ] => *)
+  (*       assert (Z.to_nat *)
+  (*                 (Integers.Ptrofs.unsigned *)
+  (*                    (Integers.Ptrofs.divu *)
+  (*                       OFFSET *)
+  (*                       (Integers.Ptrofs.repr 4))) *)
+  (*               = *)
+  (*               valueToNat x) *)
+  (*         as EXPR_OK by admit *)
+  (*     end. *)
+  (*     rewrite <- EXPR_OK. *)
+
+  (*     specialize (H7 (Integers.Ptrofs.unsigned *)
+  (*                       (Integers.Ptrofs.divu *)
+  (*                          OFFSET *)
+  (*                          (Integers.Ptrofs.repr 4)))). *)
+  (*     exploit H7; big_tac. *)
+
+  (*     (** RSBP preservation *) *)
+  (*     unfold arr_stack_based_pointers in ASBP. *)
+  (*     specialize (ASBP (Integers.Ptrofs.unsigned *)
+  (*                         (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)))). *)
+  (*     exploit ASBP; big_tac. *)
+  (*     rewrite NORMALISE in H0. rewrite H1 in H0. assumption. *)
+
+  (*   + invert MARR. crush. *)
+
+  (*     unfold Op.eval_addressing in H0. *)
+  (*     destruct (Archi.ptr64) eqn:ARCHI; crush. *)
+  (*     rewrite ARCHI in H0. crush. *)
+
+  (*     unfold check_address_parameter_unsigned in *; *)
+  (*     unfold check_address_parameter_signed in *; crush. *)
+
+  (*     assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. *)
+  (*     rewrite ZERO in H1. clear ZERO. *)
+  (*     rewrite Integers.Ptrofs.add_zero_l in H1. *)
+
+  (*     remember i0 as OFFSET. *)
+
+  (*     (** Modular preservation proof *) *)
+  (*     rename H0 into MOD_PRESERVE. *)
+
+  (*     (** Read bounds proof *) *)
+  (*     assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH. *)
+  (*     { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; crush; auto. *)
+  (*       unfold stack_bounds in BOUNDS. *)
+  (*       exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET)); big_tac. } *)
+
+  (*     (** Normalisation proof *) *)
+  (*     assert (Integers.Ptrofs.repr *)
+  (*               (4 * Integers.Ptrofs.unsigned *)
+  (*                      (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4))) = OFFSET) *)
+  (*       as NORMALISE. *)
+  (*     { replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) at 1 by reflexivity. *)
+  (*       rewrite <- PtrofsExtra.mul_unsigned. *)
+  (*       apply PtrofsExtra.mul_divu; crush. } *)
+
+  (*     (** Normalised bounds proof *) *)
+  (*     assert (0 <= *)
+  (*             Integers.Ptrofs.unsigned (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)) *)
+  (*             < (RTL.fn_stacksize f / 4)) *)
+  (*       as NORMALISE_BOUND. *)
+  (*     { split. *)
+  (*       apply Integers.Ptrofs.unsigned_range_2. *)
+  (*       assert (forall x y, Integers.Ptrofs.divu x y = Integers.Ptrofs.divu x y ) by reflexivity. *)
+  (*       unfold Integers.Ptrofs.divu at 2 in H0. *)
+  (*       rewrite H0. clear H0. *)
+  (*       rewrite Integers.Ptrofs.unsigned_repr; crush. *)
+  (*       apply Zmult_lt_reg_r with (p := 4); try lia. *)
+  (*       repeat rewrite ZLib.div_mul_undo; try lia. *)
+  (*       apply Z.div_pos; small_tac. *)
+  (*       apply Z.div_le_upper_bound; lia. } *)
+
+  (*     inversion NORMALISE_BOUND as [ NORMALISE_BOUND_LOW NORMALISE_BOUND_HIGH ]; *)
+  (*     clear NORMALISE_BOUND. *)
+
+  (*     (** Start of proof proper *) *)
+  (*     eexists. split. *)
+  (*     eapply Smallstep.plus_one. *)
+  (*     eapply HTL.step_module; eauto. *)
+  (*     apply assumption_32bit. *)
+  (*     econstructor. econstructor. econstructor. crush. *)
+  (*     econstructor. econstructor. econstructor. econstructor. crush. *)
+
+  (*     all: big_tac. *)
+
+  (*     1: { assert (HPle : Ple dst (RTL.max_reg_function f)). *)
+  (*          eapply RTL.max_reg_function_def. eassumption. auto. *)
+  (*          apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. } *)
+
+  (*     2: { assert (HPle : Ple dst (RTL.max_reg_function f)). *)
+  (*          eapply RTL.max_reg_function_def. eassumption. auto. *)
+  (*          apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. } *)
+
+  (*     (** Match assocmaps *) *)
+  (*     apply regs_lessdef_add_match; big_tac. *)
+
+  (*     (** Equality proof *) *)
+  (*     match goal with (* Prevents issues with evars *) *)
+  (*     | [ |- context [valueToNat ?x] ] => *)
+  (*       assert (Z.to_nat *)
+  (*                 (Integers.Ptrofs.unsigned *)
+  (*                    (Integers.Ptrofs.divu *)
+  (*                       OFFSET *)
+  (*                       (Integers.Ptrofs.repr 4))) *)
+  (*               = *)
+  (*               valueToNat x) *)
+  (*         as EXPR_OK by admit *)
+  (*     end. *)
+  (*     rewrite <- EXPR_OK. *)
+
+  (*     specialize (H7 (Integers.Ptrofs.unsigned *)
+  (*                       (Integers.Ptrofs.divu *)
+  (*                          OFFSET *)
+  (*                          (Integers.Ptrofs.repr 4)))). *)
+  (*     exploit H7; big_tac. *)
+
+  (*     (** RSBP preservation *) *)
+  (*     unfold arr_stack_based_pointers in ASBP. *)
+  (*     specialize (ASBP (Integers.Ptrofs.unsigned *)
+  (*                         (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)))). *)
+  (*     exploit ASBP; big_tac. *)
+  (*     rewrite NORMALISE in H0. rewrite H1 in H0. assumption. *)
+  (* Admitted. *)
+  (* Hint Resolve transl_iload_correct : htlproof. *)
+
+  (* Lemma transl_istore_correct: *)
+  (*   forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive) *)
+  (*     (rs : Registers.Regmap.t Values.val) (m : mem) (chunk : AST.memory_chunk) *)
+  (*     (addr : Op.addressing) (args : list Registers.reg) (src : Registers.reg) *)
+  (*     (pc' : RTL.node) (a : Values.val) (m' : mem), *)
+  (*     (RTL.fn_code f) ! pc = Some (RTL.Istore chunk addr args src pc') -> *)
+  (*     Op.eval_addressing ge sp addr (map (fun r : positive => Registers.Regmap.get r rs) args) = Some a -> *)
+  (*     Mem.storev chunk m a (Registers.Regmap.get src rs) = Some m' -> *)
+  (*     forall R1 : HTL.state, *)
+  (*       match_states (RTL.State s f sp pc rs m) R1 -> *)
+  (*       exists R2 : HTL.state, *)
+  (*         Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ match_states (RTL.State s f sp pc' rs m') R2. *)
+  (* Proof. *)
+  (*   intros s f sp pc rs m chunk addr args src pc' a m' H H0 H1 R1 MSTATES. *)
+  (*   inv_state. inv_arr_access. *)
+
+  (*   + (** Preamble *) *)
+  (*     invert MARR. crush. *)
+
+  (*     unfold Op.eval_addressing in H0. *)
+  (*     destruct (Archi.ptr64) eqn:ARCHI; crush. *)
+
+  (*     unfold reg_stack_based_pointers in RSBP. *)
+  (*     pose proof (RSBP r0) as RSBPr0. *)
+
+  (*     destruct (Registers.Regmap.get r0 rs) eqn:EQr0; crush. *)
+
+  (*     rewrite ARCHI in H1. crush. *)
+  (*     subst. *)
+
+  (*     pose proof MASSOC as MASSOC'. *)
+  (*     invert MASSOC'. *)
+  (*     pose proof (H0 r0). *)
+  (*     assert (HPler0 : Ple r0 (RTL.max_reg_function f)) *)
+  (*       by (eapply RTL.max_reg_function_use; eauto; crush; eauto). *)
+  (*     apply H6 in HPler0. *)
+  (*     invert HPler0; try congruence. *)
+  (*     rewrite EQr0 in H8. *)
+  (*     invert H8. *)
+  (*     clear H0. clear H6. *)
+
+  (*     unfold check_address_parameter_unsigned in *; *)
+  (*     unfold check_address_parameter_signed in *; crush. *)
+
+  (*     remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ asr # r0)) *)
+  (*                                   (Integers.Ptrofs.of_int (Integers.Int.repr z))) as OFFSET. *)
+
+  (*     (** Modular preservation proof *) *)
+  (*     assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE. *)
+  (*     { rewrite HeqOFFSET. *)
+  (*       apply PtrofsExtra.add_mod; crush; try lia. *)
+  (*       rewrite Integers.Ptrofs.unsigned_repr_eq. *)
+  (*       rewrite <- Zmod_div_mod; crush. *)
+  (*       apply PtrofsExtra.of_int_mod. *)
+  (*       rewrite Integers.Int.unsigned_repr_eq. *)
+  (*       rewrite <- Zmod_div_mod; crush. } *)
+
+  (*     (** Write bounds proof *) *)
+  (*     assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as WRITE_BOUND_HIGH. *)
+  (*     { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; crush; auto. *)
+  (*       unfold stack_bounds in BOUNDS. *)
+  (*       exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET) (Registers.Regmap.get src rs)); big_tac. *)
+  (*       apply Integers.Ptrofs.unsigned_range_2. } *)
+
+  (*     (** Start of proof proper *) *)
+  (*     eexists. split. *)
+  (*     eapply Smallstep.plus_one. *)
+  (*     eapply HTL.step_module; eauto. *)
+  (*     apply assumption_32bit. *)
+  (*     econstructor. econstructor. econstructor. *)
+  (*     eapply Verilog.stmnt_runp_Vnonblock_arr. crush. *)
+  (*     econstructor. *)
+  (*     eapply Verilog.erun_Vbinop with (EQ := ?[EQ7]). *)
+  (*     eapply Verilog.erun_Vbinop with (EQ := ?[EQ8]). *)
+  (*     econstructor. *)
+  (*     econstructor. *)
+  (*     econstructor. econstructor. econstructor. econstructor. *)
+  (*     econstructor. econstructor. econstructor. econstructor. *)
+
+  (*     all: crush. *)
+
+  (*     (** State Lookup *) *)
+  (*     unfold Verilog.merge_regs. *)
+  (*     crush. *)
+  (*     unfold_merge. *)
+  (*     apply AssocMap.gss. *)
+
+  (*     (** Match states *) *)
+  (*     rewrite assumption_32bit. *)
+  (*     econstructor; eauto. *)
+
+  (*     (** Match assocmaps *) *)
+  (*     unfold Verilog.merge_regs. crush. unfold_merge. *)
+  (*     apply regs_lessdef_add_greater. *)
+  (*     unfold Plt; lia. *)
+  (*     assumption. *)
+
+  (*     (** States well formed *) *)
+  (*     unfold state_st_wf. inversion 1. crush. *)
+  (*     unfold Verilog.merge_regs. *)
+  (*     unfold_merge. *)
+  (*     apply AssocMap.gss. *)
+
+  (*     (** Equality proof *) *)
+  (*     match goal with *)
+  (*     | [ |- context [valueToNat ?x] ] => *)
+  (*       assert (Z.to_nat *)
+  (*                 (Integers.Ptrofs.unsigned *)
+  (*                    (Integers.Ptrofs.divu *)
+  (*                       OFFSET *)
+  (*                       (Integers.Ptrofs.repr 4))) *)
+  (*               = *)
+  (*               valueToNat x) *)
+  (*         as EXPR_OK by admit *)
+  (*     end. *)
+
+  (*     assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. *)
+  (*     inversion MASSOC; revert HeqOFFSET; subst; clear MASSOC; intros HeqOFFSET. *)
+
+  (*     econstructor. *)
+  (*     repeat split; crush. *)
+  (*     unfold HTL.empty_stack. *)
+  (*     crush. *)
+  (*     unfold Verilog.merge_arrs. *)
+
+  (*     rewrite AssocMap.gcombine. *)
+  (*     2: { reflexivity. } *)
+  (*     unfold Verilog.arr_assocmap_set. *)
+  (*     rewrite AssocMap.gss. *)
+  (*     unfold Verilog.merge_arr. *)
+  (*     rewrite AssocMap.gss. *)
+  (*     setoid_rewrite H5. *)
+  (*     reflexivity. *)
+
+  (*     rewrite combine_length. *)
+  (*     rewrite <- array_set_len. *)
+  (*     unfold arr_repeat. crush. *)
+  (*     apply list_repeat_len. *)
+
+  (*     rewrite <- array_set_len. *)
+  (*     unfold arr_repeat. crush. *)
+  (*     rewrite list_repeat_len. *)
+  (*     rewrite H4. reflexivity. *)
+
+  (*     remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ asr # r0)) *)
+  (*                                   (Integers.Ptrofs.of_int (Integers.Int.repr z))) as OFFSET. *)
+
+  (*     destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET). *)
+
+  (*     erewrite Mem.load_store_same. *)
+  (*     2: { rewrite ZERO. *)
+  (*          rewrite Integers.Ptrofs.add_zero_l. *)
+  (*          rewrite e. *)
+  (*          rewrite Integers.Ptrofs.unsigned_repr. *)
+  (*          exact H1. *)
+  (*          apply Integers.Ptrofs.unsigned_range_2. } *)
+  (*     constructor. *)
+  (*     erewrite combine_lookup_second. *)
+  (*     simpl. *)
+  (*     assert (Ple src (RTL.max_reg_function f)) *)
+  (*       by (eapply RTL.max_reg_function_use; eauto; simpl; auto); *)
+  (*     apply H0 in H13. *)
+  (*     destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; invert H13; eauto. *)
+
+  (*     rewrite <- array_set_len. *)
+  (*     unfold arr_repeat. crush. *)
+  (*     rewrite list_repeat_len. auto. *)
+
+  (*     assert (4 * ptr / 4 = Integers.Ptrofs.unsigned OFFSET / 4) by (f_equal; assumption). *)
+  (*     rewrite Z.mul_comm in H13. *)
+  (*     rewrite Z_div_mult in H13; try lia. *)
+  (*     replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) in H13 by reflexivity. *)
+  (*     rewrite <- PtrofsExtra.divu_unsigned in H13; unfold_constants; try lia. *)
+  (*     rewrite H13. rewrite EXPR_OK. *)
+  (*     rewrite array_get_error_set_bound. *)
+  (*     reflexivity. *)
+  (*     unfold arr_length, arr_repeat. simpl. *)
+  (*     rewrite list_repeat_len. lia. *)
+
+  (*     erewrite Mem.load_store_other with (m1 := m). *)
+  (*     2: { exact H1. } *)
+  (*     2: { right. *)
+  (*          rewrite ZERO. *)
+  (*          rewrite Integers.Ptrofs.add_zero_l. *)
+  (*          rewrite Integers.Ptrofs.unsigned_repr. *)
+  (*          simpl. *)
+  (*          destruct (Z_le_gt_dec (4 * ptr + 4) (Integers.Ptrofs.unsigned OFFSET)); eauto. *)
+  (*          right. *)
+  (*          apply ZExtra.mod_0_bounds; try lia. *)
+  (*          apply ZLib.Z_mod_mult'. *)
+  (*          rewrite Z2Nat.id in H15; try lia. *)
+  (*          apply Zmult_lt_compat_r with (p := 4) in H15; try lia. *)
+  (*          rewrite ZLib.div_mul_undo in H15; try lia. *)
+  (*          split; try lia. *)
+  (*          apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia. *)
+  (*     } *)
+
+  (*     rewrite <- EXPR_OK. *)
+  (*     rewrite PtrofsExtra.divu_unsigned; auto; try (unfold_constants; lia). *)
+  (*     destruct (ptr ==Z Integers.Ptrofs.unsigned OFFSET / 4). *)
+  (*     apply Z.mul_cancel_r with (p := 4) in e; try lia. *)
+  (*     rewrite ZLib.div_mul_undo in e; try lia. *)
+  (*     rewrite combine_lookup_first. *)
+  (*     eapply H7; eauto. *)
+
+  (*     rewrite <- array_set_len. *)
+  (*     unfold arr_repeat. crush. *)
+  (*     rewrite list_repeat_len. auto. *)
+  (*     rewrite array_gso. *)
+  (*     unfold array_get_error. *)
+  (*     unfold arr_repeat. *)
+  (*     crush. *)
+  (*     apply list_repeat_lookup. *)
+  (*     lia. *)
+  (*     unfold_constants. *)
+  (*     intro. *)
+  (*     apply Z2Nat.inj_iff in H13; try lia. *)
+  (*     apply Z.div_pos; try lia. *)
+  (*     apply Integers.Ptrofs.unsigned_range. *)
+
+  (*     assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. *)
+  (*     unfold arr_stack_based_pointers. *)
+  (*     intros. *)
+  (*     destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET). *)
+
+  (*     crush. *)
+  (*     erewrite Mem.load_store_same. *)
+  (*     2: { rewrite ZERO. *)
+  (*          rewrite Integers.Ptrofs.add_zero_l. *)
+  (*          rewrite e. *)
+  (*          rewrite Integers.Ptrofs.unsigned_repr. *)
+  (*          exact H1. *)
+  (*          apply Integers.Ptrofs.unsigned_range_2. } *)
+  (*     crush. *)
+  (*     destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; try constructor. *)
+  (*     destruct (Archi.ptr64); try discriminate. *)
+  (*     pose proof (RSBP src). rewrite EQ_SRC in H0. *)
+  (*     assumption. *)
+
+  (*     simpl. *)
+  (*     erewrite Mem.load_store_other with (m1 := m). *)
+  (*     2: { exact H1. } *)
+  (*     2: { right. *)
+  (*          rewrite ZERO. *)
+  (*          rewrite Integers.Ptrofs.add_zero_l. *)
+  (*          rewrite Integers.Ptrofs.unsigned_repr. *)
+  (*          simpl. *)
+  (*          destruct (Z_le_gt_dec (4 * ptr + 4) (Integers.Ptrofs.unsigned OFFSET)); eauto. *)
+  (*          right. *)
+  (*          apply ZExtra.mod_0_bounds; try lia. *)
+  (*          apply ZLib.Z_mod_mult'. *)
+  (*          invert H0. *)
+  (*          apply Zmult_lt_compat_r with (p := 4) in H14; try lia. *)
+  (*          rewrite ZLib.div_mul_undo in H14; try lia. *)
+  (*          split; try lia. *)
+  (*          apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia. *)
+  (*     } *)
+  (*     apply ASBP; assumption. *)
+
+  (*     unfold stack_bounds in *. intros. *)
+  (*     simpl. *)
+  (*     assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. *)
+  (*     erewrite Mem.load_store_other with (m1 := m). *)
+  (*     2: { exact H1. } *)
+  (*     2: { right. right. simpl. *)
+  (*          rewrite ZERO. *)
+  (*          rewrite Integers.Ptrofs.add_zero_l. *)
+  (*          rewrite Integers.Ptrofs.unsigned_repr; crush; try lia. *)
+  (*          apply ZExtra.mod_0_bounds; crush; try lia. } *)
+  (*     crush. *)
+  (*     exploit (BOUNDS ptr); try lia. intros. crush. *)
+  (*     exploit (BOUNDS ptr v); try lia. intros. *)
+  (*     invert H0. *)
+  (*     match goal with | |- ?x = _ => destruct x eqn:EQ end; try reflexivity. *)
+  (*     assert (Mem.valid_access m AST.Mint32 sp' *)
+  (*                              (Integers.Ptrofs.unsigned *)
+  (*                                 (Integers.Ptrofs.add (Integers.Ptrofs.repr 0) *)
+  (*                                                      (Integers.Ptrofs.repr ptr))) Writable). *)
+  (*     { pose proof H1. eapply Mem.store_valid_access_2 in H0. *)
+  (*       exact H0. eapply Mem.store_valid_access_3. eassumption. } *)
+  (*     pose proof (Mem.valid_access_store m AST.Mint32 sp' *)
+  (*                                        (Integers.Ptrofs.unsigned *)
+  (*                                           (Integers.Ptrofs.add (Integers.Ptrofs.repr 0) *)
+  (*                                                                (Integers.Ptrofs.repr ptr))) v). *)
+  (*     apply X in H0. invert H0. congruence. *)
+
+  (*   + (** Preamble *) *)
+  (*     invert MARR. crush. *)
+
+  (*     unfold Op.eval_addressing in H0. *)
+  (*     destruct (Archi.ptr64) eqn:ARCHI; crush. *)
+
+  (*     unfold reg_stack_based_pointers in RSBP. *)
+  (*     pose proof (RSBP r0) as RSBPr0. *)
+  (*     pose proof (RSBP r1) as RSBPr1. *)
+
+  (*     destruct (Registers.Regmap.get r0 rs) eqn:EQr0; *)
+  (*     destruct (Registers.Regmap.get r1 rs) eqn:EQr1; crush. *)
+
+  (*     rewrite ARCHI in H1. crush. *)
+  (*     subst. *)
+  (*     clear RSBPr1. *)
+
+  (*     pose proof MASSOC as MASSOC'. *)
+  (*     invert MASSOC'. *)
+  (*     pose proof (H0 r0). *)
+  (*     pose proof (H0 r1). *)
+  (*     assert (HPler0 : Ple r0 (RTL.max_reg_function f)) *)
+  (*       by (eapply RTL.max_reg_function_use; eauto; crush; eauto). *)
+  (*     assert (HPler1 : Ple r1 (RTL.max_reg_function f)) *)
+  (*       by (eapply RTL.max_reg_function_use; eauto; simpl; auto). *)
+  (*     apply H6 in HPler0. *)
+  (*     apply H8 in HPler1. *)
+  (*     invert HPler0; invert HPler1; try congruence. *)
+  (*     rewrite EQr0 in H9. *)
+  (*     rewrite EQr1 in H11. *)
+  (*     invert H9. invert H11. *)
+  (*     clear H0. clear H6. clear H8. *)
+
+  (*     unfold check_address_parameter_signed in *; *)
+  (*     unfold check_address_parameter_unsigned in *; crush. *)
+
+  (*     remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ asr # r0)) *)
+  (*                                   (Integers.Ptrofs.of_int *)
+  (*                                      (Integers.Int.add (Integers.Int.mul (valueToInt asr # r1) (Integers.Int.repr z)) *)
+  (*                                                        (Integers.Int.repr z0)))) as OFFSET. *)
+
+  (*     (** Modular preservation proof *) *)
+  (*     assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE. *)
+  (*     { rewrite HeqOFFSET. *)
+  (*       apply PtrofsExtra.add_mod; crush; try lia. *)
+  (*       rewrite Integers.Ptrofs.unsigned_repr_eq. *)
+  (*       rewrite <- Zmod_div_mod; crush. *)
+  (*       apply PtrofsExtra.of_int_mod. *)
+  (*       apply IntExtra.add_mod; crush. *)
+  (*       apply IntExtra.mul_mod2; crush. *)
+  (*       rewrite Integers.Int.unsigned_repr_eq. *)
+  (*       rewrite <- Zmod_div_mod; crush. *)
+  (*       rewrite Integers.Int.unsigned_repr_eq. *)
+  (*       rewrite <- Zmod_div_mod; crush. } *)
+
+  (*     (** Write bounds proof *) *)
+  (*     assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as WRITE_BOUND_HIGH. *)
+  (*     { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; crush; auto. *)
+  (*       unfold stack_bounds in BOUNDS. *)
+  (*       exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET) (Registers.Regmap.get src rs)); auto. *)
+  (*       split; try lia; apply Integers.Ptrofs.unsigned_range_2. *)
+  (*       small_tac. } *)
+
+  (*     (** Start of proof proper *) *)
+  (*     eexists. split. *)
+  (*     eapply Smallstep.plus_one. *)
+  (*     eapply HTL.step_module; eauto. *)
+  (*     apply assumption_32bit. *)
+  (*     econstructor. econstructor. econstructor. *)
+  (*     eapply Verilog.stmnt_runp_Vnonblock_arr. crush. *)
+  (*     econstructor. *)
+  (*     eapply Verilog.erun_Vbinop with (EQ := ?[EQ9]). *)
+  (*     eapply Verilog.erun_Vbinop with (EQ := ?[EQ10]). *)
+  (*     eapply Verilog.erun_Vbinop with (EQ := ?[EQ11]). *)
+  (*     econstructor. econstructor. econstructor. econstructor. *)
+  (*     econstructor. *)
+  (*     eapply Verilog.erun_Vbinop with (EQ := ?[EQ12]). *)
+  (*     econstructor. econstructor. econstructor. econstructor. *)
+  (*     econstructor. econstructor. econstructor. econstructor. *)
+  (*     econstructor. econstructor. econstructor. econstructor. *)
+
+  (*     all: crush. *)
+
+  (*     (** State Lookup *) *)
+  (*     unfold Verilog.merge_regs. *)
+  (*     crush. *)
+  (*     unfold_merge. *)
+  (*     apply AssocMap.gss. *)
+
+  (*     (** Match states *) *)
+  (*     rewrite assumption_32bit. *)
+  (*     econstructor; eauto. *)
+
+  (*     (** Match assocmaps *) *)
+  (*     unfold Verilog.merge_regs. crush. unfold_merge. *)
+  (*     apply regs_lessdef_add_greater. *)
+  (*     unfold Plt; lia. *)
+  (*     assumption. *)
+
+  (*     (** States well formed *) *)
+  (*     unfold state_st_wf. inversion 1. crush. *)
+  (*     unfold Verilog.merge_regs. *)
+  (*     unfold_merge. *)
+  (*     apply AssocMap.gss. *)
+
+  (*     (** Equality proof *) *)
+  (*     assert (Z.to_nat *)
+  (*               (Integers.Ptrofs.unsigned *)
+  (*                  (Integers.Ptrofs.divu *)
+  (*                     OFFSET *)
+  (*                     (Integers.Ptrofs.repr 4))) *)
+  (*             = *)
+  (*             valueToNat (vdiv *)
+  (*                           (vplus (vplus asr # r0 (ZToValue 32 z0) ?EQ11) (vmul asr # r1 (ZToValue 32 z) ?EQ12) *)
+  (*                                  ?EQ10) (ZToValue 32 4) ?EQ9)) *)
+  (*       as EXPR_OK by admit. *)
+
+  (*     assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. *)
+  (*     inversion MASSOC; revert HeqOFFSET; subst; clear MASSOC; intros HeqOFFSET. *)
+
+  (*     econstructor. *)
+  (*     repeat split; crush. *)
+  (*     unfold HTL.empty_stack. *)
+  (*     crush. *)
+  (*     unfold Verilog.merge_arrs. *)
+
+  (*     rewrite AssocMap.gcombine. *)
+  (*     2: { reflexivity. } *)
+  (*     unfold Verilog.arr_assocmap_set. *)
+  (*     rewrite AssocMap.gss. *)
+  (*     unfold Verilog.merge_arr. *)
+  (*     rewrite AssocMap.gss. *)
+  (*     setoid_rewrite H5. *)
+  (*     reflexivity. *)
+
+  (*     rewrite combine_length. *)
+  (*     rewrite <- array_set_len. *)
+  (*     unfold arr_repeat. crush. *)
+  (*     apply list_repeat_len. *)
+
+  (*     rewrite <- array_set_len. *)
+  (*     unfold arr_repeat. crush. *)
+  (*     rewrite list_repeat_len. *)
+  (*     rewrite H4. reflexivity. *)
+
+  (*     remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ asr # r0)) *)
+  (*                                   (Integers.Ptrofs.of_int *)
+  (*                                      (Integers.Int.add (Integers.Int.mul (valueToInt asr # r1) (Integers.Int.repr z)) *)
+  (*                                                        (Integers.Int.repr z0)))) as OFFSET. *)
+  (*     destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET). *)
+
+  (*     erewrite Mem.load_store_same. *)
+  (*     2: { rewrite ZERO. *)
+  (*          rewrite Integers.Ptrofs.add_zero_l. *)
+  (*          rewrite e. *)
+  (*          rewrite Integers.Ptrofs.unsigned_repr. *)
+  (*          exact H1. *)
+  (*          apply Integers.Ptrofs.unsigned_range_2. } *)
+  (*     constructor. *)
+  (*     erewrite combine_lookup_second. *)
+  (*     simpl. *)
+  (*     assert (Ple src (RTL.max_reg_function f)) *)
+  (*       by (eapply RTL.max_reg_function_use; eauto; simpl; auto); *)
+  (*     apply H0 in H16. *)
+  (*     destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; invert H16; eauto. *)
+
+  (*     rewrite <- array_set_len. *)
+  (*     unfold arr_repeat. crush. *)
+  (*     rewrite list_repeat_len. auto. *)
+
+  (*     assert (4 * ptr / 4 = Integers.Ptrofs.unsigned OFFSET / 4) by (f_equal; assumption). *)
+  (*     rewrite Z.mul_comm in H16. *)
+  (*     rewrite Z_div_mult in H16; try lia. *)
+  (*     replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) in H16 by reflexivity. *)
+  (*     rewrite <- PtrofsExtra.divu_unsigned in H16; unfold_constants; try lia. *)
+  (*     rewrite H16. rewrite EXPR_OK. *)
+  (*     rewrite array_get_error_set_bound. *)
+  (*     reflexivity. *)
+  (*     unfold arr_length, arr_repeat. simpl. *)
+  (*     rewrite list_repeat_len. lia. *)
+
+  (*     erewrite Mem.load_store_other with (m1 := m). *)
+  (*     2: { exact H1. } *)
+  (*     2: { right. *)
+  (*          rewrite ZERO. *)
+  (*          rewrite Integers.Ptrofs.add_zero_l. *)
+  (*          rewrite Integers.Ptrofs.unsigned_repr. *)
+  (*          simpl. *)
+  (*          destruct (Z_le_gt_dec (4 * ptr + 4) (Integers.Ptrofs.unsigned OFFSET)); eauto. *)
+  (*          right. *)
+  (*          apply ZExtra.mod_0_bounds; try lia. *)
+  (*          apply ZLib.Z_mod_mult'. *)
+  (*          rewrite Z2Nat.id in H18; try lia. *)
+  (*          apply Zmult_lt_compat_r with (p := 4) in H18; try lia. *)
+  (*          rewrite ZLib.div_mul_undo in H18; try lia. *)
+  (*          split; try lia. *)
+  (*          apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia. *)
+  (*     } *)
+
+  (*     rewrite <- EXPR_OK. *)
+  (*     rewrite PtrofsExtra.divu_unsigned; auto; try (unfold_constants; lia). *)
+  (*     destruct (ptr ==Z Integers.Ptrofs.unsigned OFFSET / 4). *)
+  (*     apply Z.mul_cancel_r with (p := 4) in e; try lia. *)
+  (*     rewrite ZLib.div_mul_undo in e; try lia. *)
+  (*     rewrite combine_lookup_first. *)
+  (*     eapply H7; eauto. *)
+
+  (*     rewrite <- array_set_len. *)
+  (*     unfold arr_repeat. crush. *)
+  (*     rewrite list_repeat_len. auto. *)
+  (*     rewrite array_gso. *)
+  (*     unfold array_get_error. *)
+  (*     unfold arr_repeat. *)
+  (*     crush. *)
+  (*     apply list_repeat_lookup. *)
+  (*     lia. *)
+  (*     unfold_constants. *)
+  (*     intro. *)
+  (*     apply Z2Nat.inj_iff in H16; try lia. *)
+  (*     apply Z.div_pos; try lia. *)
+  (*     apply Integers.Ptrofs.unsigned_range. *)
+
+  (*     assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. *)
+  (*     unfold arr_stack_based_pointers. *)
+  (*     intros. *)
+  (*     destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET). *)
+
+  (*     crush. *)
+  (*     erewrite Mem.load_store_same. *)
+  (*     2: { rewrite ZERO. *)
+  (*          rewrite Integers.Ptrofs.add_zero_l. *)
+  (*          rewrite e. *)
+  (*          rewrite Integers.Ptrofs.unsigned_repr. *)
+  (*          exact H1. *)
+  (*          apply Integers.Ptrofs.unsigned_range_2. } *)
+  (*     crush. *)
+  (*     destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; try constructor. *)
+  (*     destruct (Archi.ptr64); try discriminate. *)
+  (*     pose proof (RSBP src). rewrite EQ_SRC in H0. *)
+  (*     assumption. *)
+
+  (*     simpl. *)
+  (*     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 H17; try lia. *)
+  (*          rewrite ZLib.div_mul_undo in H17; try lia. *)
+  (*          split; try lia. *)
+  (*          apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia. *)
+  (*     } *)
+  (*     apply ASBP; assumption. *)
+
+  (*     unfold stack_bounds in *. intros. *)
+  (*     simpl. *)
+  (*     assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. *)
+  (*     erewrite Mem.load_store_other with (m1 := m). *)
+  (*     2: { exact H1. } *)
+  (*     2: { right. right. simpl. *)
+  (*          rewrite ZERO. *)
+  (*          rewrite Integers.Ptrofs.add_zero_l. *)
+  (*          rewrite Integers.Ptrofs.unsigned_repr; crush; try lia. *)
+  (*          apply ZExtra.mod_0_bounds; crush; try lia. } *)
+  (*     crush. *)
+  (*     exploit (BOUNDS ptr); try lia. intros. crush. *)
+  (*     exploit (BOUNDS ptr v); try lia. intros. *)
+  (*     invert H0. *)
+  (*     match goal with | |- ?x = _ => destruct x eqn:EQ end; try reflexivity. *)
+  (*     assert (Mem.valid_access m AST.Mint32 sp' *)
+  (*                              (Integers.Ptrofs.unsigned *)
+  (*                                 (Integers.Ptrofs.add (Integers.Ptrofs.repr 0) *)
+  (*                                                      (Integers.Ptrofs.repr ptr))) Writable). *)
+  (*     { pose proof H1. eapply Mem.store_valid_access_2 in H0. *)
+  (*       exact H0. eapply Mem.store_valid_access_3. eassumption. } *)
+  (*     pose proof (Mem.valid_access_store m AST.Mint32 sp' *)
+  (*                                        (Integers.Ptrofs.unsigned *)
+  (*                                           (Integers.Ptrofs.add (Integers.Ptrofs.repr 0) *)
+  (*                                                                (Integers.Ptrofs.repr ptr))) v). *)
+  (*     apply X in H0. invert H0. congruence. *)
+
+  (*   + invert MARR. crush. *)
+
+  (*     unfold Op.eval_addressing in H0. *)
+  (*     destruct (Archi.ptr64) eqn:ARCHI; crush. *)
+  (*     rewrite ARCHI in H0. crush. *)
+
+  (*     unfold check_address_parameter_unsigned in *; *)
+  (*     unfold check_address_parameter_signed in *; crush. *)
+
+  (*     assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. *)
+  (*     rewrite ZERO in H1. clear ZERO. *)
+  (*     rewrite Integers.Ptrofs.add_zero_l in H1. *)
+
+  (*     remember i0 as OFFSET. *)
+
+  (*     (** Modular preservation proof *) *)
+  (*     rename H0 into MOD_PRESERVE. *)
+
+  (*     (** Write bounds proof *) *)
+  (*     assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as WRITE_BOUND_HIGH. *)
+  (*     { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; crush; auto. *)
+  (*       unfold stack_bounds in BOUNDS. *)
+  (*       exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET) (Registers.Regmap.get src rs)); auto. *)
+  (*       crush. *)
+  (*       replace (Integers.Ptrofs.repr 0) with (Integers.Ptrofs.zero) by reflexivity. *)
+  (*       small_tac. } *)
+
+  (*     (** Start of proof proper *) *)
+  (*     eexists. split. *)
+  (*     eapply Smallstep.plus_one. *)
+  (*     eapply HTL.step_module; eauto. *)
+  (*     apply assumption_32bit. *)
+  (*     econstructor. econstructor. econstructor. *)
+  (*     eapply Verilog.stmnt_runp_Vnonblock_arr. crush. *)
+  (*     econstructor. econstructor. econstructor. econstructor. *)
+
+  (*     all: crush. *)
+
+  (*     (** State Lookup *) *)
+  (*     unfold Verilog.merge_regs. *)
+  (*     crush. *)
+  (*     unfold_merge. *)
+  (*     apply AssocMap.gss. *)
+
+  (*     (** Match states *) *)
+  (*     rewrite assumption_32bit. *)
+  (*     econstructor; eauto. *)
+
+  (*     (** Match assocmaps *) *)
+  (*     unfold Verilog.merge_regs. crush. unfold_merge. *)
+  (*     apply regs_lessdef_add_greater. *)
+  (*     unfold Plt; lia. *)
+  (*     assumption. *)
+
+  (*     (** States well formed *) *)
+  (*     unfold state_st_wf. inversion 1. crush. *)
+  (*     unfold Verilog.merge_regs. *)
+  (*     unfold_merge. *)
+  (*     apply AssocMap.gss. *)
+
+  (*     (** Equality proof *) *)
+  (*     assert (Z.to_nat *)
+  (*               (Integers.Ptrofs.unsigned *)
+  (*                  (Integers.Ptrofs.divu *)
+  (*                     OFFSET *)
+  (*                     (Integers.Ptrofs.repr 4))) *)
+  (*             = *)
+  (*             valueToNat (ZToValue 32 (Integers.Ptrofs.unsigned OFFSET / 4))) *)
+  (*       as EXPR_OK by admit. *)
+
+  (*     assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. *)
+  (*     inversion MASSOC; revert HeqOFFSET; subst; clear MASSOC; intros HeqOFFSET. *)
+
+  (*     econstructor. *)
+  (*     repeat split; crush. *)
+  (*     unfold HTL.empty_stack. *)
+  (*     crush. *)
+  (*     unfold Verilog.merge_arrs. *)
+
+  (*     rewrite AssocMap.gcombine. *)
+  (*     2: { reflexivity. } *)
+  (*     unfold Verilog.arr_assocmap_set. *)
+  (*     rewrite AssocMap.gss. *)
+  (*     unfold Verilog.merge_arr. *)
+  (*     rewrite AssocMap.gss. *)
+  (*     setoid_rewrite H5. *)
+  (*     reflexivity. *)
+
+  (*     rewrite combine_length. *)
+  (*     rewrite <- array_set_len. *)
+  (*     unfold arr_repeat. crush. *)
+  (*     apply list_repeat_len. *)
+
+  (*     rewrite <- array_set_len. *)
+  (*     unfold arr_repeat. crush. *)
+  (*     rewrite list_repeat_len. *)
+  (*     rewrite H4. reflexivity. *)
+
+  (*     remember i0 as OFFSET. *)
+  (*     destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET). *)
+
+  (*     erewrite Mem.load_store_same. *)
+  (*     2: { rewrite ZERO. *)
+  (*          rewrite Integers.Ptrofs.add_zero_l. *)
+  (*          rewrite e. *)
+  (*          rewrite Integers.Ptrofs.unsigned_repr. *)
+  (*          exact H1. *)
+  (*          apply Integers.Ptrofs.unsigned_range_2. } *)
+  (*     constructor. *)
+  (*     erewrite combine_lookup_second. *)
+  (*     simpl. *)
+  (*     assert (Ple src (RTL.max_reg_function f)) *)
+  (*       by (eapply RTL.max_reg_function_use; eauto; simpl; auto); *)
+  (*     apply H0 in H8. *)
+  (*     destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; invert H8; eauto. *)
+
+  (*     rewrite <- array_set_len. *)
+  (*     unfold arr_repeat. crush. *)
+  (*     rewrite list_repeat_len. auto. *)
+
+  (*     assert (4 * ptr / 4 = Integers.Ptrofs.unsigned OFFSET / 4) by (f_equal; assumption). *)
+  (*     rewrite Z.mul_comm in H8. *)
+  (*     rewrite Z_div_mult in H8; try lia. *)
+  (*     replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) in H8 by reflexivity. *)
+  (*     rewrite <- PtrofsExtra.divu_unsigned in H8; unfold_constants; try lia. *)
+  (*     rewrite H8. rewrite EXPR_OK. *)
+  (*     rewrite array_get_error_set_bound. *)
+  (*     reflexivity. *)
+  (*     unfold arr_length, arr_repeat. simpl. *)
+  (*     rewrite list_repeat_len. lia. *)
+
+  (*     erewrite Mem.load_store_other with (m1 := m). *)
+  (*     2: { exact H1. } *)
+  (*     2: { right. *)
+  (*          rewrite ZERO. *)
+  (*          rewrite Integers.Ptrofs.add_zero_l. *)
+  (*          rewrite Integers.Ptrofs.unsigned_repr. *)
+  (*          simpl. *)
+  (*          destruct (Z_le_gt_dec (4 * ptr + 4) (Integers.Ptrofs.unsigned OFFSET)); eauto. *)
+  (*          right. *)
+  (*          apply ZExtra.mod_0_bounds; try lia. *)
+  (*          apply ZLib.Z_mod_mult'. *)
+  (*          rewrite Z2Nat.id in H11; try lia. *)
+  (*          apply Zmult_lt_compat_r with (p := 4) in H11; try lia. *)
+  (*          rewrite ZLib.div_mul_undo in H11; try lia. *)
+  (*          split; try lia. *)
+  (*          apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia. *)
+  (*     } *)
+
+  (*     rewrite <- EXPR_OK. *)
+  (*     rewrite PtrofsExtra.divu_unsigned; auto; try (unfold_constants; lia). *)
+  (*     destruct (ptr ==Z Integers.Ptrofs.unsigned OFFSET / 4). *)
+  (*     apply Z.mul_cancel_r with (p := 4) in e; try lia. *)
+  (*     rewrite ZLib.div_mul_undo in e; try lia. *)
+  (*     rewrite combine_lookup_first. *)
+  (*     eapply H7; eauto. *)
+
+  (*     rewrite <- array_set_len. *)
+  (*     unfold arr_repeat. crush. *)
+  (*     rewrite list_repeat_len. auto. *)
+  (*     rewrite array_gso. *)
+  (*     unfold array_get_error. *)
+  (*     unfold arr_repeat. *)
+  (*     crush. *)
+  (*     apply list_repeat_lookup. *)
+  (*     lia. *)
+  (*     unfold_constants. *)
+  (*     intro. *)
+  (*     apply Z2Nat.inj_iff in H8; try lia. *)
+  (*     apply Z.div_pos; try lia. *)
+  (*     apply Integers.Ptrofs.unsigned_range. *)
+
+  (*     assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. *)
+  (*     unfold arr_stack_based_pointers. *)
+  (*     intros. *)
+  (*     destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET). *)
+
+  (*     crush. *)
+  (*     erewrite Mem.load_store_same. *)
+  (*     2: { rewrite ZERO. *)
+  (*          rewrite Integers.Ptrofs.add_zero_l. *)
+  (*          rewrite e. *)
+  (*          rewrite Integers.Ptrofs.unsigned_repr. *)
+  (*          exact H1. *)
+  (*          apply Integers.Ptrofs.unsigned_range_2. } *)
+  (*     crush. *)
+  (*     destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; try constructor. *)
+  (*     destruct (Archi.ptr64); try discriminate. *)
+  (*     pose proof (RSBP src). rewrite EQ_SRC in H0. *)
+  (*     assumption. *)
+
+  (*     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 H9; try lia. *)
+  (*          rewrite ZLib.div_mul_undo in H9; try lia. *)
+  (*          split; try lia. *)
+  (*          apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia. *)
+  (*     } *)
+  (*     apply ASBP; assumption. *)
+
+  (*     unfold stack_bounds in *. intros. *)
+  (*     simpl. *)
+  (*     assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. *)
+  (*     erewrite Mem.load_store_other with (m1 := m). *)
+  (*     2: { exact H1. } *)
+  (*     2: { right. right. simpl. *)
+  (*          rewrite ZERO. *)
+  (*          rewrite Integers.Ptrofs.add_zero_l. *)
+  (*          rewrite Integers.Ptrofs.unsigned_repr; crush; try lia. *)
+  (*          apply ZExtra.mod_0_bounds; crush; try lia. } *)
+  (*     crush. *)
+  (*     exploit (BOUNDS ptr); try lia. intros. crush. *)
+  (*     exploit (BOUNDS ptr v); try lia. intros. *)
+  (*     invert H0. *)
+  (*     match goal with | |- ?x = _ => destruct x eqn:EQ end; try reflexivity. *)
+  (*     assert (Mem.valid_access m AST.Mint32 sp' *)
+  (*                              (Integers.Ptrofs.unsigned *)
+  (*                                 (Integers.Ptrofs.add (Integers.Ptrofs.repr 0) *)
+  (*                                                      (Integers.Ptrofs.repr ptr))) Writable). *)
+  (*     { pose proof H1. eapply Mem.store_valid_access_2 in H0. *)
+  (*       exact H0. eapply Mem.store_valid_access_3. eassumption. } *)
+  (*     pose proof (Mem.valid_access_store m AST.Mint32 sp' *)
+  (*                                        (Integers.Ptrofs.unsigned *)
+  (*                                           (Integers.Ptrofs.add (Integers.Ptrofs.repr 0) *)
+  (*                                                                (Integers.Ptrofs.repr ptr))) v). *)
+  (*     apply X in H0. invert H0. congruence. *)
+  (* Admitted. *)
+  (* Hint Resolve transl_istore_correct : htlproof. *)
+
+  (* Lemma transl_icond_correct: *)
+  (*   forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive) *)
+  (*     (rs : Registers.Regmap.t Values.val) (m : mem) (cond : Op.condition) (args : list Registers.reg) *)
+  (*     (ifso ifnot : RTL.node) (b : bool) (pc' : RTL.node), *)
+  (*     (RTL.fn_code f) ! pc = Some (RTL.Icond cond args ifso ifnot) -> *)
+  (*     Op.eval_condition cond (map (fun r : positive => Registers.Regmap.get r rs) args) m = Some b -> *)
+  (*     pc' = (if b then ifso else ifnot) -> *)
+  (*     forall R1 : HTL.state, *)
+  (*       match_states (RTL.State s f sp pc rs m) R1 -> *)
+  (*       exists R2 : HTL.state, *)
+  (*         Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ match_states (RTL.State s f sp pc' rs m) R2. *)
+  (* Proof. *)
+  (*   intros s f sp pc rs m cond args ifso ifnot b pc' H H0 H1 R1 MSTATE. *)
+  (*   inv_state. *)
+
+  (*   eexists. split. apply Smallstep.plus_one. *)
+  (*   eapply HTL.step_module; eauto. *)
+  (*   apply assumption_32bit. *)
+  (*   eapply Verilog.stmnt_runp_Vnonblock_reg with *)
+  (*       (rhsval := if b then posToValue 32 ifso else posToValue 32 ifnot). *)
+  (*   constructor. *)
+
+  (*   simpl. *)
+  (*   destruct b. *)
+  (*   eapply Verilog.erun_Vternary_true. *)
+  (*   eapply eval_cond_correct; eauto. *)
+  (*   constructor. *)
+  (*   apply boolToValue_ValueToBool. *)
+  (*   eapply Verilog.erun_Vternary_false. *)
+  (*   eapply eval_cond_correct; eauto. *)
+  (*   constructor. *)
+  (*   apply boolToValue_ValueToBool. *)
+  (*   constructor. *)
+
+  (*   big_tac. *)
+
+  (*   invert MARR. *)
+  (*   destruct b; rewrite assumption_32bit; big_tac. *)
+
+  (*   Unshelve. *)
+  (*   constructor. *)
+  (* Qed. *)
+  (* Hint Resolve transl_icond_correct : htlproof. *)
+
+  (* Lemma transl_ijumptable_correct: *)
+  (*   forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive) *)
+  (*     (rs : Registers.Regmap.t Values.val) (m : mem) (arg : Registers.reg) (tbl : list RTL.node) *)
+  (*     (n : Integers.Int.int) (pc' : RTL.node), *)
+  (*     (RTL.fn_code f) ! pc = Some (RTL.Ijumptable arg tbl) -> *)
+  (*     Registers.Regmap.get arg rs = Values.Vint n -> *)
+  (*     list_nth_z tbl (Integers.Int.unsigned n) = Some pc' -> *)
+  (*     forall R1 : HTL.state, *)
+  (*       match_states (RTL.State s f sp pc rs m) R1 -> *)
+  (*       exists R2 : HTL.state, *)
+  (*         Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ match_states (RTL.State s f sp pc' rs m) R2. *)
+  (* Proof. *)
+  (*   intros s f sp pc rs m arg tbl n pc' H H0 H1 R1 MSTATE. *)
+  (* Admitted. *)
+  (* Hint Resolve transl_ijumptable_correct : htlproof. *)
+
+  (* Lemma transl_ireturn_correct: *)
+  (*   forall (s : list RTL.stackframe) (f : RTL.function) (stk : Values.block) *)
+  (*     (pc : positive) (rs : RTL.regset) (m : mem) (or : option Registers.reg) *)
+  (*     (m' : mem), *)
+  (*     (RTL.fn_code f) ! pc = Some (RTL.Ireturn or) -> *)
+  (*     Mem.free m stk 0 (RTL.fn_stacksize f) = Some m' -> *)
+  (*     forall R1 : HTL.state, *)
+  (*       match_states (RTL.State s f (Values.Vptr stk Integers.Ptrofs.zero) pc rs m) R1 -> *)
+  (*       exists R2 : HTL.state, *)
+  (*         Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ *)
+  (*         match_states (RTL.Returnstate s (Registers.regmap_optget or Values.Vundef rs) m') R2. *)
+  (* Proof. *)
+  (*   intros s f stk pc rs m or m' H H0 R1 MSTATE. *)
+  (*   inv_state. *)
+
+  (*   - econstructor. split. *)
+  (*     eapply Smallstep.plus_two. *)
+
+  (*     eapply HTL.step_module; eauto. *)
+  (*     apply assumption_32bit. *)
+  (*     constructor. *)
+  (*     econstructor; simpl; trivial. *)
+  (*     econstructor; simpl; trivial. *)
+  (*     constructor. *)
+  (*     econstructor; simpl; trivial. *)
+  (*     constructor. *)
+
+  (*     constructor. constructor. *)
+
+  (*     unfold state_st_wf in WF; big_tac; eauto. *)
+
+  (*     apply HTL.step_finish. *)
+  (*     unfold Verilog.merge_regs. *)
+  (*     unfold_merge; simpl. *)
+  (*     rewrite AssocMap.gso. *)
+  (*     apply AssocMap.gss. lia. *)
+  (*     apply AssocMap.gss. *)
+  (*     rewrite Events.E0_left. reflexivity. *)
+
+  (*     constructor; auto. *)
+  (*     constructor. *)
+
+  (*   (* FIXME: Duplication *) *)
+  (*   - econstructor. split. *)
+  (*     eapply Smallstep.plus_two. *)
+  (*     eapply HTL.step_module; eauto. *)
+  (*     apply assumption_32bit. *)
+  (*     constructor. *)
+  (*     econstructor; simpl; trivial. *)
+  (*     econstructor; simpl; trivial. *)
+  (*     constructor. constructor. constructor. *)
+  (*     constructor. constructor. constructor. *)
+
+  (*     unfold state_st_wf in WF; big_tac; eauto. *)
+
+  (*     apply HTL.step_finish. *)
+  (*     unfold Verilog.merge_regs. *)
+  (*     unfold_merge. *)
+  (*     rewrite AssocMap.gso. *)
+  (*     apply AssocMap.gss. simpl; lia. *)
+  (*     apply AssocMap.gss. *)
+  (*     rewrite Events.E0_left. trivial. *)
+
+  (*     constructor; auto. *)
+
+  (*     simpl. inversion MASSOC. subst. *)
+  (*     unfold find_assocmap, AssocMapExt.get_default. rewrite AssocMap.gso. *)
+  (*     apply H1. eapply RTL.max_reg_function_use. eauto. simpl; tauto. *)
+  (*     assert (HPle : Ple r (RTL.max_reg_function f)). *)
+  (*     eapply RTL.max_reg_function_use. eassumption. simpl; auto. *)
+  (*     apply ZExtra.Ple_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. *)
+
+  (*     Unshelve. *)
+  (*     all: constructor. *)
+  (* Qed. *)
+  (* Hint Resolve transl_ireturn_correct : htlproof. *)
+
+  (* Lemma transl_callstate_correct: *)
+  (*   forall (s : list RTL.stackframe) (f : RTL.function) (args : list Values.val) *)
+  (*     (m : mem) (m' : Mem.mem') (stk : Values.block), *)
+  (*     Mem.alloc m 0 (RTL.fn_stacksize f) = (m', stk) -> *)
+  (*     forall R1 : HTL.state, *)
+  (*       match_states (RTL.Callstate s (AST.Internal f) args m) R1 -> *)
+  (*       exists R2 : HTL.state, *)
+  (*         Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ *)
+  (*         match_states *)
+  (*           (RTL.State s f (Values.Vptr stk Integers.Ptrofs.zero) (RTL.fn_entrypoint f) *)
+  (*                      (RTL.init_regs args (RTL.fn_params f)) m') R2. *)
+  (* Proof. *)
+  (*   intros s f args m m' stk H R1 MSTATE. *)
+
+  (*   inversion MSTATE; subst. inversion TF; subst. *)
+  (*   econstructor. split. apply Smallstep.plus_one. *)
+  (*   eapply HTL.step_call. crush. *)
+
+  (*   apply match_state with (sp' := stk); eauto. *)
+
+  (*   all: big_tac. *)
+
+  (*   apply regs_lessdef_add_greater. *)
+  (*   unfold Plt; lia. *)
+  (*   apply init_reg_assoc_empty. *)
+
+  (*   constructor. *)
+
+  (*   destruct (Mem.load AST.Mint32 m' stk *)
+  (*                      (Integers.Ptrofs.unsigned (Integers.Ptrofs.add *)
+  (*                                                   Integers.Ptrofs.zero *)
+  (*                                                   (Integers.Ptrofs.repr (4 * ptr))))) eqn:LOAD. *)
+  (*   pose proof Mem.load_alloc_same as LOAD_ALLOC. *)
+  (*   pose proof H as ALLOC. *)
+  (*   eapply LOAD_ALLOC in ALLOC. *)
+  (*   2: { exact LOAD. } *)
+  (*   ptrofs. rewrite LOAD. *)
+  (*   rewrite ALLOC. *)
+  (*   repeat constructor. *)
+
+  (*   ptrofs. rewrite LOAD. *)
+  (*   repeat constructor. *)
+
+  (*   unfold reg_stack_based_pointers. intros. *)
+  (*   unfold RTL.init_regs; crush. *)
+  (*   destruct (RTL.fn_params f); *)
+  (*   rewrite Registers.Regmap.gi; constructor. *)
+
+  (*   unfold arr_stack_based_pointers. intros. *)
+  (*   crush. *)
+  (*   destruct (Mem.load AST.Mint32 m' stk *)
+  (*                      (Integers.Ptrofs.unsigned (Integers.Ptrofs.add *)
+  (*                                                   Integers.Ptrofs.zero *)
+  (*                                                   (Integers.Ptrofs.repr (4 * ptr))))) eqn:LOAD. *)
+  (*   pose proof Mem.load_alloc_same as LOAD_ALLOC. *)
+  (*   pose proof H as ALLOC. *)
+  (*   eapply LOAD_ALLOC in ALLOC. *)
+  (*   2: { exact LOAD. } *)
+  (*   rewrite ALLOC. *)
+  (*   repeat constructor. *)
+  (*   constructor. *)
+
+  (*   Transparent Mem.alloc. (* TODO: Since there are opaque there's probably a lemma. *) *)
+  (*   Transparent Mem.load. *)
+  (*   Transparent Mem.store. *)
+  (*   unfold stack_bounds. *)
+  (*   split. *)
+
+  (*   unfold Mem.alloc in H. *)
+  (*   invert H. *)
+  (*   crush. *)
+  (*   unfold Mem.load. *)
+  (*   intros. *)
+  (*   match goal with | |- context[if ?x then _ else _] => destruct x end; try congruence. *)
+  (*   invert v0. unfold Mem.range_perm in H4. *)
+  (*   unfold Mem.perm in H4. crush. *)
+  (*   unfold Mem.perm_order' in H4. *)
+  (*   small_tac. *)
+  (*   exploit (H4 ptr). rewrite Integers.Ptrofs.unsigned_repr; small_tac. intros. *)
+  (*   rewrite Maps.PMap.gss in H8. *)
+  (*   match goal with | H8 : context[if ?x then _ else _] |- _ => destruct x eqn:EQ end; try contradiction. *)
+  (*   crush. *)
+  (*   apply proj_sumbool_true in H10. lia. *)
+
+  (*   unfold Mem.alloc in H. *)
+  (*   invert H. *)
+  (*   crush. *)
+  (*   unfold Mem.store. *)
+  (*   intros. *)
+  (*   match goal with | |- context[if ?x then _ else _] => destruct x end; try congruence. *)
+  (*   invert v0. unfold Mem.range_perm in H4. *)
+  (*   unfold Mem.perm in H4. crush. *)
+  (*   unfold Mem.perm_order' in H4. *)
+  (*   small_tac. *)
+  (*   exploit (H4 ptr). rewrite Integers.Ptrofs.unsigned_repr; small_tac. intros. *)
+  (*   rewrite Maps.PMap.gss in H8. *)
+  (*   match goal with | H8 : context[if ?x then _ else _] |- _ => destruct x eqn:EQ end; try contradiction. *)
+  (*   crush. *)
+  (*   apply proj_sumbool_true in H10. lia. *)
+  (*   Opaque Mem.alloc. *)
+  (*   Opaque Mem.load. *)
+  (*   Opaque Mem.store. *)
+  (* Qed. *)
+  (* Hint Resolve transl_callstate_correct : htlproof. *)
+
+  (* Lemma transl_returnstate_correct: *)
+  (*   forall (res0 : Registers.reg) (f : RTL.function) (sp : Values.val) (pc : RTL.node) *)
+  (*     (rs : RTL.regset) (s : list RTL.stackframe) (vres : Values.val) (m : mem) *)
+  (*     (R1 : HTL.state), *)
+  (*     match_states (RTL.Returnstate (RTL.Stackframe res0 f sp pc rs :: s) vres m) R1 -> *)
+  (*     exists R2 : HTL.state, *)
+  (*       Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ *)
+  (*       match_states (RTL.State s f sp pc (Registers.Regmap.set res0 vres rs) m) R2. *)
+  (* Proof. *)
+  (*   intros res0 f sp pc rs s vres m R1 MSTATE. *)
+  (*   inversion MSTATE. inversion MF. *)
+  (* Qed. *)
+  (* Hint Resolve transl_returnstate_correct : htlproof. *)
+
+  (* Lemma option_inv : *)
+  (*   forall A x y, *)
+  (*     @Some A x = Some y -> x = y. *)
+  (* Proof. intros. inversion H. trivial. Qed. *)
+
+  (* Lemma main_tprog_internal : *)
+  (*   forall b, *)
+  (*     Globalenvs.Genv.find_symbol tge tprog.(AST.prog_main) = Some b -> *)
+  (*     exists f, Genv.find_funct_ptr (Genv.globalenv tprog) b = Some (AST.Internal f). *)
+  (* Proof. *)
+  (*   intros. *)
+  (*   destruct TRANSL. unfold main_is_internal in H1. *)
+  (*   repeat (unfold_match H1). replace b with b0. *)
+  (*   exploit function_ptr_translated; eauto. intros [tf [A B]]. *)
+  (*   unfold transl_fundef, AST.transf_partial_fundef, Errors.bind in B. *)
+  (*   unfold_match B. inv B. econstructor. apply A. *)
+
+  (*   apply option_inv. rewrite <- Heqo. rewrite <- H. *)
+  (*   rewrite symbols_preserved. replace (AST.prog_main tprog) with (AST.prog_main prog). *)
+  (*   trivial. symmetry; eapply Linking.match_program_main; eauto. *)
+  (* Qed. *)
+
+  (* Lemma transl_initial_states : *)
+  (*   forall s1 : Smallstep.state (RTL.semantics prog), *)
+  (*     Smallstep.initial_state (RTL.semantics prog) s1 -> *)
+  (*     exists s2 : Smallstep.state (HTL.semantics tprog), *)
+  (*       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. *)
+  (*   replace (AST.prog_main tprog) with (AST.prog_main prog). *)
+  (*   rewrite symbols_preserved; eauto. *)
+  (*   symmetry; eapply Linking.match_program_main; eauto. *)
+  (*   apply H6. *)
+
+  (*   constructor. *)
+  (*   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 : *)
+  (*   forall (s1 : Smallstep.state (RTL.semantics prog)) *)
+  (*          (s2 : Smallstep.state (HTL.semantics tprog)) *)
+  (*          (r : Integers.Int.int), *)
+  (*     match_states s1 s2 -> *)
+  (*     Smallstep.final_state (RTL.semantics prog) s1 r -> *)
+  (*     Smallstep.final_state (HTL.semantics tprog) s2 r. *)
+  (* Proof. *)
+  (*   intros. inv H0. inv H. inv H4. invert MF. constructor. reflexivity. *)
+  (* Qed. *)
+  (* Hint Resolve transl_final_states : htlproof. *)
+
+  (* Theorem transl_step_correct: *)
+  (*   forall (S1 : RTL.state) t S2, *)
+  (*     RTL.step ge S1 t S2 -> *)
+  (*     forall (R1 : HTL.state), *)
+  (*       match_states S1 R1 -> *)
+  (*       exists R2, Smallstep.plus HTL.step tge R1 t R2 /\ match_states S2 R2. *)
+  (* Proof. *)
+  (*   induction 1; eauto with htlproof; (intros; inv_state). *)
+  (* Qed. *)
+  (* Hint Resolve transl_step_correct : htlproof. *)
+
+(*   Theorem transf_program_correct: *)
+(*     Smallstep.forward_simulation (RTL.semantics prog) (HTL.semantics tprog). *)
+(*   Proof. *)
+(*   Admitted. *)
+(*   (*   eapply Smallstep.forward_simulation_plus; eauto with htlproof. *) *)
+(*   (*   apply senv_preserved. *) *)
+(*   (* Qed. *) *)
+
+(* End CORRECTNESS. *)
diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v
index a9626c4..4662cf4 100644
--- a/src/translation/HTLgenspec.v
+++ b/src/translation/HTLgenspec.v
@@ -148,462 +148,462 @@ Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> stmnt -> stmnt -
     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)
-          (fin rtrn st stk : reg) : Prop :=
-  tr_code_intro :
-    forall s t,
-      c!pc = Some i ->
-      stmnts!pc = Some s ->
-      trans!pc = Some t ->
-      tr_instr fin rtrn st stk i s t ->
-      tr_code c pc i stmnts trans fin rtrn st stk.
-Hint Constructors tr_code : htlspec.
-
-Inductive tr_module (f : RTL.function) : module -> Prop :=
-  tr_module_intro :
-    forall data control fin rtrn st stk stk_len m start rst clk scldecls arrdecls wf,
-      m = (mkmodule f.(RTL.fn_params)
-                        data
-                        control
-                        f.(RTL.fn_entrypoint)
-                        st stk stk_len fin rtrn start rst clk scldecls arrdecls wf) ->
-      (forall pc i, Maps.PTree.get pc f.(RTL.fn_code) = Some i ->
-               tr_code f.(RTL.fn_code) pc i data control fin rtrn st stk) ->
-      stk_len = Z.to_nat (f.(RTL.fn_stacksize) / 4) ->
-      Z.modulo (f.(RTL.fn_stacksize)) 4 = 0 ->
-      0 <= f.(RTL.fn_stacksize) < Integers.Ptrofs.modulus ->
-      st = ((RTL.max_reg_function f) + 1)%positive ->
-      fin = ((RTL.max_reg_function f) + 2)%positive ->
-      rtrn = ((RTL.max_reg_function f) + 3)%positive ->
-      stk = ((RTL.max_reg_function f) + 4)%positive ->
-      start = ((RTL.max_reg_function f) + 5)%positive ->
-      rst = ((RTL.max_reg_function f) + 6)%positive ->
-      clk = ((RTL.max_reg_function f) + 7)%positive ->
-      tr_module f m.
-Hint Constructors tr_module : htlspec.
-
-Lemma create_reg_datapath_trans :
-  forall sz s s' x i iop,
-    create_reg iop sz s = OK x s' i ->
-    s.(st_datapath) = s'.(st_datapath).
-Proof. intros. monadInv H. trivial. Qed.
-Hint Resolve create_reg_datapath_trans : htlspec.
-
-Lemma create_reg_controllogic_trans :
-  forall sz s s' x i iop,
-    create_reg iop sz s = OK x s' i ->
-    s.(st_controllogic) = s'.(st_controllogic).
-Proof. intros. monadInv H. trivial. Qed.
-Hint Resolve create_reg_controllogic_trans : htlspec.
-
-Lemma declare_reg_datapath_trans :
-  forall sz s s' x i iop r,
-    declare_reg iop r sz s = OK x s' i ->
-    s.(st_datapath) = s'.(st_datapath).
-Proof. intros. monadInv H. trivial. Qed.
-Hint Resolve create_reg_datapath_trans : htlspec.
-
-Lemma declare_reg_controllogic_trans :
-  forall sz s s' x i iop r,
-    declare_reg iop r sz s = OK x s' i ->
-    s.(st_controllogic) = s'.(st_controllogic).
-Proof. intros. monadInv H. trivial. Qed.
-Hint Resolve create_reg_controllogic_trans : htlspec.
-
-Lemma declare_reg_freshreg_trans :
-  forall sz s s' x i iop r,
-    declare_reg iop r sz s = OK x s' i ->
-    s.(st_freshreg) = s'.(st_freshreg).
-Proof. inversion 1; auto. Qed.
-Hint Resolve declare_reg_freshreg_trans : htlspec.
-
-Lemma create_arr_datapath_trans :
-  forall sz ln s s' x i iop,
-    create_arr iop sz ln s = OK x s' i ->
-    s.(st_datapath) = s'.(st_datapath).
-Proof. intros. monadInv H. trivial. Qed.
-Hint Resolve create_arr_datapath_trans : htlspec.
-
-Lemma create_arr_controllogic_trans :
-  forall sz ln s s' x i iop,
-    create_arr iop sz ln s = OK x s' i ->
-    s.(st_controllogic) = s'.(st_controllogic).
-Proof. intros. monadInv H. trivial. Qed.
-Hint Resolve create_arr_controllogic_trans : htlspec.
-
-Lemma get_refl_x :
-  forall s s' x i,
-    get s = OK x s' i ->
-    s = x.
-Proof. inversion 1. trivial. Qed.
-Hint Resolve get_refl_x : htlspec.
-
-Lemma get_refl_s :
-  forall s s' x i,
-    get s = OK x s' i ->
-    s = s'.
-Proof. inversion 1. trivial. Qed.
-Hint Resolve get_refl_s : htlspec.
-
-Ltac inv_incr :=
-  repeat match goal with
-  | [ H: create_reg _ _ ?s = OK _ ?s' _ |- _ ] =>
-    let H1 := fresh "H" in
-    assert (H1 := H); eapply create_reg_datapath_trans in H;
-    eapply create_reg_controllogic_trans in H1
-  | [ H: create_arr _ _ _ ?s = OK _ ?s' _ |- _ ] =>
-    let H1 := fresh "H" in
-    assert (H1 := H); eapply create_arr_datapath_trans in H;
-    eapply create_arr_controllogic_trans in H1
-  | [ H: get ?s = OK _ _ _ |- _ ] =>
-    let H1 := fresh "H" in
-    assert (H1 := H); apply get_refl_x in H; apply get_refl_s in H1;
-    subst
-  | [ H: st_prop _ _ |- _ ] => unfold st_prop in H; destruct H
-  | [ H: st_incr _ _ |- _ ] => destruct st_incr
-  end.
-
-Lemma collect_controllogic_trans :
-  forall A f l cs cs' ci,
-  (forall s s' x i y, f y s = OK x s' i -> s.(st_controllogic) = s'.(st_controllogic)) ->
-  @HTLMonadExtra.collectlist A f l cs = OK tt cs' ci -> cs.(st_controllogic) = cs'.(st_controllogic).
-Proof.
-  induction l; intros; monadInv H0.
-  - trivial.
-  - apply H in EQ. rewrite EQ. eauto.
-Qed.
-
-Lemma collect_datapath_trans :
-  forall A f l cs cs' ci,
-  (forall s s' x i y, f y s = OK x s' i -> s.(st_datapath) = s'.(st_datapath)) ->
-  @HTLMonadExtra.collectlist A f l cs = OK tt cs' ci -> cs.(st_datapath) = cs'.(st_datapath).
-Proof.
-  induction l; intros; monadInv H0.
-  - trivial.
-  - apply H in EQ. rewrite EQ. eauto.
-Qed.
-
-Lemma collect_freshreg_trans :
-  forall A f l cs cs' ci,
-  (forall s s' x i y, f y s = OK x s' i -> s.(st_freshreg) = s'.(st_freshreg)) ->
-  @HTLMonadExtra.collectlist A f l cs = OK tt cs' ci -> cs.(st_freshreg) = cs'.(st_freshreg).
-Proof.
-  induction l; intros; monadInv H0.
-  - trivial.
-  - apply H in EQ. rewrite EQ. eauto.
-Qed.
-
-Lemma collect_declare_controllogic_trans :
-  forall io n l s s' i,
-  HTLMonadExtra.collectlist (fun r : reg => declare_reg io r n) l s = OK tt s' i ->
-  s.(st_controllogic) = s'.(st_controllogic).
-Proof.
-  intros. eapply collect_controllogic_trans; try eassumption.
-  intros. eapply declare_reg_controllogic_trans. simpl in H0. eassumption.
-Qed.
-
-Lemma collect_declare_datapath_trans :
-  forall io n l s s' i,
-  HTLMonadExtra.collectlist (fun r : reg => declare_reg io r n) l s = OK tt s' i ->
-  s.(st_datapath) = s'.(st_datapath).
-Proof.
-  intros. eapply collect_datapath_trans; try eassumption.
-  intros. eapply declare_reg_datapath_trans. simpl in H0. eassumption.
-Qed.
-
-Lemma collect_declare_freshreg_trans :
-  forall io n l s s' i,
-  HTLMonadExtra.collectlist (fun r : reg => declare_reg io r n) l s = OK tt s' i ->
-  s.(st_freshreg) = s'.(st_freshreg).
-Proof.
-  intros. eapply collect_freshreg_trans; try eassumption.
-  inversion 1. auto.
-Qed.
-
-Ltac unfold_match H :=
-  match type of H with
-  | context[match ?g with _ => _ end] => destruct g eqn:?; try discriminate
-  end.
-
-Lemma translate_eff_addressing_freshreg_trans :
-  forall op args s r s' i,
-  translate_eff_addressing op args s = OK r s' i ->
-  s.(st_freshreg) = s'.(st_freshreg).
-Proof.
-  destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto.
-Qed.
-Hint Resolve translate_eff_addressing_freshreg_trans : htlspec.
-
-Lemma translate_comparison_freshreg_trans :
-  forall op args s r s' i,
-  translate_comparison op args s = OK r s' i ->
-  s.(st_freshreg) = s'.(st_freshreg).
-Proof.
-  destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto.
-Qed.
-Hint Resolve translate_comparison_freshreg_trans : htlspec.
-
-Lemma translate_comparison_imm_freshreg_trans :
-  forall op args s r s' i n,
-  translate_comparison_imm op args n s = OK r s' i ->
-  s.(st_freshreg) = s'.(st_freshreg).
-Proof.
-  destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto.
-Qed.
-Hint Resolve translate_comparison_imm_freshreg_trans : htlspec.
-
-Lemma translate_condition_freshreg_trans :
-  forall op args s r s' i,
-  translate_condition op args s = OK r s' i ->
-  s.(st_freshreg) = s'.(st_freshreg).
-Proof.
-  destruct op; intros; simpl in *; repeat (unfold_match H); inv H; eauto with htlspec.
-Qed.
-Hint Resolve translate_condition_freshreg_trans : htlspec.
-
-Lemma translate_instr_freshreg_trans :
-  forall op args s r s' i,
-  translate_instr op args s = OK r s' i ->
-  s.(st_freshreg) = s'.(st_freshreg).
-Proof.
-  destruct op; intros; simpl in *; repeat (unfold_match H); inv H; eauto with htlspec.
-  monadInv H1. eauto with htlspec.
-Qed.
-Hint Resolve translate_instr_freshreg_trans : htlspec.
-
-Lemma translate_arr_access_freshreg_trans :
-  forall mem addr args st s r s' i,
-  translate_arr_access mem addr args st s = OK r s' i ->
-  s.(st_freshreg) = s'.(st_freshreg).
-Proof.
-  intros. unfold translate_arr_access in H. repeat (unfold_match H); inv H; eauto with htlspec.
-Qed.
-Hint Resolve translate_arr_access_freshreg_trans : htlspec.
-
-Lemma add_instr_freshreg_trans :
-  forall n n' st s r s' i,
-  add_instr n n' st s = OK r s' i ->
-  s.(st_freshreg) = s'.(st_freshreg).
-Proof. intros. unfold add_instr in H. repeat (unfold_match H). inv H. auto. Qed.
-Hint Resolve add_instr_freshreg_trans : htlspec.
-
-Lemma add_branch_instr_freshreg_trans :
-  forall n n0 n1 e s r s' i,
-  add_branch_instr e n n0 n1 s = OK r s' i ->
-  s.(st_freshreg) = s'.(st_freshreg).
-Proof. intros. unfold add_branch_instr in H. repeat (unfold_match H). inv H. auto. Qed.
-Hint Resolve add_branch_instr_freshreg_trans : htlspec.
-
-Lemma add_node_skip_freshreg_trans :
-  forall n1 n2 s r s' i,
-  add_node_skip n1 n2 s = OK r s' i ->
-  s.(st_freshreg) = s'.(st_freshreg).
-Proof. intros. unfold add_node_skip in H. repeat (unfold_match H). inv H. auto. Qed.
-Hint Resolve add_node_skip_freshreg_trans : htlspec.
-
-Lemma add_instr_skip_freshreg_trans :
-  forall n1 n2 s r s' i,
-  add_instr_skip n1 n2 s = OK r s' i ->
-  s.(st_freshreg) = s'.(st_freshreg).
-Proof. intros. unfold add_instr_skip in H. repeat (unfold_match H). inv H. auto. Qed.
-Hint Resolve add_instr_skip_freshreg_trans : htlspec.
-
-Lemma transf_instr_freshreg_trans :
-  forall fin ret st instr s v s' i,
-    transf_instr fin ret st instr s = OK v s' i ->
-    s.(st_freshreg) = s'.(st_freshreg).
-Proof.
-  intros. destruct instr eqn:?. subst. unfold transf_instr in H.
-  destruct i0; try (monadInv H); try (unfold_match H); eauto with htlspec.
-  - apply add_instr_freshreg_trans in EQ2. apply translate_instr_freshreg_trans in EQ.
-    apply declare_reg_freshreg_trans in EQ1. congruence.
-  - apply add_instr_freshreg_trans in EQ2. apply translate_arr_access_freshreg_trans in EQ.
-    apply declare_reg_freshreg_trans in EQ1. congruence.
-  - apply add_instr_freshreg_trans in EQ0. apply translate_arr_access_freshreg_trans in EQ. congruence.
-  - apply translate_condition_freshreg_trans in EQ. apply add_branch_instr_freshreg_trans in EQ0.
-    congruence.
-  - inv EQ. apply add_node_skip_freshreg_trans in EQ0. congruence.
-Qed.
-Hint Resolve transf_instr_freshreg_trans : htlspec.
-
-Lemma collect_trans_instr_freshreg_trans :
-  forall fin ret st l s s' i,
-  HTLMonadExtra.collectlist (transf_instr fin ret st) l s = OK tt s' i ->
-  s.(st_freshreg) = s'.(st_freshreg).
-Proof.
-  intros. eapply collect_freshreg_trans; try eassumption.
-  eauto with htlspec.
-Qed.
-
-Ltac rewrite_states :=
-  match goal with
-  | [ H: ?x ?s = ?x ?s' |- _ ] =>
-    let c1 := fresh "c" in
-    let c2 := fresh "c" in
-    remember (?x ?s) as c1; remember (?x ?s') as c2; try subst
-  end.
-
-Ltac inv_add_instr' H :=
-  match type of H with
-  | ?f _ _ _ = OK _ _ _ => unfold f in H
-  | ?f _ _ _ _ = OK _ _ _ => unfold f in H
-  | ?f _ _ _ _ _ = OK _ _ _ => unfold f in H
-  end; repeat unfold_match H; inversion H.
-
-Ltac inv_add_instr :=
-  lazymatch goal with
-  | H: context[add_instr_skip _ _ _] |- _ =>
-    inv_add_instr' H
-  | H: context[add_instr_skip _ _] |- _ =>
-    monadInv H; inv_incr; inv_add_instr
-  | H: context[add_instr _ _ _ _] |- _ =>
-    inv_add_instr' H
-  | H: context[add_instr _ _ _] |- _ =>
-    monadInv H; inv_incr; inv_add_instr
-  | H: context[add_branch_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 :=
-  match goal with H: option ?r |- _ => destruct H end.
-
-Lemma iter_expand_instr_spec :
-  forall l fin rtrn stack s s' i x c,
-    HTLMonadExtra.collectlist (transf_instr fin rtrn stack) l s = OK x s' i ->
-    list_norepet (List.map fst l) ->
-    (forall pc instr, In (pc, instr) l -> c!pc = Some instr) ->
-    (forall pc instr, In (pc, instr) l ->
-                      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.
-  destruct a as [pc1 instr1]; simpl in *. inv H0. monadInv H. inv_incr.
-  destruct (peq pc pc1).
-  - subst.
-    destruct instr1 eqn:?; try discriminate;
-      try destruct_optional; inv_add_instr; econstructor; try assumption.
-    + 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. inversion H9. rewrite H. apply tr_instr_Inop.
-      eapply in_map with (f := fst) in H9. 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. 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. 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.
-    + destruct H2.
-      * inversion H2.
-        replace (st_st s2) with (st_st s0) by congruence.
-        eauto with htlspec.
-      * apply in_map with (f := fst) in H2. 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.
-    + destruct H2.
-      * inversion H2.
-        replace (st_st s2) with (st_st s0) by congruence.
-        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.
-      * inversion H9.
-        replace (st_st s2) with (st_st s0) by congruence.
-        eauto with htlspec.
-      * apply in_map with (f := fst) in H9. 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.
-      * inversion H9.
-        replace (st_st s2) with (st_st s0) by congruence.
-        eauto with htlspec.
-      * apply in_map with (f := fst) in H9. contradiction.
-
-  - 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.
-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 /\ a = z.(st_freshreg) /\ c.(st_freshreg) = Pos.succ (z.(st_freshreg)).
-Proof.
-  inversion 1; split; auto.
-Qed.
-
-Lemma create_reg_inv : forall a b s r s' i,
-    create_reg a b s = OK r s' i ->
-    r = s.(st_freshreg) /\ s'.(st_freshreg) = Pos.succ (s.(st_freshreg)).
-Proof.
-  inversion 1; auto.
-Qed.
-
-Theorem transl_module_correct :
-  forall f m,
-    transl_module f = Errors.OK m -> tr_module f m.
-Proof.
-  intros until m.
-  unfold transl_module.
-  unfold run_mon.
-  destruct (transf_module f (max_state f)) eqn:?; try discriminate.
-  intros. inv H.
-  inversion s; subst.
-
-  unfold transf_module in *.
-  unfold stack_correct in *.
-  destruct (0 <=? RTL.fn_stacksize f) eqn:STACK_BOUND_LOW;
-    destruct (RTL.fn_stacksize f <? Integers.Ptrofs.modulus) eqn:STACK_BOUND_HIGH;
-    destruct (RTL.fn_stacksize f mod 4 =? 0) eqn:STACK_ALIGN;
-    crush;
-    monadInv Heqr.
-
-  repeat unfold_match EQ9. monadInv EQ9.
-
-  (* TODO: We should be able to fold this into the automation. *)
-  pose proof (create_arr_inv _ _ _ _ _ _ _ _ EQ0) as STK_LEN. inv STK_LEN. inv H5.
-  pose proof (create_reg_inv _ _ _ _ _ _ EQ) as FIN_VAL. inv FIN_VAL.
-  pose proof (create_reg_inv _ _ _ _ _ _ EQ1) as RET_VAL. inv RET_VAL.
-  destruct x3. destruct x4.
-  pose proof (collect_trans_instr_freshreg_trans _ _ _ _ _ _ _ EQ2) as TR_INSTR.
-  pose proof (collect_declare_freshreg_trans _ _ _ _ _ _ EQ3) as TR_DEC.
-  pose proof (create_reg_inv _ _ _ _ _ _ EQ4) as START_VAL. inv START_VAL.
-  pose proof (create_reg_inv _ _ _ _ _ _ EQ5) as RESET_VAL. inv RESET_VAL.
-  pose proof (create_reg_inv _ _ _ _ _ _ EQ6) as CLK_VAL. inv CLK_VAL.
-  rewrite H9 in *. rewrite H8 in *. replace (st_freshreg s4) with (st_freshreg s2) in * by congruence.
-  rewrite H6 in *. rewrite H7 in *. rewrite H5 in *. simpl in *.
-  inv_incr.
-  econstructor; simpl; auto; try lia.
-  intros.
-  assert (EQ3D := EQ3).
-  apply collect_declare_datapath_trans in EQ3.
-  apply collect_declare_controllogic_trans in EQ3D.
-  replace (st_controllogic s10) with (st_controllogic s3) by congruence.
-  replace (st_datapath s10) with (st_datapath s3) by congruence.
-  replace (st_st s10) with (st_st s3) by congruence.
-  eapply iter_expand_instr_spec; eauto with htlspec.
-  apply PTree.elements_complete.
-Qed.
+(* Inductive tr_code (c : RTL.code) (pc : RTL.node) (i : RTL.instruction) (stmnts trans : PTree.t stmnt) *)
+(*           (fin rtrn st stk : reg) : Prop := *)
+(*   tr_code_intro : *)
+(*     forall s t, *)
+(*       c!pc = Some i -> *)
+(*       stmnts!pc = Some s -> *)
+(*       trans!pc = Some t -> *)
+(*       tr_instr fin rtrn st stk i s t -> *)
+(*       tr_code c pc i stmnts trans fin rtrn st stk. *)
+(* Hint Constructors tr_code : htlspec. *)
+
+(* Inductive tr_module (f : RTL.function) : module -> Prop := *)
+(*   tr_module_intro : *)
+(*     forall data control fin rtrn st stk stk_len m start rst clk scldecls arrdecls wf, *)
+(*       m = (mkmodule f.(RTL.fn_params) *)
+(*                         data *)
+(*                         control *)
+(*                         f.(RTL.fn_entrypoint) *)
+(*                         st stk stk_len fin rtrn start rst clk scldecls arrdecls wf) -> *)
+(*       (forall pc i, Maps.PTree.get pc f.(RTL.fn_code) = Some i -> *)
+(*                tr_code f.(RTL.fn_code) pc i data control fin rtrn st stk) -> *)
+(*       stk_len = Z.to_nat (f.(RTL.fn_stacksize) / 4) -> *)
+(*       Z.modulo (f.(RTL.fn_stacksize)) 4 = 0 -> *)
+(*       0 <= f.(RTL.fn_stacksize) < Integers.Ptrofs.modulus -> *)
+(*       st = ((RTL.max_reg_function f) + 1)%positive -> *)
+(*       fin = ((RTL.max_reg_function f) + 2)%positive -> *)
+(*       rtrn = ((RTL.max_reg_function f) + 3)%positive -> *)
+(*       stk = ((RTL.max_reg_function f) + 4)%positive -> *)
+(*       start = ((RTL.max_reg_function f) + 5)%positive -> *)
+(*       rst = ((RTL.max_reg_function f) + 6)%positive -> *)
+(*       clk = ((RTL.max_reg_function f) + 7)%positive -> *)
+(*       tr_module f m. *)
+(* Hint Constructors tr_module : htlspec. *)
+
+(* Lemma create_reg_datapath_trans : *)
+(*   forall sz s s' x i iop, *)
+(*     create_reg iop sz s = OK x s' i -> *)
+(*     s.(st_datapath) = s'.(st_datapath). *)
+(* Proof. intros. monadInv H. trivial. Qed. *)
+(* Hint Resolve create_reg_datapath_trans : htlspec. *)
+
+(* Lemma create_reg_controllogic_trans : *)
+(*   forall sz s s' x i iop, *)
+(*     create_reg iop sz s = OK x s' i -> *)
+(*     s.(st_controllogic) = s'.(st_controllogic). *)
+(* Proof. intros. monadInv H. trivial. Qed. *)
+(* Hint Resolve create_reg_controllogic_trans : htlspec. *)
+
+(* Lemma declare_reg_datapath_trans : *)
+(*   forall sz s s' x i iop r, *)
+(*     declare_reg iop r sz s = OK x s' i -> *)
+(*     s.(st_datapath) = s'.(st_datapath). *)
+(* Proof. intros. monadInv H. trivial. Qed. *)
+(* Hint Resolve create_reg_datapath_trans : htlspec. *)
+
+(* Lemma declare_reg_controllogic_trans : *)
+(*   forall sz s s' x i iop r, *)
+(*     declare_reg iop r sz s = OK x s' i -> *)
+(*     s.(st_controllogic) = s'.(st_controllogic). *)
+(* Proof. intros. monadInv H. trivial. Qed. *)
+(* Hint Resolve create_reg_controllogic_trans : htlspec. *)
+
+(* Lemma declare_reg_freshreg_trans : *)
+(*   forall sz s s' x i iop r, *)
+(*     declare_reg iop r sz s = OK x s' i -> *)
+(*     s.(st_freshreg) = s'.(st_freshreg). *)
+(* Proof. inversion 1; auto. Qed. *)
+(* Hint Resolve declare_reg_freshreg_trans : htlspec. *)
+
+(* Lemma create_arr_datapath_trans : *)
+(*   forall sz ln s s' x i iop, *)
+(*     create_arr iop sz ln s = OK x s' i -> *)
+(*     s.(st_datapath) = s'.(st_datapath). *)
+(* Proof. intros. monadInv H. trivial. Qed. *)
+(* Hint Resolve create_arr_datapath_trans : htlspec. *)
+
+(* Lemma create_arr_controllogic_trans : *)
+(*   forall sz ln s s' x i iop, *)
+(*     create_arr iop sz ln s = OK x s' i -> *)
+(*     s.(st_controllogic) = s'.(st_controllogic). *)
+(* Proof. intros. monadInv H. trivial. Qed. *)
+(* Hint Resolve create_arr_controllogic_trans : htlspec. *)
+
+(* Lemma get_refl_x : *)
+(*   forall s s' x i, *)
+(*     get s = OK x s' i -> *)
+(*     s = x. *)
+(* Proof. inversion 1. trivial. Qed. *)
+(* Hint Resolve get_refl_x : htlspec. *)
+
+(* Lemma get_refl_s : *)
+(*   forall s s' x i, *)
+(*     get s = OK x s' i -> *)
+(*     s = s'. *)
+(* Proof. inversion 1. trivial. Qed. *)
+(* Hint Resolve get_refl_s : htlspec. *)
+
+(* Ltac inv_incr := *)
+(*   repeat match goal with *)
+(*   | [ H: create_reg _ _ ?s = OK _ ?s' _ |- _ ] => *)
+(*     let H1 := fresh "H" in *)
+(*     assert (H1 := H); eapply create_reg_datapath_trans in H; *)
+(*     eapply create_reg_controllogic_trans in H1 *)
+(*   | [ H: create_arr _ _ _ ?s = OK _ ?s' _ |- _ ] => *)
+(*     let H1 := fresh "H" in *)
+(*     assert (H1 := H); eapply create_arr_datapath_trans in H; *)
+(*     eapply create_arr_controllogic_trans in H1 *)
+(*   | [ H: get ?s = OK _ _ _ |- _ ] => *)
+(*     let H1 := fresh "H" in *)
+(*     assert (H1 := H); apply get_refl_x in H; apply get_refl_s in H1; *)
+(*     subst *)
+(*   | [ H: st_prop _ _ |- _ ] => unfold st_prop in H; destruct H *)
+(*   | [ H: st_incr _ _ |- _ ] => destruct st_incr *)
+(*   end. *)
+
+(* Lemma collect_controllogic_trans : *)
+(*   forall A f l cs cs' ci, *)
+(*   (forall s s' x i y, f y s = OK x s' i -> s.(st_controllogic) = s'.(st_controllogic)) -> *)
+(*   @HTLMonadExtra.collectlist A f l cs = OK tt cs' ci -> cs.(st_controllogic) = cs'.(st_controllogic). *)
+(* Proof. *)
+(*   induction l; intros; monadInv H0. *)
+(*   - trivial. *)
+(*   - apply H in EQ. rewrite EQ. eauto. *)
+(* Qed. *)
+
+(* Lemma collect_datapath_trans : *)
+(*   forall A f l cs cs' ci, *)
+(*   (forall s s' x i y, f y s = OK x s' i -> s.(st_datapath) = s'.(st_datapath)) -> *)
+(*   @HTLMonadExtra.collectlist A f l cs = OK tt cs' ci -> cs.(st_datapath) = cs'.(st_datapath). *)
+(* Proof. *)
+(*   induction l; intros; monadInv H0. *)
+(*   - trivial. *)
+(*   - apply H in EQ. rewrite EQ. eauto. *)
+(* Qed. *)
+
+(* Lemma collect_freshreg_trans : *)
+(*   forall A f l cs cs' ci, *)
+(*   (forall s s' x i y, f y s = OK x s' i -> s.(st_freshreg) = s'.(st_freshreg)) -> *)
+(*   @HTLMonadExtra.collectlist A f l cs = OK tt cs' ci -> cs.(st_freshreg) = cs'.(st_freshreg). *)
+(* Proof. *)
+(*   induction l; intros; monadInv H0. *)
+(*   - trivial. *)
+(*   - apply H in EQ. rewrite EQ. eauto. *)
+(* Qed. *)
+
+(* Lemma collect_declare_controllogic_trans : *)
+(*   forall io n l s s' i, *)
+(*   HTLMonadExtra.collectlist (fun r : reg => declare_reg io r n) l s = OK tt s' i -> *)
+(*   s.(st_controllogic) = s'.(st_controllogic). *)
+(* Proof. *)
+(*   intros. eapply collect_controllogic_trans; try eassumption. *)
+(*   intros. eapply declare_reg_controllogic_trans. simpl in H0. eassumption. *)
+(* Qed. *)
+
+(* Lemma collect_declare_datapath_trans : *)
+(*   forall io n l s s' i, *)
+(*   HTLMonadExtra.collectlist (fun r : reg => declare_reg io r n) l s = OK tt s' i -> *)
+(*   s.(st_datapath) = s'.(st_datapath). *)
+(* Proof. *)
+(*   intros. eapply collect_datapath_trans; try eassumption. *)
+(*   intros. eapply declare_reg_datapath_trans. simpl in H0. eassumption. *)
+(* Qed. *)
+
+(* Lemma collect_declare_freshreg_trans : *)
+(*   forall io n l s s' i, *)
+(*   HTLMonadExtra.collectlist (fun r : reg => declare_reg io r n) l s = OK tt s' i -> *)
+(*   s.(st_freshreg) = s'.(st_freshreg). *)
+(* Proof. *)
+(*   intros. eapply collect_freshreg_trans; try eassumption. *)
+(*   inversion 1. auto. *)
+(* Qed. *)
+
+(* Ltac unfold_match H := *)
+(*   match type of H with *)
+(*   | context[match ?g with _ => _ end] => destruct g eqn:?; try discriminate *)
+(*   end. *)
+
+(* Lemma translate_eff_addressing_freshreg_trans : *)
+(*   forall op args s r s' i, *)
+(*   translate_eff_addressing op args s = OK r s' i -> *)
+(*   s.(st_freshreg) = s'.(st_freshreg). *)
+(* Proof. *)
+(*   destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto. *)
+(* Qed. *)
+(* Hint Resolve translate_eff_addressing_freshreg_trans : htlspec. *)
+
+(* Lemma translate_comparison_freshreg_trans : *)
+(*   forall op args s r s' i, *)
+(*   translate_comparison op args s = OK r s' i -> *)
+(*   s.(st_freshreg) = s'.(st_freshreg). *)
+(* Proof. *)
+(*   destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto. *)
+(* Qed. *)
+(* Hint Resolve translate_comparison_freshreg_trans : htlspec. *)
+
+(* Lemma translate_comparison_imm_freshreg_trans : *)
+(*   forall op args s r s' i n, *)
+(*   translate_comparison_imm op args n s = OK r s' i -> *)
+(*   s.(st_freshreg) = s'.(st_freshreg). *)
+(* Proof. *)
+(*   destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto. *)
+(* Qed. *)
+(* Hint Resolve translate_comparison_imm_freshreg_trans : htlspec. *)
+
+(* Lemma translate_condition_freshreg_trans : *)
+(*   forall op args s r s' i, *)
+(*   translate_condition op args s = OK r s' i -> *)
+(*   s.(st_freshreg) = s'.(st_freshreg). *)
+(* Proof. *)
+(*   destruct op; intros; simpl in *; repeat (unfold_match H); inv H; eauto with htlspec. *)
+(* Qed. *)
+(* Hint Resolve translate_condition_freshreg_trans : htlspec. *)
+
+(* Lemma translate_instr_freshreg_trans : *)
+(*   forall op args s r s' i, *)
+(*   translate_instr op args s = OK r s' i -> *)
+(*   s.(st_freshreg) = s'.(st_freshreg). *)
+(* Proof. *)
+(*   destruct op; intros; simpl in *; repeat (unfold_match H); inv H; eauto with htlspec. *)
+(*   monadInv H1. eauto with htlspec. *)
+(* Qed. *)
+(* Hint Resolve translate_instr_freshreg_trans : htlspec. *)
+
+(* Lemma translate_arr_access_freshreg_trans : *)
+(*   forall mem addr args st s r s' i, *)
+(*   translate_arr_access mem addr args st s = OK r s' i -> *)
+(*   s.(st_freshreg) = s'.(st_freshreg). *)
+(* Proof. *)
+(*   intros. unfold translate_arr_access in H. repeat (unfold_match H); inv H; eauto with htlspec. *)
+(* Qed. *)
+(* Hint Resolve translate_arr_access_freshreg_trans : htlspec. *)
+
+(* Lemma add_instr_freshreg_trans : *)
+(*   forall n n' st s r s' i, *)
+(*   add_instr n n' st s = OK r s' i -> *)
+(*   s.(st_freshreg) = s'.(st_freshreg). *)
+(* Proof. intros. unfold add_instr in H. repeat (unfold_match H). inv H. auto. Qed. *)
+(* Hint Resolve add_instr_freshreg_trans : htlspec. *)
+
+(* Lemma add_branch_instr_freshreg_trans : *)
+(*   forall n n0 n1 e s r s' i, *)
+(*   add_branch_instr e n n0 n1 s = OK r s' i -> *)
+(*   s.(st_freshreg) = s'.(st_freshreg). *)
+(* Proof. intros. unfold add_branch_instr in H. repeat (unfold_match H). inv H. auto. Qed. *)
+(* Hint Resolve add_branch_instr_freshreg_trans : htlspec. *)
+
+(* Lemma add_node_skip_freshreg_trans : *)
+(*   forall n1 n2 s r s' i, *)
+(*   add_node_skip n1 n2 s = OK r s' i -> *)
+(*   s.(st_freshreg) = s'.(st_freshreg). *)
+(* Proof. intros. unfold add_node_skip in H. repeat (unfold_match H). inv H. auto. Qed. *)
+(* Hint Resolve add_node_skip_freshreg_trans : htlspec. *)
+
+(* Lemma add_instr_skip_freshreg_trans : *)
+(*   forall n1 n2 s r s' i, *)
+(*   add_instr_skip n1 n2 s = OK r s' i -> *)
+(*   s.(st_freshreg) = s'.(st_freshreg). *)
+(* Proof. intros. unfold add_instr_skip in H. repeat (unfold_match H). inv H. auto. Qed. *)
+(* Hint Resolve add_instr_skip_freshreg_trans : htlspec. *)
+
+(* Lemma transf_instr_freshreg_trans : *)
+(*   forall fin ret st instr s v s' i, *)
+(*     transf_instr fin ret st instr s = OK v s' i -> *)
+(*     s.(st_freshreg) = s'.(st_freshreg). *)
+(* Proof. *)
+(*   intros. destruct instr eqn:?. subst. unfold transf_instr in H. *)
+(*   destruct i0; try (monadInv H); try (unfold_match H); eauto with htlspec. *)
+(*   - apply add_instr_freshreg_trans in EQ2. apply translate_instr_freshreg_trans in EQ. *)
+(*     apply declare_reg_freshreg_trans in EQ1. congruence. *)
+(*   - apply add_instr_freshreg_trans in EQ2. apply translate_arr_access_freshreg_trans in EQ. *)
+(*     apply declare_reg_freshreg_trans in EQ1. congruence. *)
+(*   - apply add_instr_freshreg_trans in EQ0. apply translate_arr_access_freshreg_trans in EQ. congruence. *)
+(*   - apply translate_condition_freshreg_trans in EQ. apply add_branch_instr_freshreg_trans in EQ0. *)
+(*     congruence. *)
+(*   - inv EQ. apply add_node_skip_freshreg_trans in EQ0. congruence. *)
+(* Qed. *)
+(* Hint Resolve transf_instr_freshreg_trans : htlspec. *)
+
+(* Lemma collect_trans_instr_freshreg_trans : *)
+(*   forall fin ret st l s s' i, *)
+(*   HTLMonadExtra.collectlist (transf_instr fin ret st) l s = OK tt s' i -> *)
+(*   s.(st_freshreg) = s'.(st_freshreg). *)
+(* Proof. *)
+(*   intros. eapply collect_freshreg_trans; try eassumption. *)
+(*   eauto with htlspec. *)
+(* Qed. *)
+
+(* Ltac rewrite_states := *)
+(*   match goal with *)
+(*   | [ H: ?x ?s = ?x ?s' |- _ ] => *)
+(*     let c1 := fresh "c" in *)
+(*     let c2 := fresh "c" in *)
+(*     remember (?x ?s) as c1; remember (?x ?s') as c2; try subst *)
+(*   end. *)
+
+(* Ltac inv_add_instr' H := *)
+(*   match type of H with *)
+(*   | ?f _ _ _ = OK _ _ _ => unfold f in H *)
+(*   | ?f _ _ _ _ = OK _ _ _ => unfold f in H *)
+(*   | ?f _ _ _ _ _ = OK _ _ _ => unfold f in H *)
+(*   end; repeat unfold_match H; inversion H. *)
+
+(* Ltac inv_add_instr := *)
+(*   lazymatch goal with *)
+(*   | H: context[add_instr_skip _ _ _] |- _ => *)
+(*     inv_add_instr' H *)
+(*   | H: context[add_instr_skip _ _] |- _ => *)
+(*     monadInv H; inv_incr; inv_add_instr *)
+(*   | H: context[add_instr _ _ _ _] |- _ => *)
+(*     inv_add_instr' H *)
+(*   | H: context[add_instr _ _ _] |- _ => *)
+(*     monadInv H; inv_incr; inv_add_instr *)
+(*   | H: context[add_branch_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 := *)
+(*   match goal with H: option ?r |- _ => destruct H end. *)
+
+(* Lemma iter_expand_instr_spec : *)
+(*   forall l fin rtrn stack s s' i x c, *)
+(*     HTLMonadExtra.collectlist (transf_instr fin rtrn stack) l s = OK x s' i -> *)
+(*     list_norepet (List.map fst l) -> *)
+(*     (forall pc instr, In (pc, instr) l -> c!pc = Some instr) -> *)
+(*     (forall pc instr, In (pc, instr) l -> *)
+(*                       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. *)
+(*   destruct a as [pc1 instr1]; simpl in *. inv H0. monadInv H. inv_incr. *)
+(*   destruct (peq pc pc1). *)
+(*   - subst. *)
+(*     destruct instr1 eqn:?; try discriminate; *)
+(*       try destruct_optional; inv_add_instr; econstructor; try assumption. *)
+(*     + 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. inversion H9. rewrite H. apply tr_instr_Inop. *)
+(*       eapply in_map with (f := fst) in H9. 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. 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. 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. *)
+(*     + destruct H2. *)
+(*       * inversion H2. *)
+(*         replace (st_st s2) with (st_st s0) by congruence. *)
+(*         eauto with htlspec. *)
+(*       * apply in_map with (f := fst) in H2. 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. *)
+(*     + destruct H2. *)
+(*       * inversion H2. *)
+(*         replace (st_st s2) with (st_st s0) by congruence. *)
+(*         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. *)
+(*       * inversion H9. *)
+(*         replace (st_st s2) with (st_st s0) by congruence. *)
+(*         eauto with htlspec. *)
+(*       * apply in_map with (f := fst) in H9. 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. *)
+(*       * inversion H9. *)
+(*         replace (st_st s2) with (st_st s0) by congruence. *)
+(*         eauto with htlspec. *)
+(*       * apply in_map with (f := fst) in H9. contradiction. *)
+
+(*   - 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. *)
+(* 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 /\ a = z.(st_freshreg) /\ c.(st_freshreg) = Pos.succ (z.(st_freshreg)). *)
+(* Proof. *)
+(*   inversion 1; split; auto. *)
+(* Qed. *)
+
+(* Lemma create_reg_inv : forall a b s r s' i, *)
+(*     create_reg a b s = OK r s' i -> *)
+(*     r = s.(st_freshreg) /\ s'.(st_freshreg) = Pos.succ (s.(st_freshreg)). *)
+(* Proof. *)
+(*   inversion 1; auto. *)
+(* Qed. *)
+
+(* Theorem transl_module_correct : *)
+(*   forall f m, *)
+(*     transl_module f = Errors.OK m -> tr_module f m. *)
+(* Proof. *)
+(*   intros until m. *)
+(*   unfold transl_module. *)
+(*   unfold run_mon. *)
+(*   destruct (transf_module f (max_state f)) eqn:?; try discriminate. *)
+(*   intros. inv H. *)
+(*   inversion s; subst. *)
+
+(*   unfold transf_module in *. *)
+(*   unfold stack_correct in *. *)
+(*   destruct (0 <=? RTL.fn_stacksize f) eqn:STACK_BOUND_LOW; *)
+(*     destruct (RTL.fn_stacksize f <? Integers.Ptrofs.modulus) eqn:STACK_BOUND_HIGH; *)
+(*     destruct (RTL.fn_stacksize f mod 4 =? 0) eqn:STACK_ALIGN; *)
+(*     crush; *)
+(*     monadInv Heqr. *)
+
+(*   repeat unfold_match EQ9. monadInv EQ9. *)
+
+(*   (* TODO: We should be able to fold this into the automation. *) *)
+(*   pose proof (create_arr_inv _ _ _ _ _ _ _ _ EQ0) as STK_LEN. inv STK_LEN. inv H5. *)
+(*   pose proof (create_reg_inv _ _ _ _ _ _ EQ) as FIN_VAL. inv FIN_VAL. *)
+(*   pose proof (create_reg_inv _ _ _ _ _ _ EQ1) as RET_VAL. inv RET_VAL. *)
+(*   destruct x3. destruct x4. *)
+(*   pose proof (collect_trans_instr_freshreg_trans _ _ _ _ _ _ _ EQ2) as TR_INSTR. *)
+(*   pose proof (collect_declare_freshreg_trans _ _ _ _ _ _ EQ3) as TR_DEC. *)
+(*   pose proof (create_reg_inv _ _ _ _ _ _ EQ4) as START_VAL. inv START_VAL. *)
+(*   pose proof (create_reg_inv _ _ _ _ _ _ EQ5) as RESET_VAL. inv RESET_VAL. *)
+(*   pose proof (create_reg_inv _ _ _ _ _ _ EQ6) as CLK_VAL. inv CLK_VAL. *)
+(*   rewrite H9 in *. rewrite H8 in *. replace (st_freshreg s4) with (st_freshreg s2) in * by congruence. *)
+(*   rewrite H6 in *. rewrite H7 in *. rewrite H5 in *. simpl in *. *)
+(*   inv_incr. *)
+(*   econstructor; simpl; auto; try lia. *)
+(*   intros. *)
+(*   assert (EQ3D := EQ3). *)
+(*   apply collect_declare_datapath_trans in EQ3. *)
+(*   apply collect_declare_controllogic_trans in EQ3D. *)
+(*   replace (st_controllogic s10) with (st_controllogic s3) by congruence. *)
+(*   replace (st_datapath s10) with (st_datapath s3) by congruence. *)
+(*   replace (st_st s10) with (st_st s3) by congruence. *)
+(*   eapply iter_expand_instr_spec; eauto with htlspec. *)
+(*   apply PTree.elements_complete. *)
+(* Qed. *)
diff --git a/src/verilog/PrintHTL.ml b/src/verilog/PrintHTL.ml
index 0bdba51..36fdd3c 100644
--- a/src/verilog/PrintHTL.ml
+++ b/src/verilog/PrintHTL.ml
@@ -16,7 +16,7 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-open Value
+open ValueInt
 open Datatypes
 open Camlcoq
 open AST
diff --git a/src/verilog/PrintVerilog.ml b/src/verilog/PrintVerilog.ml
index 5265c97..db78ad5 100644
--- a/src/verilog/PrintVerilog.ml
+++ b/src/verilog/PrintVerilog.ml
@@ -17,7 +17,7 @@
  *)
 
 open Verilog
-open Value
+open ValueInt
 open Datatypes
 
 open Camlcoq
@@ -70,11 +70,17 @@ let unop = function
 
 let register a = sprintf "reg_%d" (P.to_int a)
 
-let literal l = sprintf "%d'd%d" (Nat.to_int l.vsize) (Z.to_int (uvalueToZ l))
+let literal l = sprintf "32'd%d" (Z.to_int (uvalueToZ l))
+
+let byte n s = sprintf "reg_%d[%d:%d]" (P.to_int s) (7 + n * 8) (n * 8)
 
 let rec pprint_expr = function
   | Vlit l -> literal l
   | Vvar s -> register s
+  | Vvarb0 s -> byte 0 s
+  | Vvarb1 s -> byte 1 s
+  | Vvarb2 s -> byte 2 s
+  | Vvarb3 s -> byte 3 s
   | Vvari (s, i) -> concat [register s; "["; pprint_expr i; "]"]
   | Vinputvar s -> register s
   | Vunop (u, e) -> concat ["("; unop u; pprint_expr e; ")"]
diff --git a/src/verilog/PrintVerilog.mli b/src/verilog/PrintVerilog.mli
index 62bf63f..5fd8fe9 100644
--- a/src/verilog/PrintVerilog.mli
+++ b/src/verilog/PrintVerilog.mli
@@ -18,8 +18,8 @@
 
 val pprint_stmnt : int -> Verilog.stmnt -> string
 
-val print_value : out_channel -> Value.value -> unit
+val print_value : out_channel -> ValueInt.value -> unit
 
 val print_program : bool -> out_channel -> Verilog.program -> unit
 
-val print_result : out_channel -> (BinNums.positive * Value.value) list -> unit
+val print_result : out_channel -> (BinNums.positive * ValueInt.value) list -> unit
diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v
index 064474a..921d9fd 100644
--- a/src/verilog/Verilog.v
+++ b/src/verilog/Verilog.v
@@ -29,7 +29,7 @@ Require Import Lia.
 
 Import ListNotations.
 
-From coqup Require Import common.Coquplib common.Show verilog.ValueInt AssocMap Array.
+From coqup Require Import common.Coquplib common.Show verilog.ValueInt IntegerExtra AssocMap Array.
 From compcert Require Events.
 From compcert Require Import Integers Errors Smallstep Globalenvs.
 
@@ -154,9 +154,13 @@ Inductive unop : Type :=
 (** ** Expressions *)
 
 Inductive expr : Type :=
-| Vlit : value -> expr
-| Vvar : reg -> expr
-| Vvari : reg -> expr -> expr
+| Vlit : value -> expr                    (** literal *)
+| Vvar : reg -> expr                      (** reg *)
+| Vvarb0 : reg -> expr                    (** 1st byte projection of reg *)
+| Vvarb1 : reg -> expr
+| Vvarb2 : reg -> expr
+| Vvarb3 : reg -> expr
+| Vvari : reg -> expr -> expr              (** array *)
 | Vinputvar : reg -> expr
 | Vbinop : binop -> expr -> expr -> expr
 | Vunop : unop -> expr -> expr
@@ -340,6 +344,22 @@ Inductive expr_runp : fext -> assocmap -> assocmap_arr -> expr -> value -> Prop
       forall fext reg stack v r,
       reg#r = v ->
       expr_runp fext reg stack (Vvar r) v
+  | erun_Vvarb0 :
+      forall fext reg stack v r,
+      reg#r = v ->
+      expr_runp fext reg stack (Vvarb0 r) (IntExtra.ibyte0 v)
+  | erun_Vvarb1 :
+      forall fext reg stack v r,
+      reg#r = v ->
+      expr_runp fext reg stack (Vvarb1 r) (IntExtra.ibyte1 v)
+  | erun_Vvarb2 :
+      forall fext reg stack v r,
+      reg#r = v ->
+      expr_runp fext reg stack (Vvarb2 r) (IntExtra.ibyte2 v)
+  | erun_Vvarb3 :
+      forall fext reg stack v r,
+      reg#r = v ->
+      expr_runp fext reg stack (Vvarb3 r) (IntExtra.ibyte3 v)
   | erun_Vvari :
       forall fext reg stack v iexp i r,
       expr_runp fext reg stack iexp i ->
@@ -429,6 +449,7 @@ Definition access_fext (f : fext) (r : reg) : res value :=
 
 Inductive location : Type :=
 | LocReg (_ : reg)
+| LocRegB (_ : reg) (_ : nat)
 | LocArray (_ : reg) (_ : nat).
 
 Inductive location_is : fext -> assocmap -> assocmap_arr -> expr -> location -> Prop :=
@@ -775,6 +796,10 @@ Proof.
   repeat (try match goal with
               | [ H : expr_runp _ _ _ (Vlit _) _ |- _ ] => invert H
               | [ H : expr_runp _ _ _ (Vvar _) _ |- _ ] => invert H
+              | [ H : expr_runp _ _ _ (Vvarb0 _) _ |- _ ] => invert H
+              | [ H : expr_runp _ _ _ (Vvarb1 _) _ |- _ ] => invert H
+              | [ H : expr_runp _ _ _ (Vvarb2 _) _ |- _ ] => invert H
+              | [ H : expr_runp _ _ _ (Vvarb3 _) _ |- _ ] => invert H
               | [ H : expr_runp _ _ _ (Vvari _ _) _ |- _ ] => invert H
               | [ H : expr_runp _ _ _ (Vinputvar _) _ |- _ ] => invert H
               | [ H : expr_runp _ _ _ (Vbinop _ _ _) _ |- _ ] => invert H