Add RTLBlock intermediate language

5 files changed, 0 insertions, 4411 deletions

diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v
deleted file mode 100644
index 68e0293..0000000
--- a/src/translation/HTLgen.v
+++ /dev/null
@@ -1,654 +0,0 @@
-(* 
- * Vericert: 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/>.
- *)
-
-From compcert Require Import Maps.
-From compcert Require Errors Globalenvs Integers.
-From compcert Require Import AST RTL.
-From vericert Require Import Verilog HTL Vericertlib AssocMap ValueInt Statemonad.
-
-Hint Resolve AssocMap.gempty : htlh.
-Hint Resolve AssocMap.gso : htlh.
-Hint Resolve AssocMap.gss : htlh.
-Hint Resolve Ple_refl : htlh.
-Hint Resolve Ple_succ : htlh.
-
-Record state: Type := mkstate {
-  st_st : reg;
-  st_freshreg: reg;
-  st_freshstate: node;
-  st_scldecls: AssocMap.t (option io * scl_decl);
-  st_arrdecls: AssocMap.t (option io * arr_decl);
-  st_datapath: datapath;
-  st_controllogic: controllogic;
-}.
-
-Definition init_state (st : reg) : state :=
-  mkstate st
-          1%positive
-          1%positive
-          (AssocMap.empty (option io * scl_decl))
-          (AssocMap.empty (option io * arr_decl))
-          (AssocMap.empty stmnt)
-          (AssocMap.empty stmnt).
-
-Module HTLState <: State.
-
-  Definition st := state.
-
-  Inductive st_incr: state -> state -> Prop :=
-    state_incr_intro:
-      forall (s1 s2: state),
-        st_st s1 = st_st s2 ->
-        Ple s1.(st_freshreg) s2.(st_freshreg) ->
-        Ple s1.(st_freshstate) s2.(st_freshstate) ->
-        (forall n,
-            s1.(st_datapath)!n = None \/ s2.(st_datapath)!n = s1.(st_datapath)!n) ->
-        (forall n,
-            s1.(st_controllogic)!n = None
-            \/ s2.(st_controllogic)!n = s1.(st_controllogic)!n) ->
-        st_incr s1 s2.
-  Hint Constructors st_incr : htlh.
-
-  Definition st_prop := st_incr.
-  Hint Unfold st_prop : htlh.
-
-  Lemma st_refl : forall s, st_prop s s. Proof. auto with htlh. Qed.
-
-  Lemma st_trans :
-    forall s1 s2 s3, st_prop s1 s2 -> st_prop s2 s3 -> st_prop s1 s3.
-  Proof.
-    intros. inv H. inv H0. apply state_incr_intro; eauto using Ple_trans; intros; try congruence.
-    - destruct H4 with n; destruct H8 with n; intuition congruence.
-    - destruct H5 with n; destruct H9 with n; intuition congruence.
-  Qed.
-
-End HTLState.
-Export HTLState.
-
-Module HTLMonad := Statemonad(HTLState).
-Export HTLMonad.
-
-Module HTLMonadExtra := Monad.MonadExtra(HTLMonad).
-Import HTLMonadExtra.
-Export MonadNotation.
-
-Definition state_goto (st : reg) (n : node) : stmnt :=
-  Vnonblock (Vvar st) (Vlit (posToValue n)).
-
-Definition state_cond (st : reg) (c : expr) (n1 n2 : node) : stmnt :=
-  Vnonblock (Vvar st) (Vternary c (posToExpr n1) (posToExpr n2)).
-
-Definition check_empty_node_datapath:
-  forall (s: state) (n: node), { s.(st_datapath)!n = None } + { True }.
-Proof.
-  intros. case (s.(st_datapath)!n); tauto.
-Defined.
-
-Definition check_empty_node_controllogic:
-  forall (s: state) (n: node), { s.(st_controllogic)!n = None } + { True }.
-Proof.
-  intros. case (s.(st_controllogic)!n); tauto.
-Defined.
-
-Lemma add_instr_state_incr :
-  forall s n n' st,
-    (st_datapath s)!n = None ->
-    (st_controllogic s)!n = None ->
-    st_incr s
-    (mkstate
-       s.(st_st)
-       s.(st_freshreg)
-       (st_freshstate s)
-       s.(st_scldecls)
-       s.(st_arrdecls)
-       (AssocMap.set n st s.(st_datapath))
-       (AssocMap.set n (state_goto s.(st_st) n') s.(st_controllogic))).
-Proof.
-  constructor; intros;
-    try (simpl; destruct (peq n n0); subst);
-    auto with htlh.
-Qed.
-
-Lemma declare_reg_state_incr :
-  forall i s r sz,
-    st_incr s
-    (mkstate
-       s.(st_st)
-       s.(st_freshreg)
-       s.(st_freshstate)
-       (AssocMap.set r (i, VScalar sz) s.(st_scldecls))
-       s.(st_arrdecls)
-       s.(st_datapath)
-       s.(st_controllogic)).
-Proof. auto with htlh. Qed.
-
-Definition declare_reg (i : option io) (r : reg) (sz : nat) : mon unit :=
-  fun s => OK tt (mkstate
-                s.(st_st)
-                s.(st_freshreg)
-                s.(st_freshstate)
-                (AssocMap.set r (i, VScalar sz) s.(st_scldecls))
-                s.(st_arrdecls)
-                s.(st_datapath)
-                s.(st_controllogic))
-              (declare_reg_state_incr i s r sz).
-
-Definition add_instr (n : node) (n' : node) (st : stmnt) : mon unit :=
-  fun s =>
-    match check_empty_node_datapath s n, check_empty_node_controllogic s n with
-    | left STM, left TRANS =>
-      OK tt (mkstate
-               s.(st_st)
-               s.(st_freshreg)
-               (st_freshstate s)
-               s.(st_scldecls)
-               s.(st_arrdecls)
-               (AssocMap.set n st s.(st_datapath))
-               (AssocMap.set n (state_goto s.(st_st) n') s.(st_controllogic)))
-         (add_instr_state_incr s n n' st STM TRANS)
-    | _, _ => Error (Errors.msg "HTL.add_instr")
-    end.
-
-Lemma add_instr_skip_state_incr :
-  forall s n st,
-    (st_datapath s)!n = None ->
-    (st_controllogic s)!n = None ->
-    st_incr s
-    (mkstate
-       s.(st_st)
-       s.(st_freshreg)
-       (st_freshstate s)
-       s.(st_scldecls)
-       s.(st_arrdecls)
-       (AssocMap.set n st s.(st_datapath))
-       (AssocMap.set n Vskip s.(st_controllogic))).
-Proof.
-  constructor; intros;
-    try (simpl; destruct (peq n n0); subst);
-    auto with htlh.
-Qed.
-
-Definition add_instr_skip (n : node) (st : stmnt) : mon unit :=
-  fun s =>
-    match check_empty_node_datapath s n, check_empty_node_controllogic s n with
-    | left STM, left TRANS =>
-      OK tt (mkstate
-               s.(st_st)
-               s.(st_freshreg)
-               (st_freshstate s)
-               s.(st_scldecls)
-               s.(st_arrdecls)
-               (AssocMap.set n st s.(st_datapath))
-               (AssocMap.set n Vskip s.(st_controllogic)))
-         (add_instr_skip_state_incr s n st STM TRANS)
-    | _, _ => Error (Errors.msg "HTL.add_instr")
-    end.
-
-Lemma add_node_skip_state_incr :
-  forall s n st,
-    (st_datapath s)!n = None ->
-    (st_controllogic s)!n = None ->
-    st_incr s
-    (mkstate
-       s.(st_st)
-       s.(st_freshreg)
-       (st_freshstate s)
-       s.(st_scldecls)
-       s.(st_arrdecls)
-       (AssocMap.set n Vskip s.(st_datapath))
-       (AssocMap.set n st s.(st_controllogic))).
-Proof.
-  constructor; intros;
-    try (simpl; destruct (peq n n0); subst);
-    auto with htlh.
-Qed.
-
-Definition add_node_skip (n : node) (st : stmnt) : mon unit :=
-  fun s =>
-    match check_empty_node_datapath s n, check_empty_node_controllogic s n with
-    | left STM, left TRANS =>
-      OK tt (mkstate
-               s.(st_st)
-               s.(st_freshreg)
-               (st_freshstate s)
-               s.(st_scldecls)
-               s.(st_arrdecls)
-               (AssocMap.set n Vskip s.(st_datapath))
-               (AssocMap.set n st s.(st_controllogic)))
-         (add_node_skip_state_incr s n st STM TRANS)
-    | _, _ => Error (Errors.msg "HTL.add_instr")
-    end.
-
-Definition nonblock (dst : reg) (e : expr) := Vnonblock (Vvar dst) e.
-Definition block (dst : reg) (e : expr) := Vblock (Vvar dst) e.
-
-Definition bop (op : binop) (r1 r2 : reg) : expr :=
-  Vbinop op (Vvar r1) (Vvar r2).
-
-Definition boplit (op : binop) (r : reg) (l : Integers.int) : expr :=
-  Vbinop op (Vvar r) (Vlit (intToValue l)).
-
-Definition boplitz (op: binop) (r: reg) (l: Z) : expr :=
-  Vbinop op (Vvar r) (Vlit (ZToValue l)).
-
-Definition translate_comparison (c : Integers.comparison) (args : list reg) : mon expr :=
-  match c, args with
-  | Integers.Ceq, r1::r2::nil => ret (bop Veq r1 r2)
-  | Integers.Cne, r1::r2::nil => ret (bop Vne r1 r2)
-  | Integers.Clt, r1::r2::nil => ret (bop Vlt r1 r2)
-  | Integers.Cgt, r1::r2::nil => ret (bop Vgt r1 r2)
-  | Integers.Cle, r1::r2::nil => ret (bop Vle r1 r2)
-  | Integers.Cge, r1::r2::nil => ret (bop Vge r1 r2)
-  | _, _ => error (Errors.msg "Htlgen: comparison instruction not implemented: other")
-  end.
-
-Definition translate_comparison_imm (c : Integers.comparison) (args : list reg) (i: Integers.int)
-  : mon expr :=
-  match c, args with
-  | Integers.Ceq, r1::nil => ret (boplit Veq r1 i)
-  | Integers.Cne, r1::nil => ret (boplit Vne r1 i)
-  | Integers.Clt, r1::nil => ret (boplit Vlt r1 i)
-  | Integers.Cgt, r1::nil => ret (boplit Vgt r1 i)
-  | Integers.Cle, r1::nil => ret (boplit Vle r1 i)
-  | Integers.Cge, r1::nil => ret (boplit Vge r1 i)
-  | _, _ => error (Errors.msg "Htlgen: comparison_imm instruction not implemented: other")
-  end.
-
-Definition translate_comparisonu (c : Integers.comparison) (args : list reg) : mon expr :=
-  match c, args with
-  | Integers.Clt, r1::r2::nil => ret (bop Vltu r1 r2)
-  | Integers.Cgt, r1::r2::nil => ret (bop Vgtu r1 r2)
-  | Integers.Cle, r1::r2::nil => ret (bop Vleu r1 r2)
-  | Integers.Cge, r1::r2::nil => ret (bop Vgeu r1 r2)
-  | _, _ => error (Errors.msg "Htlgen: comparison instruction not implemented: other")
-  end.
-
-Definition translate_comparison_immu (c : Integers.comparison) (args : list reg) (i: Integers.int)
-  : mon expr :=
-  match c, args with
-  | Integers.Clt, r1::nil => ret (boplit Vltu r1 i)
-  | Integers.Cgt, r1::nil => ret (boplit Vgtu r1 i)
-  | Integers.Cle, r1::nil => ret (boplit Vleu r1 i)
-  | Integers.Cge, r1::nil => ret (boplit Vgeu r1 i)
-  | _, _ => error (Errors.msg "Htlgen: comparison_imm instruction not implemented: other")
-  end.
-
-Definition translate_condition (c : Op.condition) (args : list reg) : mon expr :=
-  match c, args with
-  | Op.Ccomp c, _ => translate_comparison c args
-  | Op.Ccompu c, _ => translate_comparisonu c args
-  | Op.Ccompimm c i, _ => translate_comparison_imm c args i
-  | Op.Ccompuimm c i, _ => translate_comparison_immu c args i
-  | Op.Cmaskzero n, _ => error (Errors.msg "Htlgen: condition instruction not implemented: Cmaskzero")
-  | Op.Cmasknotzero n, _ => error (Errors.msg "Htlgen: condition instruction not implemented: Cmasknotzero")
-  | _, _ => error (Errors.msg "Htlgen: condition instruction not implemented: other")
-  end.
-
-Definition check_address_parameter_signed (p : Z) : bool :=
-  Z.leb Integers.Ptrofs.min_signed p
-  && Z.leb p Integers.Ptrofs.max_signed.
-
-Definition check_address_parameter_unsigned (p : Z) : bool :=
-  Z.leb p Integers.Ptrofs.max_unsigned.
-
-Definition translate_eff_addressing (a: Op.addressing) (args: list reg) : mon expr :=
-  match a, args with (* TODO: We should be more methodical here; what are the possibilities?*)
-  | Op.Aindexed off, r1::nil =>
-    if (check_address_parameter_signed off)
-    then ret (boplitz Vadd r1 off)
-    else error (Errors.msg "Veriloggen: translate_eff_addressing (Aindexed): address out of bounds")
-  | Op.Ascaled scale offset, r1::nil =>
-    if (check_address_parameter_signed scale) && (check_address_parameter_signed offset)
-    then ret (Vbinop Vadd (boplitz Vmul r1 scale) (Vlit (ZToValue offset)))
-    else error (Errors.msg "Veriloggen: translate_eff_addressing (Ascaled): address out of bounds")
-  | Op.Aindexed2 offset, r1::r2::nil =>
-    if (check_address_parameter_signed offset)
-    then ret (Vbinop Vadd (bop Vadd r1 r2) (Vlit (ZToValue offset)))
-    else error (Errors.msg "Veriloggen: translate_eff_addressing (Aindexed2): address out of bounds")
-  | Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *)
-    if (check_address_parameter_signed scale) && (check_address_parameter_signed offset)
-    then ret (Vbinop Vadd (Vvar r1) (Vbinop Vadd (boplitz Vmul r2 scale) (Vlit (ZToValue offset))))
-    else error (Errors.msg "Veriloggen: translate_eff_addressing (Aindexed2scaled): address out of bounds")
-  | Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *)
-    let a := Integers.Ptrofs.unsigned a in
-    if (check_address_parameter_unsigned a)
-    then ret (Vlit (ZToValue a))
-    else error (Errors.msg "Veriloggen: translate_eff_addressing (Ainstack): address out of bounds")
-  | _, _ => error (Errors.msg "Veriloggen: translate_eff_addressing unsuported addressing")
-  end.
-
-(** Translate an instruction to a statement. FIX mulhs mulhu *)
-Definition translate_instr (op : Op.operation) (args : list reg) : mon expr :=
-  match op, args with
-  | Op.Omove, r::nil => ret (Vvar r)
-  | Op.Ointconst n, _ => ret (Vlit (intToValue n))
-  | Op.Oneg, r::nil => ret (Vunop Vneg (Vvar r))
-  | Op.Osub, r1::r2::nil => ret (bop Vsub r1 r2)
-  | Op.Omul, r1::r2::nil => ret (bop Vmul r1 r2)
-  | Op.Omulimm n, r::nil => ret (boplit Vmul r n)
-  | Op.Omulhs, r1::r2::nil => error (Errors.msg "Htlgen: Instruction not implemented: mulhs")
-  | Op.Omulhu, r1::r2::nil => error (Errors.msg "Htlgen: Instruction not implemented: mulhu")
-  | Op.Odiv, r1::r2::nil => ret (bop Vdiv r1 r2)
-  | Op.Odivu, r1::r2::nil => ret (bop Vdivu r1 r2)
-  | Op.Omod, r1::r2::nil => ret (bop Vmod r1 r2)
-  | Op.Omodu, r1::r2::nil => ret (bop Vmodu r1 r2)
-  | Op.Oand, r1::r2::nil => ret (bop Vand r1 r2)
-  | Op.Oandimm n, r::nil => ret (boplit Vand r n)
-  | Op.Oor, r1::r2::nil => ret (bop Vor r1 r2)
-  | Op.Oorimm n, r::nil => ret (boplit Vor r n)
-  | Op.Oxor, r1::r2::nil => ret (bop Vxor r1 r2)
-  | Op.Oxorimm n, r::nil => ret (boplit Vxor r n)
-  | Op.Onot, r::nil => ret (Vunop Vnot (Vvar r))
-  | Op.Oshl, r1::r2::nil => ret (bop Vshl r1 r2)
-  | Op.Oshlimm n, r::nil => ret (boplit Vshl r n)
-  | Op.Oshr, r1::r2::nil => ret (bop Vshr r1 r2)
-  | Op.Oshrimm n, r::nil => ret (boplit Vshr r n)
-  | Op.Oshrximm n, r::nil => error (Errors.msg "Htlgen: Instruction not implemented: Oshrximm")
-  (*ret (Vbinop Vdiv (Vvar r)
-    (Vbinop Vshl (Vlit (ZToValue 1))
-    (Vlit (intToValue n))))*)
-  | Op.Oshru, r1::r2::nil => ret (bop Vshru r1 r2)
-  | Op.Oshruimm n, r::nil => ret (boplit Vshru r n)
-  | Op.Ororimm n, r::nil => error (Errors.msg "Htlgen: Instruction not implemented: Ororimm")
-  (*ret (Vbinop Vor (boplit Vshru r (Integers.Int.modu n (Integers.Int.repr 32)))
-                                        (boplit Vshl r (Integers.Int.sub (Integers.Int.repr 32) (Integers.Int.modu n (Integers.Int.repr 32)))))*)
-  | Op.Oshldimm n, r::nil => ret (Vbinop Vor (boplit Vshl r n) (boplit Vshr r (Integers.Int.sub (Integers.Int.repr 32) n)))
-  | Op.Ocmp c, _ => translate_condition c args
-  | Op.Osel c AST.Tint, r1::r2::rl =>
-    do tc <- translate_condition c rl;
-    ret (Vternary tc (Vvar r1) (Vvar r2))
-  | Op.Olea a, _ => translate_eff_addressing a args
-  | _, _ => error (Errors.msg "Htlgen: Instruction not implemented: other")
-  end.
-
-Lemma add_branch_instr_state_incr:
-  forall s e n n1 n2,
-    (st_datapath s) ! n = None ->
-    (st_controllogic s) ! n = None ->
-    st_incr s (mkstate
-                 s.(st_st)
-                (st_freshreg s)
-                (st_freshstate s)
-                s.(st_scldecls)
-                s.(st_arrdecls)
-                (AssocMap.set n Vskip (st_datapath s))
-                (AssocMap.set n (state_cond s.(st_st) e n1 n2) (st_controllogic s))).
-Proof.
-  intros. apply state_incr_intro; simpl;
-            try (intros; destruct (peq n0 n); subst);
-            auto with htlh.
-Qed.
-
-Definition add_branch_instr (e: expr) (n n1 n2: node) : mon unit :=
-  fun s =>
-    match check_empty_node_datapath s n, check_empty_node_controllogic s n with
-    | left NSTM, left NTRANS =>
-      OK tt (mkstate
-               s.(st_st)
-                (st_freshreg s)
-                (st_freshstate s)
-                s.(st_scldecls)
-                s.(st_arrdecls)
-                (AssocMap.set n Vskip (st_datapath s))
-                (AssocMap.set n (state_cond s.(st_st) e n1 n2) (st_controllogic s)))
-         (add_branch_instr_state_incr s e n n1 n2 NSTM NTRANS)
-    | _, _ => Error (Errors.msg "Htlgen: add_branch_instr")
-    end.
-
-Definition translate_arr_access (mem : AST.memory_chunk) (addr : Op.addressing)
-           (args : list reg) (stack : reg) : mon expr :=
-  match mem, addr, args with (* TODO: We should be more methodical here; what are the possibilities?*)
-  | Mint32, Op.Aindexed off, r1::nil =>
-    if (check_address_parameter_signed off)
-    then ret (Vvari stack (Vbinop Vdivu (boplitz Vadd r1 off) (Vlit (ZToValue 4))))
-    else error (Errors.msg "HTLgen: translate_arr_access address out of bounds")
-  | Mint32, Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *)
-    if (check_address_parameter_signed scale) && (check_address_parameter_signed offset)
-    then ret (Vvari stack
-                    (Vbinop Vdivu
-                            (Vbinop Vadd (boplitz Vadd r1 offset) (boplitz Vmul r2 scale))
-                            (Vlit (ZToValue 4))))
-    else error (Errors.msg "HTLgen: translate_arr_access address out of bounds")
-  | Mint32, Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *)
-    let a := Integers.Ptrofs.unsigned a in
-    if (check_address_parameter_unsigned a)
-    then ret (Vvari stack (Vlit (ZToValue (a / 4))))
-    else error (Errors.msg "HTLgen: eff_addressing out of bounds stack offset")
-  | _, _, _ => error (Errors.msg "HTLgen: translate_arr_access unsuported addressing")
-  end.
-
-Fixpoint enumerate (i : nat) (ns : list node) {struct ns} : list (nat * node) :=
-  match ns with
-  | n :: ns' => (i, n) :: enumerate (i+1) ns'
-  | nil => nil
-  end.
-
-Definition tbl_to_case_expr (st : reg) (ns : list node) : list (expr * stmnt) :=
-  List.map (fun a => match a with
-                    (i, n) => (Vlit (natToValue i), Vnonblock (Vvar st) (Vlit (posToValue n)))
-                  end)
-           (enumerate 0 ns).
-
-Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon unit :=
-  match ni with
-    (n, i) =>
-    match i with
-    | 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' =>
-      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' =>
-      if Z.leb (Z.pos n') Integers.Int.max_unsigned then
-        do src <- translate_arr_access mem addr args stack;
-        do _ <- declare_reg None dst 32;
-        add_instr n n' (nonblock dst src)
-      else error (Errors.msg "State is larger than 2^32.")
-    | Istore mem addr args src n' =>
-      if Z.leb (Z.pos n') Integers.Int.max_unsigned then
-        do dst <- translate_arr_access mem addr args stack;
-        add_instr n n' (Vnonblock dst (Vvar src)) (* TODO: Could juse use add_instr? reg exists. *)
-      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 =>
-      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))*)
-      error (Errors.msg "Ijumptable: Case statement not supported.")
-    | Ireturn r =>
-      match r with
-      | Some r' =>
-        add_instr_skip n (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vvar r')))
-      | None =>
-        add_instr_skip n (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vlit (ZToValue 0%Z))))
-      end
-    end
-  end.
-
-Lemma create_reg_state_incr:
-  forall s sz i,
-    st_incr s (mkstate
-         s.(st_st)
-         (Pos.succ (st_freshreg s))
-         (st_freshstate s)
-         (AssocMap.set s.(st_freshreg) (i, VScalar sz) s.(st_scldecls))
-         s.(st_arrdecls)
-         (st_datapath s)
-         (st_controllogic s)).
-Proof. constructor; simpl; auto with htlh. Qed.
-
-Definition create_reg (i : option io) (sz : nat) : mon reg :=
-  fun s => let r := s.(st_freshreg) in
-           OK r (mkstate
-                   s.(st_st)
-                   (Pos.succ r)
-                   (st_freshstate s)
-                   (AssocMap.set s.(st_freshreg) (i, VScalar sz) s.(st_scldecls))
-                   (st_arrdecls s)
-                   (st_datapath s)
-                   (st_controllogic s))
-              (create_reg_state_incr s sz i).
-
-Lemma create_arr_state_incr:
-  forall s sz ln i,
-    st_incr s (mkstate
-         s.(st_st)
-         (Pos.succ (st_freshreg s))
-         (st_freshstate s)
-         s.(st_scldecls)
-         (AssocMap.set s.(st_freshreg) (i, VArray sz ln) s.(st_arrdecls))
-         (st_datapath s)
-         (st_controllogic s)).
-Proof. constructor; simpl; auto with htlh. Qed.
-
-Definition create_arr (i : option io) (sz : nat) (ln : nat) : mon (reg * nat) :=
-  fun s => let r := s.(st_freshreg) in
-           OK (r, ln) (mkstate
-                   s.(st_st)
-                   (Pos.succ r)
-                   (st_freshstate s)
-                   s.(st_scldecls)
-                   (AssocMap.set s.(st_freshreg) (i, VArray sz ln) s.(st_arrdecls))
-                   (st_datapath s)
-                   (st_controllogic s))
-              (create_arr_state_incr s sz ln i).
-
-Definition stack_correct (sz : Z) : bool :=
-  (0 <=? sz) && (sz <? Integers.Ptrofs.modulus) && (Z.modulo sz 4 =? 0).
-
-Definition max_pc_map (m : Maps.PTree.t stmnt) :=
-  PTree.fold (fun m pc i => Pos.max m pc) m 1%positive.
-
-Lemma max_pc_map_sound:
-  forall m pc i, m!pc = Some i -> Ple pc (max_pc_map m).
-Proof.
-  intros until i. unfold max_pc_function.
-  apply PTree_Properties.fold_rec with (P := fun c m => c!pc = Some i -> Ple pc m).
-  (* extensionality *)
-  intros. apply H0. rewrite H; auto.
-  (* base case *)
-  rewrite PTree.gempty. congruence.
-  (* inductive case *)
-  intros. rewrite PTree.gsspec in H2. destruct (peq pc k).
-  inv H2. xomega.
-  apply Ple_trans with a. auto. xomega.
-Qed.
-
-Lemma max_pc_wf :
-  forall m, Z.pos (max_pc_map m) <= Integers.Int.max_unsigned ->
-            map_well_formed m.
-Proof.
-  unfold map_well_formed. intros.
-  exploit list_in_map_inv. eassumption. intros [x [A B]]. destruct x.
-  apply Maps.PTree.elements_complete in B. apply max_pc_map_sound in B.
-  unfold Ple in B. apply Pos2Z.pos_le_pos in B. subst.
-  simplify. transitivity (Z.pos (max_pc_map m)); eauto.
-Qed.
-
-Definition transf_module (f: function) : mon module :=
-  if stack_correct f.(fn_stacksize) then
-    do fin <- create_reg (Some Voutput) 1;
-    do rtrn <- create_reg (Some Voutput) 32;
-    do (stack, stack_len) <- create_arr None 32 (Z.to_nat (f.(fn_stacksize) / 4));
-    do _ <- collectlist (transf_instr fin rtrn stack) (Maps.PTree.elements f.(RTL.fn_code));
-    do _ <- collectlist (fun r => declare_reg (Some Vinput) r 32) f.(RTL.fn_params);
-    do start <- create_reg (Some Vinput) 1;
-    do rst <- create_reg (Some Vinput) 1;
-    do clk <- create_reg (Some Vinput) 1;
-    do current_state <- get;
-    match zle (Z.pos (max_pc_map current_state.(st_datapath))) Integers.Int.max_unsigned,
-          zle (Z.pos (max_pc_map current_state.(st_controllogic))) Integers.Int.max_unsigned with
-    | left LEDATA, left LECTRL =>
-        ret (mkmodule
-           f.(RTL.fn_params)
-           current_state.(st_datapath)
-           current_state.(st_controllogic)
-           f.(fn_entrypoint)
-           current_state.(st_st)
-           stack
-           stack_len
-           fin
-           rtrn
-           start
-           rst
-           clk
-           current_state.(st_scldecls)
-           current_state.(st_arrdecls)
-           (conj (max_pc_wf _ LECTRL) (max_pc_wf _ LEDATA)))
-    | _, _ => error (Errors.msg "More than 2^32 states.")
-    end
-  else error (Errors.msg "Stack size misalignment.").
-
-Definition max_state (f: function) : state :=
-  let st := Pos.succ (max_reg_function f) in
-  mkstate st
-          (Pos.succ st)
-          (Pos.succ (max_pc_function f))
-          (AssocMap.set st (None, VScalar 32) (st_scldecls (init_state st)))
-          (st_arrdecls (init_state st))
-          (st_datapath (init_state st))
-          (st_controllogic (init_state st)).
-
-Definition transl_module (f : function) : Errors.res module :=
-  run_mon (max_state f) (transf_module f).
-
-Definition transl_fundef := transf_partial_fundef transl_module.
-
-(* Definition transl_program (p : RTL.program) := transform_partial_program transl_fundef p. *)
-
-(*Definition transl_main_fundef f : Errors.res HTL.fundef :=
-  match f with
-  | Internal f => transl_fundef (Internal f)
-  | External f => Errors.Error (Errors.msg "Could not find internal main function")
-  end.
-
-(** Translation of a whole program. *)
-
-Definition transl_program (p: RTL.program) : Errors.res HTL.program :=
-  transform_partial_program2 (fun i f => if Pos.eqb p.(AST.prog_main) i
-                                         then transl_fundef f
-                                         else transl_main_fundef f)
-                             (fun i v => Errors.OK v) p.
-*)
-
-Definition main_is_internal (p : RTL.program) : bool :=
-  let ge := Globalenvs.Genv.globalenv p in
-  match Globalenvs.Genv.find_symbol ge p.(AST.prog_main) with
-  | Some b =>
-    match Globalenvs.Genv.find_funct_ptr ge b with
-    | Some (AST.Internal _) => true
-    | _ => false
-    end
-  | _ => false
-  end.
-
-Definition transl_program (p : RTL.program) : Errors.res HTL.program :=
-  if main_is_internal p
-  then transform_partial_program transl_fundef p
-  else Errors.Error (Errors.msg "Main function is not Internal.").
diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v
deleted file mode 100644
index bf63800..0000000
--- a/src/translation/HTLgenproof.v
+++ /dev/null
@@ -1,2683 +0,0 @@
-(*
- * Vericert: 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/>.
- *)
-
-From compcert Require RTL Registers AST.
-From compcert Require Import Integers Globalenvs Memory Linking.
-From vericert Require Import Vericertlib HTLgenspec HTLgen ValueInt AssocMap Array IntegerExtra ZExtra.
-From vericert Require HTL Verilog.
-
-Require Import Lia.
-
-Local Open Scope assocmap.
-
-Hint Resolve Smallstep.forward_simulation_plus : htlproof.
-Hint Resolve AssocMap.gss : htlproof.
-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.
-
-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.
-
-Instance TransfHTLLink (tr_fun: RTL.program -> Errors.res HTL.program):
-  TransfLink (fun (p1: RTL.program) (p2: HTL.program) => match_prog p1 p2).
-Proof.
-  red. intros. exfalso. destruct (link_linkorder _ _ _ H) as [LO1 LO2].
-  apply link_prog_inv in H.
-
-  unfold match_prog in *.
-  unfold main_is_internal in *. simplify. repeat (unfold_match H4).
-  repeat (unfold_match H3). simplify.
-  subst. rewrite H0 in *. specialize (H (AST.prog_main p2)).
-  exploit H.
-  apply Genv.find_def_symbol. exists b. split.
-  assumption. apply Genv.find_funct_ptr_iff. eassumption.
-  apply Genv.find_def_symbol. exists b0. split.
-  assumption. apply Genv.find_funct_ptr_iff. eassumption.
-  intros. inv H3. inv H5. destruct H6. inv H5.
-Qed.
-
-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.
-
-Lemma match_prog_matches :
-  forall p tp, match_prog p tp -> match_prog' p tp.
-Proof. unfold match_prog. 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 op_stack_based :
-    forall F V sp v m args rs op ge pc' res0 pc f e fin rtrn st stk,
-      tr_instr fin rtrn st stk (RTL.Iop op args res0 pc')
-               (Verilog.Vnonblock (Verilog.Vvar res0) e)
-               (state_goto st pc') ->
-      reg_stack_based_pointers sp rs ->
-      (RTL.fn_code f) ! pc = Some (RTL.Iop op args res0 pc') ->
-      @Op.eval_operation F V ge (Values.Vptr sp Ptrofs.zero) op
-                        (map (fun r : positive => Registers.Regmap.get r rs) args) m = Some v ->
-      stack_based v sp.
-  Proof.
-    Ltac solve_no_ptr :=
-      match goal with
-      | H: reg_stack_based_pointers ?sp ?rs |- stack_based (Registers.Regmap.get ?r ?rs) _ =>
-        solve [apply H]
-      | H1: reg_stack_based_pointers ?sp ?rs, H2: Registers.Regmap.get _ _ = Values.Vptr ?b ?i
-        |- context[Values.Vptr ?b _] =>
-        let H := fresh "H" in
-        assert (H: stack_based (Values.Vptr b i) sp) by (rewrite <- H2; apply H1); simplify; solve [auto]
-      | |- context[Registers.Regmap.get ?lr ?lrs] =>
-        destruct (Registers.Regmap.get lr lrs) eqn:?; simplify; auto
-      | |- stack_based (?f _) _ => unfold f
-      | |- stack_based (?f _ _) _ => unfold f
-      | |- stack_based (?f _ _ _) _ => unfold f
-      | |- stack_based (?f _ _ _ _) _ => unfold f
-      | H: ?f _ _ = Some _ |- _ =>
-        unfold f in H; repeat (unfold_match H); inv H
-      | H: ?f _ _ _ _ _ _ = Some _ |- _ =>
-        unfold f in H; repeat (unfold_match H); inv H
-      | H: map (fun r : positive => Registers.Regmap.get r _) ?args = _ |- _ =>
-        destruct args; inv H
-      | |- context[if ?c then _ else _] => destruct c; try discriminate
-      | H: match _ with _ => _ end = Some _ |- _ => repeat (unfold_match H)
-      | H: match _ with _ => _ end = OK _ _ _ |- _ => repeat (unfold_match H)
-      | |- context[match ?g with _ => _ end] => destruct g; try discriminate
-      | |- _ => simplify; solve [auto]
-      end.
-    intros F V sp v m args rs op g pc' res0 pc f e fin rtrn st stk INSTR RSBP SEL EVAL.
-    inv INSTR. unfold translate_instr in H5.
-    unfold_match H5; repeat (unfold_match H5); repeat (simplify; solve_no_ptr).
-  Qed.
-
-  Lemma int_inj :
-    forall x y,
-      Int.unsigned x = Int.unsigned y ->
-      x = y.
-  Proof.
-    intros. rewrite <- Int.repr_unsigned at 1. rewrite <- Int.repr_unsigned.
-    rewrite <- H. trivial.
-  Qed.
-
-  Ltac eval_correct_tac :=
-      match goal with
-      | |- context[valueToPtr] => unfold valueToPtr
-      | |- context[valueToInt] => unfold valueToInt
-      | |- context[bop] => unfold bop
-      | H : context[bop] |- _ => unfold bop in H
-      | |- context[boplit] => unfold boplit
-      | H : context[boplit] |- _ => unfold boplit in H
-      | |- context[boplitz] => unfold boplitz
-      | H : context[boplitz] |- _ => unfold boplitz in H
-      | |- val_value_lessdef Values.Vundef _ => solve [constructor]
-      | H : val_value_lessdef _ _ |- val_value_lessdef (Values.Vint _) _ => constructor; inv H
-      | |- val_value_lessdef (Values.Vint _) _ => constructor; auto
-      | H : ret _ _ = OK _ _ _ |- _ => inv H
-      | H : context[RTL.max_reg_function ?f]
-        |- context[_ (Registers.Regmap.get ?r ?rs) (Registers.Regmap.get ?r0 ?rs)] =>
-        let HPle1 := fresh "HPle" in
-        let HPle2 := fresh "HPle" in
-        assert (HPle1 : Ple r (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto);
-        assert (HPle2 : Ple r0 (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto);
-        apply H in HPle1; apply H in HPle2; eexists; split;
-        [econstructor; eauto; constructor; trivial | inv HPle1; inv HPle2; try (constructor; auto)]
-      | H : context[RTL.max_reg_function ?f]
-        |- context[_ (Registers.Regmap.get ?r ?rs) _] =>
-        let HPle1 := fresh "HPle" in
-        assert (HPle1 : Ple r (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto);
-        apply H in HPle1; eexists; split;
-        [econstructor; eauto; constructor; trivial | inv HPle1; try (constructor; auto)]
-      | H : _ :: _ = _ :: _ |- _ => inv H
-      | |- context[match ?d with _ => _ end] => destruct d eqn:?; try discriminate
-      | H : match ?d with _ => _ end = _ |- _ => repeat unfold_match H
-      | H : match ?d with _ => _ end _ = _ |- _ => repeat unfold_match H
-      | |- Verilog.expr_runp _ _ _ _ _ => econstructor
-      | |- val_value_lessdef (?f _ _) _ => unfold f
-      | |- val_value_lessdef (?f _) _ => unfold f
-      | H : ?f (Registers.Regmap.get _ _) _ = Some _ |- _ =>
-        unfold f in H; repeat (unfold_match H)
-      | H1 : Registers.Regmap.get ?r ?rs = Values.Vint _, H2 : val_value_lessdef (Registers.Regmap.get ?r ?rs) _
-        |- _ => rewrite H1 in H2; inv H2
-      | |- _ => eexists; split; try constructor; solve [eauto]
-      | H : context[RTL.max_reg_function ?f] |- context[_ (Verilog.Vvar ?r) (Verilog.Vvar ?r0)] =>
-        let HPle1 := fresh "H" in
-        let HPle2 := fresh "H" in
-        assert (HPle1 : Ple r (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto);
-        assert (HPle2 : Ple r0 (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto);
-        apply H in HPle1; apply H in HPle2; eexists; split; try constructor; eauto
-      | H : context[RTL.max_reg_function ?f] |- context[Verilog.Vvar ?r] =>
-        let HPle := fresh "H" in
-        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
-      | |- context[if ?c then _ else _] => destruct c eqn:?; try discriminate
-      | H : ?b = _ |- _ = boolToValue ?b => rewrite H
-      end.
-      Ltac inv_lessdef := lazymatch goal with
-      | H2 : context[RTL.max_reg_function ?f],
-        H : Registers.Regmap.get ?r ?rs = _,
-        H1 : Registers.Regmap.get ?r0 ?rs = _ |- _ =>
-        let HPle1 := fresh "HPle" in
-        assert (HPle1 : Ple r (RTL.max_reg_function f))
-          by (eapply RTL.max_reg_function_use; eauto; simpl; auto);
-        apply H2 in HPle1; inv HPle1;
-        let HPle2 := fresh "HPle" in
-        assert (HPle2 : Ple r0 (RTL.max_reg_function f))
-          by (eapply RTL.max_reg_function_use; eauto; simpl; auto);
-        apply H2 in HPle2; inv HPle2
-      | H2 : context[RTL.max_reg_function ?f], H : Registers.Regmap.get ?r ?rs = _ |- _ =>
-        let HPle1 := fresh "HPle" in
-        assert (HPle1 : Ple r (RTL.max_reg_function f))
-          by (eapply RTL.max_reg_function_use; eauto; simpl; auto);
-        apply H2 in HPle1; inv HPle1
-      end.
-      Ltac solve_cond :=
-        match goal with
-        | H : context[match _ with _ => _ end] |- _ => repeat (unfold_merge H)
-        | H : ?f = _ |- context[boolToValue ?f] => rewrite H; solve [auto]
-        | H : Values.Vptr _ _ = Registers.Regmap.get ?r ?rs,
-              H2 : Registers.Regmap.get ?r ?rs = Values.Vint _ |- _ =>
-          rewrite H2 in H; discriminate
-        | H : Values.Vundef = Registers.Regmap.get ?r ?rs,
-              H2 : Registers.Regmap.get ?r ?rs = Values.Vint _ |- _ =>
-          rewrite H2 in H; discriminate
-        | H : Values.Vint _ = Registers.Regmap.get ?r ?rs,
-              H2 : Registers.Regmap.get ?r ?rs = Values.Vundef |- _ =>
-          rewrite H2 in H; discriminate
-        | H : Values.Vint _ = Registers.Regmap.get ?r ?rs,
-              H2 : Registers.Regmap.get ?r ?rs = Values.Vtrue |- _ =>
-          rewrite H2 in H; discriminate
-        | H : Values.Vint _ = Registers.Regmap.get ?r ?rs,
-              H2 : Registers.Regmap.get ?r ?rs = Values.Vfalse |- _ =>
-          rewrite H2 in H; discriminate
-        | H : Values.Vint _ = Registers.Regmap.get ?r ?rs,
-              H2 : Registers.Regmap.get ?r ?rs = Values.Vptr _ _ |- _ =>
-          rewrite H2 in H; discriminate
-        | H : Values.Vundef = Registers.Regmap.get ?r ?rs,
-              H2 : Registers.Regmap.get ?r ?rs = Values.Vptr _ _ |- _ =>
-          rewrite H2 in H; discriminate
-        | H : Values.Vundef = Registers.Regmap.get ?r ?rs,
-              H2 : Registers.Regmap.get ?r ?rs = Values.Vtrue |- _ =>
-          rewrite H2 in H; discriminate
-        | H : Values.Vundef = Registers.Regmap.get ?r ?rs,
-              H2 : Registers.Regmap.get ?r ?rs = Values.Vfalse |- _ =>
-          rewrite H2 in H; discriminate
-        | H : Values.Vptr _ _ = Registers.Regmap.get ?r ?rs,
-              H2 : Registers.Regmap.get ?r ?rs = Values.Vundef |- _ =>
-          rewrite H2 in H; discriminate
-        | H : Values.Vptr _ _ = Registers.Regmap.get ?r ?rs,
-              H2 : Registers.Regmap.get ?r ?rs = Values.Vtrue |- _ =>
-          rewrite H2 in H; discriminate
-        | H : Values.Vptr _ _ = Registers.Regmap.get ?r ?rs,
-              H2 : Registers.Regmap.get ?r ?rs = Values.Vfalse |- _ =>
-          rewrite H2 in H; discriminate
-        | |- context[val_value_lessdef Values.Vundef _] =>
-          econstructor; split; econstructor; econstructor; auto; solve [constructor]
-        | H1 : Registers.Regmap.get ?r ?rs = Values.Vint _,
-          H2 : Values.Vint _ = Registers.Regmap.get ?r ?rs,
-          H3 : Registers.Regmap.get ?r0 ?rs = Values.Vint _,
-          H4 : Values.Vint _ = Registers.Regmap.get ?r0 ?rs|- _ =>
-          rewrite H1 in H2; rewrite H3 in H4; inv H2; inv H4; unfold valueToInt in *; constructor
-        | H1 : Registers.Regmap.get ?r ?rs = Values.Vptr _ _,
-          H2 : Values.Vptr _ _ = Registers.Regmap.get ?r ?rs,
-          H3 : Registers.Regmap.get ?r0 ?rs = Values.Vptr _ _,
-          H4 : Values.Vptr _ _ = Registers.Regmap.get ?r0 ?rs|- _ =>
-          rewrite H1 in H2; rewrite H3 in H4; inv H2; inv H4; unfold valueToInt in *; constructor;
-          unfold Ptrofs.ltu, Int.ltu in *; unfold Ptrofs.of_int in *;
-          repeat (rewrite Ptrofs.unsigned_repr in *; auto using Int.unsigned_range_2)
-        | H : _ :: _ = _ :: _ |- _ => inv H
-        | H : ret _ _ = OK _ _ _ |- _ => inv H
-        | |- _ =>
-          eexists; split; [ econstructor; econstructor; auto
-                          | simplify; inv_lessdef; repeat (unfold valueToPtr, valueToInt in *; solve_cond);
-                            unfold valueToPtr in *
-                          ]
-        end.
-
-  Lemma eval_cond_correct :
-    forall stk f sp pc rs m res ml st asr asa e b f' s s' args i cond,
-      match_states (RTL.State stk f sp pc rs m) (HTL.State res ml st asr asa) ->
-      (forall v, In v args -> Ple v (RTL.max_reg_function f)) ->
-      Op.eval_condition cond (map (fun r : positive => Registers.Regmap.get r rs) args) m = Some b ->
-      translate_condition cond args s = OK e s' i ->
-      Verilog.expr_runp f' asr asa e (boolToValue b).
-  Proof.
-    intros stk f sp pc rs m res ml st asr asa e b f' s s' args i cond MSTATE MAX_FUN EVAL TR_INSTR.
-    pose proof MSTATE as MSTATE_2. inv MSTATE.
-    inv MASSOC. unfold translate_condition, translate_comparison,
-                translate_comparisonu, translate_comparison_imm,
-                translate_comparison_immu in TR_INSTR;
-                repeat unfold_match TR_INSTR; try inv TR_INSTR; simplify_val;
-                unfold Values.Val.cmp_bool, Values.Val.of_optbool, bop, Values.Val.cmpu_bool,
-                  Int.cmpu in *;
-                repeat unfold_match EVAL.
-    - repeat econstructor. repeat unfold_match Heqo. simplify_val.
-      pose proof (MAX_FUN p) as MAX_FUN_P. apply H in MAX_FUN_P; auto.
-      pose proof (MAX_FUN p0) as MAX_FUN_P0. apply H in MAX_FUN_P0; auto.
-      inv MAX_FUN_P; inv MAX_FUN_P0; solve_cond.
-    - repeat econstructor. repeat unfold_match Heqo. simplify_val.
-      pose proof (MAX_FUN p) as MAX_FUN_P. apply H in MAX_FUN_P; auto.
-      pose proof (MAX_FUN p0) as MAX_FUN_P0. apply H in MAX_FUN_P0; auto.
-      inv MAX_FUN_P; inv MAX_FUN_P0; solve_cond.
-    - repeat econstructor. repeat unfold_match Heqo. simplify_val.
-      pose proof (MAX_FUN p) as MAX_FUN_P. apply H in MAX_FUN_P; auto.
-      pose proof (MAX_FUN p0) as MAX_FUN_P0. apply H in MAX_FUN_P0; auto.
-      inv MAX_FUN_P; inv MAX_FUN_P0; solve_cond.
-    - repeat econstructor. repeat unfold_match Heqo. simplify_val.
-      pose proof (MAX_FUN p) as MAX_FUN_P. apply H in MAX_FUN_P; auto.
-      pose proof (MAX_FUN p0) as MAX_FUN_P0. apply H in MAX_FUN_P0; auto.
-      inv MAX_FUN_P; inv MAX_FUN_P0; solve_cond.
-    - repeat econstructor. repeat unfold_match Heqo. simplify_val.
-      pose proof (MAX_FUN p) as MAX_FUN_P. apply H in MAX_FUN_P; auto.
-      pose proof (MAX_FUN p0) as MAX_FUN_P0. apply H in MAX_FUN_P0; auto.
-      inv MAX_FUN_P; inv MAX_FUN_P0; solve_cond.
-    - repeat econstructor. repeat unfold_match Heqo. simplify_val.
-      pose proof (MAX_FUN p) as MAX_FUN_P. apply H in MAX_FUN_P; auto.
-      pose proof (MAX_FUN p0) as MAX_FUN_P0. apply H in MAX_FUN_P0; auto.
-      inv MAX_FUN_P; inv MAX_FUN_P0; solve_cond.
-    - repeat econstructor. repeat unfold_match Heqo; simplify_val.
-      pose proof (MAX_FUN p) as MAX_FUN_P. apply H in MAX_FUN_P; auto.
-      pose proof (MAX_FUN p0) as MAX_FUN_P0. apply H in MAX_FUN_P0; auto.
-      inv MAX_FUN_P; inv MAX_FUN_P0; solve_cond.
-    - repeat econstructor. repeat unfold_match Heqo; simplify_val.
-      pose proof (MAX_FUN p) as MAX_FUN_P. apply H in MAX_FUN_P; auto.
-      pose proof (MAX_FUN p0) as MAX_FUN_P0. apply H in MAX_FUN_P0; auto.
-      inv MAX_FUN_P; inv MAX_FUN_P0; try solve_cond. simplify_val.
-      rewrite Heqv0 in H3. rewrite Heqv in H2. inv H2. inv H3.
-      unfold Ptrofs.ltu. unfold Int.ltu.
-      rewrite Ptrofs.unsigned_repr by apply Int.unsigned_range_2.
-      rewrite Ptrofs.unsigned_repr by apply Int.unsigned_range_2. auto.
-    - repeat econstructor.  unfold Verilog.binop_run.
-      pose proof (MAX_FUN p) as MAX_FUN_P. apply H in MAX_FUN_P; auto.
-      pose proof (MAX_FUN p0) as MAX_FUN_P0. apply H in MAX_FUN_P0; auto.
-      inv MAX_FUN_P; inv MAX_FUN_P0; simplify_val; solve_cond.
-    - repeat econstructor. simplify_val.
-      pose proof (MAX_FUN p) as MAX_FUN_P. apply H in MAX_FUN_P; auto.
-      pose proof (MAX_FUN p0) as MAX_FUN_P0. apply H in MAX_FUN_P0; auto.
-      inv MAX_FUN_P; inv MAX_FUN_P0; try solve_cond. simplify_val.
-      rewrite Heqv0 in H3. rewrite Heqv in H2. inv H2. inv H3.
-      unfold Ptrofs.ltu. unfold Int.ltu.
-      rewrite Ptrofs.unsigned_repr by apply Int.unsigned_range_2.
-      rewrite Ptrofs.unsigned_repr by apply Int.unsigned_range_2. auto.
-    - repeat econstructor.  unfold Verilog.binop_run.
-      pose proof (MAX_FUN p) as MAX_FUN_P. apply H in MAX_FUN_P; auto.
-      pose proof (MAX_FUN p0) as MAX_FUN_P0. apply H in MAX_FUN_P0; auto.
-      inv MAX_FUN_P; inv MAX_FUN_P0; simplify_val; solve_cond.
-    - repeat econstructor. simplify_val.
-      pose proof (MAX_FUN p) as MAX_FUN_P. apply H in MAX_FUN_P; auto.
-      pose proof (MAX_FUN p0) as MAX_FUN_P0. apply H in MAX_FUN_P0; auto.
-      inv MAX_FUN_P; inv MAX_FUN_P0; try solve_cond. simplify_val.
-      rewrite Heqv0 in H3. rewrite Heqv in H2. inv H2. inv H3.
-      unfold Ptrofs.ltu. unfold Int.ltu.
-      rewrite Ptrofs.unsigned_repr by apply Int.unsigned_range_2.
-      rewrite Ptrofs.unsigned_repr by apply Int.unsigned_range_2. auto.
-    - repeat econstructor.  unfold Verilog.binop_run.
-      pose proof (MAX_FUN p) as MAX_FUN_P. apply H in MAX_FUN_P; auto.
-      pose proof (MAX_FUN p0) as MAX_FUN_P0. apply H in MAX_FUN_P0; auto.
-      inv MAX_FUN_P; inv MAX_FUN_P0; simplify_val; solve_cond.
-    - repeat econstructor. simplify_val.
-      pose proof (MAX_FUN p) as MAX_FUN_P. apply H in MAX_FUN_P; auto.
-      pose proof (MAX_FUN p0) as MAX_FUN_P0. apply H in MAX_FUN_P0; auto.
-      inv MAX_FUN_P; inv MAX_FUN_P0; try solve_cond. simplify_val.
-      rewrite Heqv0 in H3. rewrite Heqv in H2. inv H2. inv H3.
-      unfold Ptrofs.ltu. unfold Int.ltu.
-      rewrite Ptrofs.unsigned_repr by apply Int.unsigned_range_2.
-      rewrite Ptrofs.unsigned_repr by apply Int.unsigned_range_2. auto.
-    - repeat econstructor. simplify_val.
-      pose proof (MAX_FUN p) as MAX_FUN_P. apply H in MAX_FUN_P; auto.
-      inv MAX_FUN_P; simplify_val; try solve_cond.
-      rewrite Heqv in H0. inv H0. auto.
-    - repeat econstructor. simplify_val.
-      pose proof (MAX_FUN p) as MAX_FUN_P. apply H in MAX_FUN_P; auto.
-      inv MAX_FUN_P; simplify_val; try solve_cond.
-      rewrite Heqv in H0. inv H0. auto.
-    - repeat econstructor. simplify_val.
-      pose proof (MAX_FUN p) as MAX_FUN_P. apply H in MAX_FUN_P; auto.
-      inv MAX_FUN_P; simplify_val; try solve_cond.
-      rewrite Heqv in H0. inv H0. auto.
-    - repeat econstructor. simplify_val.
-      pose proof (MAX_FUN p) as MAX_FUN_P. apply H in MAX_FUN_P; auto.
-      inv MAX_FUN_P; simplify_val; try solve_cond.
-      rewrite Heqv in H0. inv H0. auto.
-    - repeat econstructor. simplify_val.
-      pose proof (MAX_FUN p) as MAX_FUN_P. apply H in MAX_FUN_P; auto.
-      inv MAX_FUN_P; simplify_val; try solve_cond.
-      rewrite Heqv in H0. inv H0. auto.
-    - repeat econstructor. simplify_val.
-      pose proof (MAX_FUN p) as MAX_FUN_P. apply H in MAX_FUN_P; auto.
-      inv MAX_FUN_P; simplify_val; try solve_cond.
-      rewrite Heqv in H0. inv H0. auto.
-    - repeat econstructor. simplify_val.
-      pose proof (MAX_FUN p) as MAX_FUN_P. apply H in MAX_FUN_P; auto.
-      inv MAX_FUN_P; simplify_val; try solve_cond.
-      rewrite Heqv in H0. inv H0. auto.
-    - repeat econstructor. simplify_val.
-      pose proof (MAX_FUN p) as MAX_FUN_P. apply H in MAX_FUN_P; auto.
-      inv MAX_FUN_P; simplify_val; try solve_cond.
-      rewrite Heqv in H0. inv H0. auto.
-    - repeat econstructor. simplify_val.
-      pose proof (MAX_FUN p) as MAX_FUN_P. apply H in MAX_FUN_P; auto.
-      inv MAX_FUN_P; simplify_val; try solve_cond.
-      rewrite Heqv in H0. inv H0. auto.
-    - repeat econstructor. simplify_val.
-      pose proof (MAX_FUN p) as MAX_FUN_P. apply H in MAX_FUN_P; auto.
-      inv MAX_FUN_P; simplify_val; try solve_cond.
-      rewrite Heqv in H0. inv H0. auto.
-  Qed.
-
-  Lemma eval_cond_correct' :
-    forall e stk f sp pc rs m res ml st asr asa v f' s s' args i cond,
-      match_states (RTL.State stk f sp pc rs m) (HTL.State res ml st asr asa) ->
-      (forall v, In v args -> Ple v (RTL.max_reg_function f)) ->
-      Values.Val.of_optbool None = v ->
-      translate_condition cond args s = OK e s' i ->
-      exists v', Verilog.expr_runp f' asr asa e v' /\ val_value_lessdef v v'.
-    intros e stk f sp pc rs m res ml st asr asa v f' s s' args i cond MSTATE MAX_FUN EVAL TR_INSTR.
-    unfold translate_condition, translate_comparison, translate_comparisonu,
-    translate_comparison_imm, translate_comparison_immu, bop, boplit in *.
-    repeat unfold_match TR_INSTR; inv TR_INSTR; repeat econstructor.
-  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.
-    pose proof MSTATE as MSTATE_2. 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); inv EVAL;
-    repeat (simplify; eval_correct_tac; unfold valueToInt in *).
-    - pose proof Integers.Ptrofs.agree32_sub as H2; unfold Integers.Ptrofs.agree32 in H2.
-      unfold Ptrofs.of_int. simpl.
-      apply ptrofs_inj. assert (Archi.ptr64 = false) by auto. eapply H2 in H3.
-      rewrite Ptrofs.unsigned_repr. apply H3. 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.
-    - pose proof Integers.Ptrofs.agree32_sub as AGR; unfold Integers.Ptrofs.agree32 in AGR.
-      assert (ARCH: Archi.ptr64 = false) by auto. eapply AGR in ARCH.
-      apply int_inj. unfold Ptrofs.to_int. rewrite Int.unsigned_repr.
-      apply ARCH. pose proof Ptrofs.unsigned_range_2.
-      replace Ptrofs.max_unsigned with Int.max_unsigned; auto.
-      pose proof Ptrofs.agree32_of_int. unfold Ptrofs.agree32 in H2.
-      eapply H2 in ARCH. apply ARCH.
-      pose proof Ptrofs.agree32_of_int. unfold Ptrofs.agree32 in H2.
-      eapply H2 in ARCH. apply ARCH.
-    - rewrite H0 in Heqb. rewrite H1 in Heqb. discriminate.
-    - rewrite Heqb in Heqb0. discriminate.
-    - rewrite H0 in Heqb. rewrite H1 in Heqb. discriminate.
-    - rewrite Heqb in Heqb0. discriminate.
-    (*- unfold Int.ror. unfold Int.or. unfold Int.shru, Int.shl, Int.sub. unfold intToValue. unfold Int.modu,
-      repeat (rewrite Int.unsigned_repr). auto.*)
-    - unfold Op.eval_addressing32 in *. repeat (unfold_match H2); inv H2.
-      + unfold translate_eff_addressing in *. repeat (unfold_match H1).
-        destruct v0; inv Heql; rewrite H2; inv H1; repeat eval_correct_tac.
-        pose proof Integers.Ptrofs.agree32_add as AGR; unfold Integers.Ptrofs.agree32 in AGR. unfold ZToValue.
-        apply ptrofs_inj. unfold Ptrofs.of_int. rewrite Ptrofs.unsigned_repr.
-        apply AGR. auto. rewrite H2 in H0. inv H0. unfold valueToPtr. unfold Ptrofs.of_int.
-        rewrite Ptrofs.unsigned_repr. auto. replace Ptrofs.max_unsigned with Int.max_unsigned by auto.
-        apply Int.unsigned_range_2.
-        rewrite Ptrofs.unsigned_repr. auto. replace Ptrofs.max_unsigned with Int.max_unsigned by auto.
-        apply Int.unsigned_range_2.
-        replace Ptrofs.max_unsigned with Int.max_unsigned by auto.
-        apply Int.unsigned_range_2.
-      + unfold translate_eff_addressing in *. repeat (unfold_match H1). inv H1.
-        inv Heql. unfold boplitz. repeat (simplify; eval_correct_tac).
-        all: repeat (unfold_match Heqv).
-        * inv Heqv. unfold valueToInt in *. inv H2. inv H0. unfold valueToInt in *. trivial.
-        * constructor. unfold valueToPtr, ZToValue in *.
-          pose proof Integers.Ptrofs.agree32_add as AGR; unfold Integers.Ptrofs.agree32 in AGR. unfold ZToValue.
-          apply ptrofs_inj. unfold Ptrofs.of_int. rewrite Ptrofs.unsigned_repr.
-          apply AGR. auto. inv Heqv. rewrite Int.add_commut.
-          apply AGR. auto. inv H1. inv H0. unfold valueToPtr. unfold Ptrofs.of_int.
-          rewrite Ptrofs.unsigned_repr. auto. replace Ptrofs.max_unsigned with Int.max_unsigned by auto.
-          apply Int.unsigned_range_2.
-          unfold Ptrofs.of_int.
-          rewrite Ptrofs.unsigned_repr. inv H0. auto. replace Ptrofs.max_unsigned with Int.max_unsigned by auto.
-          apply Int.unsigned_range_2.
-          rewrite Ptrofs.unsigned_repr. auto. replace Ptrofs.max_unsigned with Int.max_unsigned by auto.
-          apply Int.unsigned_range_2.
-          apply Int.unsigned_range_2.
-        * constructor. unfold valueToPtr, ZToValue in *.
-          pose proof Integers.Ptrofs.agree32_add as AGR; unfold Integers.Ptrofs.agree32 in AGR. unfold ZToValue.
-          apply ptrofs_inj. unfold Ptrofs.of_int. rewrite Ptrofs.unsigned_repr.
-          apply AGR. auto. inv Heqv.
-          apply AGR. auto. inv H0. unfold valueToPtr, Ptrofs.of_int. rewrite Ptrofs.unsigned_repr. auto.
-          replace Ptrofs.max_unsigned with Int.max_unsigned by auto.
-          apply Int.unsigned_range_2.
-          inv H1. unfold valueToPtr, Ptrofs.of_int. rewrite Ptrofs.unsigned_repr. auto.
-          replace Ptrofs.max_unsigned with Int.max_unsigned by auto.
-          apply Int.unsigned_range_2.
-          rewrite Ptrofs.unsigned_repr. auto.
-          replace Ptrofs.max_unsigned with Int.max_unsigned by auto.
-          apply Int.unsigned_range_2. apply Int.unsigned_range_2.
-      + unfold translate_eff_addressing in *. repeat (unfold_match H1). inv H1.
-        inv Heql. unfold boplitz. repeat (simplify; eval_correct_tac).
-        all: repeat (unfold_match Heqv).
-        * unfold Values.Val.mul in Heqv. repeat (unfold_match Heqv). inv Heqv. inv H3.
-          unfold valueToInt, ZToValue. auto.
-        * unfold Values.Val.mul in Heqv. repeat (unfold_match Heqv).
-        * unfold Values.Val.mul in Heqv. repeat (unfold_match Heqv).
-        * constructor. unfold valueToPtr, ZToValue. unfold Values.Val.mul in Heqv. repeat (unfold_match Heqv).
-      + unfold translate_eff_addressing in *. repeat (unfold_match H1). inv H1.
-        inv Heql. unfold boplitz. repeat (simplify; eval_correct_tac).
-        all: repeat (unfold_match Heqv).
-        unfold valueToPtr, ZToValue.
-        repeat unfold_match Heqv0. unfold Values.Val.mul in Heqv1. repeat unfold_match Heqv1.
-        inv Heqv1. inv Heqv0. unfold valueToInt in *.
-        assert (HPle1 : Ple r0 (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto).
-        apply H in HPle1. inv HPle1. unfold valueToInt in *. rewrite Heqv2 in H2. inv H2. auto.
-        rewrite Heqv2 in H2. inv H2.
-        rewrite Heqv2 in H3. discriminate.
-        repeat unfold_match Heqv0. unfold Values.Val.mul in Heqv1. repeat unfold_match Heqv1.
-        repeat unfold_match Heqv0. unfold Values.Val.mul in Heqv1. repeat unfold_match Heqv1.
-        constructor. unfold valueToPtr, ZToValue. inv Heqv0. inv Heqv1.
-        assert (HPle1 : Ple r0 (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto).
-        apply H in HPle1. inv HPle1. unfold valueToInt in *. rewrite Heqv2 in H3. inv H3.
-
-        pose proof Integers.Ptrofs.agree32_add as AGR; unfold Integers.Ptrofs.agree32 in AGR. unfold ZToValue.
-        apply ptrofs_inj. unfold Ptrofs.of_int. rewrite Ptrofs.unsigned_repr.
-        apply AGR. auto. inv H2. unfold valueToPtr, Ptrofs.of_int. rewrite Ptrofs.unsigned_repr. auto.
-        replace Ptrofs.max_unsigned with Int.max_unsigned by auto. apply Int.unsigned_range_2.
-        apply Ptrofs.unsigned_repr. apply Int.unsigned_range_2. apply Int.unsigned_range_2.
-
-        rewrite Heqv2 in H3. inv H3.
-
-        rewrite Heqv2 in H4. inv H4.
-      + unfold translate_eff_addressing in *. repeat (unfold_match H1). inv H1.
-        inv Heql. unfold boplitz. repeat (simplify; eval_correct_tac).
-        all: repeat (unfold_match Heqv).
-        eexists. split. constructor.
-        constructor. unfold valueToPtr, ZToValue. rewrite Ptrofs.add_zero_l. unfold Ptrofs.of_int.
-        rewrite Int.unsigned_repr. symmetry. apply Ptrofs.repr_unsigned.
-        unfold check_address_parameter_unsigned in *. apply Ptrofs.unsigned_range_2.
-    - destruct (Op.eval_condition cond (map (fun r : positive => Registers.Regmap.get r rs) args) m) eqn:EQ.
-      + exploit eval_cond_correct; eauto. intros. eapply RTL.max_reg_function_use. apply INSTR. auto.
-        intros. econstructor. econstructor. eassumption. unfold boolToValue, Values.Val.of_optbool.
-        destruct b; constructor; auto.
-      + eapply eval_cond_correct'; eauto. intros. eapply RTL.max_reg_function_use. apply INSTR. auto.
-    - monadInv H1.
-      destruct (Op.eval_condition c (map (fun r1 : positive => Registers.Regmap.get r1 rs) l0) m) eqn:EQN;
-      simplify. destruct b eqn:B.
-      + exploit eval_cond_correct; eauto. intros. eapply RTL.max_reg_function_use. apply INSTR.
-        simplify; tauto. intros.
-        econstructor. econstructor. eapply Verilog.erun_Vternary_true. eassumption. econstructor. auto.
-        auto. unfold Values.Val.normalize.
-        destruct (Registers.Regmap.get r rs) eqn:EQN2; constructor.
-        * assert (HPle1 : Ple r (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto).
-          apply H in HPle1. inv HPle1. unfold valueToInt in H1. rewrite EQN2 in H1. inv H1. auto.
-          rewrite EQN2 in H1. discriminate. rewrite EQN2 in H2. discriminate.
-        * assert (HPle1 : Ple r (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto).
-          apply H in HPle1. inv HPle1. rewrite EQN2 in H1. inv H1. rewrite EQN2 in H1. inv H1. auto.
-          rewrite EQN2 in H2. discriminate.
-      + exploit eval_cond_correct; eauto. intros. eapply RTL.max_reg_function_use. apply INSTR.
-        simplify; tauto. intros.
-        econstructor. econstructor. eapply Verilog.erun_Vternary_false. eassumption. econstructor. auto.
-        auto. unfold Values.Val.normalize.
-        destruct (Registers.Regmap.get r0 rs) eqn:EQN2; constructor.
-        * assert (HPle1 : Ple r0 (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto).
-          apply H in HPle1. inv HPle1. unfold valueToInt in H1. rewrite EQN2 in H1. inv H1. auto.
-          rewrite EQN2 in H1. discriminate. rewrite EQN2 in H2. discriminate.
-        * assert (HPle1 : Ple r0 (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto).
-          apply H in HPle1. inv HPle1. rewrite EQN2 in H1. inv H1. rewrite EQN2 in H1. inv H1. auto.
-          rewrite EQN2 in H2. discriminate.
-      + exploit eval_cond_correct'; eauto. intros. eapply RTL.max_reg_function_use. apply INSTR.
-        simplify; tauto. intros. inv H0. inv H1. destruct (Int.eq_dec x0 Int.zero).
-        econstructor. econstructor. eapply Verilog.erun_Vternary_false.
-        eassumption. econstructor. auto. subst. auto. constructor.
-        econstructor. econstructor. eapply Verilog.erun_Vternary_true.
-        eassumption. econstructor. auto. unfold valueToBool. pose proof n. apply Int.eq_false in n.
-        unfold uvalueToZ. unfold Int.eq in n. unfold zeq in *.
-        destruct (Int.unsigned x0 ==Z Int.unsigned Int.zero); try discriminate.
-        rewrite <- Z.eqb_neq in n0. rewrite Int.unsigned_zero in n0. rewrite n0. auto.
-        constructor.
-  Qed.
-
-  (** The proof of semantic preservation for the translation of instructions
-      is a simulation argument based on diagrams of the following form:
-<<
-                      match_states
-    code st rs ---------------- State m st assoc
-         ||                             |
-         ||                             |
-         ||                             |
-         \/                             v
-    code st rs' --------------- State m st assoc'
-                      match_states
->>
-      where [tr_code c data control fin rtrn st] is assumed to hold.
-
-      The precondition and postcondition is that that should hold is [match_assocmaps rs assoc].
-   *)
-
-  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 _ _)] ] =>
-      let EQ := fresh "EQ" in
-      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_val; try array; try ptrofs); crush_val; auto.
-  Ltac big_tac := repeat (crush_val; try array; try ptrofs; try tac0); crush_val; 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. exact tt.
-  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. inv MARR.
-    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 H5. simplify.
-
-    all: big_tac.
-
-    assert (HPle: Ple res0 (RTL.max_reg_function f))
-        by (eapply RTL.max_reg_function_def; eauto; simpl; auto).
-
-    unfold Ple in HPle. lia.
-    apply regs_lessdef_add_match. assumption.
-    apply regs_lessdef_add_greater. unfold Plt; lia. assumption.
-    assert (HPle: Ple res0 (RTL.max_reg_function f))
-        by (eapply RTL.max_reg_function_def; eauto; simpl; auto).
-    unfold Ple in HPle; lia.
-    eapply op_stack_based; eauto.
-    inv CONST. constructor; simplify. rewrite AssocMap.gso. rewrite AssocMap.gso.
-    assumption. lia.
-    assert (HPle: Ple res0 (RTL.max_reg_function f))
-      by (eapply RTL.max_reg_function_def; eauto; simpl; auto).
-    unfold Ple in HPle. lia.
-    rewrite AssocMap.gso. rewrite AssocMap.gso.
-    assumption. lia.
-    assert (HPle: Ple res0 (RTL.max_reg_function f))
-      by (eapply RTL.max_reg_function_def; eauto; simpl; auto).
-    unfold Ple in HPle. lia.
-    Unshelve. exact tt.
-  Qed.
-  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 offset_expr_ok :
-    forall v z, (Z.to_nat
-                   (Integers.Ptrofs.unsigned
-                      (Integers.Ptrofs.divu
-                         (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ v))
-                                              (Integers.Ptrofs.of_int (Integers.Int.repr z)))
-                         (Integers.Ptrofs.repr 4)))
-                 = valueToNat (Int.divu (Int.add v (ZToValue z)) (ZToValue 4))).
-  Proof.
-    simplify_val. unfold valueToNat. unfold Int.divu, Ptrofs.divu.
-    pose proof Integers.Ptrofs.agree32_add as AGR.
-    unfold Integers.Ptrofs.agree32 in AGR.
-    assert (Ptrofs.unsigned (Ptrofs.add (Ptrofs.repr (Int.unsigned v))
-                                        (Ptrofs.repr (Int.unsigned (Int.repr z)))) =
-            Int.unsigned (Int.add v (ZToValue z))).
-    apply AGR; auto.
-    apply Ptrofs.unsigned_repr. apply Int.unsigned_range_2.
-    apply Ptrofs.unsigned_repr. apply Int.unsigned_range_2.
-    rewrite H. replace (Ptrofs.unsigned (Ptrofs.repr 4)) with 4.
-    replace (Int.unsigned (ZToValue 4)) with 4.
-    pose proof Ptrofs.agree32_repr. unfold Ptrofs.agree32 in *.
-    rewrite H0. trivial. auto.
-    unfold ZToValue. symmetry. apply Int.unsigned_repr.
-    unfold_constants. lia.
-    unfold ZToValue. symmetry. apply Int.unsigned_repr.
-    unfold_constants. lia.
-  Qed.
-
-  Lemma offset_expr_ok_2 :
-    forall v0 v1 z0 z1,
-      (Z.to_nat
-         (Integers.Ptrofs.unsigned
-            (Integers.Ptrofs.divu
-               (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ v0))
-                                    (Integers.Ptrofs.of_int
-                                       (Integers.Int.add
-                                          (Integers.Int.mul (valueToInt v1) (Integers.Int.repr z1))
-                                          (Integers.Int.repr z0)))) (Ptrofs.repr 4))))
-      = valueToNat (Int.divu (Int.add (Int.add v0 (ZToValue z0))
-                                      (Int.mul v1 (ZToValue z1))) (ZToValue 4)).
-    intros. unfold ZToValue, valueToNat, valueToInt, Ptrofs.divu, Int.divu, Ptrofs.of_int.
-
-    assert (H : (Ptrofs.unsigned
-             (Ptrofs.add (Ptrofs.repr (uvalueToZ v0))
-                (Ptrofs.of_int (Int.add (Int.mul (valueToInt v1) (Int.repr z1)) (Int.repr z0)))) /
-           Ptrofs.unsigned (Ptrofs.repr 4))
-                = (Int.unsigned (Int.add (Int.add v0 (Int.repr z0)) (Int.mul v1 (Int.repr z1))) /
-           Int.unsigned (Int.repr 4))).
-    { unfold ZToValue, valueToNat, valueToInt, Ptrofs.divu, Int.divu, Ptrofs.of_int.
-      rewrite Ptrofs.unsigned_repr by (unfold_constants; lia).
-      rewrite Int.unsigned_repr by (unfold_constants; lia).
-
-      unfold Ptrofs.of_int. rewrite Int.add_commut.
-      pose proof Integers.Ptrofs.agree32_add as AGR. unfold Ptrofs.agree32 in *.
-      erewrite AGR.
-      3: { unfold uvalueToZ. rewrite Ptrofs.unsigned_repr. trivial. apply Int.unsigned_range_2. }
-      3: { rewrite Ptrofs.unsigned_repr. trivial. apply Int.unsigned_range_2. }
-      rewrite Int.add_assoc. trivial. auto.
-    }
-
-    rewrite <- H. auto.
-
-  Qed.
-
-  Lemma offset_expr_ok_3 :
-    forall OFFSET,
-      Z.to_nat (Ptrofs.unsigned (Ptrofs.divu OFFSET (Ptrofs.repr 4)))
-      = valueToNat (ZToValue (Ptrofs.unsigned OFFSET / 4)).
-  Proof. auto. Qed.
-
-  Lemma 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. inv CONST. crush.
-
-      unfold Op.eval_addressing in H0.
-      destruct (Archi.ptr64) eqn:ARCHI; crush.
-
-      unfold reg_stack_based_pointers in RSBP.
-      pose proof (RSBP r0) as RSBPr0.
-
-      destruct (Registers.Regmap.get r0 rs) eqn:EQr0; crush.
-
-      rewrite ARCHI in H1. crush.
-      subst.
-
-      pose proof MASSOC as MASSOC'.
-      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 H0 in HPler0.
-      invert HPler0; try congruence.
-      rewrite EQr0 in H11.
-      invert H11.
-
-      unfold check_address_parameter_signed in *;
-      unfold check_address_parameter_unsigned in *; crush.
-
-      remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ asr # r0))
-                                    (Integers.Ptrofs.of_int (Integers.Int.repr z))) as OFFSET.
-
-      (** Modular preservation proof *)
-      assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE.
-      { apply Mem.load_valid_access in H1. unfold Mem.valid_access in *. simplify.
-        apply Zdivide_mod. assumption. }
-
-      (** Read bounds proof *)
-      assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH.
-      { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; crush; auto.
-        unfold stack_bounds in BOUNDS.
-        exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET)); auto.
-        split; try lia; apply Integers.Ptrofs.unsigned_range_2.
-        small_tac. }
-
-      (** Normalisation proof *)
-      assert (Integers.Ptrofs.repr
-                (4 * Integers.Ptrofs.unsigned
-                       (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4))) = OFFSET)
-        as NORMALISE.
-      { replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) at 1 by reflexivity.
-        rewrite <- PtrofsExtra.mul_unsigned.
-        apply PtrofsExtra.mul_divu; crush; auto. }
-
-      (** Normalised bounds proof *)
-      assert (0 <=
-              Integers.Ptrofs.unsigned (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4))
-              < (RTL.fn_stacksize f / 4))
-        as NORMALISE_BOUND.
-      { split.
-        apply Integers.Ptrofs.unsigned_range_2.
-        assert (HDIV: forall x y, Integers.Ptrofs.divu x y = Integers.Ptrofs.divu x y ) by reflexivity.
-        unfold Integers.Ptrofs.divu at 2 in HDIV.
-        rewrite HDIV. clear HDIV.
-        rewrite Integers.Ptrofs.unsigned_repr; crush.
-        apply Zmult_lt_reg_r with (p := 4); try lia.
-        repeat rewrite ZLib.div_mul_undo; try lia.
-        apply Z.div_pos; small_tac.
-        apply Z.div_le_upper_bound; small_tac. }
-
-      inversion NORMALISE_BOUND as [ NORMALISE_BOUND_LOW NORMALISE_BOUND_HIGH ];
-      clear NORMALISE_BOUND.
-
-      (** Start of proof proper *)
-      eexists. split.
-      eapply Smallstep.plus_one.
-      eapply HTL.step_module; eauto.
-      econstructor. econstructor. econstructor. crush.
-      econstructor. econstructor. econstructor. crush.
-      econstructor. econstructor.
-      econstructor. econstructor. econstructor. econstructor.
-      econstructor. econstructor.
-
-      all: big_tac.
-
-      1: {
-        assert (HPle : Ple dst (RTL.max_reg_function f)).
-        eapply RTL.max_reg_function_def. eassumption. auto.
-        apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption.
-      }
-
-      2: {
-        assert (HPle : Ple dst (RTL.max_reg_function f)).
-        eapply RTL.max_reg_function_def. eassumption. auto.
-        apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption.
-      }
-
-      (** Match assocmaps *)
-      apply regs_lessdef_add_match; big_tac.
-
-      (** Equality proof *)
-      rewrite <- offset_expr_ok.
-
-      specialize (H9 (Integers.Ptrofs.unsigned
-                        (Integers.Ptrofs.divu
-                           OFFSET
-                           (Integers.Ptrofs.repr 4)))).
-      exploit H9; big_tac.
-
-      (** RSBP preservation *)
-      unfold arr_stack_based_pointers in ASBP.
-      specialize (ASBP (Integers.Ptrofs.unsigned
-                          (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)))).
-      exploit ASBP; big_tac.
-      rewrite NORMALISE in H14. rewrite HeqOFFSET in H14. rewrite H1 in H14. assumption.
-      constructor; simplify. rewrite AssocMap.gso. rewrite AssocMap.gso.
-      assumption. lia.
-      assert (HPle: Ple dst (RTL.max_reg_function f))
-        by (eapply RTL.max_reg_function_def; eauto; simpl; auto).
-      unfold Ple in HPle. lia.
-      rewrite AssocMap.gso. rewrite AssocMap.gso.
-      assumption. lia.
-      assert (HPle: Ple dst (RTL.max_reg_function f))
-        by (eapply RTL.max_reg_function_def; eauto; simpl; auto).
-      unfold Ple in HPle. lia.
-    + (** Preamble *)
-      invert MARR. inv CONST. crush.
-
-      unfold Op.eval_addressing in H0.
-      destruct (Archi.ptr64) eqn:ARCHI; crush.
-
-      unfold reg_stack_based_pointers in RSBP.
-      pose proof (RSBP r0) as RSBPr0.
-      pose proof (RSBP r1) as RSBPr1.
-
-      destruct (Registers.Regmap.get r0 rs) eqn:EQr0;
-      destruct (Registers.Regmap.get r1 rs) eqn:EQr1; crush.
-
-      rewrite ARCHI in H1. crush.
-      subst.
-      clear RSBPr1.
-
-      pose proof MASSOC as MASSOC'.
-      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 H8 in HPler0.
-      apply H11 in HPler1.
-      invert HPler0; invert HPler1; try congruence.
-      rewrite EQr0 in H13.
-      rewrite EQr1 in H14.
-      invert H13. invert H14.
-      clear H0. clear H8. clear H11.
-
-      unfold check_address_parameter_signed in *;
-      unfold check_address_parameter_unsigned in *; crush.
-
-      remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ asr # r0))
-                                    (Integers.Ptrofs.of_int
-                                       (Integers.Int.add (Integers.Int.mul (valueToInt asr # r1) (Integers.Int.repr z))
-                                                         (Integers.Int.repr z0)))) as OFFSET.
-
-      (** Modular preservation proof *)
-      assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE.
-      { apply Mem.load_valid_access in H1. unfold Mem.valid_access in *. simplify.
-        apply Zdivide_mod. assumption. }
-
-      (** Read bounds proof *)
-      assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH.
-      { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; crush; auto.
-        unfold stack_bounds in BOUNDS.
-        exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET)); auto.
-        split; try lia; apply Integers.Ptrofs.unsigned_range_2.
-        small_tac. }
-
-      (** Normalisation proof *)
-      assert (Integers.Ptrofs.repr
-                (4 * Integers.Ptrofs.unsigned
-                       (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4))) = OFFSET)
-        as NORMALISE.
-      { replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) at 1 by reflexivity.
-        rewrite <- PtrofsExtra.mul_unsigned.
-        apply PtrofsExtra.mul_divu; crush. }
-
-      (** Normalised bounds proof *)
-      assert (0 <=
-              Integers.Ptrofs.unsigned (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4))
-              < (RTL.fn_stacksize f / 4))
-        as NORMALISE_BOUND.
-      { split.
-        apply Integers.Ptrofs.unsigned_range_2.
-        assert (forall x y, Integers.Ptrofs.divu x y = Integers.Ptrofs.divu x y ) by reflexivity.
-        unfold Integers.Ptrofs.divu at 2 in H14.
-        rewrite H14. clear H14.
-        rewrite Integers.Ptrofs.unsigned_repr; crush.
-        apply Zmult_lt_reg_r with (p := 4); try lia.
-        repeat rewrite ZLib.div_mul_undo; try lia.
-        apply Z.div_pos; small_tac.
-        apply Z.div_le_upper_bound; lia. }
-
-      inversion NORMALISE_BOUND as [ NORMALISE_BOUND_LOW NORMALISE_BOUND_HIGH ];
-      clear NORMALISE_BOUND.
-
-      (** Start of proof proper *)
-      eexists. split.
-      eapply Smallstep.plus_one.
-      eapply HTL.step_module; eauto.
-      econstructor. econstructor. econstructor. crush.
-      econstructor. econstructor. econstructor. crush.
-      econstructor. econstructor. econstructor.
-      econstructor. econstructor. econstructor. econstructor.
-      econstructor. econstructor. auto. econstructor.
-      econstructor. econstructor. econstructor. econstructor.
-      all: big_tac.
-
-      1: { assert (HPle : Ple dst (RTL.max_reg_function f)).
-           eapply RTL.max_reg_function_def. eassumption. auto.
-           apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. }
-
-      2: { assert (HPle : Ple dst (RTL.max_reg_function f)).
-           eapply RTL.max_reg_function_def. eassumption. auto.
-           apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. }
-
-      (** Match assocmaps *)
-      apply regs_lessdef_add_match; big_tac.
-
-      (** Equality proof *)
-      rewrite <- offset_expr_ok_2.
-
-      specialize (H9 (Integers.Ptrofs.unsigned
-                        (Integers.Ptrofs.divu
-                           OFFSET
-                           (Integers.Ptrofs.repr 4)))).
-      exploit H9; big_tac.
-
-      (** RSBP preservation *)
-      unfold arr_stack_based_pointers in ASBP.
-      specialize (ASBP (Integers.Ptrofs.unsigned
-                          (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)))).
-      exploit ASBP; big_tac.
-      rewrite NORMALISE in H14. rewrite HeqOFFSET in H14. rewrite H1 in H14. assumption.
-
-      constructor; simplify. rewrite AssocMap.gso. rewrite AssocMap.gso.
-      assumption. lia.
-      assert (HPle: Ple dst (RTL.max_reg_function f))
-        by (eapply RTL.max_reg_function_def; eauto; simpl; auto).
-      unfold Ple in HPle. lia.
-      rewrite AssocMap.gso. rewrite AssocMap.gso.
-      assumption. lia.
-      assert (HPle: Ple dst (RTL.max_reg_function f))
-        by (eapply RTL.max_reg_function_def; eauto; simpl; auto).
-      unfold Ple in HPle. lia.
-
-    + invert MARR. inv CONST. crush.
-
-      unfold Op.eval_addressing in H0.
-      destruct (Archi.ptr64) eqn:ARCHI; crush.
-      rewrite ARCHI in H0. crush.
-
-      unfold check_address_parameter_unsigned in *;
-      unfold check_address_parameter_signed in *; crush.
-
-      assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
-      rewrite ZERO in H1. clear ZERO.
-      rewrite Integers.Ptrofs.add_zero_l in H1.
-
-      remember i0 as OFFSET.
-
-      (** Modular preservation proof *)
-      assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE.
-      { apply Mem.load_valid_access in H1. unfold Mem.valid_access in *. simplify.
-        apply Zdivide_mod. assumption. }
-
-      (** Read bounds proof *)
-      assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH.
-      { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:?EQ; crush; auto.
-        unfold stack_bounds in BOUNDS.
-        exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET)); big_tac. }
-
-      (** Normalisation proof *)
-      assert (Integers.Ptrofs.repr
-                (4 * Integers.Ptrofs.unsigned
-                       (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4))) = OFFSET)
-        as NORMALISE.
-      { replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) at 1 by reflexivity.
-        rewrite <- PtrofsExtra.mul_unsigned.
-        apply PtrofsExtra.mul_divu; crush. }
-
-      (** Normalised bounds proof *)
-      assert (0 <=
-              Integers.Ptrofs.unsigned (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4))
-              < (RTL.fn_stacksize f / 4))
-        as NORMALISE_BOUND.
-      { split.
-        apply Integers.Ptrofs.unsigned_range_2.
-        assert (forall x y, Integers.Ptrofs.divu x y = Integers.Ptrofs.divu x y ) by reflexivity.
-        unfold Integers.Ptrofs.divu at 2 in H0.
-        rewrite H0. clear H0.
-        rewrite Integers.Ptrofs.unsigned_repr; crush.
-        apply Zmult_lt_reg_r with (p := 4); try lia.
-        repeat rewrite ZLib.div_mul_undo; try lia.
-        apply Z.div_pos; small_tac.
-        apply Z.div_le_upper_bound; lia. }
-
-      inversion NORMALISE_BOUND as [ NORMALISE_BOUND_LOW NORMALISE_BOUND_HIGH ];
-      clear NORMALISE_BOUND.
-
-      (** Start of proof proper *)
-      eexists. split.
-      eapply Smallstep.plus_one.
-      eapply HTL.step_module; eauto.
-      econstructor. econstructor. econstructor. crush.
-      econstructor. econstructor. econstructor. econstructor. crush.
-
-      all: big_tac.
-
-      1: { assert (HPle : Ple dst (RTL.max_reg_function f)).
-           eapply RTL.max_reg_function_def. eassumption. auto.
-           apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. }
-
-      2: { assert (HPle : Ple dst (RTL.max_reg_function f)).
-           eapply RTL.max_reg_function_def. eassumption. auto.
-           apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. }
-
-      (** Match assocmaps *)
-      apply regs_lessdef_add_match; big_tac.
-
-      (** Equality proof *)
-      rewrite <- offset_expr_ok_3.
-
-      specialize (H9 (Integers.Ptrofs.unsigned
-                        (Integers.Ptrofs.divu
-                           OFFSET
-                           (Integers.Ptrofs.repr 4)))).
-      exploit H9; big_tac.
-
-      (** RSBP preservation *)
-      unfold arr_stack_based_pointers in ASBP.
-      specialize (ASBP (Integers.Ptrofs.unsigned
-                          (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)))).
-      exploit ASBP; big_tac.
-      rewrite NORMALISE in H0. rewrite H1 in H0. assumption.
-
-      constructor; simplify. rewrite AssocMap.gso. rewrite AssocMap.gso.
-      assumption. lia.
-      assert (HPle: Ple dst (RTL.max_reg_function f))
-        by (eapply RTL.max_reg_function_def; eauto; simpl; auto).
-      unfold Ple in HPle. lia.
-      rewrite AssocMap.gso. rewrite AssocMap.gso.
-      assumption. lia.
-      assert (HPle: Ple dst (RTL.max_reg_function f))
-        by (eapply RTL.max_reg_function_def; eauto; simpl; auto).
-      unfold Ple in HPle. lia.
-
-      Unshelve.
-      exact (Values.Vint (Int.repr 0)).
-      exact tt.
-      exact (Values.Vint (Int.repr 0)).
-      exact tt.
-      exact (Values.Vint (Int.repr 0)).
-      exact tt.
-  Qed.
-  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. inv CONST. crush.
-
-      unfold Op.eval_addressing in H0.
-      destruct (Archi.ptr64) eqn:ARCHI; crush.
-
-      unfold reg_stack_based_pointers in RSBP.
-      pose proof (RSBP r0) as RSBPr0.
-
-      destruct (Registers.Regmap.get r0 rs) eqn:EQr0; crush.
-
-      rewrite ARCHI in H1. crush.
-      subst.
-
-      pose proof MASSOC as MASSOC'.
-      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 H8 in HPler0.
-      invert HPler0; try congruence.
-      rewrite EQr0 in H11.
-      invert H11.
-      clear H0. clear H8.
-
-      unfold check_address_parameter_unsigned in *;
-      unfold check_address_parameter_signed in *; crush.
-
-      remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ asr # r0))
-                                    (Integers.Ptrofs.of_int (Integers.Int.repr z))) as OFFSET.
-
-      (** Modular preservation proof *)
-      assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE.
-      { apply Mem.store_valid_access_3 in H1. unfold Mem.valid_access in *. simplify.
-        apply Zdivide_mod. assumption. }
-
-      (** Write bounds proof *)
-      assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as WRITE_BOUND_HIGH.
-      { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; crush; auto.
-        unfold stack_bounds in BOUNDS.
-        exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET) (Registers.Regmap.get src rs)); big_tac.
-        apply Integers.Ptrofs.unsigned_range_2. }
-
-      (** Start of proof proper *)
-      eexists. split.
-      eapply Smallstep.plus_one.
-      eapply HTL.step_module; eauto.
-      econstructor. econstructor. econstructor.
-      eapply Verilog.stmnt_runp_Vnonblock_arr. crush.
-      econstructor.
-      econstructor.
-      econstructor.
-      econstructor. econstructor. econstructor. econstructor.
-      econstructor. econstructor. econstructor. econstructor.
-
-      all: crush.
-
-      (** State Lookup *)
-      unfold Verilog.merge_regs.
-      crush.
-      unfold_merge.
-      apply AssocMap.gss.
-
-      (** Match states *)
-      econstructor; eauto.
-
-      (** Match assocmaps *)
-      unfold Verilog.merge_regs. crush. unfold_merge.
-      apply regs_lessdef_add_greater.
-      unfold Plt; lia.
-      assumption.
-
-      (** States well formed *)
-      unfold state_st_wf. inversion 1. crush.
-      unfold Verilog.merge_regs.
-      unfold_merge.
-      apply AssocMap.gss.
-
-      (** Equality proof *)
-
-      assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
-      inversion MASSOC; revert HeqOFFSET; subst; clear MASSOC; intros HeqOFFSET.
-
-      econstructor.
-      repeat split; crush.
-      unfold HTL.empty_stack.
-      crush.
-      unfold Verilog.merge_arrs.
-
-      rewrite AssocMap.gcombine.
-      2: { reflexivity. }
-      unfold Verilog.arr_assocmap_set.
-      rewrite AssocMap.gss.
-      unfold Verilog.merge_arr.
-      rewrite AssocMap.gss.
-      setoid_rewrite H7.
-      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.
-           rewrite HeqOFFSET.
-           exact H1.
-           apply Integers.Ptrofs.unsigned_range_2. }
-      constructor.
-      erewrite combine_lookup_second.
-      simplify.
-      assert (HPle : Ple src (RTL.max_reg_function f))
-        by (eapply RTL.max_reg_function_use; eauto; simpl; auto);
-      apply H11 in HPle.
-      destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; invert HPle; eauto.
-
-      rewrite <- array_set_len.
-      unfold arr_repeat. crush.
-      rewrite list_repeat_len. auto.
-
-      assert (HMul : 4 * ptr / 4 = Integers.Ptrofs.unsigned OFFSET / 4) by (f_equal; assumption).
-      rewrite Z.mul_comm in HMul.
-      rewrite Z_div_mult in HMul; try lia.
-      replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) in HMul by reflexivity.
-      rewrite <- PtrofsExtra.divu_unsigned in HMul; unfold_constants; try lia.
-      rewrite HMul. rewrite <- offset_expr_ok.
-      rewrite HeqOFFSET.
-      rewrite array_get_error_set_bound.
-      reflexivity.
-      unfold arr_length, arr_repeat. simpl.
-      rewrite list_repeat_len. rewrite HeqOFFSET in HMul. lia.
-
-      erewrite Mem.load_store_other with (m1 := m).
-      2: { exact H1. }
-      2: { right.
-           rewrite ZERO.
-           rewrite Integers.Ptrofs.add_zero_l.
-           rewrite Integers.Ptrofs.unsigned_repr.
-           simpl.
-           rewrite HeqOFFSET in *. simplify_val.
-           destruct (Z_le_gt_dec (4 * ptr + 4) (Integers.Ptrofs.unsigned OFFSET)); eauto.
-           rewrite HeqOFFSET in *. simplify_val.
-           left; auto.
-           rewrite HeqOFFSET in *. simplify_val.
-           right.
-           apply ZExtra.mod_0_bounds; try lia.
-           apply ZLib.Z_mod_mult'.
-           rewrite Z2Nat.id in H15; try lia.
-           apply Zmult_lt_compat_r with (p := 4) in H15; try lia.
-           rewrite ZLib.div_mul_undo in H15; try lia.
-           split; try lia.
-           apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia.
-      }
-
-      rewrite <- offset_expr_ok.
-      rewrite PtrofsExtra.divu_unsigned; auto; try (unfold_constants; lia).
-      destruct (ptr ==Z Integers.Ptrofs.unsigned OFFSET / 4).
-      apply Z.mul_cancel_r with (p := 4) in e; try lia.
-      rewrite ZLib.div_mul_undo in e; try lia.
-      rewrite combine_lookup_first.
-      eapply H9; eauto.
-
-      rewrite <- array_set_len.
-      unfold arr_repeat. crush.
-      rewrite list_repeat_len. auto.
-      rewrite array_gso.
-      unfold array_get_error.
-      unfold arr_repeat.
-      crush.
-      apply list_repeat_lookup.
-      lia.
-      unfold_constants.
-      intro.
-      apply Z2Nat.inj_iff in H13; rewrite HeqOFFSET in n0; try lia.
-      apply Z.div_pos; try lia.
-      apply Integers.Ptrofs.unsigned_range.
-      apply Integers.Ptrofs.unsigned_range_2.
-
-      assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO1 by reflexivity.
-      unfold arr_stack_based_pointers.
-      intros.
-      destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET).
-
-      crush.
-      erewrite Mem.load_store_same.
-      2: { rewrite ZERO1.
-           rewrite Integers.Ptrofs.add_zero_l.
-           rewrite e.
-           rewrite Integers.Ptrofs.unsigned_repr.
-           exact H1.
-           apply Integers.Ptrofs.unsigned_range_2. }
-      crush.
-      destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; try constructor.
-      destruct (Archi.ptr64); try discriminate.
-      pose proof (RSBP src). rewrite EQ_SRC in H11.
-      assumption.
-
-      simpl.
-      erewrite Mem.load_store_other with (m1 := m).
-      2: { exact H1. }
-      2: { right.
-           rewrite ZERO1.
-           rewrite Integers.Ptrofs.add_zero_l.
-           rewrite Integers.Ptrofs.unsigned_repr.
-           simpl.
-           destruct (Z_le_gt_dec (4 * ptr + 4) (Integers.Ptrofs.unsigned OFFSET)); eauto.
-           rewrite HeqOFFSET in *. simplify_val.
-           left; auto.
-           rewrite HeqOFFSET in *. simplify_val.
-           right.
-           apply ZExtra.mod_0_bounds; try lia.
-           apply ZLib.Z_mod_mult'.
-           invert H11.
-           apply Zmult_lt_compat_r with (p := 4) in H14; try lia.
-           rewrite ZLib.div_mul_undo in H14; try lia.
-           split; try lia.
-           apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia.
-      }
-      apply ASBP; assumption.
-
-      unfold stack_bounds in *. intros.
-      simpl.
-      assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
-      erewrite Mem.load_store_other with (m1 := m).
-      2: { exact H1. }
-      2: { rewrite HeqOFFSET in *. simplify_val.
-        right. right. simpl.
-           rewrite ZERO.
-           rewrite Integers.Ptrofs.add_zero_l.
-           rewrite Integers.Ptrofs.unsigned_repr; crush; try lia.
-           apply ZExtra.mod_0_bounds; crush; try lia. }
-      crush.
-      exploit (BOUNDS ptr); try lia. intros. crush.
-      exploit (BOUNDS ptr v); try lia. intros.
-      invert H11.
-      match goal with | |- ?x = _ => destruct x eqn:EQ end; try reflexivity.
-      assert (Mem.valid_access m AST.Mint32 sp'
-                               (Integers.Ptrofs.unsigned
-                                  (Integers.Ptrofs.add (Integers.Ptrofs.repr 0)
-                                                       (Integers.Ptrofs.repr ptr))) Writable).
-      { pose proof H1. eapply Mem.store_valid_access_2 in H11.
-        exact H11. eapply Mem.store_valid_access_3. eassumption. }
-      pose proof (Mem.valid_access_store m AST.Mint32 sp'
-                                         (Integers.Ptrofs.unsigned
-                                            (Integers.Ptrofs.add (Integers.Ptrofs.repr 0)
-                                                                 (Integers.Ptrofs.repr ptr))) v).
-      apply X in H11. invert H11. congruence.
-
-      constructor; simplify. unfold Verilog.merge_regs. unfold_merge.
-      rewrite AssocMap.gso.
-      assumption. lia.
-      unfold Verilog.merge_regs. unfold_merge.
-      rewrite AssocMap.gso.
-      assumption. lia.
-
-    + (** Preamble *)
-      invert MARR. inv CONST. crush.
-
-      unfold Op.eval_addressing in H0.
-      destruct (Archi.ptr64) eqn:ARCHI; crush.
-
-      unfold reg_stack_based_pointers in RSBP.
-      pose proof (RSBP r0) as RSBPr0.
-      pose proof (RSBP r1) as RSBPr1.
-
-      destruct (Registers.Regmap.get r0 rs) eqn:EQr0;
-      destruct (Registers.Regmap.get r1 rs) eqn:EQr1; crush.
-
-      rewrite ARCHI in H1. crush.
-      subst.
-      clear RSBPr1.
-
-      pose proof MASSOC as MASSOC'.
-      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 H8 in HPler0.
-      apply H11 in HPler1.
-      invert HPler0; invert HPler1; try congruence.
-      rewrite EQr0 in H13.
-      rewrite EQr1 in H14.
-      invert H13. invert H14.
-      clear H0. clear H8. clear H11.
-
-      unfold check_address_parameter_signed in *;
-      unfold check_address_parameter_unsigned in *; crush.
-
-      remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ asr # r0))
-                                    (Integers.Ptrofs.of_int
-                                       (Integers.Int.add (Integers.Int.mul (valueToInt asr # r1) (Integers.Int.repr z))
-                                                         (Integers.Int.repr z0)))) as OFFSET.
-
-      (** Modular preservation proof *)
-      assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE.
-      { apply Mem.store_valid_access_3 in H1. unfold Mem.valid_access in *. simplify.
-        apply Zdivide_mod. assumption. }
-
-      (** Write bounds proof *)
-      assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as WRITE_BOUND_HIGH.
-      { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; crush; auto.
-        unfold stack_bounds in BOUNDS.
-        exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET) (Registers.Regmap.get src rs)); auto.
-        split; try lia; apply Integers.Ptrofs.unsigned_range_2.
-        small_tac. }
-
-      (** Start of proof proper *)
-      eexists. split.
-      eapply Smallstep.plus_one.
-      eapply HTL.step_module; eauto.
-      econstructor. econstructor. econstructor.
-      eapply Verilog.stmnt_runp_Vnonblock_arr. crush.
-      econstructor.
-      econstructor. econstructor. econstructor. econstructor.
-      econstructor.
-      econstructor. econstructor. econstructor. econstructor.
-      econstructor. econstructor. econstructor. econstructor.
-      econstructor. econstructor. econstructor. econstructor.
-
-      all: crush.
-
-      (** State Lookup *)
-      unfold Verilog.merge_regs.
-      crush.
-      unfold_merge.
-      apply AssocMap.gss.
-
-      (** Match states *)
-      econstructor; eauto.
-
-      (** Match assocmaps *)
-      unfold Verilog.merge_regs. crush. unfold_merge.
-      apply regs_lessdef_add_greater.
-      unfold Plt; lia.
-      assumption.
-
-      (** States well formed *)
-      unfold state_st_wf. inversion 1. crush.
-      unfold Verilog.merge_regs.
-      unfold_merge.
-      apply AssocMap.gss.
-
-      (** Equality proof *)
-      assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
-      inversion MASSOC; revert HeqOFFSET; subst; clear MASSOC; intros HeqOFFSET.
-
-      econstructor.
-      repeat split; crush.
-      unfold HTL.empty_stack.
-      crush.
-      unfold Verilog.merge_arrs.
-
-      rewrite AssocMap.gcombine.
-      2: { reflexivity. }
-      unfold Verilog.arr_assocmap_set.
-      rewrite AssocMap.gss.
-      unfold Verilog.merge_arr.
-      rewrite AssocMap.gss.
-      setoid_rewrite H7.
-      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.
-           rewrite HeqOFFSET.
-           exact H1.
-           apply Integers.Ptrofs.unsigned_range_2. }
-      constructor.
-      erewrite combine_lookup_second.
-      simpl.
-      assert (Ple src (RTL.max_reg_function f))
-        by (eapply RTL.max_reg_function_use; eauto; simpl; auto);
-      apply H14 in H15.
-      destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; invert H15; eauto.
-
-      rewrite <- array_set_len.
-      unfold arr_repeat. crush.
-      rewrite list_repeat_len. auto.
-
-      assert (4 * ptr / 4 = Integers.Ptrofs.unsigned OFFSET / 4) by (f_equal; assumption).
-      rewrite Z.mul_comm in H15.
-      rewrite Z_div_mult in H15; try lia.
-      replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) in H15 by reflexivity.
-      rewrite <- PtrofsExtra.divu_unsigned in H15; unfold_constants; try lia.
-      rewrite H15. rewrite <- offset_expr_ok_2.
-      rewrite HeqOFFSET in *.
-      rewrite array_get_error_set_bound.
-      reflexivity.
-      unfold arr_length, arr_repeat. simpl.
-      rewrite list_repeat_len. lia.
-
-      erewrite Mem.load_store_other with (m1 := m).
-      2: { exact H1. }
-      2: { right.
-           rewrite ZERO.
-           rewrite Integers.Ptrofs.add_zero_l.
-           rewrite Integers.Ptrofs.unsigned_repr.
-           simpl.
-           destruct (Z_le_gt_dec (4 * ptr + 4) (Integers.Ptrofs.unsigned OFFSET)); eauto.
-           rewrite HeqOFFSET in *. simplify_val.
-           left; auto.
-           rewrite HeqOFFSET in *. simplify_val.
-           right.
-           apply ZExtra.mod_0_bounds; try lia.
-           apply ZLib.Z_mod_mult'.
-           rewrite Z2Nat.id in H17; try lia.
-           apply Zmult_lt_compat_r with (p := 4) in H17; try lia.
-           rewrite ZLib.div_mul_undo in H17; try lia.
-           split; try lia.
-           apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia.
-      }
-
-      rewrite <- offset_expr_ok_2.
-      rewrite PtrofsExtra.divu_unsigned; auto; try (unfold_constants; lia).
-      destruct (ptr ==Z Integers.Ptrofs.unsigned OFFSET / 4).
-      apply Z.mul_cancel_r with (p := 4) in e; try lia.
-      rewrite ZLib.div_mul_undo in e; try lia.
-      rewrite combine_lookup_first.
-      eapply H9; eauto.
-
-      rewrite <- array_set_len.
-      unfold arr_repeat. crush.
-      rewrite list_repeat_len. auto.
-      rewrite array_gso.
-      unfold array_get_error.
-      unfold arr_repeat.
-      crush.
-      apply list_repeat_lookup.
-      lia.
-      unfold_constants.
-      intro.
-      rewrite HeqOFFSET in *.
-      apply Z2Nat.inj_iff in H15; try lia.
-      apply Z.div_pos; try lia.
-      apply Integers.Ptrofs.unsigned_range.
-      apply Integers.Ptrofs.unsigned_range_2.
-
-      assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO1 by reflexivity.
-      unfold arr_stack_based_pointers.
-      intros.
-      destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET).
-
-      crush.
-      erewrite Mem.load_store_same.
-      2: { rewrite ZERO1.
-           rewrite Integers.Ptrofs.add_zero_l.
-           rewrite e.
-           rewrite Integers.Ptrofs.unsigned_repr.
-           exact H1.
-           apply Integers.Ptrofs.unsigned_range_2. }
-      crush.
-      destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; try constructor.
-      destruct (Archi.ptr64); try discriminate.
-      pose proof (RSBP src). rewrite EQ_SRC in H14.
-      assumption.
-
-      simpl.
-      erewrite Mem.load_store_other with (m1 := m).
-      2: { exact H1. }
-      2: { right.
-           rewrite ZERO1.
-           rewrite Integers.Ptrofs.add_zero_l.
-           rewrite Integers.Ptrofs.unsigned_repr.
-           simpl.
-           destruct (Z_le_gt_dec (4 * ptr + 4) (Integers.Ptrofs.unsigned OFFSET)); eauto.
-           rewrite HeqOFFSET in *. simplify_val.
-           left; auto.
-           rewrite HeqOFFSET in *. simplify_val.
-           right.
-           apply ZExtra.mod_0_bounds; try lia.
-           apply ZLib.Z_mod_mult'.
-           invert H14.
-           apply Zmult_lt_compat_r with (p := 4) in H16; try lia.
-           rewrite ZLib.div_mul_undo in H16; try lia.
-           split; try lia.
-           apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia.
-      }
-      apply ASBP; assumption.
-
-      unfold stack_bounds in *. intros.
-      simpl.
-      assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
-      erewrite Mem.load_store_other with (m1 := m).
-      2: { exact H1. }
-      2: { rewrite HeqOFFSET in *. simplify_val.
-           right. right. simpl.
-           rewrite ZERO.
-           rewrite Integers.Ptrofs.add_zero_l.
-           rewrite Integers.Ptrofs.unsigned_repr; crush; try lia.
-           apply ZExtra.mod_0_bounds; crush; try lia. }
-      crush.
-      exploit (BOUNDS ptr); try lia. intros. crush.
-      exploit (BOUNDS ptr v); try lia. intros.
-      simplify.
-      match goal with | |- ?x = _ => destruct x eqn:EQ end; try reflexivity.
-      assert (Mem.valid_access m AST.Mint32 sp'
-                               (Integers.Ptrofs.unsigned
-                                  (Integers.Ptrofs.add (Integers.Ptrofs.repr 0)
-                                                       (Integers.Ptrofs.repr ptr))) Writable).
-      { pose proof H1. eapply Mem.store_valid_access_2 in H14.
-        exact H14. eapply Mem.store_valid_access_3. eassumption. }
-      pose proof (Mem.valid_access_store m AST.Mint32 sp'
-                                         (Integers.Ptrofs.unsigned
-                                            (Integers.Ptrofs.add (Integers.Ptrofs.repr 0)
-                                                                 (Integers.Ptrofs.repr ptr))) v).
-      apply X in H14. invert H14. congruence.
-
-      constructor; simplify. unfold Verilog.merge_regs. unfold_merge. rewrite AssocMap.gso.
-      assumption. lia.
-      unfold Verilog.merge_regs. unfold_merge. rewrite AssocMap.gso.
-      assumption. lia.
-
-    + invert MARR. inv CONST. crush.
-
-      unfold Op.eval_addressing in H0.
-      destruct (Archi.ptr64) eqn:ARCHI; crush.
-      rewrite ARCHI in H0. crush.
-
-      unfold check_address_parameter_unsigned in *;
-      unfold check_address_parameter_signed in *; crush.
-
-      assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
-      rewrite ZERO in H1. clear ZERO.
-      rewrite Integers.Ptrofs.add_zero_l in H1.
-
-      remember i0 as OFFSET.
-
-      (** Modular preservation proof *)
-      assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE.
-      { apply Mem.store_valid_access_3 in H1. unfold Mem.valid_access in *. simplify.
-        apply Zdivide_mod. assumption. }
-
-      (** Write bounds proof *)
-      assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as WRITE_BOUND_HIGH.
-      { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:?EQ; crush; auto.
-        unfold stack_bounds in BOUNDS.
-        exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET) (Registers.Regmap.get src rs)); auto.
-        crush.
-        replace (Integers.Ptrofs.repr 0) with (Integers.Ptrofs.zero) by reflexivity.
-        small_tac. }
-
-      (** Start of proof proper *)
-      eexists. split.
-      eapply Smallstep.plus_one.
-      eapply HTL.step_module; eauto.
-      econstructor. econstructor. econstructor.
-      eapply Verilog.stmnt_runp_Vnonblock_arr. crush.
-      econstructor. econstructor. econstructor. econstructor.
-
-      all: crush.
-
-      (** State Lookup *)
-      unfold Verilog.merge_regs.
-      crush.
-      unfold_merge.
-      apply AssocMap.gss.
-
-      (** Match states *)
-      econstructor; eauto.
-
-      (** Match assocmaps *)
-      unfold Verilog.merge_regs. crush. unfold_merge.
-      apply regs_lessdef_add_greater.
-      unfold Plt; lia.
-      assumption.
-
-      (** States well formed *)
-      unfold state_st_wf. inversion 1. crush.
-      unfold Verilog.merge_regs.
-      unfold_merge.
-      apply AssocMap.gss.
-
-      (** Equality proof *)
-
-      assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
-      inversion MASSOC; revert HeqOFFSET; subst; clear MASSOC; intros HeqOFFSET.
-
-      econstructor.
-      repeat split; crush.
-      unfold HTL.empty_stack.
-      crush.
-      unfold Verilog.merge_arrs.
-
-      rewrite AssocMap.gcombine.
-      2: { reflexivity. }
-      unfold Verilog.arr_assocmap_set.
-      rewrite AssocMap.gss.
-      unfold Verilog.merge_arr.
-      rewrite AssocMap.gss.
-      setoid_rewrite H7.
-      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 <- offset_expr_ok_3.
-      rewrite array_get_error_set_bound.
-      reflexivity.
-      unfold arr_length, arr_repeat. simpl.
-      rewrite list_repeat_len. lia.
-
-      erewrite Mem.load_store_other with (m1 := m).
-      2: { exact H1. }
-      2: { right.
-           rewrite ZERO.
-           rewrite Integers.Ptrofs.add_zero_l.
-           rewrite Integers.Ptrofs.unsigned_repr.
-           simpl.
-           destruct (Z_le_gt_dec (4 * ptr + 4) (Integers.Ptrofs.unsigned OFFSET)); eauto.
-           right.
-           apply ZExtra.mod_0_bounds; try lia.
-           apply ZLib.Z_mod_mult'.
-           rewrite Z2Nat.id in H13; try lia.
-           apply Zmult_lt_compat_r with (p := 4) in H13; try lia.
-           rewrite ZLib.div_mul_undo in H13; try lia.
-           split; try lia.
-           apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia.
-      }
-
-      rewrite <- offset_expr_ok_3.
-      rewrite PtrofsExtra.divu_unsigned; auto; try (unfold_constants; lia).
-      destruct (ptr ==Z Integers.Ptrofs.unsigned OFFSET / 4).
-      apply Z.mul_cancel_r with (p := 4) in e; try lia.
-      rewrite ZLib.div_mul_undo in e; try lia.
-      rewrite combine_lookup_first.
-      eapply H9; eauto.
-
-      rewrite <- array_set_len.
-      unfold arr_repeat. crush.
-      rewrite list_repeat_len. auto.
-      rewrite array_gso.
-      unfold array_get_error.
-      unfold arr_repeat.
-      crush.
-      apply list_repeat_lookup.
-      lia.
-      unfold_constants.
-      intro.
-      apply Z2Nat.inj_iff in H8; try lia.
-      apply Z.div_pos; try lia.
-      apply Integers.Ptrofs.unsigned_range.
-
-      assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
-      unfold arr_stack_based_pointers.
-      intros.
-      destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET).
-
-      crush.
-      erewrite Mem.load_store_same.
-      2: { rewrite ZERO.
-           rewrite Integers.Ptrofs.add_zero_l.
-           rewrite e.
-           rewrite Integers.Ptrofs.unsigned_repr.
-           exact H1.
-           apply Integers.Ptrofs.unsigned_range_2. }
-      crush.
-      destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; try constructor.
-      destruct (Archi.ptr64); try discriminate.
-      pose proof (RSBP src). rewrite EQ_SRC in H0.
-      assumption.
-
-      simpl.
-      erewrite Mem.load_store_other with (m1 := m).
-      2: { exact H1. }
-      2: { right.
-           rewrite ZERO.
-           rewrite Integers.Ptrofs.add_zero_l.
-           rewrite Integers.Ptrofs.unsigned_repr.
-           simpl.
-           destruct (Z_le_gt_dec (4 * ptr + 4) (Integers.Ptrofs.unsigned OFFSET)); eauto.
-           right.
-           apply ZExtra.mod_0_bounds; try lia.
-           apply ZLib.Z_mod_mult'.
-           invert H0.
-           apply Zmult_lt_compat_r with (p := 4) in H11; try lia.
-           rewrite ZLib.div_mul_undo in H11; try lia.
-           split; try lia.
-           apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia.
-      }
-      apply ASBP; assumption.
-
-      unfold stack_bounds in *. intros.
-      simpl.
-      assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity.
-      erewrite Mem.load_store_other with (m1 := m).
-      2: { exact H1. }
-      2: { right. right. simpl.
-           rewrite ZERO.
-           rewrite Integers.Ptrofs.add_zero_l.
-           rewrite Integers.Ptrofs.unsigned_repr; crush; try lia.
-           apply ZExtra.mod_0_bounds; crush; try lia. }
-      crush.
-      exploit (BOUNDS ptr); try lia. intros. crush.
-      exploit (BOUNDS ptr v); try lia. intros.
-      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.
-
-      constructor; simplify. unfold Verilog.merge_regs. unfold_merge. rewrite AssocMap.gso.
-      assumption. lia.
-      unfold Verilog.merge_regs. unfold_merge. rewrite AssocMap.gso.
-      assumption. lia.
-
-      Unshelve.
-      exact tt.
-      exact (Values.Vint (Int.repr 0)).
-      exact tt.
-      exact (Values.Vint (Int.repr 0)).
-      exact tt.
-      exact (Values.Vint (Int.repr 0)).
-  Qed.
-  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.
-    destruct b.
-    - eexists. split. apply Smallstep.plus_one.
-      clear H33.
-      eapply HTL.step_module; eauto.
-      inv CONST; assumption.
-      inv CONST; assumption.
-      econstructor; simpl; trivial.
-      constructor; trivial.
-      eapply Verilog.erun_Vternary_true; simpl; eauto.
-      eapply eval_cond_correct; eauto. intros.
-      intros. eapply RTL.max_reg_function_use. apply H22. auto.
-      econstructor. auto.
-      simpl. econstructor. unfold Verilog.merge_regs. unfold_merge. simpl.
-      apply AssocMap.gss.
-
-      inv MARR. inv CONST.
-      big_tac.
-      constructor; rewrite AssocMap.gso; simplify; try assumption; lia.
-    - eexists. split. apply Smallstep.plus_one.
-      clear H32.
-      eapply HTL.step_module; eauto.
-      inv CONST; assumption.
-      inv CONST; assumption.
-      econstructor; simpl; trivial.
-      constructor; trivial.
-      eapply Verilog.erun_Vternary_false; simpl; eauto.
-      eapply eval_cond_correct; eauto. intros.
-      intros. eapply RTL.max_reg_function_use. apply H22. auto.
-      econstructor. auto.
-      simpl. econstructor. unfold Verilog.merge_regs. unfold_merge. simpl.
-      apply AssocMap.gss.
-
-      inv MARR. inv CONST.
-      big_tac.
-      constructor; rewrite AssocMap.gso; simplify; try assumption; lia.
-
-      Unshelve. all: exact tt.
-  Qed.
-  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.
-  
-  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
deleted file mode 100644
index 541f9fa..0000000
--- a/src/translation/HTLgenspec.v
+++ /dev/null
@@ -1,641 +0,0 @@
-(*
- * Vericert: 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/>.
- *)
-
-From compcert Require RTL Op Maps Errors.
-From compcert Require Import Maps Integers.
-From vericert Require Import Vericertlib Verilog ValueInt HTL HTLgen AssocMap.
-Require Import Lia.
-
-Hint Resolve Maps.PTree.elements_keys_norepet : htlspec.
-Hint Resolve Maps.PTree.elements_correct : htlspec.
-
-Remark bind_inversion:
-  forall (A B: Type) (f: mon A) (g: A -> mon B)
-         (y: B) (s1 s3: st) (i: st_incr s1 s3),
-    bind f g s1 = OK y s3 i ->
-    exists x, exists s2, exists i1, exists i2,
-            f s1 = OK x s2 i1 /\ g x s2 = OK y s3 i2.
-Proof.
-  intros until i. unfold bind. destruct (f s1); intros.
-  discriminate.
-  exists a; exists s'; exists s.
-  destruct (g a s'); inv H.
-  exists s0; auto.
-Qed.
-
-Remark bind2_inversion:
-  forall (A B C: Type) (f: mon (A*B)) (g: A -> B -> mon C)
-         (z: C) (s1 s3: st) (i: st_incr s1 s3),
-    bind2 f g s1 = OK z s3 i ->
-    exists x, exists y, exists s2, exists i1, exists i2,
-              f s1 = OK (x, y) s2 i1 /\ g x y s2 = OK z s3 i2.
-Proof.
-  unfold bind2; intros.
-  exploit bind_inversion; eauto.
-  intros [[x y] [s2 [i1 [i2 [P Q]]]]]. simpl in Q.
-  exists x; exists y; exists s2; exists i1; exists i2; auto.
-Qed.
-
-Ltac monadInv1 H :=
-  match type of H with
-  | (OK _ _ _ = OK _ _ _) =>
-    inversion H; clear H; try subst
-  | (Error _ _ = OK _ _ _) =>
-    discriminate
-  | (ret _ _ = OK _ _ _) =>
-    inversion H; clear H; try subst
-  | (error _ _ = OK _ _ _) =>
-    discriminate
-  | (bind ?F ?G ?S = OK ?X ?S' ?I) =>
-    let x := fresh "x" in (
-      let s := fresh "s" in (
-        let i1 := fresh "INCR" in (
-          let i2 := fresh "INCR" in (
-            let EQ1 := fresh "EQ" in (
-              let EQ2 := fresh "EQ" in (
-                destruct (bind_inversion _ _ F G X S S' I H) as [x [s [i1 [i2 [EQ1 EQ2]]]]];
-                clear H;
-                try (monadInv1 EQ2)))))))
-  | (bind2 ?F ?G ?S = OK ?X ?S' ?I) =>
-    let x1 := fresh "x" in (
-      let x2 := fresh "x" in (
-        let s := fresh "s" in (
-          let i1 := fresh "INCR" in (
-            let i2 := fresh "INCR" in (
-              let EQ1 := fresh "EQ" in (
-                let EQ2 := fresh "EQ" in (
-                  destruct (bind2_inversion _ _ _ F G X S S' I H) as [x1 [x2 [s [i1 [i2 [EQ1 EQ2]]]]]];
-                  clear H;
-                  try (monadInv1 EQ2))))))))
-  end.
-
-Ltac monadInv H :=
-  match type of H with
-  | (ret _ _ = OK _ _ _) => monadInv1 H
-  | (error _ _ = OK _ _ _) => monadInv1 H
-  | (bind ?F ?G ?S = OK ?X ?S' ?I) => monadInv1 H
-  | (bind2 ?F ?G ?S = OK ?X ?S' ?I) => monadInv1 H
-  | (?F _ _ _ _ _ _ _ _ = OK _ _ _) =>
-    ((progress simpl in H) || unfold F in H); monadInv1 H
-  | (?F _ _ _ _ _ _ _ = OK _ _ _) =>
-    ((progress simpl in H) || unfold F in H); monadInv1 H
-  | (?F _ _ _ _ _ _ = OK _ _ _) =>
-    ((progress simpl in H) || unfold F in H); monadInv1 H
-  | (?F _ _ _ _ _ = OK _ _ _) =>
-    ((progress simpl in H) || unfold F in H); monadInv1 H
-  | (?F _ _ _ _ = OK _ _ _) =>
-    ((progress simpl in H) || unfold F in H); monadInv1 H
-  | (?F _ _ _ = OK _ _ _) =>
-    ((progress simpl in H) || unfold F in H); monadInv1 H
-  | (?F _ _ = OK _ _ _) =>
-    ((progress simpl in H) || unfold F in H); monadInv1 H
-  | (?F _ = OK _ _ _) =>
-    ((progress simpl in H) || unfold F in H); monadInv1 H
-  end.
-
-(** * Relational specification of the translation *)
-
-(** We now define inductive predicates that characterise the fact that the
-statemachine that is created by the translation contains the correct
-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 :
-    tr_instr fin rtrn st stk (RTL.Ireturn None) (Vseq (block fin (Vlit (ZToValue 1%Z)))
-                                                  (block rtrn (Vlit (ZToValue 0%Z)))) Vskip
-| tr_instr_Ireturn_Some :
-    forall r,
-      tr_instr fin rtrn st stk (RTL.Ireturn (Some r))
-               (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vvar r))) Vskip
-| tr_instr_Iload :
-    forall mem addr args s s' i c dst n,
-      Z.pos n <= Int.max_unsigned ->
-      translate_arr_access mem addr args stk s = OK c s' i ->
-      tr_instr fin rtrn st stk (RTL.Iload mem addr args dst n) (nonblock dst c) (state_goto st n)
-| tr_instr_Istore :
-    forall mem addr args s s' i c src n,
-      Z.pos n <= Int.max_unsigned ->
-      translate_arr_access mem addr args stk s = OK c s' i ->
-      tr_instr fin rtrn st stk (RTL.Istore mem addr args src n) (Vnonblock c (Vvar src))
-               (state_goto st n).
-(*| tr_instr_Ijumptable :
-    forall cexpr tbl r,
-    cexpr = tbl_to_case_expr st tbl ->
-    tr_instr fin rtrn st stk (RTL.Ijumptable r tbl) (Vskip) (Vcase (Vvar r) cexpr (Some Vskip)).*)
-Hint Constructors tr_instr : htlspec.
-
-Inductive tr_code (c : RTL.code) (pc : RTL.node) (i : RTL.instruction) (stmnts trans : PTree.t stmnt)
-          (fin rtrn st stk : reg) : Prop :=
-  tr_code_intro :
-    forall s t,
-      c!pc = Some i ->
-      stmnts!pc = Some s ->
-      trans!pc = Some t ->
-      tr_instr fin rtrn st stk i s t ->
-      tr_code c pc i stmnts trans fin rtrn st stk.
-Hint Constructors tr_code : htlspec.
-
-Inductive tr_module (f : RTL.function) : module -> Prop :=
-  tr_module_intro :
-    forall data control fin rtrn st stk stk_len m start rst clk scldecls arrdecls wf,
-      m = (mkmodule f.(RTL.fn_params)
-                        data
-                        control
-                        f.(RTL.fn_entrypoint)
-                        st stk stk_len fin rtrn start rst clk scldecls arrdecls wf) ->
-      (forall pc i, Maps.PTree.get pc f.(RTL.fn_code) = Some i ->
-               tr_code f.(RTL.fn_code) pc i data control fin rtrn st stk) ->
-      stk_len = Z.to_nat (f.(RTL.fn_stacksize) / 4) ->
-      Z.modulo (f.(RTL.fn_stacksize)) 4 = 0 ->
-      0 <= f.(RTL.fn_stacksize) < Integers.Ptrofs.modulus ->
-      st = ((RTL.max_reg_function f) + 1)%positive ->
-      fin = ((RTL.max_reg_function f) + 2)%positive ->
-      rtrn = ((RTL.max_reg_function f) + 3)%positive ->
-      stk = ((RTL.max_reg_function f) + 4)%positive ->
-      start = ((RTL.max_reg_function f) + 5)%positive ->
-      rst = ((RTL.max_reg_function f) + 6)%positive ->
-      clk = ((RTL.max_reg_function f) + 7)%positive ->
-      tr_module f m.
-Hint Constructors tr_module : htlspec.
-
-Lemma create_reg_datapath_trans :
-  forall sz s s' x i iop,
-    create_reg iop sz s = OK x s' i ->
-    s.(st_datapath) = s'.(st_datapath).
-Proof. intros. monadInv H. trivial. Qed.
-Hint Resolve create_reg_datapath_trans : htlspec.
-
-Lemma create_reg_controllogic_trans :
-  forall sz s s' x i iop,
-    create_reg iop sz s = OK x s' i ->
-    s.(st_controllogic) = s'.(st_controllogic).
-Proof. intros. monadInv H. trivial. Qed.
-Hint Resolve create_reg_controllogic_trans : htlspec.
-
-Lemma declare_reg_datapath_trans :
-  forall sz s s' x i iop r,
-    declare_reg iop r sz s = OK x s' i ->
-    s.(st_datapath) = s'.(st_datapath).
-Proof. intros. monadInv H. trivial. Qed.
-Hint Resolve create_reg_datapath_trans : htlspec.
-
-Lemma declare_reg_controllogic_trans :
-  forall sz s s' x i iop r,
-    declare_reg iop r sz s = OK x s' i ->
-    s.(st_controllogic) = s'.(st_controllogic).
-Proof. intros. monadInv H. trivial. Qed.
-Hint Resolve create_reg_controllogic_trans : htlspec.
-
-Lemma declare_reg_freshreg_trans :
-  forall sz s s' x i iop r,
-    declare_reg iop r sz s = OK x s' i ->
-    s.(st_freshreg) = s'.(st_freshreg).
-Proof. inversion 1; auto. Qed.
-Hint Resolve declare_reg_freshreg_trans : htlspec.
-
-Lemma create_arr_datapath_trans :
-  forall sz ln s s' x i iop,
-    create_arr iop sz ln s = OK x s' i ->
-    s.(st_datapath) = s'.(st_datapath).
-Proof. intros. monadInv H. trivial. Qed.
-Hint Resolve create_arr_datapath_trans : htlspec.
-
-Lemma create_arr_controllogic_trans :
-  forall sz ln s s' x i iop,
-    create_arr iop sz ln s = OK x s' i ->
-    s.(st_controllogic) = s'.(st_controllogic).
-Proof. intros. monadInv H. trivial. Qed.
-Hint Resolve create_arr_controllogic_trans : htlspec.
-
-Lemma get_refl_x :
-  forall s s' x i,
-    get s = OK x s' i ->
-    s = x.
-Proof. inversion 1. trivial. Qed.
-Hint Resolve get_refl_x : htlspec.
-
-Lemma get_refl_s :
-  forall s s' x i,
-    get s = OK x s' i ->
-    s = s'.
-Proof. inversion 1. trivial. Qed.
-Hint Resolve get_refl_s : htlspec.
-
-Ltac inv_incr :=
-  repeat match goal with
-  | [ H: create_reg _ _ ?s = OK _ ?s' _ |- _ ] =>
-    let H1 := fresh "H" in
-    assert (H1 := H); eapply create_reg_datapath_trans in H;
-    eapply create_reg_controllogic_trans in H1
-  | [ H: create_arr _ _ _ ?s = OK _ ?s' _ |- _ ] =>
-    let H1 := fresh "H" in
-    assert (H1 := H); eapply create_arr_datapath_trans in H;
-    eapply create_arr_controllogic_trans in H1
-  | [ H: get ?s = OK _ _ _ |- _ ] =>
-    let H1 := fresh "H" in
-    assert (H1 := H); apply get_refl_x in H; apply get_refl_s in H1;
-    subst
-  | [ H: st_prop _ _ |- _ ] => unfold st_prop in H; destruct H
-  | [ H: st_incr _ _ |- _ ] => destruct st_incr
-  end.
-
-Lemma collect_controllogic_trans :
-  forall A f l cs cs' ci,
-  (forall s s' x i y, f y s = OK x s' i -> s.(st_controllogic) = s'.(st_controllogic)) ->
-  @HTLMonadExtra.collectlist A f l cs = OK tt cs' ci -> cs.(st_controllogic) = cs'.(st_controllogic).
-Proof.
-  induction l; intros; monadInv H0.
-  - trivial.
-  - apply H in EQ. rewrite EQ. eauto.
-Qed.
-
-Lemma collect_datapath_trans :
-  forall A f l cs cs' ci,
-  (forall s s' x i y, f y s = OK x s' i -> s.(st_datapath) = s'.(st_datapath)) ->
-  @HTLMonadExtra.collectlist A f l cs = OK tt cs' ci -> cs.(st_datapath) = cs'.(st_datapath).
-Proof.
-  induction l; intros; monadInv H0.
-  - trivial.
-  - apply H in EQ. rewrite EQ. eauto.
-Qed.
-
-Lemma collect_freshreg_trans :
-  forall A f l cs cs' ci,
-  (forall s s' x i y, f y s = OK x s' i -> s.(st_freshreg) = s'.(st_freshreg)) ->
-  @HTLMonadExtra.collectlist A f l cs = OK tt cs' ci -> cs.(st_freshreg) = cs'.(st_freshreg).
-Proof.
-  induction l; intros; monadInv H0.
-  - trivial.
-  - apply H in EQ. rewrite EQ. eauto.
-Qed.
-
-Lemma collect_declare_controllogic_trans :
-  forall io n l s s' i,
-  HTLMonadExtra.collectlist (fun r : reg => declare_reg io r n) l s = OK tt s' i ->
-  s.(st_controllogic) = s'.(st_controllogic).
-Proof.
-  intros. eapply collect_controllogic_trans; try eassumption.
-  intros. eapply declare_reg_controllogic_trans. simpl in H0. eassumption.
-Qed.
-
-Lemma collect_declare_datapath_trans :
-  forall io n l s s' i,
-  HTLMonadExtra.collectlist (fun r : reg => declare_reg io r n) l s = OK tt s' i ->
-  s.(st_datapath) = s'.(st_datapath).
-Proof.
-  intros. eapply collect_datapath_trans; try eassumption.
-  intros. eapply declare_reg_datapath_trans. simpl in H0. eassumption.
-Qed.
-
-Lemma collect_declare_freshreg_trans :
-  forall io n l s s' i,
-  HTLMonadExtra.collectlist (fun r : reg => declare_reg io r n) l s = OK tt s' i ->
-  s.(st_freshreg) = s'.(st_freshreg).
-Proof.
-  intros. eapply collect_freshreg_trans; try eassumption.
-  inversion 1. auto.
-Qed.
-
-Ltac unfold_match H :=
-  match type of H with
-  | context[match ?g with _ => _ end] => destruct g eqn:?; try discriminate
-  end.
-
-Lemma translate_eff_addressing_freshreg_trans :
-  forall op args s r s' i,
-  translate_eff_addressing op args s = OK r s' i ->
-  s.(st_freshreg) = s'.(st_freshreg).
-Proof.
-  destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto.
-Qed.
-Hint Resolve translate_eff_addressing_freshreg_trans : htlspec.
-
-Lemma translate_comparison_freshreg_trans :
-  forall op args s r s' i,
-  translate_comparison op args s = OK r s' i ->
-  s.(st_freshreg) = s'.(st_freshreg).
-Proof.
-  destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto.
-Qed.
-Hint Resolve translate_comparison_freshreg_trans : htlspec.
-
-Lemma translate_comparisonu_freshreg_trans :
-  forall op args s r s' i,
-  translate_comparisonu op args s = OK r s' i ->
-  s.(st_freshreg) = s'.(st_freshreg).
-Proof.
-  destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto.
-Qed.
-Hint Resolve translate_comparisonu_freshreg_trans : htlspec.
-
-Lemma translate_comparison_imm_freshreg_trans :
-  forall op args s r s' i n,
-  translate_comparison_imm op args n s = OK r s' i ->
-  s.(st_freshreg) = s'.(st_freshreg).
-Proof.
-  destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto.
-Qed.
-Hint Resolve translate_comparison_imm_freshreg_trans : htlspec.
-
-Lemma translate_comparison_immu_freshreg_trans :
-  forall op args s r s' i n,
-  translate_comparison_immu op args n s = OK r s' i ->
-  s.(st_freshreg) = s'.(st_freshreg).
-Proof.
-  destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto.
-Qed.
-Hint Resolve translate_comparison_immu_freshreg_trans : htlspec.
-
-Lemma translate_condition_freshreg_trans :
-  forall op args s r s' i,
-  translate_condition op args s = OK r s' i ->
-  s.(st_freshreg) = s'.(st_freshreg).
-Proof.
-  destruct op; intros; simpl in *; repeat (unfold_match H); inv H; eauto with htlspec.
-Qed.
-Hint Resolve translate_condition_freshreg_trans : htlspec.
-
-Lemma translate_instr_freshreg_trans :
-  forall op args s r s' i,
-  translate_instr op args s = OK r s' i ->
-  s.(st_freshreg) = s'.(st_freshreg).
-Proof.
-  destruct op; intros; simpl in *; repeat (unfold_match H); inv H; eauto with htlspec.
-  monadInv H1. eauto with htlspec.
-Qed.
-Hint Resolve translate_instr_freshreg_trans : htlspec.
-
-Lemma translate_arr_access_freshreg_trans :
-  forall mem addr args st s r s' i,
-  translate_arr_access mem addr args st s = OK r s' i ->
-  s.(st_freshreg) = s'.(st_freshreg).
-Proof.
-  intros. unfold translate_arr_access in H. repeat (unfold_match H); inv H; eauto with htlspec.
-Qed.
-Hint Resolve translate_arr_access_freshreg_trans : htlspec.
-
-Lemma add_instr_freshreg_trans :
-  forall n n' st s r s' i,
-  add_instr n n' st s = OK r s' i ->
-  s.(st_freshreg) = s'.(st_freshreg).
-Proof. intros. unfold add_instr in H. repeat (unfold_match H). inv H. auto. Qed.
-Hint Resolve add_instr_freshreg_trans : htlspec.
-
-Lemma add_branch_instr_freshreg_trans :
-  forall n n0 n1 e s r s' i,
-  add_branch_instr e n n0 n1 s = OK r s' i ->
-  s.(st_freshreg) = s'.(st_freshreg).
-Proof. intros. unfold add_branch_instr in H. repeat (unfold_match H). inv H. auto. Qed.
-Hint Resolve add_branch_instr_freshreg_trans : htlspec.
-
-Lemma add_node_skip_freshreg_trans :
-  forall n1 n2 s r s' i,
-  add_node_skip n1 n2 s = OK r s' i ->
-  s.(st_freshreg) = s'.(st_freshreg).
-Proof. intros. unfold add_node_skip in H. repeat (unfold_match H). inv H. auto. Qed.
-Hint Resolve add_node_skip_freshreg_trans : htlspec.
-
-Lemma add_instr_skip_freshreg_trans :
-  forall n1 n2 s r s' i,
-  add_instr_skip n1 n2 s = OK r s' i ->
-  s.(st_freshreg) = s'.(st_freshreg).
-Proof. intros. unfold add_instr_skip in H. repeat (unfold_match H). inv H. auto. Qed.
-Hint Resolve add_instr_skip_freshreg_trans : htlspec.
-
-Lemma transf_instr_freshreg_trans :
-  forall fin ret st instr s v s' i,
-    transf_instr fin ret st instr s = OK v s' i ->
-    s.(st_freshreg) = s'.(st_freshreg).
-Proof.
-  intros. destruct instr eqn:?. subst. unfold transf_instr in H.
-  destruct i0; try (monadInv H); try (unfold_match H); eauto with htlspec.
-  - monadInv H. apply add_instr_freshreg_trans in EQ2. apply translate_instr_freshreg_trans in EQ.
-    apply declare_reg_freshreg_trans in EQ1. congruence.
-  - monadInv H. apply add_instr_freshreg_trans in EQ2. apply translate_arr_access_freshreg_trans in EQ.
-    apply declare_reg_freshreg_trans in EQ1. congruence.
-  - monadInv H. apply add_instr_freshreg_trans in EQ0. apply translate_arr_access_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.
-Hint Resolve transf_instr_freshreg_trans : htlspec.
-
-Lemma collect_trans_instr_freshreg_trans :
-  forall fin ret st l s s' i,
-  HTLMonadExtra.collectlist (transf_instr fin ret st) l s = OK tt s' i ->
-  s.(st_freshreg) = s'.(st_freshreg).
-Proof.
-  intros. eapply collect_freshreg_trans; try eassumption.
-  eauto with htlspec.
-Qed.
-
-Ltac rewrite_states :=
-  match goal with
-  | [ H: ?x ?s = ?x ?s' |- _ ] =>
-    let c1 := fresh "c" in
-    let c2 := fresh "c" in
-    remember (?x ?s) as c1; remember (?x ?s') as c2; try subst
-  end.
-
-Ltac inv_add_instr' H :=
-  match type of H with
-  | ?f _ _ = OK _ _ _ => unfold f in H
-  | ?f _ _ _ = OK _ _ _ => unfold f in H
-  | ?f _ _ _ _ = OK _ _ _ => unfold f in H
-  | ?f _ _ _ _ _ = OK _ _ _ => unfold f in H
-  | ?f _ _ _ _ _ _ = OK _ _ _ => unfold f in H
-  end; repeat unfold_match H; inversion H.
-
-Ltac inv_add_instr :=
-  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 _ _] |- _ =>
-    monadInv H; inv_incr; inv_add_instr
-  | H: context[add_instr _ _ _ _] |- _ =>
-    inv_add_instr' H
-  | H: context[add_instr _ _ _] |- _ =>
-    monadInv H; inv_incr; inv_add_instr
-  | H: context[add_branch_instr _ _ _ _ _] |- _ =>
-    inv_add_instr' H
-  | H: context[add_branch_instr _ _ _ _] |- _ =>
-    monadInv H; inv_incr; inv_add_instr
-  | H: context[add_node_skip _ _ _] |- _ =>
-    inv_add_instr' H
-  | H: context[add_node_skip _ _] |- _ =>
-    monadInv H; inv_incr; inv_add_instr
-  end.
-
-Ltac destruct_optional :=
-  match goal with H: option ?r |- _ => destruct H end.
-
-Lemma iter_expand_instr_spec :
-  forall l fin rtrn stack s s' i x c,
-    HTLMonadExtra.collectlist (transf_instr fin rtrn stack) l s = OK x s' i ->
-    list_norepet (List.map fst l) ->
-    (forall pc instr, In (pc, instr) l -> c!pc = Some instr) ->
-    (forall pc instr, In (pc, instr) l ->
-                      c!pc = Some instr ->
-                      tr_code c pc instr s'.(st_datapath) s'.(st_controllogic) fin rtrn s'.(st_st) stack).
-Proof.
-  induction l; simpl; intros; try contradiction.
-  destruct a as [pc1 instr1]; simpl in *. inv H0. monadInv H. inv_incr.
-  destruct (peq pc pc1).
-  - subst.
-    destruct instr1 eqn:?; try discriminate;
-      try destruct_optional; inv_add_instr; econstructor; try assumption.
-    + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence.
-    + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence.
-    + inversion H2. inversion H9. rewrite H. apply tr_instr_Inop.
-      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 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 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.
-
-    + 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; try (apply Z.leb_le; apply andb_prop in EQN; apply EQN).
-        eauto with htlspec.
-      * apply in_map with (f := fst) in H2. contradiction.
-
-    (*+ destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence.
-    + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence.
-    + inversion H2.
-      * inversion H14. constructor. congruence.
-      * apply in_map with (f := fst) in H14. contradiction.
-      *)
-    + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence.
-    + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence.
-    + inversion H2.
-      * inversion H9.
-        replace (st_st s2) with (st_st s0) by congruence.
-        eauto with htlspec.
-      * apply in_map with (f := fst) in H9. contradiction.
-
-    + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence.
-    + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence.
-    + inversion H2.
-      * inversion H9.
-        replace (st_st s2) with (st_st s0) by congruence.
-        eauto with htlspec.
-      * apply in_map with (f := fst) in H9. contradiction.
-
-  - eapply IHl. apply EQ0. assumption.
-    destruct H2. inversion H2. subst. contradiction.
-    intros. specialize H1 with pc0 instr0. destruct H1. tauto. trivial.
-    destruct H2. inv H2. contradiction. assumption. assumption.
-Qed.
-Hint Resolve iter_expand_instr_spec : htlspec.
-
-Lemma create_arr_inv : forall w x y z a b c d,
-    create_arr w x y z = OK (a, b) c d ->
-    y = b /\ a = z.(st_freshreg) /\ c.(st_freshreg) = Pos.succ (z.(st_freshreg)).
-Proof.
-  inversion 1; split; auto.
-Qed.
-
-Lemma create_reg_inv : forall a b s r s' i,
-    create_reg a b s = OK r s' i ->
-    r = s.(st_freshreg) /\ s'.(st_freshreg) = Pos.succ (s.(st_freshreg)).
-Proof.
-  inversion 1; auto.
-Qed.
-
-Theorem transl_module_correct :
-  forall f m,
-    transl_module f = Errors.OK m -> tr_module f m.
-Proof.
-  intros until m.
-  unfold transl_module.
-  unfold run_mon.
-  destruct (transf_module f (max_state f)) eqn:?; try discriminate.
-  intros. inv H.
-  inversion s; subst.
-
-  unfold transf_module in *.
-  unfold stack_correct in *.
-  destruct (0 <=? RTL.fn_stacksize f) eqn:STACK_BOUND_LOW;
-    destruct (RTL.fn_stacksize f <? Integers.Ptrofs.modulus) eqn:STACK_BOUND_HIGH;
-    destruct (RTL.fn_stacksize f mod 4 =? 0) eqn:STACK_ALIGN;
-    crush;
-    monadInv Heqr.
-
-  repeat unfold_match EQ9. monadInv EQ9.
-
-  (* TODO: We should be able to fold this into the automation. *)
-  pose proof (create_arr_inv _ _ _ _ _ _ _ _ EQ0) as STK_LEN. inv STK_LEN. inv H5.
-  pose proof (create_reg_inv _ _ _ _ _ _ EQ) as FIN_VAL. inv FIN_VAL.
-  pose proof (create_reg_inv _ _ _ _ _ _ EQ1) as RET_VAL. inv RET_VAL.
-  destruct x3. destruct x4.
-  pose proof (collect_trans_instr_freshreg_trans _ _ _ _ _ _ _ EQ2) as TR_INSTR.
-  pose proof (collect_declare_freshreg_trans _ _ _ _ _ _ EQ3) as TR_DEC.
-  pose proof (create_reg_inv _ _ _ _ _ _ EQ4) as START_VAL. inv START_VAL.
-  pose proof (create_reg_inv _ _ _ _ _ _ EQ5) as RESET_VAL. inv RESET_VAL.
-  pose proof (create_reg_inv _ _ _ _ _ _ EQ6) as CLK_VAL. inv CLK_VAL.
-  rewrite H9 in *. rewrite H8 in *. replace (st_freshreg s4) with (st_freshreg s2) in * by congruence.
-  rewrite H6 in *. rewrite H7 in *. rewrite H5 in *. simpl in *.
-  inv_incr.
-  econstructor; simpl; auto; try lia.
-  intros.
-  assert (EQ3D := EQ3).
-  apply collect_declare_datapath_trans in EQ3.
-  apply collect_declare_controllogic_trans in EQ3D.
-  replace (st_controllogic s10) with (st_controllogic s3) by congruence.
-  replace (st_datapath s10) with (st_datapath s3) by congruence.
-  replace (st_st s10) with (st_st s3) by congruence.
-  eapply iter_expand_instr_spec; eauto with htlspec.
-  apply PTree.elements_complete.
-Qed.
diff --git a/src/translation/Veriloggen.v b/src/translation/Veriloggen.v
deleted file mode 100644
index a0be0fa..0000000
--- a/src/translation/Veriloggen.v
+++ /dev/null
@@ -1,65 +0,0 @@
-(*
- * Vericert: 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/>.
- *)
-
-From compcert Require Import Maps.
-From compcert Require Errors.
-From compcert Require Import AST.
-From vericert Require Import Verilog HTL Vericertlib AssocMap ValueInt.
-
-Definition transl_list_fun (a : node * Verilog.stmnt) :=
-  let (n, stmnt) := a in
-  (Vlit (posToValue n), stmnt).
-
-Definition transl_list st := map transl_list_fun st.
-
-Definition scl_to_Vdecl_fun (a : reg * (option io * scl_decl)) :=
-  match a with (r, (io, VScalar sz)) => (Vdecl io r sz) end.
-
-Definition scl_to_Vdecl scldecl := map scl_to_Vdecl_fun scldecl.
-
-Definition arr_to_Vdeclarr_fun (a : reg * (option io * arr_decl)) :=
-  match a with (r, (io, VArray sz l)) => (Vdeclarr io r sz l) end.
-
-Definition arr_to_Vdeclarr arrdecl := map arr_to_Vdeclarr_fun arrdecl.
-
-Definition transl_module (m : HTL.module) : Verilog.module :=
-  let case_el_ctrl := transl_list (PTree.elements m.(mod_controllogic)) in
-  let case_el_data := transl_list (PTree.elements m.(mod_datapath)) in
-  let body :=
-      Valways (Vposedge m.(mod_clk)) (Vcond (Vbinop Veq (Vvar m.(mod_reset)) (Vlit (ZToValue 1)))
-                                               (Vnonblock (Vvar m.(mod_st)) (Vlit (posToValue m.(mod_entrypoint))))
-                                               (Vcase (Vvar m.(mod_st)) case_el_ctrl (Some Vskip)))
-      :: Valways (Vposedge m.(mod_clk)) (Vcase (Vvar m.(mod_st)) case_el_data (Some Vskip))
-      :: List.map Vdeclaration (arr_to_Vdeclarr (AssocMap.elements m.(mod_arrdecls))
-                          ++ scl_to_Vdecl (AssocMap.elements m.(mod_scldecls))) in
-  Verilog.mkmodule m.(mod_start)
-                   m.(mod_reset)
-                   m.(mod_clk)
-                   m.(mod_finish)
-                   m.(mod_return)
-                   m.(mod_st)
-                   m.(mod_stk)
-                   m.(mod_stk_len)
-                   m.(mod_params)
-                   body
-                   m.(mod_entrypoint).
-
-Definition transl_fundef := transf_fundef transl_module.
-
-Definition transl_program (p: HTL.program) : Verilog.program :=
-  transform_program transl_fundef p.
diff --git a/src/translation/Veriloggenproof.v b/src/translation/Veriloggenproof.v
deleted file mode 100644
index 9abbd4b..0000000
--- a/src/translation/Veriloggenproof.v
+++ /dev/null
@@ -1,368 +0,0 @@
-(*
- * Vericert: 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/>.
- *)
-
-From compcert Require Import Smallstep Linking Integers Globalenvs.
-From vericert Require HTL.
-From vericert Require Import Vericertlib Veriloggen Verilog ValueInt AssocMap.
-Require Import Lia.
-
-Local Open Scope assocmap.
-
-Definition match_prog (prog : HTL.program) (tprog : Verilog.program) :=
-  match_program (fun cu f tf => tf = transl_fundef f) eq prog tprog.
-
-Lemma transf_program_match:
-  forall prog, match_prog prog (transl_program prog).
-Proof.
-  intros. eapply match_transform_program_contextual. auto.
-Qed.
-
-Inductive match_stacks : list HTL.stackframe -> list stackframe -> Prop :=
-| match_stack :
-    forall res m pc reg_assoc arr_assoc hstk vstk,
-      match_stacks hstk vstk ->
-      match_stacks (HTL.Stackframe res m pc reg_assoc arr_assoc :: hstk)
-                   (Stackframe res (transl_module m) pc
-                                       reg_assoc arr_assoc :: vstk)
-| match_stack_nil : match_stacks nil nil.
-
-Inductive match_states : HTL.state -> state -> Prop :=
-| match_state :
-    forall m st reg_assoc arr_assoc hstk vstk,
-      match_stacks hstk vstk ->
-      match_states (HTL.State hstk m st reg_assoc arr_assoc)
-                   (State vstk (transl_module m) st reg_assoc arr_assoc)
-| match_returnstate :
-    forall v hstk vstk,
-      match_stacks hstk vstk ->
-      match_states (HTL.Returnstate hstk v) (Returnstate vstk v)
-| match_initial_call :
-    forall m,
-      match_states (HTL.Callstate nil m nil) (Callstate nil (transl_module m) nil).
-
-Lemma Vlit_inj :
-  forall a b, Vlit a = Vlit b -> a = b.
-Proof. inversion 1. trivial. Qed.
-
-Lemma posToValue_inj :
-  forall a b,
-    0 <= Z.pos a <= Int.max_unsigned ->
-    0 <= Z.pos b <= Int.max_unsigned ->
-    posToValue a = posToValue b ->
-    a = b.
-Proof.
-  intros. rewrite <- Pos2Z.id at 1. rewrite <- Pos2Z.id.
-  rewrite <- Int.unsigned_repr at 1; try assumption.
-  symmetry.
-  rewrite <- Int.unsigned_repr at 1; try assumption.
-  unfold posToValue in *. rewrite H1; auto.
-Qed.
-
-Lemma valueToPos_inj :
-  forall a b,
-    0 < Int.unsigned a ->
-    0 < Int.unsigned b ->
-    valueToPos a = valueToPos b ->
-    a = b.
-Proof.
-  intros. unfold valueToPos in *.
-  rewrite <- Int.repr_unsigned at 1.
-  rewrite <- Int.repr_unsigned.
-  apply Pos2Z.inj_iff in H1.
-  rewrite Z2Pos.id in H1; auto.
-  rewrite Z2Pos.id in H1; auto.
-  rewrite H1. auto.
-Qed.
-
-Lemma unsigned_posToValue_le :
-  forall p,
-    Z.pos p <= Int.max_unsigned ->
-    0 < Int.unsigned (posToValue p).
-Proof.
-  intros. unfold posToValue. rewrite Int.unsigned_repr; lia.
-Qed.
-
-Lemma transl_list_fun_fst :
-  forall p1 p2 a b,
-    0 <= Z.pos p1 <= Int.max_unsigned ->
-    0 <= Z.pos p2 <= Int.max_unsigned ->
-    transl_list_fun (p1, a) = transl_list_fun (p2, b) ->
-    (p1, a) = (p2, b).
-Proof.
-  intros. unfold transl_list_fun in H1. apply pair_equal_spec in H1.
-  destruct H1. rewrite H2. apply Vlit_inj in H1.
-  apply posToValue_inj in H1; try assumption.
-  rewrite H1; auto.
-Qed.
-
-Lemma Zle_relax :
-  forall p q r,
-  p < q <= r ->
-  p <= q <= r.
-Proof. lia. Qed.
-Hint Resolve Zle_relax : verilogproof.
-
-Lemma transl_in :
-  forall l p,
-  0 <= Z.pos p <= Int.max_unsigned ->
-  (forall p0, In p0 (List.map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) ->
-  In (Vlit (posToValue p)) (map fst (map transl_list_fun l)) ->
-  In p (map fst l).
-Proof.
-  induction l.
-  - simplify. auto.
-  - intros. destruct a. simplify. destruct (peq p0 p); auto.
-    right. inv H1. apply Vlit_inj in H. apply posToValue_inj in H; auto. contradiction.
-    auto with verilogproof.
-    apply IHl; auto.
-Qed.
-
-Lemma transl_notin :
-  forall l p,
-    0 <= Z.pos p <= Int.max_unsigned ->
-    (forall p0, In p0 (List.map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) ->
-    ~ In p (List.map fst l) -> ~ In (Vlit (posToValue p)) (List.map fst (transl_list l)).
-Proof.
-  induction l; auto. intros. destruct a. unfold not in *. intros.
-  simplify.
-  destruct (peq p0 p). apply H1. auto. apply H1.
-  unfold transl_list in *. inv H2. apply Vlit_inj in H. apply posToValue_inj in H.
-  contradiction.
-  auto with verilogproof. auto.
-  right. apply transl_in; auto.
-Qed.
-
-Lemma transl_norepet :
-  forall l,
-    (forall p0, In p0 (List.map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) ->
-    list_norepet (List.map fst l) -> list_norepet (List.map fst (transl_list l)).
-Proof.
-  induction l.
-  - intros. simpl. apply list_norepet_nil.
-  - destruct a. intros. simpl. apply list_norepet_cons.
-    inv H0. apply transl_notin. apply Zle_relax. apply H. simplify; auto.
-    intros. apply H. destruct (peq p0 p); subst; simplify; auto.
-    assumption. apply IHl. intros. apply H. destruct (peq p0 p); subst; simplify; auto.
-    simplify. inv H0. assumption.
-Qed.
-
-Lemma transl_list_correct :
-  forall l v ev f asr asa asrn asan asr' asa' asrn' asan',
-    (forall p0, In p0 (List.map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) ->
-    list_norepet (List.map fst l) ->
-    asr!ev = Some v ->
-    (forall p s,
-        In (p, s) l ->
-        v = posToValue p ->
-        stmnt_runp f
-                   {| assoc_blocking := asr; assoc_nonblocking := asrn |}
-                   {| assoc_blocking := asa; assoc_nonblocking := asan |}
-                   s
-                   {| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
-                   {| assoc_blocking := asa'; assoc_nonblocking := asan' |} ->
-        stmnt_runp f
-                   {| assoc_blocking := asr; assoc_nonblocking := asrn |}
-                   {| assoc_blocking := asa; assoc_nonblocking := asan |}
-                   (Vcase (Vvar ev) (transl_list l) (Some Vskip))
-                   {| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
-                   {| assoc_blocking := asa'; assoc_nonblocking := asan' |}).
-Proof.
-  induction l as [| a l IHl].
-  - contradiction.
-  - intros v ev f asr asa asrn asan asr' asa' asrn' asan' BOUND NOREP ASSOC p s IN EQ SRUN.
-    destruct a as [p' s']. simplify.
-    destruct (peq p p'); subst. eapply stmnt_runp_Vcase_match.
-    constructor. simplify. unfold AssocMap.find_assocmap, AssocMapExt.get_default.
-    rewrite ASSOC. trivial. constructor. auto.
-    inversion IN as [INV | INV]. inversion INV as [INV2]; subst. assumption.
-    inv NOREP. eapply in_map with (f := fst) in INV. contradiction.
-
-    eapply stmnt_runp_Vcase_nomatch. constructor. simplify.
-    unfold AssocMap.find_assocmap, AssocMapExt.get_default. rewrite ASSOC.
-    trivial. constructor. unfold not. intros. apply n. apply posToValue_inj.
-    apply Zle_relax. apply BOUND. right. inv IN. inv H0; contradiction.
-    eapply in_map with (f := fst) in H0. auto.
-    apply Zle_relax. apply BOUND; auto. auto.
-
-    eapply IHl. auto. inv NOREP. auto. eassumption. inv IN. inv H. contradiction. apply H.
-    trivial. assumption.
-Qed.
-Hint Resolve transl_list_correct : verilogproof.
-
-Lemma pc_wf :
-  forall A m p v,
-  (forall p0, In p0 (List.map fst (@AssocMap.elements A m)) -> 0 < Z.pos p0 <= Int.max_unsigned) ->
-  m!p = Some v ->
-  0 <= Z.pos p <= Int.max_unsigned.
-Proof.
-  intros A m p v LT S. apply Zle_relax. apply LT.
-  apply AssocMap.elements_correct in S. remember (p, v) as x.
-  exploit in_map. apply S. instantiate (1 := fst). subst. simplify. auto.
-Qed.
-
-Lemma mis_stepp_decl :
-  forall l asr asa f,
-    mis_stepp f asr asa (map Vdeclaration l) asr asa.
-Proof.
-  induction l.
-  - intros. constructor.
-  - intros. simplify. econstructor. constructor. auto.
-Qed.
-Hint Resolve mis_stepp_decl : verilogproof.
-
-Section CORRECTNESS.
-
-  Variable prog: HTL.program.
-  Variable tprog: program.
-
-  Hypothesis TRANSL : match_prog prog tprog.
-
-  Let ge : HTL.genv := Globalenvs.Genv.globalenv prog.
-  Let tge : genv := Globalenvs.Genv.globalenv tprog.
-
-  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.
-  Hint Resolve symbols_preserved : verilogproof.
-
-  Lemma function_ptr_translated:
-    forall (b: Values.block) (f: HTL.fundef),
-      Genv.find_funct_ptr ge b = Some f ->
-      exists tf,
-        Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = tf.
-  Proof.
-    intros. exploit (Genv.find_funct_ptr_match TRANSL); eauto.
-    intros (cu & tf & P & Q & R); exists tf; auto.
-  Qed.
-  Hint Resolve function_ptr_translated : verilogproof.
-
-  Lemma functions_translated:
-    forall (v: Values.val) (f: HTL.fundef),
-      Genv.find_funct ge v = Some f ->
-      exists tf,
-        Genv.find_funct tge v = Some tf /\ transl_fundef f = tf.
-  Proof.
-    intros. exploit (Genv.find_funct_match TRANSL); eauto.
-    intros (cu & tf & P & Q & R); exists tf; auto.
-  Qed.
-  Hint Resolve functions_translated : verilogproof.
-
-  Lemma senv_preserved:
-    Senv.equiv (Genv.to_senv ge) (Genv.to_senv tge).
-  Proof.
-    intros. eapply (Genv.senv_match TRANSL).
-  Qed.
-  Hint Resolve senv_preserved : verilogproof.
-
-  Theorem transl_step_correct :
-    forall (S1 : HTL.state) t S2,
-      HTL.step ge S1 t S2 ->
-      forall (R1 : state),
-        match_states S1 R1 ->
-        exists R2, Smallstep.plus step tge R1 t R2 /\ match_states S2 R2.
-  Proof.
-    induction 1; intros R1 MSTATE; inv MSTATE.
-    - econstructor; split. apply Smallstep.plus_one. econstructor.
-      assumption. assumption. eassumption. apply valueToPos_posToValue.
-      split. lia.
-      eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _].
-      split. lia. apply HP. eassumption. eassumption.
-      econstructor. econstructor. eapply stmnt_runp_Vcond_false. econstructor. econstructor.
-      simpl. unfold find_assocmap. unfold AssocMapExt.get_default.
-      rewrite H. trivial.
-
-      econstructor. simpl. auto. auto.
-
-      eapply transl_list_correct.
-      intros. split. lia. pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _]. auto.
-      apply Maps.PTree.elements_keys_norepet. eassumption.
-      2: { apply valueToPos_inj. apply unsigned_posToValue_le.
-           eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _].
-           split. lia. apply HP. eassumption. eassumption.
-           apply unsigned_posToValue_le. eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP.
-           destruct HP as [HP _].
-           split. lia. apply HP. eassumption. eassumption. trivial.
-      }
-      apply Maps.PTree.elements_correct. eassumption. eassumption.
-
-      econstructor. econstructor.
-
-      eapply transl_list_correct.
-      intros. split. lia. pose proof (HTL.mod_wf m) as HP. destruct HP as [_ HP]. auto.
-      apply Maps.PTree.elements_keys_norepet. eassumption.
-      2: { apply valueToPos_inj. apply unsigned_posToValue_le.
-           eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _].
-           split. lia. apply HP. eassumption. eassumption.
-           apply unsigned_posToValue_le. eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP.
-           destruct HP as [HP _].
-           split. lia. apply HP. eassumption. eassumption. trivial.
-      }
-      apply Maps.PTree.elements_correct. eassumption. eassumption.
-
-      apply mis_stepp_decl. trivial. trivial. simpl. eassumption. auto.
-      rewrite valueToPos_posToValue. constructor; assumption. lia.
-
-    - econstructor; split. apply Smallstep.plus_one. apply step_finish. assumption. eassumption.
-      constructor; assumption.
-    - econstructor; split. apply Smallstep.plus_one. constructor.
-
-      constructor. constructor.
-    - inv H3. econstructor; split. apply Smallstep.plus_one. constructor. trivial.
-
-      apply match_state. assumption.
-  Qed.
-  Hint Resolve transl_step_correct : verilogproof.
-
-  Lemma transl_initial_states :
-    forall s1 : Smallstep.state (HTL.semantics prog),
-      Smallstep.initial_state (HTL.semantics prog) s1 ->
-      exists s2 : Smallstep.state (Verilog.semantics tprog),
-        Smallstep.initial_state (Verilog.semantics tprog) s2 /\ match_states s1 s2.
-  Proof.
-    induction 1.
-    econstructor; split. econstructor.
-    apply (Genv.init_mem_transf TRANSL); eauto.
-    rewrite symbols_preserved.
-    replace (AST.prog_main tprog) with (AST.prog_main prog); eauto.
-    symmetry; eapply Linking.match_program_main; eauto.
-    exploit function_ptr_translated; eauto. intros [tf [A B]].
-    inv B. eauto.
-    constructor.
-  Qed.
-  Hint Resolve transl_initial_states : verilogproof.
-
-  Lemma transl_final_states :
-    forall (s1 : Smallstep.state (HTL.semantics prog))
-           (s2 : Smallstep.state (Verilog.semantics tprog))
-           (r : Integers.Int.int),
-      match_states s1 s2 ->
-      Smallstep.final_state (HTL.semantics prog) s1 r ->
-      Smallstep.final_state (Verilog.semantics tprog) s2 r.
-  Proof.
-    intros. inv H0. inv H. inv H3. constructor. reflexivity.
-  Qed.
-  Hint Resolve transl_final_states : verilogproof.
-
-  Theorem transf_program_correct:
-    forward_simulation (HTL.semantics prog) (Verilog.semantics tprog).
-  Proof.
-    eapply Smallstep.forward_simulation_plus; eauto with verilogproof.
-    apply senv_preserved.
-  Qed.
-
-End CORRECTNESS.