Merge branch 'develop' of github.com:ymherklotz/coqup into byte-addressing

7 files changed, 2238 insertions, 2201 deletions

diff --git a/src/Compiler.v b/src/Compiler.v
index a34b359..17d8921 100644
--- a/src/Compiler.v
+++ b/src/Compiler.v
@@ -48,7 +48,9 @@ From compcert.driver Require
 From coqup Require
      Verilog
      Veriloggen
-     HTLgen.
+     Veriloggenproof
+     HTLgen
+     HTLgenproof.
 
 Parameter print_RTL: Z -> RTL.program -> unit.
 Parameter print_HTL: HTL.program -> unit.
@@ -107,6 +109,9 @@ Definition CompCert's_passes :=
   ::: mkpass Cminorgenproof.match_prog
   ::: mkpass Selectionproof.match_prog
   ::: mkpass RTLgenproof.match_prog
+  ::: mkpass Inliningproof.match_prog
+  ::: mkpass HTLgenproof.match_prog
+  ::: mkpass Veriloggenproof.match_prog
   ::: pass_nil _.
 
 Definition match_prog: Csyntax.program -> RTL.program -> Prop :=
diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v
index 09af28a..65b6627 100644
--- a/src/translation/HTLgen.v
+++ b/src/translation/HTLgen.v
@@ -432,24 +432,35 @@ Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon uni
   match ni with
     (n, i) =>
     match i with
-    | Inop n' => add_instr n n' Vskip
+    | Inop n' =>
+      if Z.leb (Z.pos n') Integers.Int.max_unsigned then
+        add_instr n n' Vskip
+      else error (Errors.msg "State is larger than 2^32.")
     | Iop op args dst n' =>
-      do instr <- translate_instr op args;
-      do _ <- declare_reg None dst 32;
-      add_instr n n' (nonblock dst instr)
+      if Z.leb (Z.pos n') Integers.Int.max_unsigned then
+        do instr <- translate_instr op args;
+        do _ <- declare_reg None dst 32;
+        add_instr n n' (nonblock dst instr)
+      else error (Errors.msg "State is larger than 2^32.")
     | Iload mem addr args dst n' =>
-      do addr' <- translate_eff_addressing addr args;
-      do _ <- declare_reg None dst 32;
-      add_instr n n' $ create_single_cycle_load stack addr' dst
+      if Z.leb (Z.pos n') Integers.Int.max_unsigned
+      then do addr' <- translate_eff_addressing addr args;
+           do _ <- declare_reg None dst 32;
+           add_instr n n' $ create_single_cycle_load stack addr' dst
+      else error (Errors.msg "State is larger than 2^32.")
     | Istore mem addr args src n' =>
-      do addr' <- translate_eff_addressing addr args;
-      add_instr n n' $ create_single_cycle_store stack addr' src
+      if Z.leb (Z.pos n') Integers.Int.max_unsigned
+      then do addr' <- translate_eff_addressing addr args;
+           add_instr n n' $ create_single_cycle_store stack addr' src
+      else error (Errors.msg "State is larger than 2^32.")
     | Icall _ _ _ _ _ => error (Errors.msg "Calls are not implemented.")
     | Itailcall _ _ _ => error (Errors.msg "Tailcalls are not implemented.")
     | Ibuiltin _ _ _ _ => error (Errors.msg "Builtin functions not implemented.")
     | Icond cond args n1 n2 =>
-      do e <- translate_condition cond args;
-      add_branch_instr e n n1 n2
+      if Z.leb (Z.pos n1) Integers.Int.max_unsigned && Z.leb (Z.pos n2) Integers.Int.max_unsigned then
+        do e <- translate_condition cond args;
+        add_branch_instr e n n1 n2
+      else error (Errors.msg "State is larger than 2^32.")
     | Ijumptable r tbl =>
       do s <- get;
       add_node_skip n (Vcase (Vvar r) (tbl_to_case_expr s.(st_st) tbl) (Some Vskip))
diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v
index e404c82..338e77d 100644
--- a/src/translation/HTLgenproof.v
+++ b/src/translation/HTLgenproof.v
@@ -31,2159 +31,2177 @@ Hint Resolve AssocMap.gso : htlproof.
 
 Hint Unfold find_assocmap AssocMapExt.get_default : htlproof.
 
-(* Inductive match_assocmaps : RTL.function -> RTL.regset -> assocmap -> Prop := *)
-(*   match_assocmap : forall f rs am, *)
-(*     (forall r, Ple r (RTL.max_reg_function f) -> *)
-(*                val_value_lessdef (Registers.Regmap.get r rs) am#r) -> *)
-(*     match_assocmaps f rs am. *)
-(* Hint Constructors match_assocmaps : htlproof. *)
-
-(* Definition state_st_wf (m : HTL.module) (s : HTL.state) := *)
-(*   forall st asa asr res, *)
-(*   s = HTL.State res m st asa asr -> *)
-(*   asa!(m.(HTL.mod_st)) = Some (posToValue st). *)
-(* Hint Unfold state_st_wf : htlproof. *)
-
-(* Inductive match_arrs (m : HTL.module) (f : RTL.function) (sp : Values.val) (mem : mem) : *)
-(*   Verilog.assocmap_arr -> Prop := *)
-(* | match_arr : forall asa stack, *)
-(*     asa ! (m.(HTL.mod_stk)) = Some stack /\ *)
-(*     stack.(arr_length) = Z.to_nat (f.(RTL.fn_stacksize) / 4) /\ *)
-(*     (forall ptr, *)
-(*         0 <= ptr < Z.of_nat m.(HTL.mod_stk_len) -> *)
-(*         opt_val_value_lessdef (Mem.loadv AST.Mint32 mem *)
-(*                                          (Values.Val.offset_ptr sp (Integers.Ptrofs.repr (4 * ptr)))) *)
-(*                               (Option.default (NToValue 0) *)
-(*                                  (Option.join (array_get_error (Z.to_nat ptr) stack)))) -> *)
-(*     match_arrs m f sp mem asa. *)
-
-(* Definition stack_based (v : Values.val) (sp : Values.block) : Prop := *)
-(*    match v with *)
-(*    | Values.Vptr sp' off => sp' = sp *)
-(*    | _ => True *)
-(*    end. *)
-
-(* Definition reg_stack_based_pointers (sp : Values.block) (rs : Registers.Regmap.t Values.val) : Prop := *)
-(*   forall r, stack_based (Registers.Regmap.get r rs) sp. *)
-
-(* Definition arr_stack_based_pointers (spb : Values.block) (m : mem) (stack_length : Z) *)
-(*   (sp : Values.val) : Prop := *)
-(*   forall ptr, *)
-(*     0 <= ptr < (stack_length / 4) -> *)
-(*     stack_based (Option.default *)
-(*                    Values.Vundef *)
-(*                    (Mem.loadv AST.Mint32 m *)
-(*                               (Values.Val.offset_ptr sp (Integers.Ptrofs.repr (4 * ptr))))) *)
-(*                 spb. *)
-
-(* Definition stack_bounds (sp : Values.val) (hi : Z) (m : mem) : Prop := *)
-(*   forall ptr v, *)
-(*     hi <= ptr <= Integers.Ptrofs.max_unsigned -> *)
-(*     Z.modulo ptr 4 = 0 -> *)
-(*     Mem.loadv AST.Mint32 m (Values.Val.offset_ptr sp (Integers.Ptrofs.repr ptr )) = None /\ *)
-(*     Mem.storev AST.Mint32 m (Values.Val.offset_ptr sp (Integers.Ptrofs.repr ptr )) v = None. *)
-
-(* Inductive match_frames : list RTL.stackframe -> list HTL.stackframe -> Prop := *)
-(* | match_frames_nil : *)
-(*     match_frames nil nil. *)
-
-(*   Lemma assumption_32bit : *)
-(*     forall v, *)
-(*       valueToPos (posToValue v) = v. *)
-(*   Proof. *)
-(*   Admitted. *)
-
-(* Inductive match_states : RTL.state -> HTL.state -> Prop := *)
-(* | match_state : forall asa asr sf f sp sp' rs mem m st res *)
-(*     (MASSOC : match_assocmaps f rs asr) *)
-(*     (TF : tr_module f m) *)
-(*     (WF : state_st_wf m (HTL.State res m st asr asa)) *)
-(*     (MF : match_frames sf res) *)
-(*     (MARR : match_arrs m f sp mem asa) *)
-(*     (SP : sp = Values.Vptr sp' (Integers.Ptrofs.repr 0)) *)
-(*     (RSBP : reg_stack_based_pointers sp' rs) *)
-(*     (ASBP : arr_stack_based_pointers sp' mem (f.(RTL.fn_stacksize)) sp) *)
-(*     (BOUNDS : stack_bounds sp (f.(RTL.fn_stacksize)) mem), *)
-(*     match_states (RTL.State sf f sp st rs mem) *)
-(*                  (HTL.State res m st asr asa) *)
-(* | match_returnstate : *)
-(*     forall *)
-(*       v v' stack mem res *)
-(*       (MF : match_frames stack res), *)
-(*       val_value_lessdef v v' -> *)
-(*       match_states (RTL.Returnstate stack v mem) (HTL.Returnstate res v') *)
-(* | match_initial_call : *)
-(*     forall f m m0 *)
-(*     (TF : tr_module f m), *)
-(*       match_states (RTL.Callstate nil (AST.Internal f) nil m0) (HTL.Callstate nil m nil). *)
-(* Hint Constructors match_states : htlproof. *)
-
-(* Definition match_prog (p: RTL.program) (tp: HTL.program) := *)
-(*   Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq p tp /\ *)
-(*   main_is_internal p = true. *)
-
-(* Definition match_prog_matches : *)
-(*   forall p tp, *)
-(*     match_prog p tp -> *)
-(*     Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq p tp. *)
-(*   Proof. intros. unfold match_prog in H. tauto. Qed. *)
-
-(* Lemma transf_program_match: *)
-(*   forall p tp, HTLgen.transl_program p = Errors.OK tp -> match_prog p tp. *)
-(* Proof. *)
-(*   intros. unfold transl_program in H. *)
-(*   destruct (main_is_internal p) eqn:?; try discriminate. *)
-(*   unfold match_prog. split. *)
-(*   apply Linking.match_transform_partial_program; auto. *)
-(*   assumption. *)
-(* Qed. *)
-
-(* Lemma regs_lessdef_add_greater : *)
-(*   forall f rs1 rs2 n v, *)
-(*     Plt (RTL.max_reg_function f) n -> *)
-(*     match_assocmaps f rs1 rs2 -> *)
-(*     match_assocmaps f rs1 (AssocMap.set n v rs2). *)
-(* Proof. *)
-(*   inversion 2; subst. *)
-(*   intros. constructor. *)
-(*   intros. unfold find_assocmap. unfold AssocMapExt.get_default. *)
-(*   rewrite AssocMap.gso. eauto. *)
-(*   apply Pos.le_lt_trans with _ _ n in H2. *)
-(*   unfold not. intros. subst. eapply Pos.lt_irrefl. eassumption. assumption. *)
-(* Qed. *)
-(* Hint Resolve regs_lessdef_add_greater : htlproof. *)
-
-(* Lemma regs_lessdef_add_match : *)
-(*   forall f rs am r v v', *)
-(*     val_value_lessdef v v' -> *)
-(*     match_assocmaps f rs am -> *)
-(*     match_assocmaps f (Registers.Regmap.set r v rs) (AssocMap.set r v' am). *)
-(* Proof. *)
-(*   inversion 2; subst. *)
-(*   constructor. intros. *)
-(*   destruct (peq r0 r); subst. *)
-(*   rewrite Registers.Regmap.gss. *)
-(*   unfold find_assocmap. unfold AssocMapExt.get_default. *)
-(*   rewrite AssocMap.gss. assumption. *)
-
-(*   rewrite Registers.Regmap.gso; try assumption. *)
-(*   unfold find_assocmap. unfold AssocMapExt.get_default. *)
-(*   rewrite AssocMap.gso; eauto. *)
-(* Qed. *)
-(* Hint Resolve regs_lessdef_add_match : htlproof. *)
-
-(* Lemma list_combine_none : *)
-(*   forall n l, *)
-(*     length l = n -> *)
-(*     list_combine Verilog.merge_cell (list_repeat None n) l = l. *)
-(* Proof. *)
-(*   induction n; intros; crush. *)
-(*   - symmetry. apply length_zero_iff_nil. auto. *)
-(*   - destruct l; crush. *)
-(*     rewrite list_repeat_cons. *)
-(*     crush. f_equal. *)
-(*     eauto. *)
-(* Qed. *)
-
-(* Lemma combine_none : *)
-(*   forall n a, *)
-(*     a.(arr_length) = n -> *)
-(*     arr_contents (combine Verilog.merge_cell (arr_repeat None n) a) = arr_contents a. *)
-(* Proof. *)
-(*   intros. *)
-(*   unfold combine. *)
-(*   crush. *)
-
-(*   rewrite <- (arr_wf a) in H. *)
-(*   apply list_combine_none. *)
-(*   assumption. *)
-(* Qed. *)
-
-(* Lemma list_combine_lookup_first : *)
-(*   forall l1 l2 n, *)
-(*     length l1 = length l2 -> *)
-(*     nth_error l1 n = Some None -> *)
-(*     nth_error (list_combine Verilog.merge_cell l1 l2) n = nth_error l2 n. *)
-(* Proof. *)
-(*   induction l1; intros; crush. *)
-
-(*   rewrite nth_error_nil in H0. *)
-(*   discriminate. *)
-
-(*   destruct l2 eqn:EQl2. crush. *)
-(*   simpl in H. invert H. *)
-(*   destruct n; simpl in *. *)
-(*   invert H0. simpl. reflexivity. *)
-(*   eauto. *)
-(* Qed. *)
-
-(* Lemma combine_lookup_first : *)
-(*   forall a1 a2 n, *)
-(*     a1.(arr_length) = a2.(arr_length) -> *)
-(*     array_get_error n a1 = Some None -> *)
-(*     array_get_error n (combine Verilog.merge_cell a1 a2) = array_get_error n a2. *)
-(* Proof. *)
-(*   intros. *)
-
-(*   unfold array_get_error in *. *)
-(*   apply list_combine_lookup_first; eauto. *)
-(*   rewrite a1.(arr_wf). rewrite a2.(arr_wf). *)
-(*   assumption. *)
-(* Qed. *)
-
-(* Lemma list_combine_lookup_second : *)
-(*   forall l1 l2 n x, *)
-(*     length l1 = length l2 -> *)
-(*     nth_error l1 n = Some (Some x) -> *)
-(*     nth_error (list_combine Verilog.merge_cell l1 l2) n = Some (Some x). *)
-(* Proof. *)
-(*   induction l1; intros; crush; auto. *)
-
-(*   destruct l2 eqn:EQl2. crush. *)
-(*   simpl in H. invert H. *)
-(*   destruct n; simpl in *. *)
-(*   invert H0. simpl. reflexivity. *)
-(*   eauto. *)
-(* Qed. *)
-
-(* Lemma combine_lookup_second : *)
-(*   forall a1 a2 n x, *)
-(*     a1.(arr_length) = a2.(arr_length) -> *)
-(*     array_get_error n a1 = Some (Some x) -> *)
-(*     array_get_error n (combine Verilog.merge_cell a1 a2) = Some (Some x). *)
-(* Proof. *)
-(*   intros. *)
-
-(*   unfold array_get_error in *. *)
-(*   apply list_combine_lookup_second; eauto. *)
-(*   rewrite a1.(arr_wf). rewrite a2.(arr_wf). *)
-(*   assumption. *)
-(* Qed. *)
-
-(* Ltac inv_state := *)
-(*   match goal with *)
-(*     MSTATE : match_states _ _ |- _ => *)
-(*     inversion MSTATE; *)
-(*     match goal with *)
-(*       TF : tr_module _ _ |- _ => *)
-(*       inversion TF; *)
-(*       match goal with *)
-(*         TC : forall _ _, *)
-(*           Maps.PTree.get _ _ = Some _ -> tr_code _ _ _ _ _ _ _ _ _, *)
-(*         H : Maps.PTree.get _ _ = Some _ |- _ => *)
-(*         apply TC in H; inversion H; *)
-(*         match goal with *)
-(*           TI : context[tr_instr] |- _ => *)
-(*           inversion TI *)
-(*         end *)
-(*       end *)
-(*     end *)
-(* end; subst. *)
-
-(* Ltac unfold_func H := *)
-(*   match type of H with *)
-(*   | ?f = _ => unfold f in H; repeat (unfold_match H) *)
-(*   | ?f _ = _ => unfold f in H; repeat (unfold_match H) *)
-(*   | ?f _ _ = _ => unfold f in H; repeat (unfold_match H) *)
-(*   | ?f _ _ _ = _ => unfold f in H; repeat (unfold_match H) *)
-(*   | ?f _ _ _ _ = _ => unfold f in H; repeat (unfold_match H) *)
-(*   end. *)
-
-(* Lemma init_reg_assoc_empty : *)
-(*   forall f l, *)
-(*     match_assocmaps f (RTL.init_regs nil l) (HTL.init_regs nil l). *)
-(* Proof. *)
-(*   induction l; simpl; constructor; intros. *)
-(*   - rewrite Registers.Regmap.gi. unfold find_assocmap. *)
-(*     unfold AssocMapExt.get_default. rewrite AssocMap.gempty. *)
-(*     constructor. *)
-
-(*   - rewrite Registers.Regmap.gi. unfold find_assocmap. *)
-(*     unfold AssocMapExt.get_default. rewrite AssocMap.gempty. *)
-(*     constructor. *)
-(* Qed. *)
-
-(* Lemma arr_lookup_some: *)
-(*   forall (z : Z) (r0 : Registers.reg) (r : Verilog.reg) (asr : assocmap) (asa : Verilog.assocmap_arr) *)
-(*     (stack : Array (option value)) (H5 : asa ! r = Some stack) n, *)
-(*     exists x, Verilog.arr_assocmap_lookup asa r n = Some x. *)
-(* Proof. *)
-(*   intros z r0 r asr asa stack H5 n. *)
-(*   eexists. *)
-(*   unfold Verilog.arr_assocmap_lookup. rewrite H5. reflexivity. *)
-(* Qed. *)
-(* Hint Resolve arr_lookup_some : htlproof. *)
-
-(* Section CORRECTNESS. *)
-
-(*   Variable prog : RTL.program. *)
-(*   Variable tprog : HTL.program. *)
-
-(*   Hypothesis TRANSL : match_prog prog tprog. *)
-
-(*   Lemma TRANSL' : *)
-(*     Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq prog tprog. *)
-(*   Proof. intros; apply match_prog_matches; assumption. Qed. *)
-
-(*   Let ge : RTL.genv := Globalenvs.Genv.globalenv prog. *)
-(*   Let tge : HTL.genv := Globalenvs.Genv.globalenv tprog. *)
-
-(*   Lemma symbols_preserved: *)
-(*     forall (s: AST.ident), Genv.find_symbol tge s = Genv.find_symbol ge s. *)
-(*   Proof. intros. eapply (Genv.find_symbol_match TRANSL'). Qed. *)
-
-(*   Lemma function_ptr_translated: *)
-(*     forall (b: Values.block) (f: RTL.fundef), *)
-(*       Genv.find_funct_ptr ge b = Some f -> *)
-(*       exists tf, *)
-(*         Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = Errors.OK tf. *)
-(*   Proof. *)
-(*     intros. exploit (Genv.find_funct_ptr_match TRANSL'); eauto. *)
-(*     intros (cu & tf & P & Q & R); exists tf; auto. *)
-(*   Qed. *)
-
-(*   Lemma functions_translated: *)
-(*     forall (v: Values.val) (f: RTL.fundef), *)
-(*       Genv.find_funct ge v = Some f -> *)
-(*       exists tf, *)
-(*         Genv.find_funct tge v = Some tf /\ transl_fundef f = Errors.OK tf. *)
-(*   Proof. *)
-(*     intros. exploit (Genv.find_funct_match TRANSL'); eauto. *)
-(*     intros (cu & tf & P & Q & R); exists tf; auto. *)
-(*   Qed. *)
-
-(*   Lemma senv_preserved: *)
-(*     Senv.equiv (Genv.to_senv ge) (Genv.to_senv tge). *)
-(*   Proof *)
-(*     (Genv.senv_transf_partial TRANSL'). *)
-(*   Hint Resolve senv_preserved : htlproof. *)
-
-(*   Lemma ptrofs_inj : *)
-(*     forall a b, *)
-(*       Ptrofs.unsigned a = Ptrofs.unsigned b -> a = b. *)
-(*   Proof. *)
-(*     intros. rewrite <- Ptrofs.repr_unsigned. symmetry. rewrite <- Ptrofs.repr_unsigned. *)
-(*     rewrite H. auto. *)
-(*   Qed. *)
-
-(*   Lemma eval_correct : *)
-(*     forall s sp op rs m v e asr asa f f' stk s' i pc res0 pc' args res ml st, *)
-(*       match_states (RTL.State stk f sp pc rs m) (HTL.State res ml st asr asa) -> *)
-(*       (RTL.fn_code f) ! pc = Some (RTL.Iop op args res0 pc') -> *)
-(*       Op.eval_operation ge sp op *)
-(*                         (List.map (fun r : BinNums.positive => Registers.Regmap.get r rs) args) m = Some v -> *)
-(*       translate_instr op args s = OK e s' i -> *)
-(*       exists v', Verilog.expr_runp f' asr asa e v' /\ val_value_lessdef v v'. *)
-(*   Proof. *)
-(*     intros s sp op rs m v e asr asa f f' stk s' i pc pc' res0 args res ml st MSTATE INSTR EVAL TR_INSTR. *)
-(*     inv MSTATE. inv MASSOC. unfold translate_instr in TR_INSTR; repeat (unfold_match TR_INSTR); inv TR_INSTR; *)
-(*     unfold Op.eval_operation in EVAL; repeat (unfold_match EVAL); simplify. *)
-(*     - inv Heql. *)
-(*       assert (HPle : Ple r (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto). *)
-(*       apply H in HPle. eexists. split; try constructor; eauto. *)
-(*     - eexists. split. constructor. constructor. auto. *)
-(*     - inv Heql. *)
-(*       assert (HPle : Ple r (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto). *)
-(*       apply H in HPle. *)
-(*       eexists. split. econstructor; eauto. constructor. trivial. *)
-(*       unfold Verilog.unop_run. unfold Values.Val.neg. destruct (Registers.Regmap.get r rs) eqn:?; constructor. *)
-(*       inv HPle. auto. *)
-(*     - inv Heql. *)
-(*       assert (HPle : Ple r (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto). *)
-(*       assert (HPle0 : Ple r0 (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto). *)
-(*       apply H in HPle. apply H in HPle0. *)
-(*       eexists. split. econstructor; eauto. constructor. trivial. *)
-(*       constructor. trivial. simplify. inv HPle. inv HPle0; constructor; auto. *)
-(*       + inv HPle0. constructor. unfold valueToPtr. Search Integers.Ptrofs.sub Integers.int. *)
-(*         pose proof Integers.Ptrofs.agree32_sub. unfold Integers.Ptrofs.agree32 in H3. *)
-(*         Print Integers.Ptrofs.agree32. unfold Ptrofs.of_int. simpl. *)
-(*         apply ptrofs_inj. assert (Archi.ptr64 = false) by auto. eapply H3 in H4. *)
-(*         rewrite Ptrofs.unsigned_repr. apply H4. replace Ptrofs.max_unsigned with Int.max_unsigned; auto. *)
-(*         apply Int.unsigned_range_2. *)
-(*         auto. rewrite Ptrofs.unsigned_repr. replace Ptrofs.max_unsigned with Int.max_unsigned; auto. *)
-(*         apply Int.unsigned_range_2. rewrite Ptrofs.unsigned_repr. auto. *)
-(*         replace Ptrofs.max_unsigned with Int.max_unsigned; auto. *)
-(*         apply Int.unsigned_range_2. *)
-(*         Admitted. *)
-
-(*   Lemma eval_cond_correct : *)
-(*     forall cond (args : list Registers.reg) s1 c s' i rs args m b f asr asa, *)
-(*       translate_condition cond args s1 = OK c s' i -> *)
-(*       Op.eval_condition *)
-(*         cond *)
-(*         (List.map (fun r : BinNums.positive => Registers.Regmap.get r rs) args) *)
-(*         m = Some b -> *)
-(*       Verilog.expr_runp f asr asa c (boolToValue b). *)
-(*   Admitted. *)
-
-(*   (** The proof of semantic preservation for the translation of instructions *)
-(*       is a simulation argument based on diagrams of the following form: *)
-(* << *)
-(*                       match_states *)
-(*     code st rs ---------------- State m st assoc *)
-(*          ||                             | *)
-(*          ||                             | *)
-(*          ||                             | *)
-(*          \/                             v *)
-(*     code st rs' --------------- State m st assoc' *)
-(*                       match_states *)
-(* >> *)
-(*       where [tr_code c data control fin rtrn st] is assumed to hold. *)
-
-(*       The precondition and postcondition is that that should hold is [match_assocmaps rs assoc]. *)
-(*    *) *)
-
-(*   Definition transl_instr_prop (instr : RTL.instruction) : Prop := *)
-(*     forall m asr asa fin rtrn st stmt trans res, *)
-(*       tr_instr fin rtrn st (m.(HTL.mod_stk)) instr stmt trans -> *)
-(*       exists asr' asa', *)
-(*         HTL.step tge (HTL.State res m st asr asa) Events.E0 (HTL.State res m st asr' asa'). *)
-
-(*   Opaque combine. *)
-
-(*   Ltac tac0 := *)
-(*     match goal with *)
-(*     | [ |- context[valueToPos (posToValue _)] ] => rewrite assumption_32bit *)
-
-(*     | [ |- context[Verilog.merge_arrs _ _] ] => unfold Verilog.merge_arrs *)
-(*     | [ |- context[Verilog.merge_arr] ] => unfold Verilog.merge_arr *)
-(*     | [ |- context[Verilog.merge_regs _ _] ] => unfold Verilog.merge_regs; crush; unfold_merge *)
-(*     | [ |- context[reg_stack_based_pointers] ] => unfold reg_stack_based_pointers; intros *)
-(*     | [ |- context[Verilog.arr_assocmap_set _ _ _ _] ] => unfold Verilog.arr_assocmap_set *)
-
-(*     | [ |- context[HTL.empty_stack] ] => unfold HTL.empty_stack *)
-
-(*     | [ |- context[_ # ?d <- _ ! ?d] ] => rewrite AssocMap.gss *)
-(*     | [ |- context[_ # ?d <- _ ! ?s] ] => rewrite AssocMap.gso *)
-(*     | [ |- context[(AssocMap.empty _) ! _] ] => rewrite AssocMap.gempty *)
-
-(*     | [ |- context[array_get_error _ (combine Verilog.merge_cell (arr_repeat None _) _)] ] => *)
-(*       rewrite combine_lookup_first *)
-
-(*     | [ |- state_st_wf _ _ ] => unfold state_st_wf; inversion 1 *)
-(*     | [ |- context[match_states _ _] ] => econstructor; auto *)
-(*     | [ |- match_arrs _ _ _ _ _ ] => econstructor; auto *)
-(*     | [ |- match_assocmaps _ _ _ # _ <- (posToValue _) ] => *)
-(*       apply regs_lessdef_add_greater; [> unfold Plt; lia | assumption] *)
-
-(*     | [ H : ?asa ! ?r = Some _ |- Verilog.arr_assocmap_lookup ?asa ?r _ = Some _ ] => *)
-(*       unfold Verilog.arr_assocmap_lookup; setoid_rewrite H; f_equal *)
-(*     | [ |- context[(AssocMap.combine _ _ _) ! _] ] => *)
-(*       try (rewrite AssocMap.gcombine; [> | reflexivity]) *)
-
-(*     | [ |- context[Registers.Regmap.get ?d (Registers.Regmap.set ?d _ _)] ] => *)
-(*       rewrite Registers.Regmap.gss *)
-(*     | [ |- context[Registers.Regmap.get ?s (Registers.Regmap.set ?d _ _)] ] => *)
-(*       destruct (Pos.eq_dec s d) as [EQ|EQ]; *)
-(*       [> rewrite EQ | rewrite Registers.Regmap.gso; auto] *)
-
-(*     | [ H : opt_val_value_lessdef _ _ |- _ ] => invert H *)
-(*     | [ H : context[Z.of_nat (Z.to_nat _)] |- _ ] => rewrite Z2Nat.id in H; [> solve crush |] *)
-(*     | [ H : _ ! _ = Some _ |- _] => setoid_rewrite H *)
-(*     end. *)
-
-(*   Ltac small_tac := repeat (crush; try array; try ptrofs); crush; auto. *)
-(*   Ltac big_tac := repeat (crush; try array; try ptrofs; try tac0); crush; auto. *)
-
-  (* Lemma transl_inop_correct: *)
-  (*   forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive) *)
-  (*     (rs : RTL.regset) (m : mem) (pc' : RTL.node), *)
-  (*     (RTL.fn_code f) ! pc = Some (RTL.Inop pc') -> *)
-  (*     forall R1 : HTL.state, *)
-  (*       match_states (RTL.State s f sp pc rs m) R1 -> *)
-  (*       exists R2 : HTL.state, *)
-  (*         Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ match_states (RTL.State s f sp pc' rs m) R2. *)
-  (* Proof. *)
-  (*   intros s f sp pc rs m pc' H R1 MSTATE. *)
-  (*   inv_state. *)
-
-  (*   unfold match_prog in TRANSL. *)
-  (*   econstructor. *)
-  (*   split. *)
-  (*   apply Smallstep.plus_one. *)
-  (*   eapply HTL.step_module; eauto. *)
-  (*   apply assumption_32bit. *)
-  (*   (* processing of state *) *)
-  (*   econstructor. *)
-  (*   crush. *)
-  (*   econstructor. *)
-  (*   econstructor. *)
-  (*   econstructor. *)
-
-  (*   all: invert MARR; big_tac. *)
-  (*   Unshelve. *)
-  (*   constructor. *)
-  (* Qed. *)
-  (* Hint Resolve transl_inop_correct : htlproof. *)
-
-  (* Lemma transl_iop_correct: *)
-  (*   forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive) *)
-  (*     (rs : Registers.Regmap.t Values.val) (m : mem) (op : Op.operation) (args : list Registers.reg) *)
-  (*     (res0 : Registers.reg) (pc' : RTL.node) (v : Values.val), *)
-  (*     (RTL.fn_code f) ! pc = Some (RTL.Iop op args res0 pc') -> *)
-  (*     Op.eval_operation ge sp op (map (fun r : positive => Registers.Regmap.get r rs) args) m = Some v -> *)
-  (*     forall R1 : HTL.state, *)
-  (*       match_states (RTL.State s f sp pc rs m) R1 -> *)
-  (*       exists R2 : HTL.state, *)
-  (*         Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ *)
-  (*         match_states (RTL.State s f sp pc' (Registers.Regmap.set res0 v rs) m) R2. *)
-  (* Proof. *)
-  (*   intros s f sp pc rs m op args res0 pc' v H H0 R1 MSTATE. *)
-  (*   inv_state. *)
-  (*   exploit eval_correct; eauto. intros. inversion H1. inversion H2. *)
-  (*   econstructor. split. *)
-  (*   apply Smallstep.plus_one. *)
-  (*   eapply HTL.step_module; eauto. *)
-  (*   apply assumption_32bit. *)
-  (*   econstructor; simpl; trivial. *)
-  (*   constructor; trivial. *)
-  (*   econstructor; simpl; eauto. *)
-  (*   simpl. econstructor. econstructor. *)
-  (*   apply H3. simplify. *)
-
-  (*   all: big_tac. *)
-
-  (*   assert (Ple res0 (RTL.max_reg_function f)) *)
-  (*       by (eapply RTL.max_reg_function_def; eauto; simpl; auto). *)
-
-  (*   unfold Ple in H10. lia. *)
-  (*   apply regs_lessdef_add_match. assumption. *)
-  (*   apply regs_lessdef_add_greater. unfold Plt; lia. assumption. *)
-  (*   assert (Ple res0 (RTL.max_reg_function f)) *)
-  (*       by (eapply RTL.max_reg_function_def; eauto; simpl; auto). *)
-  (*   unfold Ple in H12; lia. *)
-  (*   unfold_merge. simpl. *)
-  (*   rewrite AssocMap.gso. *)
-  (*   apply AssocMap.gss. *)
-  (*   apply st_greater_than_res. *)
-
-  (*   (*match_states*) *)
-  (*     assert (pc' = valueToPos (posToValue 32 pc')). auto using assumption_32bit. *)
-  (*   rewrite <- H1. *)
-  (*   constructor; auto. *)
-  (*   unfold_merge. *)
-  (*   apply regs_lessdef_add_match. *)
-  (*   constructor. *)
-  (*   apply regs_lessdef_add_greater. *)
-  (*   apply greater_than_max_func. *)
-  (*   assumption. *)
-
-  (*   unfold state_st_wf. intros. inversion H2. subst. *)
-  (*   unfold_merge. *)
-  (*   rewrite AssocMap.gso. *)
-  (*   apply AssocMap.gss. *)
-  (*   apply st_greater_than_res. *)
-
-  (*    + econstructor. split. *)
-  (*    apply Smallstep.plus_one. *)
-  (*    eapply HTL.step_module; eauto. *)
-  (*    econstructor; simpl; trivial. *)
-  (*    constructor; trivial. *)
-  (*    econstructor; simpl; eauto. *)
-  (*    eapply eval_correct; eauto. *)
-  (*    constructor. rewrite valueToInt_intToValue. trivial. *)
-  (*    unfold_merge. simpl. *)
-  (*    rewrite AssocMap.gso. *)
-  (*    apply AssocMap.gss. *)
-  (*    apply st_greater_than_res. *)
-
-  (*     match_states *)
-  (*    assert (pc' = valueToPos (posToValue 32 pc')). auto using assumption_32bit. *)
-  (*    rewrite <- H1. *)
-  (*    constructor. *)
-  (*    unfold_merge. *)
-  (*    apply regs_lessdef_add_match. *)
-  (*    constructor. *)
-  (*    symmetry. apply valueToInt_intToValue. *)
-  (*    apply regs_lessdef_add_greater. *)
-  (*    apply greater_than_max_func. *)
-  (*    assumption. assumption. *)
-
-  (*    unfold state_st_wf. intros. inversion H2. subst. *)
-  (*    unfold_merge. *)
-  (*    rewrite AssocMap.gso. *)
-  (*    apply AssocMap.gss. *)
-  (*    apply st_greater_than_res. *)
-  (*    assumption. *)
-  (* Admitted. *)
-  (* Hint Resolve transl_iop_correct : htlproof. *)
-
-  (* Ltac tac := *)
-  (*   repeat match goal with *)
-  (*          | [ _ : error _ _ = OK _ _ _ |- _ ] => discriminate *)
-  (*          | [ _ : context[if (?x && ?y) then _ else _] |- _ ] => *)
-  (*            let EQ1 := fresh "EQ" in *)
-  (*            let EQ2 := fresh "EQ" in *)
-  (*            destruct x eqn:EQ1; destruct y eqn:EQ2; simpl in * *)
-  (*          | [ _ : context[if ?x then _ else _] |- _ ] => *)
-  (*            let EQ := fresh "EQ" in *)
-  (*            destruct x eqn:EQ; simpl in * *)
-  (*          | [ H : ret _ _ = _  |- _ ] => invert H *)
-  (*          | [ _ : context[match ?x with | _ => _ end] |- _ ] => destruct x *)
-  (*          end. *)
-
-  (* Ltac inv_arr_access := *)
-  (*   match goal with *)
-  (*   | [ _ : translate_arr_access ?chunk ?addr ?args _ _ = OK ?c _ _ |- _] => *)
-  (*     destruct c, chunk, addr, args; crush; tac; crush *)
-  (*   end. *)
-
-  (* Lemma transl_iload_correct: *)
-  (*   forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive) *)
-  (*     (rs : Registers.Regmap.t Values.val) (m : mem) (chunk : AST.memory_chunk) *)
-  (*     (addr : Op.addressing) (args : list Registers.reg) (dst : Registers.reg) *)
-  (*     (pc' : RTL.node) (a v : Values.val), *)
-  (*     (RTL.fn_code f) ! pc = Some (RTL.Iload chunk addr args dst pc') -> *)
-  (*     Op.eval_addressing ge sp addr (map (fun r : positive => Registers.Regmap.get r rs) args) = Some a -> *)
-  (*     Mem.loadv chunk m a = Some v -> *)
-  (*     forall R1 : HTL.state, *)
-  (*       match_states (RTL.State s f sp pc rs m) R1 -> *)
-  (*       exists R2 : HTL.state, *)
-  (*         Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ *)
-  (*         match_states (RTL.State s f sp pc' (Registers.Regmap.set dst v rs) m) R2. *)
-  (* Proof. *)
-  (*   intros s f sp pc rs m chunk addr args dst pc' a v H H0 H1 R1 MSTATE. *)
-  (*   inv_state. inv_arr_access. *)
-
-  (*   + (** Preamble *) *)
-  (*     invert MARR. crush. *)
-
-  (*     unfold Op.eval_addressing in H0. *)
-  (*     destruct (Archi.ptr64) eqn:ARCHI; crush. *)
-
-  (*     unfold reg_stack_based_pointers in RSBP. *)
-  (*     pose proof (RSBP r0) as RSBPr0. *)
-
-  (*     destruct (Registers.Regmap.get r0 rs) eqn:EQr0; crush. *)
-
-  (*     rewrite ARCHI in H1. crush. *)
-  (*     subst. *)
-
-  (*     pose proof MASSOC as MASSOC'. *)
-  (*     invert MASSOC'. *)
-  (*     pose proof (H0 r0). *)
-  (*     assert (HPler0 : Ple r0 (RTL.max_reg_function f)) *)
-  (*       by (eapply RTL.max_reg_function_use; eauto; crush; eauto). *)
-  (*     apply H6 in HPler0. *)
-  (*     invert HPler0; try congruence. *)
-  (*     rewrite EQr0 in H8. *)
-  (*     invert H8. *)
-  (*     clear H0. clear H6. *)
-
-  (*     unfold check_address_parameter_signed in *; *)
-  (*     unfold check_address_parameter_unsigned in *; crush. *)
-
-  (*     remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ asr # r0)) *)
-  (*                                   (Integers.Ptrofs.of_int (Integers.Int.repr z))) as OFFSET. *)
-
-  (*     (** Modular preservation proof *) *)
-  (*     assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE. *)
-  (*     { rewrite HeqOFFSET. *)
-  (*       apply PtrofsExtra.add_mod; crush. *)
-  (*       rewrite Integers.Ptrofs.unsigned_repr_eq. *)
-  (*       rewrite <- Zmod_div_mod; crush. *)
-  (*       apply PtrofsExtra.of_int_mod. *)
-  (*       rewrite Integers.Int.unsigned_repr_eq. *)
-  (*       rewrite <- Zmod_div_mod; crush. } *)
-
-  (*     (** Read bounds proof *) *)
-  (*     assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH. *)
-  (*     { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; crush; auto. *)
-  (*       unfold stack_bounds in BOUNDS. *)
-  (*       exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET)); auto. *)
-  (*       split; try lia; apply Integers.Ptrofs.unsigned_range_2. *)
-  (*       small_tac. } *)
-
-  (*     (** Normalisation proof *) *)
-  (*     assert (Integers.Ptrofs.repr *)
-  (*               (4 * Integers.Ptrofs.unsigned *)
-  (*                      (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4))) = OFFSET) *)
-  (*       as NORMALISE. *)
-  (*     { replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) at 1 by reflexivity. *)
-  (*       rewrite <- PtrofsExtra.mul_unsigned. *)
-  (*       apply PtrofsExtra.mul_divu; crush; auto. } *)
-
-  (*     (** Normalised bounds proof *) *)
-  (*     assert (0 <= *)
-  (*             Integers.Ptrofs.unsigned (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)) *)
-  (*             < (RTL.fn_stacksize f / 4)) *)
-  (*       as NORMALISE_BOUND. *)
-  (*     { split. *)
-  (*       apply Integers.Ptrofs.unsigned_range_2. *)
-  (*       assert (forall x y, Integers.Ptrofs.divu x y = Integers.Ptrofs.divu x y ) by reflexivity. *)
-  (*       unfold Integers.Ptrofs.divu at 2 in H0. *)
-  (*       rewrite H0. clear H0. *)
-  (*       rewrite Integers.Ptrofs.unsigned_repr; crush. *)
-  (*       apply Zmult_lt_reg_r with (p := 4); try lia. *)
-  (*       repeat rewrite ZLib.div_mul_undo; try lia. *)
-  (*       apply Z.div_pos; small_tac. *)
-  (*       apply Z.div_le_upper_bound; small_tac. } *)
-
-  (*     inversion NORMALISE_BOUND as [ NORMALISE_BOUND_LOW NORMALISE_BOUND_HIGH ]; *)
-  (*     clear NORMALISE_BOUND. *)
-
-  (*     (** Start of proof proper *) *)
-  (*     eexists. split. *)
-  (*     eapply Smallstep.plus_one. *)
-  (*     eapply HTL.step_module; eauto. *)
-  (*     apply assumption_32bit. *)
-  (*     econstructor. econstructor. econstructor. crush. *)
-  (*     econstructor. econstructor. econstructor. crush. *)
-  (*     econstructor. econstructor. *)
-  (*     econstructor. econstructor. econstructor. econstructor. *)
-  (*     econstructor. econstructor. econstructor. econstructor. *)
-
-  (*     all: big_tac. *)
-
-  (*     1: { *)
-  (*       assert (HPle : Ple dst (RTL.max_reg_function f)). *)
-  (*       eapply RTL.max_reg_function_def. eassumption. auto. *)
-  (*       apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. *)
-  (*     } *)
-
-  (*     2: { *)
-  (*       assert (HPle : Ple dst (RTL.max_reg_function f)). *)
-  (*       eapply RTL.max_reg_function_def. eassumption. auto. *)
-  (*       apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. *)
-  (*     } *)
-
-  (*     (** Match assocmaps *) *)
-  (*     apply regs_lessdef_add_match; big_tac. *)
-
-  (*     (** Equality proof *) *)
-  (*     match goal with *)
-  (*     | [ |- context [valueToNat ?x] ] => *)
-  (*       assert (Z.to_nat *)
-  (*                 (Integers.Ptrofs.unsigned *)
-  (*                    (Integers.Ptrofs.divu *)
-  (*                       OFFSET *)
-  (*                       (Integers.Ptrofs.repr 4))) *)
-  (*               = *)
-  (*               valueToNat x) *)
-  (*         as EXPR_OK by admit *)
-  (*     end. *)
-  (*     rewrite <- EXPR_OK. *)
-
-  (*     specialize (H7 (Integers.Ptrofs.unsigned *)
-  (*                       (Integers.Ptrofs.divu *)
-  (*                          OFFSET *)
-  (*                          (Integers.Ptrofs.repr 4)))). *)
-  (*     exploit H7; big_tac. *)
-
-  (*     (** RSBP preservation *) *)
-  (*     unfold arr_stack_based_pointers in ASBP. *)
-  (*     specialize (ASBP (Integers.Ptrofs.unsigned *)
-  (*                         (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)))). *)
-  (*     exploit ASBP; big_tac. *)
-  (*     rewrite NORMALISE in H0. rewrite H1 in H0. assumption. *)
-
-  (*   + (** Preamble *) *)
-  (*     invert MARR. crush. *)
-
-  (*     unfold Op.eval_addressing in H0. *)
-  (*     destruct (Archi.ptr64) eqn:ARCHI; crush. *)
-
-  (*     unfold reg_stack_based_pointers in RSBP. *)
-  (*     pose proof (RSBP r0) as RSBPr0. *)
-  (*     pose proof (RSBP r1) as RSBPr1. *)
-
-  (*     destruct (Registers.Regmap.get r0 rs) eqn:EQr0; *)
-  (*     destruct (Registers.Regmap.get r1 rs) eqn:EQr1; crush. *)
-
-  (*     rewrite ARCHI in H1. crush. *)
-  (*     subst. *)
-  (*     clear RSBPr1. *)
-
-  (*     pose proof MASSOC as MASSOC'. *)
-  (*     invert MASSOC'. *)
-  (*     pose proof (H0 r0). *)
-  (*     pose proof (H0 r1). *)
-  (*     assert (HPler0 : Ple r0 (RTL.max_reg_function f)) *)
-  (*       by (eapply RTL.max_reg_function_use; eauto; crush; eauto). *)
-  (*     assert (HPler1 : Ple r1 (RTL.max_reg_function f)) *)
-  (*       by (eapply RTL.max_reg_function_use; eauto; simpl; auto). *)
-  (*     apply H6 in HPler0. *)
-  (*     apply H8 in HPler1. *)
-  (*     invert HPler0; invert HPler1; try congruence. *)
-  (*     rewrite EQr0 in H9. *)
-  (*     rewrite EQr1 in H11. *)
-  (*     invert H9. invert H11. *)
-  (*     clear H0. clear H6. clear H8. *)
-
-  (*     unfold check_address_parameter_signed in *; *)
-  (*     unfold check_address_parameter_unsigned in *; crush. *)
-
-  (*     remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ asr # r0)) *)
-  (*                                   (Integers.Ptrofs.of_int *)
-  (*                                      (Integers.Int.add (Integers.Int.mul (valueToInt asr # r1) (Integers.Int.repr z)) *)
-  (*                                                        (Integers.Int.repr z0)))) as OFFSET. *)
-
-  (*     (** Modular preservation proof *) *)
-  (*     assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE. *)
-  (*     { rewrite HeqOFFSET. *)
-  (*       apply PtrofsExtra.add_mod; crush; try lia. *)
-  (*       rewrite Integers.Ptrofs.unsigned_repr_eq. *)
-  (*       rewrite <- Zmod_div_mod; crush. *)
-  (*       apply PtrofsExtra.of_int_mod. *)
-  (*       apply IntExtra.add_mod; crush. *)
-  (*       apply IntExtra.mul_mod2; crush. *)
-  (*       rewrite Integers.Int.unsigned_repr_eq. *)
-  (*       rewrite <- Zmod_div_mod; crush. *)
-  (*       rewrite Integers.Int.unsigned_repr_eq. *)
-  (*       rewrite <- Zmod_div_mod; crush. } *)
-
-  (*     (** Read bounds proof *) *)
-  (*     assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH. *)
-  (*     { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; crush; auto. *)
-  (*       unfold stack_bounds in BOUNDS. *)
-  (*       exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET)); auto. *)
-  (*       split; try lia; apply Integers.Ptrofs.unsigned_range_2. *)
-  (*       small_tac. } *)
-
-  (*     (** Normalisation proof *) *)
-  (*     assert (Integers.Ptrofs.repr *)
-  (*               (4 * Integers.Ptrofs.unsigned *)
-  (*                      (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4))) = OFFSET) *)
-  (*       as NORMALISE. *)
-  (*     { replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) at 1 by reflexivity. *)
-  (*       rewrite <- PtrofsExtra.mul_unsigned. *)
-  (*       apply PtrofsExtra.mul_divu; crush. } *)
-
-  (*     (** Normalised bounds proof *) *)
-  (*     assert (0 <= *)
-  (*             Integers.Ptrofs.unsigned (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)) *)
-  (*             < (RTL.fn_stacksize f / 4)) *)
-  (*       as NORMALISE_BOUND. *)
-  (*     { split. *)
-  (*       apply Integers.Ptrofs.unsigned_range_2. *)
-  (*       assert (forall x y, Integers.Ptrofs.divu x y = Integers.Ptrofs.divu x y ) by reflexivity. *)
-  (*       unfold Integers.Ptrofs.divu at 2 in H0. *)
-  (*       rewrite H0. clear H0. *)
-  (*       rewrite Integers.Ptrofs.unsigned_repr; crush. *)
-  (*       apply Zmult_lt_reg_r with (p := 4); try lia. *)
-  (*       repeat rewrite ZLib.div_mul_undo; try lia. *)
-  (*       apply Z.div_pos; small_tac. *)
-  (*       apply Z.div_le_upper_bound; lia. } *)
-
-  (*     inversion NORMALISE_BOUND as [ NORMALISE_BOUND_LOW NORMALISE_BOUND_HIGH ]; *)
-  (*     clear NORMALISE_BOUND. *)
-
-  (*     (** Start of proof proper *) *)
-  (*     eexists. split. *)
-  (*     eapply Smallstep.plus_one. *)
-  (*     eapply HTL.step_module; eauto. *)
-  (*     apply assumption_32bit. *)
-  (*     econstructor. econstructor. econstructor. crush. *)
-  (*     econstructor. econstructor. econstructor. crush. *)
-  (*     econstructor. econstructor. econstructor. *)
-  (*     econstructor. econstructor. econstructor. econstructor. *)
-  (*     econstructor. *)
-  (*     eapply Verilog.erun_Vbinop with (EQ := ?[EQ6]). *)
-  (*     econstructor. econstructor. econstructor. econstructor. *)
-  (*     econstructor. econstructor. econstructor. econstructor. *)
-  (*     econstructor. econstructor. *)
-
-  (*     all: big_tac. *)
-
-  (*     1: { assert (HPle : Ple dst (RTL.max_reg_function f)). *)
-  (*          eapply RTL.max_reg_function_def. eassumption. auto. *)
-  (*          apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. } *)
-
-  (*     2: { assert (HPle : Ple dst (RTL.max_reg_function f)). *)
-  (*          eapply RTL.max_reg_function_def. eassumption. auto. *)
-  (*          apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. } *)
-
-  (*     (** Match assocmaps *) *)
-  (*     apply regs_lessdef_add_match; big_tac. *)
-
-  (*     (** Equality proof *) *)
-  (*     match goal with *)
-  (*     | [ |- context [valueToNat ?x] ] => *)
-  (*       assert (Z.to_nat *)
-  (*                 (Integers.Ptrofs.unsigned *)
-  (*                    (Integers.Ptrofs.divu *)
-  (*                       OFFSET *)
-  (*                       (Integers.Ptrofs.repr 4))) *)
-  (*               = *)
-  (*               valueToNat x) *)
-  (*         as EXPR_OK by admit *)
-  (*     end. *)
-  (*     rewrite <- EXPR_OK. *)
-
-  (*     specialize (H7 (Integers.Ptrofs.unsigned *)
-  (*                       (Integers.Ptrofs.divu *)
-  (*                          OFFSET *)
-  (*                          (Integers.Ptrofs.repr 4)))). *)
-  (*     exploit H7; big_tac. *)
-
-  (*     (** RSBP preservation *) *)
-  (*     unfold arr_stack_based_pointers in ASBP. *)
-  (*     specialize (ASBP (Integers.Ptrofs.unsigned *)
-  (*                         (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)))). *)
-  (*     exploit ASBP; big_tac. *)
-  (*     rewrite NORMALISE in H0. rewrite H1 in H0. assumption. *)
-
-  (*   + invert MARR. crush. *)
-
-  (*     unfold Op.eval_addressing in H0. *)
-  (*     destruct (Archi.ptr64) eqn:ARCHI; crush. *)
-  (*     rewrite ARCHI in H0. crush. *)
-
-  (*     unfold check_address_parameter_unsigned in *; *)
-  (*     unfold check_address_parameter_signed in *; crush. *)
-
-  (*     assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. *)
-  (*     rewrite ZERO in H1. clear ZERO. *)
-  (*     rewrite Integers.Ptrofs.add_zero_l in H1. *)
-
-  (*     remember i0 as OFFSET. *)
-
-  (*     (** Modular preservation proof *) *)
-  (*     rename H0 into MOD_PRESERVE. *)
-
-  (*     (** Read bounds proof *) *)
-  (*     assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH. *)
-  (*     { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; crush; auto. *)
-  (*       unfold stack_bounds in BOUNDS. *)
-  (*       exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET)); big_tac. } *)
-
-  (*     (** Normalisation proof *) *)
-  (*     assert (Integers.Ptrofs.repr *)
-  (*               (4 * Integers.Ptrofs.unsigned *)
-  (*                      (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4))) = OFFSET) *)
-  (*       as NORMALISE. *)
-  (*     { replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) at 1 by reflexivity. *)
-  (*       rewrite <- PtrofsExtra.mul_unsigned. *)
-  (*       apply PtrofsExtra.mul_divu; crush. } *)
-
-  (*     (** Normalised bounds proof *) *)
-  (*     assert (0 <= *)
-  (*             Integers.Ptrofs.unsigned (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)) *)
-  (*             < (RTL.fn_stacksize f / 4)) *)
-  (*       as NORMALISE_BOUND. *)
-  (*     { split. *)
-  (*       apply Integers.Ptrofs.unsigned_range_2. *)
-  (*       assert (forall x y, Integers.Ptrofs.divu x y = Integers.Ptrofs.divu x y ) by reflexivity. *)
-  (*       unfold Integers.Ptrofs.divu at 2 in H0. *)
-  (*       rewrite H0. clear H0. *)
-  (*       rewrite Integers.Ptrofs.unsigned_repr; crush. *)
-  (*       apply Zmult_lt_reg_r with (p := 4); try lia. *)
-  (*       repeat rewrite ZLib.div_mul_undo; try lia. *)
-  (*       apply Z.div_pos; small_tac. *)
-  (*       apply Z.div_le_upper_bound; lia. } *)
-
-  (*     inversion NORMALISE_BOUND as [ NORMALISE_BOUND_LOW NORMALISE_BOUND_HIGH ]; *)
-  (*     clear NORMALISE_BOUND. *)
-
-  (*     (** Start of proof proper *) *)
-  (*     eexists. split. *)
-  (*     eapply Smallstep.plus_one. *)
-  (*     eapply HTL.step_module; eauto. *)
-  (*     apply assumption_32bit. *)
-  (*     econstructor. econstructor. econstructor. crush. *)
-  (*     econstructor. econstructor. econstructor. econstructor. crush. *)
-
-  (*     all: big_tac. *)
-
-  (*     1: { assert (HPle : Ple dst (RTL.max_reg_function f)). *)
-  (*          eapply RTL.max_reg_function_def. eassumption. auto. *)
-  (*          apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. } *)
-
-  (*     2: { assert (HPle : Ple dst (RTL.max_reg_function f)). *)
-  (*          eapply RTL.max_reg_function_def. eassumption. auto. *)
-  (*          apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. } *)
-
-  (*     (** Match assocmaps *) *)
-  (*     apply regs_lessdef_add_match; big_tac. *)
-
-  (*     (** Equality proof *) *)
-  (*     match goal with (* Prevents issues with evars *) *)
-  (*     | [ |- context [valueToNat ?x] ] => *)
-  (*       assert (Z.to_nat *)
-  (*                 (Integers.Ptrofs.unsigned *)
-  (*                    (Integers.Ptrofs.divu *)
-  (*                       OFFSET *)
-  (*                       (Integers.Ptrofs.repr 4))) *)
-  (*               = *)
-  (*               valueToNat x) *)
-  (*         as EXPR_OK by admit *)
-  (*     end. *)
-  (*     rewrite <- EXPR_OK. *)
-
-  (*     specialize (H7 (Integers.Ptrofs.unsigned *)
-  (*                       (Integers.Ptrofs.divu *)
-  (*                          OFFSET *)
-  (*                          (Integers.Ptrofs.repr 4)))). *)
-  (*     exploit H7; big_tac. *)
-
-  (*     (** RSBP preservation *) *)
-  (*     unfold arr_stack_based_pointers in ASBP. *)
-  (*     specialize (ASBP (Integers.Ptrofs.unsigned *)
-  (*                         (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)))). *)
-  (*     exploit ASBP; big_tac. *)
-  (*     rewrite NORMALISE in H0. rewrite H1 in H0. assumption. *)
-  (* Admitted. *)
-  (* Hint Resolve transl_iload_correct : htlproof. *)
-
-  (* Lemma transl_istore_correct: *)
-  (*   forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive) *)
-  (*     (rs : Registers.Regmap.t Values.val) (m : mem) (chunk : AST.memory_chunk) *)
-  (*     (addr : Op.addressing) (args : list Registers.reg) (src : Registers.reg) *)
-  (*     (pc' : RTL.node) (a : Values.val) (m' : mem), *)
-  (*     (RTL.fn_code f) ! pc = Some (RTL.Istore chunk addr args src pc') -> *)
-  (*     Op.eval_addressing ge sp addr (map (fun r : positive => Registers.Regmap.get r rs) args) = Some a -> *)
-  (*     Mem.storev chunk m a (Registers.Regmap.get src rs) = Some m' -> *)
-  (*     forall R1 : HTL.state, *)
-  (*       match_states (RTL.State s f sp pc rs m) R1 -> *)
-  (*       exists R2 : HTL.state, *)
-  (*         Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ match_states (RTL.State s f sp pc' rs m') R2. *)
-  (* Proof. *)
-  (*   intros s f sp pc rs m chunk addr args src pc' a m' H H0 H1 R1 MSTATES. *)
-  (*   inv_state. inv_arr_access. *)
-
-  (*   + (** Preamble *) *)
-  (*     invert MARR. crush. *)
-
-  (*     unfold Op.eval_addressing in H0. *)
-  (*     destruct (Archi.ptr64) eqn:ARCHI; crush. *)
-
-  (*     unfold reg_stack_based_pointers in RSBP. *)
-  (*     pose proof (RSBP r0) as RSBPr0. *)
-
-  (*     destruct (Registers.Regmap.get r0 rs) eqn:EQr0; crush. *)
-
-  (*     rewrite ARCHI in H1. crush. *)
-  (*     subst. *)
-
-  (*     pose proof MASSOC as MASSOC'. *)
-  (*     invert MASSOC'. *)
-  (*     pose proof (H0 r0). *)
-  (*     assert (HPler0 : Ple r0 (RTL.max_reg_function f)) *)
-  (*       by (eapply RTL.max_reg_function_use; eauto; crush; eauto). *)
-  (*     apply H6 in HPler0. *)
-  (*     invert HPler0; try congruence. *)
-  (*     rewrite EQr0 in H8. *)
-  (*     invert H8. *)
-  (*     clear H0. clear H6. *)
-
-  (*     unfold check_address_parameter_unsigned in *; *)
-  (*     unfold check_address_parameter_signed in *; crush. *)
-
-  (*     remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ asr # r0)) *)
-  (*                                   (Integers.Ptrofs.of_int (Integers.Int.repr z))) as OFFSET. *)
-
-  (*     (** Modular preservation proof *) *)
-  (*     assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE. *)
-  (*     { rewrite HeqOFFSET. *)
-  (*       apply PtrofsExtra.add_mod; crush; try lia. *)
-  (*       rewrite Integers.Ptrofs.unsigned_repr_eq. *)
-  (*       rewrite <- Zmod_div_mod; crush. *)
-  (*       apply PtrofsExtra.of_int_mod. *)
-  (*       rewrite Integers.Int.unsigned_repr_eq. *)
-  (*       rewrite <- Zmod_div_mod; crush. } *)
-
-  (*     (** Write bounds proof *) *)
-  (*     assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as WRITE_BOUND_HIGH. *)
-  (*     { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; crush; auto. *)
-  (*       unfold stack_bounds in BOUNDS. *)
-  (*       exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET) (Registers.Regmap.get src rs)); big_tac. *)
-  (*       apply Integers.Ptrofs.unsigned_range_2. } *)
-
-  (*     (** Start of proof proper *) *)
-  (*     eexists. split. *)
-  (*     eapply Smallstep.plus_one. *)
-  (*     eapply HTL.step_module; eauto. *)
-  (*     apply assumption_32bit. *)
-  (*     econstructor. econstructor. econstructor. *)
-  (*     eapply Verilog.stmnt_runp_Vnonblock_arr. crush. *)
-  (*     econstructor. *)
-  (*     eapply Verilog.erun_Vbinop with (EQ := ?[EQ7]). *)
-  (*     eapply Verilog.erun_Vbinop with (EQ := ?[EQ8]). *)
-  (*     econstructor. *)
-  (*     econstructor. *)
-  (*     econstructor. econstructor. econstructor. econstructor. *)
-  (*     econstructor. econstructor. econstructor. econstructor. *)
-
-  (*     all: crush. *)
-
-  (*     (** State Lookup *) *)
-  (*     unfold Verilog.merge_regs. *)
-  (*     crush. *)
-  (*     unfold_merge. *)
-  (*     apply AssocMap.gss. *)
-
-  (*     (** Match states *) *)
-  (*     rewrite assumption_32bit. *)
-  (*     econstructor; eauto. *)
-
-  (*     (** Match assocmaps *) *)
-  (*     unfold Verilog.merge_regs. crush. unfold_merge. *)
-  (*     apply regs_lessdef_add_greater. *)
-  (*     unfold Plt; lia. *)
-  (*     assumption. *)
-
-  (*     (** States well formed *) *)
-  (*     unfold state_st_wf. inversion 1. crush. *)
-  (*     unfold Verilog.merge_regs. *)
-  (*     unfold_merge. *)
-  (*     apply AssocMap.gss. *)
-
-  (*     (** Equality proof *) *)
-  (*     match goal with *)
-  (*     | [ |- context [valueToNat ?x] ] => *)
-  (*       assert (Z.to_nat *)
-  (*                 (Integers.Ptrofs.unsigned *)
-  (*                    (Integers.Ptrofs.divu *)
-  (*                       OFFSET *)
-  (*                       (Integers.Ptrofs.repr 4))) *)
-  (*               = *)
-  (*               valueToNat x) *)
-  (*         as EXPR_OK by admit *)
-  (*     end. *)
-
-  (*     assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. *)
-  (*     inversion MASSOC; revert HeqOFFSET; subst; clear MASSOC; intros HeqOFFSET. *)
-
-  (*     econstructor. *)
-  (*     repeat split; crush. *)
-  (*     unfold HTL.empty_stack. *)
-  (*     crush. *)
-  (*     unfold Verilog.merge_arrs. *)
-
-  (*     rewrite AssocMap.gcombine. *)
-  (*     2: { reflexivity. } *)
-  (*     unfold Verilog.arr_assocmap_set. *)
-  (*     rewrite AssocMap.gss. *)
-  (*     unfold Verilog.merge_arr. *)
-  (*     rewrite AssocMap.gss. *)
-  (*     setoid_rewrite H5. *)
-  (*     reflexivity. *)
-
-  (*     rewrite combine_length. *)
-  (*     rewrite <- array_set_len. *)
-  (*     unfold arr_repeat. crush. *)
-  (*     apply list_repeat_len. *)
-
-  (*     rewrite <- array_set_len. *)
-  (*     unfold arr_repeat. crush. *)
-  (*     rewrite list_repeat_len. *)
-  (*     rewrite H4. reflexivity. *)
-
-  (*     remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ asr # r0)) *)
-  (*                                   (Integers.Ptrofs.of_int (Integers.Int.repr z))) as OFFSET. *)
-
-  (*     destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET). *)
-
-  (*     erewrite Mem.load_store_same. *)
-  (*     2: { rewrite ZERO. *)
-  (*          rewrite Integers.Ptrofs.add_zero_l. *)
-  (*          rewrite e. *)
-  (*          rewrite Integers.Ptrofs.unsigned_repr. *)
-  (*          exact H1. *)
-  (*          apply Integers.Ptrofs.unsigned_range_2. } *)
-  (*     constructor. *)
-  (*     erewrite combine_lookup_second. *)
-  (*     simpl. *)
-  (*     assert (Ple src (RTL.max_reg_function f)) *)
-  (*       by (eapply RTL.max_reg_function_use; eauto; simpl; auto); *)
-  (*     apply H0 in H13. *)
-  (*     destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; invert H13; eauto. *)
-
-  (*     rewrite <- array_set_len. *)
-  (*     unfold arr_repeat. crush. *)
-  (*     rewrite list_repeat_len. auto. *)
-
-  (*     assert (4 * ptr / 4 = Integers.Ptrofs.unsigned OFFSET / 4) by (f_equal; assumption). *)
-  (*     rewrite Z.mul_comm in H13. *)
-  (*     rewrite Z_div_mult in H13; try lia. *)
-  (*     replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) in H13 by reflexivity. *)
-  (*     rewrite <- PtrofsExtra.divu_unsigned in H13; unfold_constants; try lia. *)
-  (*     rewrite H13. rewrite EXPR_OK. *)
-  (*     rewrite array_get_error_set_bound. *)
-  (*     reflexivity. *)
-  (*     unfold arr_length, arr_repeat. simpl. *)
-  (*     rewrite list_repeat_len. lia. *)
-
-  (*     erewrite Mem.load_store_other with (m1 := m). *)
-  (*     2: { exact H1. } *)
-  (*     2: { right. *)
-  (*          rewrite ZERO. *)
-  (*          rewrite Integers.Ptrofs.add_zero_l. *)
-  (*          rewrite Integers.Ptrofs.unsigned_repr. *)
-  (*          simpl. *)
-  (*          destruct (Z_le_gt_dec (4 * ptr + 4) (Integers.Ptrofs.unsigned OFFSET)); eauto. *)
-  (*          right. *)
-  (*          apply ZExtra.mod_0_bounds; try lia. *)
-  (*          apply ZLib.Z_mod_mult'. *)
-  (*          rewrite Z2Nat.id in H15; try lia. *)
-  (*          apply Zmult_lt_compat_r with (p := 4) in H15; try lia. *)
-  (*          rewrite ZLib.div_mul_undo in H15; try lia. *)
-  (*          split; try lia. *)
-  (*          apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia. *)
-  (*     } *)
-
-  (*     rewrite <- EXPR_OK. *)
-  (*     rewrite PtrofsExtra.divu_unsigned; auto; try (unfold_constants; lia). *)
-  (*     destruct (ptr ==Z Integers.Ptrofs.unsigned OFFSET / 4). *)
-  (*     apply Z.mul_cancel_r with (p := 4) in e; try lia. *)
-  (*     rewrite ZLib.div_mul_undo in e; try lia. *)
-  (*     rewrite combine_lookup_first. *)
-  (*     eapply H7; eauto. *)
-
-  (*     rewrite <- array_set_len. *)
-  (*     unfold arr_repeat. crush. *)
-  (*     rewrite list_repeat_len. auto. *)
-  (*     rewrite array_gso. *)
-  (*     unfold array_get_error. *)
-  (*     unfold arr_repeat. *)
-  (*     crush. *)
-  (*     apply list_repeat_lookup. *)
-  (*     lia. *)
-  (*     unfold_constants. *)
-  (*     intro. *)
-  (*     apply Z2Nat.inj_iff in H13; try lia. *)
-  (*     apply Z.div_pos; try lia. *)
-  (*     apply Integers.Ptrofs.unsigned_range. *)
-
-  (*     assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. *)
-  (*     unfold arr_stack_based_pointers. *)
-  (*     intros. *)
-  (*     destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET). *)
-
-  (*     crush. *)
-  (*     erewrite Mem.load_store_same. *)
-  (*     2: { rewrite ZERO. *)
-  (*          rewrite Integers.Ptrofs.add_zero_l. *)
-  (*          rewrite e. *)
-  (*          rewrite Integers.Ptrofs.unsigned_repr. *)
-  (*          exact H1. *)
-  (*          apply Integers.Ptrofs.unsigned_range_2. } *)
-  (*     crush. *)
-  (*     destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; try constructor. *)
-  (*     destruct (Archi.ptr64); try discriminate. *)
-  (*     pose proof (RSBP src). rewrite EQ_SRC in H0. *)
-  (*     assumption. *)
-
-  (*     simpl. *)
-  (*     erewrite Mem.load_store_other with (m1 := m). *)
-  (*     2: { exact H1. } *)
-  (*     2: { right. *)
-  (*          rewrite ZERO. *)
-  (*          rewrite Integers.Ptrofs.add_zero_l. *)
-  (*          rewrite Integers.Ptrofs.unsigned_repr. *)
-  (*          simpl. *)
-  (*          destruct (Z_le_gt_dec (4 * ptr + 4) (Integers.Ptrofs.unsigned OFFSET)); eauto. *)
-  (*          right. *)
-  (*          apply ZExtra.mod_0_bounds; try lia. *)
-  (*          apply ZLib.Z_mod_mult'. *)
-  (*          invert H0. *)
-  (*          apply Zmult_lt_compat_r with (p := 4) in H14; try lia. *)
-  (*          rewrite ZLib.div_mul_undo in H14; try lia. *)
-  (*          split; try lia. *)
-  (*          apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia. *)
-  (*     } *)
-  (*     apply ASBP; assumption. *)
-
-  (*     unfold stack_bounds in *. intros. *)
-  (*     simpl. *)
-  (*     assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. *)
-  (*     erewrite Mem.load_store_other with (m1 := m). *)
-  (*     2: { exact H1. } *)
-  (*     2: { right. right. simpl. *)
-  (*          rewrite ZERO. *)
-  (*          rewrite Integers.Ptrofs.add_zero_l. *)
-  (*          rewrite Integers.Ptrofs.unsigned_repr; crush; try lia. *)
-  (*          apply ZExtra.mod_0_bounds; crush; try lia. } *)
-  (*     crush. *)
-  (*     exploit (BOUNDS ptr); try lia. intros. crush. *)
-  (*     exploit (BOUNDS ptr v); try lia. intros. *)
-  (*     invert H0. *)
-  (*     match goal with | |- ?x = _ => destruct x eqn:EQ end; try reflexivity. *)
-  (*     assert (Mem.valid_access m AST.Mint32 sp' *)
-  (*                              (Integers.Ptrofs.unsigned *)
-  (*                                 (Integers.Ptrofs.add (Integers.Ptrofs.repr 0) *)
-  (*                                                      (Integers.Ptrofs.repr ptr))) Writable). *)
-  (*     { pose proof H1. eapply Mem.store_valid_access_2 in H0. *)
-  (*       exact H0. eapply Mem.store_valid_access_3. eassumption. } *)
-  (*     pose proof (Mem.valid_access_store m AST.Mint32 sp' *)
-  (*                                        (Integers.Ptrofs.unsigned *)
-  (*                                           (Integers.Ptrofs.add (Integers.Ptrofs.repr 0) *)
-  (*                                                                (Integers.Ptrofs.repr ptr))) v). *)
-  (*     apply X in H0. invert H0. congruence. *)
-
-  (*   + (** Preamble *) *)
-  (*     invert MARR. crush. *)
-
-  (*     unfold Op.eval_addressing in H0. *)
-  (*     destruct (Archi.ptr64) eqn:ARCHI; crush. *)
-
-  (*     unfold reg_stack_based_pointers in RSBP. *)
-  (*     pose proof (RSBP r0) as RSBPr0. *)
-  (*     pose proof (RSBP r1) as RSBPr1. *)
-
-  (*     destruct (Registers.Regmap.get r0 rs) eqn:EQr0; *)
-  (*     destruct (Registers.Regmap.get r1 rs) eqn:EQr1; crush. *)
-
-  (*     rewrite ARCHI in H1. crush. *)
-  (*     subst. *)
-  (*     clear RSBPr1. *)
-
-  (*     pose proof MASSOC as MASSOC'. *)
-  (*     invert MASSOC'. *)
-  (*     pose proof (H0 r0). *)
-  (*     pose proof (H0 r1). *)
-  (*     assert (HPler0 : Ple r0 (RTL.max_reg_function f)) *)
-  (*       by (eapply RTL.max_reg_function_use; eauto; crush; eauto). *)
-  (*     assert (HPler1 : Ple r1 (RTL.max_reg_function f)) *)
-  (*       by (eapply RTL.max_reg_function_use; eauto; simpl; auto). *)
-  (*     apply H6 in HPler0. *)
-  (*     apply H8 in HPler1. *)
-  (*     invert HPler0; invert HPler1; try congruence. *)
-  (*     rewrite EQr0 in H9. *)
-  (*     rewrite EQr1 in H11. *)
-  (*     invert H9. invert H11. *)
-  (*     clear H0. clear H6. clear H8. *)
-
-  (*     unfold check_address_parameter_signed in *; *)
-  (*     unfold check_address_parameter_unsigned in *; crush. *)
-
-  (*     remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ asr # r0)) *)
-  (*                                   (Integers.Ptrofs.of_int *)
-  (*                                      (Integers.Int.add (Integers.Int.mul (valueToInt asr # r1) (Integers.Int.repr z)) *)
-  (*                                                        (Integers.Int.repr z0)))) as OFFSET. *)
-
-  (*     (** Modular preservation proof *) *)
-  (*     assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE. *)
-  (*     { rewrite HeqOFFSET. *)
-  (*       apply PtrofsExtra.add_mod; crush; try lia. *)
-  (*       rewrite Integers.Ptrofs.unsigned_repr_eq. *)
-  (*       rewrite <- Zmod_div_mod; crush. *)
-  (*       apply PtrofsExtra.of_int_mod. *)
-  (*       apply IntExtra.add_mod; crush. *)
-  (*       apply IntExtra.mul_mod2; crush. *)
-  (*       rewrite Integers.Int.unsigned_repr_eq. *)
-  (*       rewrite <- Zmod_div_mod; crush. *)
-  (*       rewrite Integers.Int.unsigned_repr_eq. *)
-  (*       rewrite <- Zmod_div_mod; crush. } *)
-
-  (*     (** Write bounds proof *) *)
-  (*     assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as WRITE_BOUND_HIGH. *)
-  (*     { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; crush; auto. *)
-  (*       unfold stack_bounds in BOUNDS. *)
-  (*       exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET) (Registers.Regmap.get src rs)); auto. *)
-  (*       split; try lia; apply Integers.Ptrofs.unsigned_range_2. *)
-  (*       small_tac. } *)
-
-  (*     (** Start of proof proper *) *)
-  (*     eexists. split. *)
-  (*     eapply Smallstep.plus_one. *)
-  (*     eapply HTL.step_module; eauto. *)
-  (*     apply assumption_32bit. *)
-  (*     econstructor. econstructor. econstructor. *)
-  (*     eapply Verilog.stmnt_runp_Vnonblock_arr. crush. *)
-  (*     econstructor. *)
-  (*     eapply Verilog.erun_Vbinop with (EQ := ?[EQ9]). *)
-  (*     eapply Verilog.erun_Vbinop with (EQ := ?[EQ10]). *)
-  (*     eapply Verilog.erun_Vbinop with (EQ := ?[EQ11]). *)
-  (*     econstructor. econstructor. econstructor. econstructor. *)
-  (*     econstructor. *)
-  (*     eapply Verilog.erun_Vbinop with (EQ := ?[EQ12]). *)
-  (*     econstructor. econstructor. econstructor. econstructor. *)
-  (*     econstructor. econstructor. econstructor. econstructor. *)
-  (*     econstructor. econstructor. econstructor. econstructor. *)
-
-  (*     all: crush. *)
-
-  (*     (** State Lookup *) *)
-  (*     unfold Verilog.merge_regs. *)
-  (*     crush. *)
-  (*     unfold_merge. *)
-  (*     apply AssocMap.gss. *)
-
-  (*     (** Match states *) *)
-  (*     rewrite assumption_32bit. *)
-  (*     econstructor; eauto. *)
-
-  (*     (** Match assocmaps *) *)
-  (*     unfold Verilog.merge_regs. crush. unfold_merge. *)
-  (*     apply regs_lessdef_add_greater. *)
-  (*     unfold Plt; lia. *)
-  (*     assumption. *)
-
-  (*     (** States well formed *) *)
-  (*     unfold state_st_wf. inversion 1. crush. *)
-  (*     unfold Verilog.merge_regs. *)
-  (*     unfold_merge. *)
-  (*     apply AssocMap.gss. *)
-
-  (*     (** Equality proof *) *)
-  (*     assert (Z.to_nat *)
-  (*               (Integers.Ptrofs.unsigned *)
-  (*                  (Integers.Ptrofs.divu *)
-  (*                     OFFSET *)
-  (*                     (Integers.Ptrofs.repr 4))) *)
-  (*             = *)
-  (*             valueToNat (vdiv *)
-  (*                           (vplus (vplus asr # r0 (ZToValue 32 z0) ?EQ11) (vmul asr # r1 (ZToValue 32 z) ?EQ12) *)
-  (*                                  ?EQ10) (ZToValue 32 4) ?EQ9)) *)
-  (*       as EXPR_OK by admit. *)
-
-  (*     assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. *)
-  (*     inversion MASSOC; revert HeqOFFSET; subst; clear MASSOC; intros HeqOFFSET. *)
-
-  (*     econstructor. *)
-  (*     repeat split; crush. *)
-  (*     unfold HTL.empty_stack. *)
-  (*     crush. *)
-  (*     unfold Verilog.merge_arrs. *)
-
-  (*     rewrite AssocMap.gcombine. *)
-  (*     2: { reflexivity. } *)
-  (*     unfold Verilog.arr_assocmap_set. *)
-  (*     rewrite AssocMap.gss. *)
-  (*     unfold Verilog.merge_arr. *)
-  (*     rewrite AssocMap.gss. *)
-  (*     setoid_rewrite H5. *)
-  (*     reflexivity. *)
-
-  (*     rewrite combine_length. *)
-  (*     rewrite <- array_set_len. *)
-  (*     unfold arr_repeat. crush. *)
-  (*     apply list_repeat_len. *)
-
-  (*     rewrite <- array_set_len. *)
-  (*     unfold arr_repeat. crush. *)
-  (*     rewrite list_repeat_len. *)
-  (*     rewrite H4. reflexivity. *)
-
-  (*     remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ asr # r0)) *)
-  (*                                   (Integers.Ptrofs.of_int *)
-  (*                                      (Integers.Int.add (Integers.Int.mul (valueToInt asr # r1) (Integers.Int.repr z)) *)
-  (*                                                        (Integers.Int.repr z0)))) as OFFSET. *)
-  (*     destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET). *)
-
-  (*     erewrite Mem.load_store_same. *)
-  (*     2: { rewrite ZERO. *)
-  (*          rewrite Integers.Ptrofs.add_zero_l. *)
-  (*          rewrite e. *)
-  (*          rewrite Integers.Ptrofs.unsigned_repr. *)
-  (*          exact H1. *)
-  (*          apply Integers.Ptrofs.unsigned_range_2. } *)
-  (*     constructor. *)
-  (*     erewrite combine_lookup_second. *)
-  (*     simpl. *)
-  (*     assert (Ple src (RTL.max_reg_function f)) *)
-  (*       by (eapply RTL.max_reg_function_use; eauto; simpl; auto); *)
-  (*     apply H0 in H16. *)
-  (*     destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; invert H16; eauto. *)
-
-  (*     rewrite <- array_set_len. *)
-  (*     unfold arr_repeat. crush. *)
-  (*     rewrite list_repeat_len. auto. *)
-
-  (*     assert (4 * ptr / 4 = Integers.Ptrofs.unsigned OFFSET / 4) by (f_equal; assumption). *)
-  (*     rewrite Z.mul_comm in H16. *)
-  (*     rewrite Z_div_mult in H16; try lia. *)
-  (*     replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) in H16 by reflexivity. *)
-  (*     rewrite <- PtrofsExtra.divu_unsigned in H16; unfold_constants; try lia. *)
-  (*     rewrite H16. rewrite EXPR_OK. *)
-  (*     rewrite array_get_error_set_bound. *)
-  (*     reflexivity. *)
-  (*     unfold arr_length, arr_repeat. simpl. *)
-  (*     rewrite list_repeat_len. lia. *)
-
-  (*     erewrite Mem.load_store_other with (m1 := m). *)
-  (*     2: { exact H1. } *)
-  (*     2: { right. *)
-  (*          rewrite ZERO. *)
-  (*          rewrite Integers.Ptrofs.add_zero_l. *)
-  (*          rewrite Integers.Ptrofs.unsigned_repr. *)
-  (*          simpl. *)
-  (*          destruct (Z_le_gt_dec (4 * ptr + 4) (Integers.Ptrofs.unsigned OFFSET)); eauto. *)
-  (*          right. *)
-  (*          apply ZExtra.mod_0_bounds; try lia. *)
-  (*          apply ZLib.Z_mod_mult'. *)
-  (*          rewrite Z2Nat.id in H18; try lia. *)
-  (*          apply Zmult_lt_compat_r with (p := 4) in H18; try lia. *)
-  (*          rewrite ZLib.div_mul_undo in H18; try lia. *)
-  (*          split; try lia. *)
-  (*          apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia. *)
-  (*     } *)
-
-  (*     rewrite <- EXPR_OK. *)
-  (*     rewrite PtrofsExtra.divu_unsigned; auto; try (unfold_constants; lia). *)
-  (*     destruct (ptr ==Z Integers.Ptrofs.unsigned OFFSET / 4). *)
-  (*     apply Z.mul_cancel_r with (p := 4) in e; try lia. *)
-  (*     rewrite ZLib.div_mul_undo in e; try lia. *)
-  (*     rewrite combine_lookup_first. *)
-  (*     eapply H7; eauto. *)
-
-  (*     rewrite <- array_set_len. *)
-  (*     unfold arr_repeat. crush. *)
-  (*     rewrite list_repeat_len. auto. *)
-  (*     rewrite array_gso. *)
-  (*     unfold array_get_error. *)
-  (*     unfold arr_repeat. *)
-  (*     crush. *)
-  (*     apply list_repeat_lookup. *)
-  (*     lia. *)
-  (*     unfold_constants. *)
-  (*     intro. *)
-  (*     apply Z2Nat.inj_iff in H16; try lia. *)
-  (*     apply Z.div_pos; try lia. *)
-  (*     apply Integers.Ptrofs.unsigned_range. *)
-
-  (*     assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. *)
-  (*     unfold arr_stack_based_pointers. *)
-  (*     intros. *)
-  (*     destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET). *)
-
-  (*     crush. *)
-  (*     erewrite Mem.load_store_same. *)
-  (*     2: { rewrite ZERO. *)
-  (*          rewrite Integers.Ptrofs.add_zero_l. *)
-  (*          rewrite e. *)
-  (*          rewrite Integers.Ptrofs.unsigned_repr. *)
-  (*          exact H1. *)
-  (*          apply Integers.Ptrofs.unsigned_range_2. } *)
-  (*     crush. *)
-  (*     destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; try constructor. *)
-  (*     destruct (Archi.ptr64); try discriminate. *)
-  (*     pose proof (RSBP src). rewrite EQ_SRC in H0. *)
-  (*     assumption. *)
-
-  (*     simpl. *)
-  (*     erewrite Mem.load_store_other with (m1 := m). *)
-  (*     2: { exact H1. } *)
-  (*     2: { right. *)
-  (*          rewrite ZERO. *)
-  (*          rewrite Integers.Ptrofs.add_zero_l. *)
-  (*          rewrite Integers.Ptrofs.unsigned_repr. *)
-  (*          simpl. *)
-  (*          destruct (Z_le_gt_dec (4 * ptr + 4) (Integers.Ptrofs.unsigned OFFSET)); eauto. *)
-  (*          right. *)
-  (*          apply ZExtra.mod_0_bounds; try lia. *)
-  (*          apply ZLib.Z_mod_mult'. *)
-  (*          invert H0. *)
-  (*          apply Zmult_lt_compat_r with (p := 4) in H17; try lia. *)
-  (*          rewrite ZLib.div_mul_undo in H17; try lia. *)
-  (*          split; try lia. *)
-  (*          apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia. *)
-  (*     } *)
-  (*     apply ASBP; assumption. *)
-
-  (*     unfold stack_bounds in *. intros. *)
-  (*     simpl. *)
-  (*     assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. *)
-  (*     erewrite Mem.load_store_other with (m1 := m). *)
-  (*     2: { exact H1. } *)
-  (*     2: { right. right. simpl. *)
-  (*          rewrite ZERO. *)
-  (*          rewrite Integers.Ptrofs.add_zero_l. *)
-  (*          rewrite Integers.Ptrofs.unsigned_repr; crush; try lia. *)
-  (*          apply ZExtra.mod_0_bounds; crush; try lia. } *)
-  (*     crush. *)
-  (*     exploit (BOUNDS ptr); try lia. intros. crush. *)
-  (*     exploit (BOUNDS ptr v); try lia. intros. *)
-  (*     invert H0. *)
-  (*     match goal with | |- ?x = _ => destruct x eqn:EQ end; try reflexivity. *)
-  (*     assert (Mem.valid_access m AST.Mint32 sp' *)
-  (*                              (Integers.Ptrofs.unsigned *)
-  (*                                 (Integers.Ptrofs.add (Integers.Ptrofs.repr 0) *)
-  (*                                                      (Integers.Ptrofs.repr ptr))) Writable). *)
-  (*     { pose proof H1. eapply Mem.store_valid_access_2 in H0. *)
-  (*       exact H0. eapply Mem.store_valid_access_3. eassumption. } *)
-  (*     pose proof (Mem.valid_access_store m AST.Mint32 sp' *)
-  (*                                        (Integers.Ptrofs.unsigned *)
-  (*                                           (Integers.Ptrofs.add (Integers.Ptrofs.repr 0) *)
-  (*                                                                (Integers.Ptrofs.repr ptr))) v). *)
-  (*     apply X in H0. invert H0. congruence. *)
-
-  (*   + invert MARR. crush. *)
-
-  (*     unfold Op.eval_addressing in H0. *)
-  (*     destruct (Archi.ptr64) eqn:ARCHI; crush. *)
-  (*     rewrite ARCHI in H0. crush. *)
-
-  (*     unfold check_address_parameter_unsigned in *; *)
-  (*     unfold check_address_parameter_signed in *; crush. *)
-
-  (*     assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. *)
-  (*     rewrite ZERO in H1. clear ZERO. *)
-  (*     rewrite Integers.Ptrofs.add_zero_l in H1. *)
-
-  (*     remember i0 as OFFSET. *)
-
-  (*     (** Modular preservation proof *) *)
-  (*     rename H0 into MOD_PRESERVE. *)
-
-  (*     (** Write bounds proof *) *)
-  (*     assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as WRITE_BOUND_HIGH. *)
-  (*     { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; crush; auto. *)
-  (*       unfold stack_bounds in BOUNDS. *)
-  (*       exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET) (Registers.Regmap.get src rs)); auto. *)
-  (*       crush. *)
-  (*       replace (Integers.Ptrofs.repr 0) with (Integers.Ptrofs.zero) by reflexivity. *)
-  (*       small_tac. } *)
-
-  (*     (** Start of proof proper *) *)
-  (*     eexists. split. *)
-  (*     eapply Smallstep.plus_one. *)
-  (*     eapply HTL.step_module; eauto. *)
-  (*     apply assumption_32bit. *)
-  (*     econstructor. econstructor. econstructor. *)
-  (*     eapply Verilog.stmnt_runp_Vnonblock_arr. crush. *)
-  (*     econstructor. econstructor. econstructor. econstructor. *)
-
-  (*     all: crush. *)
-
-  (*     (** State Lookup *) *)
-  (*     unfold Verilog.merge_regs. *)
-  (*     crush. *)
-  (*     unfold_merge. *)
-  (*     apply AssocMap.gss. *)
-
-  (*     (** Match states *) *)
-  (*     rewrite assumption_32bit. *)
-  (*     econstructor; eauto. *)
-
-  (*     (** Match assocmaps *) *)
-  (*     unfold Verilog.merge_regs. crush. unfold_merge. *)
-  (*     apply regs_lessdef_add_greater. *)
-  (*     unfold Plt; lia. *)
-  (*     assumption. *)
-
-  (*     (** States well formed *) *)
-  (*     unfold state_st_wf. inversion 1. crush. *)
-  (*     unfold Verilog.merge_regs. *)
-  (*     unfold_merge. *)
-  (*     apply AssocMap.gss. *)
-
-  (*     (** Equality proof *) *)
-  (*     assert (Z.to_nat *)
-  (*               (Integers.Ptrofs.unsigned *)
-  (*                  (Integers.Ptrofs.divu *)
-  (*                     OFFSET *)
-  (*                     (Integers.Ptrofs.repr 4))) *)
-  (*             = *)
-  (*             valueToNat (ZToValue 32 (Integers.Ptrofs.unsigned OFFSET / 4))) *)
-  (*       as EXPR_OK by admit. *)
-
-  (*     assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. *)
-  (*     inversion MASSOC; revert HeqOFFSET; subst; clear MASSOC; intros HeqOFFSET. *)
-
-  (*     econstructor. *)
-  (*     repeat split; crush. *)
-  (*     unfold HTL.empty_stack. *)
-  (*     crush. *)
-  (*     unfold Verilog.merge_arrs. *)
-
-  (*     rewrite AssocMap.gcombine. *)
-  (*     2: { reflexivity. } *)
-  (*     unfold Verilog.arr_assocmap_set. *)
-  (*     rewrite AssocMap.gss. *)
-  (*     unfold Verilog.merge_arr. *)
-  (*     rewrite AssocMap.gss. *)
-  (*     setoid_rewrite H5. *)
-  (*     reflexivity. *)
-
-  (*     rewrite combine_length. *)
-  (*     rewrite <- array_set_len. *)
-  (*     unfold arr_repeat. crush. *)
-  (*     apply list_repeat_len. *)
-
-  (*     rewrite <- array_set_len. *)
-  (*     unfold arr_repeat. crush. *)
-  (*     rewrite list_repeat_len. *)
-  (*     rewrite H4. reflexivity. *)
-
-  (*     remember i0 as OFFSET. *)
-  (*     destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET). *)
-
-  (*     erewrite Mem.load_store_same. *)
-  (*     2: { rewrite ZERO. *)
-  (*          rewrite Integers.Ptrofs.add_zero_l. *)
-  (*          rewrite e. *)
-  (*          rewrite Integers.Ptrofs.unsigned_repr. *)
-  (*          exact H1. *)
-  (*          apply Integers.Ptrofs.unsigned_range_2. } *)
-  (*     constructor. *)
-  (*     erewrite combine_lookup_second. *)
-  (*     simpl. *)
-  (*     assert (Ple src (RTL.max_reg_function f)) *)
-  (*       by (eapply RTL.max_reg_function_use; eauto; simpl; auto); *)
-  (*     apply H0 in H8. *)
-  (*     destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; invert H8; eauto. *)
-
-  (*     rewrite <- array_set_len. *)
-  (*     unfold arr_repeat. crush. *)
-  (*     rewrite list_repeat_len. auto. *)
-
-  (*     assert (4 * ptr / 4 = Integers.Ptrofs.unsigned OFFSET / 4) by (f_equal; assumption). *)
-  (*     rewrite Z.mul_comm in H8. *)
-  (*     rewrite Z_div_mult in H8; try lia. *)
-  (*     replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) in H8 by reflexivity. *)
-  (*     rewrite <- PtrofsExtra.divu_unsigned in H8; unfold_constants; try lia. *)
-  (*     rewrite H8. rewrite EXPR_OK. *)
-  (*     rewrite array_get_error_set_bound. *)
-  (*     reflexivity. *)
-  (*     unfold arr_length, arr_repeat. simpl. *)
-  (*     rewrite list_repeat_len. lia. *)
-
-  (*     erewrite Mem.load_store_other with (m1 := m). *)
-  (*     2: { exact H1. } *)
-  (*     2: { right. *)
-  (*          rewrite ZERO. *)
-  (*          rewrite Integers.Ptrofs.add_zero_l. *)
-  (*          rewrite Integers.Ptrofs.unsigned_repr. *)
-  (*          simpl. *)
-  (*          destruct (Z_le_gt_dec (4 * ptr + 4) (Integers.Ptrofs.unsigned OFFSET)); eauto. *)
-  (*          right. *)
-  (*          apply ZExtra.mod_0_bounds; try lia. *)
-  (*          apply ZLib.Z_mod_mult'. *)
-  (*          rewrite Z2Nat.id in H11; try lia. *)
-  (*          apply Zmult_lt_compat_r with (p := 4) in H11; try lia. *)
-  (*          rewrite ZLib.div_mul_undo in H11; try lia. *)
-  (*          split; try lia. *)
-  (*          apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia. *)
-  (*     } *)
-
-  (*     rewrite <- EXPR_OK. *)
-  (*     rewrite PtrofsExtra.divu_unsigned; auto; try (unfold_constants; lia). *)
-  (*     destruct (ptr ==Z Integers.Ptrofs.unsigned OFFSET / 4). *)
-  (*     apply Z.mul_cancel_r with (p := 4) in e; try lia. *)
-  (*     rewrite ZLib.div_mul_undo in e; try lia. *)
-  (*     rewrite combine_lookup_first. *)
-  (*     eapply H7; eauto. *)
-
-  (*     rewrite <- array_set_len. *)
-  (*     unfold arr_repeat. crush. *)
-  (*     rewrite list_repeat_len. auto. *)
-  (*     rewrite array_gso. *)
-  (*     unfold array_get_error. *)
-  (*     unfold arr_repeat. *)
-  (*     crush. *)
-  (*     apply list_repeat_lookup. *)
-  (*     lia. *)
-  (*     unfold_constants. *)
-  (*     intro. *)
-  (*     apply Z2Nat.inj_iff in H8; try lia. *)
-  (*     apply Z.div_pos; try lia. *)
-  (*     apply Integers.Ptrofs.unsigned_range. *)
-
-  (*     assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. *)
-  (*     unfold arr_stack_based_pointers. *)
-  (*     intros. *)
-  (*     destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET). *)
-
-  (*     crush. *)
-  (*     erewrite Mem.load_store_same. *)
-  (*     2: { rewrite ZERO. *)
-  (*          rewrite Integers.Ptrofs.add_zero_l. *)
-  (*          rewrite e. *)
-  (*          rewrite Integers.Ptrofs.unsigned_repr. *)
-  (*          exact H1. *)
-  (*          apply Integers.Ptrofs.unsigned_range_2. } *)
-  (*     crush. *)
-  (*     destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; try constructor. *)
-  (*     destruct (Archi.ptr64); try discriminate. *)
-  (*     pose proof (RSBP src). rewrite EQ_SRC in H0. *)
-  (*     assumption. *)
-
-  (*     simpl. *)
-  (*     erewrite Mem.load_store_other with (m1 := m). *)
-  (*     2: { exact H1. } *)
-  (*     2: { right. *)
-  (*          rewrite ZERO. *)
-  (*          rewrite Integers.Ptrofs.add_zero_l. *)
-  (*          rewrite Integers.Ptrofs.unsigned_repr. *)
-  (*          simpl. *)
-  (*          destruct (Z_le_gt_dec (4 * ptr + 4) (Integers.Ptrofs.unsigned OFFSET)); eauto. *)
-  (*          right. *)
-  (*          apply ZExtra.mod_0_bounds; try lia. *)
-  (*          apply ZLib.Z_mod_mult'. *)
-  (*          invert H0. *)
-  (*          apply Zmult_lt_compat_r with (p := 4) in H9; try lia. *)
-  (*          rewrite ZLib.div_mul_undo in H9; try lia. *)
-  (*          split; try lia. *)
-  (*          apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia. *)
-  (*     } *)
-  (*     apply ASBP; assumption. *)
-
-  (*     unfold stack_bounds in *. intros. *)
-  (*     simpl. *)
-  (*     assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. *)
-  (*     erewrite Mem.load_store_other with (m1 := m). *)
-  (*     2: { exact H1. } *)
-  (*     2: { right. right. simpl. *)
-  (*          rewrite ZERO. *)
-  (*          rewrite Integers.Ptrofs.add_zero_l. *)
-  (*          rewrite Integers.Ptrofs.unsigned_repr; crush; try lia. *)
-  (*          apply ZExtra.mod_0_bounds; crush; try lia. } *)
-  (*     crush. *)
-  (*     exploit (BOUNDS ptr); try lia. intros. crush. *)
-  (*     exploit (BOUNDS ptr v); try lia. intros. *)
-  (*     invert H0. *)
-  (*     match goal with | |- ?x = _ => destruct x eqn:EQ end; try reflexivity. *)
-  (*     assert (Mem.valid_access m AST.Mint32 sp' *)
-  (*                              (Integers.Ptrofs.unsigned *)
-  (*                                 (Integers.Ptrofs.add (Integers.Ptrofs.repr 0) *)
-  (*                                                      (Integers.Ptrofs.repr ptr))) Writable). *)
-  (*     { pose proof H1. eapply Mem.store_valid_access_2 in H0. *)
-  (*       exact H0. eapply Mem.store_valid_access_3. eassumption. } *)
-  (*     pose proof (Mem.valid_access_store m AST.Mint32 sp' *)
-  (*                                        (Integers.Ptrofs.unsigned *)
-  (*                                           (Integers.Ptrofs.add (Integers.Ptrofs.repr 0) *)
-  (*                                                                (Integers.Ptrofs.repr ptr))) v). *)
-  (*     apply X in H0. invert H0. congruence. *)
-  (* Admitted. *)
-  (* Hint Resolve transl_istore_correct : htlproof. *)
-
-  (* Lemma transl_icond_correct: *)
-  (*   forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive) *)
-  (*     (rs : Registers.Regmap.t Values.val) (m : mem) (cond : Op.condition) (args : list Registers.reg) *)
-  (*     (ifso ifnot : RTL.node) (b : bool) (pc' : RTL.node), *)
-  (*     (RTL.fn_code f) ! pc = Some (RTL.Icond cond args ifso ifnot) -> *)
-  (*     Op.eval_condition cond (map (fun r : positive => Registers.Regmap.get r rs) args) m = Some b -> *)
-  (*     pc' = (if b then ifso else ifnot) -> *)
-  (*     forall R1 : HTL.state, *)
-  (*       match_states (RTL.State s f sp pc rs m) R1 -> *)
-  (*       exists R2 : HTL.state, *)
-  (*         Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ match_states (RTL.State s f sp pc' rs m) R2. *)
-  (* Proof. *)
-  (*   intros s f sp pc rs m cond args ifso ifnot b pc' H H0 H1 R1 MSTATE. *)
-  (*   inv_state. *)
-
-  (*   eexists. split. apply Smallstep.plus_one. *)
-  (*   eapply HTL.step_module; eauto. *)
-  (*   apply assumption_32bit. *)
-  (*   eapply Verilog.stmnt_runp_Vnonblock_reg with *)
-  (*       (rhsval := if b then posToValue 32 ifso else posToValue 32 ifnot). *)
-  (*   constructor. *)
-
-  (*   simpl. *)
-  (*   destruct b. *)
-  (*   eapply Verilog.erun_Vternary_true. *)
-  (*   eapply eval_cond_correct; eauto. *)
-  (*   constructor. *)
-  (*   apply boolToValue_ValueToBool. *)
-  (*   eapply Verilog.erun_Vternary_false. *)
-  (*   eapply eval_cond_correct; eauto. *)
-  (*   constructor. *)
-  (*   apply boolToValue_ValueToBool. *)
-  (*   constructor. *)
-
-  (*   big_tac. *)
-
-  (*   invert MARR. *)
-  (*   destruct b; rewrite assumption_32bit; big_tac. *)
-
-  (*   Unshelve. *)
-  (*   constructor. *)
-  (* Qed. *)
-  (* Hint Resolve transl_icond_correct : htlproof. *)
-
-  (* Lemma transl_ijumptable_correct: *)
-  (*   forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive) *)
-  (*     (rs : Registers.Regmap.t Values.val) (m : mem) (arg : Registers.reg) (tbl : list RTL.node) *)
-  (*     (n : Integers.Int.int) (pc' : RTL.node), *)
-  (*     (RTL.fn_code f) ! pc = Some (RTL.Ijumptable arg tbl) -> *)
-  (*     Registers.Regmap.get arg rs = Values.Vint n -> *)
-  (*     list_nth_z tbl (Integers.Int.unsigned n) = Some pc' -> *)
-  (*     forall R1 : HTL.state, *)
-  (*       match_states (RTL.State s f sp pc rs m) R1 -> *)
-  (*       exists R2 : HTL.state, *)
-  (*         Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ match_states (RTL.State s f sp pc' rs m) R2. *)
-  (* Proof. *)
-  (*   intros s f sp pc rs m arg tbl n pc' H H0 H1 R1 MSTATE. *)
-  (* Admitted. *)
-  (* Hint Resolve transl_ijumptable_correct : htlproof. *)
-
-  (* Lemma transl_ireturn_correct: *)
-  (*   forall (s : list RTL.stackframe) (f : RTL.function) (stk : Values.block) *)
-  (*     (pc : positive) (rs : RTL.regset) (m : mem) (or : option Registers.reg) *)
-  (*     (m' : mem), *)
-  (*     (RTL.fn_code f) ! pc = Some (RTL.Ireturn or) -> *)
-  (*     Mem.free m stk 0 (RTL.fn_stacksize f) = Some m' -> *)
-  (*     forall R1 : HTL.state, *)
-  (*       match_states (RTL.State s f (Values.Vptr stk Integers.Ptrofs.zero) pc rs m) R1 -> *)
-  (*       exists R2 : HTL.state, *)
-  (*         Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ *)
-  (*         match_states (RTL.Returnstate s (Registers.regmap_optget or Values.Vundef rs) m') R2. *)
-  (* Proof. *)
-  (*   intros s f stk pc rs m or m' H H0 R1 MSTATE. *)
-  (*   inv_state. *)
-
-  (*   - econstructor. split. *)
-  (*     eapply Smallstep.plus_two. *)
-
-  (*     eapply HTL.step_module; eauto. *)
-  (*     apply assumption_32bit. *)
-  (*     constructor. *)
-  (*     econstructor; simpl; trivial. *)
-  (*     econstructor; simpl; trivial. *)
-  (*     constructor. *)
-  (*     econstructor; simpl; trivial. *)
-  (*     constructor. *)
-
-  (*     constructor. constructor. *)
-
-  (*     unfold state_st_wf in WF; big_tac; eauto. *)
-
-  (*     apply HTL.step_finish. *)
-  (*     unfold Verilog.merge_regs. *)
-  (*     unfold_merge; simpl. *)
-  (*     rewrite AssocMap.gso. *)
-  (*     apply AssocMap.gss. lia. *)
-  (*     apply AssocMap.gss. *)
-  (*     rewrite Events.E0_left. reflexivity. *)
-
-  (*     constructor; auto. *)
-  (*     constructor. *)
-
-  (*   (* FIXME: Duplication *) *)
-  (*   - econstructor. split. *)
-  (*     eapply Smallstep.plus_two. *)
-  (*     eapply HTL.step_module; eauto. *)
-  (*     apply assumption_32bit. *)
-  (*     constructor. *)
-  (*     econstructor; simpl; trivial. *)
-  (*     econstructor; simpl; trivial. *)
-  (*     constructor. constructor. constructor. *)
-  (*     constructor. constructor. constructor. *)
-
-  (*     unfold state_st_wf in WF; big_tac; eauto. *)
-
-  (*     apply HTL.step_finish. *)
-  (*     unfold Verilog.merge_regs. *)
-  (*     unfold_merge. *)
-  (*     rewrite AssocMap.gso. *)
-  (*     apply AssocMap.gss. simpl; lia. *)
-  (*     apply AssocMap.gss. *)
-  (*     rewrite Events.E0_left. trivial. *)
-
-  (*     constructor; auto. *)
-
-  (*     simpl. inversion MASSOC. subst. *)
-  (*     unfold find_assocmap, AssocMapExt.get_default. rewrite AssocMap.gso. *)
-  (*     apply H1. eapply RTL.max_reg_function_use. eauto. simpl; tauto. *)
-  (*     assert (HPle : Ple r (RTL.max_reg_function f)). *)
-  (*     eapply RTL.max_reg_function_use. eassumption. simpl; auto. *)
-  (*     apply ZExtra.Ple_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. *)
-
-  (*     Unshelve. *)
-  (*     all: constructor. *)
-  (* Qed. *)
-  (* Hint Resolve transl_ireturn_correct : htlproof. *)
-
-  (* Lemma transl_callstate_correct: *)
-  (*   forall (s : list RTL.stackframe) (f : RTL.function) (args : list Values.val) *)
-  (*     (m : mem) (m' : Mem.mem') (stk : Values.block), *)
-  (*     Mem.alloc m 0 (RTL.fn_stacksize f) = (m', stk) -> *)
-  (*     forall R1 : HTL.state, *)
-  (*       match_states (RTL.Callstate s (AST.Internal f) args m) R1 -> *)
-  (*       exists R2 : HTL.state, *)
-  (*         Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ *)
-  (*         match_states *)
-  (*           (RTL.State s f (Values.Vptr stk Integers.Ptrofs.zero) (RTL.fn_entrypoint f) *)
-  (*                      (RTL.init_regs args (RTL.fn_params f)) m') R2. *)
-  (* Proof. *)
-  (*   intros s f args m m' stk H R1 MSTATE. *)
-
-  (*   inversion MSTATE; subst. inversion TF; subst. *)
-  (*   econstructor. split. apply Smallstep.plus_one. *)
-  (*   eapply HTL.step_call. crush. *)
-
-  (*   apply match_state with (sp' := stk); eauto. *)
-
-  (*   all: big_tac. *)
-
-  (*   apply regs_lessdef_add_greater. *)
-  (*   unfold Plt; lia. *)
-  (*   apply init_reg_assoc_empty. *)
-
-  (*   constructor. *)
-
-  (*   destruct (Mem.load AST.Mint32 m' stk *)
-  (*                      (Integers.Ptrofs.unsigned (Integers.Ptrofs.add *)
-  (*                                                   Integers.Ptrofs.zero *)
-  (*                                                   (Integers.Ptrofs.repr (4 * ptr))))) eqn:LOAD. *)
-  (*   pose proof Mem.load_alloc_same as LOAD_ALLOC. *)
-  (*   pose proof H as ALLOC. *)
-  (*   eapply LOAD_ALLOC in ALLOC. *)
-  (*   2: { exact LOAD. } *)
-  (*   ptrofs. rewrite LOAD. *)
-  (*   rewrite ALLOC. *)
-  (*   repeat constructor. *)
-
-  (*   ptrofs. rewrite LOAD. *)
-  (*   repeat constructor. *)
-
-  (*   unfold reg_stack_based_pointers. intros. *)
-  (*   unfold RTL.init_regs; crush. *)
-  (*   destruct (RTL.fn_params f); *)
-  (*   rewrite Registers.Regmap.gi; constructor. *)
-
-  (*   unfold arr_stack_based_pointers. intros. *)
-  (*   crush. *)
-  (*   destruct (Mem.load AST.Mint32 m' stk *)
-  (*                      (Integers.Ptrofs.unsigned (Integers.Ptrofs.add *)
-  (*                                                   Integers.Ptrofs.zero *)
-  (*                                                   (Integers.Ptrofs.repr (4 * ptr))))) eqn:LOAD. *)
-  (*   pose proof Mem.load_alloc_same as LOAD_ALLOC. *)
-  (*   pose proof H as ALLOC. *)
-  (*   eapply LOAD_ALLOC in ALLOC. *)
-  (*   2: { exact LOAD. } *)
-  (*   rewrite ALLOC. *)
-  (*   repeat constructor. *)
-  (*   constructor. *)
-
-  (*   Transparent Mem.alloc. (* TODO: Since there are opaque there's probably a lemma. *) *)
-  (*   Transparent Mem.load. *)
-  (*   Transparent Mem.store. *)
-  (*   unfold stack_bounds. *)
-  (*   split. *)
-
-  (*   unfold Mem.alloc in H. *)
-  (*   invert H. *)
-  (*   crush. *)
-  (*   unfold Mem.load. *)
-  (*   intros. *)
-  (*   match goal with | |- context[if ?x then _ else _] => destruct x end; try congruence. *)
-  (*   invert v0. unfold Mem.range_perm in H4. *)
-  (*   unfold Mem.perm in H4. crush. *)
-  (*   unfold Mem.perm_order' in H4. *)
-  (*   small_tac. *)
-  (*   exploit (H4 ptr). rewrite Integers.Ptrofs.unsigned_repr; small_tac. intros. *)
-  (*   rewrite Maps.PMap.gss in H8. *)
-  (*   match goal with | H8 : context[if ?x then _ else _] |- _ => destruct x eqn:EQ end; try contradiction. *)
-  (*   crush. *)
-  (*   apply proj_sumbool_true in H10. lia. *)
-
-  (*   unfold Mem.alloc in H. *)
-  (*   invert H. *)
-  (*   crush. *)
-  (*   unfold Mem.store. *)
-  (*   intros. *)
-  (*   match goal with | |- context[if ?x then _ else _] => destruct x end; try congruence. *)
-  (*   invert v0. unfold Mem.range_perm in H4. *)
-  (*   unfold Mem.perm in H4. crush. *)
-  (*   unfold Mem.perm_order' in H4. *)
-  (*   small_tac. *)
-  (*   exploit (H4 ptr). rewrite Integers.Ptrofs.unsigned_repr; small_tac. intros. *)
-  (*   rewrite Maps.PMap.gss in H8. *)
-  (*   match goal with | H8 : context[if ?x then _ else _] |- _ => destruct x eqn:EQ end; try contradiction. *)
-  (*   crush. *)
-  (*   apply proj_sumbool_true in H10. lia. *)
-  (*   Opaque Mem.alloc. *)
-  (*   Opaque Mem.load. *)
-  (*   Opaque Mem.store. *)
-  (* Qed. *)
-  (* Hint Resolve transl_callstate_correct : htlproof. *)
-
-  (* Lemma transl_returnstate_correct: *)
-  (*   forall (res0 : Registers.reg) (f : RTL.function) (sp : Values.val) (pc : RTL.node) *)
-  (*     (rs : RTL.regset) (s : list RTL.stackframe) (vres : Values.val) (m : mem) *)
-  (*     (R1 : HTL.state), *)
-  (*     match_states (RTL.Returnstate (RTL.Stackframe res0 f sp pc rs :: s) vres m) R1 -> *)
-  (*     exists R2 : HTL.state, *)
-  (*       Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ *)
-  (*       match_states (RTL.State s f sp pc (Registers.Regmap.set res0 vres rs) m) R2. *)
-  (* Proof. *)
-  (*   intros res0 f sp pc rs s vres m R1 MSTATE. *)
-  (*   inversion MSTATE. inversion MF. *)
-  (* Qed. *)
-  (* Hint Resolve transl_returnstate_correct : htlproof. *)
-
-  (* Lemma option_inv : *)
-  (*   forall A x y, *)
-  (*     @Some A x = Some y -> x = y. *)
-  (* Proof. intros. inversion H. trivial. Qed. *)
-
-  (* Lemma main_tprog_internal : *)
-  (*   forall b, *)
-  (*     Globalenvs.Genv.find_symbol tge tprog.(AST.prog_main) = Some b -> *)
-  (*     exists f, Genv.find_funct_ptr (Genv.globalenv tprog) b = Some (AST.Internal f). *)
-  (* Proof. *)
-  (*   intros. *)
-  (*   destruct TRANSL. unfold main_is_internal in H1. *)
-  (*   repeat (unfold_match H1). replace b with b0. *)
-  (*   exploit function_ptr_translated; eauto. intros [tf [A B]]. *)
-  (*   unfold transl_fundef, AST.transf_partial_fundef, Errors.bind in B. *)
-  (*   unfold_match B. inv B. econstructor. apply A. *)
-
-  (*   apply option_inv. rewrite <- Heqo. rewrite <- H. *)
-  (*   rewrite symbols_preserved. replace (AST.prog_main tprog) with (AST.prog_main prog). *)
-  (*   trivial. symmetry; eapply Linking.match_program_main; eauto. *)
-  (* Qed. *)
-
-  (* Lemma transl_initial_states : *)
-  (*   forall s1 : Smallstep.state (RTL.semantics prog), *)
-  (*     Smallstep.initial_state (RTL.semantics prog) s1 -> *)
-  (*     exists s2 : Smallstep.state (HTL.semantics tprog), *)
-  (*       Smallstep.initial_state (HTL.semantics tprog) s2 /\ match_states s1 s2. *)
-  (* Proof. *)
-  (*   induction 1. *)
-  (*   destruct TRANSL. unfold main_is_internal in H4. *)
-  (*   repeat (unfold_match H4). *)
-  (*   assert (f = AST.Internal f1). apply option_inv. *)
-  (*   rewrite <- Heqo0. rewrite <- H1. replace b with b0. *)
-  (*   auto. apply option_inv. rewrite <- H0. rewrite <- Heqo. *)
-  (*   trivial. *)
-  (*   exploit function_ptr_translated; eauto. *)
-  (*   intros [tf [A B]]. *)
-  (*   unfold transl_fundef, Errors.bind in B. *)
-  (*   unfold AST.transf_partial_fundef, Errors.bind in B. *)
-  (*   repeat (unfold_match B). inversion B. subst. *)
-  (*   exploit main_tprog_internal; eauto; intros. *)
-  (*   rewrite symbols_preserved. replace (AST.prog_main tprog) with (AST.prog_main prog). *)
-  (*   apply Heqo. symmetry; eapply Linking.match_program_main; eauto. *)
-  (*   inversion H5. *)
-  (*   econstructor; split. econstructor. *)
-  (*   apply (Genv.init_mem_transf_partial TRANSL'); eauto. *)
-  (*   replace (AST.prog_main tprog) with (AST.prog_main prog). *)
-  (*   rewrite symbols_preserved; eauto. *)
-  (*   symmetry; eapply Linking.match_program_main; eauto. *)
-  (*   apply H6. *)
-
-  (*   constructor. *)
-  (*   apply transl_module_correct. *)
-  (*   assert (Some (AST.Internal x) = Some (AST.Internal m)). *)
-  (*   replace (AST.fundef HTL.module) with (HTL.fundef). *)
-  (*   rewrite <- H6. setoid_rewrite <- A. trivial. *)
-  (*   trivial. inv H7. assumption. *)
-  (* Qed. *)
-  (* Hint Resolve transl_initial_states : htlproof. *)
-
-  (* Lemma transl_final_states : *)
-  (*   forall (s1 : Smallstep.state (RTL.semantics prog)) *)
-  (*          (s2 : Smallstep.state (HTL.semantics tprog)) *)
-  (*          (r : Integers.Int.int), *)
-  (*     match_states s1 s2 -> *)
-  (*     Smallstep.final_state (RTL.semantics prog) s1 r -> *)
-  (*     Smallstep.final_state (HTL.semantics tprog) s2 r. *)
-  (* Proof. *)
-  (*   intros. inv H0. inv H. inv H4. invert MF. constructor. reflexivity. *)
-  (* Qed. *)
-  (* Hint Resolve transl_final_states : htlproof. *)
-
-  (* Theorem transl_step_correct: *)
-  (*   forall (S1 : RTL.state) t S2, *)
-  (*     RTL.step ge S1 t S2 -> *)
-  (*     forall (R1 : HTL.state), *)
-  (*       match_states S1 R1 -> *)
-  (*       exists R2, Smallstep.plus HTL.step tge R1 t R2 /\ match_states S2 R2. *)
-  (* Proof. *)
-  (*   induction 1; eauto with htlproof; (intros; inv_state). *)
-  (* Qed. *)
-  (* Hint Resolve transl_step_correct : htlproof. *)
-
-(*   Theorem transf_program_correct: *)
-(*     Smallstep.forward_simulation (RTL.semantics prog) (HTL.semantics tprog). *)
-(*   Proof. *)
-(*   Admitted. *)
-(*   (*   eapply Smallstep.forward_simulation_plus; eauto with htlproof. *) *)
-(*   (*   apply senv_preserved. *) *)
-(*   (* Qed. *) *)
-
-(* End CORRECTNESS. *)
+Inductive match_assocmaps : RTL.function -> RTL.regset -> assocmap -> Prop :=
+  match_assocmap : forall f rs am,
+    (forall r, Ple r (RTL.max_reg_function f) ->
+               val_value_lessdef (Registers.Regmap.get r rs) am#r) ->
+    match_assocmaps f rs am.
+Hint Constructors match_assocmaps : htlproof.
+
+Definition state_st_wf (m : HTL.module) (s : HTL.state) :=
+  forall st asa asr res,
+  s = HTL.State res m st asa asr ->
+  asa!(m.(HTL.mod_st)) = Some (posToValue st).
+Hint Unfold state_st_wf : htlproof.
+
+Inductive match_arrs (m : HTL.module) (f : RTL.function) (sp : Values.val) (mem : mem) :
+  Verilog.assocmap_arr -> Prop :=
+| match_arr : forall asa stack,
+    asa ! (m.(HTL.mod_stk)) = Some stack /\
+    stack.(arr_length) = Z.to_nat (f.(RTL.fn_stacksize) / 4) /\
+    (forall ptr,
+        0 <= ptr < Z.of_nat m.(HTL.mod_stk_len) ->
+        opt_val_value_lessdef (Mem.loadv AST.Mint32 mem
+                                         (Values.Val.offset_ptr sp (Integers.Ptrofs.repr (4 * ptr))))
+                              (Option.default (NToValue 0)
+                                 (Option.join (array_get_error (Z.to_nat ptr) stack)))) ->
+    match_arrs m f sp mem asa.
+
+Definition stack_based (v : Values.val) (sp : Values.block) : Prop :=
+   match v with
+   | Values.Vptr sp' off => sp' = sp
+   | _ => True
+   end.
+
+Definition reg_stack_based_pointers (sp : Values.block) (rs : Registers.Regmap.t Values.val) : Prop :=
+  forall r, stack_based (Registers.Regmap.get r rs) sp.
+
+Definition arr_stack_based_pointers (spb : Values.block) (m : mem) (stack_length : Z)
+  (sp : Values.val) : Prop :=
+  forall ptr,
+    0 <= ptr < (stack_length / 4) ->
+    stack_based (Option.default
+                   Values.Vundef
+                   (Mem.loadv AST.Mint32 m
+                              (Values.Val.offset_ptr sp (Integers.Ptrofs.repr (4 * ptr)))))
+                spb.
+
+Definition stack_bounds (sp : Values.val) (hi : Z) (m : mem) : Prop :=
+  forall ptr v,
+    hi <= ptr <= Integers.Ptrofs.max_unsigned ->
+    Z.modulo ptr 4 = 0 ->
+    Mem.loadv AST.Mint32 m (Values.Val.offset_ptr sp (Integers.Ptrofs.repr ptr )) = None /\
+    Mem.storev AST.Mint32 m (Values.Val.offset_ptr sp (Integers.Ptrofs.repr ptr )) v = None.
+
+Inductive match_frames : list RTL.stackframe -> list HTL.stackframe -> Prop :=
+| match_frames_nil :
+    match_frames nil nil.
+
+Inductive match_constants : HTL.module -> assocmap -> Prop :=
+  match_constant :
+    forall m asr,
+      asr!(HTL.mod_reset m) = Some (ZToValue 0) ->
+      asr!(HTL.mod_finish m) = Some (ZToValue 0) ->
+      match_constants m asr.
+
+Inductive match_states : RTL.state -> HTL.state -> Prop :=
+| match_state : forall asa asr sf f sp sp' rs mem m st res
+    (MASSOC : match_assocmaps f rs asr)
+    (TF : tr_module f m)
+    (WF : state_st_wf m (HTL.State res m st asr asa))
+    (MF : match_frames sf res)
+    (MARR : match_arrs m f sp mem asa)
+    (SP : sp = Values.Vptr sp' (Integers.Ptrofs.repr 0))
+    (RSBP : reg_stack_based_pointers sp' rs)
+    (ASBP : arr_stack_based_pointers sp' mem (f.(RTL.fn_stacksize)) sp)
+    (BOUNDS : stack_bounds sp (f.(RTL.fn_stacksize)) mem)
+    (CONST : match_constants m asr),
+    match_states (RTL.State sf f sp st rs mem)
+                 (HTL.State res m st asr asa)
+| match_returnstate :
+    forall
+      v v' stack mem res
+      (MF : match_frames stack res),
+      val_value_lessdef v v' ->
+      match_states (RTL.Returnstate stack v mem) (HTL.Returnstate res v')
+| match_initial_call :
+    forall f m m0
+    (TF : tr_module f m),
+      match_states (RTL.Callstate nil (AST.Internal f) nil m0) (HTL.Callstate nil m nil).
+Hint Constructors match_states : htlproof.
+
+Definition match_prog (p: RTL.program) (tp: HTL.program) :=
+  Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq p tp /\
+  main_is_internal p = true.
+
+Definition match_prog_matches :
+  forall p tp,
+    match_prog p tp ->
+    Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq p tp.
+  Proof. intros. unfold match_prog in H. tauto. Qed.
+
+Lemma transf_program_match:
+  forall p tp, HTLgen.transl_program p = Errors.OK tp -> match_prog p tp.
+Proof.
+  intros. unfold transl_program in H.
+  destruct (main_is_internal p) eqn:?; try discriminate.
+  unfold match_prog. split.
+  apply Linking.match_transform_partial_program; auto.
+  assumption.
+Qed.
+
+Lemma regs_lessdef_add_greater :
+  forall f rs1 rs2 n v,
+    Plt (RTL.max_reg_function f) n ->
+    match_assocmaps f rs1 rs2 ->
+    match_assocmaps f rs1 (AssocMap.set n v rs2).
+Proof.
+  inversion 2; subst.
+  intros. constructor.
+  intros. unfold find_assocmap. unfold AssocMapExt.get_default.
+  rewrite AssocMap.gso. eauto.
+  apply Pos.le_lt_trans with _ _ n in H2.
+  unfold not. intros. subst. eapply Pos.lt_irrefl. eassumption. assumption.
+Qed.
+Hint Resolve regs_lessdef_add_greater : htlproof.
+
+Lemma regs_lessdef_add_match :
+  forall f rs am r v v',
+    val_value_lessdef v v' ->
+    match_assocmaps f rs am ->
+    match_assocmaps f (Registers.Regmap.set r v rs) (AssocMap.set r v' am).
+Proof.
+  inversion 2; subst.
+  constructor. intros.
+  destruct (peq r0 r); subst.
+  rewrite Registers.Regmap.gss.
+  unfold find_assocmap. unfold AssocMapExt.get_default.
+  rewrite AssocMap.gss. assumption.
+
+  rewrite Registers.Regmap.gso; try assumption.
+  unfold find_assocmap. unfold AssocMapExt.get_default.
+  rewrite AssocMap.gso; eauto.
+Qed.
+Hint Resolve regs_lessdef_add_match : htlproof.
+
+Lemma list_combine_none :
+  forall n l,
+    length l = n ->
+    list_combine Verilog.merge_cell (list_repeat None n) l = l.
+Proof.
+  induction n; intros; crush.
+  - symmetry. apply length_zero_iff_nil. auto.
+  - destruct l; crush.
+    rewrite list_repeat_cons.
+    crush. f_equal.
+    eauto.
+Qed.
+
+Lemma combine_none :
+  forall n a,
+    a.(arr_length) = n ->
+    arr_contents (combine Verilog.merge_cell (arr_repeat None n) a) = arr_contents a.
+Proof.
+  intros.
+  unfold combine.
+  crush.
+
+  rewrite <- (arr_wf a) in H.
+  apply list_combine_none.
+  assumption.
+Qed.
+
+Lemma list_combine_lookup_first :
+  forall l1 l2 n,
+    length l1 = length l2 ->
+    nth_error l1 n = Some None ->
+    nth_error (list_combine Verilog.merge_cell l1 l2) n = nth_error l2 n.
+Proof.
+  induction l1; intros; crush.
+
+  rewrite nth_error_nil in H0.
+  discriminate.
+
+  destruct l2 eqn:EQl2. crush.
+  simpl in H. invert H.
+  destruct n; simpl in *.
+  invert H0. simpl. reflexivity.
+  eauto.
+Qed.
+
+Lemma combine_lookup_first :
+  forall a1 a2 n,
+    a1.(arr_length) = a2.(arr_length) ->
+    array_get_error n a1 = Some None ->
+    array_get_error n (combine Verilog.merge_cell a1 a2) = array_get_error n a2.
+Proof.
+  intros.
+
+  unfold array_get_error in *.
+  apply list_combine_lookup_first; eauto.
+  rewrite a1.(arr_wf). rewrite a2.(arr_wf).
+  assumption.
+Qed.
+
+Lemma list_combine_lookup_second :
+  forall l1 l2 n x,
+    length l1 = length l2 ->
+    nth_error l1 n = Some (Some x) ->
+    nth_error (list_combine Verilog.merge_cell l1 l2) n = Some (Some x).
+Proof.
+  induction l1; intros; crush; auto.
+
+  destruct l2 eqn:EQl2. crush.
+  simpl in H. invert H.
+  destruct n; simpl in *.
+  invert H0. simpl. reflexivity.
+  eauto.
+Qed.
+
+Lemma combine_lookup_second :
+  forall a1 a2 n x,
+    a1.(arr_length) = a2.(arr_length) ->
+    array_get_error n a1 = Some (Some x) ->
+    array_get_error n (combine Verilog.merge_cell a1 a2) = Some (Some x).
+Proof.
+  intros.
+
+  unfold array_get_error in *.
+  apply list_combine_lookup_second; eauto.
+  rewrite a1.(arr_wf). rewrite a2.(arr_wf).
+  assumption.
+Qed.
+
+Ltac inv_state :=
+  match goal with
+    MSTATE : match_states _ _ |- _ =>
+    inversion MSTATE;
+    match goal with
+      TF : tr_module _ _ |- _ =>
+      inversion TF;
+      match goal with
+        TC : forall _ _,
+          Maps.PTree.get _ _ = Some _ -> tr_code _ _ _ _ _ _ _ _ _,
+        H : Maps.PTree.get _ _ = Some _ |- _ =>
+        apply TC in H; inversion H;
+        match goal with
+          TI : context[tr_instr] |- _ =>
+          inversion TI
+        end
+      end
+    end
+end; subst.
+
+Ltac unfold_func H :=
+  match type of H with
+  | ?f = _ => unfold f in H; repeat (unfold_match H)
+  | ?f _ = _ => unfold f in H; repeat (unfold_match H)
+  | ?f _ _ = _ => unfold f in H; repeat (unfold_match H)
+  | ?f _ _ _ = _ => unfold f in H; repeat (unfold_match H)
+  | ?f _ _ _ _ = _ => unfold f in H; repeat (unfold_match H)
+  end.
+
+Lemma init_reg_assoc_empty :
+  forall f l,
+    match_assocmaps f (RTL.init_regs nil l) (HTL.init_regs nil l).
+Proof.
+  induction l; simpl; constructor; intros.
+  - rewrite Registers.Regmap.gi. unfold find_assocmap.
+    unfold AssocMapExt.get_default. rewrite AssocMap.gempty.
+    constructor.
+
+  - rewrite Registers.Regmap.gi. unfold find_assocmap.
+    unfold AssocMapExt.get_default. rewrite AssocMap.gempty.
+    constructor.
+Qed.
+
+Lemma arr_lookup_some:
+  forall (z : Z) (r0 : Registers.reg) (r : Verilog.reg) (asr : assocmap) (asa : Verilog.assocmap_arr)
+    (stack : Array (option value)) (H5 : asa ! r = Some stack) n,
+    exists x, Verilog.arr_assocmap_lookup asa r n = Some x.
+Proof.
+  intros z r0 r asr asa stack H5 n.
+  eexists.
+  unfold Verilog.arr_assocmap_lookup. rewrite H5. reflexivity.
+Qed.
+Hint Resolve arr_lookup_some : htlproof.
+
+Section CORRECTNESS.
+
+  Variable prog : RTL.program.
+  Variable tprog : HTL.program.
+
+  Hypothesis TRANSL : match_prog prog tprog.
+
+  Lemma TRANSL' :
+    Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq prog tprog.
+  Proof. intros; apply match_prog_matches; assumption. Qed.
+
+  Let ge : RTL.genv := Globalenvs.Genv.globalenv prog.
+  Let tge : HTL.genv := Globalenvs.Genv.globalenv tprog.
+
+  Lemma symbols_preserved:
+    forall (s: AST.ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
+  Proof. intros. eapply (Genv.find_symbol_match TRANSL'). Qed.
+
+  Lemma function_ptr_translated:
+    forall (b: Values.block) (f: RTL.fundef),
+      Genv.find_funct_ptr ge b = Some f ->
+      exists tf,
+        Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = Errors.OK tf.
+  Proof.
+    intros. exploit (Genv.find_funct_ptr_match TRANSL'); eauto.
+    intros (cu & tf & P & Q & R); exists tf; auto.
+  Qed.
+
+  Lemma functions_translated:
+    forall (v: Values.val) (f: RTL.fundef),
+      Genv.find_funct ge v = Some f ->
+      exists tf,
+        Genv.find_funct tge v = Some tf /\ transl_fundef f = Errors.OK tf.
+  Proof.
+    intros. exploit (Genv.find_funct_match TRANSL'); eauto.
+    intros (cu & tf & P & Q & R); exists tf; auto.
+  Qed.
+
+  Lemma senv_preserved:
+    Senv.equiv (Genv.to_senv ge) (Genv.to_senv tge).
+  Proof
+    (Genv.senv_transf_partial TRANSL').
+  Hint Resolve senv_preserved : htlproof.
+
+  Lemma ptrofs_inj :
+    forall a b,
+      Ptrofs.unsigned a = Ptrofs.unsigned b -> a = b.
+  Proof.
+    intros. rewrite <- Ptrofs.repr_unsigned. symmetry. rewrite <- Ptrofs.repr_unsigned.
+    rewrite H. auto.
+  Qed.
+
+  Lemma eval_correct :
+    forall s sp op rs m v e asr asa f f' stk s' i pc res0 pc' args res ml st,
+      match_states (RTL.State stk f sp pc rs m) (HTL.State res ml st asr asa) ->
+      (RTL.fn_code f) ! pc = Some (RTL.Iop op args res0 pc') ->
+      Op.eval_operation ge sp op
+                        (List.map (fun r : BinNums.positive => Registers.Regmap.get r rs) args) m = Some v ->
+      translate_instr op args s = OK e s' i ->
+      exists v', Verilog.expr_runp f' asr asa e v' /\ val_value_lessdef v v'.
+  Proof.
+    intros s sp op rs m v e asr asa f f' stk s' i pc pc' res0 args res ml st MSTATE INSTR EVAL TR_INSTR.
+    inv MSTATE. inv MASSOC. unfold translate_instr in TR_INSTR; repeat (unfold_match TR_INSTR); inv TR_INSTR;
+    unfold Op.eval_operation in EVAL; repeat (unfold_match EVAL); simplify.
+    - inv Heql.
+      assert (HPle : Ple r (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto).
+      apply H in HPle. eexists. split; try constructor; eauto.
+    - eexists. split. constructor. constructor. auto.
+    - inv Heql.
+      assert (HPle : Ple r (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto).
+      apply H in HPle.
+      eexists. split. econstructor; eauto. constructor. trivial.
+      unfold Verilog.unop_run. unfold Values.Val.neg. destruct (Registers.Regmap.get r rs) eqn:?; constructor.
+      inv HPle. auto.
+    - inv Heql.
+      assert (HPle : Ple r (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto).
+      assert (HPle0 : Ple r0 (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto).
+      apply H in HPle. apply H in HPle0.
+      eexists. split. econstructor; eauto. constructor. trivial.
+      constructor. trivial. simplify. inv HPle. inv HPle0; constructor; auto.
+      + inv HPle0. constructor. unfold valueToPtr. Search Integers.Ptrofs.sub Integers.int.
+        pose proof Integers.Ptrofs.agree32_sub. unfold Integers.Ptrofs.agree32 in H3.
+        Print Integers.Ptrofs.agree32. unfold Ptrofs.of_int. simpl.
+        apply ptrofs_inj. assert (Archi.ptr64 = false) by auto. eapply H3 in H4.
+        rewrite Ptrofs.unsigned_repr. apply H4. replace Ptrofs.max_unsigned with Int.max_unsigned; auto.
+        apply Int.unsigned_range_2.
+        auto. rewrite Ptrofs.unsigned_repr. replace Ptrofs.max_unsigned with Int.max_unsigned; auto.
+        apply Int.unsigned_range_2. rewrite Ptrofs.unsigned_repr. auto.
+        replace Ptrofs.max_unsigned with Int.max_unsigned; auto.
+        apply Int.unsigned_range_2.
+        Admitted.
+
+  Lemma eval_cond_correct :
+    forall cond (args : list Registers.reg) s1 c s' i rs args m b f asr asa,
+      translate_condition cond args s1 = OK c s' i ->
+      Op.eval_condition
+        cond
+        (List.map (fun r : BinNums.positive => Registers.Regmap.get r rs) args)
+        m = Some b ->
+      Verilog.expr_runp f asr asa c (boolToValue b).
+  Admitted.
+
+  (** The proof of semantic preservation for the translation of instructions
+      is a simulation argument based on diagrams of the following form:
+<<
+                      match_states
+    code st rs ---------------- State m st assoc
+         ||                             |
+         ||                             |
+         ||                             |
+         \/                             v
+    code st rs' --------------- State m st assoc'
+                      match_states
+>>
+      where [tr_code c data control fin rtrn st] is assumed to hold.
+
+      The precondition and postcondition is that that should hold is [match_assocmaps rs assoc].
+   *)
+
+  Definition transl_instr_prop (instr : RTL.instruction) : Prop :=
+    forall m asr asa fin rtrn st stmt trans res,
+      tr_instr fin rtrn st (m.(HTL.mod_stk)) instr stmt trans ->
+      exists asr' asa',
+        HTL.step tge (HTL.State res m st asr asa) Events.E0 (HTL.State res m st asr' asa').
+
+  Opaque combine.
+
+  Ltac tac0 :=
+    match goal with
+    | [ |- context[Verilog.merge_arrs _ _] ] => unfold Verilog.merge_arrs
+    | [ |- context[Verilog.merge_arr] ] => unfold Verilog.merge_arr
+    | [ |- context[Verilog.merge_regs _ _] ] => unfold Verilog.merge_regs; crush; unfold_merge
+    | [ |- context[reg_stack_based_pointers] ] => unfold reg_stack_based_pointers; intros
+    | [ |- context[Verilog.arr_assocmap_set _ _ _ _] ] => unfold Verilog.arr_assocmap_set
+
+    | [ |- context[HTL.empty_stack] ] => unfold HTL.empty_stack
+
+    | [ |- context[_ # ?d <- _ ! ?d] ] => rewrite AssocMap.gss
+    | [ |- context[_ # ?d <- _ ! ?s] ] => rewrite AssocMap.gso
+    | [ |- context[(AssocMap.empty _) ! _] ] => rewrite AssocMap.gempty
+
+    | [ |- context[array_get_error _ (combine Verilog.merge_cell (arr_repeat None _) _)] ] =>
+      rewrite combine_lookup_first
+
+    | [ |- state_st_wf _ _ ] => unfold state_st_wf; inversion 1
+    | [ |- context[match_states _ _] ] => econstructor; auto
+    | [ |- match_arrs _ _ _ _ _ ] => econstructor; auto
+    | [ |- match_assocmaps _ _ _ # _ <- (posToValue _) ] =>
+      apply regs_lessdef_add_greater; [> unfold Plt; lia | assumption]
+
+    | [ H : ?asa ! ?r = Some _ |- Verilog.arr_assocmap_lookup ?asa ?r _ = Some _ ] =>
+      unfold Verilog.arr_assocmap_lookup; setoid_rewrite H; f_equal
+    | [ |- context[(AssocMap.combine _ _ _) ! _] ] =>
+      try (rewrite AssocMap.gcombine; [> | reflexivity])
+
+    | [ |- context[Registers.Regmap.get ?d (Registers.Regmap.set ?d _ _)] ] =>
+      rewrite Registers.Regmap.gss
+    | [ |- context[Registers.Regmap.get ?s (Registers.Regmap.set ?d _ _)] ] =>
+      destruct (Pos.eq_dec s d) as [EQ|EQ];
+      [> rewrite EQ | rewrite Registers.Regmap.gso; auto]
+
+    | [ H : opt_val_value_lessdef _ _ |- _ ] => invert H
+    | [ H : context[Z.of_nat (Z.to_nat _)] |- _ ] => rewrite Z2Nat.id in H; [> solve crush |]
+    | [ H : _ ! _ = Some _ |- _] => setoid_rewrite H
+    end.
+
+  Ltac small_tac := repeat (crush; try array; try ptrofs); crush; auto.
+  Ltac big_tac := repeat (crush; try array; try ptrofs; try tac0); crush; auto.
+
+  Lemma transl_inop_correct:
+    forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive)
+      (rs : RTL.regset) (m : mem) (pc' : RTL.node),
+      (RTL.fn_code f) ! pc = Some (RTL.Inop pc') ->
+      forall R1 : HTL.state,
+        match_states (RTL.State s f sp pc rs m) R1 ->
+        exists R2 : HTL.state,
+          Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ match_states (RTL.State s f sp pc' rs m) R2.
+  Proof.
+    intros s f sp pc rs m pc' H R1 MSTATE.
+    inv_state.
+
+    unfold match_prog in TRANSL.
+    econstructor.
+    split.
+    apply Smallstep.plus_one.
+    eapply HTL.step_module; eauto.
+    inv CONST; assumption.
+    inv CONST; assumption. 
+    (* processing of state *)
+    econstructor.
+    crush.
+    econstructor.
+    econstructor.
+    econstructor.
+
+    all: invert MARR; big_tac.
+
+    inv CONST; constructor; simplify; rewrite AssocMap.gso; auto; lia.
+
+    Unshelve. auto.
+  Qed.
+  Hint Resolve transl_inop_correct : htlproof.
+
+  Lemma transl_iop_correct:
+    forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive)
+      (rs : Registers.Regmap.t Values.val) (m : mem) (op : Op.operation) (args : list Registers.reg)
+      (res0 : Registers.reg) (pc' : RTL.node) (v : Values.val),
+      (RTL.fn_code f) ! pc = Some (RTL.Iop op args res0 pc') ->
+      Op.eval_operation ge sp op (map (fun r : positive => Registers.Regmap.get r rs) args) m = Some v ->
+      forall R1 : HTL.state,
+        match_states (RTL.State s f sp pc rs m) R1 ->
+        exists R2 : HTL.state,
+          Smallstep.plus HTL.step tge R1 Events.E0 R2 /\
+          match_states (RTL.State s f sp pc' (Registers.Regmap.set res0 v rs) m) R2.
+  Proof.
+    intros s f sp pc rs m op args res0 pc' v H H0 R1 MSTATE.
+    inv_state.
+    exploit eval_correct; eauto. intros. inversion H1. inversion H2.
+    econstructor. split.
+    apply Smallstep.plus_one.
+    eapply HTL.step_module; eauto.
+    inv CONST. assumption.
+    inv CONST. assumption.
+    econstructor; simpl; trivial.
+    constructor; trivial.
+    econstructor; simpl; eauto.
+    simpl. econstructor. econstructor.
+    apply H3. simplify.
+
+    all: big_tac.
+
+    assert (Ple res0 (RTL.max_reg_function f))
+        by (eapply RTL.max_reg_function_def; eauto; simpl; auto).
+
+    unfold Ple in H10. lia.
+    apply regs_lessdef_add_match. assumption.
+    apply regs_lessdef_add_greater. unfold Plt; lia. assumption.
+    assert (Ple res0 (RTL.max_reg_function f))
+        by (eapply RTL.max_reg_function_def; eauto; simpl; auto).
+    unfold Ple in H12; lia.
+    Admitted.
+(*    unfold_merge. simpl.
+    rewrite AssocMap.gso.
+    apply AssocMap.gss.
+    apply st_greater_than_res.
+
+    (*match_states*)
+      assert (pc' = valueToPos (posToValue 32 pc')). auto using assumption_32bit.
+    rewrite <- H1.
+    constructor; auto.
+    unfold_merge.
+    apply regs_lessdef_add_match.
+    constructor.
+    apply regs_lessdef_add_greater.
+    apply greater_than_max_func.
+    assumption.
+
+    unfold state_st_wf. intros. inversion H2. subst.
+    unfold_merge.
+    rewrite AssocMap.gso.
+    apply AssocMap.gss.
+    apply st_greater_than_res.
+
+     + econstructor. split.
+     apply Smallstep.plus_one.
+     eapply HTL.step_module; eauto.
+     econstructor; simpl; trivial.
+     constructor; trivial.
+     econstructor; simpl; eauto.
+     eapply eval_correct; eauto.
+     constructor. rewrite valueToInt_intToValue. trivial.
+     unfold_merge. simpl.
+     rewrite AssocMap.gso.
+     apply AssocMap.gss.
+     apply st_greater_than_res.
+
+      match_states
+     assert (pc' = valueToPos (posToValue 32 pc')). auto using assumption_32bit.
+     rewrite <- H1.
+     constructor.
+     unfold_merge.
+     apply regs_lessdef_add_match.
+     constructor.
+     symmetry. apply valueToInt_intToValue.
+     apply regs_lessdef_add_greater.
+     apply greater_than_max_func.
+     assumption. assumption.
+
+     unfold state_st_wf. intros. inversion H2. subst.
+     unfold_merge.
+     rewrite AssocMap.gso.
+     apply AssocMap.gss.
+     apply st_greater_than_res.
+     assumption.
+  Admitted.*)
+  Hint Resolve transl_iop_correct : htlproof.
+
+  Ltac tac :=
+    repeat match goal with
+           | [ _ : error _ _ = OK _ _ _ |- _ ] => discriminate
+           | [ _ : context[if (?x && ?y) then _ else _] |- _ ] =>
+             let EQ1 := fresh "EQ" in
+             let EQ2 := fresh "EQ" in
+             destruct x eqn:EQ1; destruct y eqn:EQ2; simpl in *
+           | [ _ : context[if ?x then _ else _] |- _ ] =>
+             let EQ := fresh "EQ" in
+             destruct x eqn:EQ; simpl in *
+           | [ H : ret _ _ = _  |- _ ] => invert H
+           | [ _ : context[match ?x with | _ => _ end] |- _ ] => destruct x
+           end.
+
+  Ltac inv_arr_access :=
+    match goal with
+    | [ _ : translate_arr_access ?chunk ?addr ?args _ _ = OK ?c _ _ |- _] =>
+      destruct c, chunk, addr, args; crush; tac; crush
+    end.
+
+  Lemma transl_iload_correct:
+    forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive)
+      (rs : Registers.Regmap.t Values.val) (m : mem) (chunk : AST.memory_chunk)
+      (addr : Op.addressing) (args : list Registers.reg) (dst : Registers.reg)
+      (pc' : RTL.node) (a v : Values.val),
+      (RTL.fn_code f) ! pc = Some (RTL.Iload chunk addr args dst pc') ->
+      Op.eval_addressing ge sp addr (map (fun r : positive => Registers.Regmap.get r rs) args) = Some a ->
+      Mem.loadv chunk m a = Some v ->
+      forall R1 : HTL.state,
+        match_states (RTL.State s f sp pc rs m) R1 ->
+        exists R2 : HTL.state,
+          Smallstep.plus HTL.step tge R1 Events.E0 R2 /\
+          match_states (RTL.State s f sp pc' (Registers.Regmap.set dst v rs) m) R2.
+  Proof.
+    intros s f sp pc rs m chunk addr args dst pc' a v H H0 H1 R1 MSTATE.
+    inv_state. inv_arr_access.
+
+    + (** Preamble *)
+      invert MARR. crush.
+
+      unfold Op.eval_addressing in H0.
+      destruct (Archi.ptr64) eqn:ARCHI; crush.
+
+      unfold reg_stack_based_pointers in RSBP.
+      pose proof (RSBP r0) as RSBPr0.
+
+      destruct (Registers.Regmap.get r0 rs) eqn:EQr0; crush.
+
+      rewrite ARCHI in H1. crush.
+      subst.
+
+      pose proof MASSOC as MASSOC'.
+      invert MASSOC'.
+      pose proof (H0 r0).
+      assert (HPler0 : Ple r0 (RTL.max_reg_function f))
+        by (eapply RTL.max_reg_function_use; eauto; crush; eauto).
+      apply H6 in HPler0.
+      invert HPler0; try congruence.
+      rewrite EQr0 in H8.
+      invert H8.
+      clear H0. clear H6.
+
+      unfold check_address_parameter_signed in *;
+      unfold check_address_parameter_unsigned in *; crush.
+
+      remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ asr # r0))
+                                    (Integers.Ptrofs.of_int (Integers.Int.repr z))) as OFFSET.
+
+      (** Modular preservation proof *)
+      (*assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE.
+      { rewrite HeqOFFSET.
+        apply PtrofsExtra.add_mod; crush.
+        rewrite Integers.Ptrofs.unsigned_repr_eq.
+        rewrite <- Zmod_div_mod; crush.
+        apply PtrofsExtra.of_int_mod.
+        rewrite Integers.Int.unsigned_repr_eq.
+        rewrite <- Zmod_div_mod; crush. }
+
+      (** Read bounds proof *)
+      assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH.
+      { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; crush; auto.
+        unfold stack_bounds in BOUNDS.
+        exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET)); auto.
+        split; try lia; apply Integers.Ptrofs.unsigned_range_2.
+        small_tac. }
+
+      (** Normalisation proof *)
+      assert (Integers.Ptrofs.repr
+                (4 * Integers.Ptrofs.unsigned
+                       (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4))) = OFFSET)
+        as NORMALISE.
+      { replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) at 1 by reflexivity.
+        rewrite <- PtrofsExtra.mul_unsigned.
+        apply PtrofsExtra.mul_divu; crush; auto. }
+
+      (** Normalised bounds proof *)
+      assert (0 <=
+              Integers.Ptrofs.unsigned (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4))
+              < (RTL.fn_stacksize f / 4))
+        as NORMALISE_BOUND.
+      { split.
+        apply Integers.Ptrofs.unsigned_range_2.
+        assert (forall x y, Integers.Ptrofs.divu x y = Integers.Ptrofs.divu x y ) by reflexivity.
+        unfold Integers.Ptrofs.divu at 2 in H0.
+        rewrite H0. clear H0.
+        rewrite Integers.Ptrofs.unsigned_repr; crush.
+        apply Zmult_lt_reg_r with (p := 4); try lia.
+        repeat rewrite ZLib.div_mul_undo; try lia.
+        apply Z.div_pos; small_tac.
+        apply Z.div_le_upper_bound; small_tac. }
+
+      inversion NORMALISE_BOUND as [ NORMALISE_BOUND_LOW NORMALISE_BOUND_HIGH ];
+      clear NORMALISE_BOUND.
+
+      (** Start of proof proper *)
+      eexists. split.
+      eapply Smallstep.plus_one.
+      eapply HTL.step_module; eauto.
+      apply assumption_32bit.
+      econstructor. econstructor. econstructor. crush.
+      econstructor. econstructor. econstructor. crush.
+      econstructor. econstructor.
+      econstructor. econstructor. econstructor. econstructor.
+      econstructor. econstructor. econstructor. econstructor.
+
+      all: big_tac.
+
+      1: {
+        assert (HPle : Ple dst (RTL.max_reg_function f)).
+        eapply RTL.max_reg_function_def. eassumption. auto.
+        apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption.
+      }
+
+      2: {
+        assert (HPle : Ple dst (RTL.max_reg_function f)).
+        eapply RTL.max_reg_function_def. eassumption. auto.
+        apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption.
+      }
+
+      (** Match assocmaps *)
+      apply regs_lessdef_add_match; big_tac.
+
+      (** Equality proof *)
+      match goal with
+      | [ |- context [valueToNat ?x] ] =>
+        assert (Z.to_nat
+                  (Integers.Ptrofs.unsigned
+                     (Integers.Ptrofs.divu
+                        OFFSET
+                        (Integers.Ptrofs.repr 4)))
+                =
+                valueToNat x)
+          as EXPR_OK by admit
+      end.
+      rewrite <- EXPR_OK.
+
+      specialize (H7 (Integers.Ptrofs.unsigned
+                        (Integers.Ptrofs.divu
+                           OFFSET
+                           (Integers.Ptrofs.repr 4)))).
+      exploit H7; big_tac.
+
+      (** RSBP preservation *)
+      unfold arr_stack_based_pointers in ASBP.
+      specialize (ASBP (Integers.Ptrofs.unsigned
+                          (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)))).
+      exploit ASBP; big_tac.
+      rewrite NORMALISE in H0. rewrite H1 in H0. assumption.
+
+    + (** Preamble *)
+      invert MARR. crush.
+
+      unfold Op.eval_addressing in H0.
+      destruct (Archi.ptr64) eqn:ARCHI; crush.
+
+      unfold reg_stack_based_pointers in RSBP.
+      pose proof (RSBP r0) as RSBPr0.
+      pose proof (RSBP r1) as RSBPr1.
+
+      destruct (Registers.Regmap.get r0 rs) eqn:EQr0;
+      destruct (Registers.Regmap.get r1 rs) eqn:EQr1; crush.
+
+      rewrite ARCHI in H1. crush.
+      subst.
+      clear RSBPr1.
+
+      pose proof MASSOC as MASSOC'.
+      invert MASSOC'.
+      pose proof (H0 r0).
+      pose proof (H0 r1).
+      assert (HPler0 : Ple r0 (RTL.max_reg_function f))
+        by (eapply RTL.max_reg_function_use; eauto; crush; eauto).
+      assert (HPler1 : Ple r1 (RTL.max_reg_function f))
+        by (eapply RTL.max_reg_function_use; eauto; simpl; auto).
+      apply H6 in HPler0.
+      apply H8 in HPler1.
+      invert HPler0; invert HPler1; try congruence.
+      rewrite EQr0 in H9.
+      rewrite EQr1 in H11.
+      invert H9. invert H11.
+      clear H0. clear H6. clear H8.
+
+      unfold check_address_parameter_signed in *;
+      unfold check_address_parameter_unsigned in *; crush.
+
+      remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ asr # r0))
+                                    (Integers.Ptrofs.of_int
+                                       (Integers.Int.add (Integers.Int.mul (valueToInt asr # r1) (Integers.Int.repr z))
+                                                         (Integers.Int.repr z0)))) as OFFSET.
+
+      (** Modular preservation proof *)
+      assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE.
+      { rewrite HeqOFFSET.
+        apply PtrofsExtra.add_mod; crush; try lia.
+        rewrite Integers.Ptrofs.unsigned_repr_eq.
+        rewrite <- Zmod_div_mod; crush.
+        apply PtrofsExtra.of_int_mod.
+        apply IntExtra.add_mod; crush.
+        apply IntExtra.mul_mod2; crush.
+        rewrite Integers.Int.unsigned_repr_eq.
+        rewrite <- Zmod_div_mod; crush.
+        rewrite Integers.Int.unsigned_repr_eq.
+        rewrite <- Zmod_div_mod; crush. }
+
+      (** Read bounds proof *)
+      assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH.
+      { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; crush; auto.
+        unfold stack_bounds in BOUNDS.
+        exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET)); auto.
+        split; try lia; apply Integers.Ptrofs.unsigned_range_2.
+        small_tac. }
+
+      (** Normalisation proof *)
+      assert (Integers.Ptrofs.repr
+                (4 * Integers.Ptrofs.unsigned
+                       (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4))) = OFFSET)
+        as NORMALISE.
+      { replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) at 1 by reflexivity.
+        rewrite <- PtrofsExtra.mul_unsigned.
+        apply PtrofsExtra.mul_divu; crush. }
+
+      (** Normalised bounds proof *)
+      assert (0 <=
+              Integers.Ptrofs.unsigned (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4))
+              < (RTL.fn_stacksize f / 4))
+        as NORMALISE_BOUND.
+      { split.
+        apply Integers.Ptrofs.unsigned_range_2.
+        assert (forall x y, Integers.Ptrofs.divu x y = Integers.Ptrofs.divu x y ) by reflexivity.
+        unfold Integers.Ptrofs.divu at 2 in H0.
+        rewrite H0. clear H0.
+        rewrite Integers.Ptrofs.unsigned_repr; crush.
+        apply Zmult_lt_reg_r with (p := 4); try lia.
+        repeat rewrite ZLib.div_mul_undo; try lia.
+        apply Z.div_pos; small_tac.
+        apply Z.div_le_upper_bound; lia. }
+
+      inversion NORMALISE_BOUND as [ NORMALISE_BOUND_LOW NORMALISE_BOUND_HIGH ];
+      clear NORMALISE_BOUND.
+
+      (** Start of proof proper *)
+      eexists. split.
+      eapply Smallstep.plus_one.
+      eapply HTL.step_module; eauto.
+      apply assumption_32bit.
+      econstructor. econstructor. econstructor. crush.
+      econstructor. econstructor. econstructor. crush.
+      econstructor. econstructor. econstructor.
+      econstructor. econstructor. econstructor. econstructor.
+      econstructor.
+      eapply Verilog.erun_Vbinop with (EQ := ?[EQ6]).
+      econstructor. econstructor. econstructor. econstructor.
+      econstructor. econstructor. econstructor. econstructor.
+      econstructor. econstructor.
+
+      all: big_tac.
+
+      1: { assert (HPle : Ple dst (RTL.max_reg_function f)).
+           eapply RTL.max_reg_function_def. eassumption. auto.
+           apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. }
+
+      2: { assert (HPle : Ple dst (RTL.max_reg_function f)).
+           eapply RTL.max_reg_function_def. eassumption. auto.
+           apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. }
+
+      (** Match assocmaps *)
+      apply regs_lessdef_add_match; big_tac.
+
+      (** Equality proof *)
+      match goal with
+      | [ |- context [valueToNat ?x] ] =>
+        assert (Z.to_nat
+                  (Integers.Ptrofs.unsigned
+                     (Integers.Ptrofs.divu
+                        OFFSET
+                        (Integers.Ptrofs.repr 4)))
+                =
+                valueToNat x)
+          as EXPR_OK by admit
+      end.
+      rewrite <- EXPR_OK.
+
+      specialize (H7 (Integers.Ptrofs.unsigned
+                        (Integers.Ptrofs.divu
+                           OFFSET
+                           (Integers.Ptrofs.repr 4)))).
+      exploit H7; big_tac.
+
+      (** RSBP preservation *)
+      unfold arr_stack_based_pointers in ASBP.
+      specialize (ASBP (Integers.Ptrofs.unsigned
+                          (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)))).
+      exploit ASBP; big_tac.
+      rewrite NORMALISE in H0. rewrite H1 in H0. assumption.
+
+    + invert MARR. crush.
+
+      unfold Op.eval_addressing in H0.
+      destruct (Archi.ptr64) eqn:ARCHI; crush.
+      rewrite ARCHI in H0. crush.
+
+      unfold check_address_parameter_unsigned in *;
+      unfold check_address_parameter_signed in *; crush.
+
+      assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
+      rewrite ZERO in H1. clear ZERO.
+      rewrite Integers.Ptrofs.add_zero_l in H1.
+
+      remember i0 as OFFSET.
+
+      (** Modular preservation proof *)
+      rename H0 into MOD_PRESERVE.
+
+      (** Read bounds proof *)
+      assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH.
+      { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; crush; auto.
+        unfold stack_bounds in BOUNDS.
+        exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET)); big_tac. }
+
+      (** Normalisation proof *)
+      assert (Integers.Ptrofs.repr
+                (4 * Integers.Ptrofs.unsigned
+                       (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4))) = OFFSET)
+        as NORMALISE.
+      { replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) at 1 by reflexivity.
+        rewrite <- PtrofsExtra.mul_unsigned.
+        apply PtrofsExtra.mul_divu; crush. }
+
+      (** Normalised bounds proof *)
+      assert (0 <=
+              Integers.Ptrofs.unsigned (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4))
+              < (RTL.fn_stacksize f / 4))
+        as NORMALISE_BOUND.
+      { split.
+        apply Integers.Ptrofs.unsigned_range_2.
+        assert (forall x y, Integers.Ptrofs.divu x y = Integers.Ptrofs.divu x y ) by reflexivity.
+        unfold Integers.Ptrofs.divu at 2 in H0.
+        rewrite H0. clear H0.
+        rewrite Integers.Ptrofs.unsigned_repr; crush.
+        apply Zmult_lt_reg_r with (p := 4); try lia.
+        repeat rewrite ZLib.div_mul_undo; try lia.
+        apply Z.div_pos; small_tac.
+        apply Z.div_le_upper_bound; lia. }
+
+      inversion NORMALISE_BOUND as [ NORMALISE_BOUND_LOW NORMALISE_BOUND_HIGH ];
+      clear NORMALISE_BOUND.
+
+      (** Start of proof proper *)
+      eexists. split.
+      eapply Smallstep.plus_one.
+      eapply HTL.step_module; eauto.
+      apply assumption_32bit.
+      econstructor. econstructor. econstructor. crush.
+      econstructor. econstructor. econstructor. econstructor. crush.
+
+      all: big_tac.
+
+      1: { assert (HPle : Ple dst (RTL.max_reg_function f)).
+           eapply RTL.max_reg_function_def. eassumption. auto.
+           apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. }
+
+      2: { assert (HPle : Ple dst (RTL.max_reg_function f)).
+           eapply RTL.max_reg_function_def. eassumption. auto.
+           apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. }
+
+      (** Match assocmaps *)
+      apply regs_lessdef_add_match; big_tac.
+
+      (** Equality proof *)
+      match goal with (* Prevents issues with evars *)
+      | [ |- context [valueToNat ?x] ] =>
+        assert (Z.to_nat
+                  (Integers.Ptrofs.unsigned
+                     (Integers.Ptrofs.divu
+                        OFFSET
+                        (Integers.Ptrofs.repr 4)))
+                =
+                valueToNat x)
+          as EXPR_OK by admit
+      end.
+      rewrite <- EXPR_OK.
+
+      specialize (H7 (Integers.Ptrofs.unsigned
+                        (Integers.Ptrofs.divu
+                           OFFSET
+                           (Integers.Ptrofs.repr 4)))).
+      exploit H7; big_tac.
+
+      (** RSBP preservation *)
+      unfold arr_stack_based_pointers in ASBP.
+      specialize (ASBP (Integers.Ptrofs.unsigned
+                          (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)))).
+      exploit ASBP; big_tac.
+      rewrite NORMALISE in H0. rewrite H1 in H0. assumption.*)
+  Admitted.
+  Hint Resolve transl_iload_correct : htlproof.
+
+  Lemma transl_istore_correct:
+    forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive)
+      (rs : Registers.Regmap.t Values.val) (m : mem) (chunk : AST.memory_chunk)
+      (addr : Op.addressing) (args : list Registers.reg) (src : Registers.reg)
+      (pc' : RTL.node) (a : Values.val) (m' : mem),
+      (RTL.fn_code f) ! pc = Some (RTL.Istore chunk addr args src pc') ->
+      Op.eval_addressing ge sp addr (map (fun r : positive => Registers.Regmap.get r rs) args) = Some a ->
+      Mem.storev chunk m a (Registers.Regmap.get src rs) = Some m' ->
+      forall R1 : HTL.state,
+        match_states (RTL.State s f sp pc rs m) R1 ->
+        exists R2 : HTL.state,
+          Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ match_states (RTL.State s f sp pc' rs m') R2.
+  Proof.
+(*    intros s f sp pc rs m chunk addr args src pc' a m' H H0 H1 R1 MSTATES.
+    inv_state. inv_arr_access.
+
+    + (** Preamble *)
+      invert MARR. crush.
+
+      unfold Op.eval_addressing in H0.
+      destruct (Archi.ptr64) eqn:ARCHI; crush.
+
+      unfold reg_stack_based_pointers in RSBP.
+      pose proof (RSBP r0) as RSBPr0.
+
+      destruct (Registers.Regmap.get r0 rs) eqn:EQr0; crush.
+
+      rewrite ARCHI in H1. crush.
+      subst.
+
+      pose proof MASSOC as MASSOC'.
+      invert MASSOC'.
+      pose proof (H0 r0).
+      assert (HPler0 : Ple r0 (RTL.max_reg_function f))
+        by (eapply RTL.max_reg_function_use; eauto; crush; eauto).
+      apply H6 in HPler0.
+      invert HPler0; try congruence.
+      rewrite EQr0 in H8.
+      invert H8.
+      clear H0. clear H6.
+
+      unfold check_address_parameter_unsigned in *;
+      unfold check_address_parameter_signed in *; crush.
+
+      remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ asr # r0))
+                                    (Integers.Ptrofs.of_int (Integers.Int.repr z))) as OFFSET.
+
+      (** Modular preservation proof *)
+      assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE.
+      { rewrite HeqOFFSET.
+        apply PtrofsExtra.add_mod; crush; try lia.
+        rewrite Integers.Ptrofs.unsigned_repr_eq.
+        rewrite <- Zmod_div_mod; crush.
+        apply PtrofsExtra.of_int_mod.
+        rewrite Integers.Int.unsigned_repr_eq.
+        rewrite <- Zmod_div_mod; crush. }
+
+      (** Write bounds proof *)
+      assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as WRITE_BOUND_HIGH.
+      { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; crush; auto.
+        unfold stack_bounds in BOUNDS.
+        exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET) (Registers.Regmap.get src rs)); big_tac.
+        apply Integers.Ptrofs.unsigned_range_2. }
+
+      (** Start of proof proper *)
+      eexists. split.
+      eapply Smallstep.plus_one.
+      eapply HTL.step_module; eauto.
+      apply assumption_32bit.
+      econstructor. econstructor. econstructor.
+      eapply Verilog.stmnt_runp_Vnonblock_arr. crush.
+      econstructor.
+      eapply Verilog.erun_Vbinop with (EQ := ?[EQ7]).
+      eapply Verilog.erun_Vbinop with (EQ := ?[EQ8]).
+      econstructor.
+      econstructor.
+      econstructor. econstructor. econstructor. econstructor.
+      econstructor. econstructor. econstructor. econstructor.
+
+      all: crush.
+
+      (** State Lookup *)
+      unfold Verilog.merge_regs.
+      crush.
+      unfold_merge.
+      apply AssocMap.gss.
+
+      (** Match states *)
+      rewrite assumption_32bit.
+      econstructor; eauto.
+
+      (** Match assocmaps *)
+      unfold Verilog.merge_regs. crush. unfold_merge.
+      apply regs_lessdef_add_greater.
+      unfold Plt; lia.
+      assumption.
+
+      (** States well formed *)
+      unfold state_st_wf. inversion 1. crush.
+      unfold Verilog.merge_regs.
+      unfold_merge.
+      apply AssocMap.gss.
+
+      (** Equality proof *)
+      match goal with
+      | [ |- context [valueToNat ?x] ] =>
+        assert (Z.to_nat
+                  (Integers.Ptrofs.unsigned
+                     (Integers.Ptrofs.divu
+                        OFFSET
+                        (Integers.Ptrofs.repr 4)))
+                =
+                valueToNat x)
+          as EXPR_OK by admit
+      end.
+
+      assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
+      inversion MASSOC; revert HeqOFFSET; subst; clear MASSOC; intros HeqOFFSET.
+
+      econstructor.
+      repeat split; crush.
+      unfold HTL.empty_stack.
+      crush.
+      unfold Verilog.merge_arrs.
+
+      rewrite AssocMap.gcombine.
+      2: { reflexivity. }
+      unfold Verilog.arr_assocmap_set.
+      rewrite AssocMap.gss.
+      unfold Verilog.merge_arr.
+      rewrite AssocMap.gss.
+      setoid_rewrite H5.
+      reflexivity.
+
+      rewrite combine_length.
+      rewrite <- array_set_len.
+      unfold arr_repeat. crush.
+      apply list_repeat_len.
+
+      rewrite <- array_set_len.
+      unfold arr_repeat. crush.
+      rewrite list_repeat_len.
+      rewrite H4. reflexivity.
+
+      remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ asr # r0))
+                                    (Integers.Ptrofs.of_int (Integers.Int.repr z))) as OFFSET.
+
+      destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET).
+
+      erewrite Mem.load_store_same.
+      2: { rewrite ZERO.
+           rewrite Integers.Ptrofs.add_zero_l.
+           rewrite e.
+           rewrite Integers.Ptrofs.unsigned_repr.
+           exact H1.
+           apply Integers.Ptrofs.unsigned_range_2. }
+      constructor.
+      erewrite combine_lookup_second.
+      simpl.
+      assert (Ple src (RTL.max_reg_function f))
+        by (eapply RTL.max_reg_function_use; eauto; simpl; auto);
+      apply H0 in H13.
+      destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; invert H13; eauto.
+
+      rewrite <- array_set_len.
+      unfold arr_repeat. crush.
+      rewrite list_repeat_len. auto.
+
+      assert (4 * ptr / 4 = Integers.Ptrofs.unsigned OFFSET / 4) by (f_equal; assumption).
+      rewrite Z.mul_comm in H13.
+      rewrite Z_div_mult in H13; try lia.
+      replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) in H13 by reflexivity.
+      rewrite <- PtrofsExtra.divu_unsigned in H13; unfold_constants; try lia.
+      rewrite H13. rewrite EXPR_OK.
+      rewrite array_get_error_set_bound.
+      reflexivity.
+      unfold arr_length, arr_repeat. simpl.
+      rewrite list_repeat_len. lia.
+
+      erewrite Mem.load_store_other with (m1 := m).
+      2: { exact H1. }
+      2: { right.
+           rewrite ZERO.
+           rewrite Integers.Ptrofs.add_zero_l.
+           rewrite Integers.Ptrofs.unsigned_repr.
+           simpl.
+           destruct (Z_le_gt_dec (4 * ptr + 4) (Integers.Ptrofs.unsigned OFFSET)); eauto.
+           right.
+           apply ZExtra.mod_0_bounds; try lia.
+           apply ZLib.Z_mod_mult'.
+           rewrite Z2Nat.id in H15; try lia.
+           apply Zmult_lt_compat_r with (p := 4) in H15; try lia.
+           rewrite ZLib.div_mul_undo in H15; try lia.
+           split; try lia.
+           apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia.
+      }
+
+      rewrite <- EXPR_OK.
+      rewrite PtrofsExtra.divu_unsigned; auto; try (unfold_constants; lia).
+      destruct (ptr ==Z Integers.Ptrofs.unsigned OFFSET / 4).
+      apply Z.mul_cancel_r with (p := 4) in e; try lia.
+      rewrite ZLib.div_mul_undo in e; try lia.
+      rewrite combine_lookup_first.
+      eapply H7; eauto.
+
+      rewrite <- array_set_len.
+      unfold arr_repeat. crush.
+      rewrite list_repeat_len. auto.
+      rewrite array_gso.
+      unfold array_get_error.
+      unfold arr_repeat.
+      crush.
+      apply list_repeat_lookup.
+      lia.
+      unfold_constants.
+      intro.
+      apply Z2Nat.inj_iff in H13; try lia.
+      apply Z.div_pos; try lia.
+      apply Integers.Ptrofs.unsigned_range.
+
+      assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
+      unfold arr_stack_based_pointers.
+      intros.
+      destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET).
+
+      crush.
+      erewrite Mem.load_store_same.
+      2: { rewrite ZERO.
+           rewrite Integers.Ptrofs.add_zero_l.
+           rewrite e.
+           rewrite Integers.Ptrofs.unsigned_repr.
+           exact H1.
+           apply Integers.Ptrofs.unsigned_range_2. }
+      crush.
+      destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; try constructor.
+      destruct (Archi.ptr64); try discriminate.
+      pose proof (RSBP src). rewrite EQ_SRC in H0.
+      assumption.
+
+      simpl.
+      erewrite Mem.load_store_other with (m1 := m).
+      2: { exact H1. }
+      2: { right.
+           rewrite ZERO.
+           rewrite Integers.Ptrofs.add_zero_l.
+           rewrite Integers.Ptrofs.unsigned_repr.
+           simpl.
+           destruct (Z_le_gt_dec (4 * ptr + 4) (Integers.Ptrofs.unsigned OFFSET)); eauto.
+           right.
+           apply ZExtra.mod_0_bounds; try lia.
+           apply ZLib.Z_mod_mult'.
+           invert H0.
+           apply Zmult_lt_compat_r with (p := 4) in H14; try lia.
+           rewrite ZLib.div_mul_undo in H14; try lia.
+           split; try lia.
+           apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia.
+      }
+      apply ASBP; assumption.
+
+      unfold stack_bounds in *. intros.
+      simpl.
+      assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
+      erewrite Mem.load_store_other with (m1 := m).
+      2: { exact H1. }
+      2: { right. right. simpl.
+           rewrite ZERO.
+           rewrite Integers.Ptrofs.add_zero_l.
+           rewrite Integers.Ptrofs.unsigned_repr; crush; try lia.
+           apply ZExtra.mod_0_bounds; crush; try lia. }
+      crush.
+      exploit (BOUNDS ptr); try lia. intros. crush.
+      exploit (BOUNDS ptr v); try lia. intros.
+      invert H0.
+      match goal with | |- ?x = _ => destruct x eqn:EQ end; try reflexivity.
+      assert (Mem.valid_access m AST.Mint32 sp'
+                               (Integers.Ptrofs.unsigned
+                                  (Integers.Ptrofs.add (Integers.Ptrofs.repr 0)
+                                                       (Integers.Ptrofs.repr ptr))) Writable).
+      { pose proof H1. eapply Mem.store_valid_access_2 in H0.
+        exact H0. eapply Mem.store_valid_access_3. eassumption. }
+      pose proof (Mem.valid_access_store m AST.Mint32 sp'
+                                         (Integers.Ptrofs.unsigned
+                                            (Integers.Ptrofs.add (Integers.Ptrofs.repr 0)
+                                                                 (Integers.Ptrofs.repr ptr))) v).
+      apply X in H0. invert H0. congruence.
+
+    + (** Preamble *)
+      invert MARR. crush.
+
+      unfold Op.eval_addressing in H0.
+      destruct (Archi.ptr64) eqn:ARCHI; crush.
+
+      unfold reg_stack_based_pointers in RSBP.
+      pose proof (RSBP r0) as RSBPr0.
+      pose proof (RSBP r1) as RSBPr1.
+
+      destruct (Registers.Regmap.get r0 rs) eqn:EQr0;
+      destruct (Registers.Regmap.get r1 rs) eqn:EQr1; crush.
+
+      rewrite ARCHI in H1. crush.
+      subst.
+      clear RSBPr1.
+
+      pose proof MASSOC as MASSOC'.
+      invert MASSOC'.
+      pose proof (H0 r0).
+      pose proof (H0 r1).
+      assert (HPler0 : Ple r0 (RTL.max_reg_function f))
+        by (eapply RTL.max_reg_function_use; eauto; crush; eauto).
+      assert (HPler1 : Ple r1 (RTL.max_reg_function f))
+        by (eapply RTL.max_reg_function_use; eauto; simpl; auto).
+      apply H6 in HPler0.
+      apply H8 in HPler1.
+      invert HPler0; invert HPler1; try congruence.
+      rewrite EQr0 in H9.
+      rewrite EQr1 in H11.
+      invert H9. invert H11.
+      clear H0. clear H6. clear H8.
+
+      unfold check_address_parameter_signed in *;
+      unfold check_address_parameter_unsigned in *; crush.
+
+      remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ asr # r0))
+                                    (Integers.Ptrofs.of_int
+                                       (Integers.Int.add (Integers.Int.mul (valueToInt asr # r1) (Integers.Int.repr z))
+                                                         (Integers.Int.repr z0)))) as OFFSET.
+
+      (** Modular preservation proof *)
+      assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE.
+      { rewrite HeqOFFSET.
+        apply PtrofsExtra.add_mod; crush; try lia.
+        rewrite Integers.Ptrofs.unsigned_repr_eq.
+        rewrite <- Zmod_div_mod; crush.
+        apply PtrofsExtra.of_int_mod.
+        apply IntExtra.add_mod; crush.
+        apply IntExtra.mul_mod2; crush.
+        rewrite Integers.Int.unsigned_repr_eq.
+        rewrite <- Zmod_div_mod; crush.
+        rewrite Integers.Int.unsigned_repr_eq.
+        rewrite <- Zmod_div_mod; crush. }
+
+      (** Write bounds proof *)
+      assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as WRITE_BOUND_HIGH.
+      { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; crush; auto.
+        unfold stack_bounds in BOUNDS.
+        exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET) (Registers.Regmap.get src rs)); auto.
+        split; try lia; apply Integers.Ptrofs.unsigned_range_2.
+        small_tac. }
+
+      (** Start of proof proper *)
+      eexists. split.
+      eapply Smallstep.plus_one.
+      eapply HTL.step_module; eauto.
+      apply assumption_32bit.
+      econstructor. econstructor. econstructor.
+      eapply Verilog.stmnt_runp_Vnonblock_arr. crush.
+      econstructor.
+      eapply Verilog.erun_Vbinop with (EQ := ?[EQ9]).
+      eapply Verilog.erun_Vbinop with (EQ := ?[EQ10]).
+      eapply Verilog.erun_Vbinop with (EQ := ?[EQ11]).
+      econstructor. econstructor. econstructor. econstructor.
+      econstructor.
+      eapply Verilog.erun_Vbinop with (EQ := ?[EQ12]).
+      econstructor. econstructor. econstructor. econstructor.
+      econstructor. econstructor. econstructor. econstructor.
+      econstructor. econstructor. econstructor. econstructor.
+
+      all: crush.
+
+      (** State Lookup *)
+      unfold Verilog.merge_regs.
+      crush.
+      unfold_merge.
+      apply AssocMap.gss.
+
+      (** Match states *)
+      rewrite assumption_32bit.
+      econstructor; eauto.
+
+      (** Match assocmaps *)
+      unfold Verilog.merge_regs. crush. unfold_merge.
+      apply regs_lessdef_add_greater.
+      unfold Plt; lia.
+      assumption.
+
+      (** States well formed *)
+      unfold state_st_wf. inversion 1. crush.
+      unfold Verilog.merge_regs.
+      unfold_merge.
+      apply AssocMap.gss.
+
+      (** Equality proof *)
+      assert (Z.to_nat
+                (Integers.Ptrofs.unsigned
+                   (Integers.Ptrofs.divu
+                      OFFSET
+                      (Integers.Ptrofs.repr 4)))
+              =
+              valueToNat (vdiv
+                            (vplus (vplus asr # r0 (ZToValue 32 z0) ?EQ11) (vmul asr # r1 (ZToValue 32 z) ?EQ12)
+                                   ?EQ10) (ZToValue 32 4) ?EQ9))
+        as EXPR_OK by admit.
+
+      assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
+      inversion MASSOC; revert HeqOFFSET; subst; clear MASSOC; intros HeqOFFSET.
+
+      econstructor.
+      repeat split; crush.
+      unfold HTL.empty_stack.
+      crush.
+      unfold Verilog.merge_arrs.
+
+      rewrite AssocMap.gcombine.
+      2: { reflexivity. }
+      unfold Verilog.arr_assocmap_set.
+      rewrite AssocMap.gss.
+      unfold Verilog.merge_arr.
+      rewrite AssocMap.gss.
+      setoid_rewrite H5.
+      reflexivity.
+
+      rewrite combine_length.
+      rewrite <- array_set_len.
+      unfold arr_repeat. crush.
+      apply list_repeat_len.
+
+      rewrite <- array_set_len.
+      unfold arr_repeat. crush.
+      rewrite list_repeat_len.
+      rewrite H4. reflexivity.
+
+      remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ asr # r0))
+                                    (Integers.Ptrofs.of_int
+                                       (Integers.Int.add (Integers.Int.mul (valueToInt asr # r1) (Integers.Int.repr z))
+                                                         (Integers.Int.repr z0)))) as OFFSET.
+      destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET).
+
+      erewrite Mem.load_store_same.
+      2: { rewrite ZERO.
+           rewrite Integers.Ptrofs.add_zero_l.
+           rewrite e.
+           rewrite Integers.Ptrofs.unsigned_repr.
+           exact H1.
+           apply Integers.Ptrofs.unsigned_range_2. }
+      constructor.
+      erewrite combine_lookup_second.
+      simpl.
+      assert (Ple src (RTL.max_reg_function f))
+        by (eapply RTL.max_reg_function_use; eauto; simpl; auto);
+      apply H0 in H16.
+      destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; invert H16; eauto.
+
+      rewrite <- array_set_len.
+      unfold arr_repeat. crush.
+      rewrite list_repeat_len. auto.
+
+      assert (4 * ptr / 4 = Integers.Ptrofs.unsigned OFFSET / 4) by (f_equal; assumption).
+      rewrite Z.mul_comm in H16.
+      rewrite Z_div_mult in H16; try lia.
+      replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) in H16 by reflexivity.
+      rewrite <- PtrofsExtra.divu_unsigned in H16; unfold_constants; try lia.
+      rewrite H16. rewrite EXPR_OK.
+      rewrite array_get_error_set_bound.
+      reflexivity.
+      unfold arr_length, arr_repeat. simpl.
+      rewrite list_repeat_len. lia.
+
+      erewrite Mem.load_store_other with (m1 := m).
+      2: { exact H1. }
+      2: { right.
+           rewrite ZERO.
+           rewrite Integers.Ptrofs.add_zero_l.
+           rewrite Integers.Ptrofs.unsigned_repr.
+           simpl.
+           destruct (Z_le_gt_dec (4 * ptr + 4) (Integers.Ptrofs.unsigned OFFSET)); eauto.
+           right.
+           apply ZExtra.mod_0_bounds; try lia.
+           apply ZLib.Z_mod_mult'.
+           rewrite Z2Nat.id in H18; try lia.
+           apply Zmult_lt_compat_r with (p := 4) in H18; try lia.
+           rewrite ZLib.div_mul_undo in H18; try lia.
+           split; try lia.
+           apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia.
+      }
+
+      rewrite <- EXPR_OK.
+      rewrite PtrofsExtra.divu_unsigned; auto; try (unfold_constants; lia).
+      destruct (ptr ==Z Integers.Ptrofs.unsigned OFFSET / 4).
+      apply Z.mul_cancel_r with (p := 4) in e; try lia.
+      rewrite ZLib.div_mul_undo in e; try lia.
+      rewrite combine_lookup_first.
+      eapply H7; eauto.
+
+      rewrite <- array_set_len.
+      unfold arr_repeat. crush.
+      rewrite list_repeat_len. auto.
+      rewrite array_gso.
+      unfold array_get_error.
+      unfold arr_repeat.
+      crush.
+      apply list_repeat_lookup.
+      lia.
+      unfold_constants.
+      intro.
+      apply Z2Nat.inj_iff in H16; try lia.
+      apply Z.div_pos; try lia.
+      apply Integers.Ptrofs.unsigned_range.
+
+      assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
+      unfold arr_stack_based_pointers.
+      intros.
+      destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET).
+
+      crush.
+      erewrite Mem.load_store_same.
+      2: { rewrite ZERO.
+           rewrite Integers.Ptrofs.add_zero_l.
+           rewrite e.
+           rewrite Integers.Ptrofs.unsigned_repr.
+           exact H1.
+           apply Integers.Ptrofs.unsigned_range_2. }
+      crush.
+      destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; try constructor.
+      destruct (Archi.ptr64); try discriminate.
+      pose proof (RSBP src). rewrite EQ_SRC in H0.
+      assumption.
+
+      simpl.
+      erewrite Mem.load_store_other with (m1 := m).
+      2: { exact H1. }
+      2: { right.
+           rewrite ZERO.
+           rewrite Integers.Ptrofs.add_zero_l.
+           rewrite Integers.Ptrofs.unsigned_repr.
+           simpl.
+           destruct (Z_le_gt_dec (4 * ptr + 4) (Integers.Ptrofs.unsigned OFFSET)); eauto.
+           right.
+           apply ZExtra.mod_0_bounds; try lia.
+           apply ZLib.Z_mod_mult'.
+           invert H0.
+           apply Zmult_lt_compat_r with (p := 4) in H17; try lia.
+           rewrite ZLib.div_mul_undo in H17; try lia.
+           split; try lia.
+           apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia.
+      }
+      apply ASBP; assumption.
+
+      unfold stack_bounds in *. intros.
+      simpl.
+      assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
+      erewrite Mem.load_store_other with (m1 := m).
+      2: { exact H1. }
+      2: { right. right. simpl.
+           rewrite ZERO.
+           rewrite Integers.Ptrofs.add_zero_l.
+           rewrite Integers.Ptrofs.unsigned_repr; crush; try lia.
+           apply ZExtra.mod_0_bounds; crush; try lia. }
+      crush.
+      exploit (BOUNDS ptr); try lia. intros. crush.
+      exploit (BOUNDS ptr v); try lia. intros.
+      invert H0.
+      match goal with | |- ?x = _ => destruct x eqn:EQ end; try reflexivity.
+      assert (Mem.valid_access m AST.Mint32 sp'
+                               (Integers.Ptrofs.unsigned
+                                  (Integers.Ptrofs.add (Integers.Ptrofs.repr 0)
+                                                       (Integers.Ptrofs.repr ptr))) Writable).
+      { pose proof H1. eapply Mem.store_valid_access_2 in H0.
+        exact H0. eapply Mem.store_valid_access_3. eassumption. }
+      pose proof (Mem.valid_access_store m AST.Mint32 sp'
+                                         (Integers.Ptrofs.unsigned
+                                            (Integers.Ptrofs.add (Integers.Ptrofs.repr 0)
+                                                                 (Integers.Ptrofs.repr ptr))) v).
+      apply X in H0. invert H0. congruence.
+
+    + invert MARR. crush.
+
+      unfold Op.eval_addressing in H0.
+      destruct (Archi.ptr64) eqn:ARCHI; crush.
+      rewrite ARCHI in H0. crush.
+
+      unfold check_address_parameter_unsigned in *;
+      unfold check_address_parameter_signed in *; crush.
+
+      assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
+      rewrite ZERO in H1. clear ZERO.
+      rewrite Integers.Ptrofs.add_zero_l in H1.
+
+      remember i0 as OFFSET.
+
+      (** Modular preservation proof *)
+      rename H0 into MOD_PRESERVE.
+
+      (** Write bounds proof *)
+      assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as WRITE_BOUND_HIGH.
+      { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; crush; auto.
+        unfold stack_bounds in BOUNDS.
+        exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET) (Registers.Regmap.get src rs)); auto.
+        crush.
+        replace (Integers.Ptrofs.repr 0) with (Integers.Ptrofs.zero) by reflexivity.
+        small_tac. }
+
+      (** Start of proof proper *)
+      eexists. split.
+      eapply Smallstep.plus_one.
+      eapply HTL.step_module; eauto.
+      apply assumption_32bit.
+      econstructor. econstructor. econstructor.
+      eapply Verilog.stmnt_runp_Vnonblock_arr. crush.
+      econstructor. econstructor. econstructor. econstructor.
+
+      all: crush.
+
+      (** State Lookup *)
+      unfold Verilog.merge_regs.
+      crush.
+      unfold_merge.
+      apply AssocMap.gss.
+
+      (** Match states *)
+      rewrite assumption_32bit.
+      econstructor; eauto.
+
+      (** Match assocmaps *)
+      unfold Verilog.merge_regs. crush. unfold_merge.
+      apply regs_lessdef_add_greater.
+      unfold Plt; lia.
+      assumption.
+
+      (** States well formed *)
+      unfold state_st_wf. inversion 1. crush.
+      unfold Verilog.merge_regs.
+      unfold_merge.
+      apply AssocMap.gss.
+
+      (** Equality proof *)
+      assert (Z.to_nat
+                (Integers.Ptrofs.unsigned
+                   (Integers.Ptrofs.divu
+                      OFFSET
+                      (Integers.Ptrofs.repr 4)))
+              =
+              valueToNat (ZToValue 32 (Integers.Ptrofs.unsigned OFFSET / 4)))
+        as EXPR_OK by admit.
+
+      assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
+      inversion MASSOC; revert HeqOFFSET; subst; clear MASSOC; intros HeqOFFSET.
+
+      econstructor.
+      repeat split; crush.
+      unfold HTL.empty_stack.
+      crush.
+      unfold Verilog.merge_arrs.
+
+      rewrite AssocMap.gcombine.
+      2: { reflexivity. }
+      unfold Verilog.arr_assocmap_set.
+      rewrite AssocMap.gss.
+      unfold Verilog.merge_arr.
+      rewrite AssocMap.gss.
+      setoid_rewrite H5.
+      reflexivity.
+
+      rewrite combine_length.
+      rewrite <- array_set_len.
+      unfold arr_repeat. crush.
+      apply list_repeat_len.
+
+      rewrite <- array_set_len.
+      unfold arr_repeat. crush.
+      rewrite list_repeat_len.
+      rewrite H4. reflexivity.
+
+      remember i0 as OFFSET.
+      destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET).
+
+      erewrite Mem.load_store_same.
+      2: { rewrite ZERO.
+           rewrite Integers.Ptrofs.add_zero_l.
+           rewrite e.
+           rewrite Integers.Ptrofs.unsigned_repr.
+           exact H1.
+           apply Integers.Ptrofs.unsigned_range_2. }
+      constructor.
+      erewrite combine_lookup_second.
+      simpl.
+      assert (Ple src (RTL.max_reg_function f))
+        by (eapply RTL.max_reg_function_use; eauto; simpl; auto);
+      apply H0 in H8.
+      destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; invert H8; eauto.
+
+      rewrite <- array_set_len.
+      unfold arr_repeat. crush.
+      rewrite list_repeat_len. auto.
+
+      assert (4 * ptr / 4 = Integers.Ptrofs.unsigned OFFSET / 4) by (f_equal; assumption).
+      rewrite Z.mul_comm in H8.
+      rewrite Z_div_mult in H8; try lia.
+      replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) in H8 by reflexivity.
+      rewrite <- PtrofsExtra.divu_unsigned in H8; unfold_constants; try lia.
+      rewrite H8. rewrite EXPR_OK.
+      rewrite array_get_error_set_bound.
+      reflexivity.
+      unfold arr_length, arr_repeat. simpl.
+      rewrite list_repeat_len. lia.
+
+      erewrite Mem.load_store_other with (m1 := m).
+      2: { exact H1. }
+      2: { right.
+           rewrite ZERO.
+           rewrite Integers.Ptrofs.add_zero_l.
+           rewrite Integers.Ptrofs.unsigned_repr.
+           simpl.
+           destruct (Z_le_gt_dec (4 * ptr + 4) (Integers.Ptrofs.unsigned OFFSET)); eauto.
+           right.
+           apply ZExtra.mod_0_bounds; try lia.
+           apply ZLib.Z_mod_mult'.
+           rewrite Z2Nat.id in H11; try lia.
+           apply Zmult_lt_compat_r with (p := 4) in H11; try lia.
+           rewrite ZLib.div_mul_undo in H11; try lia.
+           split; try lia.
+           apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia.
+      }
+
+      rewrite <- EXPR_OK.
+      rewrite PtrofsExtra.divu_unsigned; auto; try (unfold_constants; lia).
+      destruct (ptr ==Z Integers.Ptrofs.unsigned OFFSET / 4).
+      apply Z.mul_cancel_r with (p := 4) in e; try lia.
+      rewrite ZLib.div_mul_undo in e; try lia.
+      rewrite combine_lookup_first.
+      eapply H7; eauto.
+
+      rewrite <- array_set_len.
+      unfold arr_repeat. crush.
+      rewrite list_repeat_len. auto.
+      rewrite array_gso.
+      unfold array_get_error.
+      unfold arr_repeat.
+      crush.
+      apply list_repeat_lookup.
+      lia.
+      unfold_constants.
+      intro.
+      apply Z2Nat.inj_iff in H8; try lia.
+      apply Z.div_pos; try lia.
+      apply Integers.Ptrofs.unsigned_range.
+
+      assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
+      unfold arr_stack_based_pointers.
+      intros.
+      destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET).
+
+      crush.
+      erewrite Mem.load_store_same.
+      2: { rewrite ZERO.
+           rewrite Integers.Ptrofs.add_zero_l.
+           rewrite e.
+           rewrite Integers.Ptrofs.unsigned_repr.
+           exact H1.
+           apply Integers.Ptrofs.unsigned_range_2. }
+      crush.
+      destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; try constructor.
+      destruct (Archi.ptr64); try discriminate.
+      pose proof (RSBP src). rewrite EQ_SRC in H0.
+      assumption.
+
+      simpl.
+      erewrite Mem.load_store_other with (m1 := m).
+      2: { exact H1. }
+      2: { right.
+           rewrite ZERO.
+           rewrite Integers.Ptrofs.add_zero_l.
+           rewrite Integers.Ptrofs.unsigned_repr.
+           simpl.
+           destruct (Z_le_gt_dec (4 * ptr + 4) (Integers.Ptrofs.unsigned OFFSET)); eauto.
+           right.
+           apply ZExtra.mod_0_bounds; try lia.
+           apply ZLib.Z_mod_mult'.
+           invert H0.
+           apply Zmult_lt_compat_r with (p := 4) in H9; try lia.
+           rewrite ZLib.div_mul_undo in H9; try lia.
+           split; try lia.
+           apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia.
+      }
+      apply ASBP; assumption.
+
+      unfold stack_bounds in *. intros.
+      simpl.
+      assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
+      erewrite Mem.load_store_other with (m1 := m).
+      2: { exact H1. }
+      2: { right. right. simpl.
+           rewrite ZERO.
+           rewrite Integers.Ptrofs.add_zero_l.
+           rewrite Integers.Ptrofs.unsigned_repr; crush; try lia.
+           apply ZExtra.mod_0_bounds; crush; try lia. }
+      crush.
+      exploit (BOUNDS ptr); try lia. intros. crush.
+      exploit (BOUNDS ptr v); try lia. intros.
+      invert H0.
+      match goal with | |- ?x = _ => destruct x eqn:EQ end; try reflexivity.
+      assert (Mem.valid_access m AST.Mint32 sp'
+                               (Integers.Ptrofs.unsigned
+                                  (Integers.Ptrofs.add (Integers.Ptrofs.repr 0)
+                                                       (Integers.Ptrofs.repr ptr))) Writable).
+      { pose proof H1. eapply Mem.store_valid_access_2 in H0.
+        exact H0. eapply Mem.store_valid_access_3. eassumption. }
+      pose proof (Mem.valid_access_store m AST.Mint32 sp'
+                                         (Integers.Ptrofs.unsigned
+                                            (Integers.Ptrofs.add (Integers.Ptrofs.repr 0)
+                                                                 (Integers.Ptrofs.repr ptr))) v).
+      apply X in H0. invert H0. congruence.*)
+  Admitted.
+  Hint Resolve transl_istore_correct : htlproof.
+
+  Lemma transl_icond_correct:
+    forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive)
+      (rs : Registers.Regmap.t Values.val) (m : mem) (cond : Op.condition) (args : list Registers.reg)
+      (ifso ifnot : RTL.node) (b : bool) (pc' : RTL.node),
+      (RTL.fn_code f) ! pc = Some (RTL.Icond cond args ifso ifnot) ->
+      Op.eval_condition cond (map (fun r : positive => Registers.Regmap.get r rs) args) m = Some b ->
+      pc' = (if b then ifso else ifnot) ->
+      forall R1 : HTL.state,
+        match_states (RTL.State s f sp pc rs m) R1 ->
+        exists R2 : HTL.state,
+          Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ match_states (RTL.State s f sp pc' rs m) R2.
+  Proof.
+    intros s f sp pc rs m cond args ifso ifnot b pc' H H0 H1 R1 MSTATE.
+    inv_state.
+
+    eexists. split. apply Smallstep.plus_one.
+    eapply HTL.step_module; eauto.
+    inv CONST; assumption.
+    inv CONST; assumption.
+(*    eapply Verilog.stmnt_runp_Vnonblock_reg with
+        (rhsval := if b then posToValue 32 ifso else posToValue 32 ifnot).
+    constructor.
+
+    simpl.
+    destruct b.
+    eapply Verilog.erun_Vternary_true.
+    eapply eval_cond_correct; eauto.
+    constructor.
+    apply boolToValue_ValueToBool.
+    eapply Verilog.erun_Vternary_false.
+    eapply eval_cond_correct; eauto.
+    constructor.
+    apply boolToValue_ValueToBool.
+    constructor.
+
+    big_tac.
+
+    invert MARR.
+    destruct b; rewrite assumption_32bit; big_tac.
+
+    Unshelve.
+    constructor.
+  Qed.*)
+  Admitted.
+  Hint Resolve transl_icond_correct : htlproof.
+
+  Lemma transl_ijumptable_correct:
+    forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive)
+      (rs : Registers.Regmap.t Values.val) (m : mem) (arg : Registers.reg) (tbl : list RTL.node)
+      (n : Integers.Int.int) (pc' : RTL.node),
+      (RTL.fn_code f) ! pc = Some (RTL.Ijumptable arg tbl) ->
+      Registers.Regmap.get arg rs = Values.Vint n ->
+      list_nth_z tbl (Integers.Int.unsigned n) = Some pc' ->
+      forall R1 : HTL.state,
+        match_states (RTL.State s f sp pc rs m) R1 ->
+        exists R2 : HTL.state,
+          Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ match_states (RTL.State s f sp pc' rs m) R2.
+  Proof.
+    intros s f sp pc rs m arg tbl n pc' H H0 H1 R1 MSTATE.
+  Admitted.
+  Hint Resolve transl_ijumptable_correct : htlproof.
+
+  Lemma transl_ireturn_correct:
+    forall (s : list RTL.stackframe) (f : RTL.function) (stk : Values.block)
+      (pc : positive) (rs : RTL.regset) (m : mem) (or : option Registers.reg)
+      (m' : mem),
+      (RTL.fn_code f) ! pc = Some (RTL.Ireturn or) ->
+      Mem.free m stk 0 (RTL.fn_stacksize f) = Some m' ->
+      forall R1 : HTL.state,
+        match_states (RTL.State s f (Values.Vptr stk Integers.Ptrofs.zero) pc rs m) R1 ->
+        exists R2 : HTL.state,
+          Smallstep.plus HTL.step tge R1 Events.E0 R2 /\
+          match_states (RTL.Returnstate s (Registers.regmap_optget or Values.Vundef rs) m') R2.
+  Proof.
+    intros s f stk pc rs m or m' H H0 R1 MSTATE.
+    inv_state.
+
+    - econstructor. split.
+      eapply Smallstep.plus_two.
+
+      eapply HTL.step_module; eauto.
+      inv CONST; assumption.
+      inv CONST; assumption.
+      constructor.
+      econstructor; simpl; trivial.
+      econstructor; simpl; trivial.
+      constructor.
+      econstructor; simpl; trivial.
+      constructor.
+
+      constructor. constructor.
+
+      unfold state_st_wf in WF; big_tac; eauto.
+      destruct wf as [HCTRL HDATA]. apply HCTRL.
+      apply AssocMapExt.elements_iff. eexists.
+      match goal with H: control ! pc = Some _ |- _ => apply H end.
+
+      apply HTL.step_finish.
+      unfold Verilog.merge_regs.
+      unfold_merge; simpl.
+      rewrite AssocMap.gso.
+      apply AssocMap.gss. lia.
+      apply AssocMap.gss.
+      rewrite Events.E0_left. reflexivity.
+
+      constructor; auto.
+      constructor.
+
+    (* FIXME: Duplication *)
+    - econstructor. split.
+      eapply Smallstep.plus_two.
+      eapply HTL.step_module; eauto.
+      inv CONST; assumption.
+      inv CONST; assumption.
+      constructor.
+      econstructor; simpl; trivial.
+      econstructor; simpl; trivial.
+      constructor. constructor. constructor.
+      constructor. constructor. constructor.
+
+      unfold state_st_wf in WF; big_tac; eauto.
+
+      destruct wf as [HCTRL HDATA]. apply HCTRL.
+      apply AssocMapExt.elements_iff. eexists.
+      match goal with H: control ! pc = Some _ |- _ => apply H end.
+
+      apply HTL.step_finish.
+      unfold Verilog.merge_regs.
+      unfold_merge.
+      rewrite AssocMap.gso.
+      apply AssocMap.gss. simpl; lia.
+      apply AssocMap.gss.
+      rewrite Events.E0_left. trivial.
+
+      constructor; auto.
+
+      simpl. inversion MASSOC. subst.
+      unfold find_assocmap, AssocMapExt.get_default. rewrite AssocMap.gso.
+      apply H1. eapply RTL.max_reg_function_use. eauto. simpl; tauto.
+      assert (HPle : Ple r (RTL.max_reg_function f)).
+      eapply RTL.max_reg_function_use. eassumption. simpl; auto.
+      apply ZExtra.Ple_not_eq. apply ZExtra.Ple_Plt_Succ. assumption.
+
+      Unshelve.
+      all: constructor.
+  Qed.
+  Hint Resolve transl_ireturn_correct : htlproof.
+
+  Lemma transl_callstate_correct:
+    forall (s : list RTL.stackframe) (f : RTL.function) (args : list Values.val)
+      (m : mem) (m' : Mem.mem') (stk : Values.block),
+      Mem.alloc m 0 (RTL.fn_stacksize f) = (m', stk) ->
+      forall R1 : HTL.state,
+        match_states (RTL.Callstate s (AST.Internal f) args m) R1 ->
+        exists R2 : HTL.state,
+          Smallstep.plus HTL.step tge R1 Events.E0 R2 /\
+          match_states
+            (RTL.State s f (Values.Vptr stk Integers.Ptrofs.zero) (RTL.fn_entrypoint f)
+                       (RTL.init_regs args (RTL.fn_params f)) m') R2.
+  Proof.
+    intros s f args m m' stk H R1 MSTATE.
+
+    inversion MSTATE; subst. inversion TF; subst.
+    econstructor. split. apply Smallstep.plus_one.
+    eapply HTL.step_call. crush.
+
+    apply match_state with (sp' := stk); eauto.
+
+    all: big_tac.
+
+    apply regs_lessdef_add_greater. unfold Plt; lia.
+    apply regs_lessdef_add_greater. unfold Plt; lia.
+    apply regs_lessdef_add_greater. unfold Plt; lia.
+    apply init_reg_assoc_empty.
+
+    constructor.
+
+    destruct (Mem.load AST.Mint32 m' stk
+                       (Integers.Ptrofs.unsigned (Integers.Ptrofs.add
+                                                    Integers.Ptrofs.zero
+                                                    (Integers.Ptrofs.repr (4 * ptr))))) eqn:LOAD.
+    pose proof Mem.load_alloc_same as LOAD_ALLOC.
+    pose proof H as ALLOC.
+    eapply LOAD_ALLOC in ALLOC.
+    2: { exact LOAD. }
+    ptrofs. rewrite LOAD.
+    rewrite ALLOC.
+    repeat constructor.
+
+    ptrofs. rewrite LOAD.
+    repeat constructor.
+
+    unfold reg_stack_based_pointers. intros.
+    unfold RTL.init_regs; crush.
+    destruct (RTL.fn_params f);
+    rewrite Registers.Regmap.gi; constructor.
+
+    unfold arr_stack_based_pointers. intros.
+    crush.
+    destruct (Mem.load AST.Mint32 m' stk
+                       (Integers.Ptrofs.unsigned (Integers.Ptrofs.add
+                                                    Integers.Ptrofs.zero
+                                                    (Integers.Ptrofs.repr (4 * ptr))))) eqn:LOAD.
+    pose proof Mem.load_alloc_same as LOAD_ALLOC.
+    pose proof H as ALLOC.
+    eapply LOAD_ALLOC in ALLOC.
+    2: { exact LOAD. }
+    rewrite ALLOC.
+    repeat constructor.
+    constructor.
+
+    Transparent Mem.alloc. (* TODO: Since there are opaque there's probably a lemma. *)
+    Transparent Mem.load.
+    Transparent Mem.store.
+    unfold stack_bounds.
+    split.
+
+    unfold Mem.alloc in H.
+    invert H.
+    crush.
+    unfold Mem.load.
+    intros.
+    match goal with | |- context[if ?x then _ else _] => destruct x end; try congruence.
+    invert v0. unfold Mem.range_perm in H4.
+    unfold Mem.perm in H4. crush.
+    unfold Mem.perm_order' in H4.
+    small_tac.
+    exploit (H4 ptr). rewrite Integers.Ptrofs.unsigned_repr; small_tac. intros.
+    rewrite Maps.PMap.gss in H8.
+    match goal with | H8 : context[if ?x then _ else _] |- _ => destruct x eqn:EQ end; try contradiction.
+    crush.
+    apply proj_sumbool_true in H10. lia.
+
+    unfold Mem.alloc in H.
+    invert H.
+    crush.
+    unfold Mem.store.
+    intros.
+    match goal with | |- context[if ?x then _ else _] => destruct x end; try congruence.
+    invert v0. unfold Mem.range_perm in H4.
+    unfold Mem.perm in H4. crush.
+    unfold Mem.perm_order' in H4.
+    small_tac.
+    exploit (H4 ptr). rewrite Integers.Ptrofs.unsigned_repr; small_tac. intros.
+    rewrite Maps.PMap.gss in H8.
+    match goal with | H8 : context[if ?x then _ else _] |- _ => destruct x eqn:EQ end; try contradiction.
+    crush.
+    apply proj_sumbool_true in H10. lia.
+    constructor. simplify. rewrite AssocMap.gss.
+    simplify. rewrite AssocMap.gso. apply AssocMap.gss. simplify. lia.
+    Opaque Mem.alloc.
+    Opaque Mem.load.
+    Opaque Mem.store.
+  Qed.
+  Hint Resolve transl_callstate_correct : htlproof.
+
+  Lemma transl_returnstate_correct:
+    forall (res0 : Registers.reg) (f : RTL.function) (sp : Values.val) (pc : RTL.node)
+      (rs : RTL.regset) (s : list RTL.stackframe) (vres : Values.val) (m : mem)
+      (R1 : HTL.state),
+      match_states (RTL.Returnstate (RTL.Stackframe res0 f sp pc rs :: s) vres m) R1 ->
+      exists R2 : HTL.state,
+        Smallstep.plus HTL.step tge R1 Events.E0 R2 /\
+        match_states (RTL.State s f sp pc (Registers.Regmap.set res0 vres rs) m) R2.
+  Proof.
+    intros res0 f sp pc rs s vres m R1 MSTATE.
+    inversion MSTATE. inversion MF.
+  Qed.
+  Hint Resolve transl_returnstate_correct : htlproof.
+
+  Lemma option_inv :
+    forall A x y,
+      @Some A x = Some y -> x = y.
+  Proof. intros. inversion H. trivial. Qed.
+
+  Lemma main_tprog_internal :
+    forall b,
+      Globalenvs.Genv.find_symbol tge tprog.(AST.prog_main) = Some b ->
+      exists f, Genv.find_funct_ptr (Genv.globalenv tprog) b = Some (AST.Internal f).
+  Proof.
+    intros.
+    destruct TRANSL. unfold main_is_internal in H1.
+    repeat (unfold_match H1). replace b with b0.
+    exploit function_ptr_translated; eauto. intros [tf [A B]].
+    unfold transl_fundef, AST.transf_partial_fundef, Errors.bind in B.
+    unfold_match B. inv B. econstructor. apply A.
+
+    apply option_inv. rewrite <- Heqo. rewrite <- H.
+    rewrite symbols_preserved. replace (AST.prog_main tprog) with (AST.prog_main prog).
+    trivial. symmetry; eapply Linking.match_program_main; eauto.
+  Qed.
+
+  Lemma transl_initial_states :
+    forall s1 : Smallstep.state (RTL.semantics prog),
+      Smallstep.initial_state (RTL.semantics prog) s1 ->
+      exists s2 : Smallstep.state (HTL.semantics tprog),
+        Smallstep.initial_state (HTL.semantics tprog) s2 /\ match_states s1 s2.
+  Proof.
+    induction 1.
+    destruct TRANSL. unfold main_is_internal in H4.
+    repeat (unfold_match H4).
+    assert (f = AST.Internal f1). apply option_inv.
+    rewrite <- Heqo0. rewrite <- H1. replace b with b0.
+    auto. apply option_inv. rewrite <- H0. rewrite <- Heqo.
+    trivial.
+    exploit function_ptr_translated; eauto.
+    intros [tf [A B]].
+    unfold transl_fundef, Errors.bind in B.
+    unfold AST.transf_partial_fundef, Errors.bind in B.
+    repeat (unfold_match B). inversion B. subst.
+    exploit main_tprog_internal; eauto; intros.
+    rewrite symbols_preserved. replace (AST.prog_main tprog) with (AST.prog_main prog).
+    apply Heqo. symmetry; eapply Linking.match_program_main; eauto.
+    inversion H5.
+    econstructor; split. econstructor.
+    apply (Genv.init_mem_transf_partial TRANSL'); eauto.
+    replace (AST.prog_main tprog) with (AST.prog_main prog).
+    rewrite symbols_preserved; eauto.
+    symmetry; eapply Linking.match_program_main; eauto.
+    apply H6.
+
+    constructor.
+    apply transl_module_correct.
+    assert (Some (AST.Internal x) = Some (AST.Internal m)).
+    replace (AST.fundef HTL.module) with (HTL.fundef).
+    rewrite <- H6. setoid_rewrite <- A. trivial.
+    trivial. inv H7. assumption.
+  Qed.
+  Hint Resolve transl_initial_states : htlproof.
+
+  Lemma transl_final_states :
+    forall (s1 : Smallstep.state (RTL.semantics prog))
+           (s2 : Smallstep.state (HTL.semantics tprog))
+           (r : Integers.Int.int),
+      match_states s1 s2 ->
+      Smallstep.final_state (RTL.semantics prog) s1 r ->
+      Smallstep.final_state (HTL.semantics tprog) s2 r.
+  Proof.
+    intros. inv H0. inv H. inv H4. invert MF. constructor. reflexivity.
+  Qed.
+  Hint Resolve transl_final_states : htlproof.
+
+  Theorem transl_step_correct:
+    forall (S1 : RTL.state) t S2,
+      RTL.step ge S1 t S2 ->
+      forall (R1 : HTL.state),
+        match_states S1 R1 ->
+        exists R2, Smallstep.plus HTL.step tge R1 t R2 /\ match_states S2 R2.
+  Proof.
+    induction 1; eauto with htlproof; (intros; inv_state).
+  Qed.
+  Hint Resolve transl_step_correct : htlproof.
+
+  Theorem transf_program_correct:
+    Smallstep.forward_simulation (RTL.semantics prog) (HTL.semantics tprog).
+  Proof.
+    eapply Smallstep.forward_simulation_plus; eauto with htlproof.
+    apply senv_preserved.
+  Qed.
+
+End CORRECTNESS.
diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v
index bbcde14..aba5d0c 100644
--- a/src/translation/HTLgenspec.v
+++ b/src/translation/HTLgenspec.v
@@ -17,7 +17,7 @@
  *)
 
 From compcert Require RTL Op Maps Errors.
-From compcert Require Import Maps.
+From compcert Require Import Maps Integers.
 From coqup Require Import Coquplib Verilog ValueInt HTL HTLgen AssocMap.
 Require Import Lia.
 
@@ -117,13 +117,17 @@ translations for each of the elements *)
 Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> stmnt -> stmnt -> Prop :=
 | tr_instr_Inop :
     forall n,
+      Z.pos n <= Int.max_unsigned ->
       tr_instr fin rtrn st stk (RTL.Inop n) Vskip (state_goto st n)
 | tr_instr_Iop :
     forall n op args dst s s' e i,
+      Z.pos n <= Int.max_unsigned ->
       translate_instr op args s = OK e s' i ->
       tr_instr fin rtrn st stk (RTL.Iop op args dst n) (Vnonblock (Vvar dst) e) (state_goto st n)
 | tr_instr_Icond :
     forall n1 n2 cond args s s' i c,
+      Z.pos n1 <= Int.max_unsigned ->
+      Z.pos n2 <= Int.max_unsigned ->
       translate_condition cond args s = OK c s' i ->
       tr_instr fin rtrn st stk (RTL.Icond cond args n1 n2) Vskip (state_cond st c n1 n2)
 | tr_instr_Ireturn_None :
@@ -135,11 +139,13 @@ Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> stmnt -> stmnt -
                (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vvar r))) Vskip
 | tr_instr_Iload :
     forall mem addr args s s' i e dst n,
+      Z.pos n <= Int.max_unsigned ->
       translate_eff_addressing addr args s = OK e s' i ->
       tr_instr fin rtrn st stk (RTL.Iload mem addr args dst n)
                                (create_single_cycle_load stk e dst) (state_goto st n)
 | tr_instr_Istore :
     forall mem addr args s s' i e src n,
+      Z.pos n <= Int.max_unsigned ->
       translate_eff_addressing addr args s = OK e s' i ->
       tr_instr fin rtrn st stk (RTL.Istore mem addr args src n)
                                (create_single_cycle_store stk e src) (state_goto st n)
@@ -407,13 +413,15 @@ Lemma transf_instr_freshreg_trans :
 Proof.
   intros. destruct instr eqn:?. subst. unfold transf_instr in H.
   destruct i0; try (monadInv H); try (unfold_match H); eauto with htlspec.
-  - apply add_instr_freshreg_trans in EQ2. apply translate_instr_freshreg_trans in EQ.
+  - monadInv H. apply add_instr_freshreg_trans in EQ2. apply translate_instr_freshreg_trans in EQ.
     apply declare_reg_freshreg_trans in EQ1. congruence.
-  - apply add_instr_freshreg_trans in EQ2. apply translate_eff_addressing_freshreg_trans in EQ.
+  - monadInv H. apply add_instr_freshreg_trans in EQ2.
+    apply translate_eff_addressing_freshreg_trans in EQ.
     apply declare_reg_freshreg_trans in EQ1. congruence.
-  - apply add_instr_freshreg_trans in EQ0. apply translate_eff_addressing_freshreg_trans in EQ.
-    congruence.
-  - apply translate_condition_freshreg_trans in EQ. apply add_branch_instr_freshreg_trans in EQ0.
+  - monadInv H. apply add_instr_freshreg_trans in EQ0.
+    apply translate_eff_addressing_freshreg_trans in EQ. congruence.
+  - monadInv H. apply translate_condition_freshreg_trans in EQ.
+    apply add_branch_instr_freshreg_trans in EQ0.
     congruence.
   - inv EQ. apply add_node_skip_freshreg_trans in EQ0. congruence.
 Qed.
@@ -438,13 +446,16 @@ Ltac rewrite_states :=
 
 Ltac inv_add_instr' H :=
   match type of H with
+  | ?f _ _ = OK _ _ _ => unfold f in H
   | ?f _ _ _ = OK _ _ _ => unfold f in H
   | ?f _ _ _ _ = OK _ _ _ => unfold f in H
   | ?f _ _ _ _ _ = OK _ _ _ => unfold f in H
+  | ?f _ _ _ _ _ _ = OK _ _ _ => unfold f in H
   end; repeat unfold_match H; inversion H.
 
 Ltac inv_add_instr :=
-  lazymatch goal with
+  match goal with
+  | H: (if ?c then _ else _) _ = OK _ _ _ |- _ => destruct c eqn:EQN; try discriminate; inv_add_instr
   | H: context[add_instr_skip _ _ _] |- _ =>
     inv_add_instr' H
   | H: context[add_instr_skip _ _] |- _ =>
@@ -484,23 +495,27 @@ Proof.
     + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence.
     + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence.
     + inversion H2. inversion H9. rewrite H. apply tr_instr_Inop.
+      apply Z.leb_le. assumption.
       eapply in_map with (f := fst) in H9. contradiction.
 
     + destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence.
     + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence.
     + inversion H2. inversion H14. unfold nonblock. replace (st_st s4) with (st_st s2) by congruence.
-      econstructor. apply EQ1. eapply in_map with (f := fst) in H14. contradiction.
+      econstructor. apply Z.leb_le; assumption.
+      apply EQ1. eapply in_map with (f := fst) in H14. contradiction.
 
     + destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence.
     + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence.
     + inversion H2. inversion H14. rewrite <- e2. replace (st_st s2) with (st_st s0) by congruence.
-      econstructor. apply EQ1. eapply in_map with (f := fst) in H14. contradiction.
+      econstructor. apply Z.leb_le; assumption.
+      apply EQ1. eapply in_map with (f := fst) in H14. contradiction.
 
     + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence.
     + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence.
     + destruct H2.
       * inversion H2.
         replace (st_st s2) with (st_st s0) by congruence.
+        econstructor. apply Z.leb_le; assumption.
         eauto with htlspec.
       * apply in_map with (f := fst) in H2. contradiction.
 
@@ -509,6 +524,7 @@ Proof.
     + destruct H2.
       * inversion H2.
         replace (st_st s2) with (st_st s0) by congruence.
+        econstructor; try (apply Z.leb_le; apply andb_prop in EQN; apply EQN).
         eauto with htlspec.
       * apply in_map with (f := fst) in H2. contradiction.
 
diff --git a/src/translation/Veriloggenspec.v b/src/translation/Veriloggenspec.v
deleted file mode 100644
index 7dc632c..0000000
--- a/src/translation/Veriloggenspec.v
+++ /dev/null
@@ -1,17 +0,0 @@
-(*
- * CoqUp: Verified high-level synthesis.
- * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com>
- *
- * This program is free software: you can redistribute it and/or modify
- * it under the terms of the GNU General Public License as published by
- * the Free Software Foundation, either version 3 of the License, or
- * (at your option) any later version.
- *
- * This program is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with this program.  If not, see <https://www.gnu.org/licenses/>.
- *)
diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v
index 3ba5b59..b3d1442 100644
--- a/src/verilog/HTL.v
+++ b/src/verilog/HTL.v
@@ -141,8 +141,10 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop :=
     forall g m args res,
       step g (Callstate res m args) Events.E0
            (State res m m.(mod_entrypoint)
-             (AssocMap.set (mod_st m) (posToValue m.(mod_entrypoint))
-                           (init_regs args m.(mod_params)))
+             (AssocMap.set (mod_reset m) (ZToValue 0)
+              (AssocMap.set (mod_finish m) (ZToValue 0)
+               (AssocMap.set (mod_st m) (posToValue m.(mod_entrypoint))
+                (init_regs args m.(mod_params)))))
              (empty_stack m))
 | step_return :
     forall g m asr asa i r sf pc mst,
diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v
index 921d9fd..108ac72 100644
--- a/src/verilog/Verilog.v
+++ b/src/verilog/Verilog.v
@@ -757,8 +757,10 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop :=
     forall g res m args,
     step g (Callstate res m args) Events.E0
          (State res m m.(mod_entrypoint)
-          (AssocMap.set m.(mod_st) (posToValue m.(mod_entrypoint))
-           (init_params args m.(mod_args)))
+          (AssocMap.set (mod_reset m) (ZToValue 0)
+           (AssocMap.set (mod_finish m) (ZToValue 0)
+            (AssocMap.set m.(mod_st) (posToValue m.(mod_entrypoint))
+             (init_params args m.(mod_args)))))
           (empty_stack m))
 | step_return :
     forall g m asr i r sf pc mst asa,
@@ -909,9 +911,9 @@ Lemma semantics_determinate :
 Proof.
   intros. constructor; set (ge := Globalenvs.Genv.globalenv p); simplify.
   - invert H; invert H0; constructor. (* Traces are always empty *)
-  - invert H; invert H0; crush.
-    (*pose proof (mis_stepp_determinate H4 H13)*)
-    admit.
+  - invert H; invert H0; crush. assert (f = f0) by admit; subst.
+    pose proof (mis_stepp_determinate H5 H15).
+    crush.
   - constructor. invert H; crush.
   - invert H; invert H0; unfold ge0, ge1 in *; crush.
   - red; simplify; intro; invert H0; invert H; crush.