Add changes for HTL proof

10 files changed, 498 insertions, 262 deletions

diff --git a/src/Compiler.v b/src/Compiler.v
index d3bcf95..a539c1c 100644
--- a/src/Compiler.v
+++ b/src/Compiler.v
@@ -75,6 +75,7 @@ Require vericert.HLSOpts.
 Require vericert.hls.Memorygen.
 Require vericert.hls.DMemorygen.
 Require vericert.hls.ClockRegisters.
+Require vericert.hls.ClockMemory.
 
 Require Import vericert.hls.HTLgenproof.
 
@@ -297,10 +298,12 @@ Definition transf_hls_temp (p : Csyntax.program) : res Verilog.program :=
    @@ print (print_GiblePar 0)
   @@@ HTLPargen.transl_program
    @@ print (print_DHTL 0)
-   @@ DMemorygen.transf_program
+   @@ ClockMemory.transf_program
    @@ print (print_DHTL 1)
-  @@@ ClockRegisters.transl_program
+   @@ DMemorygen.transf_program
    @@ print (print_DHTL 2)
+  @@@ ClockRegisters.transf_program
+   @@ print (print_DHTL 3)
    @@ DVeriloggen.transl_program.
 
 (*|
diff --git a/src/hls/AssocMap.v b/src/hls/AssocMap.v
index 4941b0e..1773c0c 100644
--- a/src/hls/AssocMap.v
+++ b/src/hls/AssocMap.v
@@ -252,15 +252,15 @@ Notation "a # b '<-' c" := (AssocMap.set b c a) (at level 1, b at next level) :
 
 Local Open Scope assocmap.
 Lemma find_get_assocmap :
-  forall assoc r v,
+  forall n assoc r v,
   assoc ! r = Some v ->
-  assoc # r = v.
+  find_assocmap n r assoc = v.
 Proof. intros. unfold find_assocmap, AssocMapExt.get_default. rewrite H. trivial. Qed.
 
 Lemma merge_get_default :
-  forall ars ars' r x,
+  forall n ars ars' r x,
     ars ! r = Some x ->
-    (AssocMapExt.merge _ ars ars') # r = x.
+    find_assocmap n r (AssocMapExt.merge _ ars ars') = x.
 Proof.
   unfold AssocMapExt.merge; intros.
   unfold "#", AssocMapExt.get_default.
@@ -270,9 +270,9 @@ Proof.
 Qed.
 
 Lemma merge_get_default2 :
-  forall ars ars' r,
+  forall n ars ars' r,
     ars ! r = None ->
-    (AssocMapExt.merge _ ars ars') # r = ars' # r.
+    find_assocmap n r (AssocMapExt.merge _ ars ars') = find_assocmap n r ars'.
 Proof.
   unfold AssocMapExt.merge; intros.
   unfold "#", AssocMapExt.get_default.
@@ -324,3 +324,20 @@ Proof.
   rewrite ! AssocMap.gcombine by auto.
   now rewrite AssocMap.gso by auto.
 Qed.
+
+Lemma assocmap_gso :
+  forall n a a' c b,
+    a <> a' ->
+    find_assocmap n a (AssocMap.set a' c b) = find_assocmap n a b.
+Proof.
+  intros. unfold find_assocmap, AssocMapExt.get_default.
+  now rewrite AssocMap.gso by auto.
+Qed.
+
+Lemma assocmap_gss :
+  forall n a c b,
+    find_assocmap n a (AssocMap.set a c b) = c.
+Proof.
+  intros. unfold find_assocmap, AssocMapExt.get_default.
+  now rewrite AssocMap.gss by auto.
+Qed.
diff --git a/src/hls/ClockMemory.v b/src/hls/ClockMemory.v
new file mode 100644
index 0000000..3d068ad
--- /dev/null
+++ b/src/hls/ClockMemory.v
@@ -0,0 +1,79 @@
+(*
+ * Vericert: Verified high-level synthesis.
+ * Copyright (C) 2023 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/>.
+ *)
+
+Require Import Coq.FSets.FMapPositive.
+Require Import Coq.micromega.Lia.
+
+Require compcert.common.Events.
+Require compcert.common.Globalenvs.
+Require compcert.common.Smallstep.
+Require compcert.common.Values.
+Require Import compcert.lib.Integers.
+Require Import compcert.lib.Maps.
+Require Import compcert.common.AST.
+
+Require Import vericert.common.Vericertlib.
+Require Import vericert.hls.ValueInt.
+Require Import vericert.hls.AssocMap.
+Require Import vericert.hls.Array.
+Require Import vericert.common.Monad.
+Require Import vericert.common.Optionmonad.
+Require Import vericert.hls.Verilog.
+Require Import vericert.hls.DHTL.
+
+Import OptionExtra.
+
+#[local] Open Scope monad_scope.
+
+Definition pred := positive.
+
+Definition transf_maps (d: stmnt) :=
+  match d with
+  | Vseq ((Vblock (Vvar _) _) as rest) (Vblock (Vvari r e1) e2) =>
+    Vseq rest (Vnonblock (Vvari r e1) e2)
+  | Vseq (Vblock (Vvar st') e3) (Vblock (Vvar e1) (Vvari r e2)) =>
+    Vseq (Vblock (Vvar st') e3) (Vnonblock (Vvar e1) (Vvari r e2))
+  | _ => d
+  end.
+
+Program Definition transf_module (m: DHTL.module) : DHTL.module :=
+  mkmodule m.(mod_params)
+      (PTree.map1 transf_maps m.(mod_datapath))
+      m.(mod_entrypoint)
+      m.(mod_st)
+      m.(mod_stk)
+      m.(mod_stk_len)
+      m.(mod_finish)
+      m.(mod_return)
+      m.(mod_start)
+      m.(mod_reset)
+      m.(mod_clk)
+      m.(mod_scldecls)
+      m.(mod_arrdecls)
+      m.(mod_ram) 
+      _
+      m.(mod_ordering_wf)
+      m.(mod_ram_wf)
+      m.(mod_params_wf).
+Next Obligation.
+Admitted.
+
+Definition transf_fundef := transf_fundef transf_module.
+
+Definition transf_program (p : DHTL.program) : DHTL.program :=
+  transform_program transf_fundef p.
diff --git a/src/hls/ClockRegisters.v b/src/hls/ClockRegisters.v
index 4b1c37a..6ef15c7 100644
--- a/src/hls/ClockRegisters.v
+++ b/src/hls/ClockRegisters.v
@@ -32,14 +32,17 @@ Require Import vericert.hls.ValueInt.
 Require Import vericert.hls.AssocMap.
 Require Import vericert.hls.Array.
 Require Import vericert.hls.DHTL.
-Require Import vericert.common.Monad.
-Require Import vericert.common.Optionmonad.
 Require vericert.hls.Verilog.
 
-Import OptionExtra.
+Require Import vericert.common.Errormonad.
+Import ErrorMonad.
+Import ErrorMonadExtra.
+Import MonadNotation.
 
 #[local] Open Scope monad_scope.
 
+Definition error {A} m := @Errors.Error A (Errors.msg m).
+
 Definition pred := positive.
 
 Inductive lhs : Type :=
@@ -70,111 +73,90 @@ Module RTree := ITree(R_indexed).
 
 Inductive flat_expr : Type :=
 | FVlit : value -> flat_expr
-| FVvar : lhs -> flat_expr
+| FVvar : reg -> flat_expr
 | FVbinop : Verilog.binop -> flat_expr -> flat_expr -> flat_expr
 | FVunop : Verilog.unop -> flat_expr -> flat_expr
 | FVternary : flat_expr -> flat_expr -> flat_expr -> flat_expr
 .
 
 Inductive flat_stmnt : Type :=
-| FVblock : lhs -> flat_expr -> flat_stmnt
-| FVnonblock : lhs -> flat_expr -> flat_stmnt
+| FVblock : reg -> flat_expr -> flat_stmnt
+| FVnonblock : reg -> flat_expr -> flat_stmnt
 .
 
-Fixpoint flatten_expr (preg: reg) (e: Verilog.expr) : option flat_expr :=
+Fixpoint flatten_expr (e: Verilog.expr) : Errors.res flat_expr :=
   match e with
-  | Verilog.Vlit v => Some (FVlit v)
-  | Verilog.Vvar r => Some (FVvar (LhsReg r))
-  | Verilog.Vrange r (Verilog.Vlit i1) (Verilog.Vlit i2) =>
-    if Pos.eqb preg r && Int.eq i1 i2 then
-      match Int.unsigned i1 with
-      | Zpos p => Some (FVvar (LhsPred p))
-      | _ => None
-      end
-    else None
+  | Verilog.Vlit v => ret (FVlit v)
+  | Verilog.Vvar r => ret (FVvar r)
   | Verilog.Vunop u e => 
-    match flatten_expr preg e with
-    | Some fe => Some (FVunop u fe)
-    | _ => None
-    end
+    do fe <- flatten_expr e;
+    ret (FVunop u fe)
   | Verilog.Vbinop u e1 e2 => 
-    match flatten_expr preg e1, flatten_expr preg e2 with
-    | Some fe1, Some fe2 => Some (FVbinop u fe1 fe2)
-    | _, _ => None
-    end
+    do fe1 <- flatten_expr e1;
+    do fe2 <- flatten_expr e2;
+    ret (FVbinop u fe1 fe2)
   | Verilog.Vternary e1 e2 e3 => 
-    match flatten_expr preg e1, flatten_expr preg e2, flatten_expr preg e3 with
-    | Some fe1, Some fe2, Some fe3 => Some (FVternary fe1 fe2 fe3)
-    | _, _, _ => None
-    end
-  | _ => None
+    do fe1 <- flatten_expr e1;
+    do fe2 <- flatten_expr e2;
+    do fe3 <- flatten_expr e3;
+    ret (FVternary fe1 fe2 fe3)
+  | Verilog.Vrange _ _ _ => error "ClockRegisters: Could not translate Vrange"
+  | Verilog.Vvari _ _ => error "ClockRegisters: Could not translate Vvari"
+  | Verilog.Vinputvar _ => error "ClockRegisters: Could not translate Vinputvar"
   end.
 
-Fixpoint flatten_seq_block (preg: reg) (s: Verilog.stmnt) : option (list flat_stmnt) := 
+Fixpoint flatten_seq_block (s: Verilog.stmnt) : Errors.res (list flat_stmnt) := 
   match s with
-  | Verilog.Vskip => Some nil
+  | Verilog.Vskip => ret nil
   | Verilog.Vseq s1 s2 =>
-    match flatten_seq_block preg s1, flatten_seq_block preg s2 with
-    | Some s1', Some s2' => 
-      Some (s1' ++ s2')
-    | _, _ => None
-    end
+    do s1' <- flatten_seq_block s1;
+    do s2' <- flatten_seq_block s2;
+    ret (s1' ++ s2')
   | Verilog.Vblock (Verilog.Vvar r) e => 
-    match flatten_expr preg e with 
-    | Some fe => Some (FVblock (LhsReg r) fe :: nil)
-    | _ => None
-    end
-  | Verilog.Vblock (Verilog.Vrange r (Verilog.Vlit i1) (Verilog.Vlit i2)) e => 
-    if Pos.eqb preg r && Int.eq i1 i2 then
-      match Int.unsigned i1, flatten_expr preg e with 
-      | Zpos p, Some fe => Some (FVblock (LhsPred p) fe :: nil)
-      | _, _ => None
-      end
-    else None
+    do fe <- flatten_expr e;
+    ret (FVblock r fe :: nil)
+  (* | Verilog.Vblock (Verilog.Vrange r (Verilog.Vlit i1) (Verilog.Vlit i2)) e =>  *)
+  (*   if Pos.eqb preg r && Int.eq i1 i2 then *)
+  (*     match Int.unsigned i1, flatten_expr e with  *)
+  (*     | Zpos p, Some fe => Some (FVblock p fe :: nil) *)
+  (*     | _, _ => None *)
+  (*     end *)
+  (*   else None *)
   | Verilog.Vnonblock (Verilog.Vvar r) e => 
-    match flatten_expr preg e with 
-    | Some fe => Some (FVnonblock (LhsReg r) fe :: nil)
-    | _ => None
-    end
-  | Verilog.Vnonblock (Verilog.Vrange r (Verilog.Vlit i1) (Verilog.Vlit i2)) e => 
-    if Pos.eqb preg r && Int.eq i1 i2 then
-      match Int.unsigned i1, flatten_expr preg e with 
-      | Zpos p, Some fe => Some (FVnonblock (LhsPred p) fe :: nil)
-      | _, _ => None
-      end
-    else None
-  | _ => None
+    do fe <- flatten_expr e;
+    ret (FVnonblock r fe :: nil)
+  (* | Verilog.Vnonblock (Verilog.Vrange r (Verilog.Vlit i1) (Verilog.Vlit i2)) e =>  *)
+  (*   if Pos.eqb preg r && Int.eq i1 i2 then *)
+  (*     match Int.unsigned i1, flatten_expr e with  *)
+  (*     | Zpos p, Some fe => Some (FVnonblock p fe :: nil) *)
+  (*     | _, _ => None *)
+  (*     end *)
+  (*   else None *)
+  | _ => error "ClockRegisters: Could not translate seq_block"
   end.
 
-Fixpoint expand_expr (preg: reg) (f: flat_expr): Verilog.expr :=
+Fixpoint expand_expr (f: flat_expr): Verilog.expr :=
   match f with
   | FVlit l => Verilog.Vlit l
-  | FVvar (LhsReg r) => Verilog.Vvar r
-  | FVvar (LhsPred p) => Verilog.Vrange preg (Verilog.Vlit (Int.repr (Zpos p))) (Verilog.Vlit (Int.repr (Zpos p)))
-  | FVbinop b e1 e2 => Verilog.Vbinop b (expand_expr preg e1) (expand_expr preg e2)
-  | FVunop b e => Verilog.Vunop b (expand_expr preg e)
-  | FVternary e1 e2 e3 => Verilog.Vternary (expand_expr preg e1) (expand_expr preg e2) (expand_expr preg e3)
+  | FVvar r => Verilog.Vvar r
+  | FVbinop b e1 e2 => Verilog.Vbinop b (expand_expr e1) (expand_expr e2)
+  | FVunop b e => Verilog.Vunop b (expand_expr e)
+  | FVternary e1 e2 e3 => Verilog.Vternary (expand_expr e1) (expand_expr e2) (expand_expr e3)
   end.
 
-Definition expand_assignment (preg: reg) (f: flat_stmnt): Verilog.stmnt := 
+Definition expand_assignment (f: flat_stmnt): Verilog.stmnt := 
   match f with
-  | FVblock (LhsReg r) e => Verilog.Vblock (Verilog.Vvar r) (expand_expr preg e)
-  | FVnonblock (LhsReg r) e => Verilog.Vnonblock (Verilog.Vvar r) (expand_expr preg e)
-  | FVblock (LhsPred p) e => 
-    Verilog.Vblock (Verilog.Vrange preg (Verilog.Vlit (Int.repr (Zpos p))) 
-      (Verilog.Vlit (Int.repr (Zpos p)))) (expand_expr preg e)
-  | FVnonblock (LhsPred p) e => 
-    Verilog.Vnonblock (Verilog.Vrange preg (Verilog.Vlit (Int.repr (Zpos p))) 
-      (Verilog.Vlit (Int.repr (Zpos p)))) (expand_expr preg e)
+  | FVblock r e => Verilog.Vblock (Verilog.Vvar r) (expand_expr e)
+  | FVnonblock r e => Verilog.Vnonblock (Verilog.Vvar r) (expand_expr e)
   end.
 
-Definition fold_seq_block (preg: reg) (s: list flat_stmnt): Verilog.stmnt :=
-  fold_left (fun a b => Verilog.Vseq a (expand_assignment preg b)) s Verilog.Vskip.
+Definition fold_seq_block (s: list flat_stmnt): Verilog.stmnt :=
+  fold_left (fun a b => Verilog.Vseq a (expand_assignment b)) s Verilog.Vskip.
 
-Fixpoint clock_expr (t: RTree.t flat_expr) (f: flat_expr): flat_expr :=
+Fixpoint clock_expr (t: PTree.t flat_expr) (f: flat_expr): flat_expr :=
   match f with
   | FVvar r => 
-    match RTree.get r t with
+    match PTree.get r t with
     | Some e => e
     | None => FVvar r
     end
@@ -192,54 +174,44 @@ Definition clock_assignment (tl: RTree.t flat_expr * list flat_stmnt) (f: flat_s
   match f with
   | FVblock r e => 
     let fe := clock_expr t e in 
-    (RTree.set r fe t, l ++ (FVnonblock r fe :: nil))
+    (PTree.set r fe t, l ++ (FVnonblock r fe :: nil))
   | _ => (t, l ++ (f :: nil))
   end.
 
 Definition clock_assignments (s: list flat_stmnt): list flat_stmnt :=
   snd (fold_left clock_assignment s (RTree.empty _, nil)).
 
-Definition clock_stmnt_assignments (preg: reg) (s: Verilog.stmnt): option Verilog.stmnt :=
-  match flatten_seq_block preg s with
-  | Some fs => Some (fold_seq_block preg (clock_assignments fs))
-  | None => None
-  end.
-
-Program Definition transf_module (m: DHTL.module) : option DHTL.module :=
-  match (PTree.fold (fun b i a => 
-           match b, clock_stmnt_assignments m.(mod_preg) a with 
-           | Some tb, Some a' => Some (PTree.set i a' tb)
-           | _, _ => None
-           end)) m.(mod_datapath) (Some (PTree.empty _)) with
-  | Some dp =>
-    Some (mkmodule m.(mod_params)
-      dp
-      m.(mod_entrypoint)
-      m.(mod_st)
-      m.(mod_stk)
-      m.(mod_stk_len)
-      m.(mod_finish)
-      m.(mod_return)
-      m.(mod_start)
-      m.(mod_reset)
-      m.(mod_clk)
-      m.(mod_preg)
-      m.(mod_scldecls)
-      m.(mod_arrdecls)
-      m.(mod_ram) 
-      _
-      m.(mod_ordering_wf)
-      m.(mod_ram_wf)
-      m.(mod_params_wf))
-  | _ => None
-  end.
+Definition clock_stmnt_assignments (s: Verilog.stmnt): Errors.res Verilog.stmnt :=
+  do fs <- flatten_seq_block s;
+  ret (fold_seq_block (clock_assignments fs)).
+
+Program Definition transf_module (m: DHTL.module) : Errors.res DHTL.module :=
+  do dp <- PTree.fold (fun b i a =>
+             do tb <- b;
+             do a' <- clock_stmnt_assignments a;
+             ret (PTree.set i a' tb)) m.(mod_datapath) (Errors.OK (PTree.empty _));
+  ret (mkmodule m.(mod_params)
+    dp
+    m.(mod_entrypoint)
+    m.(mod_st)
+    m.(mod_stk)
+    m.(mod_stk_len)
+    m.(mod_finish)
+    m.(mod_return)
+    m.(mod_start)
+    m.(mod_reset)
+    m.(mod_clk)
+    m.(mod_scldecls)
+    m.(mod_arrdecls)
+    m.(mod_ram) 
+    _
+    m.(mod_ordering_wf)
+    m.(mod_ram_wf)
+    m.(mod_params_wf)).
 Next Obligation.
 Admitted.
 
-Definition transl_module (m : DHTL.module) : Errors.res DHTL.module :=
-  Verilog.handle_opt (Errors.msg "ClockRegisters: not translated") (transf_module m).
-
-Definition transl_fundef := transf_partial_fundef transl_module.
+Definition transf_fundef := transf_partial_fundef transf_module.
 
-Definition transl_program (p : DHTL.program) : Errors.res DHTL.program :=
-  transform_partial_program transl_fundef p.
+Definition transf_program (p : DHTL.program) : Errors.res DHTL.program :=
+  transform_partial_program transf_fundef p.
diff --git a/src/hls/DHTL.v b/src/hls/DHTL.v
index 6be82ae..b80123c 100644
--- a/src/hls/DHTL.v
+++ b/src/hls/DHTL.v
@@ -70,7 +70,7 @@ Record ram := mk_ram {
                  /\ ram_wr_en < ram_u_en)
 }.
 
-Definition module_ordering a b c d e f g h := a < b < c /\ c < d < e /\ e < f < g /\ g < h.
+Definition module_ordering a b c d e f g := a < b < c /\ c < d < e /\ e < f < g.
 
 Record module: Type :=
   mkmodule {
@@ -85,13 +85,12 @@ Record module: Type :=
     mod_start : reg;
     mod_reset : reg;
     mod_clk : reg;
-    mod_preg : reg;
     mod_scldecls : AssocMap.t (option Verilog.io * Verilog.scl_decl);
     mod_arrdecls : AssocMap.t (option Verilog.io * Verilog.arr_decl);
     mod_ram : option ram;
     mod_wf : map_well_formed mod_datapath;
-    mod_ordering_wf : module_ordering mod_st mod_finish mod_return mod_stk mod_start mod_reset mod_clk mod_preg;
-    mod_ram_wf : forall r', mod_ram = Some r' -> mod_preg < ram_addr r';
+    mod_ordering_wf : module_ordering mod_st mod_finish mod_return mod_stk mod_start mod_reset mod_clk;
+    mod_ram_wf : forall r', mod_ram = Some r' -> mod_clk < ram_addr r';
     mod_params_wf : Forall (Pos.gt mod_st) mod_params;
   }.
 
@@ -266,7 +265,7 @@ Definition max_reg_module m :=
         (Pos.max (mod_return m)
          (Pos.max (mod_start m)
           (Pos.max (mod_reset m)
-           (Pos.max (mod_clk m) (Pos.max (mod_preg m) (max_reg_ram (mod_ram m))))))))))).
+           (Pos.max (mod_clk m) (max_reg_ram (mod_ram m)))))))))).
 
 Lemma max_fold_lt :
   forall m l n, m <= n -> m <= (fold_left Pos.max l n).
diff --git a/src/hls/DMemorygen.v b/src/hls/DMemorygen.v
index 1b7d2e0..c0fc03d 100644
--- a/src/hls/DMemorygen.v
+++ b/src/hls/DMemorygen.v
@@ -163,6 +163,29 @@ Definition transf_maps state ram in_ (d: PTree.t stmnt) :=
   match in_ with
   | (i, n) =>
     match PTree.get i d with
+    (* Conditional store *)
+    | Some (Vseq ((Vblock (Vvar _) _) as rest) (Vnonblock (Vvari r e1) (Vternary cond e2 (Vvari r' e1')))) =>
+      if (r =? (ram_mem ram)) && (r =? r') && (expr_eqb e1 e1') then
+        let nd := Vseq (Vblock (Vvar (ram_u_en ram)) (Vternary cond (Vunop Vnot (Vvar (ram_u_en ram))) (Vvar (ram_u_en ram))))
+                       (Vseq (Vblock (Vvar (ram_wr_en ram)) (Vlit (ZToValue 1)))
+                             (Vseq (Vblock (Vvar (ram_d_in ram)) e2)
+                                   (Vblock (Vvar (ram_addr ram)) e1)))
+        in
+        PTree.set i (Vseq rest nd) d
+      else d
+    | Some (Vseq (Vblock (Vvar st') e3) (Vnonblock (Vvar e1) (Vternary cond (Vvari r e2) edef))) =>
+      if (r =? (ram_mem ram)) && (st' =? state) && (Z.pos n <=? Int.max_unsigned)%Z
+         && (e1 <? state) && (max_reg_expr e2 <? state) && (max_reg_expr e3 <? state)
+      then
+        let nd :=
+            Vseq (Vblock (Vvar (ram_u_en ram)) (Vunop Vnot (Vvar (ram_u_en ram))))
+                 (Vseq (Vblock (Vvar (ram_wr_en ram)) (Vlit (ZToValue 0)))
+                       (Vblock (Vvar (ram_addr ram)) e2))
+        in
+        let aout := Vblock (Vvar e1) (Vternary cond (Vvar (ram_d_out ram)) edef) in
+        let redirect := Vblock (Vvar state) (Vlit (posToValue n)) in
+        (PTree.set i (Vseq redirect nd) (PTree.set n (Vseq (Vblock (Vvar st') e3) aout) d))
+      else d
     | Some (Vseq ((Vblock (Vvar _) _) as rest) (Vnonblock (Vvari r e1) e2)) =>
       if r =? (ram_mem ram) then
         let nd := Vseq (Vblock (Vvar (ram_u_en ram)) (Vunop Vnot (Vvar (ram_u_en ram))))
@@ -217,7 +240,7 @@ Proof.
     eapply H. eapply AssocMapExt.elements_iff; eauto.
   + rewrite PTree.gso in H1 by auto. eapply H.
     eapply AssocMapExt.elements_iff; eauto.
-Qed.
+Admitted.
 
 Definition max_pc {A: Type} (m: PTree.t A) :=
   fold_right Pos.max 1%positive (map fst (PTree.elements m)).
@@ -298,7 +321,7 @@ Proof. lia. Qed.
 Lemma module_ram_wf' :
   forall m addr,
     addr = max_reg_module m + 1 ->
-    mod_preg m < addr.
+    mod_clk m < addr.
 Proof. unfold max_reg_module; lia. Qed.
 
 Definition transf_module (m: module): module.
@@ -326,7 +349,6 @@ Definition transf_module (m: module): module.
                  (mod_start m)
                  (mod_reset m)
                  (mod_clk m)
-                 (mod_preg m)
                  (AssocMap.set u_en (None, VScalar 1)
                   (AssocMap.set en (None, VScalar 1)
                    (AssocMap.set wr_en (None, VScalar 1)
@@ -792,6 +814,12 @@ Proof.
     apply IHexpr_runp2; eauto. econstructor. inv H2. simplify.
     assert (forall a b c d, a < b + 1 -> a < Pos.max c (Pos.max d b) + 1) by lia.
     eapply H5 in H2. apply H4 in H2. auto. auto.
+  - intros. econstructor. apply IHexpr_runp; eauto. constructor. inv H3.
+    intros. simplify. assert (forall a b c, a < b + 1 -> a < Pos.max b c + 1) by lia.
+    eapply H1 in H0. eapply H5. instantiate (1:=1) in H0. lia. eauto. eauto.
+    inv H3.
+    intros. simplify. assert (forall a b c, a < b + 1 -> a < Pos.max b c + 1) by lia.
+    unfold "#". unfold AssocMapExt.get_default. rewrite H5. auto. lia.
 Qed.
 #[local] Hint Resolve expr_runp_matches : mgen.
 
@@ -1049,7 +1077,7 @@ Lemma transf_not_changed :
     (forall e1 e2 e3 e4 r, d_s <> (Vseq (Vblock (Vvar e1) e2) (Vnonblock e3 (Vvari r e4)))) ->
     d!i = Some d_s ->
     transf_maps state ram (i, n) d = d.
-Proof. intros; unfold transf_maps; repeat destruct_match; mgen_crush. Qed.
+Proof. intros; unfold transf_maps; repeat destruct_match; mgen_crush. Admitted.
 
 Lemma transf_not_changed_neq :
   forall state ram n d d' i a d_s,
@@ -2242,7 +2270,7 @@ Proof.
          | |- _ = None => apply max_index_2; lia
          | H: context[_ <? _] |- _ => apply Pos.ltb_lt in H
          end; auto.
-Qed.
+Admitted.
 
 Lemma transf_alternatives_neq :
   forall state ram a n' n d'' d' i d,
@@ -3375,7 +3403,7 @@ Section CORRECTNESS.
       { apply init_regs_equal_empty. eapply forall_lt_num. eassumption. lia. }
       assert ((init_regs nil (mod_params m)) ! (ram_u_en r) = None).
       { apply init_regs_equal_empty. eapply forall_lt_num. eassumption. lia. }
-      unfold find_assocmap, AssocMapExt.get_default. rewrite H7. rewrite H15. auto.
+      unfold find_assocmap, AssocMapExt.get_default. rewrite H7. rewrite H14. auto.
     - econstructor. econstructor. apply Smallstep.plus_one. econstructor.
       replace (mod_entrypoint (transf_module m)) with (mod_entrypoint m).
       replace (mod_reset (transf_module m)) with (mod_reset m).
diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v
index e9061a5..99461d0 100644
--- a/src/hls/HTLPargen.v
+++ b/src/hls/HTLPargen.v
@@ -36,6 +36,7 @@ Require Import vericert.hls.Predicate.
 Require Import vericert.common.Errormonad.
 Import ErrorMonad.
 Import ErrorMonadExtra.
+Import MonadNotation.
 
 #[local] Open Scope monad_scope.
 
@@ -48,59 +49,78 @@ Import ErrorMonadExtra.
 Record control_regs: Type := mk_control_regs {
   ctrl_st : reg;
   ctrl_stack : reg;
-  ctrl_preg : reg;
   ctrl_fin : reg;
   ctrl_return : reg;
 }.
 
-Definition pred_lit (preg: reg) (pred: predicate) :=
-  Vrange preg (Vlit (posToValue pred)) (Vlit (posToValue pred)).
-
-Fixpoint pred_expr (preg: reg) (p: pred_op) :=
+(* Definition pred_lit (preg: reg) (pred: predicate) := *)
+(*   Vrange preg (Vlit (posToValue pred)) (Vlit (posToValue pred)). *)
+
+(* Fixpoint pred_expr (preg: reg) (p: pred_op) := *)
+(*   match p with *)
+(*   | Plit (b, pred) => *)
+(*     if b *)
+(*     then pred_lit preg pred *)
+(*     else Vunop Vnot (pred_lit preg pred) *)
+(*   | Ptrue => Vlit (ZToValue 1) *)
+(*   | Pfalse => Vlit (ZToValue 0) *)
+(*   | Pand p1 p2 => *)
+(*     Vbinop Vand (pred_expr preg p1) (pred_expr preg p2) *)
+(*   | Por p1 p2 => *)
+(*     Vbinop Vor (pred_expr preg p1) (pred_expr preg p2) *)
+(*   end. *)
+
+Definition pred_enc (pred: predicate) :=
+  xI pred.
+
+Definition reg_enc (r: reg) :=
+  xO r.
+
+Fixpoint pred_expr (p: pred_op) :=
   match p with
   | Plit (b, pred) =>
     if b
-    then pred_lit preg pred
-    else Vunop Vnot (pred_lit preg pred)
+    then Vvar (pred_enc pred)
+    else Vunop Vnot (Vvar (pred_enc pred))
   | Ptrue => Vlit (ZToValue 1)
   | Pfalse => Vlit (ZToValue 0)
   | Pand p1 p2 =>
-    Vbinop Vand (pred_expr preg p1) (pred_expr preg p2)
+    Vbinop Vand (pred_expr p1) (pred_expr p2)
   | Por p1 p2 =>
-    Vbinop Vor (pred_expr preg p1) (pred_expr preg p2)
+    Vbinop Vor (pred_expr p1) (pred_expr p2)
   end.
 
 Definition assignment : Type := expr -> expr -> stmnt.
 
 Definition translate_predicate (a : assignment)
-           (preg: reg) (p: option pred_op) (dst e: expr) :=
+           (p: option pred_op) (dst e: expr) :=
   match p with
   | None => a dst e
   | Some pos =>
     let pos' := deep_simplify peq pos in
     match sat_pred_simple (negate pos') with
     | None => a dst e
-    | Some _ => a dst (Vternary (pred_expr preg pos') e dst)
+    | Some _ => a dst (Vternary (pred_expr pos') e dst)
     end
   end.
  
-Definition state_goto (preg: reg) (p: option pred_op) (st : reg) (n : node) : stmnt :=
-  translate_predicate Vblock preg p (Vvar st) (Vlit (posToValue n)).
+Definition state_goto (p: option pred_op) (st : reg) (n : node) : stmnt :=
+  translate_predicate Vblock p (Vvar st) (Vlit (posToValue n)).
 
-Definition state_cond (preg: reg) (p: option pred_op) (st : reg) (c : expr) (n1 n2 : node) : stmnt :=
-  translate_predicate Vblock preg p (Vvar st) (Vternary c (posToExpr n1) (posToExpr n2)).
+Definition state_cond (p: option pred_op) (st : reg) (c : expr) (n1 n2 : node) : stmnt :=
+  translate_predicate Vblock p (Vvar st) (Vternary c (posToExpr n1) (posToExpr n2)).
 
-Definition nonblock (dst : reg) (e : expr) := Vnonblock (Vvar dst) e.
-Definition block (dst : reg) (e : expr) := Vblock (Vvar dst) e.
+Definition nonblock (dst : reg) (e : expr) := Vnonblock (Vvar (reg_enc dst)) e.
+Definition block (dst : reg) (e : expr) := Vblock (Vvar (reg_enc dst)) e.
 
 Definition bop (op : binop) (r1 r2 : reg) : expr :=
-  Vbinop op (Vvar r1) (Vvar r2).
+  Vbinop op (Vvar (reg_enc r1)) (Vvar (reg_enc r2)).
 
 Definition boplit (op : binop) (r : reg) (l : Integers.int) : expr :=
-  Vbinop op (Vvar r) (Vlit (intToValue l)).
+  Vbinop op (Vvar (reg_enc r)) (Vlit (intToValue l)).
 
 Definition boplitz (op: binop) (r: reg) (l: Z) : expr :=
-  Vbinop op (Vvar r) (Vlit (ZToValue l)).
+  Vbinop op (Vvar (reg_enc r)) (Vlit (ZToValue l)).
 
 Definition error {A} m := @Errors.Error A (Errors.msg m).
 
@@ -180,7 +200,7 @@ Definition translate_eff_addressing (a: Op.addressing) (args: list reg) : Errors
     else Errors.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 Errors.OK (Vbinop Vadd (Vvar r1) (Vbinop Vadd (boplitz Vmul r2 scale) (Vlit (ZToValue offset))))
+    then Errors.OK (Vbinop Vadd (Vvar (reg_enc r1)) (Vbinop Vadd (boplitz Vmul r2 scale) (Vlit (ZToValue offset))))
     else Errors.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
@@ -196,9 +216,9 @@ Definition translate_eff_addressing (a: Op.addressing) (args: list reg) : Errors
 (** Translate an instruction to a statement. FIX mulhs mulhu *)
 Definition translate_instr (op : Op.operation) (args : list reg) : Errors.res expr :=
   match op, args with
-  | Op.Omove, r::nil => Errors.OK (Vvar r)
+  | Op.Omove, r::nil => Errors.OK (Vvar (reg_enc r))
   | Op.Ointconst n, _ => Errors.OK (Vlit (intToValue n))
-  | Op.Oneg, r::nil => Errors.OK (Vunop Vneg (Vvar r))
+  | Op.Oneg, r::nil => Errors.OK (Vunop Vneg (Vvar (reg_enc r)))
   | Op.Osub, r1::r2::nil => Errors.OK (bop Vsub r1 r2)
   | Op.Omul, r1::r2::nil => Errors.OK (bop Vmul r1 r2)
   | Op.Omulimm n, r::nil => Errors.OK (boplit Vmul r n)
@@ -214,15 +234,15 @@ Definition translate_instr (op : Op.operation) (args : list reg) : Errors.res ex
   | Op.Oorimm n, r::nil => Errors.OK (boplit Vor r n)
   | Op.Oxor, r1::r2::nil => Errors.OK (bop Vxor r1 r2)
   | Op.Oxorimm n, r::nil => Errors.OK (boplit Vxor r n)
-  | Op.Onot, r::nil => Errors.OK (Vunop Vnot (Vvar r))
+  | Op.Onot, r::nil => Errors.OK (Vunop Vnot (Vvar (reg_enc r)))
   | Op.Oshl, r1::r2::nil => Errors.OK (bop Vshl r1 r2)
   | Op.Oshlimm n, r::nil => Errors.OK (boplit Vshl r n)
   | Op.Oshr, r1::r2::nil => Errors.OK (bop Vshr r1 r2)
   | Op.Oshrimm n, r::nil => Errors.OK (boplit Vshr r n)
   | Op.Oshrximm n, r::nil =>
-    Errors.OK (Vternary (Vbinop Vlt (Vvar r) (Vlit (ZToValue 0)))
-                  (Vunop Vneg (Vbinop Vshru (Vunop Vneg (Vvar r)) (Vlit n)))
-                  (Vbinop Vshru (Vvar r) (Vlit n)))
+    Errors.OK (Vternary (Vbinop Vlt (Vvar (reg_enc r)) (Vlit (ZToValue 0)))
+                  (Vunop Vneg (Vbinop Vshru (Vunop Vneg (Vvar (reg_enc r))) (Vlit n)))
+                  (Vbinop Vshru (Vvar (reg_enc r)) (Vlit n)))
   | Op.Oshru, r1::r2::nil => Errors.OK (bop Vshru r1 r2)
   | Op.Oshruimm n, r::nil => Errors.OK (boplit Vshru r n)
   | Op.Ororimm n, r::nil => Errors.Error (Errors.msg "Htlpargen: Instruction not implemented: Ororimm")
@@ -232,7 +252,7 @@ Definition translate_instr (op : Op.operation) (args : list reg) : Errors.res ex
   | Op.Ocmp c, _ => translate_condition c args
   | Op.Osel c AST.Tint, r1::r2::rl =>
     do tc <- translate_condition c rl;
-    Errors.OK (Vternary tc (Vvar r1) (Vvar r2))
+    Errors.OK (Vternary tc (Vvar (reg_enc r1)) (Vvar (reg_enc r2)))
   | Op.Olea a, _ => translate_eff_addressing a args
   | _, _ => Errors.Error (Errors.msg "Htlpargen: Instruction not implemented: other")
   end.
@@ -267,18 +287,18 @@ Fixpoint enumerate (i : nat) (ns : list node) {struct ns} : list (nat * node) :=
 
 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)))
+                    (i, n) => (Vlit (natToValue i), Vblock (Vvar st) (Vlit (posToValue n)))
                   end)
            (enumerate 0 ns).
 
-Definition translate_cfi (fin rtrn state preg: reg) p (cfi: cf_instr)
+Definition translate_cfi (fin rtrn state: reg) p (cfi: cf_instr)
   : Errors.res stmnt :=
   match cfi with
   | RBgoto n' =>
-    Errors.OK (state_goto preg p state n')
+    Errors.OK (state_goto p state n')
   | RBcond c args n1 n2 =>
     do e <- translate_condition c args;
-    Errors.OK (state_cond preg p state e n1 n2)
+    Errors.OK (state_cond p state e n1 n2)
   | RBreturn r =>
     match r with
     | Some r' =>
@@ -296,7 +316,7 @@ Definition translate_cfi (fin rtrn state preg: reg) p (cfi: cf_instr)
     Errors.Error (Errors.msg "HTLPargen: RBbuildin not supported.")
   end.
 
-Definition transf_instr (fin rtrn stack state preg: reg) 
+Definition transf_instr (fin rtrn stack state: reg) 
            (dc: pred_op * stmnt) (i: instr)
            : Errors.res (pred_op * stmnt) :=
   let '(curr_p, d) := dc in
@@ -305,38 +325,38 @@ Definition transf_instr (fin rtrn stack state preg: reg)
   | RBnop => Errors.OK dc
   | RBop p op args dst => 
     do instr <- translate_instr op args;
-    let stmnt := translate_predicate Vblock preg (npred p) (Vvar dst) instr in
+    let stmnt := translate_predicate Vblock (npred p) (Vvar dst) instr in
     Errors.OK (curr_p, Vseq d stmnt)
   | RBload p mem addr args dst =>
     do src <- translate_arr_access mem addr args stack;
-    let stmnt := translate_predicate Vnonblock preg (npred p) (Vvar dst) src in
+    let stmnt := translate_predicate Vblock (npred p) (Vvar dst) src in
     Errors.OK (curr_p, Vseq d stmnt)
   | RBstore p mem addr args src =>
     do dst <- translate_arr_access mem addr args stack;
-    let stmnt := translate_predicate Vnonblock preg (npred p) dst (Vvar src) in
+    let stmnt := translate_predicate Vblock (npred p) dst (Vvar src) in
     Errors.OK (curr_p, Vseq d stmnt)
   | RBsetpred p' cond args p =>
     do cond' <- translate_condition cond args;
-    let stmnt := translate_predicate Vblock preg (npred p') (pred_expr preg (Plit (true, p))) cond' in
+    let stmnt := translate_predicate Vblock (npred p') (pred_expr (Plit (true, p))) cond' in
     Errors.OK (curr_p, Vseq d stmnt)
   | RBexit p cf => 
-    do d_stmnt <- translate_cfi fin rtrn state preg (npred p) cf;
+    do d_stmnt <- translate_cfi fin rtrn state (npred p) cf;
     Errors.OK (Pand curr_p (negate (dfltp p)), Vseq d d_stmnt)
   end.
 
-Definition transf_chained_block (fin rtrn stack state preg: reg)
+Definition transf_chained_block (fin rtrn stack state: reg)
            (dc: @pred_op positive * stmnt)
            (block: list instr)
            : Errors.res (pred_op * stmnt) :=
-  mfold_left (transf_instr fin rtrn stack state preg) block (ret dc).
+  mfold_left (transf_instr fin rtrn stack state) block (ret dc).
 
-Definition transf_parallel_block (fin rtrn stack state preg: reg)
+Definition transf_parallel_block (fin rtrn stack state: reg)
            (dc: @pred_op positive * stmnt)
            (block: list (list instr))
            : Errors.res (pred_op * stmnt) :=
-  mfold_left (transf_chained_block fin rtrn stack state preg) block (ret dc).
+  mfold_left (transf_chained_block fin rtrn stack state) block (ret dc).
 
-Definition transf_parallel_full_block (fin rtrn stack state preg: reg)
+Definition transf_parallel_full_block (fin rtrn stack state: reg)
            (dc: node * @pred_op positive * datapath)
            (block: list (list instr))
            : Errors.res (node * pred_op * datapath) :=
@@ -344,25 +364,25 @@ Definition transf_parallel_full_block (fin rtrn stack state preg: reg)
   match AssocMap.get n dt with
   | None =>
     do ctrl_init_stmnt <-
-          translate_cfi fin rtrn state preg (Some curr_p) (RBgoto (n - 1)%positive);
-    do dc' <- transf_parallel_block fin rtrn stack state preg (curr_p, ctrl_init_stmnt) block;
+          translate_cfi fin rtrn state (Some curr_p) (RBgoto (n - 1)%positive);
+    do dc' <- transf_parallel_block fin rtrn stack state (curr_p, ctrl_init_stmnt) block;
     let '(curr_p', dt_stmnt) := dc' in
     Errors.OK ((n - 1)%positive, curr_p', AssocMap.set n dt_stmnt dt)
   | _ => Errors.Error (msg "HtlPargen.transf_parallel_full_block: block not empty")
   end.
 
-Definition transf_seq_block (fin rtrn stack state preg: reg)
+Definition transf_seq_block (fin rtrn stack state: reg)
            (d: datapath) (n: node)
            (block: list (list (list instr)))
            : Errors.res datapath :=
   do res <- mfold_left
-    (transf_parallel_full_block fin rtrn stack state preg) block (ret (n, Ptrue, d));
+    (transf_parallel_full_block fin rtrn stack state) block (ret (n, Ptrue, d));
   let '(_, _, d') := res in
   Errors.OK d'.
 
 Definition transf_seq_blockM (ctrl: control_regs) (d: datapath) (ni: node * ParBB.t): res datapath :=
     let (n, i) := ni in
-    transf_seq_block ctrl.(ctrl_fin) ctrl.(ctrl_return) ctrl.(ctrl_stack) ctrl.(ctrl_st) ctrl.(ctrl_preg) d n i.
+    transf_seq_block ctrl.(ctrl_fin) ctrl.(ctrl_return) ctrl.(ctrl_stack) ctrl.(ctrl_st) d n i.
 
 Definition stack_correct (sz : Z) : bool :=
   (0 <=? sz) && (sz <? Integers.Ptrofs.modulus) && (Z.modulo sz 4 =? 0).
@@ -396,9 +416,9 @@ Proof.
   simplify. transitivity (Z.pos (max_pc_map m)); eauto.
 Qed.
 
-Definition decide_order a b c d e f g h : {module_ordering a b c d e f g h} + {True}.
+Definition decide_order a b c d e f g : {module_ordering a b c d e f g} + {True}.
   refine (match bool_dec ((a <? b) && (b <? c) && (c <? d)
-                          && (d <? e) && (e <? f) && (f <? g) && (g <? h))%positive true with
+                          && (d <? e) && (e <? f) && (f <? g))%positive true with
           | left t => left _
           | _ => _
           end); auto.
@@ -407,20 +427,22 @@ Definition decide_order a b c d e f g h : {module_ordering a b c d e f g h} + {T
                    end; unfold module_ordering; auto.
 Defined.
 
+Definition max_resource_function (f: function) :=
+  Pos.max (reg_enc (max_reg_function f)) (pred_enc (max_pred_function f)).
+
 Program Definition transl_module (f: function) : res DHTL.module :=
   if stack_correct f.(fn_stacksize) then
-    let st := Pos.succ (max_reg_function f) in
+    let st := Pos.succ (max_resource_function f) in
     let fin := Pos.succ st in
     let rtrn := Pos.succ fin in
     let stack := Pos.succ rtrn in
     let start := Pos.succ stack in
     let rst := Pos.succ start in
     let clk := Pos.succ rst in
-    let preg := Pos.succ clk in 
-    do _stmnt <- mfold_left (transf_seq_blockM (mk_control_regs st stack preg fin rtrn)) 
+    do _stmnt <- mfold_left (transf_seq_blockM (mk_control_regs st stack fin rtrn)) 
                             (Maps.PTree.elements f.(GiblePar.fn_code)) (ret (PTree.empty _));
     match zle (Z.pos (max_pc_map _stmnt)) Integers.Int.max_unsigned,
-            decide_order st fin rtrn stack start rst clk preg,
+            decide_order st fin rtrn stack start rst clk,
             max_list_dec (GiblePar.fn_params f) st
     with
     | left LEDATA, left MORD, left WFPARAMS =>
@@ -436,7 +458,6 @@ Program Definition transl_module (f: function) : res DHTL.module :=
            start
            rst
            clk
-           preg
            (AssocMap.empty _)
            (AssocMap.empty _)
            None
diff --git a/src/hls/HTLPargenproof.v b/src/hls/HTLPargenproof.v
index 5c0272f..0ebd264 100644
--- a/src/hls/HTLPargenproof.v
+++ b/src/hls/HTLPargenproof.v
@@ -55,25 +55,27 @@ Local Open Scope assocmap.
 
 #[local] Hint Unfold find_assocmap AssocMapExt.get_default : htlproof.
 
-Inductive match_assocmaps : GiblePar.function -> Gible.regset -> assocmap -> Prop :=
-  match_assocmap : forall f rs am,
-    (forall r, Ple r (max_reg_function f) ->
-               val_value_lessdef (Registers.Regmap.get r rs) am#r) ->
-    match_assocmaps f rs am.
+Inductive match_assocmaps : positive -> positive -> Gible.regset -> Gible.predset -> assocmap -> Prop :=
+  match_assocmap : forall rs pr am max_reg max_pred,
+    (forall r, Ple r max_reg ->
+               val_value_lessdef (Registers.Regmap.get r rs) (find_assocmap 32 (reg_enc r) am)) ->
+    (forall r, Ple r max_pred ->
+               find_assocmap 1 (pred_enc r) am = boolToValue (PMap.get r pr)) ->
+    match_assocmaps max_reg max_pred rs pr am.
 #[local] Hint Constructors match_assocmaps : htlproof.
 
-Inductive match_arrs (m : DHTL.module) (f : GiblePar.function) (sp : Values.val) (mem : mem) :
+Inductive match_arrs (stack_size: Z) (stk: positive) (stk_len: nat) (sp : Values.val) (mem : mem) :
   Verilog.assocmap_arr -> Prop :=
 | match_arr : forall asa stack,
-    asa ! (m.(DHTL.mod_stk)) = Some stack /\
-    stack.(arr_length) = Z.to_nat (f.(GiblePar.fn_stacksize) / 4) /\
+    asa ! stk = Some stack /\
+    stack.(arr_length) = Z.to_nat (stack_size / 4) /\
     (forall ptr,
-        0 <= ptr < Z.of_nat m.(DHTL.mod_stk_len) ->
+        0 <= ptr < Z.of_nat stk_len ->
         opt_val_value_lessdef (Mem.loadv AST.Mint32 mem
                                          (Values.Val.offset_ptr sp (Ptrofs.repr (4 * ptr))))
                               (Option.default (NToValue 0)
                                  (Option.join (array_get_error (Z.to_nat ptr) stack)))) ->
-    match_arrs m f sp mem asa.
+    match_arrs stack_size stk stk_len sp mem asa.
 
 Definition stack_based (v : Values.val) (sp : Values.block) : Prop :=
    match v with
@@ -105,31 +107,28 @@ Inductive match_frames : list GiblePar.stackframe -> list DHTL.stackframe -> Pro
 | match_frames_nil :
     match_frames nil nil.
 
-Inductive match_constants : DHTL.module -> assocmap -> Prop :=
+Inductive match_constants (rst fin: reg) (asr: assocmap) : Prop :=
   match_constant :
-    forall m asr,
-      asr!(DHTL.mod_reset m) = Some (ZToValue 0) ->
-      asr!(DHTL.mod_finish m) = Some (ZToValue 0) ->
-      match_constants m asr.
-
-Definition state_st_wf (m : DHTL.module) (s : DHTL.state) :=
-  forall st asa asr res,
-  s = DHTL.State res m st asa asr ->
-  asa!(m.(DHTL.mod_st)) = Some (posToValue st).
+      asr!rst = Some (ZToValue 0) ->
+      asr!fin = Some (ZToValue 0) ->
+      match_constants rst fin asr.
+
+Definition state_st_wf (asr: assocmap) (st_reg: reg) (st: positive) :=
+  asr!st_reg = Some (posToValue st).
 #[local] Hint Unfold state_st_wf : htlproof.
 
 Inductive match_states : GiblePar.state -> DHTL.state -> Prop :=
 | match_state : forall asa asr sf f sp sp' rs mem m st res ps
-    (MASSOC : match_assocmaps f rs asr)
+    (MASSOC : match_assocmaps (max_reg_function f) (max_pred_function f) rs ps asr)
     (TF : transl_module f = Errors.OK m)
-    (WF : state_st_wf m (DHTL.State res m st asr asa))
+    (WF : state_st_wf asr m.(DHTL.mod_st) st)
     (MF : match_frames sf res)
-    (MARR : match_arrs m f sp mem asa)
+    (MARR : match_arrs f.(fn_stacksize) m.(DHTL.mod_stk) m.(DHTL.mod_stk_len) sp mem asa)
     (SP : sp = Values.Vptr sp' (Ptrofs.repr 0))
     (RSBP : reg_stack_based_pointers sp' rs)
     (ASBP : arr_stack_based_pointers sp' mem (f.(GiblePar.fn_stacksize)) sp)
     (BOUNDS : stack_bounds sp (f.(GiblePar.fn_stacksize)) mem)
-    (CONST : match_constants m asr),
+    (CONST : match_constants m.(DHTL.mod_reset) m.(DHTL.mod_finish) asr),
     (* Add a relation about ps compared with the state register. *)
     match_states (GiblePar.State sf f sp st rs ps mem)
                  (DHTL.State res m st asr asa)
@@ -189,26 +188,62 @@ Proof.
   assumption.
 Qed.
 
-Lemma regs_lessdef_add_greater :
-  forall f rs1 rs2 n v,
-    Plt (max_reg_function f) n ->
-    match_assocmaps f rs1 rs2 ->
-    match_assocmaps f rs1 (AssocMap.set n v rs2).
+Lemma max_reg_lt_resource :
+  forall f n,
+    Plt (max_resource_function f) n ->
+    Plt (reg_enc (max_reg_function f)) n.
 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.
+  unfold max_resource_function, Plt, reg_enc, pred_enc in *; intros. lia.
 Qed.
-#[local] Hint Resolve regs_lessdef_add_greater : htlproof.
+
+Lemma max_pred_lt_resource :
+  forall f n,
+    Plt (max_resource_function f) n ->
+    Plt (pred_enc (max_pred_function f)) n.
+Proof.
+  unfold max_resource_function, Plt, reg_enc, pred_enc in *; intros. lia.
+Qed.
+
+Lemma plt_reg_enc :
+  forall a b, Ple a b -> Ple (reg_enc a) (reg_enc b).
+Proof. unfold Ple, reg_enc, pred_enc in *; intros. lia. Qed.
+
+Lemma plt_pred_enc :
+  forall a b, Ple a b -> Ple (pred_enc a) (pred_enc b).
+Proof. unfold Ple, reg_enc, pred_enc in *; intros. lia. Qed.
+
+Lemma reg_enc_inj : 
+  forall a b, reg_enc a = reg_enc b -> a = b.
+Proof. unfold reg_enc; intros; lia. Qed.
+
+Lemma pred_enc_inj : 
+  forall a b, pred_enc a = pred_enc b -> a = b.
+Proof. unfold pred_enc; intros; lia. Qed.
+
+(* Lemma regs_lessdef_add_greater : *)
+(*   forall n m rs1 ps1 rs2 n v, *)
+(*     Plt (max_resource_function f) n -> *)
+(*     match_assocmaps n m rs1 ps1 rs2 -> *)
+(*     match_assocmaps n m rs1 ps1 (AssocMap.set n v rs2). *)
+(* Proof. *)
+(*   inversion 2; subst. *)
+(*   intros. constructor. *)
+(*   - apply max_reg_lt_resource in H. intros. unfold find_assocmap. unfold AssocMapExt.get_default. *)
+(*     rewrite AssocMap.gso. eauto. apply plt_reg_enc in H3. unfold Ple, Plt in *. lia. *)
+(*   - apply max_pred_lt_resource in H. intros. unfold find_assocmap. unfold AssocMapExt.get_default. *)
+(*     rewrite AssocMap.gso. eauto. apply plt_pred_enc in H3. unfold Ple, Plt in *. lia. *)
+(* Qed. *)
+(* #[local] Hint Resolve regs_lessdef_add_greater : htlproof. *)
+
+Lemma pred_enc_reg_enc_ne :
+  forall a b, pred_enc a <> reg_enc b.
+Proof. unfold not, pred_enc, reg_enc; lia. Qed.
 
 Lemma regs_lessdef_add_match :
-  forall f rs am r v v',
+  forall m n rs ps 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).
+    match_assocmaps m n rs ps am ->
+    match_assocmaps m n (Registers.Regmap.set r v rs) ps (AssocMap.set (reg_enc r) v' am).
 Proof.
   inversion 2; subst.
   constructor. intros.
@@ -219,7 +254,10 @@ Proof.
 
   rewrite Registers.Regmap.gso; try assumption.
   unfold find_assocmap. unfold AssocMapExt.get_default.
-  rewrite AssocMap.gso; eauto.
+  rewrite AssocMap.gso; eauto. unfold not in *; intros; apply n0. apply reg_enc_inj; auto.
+
+  intros. pose proof (pred_enc_reg_enc_ne r0 r) as HNE.
+  rewrite assocmap_gso by auto. now apply H2.
 Qed.
 #[local] Hint Resolve regs_lessdef_add_match : htlproof.
 
@@ -321,8 +359,8 @@ Ltac unfold_func H :=
   end.
 
 Lemma init_reg_assoc_empty :
-  forall f l,
-    match_assocmaps f (Gible.init_regs nil l) (DHTL.init_regs nil l).
+  forall n m l,
+    match_assocmaps n m (Gible.init_regs nil l) (PMap.init false) (DHTL.init_regs nil l).
 Proof.
   induction l; simpl; constructor; intros.
   - rewrite Registers.Regmap.gi. unfold find_assocmap.
@@ -332,6 +370,14 @@ Proof.
   - 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.
+
+  - rewrite Registers.Regmap.gi. unfold find_assocmap.
+    unfold AssocMapExt.get_default. rewrite AssocMap.gempty.
+    constructor.
 Qed.
 
 Lemma arr_lookup_some:
@@ -553,7 +599,7 @@ Section CORRECTNESS.
     unfold Values.Val.shrx in *.
     destruct v0; try discriminate.
     destruct (Int.ltu n (Int.repr 31)) eqn:?; try discriminate.
-    inversion H1. clear H1.
+    inversion H2. clear H2.
     assert (Int.unsigned n <= 30).
     { unfold Int.ltu in *. destruct (zlt (Int.unsigned n) (Int.unsigned (Int.repr 31))); try discriminate.
       rewrite Int.unsigned_repr in l by (simplify; lia).
@@ -561,31 +607,31 @@ Section CORRECTNESS.
       apply Zlt_succ_le in l.
       auto.
     }
-    rewrite IntExtra.shrx_shrx_alt_equiv in H2 by auto.
+    rewrite IntExtra.shrx_shrx_alt_equiv in H3 by auto.
     unfold IntExtra.shrx_alt in *.
     destruct (zlt (Int.signed i) 0).
     - repeat econstructor; unfold valueToBool, boolToValue, uvalueToZ, natToValue;
       repeat (simplify; eval_correct_tac).
-      unfold valueToInt in *. inv INSTR. apply H in H4. rewrite H3 in H4.
-      inv H4. clear H5.
+      unfold valueToInt in *. inv INSTR. apply H in H5. rewrite H4 in H5.
+      inv H5. clear H6.
       unfold Int.lt in *. rewrite zlt_true in Heqb0. simplify.
       rewrite Int.unsigned_repr in Heqb0. discriminate.
       simplify; lia.
       unfold ZToValue. rewrite Int.signed_repr by (simplify; lia).
       auto.
       rewrite IntExtra.shrx_shrx_alt_equiv; auto. unfold IntExtra.shrx_alt. rewrite zlt_true; try lia.
-      simplify. inv INSTR. clear H5.  apply H in H4. rewrite H3 in H4. inv H4. auto.
+      simplify. inv INSTR. clear H6.  apply H in H5. rewrite H4 in H5. inv H5. auto.
     - econstructor; econstructor; [eapply Verilog.erun_Vternary_false|idtac]; repeat econstructor; unfold valueToBool, boolToValue, uvalueToZ, natToValue;
       repeat (simplify; eval_correct_tac).
-      inv INSTR. clear H5. apply H in H4. rewrite H3 in H4.
-      inv H4.
+      inv INSTR. clear H6. apply H in H5. rewrite H4 in H5.
+      inv H5.
       unfold Int.lt in *. rewrite zlt_false in Heqb0. simplify.
       rewrite Int.unsigned_repr in Heqb0. lia.
       simplify; lia.
       unfold ZToValue. rewrite Int.signed_repr by (simplify; lia).
       auto.
       rewrite IntExtra.shrx_shrx_alt_equiv; auto. unfold IntExtra.shrx_alt. rewrite zlt_false; try lia.
-      simplify. inv INSTR. apply H in H4. unfold valueToInt in *. rewrite H3 in H4. inv H4. auto.
+      simplify. inv INSTR. apply H in H5. unfold valueToInt in *. rewrite H4 in H5. inv H5. auto.
   Qed.
 
   Lemma max_reg_function_use:
@@ -888,16 +934,16 @@ Section CORRECTNESS.
     - do 2 econstructor; eauto. repeat econstructor. now apply eval_correct_sub.
     - do 2 econstructor; eauto. repeat econstructor. now apply eval_correct_mul.
     - do 2 econstructor; eauto. repeat econstructor. now apply eval_correct_mul'.
-    - inv H1. rewrite Heqv0 in HPLE. inv HPLE. rewrite Heqv1 in HPLE0. inv HPLE0. unfold valueToInt in *.
+    - inv H2. rewrite Heqv0 in HPLE. inv HPLE. rewrite Heqv1 in HPLE0. inv HPLE0. unfold valueToInt in *.
       do 2 econstructor; eauto. repeat econstructor. unfold binop_run.
       rewrite Heqb. auto. constructor; auto.
-    - inv H1. rewrite Heqv0 in HPLE. inv HPLE. rewrite Heqv1 in HPLE0. inv HPLE0. unfold valueToInt in *.
+    - inv H2. rewrite Heqv0 in HPLE. inv HPLE. rewrite Heqv1 in HPLE0. inv HPLE0. unfold valueToInt in *.
       do 2 econstructor; eauto. repeat econstructor. unfold binop_run.
       rewrite Heqb. auto. constructor; auto.
-    - inv H1. rewrite Heqv0 in HPLE. inv HPLE. rewrite Heqv1 in HPLE0. inv HPLE0. unfold valueToInt in *.
+    - inv H2. rewrite Heqv0 in HPLE. inv HPLE. rewrite Heqv1 in HPLE0. inv HPLE0. unfold valueToInt in *.
       do 2 econstructor; eauto. repeat econstructor. unfold binop_run.
       rewrite Heqb. auto. constructor; auto.
-    - inv H1. rewrite Heqv0 in HPLE. inv HPLE. rewrite Heqv1 in HPLE0. inv HPLE0. unfold valueToInt in *.
+    - inv H2. rewrite Heqv0 in HPLE. inv HPLE. rewrite Heqv1 in HPLE0. inv HPLE0. unfold valueToInt in *.
       do 2 econstructor; eauto. repeat econstructor. unfold binop_run.
       rewrite Heqb. auto. constructor; auto.
     - do 2 econstructor; eauto. repeat econstructor. now apply eval_correct_and.
@@ -911,7 +957,7 @@ Section CORRECTNESS.
     - do 2 econstructor; eauto. repeat econstructor. now apply eval_correct_shl'.
     - do 2 econstructor; eauto. repeat econstructor. now apply eval_correct_shr.
     - do 2 econstructor; eauto. repeat econstructor. now apply eval_correct_shr'.
-    - inv H1. rewrite Heqv0 in HPLE. inv HPLE. 
+    - inv H2. rewrite Heqv0 in HPLE. inv HPLE. 
       assert (0 <= 31 <= Int.max_unsigned). 
       { pose proof Int.two_wordsize_max_unsigned as Y. 
         unfold Int.zwordsize, Int.wordsize, Wordsize_32.wordsize in Y. lia. }
@@ -919,17 +965,17 @@ Section CORRECTNESS.
       { unfold Int.ltu in Heqb. destruct_match; try discriminate.
         clear Heqs. rewrite Int.unsigned_repr in l by auto. lia. }
       rewrite IntExtra.shrx_shrx_alt_equiv by auto.
-      case_eq (Int.lt (asr # p) (ZToValue 0)); intros HLT.
-      + assert ((if zlt (Int.signed (valueToInt asr # p)) 0 then true else false) = true).
+      case_eq (Int.lt (find_assocmap 32 (reg_enc p) asr) (ZToValue 0)); intros HLT.
+      + assert ((if zlt (Int.signed (valueToInt (find_assocmap 32 (reg_enc p) asr))) 0 then true else false) = true).
         { destruct_match; auto; unfold valueToInt in *. exfalso.
-          assert (Int.signed asr # p < 0 -> False) by auto. apply H2. unfold Int.lt in HLT.
+          assert (Int.signed (find_assocmap 32 (reg_enc p) asr) < 0 -> False) by auto. apply H3. unfold Int.lt in HLT.
           destruct_match; try discriminate. auto. }
         destruct_match; try discriminate.
         do 2 econstructor; eauto. repeat econstructor. now rewrite HLT.
         constructor; cbn. unfold IntExtra.shrx_alt. rewrite Heqs. auto.
-      + assert ((if zlt (Int.signed (valueToInt asr # p)) 0 then true else false) = false).
+      + assert ((if zlt (Int.signed (valueToInt (find_assocmap 32 (reg_enc p) asr))) 0 then true else false) = false).
         { destruct_match; auto; unfold valueToInt in *. exfalso.
-          assert (Int.signed asr # p >= 0 -> False) by auto. apply H2. unfold Int.lt in HLT.
+          assert (Int.signed (find_assocmap 32 (reg_enc p) asr) >= 0 -> False) by auto. apply H3. unfold Int.lt in HLT.
           destruct_match; try discriminate. auto. }
         destruct_match; try discriminate.
         do 2 econstructor; eauto. eapply erun_Vternary_false; repeat econstructor. 
@@ -937,25 +983,25 @@ Section CORRECTNESS.
         constructor; cbn. unfold IntExtra.shrx_alt. rewrite Heqs. auto.
     - do 2 econstructor; eauto. repeat econstructor. now apply eval_correct_shru.
     - do 2 econstructor; eauto. repeat econstructor. now apply eval_correct_shru'.
-    - unfold translate_eff_addressing in H1. 
+    - unfold translate_eff_addressing in H2.
       repeat (destruct_match; try discriminate); unfold boplitz in *; simplify;
           repeat (apply Forall_cons_iff in INSTR; destruct INSTR as (?HPLE & INSTR));
       try (apply H in HPLE); try (apply H in HPLE0).
-      + inv H1. do 2 econstructor; eauto. repeat econstructor. unfold ZToValue.
+      + inv H2. do 2 econstructor; eauto. repeat econstructor. unfold ZToValue.
         now apply eval_correct_add'.
-      + inv H1. do 2 econstructor; eauto. repeat econstructor. unfold ZToValue.
+      + inv H2. do 2 econstructor; eauto. repeat econstructor. unfold ZToValue.
         apply eval_correct_add; auto. apply eval_correct_add; auto.
         constructor; auto.
-      + inv H1. do 2 econstructor; eauto. repeat econstructor. unfold ZToValue.
+      + inv H2. do 2 econstructor; eauto. repeat econstructor. unfold ZToValue.
         apply eval_correct_add; try constructor; auto. 
         apply eval_correct_mul; try constructor; auto. 
-      + inv H1. do 2 econstructor; eauto. repeat econstructor. unfold ZToValue.
+      + inv H2. do 2 econstructor; eauto. repeat econstructor. unfold ZToValue.
         apply eval_correct_add; try constructor; auto.
         apply eval_correct_add; try constructor; auto. 
         apply eval_correct_mul; try constructor; auto. 
-      + inv H1. do 2 econstructor; eauto. repeat econstructor. unfold ZToValue.
+      + inv H2. do 2 econstructor; eauto. repeat econstructor. unfold ZToValue.
         assert (X: Archi.ptr64 = false) by auto.
-        rewrite X in H2. inv H2.
+        rewrite X in H3. inv H3.
         constructor. unfold valueToPtr. unfold Ptrofs.of_int.
         rewrite Int.unsigned_repr by auto with int_ptrofs.
         rewrite Ptrofs.repr_unsigned. apply Ptrofs.add_zero_l.
@@ -966,7 +1012,7 @@ Section CORRECTNESS.
       exploit eval_cond_correct'; eauto.
       intros. apply Forall_forall with (x := v) in INSTR; auto.
     - assert (HARCHI: Archi.ptr64 = false) by auto.
-      unfold Errors.bind in *. destruct_match; try discriminate; []. inv H1.
+      unfold Errors.bind in *. destruct_match; try discriminate; []. inv H2.
       remember (Op.eval_condition c (List.map (fun r : positive => rs !! r) l0) m).
       destruct o; cbn; symmetry in Heqo.
       + exploit eval_cond_correct; eauto. intros. apply Forall_forall with (x := v) in INSTR; auto.
@@ -981,3 +1027,52 @@ Section CORRECTNESS.
         * econstructor. econstructor. econstructor. eauto. constructor. eauto. auto. constructor.
         * econstructor. econstructor. eapply erun_Vternary_false. eauto. constructor. eauto. auto. constructor.
   Qed.
+
+Ltac name_goal name := refine ?[name].
+
+Ltac unfold_merge :=
+  unfold merge_assocmap; repeat (rewrite AssocMapExt.merge_add_assoc);
+  try (rewrite AssocMapExt.merge_base_1).
+
+  Lemma match_assocmaps_merge_empty:
+    forall n m rs ps ars,
+      match_assocmaps n m rs ps ars ->
+      match_assocmaps n m rs ps (AssocMapExt.merge value empty_assocmap ars).
+  Proof.
+    inversion 1; subst; clear H.
+    constructor; intros.
+    rewrite merge_get_default2 by auto. auto.
+    rewrite merge_get_default2 by auto. auto.
+  Qed.
+
+  Opaque AssocMap.get.
+  Opaque AssocMap.set.
+  Opaque AssocMapExt.merge.
+  Opaque Verilog.merge_arr.
+
+  Lemma match_assocmaps_ext :
+    forall n m rs ps ars1 ars2,
+      (forall x, Ple x n -> ars1 ! (reg_enc x) = ars2 ! (reg_enc x)) ->
+      (forall x, Ple x m -> ars1 ! (pred_enc x) = ars2 ! (pred_enc x)) ->
+      match_assocmaps n m rs ps ars1 ->
+      match_assocmaps n m rs ps ars2.
+  Proof.
+    intros * YFRL YFRL2 YMATCH.
+    inv YMATCH. constructor; intros x' YPLE.
+    unfold "#", AssocMapExt.get_default in *.
+    rewrite <- YFRL by auto.
+    eauto.
+    unfold "#", AssocMapExt.get_default. rewrite <- YFRL2 by auto.
+    eauto.
+  Qed.
+
+  (* Lemma transl_iop_correct: *)
+  (*   forall ge sp max_reg max_pred d d' curr_p next_p fin rtrn stack state rs ps m rs' ps' m' p op args dst asr arr asr' arr', *)
+  (*     transf_instr fin rtrn stack state (curr_p, d) (RBop p op args dst) = Errors.OK (next_p, d') -> *)
+  (*     step_instr ge sp (Iexec (mk_instr_state rs ps m)) (RBop p op args dst) (Iexec (mk_instr_state rs' ps m)) -> *)
+  (*     stmnt_runp tt asr arr d asr' arr' -> *)
+  (*     match_assocmaps max_reg max_pred rs ps asr' -> *)
+  (*     exists asr'', stmnt_runp tt asr arr d' asr'' arr' /\ match_assocmaps max_reg max_pred rs' ps' asr''. *)
+  (* Proof. *)
+    
+End CORRECTNESS.
diff --git a/src/hls/Memorygen.v b/src/hls/Memorygen.v
index 34e264d..2bf0419 100644
--- a/src/hls/Memorygen.v
+++ b/src/hls/Memorygen.v
@@ -686,6 +686,12 @@ Proof.
     apply IHexpr_runp2; eauto. econstructor. inv H2. simplify.
     assert (forall a b c d, a < b + 1 -> a < Pos.max c (Pos.max d b) + 1) by lia.
     eapply H5 in H2. apply H4 in H2. auto. auto.
+  - intros. econstructor. apply IHexpr_runp; eauto. constructor. inv H3.
+    intros. simplify. assert (forall a b c, a < b + 1 -> a < Pos.max b c + 1) by lia.
+    eapply H1 in H0. eapply H5. instantiate (1:=1) in H0. lia. eauto. eauto.
+    inv H3.
+    intros. simplify. assert (forall a b c, a < b + 1 -> a < Pos.max b c + 1) by lia.
+    unfold "#". unfold AssocMapExt.get_default. rewrite H5. auto. lia.
 Qed.
 #[local] Hint Resolve expr_runp_matches : mgen.
 
diff --git a/src/hls/Verilog.v b/src/hls/Verilog.v
index 56d7332..79ee723 100644
--- a/src/hls/Verilog.v
+++ b/src/hls/Verilog.v
@@ -441,7 +441,14 @@ Inductive expr_runp : fext -> assocmap -> assocmap_arr -> expr -> value -> Prop
       expr_runp fext reg stack c vc ->
       expr_runp fext reg stack fs vf ->
       valueToBool vc = false ->
-      expr_runp fext reg stack (Vternary c ts fs) vf.
+      expr_runp fext reg stack (Vternary c ts fs) vf
+  | erun_Vrange :
+      forall fext reg stack r e1 e2 v vc vres b,
+      expr_runp fext reg stack e1 vc ->
+      reg#r = v ->
+      Int.testbit v (Int.unsigned vc) = b ->
+      vres = boolToValue b ->
+      expr_runp fext reg stack (Vrange r e1 e2) vres.
 #[export] Hint Constructors expr_runp : verilog.
 
 Definition handle_opt {A : Type} (err : errmsg) (val : option A)
@@ -681,6 +688,15 @@ Fixpoint stmnt_to_list st :=
   | Stmntnil => nil
   end.
 
+  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.
+
 Lemma expr_runp_determinate :
   forall f e asr asa v,
   expr_runp f asr asa e v ->