Changed and proved some more theorems

4 files changed, 2192 insertions, 1338 deletions

diff --git a/src/hls/DHTLgen.v b/src/hls/DHTLgen.v
index d573dda..d9e1cd4 100644
--- a/src/hls/DHTLgen.v
+++ b/src/hls/DHTLgen.v
@@ -291,7 +291,7 @@ Definition tbl_to_case_expr (st : reg) (ns : list node) : list (expr * stmnt) :=
                   end)
            (enumerate 0 ns).
 
-Definition translate_cfi (ctrl: control_regs) p (cfi: cf_instr)
+Definition translate_cfi curr_n (ctrl: control_regs) p (cfi: cf_instr)
   : Errors.res stmnt :=
   match cfi with
   | RBgoto n' =>
@@ -302,9 +302,13 @@ Definition translate_cfi (ctrl: control_regs) p (cfi: cf_instr)
   | RBreturn r =>
     match r with
     | Some r' =>
-      Errors.OK (Vseq (Vblock (Vvar ctrl.(ctrl_fin)) (Vlit (ZToValue 1%Z))) (Vblock (Vvar ctrl.(ctrl_return)) (Vvar (reg_enc r'))))
+      Errors.OK (Vseq (Vseq (translate_predicate Vblock p (Vvar ctrl.(ctrl_fin)) (Vlit (ZToValue 1)))
+                 (translate_predicate Vblock p (Vvar ctrl.(ctrl_return)) (Vvar (reg_enc r')))) 
+                 (state_goto p ctrl.(ctrl_st) curr_n))
     | None =>
-      Errors.OK (Vseq (Vblock (Vvar ctrl.(ctrl_fin)) (Vlit (ZToValue 1%Z))) (Vblock (Vvar ctrl.(ctrl_return)) (Vlit (ZToValue 0%Z))))
+      Errors.OK (Vseq (Vseq (translate_predicate Vblock p (Vvar ctrl.(ctrl_fin)) (Vlit (ZToValue 1)))
+                 (translate_predicate Vblock p (Vvar ctrl.(ctrl_return)) (Vlit (ZToValue 0)))) 
+                 (state_goto p ctrl.(ctrl_st) curr_n))
     end
   | RBjumptable r tbl =>
     Errors.OK (Vcase (Vvar (reg_enc r)) (list_to_stmnt (tbl_to_case_expr ctrl.(ctrl_st) tbl)) (Some Vskip))
@@ -316,7 +320,23 @@ Definition translate_cfi (ctrl: control_regs) p (cfi: cf_instr)
     Errors.Error (Errors.msg "HTLPargen: RBbuildin not supported.")
   end.
 
-Definition transf_instr (ctrl: control_regs) (dc: pred_op * stmnt) (i: instr)
+Definition assert_ (b: bool) m: res unit :=
+  if b then OK tt else Error (msg m).
+
+Definition check_cfi n (cfi: cf_instr): res unit :=
+  do _assert <- assert_ (Z.pos n <=? Integers.Int.max_unsigned) "DHTLgen: State larger than 2^32";
+  match cfi with
+  | RBgoto n' =>
+    assert_ (Z.pos n' <=? Integers.Int.max_unsigned) "DHTLgen: State larger than 2^32"
+  | RBcond c args n1 n2 =>
+    assert_ ((Z.pos n1 <=? Integers.Int.max_unsigned) 
+             && (Z.pos n2 <=? Integers.Int.max_unsigned)) "DHTLgen: State larger than 2^32"
+  | RBjumptable r tbl =>
+    assert_ (forallb (fun x => Z.pos x <=? Integers.Int.max_unsigned) tbl) "DHTLgen: State larger than 2^32"
+  | _ => OK tt
+  end.
+
+Definition transf_instr n (ctrl: control_regs) (dc: pred_op * stmnt) (i: instr)
            : Errors.res (pred_op * stmnt) :=
   let '(curr_p, d) := dc in
   let npred p := Some (Pand curr_p (dfltp p)) in
@@ -339,24 +359,25 @@ Definition transf_instr (ctrl: control_regs) (dc: pred_op * stmnt) (i: instr)
     let stmnt := translate_predicate Vblock (npred p') (pred_expr (Plit (true, p))) cond' in
     Errors.OK (curr_p, Vseq d stmnt)
   | RBexit p cf => 
-    do d_stmnt <- translate_cfi ctrl (npred p) cf;
+    do _check <- check_cfi n cf;
+    do d_stmnt <- translate_cfi n ctrl (npred p) cf;
     Errors.OK (Pand curr_p (negate (dfltp p)), Vseq d d_stmnt)
   end.
 
-Definition transf_chained_block (ctrl: control_regs) (dc: @pred_op positive * stmnt) (block: list instr)
+Definition transf_chained_block n (ctrl: control_regs) (dc: @pred_op positive * stmnt) (block: list instr)
            : Errors.res (pred_op * stmnt) :=
-  mfold_left (transf_instr ctrl) block (OK dc).
+  mfold_left (transf_instr n ctrl) block (OK dc).
 
-Definition transf_parallel_block (ctrl: control_regs) (block: list (list instr))
+Definition transf_parallel_block n (ctrl: control_regs) (block: list (list instr))
            : Errors.res (pred_op * stmnt) :=
-  mfold_left (transf_chained_block ctrl) block (OK (Ptrue, Vskip)).
+  mfold_left (transf_chained_block n ctrl) block (OK (Ptrue, Vskip)).
 
 Definition transf_seq_block (ctrl: control_regs) (d: datapath) (ni: node * SubParBB.t)
            : Errors.res datapath :=
   let (n, bb) := ni in
   match d ! n with
   | None => 
-    do (_pred, stmnt) <- transf_chained_block ctrl (Ptrue, Vskip) (concat bb);
+    do (_pred, stmnt) <- transf_chained_block n ctrl (Ptrue, Vskip) (concat bb);
     OK (PTree.set n stmnt d)
   | _ => Error (msg "DHTLgen: overwriting location")
   end.
diff --git a/src/hls/DHTLgenproof.v b/src/hls/DHTLgenproof.v
index bd8320e..6b2cc8d 100644
--- a/src/hls/DHTLgenproof.v
+++ b/src/hls/DHTLgenproof.v
@@ -49,11 +49,16 @@ Require Import Lia.
 
 Local Open Scope assocmap.
 
+Local Opaque Int.max_unsigned.
+
 #[local] Hint Resolve AssocMap.gss : htlproof.
 #[local] Hint Resolve AssocMap.gso : htlproof.
 
 #[local] Hint Unfold find_assocmap AssocMapExt.get_default : htlproof.
 
+Definition get_mem n r := 
+  Option.default (NToValue 0) (Option.join (array_get_error n r)).
+
 Inductive match_assocmaps : positive -> positive -> Gible.regset -> Gible.predset -> assocmap -> Prop :=
   match_assocmap : forall rs pr am max_reg max_pred,
     (forall r, Ple r max_reg ->
@@ -73,8 +78,7 @@ Inductive match_arrs (stack_size: Z) (stk: positive) (stk_len: nat) (sp : Values
         0 <= ptr < Z.of_nat stack.(arr_length) ->
         opt_val_value_lessdef (Mem.loadv AST.Mint32 mem
                                          (Values.Val.offset_ptr sp (Ptrofs.repr (4 * ptr))))
-                              (Option.default (NToValue 0)
-                                 (Option.join (array_get_error (Z.to_nat ptr) stack)))) ->
+                              (get_mem (Z.to_nat ptr) stack)) ->
     match_arrs stack_size stk stk_len sp mem asa.
 
 Definition stack_based (v : Values.val) (sp : Values.block) : Prop :=
@@ -1104,6 +1108,7 @@ Ltac unfold_merge :=
              (combine merge_cell (arr_repeat None (Datatypes.length arr_contents))
                 {| arr_contents := arr_contents; arr_length := Datatypes.length arr_contents; arr_wf := eq_refl |}))).
       { apply array_get_error_equal; auto. cbn. now rewrite list_combine_none. }
+      unfold get_mem in *.
       rewrite <- H1. auto.
   Qed.
 
@@ -1265,8 +1270,8 @@ Proof.
 Qed.
 
   Lemma transl_iop_correct:
-    forall ctrl sp max_reg max_pred d d' curr_p next_p rs ps m rs' ps' p op args dst asr arr asr' arr' stk stk_len,
-      transf_instr ctrl (curr_p, d) (RBop p op args dst) = Errors.OK (next_p, d') ->
+    forall ctrl sp max_reg max_pred d d' curr_p next_p rs ps m rs' ps' p op args dst asr arr asr' arr' stk stk_len n,
+      transf_instr n ctrl (curr_p, d) (RBop p op args dst) = Errors.OK (next_p, d') ->
       step_instr ge sp (Iexec (mk_instr_state rs ps m)) (RBop p op args dst) (Iexec (mk_instr_state rs' ps m)) ->
       stmnt_runp tt (e_assoc asr) (e_assoc_arr stk stk_len arr) d (e_assoc asr') (e_assoc_arr stk stk_len arr') ->
       match_assocmaps max_reg max_pred rs ps asr' ->
@@ -1387,6 +1392,17 @@ Opaque Mem.alloc.
     eauto.
   Qed.
 
+  Lemma mfold_left_app:
+    forall A B f a l x y, 
+      @mfold_left A B f (a ++ l) x = OK y ->
+      exists y', @mfold_left A B f a x = OK y' /\ @mfold_left A B f l (OK y') = OK y.
+  Proof.
+    induction a.
+    - intros. destruct x; [|now rewrite mfold_left_error in H]. exists a. eauto.
+    - intros. destruct x; [|now rewrite mfold_left_error in H]. rewrite <- app_comm_cons in H.
+      exploit mfold_left_cons; eauto.
+  Qed.
+
   Lemma step_cf_instr_pc_ind :
     forall s f sp rs' pr' m' pc pc' cf t state,
       step_cf_instr ge (GibleSubPar.State s f sp pc rs' pr' m') cf t state ->
@@ -1444,10 +1460,812 @@ Opaque Mem.alloc.
       + cbn in *. eapply step_exec_concat2'; eauto.
   Qed.
 
+  Lemma one_ne_zero:
+    Int.repr 1 <> Int.repr 0.
+  Proof.
+    unfold not; intros.
+    assert (Int.unsigned (Int.repr 1) = Int.unsigned (Int.repr 0)) by (now rewrite H).
+    rewrite ! Int.unsigned_repr in H0 by crush. lia.
+  Qed.
+
+  Lemma int_and_boolToValue :
+    forall b1 b2,
+      Int.and (boolToValue b1) (boolToValue b2) = boolToValue (b1 && b2).
+  Proof.
+    destruct b1; destruct b2; cbn; unfold boolToValue; unfold natToValue;
+    replace (Z.of_nat 1) with 1 by auto;
+    replace (Z.of_nat 0) with 0 by auto.
+    - apply Int.and_idem.
+    - apply Int.and_zero.
+    - apply Int.and_zero_l.
+    - apply Int.and_zero.
+  Qed.
+
+  Lemma int_or_boolToValue :
+    forall b1 b2,
+      Int.or (boolToValue b1) (boolToValue b2) = boolToValue (b1 || b2).
+  Proof.
+    destruct b1; destruct b2; cbn; unfold boolToValue; unfold natToValue;
+    replace (Z.of_nat 1) with 1 by auto;
+    replace (Z.of_nat 0) with 0 by auto.
+    - apply Int.or_idem.
+    - apply Int.or_zero.
+    - apply Int.or_zero_l.
+    - apply Int.or_zero_l.
+  Qed.
+
+  Lemma pred_expr_correct :
+    forall curr_p pr asr asa,
+      (forall r, Ple r (max_predicate curr_p) ->
+          find_assocmap 1 (pred_enc r) asr = boolToValue (PMap.get r pr)) ->
+      expr_runp tt asr asa (pred_expr curr_p) (boolToValue (eval_predf pr curr_p)).
+  Proof.
+    induction curr_p.
+    - intros * HFRL. cbn. destruct p as [b p']. destruct b.
+      + constructor. eapply HFRL. cbn. unfold Ple. lia.
+      + econstructor. constructor. eapply HFRL. cbn. unfold Ple; lia.
+        econstructor. cbn. f_equal. unfold boolToValue.
+        f_equal. destruct pr !! p' eqn:?. cbn.
+        rewrite Int.eq_false; auto. unfold natToValue.
+        replace (Z.of_nat 1) with 1 by auto. unfold Int.zero.
+        apply one_ne_zero.
+        cbn. rewrite Int.eq_true; auto.
+    - intros. cbn. constructor.
+    - intros. cbn. constructor.
+    - cbn -[eval_predf]; intros. econstructor. eapply IHcurr_p1. intros. eapply H.
+      unfold Ple in *. lia.
+      eapply IHcurr_p2; intros. eapply H. unfold Ple in *; lia.
+      cbn -[eval_predf]. f_equal. symmetry. apply int_and_boolToValue.
+    - cbn -[eval_predf]; intros. econstructor. eapply IHcurr_p1. intros. eapply H.
+      unfold Ple in *. lia.
+      eapply IHcurr_p2; intros. eapply H. unfold Ple in *; lia.
+      cbn -[eval_predf]. f_equal. symmetry. apply int_or_boolToValue.
+  Qed.
+
+  Local Opaque deep_simplify.
+
+  Lemma valueToBool_correct: 
+    forall b,
+      valueToBool (boolToValue b) = b.
+  Proof.
+    unfold valueToBool, boolToValue; intros. 
+    unfold uvalueToZ, natToValue. destruct b; cbn;
+    rewrite Int.unsigned_repr; crush.
+  Qed.
+
+  Lemma negb_inj':
+    forall a b, a = b -> negb a = negb b.
+  Proof. intros. destruct a, b; auto. Qed.
+
+  Lemma transl_predicate_correct :
+    forall asr asa a b asr' asa' p r e max_pred max_reg rs ps,
+      stmnt_runp tt (e_assoc asr) (e_assoc_arr a b asa) (translate_predicate Vblock (Some p) (Vvar r) e) (e_assoc asr') (e_assoc_arr a b asa') ->
+      Ple (max_predicate p) max_pred ->
+      match_assocmaps max_reg max_pred rs ps asr ->
+      eval_predf ps p = false ->
+      (forall x, asr # x = asr' # x) /\ asa = asa'.
+  Proof.
+    intros * HSTMNT HPLE HMATCH HEVAL *.
+    pose proof HEVAL as HEVAL_DEEP.
+    erewrite <- eval_predf_deep_simplify in HEVAL_DEEP.
+    cbn in *. destruct_match.
+    - inv HSTMNT; inv H6. split; auto. intros.
+      exploit pred_expr_correct. inv HMATCH; eauto. intros. eapply H0. instantiate (1 := deep_simplify peq p) in H1.
+      eapply max_predicate_deep_simplify in H1. unfold Ple in *. lia.
+      intros. inv H7. unfold e_assoc in *; cbn in *. 
+      pose proof H as H'. eapply expr_runp_determinate in H6; eauto. rewrite HEVAL_DEEP in H6.
+      rewrite H6 in H10. now rewrite valueToBool_correct in H10.
+      unfold e_assoc_arr, e_assoc in *; cbn in *. inv H9.
+      destruct (peq r0 x); subst; [now rewrite assocmap_gss|now rewrite assocmap_gso by auto].
+    - unfold sat_pred_simple in Heqo. repeat (destruct_match; try discriminate).
+      unfold eval_predf in HEVAL_DEEP. 
+      apply negb_inj' in HEVAL_DEEP.
+      rewrite <- negate_correct in HEVAL_DEEP. rewrite e0 in HEVAL_DEEP. discriminate.
+  Qed.
+
+  Inductive lessdef_memory: option value -> option value -> Prop := 
+  | lessdef_memory_none: 
+    lessdef_memory None (Some (ZToValue 0))
+  | lessdef_memory_eq: forall a,
+    lessdef_memory a a.
+
+  Lemma transl_predicate_correct_arr :
+    forall asr asa a b asr' asa' p r e max_pred max_reg rs ps e1,
+      stmnt_runp tt (e_assoc asr) (e_assoc_arr a b asa) (translate_predicate Vblock (Some p) (Vvari r e1) e) (e_assoc asr') (e_assoc_arr a b asa') ->
+      Ple (max_predicate p) max_pred ->
+      match_assocmaps max_reg max_pred rs ps asr ->
+      eval_predf ps p = false ->
+      asr = asr' /\ (forall x a, asa ! x = Some a -> exists a', asa' ! x = Some a'
+                     /\ (forall y, (y < arr_length a)%nat -> exists av av', array_get_error y a = Some av /\ array_get_error y a' = Some av' /\ lessdef_memory av av')).
+  Proof.
+    intros * HSTMNT HPLE HMATCH HEVAL *.
+    pose proof HEVAL as HEVAL_DEEP.
+    erewrite <- eval_predf_deep_simplify in HEVAL_DEEP.
+    cbn in *. destruct_match.
+    - inv HSTMNT; inv H6; split; auto; intros.
+      exploit pred_expr_correct. inv HMATCH; eauto. intros. eapply H1. instantiate (1 := deep_simplify peq p) in H2.
+      eapply max_predicate_deep_simplify in H2. unfold Ple in *. lia.
+      intros. inv H7. unfold e_assoc in *; cbn in *.
+      pose proof H0 as H'. eapply expr_runp_determinate in H9; eauto. rewrite HEVAL_DEEP in H9.
+      rewrite H9 in H12. now rewrite valueToBool_correct in H12.
+      unfold e_assoc_arr, e_assoc in *; cbn in *. inv H11.
+      destruct (peq r0 x); subst. 
+      + unfold arr_assocmap_set. rewrite H.
+        rewrite AssocMap.gss. eexists. split; eauto. unfold arr_assocmap_lookup in H10.
+        rewrite H in H10. inv H10. eapply expr_runp_determinate in H3; eauto. subst.
+        intros.
+        destruct (Nat.eq_dec y (valueToNat i)); subst.
+        * rewrite array_get_error_set_bound by auto.
+          destruct (array_get_error (valueToNat i) a1) eqn:?.
+          -- do 2 eexists. split; eauto. split. eauto.
+             destruct o; cbn; constructor.
+          -- exploit (@array_get_error_bound (option value)); eauto. simplify. 
+             rewrite H3 in Heqo0. discriminate.
+        * rewrite array_gso by auto.
+          exploit (@array_get_error_bound (option value)); eauto. simplify.
+          rewrite H3. do 2 eexists; repeat split; constructor.
+      + unfold arr_assocmap_set. destruct_match.
+        * rewrite PTree.gso by auto. setoid_rewrite H. eexists. split; eauto.
+          intros. exploit (@array_get_error_bound (option value)); eauto. simplify.
+          rewrite H4. do 2 eexists; repeat split; constructor.
+        * eexists. split; eauto. intros. exploit (@array_get_error_bound (option value)); eauto. simplify.
+          rewrite H4. do 2 eexists; repeat split; constructor.
+    - unfold sat_pred_simple in Heqo. repeat (destruct_match; try discriminate).
+      unfold eval_predf in HEVAL_DEEP. 
+      apply negb_inj' in HEVAL_DEEP.
+      rewrite <- negate_correct in HEVAL_DEEP. rewrite e0 in HEVAL_DEEP. discriminate.
+  Qed.
+
+  Lemma transl_predicate_correct2 :
+    forall asr asa a b p r e max_pred max_reg rs ps,
+      Ple (max_predicate p) max_pred ->
+      match_assocmaps max_reg max_pred rs ps asr ->
+      eval_predf ps p = false ->
+      exists asr', stmnt_runp tt (e_assoc asr) (e_assoc_arr a b asa) (translate_predicate Vblock (Some p) (Vvar r) e) (e_assoc asr') (e_assoc_arr a b asa) /\ (forall x, asr # x = asr' # x).
+  Proof.
+    intros * HPLE HMATCH HEVAL. pose proof HEVAL as HEVAL_DEEP. 
+    unfold translate_predicate. erewrite <- eval_predf_deep_simplify in HEVAL_DEEP.
+    destruct_match.
+    - econstructor; split.
+      + econstructor; [econstructor|]. eapply erun_Vternary_false. 
+        * eapply pred_expr_correct. intros. eapply max_predicate_deep_simplify in H.
+        inv HMATCH. eapply H1; unfold Ple in *. lia.
+        * now econstructor.
+        * rewrite HEVAL_DEEP. auto.
+      + intros. destruct (peq x r); subst.
+        * now rewrite assocmap_gss.
+        * now rewrite assocmap_gso.
+   - unfold sat_pred_simple in Heqo. repeat (destruct_match; try discriminate).
+     apply negb_inj' in HEVAL_DEEP. unfold eval_predf in *. rewrite <- negate_correct in HEVAL_DEEP.
+     now rewrite e0 in HEVAL_DEEP.
+  Qed.
+
+  Lemma arr_assocmap_set_gss :
+    forall r i v asa ar,
+      asa ! r = Some ar ->
+      (arr_assocmap_set r i v asa) ! r = Some (array_set i (Some v) ar).
+  Proof.
+    unfold arr_assocmap_set.
+    intros. rewrite H. rewrite PTree.gss. auto.
+  Qed.
+
+  Lemma arr_assocmap_set_gso :
+    forall r x i v asa ar,
+      asa ! x = Some ar ->
+      r <> x ->
+      (arr_assocmap_set r i v asa) ! x = asa ! x.
+  Proof.
+    unfold arr_assocmap_set. intros. 
+    destruct (asa!r) eqn:?; auto; now rewrite PTree.gso by auto.
+  Qed.
+
+  Lemma arr_assocmap_set_gs2 :
+    forall r x i v asa,
+      asa ! x = None ->
+      (arr_assocmap_set r i v asa) ! x = None.
+  Proof.
+    unfold arr_assocmap_set. intros. 
+    destruct (peq r x); subst; [now rewrite H|].
+    destruct (asa!r) eqn:?; auto.
+    now rewrite PTree.gso by auto.
+  Qed.
+
+  Lemma get_mem_set_array_gss :
+    forall y a x,
+      (y < arr_length a)%nat ->
+      get_mem y (array_set y (Some x) a) = x.
+  Proof.
+    unfold get_mem; intros.
+    rewrite array_get_error_set_bound by eauto; auto.
+  Qed.
+
+  Lemma get_mem_set_array_gss2 :
+    forall y a,
+      (y < arr_length a)%nat ->
+      get_mem y (array_set y None a) = ZToValue 0.
+  Proof.
+    unfold get_mem; intros.
+    rewrite array_get_error_set_bound by eauto; auto.
+  Qed.
+
+  Lemma get_mem_set_array_gso :
+    forall y a x z,
+      y <> z ->
+      get_mem y (array_set z x a) = get_mem y a.
+  Proof. unfold get_mem; intros. now rewrite array_gso by auto. Qed.
+
+  Lemma get_mem_set_array_gso2 :
+    forall y a x z,
+      (y >= arr_length a)%nat ->
+      get_mem y (array_set z x a) = ZToValue 0.
+  Proof.
+    intros; unfold get_mem. unfold array_get_error.
+    erewrite array_set_len with (i:=z) (x:=x) in H.
+    remember (array_set z x a). destruct a0. cbn in *. rewrite <- arr_wf in H.
+    assert (Datatypes.length arr_contents <= y)%nat by lia.
+    apply nth_error_None in H0. rewrite H0. auto.
+  Qed.
+
+  Lemma get_mem_set_array_gss3 :
+    forall y a,
+      get_mem y (array_set y None a) = ZToValue 0.
+  Proof.
+    intros.
+    assert (y < arr_length a \/ y >= arr_length a)%nat by lia.
+    inv H.
+    - now rewrite get_mem_set_array_gss2.
+    - now rewrite get_mem_set_array_gso2.
+  Qed.
+
+  Lemma arr_assocmap_lookup_get_mem: 
+    forall asa r i v,
+      arr_assocmap_lookup asa r i = Some v ->
+      exists ar, asa ! r = Some ar /\ get_mem i ar = v.
+  Proof.
+    unfold arr_assocmap_lookup in *; intros.
+    repeat (destruct_match; try discriminate). inv H.
+    eexists; eauto.
+  Qed.
+
+  Lemma transl_predicate_correct_arr2 :
+    forall asr asa a b p r e max_pred max_reg rs ps e1 v1 ar,
+      Ple (max_predicate p) max_pred ->
+      match_assocmaps max_reg max_pred rs ps asr ->
+      eval_predf ps p = false ->
+      expr_runp tt (assoc_blocking (e_assoc asr)) (assoc_blocking (e_assoc_arr a b asa)) e1 v1 ->
+      arr_assocmap_lookup (assoc_blocking (e_assoc_arr a b asa)) r (valueToNat v1) = Some ar ->
+      exists asa', stmnt_runp tt (e_assoc asr) (e_assoc_arr a b asa) (translate_predicate Vblock (Some p) (Vvari r e1) e) (e_assoc asr) (e_assoc_arr a b asa') 
+      /\ (forall x a, asa ! x = Some a -> 
+            exists a', asa' ! x = Some a'
+            /\ (forall y, (y < arr_length a)%nat -> get_mem y a = get_mem y a')
+            /\ (arr_length a = arr_length a')).
+  Proof.
+    intros * HPLE HMATCH HEVAL HEXPRRUN HLOOKUP. pose proof HEVAL as HEVAL_DEEP. 
+    unfold translate_predicate. erewrite <- eval_predf_deep_simplify in HEVAL_DEEP.
+    destruct_match.
+    - econstructor; split.
+      + econstructor; [econstructor|]; eauto. eapply erun_Vternary_false.
+        * eapply pred_expr_correct. intros. eapply max_predicate_deep_simplify in H.
+          inv HMATCH. eapply H1; unfold Ple in *. lia.
+        * econstructor; eauto.
+        * rewrite HEVAL_DEEP. auto.
+      + intros. destruct (peq x r); subst.
+        * erewrite arr_assocmap_set_gss by eauto.
+          eexists; repeat split; eauto; intros.
+          destruct (Nat.eq_dec y (valueToNat v1)); subst.
+          -- rewrite get_mem_set_array_gss by auto. 
+             exploit arr_assocmap_lookup_get_mem; eauto. intros (ar' & HASSOC & HGET).
+             unfold e_assoc_arr in HASSOC. cbn in *. rewrite HASSOC in H. inv H. auto.
+          -- now rewrite get_mem_set_array_gso by auto.
+        * erewrite arr_assocmap_set_gso by eauto. unfold e_assoc_arr; cbn. eexists; split; eauto.
+   - unfold sat_pred_simple in Heqo. repeat (destruct_match; try discriminate).
+     apply negb_inj' in HEVAL_DEEP. unfold eval_predf in *. rewrite <- negate_correct in HEVAL_DEEP.
+     now rewrite e0 in HEVAL_DEEP.
+  Qed.
+
+  Definition unchanged (asr : assocmap) asa asr' asa' :=
+    (forall x, asr ! x = asr' ! x)
+    /\ (forall x a, asa ! x = Some a -> 
+          exists a', asa' ! x = Some a'
+          /\ (forall y, (y < arr_length a)%nat -> get_mem y a = get_mem y a')
+          /\ arr_length a = arr_length a').
+
+  Lemma unchanged_refl :
+    forall a b, unchanged a b a b.
+  Proof.
+    unfold unchanged; split; intros. eauto.
+    eexists; eauto.
+  Qed.
+
+  Lemma unchanged_trans :
+    forall a b a' b' a'' b'', unchanged a b a' b' -> unchanged a' b' a'' b'' -> unchanged a b a'' b''.
+  Proof.
+    unfold unchanged; simplify; intros.
+    congruence.
+    pose proof H as H'. apply H3 in H'. simplify. pose proof H5 as H5'.
+    apply H2 in H5'. simplify. eexists; eauto; simplify; eauto; try congruence.
+    intros. rewrite H4 by auto. now rewrite <- H6 by lia.
+  Qed.
+
+  Lemma transl_step_state_correct_single_instr :
+    forall s f sp pc curr_p next_p rs rs' m m' pr pr' m_ s' stmnt stmnt' asr0 asa0 asr asa n i,
+      (* (fn_code f) ! pc = Some bb -> *)
+      transf_instr n (mk_ctrl f) (curr_p, stmnt) i = OK (next_p, stmnt') ->
+      stmnt_runp tt (e_assoc asr0) (e_assoc_arr (DHTL.mod_stk m_) (DHTL.mod_stk_len m_) asa0) stmnt (e_assoc asr) (e_assoc_arr (DHTL.mod_stk m_) (DHTL.mod_stk_len m_) asa) ->
+      eval_predf pr curr_p = true ->
+      step_instr ge sp (Iexec {| is_rs := rs; is_ps := pr; is_mem := m |}) i
+             (Iexec {| is_rs := rs'; is_ps := pr'; is_mem := m' |}) ->
+      match_states (GibleSubPar.State s f sp pc rs pr m) (DHTL.State s' m_ pc asr asa) ->
+      exists asr' asa',
+        stmnt_runp tt (e_assoc asr0) (e_assoc_arr (DHTL.mod_stk m_) (DHTL.mod_stk_len m_) asa0) stmnt' (e_assoc asr') (e_assoc_arr (DHTL.mod_stk m_) (DHTL.mod_stk_len m_) asa')
+        /\ match_states (GibleSubPar.State s f sp pc rs' pr' m') (DHTL.State s' m_ pc asr' asa')
+        /\ eval_predf pr' next_p = true.
+  Proof. Admitted.
+
+  Lemma transl_step_state_correct_single_instr_term :
+    forall s f sp pc curr_p next_p rs rs' m m' pr pr' m_ s' stmnt stmnt' asr0 asa0 asr asa n i cf pc',
+      (* (fn_code f) ! pc = Some bb -> *)
+      transf_instr n (mk_ctrl f) (curr_p, stmnt) i = OK (next_p, stmnt') ->
+      stmnt_runp tt (e_assoc asr0) (e_assoc_arr (DHTL.mod_stk m_) (DHTL.mod_stk_len m_) asa0) stmnt (e_assoc asr) (e_assoc_arr (DHTL.mod_stk m_) (DHTL.mod_stk_len m_) asa) ->
+      eval_predf pr curr_p = true ->
+      step_instr ge sp (Iexec {| is_rs := rs; is_ps := pr; is_mem := m |}) i
+             (Iterm {| is_rs := rs'; is_ps := pr'; is_mem := m' |} cf) ->
+      step_cf_instr ge (GibleSubPar.State s f sp pc rs' pr' m') cf Events.E0 (GibleSubPar.State s f sp pc' rs' pr' m') ->
+      match_states (GibleSubPar.State s f sp pc rs pr m) (DHTL.State s' m_ pc asr asa) ->
+      exists asr' asa',
+        stmnt_runp tt (e_assoc asr0) (e_assoc_arr (DHTL.mod_stk m_) (DHTL.mod_stk_len m_) asa0) stmnt' (e_assoc asr') (e_assoc_arr (DHTL.mod_stk m_) (DHTL.mod_stk_len m_) asa')
+        /\ match_states (GibleSubPar.State s f sp pc' rs' pr' m') (DHTL.State s' m_ pc' asr' asa')
+        /\ eval_predf pr' next_p = false.
+  Proof. Admitted.
+
+  Lemma transl_step_state_correct_single_instr_term_return :
+    forall s f sp pc curr_p next_p rs rs' m m' pr pr' m_ s' stmnt stmnt' asr0 asa0 asr asa n i cf v m'',
+      (* (fn_code f) ! pc = Some bb -> *)
+      transf_instr n (mk_ctrl f) (curr_p, stmnt) i = OK (next_p, stmnt') ->
+      stmnt_runp tt (e_assoc asr0) (e_assoc_arr (DHTL.mod_stk m_) (DHTL.mod_stk_len m_) asa0) stmnt (e_assoc asr) (e_assoc_arr (DHTL.mod_stk m_) (DHTL.mod_stk_len m_) asa) ->
+      eval_predf pr curr_p = true ->
+      step_instr ge sp (Iexec {| is_rs := rs; is_ps := pr; is_mem := m |}) i
+             (Iterm {| is_rs := rs'; is_ps := pr'; is_mem := m' |} cf) ->
+      step_cf_instr ge (GibleSubPar.State s f sp pc rs' pr' m') cf Events.E0 (GibleSubPar.Returnstate s v m'') ->
+      match_states (GibleSubPar.State s f sp pc rs pr m) (DHTL.State s' m_ pc asr asa) ->
+      exists retval,
+        stmnt_runp tt (e_assoc asr0) (e_assoc_arr (DHTL.mod_stk m_) (DHTL.mod_stk_len m_) asa0) stmnt' (e_assoc (AssocMap.set m_.(DHTL.mod_st) (posToValue n) (AssocMap.set (m_.(DHTL.mod_return)) retval (AssocMap.set (m_.(DHTL.mod_finish)) (ZToValue 1) asr)))) (e_assoc_arr (DHTL.mod_stk m_) (DHTL.mod_stk_len m_) asa)
+        /\ val_value_lessdef v retval
+        /\ eval_predf pr' next_p = false.
+  Proof. Admitted.
+
+  #[local] Ltac destr := destruct_match; try discriminate; [].
+
+  Lemma pred_in_pred_uses:
+    forall A (p: A) pop,
+      PredIn p pop ->
+      In p (predicate_use pop).
+  Proof.
+    induction pop; crush.
+    - destr. inv Heqp1. inv H. now constructor.
+    - inv H.
+    - inv H.
+    - apply in_or_app. inv H. inv H1; intuition.
+    - apply in_or_app. inv H. inv H1; intuition.
+  Qed.
+
+  Lemma le_max_pred :
+    forall p max_pred,
+      Forall (fun x : positive => Ple x max_pred) (predicate_use p) ->
+      Ple (max_predicate p) max_pred.
+  Proof.
+    induction p; intros.
+    - intros; cbn. destruct_match. inv Heqp0. cbn in *. now inv H.
+    - cbn. unfold Ple. lia.
+    - cbn. unfold Ple. lia.
+    - cbn in *. eapply Forall_app in H. inv H. unfold Ple in *. eapply IHp1 in H0.
+      eapply IHp2 in H1. lia.
+    - cbn in *. eapply Forall_app in H. inv H. unfold Ple in *. eapply IHp1 in H0.
+      eapply IHp2 in H1. lia.
+  Qed.
+
+  (* Lemma storev_stack_bounds : *)
+  (*   forall m sp v dst m' hi, *)
+  (*     Mem.storev Mint32 m (Values.Vptr sp (Ptrofs.repr v)) dst = Some m' -> *)
+  (*     stack_bounds (Values.Vptr sp (Ptrofs.repr 0)) hi m -> *)
+  (*     v mod 4 = 0 -> *)
+  (*     0 <= v < hi. *)
+  (* Proof. *)
+  (*   intros. unfold stack_bounds in *. *)
+  (*   assert (0 <= v < hi \/ hi <= ) *)
+
+  Ltac tac :=
+    repeat match goal with
+           | [ _ : error _ _ = OK _ _ _ |- _ ] => discriminate
+           | [ _ : context[if (?x && ?y) then _ else _] |- _ ] =>
+             let EQ1 := fresh "EQ" in
+             let EQ2 := fresh "EQ" in
+             destruct x eqn:EQ1; destruct y eqn:EQ2; simpl in *
+           | [ _ : context[if ?x then _ else _] |- _ ] =>
+             let EQ := fresh "EQ" in
+             destruct x eqn:EQ; simpl in *
+           | [ H : ret _ _ = _  |- _ ] => inv H
+           | [ _ : context[match ?x with | _ => _ end] |- _ ] => destruct x
+           end.
+
+  Ltac inv_arr_access :=
+    match goal with
+    | [ _ : translate_arr_access ?chunk ?addr ?args _ _ = OK ?c _ _ |- _] =>
+      destruct c, chunk, addr, args; crush; tac; crush
+    end.
+
+  Lemma offset_expr_ok :
+    forall v z, (Z.to_nat
+                   (Integers.Ptrofs.unsigned
+                      (Integers.Ptrofs.divu
+                         (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ v))
+                                              (Integers.Ptrofs.of_int (Integers.Int.repr z)))
+                         (Integers.Ptrofs.repr 4)))
+                 = valueToNat (Int.divu (Int.add v (ZToValue z)) (ZToValue 4))).
+  Proof.
+    simplify_val. unfold valueToNat. unfold Int.divu, Ptrofs.divu.
+    pose proof Integers.Ptrofs.agree32_add as AGR.
+    unfold Integers.Ptrofs.agree32 in AGR.
+    assert (Ptrofs.unsigned (Ptrofs.add (Ptrofs.repr (Int.unsigned v))
+                                        (Ptrofs.repr (Int.unsigned (Int.repr z)))) =
+            Int.unsigned (Int.add v (ZToValue z))).
+    apply AGR; auto.
+    apply Ptrofs.unsigned_repr. apply Int.unsigned_range_2.
+    apply Ptrofs.unsigned_repr. apply Int.unsigned_range_2.
+    rewrite H. replace (Ptrofs.unsigned (Ptrofs.repr 4)) with 4.
+    replace (Int.unsigned (ZToValue 4)) with 4.
+    pose proof Ptrofs.agree32_repr. unfold Ptrofs.agree32 in *.
+    rewrite H0. trivial. auto.
+    unfold ZToValue. symmetry. apply Int.unsigned_repr.
+    unfold_constants. lia.
+    unfold ZToValue. symmetry. apply Int.unsigned_repr.
+    unfold_constants. lia.
+  Qed.
+
+  Lemma offset_expr_ok_2 :
+    forall v0 v1 z0 z1,
+      (Z.to_nat
+         (Integers.Ptrofs.unsigned
+            (Integers.Ptrofs.divu
+               (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ v0))
+                                    (Integers.Ptrofs.of_int
+                                       (Integers.Int.add
+                                          (Integers.Int.mul (valueToInt v1) (Integers.Int.repr z1))
+                                          (Integers.Int.repr z0)))) (Ptrofs.repr 4))))
+      = valueToNat (Int.divu (Int.add (Int.add v0 (ZToValue z0))
+                                      (Int.mul v1 (ZToValue z1))) (ZToValue 4)).
+    intros. unfold ZToValue, valueToNat, valueToInt, Ptrofs.divu, Int.divu, Ptrofs.of_int.
+
+    assert (H : (Ptrofs.unsigned
+             (Ptrofs.add (Ptrofs.repr (uvalueToZ v0))
+                (Ptrofs.of_int (Int.add (Int.mul (valueToInt v1) (Int.repr z1)) (Int.repr z0)))) /
+           Ptrofs.unsigned (Ptrofs.repr 4))
+                = (Int.unsigned (Int.add (Int.add v0 (Int.repr z0)) (Int.mul v1 (Int.repr z1))) /
+           Int.unsigned (Int.repr 4))).
+    { unfold ZToValue, valueToNat, valueToInt, Ptrofs.divu, Int.divu, Ptrofs.of_int.
+      rewrite Ptrofs.unsigned_repr by (unfold_constants; lia).
+      rewrite Int.unsigned_repr by (unfold_constants; lia).
+
+      unfold Ptrofs.of_int. rewrite Int.add_commut.
+      pose proof Integers.Ptrofs.agree32_add as AGR. unfold Ptrofs.agree32 in *.
+      erewrite AGR.
+      3: { unfold uvalueToZ. rewrite Ptrofs.unsigned_repr. trivial. apply Int.unsigned_range_2. }
+      3: { rewrite Ptrofs.unsigned_repr. trivial. apply Int.unsigned_range_2. }
+      rewrite Int.add_assoc. trivial. auto.
+    }
+
+    rewrite <- H. auto.
+
+  Qed.
+
+  Lemma offset_expr_ok_3 :
+    forall OFFSET,
+      Z.to_nat (Ptrofs.unsigned (Ptrofs.divu OFFSET (Ptrofs.repr 4)))
+      = valueToNat (ZToValue (Ptrofs.unsigned OFFSET / 4)).
+  Proof. auto. Qed.
+
+  Lemma storev_mod_ok' :
+    forall m sp' ptr src m',
+      0 <= ptr <= Ptrofs.max_unsigned ->
+      Mem.storev Mint32 m (Values.Val.offset_ptr (Values.Vptr sp' (Ptrofs.repr 0)) (Ptrofs.repr ptr)) src = Some m' ->
+      ptr mod 4 = 0.
+  Proof.
+    unfold Mem.storev; intros * BOUND **. repeat destruct_match; try discriminate.
+    eapply Mem.store_valid_access_3 in H.
+    unfold Mem.valid_access in H. inv H. apply Zdivide_mod. cbn -[Ptrofs.max_unsigned]in *.
+    inv Heqv. rewrite Ptrofs.add_unsigned in H1.
+    rewrite ! Ptrofs.unsigned_repr in H1; try lia. auto.
+    rewrite ! Ptrofs.unsigned_repr; lia.
+  Qed.
+
+  Lemma loadv_mod_ok' :
+    forall m sp' ptr v,
+      0 <= ptr <= Ptrofs.max_unsigned ->
+      Mem.loadv Mint32 m (Values.Val.offset_ptr (Values.Vptr sp' (Ptrofs.repr 0)) (Ptrofs.repr ptr)) = Some v ->
+      ptr mod 4 = 0.
+  Proof.
+    unfold Mem.loadv; intros * BOUND **. repeat destruct_match; try discriminate.
+    eapply Mem.load_valid_access in H.
+    unfold Mem.valid_access in H. inv H. apply Zdivide_mod. cbn -[Ptrofs.max_unsigned]in *.
+    inv Heqv0. rewrite Ptrofs.add_unsigned in H1.
+    rewrite ! Ptrofs.unsigned_repr in H1; try lia. auto.
+    rewrite ! Ptrofs.unsigned_repr; lia.
+  Qed.
+
+  Lemma offset_ptr_equiv :
+    forall sp' v,
+      Values.Val.offset_ptr (Values.Vptr sp' (Ptrofs.repr 0)) v = Values.Vptr sp' v.
+  Proof.
+    unfold Values.Val.offset_ptr; intros.
+    replace (Ptrofs.repr 0) with Ptrofs.zero by auto.
+    now rewrite Ptrofs.add_zero_l.
+  Qed.
+
+  Lemma loadv_mod_ok :
+    forall m sp' ptr v,
+      0 <= ptr <= Ptrofs.max_unsigned ->
+      Mem.loadv Mint32 m (Values.Vptr sp' (Ptrofs.repr ptr)) = Some v ->
+      ptr mod 4 = 0.
+  Proof.
+    intros. eapply loadv_mod_ok'; eauto.
+    rewrite offset_ptr_equiv; eauto.
+  Qed.
+
+  Lemma storev_mod_ok :
+    forall m sp' ptr src m',
+      0 <= ptr <= Ptrofs.max_unsigned ->
+      Mem.storev Mint32 m (Values.Vptr sp' (Ptrofs.repr ptr)) src = Some m' ->
+      ptr mod 4 = 0.
+  Proof.
+    intros. eapply storev_mod_ok'; eauto.
+    rewrite offset_ptr_equiv; eauto.
+  Qed.
+
+  Lemma loadv_mod_ok2 :
+    forall m sp' v v',
+      Mem.loadv Mint32 m (Values.Vptr sp' v) = Some v' ->
+      (Ptrofs.unsigned v) mod 4 = 0.
+  Proof.
+    unfold Mem.loadv; intros. repeat destruct_match; try discriminate.
+    eapply Mem.load_valid_access in H.
+    unfold Mem.valid_access in H. inv H. apply Zdivide_mod. cbn -[Ptrofs.max_unsigned]in *.
+    auto.
+  Qed.
+
+  Lemma storev_mod_ok2 :
+    forall m sp' src m' v,
+      Mem.storev Mint32 m (Values.Vptr sp' v) src = Some m' ->
+      (Ptrofs.unsigned v) mod 4 = 0.
+  Proof.
+    unfold Mem.storev; intros. repeat destruct_match; try discriminate.
+    eapply Mem.store_valid_access_3 in H.
+    unfold Mem.valid_access in H. inv H. apply Zdivide_mod. cbn -[Ptrofs.max_unsigned]in *.
+    auto.
+  Qed.
+
+  Lemma storev_exists_ptr:
+    forall m v src m',
+      Mem.storev Mint32 m v src = Some m' ->
+      exists sp v', v = Values.Vptr sp v'.
+  Proof.
+    intros.
+    unfold Mem.storev in *. destruct_match; try discriminate.
+    subst. eauto.
+  Qed.
+
+  Lemma val_add_stack_based :
+    forall v1 v2 sp,
+      stack_based v1 sp ->
+      stack_based v2 sp ->
+      stack_based (Values.Val.add v1 v2) sp.
+  Proof.
+    intros. destruct v1, v2; auto.
+    inv H. inv H0. cbn; auto.
+  Qed.
+
+  Lemma ptrofs_unsigned_add_0:
+    forall x0,
+      Ptrofs.unsigned (Ptrofs.add (Ptrofs.repr 0) (Ptrofs.repr (Ptrofs.unsigned x0))) = Ptrofs.unsigned x0.
+  Proof.
+    intros. replace (Ptrofs.repr 0) with (Ptrofs.zero) by auto.
+    rewrite Ptrofs.add_zero_l. rewrite Ptrofs.unsigned_repr; auto.
+    apply Ptrofs.unsigned_range_2.
+  Qed.
+
+  Lemma exists_ptr_add_int :
+    forall a b sp' x0,
+      Values.Val.add a (Values.Vint b) = Values.Vptr sp' x0 ->
+      exists a', a = Values.Vptr sp' a'.
+  Proof.
+    intros. destruct a; eauto; cbn in *; try discriminate.
+    assert (Xx: Archi.ptr64 = false) by auto. rewrite Xx in H. inv H. eauto.
+  Qed.
+
+  Lemma transl_arr_access_correct :
+    forall addr args e rs ps m sp a chnk src m' s f pc s' m_ asr arr,
+      translate_arr_access chnk addr args m_.(DHTL.mod_stk) = OK e ->
+      Op.eval_addressing ge sp addr (List.map (fun r => Registers.Regmap.get r rs) args) = Some a ->
+      Mem.storev chnk m a (Registers.Regmap.get src rs) = Some m' ->
+      match_states (GibleSubPar.State s f sp pc rs ps m) (DHTL.State s' m_ pc asr arr) ->
+      exists x, expr_runp tt asr arr e x.
+  Proof.
+    assert (HARCH: Archi.ptr64 = false) by auto.
+    intros. unfold translate_arr_access in *. repeat destr.
+    destruct_match; try discriminate; repeat destr.
+    - inv H. cbn in *. unfold Op.eval_addressing in *. rewrite HARCH in H0.
+      cbn in *. inv H0. inv H2. unfold stack_bounds in *.
+      exploit storev_exists_ptr; eauto. simplify.
+      assert (stack_based (Values.Vint (Int.repr z)) sp') by (cbn; auto).
+      assert (stack_based (rs !! r) sp') by (cbn; auto).
+      eapply val_add_stack_based in H0; eauto. rewrite H in H0. cbn in *. inv H0.
+      rewrite H in H1. exploit storev_mod_ok2; eauto; intros.
+      specialize (BOUNDS (Ptrofs.unsigned x0) rs !! src).
+      pose proof (ptrofs_unsigned_lt_int_max x0).
+      assert (0 <= Ptrofs.unsigned x0 < fn_stacksize f \/ fn_stacksize f <= Ptrofs.unsigned x0 <= Int.max_unsigned) by lia.
+      inv H4.
+      + inv MARR. inv H4. eexists. econstructor. econstructor. econstructor. econstructor.
+        eauto. econstructor. cbn. eauto. econstructor. cbn. unfold ZToValue.
+        unfold Int.zero. unfold Int.eq. rewrite ! Int.unsigned_repr by crush.
+        cbn. eauto. (* exploit exists_ptr_add_int; eauto. intros (a & HPTR). *)
+        (* rewrite HPTR in H. cbn in H. *)
+        assert (HARCHI: Archi.ptr64 = false) by auto.
+        unfold arr_assocmap_lookup. setoid_rewrite H6. eauto.
+      + apply BOUNDS in H5; auto. inv H5. rewrite ptrofs_unsigned_add_0 in H6.
+        unfold Mem.storev in H1. rewrite H6 in H1. discriminate.
+    - inv H. inv H2. inv MARR. inv H. repeat econstructor. unfold arr_assocmap_lookup.
+      setoid_rewrite H2. auto.
+    - inv H. inv H2. inv MARR. inv H. repeat econstructor. unfold arr_assocmap_lookup.
+      setoid_rewrite H2. auto.
+  Qed.
+
+  Lemma transl_step_state_correct_single_false_standard :
+    forall f bb curr_p next_p m_ stmnt stmnt' asr0 asa0 asr asa n max_reg max_pred rs ps sp m o,
+      (* (fn_code f) ! pc = Some bb -> *)
+      transf_instr n (mk_ctrl f) (curr_p, stmnt) bb = OK (next_p, stmnt') ->
+      stmnt_runp tt (e_assoc asr0) (e_assoc_arr (DHTL.mod_stk m_) (DHTL.mod_stk_len m_) asa0) stmnt (e_assoc asr) (e_assoc_arr (DHTL.mod_stk m_) (DHTL.mod_stk_len m_) asa) ->
+      Forall (fun x => Ple x max_pred) (pred_uses bb) ->
+      Ple (max_predicate curr_p) max_pred ->
+      eval_predf ps curr_p = false ->
+      match_assocmaps max_reg max_pred rs ps asr ->
+      step_instr ge sp (Iexec (mk_instr_state rs ps m)) bb o ->
+      (forall a b c d e, bb <> RBstore a b c d e) ->
+      (forall a b, bb <> RBexit a b) ->
+      exists asr' asa', stmnt_runp tt (e_assoc asr0) (e_assoc_arr (DHTL.mod_stk m_) (DHTL.mod_stk_len m_) asa0) stmnt' 
+        (e_assoc asr') (e_assoc_arr (DHTL.mod_stk m_) (DHTL.mod_stk_len m_) asa') 
+        /\ unchanged asr asa asr' asa'
+        /\ Ple (max_predicate next_p) max_pred 
+        /\ eval_predf ps next_p = false.
+  Proof.
+    destruct bb; intros * HTRANSF HSTMNT HFRL HPLE HEVAL HMATCH HSTEP_INSTR HNO_RBSTORE HNO_EXIT.
+    - cbn in HTRANSF. inv HTRANSF. exists asr, asa; repeat split; eauto.
+    - cbn -[translate_predicate deep_simplify] in HTRANSF; unfold Errors.bind in HTRANSF.
+      destruct_match; try discriminate.
+      assert (forall A a b, @OK A a = OK b -> a = b) by now inversion 1. apply H in HTRANSF.
+      assert (forall A B (a b: A) (c d: B), (a, c) = (b, d) -> a = b /\ c = d) by now inversion 1. 
+      apply H0 in HTRANSF. destruct HTRANSF. rewrite H1 in *. rewrite <- H2 in *.
+      assert (eval_predf ps (Pand next_p (dfltp o)) = false).
+      { rewrite eval_predf_Pand. subst. rewrite HEVAL. auto. }
+      assert (Ple (max_predicate (Pand next_p (dfltp o))) max_pred).
+      { cbn. cbn in HFRL. destruct o; cbn; [|unfold Ple in *; lia].
+        eapply le_max_pred in HFRL. unfold Ple in *; lia. }
+      exploit transl_predicate_correct2; eauto. intros (asr' & HSTMNT' & FRL).
+      exists asr', asa. repeat split; eauto.
+      econstructor; eauto.
+    - cbn -[translate_predicate deep_simplify] in HTRANSF; unfold Errors.bind in HTRANSF.
+      destruct_match; try discriminate.
+      assert (forall A a b, @OK A a = OK b -> a = b) by now inversion 1. apply H in HTRANSF.
+      assert (forall A B (a b: A) (c d: B), (a, c) = (b, d) -> a = b /\ c = d) by now inversion 1. 
+      apply H0 in HTRANSF. destruct HTRANSF. rewrite H1 in *. rewrite <- H2 in *.
+      assert (eval_predf ps (Pand next_p (dfltp o)) = false).
+      { rewrite eval_predf_Pand. subst. rewrite HEVAL. auto. }
+      assert (Ple (max_predicate (Pand next_p (dfltp o))) max_pred).
+      { cbn. cbn in HFRL. destruct o; cbn; [|unfold Ple in *; lia].
+        eapply le_max_pred in HFRL. unfold Ple in *; lia. }
+      exploit transl_predicate_correct2; eauto. intros (asr' & HSTMNT' & FRL).
+      exists asr', asa. repeat split; eauto.
+      econstructor; eauto.
+    - exfalso; eapply HNO_RBSTORE; auto.
+    - cbn -[translate_predicate deep_simplify] in HTRANSF; unfold Errors.bind in HTRANSF.
+      destruct_match; try discriminate.
+      assert (forall A a b, @OK A a = OK b -> a = b) by now inversion 1. apply H in HTRANSF.
+      assert (forall A B (a b: A) (c d: B), (a, c) = (b, d) -> a = b /\ c = d) by now inversion 1. 
+      apply H0 in HTRANSF. destruct HTRANSF. rewrite H1 in *. rewrite <- H2 in *.
+      assert (eval_predf ps (Pand next_p (dfltp o)) = false).
+      { rewrite eval_predf_Pand. subst. rewrite HEVAL. auto. }
+      assert (Ple (max_predicate (Pand next_p (dfltp o))) max_pred).
+      { cbn. cbn in HFRL. destruct o; cbn; [|unfold Ple in *; lia]. inv HFRL.
+        eapply le_max_pred in H7. unfold Ple in *; lia. }
+      exploit transl_predicate_correct2; eauto. intros (asr' & HSTMNT' & FRL).
+      exists asr', asa. repeat split; eauto.
+      econstructor; eauto.
+    - exfalso; eapply HNO_EXIT; auto.
+  Qed.
+
+  Lemma unchanged_implies_match :
+    forall s f sp rs ps m s' m_ pc asr' asa' asa asr,
+      unchanged asr' asa' asr asa ->
+      match_states (GibleSubPar.State s f sp pc rs ps m) (DHTL.State s' m_ pc asr' asa') ->
+      match_states (GibleSubPar.State s f sp pc rs ps m) (DHTL.State s' m_ pc asr asa).
+  Proof.
+    intros. inv H. inv H0.
+    econstructor; auto.
+    - econstructor; intros; inv MASSOC; rewrite <- H1; eauto.
+    - unfold state_st_wf in *. destruct 
+
+  Lemma transl_step_state_correct_single_false_standard_top :
+    forall f s s' pc bb curr_p next_p m_ stmnt stmnt' asr0 asa0 asr asa n rs ps sp m o,
+      (* (fn_code f) ! pc = Some bb -> *)
+      transf_instr n (mk_ctrl f) (curr_p, stmnt) bb = OK (next_p, stmnt') ->
+      stmnt_runp tt (e_assoc asr0) (e_assoc_arr (DHTL.mod_stk m_) (DHTL.mod_stk_len m_) asa0) 
+        stmnt (e_assoc asr) (e_assoc_arr (DHTL.mod_stk m_) (DHTL.mod_stk_len m_) asa) ->
+      Forall (fun x => Ple x (max_pred_function f)) (pred_uses bb) ->
+      Ple (max_predicate curr_p) (max_pred_function f) ->
+      eval_predf ps curr_p = false ->
+      match_states (GibleSubPar.State s f sp pc rs ps m) (DHTL.State s' m_ pc asr asa) ->
+      step_instr ge sp (Iexec (mk_instr_state rs ps m)) bb o ->
+      exists asr' asa', 
+        stmnt_runp tt (e_assoc asr0) (e_assoc_arr (DHTL.mod_stk m_) (DHTL.mod_stk_len m_) asa0) stmnt' 
+          (e_assoc asr') (e_assoc_arr (DHTL.mod_stk m_) (DHTL.mod_stk_len m_) asa') 
+        /\ match_states (GibleSubPar.State s f sp pc rs ps m) (DHTL.State s' m_ pc asr' asa')
+        /\ Ple (max_predicate next_p) (max_pred_function f)
+        /\ eval_predf ps next_p = false.
+  Proof.
+    intros * HTRANSF HSTMNT HFRL HPLE HEVAL HMATCH HSTEP. destruct bb.
+    - inv HMATCH.
+      exploit transl_step_state_correct_single_false_standard; eauto; try discriminate.
+      intros (asr' & asa' & HSTMNT' & HUNCHG & HPLE' & HEVAL').
+      exists asr', asa'. repeat split; auto.
+
+  Lemma iterm_intermediate_state :
+    forall sp rs pr m bb rs' pr' m' cf,
+      SubParBB.step_instr_list ge sp (Iexec {| is_rs := rs; is_ps := pr; is_mem := m |}) bb
+               (Iterm {| is_rs := rs'; is_ps := pr'; is_mem := m' |} cf) ->
+      exists bb' i bb'', 
+        SubParBB.step_instr_list ge sp (Iexec {| is_rs := rs; is_ps := pr; is_mem := m |}) bb'
+               (Iexec {| is_rs := rs'; is_ps := pr'; is_mem := m' |})
+        /\ step_instr ge sp (Iexec {| is_rs := rs'; is_ps := pr'; is_mem := m' |}) i (Iterm {| is_rs := rs'; is_ps := pr'; is_mem := m' |} cf)
+        /\ bb = bb' ++ (i :: bb'').
+  Proof. Admitted.
+
+  Lemma transl_step_state_correct_instr :
+    forall s f sp bb pc curr_p next_p rs rs' m m' pr pr' m_ s' stmnt stmnt' asr0 asa0 asr asa n,
+      (* (fn_code f) ! pc = Some bb -> *)
+      mfold_left (transf_instr n (mk_ctrl f)) bb (OK (curr_p, stmnt)) = OK (next_p, stmnt') ->
+      stmnt_runp tt (e_assoc asr0) (e_assoc_arr (DHTL.mod_stk m_) (DHTL.mod_stk_len m_) asa0) stmnt (e_assoc asr) (e_assoc_arr (DHTL.mod_stk m_) (DHTL.mod_stk_len m_) asa) ->
+      eval_predf pr curr_p = true ->
+      SubParBB.step_instr_list ge sp (Iexec {| is_rs := rs; is_ps := pr; is_mem := m |}) bb
+             (Iexec {| is_rs := rs'; is_ps := pr'; is_mem := m' |}) ->
+      match_states (GibleSubPar.State s f sp pc rs pr m) (DHTL.State s' m_ pc asr asa) ->
+      exists asr' asa',
+        stmnt_runp tt (e_assoc asr0) (e_assoc_arr (DHTL.mod_stk m_) (DHTL.mod_stk_len m_) asa0) stmnt' (e_assoc asr') (e_assoc_arr (DHTL.mod_stk m_) (DHTL.mod_stk_len m_) asa')
+        /\ match_states (GibleSubPar.State s f sp pc rs' pr' m') (DHTL.State s' m_ pc asr' asa')
+        /\ eval_predf pr' next_p = true.
+  Proof. Admitted.
+
+  Lemma transl_step_state_correct_instr_false :
+    forall f bb curr_p next_p m_ stmnt stmnt' asr0 asa0 asr asa n max_reg max_pred rs ps,
+      (* (fn_code f) ! pc = Some bb -> *)
+      mfold_left (transf_instr n (mk_ctrl f)) bb (OK (curr_p, stmnt)) = OK (next_p, stmnt') ->
+      stmnt_runp tt (e_assoc asr0) (e_assoc_arr (DHTL.mod_stk m_) (DHTL.mod_stk_len m_) asa0) stmnt (e_assoc asr) (e_assoc_arr (DHTL.mod_stk m_) (DHTL.mod_stk_len m_) asa) ->
+      Forall (fun i => Forall (fun x : positive => Ple x max_pred) (pred_uses i)) bb ->
+      Ple (max_predicate curr_p) max_pred ->
+      eval_predf ps curr_p = false ->
+      match_assocmaps max_reg max_pred rs ps asr ->
+      stmnt_runp tt (e_assoc asr0) (e_assoc_arr (DHTL.mod_stk m_) (DHTL.mod_stk_len m_) asa0) stmnt' (e_assoc asr) (e_assoc_arr (DHTL.mod_stk m_) (DHTL.mod_stk_len m_) asa).
+  Proof.
+    induction bb.
+    - cbn; inversion 2; auto.
+    - intros * HFOLD HSTMNT HFRL HPLE HEVAL HMATCH. exploit mfold_left_cons; eauto.
+      intros (x' & y' & HFOLD' & HTRANS & HINV). inv HINV. destruct y'.
+  (*     exploit transl_step_state_correct_single_false; eauto; intros. inv HFRL; eauto. *)
+  (*     inv H. inv H1. *)
+  (*     exploit IHbb; eauto. inv HFRL; eauto. *)
+  (* Qed. *) Admitted.
+
   Lemma transl_step_state_correct_instr_state :
-    forall s f sp bb pc curr_p next_p rs rs' m m' pr pr' m_ s' stmnt stmnt' asr0 asa0 asr asa cf pc',
+    forall s f sp bb pc curr_p next_p rs rs' m m' pr pr' m_ s' stmnt stmnt' asr0 asa0 asr asa cf pc' n,
       (* (fn_code f) ! pc = Some bb -> *)
-      mfold_left (transf_instr (mk_ctrl f)) bb (OK (curr_p, stmnt)) = OK (next_p, stmnt') ->
+      mfold_left (transf_instr n (mk_ctrl f)) bb (OK (curr_p, stmnt)) = OK (next_p, stmnt') ->
       stmnt_runp tt (e_assoc asr0) (e_assoc_arr (DHTL.mod_stk m_) (DHTL.mod_stk_len m_) asa0) stmnt (e_assoc asr) (e_assoc_arr (DHTL.mod_stk m_) (DHTL.mod_stk_len m_) asa) ->
       eval_predf pr curr_p = true ->
       SubParBB.step_instr_list ge sp (Iexec {| is_rs := rs; is_ps := pr; is_mem := m |}) bb
@@ -1457,30 +2275,60 @@ Opaque Mem.alloc.
       exists asr' asa',
         stmnt_runp tt (e_assoc asr0) (e_assoc_arr (DHTL.mod_stk m_) (DHTL.mod_stk_len m_) asa0) stmnt' (e_assoc asr') (e_assoc_arr (DHTL.mod_stk m_) (DHTL.mod_stk_len m_) asa')
         /\ match_states (GibleSubPar.State s f sp pc' rs' pr' m') (DHTL.State s' m_ pc' asr' asa').
-  Proof. Admitted.
+  Proof. 
+    intros * HFOLD HSTMNT HEVAL HSTEP HSTEPCF HMATCH.
+    exploit iterm_intermediate_state; eauto.
+    intros (bb' & i & bb'' & HSTEP' & HSTEPINSTR & HBB). subst.
+    exploit mfold_left_app; eauto. intros (y' & HFOLD1 & HFOLD2).
+    exploit mfold_left_cons; eauto. intros (x' & y_other & HFOLDFINAL & HINSTR & HSUBST).
+    inv HSUBST.
+    destruct x'. destruct y_other.
+    exploit transl_step_state_correct_instr; try eapply HFOLD1; eauto.
+    intros (asr' & asa' & HSTMNT' & HMATCH' & HNEXT).
+    exploit transl_step_state_correct_single_instr_term; eauto.
+    intros (asr'0 & asa'0 & HSTMNT'' & HMATCH'' & HNEXT'').
+    exploit transl_step_state_correct_instr_false; eauto.
+  Admitted.
 
   Lemma transl_step_state_correct_instr_return :
-    forall s f sp bb pc curr_p next_p rs rs' m m' pr pr' m_ s' stmnt stmnt' asr0 asa0 asr asa cf v,
+    forall s f sp bb pc curr_p next_p rs rs' m m' pr pr' m_ s' stmnt stmnt' asr0 asa0 asr asa cf v m'' n,
       (* (fn_code f) ! pc = Some bb -> *)
-      mfold_left (transf_instr (mk_ctrl f)) bb (OK (curr_p, stmnt)) = OK (next_p, stmnt') ->
+      mfold_left (transf_instr n (mk_ctrl f)) bb (OK (curr_p, stmnt)) = OK (next_p, stmnt') ->
       stmnt_runp tt (e_assoc asr0) (e_assoc_arr (DHTL.mod_stk m_) (DHTL.mod_stk_len m_) asa0) stmnt (e_assoc asr) (e_assoc_arr (DHTL.mod_stk m_) (DHTL.mod_stk_len m_) asa) ->
       eval_predf pr curr_p = true ->
       SubParBB.step_instr_list ge sp (Iexec {| is_rs := rs; is_ps := pr; is_mem := m |}) bb
              (Iterm {| is_rs := rs'; is_ps := pr'; is_mem := m' |} cf) ->
-      step_cf_instr ge (GibleSubPar.State s f sp pc rs' pr' m') cf Events.E0 (GibleSubPar.Returnstate s v m') ->
+      step_cf_instr ge (GibleSubPar.State s f sp pc rs' pr' m') cf Events.E0 (GibleSubPar.Returnstate s v m'') ->
       match_states (GibleSubPar.State s f sp pc rs pr m) (DHTL.State s' m_ pc asr asa) ->
       exists asr' asa' retval,
         stmnt_runp tt (e_assoc asr0) (e_assoc_arr (DHTL.mod_stk m_) (DHTL.mod_stk_len m_) asa0) stmnt' (e_assoc asr') (e_assoc_arr (DHTL.mod_stk m_) (DHTL.mod_stk_len m_) asa')
         /\ val_value_lessdef v retval
         /\ asr'!(m_.(DHTL.mod_finish)) = Some (ZToValue 1)
         /\ asr'!(m_.(DHTL.mod_return)) = Some retval
-        /\ match_states (GibleSubPar.Returnstate s v m') (DHTL.Returnstate s' retval).
-  Proof. Admitted.
+        /\ asr'!(m_.(DHTL.mod_st)) = Some (posToValue n).
+  Proof.
+    intros * HFOLD HSTMNT HEVAL HSTEP HSTEPCF HMATCH.
+    exploit iterm_intermediate_state; eauto.
+    intros (bb' & i & bb'' & HSTEP' & HSTEPINSTR & HBB). subst.
+    exploit mfold_left_app; eauto. intros (y' & HFOLD1 & HFOLD2).
+    exploit mfold_left_cons; eauto. intros (x' & y_other & HFOLDFINAL & HINSTR & HSUBST).
+    inv HSUBST.
+    destruct x'. destruct y_other.
+    exploit transl_step_state_correct_instr; try eapply HFOLD1; eauto.
+    intros (asr' & asa' & HSTMNT' & HMATCH' & HNEXT).
+    exploit transl_step_state_correct_single_instr_term_return; eauto.
+    intros (v' & HSTMNT'' & HEVAL2 & HEVAL3).
+    exploit transl_step_state_correct_instr_false; eauto.
+    intros.
+    pose proof (mod_ordering_wf m_). unfold module_ordering in H0. inv H0. inv H2.
+    eexists. exists asa'. exists v'.
+    repeat split; eauto; repeat rewrite PTree.gso by lia; apply PTree.gss.
+  Qed.
 
   Lemma transl_step_state_correct_chained_state :
-    forall s f sp bb pc pc' curr_p next_p rs rs' m m' pr pr' m_ s' stmnt stmnt' asr0 asa0 asr asa cf,
+    forall s f sp bb pc pc' curr_p next_p rs rs' m m' pr pr' m_ s' stmnt stmnt' asr0 asa0 asr asa cf n,
       (* (fn_code f) ! pc = Some bb -> *)
-      mfold_left (transf_chained_block (mk_ctrl f)) bb (OK (curr_p, stmnt)) = OK (next_p, stmnt') ->
+      mfold_left (transf_chained_block n (mk_ctrl f)) bb (OK (curr_p, stmnt)) = OK (next_p, stmnt') ->
       stmnt_runp tt (e_assoc asr0) (e_assoc_arr (DHTL.mod_stk m_) (DHTL.mod_stk_len m_) asa0) stmnt (e_assoc asr) (e_assoc_arr (DHTL.mod_stk m_) (DHTL.mod_stk_len m_) asa) ->
       eval_predf pr curr_p = true ->
       SubParBB.step ge sp (Iexec {| is_rs := rs; is_ps := pr; is_mem := m |}) bb
@@ -1493,10 +2341,10 @@ Opaque Mem.alloc.
   Proof. Abort.
 
   Lemma transl_step_through_cfi' :
-    forall bb ctrl curr_p stmnt next_p stmnt' p cf,
-      mfold_left (transf_instr ctrl) bb (OK (curr_p, stmnt)) = OK (next_p, stmnt') ->
+    forall bb ctrl curr_p stmnt next_p stmnt' p cf n,
+      mfold_left (transf_instr n ctrl) bb (OK (curr_p, stmnt)) = OK (next_p, stmnt') ->
       In (RBexit p cf) bb ->
-      exists curr_p' stmnt'', translate_cfi ctrl (Some (Pand curr_p' (dfltp p))) cf = OK stmnt''.
+      exists curr_p' stmnt'', translate_cfi n ctrl (Some (Pand curr_p' (dfltp p))) cf = OK stmnt'' /\ check_cfi n cf = OK tt.
   Proof.
     induction bb.
     - inversion 2.
@@ -1506,15 +2354,15 @@ Opaque Mem.alloc.
       inversion HSUBST. inv H0. clear HSUBST.
       inv HIN; destruct y'; eauto.
       cbn in HTRANSF. unfold Errors.bind in HTRANSF. repeat (destruct_match; try discriminate; []).
-      inv HTRANSF. eauto.
+      inv HTRANSF. destruct u. eauto.
   Qed.
 
   Lemma transl_step_through_cfi :
-    forall bb ctrl curr_p stmnt next_p stmnt' l p cf,
-      mfold_left (transf_chained_block ctrl) bb (OK (curr_p, stmnt)) = OK (next_p, stmnt') ->
+    forall bb ctrl curr_p stmnt next_p stmnt' l p cf n,
+      mfold_left (transf_chained_block n ctrl) bb (OK (curr_p, stmnt)) = OK (next_p, stmnt') ->
       In l bb ->
       In (RBexit p cf) l ->
-      exists curr_p' stmnt'', translate_cfi ctrl (Some (Pand curr_p' (dfltp p))) cf = OK stmnt''.
+      exists curr_p' stmnt'', translate_cfi n ctrl (Some (Pand curr_p' (dfltp p))) cf = OK stmnt''.
   Proof.
     induction bb.
     - inversion 2.
@@ -1524,6 +2372,7 @@ Opaque Mem.alloc.
       destruct y'. inv HSUBST.
       inv HIN1; eauto.
       exploit transl_step_through_cfi'; eauto.
+      simplify. eauto.
   Qed.
 
   Lemma cf_in_bb_subparbb' :
@@ -1556,8 +2405,8 @@ Opaque Mem.alloc.
   Qed.
 
   Lemma match_states_cf_events_translate_cfi:
-    forall T1 cf T2 p t ctrl stmnt,
-      translate_cfi ctrl p cf = OK stmnt ->
+    forall T1 cf T2 p t ctrl stmnt n,
+      translate_cfi n ctrl p cf = OK stmnt ->
       step_cf_instr ge T1 cf t T2 ->
       t = Events.E0.
   Proof.
@@ -1566,8 +2415,8 @@ Opaque Mem.alloc.
   Qed.
 
   Lemma match_states_cf_states_translate_cfi:
-    forall T1 cf T2 p t ctrl stmnt,
-      translate_cfi ctrl p cf = OK stmnt ->
+    forall T1 cf T2 p t ctrl stmnt n,
+      translate_cfi n ctrl p cf = OK stmnt ->
       step_cf_instr ge T1 cf t T2 ->
       exists s f sp pc rs pr m,
         T1 = GibleSubPar.State s f sp pc rs pr m
@@ -1578,106 +2427,18 @@ Opaque Mem.alloc.
     destruct cf; try discriminate; inv HSTEP; try (now repeat econstructor).
   Qed.
 
-  Lemma one_ne_zero:
-    Int.repr 1 <> Int.repr 0.
-  Proof.
-    unfold not; intros.
-    assert (Int.unsigned (Int.repr 1) = Int.unsigned (Int.repr 0)) by (now rewrite H).
-    rewrite ! Int.unsigned_repr in H0 by crush. lia.
-  Qed.
-
-  Lemma int_and_boolToValue :
-    forall b1 b2,
-      Int.and (boolToValue b1) (boolToValue b2) = boolToValue (b1 && b2).
-  Proof.
-    destruct b1; destruct b2; cbn; unfold boolToValue; unfold natToValue;
-    replace (Z.of_nat 1) with 1 by auto;
-    replace (Z.of_nat 0) with 0 by auto.
-    - apply Int.and_idem.
-    - apply Int.and_zero.
-    - apply Int.and_zero_l.
-    - apply Int.and_zero.
-  Qed.
-
-  Lemma int_or_boolToValue :
-    forall b1 b2,
-      Int.or (boolToValue b1) (boolToValue b2) = boolToValue (b1 || b2).
-  Proof.
-    destruct b1; destruct b2; cbn; unfold boolToValue; unfold natToValue;
-    replace (Z.of_nat 1) with 1 by auto;
-    replace (Z.of_nat 0) with 0 by auto.
-    - apply Int.or_idem.
-    - apply Int.or_zero.
-    - apply Int.or_zero_l.
-    - apply Int.or_zero_l.
-  Qed.
-
-  Lemma translate_pred_correct :
-    forall curr_p pr asr asa,
-      (forall r, Ple r (max_predicate curr_p) ->
-          find_assocmap 1 (pred_enc r) asr = boolToValue (PMap.get r pr)) ->
-      expr_runp tt asr asa (pred_expr curr_p) (boolToValue (eval_predf pr curr_p)).
-  Proof.
-    induction curr_p.
-    - intros * HFRL. cbn. destruct p as [b p']. destruct b.
-      + constructor. eapply HFRL. cbn. unfold Ple. lia.
-      + econstructor. constructor. eapply HFRL. cbn. unfold Ple; lia.
-        econstructor. cbn. f_equal. unfold boolToValue.
-        f_equal. destruct pr !! p' eqn:?. cbn.
-        rewrite Int.eq_false; auto. unfold natToValue.
-        replace (Z.of_nat 1) with 1 by auto. unfold Int.zero.
-        apply one_ne_zero.
-        cbn. rewrite Int.eq_true; auto.
-    - intros. cbn. constructor.
-    - intros. cbn. constructor.
-    - cbn -[eval_predf]; intros. econstructor. eapply IHcurr_p1. intros. eapply H.
-      unfold Ple in *. lia.
-      eapply IHcurr_p2; intros. eapply H. unfold Ple in *; lia.
-      cbn -[eval_predf]. f_equal. symmetry. apply int_and_boolToValue.
-    - cbn -[eval_predf]; intros. econstructor. eapply IHcurr_p1. intros. eapply H.
-      unfold Ple in *. lia.
-      eapply IHcurr_p2; intros. eapply H. unfold Ple in *; lia.
-      cbn -[eval_predf]. f_equal. symmetry. apply int_or_boolToValue.
-  Qed.
-
-  Lemma max_predicate_deep_simplify' :
-    forall peq curr r,
-      (r <= max_predicate (deep_simplify' peq curr))%positive ->
-      (r <= max_predicate curr)%positive.
-  Proof.
-    destruct curr; cbn -[deep_simplify']; auto.
-    - intros. unfold deep_simplify' in H.
-      destruct curr1; destruct curr2; try (destruct_match; cbn in *); lia.
-    - intros. unfold deep_simplify' in H.
-      destruct curr1; destruct curr2; try (destruct_match; cbn in *); lia.
-  Qed.
-
-  Lemma max_predicate_deep_simplify :
-    forall peq curr r,
-      (r <= max_predicate (deep_simplify peq curr))%positive ->
-      (r <= max_predicate curr)%positive.
-  Proof.
-    induction curr; try solve [cbn; auto]; cbn -[deep_simplify'] in *.
-    - intros. apply max_predicate_deep_simplify' in H. cbn -[deep_simplify'] in *.
-      assert (HX: (r <= max_predicate (deep_simplify peq curr1))%positive \/ (r <= max_predicate (deep_simplify peq curr2))%positive) by lia.
-      inv HX; [eapply IHcurr1 in H0 | eapply IHcurr2 in H0]; lia.
-    - intros. apply max_predicate_deep_simplify' in H. cbn -[deep_simplify'] in *.
-      assert (HX: (r <= max_predicate (deep_simplify peq curr1))%positive \/ (r <= max_predicate (deep_simplify peq curr2))%positive) by lia.
-      inv HX; [eapply IHcurr1 in H0 | eapply IHcurr2 in H0]; lia.
-  Qed.
-
   Lemma translate_cfi_goto:
-    forall pr curr_p pc s ctrl asr asa,
+    forall pr curr_p pc s ctrl asr asa n,
       (forall r, Ple r (max_predicate curr_p) ->
         find_assocmap 1 (pred_enc r) asr = boolToValue (PMap.get r pr)) ->
       eval_predf pr curr_p = true ->
-      translate_cfi ctrl (Some curr_p) (RBgoto pc) = OK s ->
+      translate_cfi n ctrl (Some curr_p) (RBgoto pc) = OK s ->
       stmnt_runp tt (e_assoc asr) asa s
         (e_assoc (AssocMap.set ctrl.(ctrl_st) (posToValue pc) asr)) asa.
   Proof.
     intros * HPLE HEVAL HTRANSL. unfold translate_cfi in *.
     inversion_clear HTRANSL as []. destruct_match.
-    - constructor. constructor. econstructor. eapply translate_pred_correct.
+    - constructor. constructor. econstructor. eapply pred_expr_correct.
       intros. unfold Ple in *. eapply HPLE.
       now apply max_predicate_deep_simplify in H.
       eauto. constructor. rewrite eval_predf_deep_simplify. rewrite HEVAL. auto.
@@ -1685,8 +2446,8 @@ Opaque Mem.alloc.
   Qed.
 
   Lemma translate_cfi_goto_none:
-    forall pc s ctrl asr asa,
-      translate_cfi ctrl None (RBgoto pc) = OK s ->
+    forall pc s ctrl asr asa n,
+      translate_cfi n ctrl None (RBgoto pc) = OK s ->
       stmnt_runp tt (e_assoc asr) asa s
         (e_assoc (AssocMap.set ctrl.(ctrl_st) (posToValue pc) asr)) asa.
   Proof. intros; inversion_clear H as []; repeat constructor. Qed.
@@ -1727,7 +2488,7 @@ Opaque Mem.alloc.
     forall l ctrl d_in d_out pc bb,
       mfold_left (transf_seq_block ctrl) l (OK d_in) = OK d_out ->
       In (pc, bb) l ->
-      exists pred' stmnt, transf_chained_block ctrl (Ptrue, Vskip) (concat bb) = OK (pred', stmnt)
+      exists n pred' stmnt, transf_chained_block n ctrl (Ptrue, Vskip) (concat bb) = OK (pred', stmnt)
         /\ d_out ! pc = Some stmnt.
   Proof.
     induction l; [now inversion 2|].
@@ -1746,10 +2507,33 @@ Opaque Mem.alloc.
     forall ctrl d_in d_out pc bb c,
       mfold_left (transf_seq_block ctrl) (PTree.elements c) (OK d_in) = OK d_out ->
       c ! pc = Some bb ->
-      exists pred' stmnt, transf_chained_block ctrl (Ptrue, Vskip) (concat bb) = OK (pred', stmnt)
+      exists n pred' stmnt, transf_chained_block n ctrl (Ptrue, Vskip) (concat bb) = OK (pred', stmnt)
         /\ d_out ! pc = Some stmnt.
   Proof. intros. eapply transl_spec_correct'; eauto using PTree.elements_correct. Qed.
 
+  Lemma lt_check_step_cf_instr :
+    forall s f sp pc rs pr m cf t s' f' sp' x rs' pr' m' ctrl p st n,
+      translate_cfi n ctrl p cf = OK st ->
+      check_cfi n cf = OK tt ->
+      step_cf_instr ge (GibleSubPar.State s f sp pc rs pr m) cf t
+            (GibleSubPar.State s' f' sp' x rs' pr' m') ->
+      Z.pos x <= Int.max_unsigned.
+  Proof.
+    intros.
+    destruct cf; cbn in *; try discriminate; unfold check_cfi, assert_, Errors.bind in *; repeat (destruct_match; try discriminate); simplify; inv H1; try destruct_match; try lia.
+    apply list_nth_z_in in H19.
+    eapply forallb_forall in Heqb; eauto. lia.
+  Qed.
+
+  Lemma lt_check_step_cf_instr2 :
+    forall cf n,
+      check_cfi n cf = OK tt ->
+      Z.pos n <= Int.max_unsigned.
+  Proof.
+    intros.
+    destruct cf; cbn in *; try discriminate; unfold check_cfi, assert_, Errors.bind in *; repeat (destruct_match; try discriminate); simplify; try destruct_match; try lia.
+  Qed.
+
   Lemma transl_step_state_correct :
     forall s f sp pc rs rs' m m' bb pr pr' state cf t,
       (fn_code f) ! pc = Some bb ->
@@ -1766,10 +2550,10 @@ Opaque Mem.alloc.
     unfold transl_module, Errors.bind, bind, ret in HTRANSL.
     repeat (destruct_match; try discriminate; []).
     exploit transl_spec_correct; eauto.
-    intros (pred' & stmnt0 & HTRANSF & HGET).
+    intros (n & pred' & stmnt0 & HTRANSF & HGET).
     exploit step_exec_concat; eauto; intros HCONCAT.
     exploit cf_in_bb_subparbb'; eauto. intros (exit_p & HINEXIT & HTRUTHY).
-    exploit transl_step_through_cfi'; eauto. intros (curr_p & _stmnt & HCFI).
+    exploit transl_step_through_cfi'; eauto. intros (curr_p & _stmnt & HCFI & HCHECK).
     exploit match_states_cf_states_translate_cfi; eauto. intros (s0 & f1 & sp0 & pc0 & rs0 & pr0 & m2 & HPARSTATE & HEXISTS).
     exploit match_states_cf_events_translate_cfi; eauto; intros; subst.
     inv HEXISTS.
@@ -1780,6 +2564,29 @@ Opaque Mem.alloc.
       apply Smallstep.plus_one. econstructor; eauto.
       inv HTRANSL. auto. erewrite transl_module_ram_none by eauto. constructor.
       inv HMATCH'. unfold state_st_wf in WF0. auto.
+      eapply lt_check_step_cf_instr; eauto.
+    - inv HPARSTATE; simplify. exploit transl_step_state_correct_instr_return; eauto.
+      constructor. intros (asr' & asa' & retval & HSTMNT_RUN & HVAL & HASR1 & HASR2 & HASR3).
+      inv HMATCH. inv CONST.
+      econstructor. split.
+      eapply Smallstep.plus_two.
+      econstructor.
+      + eauto.
+      + eauto.
+      + eauto.
+      + inv HTRANSL. eauto.
+      + eauto.
+      + erewrite transl_module_ram_none by eauto. constructor.
+      + eauto.
+      + eauto.
+      + unfold merge_regs. rewrite AssocMapExt.merge_base_1. rewrite AssocMapExt.merge_base_1. eauto.
+      + eapply lt_check_step_cf_instr2; eauto.
+      + eapply DHTL.step_finish.
+        * now do 2 rewrite AssocMapExt.merge_base_1.
+        * do 2 rewrite AssocMapExt.merge_base_1; eauto.
+      + auto.
+      + constructor. auto. auto.
+  Qed.
 
   Theorem transl_step_correct:
     forall (S1 : GibleSubPar.state) t S2,
diff --git a/src/hls/HTLgenproof.v b/src/hls/HTLgenproof.v
index 1668580..4475342 100644
--- a/src/hls/HTLgenproof.v
+++ b/src/hls/HTLgenproof.v
@@ -1328,373 +1328,373 @@ Ltac unfold_merge :=
           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. *) admit. admit. admit. admit.
+
+      (** Equality proof *)
+      rewrite <- offset_expr_ok.
+
+      specialize (H9 (Integers.Ptrofs.unsigned
+                        (Integers.Ptrofs.divu
+                           OFFSET
+                           (Integers.Ptrofs.repr 4)))).
+      exploit H9; big_tac. admit.
+
+      (** 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.
 
@@ -1711,861 +1711,861 @@ Ltac unfold_merge :=
         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. *)
+    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.
 
-  (*     (** State Lookup *) *)
-  (*     unfold Verilog.merge_regs. *)
-  (*     crush. *)
-  (*     unfold_merge. *)
-  (*     apply AssocMap.gss. *)
+      all: try constructor; crush.
 
-  (*     (** Match states *) *)
-  (*     econstructor; eauto. *)
+      (** State Lookup *)
+      unfold Verilog.merge_regs.
+      crush.
+      unfold_merge.
+      apply AssocMap.gss.
 
-  (*     (** Match assocmaps *) *)
-  (*     unfold Verilog.merge_regs. crush. unfold_merge. *)
-  (*     apply regs_lessdef_add_greater. *)
-  (*     unfold Plt; lia. *)
-  (*     assumption. *)
+      (** Match states *)
+      econstructor; eauto.
 
-  (*     (** States well formed *) *)
-  (*     unfold state_st_wf. inversion 1. crush. *)
-  (*     unfold Verilog.merge_regs. *)
-  (*     unfold_merge. *)
-  (*     apply AssocMap.gss. *)
+      (** Match assocmaps *)
+      unfold Verilog.merge_regs. crush. unfold_merge.
+      apply regs_lessdef_add_greater.
+      unfold Plt; lia.
+      assumption.
 
-  (*     (** 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. *)
+      (** 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.
+      }
 
-  (*     (** Match states *) *)
-  (*     econstructor; eauto. *)
+      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 assocmaps *) *)
-  (*     unfold Verilog.merge_regs. crush. unfold_merge. *)
-  (*     apply regs_lessdef_add_greater. *)
-  (*     unfold Plt; lia. *)
-  (*     assumption. *)
+      (** Match states *)
+      econstructor; eauto.
 
-  (*     (** States well formed *) *)
-  (*     unfold state_st_wf. inversion 1. crush. *)
-  (*     unfold Verilog.merge_regs. *)
-  (*     unfold_merge. *)
-  (*     apply AssocMap.gss. *)
+      (** Match assocmaps *)
+      unfold Verilog.merge_regs. crush. unfold_merge.
+      apply regs_lessdef_add_greater.
+      unfold Plt; lia.
+      assumption.
 
-  (*     (** 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. *)
+      (** 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.
+      }
 
-  (*     all: try constructor; crush. *)
+      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.
 
-  (*     (** State Lookup *) *)
-  (*     unfold Verilog.merge_regs. *)
-  (*     crush. *)
-  (*     unfold_merge. *)
-  (*     apply AssocMap.gss. *)
+      all: try constructor; crush.
 
-  (*     (** Match states *) *)
-  (*     econstructor; eauto. *)
+      (** State Lookup *)
+      unfold Verilog.merge_regs.
+      crush.
+      unfold_merge.
+      apply AssocMap.gss.
 
-  (*     (** Match assocmaps *) *)
-  (*     unfold Verilog.merge_regs. crush. unfold_merge. *)
-  (*     apply regs_lessdef_add_greater. *)
-  (*     unfold Plt; lia. *)
-  (*     assumption. *)
+      (** Match states *)
+      econstructor; eauto.
 
-  (*     (** States well formed *) *)
-  (*     unfold state_st_wf. inversion 1. crush. *)
-  (*     unfold Verilog.merge_regs. *)
-  (*     unfold_merge. *)
-  (*     apply AssocMap.gss. *)
+      (** Match assocmaps *)
+      unfold Verilog.merge_regs. crush. unfold_merge.
+      apply regs_lessdef_add_greater.
+      unfold Plt; lia.
+      assumption.
 
-  (*     (** 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. *)
+      (** 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.
+      }
 
-  (*     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.
+      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:
diff --git a/src/hls/Predicate.v b/src/hls/Predicate.v
index 7786c5d..8ff61e7 100644
--- a/src/hls/Predicate.v
+++ b/src/hls/Predicate.v
@@ -672,6 +672,32 @@ Fixpoint max_predicate (p: pred_op) : positive :=
   | Por a b => Pos.max (max_predicate a) (max_predicate b)
   end.
 
+  Lemma max_predicate_deep_simplify' :
+    forall peq curr r,
+      (r <= max_predicate (deep_simplify' peq curr))%positive ->
+      (r <= max_predicate curr)%positive.
+  Proof.
+    destruct curr; cbn -[deep_simplify']; auto.
+    - intros. unfold deep_simplify' in H.
+      destruct curr1; destruct curr2; try (destruct_match; cbn in *); lia.
+    - intros. unfold deep_simplify' in H.
+      destruct curr1; destruct curr2; try (destruct_match; cbn in *); lia.
+  Qed.
+
+  Lemma max_predicate_deep_simplify :
+    forall peq curr r,
+      (r <= max_predicate (deep_simplify peq curr))%positive ->
+      (r <= max_predicate curr)%positive.
+  Proof.
+    induction curr; try solve [cbn; auto]; cbn -[deep_simplify'] in *.
+    - intros. apply max_predicate_deep_simplify' in H. cbn -[deep_simplify'] in *.
+      assert (HX: (r <= max_predicate (deep_simplify peq curr1))%positive \/ (r <= max_predicate (deep_simplify peq curr2))%positive) by lia.
+      inv HX; [eapply IHcurr1 in H0 | eapply IHcurr2 in H0]; lia.
+    - intros. apply max_predicate_deep_simplify' in H. cbn -[deep_simplify'] in *.
+      assert (HX: (r <= max_predicate (deep_simplify peq curr1))%positive \/ (r <= max_predicate (deep_simplify peq curr2))%positive) by lia.
+      inv HX; [eapply IHcurr1 in H0 | eapply IHcurr2 in H0]; lia.
+  Qed.
+
 Definition tseytin (p: pred_op) :
   {fm: formula | forall a,
       sat_predicate p a = true <-> sat_formula fm a}.