From 502e49e2f8c95b40cd0761cbb69c863904169f8b Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Sat, 29 Jul 2023 13:49:03 +0100
Subject: Add beginning to memory generation proof

---
 src/hls/HTLgenproof.v | 2843 +++++++++++++++++++++++++------------------------
 1 file changed, 1477 insertions(+), 1366 deletions(-)

(limited to 'src/hls/HTLgenproof.v')

diff --git a/src/hls/HTLgenproof.v b/src/hls/HTLgenproof.v
index 272a434..75ee2fb 100644
--- a/src/hls/HTLgenproof.v
+++ b/src/hls/HTLgenproof.v
@@ -34,7 +34,6 @@ Require vericert.hls.HTL.
 Require Import vericert.hls.HTLgen.
 Require Import vericert.hls.HTLgenspec.
 Require Import vericert.hls.ValueInt.
-Require Import vericert.hls.FunctionalUnits.
 Require vericert.hls.Verilog.
 
 Require Import Lia.
@@ -63,10 +62,10 @@ Definition state_st_wf (m : HTL.module) (s : HTL.state) :=
 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_ram).(ram_mem)) = Some stack /\
+    asa ! (m.(HTL.mod_stk)) = Some stack /\
     stack.(arr_length) = Z.to_nat (f.(RTL.fn_stacksize) / 4) /\
     (forall ptr,
-        0 <= ptr < Z.of_nat m.(HTL.mod_ram).(ram_size) ->
+        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)
@@ -406,7 +405,7 @@ Section CORRECTNESS.
   Lemma op_stack_based :
     forall F V sp v m args rs op ge pc' res0 pc f e fin rtrn st stk,
       tr_instr fin rtrn st stk (RTL.Iop op args res0 pc')
-               (Verilog.Vblock (Verilog.Vvar res0) e)
+               (Verilog.Vnonblock (Verilog.Vvar res0) e)
                (state_goto st pc') ->
       reg_stack_based_pointers sp rs ->
       (RTL.fn_code f) ! pc = Some (RTL.Iop op args res0 pc') ->
@@ -1004,42 +1003,40 @@ Section CORRECTNESS.
         constructor.
   Qed.
 
-(*|
-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``.
-|*)
+  (** 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_ram).(ram_mem)) instr stmt trans ->
+      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 name_goal name := refine ?[name].
+
+Ltac unfold_merge :=
+  unfold merge_assocmap; repeat (rewrite AssocMapExt.merge_add_assoc);
+  try (rewrite AssocMapExt.merge_base_1).
 
   Ltac tac0 :=
     match goal with
     | [ |- HTL.exec_ram _ _ _ _ _ ] => constructor
-    | [ |- 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[Verilog.merge_regs _ _] ] => unfold Verilog.merge_regs; cbn; 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
 
@@ -1071,11 +1068,97 @@ rs assoc``.
     | [ H : opt_val_value_lessdef _ _ |- _ ] => inv H
     | [ H : context[Z.of_nat (Z.to_nat _)] |- _ ] => rewrite Z2Nat.id in H; [> solve crush |]
     | [ H : _ ! _ = Some _ |- _] => setoid_rewrite H
+    | [ |- context[AssocMapExt.merge]] => progress unfold_merge
     end.
 
+  Ltac simplify_local := intros; unfold_constants; cbn in *;
+                         repeat (nicify_hypotheses; nicify_goals; kill_bools; substpp);
+                         cbn in *.
+
+  Ltac simplify_val := repeat (simplify_local; unfold uvalueToZ, valueToPtr, Ptrofs.of_int, valueToInt, intToValue,
+                                 ptrToValue in *).
+
+                               Ltac crush_val := simplify_val; try discriminate; try congruence; try lia; liapp; try assumption.
+
   Ltac small_tac := repeat (crush_val; try array; try ptrofs); crush_val; auto.
   Ltac big_tac := repeat (crush_val; try array; try ptrofs; try tac0); crush_val; auto.
 
+  Lemma merge_get_default :
+    forall ars ars' r x,
+      ars ! r = Some x ->
+      (AssocMapExt.merge _ ars ars') # r = x.
+  Proof.
+    unfold AssocMapExt.merge; intros.
+    unfold "#", AssocMapExt.get_default.
+    rewrite AssocMap.gcombine by auto.
+    unfold AssocMapExt.merge_atom. 
+    now rewrite !H.
+  Qed.
+
+  Lemma merge_get_default2 :
+    forall ars ars' r,
+      ars ! r = None ->
+      (AssocMapExt.merge _ ars ars') # r = ars' # r.
+  Proof.
+    unfold AssocMapExt.merge; intros.
+    unfold "#", AssocMapExt.get_default.
+    rewrite AssocMap.gcombine by auto.
+    unfold AssocMapExt.merge_atom. 
+    now rewrite !H.
+  Qed.
+
+  Lemma merge_get_default3 :
+    forall A ars ars' r,
+      ars ! r = None ->
+      (AssocMapExt.merge A ars ars') ! r = ars' ! r.
+  Proof.
+    unfold AssocMapExt.merge; intros.
+    unfold "#", AssocMapExt.get_default.
+    rewrite AssocMap.gcombine by auto.
+    unfold AssocMapExt.merge_atom.
+    now rewrite !H.
+  Qed.
+
+  Lemma merge_get_default4 :
+    forall A ars ars' r x,
+      ars ! r = Some x ->
+      (AssocMapExt.merge A ars ars') ! r = Some x.
+  Proof.
+    unfold AssocMapExt.merge; intros.
+    unfold "#", AssocMapExt.get_default.
+    rewrite AssocMap.gcombine by auto.
+    unfold AssocMapExt.merge_atom. 
+    now rewrite !H.
+  Qed.
+
+  Lemma match_assocmaps_merge_empty:
+    forall f rs ars,
+      match_assocmaps f rs ars ->
+      match_assocmaps f rs (AssocMapExt.merge value empty_assocmap ars).
+  Proof.
+    inversion 1; subst; clear H.
+    constructor; intros.
+    rewrite merge_get_default2; auto.
+  Qed.
+
+  Opaque AssocMap.get.
+  Opaque AssocMap.set.
+  Opaque AssocMapExt.merge.
+  Opaque Verilog.merge_arr.
+
+  Lemma match_assocmaps_ext :
+    forall f rs ars1 ars2,
+      (forall x, Ple x (RTL.max_reg_function f) -> ars1 ! x = ars2 ! x) ->
+      match_assocmaps f rs ars1 ->
+      match_assocmaps f rs ars2.
+  Proof.
+    intros * YFRL YMATCH.
+    inv YMATCH. constructor; intros x' YPLE.
+    unfold "#", AssocMapExt.get_default in *. 
+    rewrite <- YFRL by auto.
+    eauto.
+  Qed.
+
   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),
@@ -1094,17 +1177,33 @@ rs assoc``.
     apply Smallstep.plus_one.
     eapply HTL.step_module; eauto.
     inv CONST; assumption.
-    inv CONST; assumption.
+    inv CONST; assumption. 
     (* processing of state *)
     econstructor.
-    (* crush. *)
-    (* econstructor. *)
-    (* econstructor. *)
-    (* econstructor. *)
-
-    (* all: inv MARR; big_tac. *) Abort.
-
-(*    inv CONST; constructor; simplify; rewrite AssocMap.gso; auto; lia.
+    crush.
+    econstructor.
+    econstructor.
+    econstructor.
+    big_tac.
+    cbn.
+
+    solve [inv MARR; big_tac].
+
+    (* inv MARR; big_tac. *)
+    inv MARR; big_tac; auto.
+
+    - eapply match_assocmaps_ext; [|eauto]; intros.
+      repeat unfold_merge. rewrite AssocMap.gso by (unfold Ple in *; lia).
+      rewrite AssocMapExt.merge_base_1; auto.
+    - rewrite <- H1. unfold Verilog.merge_arrs.
+      rewrite !AssocMap.gcombine by auto. rewrite !AssocMap.gss.
+      setoid_rewrite H1.
+      repeat erewrite Verilog.merge_arr_empty2; eauto.
+    - inv CONST; cbn in *. constructor; cbn in *. 
+      + repeat unfold_merge. rewrite AssocMap.gso by lia.
+        unfold_merge; auto.
+      + repeat unfold_merge. rewrite AssocMap.gso by lia.
+        unfold_merge; auto.
 
     Unshelve. exact tt.
   Qed.
@@ -1138,27 +1237,38 @@ rs assoc``.
 
     all: big_tac.
 
-    assert (HPle: Ple res0 (RTL.max_reg_function f))
+    - assert (HPle: Ple res0 (RTL.max_reg_function f))
         by (eapply RTL.max_reg_function_def; eauto; simpl; auto).
-
-    unfold Ple in HPle. lia.
-    apply regs_lessdef_add_match. assumption.
-    apply regs_lessdef_add_greater. unfold Plt; lia. assumption.
-    assert (HPle: Ple res0 (RTL.max_reg_function f))
+      unfold Ple in HPle. lia.
+    - eapply match_assocmaps_merge_empty. eapply match_assocmaps_ext; intros.
+      unfold Ple in *. instantiate (1 := asr # res0 <- x).
+      destruct (peq res0 x1); subst.
+      + rewrite merge_get_default4 with (x := x);
+        apply AssocMap.gss.
+      + rewrite merge_get_default3; [now rewrite AssocMap.gso by auto|].
+        rewrite AssocMap.gso by auto.
+        now rewrite AssocMap.gso by lia.
+      + now apply regs_lessdef_add_match.
+    - assert (HPle: Ple res0 (RTL.max_reg_function f))
         by (eapply RTL.max_reg_function_def; eauto; simpl; auto).
-    unfold Ple in HPle; lia.
-    eapply op_stack_based; eauto.
-    inv CONST. constructor; simplify. rewrite AssocMap.gso. rewrite AssocMap.gso.
-    assumption. lia.
-    assert (HPle: Ple res0 (RTL.max_reg_function f))
-      by (eapply RTL.max_reg_function_def; eauto; simpl; auto).
-    unfold Ple in HPle. lia.
-    rewrite AssocMap.gso. rewrite AssocMap.gso.
-    assumption. lia.
-    assert (HPle: Ple res0 (RTL.max_reg_function f))
-      by (eapply RTL.max_reg_function_def; eauto; simpl; auto).
-    unfold Ple in HPle. lia.
-    Unshelve. exact tt.
+      unfold Ple in HPle. lia.
+    - unfold Verilog.merge_arrs.
+      rewrite ! AssocMap.gcombine by auto. rewrite ! AssocMap.gss.
+      erewrite ! Verilog.merge_arr_empty2; eauto.
+      erewrite ! Verilog.merge_arr_empty2; eauto.
+    - assumption.
+    - eapply op_stack_based; eauto.
+    - assert (HPle: Ple res0 (RTL.max_reg_function f))
+        by (eapply RTL.max_reg_function_def; eauto; simpl; auto).
+      unfold Ple in *.
+      inv CONST. constructor; cbn.
+      repeat rewrite merge_get_default3 by solve [auto | lia].
+      rewrite merge_get_default3; [eauto | ].
+      repeat rewrite AssocMap.gso by solve [auto | lia]. auto.
+      repeat rewrite merge_get_default3 by solve [auto | lia].
+      rewrite merge_get_default3; [eauto | ].
+      repeat rewrite AssocMap.gso by solve [auto | lia]. auto.
+      Unshelve. apply tt.
   Qed.
   #[local] Hint Resolve transl_iop_correct : htlproof.
 
@@ -1266,373 +1376,374 @@ rs assoc``.
           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 *)
-      inv MARR. inv CONST. 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'.
-      inv 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 H0 in HPler0.
-      inv HPler0; try congruence.
-      rewrite EQr0 in H11.
-      inv H11.
-
-      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.
-      { apply Mem.load_valid_access in H1. unfold Mem.valid_access in *. simplify.
-        apply Zdivide_mod. assumption. }
-
-      (** 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 (HDIV: forall x y, Integers.Ptrofs.divu x y = Integers.Ptrofs.divu x y ) by reflexivity.
-        unfold Integers.Ptrofs.divu at 2 in HDIV.
-        rewrite HDIV. clear HDIV.
-        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.
-      econstructor. econstructor. econstructor. crush.
-      econstructor. econstructor. econstructor. crush.
-      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 *)
-      rewrite <- offset_expr_ok.
-
-      specialize (H9 (Integers.Ptrofs.unsigned
-                        (Integers.Ptrofs.divu
-                           OFFSET
-                           (Integers.Ptrofs.repr 4)))).
-      exploit H9; 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 H14. rewrite HeqOFFSET in H14. rewrite H1 in H14. assumption.
-      constructor; simplify. rewrite AssocMap.gso. rewrite AssocMap.gso.
-      assumption. lia.
-      assert (HPle: Ple dst (RTL.max_reg_function f))
-        by (eapply RTL.max_reg_function_def; eauto; simpl; auto).
-      unfold Ple in HPle. lia.
-      rewrite AssocMap.gso. rewrite AssocMap.gso.
-      assumption. lia.
-      assert (HPle: Ple dst (RTL.max_reg_function f))
-        by (eapply RTL.max_reg_function_def; eauto; simpl; auto).
-      unfold Ple in HPle. lia.
-    + (** Preamble *)
-      inv MARR. inv CONST. 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'.
-      inv 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 H8 in HPler0.
-      apply H11 in HPler1.
-      inv HPler0; inv HPler1; try congruence.
-      rewrite EQr0 in H13.
-      rewrite EQr1 in H14.
-      inv H13. inv H14.
-      clear H0. clear H8. clear H11.
-
-      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.
-      { apply Mem.load_valid_access in H1. unfold Mem.valid_access in *. simplify.
-        apply Zdivide_mod. assumption. }
-
-      (** 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 H14.
-        rewrite H14. clear H14.
-        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.
-      econstructor. econstructor. econstructor. crush.
-      econstructor. econstructor. econstructor. crush.
-      econstructor. econstructor. econstructor.
-      econstructor. econstructor. econstructor. econstructor.
-      econstructor. econstructor. auto. 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 *)
-      rewrite <- offset_expr_ok_2.
-
-      specialize (H9 (Integers.Ptrofs.unsigned
-                        (Integers.Ptrofs.divu
-                           OFFSET
-                           (Integers.Ptrofs.repr 4)))).
-      exploit H9; 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 H14. rewrite HeqOFFSET in H14. rewrite H1 in H14. assumption.
-
-      constructor; simplify. rewrite AssocMap.gso. rewrite AssocMap.gso.
-      assumption. lia.
-      assert (HPle: Ple dst (RTL.max_reg_function f))
-        by (eapply RTL.max_reg_function_def; eauto; simpl; auto).
-      unfold Ple in HPle. lia.
-      rewrite AssocMap.gso. rewrite AssocMap.gso.
-      assumption. lia.
-      assert (HPle: Ple dst (RTL.max_reg_function f))
-        by (eapply RTL.max_reg_function_def; eauto; simpl; auto).
-      unfold Ple in HPle. lia.
-
-    + inv MARR. inv CONST. 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 *)
-      assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE.
-      { apply Mem.load_valid_access in H1. unfold Mem.valid_access in *. simplify.
-        apply Zdivide_mod. assumption. }
-
-      (** 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.
-      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 *)
-      rewrite <- offset_expr_ok_3.
-
-      specialize (H9 (Integers.Ptrofs.unsigned
-                        (Integers.Ptrofs.divu
-                           OFFSET
-                           (Integers.Ptrofs.repr 4)))).
-      exploit H9; 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.
-
-      constructor; simplify. rewrite AssocMap.gso. rewrite AssocMap.gso.
-      assumption. lia.
-      assert (HPle: Ple dst (RTL.max_reg_function f))
-        by (eapply RTL.max_reg_function_def; eauto; simpl; auto).
-      unfold Ple in HPle. lia.
-      rewrite AssocMap.gso. rewrite AssocMap.gso.
-      assumption. lia.
-      assert (HPle: Ple dst (RTL.max_reg_function f))
-        by (eapply RTL.max_reg_function_def; eauto; simpl; auto).
-      unfold Ple in HPle. lia.
-
-      Unshelve.
-      exact (Values.Vint (Int.repr 0)).
-      exact tt.
-      exact (Values.Vint (Int.repr 0)).
-      exact tt.
-      exact (Values.Vint (Int.repr 0)).
-      exact tt.
-  Qed.
+    (* 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 *) *)
+    (*   inv MARR. inv CONST. 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'. *)
+    (*   inv 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 H0 in HPler0. *)
+    (*   inv HPler0; try congruence. *)
+    (*   rewrite EQr0 in H11. *)
+    (*   inv H11. *)
+
+    (*   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. *)
+    (*   { apply Mem.load_valid_access in H1. unfold Mem.valid_access in *. simplify. *)
+    (*     apply Zdivide_mod. assumption. } *)
+
+    (*   (** 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 (HDIV: forall x y, Integers.Ptrofs.divu x y = Integers.Ptrofs.divu x y ) by reflexivity. *)
+    (*     unfold Integers.Ptrofs.divu at 2 in HDIV. *)
+    (*     rewrite HDIV. clear HDIV. *)
+    (*     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. *)
+    (*   econstructor. econstructor. econstructor. crush. *)
+    (*   econstructor. econstructor. econstructor. crush. *)
+    (*   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 *) *)
+    (*   rewrite <- offset_expr_ok. *)
+
+    (*   specialize (H9 (Integers.Ptrofs.unsigned *)
+    (*                     (Integers.Ptrofs.divu *)
+    (*                        OFFSET *)
+    (*                        (Integers.Ptrofs.repr 4)))). *)
+    (*   exploit H9; 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 H14. rewrite HeqOFFSET in H14. rewrite H1 in H14. assumption. *)
+    (*   constructor; simplify. rewrite AssocMap.gso. rewrite AssocMap.gso. *)
+    (*   assumption. lia. *)
+    (*   assert (HPle: Ple dst (RTL.max_reg_function f)) *)
+    (*     by (eapply RTL.max_reg_function_def; eauto; simpl; auto). *)
+    (*   unfold Ple in HPle. lia. *)
+    (*   rewrite AssocMap.gso. rewrite AssocMap.gso. *)
+    (*   assumption. lia. *)
+    (*   assert (HPle: Ple dst (RTL.max_reg_function f)) *)
+    (*     by (eapply RTL.max_reg_function_def; eauto; simpl; auto). *)
+    (*   unfold Ple in HPle. lia. *)
+    (* + (** Preamble *) *)
+    (*   inv MARR. inv CONST. 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'. *)
+    (*   inv 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 H8 in HPler0. *)
+    (*   apply H11 in HPler1. *)
+    (*   inv HPler0; inv HPler1; try congruence. *)
+    (*   rewrite EQr0 in H13. *)
+    (*   rewrite EQr1 in H14. *)
+    (*   inv H13. inv H14. *)
+    (*   clear H0. clear H8. clear H11. *)
+
+    (*   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. *)
+    (*   { apply Mem.load_valid_access in H1. unfold Mem.valid_access in *. simplify. *)
+    (*     apply Zdivide_mod. assumption. } *)
+
+    (*   (** 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 H14. *)
+    (*     rewrite H14. clear H14. *)
+    (*     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. *)
+    (*   econstructor. econstructor. econstructor. crush. *)
+    (*   econstructor. econstructor. econstructor. crush. *)
+    (*   econstructor. econstructor. econstructor. *)
+    (*   econstructor. econstructor. econstructor. econstructor. *)
+    (*   econstructor. econstructor. auto. 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 *) *)
+    (*   rewrite <- offset_expr_ok_2. *)
+
+    (*   specialize (H9 (Integers.Ptrofs.unsigned *)
+    (*                     (Integers.Ptrofs.divu *)
+    (*                        OFFSET *)
+    (*                        (Integers.Ptrofs.repr 4)))). *)
+    (*   exploit H9; 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 H14. rewrite HeqOFFSET in H14. rewrite H1 in H14. assumption. *)
+
+    (*   constructor; simplify. rewrite AssocMap.gso. rewrite AssocMap.gso. *)
+    (*   assumption. lia. *)
+    (*   assert (HPle: Ple dst (RTL.max_reg_function f)) *)
+    (*     by (eapply RTL.max_reg_function_def; eauto; simpl; auto). *)
+    (*   unfold Ple in HPle. lia. *)
+    (*   rewrite AssocMap.gso. rewrite AssocMap.gso. *)
+    (*   assumption. lia. *)
+    (*   assert (HPle: Ple dst (RTL.max_reg_function f)) *)
+    (*     by (eapply RTL.max_reg_function_def; eauto; simpl; auto). *)
+    (*   unfold Ple in HPle. lia. *)
+
+    (* + inv MARR. inv CONST. 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 *) *)
+    (*   assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE. *)
+    (*   { apply Mem.load_valid_access in H1. unfold Mem.valid_access in *. simplify. *)
+    (*     apply Zdivide_mod. assumption. } *)
+
+    (*   (** 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. *)
+    (*   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 *) *)
+    (*   rewrite <- offset_expr_ok_3. *)
+
+    (*   specialize (H9 (Integers.Ptrofs.unsigned *)
+    (*                     (Integers.Ptrofs.divu *)
+    (*                        OFFSET *)
+    (*                        (Integers.Ptrofs.repr 4)))). *)
+    (*   exploit H9; 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. *)
+
+    (*   constructor; simplify. rewrite AssocMap.gso. rewrite AssocMap.gso. *)
+    (*   assumption. lia. *)
+    (*   assert (HPle: Ple dst (RTL.max_reg_function f)) *)
+    (*     by (eapply RTL.max_reg_function_def; eauto; simpl; auto). *)
+    (*   unfold Ple in HPle. lia. *)
+    (*   rewrite AssocMap.gso. rewrite AssocMap.gso. *)
+    (*   assumption. lia. *)
+    (*   assert (HPle: Ple dst (RTL.max_reg_function f)) *)
+    (*     by (eapply RTL.max_reg_function_def; eauto; simpl; auto). *)
+    (*   unfold Ple in HPle. lia. *)
+
+    (*   Unshelve. *)
+    (*   exact (Values.Vint (Int.repr 0)). *)
+    (*   exact tt. *)
+    (*   exact (Values.Vint (Int.repr 0)). *)
+    (*   exact tt. *)
+    (*   exact (Values.Vint (Int.repr 0)). *)
+    (*   exact tt. *)
+  (* Qed. *)
+  Admitted.
   #[local] Hint Resolve transl_iload_correct : htlproof.
 
   Lemma transl_istore_correct:
@@ -1648,861 +1759,861 @@ rs assoc``.
         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 *)
-      inv MARR. inv CONST. 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'.
-      inv 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 H8 in HPler0.
-      inv HPler0; try congruence.
-      rewrite EQr0 in H11.
-      inv H11.
-      clear H0. clear H8.
-
-      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.
-      { apply Mem.store_valid_access_3 in H1. unfold Mem.valid_access in *. simplify.
-        apply Zdivide_mod. assumption. }
-
-      (** Write bounds proof *)
-      assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as WRITE_BOUND_HIGH.
-      { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; crush; auto.
-        unfold stack_bounds in BOUNDS.
-        exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET) (Registers.Regmap.get src rs)); big_tac.
-        apply Integers.Ptrofs.unsigned_range_2. }
-
-      (** Start of proof proper *)
-      eexists. split.
-      eapply Smallstep.plus_one.
-      eapply HTL.step_module; eauto.
-      econstructor. econstructor. econstructor.
-      eapply Verilog.stmnt_runp_Vnonblock_arr. crush.
-      econstructor.
-      econstructor.
-      econstructor.
-      econstructor. econstructor. econstructor. econstructor.
-      econstructor. econstructor. econstructor. econstructor.
-
-      all: try constructor; crush.
-
-      (** State Lookup *)
-      unfold Verilog.merge_regs.
-      crush.
-      unfold_merge.
-      apply AssocMap.gss.
-
-      (** Match states *)
-      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 (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 by reflexivity.
-      rewrite AssocMap.gss.
-      erewrite Verilog.merge_arr_empty2.
-      unfold Verilog.arr_assocmap_set.
-      rewrite AssocMap.gcombine by reflexivity.
-      rewrite AssocMap.gss.
-      rewrite AssocMap.gss.
-      unfold Verilog.merge_arr.
-      setoid_rewrite H7.
-      reflexivity.
-
-      rewrite AssocMap.gcombine by reflexivity.
-      unfold Verilog.merge_arr.
-      unfold Verilog.arr_assocmap_set.
-      rewrite AssocMap.gss.
-      rewrite AssocMap.gss.
-      setoid_rewrite H7.
-      reflexivity.
-
-      rewrite combine_length.
-      rewrite <- array_set_len.
-      unfold arr_repeat. crush.
-      symmetry.
-      apply list_repeat_len.
-
-      rewrite <- array_set_len.
-      unfold arr_repeat. crush.
-      rewrite H4.
-      apply list_repeat_len.
-
-      rewrite combine_length.
-      rewrite <- array_set_len.
-      unfold arr_repeat. crush.
-      apply list_repeat_len.
-
-      rewrite <- array_set_len.
-      unfold arr_repeat. crush.
-      rewrite H4.
-      apply list_repeat_len.
-
-      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.
-           rewrite HeqOFFSET.
-           exact H1.
-           apply Integers.Ptrofs.unsigned_range_2. }
-      constructor.
-      erewrite combine_lookup_second.
-      simplify.
-      assert (HPle : Ple src (RTL.max_reg_function f))
-        by (eapply RTL.max_reg_function_use; eauto; simpl; auto);
-      apply H11 in HPle.
-      destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; inv HPle; eauto.
-
-      rewrite <- array_set_len.
-      unfold arr_repeat. crush.
-      rewrite list_repeat_len. auto.
-
-      assert (HMul : 4 * ptr / 4 = Integers.Ptrofs.unsigned OFFSET / 4) by (f_equal; assumption).
-      rewrite Z.mul_comm in HMul.
-      rewrite Z_div_mult in HMul; try lia.
-      replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) in HMul by reflexivity.
-      rewrite <- PtrofsExtra.divu_unsigned in HMul; unfold_constants; try lia.
-      rewrite HMul. rewrite <- offset_expr_ok.
-      rewrite HeqOFFSET.
-      rewrite array_get_error_set_bound.
-      reflexivity.
-      unfold arr_length, arr_repeat. simpl.
-      rewrite list_repeat_len. rewrite HeqOFFSET in HMul. 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.
-           rewrite HeqOFFSET in *. simplify_val.
-           destruct (Z_le_gt_dec (4 * ptr + 4) (Integers.Ptrofs.unsigned OFFSET)); eauto.
-           rewrite HeqOFFSET in *. simplify_val.
-           left; auto.
-           rewrite HeqOFFSET in *. simplify_val.
-           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 <- offset_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 H9; 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; rewrite HeqOFFSET in n0; try lia.
-      apply Z.div_pos; try lia.
-      apply Integers.Ptrofs.unsigned_range.
-      apply Integers.Ptrofs.unsigned_range_2.
-
-      assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO1 by reflexivity.
-      unfold arr_stack_based_pointers.
-      intros.
-      destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET).
-
-      crush.
-      erewrite Mem.load_store_same.
-      2: { rewrite ZERO1.
-           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 H11.
-      assumption.
-
-      simpl.
-      erewrite Mem.load_store_other with (m1 := m).
-      2: { exact H1. }
-      2: { right.
-           rewrite ZERO1.
-           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.
-           rewrite HeqOFFSET in *. simplify_val.
-           left; auto.
-           rewrite HeqOFFSET in *. simplify_val.
-           right.
-           apply ZExtra.mod_0_bounds; try lia.
-           apply ZLib.Z_mod_mult'.
-           inv H11.
-           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: { rewrite HeqOFFSET in *. simplify_val.
-        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.
-      inv H11.
-      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 H11.
-        exact H11. 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 H11. inv H11. congruence.
-
-      constructor; simplify. unfold Verilog.merge_regs. unfold_merge.
-      rewrite AssocMap.gso.
-      assumption. lia.
-      unfold Verilog.merge_regs. unfold_merge.
-      rewrite AssocMap.gso.
-      assumption. lia.
-
-    + (** Preamble *)
-      inv MARR. inv CONST. 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'.
-      inv 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 H8 in HPler0.
-      apply H11 in HPler1.
-      inv HPler0; inv HPler1; try congruence.
-      rewrite EQr0 in H13.
-      rewrite EQr1 in H14.
-      inv H13. inv H14.
-      clear H0. clear H8. clear H11.
-
-      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.
-      { apply Mem.store_valid_access_3 in H1. unfold Mem.valid_access in *. simplify.
-        apply Zdivide_mod. assumption. }
-
-      (** Write bounds proof *)
-      assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as WRITE_BOUND_HIGH.
-      { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; crush; auto.
-        unfold stack_bounds in BOUNDS.
-        exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET) (Registers.Regmap.get src rs)); auto.
-        split; try lia; apply Integers.Ptrofs.unsigned_range_2.
-        small_tac. }
-
-      (** Start of proof proper *)
-      eexists. split.
-      eapply Smallstep.plus_one.
-      eapply HTL.step_module; eauto.
-      econstructor. econstructor. econstructor.
-      eapply Verilog.stmnt_runp_Vnonblock_arr. crush.
-      econstructor.
-      econstructor. econstructor. econstructor. econstructor.
-      econstructor.
-      econstructor. econstructor. econstructor. econstructor.
-      econstructor. econstructor. econstructor. econstructor.
-      econstructor. econstructor. econstructor. econstructor.
-
-      all: try constructor; crush.
-
-      (** State Lookup *)
-      unfold Verilog.merge_regs.
-      crush.
-      unfold_merge.
-      apply AssocMap.gss.
-
-      (** Match states *)
-      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 (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 by reflexivity.
-      rewrite AssocMap.gss.
-      erewrite Verilog.merge_arr_empty2.
-      unfold Verilog.arr_assocmap_set.
-      rewrite AssocMap.gcombine by reflexivity.
-      rewrite AssocMap.gss.
-      rewrite AssocMap.gss.
-      unfold Verilog.merge_arr.
-      setoid_rewrite H7.
-      reflexivity.
-
-      rewrite AssocMap.gcombine by reflexivity.
-      unfold Verilog.merge_arr.
-      unfold Verilog.arr_assocmap_set.
-      rewrite AssocMap.gss.
-      rewrite AssocMap.gss.
-      setoid_rewrite H7.
-      reflexivity.
-
-      rewrite combine_length.
-      rewrite <- array_set_len.
-      unfold arr_repeat. crush.
-      symmetry.
-      apply list_repeat_len.
-
-      rewrite <- array_set_len.
-      unfold arr_repeat. crush.
-      rewrite H4.
-      apply list_repeat_len.
-
-      rewrite combine_length.
-      rewrite <- array_set_len.
-      unfold arr_repeat. crush.
-      apply list_repeat_len.
-
-      rewrite <- array_set_len.
-      unfold arr_repeat. crush.
-      rewrite H4.
-      apply list_repeat_len.
-
-      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.
-           rewrite HeqOFFSET.
-           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 H14 in H15.
-      destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; inv H15; 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 H15.
-      rewrite Z_div_mult in H15; try lia.
-      replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) in H15 by reflexivity.
-      rewrite <- PtrofsExtra.divu_unsigned in H15; unfold_constants; try lia.
-      rewrite H15. rewrite <- offset_expr_ok_2.
-      rewrite HeqOFFSET in *.
-      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.
-           rewrite HeqOFFSET in *. simplify_val.
-           left; auto.
-           rewrite HeqOFFSET in *. simplify_val.
-           right.
-           apply ZExtra.mod_0_bounds; try lia.
-           apply ZLib.Z_mod_mult'.
-           rewrite Z2Nat.id in H17; try lia.
-           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.
-      }
-
-      rewrite <- offset_expr_ok_2.
-      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 H9; 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.
-      rewrite HeqOFFSET in *.
-      apply Z2Nat.inj_iff in H15; try lia.
-      apply Z.div_pos; try lia.
-      apply Integers.Ptrofs.unsigned_range.
-      apply Integers.Ptrofs.unsigned_range_2.
-
-      assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO1 by reflexivity.
-      unfold arr_stack_based_pointers.
-      intros.
-      destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET).
-
-      crush.
-      erewrite Mem.load_store_same.
-      2: { rewrite ZERO1.
-           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 H14.
-      assumption.
-
-      simpl.
-      erewrite Mem.load_store_other with (m1 := m).
-      2: { exact H1. }
-      2: { right.
-           rewrite ZERO1.
-           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.
-           rewrite HeqOFFSET in *. simplify_val.
-           left; auto.
-           rewrite HeqOFFSET in *. simplify_val.
-           right.
-           apply ZExtra.mod_0_bounds; try lia.
-           apply ZLib.Z_mod_mult'.
-           inv H14.
-           apply Zmult_lt_compat_r with (p := 4) in H16; try lia.
-           rewrite ZLib.div_mul_undo in H16; 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: { rewrite HeqOFFSET in *. simplify_val.
-           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.
-      simplify.
-      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 H14.
-        exact H14. 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 H14. inv H14. congruence.
-
-      constructor; simplify. unfold Verilog.merge_regs. unfold_merge. rewrite AssocMap.gso.
-      assumption. lia.
-      unfold Verilog.merge_regs. unfold_merge. rewrite AssocMap.gso.
-      assumption. lia.
-
-    + inv MARR. inv CONST. 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 *)
-      assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE.
-      { apply Mem.store_valid_access_3 in H1. unfold Mem.valid_access in *. simplify.
-        apply Zdivide_mod. assumption. }
-
-      (** Write bounds proof *)
-      assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as WRITE_BOUND_HIGH.
-      { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:?EQ; crush; auto.
-        unfold stack_bounds in BOUNDS.
-        exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET) (Registers.Regmap.get src rs)); auto.
-        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.
-      econstructor. econstructor. econstructor.
-      eapply Verilog.stmnt_runp_Vnonblock_arr. crush.
-      econstructor. econstructor. econstructor. econstructor.
-
-      all: try constructor; crush.
-
-      (** State Lookup *)
-      unfold Verilog.merge_regs.
-      crush.
-      unfold_merge.
-      apply AssocMap.gss.
-
-      (** Match states *)
-      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 (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 by reflexivity.
-      rewrite AssocMap.gss.
-      erewrite Verilog.merge_arr_empty2.
-      unfold Verilog.arr_assocmap_set.
-      rewrite AssocMap.gcombine by reflexivity.
-      rewrite AssocMap.gss.
-      rewrite AssocMap.gss.
-      unfold Verilog.merge_arr.
-      setoid_rewrite H7.
-      reflexivity.
-
-      rewrite AssocMap.gcombine by reflexivity.
-      unfold Verilog.merge_arr.
-      unfold Verilog.arr_assocmap_set.
-      rewrite AssocMap.gss.
-      rewrite AssocMap.gss.
-      setoid_rewrite H7.
-      reflexivity.
-
-      rewrite combine_length.
-      rewrite <- array_set_len.
-      unfold arr_repeat. crush.
-      symmetry.
-      apply list_repeat_len.
-
-      rewrite <- array_set_len.
-      unfold arr_repeat. crush.
-      rewrite H4.
-      apply list_repeat_len.
-
-      rewrite combine_length.
-      rewrite <- array_set_len.
-      unfold arr_repeat. crush.
-      apply list_repeat_len.
-
-      rewrite <- array_set_len.
-      unfold arr_repeat. crush.
-      rewrite H4.
-      apply list_repeat_len.
-
-      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; inv 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 <- offset_expr_ok_3.
-      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 H13; try lia.
-           apply Zmult_lt_compat_r with (p := 4) in H13; try lia.
-           rewrite ZLib.div_mul_undo in H13; try lia.
-           split; try lia.
-           apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia.
-      }
-
-      rewrite <- offset_expr_ok_3.
-      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 H9; 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'.
-           inv H0.
-           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.
-      }
-      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.
-      inv 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. inv H0. congruence.
-
-      constructor; simplify. unfold Verilog.merge_regs. unfold_merge. rewrite AssocMap.gso.
-      assumption. lia.
-      unfold Verilog.merge_regs. unfold_merge. rewrite AssocMap.gso.
-      assumption. lia.
-
-      Unshelve.
-      exact tt.
-      exact (Values.Vint (Int.repr 0)).
-      exact tt.
-      exact (Values.Vint (Int.repr 0)).
-      exact tt.
-      exact (Values.Vint (Int.repr 0)).
-  Qed.
+    (* 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 *) *)
+  (*     inv MARR. inv CONST. 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'. *)
+  (*     inv 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 H8 in HPler0. *)
+  (*     inv HPler0; try congruence. *)
+  (*     rewrite EQr0 in H11. *)
+  (*     inv H11. *)
+  (*     clear H0. clear H8. *)
+
+  (*     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. *)
+  (*     { apply Mem.store_valid_access_3 in H1. unfold Mem.valid_access in *. simplify. *)
+  (*       apply Zdivide_mod. assumption. } *)
+
+  (*     (** Write bounds proof *) *)
+  (*     assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as WRITE_BOUND_HIGH. *)
+  (*     { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; crush; auto. *)
+  (*       unfold stack_bounds in BOUNDS. *)
+  (*       exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET) (Registers.Regmap.get src rs)); big_tac. *)
+  (*       apply Integers.Ptrofs.unsigned_range_2. } *)
+
+  (*     (** Start of proof proper *) *)
+  (*     eexists. split. *)
+  (*     eapply Smallstep.plus_one. *)
+  (*     eapply HTL.step_module; eauto. *)
+  (*     econstructor. econstructor. econstructor. *)
+  (*     eapply Verilog.stmnt_runp_Vnonblock_arr. crush. *)
+  (*     econstructor. *)
+  (*     econstructor. *)
+  (*     econstructor. *)
+  (*     econstructor. econstructor. econstructor. econstructor. *)
+  (*     econstructor. econstructor. econstructor. econstructor. *)
+
+  (*     all: try constructor; crush. *)
+
+  (*     (** State Lookup *) *)
+  (*     unfold Verilog.merge_regs. *)
+  (*     crush. *)
+  (*     unfold_merge. *)
+  (*     apply AssocMap.gss. *)
+
+  (*     (** Match states *) *)
+  (*     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 (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 by reflexivity. *)
+  (*     rewrite AssocMap.gss. *)
+  (*     erewrite Verilog.merge_arr_empty2. *)
+  (*     unfold Verilog.arr_assocmap_set. *)
+  (*     rewrite AssocMap.gcombine by reflexivity. *)
+  (*     rewrite AssocMap.gss. *)
+  (*     rewrite AssocMap.gss. *)
+  (*     unfold Verilog.merge_arr. *)
+  (*     setoid_rewrite H7. *)
+  (*     reflexivity. *)
+
+  (*     rewrite AssocMap.gcombine by reflexivity. *)
+  (*     unfold Verilog.merge_arr. *)
+  (*     unfold Verilog.arr_assocmap_set. *)
+  (*     rewrite AssocMap.gss. *)
+  (*     rewrite AssocMap.gss. *)
+  (*     setoid_rewrite H7. *)
+  (*     reflexivity. *)
+
+  (*     rewrite combine_length. *)
+  (*     rewrite <- array_set_len. *)
+  (*     unfold arr_repeat. crush. *)
+  (*     symmetry. *)
+  (*     apply list_repeat_len. *)
+
+  (*     rewrite <- array_set_len. *)
+  (*     unfold arr_repeat. crush. *)
+  (*     rewrite H4. *)
+  (*     apply list_repeat_len. *)
+
+  (*     rewrite combine_length. *)
+  (*     rewrite <- array_set_len. *)
+  (*     unfold arr_repeat. crush. *)
+  (*     apply list_repeat_len. *)
+
+  (*     rewrite <- array_set_len. *)
+  (*     unfold arr_repeat. crush. *)
+  (*     rewrite H4. *)
+  (*     apply list_repeat_len. *)
+
+  (*     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. *)
+  (*          rewrite HeqOFFSET. *)
+  (*          exact H1. *)
+  (*          apply Integers.Ptrofs.unsigned_range_2. } *)
+  (*     constructor. *)
+  (*     erewrite combine_lookup_second. *)
+  (*     simplify. *)
+  (*     assert (HPle : Ple src (RTL.max_reg_function f)) *)
+  (*       by (eapply RTL.max_reg_function_use; eauto; simpl; auto); *)
+  (*     apply H11 in HPle. *)
+  (*     destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; inv HPle; eauto. *)
+
+  (*     rewrite <- array_set_len. *)
+  (*     unfold arr_repeat. crush. *)
+  (*     rewrite list_repeat_len. auto. *)
+
+  (*     assert (HMul : 4 * ptr / 4 = Integers.Ptrofs.unsigned OFFSET / 4) by (f_equal; assumption). *)
+  (*     rewrite Z.mul_comm in HMul. *)
+  (*     rewrite Z_div_mult in HMul; try lia. *)
+  (*     replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) in HMul by reflexivity. *)
+  (*     rewrite <- PtrofsExtra.divu_unsigned in HMul; unfold_constants; try lia. *)
+  (*     rewrite HMul. rewrite <- offset_expr_ok. *)
+  (*     rewrite HeqOFFSET. *)
+  (*     rewrite array_get_error_set_bound. *)
+  (*     reflexivity. *)
+  (*     unfold arr_length, arr_repeat. simpl. *)
+  (*     rewrite list_repeat_len. rewrite HeqOFFSET in HMul. 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. *)
+  (*          rewrite HeqOFFSET in *. simplify_val. *)
+  (*          destruct (Z_le_gt_dec (4 * ptr + 4) (Integers.Ptrofs.unsigned OFFSET)); eauto. *)
+  (*          rewrite HeqOFFSET in *. simplify_val. *)
+  (*          left; auto. *)
+  (*          rewrite HeqOFFSET in *. simplify_val. *)
+  (*          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 <- offset_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 H9; 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; rewrite HeqOFFSET in n0; try lia. *)
+  (*     apply Z.div_pos; try lia. *)
+  (*     apply Integers.Ptrofs.unsigned_range. *)
+  (*     apply Integers.Ptrofs.unsigned_range_2. *)
+
+  (*     assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO1 by reflexivity. *)
+  (*     unfold arr_stack_based_pointers. *)
+  (*     intros. *)
+  (*     destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET). *)
+
+  (*     crush. *)
+  (*     erewrite Mem.load_store_same. *)
+  (*     2: { rewrite ZERO1. *)
+  (*          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 H11. *)
+  (*     assumption. *)
+
+  (*     simpl. *)
+  (*     erewrite Mem.load_store_other with (m1 := m). *)
+  (*     2: { exact H1. } *)
+  (*     2: { right. *)
+  (*          rewrite ZERO1. *)
+  (*          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. *)
+  (*          rewrite HeqOFFSET in *. simplify_val. *)
+  (*          left; auto. *)
+  (*          rewrite HeqOFFSET in *. simplify_val. *)
+  (*          right. *)
+  (*          apply ZExtra.mod_0_bounds; try lia. *)
+  (*          apply ZLib.Z_mod_mult'. *)
+  (*          inv H11. *)
+  (*          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: { rewrite HeqOFFSET in *. simplify_val. *)
+  (*       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. *)
+  (*     inv H11. *)
+  (*     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 H11. *)
+  (*       exact H11. 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 H11. inv H11. congruence. *)
+
+  (*     constructor; simplify. unfold Verilog.merge_regs. unfold_merge. *)
+  (*     rewrite AssocMap.gso. *)
+  (*     assumption. lia. *)
+  (*     unfold Verilog.merge_regs. unfold_merge. *)
+  (*     rewrite AssocMap.gso. *)
+  (*     assumption. lia. *)
+
+  (*   + (** Preamble *) *)
+  (*     inv MARR. inv CONST. 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'. *)
+  (*     inv 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 H8 in HPler0. *)
+  (*     apply H11 in HPler1. *)
+  (*     inv HPler0; inv HPler1; try congruence. *)
+  (*     rewrite EQr0 in H13. *)
+  (*     rewrite EQr1 in H14. *)
+  (*     inv H13. inv H14. *)
+  (*     clear H0. clear H8. clear H11. *)
+
+  (*     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. *)
+  (*     { apply Mem.store_valid_access_3 in H1. unfold Mem.valid_access in *. simplify. *)
+  (*       apply Zdivide_mod. assumption. } *)
+
+  (*     (** Write bounds proof *) *)
+  (*     assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as WRITE_BOUND_HIGH. *)
+  (*     { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; crush; auto. *)
+  (*       unfold stack_bounds in BOUNDS. *)
+  (*       exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET) (Registers.Regmap.get src rs)); auto. *)
+  (*       split; try lia; apply Integers.Ptrofs.unsigned_range_2. *)
+  (*       small_tac. } *)
+
+  (*     (** Start of proof proper *) *)
+  (*     eexists. split. *)
+  (*     eapply Smallstep.plus_one. *)
+  (*     eapply HTL.step_module; eauto. *)
+  (*     econstructor. econstructor. econstructor. *)
+  (*     eapply Verilog.stmnt_runp_Vnonblock_arr. crush. *)
+  (*     econstructor. *)
+  (*     econstructor. econstructor. econstructor. econstructor. *)
+  (*     econstructor. *)
+  (*     econstructor. econstructor. econstructor. econstructor. *)
+  (*     econstructor. econstructor. econstructor. econstructor. *)
+  (*     econstructor. econstructor. econstructor. econstructor. *)
+
+  (*     all: try constructor; crush. *)
+
+  (*     (** State Lookup *) *)
+  (*     unfold Verilog.merge_regs. *)
+  (*     crush. *)
+  (*     unfold_merge. *)
+  (*     apply AssocMap.gss. *)
+
+  (*     (** Match states *) *)
+  (*     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 (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 by reflexivity. *)
+  (*     rewrite AssocMap.gss. *)
+  (*     erewrite Verilog.merge_arr_empty2. *)
+  (*     unfold Verilog.arr_assocmap_set. *)
+  (*     rewrite AssocMap.gcombine by reflexivity. *)
+  (*     rewrite AssocMap.gss. *)
+  (*     rewrite AssocMap.gss. *)
+  (*     unfold Verilog.merge_arr. *)
+  (*     setoid_rewrite H7. *)
+  (*     reflexivity. *)
+
+  (*     rewrite AssocMap.gcombine by reflexivity. *)
+  (*     unfold Verilog.merge_arr. *)
+  (*     unfold Verilog.arr_assocmap_set. *)
+  (*     rewrite AssocMap.gss. *)
+  (*     rewrite AssocMap.gss. *)
+  (*     setoid_rewrite H7. *)
+  (*     reflexivity. *)
+
+  (*     rewrite combine_length. *)
+  (*     rewrite <- array_set_len. *)
+  (*     unfold arr_repeat. crush. *)
+  (*     symmetry. *)
+  (*     apply list_repeat_len. *)
+
+  (*     rewrite <- array_set_len. *)
+  (*     unfold arr_repeat. crush. *)
+  (*     rewrite H4. *)
+  (*     apply list_repeat_len. *)
+
+  (*     rewrite combine_length. *)
+  (*     rewrite <- array_set_len. *)
+  (*     unfold arr_repeat. crush. *)
+  (*     apply list_repeat_len. *)
+
+  (*     rewrite <- array_set_len. *)
+  (*     unfold arr_repeat. crush. *)
+  (*     rewrite H4. *)
+  (*     apply list_repeat_len. *)
+
+  (*     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. *)
+  (*          rewrite HeqOFFSET. *)
+  (*          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 H14 in H15. *)
+  (*     destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; inv H15; 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 H15. *)
+  (*     rewrite Z_div_mult in H15; try lia. *)
+  (*     replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) in H15 by reflexivity. *)
+  (*     rewrite <- PtrofsExtra.divu_unsigned in H15; unfold_constants; try lia. *)
+  (*     rewrite H15. rewrite <- offset_expr_ok_2. *)
+  (*     rewrite HeqOFFSET in *. *)
+  (*     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. *)
+  (*          rewrite HeqOFFSET in *. simplify_val. *)
+  (*          left; auto. *)
+  (*          rewrite HeqOFFSET in *. simplify_val. *)
+  (*          right. *)
+  (*          apply ZExtra.mod_0_bounds; try lia. *)
+  (*          apply ZLib.Z_mod_mult'. *)
+  (*          rewrite Z2Nat.id in H17; try lia. *)
+  (*          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. *)
+  (*     } *)
+
+  (*     rewrite <- offset_expr_ok_2. *)
+  (*     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 H9; 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. *)
+  (*     rewrite HeqOFFSET in *. *)
+  (*     apply Z2Nat.inj_iff in H15; try lia. *)
+  (*     apply Z.div_pos; try lia. *)
+  (*     apply Integers.Ptrofs.unsigned_range. *)
+  (*     apply Integers.Ptrofs.unsigned_range_2. *)
+
+  (*     assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO1 by reflexivity. *)
+  (*     unfold arr_stack_based_pointers. *)
+  (*     intros. *)
+  (*     destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET). *)
+
+  (*     crush. *)
+  (*     erewrite Mem.load_store_same. *)
+  (*     2: { rewrite ZERO1. *)
+  (*          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 H14. *)
+  (*     assumption. *)
+
+  (*     simpl. *)
+  (*     erewrite Mem.load_store_other with (m1 := m). *)
+  (*     2: { exact H1. } *)
+  (*     2: { right. *)
+  (*          rewrite ZERO1. *)
+  (*          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. *)
+  (*          rewrite HeqOFFSET in *. simplify_val. *)
+  (*          left; auto. *)
+  (*          rewrite HeqOFFSET in *. simplify_val. *)
+  (*          right. *)
+  (*          apply ZExtra.mod_0_bounds; try lia. *)
+  (*          apply ZLib.Z_mod_mult'. *)
+  (*          inv H14. *)
+  (*          apply Zmult_lt_compat_r with (p := 4) in H16; try lia. *)
+  (*          rewrite ZLib.div_mul_undo in H16; 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: { rewrite HeqOFFSET in *. simplify_val. *)
+  (*          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. *)
+  (*     simplify. *)
+  (*     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 H14. *)
+  (*       exact H14. 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 H14. inv H14. congruence. *)
+
+  (*     constructor; simplify. unfold Verilog.merge_regs. unfold_merge. rewrite AssocMap.gso. *)
+  (*     assumption. lia. *)
+  (*     unfold Verilog.merge_regs. unfold_merge. rewrite AssocMap.gso. *)
+  (*     assumption. lia. *)
+
+  (*   + inv MARR. inv CONST. 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 *) *)
+  (*     assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE. *)
+  (*     { apply Mem.store_valid_access_3 in H1. unfold Mem.valid_access in *. simplify. *)
+  (*       apply Zdivide_mod. assumption. } *)
+
+  (*     (** Write bounds proof *) *)
+  (*     assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as WRITE_BOUND_HIGH. *)
+  (*     { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:?EQ; crush; auto. *)
+  (*       unfold stack_bounds in BOUNDS. *)
+  (*       exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET) (Registers.Regmap.get src rs)); auto. *)
+  (*       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. *)
+  (*     econstructor. econstructor. econstructor. *)
+  (*     eapply Verilog.stmnt_runp_Vnonblock_arr. crush. *)
+  (*     econstructor. econstructor. econstructor. econstructor. *)
+
+  (*     all: try constructor; crush. *)
+
+  (*     (** State Lookup *) *)
+  (*     unfold Verilog.merge_regs. *)
+  (*     crush. *)
+  (*     unfold_merge. *)
+  (*     apply AssocMap.gss. *)
+
+  (*     (** Match states *) *)
+  (*     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 (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 by reflexivity. *)
+  (*     rewrite AssocMap.gss. *)
+  (*     erewrite Verilog.merge_arr_empty2. *)
+  (*     unfold Verilog.arr_assocmap_set. *)
+  (*     rewrite AssocMap.gcombine by reflexivity. *)
+  (*     rewrite AssocMap.gss. *)
+  (*     rewrite AssocMap.gss. *)
+  (*     unfold Verilog.merge_arr. *)
+  (*     setoid_rewrite H7. *)
+  (*     reflexivity. *)
+
+  (*     rewrite AssocMap.gcombine by reflexivity. *)
+  (*     unfold Verilog.merge_arr. *)
+  (*     unfold Verilog.arr_assocmap_set. *)
+  (*     rewrite AssocMap.gss. *)
+  (*     rewrite AssocMap.gss. *)
+  (*     setoid_rewrite H7. *)
+  (*     reflexivity. *)
+
+  (*     rewrite combine_length. *)
+  (*     rewrite <- array_set_len. *)
+  (*     unfold arr_repeat. crush. *)
+  (*     symmetry. *)
+  (*     apply list_repeat_len. *)
+
+  (*     rewrite <- array_set_len. *)
+  (*     unfold arr_repeat. crush. *)
+  (*     rewrite H4. *)
+  (*     apply list_repeat_len. *)
+
+  (*     rewrite combine_length. *)
+  (*     rewrite <- array_set_len. *)
+  (*     unfold arr_repeat. crush. *)
+  (*     apply list_repeat_len. *)
+
+  (*     rewrite <- array_set_len. *)
+  (*     unfold arr_repeat. crush. *)
+  (*     rewrite H4. *)
+  (*     apply list_repeat_len. *)
+
+  (*     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; inv 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 <- offset_expr_ok_3. *)
+  (*     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 H13; try lia. *)
+  (*          apply Zmult_lt_compat_r with (p := 4) in H13; try lia. *)
+  (*          rewrite ZLib.div_mul_undo in H13; try lia. *)
+  (*          split; try lia. *)
+  (*          apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia. *)
+  (*     } *)
+
+  (*     rewrite <- offset_expr_ok_3. *)
+  (*     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 H9; 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'. *)
+  (*          inv H0. *)
+  (*          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. *)
+  (*     } *)
+  (*     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. *)
+  (*     inv 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. inv H0. congruence. *)
+
+  (*     constructor; simplify. unfold Verilog.merge_regs. unfold_merge. rewrite AssocMap.gso. *)
+  (*     assumption. lia. *)
+  (*     unfold Verilog.merge_regs. unfold_merge. rewrite AssocMap.gso. *)
+  (*     assumption. lia. *)
+
+  (*     Unshelve. *)
+  (*     exact tt. *)
+  (*     exact (Values.Vint (Int.repr 0)). *)
+  (*     exact tt. *)
+  (*     exact (Values.Vint (Int.repr 0)). *)
+  (*     exact tt. *)
+  (*     exact (Values.Vint (Int.repr 0)). *)
+  (* Qed. *) Admitted.
   #[local] Hint Resolve transl_istore_correct : htlproof.
 
   Lemma transl_icond_correct:
@@ -2532,48 +2643,48 @@ rs assoc``.
       intros. eapply RTL.max_reg_function_use. apply H22. auto.
       econstructor. auto.
       simpl. econstructor. constructor. unfold Verilog.merge_regs. unfold_merge. simpl.
-      apply AssocMap.gss.
+      unfold_merge. apply AssocMap.gss.
 
       inv MARR. inv CONST.
       big_tac.
-      constructor; rewrite AssocMap.gso; simplify; try assumption; lia.
-    - eexists. split. apply Smallstep.plus_one.
-      clear H32.
-      eapply HTL.step_module; eauto.
-      inv CONST; assumption.
-      inv CONST; assumption.
-      econstructor; simpl; trivial.
-      constructor; trivial.
-      eapply Verilog.erun_Vternary_false; simpl; eauto.
-      eapply eval_cond_correct; eauto. intros.
-      intros. eapply RTL.max_reg_function_use. apply H22. auto.
-      econstructor. auto.
-      simpl. econstructor. constructor. unfold Verilog.merge_regs. unfold_merge. simpl.
-      apply AssocMap.gss.
-
-      inv MARR. inv CONST.
-      big_tac.
-      constructor; rewrite AssocMap.gso; simplify; try assumption; lia.
-
-      Unshelve. all: exact tt.
-  Qed.
+  (*     constructor; rewrite AssocMap.gso; simplify; try assumption; lia. *)
+  (*   - eexists. split. apply Smallstep.plus_one. *)
+  (*     clear H32. *)
+  (*     eapply HTL.step_module; eauto. *)
+  (*     inv CONST; assumption. *)
+  (*     inv CONST; assumption. *)
+  (*     econstructor; simpl; trivial. *)
+  (*     constructor; trivial. *)
+  (*     eapply Verilog.erun_Vternary_false; simpl; eauto. *)
+  (*     eapply eval_cond_correct; eauto. intros. *)
+  (*     intros. eapply RTL.max_reg_function_use. apply H22. auto. *)
+  (*     econstructor. auto. *)
+  (*     simpl. econstructor. constructor. unfold Verilog.merge_regs. unfold_merge. simpl. *)
+  (*     apply AssocMap.gss. *)
+
+  (*     inv MARR. inv CONST. *)
+  (*     big_tac. *)
+  (*     constructor; rewrite AssocMap.gso; simplify; try assumption; lia. *)
+
+  (*     Unshelve. all: exact tt. *)
+  (* Qed. *) Admitted.
   #[local] 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.
-
-  #[local] Hint Resolve transl_ijumptable_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. *)
+  
+  (* #[local] Hint Resolve transl_ijumptable_correct : htlproof.*)
 
   Lemma transl_ireturn_correct:
     forall (s : list RTL.stackframe) (f : RTL.function) (stk : Values.block)
@@ -2613,54 +2724,54 @@ rs assoc``.
       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.
-      inv CONST; assumption.
-      inv CONST; assumption.
-      constructor.
-      econstructor; simpl; trivial.
-      econstructor; simpl; trivial.
-      constructor. constructor. constructor.
-      constructor. constructor. constructor.
-      constructor.
-
-      unfold state_st_wf in WF; big_tac; eauto.
-
-      destruct wf1 as [HCTRL HDATA]. apply HCTRL.
-      apply AssocMapExt.elements_iff. eexists.
-      match goal with H: control ! pc = Some _ |- _ => apply H end.
-
-      apply HTL.step_finish.
-      unfold Verilog.merge_regs.
-      unfold_merge.
-      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.
+  (*     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. *)
+  (*     inv CONST; assumption. *)
+  (*     inv CONST; assumption. *)
+  (*     constructor. *)
+  (*     econstructor; simpl; trivial. *)
+  (*     econstructor; simpl; trivial. *)
+  (*     constructor. constructor. constructor. *)
+  (*     constructor. constructor. constructor. *)
+  (*     constructor. *)
+
+  (*     unfold state_st_wf in WF; big_tac; eauto. *)
+
+  (*     destruct wf1 as [HCTRL HDATA]. apply HCTRL. *)
+  (*     apply AssocMapExt.elements_iff. eexists. *)
+  (*     match goal with H: control ! pc = Some _ |- _ => apply H end. *)
+
+  (*     apply HTL.step_finish. *)
+  (*     unfold Verilog.merge_regs. *)
+  (*     unfold_merge. *)
+  (*     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. *) Admitted.
   #[local] Hint Resolve transl_ireturn_correct : htlproof.
 
   Lemma transl_callstate_correct:
@@ -2866,13 +2977,13 @@ rs assoc``.
   Proof.
     induction 1; eauto with htlproof; (intros; inv_state).
   Qed.
-  #[local] Hint Resolve transl_step_correct : htlproof.*)
+  #[local] 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.*)Admitted.
+  Qed.
 
 End CORRECTNESS.
-- 
cgit