Finish load and store proof, but broke top-level

7 files changed, 317 insertions, 289 deletions

diff --git a/src/hls/HTL.v b/src/hls/HTL.v
index 98ea6d0..e614246 100644
--- a/src/hls/HTL.v
+++ b/src/hls/HTL.v
@@ -18,6 +18,7 @@
  *)
 
 Require Import Coq.FSets.FMapPositive.
+Require Import Coq.micromega.Lia.
 
 Require compcert.common.Events.
 Require compcert.common.Globalenvs.
@@ -32,6 +33,8 @@ Require Import vericert.hls.AssocMap.
 Require Import vericert.hls.Array.
 Require vericert.hls.Verilog.
 
+Local Open Scope positive.
+
 (** The purpose of the hardware transfer language (HTL) is to create a more
 hardware-like layout that is still similar to the register transfer language
 (RTL) that it came from. The main change is that function calls become module
@@ -49,7 +52,7 @@ Definition controllogic := PTree.t Verilog.stmnt.
 Definition map_well_formed {A : Type} (m : PTree.t A) : Prop :=
   forall p0 : positive,
     In p0 (map fst (Maps.PTree.elements m)) ->
-    Z.pos p0 <= Integers.Int.max_unsigned.
+    (Z.pos p0 <= Integers.Int.max_unsigned)%Z.
 
 Record ram := mk_ram {
   ram_size: nat;
@@ -64,9 +67,11 @@ Record ram := mk_ram {
                  /\ ram_en < ram_d_in
                  /\ ram_d_in < ram_d_out
                  /\ ram_d_out < ram_wr_en
-                 /\ ram_wr_en < ram_u_en)%positive
+                 /\ ram_wr_en < ram_u_en)
 }.
 
+Definition module_ordering a b c d e f g := a < b < c /\ c < d < e /\ e < f < g.
+
 Record module: Type :=
   mkmodule {
     mod_params : list reg;
@@ -84,7 +89,9 @@ Record module: Type :=
     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_controllogic /\ map_well_formed mod_datapath);
+    mod_wf : map_well_formed mod_controllogic /\ 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_ram_wf : forall r', mod_ram = Some r' -> mod_clk < ram_addr r';
   }.
 
 Definition fundef := AST.fundef module.
@@ -198,7 +205,7 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop :=
       asr' = Verilog.merge_regs nasr3 basr3 ->
       asa' = Verilog.merge_arrs nasa3 basa3 ->
       asr'!(m.(mod_st)) = Some (posToValue pstval) ->
-      Z.pos pstval <= Integers.Int.max_unsigned ->
+      (Z.pos pstval <= Integers.Int.max_unsigned)%Z ->
       step g (State sf m st asr asa) Events.E0 (State sf m pstval asr' asa')
 | step_finish :
     forall g m st asr asa retval sf,
@@ -237,3 +244,97 @@ Inductive final_state : state -> Integers.int -> Prop :=
 Definition semantics (m : program) :=
   Smallstep.Semantics step (initial_state m) final_state
                       (Globalenvs.Genv.globalenv m).
+
+Definition max_pc_function (m: module) :=
+  List.fold_left Pos.max (List.map fst (PTree.elements m.(mod_controllogic))) 1.
+
+Definition max_list := fold_right Pos.max 1.
+
+Definition max_stmnt_tree t :=
+  PTree.fold (fun i _ st => Pos.max (Verilog.max_reg_stmnt st) i) t 1.
+
+Definition max_reg_ram r :=
+  match r with
+  | None => 1
+  | Some ram => Pos.max (ram_mem ram)
+                (Pos.max (ram_en ram)
+                 (Pos.max (ram_addr ram)
+                  (Pos.max (ram_addr ram)
+                   (Pos.max (ram_wr_en ram)
+                    (Pos.max (ram_d_in ram)
+                     (Pos.max (ram_d_out ram) (ram_u_en ram)))))))
+  end.
+
+Definition max_reg_module m :=
+  Pos.max (max_list (mod_params m))
+   (Pos.max (max_stmnt_tree (mod_datapath m))
+    (Pos.max (max_stmnt_tree (mod_controllogic m))
+     (Pos.max (mod_st m)
+      (Pos.max (mod_stk m)
+       (Pos.max (mod_finish m)
+        (Pos.max (mod_return m)
+         (Pos.max (mod_start m)
+          (Pos.max (mod_reset 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).
+Proof. induction l; crush; apply IHl; lia. Qed.
+
+Lemma max_fold_lt2 :
+  forall (l: list (positive * Verilog.stmnt)) v n,
+    v <= n ->
+    v <= fold_left (fun a p => Pos.max (Verilog.max_reg_stmnt (snd p)) a) l n.
+Proof. induction l; crush; apply IHl; lia. Qed.
+
+Lemma max_fold_lt3 :
+  forall (l: list (positive * Verilog.stmnt)) v v',
+    v <= v' ->
+    fold_left (fun a0 p => Pos.max (Verilog.max_reg_stmnt (snd p)) a0) l v
+    <= fold_left (fun a0 p => Pos.max (Verilog.max_reg_stmnt (snd p)) a0) l v'.
+Proof. induction l; crush; apply IHl; lia. Qed.
+
+Lemma max_fold_lt4 :
+  forall (l: list (positive * Verilog.stmnt)) (a: positive * Verilog.stmnt),
+    fold_left (fun a0 p => Pos.max (Verilog.max_reg_stmnt (snd p)) a0) l 1
+    <= fold_left (fun a0 p => Pos.max (Verilog.max_reg_stmnt (snd p)) a0) l
+                 (Pos.max (Verilog.max_reg_stmnt (snd a)) 1).
+Proof. intros; apply max_fold_lt3; lia. Qed.
+
+Lemma max_reg_stmnt_lt_stmnt_tree':
+  forall l (i: positive) v,
+    In (i, v) l ->
+    list_norepet (map fst l) ->
+    Verilog.max_reg_stmnt v <= fold_left (fun a p => Pos.max (Verilog.max_reg_stmnt (snd p)) a) l 1.
+Proof.
+  induction l; crush. inv H; inv H0; simplify. apply max_fold_lt2. lia.
+  transitivity (fold_left (fun (a : positive) (p : positive * Verilog.stmnt) =>
+                             Pos.max (Verilog.max_reg_stmnt (snd p)) a) l 1).
+  eapply IHl; eauto. apply max_fold_lt4.
+Qed.
+
+Lemma max_reg_stmnt_le_stmnt_tree :
+  forall d i v,
+    d ! i = Some v ->
+    Verilog.max_reg_stmnt v <= max_stmnt_tree d.
+Proof.
+  intros. unfold max_stmnt_tree. rewrite PTree.fold_spec.
+  apply PTree.elements_correct in H.
+  eapply max_reg_stmnt_lt_stmnt_tree'; eauto.
+  apply PTree.elements_keys_norepet.
+Qed.
+
+Lemma max_reg_stmnt_lt_stmnt_tree :
+  forall d i v,
+    d ! i = Some v ->
+    Verilog.max_reg_stmnt v < max_stmnt_tree d + 1.
+Proof. intros. apply max_reg_stmnt_le_stmnt_tree in H; lia. Qed.
+
+Lemma max_stmnt_lt_module :
+  forall m d i,
+    (mod_controllogic m) ! i = Some d \/ (mod_datapath m) ! i = Some d ->
+    Verilog.max_reg_stmnt d < max_reg_module m + 1.
+Proof.
+  inversion 1 as [ Hv | Hv ]; unfold max_reg_module;
+  apply max_reg_stmnt_le_stmnt_tree in Hv; lia.
+Qed.
diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v
index 9bf7ed7..50defee 100644
--- a/src/hls/HTLPargen.v
+++ b/src/hls/HTLPargen.v
@@ -786,7 +786,19 @@ Definition transf_bblock (fin rtrn stack preg: reg) (ni : node * bblock)
   | _ => translate_cfi fin rtrn stack preg (nstate, bb.(bb_exit))
   end.
 
-Definition transf_module (f: function) : mon HTL.module :=
+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))%positive true with
+          | left t => left _
+          | _ => _
+          end); auto.
+  simplify; repeat match goal with
+                   | H: context[(_ <? _)%positive] |- _ => apply Pos.ltb_lt in H
+                   end; unfold module_ordering; auto.
+Defined.
+
+Definition transf_module (f: function) : mon HTL.module.
+  refine (
   if stack_correct f.(fn_stacksize) then
     do fin <- create_reg (Some Voutput) 1;
     do rtrn <- create_reg (Some Voutput) 32;
@@ -804,8 +816,10 @@ Definition transf_module (f: function) : mon HTL.module :=
     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 =>
+              Integers.Int.max_unsigned,
+          decide_order (st_st current_state) fin rtrn stack start rst clk
+    with
+    | left LEDATA, left LECTRL, left MORD =>
         ret (HTL.mkmodule
            f.(fn_params)
            current_state.(st_datapath)
@@ -822,10 +836,13 @@ Definition transf_module (f: function) : mon HTL.module :=
            current_state.(st_scldecls)
            current_state.(st_arrdecls)
            None
-           (conj (max_pc_wf _ LECTRL) (max_pc_wf _ LEDATA)))
-    | _, _ => error (Errors.msg "More than 2^32 states.")
+           (conj (max_pc_wf _ LECTRL) (max_pc_wf _ LEDATA))
+           MORD
+           _)
+    | _, _, _ => error (Errors.msg "More than 2^32 states.")
     end
-  else error (Errors.msg "Stack size misalignment.").
+  else error (Errors.msg "Stack size misalignment.")); discriminate.
+Defined.
 
 Definition max_state (f: function) : state :=
   let st := Pos.succ (max_reg_function f) in
diff --git a/src/hls/HTLgen.v b/src/hls/HTLgen.v
index c071868..b55d7a3 100644
--- a/src/hls/HTLgen.v
+++ b/src/hls/HTLgen.v
@@ -583,7 +583,19 @@ Proof.
   simplify. transitivity (Z.pos (max_pc_map m)); eauto.
 Qed.
 
-Definition transf_module (f: function) : mon HTL.module :=
+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))%positive true with
+          | left t => left _
+          | _ => _
+          end); auto.
+  simplify; repeat match goal with
+                   | H: context[(_ <? _)%positive] |- _ => apply Pos.ltb_lt in H
+                   end; unfold module_ordering; auto.
+Defined.
+
+Definition transf_module (f: function) : mon HTL.module.
+  refine (
   if stack_correct f.(fn_stacksize) then
     do fin <- create_reg (Some Voutput) 1;
     do rtrn <- create_reg (Some Voutput) 32;
@@ -595,8 +607,10 @@ Definition transf_module (f: function) : mon HTL.module :=
     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 =>
+          zle (Z.pos (max_pc_map current_state.(st_controllogic))) Integers.Int.max_unsigned,
+          decide_order (st_st current_state) fin rtrn stack start rst clk
+    with
+    | left LEDATA, left LECTRL, left MORD =>
         ret (HTL.mkmodule
            f.(RTL.fn_params)
            current_state.(st_datapath)
@@ -613,16 +627,19 @@ Definition transf_module (f: function) : mon HTL.module :=
            current_state.(st_scldecls)
            current_state.(st_arrdecls)
            None
-           (conj (max_pc_wf _ LECTRL) (max_pc_wf _ LEDATA)))
-    | _, _ => error (Errors.msg "More than 2^32 states.")
+           (conj (max_pc_wf _ LECTRL) (max_pc_wf _ LEDATA))
+           MORD
+           _)
+    | _, _, _ => error (Errors.msg "More than 2^32 states.")
     end
-  else error (Errors.msg "Stack size misalignment.").
+  else error (Errors.msg "Stack size misalignment.")); discriminate.
+Defined.
 
 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))
+          (Pos.succ (RTL.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))
@@ -633,23 +650,6 @@ Definition transl_module (f : function) : Errors.res HTL.module :=
 
 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
diff --git a/src/hls/HTLgenspec.v b/src/hls/HTLgenspec.v
index 7cb6d8c..6a10fa2 100644
--- a/src/hls/HTLgenspec.v
+++ b/src/hls/HTLgenspec.v
@@ -178,12 +178,12 @@ 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,
+    forall data control fin rtrn st stk stk_len m start rst clk scldecls arrdecls wf1 wf2 wf3,
       m = (mkmodule f.(RTL.fn_params)
                         data
                         control
                         f.(RTL.fn_entrypoint)
-                        st stk stk_len fin rtrn start rst clk scldecls arrdecls None wf) ->
+                        st stk stk_len fin rtrn start rst clk scldecls arrdecls None wf1 wf2 wf3) ->
       (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) ->
@@ -648,5 +648,9 @@ Proof.
   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.
+  rewrite H5. rewrite H7. apply EQ2.
   apply PTree.elements_complete.
+  eauto with htlspec.
+  erewrite <- collect_declare_freshreg_trans; try eassumption.
+  lia.
 Qed.
diff --git a/src/hls/Memorygen.v b/src/hls/Memorygen.v
index 87317ef..4f74b3f 100644
--- a/src/hls/Memorygen.v
+++ b/src/hls/Memorygen.v
@@ -39,6 +39,10 @@ Require Import vericert.hls.Array.
 Local Open Scope positive.
 Local Open Scope assocmap.
 
+Hint Resolve max_reg_stmnt_le_stmnt_tree : mgen.
+Hint Resolve max_reg_stmnt_lt_stmnt_tree : mgen.
+Hint Resolve max_stmnt_lt_module : mgen.
+
 Lemma int_eq_not_false : forall x, Int.eq x (Int.not x) = false.
 Proof.
   intros. unfold Int.eq.
@@ -48,138 +52,6 @@ Proof.
   specialize (X (Int.unsigned x)). apply zeq_false; auto.
 Qed.
 
-Definition max_pc_function (m: module) :=
-  List.fold_left Pos.max (List.map fst (PTree.elements m.(mod_controllogic))) 1.
-
-Fixpoint max_reg_expr (e: expr) :=
-  match e with
-  | Vlit _ => 1
-  | Vvar r => r
-  | Vvari r e => Pos.max r (max_reg_expr e)
-  | Vrange r e1 e2 => Pos.max r (Pos.max (max_reg_expr e1) (max_reg_expr e2))
-  | Vinputvar r => r
-  | Vbinop _ e1 e2 => Pos.max (max_reg_expr e1) (max_reg_expr e2)
-  | Vunop _ e => max_reg_expr e
-  | Vternary e1 e2 e3 => Pos.max (max_reg_expr e1) (Pos.max (max_reg_expr e2) (max_reg_expr e3))
-  end.
-
-Fixpoint max_reg_stmnt (st: stmnt) :=
-  match st with
-  | Vskip => 1
-  | Vseq s1 s2 => Pos.max (max_reg_stmnt s1) (max_reg_stmnt s2)
-  | Vcond e s1 s2 =>
-    Pos.max (max_reg_expr e)
-            (Pos.max (max_reg_stmnt s1) (max_reg_stmnt s2))
-  | Vcase e stl None => Pos.max (max_reg_expr e) (max_reg_stmnt_expr_list stl)
-  | Vcase e stl (Some s) =>
-    Pos.max (max_reg_stmnt s)
-            (Pos.max (max_reg_expr e) (max_reg_stmnt_expr_list stl))
-  | Vblock e1 e2 => Pos.max (max_reg_expr e1) (max_reg_expr e2)
-  | Vnonblock e1 e2 => Pos.max (max_reg_expr e1) (max_reg_expr e2)
-  end
-with max_reg_stmnt_expr_list (stl: stmnt_expr_list) :=
-  match stl with
-  | Stmntnil => 1
-  | Stmntcons e s stl' =>
-    Pos.max (max_reg_expr e)
-            (Pos.max (max_reg_stmnt s)
-                     (max_reg_stmnt_expr_list stl'))
-  end.
-
-Definition max_list := fold_right Pos.max 1.
-
-Definition max_stmnt_tree t :=
-  PTree.fold (fun i _ st => Pos.max (max_reg_stmnt st) i) t 1.
-
-Definition max_reg_ram r :=
-  match r with
-  | None => 1
-  | Some ram => Pos.max (ram_mem ram)
-                (Pos.max (ram_en ram)
-                 (Pos.max (ram_addr ram)
-                  (Pos.max (ram_addr ram)
-                   (Pos.max (ram_wr_en ram)
-                    (Pos.max (ram_d_in ram)
-                     (Pos.max (ram_d_out ram) (ram_u_en ram)))))))
-  end.
-
-Definition max_reg_module m :=
-  Pos.max (max_list (mod_params m))
-   (Pos.max (max_stmnt_tree (mod_datapath m))
-    (Pos.max (max_stmnt_tree (mod_controllogic m))
-     (Pos.max (mod_st m)
-      (Pos.max (mod_stk m)
-       (Pos.max (mod_finish m)
-        (Pos.max (mod_return m)
-         (Pos.max (mod_start m)
-          (Pos.max (mod_reset 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).
-Proof. induction l; crush; apply IHl; lia. Qed.
-
-Lemma max_fold_lt2 :
-  forall (l: list (positive * stmnt)) v n,
-    v <= n ->
-    v <= fold_left (fun a p => Pos.max (max_reg_stmnt (snd p)) a) l n.
-Proof. induction l; crush; apply IHl; lia. Qed.
-
-Lemma max_fold_lt3 :
-  forall (l: list (positive * stmnt)) v v',
-    v <= v' ->
-    fold_left (fun a0 p => Pos.max (max_reg_stmnt (snd p)) a0) l v
-    <= fold_left (fun a0 p => Pos.max (max_reg_stmnt (snd p)) a0) l v'.
-Proof. induction l; crush; apply IHl; lia. Qed.
-
-Lemma max_fold_lt4 :
-  forall (l: list (positive * stmnt)) (a: positive * stmnt),
-    fold_left (fun a0 p => Pos.max (max_reg_stmnt (snd p)) a0) l 1
-    <= fold_left (fun a0 p => Pos.max (max_reg_stmnt (snd p)) a0) l
-                 (Pos.max (max_reg_stmnt (snd a)) 1).
-Proof. intros; apply max_fold_lt3; lia. Qed.
-
-Lemma max_reg_stmnt_lt_stmnt_tree':
-  forall l (i: positive) v,
-    In (i, v) l ->
-    list_norepet (map fst l) ->
-    max_reg_stmnt v <= fold_left (fun a p => Pos.max (max_reg_stmnt (snd p)) a) l 1.
-Proof.
-  induction l; crush. inv H; inv H0; simplify. apply max_fold_lt2. lia.
-  transitivity (fold_left (fun (a : positive) (p : positive * stmnt) =>
-                             Pos.max (max_reg_stmnt (snd p)) a) l 1).
-  eapply IHl; eauto. apply max_fold_lt4.
-Qed.
-
-Lemma max_reg_stmnt_le_stmnt_tree :
-  forall d i v,
-    d ! i = Some v ->
-    max_reg_stmnt v <= max_stmnt_tree d.
-Proof.
-  intros. unfold max_stmnt_tree. rewrite PTree.fold_spec.
-  apply PTree.elements_correct in H.
-  eapply max_reg_stmnt_lt_stmnt_tree'; eauto.
-  apply PTree.elements_keys_norepet.
-Qed.
-Hint Resolve max_reg_stmnt_le_stmnt_tree : mgen.
-
-Lemma max_reg_stmnt_lt_stmnt_tree :
-  forall d i v,
-    d ! i = Some v ->
-    max_reg_stmnt v < max_stmnt_tree d + 1.
-Proof. intros. apply max_reg_stmnt_le_stmnt_tree in H; lia. Qed.
-Hint Resolve max_reg_stmnt_lt_stmnt_tree : mgen.
-
-Lemma max_stmnt_lt_module :
-  forall m d i,
-    (mod_controllogic m) ! i = Some d \/ (mod_datapath m) ! i = Some d ->
-    max_reg_stmnt d < max_reg_module m + 1.
-Proof.
-  inversion 1 as [ Hv | Hv ]; unfold max_reg_module;
-  apply max_reg_stmnt_le_stmnt_tree in Hv; lia.
-Qed.
-Hint Resolve max_stmnt_lt_module : mgen.
-
 Definition transf_maps state ram in_ (dc: PTree.t stmnt * PTree.t stmnt) :=
   match dc, in_ with
   | (d, c), (i, n) =>
@@ -194,7 +66,9 @@ Definition transf_maps state ram in_ (dc: PTree.t stmnt * PTree.t stmnt) :=
         (PTree.set i nd d, c)
       else dc
     | Some (Vnonblock (Vvar e1) (Vvari r e2)), Some (Vnonblock (Vvar st') e3) =>
-      if (r =? (ram_mem ram)) && (st' =? state) then
+      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 (Vnonblock (Vvar (ram_u_en ram)) (Vunop Vnot (Vvar (ram_u_en ram))))
                  (Vseq (Vnonblock (Vvar (ram_wr_en ram)) (Vlit (ZToValue 0)))
@@ -228,24 +102,6 @@ Proof. Abort.
   apply PTree.elements_complete in H4.
 Abort.*)
 
-Definition set_mod_datapath d c wf m :=
-  mkmodule (mod_params m)
-           d
-           c
-           (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)
-           wf.
-
 Lemma is_wf:
   forall A nc nd,
     @map_well_formed A nc /\ @map_well_formed A nd.
@@ -309,13 +165,14 @@ Lemma ram_wf :
     x + 1 < x + 2 /\ x + 2 < x + 3 /\ x + 3 < x + 4 /\ x + 4 < x + 5 /\ x + 5 < x + 6.
 Proof. lia. Qed.
 
-Definition module_ordering m :=
-  (mod_st m <? mod_finish m) && (mod_finish m <? mod_return m) && (mod_return m <? mod_stk m)
-  && (mod_stk m <? mod_start m) && (mod_start m <? mod_reset m) && (mod_reset m <? mod_clk m)
-  && (max_stmnt_tree (mod_datapath m) <? mod_st m)
-  && (max_stmnt_tree (mod_controllogic m) <? mod_st m).
+Lemma module_ram_wf' :
+  forall m addr,
+    addr = max_reg_module m + 1 ->
+    mod_clk m < addr.
+Proof. unfold max_reg_module; lia. Qed.
 
-Definition transf_module (m: module): module :=
+Definition transf_module (m: module): module.
+  refine (
   let max_reg := max_reg_module m in
   let addr := max_reg+1 in
   let en := max_reg+2 in
@@ -326,10 +183,9 @@ Definition transf_module (m: module): module :=
   let new_size := (mod_stk_len m) in
   let ram := mk_ram new_size (mod_stk m) en u_en addr wr_en d_in d_out ltac:(eauto using ram_wf) in
   match transf_code (mod_st m) ram (mod_datapath m) (mod_controllogic m),
-        mod_ram m,
-        module_ordering m
+        mod_ram m
   with
-  | (nd, nc), None, true =>
+  | (nd, nc), None =>
     mkmodule m.(mod_params)
                  nd
                  nc
@@ -351,9 +207,11 @@ Definition transf_module (m: module): module :=
                        (AssocMap.set m.(mod_stk)
                                  (None, VArray 32 (2 ^ Nat.log2_up new_size))%nat m.(mod_arrdecls))
                  (Some ram)
-                 (is_wf _ nc nd)
-  | _, _, _ => m
-  end.
+                 _ _ _
+  | _, _ => m
+  end). apply is_wf. exact (mod_ordering_wf m).
+  inversion 1; subst. auto using module_ram_wf'.
+Defined.
 
 Definition transf_fundef := transf_fundef transf_module.
 
@@ -1337,7 +1195,6 @@ Hint Resolve max_module_stmnts : mgen.
 Lemma transf_module_code :
   forall m,
     mod_ram m = None ->
-    module_ordering m = true ->
     transf_code (mod_st m)
                 {| ram_size := mod_stk_len m;
                    ram_mem := mod_stk m;
@@ -1354,8 +1211,8 @@ Proof. unfold transf_module; intros; repeat destruct_match; crush. Qed.
 Hint Resolve transf_module_code : mgen.
 
 Lemma transf_module_code_ram :
-  forall m r, mod_ram m = Some r \/ module_ordering m = false -> transf_module m = m.
-Proof. unfold transf_module; intros; destruct H; repeat destruct_match; crush. Qed.
+  forall m r, mod_ram m = Some r -> transf_module m = m.
+Proof. unfold transf_module; intros; repeat destruct_match; crush. Qed.
 Hint Resolve transf_module_code_ram : mgen.
 
 Lemma mod_reset_lt : forall m, mod_reset m < max_reg_module m + 1.
@@ -2447,7 +2304,11 @@ Definition alt_load state ram d (c : AssocMap.t stmnt) d' c' i n :=
     /\ c' ! i = Some (Vnonblock (Vvar state) (Vlit (posToValue n)))
     /\ c' ! n = Some (Vnonblock (Vvar state) ns)
     /\ c ! i = Some (Vnonblock (Vvar state) ns)
-    /\ d ! i = Some (Vnonblock (Vvar e1) (Vvari (ram_mem ram) e2)).
+    /\ d ! i = Some (Vnonblock (Vvar e1) (Vvari (ram_mem ram) e2))
+    /\ e1 < state
+    /\ max_reg_expr e2 < state
+    /\ max_reg_expr ns < state
+    /\ (Z.pos n <= Int.max_unsigned)%Z.
 
 Definition alternatives state ram d c d' c' i n :=
   alt_unchanged d c d' c' i
@@ -2475,6 +2336,7 @@ Proof.
          | |- ( _ # ?s <- _ ) ! ?s = Some _ => apply AssocMap.gss
          | |- ( _ # ?s <- _ ) ! ?r = Some _ => rewrite AssocMap.gso by lia
          | |- _ = None => apply max_index_2; lia
+         | H: context[_ <? _] |- _ => apply Pos.ltb_lt in H
          end; auto.
 Qed.
 
@@ -2837,7 +2699,6 @@ Lemma translation_correct :
     (Z.pos pstval <= 4294967295)%Z ->
     match_states (State sf m st asr asa) (State res' (transf_module m) st asr'0 asa'0) ->
     mod_ram m = None ->
-    module_ordering m = true ->
     exists R2 : state,
       Smallstep.plus step tge (State res' (transf_module m) st asr'0 asa'0) Events.E0 R2 /\
       match_states (State sf m pstval (merge_regs nasr3 basr3) (merge_arrs nasa3 basa3)) R2.
@@ -2858,10 +2719,10 @@ Proof.
   repeat match goal with H: _ \/ _ |- _ => inv H end.
   - unfold alt_unchanged in *; simplify.
     assert (MATCH_SIZE1: match_empty_size m nasa1 /\ match_empty_size m basa1).
-    { eapply match_arrs_size_stmnt_preserved2; eauto. unfold match_empty_size; mgen_crush. }
+    { eapply match_arrs_size_stmnt_preserved2; eauto. unfold match_empty_size; eauto with mgen. }
     assert (MATCH_SIZE2: match_empty_size m nasa2 /\ match_empty_size m basa2).
     { eapply match_arrs_size_stmnt_preserved2; mgen_crush. } simplify.
-    assert (MATCH_ARR3: match_arrs_size nasa2 basa2) by mgen_crush.
+    assert (MATCH_ARR3: match_arrs_size nasa2 basa2) by eauto with mgen.
     exploit match_states_same; try solve [apply H4 | eapply max_stmnt_lt_module; eauto
                                           | econstructor; eauto with mgen];
     intros; repeat inv_exists; simplify; tac0.
@@ -2869,27 +2730,27 @@ Proof.
                                           | econstructor; eauto with mgen];
     intros; repeat inv_exists; simplify; tac0.
     assert (MATCH_SIZE1': match_empty_size m ran'0 /\ match_empty_size m rab'0).
-    { eapply match_arrs_size_stmnt_preserved2; eauto. unfold match_empty_size; mgen_crush.
+    { eapply match_arrs_size_stmnt_preserved2; eauto. unfold match_empty_size; eauto with mgen.
       rewrite empty_stack_transf; eauto with mgen. }
     assert (MATCH_SIZE2': match_empty_size m ran'2 /\ match_empty_size m rab'2).
     { eapply match_arrs_size_stmnt_preserved2; mgen_crush. } simplify.
-    assert (MATCH_ARR3': match_arrs_size ran'2 rab'2) by mgen_crush.
+    assert (MATCH_ARR3': match_arrs_size ran'2 rab'2) by eauto with mgen.
     do 2 econstructor. apply Smallstep.plus_one. econstructor.
-    mgen_crush. mgen_crush. mgen_crush.
-    rewrite <- H13. eassumption. rewrite <- H7. eassumption.
-    eauto. mgen_crush. eauto.
-    rewrite empty_stack_transf. unfold transf_module; repeat destruct_match; crush.
+    eauto with mgen. eauto with mgen. eauto with mgen.
+    rewrite <- H12. eassumption. rewrite <- H7. eassumption.
+    eauto. eauto with mgen. eauto.
+    rewrite empty_stack_transf. unfold transf_module; repeat destruct_match; try discriminate.
     econstructor. simplify.
     unfold disable_ram in *. unfold transf_module in DISABLE_RAM.
-    repeat destruct_match; crush.
-    pose proof H18 as R1. apply max_reg_stmnt_not_modified with (r := max_reg_module m + 2) in R1.
-    pose proof H18 as R2. eapply max_reg_stmnt_not_modified_nb with (r := max_reg_module m + 2) in R2.
-    pose proof H19 as R3. eapply max_reg_stmnt_not_modified with (r := max_reg_module m + 2) in R3.
-    pose proof H19 as R4. eapply max_reg_stmnt_not_modified_nb with (r := max_reg_module m + 2) in R4.
-    pose proof H18 as R1'. apply max_reg_stmnt_not_modified with (r := max_reg_module m + 6) in R1'.
-    pose proof H18 as R2'. eapply max_reg_stmnt_not_modified_nb with (r := max_reg_module m + 6) in R2'.
-    pose proof H19 as R3'. eapply max_reg_stmnt_not_modified with (r := max_reg_module m + 6) in R3'.
-    pose proof H19 as R4'. eapply max_reg_stmnt_not_modified_nb with (r := max_reg_module m + 6) in R4'.
+    repeat destruct_match; try discriminate; []. inv Heqp. simplify.
+    pose proof H17 as R1. apply max_reg_stmnt_not_modified with (r := max_reg_module m + 2) in R1.
+    pose proof H17 as R2. eapply max_reg_stmnt_not_modified_nb with (r := max_reg_module m + 2) in R2.
+    pose proof H18 as R3. eapply max_reg_stmnt_not_modified with (r := max_reg_module m + 2) in R3.
+    pose proof H18 as R4. eapply max_reg_stmnt_not_modified_nb with (r := max_reg_module m + 2) in R4.
+    pose proof H17 as R1'. apply max_reg_stmnt_not_modified with (r := max_reg_module m + 6) in R1'.
+    pose proof H17 as R2'. eapply max_reg_stmnt_not_modified_nb with (r := max_reg_module m + 6) in R2'.
+    pose proof H18 as R3'. eapply max_reg_stmnt_not_modified with (r := max_reg_module m + 6) in R3'.
+    pose proof H18 as R4'. eapply max_reg_stmnt_not_modified_nb with (r := max_reg_module m + 6) in R4'.
     simplify.
     pose proof DISABLE_RAM as DISABLE_RAM1.
     eapply int_eq_not_changed with (ar' := rab') in DISABLE_RAM; try congruence.
@@ -2905,18 +2766,18 @@ Proof.
     eapply max_reg_module_datapath_gt; eauto; remember (max_reg_module m); lia.
     eapply max_reg_module_controllogic_gt; eauto; remember (max_reg_module m); lia.
     eapply max_reg_module_controllogic_gt; eauto; remember (max_reg_module m); lia.
-    auto. auto. mgen_crush. auto.
+    auto. auto. eauto with mgen. auto.
     econstructor; mgen_crush. apply merge_arr_empty; mgen_crush.
     unfold disable_ram in *. unfold transf_module in DISABLE_RAM.
     repeat destruct_match; crush. unfold transf_module in Heqo; repeat destruct_match; crush.
-    pose proof H18 as R1. apply max_reg_stmnt_not_modified with (r := max_reg_module m + 2) in R1.
-    pose proof H18 as R2. eapply max_reg_stmnt_not_modified_nb with (r := max_reg_module m + 2) in R2.
-    pose proof H19 as R3. eapply max_reg_stmnt_not_modified with (r := max_reg_module m + 2) in R3.
-    pose proof H19 as R4. eapply max_reg_stmnt_not_modified_nb with (r := max_reg_module m + 2) in R4.
-    pose proof H18 as R1'. apply max_reg_stmnt_not_modified with (r := max_reg_module m + 6) in R1'.
-    pose proof H18 as R2'. eapply max_reg_stmnt_not_modified_nb with (r := max_reg_module m + 6) in R2'.
-    pose proof H19 as R3'. eapply max_reg_stmnt_not_modified with (r := max_reg_module m + 6) in R3'.
-    pose proof H19 as R4'. eapply max_reg_stmnt_not_modified_nb with (r := max_reg_module m + 6) in R4'.
+    pose proof H17 as R1. apply max_reg_stmnt_not_modified with (r := max_reg_module m + 2) in R1.
+    pose proof H17 as R2. eapply max_reg_stmnt_not_modified_nb with (r := max_reg_module m + 2) in R2.
+    pose proof H18 as R3. eapply max_reg_stmnt_not_modified with (r := max_reg_module m + 2) in R3.
+    pose proof H18 as R4. eapply max_reg_stmnt_not_modified_nb with (r := max_reg_module m + 2) in R4.
+    pose proof H17 as R1'. apply max_reg_stmnt_not_modified with (r := max_reg_module m + 6) in R1'.
+    pose proof H17 as R2'. eapply max_reg_stmnt_not_modified_nb with (r := max_reg_module m + 6) in R2'.
+    pose proof H18 as R3'. eapply max_reg_stmnt_not_modified with (r := max_reg_module m + 6) in R3'.
+    pose proof H18 as R4'. eapply max_reg_stmnt_not_modified_nb with (r := max_reg_module m + 6) in R4'.
     simplify.
     pose proof DISABLE_RAM as DISABLE_RAM1.
     eapply int_eq_not_changed with (ar' := rab') in DISABLE_RAM; try congruence.
@@ -2932,33 +2793,34 @@ Proof.
     eapply max_reg_module_datapath_gt; eauto; remember (max_reg_module m); lia.
     eapply max_reg_module_controllogic_gt; eauto; remember (max_reg_module m); lia.
     eapply max_reg_module_controllogic_gt; eauto; remember (max_reg_module m); lia.
-  - unfold alt_store in *; simplify. inv H6. inv H20. inv H20. simplify.
+  - unfold alt_store in *; simplify. inv H6. inv H19. inv H19. simplify.
     exploit match_states_same; try solve [eapply H4 | eapply max_stmnt_lt_module; eauto
                                           | econstructor; eauto with mgen];
     intros; repeat inv_exists; simplify; tac0.
-    do 2 econstructor. apply Smallstep.plus_one. econstructor. mgen_crush. mgen_crush.
-    mgen_crush. rewrite H7. eassumption. eassumption. eassumption. mgen_crush.
+    do 2 econstructor. apply Smallstep.plus_one. econstructor. solve [eauto with mgen]. solve [eauto with mgen].
+    solve [eauto with mgen].
+    rewrite H7. eassumption. eassumption. eassumption. solve [eauto with mgen].
     econstructor. econstructor. econstructor. econstructor. econstructor.
-    simplify. auto. auto. auto. econstructor. econstructor. econstructor.
+    auto. auto. auto. econstructor. econstructor. econstructor.
     econstructor. econstructor. econstructor. econstructor.
-    simplify. eapply expr_runp_matches2. eassumption. 2: { eassumption. }
+    eapply expr_runp_matches2. eassumption. 2: { eassumption. }
     pose proof H3 as X. apply max_reg_stmnt_le_stmnt_tree in X.
     apply expr_lt_max_module_datapath in X; simplify; remember (max_reg_module m); lia.
     auto.
-    econstructor. econstructor. simplify. eapply expr_runp_matches2; eauto.
+    econstructor. econstructor. eapply expr_runp_matches2; eauto.
     pose proof H3 as X. apply max_reg_stmnt_le_stmnt_tree in X.
     apply expr_lt_max_module_datapath in X.
     remember (max_reg_module m); simplify; lia.
 
-    simplify. rewrite empty_stack_transf.
+    rewrite empty_stack_transf.
     unfold transf_module; repeat destruct_match; try discriminate; simplify; [].
     eapply exec_ram_Some_write.
     3: {
       simplify. unfold merge_regs. repeat rewrite AssocMapExt.merge_add_assoc.
       repeat rewrite find_assocmap_gso by lia.
-      pose proof H13 as X.
+      pose proof H12 as X.
       eapply max_reg_stmnt_not_modified_nb with (r := (max_reg_module m + 2)) in X.
-      simplify. rewrite  AssocMap.gempty in X.
+      rewrite AssocMap.gempty in X.
       apply merge_find_assocmap. auto.
       apply max_reg_stmnt_le_stmnt_tree in H2.
       apply expr_lt_max_module_controllogic in H2. lia.
@@ -2969,19 +2831,19 @@ Proof.
     }
     { unfold disable_ram in *. unfold transf_module in DISABLE_RAM;
                                repeat destruct_match; try discriminate.
-      simplify. inv Heqp.
-      pose proof H13 as X2.
-      pose proof H13 as X4.
+      inv Heqp.
+      pose proof H12 as X2.
+      pose proof H12 as X4.
       apply max_reg_stmnt_not_modified with (r := max_reg_module m + 2) in X2.
-      apply max_reg_stmnt_not_modified with (r := max_reg_module m + 6) in X4. simplify.
+      apply max_reg_stmnt_not_modified with (r := max_reg_module m + 6) in X4.
       assert (forall ar ar' x, ar ! x = ar' ! x -> ar # x = ar' # x).
       { intros. unfold find_assocmap, AssocMapExt.get_default. rewrite H6. auto. }
-      apply H6 in X2. apply H6 in X4. rewrite <- X2. rewrite <- X4.
+      apply H6 in X2. apply H6 in X4. simplify. rewrite <- X2. rewrite <- X4.
       apply int_eq_not. auto.
       apply max_reg_stmnt_le_stmnt_tree in H2.
-      apply expr_lt_max_module_controllogic in H2. remember (max_reg_module m). lia.
+      apply expr_lt_max_module_controllogic in H2. simplify. remember (max_reg_module m). lia.
       apply max_reg_stmnt_le_stmnt_tree in H2.
-      apply expr_lt_max_module_controllogic in H2. remember (max_reg_module m). lia.
+      apply expr_lt_max_module_controllogic in H2. simplify. remember (max_reg_module m). lia.
     }
     2: {
       simplify. unfold merge_regs. repeat rewrite AssocMapExt.merge_add_assoc.
@@ -3003,10 +2865,10 @@ Proof.
     unfold transf_module; repeat destruct_match; try discriminate; simplify.
     replace (AssocMapExt.merge value ran' rab') with (merge_regs ran' rab');
     [|unfold merge_regs; auto].
-    pose proof H20 as X.
+    pose proof H19 as X.
     eapply match_assocmaps_merge in X.
-    2: { apply H22. }
-    inv X. rewrite <- H12. eassumption. unfold transf_module in H6; repeat destruct_match;
+    2: { apply H21. }
+    inv X. rewrite <- H14. eassumption. unfold transf_module in H6; repeat destruct_match;
                                         try discriminate; simplify.
     lia. auto.
 
@@ -3014,7 +2876,7 @@ Proof.
     rewrite AssocMapExt.merge_base_1.
     remember (max_reg_module m).
     repeat (apply match_assocmaps_gt; [lia|]).
-    mgen_crush.
+    solve [eauto with mgen].
 
     apply merge_arr_empty. apply match_empty_size_merge.
     apply match_empty_assocmap_set.
@@ -3023,9 +2885,9 @@ Proof.
     apply match_arrs_merge_set2; auto.
     eapply match_arrs_size_stmnt_preserved in H4; mgen_crush.
     eapply match_arrs_size_stmnt_preserved in H4; mgen_crush.
-    eapply match_arrs_size_stmnt_preserved in H13; mgen_crush.
+    eapply match_arrs_size_stmnt_preserved in H12; mgen_crush.
     rewrite empty_stack_transf. mgen_crush.
-    eapply match_arrs_size_stmnt_preserved in H13; mgen_crush.
+    eapply match_arrs_size_stmnt_preserved in H12; mgen_crush.
     rewrite empty_stack_transf. mgen_crush.
     auto.
     apply merge_arr_empty_match.
@@ -3033,7 +2895,7 @@ Proof.
     eapply match_arrs_size_stmnt_preserved in H4; mgen_crush.
     eapply match_arrs_size_stmnt_preserved in H4; mgen_crush.
     apply match_empty_size_merge. apply match_empty_assocmap_set.
-    mgen_crush. eapply match_arrs_size_stmnt_preserved in H13; mgen_crush.
+    mgen_crush. eapply match_arrs_size_stmnt_preserved in H12; mgen_crush.
     rewrite empty_stack_transf; mgen_crush.
     unfold disable_ram. unfold transf_module; repeat destruct_match; try discriminate; simplify.
     unfold merge_regs. unfold_merge.
@@ -3042,19 +2904,22 @@ Proof.
     repeat rewrite find_assocmap_gso by lia.
     rewrite find_assocmap_gss. apply Int.eq_true.
   - unfold alt_load in *; simplify. inv H6.
-    2: { inv H23. }
-    inv H23. inv H27. simplify. inv H4.
-    2: { inv H24. }
-    inv H24.
+    2: { match goal with H: context[location_is] |- _ => inv H end. }
+    match goal with H: context[location_is] |- _ => inv H end.
+    inv H30. simplify. inv H4.
+    2: { match goal with H: context[location_is] |- _ => inv H end. }
+    inv H27. simplify.
     do 2 econstructor. eapply Smallstep.plus_two.
     econstructor. mgen_crush. mgen_crush. mgen_crush. eassumption.
-    eassumption. econstructor. simplify. econstructor. econstructor. simplify.
-    mgen_crush. econstructor. econstructor. simplify. econstructor. simplify.
+    eassumption. econstructor. simplify. econstructor. econstructor.
+    solve [eauto with mgen]. econstructor. econstructor. econstructor.
     econstructor. econstructor. auto. auto. auto.
-    econstructor. econstructor. simplify. econstructor. simplify.
-    econstructor. econstructor. econstructor. simplify. eapply expr_runp_matches2; eauto.
+    econstructor. econstructor. econstructor.
+    econstructor. econstructor. econstructor. eapply expr_runp_matches2; auto. eassumption.
+    2: { eassumption. }
     pose proof H3 as X. apply max_reg_stmnt_le_stmnt_tree in X.
     apply expr_lt_max_module_datapath in X. simplify. remember (max_reg_module m); lia.
+    auto.
 
     simplify. rewrite empty_stack_transf. unfold transf_module; repeat destruct_match; crush.
     eapply exec_ram_Some_read; simplify.
@@ -3070,7 +2935,7 @@ Proof.
       repeat destruct_match; try discriminate. simplify. apply int_eq_not. auto. }
     { unfold merge_regs; unfold_merge. repeat rewrite AssocMap.gso by lia. apply AssocMap.gss. }
     { unfold merge_regs; unfold_merge. apply AssocMap.gss. }
-    { eapply match_arrs_read. apply H23. mgen_crush. }
+    { eapply match_arrs_read. eassumption. mgen_crush. }
     { crush. }
     { crush. }
     { unfold merge_regs. unfold_merge.
@@ -3080,7 +2945,7 @@ Proof.
       remember (max_reg_module m). repeat rewrite AssocMap.gso by lia.
       apply AssocMap.gss.
     }
-    { assert (Z.pos x <= Int.max_unsigned)%Z by admit; auto. }
+    { auto. }
 
     { econstructor.
       { unfold merge_regs. unfold_merge.
@@ -3088,26 +2953,26 @@ Proof.
         { unfold max_reg_module; lia. }
         unfold transf_module; repeat destruct_match; try discriminate; simplify.
         assert (mod_st m < mod_reset m).
-        { unfold module_ordering in *. simplify.
+        { pose proof (mod_ordering_wf m); unfold module_ordering in *. simplify.
           repeat match goal with
                  | H: context[_ <? _] |- _ => apply Pos.ltb_lt in H
                  end; lia.
         }
         repeat rewrite AssocMap.gso by lia.
-        inv ASSOC. rewrite <- H12. auto. lia.
+        inv ASSOC. rewrite <- H19. auto. lia.
       }
       { unfold merge_regs. unfold_merge.
         assert (mod_finish m < max_reg_module m + 1).
         { unfold max_reg_module; lia. }
         unfold transf_module; repeat destruct_match; try discriminate; simplify.
         assert (mod_st m < mod_finish m).
-        { unfold module_ordering in *. simplify.
+        { pose proof (mod_ordering_wf m). unfold module_ordering in *. simplify.
           repeat match goal with
                  | H: context[_ <? _] |- _ => apply Pos.ltb_lt in H
                  end; lia.
         }
         repeat rewrite AssocMap.gso by lia.
-        inv ASSOC. rewrite <- H12. auto. lia.
+        inv ASSOC. rewrite <- H19. auto. lia.
       }
       { unfold merge_regs. unfold_merge.
         assert (mod_st m < max_reg_module m + 1).
@@ -3340,9 +3205,7 @@ Section CORRECTNESS.
       end.
     induction 1; destruct (mod_ram m) eqn:RAM; simplify; repeat transf_step_correct_assum;
       repeat transf_step_correct_tac.
-    - assert (RAM0: transf_module m = m).
-      { eapply transf_module_code_ram. left. eassumption. }
-      assert (MATCH_SIZE1: match_empty_size m nasa1 /\ match_empty_size m basa1).
+    - assert (MATCH_SIZE1: match_empty_size m nasa1 /\ match_empty_size m basa1).
       { eapply match_arrs_size_stmnt_preserved2; eauto. unfold match_empty_size; mgen_crush. }
       simplify.
       assert (MATCH_SIZE2: match_empty_size m nasa2 /\ match_empty_size m basa2).
@@ -3353,17 +3216,17 @@ Section CORRECTNESS.
       assert (MATCH_ARR3: match_arrs_size nasa3 basa3) by mgen_crush.
       exploit match_states_same. apply H4. eauto with mgen.
       econstructor; eauto. econstructor; eauto. econstructor; eauto. econstructor; eauto.
-      intros. repeat inv_exists. simplify. inv H17. inv H20.
+      intros. repeat inv_exists. simplify. inv H18. inv H21.
       exploit match_states_same. apply H6. eauto with mgen.
-      econstructor; eauto. econstructor; eauto. intros. repeat inv_exists. simplify. inv H17. inv H22.
+      econstructor; eauto. econstructor; eauto. intros. repeat inv_exists. simplify. inv H18. inv H23.
       exploit exec_ram_same; eauto. eauto with mgen.
       econstructor. eapply match_assocmaps_merge; eauto. eauto with mgen.
       econstructor.
       apply match_arrs_merge; eauto with mgen. eauto with mgen.
-      intros. repeat inv_exists. simplify. inv H17. inv H27.
+      intros. repeat inv_exists. simplify. inv H18. inv H28.
       econstructor; simplify. apply Smallstep.plus_one. econstructor.
       mgen_crush. mgen_crush. mgen_crush. rewrite RAM0; eassumption. rewrite RAM0; eassumption.
-      rewrite RAM0. eassumption. mgen_crush. eassumption. rewrite RAM0 in H20. rewrite RAM0.
+      rewrite RAM0. eassumption. mgen_crush. eassumption. rewrite RAM0 in H21. rewrite RAM0.
       rewrite RAM. eassumption. eauto. eauto. eauto with mgen. eauto.
       econstructor. mgen_crush. apply match_arrs_merge; mgen_crush. eauto.
       apply match_empty_size_merge; mgen_crush; mgen_crush.
@@ -3379,16 +3242,14 @@ Section CORRECTNESS.
       apply match_empty_size_merge; mgen_crush; mgen_crush.
       unfold disable_ram.
       unfold transf_module; repeat destruct_match; crush.
-      apply exec_ram_resets_en in H20. unfold merge_reg_assocs in H20.
+      apply exec_ram_resets_en in H21. unfold merge_reg_assocs in H21.
       simplify. auto. auto.
-    - eapply translation_correct; eauto. admit.
+    - eapply translation_correct; eauto.
     - do 2 econstructor. apply Smallstep.plus_one.
       apply step_finish; mgen_crush. constructor; eauto.
     - do 2 econstructor. apply Smallstep.plus_one.
       apply step_finish; mgen_crush. econstructor; eauto.
-    - assert (RAM0: transf_module m = m).
-      { eapply transf_module_code_ram. left. eassumption. }
-      econstructor. econstructor. apply Smallstep.plus_one. econstructor.
+    - econstructor. econstructor. apply Smallstep.plus_one. econstructor.
       replace (mod_entrypoint (transf_module m)) with (mod_entrypoint m) by (rewrite RAM0; auto).
       replace (mod_reset (transf_module m)) with (mod_reset m) by (rewrite RAM0; auto).
       replace (mod_finish (transf_module m)) with (mod_finish m) by (rewrite RAM0; auto).
@@ -3411,12 +3272,10 @@ Section CORRECTNESS.
       unfold find_assocmap, AssocMapExt.get_default. destruct_match.
       rewrite AssocMap.gso in Heqo by admit. rewrite AssocMap.gso in Heqo by admit.
       rewrite AssocMap.gso in Heqo by admit. admit. admit.
-    - assert (RAM0: transf_module m = m).
-      { eapply transf_module_code_ram. left. eassumption. }
-      inv STACKS. destruct b1; subst.
+    - inv STACKS. destruct b1; subst.
       econstructor. econstructor. apply Smallstep.plus_one.
       econstructor. eauto.
-      clear Learn. inv H0. inv H2. inv STACKS. inv H2. constructor.
+      clear Learn. inv H0. inv H3. inv STACKS. inv H3. constructor.
       constructor. intros.
       rewrite RAM0.
       destruct (Pos.eq_dec r res); subst.
@@ -3428,11 +3287,20 @@ Section CORRECTNESS.
       rewrite AssocMap.gss.
       rewrite AssocMap.gss. auto.
       rewrite AssocMap.gso; auto.
-      symmetry. rewrite AssocMap.gso; auto. inv MATCH_ASSOC0. apply H0. auto.
+      symmetry. rewrite AssocMap.gso; auto. inv MATCH_ASSOC0. apply H1. auto.
       auto. auto. auto. auto.
       rewrite RAM0. rewrite RAM. rewrite RAM0 in DISABLE_RAM. rewrite RAM in DISABLE_RAM.
-      apply disable_ram_set_gso.
-      apply disable_ram_set_gso. auto. admit. admit. admit. admit.
+      apply disable_ram_set_gso
+      apply disable_ram_set_gso. auto.
+      pose proof (mod_ordering_wf m); unfold module_ordering in *.
+      pose proof (ram_ordering r0). simplify.
+      pose proof (mod_ram_wf m r0 H). lia.
+      pose proof (mod_ordering_wf m); unfold module_ordering in *.
+      pose proof (ram_ordering r0). simplify.
+      pose proof (mod_ram_wf m r0 H). lia.
+      pose proof (mod_ordering_wf m); unfold module_ordering in *.
+      pose proof (ram_ordering r0). simplify.
+      pose proof (mod_ram_wf m r0 H).
     - inv STACKS. destruct b1; subst.
       econstructor. econstructor. apply Smallstep.plus_one.
       econstructor. eauto.
diff --git a/src/hls/Verilog.v b/src/hls/Verilog.v
index 46a9674..1dc7e99 100644
--- a/src/hls/Verilog.v
+++ b/src/hls/Verilog.v
@@ -821,3 +821,40 @@ Proof.
   - red; simplify; intro; invert H0; invert H; crush.
   - invert H; invert H0; crush.
 Qed.
+
+Local Open Scope positive.
+
+Fixpoint max_reg_expr (e: expr) :=
+  match e with
+  | Vlit _ => 1
+  | Vvar r => r
+  | Vvari r e => Pos.max r (max_reg_expr e)
+  | Vrange r e1 e2 => Pos.max r (Pos.max (max_reg_expr e1) (max_reg_expr e2))
+  | Vinputvar r => r
+  | Vbinop _ e1 e2 => Pos.max (max_reg_expr e1) (max_reg_expr e2)
+  | Vunop _ e => max_reg_expr e
+  | Vternary e1 e2 e3 => Pos.max (max_reg_expr e1) (Pos.max (max_reg_expr e2) (max_reg_expr e3))
+  end.
+
+Fixpoint max_reg_stmnt (st: stmnt) :=
+  match st with
+  | Vskip => 1
+  | Vseq s1 s2 => Pos.max (max_reg_stmnt s1) (max_reg_stmnt s2)
+  | Vcond e s1 s2 =>
+    Pos.max (max_reg_expr e)
+            (Pos.max (max_reg_stmnt s1) (max_reg_stmnt s2))
+  | Vcase e stl None => Pos.max (max_reg_expr e) (max_reg_stmnt_expr_list stl)
+  | Vcase e stl (Some s) =>
+    Pos.max (max_reg_stmnt s)
+            (Pos.max (max_reg_expr e) (max_reg_stmnt_expr_list stl))
+  | Vblock e1 e2 => Pos.max (max_reg_expr e1) (max_reg_expr e2)
+  | Vnonblock e1 e2 => Pos.max (max_reg_expr e1) (max_reg_expr e2)
+  end
+with max_reg_stmnt_expr_list (stl: stmnt_expr_list) :=
+  match stl with
+  | Stmntnil => 1
+  | Stmntcons e s stl' =>
+    Pos.max (max_reg_expr e)
+            (Pos.max (max_reg_stmnt s)
+                     (max_reg_stmnt_expr_list stl'))
+  end.
diff --git a/src/hls/Veriloggenproof.v b/src/hls/Veriloggenproof.v
index ccc0688..b621632 100644
--- a/src/hls/Veriloggenproof.v
+++ b/src/hls/Veriloggenproof.v
@@ -421,8 +421,8 @@ Section CORRECTNESS.
       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.
+      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.
@@ -468,7 +468,8 @@ Section CORRECTNESS.
       econstructor. econstructor.
 
       eapply transl_list_correct.
-      intros. split. lia. pose proof (HTL.mod_wf m) as HP. destruct HP as [_ HP]. auto.
+      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 _].