Merge branch 'oopsla21' into sharing-merge

18 files changed, 3927 insertions, 1405 deletions

diff --git a/src/hls/AssocMap.v b/src/hls/AssocMap.v
index d408b1f..7b9ef9f 100644
--- a/src/hls/AssocMap.v
+++ b/src/hls/AssocMap.v
@@ -98,6 +98,17 @@ Module AssocMapExt.
     Qed.
     Hint Resolve merge_correct_2 : assocmap.
 
+    Lemma merge_correct_3 :
+      forall am bm k,
+      get k am = None ->
+      get k bm = None ->
+      get k (merge am bm) = None.
+    Proof.
+      induction am; intros; destruct k; destruct bm; try (destruct o); simpl;
+        try rewrite gempty in H; try discriminate; try assumption; auto.
+    Qed.
+    Hint Resolve merge_correct_3 : assocmap.
+
     Definition merge_fold (am bm : t A) : t A :=
       fold_right (fun p a => set (fst p) (snd p) a) bm (elements am).
 
diff --git a/src/hls/FunctionalUnits.v b/src/hls/FunctionalUnits.v
index 019cf15..e4d51b3 100644
--- a/src/hls/FunctionalUnits.v
+++ b/src/hls/FunctionalUnits.v
@@ -23,19 +23,22 @@ Require Import vericert.common.Vericertlib.
 
 Inductive funct_unit: Type :=
 | SignedDiv (size: positive) (numer denom quot rem: reg): funct_unit
-| UnsignedDiv (size: positive) (numer denom quot rem: reg): funct_unit.
+| UnsignedDiv (size: positive) (numer denom quot rem: reg): funct_unit
+| Ram (size: positive) (addr d_in d_out wr_en: reg): funct_unit.
 
 Record funct_units := mk_avail_funct_units {
     avail_sdiv: option positive;
     avail_udiv: option positive;
+    avail_ram: option positive;
     avail_units: PTree.t funct_unit;
   }.
 
 Definition initial_funct_units :=
-  mk_avail_funct_units None None (PTree.empty funct_unit).
+  mk_avail_funct_units None None None (PTree.empty funct_unit).
 
 Definition funct_unit_stages (f: funct_unit) : positive :=
   match f with
   | SignedDiv s _ _ _ _ => s
   | UnsignedDiv s _ _ _ _ => s
+  | _ => 1
   end.
diff --git a/src/hls/HTL.v b/src/hls/HTL.v
index d777d66..886f86d 100644
--- a/src/hls/HTL.v
+++ b/src/hls/HTL.v
@@ -18,12 +18,13 @@
  *)
 
 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 compcert.lib.Integers.
+Require Import compcert.lib.Integers.
 Require Import compcert.lib.Maps.
 
 Require Import vericert.common.Vericertlib.
@@ -33,6 +34,8 @@ Require Import vericert.hls.Array.
 Require Import vericert.common.Maps.
 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
@@ -53,7 +56,25 @@ Definition controllogic := PTree.t control_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;
+  ram_mem: reg;
+  ram_en: reg;
+  ram_u_en: reg;
+  ram_addr: reg;
+  ram_wr_en: reg;
+  ram_d_in: reg;
+  ram_d_out: reg;
+  ram_ordering: (ram_addr < ram_en
+                 /\ ram_en < ram_d_in
+                 /\ ram_d_in < ram_d_out
+                 /\ ram_d_out < ram_wr_en
+                 /\ 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.
 
 Inductive controlsignal : Type :=
   | ctrl_finish : controlsignal
@@ -90,6 +111,11 @@ Record module: Type :=
         These will be mapped to the same verilog register. *)
     mod_externctrl : AssocMap.t (ident * controlsignal);
     mod_wf : (map_well_formed mod_controllogic /\ map_well_formed mod_datapath);
+    mod_ram : option ram;
+    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';
+    mod_params_wf : Forall (Pos.gt mod_st) mod_params;
   }.
 
 Definition fundef := AST.fundef module.
@@ -161,12 +187,47 @@ Inductive state : Type :=
            (m : module)
            (args : list value), state.
 
+Inductive exec_ram:
+  Verilog.reg_associations -> Verilog.arr_associations -> option ram ->
+  Verilog.reg_associations -> Verilog.arr_associations -> Prop :=
+| exec_ram_Some_idle:
+    forall ra ar r,
+      Int.eq (Verilog.assoc_blocking ra)#(ram_en r, 32)
+             (Verilog.assoc_blocking ra)#(ram_u_en r, 32) = true ->
+      exec_ram ra ar (Some r) ra ar
+| exec_ram_Some_write:
+    forall ra ar r d_in addr en wr_en u_en,
+      Int.eq en u_en = false ->
+      Int.eq wr_en (ZToValue 0) = false ->
+      (Verilog.assoc_blocking ra)#(ram_en r, 32) = en ->
+      (Verilog.assoc_blocking ra)!(ram_u_en r) = Some u_en ->
+      (Verilog.assoc_blocking ra)!(ram_wr_en r) = Some wr_en ->
+      (Verilog.assoc_blocking ra)!(ram_d_in r) = Some d_in ->
+      (Verilog.assoc_blocking ra)!(ram_addr r) = Some addr ->
+      exec_ram ra ar (Some r) (Verilog.nonblock_reg (ram_en r) ra u_en)
+               (Verilog.nonblock_arr (ram_mem r) (valueToNat addr) ar d_in)
+| exec_ram_Some_read:
+    forall ra ar r addr v_d_out en u_en,
+      Int.eq en u_en = false ->
+      (Verilog.assoc_blocking ra)#(ram_en r, 32) = en ->
+      (Verilog.assoc_blocking ra)!(ram_u_en r) = Some u_en ->
+      (Verilog.assoc_blocking ra)!(ram_wr_en r) = Some (ZToValue 0) ->
+      (Verilog.assoc_blocking ra)!(ram_addr r) = Some addr ->
+      Verilog.arr_assocmap_lookup (Verilog.assoc_blocking ar)
+                                  (ram_mem r) (valueToNat addr) = Some v_d_out ->
+      exec_ram ra ar (Some r) (Verilog.nonblock_reg (ram_en r)
+                               (Verilog.nonblock_reg (ram_d_out r) ra v_d_out) u_en) ar
+| exec_ram_None:
+    forall r a,
+      exec_ram r a None r a.
+
 Inductive step : genv -> state -> Events.trace -> state -> Prop :=
 | step_module :
     forall g mid m st sf ctrl_stmnt data_stmnt
       asr asa
       basr1 basa1 nasr1 nasa1
       basr2 basa2 nasr2 nasa2
+      basr3 basa3 nasr3 nasa3
       asr' asa'
       f pstval,
       asr!(mod_reset m) = Some (ZToValue 0) ->
@@ -187,8 +248,14 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop :=
         data_stmnt
         (Verilog.mkassociations basr2 nasr2)
         (Verilog.mkassociations basa2 nasa2) ->
-      asr' = Verilog.merge_regs nasr2 basr2 ->
-      asa' = Verilog.merge_arrs nasa2 basa2 ->
+      exec_ram
+        (Verilog.mkassociations (Verilog.merge_regs nasr2 basr2) empty_assocmap)
+        (Verilog.mkassociations (Verilog.merge_arrs nasa2 basa2) (empty_stack m))
+        (mod_ram m)
+        (Verilog.mkassociations basr3 nasr3)
+        (Verilog.mkassociations basa3 nasa3) ->
+      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 ->
       step g
@@ -263,3 +330,110 @@ 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.
+
+Lemma max_list_correct l st : st > max_list l -> Forall (Pos.gt st) l.
+Proof. induction l; crush; constructor; [|apply IHl]; lia. Qed.
+
+Definition max_list_dec (l: list reg) (st: reg) : {Forall (Pos.gt st) l} + {True}.
+  refine (
+      match bool_dec (max_list l <? st) true with
+      | left _ => left _
+      | _ => _
+      end
+    ); auto.
+  apply max_list_correct. apply Pos.ltb_lt in e. lia.
+Qed.
diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v
index 2cfcba4..d292722 100644
--- a/src/hls/HTLPargen.v
+++ b/src/hls/HTLPargen.v
@@ -641,9 +641,9 @@ Definition add_control_instr_force_state_incr :
        s.(st_arrdecls)
        s.(st_datapath)
        (AssocMap.set n st s.(st_controllogic))).
-Admitted.
+Abort.
 
-Definition add_control_instr_force (n : node) (st : stmnt) : mon unit :=
+(*Definition add_control_instr_force (n : node) (st : stmnt) : mon unit :=
   fun s =>
     OK tt (mkstate
       s.(st_st)
@@ -707,7 +707,7 @@ Lemma create_new_state_state_incr:
        s.(st_arrdecls)
        s.(st_datapath)
        s.(st_controllogic)).
-Admitted.
+Abort.
 
 Definition create_new_state (p: node): mon node :=
   fun s => OK s.(st_freshstate)
@@ -757,7 +757,7 @@ Fixpoint translate_cfi' (fin rtrn stack preg: reg) (cfi: cf_instr)
     ret ((Vcond (pred_expr preg p) tc1s tc2s), (Vcond (pred_expr preg p) tc1c tc2c))
   | RBjumptable r tbl =>
     do s <- get;
-    ret (Vskip, Vcase (Vvar r) (tbl_to_case_expr s.(st_st) tbl) (Some Vskip))
+    ret (Vskip, Vcase (Vvar r) (list_to_stmnt (tbl_to_case_expr s.(st_st) tbl)) (Some Vskip))
   | RBcall sig ri rl r n =>
     error (Errors.msg "HTLPargen: RPcall not supported.")
   | RBtailcall sig ri lr =>
@@ -785,7 +785,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;
@@ -800,9 +812,14 @@ Definition transf_module (f: function) : mon HTL.module :=
     do rst <- create_reg (Some Vinput) 1;
     do clk <- create_reg (Some Vinput) 1;
     do current_state <- get;
-    match zle (Z.pos (max_pc_map current_state.(st_datapath))) Integers.Int.max_unsigned,
-          zle (Z.pos (max_pc_map current_state.(st_controllogic))) Integers.Int.max_unsigned with
-    | left LEDATA, left LECTRL =>
+    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,
+          decide_order (st_st current_state) fin rtrn stack start rst clk,
+          max_list_dec (fn_params f) (st_st current_state)
+    with
+    | left LEDATA, left LECTRL, left MORD, left WFPARAMS =>
         ret (HTL.mkmodule
            f.(fn_params)
            current_state.(st_datapath)
@@ -818,11 +835,15 @@ Definition transf_module (f: function) : mon HTL.module :=
            clk
            current_state.(st_scldecls)
            current_state.(st_arrdecls)
-           (AssocMap.empty (ident * controlsignal))
-           (conj (max_pc_wf _ _ LECTRL) (max_pc_wf _ _ LEDATA)))
-    | _, _ => error (Errors.msg "More than 2^32 states.")
+           None
+           (conj (max_pc_wf _ LECTRL) (max_pc_wf _ LEDATA))
+           MORD
+           _
+           WFPARAMS)
+    | _, _, _, _ => 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
@@ -854,3 +875,4 @@ Definition transl_program (p : RTLBlockInstr.program) : Errors.res HTL.program :
   if main_is_internal p
   then transform_partial_program transl_fundef p
   else Errors.Error (Errors.msg "Main function is not Internal.").
+*)
diff --git a/src/hls/HTLgen.v b/src/hls/HTLgen.v
index 3b4b934..0b7f3ec 100644
--- a/src/hls/HTLgen.v
+++ b/src/hls/HTLgen.v
@@ -600,7 +600,45 @@ Definition stack_correct (sz : Z) : bool :=
 
 Definition declare_params params := collectlist (fun r => declare_reg (Some Vinput) r 32) params.
 
-Definition transf_module (ge : RTL.genv) (main : ident) (f: function) : mon HTL.module :=
+Lemma max_pc_map_sound:
+  forall m pc i, m!pc = Some i -> Ple pc (max_pc_map m).
+Proof.
+  intros until i. unfold max_pc_function.
+  apply PTree_Properties.fold_rec with (P := fun c m => c!pc = Some i -> Ple pc m).
+  (* extensionality *)
+  intros. apply H0. rewrite H; auto.
+  (* base case *)
+  rewrite PTree.gempty. congruence.
+  (* inductive case *)
+  intros. rewrite PTree.gsspec in H2. destruct (peq pc k).
+  inv H2. unfold Ple; lia.
+  apply Ple_trans with a. auto. unfold Ple; lia.
+Qed.
+
+Lemma max_pc_wf :
+  forall m, Z.pos (max_pc_map m) <= Integers.Int.max_unsigned ->
+            map_well_formed m.
+Proof.
+  unfold map_well_formed. intros.
+  exploit list_in_map_inv. eassumption. intros [x [A B]]. destruct x.
+  apply Maps.PTree.elements_complete in B. apply max_pc_map_sound in B.
+  unfold Ple in B. apply Pos2Z.pos_le_pos in B. subst.
+  simplify. transitivity (Z.pos (max_pc_map m)); eauto.
+Qed.
+
+Definition 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 _ <- declare_params (RTL.fn_params f);
     do fin <- create_reg (Some Voutput) 1;
@@ -612,8 +650,11 @@ Definition transf_module (ge : RTL.genv) (main : ident) (f: function) : mon HTL.
     do _ <- collectlist (transf_instr ge fin rtrn stack) (Maps.PTree.elements f.(RTL.fn_code));
     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,
+          max_list_dec (RTL.fn_params f) (st_st current_state)
+    with
+    | left LEDATA, left LECTRL, left MORD, left WFPARAMS =>
         ret (HTL.mkmodule
            f.(RTL.fn_params)
            current_state.(st_datapath)
@@ -630,16 +671,21 @@ Definition transf_module (ge : RTL.genv) (main : ident) (f: function) : mon HTL.
            current_state.(st_scldecls)
            current_state.(st_arrdecls)
            current_state.(st_externctrl)
-           (conj (max_pc_wf _ _ LECTRL) (max_pc_wf _ _ LEDATA)))
-    | _, _ => error (Errors.msg "More than 2^32 states.")
+           None
+           (conj (max_pc_wf _ LECTRL) (max_pc_wf _ LEDATA))
+           MORD
+           _
+           WFPARAMS)
+    | _, _, _, _ => 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_externctrl (init_state st))
@@ -660,23 +706,6 @@ Definition transl_module (prog : RTL.program) (f : function) : Errors.res HTL.mo
 
 Definition transl_fundef prog := transf_partial_fundef (transl_module prog).
 
-(* 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/HTLgenproof.v b/src/hls/HTLgenproof.v
index c1298c1..c2cbbf8 100644
--- a/src/hls/HTLgenproof.v
+++ b/src/hls/HTLgenproof.v
@@ -1,4 +1,4 @@
- (*
+(*
  * Vericert: Verified high-level synthesis.
  * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com>
  *               2020 James Pollard <j@mes.dev>
@@ -1131,6 +1131,7 @@ Section CORRECTNESS.
 
   Ltac tac0 :=
     match goal with
+    | [ |- HTL.exec_ram _ _ _ _ _ ] => constructor
     | [ |- context[Verilog.merge_arrs _ _] ] => unfold Verilog.merge_arrs
     | [ |- context[Verilog.merge_arr] ] => unfold Verilog.merge_arr
     | [ |- context[Verilog.merge_regs _ _] ] => unfold Verilog.merge_regs; crush; unfold_merge
@@ -2248,7 +2249,7 @@ Section CORRECTNESS.
       econstructor. econstructor. econstructor. econstructor.
       econstructor. econstructor. econstructor. econstructor.
 
-      all: crush.
+      all: try constructor; crush.
 
       (** State Lookup *)
       unfold Verilog.merge_regs.
@@ -2284,11 +2285,21 @@ Section CORRECTNESS.
       crush.
       unfold Verilog.merge_arrs.
 
-      rewrite AssocMap.gcombine.
-      2: { reflexivity. }
+      rewrite AssocMap.gcombine by reflexivity.
+      rewrite AssocMap.gss.
+      erewrite Verilog.merge_arr_empty2.
       unfold Verilog.arr_assocmap_set.
+      rewrite AssocMap.gcombine by reflexivity.
+      rewrite AssocMap.gss.
       rewrite AssocMap.gss.
       unfold Verilog.merge_arr.
+      setoid_rewrite H7.
+      reflexivity.
+
+      rewrite AssocMap.gcombine by reflexivity.
+      unfold Verilog.merge_arr.
+      unfold Verilog.arr_assocmap_set.
+      rewrite AssocMap.gss.
       rewrite AssocMap.gss.
       setoid_rewrite H7.
       reflexivity.
@@ -2296,12 +2307,23 @@ Section CORRECTNESS.
       rewrite combine_length.
       rewrite <- array_set_len.
       unfold arr_repeat. crush.
+      symmetry.
       apply list_repeat_len.
 
       rewrite <- array_set_len.
       unfold arr_repeat. crush.
-      rewrite list_repeat_len.
-      rewrite H4. reflexivity.
+      rewrite H4.
+      apply list_repeat_len.
+
+      rewrite combine_length.
+      rewrite <- array_set_len.
+      unfold arr_repeat. crush.
+      apply list_repeat_len.
+
+      rewrite <- array_set_len.
+      unfold arr_repeat. crush.
+      rewrite H4.
+      apply list_repeat_len.
 
       remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ asr # r0))
                                     (Integers.Ptrofs.of_int (Integers.Int.repr z))) as OFFSET.
@@ -2530,7 +2552,7 @@ Section CORRECTNESS.
       econstructor. econstructor. econstructor. econstructor.
       econstructor. econstructor. econstructor. econstructor.
 
-      all: crush.
+      all: try constructor; crush.
 
       (** State Lookup *)
       unfold Verilog.merge_regs.
@@ -2565,11 +2587,21 @@ Section CORRECTNESS.
       crush.
       unfold Verilog.merge_arrs.
 
-      rewrite AssocMap.gcombine.
-      2: { reflexivity. }
+      rewrite AssocMap.gcombine by reflexivity.
+      rewrite AssocMap.gss.
+      erewrite Verilog.merge_arr_empty2.
       unfold Verilog.arr_assocmap_set.
+      rewrite AssocMap.gcombine by reflexivity.
+      rewrite AssocMap.gss.
       rewrite AssocMap.gss.
       unfold Verilog.merge_arr.
+      setoid_rewrite H7.
+      reflexivity.
+
+      rewrite AssocMap.gcombine by reflexivity.
+      unfold Verilog.merge_arr.
+      unfold Verilog.arr_assocmap_set.
+      rewrite AssocMap.gss.
       rewrite AssocMap.gss.
       setoid_rewrite H7.
       reflexivity.
@@ -2577,12 +2609,23 @@ Section CORRECTNESS.
       rewrite combine_length.
       rewrite <- array_set_len.
       unfold arr_repeat. crush.
+      symmetry.
+      apply list_repeat_len.
+
+      rewrite <- array_set_len.
+      unfold arr_repeat. crush.
+      rewrite H4.
+      apply list_repeat_len.
+
+      rewrite combine_length.
+      rewrite <- array_set_len.
+      unfold arr_repeat. crush.
       apply list_repeat_len.
 
       rewrite <- array_set_len.
       unfold arr_repeat. crush.
-      rewrite list_repeat_len.
-      rewrite H4. reflexivity.
+      rewrite H4.
+      apply list_repeat_len.
 
       remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ asr # r0))
                                     (Integers.Ptrofs.of_int
@@ -2780,7 +2823,7 @@ Section CORRECTNESS.
       eapply Verilog.stmnt_runp_Vnonblock_arr. crush.
       econstructor. econstructor. econstructor. econstructor.
 
-      all: crush.
+      all: try constructor; crush.
 
       (** State Lookup *)
       unfold Verilog.merge_regs.
@@ -2817,11 +2860,21 @@ Section CORRECTNESS.
       crush.
       unfold Verilog.merge_arrs.
 
-      rewrite AssocMap.gcombine.
-      2: { reflexivity. }
+      rewrite AssocMap.gcombine by reflexivity.
+      rewrite AssocMap.gss.
+      erewrite Verilog.merge_arr_empty2.
       unfold Verilog.arr_assocmap_set.
+      rewrite AssocMap.gcombine by reflexivity.
+      rewrite AssocMap.gss.
       rewrite AssocMap.gss.
       unfold Verilog.merge_arr.
+      setoid_rewrite H7.
+      reflexivity.
+
+      rewrite AssocMap.gcombine by reflexivity.
+      unfold Verilog.merge_arr.
+      unfold Verilog.arr_assocmap_set.
+      rewrite AssocMap.gss.
       rewrite AssocMap.gss.
       setoid_rewrite H7.
       reflexivity.
@@ -2829,12 +2882,23 @@ Section CORRECTNESS.
       rewrite combine_length.
       rewrite <- array_set_len.
       unfold arr_repeat. crush.
+      symmetry.
       apply list_repeat_len.
 
       rewrite <- array_set_len.
       unfold arr_repeat. crush.
-      rewrite list_repeat_len.
-      rewrite H4. reflexivity.
+      rewrite H4.
+      apply list_repeat_len.
+
+      rewrite combine_length.
+      rewrite <- array_set_len.
+      unfold arr_repeat. crush.
+      apply list_repeat_len.
+
+      rewrite <- array_set_len.
+      unfold arr_repeat. crush.
+      rewrite H4.
+      apply list_repeat_len.
 
       remember i as OFFSET.
       destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET).
@@ -3014,7 +3078,7 @@ Section CORRECTNESS.
       eapply eval_cond_correct; eauto. intros.
       intros. eapply RTL.max_reg_function_use. eauto. auto.
       econstructor. auto.
-      simpl. econstructor. unfold Verilog.merge_regs. unfold_merge. simpl.
+      simpl. econstructor. constructor. unfold Verilog.merge_regs. unfold_merge. simpl.
       apply AssocMap.gss.
 
       inv MARR. inv CONST.
@@ -3034,7 +3098,7 @@ Section CORRECTNESS.
       eapply eval_cond_correct; eauto. intros.
       intros. eapply RTL.max_reg_function_use. eauto. auto.
       econstructor. auto.
-      simpl. econstructor. unfold Verilog.merge_regs. unfold_merge. simpl.
+      simpl. econstructor. constructor. unfold Verilog.merge_regs. unfold_merge. simpl.
       apply AssocMap.gss.
 
       inv MARR. inv CONST.
diff --git a/src/hls/Memorygen.v b/src/hls/Memorygen.v
new file mode 100644
index 0000000..1dd6603
--- /dev/null
+++ b/src/hls/Memorygen.v
@@ -0,0 +1,3203 @@
+(*
+ * Vericert: Verified high-level synthesis.
+ * Copyright (C) 2021 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.micromega.Lia.
+
+Require Import compcert.backend.Registers.
+Require Import compcert.common.AST.
+Require Import compcert.common.Globalenvs.
+Require compcert.common.Memory.
+Require Import compcert.common.Values.
+Require Import compcert.lib.Floats.
+Require Import compcert.lib.Integers.
+Require Import compcert.lib.Maps.
+Require compcert.common.Smallstep.
+Require compcert.verilog.Op.
+
+Require Import vericert.common.Vericertlib.
+Require Import vericert.hls.ValueInt.
+Require Import vericert.hls.Verilog.
+Require Import vericert.hls.HTL.
+Require Import vericert.hls.AssocMap.
+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.
+  rewrite Int.unsigned_not.
+  replace Int.max_unsigned with 4294967295%Z by crush.
+  assert (X: forall x, (x <> 4294967295 - x)%Z) by lia.
+  specialize (X (Int.unsigned x)). apply zeq_false; auto.
+Qed.
+
+Definition transf_maps state ram in_ (dc: PTree.t stmnt * PTree.t stmnt) :=
+  match dc, in_ with
+  | (d, c), (i, n) =>
+    match PTree.get i d, PTree.get i c with
+    | Some (Vnonblock (Vvari r e1) e2), Some c_s =>
+      if r =? (ram_mem ram) 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 1)))
+                             (Vseq (Vnonblock (Vvar (ram_d_in ram)) e2)
+                                   (Vnonblock (Vvar (ram_addr ram)) e1)))
+        in
+        (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) && (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)))
+                       (Vnonblock (Vvar (ram_addr ram)) e2))
+        in
+        let aout := Vnonblock (Vvar e1) (Vvar (ram_d_out ram)) in
+        let redirect := Vnonblock (Vvar state) (Vlit (posToValue n)) in
+        (PTree.set i nd (PTree.set n aout d),
+         PTree.set i redirect (PTree.set n (Vnonblock (Vvar st') e3) c))
+      else dc
+    | _, _ => dc
+    end
+  end.
+
+Lemma transf_maps_wf :
+  forall state ram d c d' c' i,
+    map_well_formed c /\ map_well_formed d ->
+    transf_maps state ram i (d, c) = (d', c') ->
+    map_well_formed c' /\ map_well_formed d'.
+Proof.
+  unfold transf_maps; intros; repeat destruct_match;
+  match goal with
+  | H: (_, _) = (_, _) |- _ => inv H
+  end; auto.
+  unfold map_well_formed.
+  simplify; intros.
+  destruct (Pos.eq_dec p0 p1); subst; auto.
+  destruct (Pos.eq_dec p p1); subst. unfold map_well_formed in *.
+  apply AssocMap.elements_correct in Heqo.
+  eapply in_map with (f := fst) in Heqo. simplify.
+  apply H1 in Heqo. auto.
+  apply AssocMapExt.elements_iff in H3. inv H3.
+  repeat rewrite AssocMap.gso in H8 by lia.
+  apply AssocMap.elements_correct in H8.
+  eapply in_map with (f := fst) in H8. simplify.
+  unfold map_well_formed in *. apply H0 in H8. auto.
+  apply AssocMapExt.elements_iff in H3. inv H3.
+  destruct (Pos.eq_dec p0 p1); subst; auto.
+  destruct (Pos.eq_dec p p1); subst. unfold map_well_formed in *.
+  apply AssocMap.elements_correct in Heqo.
+  eapply in_map with (f := fst) in Heqo. simplify.
+  apply H1 in Heqo. auto.
+  repeat rewrite AssocMap.gso in H8 by lia.
+  apply AssocMap.elements_correct in H8.
+  eapply in_map with (f := fst) in H8. simplify.
+  unfold map_well_formed in *. apply H1 in H8. auto.
+  unfold map_well_formed in *; simplify; intros.
+  destruct (Pos.eq_dec p0 p1); subst; auto.
+  destruct (Pos.eq_dec p p1); subst. unfold map_well_formed in *.
+  apply AssocMap.elements_correct in Heqo.
+  eapply in_map with (f := fst) in Heqo. simplify.
+  apply H1 in Heqo. auto.
+  apply AssocMapExt.elements_iff in H. inv H.
+  repeat rewrite AssocMap.gso in H2 by lia.
+  apply AssocMap.elements_correct in H2.
+  eapply in_map with (f := fst) in H2. simplify.
+  unfold map_well_formed in *. apply H1 in H2. auto.
+Qed.
+
+Definition max_pc {A: Type} (m: PTree.t A) :=
+  fold_right Pos.max 1%positive (map fst (PTree.elements m)).
+
+Fixpoint zip_range {A: Type} n (l: list A) {struct l} :=
+  match l with
+  | nil => nil
+  | a :: b => (a, n) :: zip_range (n+1) b
+  end.
+
+Lemma zip_range_fst_idem : forall A (l: list A) a, map fst (zip_range a l) = l.
+Proof. induction l; crush. Qed.
+
+Lemma zip_range_not_in_snd :
+  forall A (l: list A) a n, a < n -> ~ In a (map snd (zip_range n l)).
+Proof.
+  unfold not; induction l; crush.
+  inv H0; try lia. eapply IHl.
+  assert (X: a0 < n + 1) by lia. apply X; auto. auto.
+Qed.
+
+Lemma zip_range_snd_no_repet :
+  forall A (l: list A) a, list_norepet (map snd (zip_range a l)).
+Proof.
+  induction l; crush; constructor; auto; [].
+  apply zip_range_not_in_snd; lia.
+Qed.
+
+Lemma zip_range_in :
+  forall A (l: list A) a n i, In (a, i) (zip_range n l) -> In a l.
+Proof.
+  induction l; crush. inv H. inv H0. auto. right. eapply IHl; eauto.
+Qed.
+
+Lemma zip_range_not_in :
+  forall A (l: list A) a i n, ~ In a l -> ~ In (a, i) (zip_range n l).
+Proof.
+  unfold not; induction l; crush. inv H0. inv H1. apply H. left. auto.
+  apply H. right. eapply zip_range_in; eauto.
+Qed.
+
+Lemma zip_range_no_repet :
+  forall A (l: list A) a, list_norepet l -> list_norepet (zip_range a l).
+Proof.
+  induction l; simplify; constructor;
+  match goal with H: list_norepet _ |- _ => inv H end;
+  [apply zip_range_not_in|]; auto.
+Qed.
+
+Definition transf_code state ram d c :=
+  fold_right (transf_maps state ram) (d, c)
+             (zip_range (Pos.max (max_pc c) (max_pc d) + 1)
+                        (map fst (PTree.elements d))).
+
+Lemma transf_code_wf' :
+  forall l c d state ram c' d',
+    map_well_formed c /\ map_well_formed d ->
+    fold_right (transf_maps state ram) (d, c) l = (d', c') ->
+    map_well_formed c' /\ map_well_formed d'.
+Proof.
+  induction l; intros; simpl in *. inv H0; auto.
+  remember (fold_right (transf_maps state ram) (d, c) l). destruct p.
+  apply transf_maps_wf in H0. auto. eapply IHl; eauto.
+Qed.
+
+Lemma transf_code_wf :
+  forall c d state ram c' d',
+    map_well_formed c /\ map_well_formed d ->
+    transf_code state ram d c = (d', c') ->
+    map_well_formed c' /\ map_well_formed d'.
+Proof. eauto using transf_code_wf'. Qed.
+
+Lemma ram_wf :
+  forall x,
+    x + 1 < x + 2 /\ x + 2 < x + 3 /\ x + 3 < x + 4 /\ x + 4 < x + 5 /\ x + 5 < x + 6.
+Proof. lia. Qed.
+
+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.
+  refine (
+  let max_reg := max_reg_module m in
+  let addr := max_reg+1 in
+  let en := max_reg+2 in
+  let d_in := max_reg+3 in
+  let d_out := max_reg+4 in
+  let wr_en := max_reg+5 in
+  let u_en := max_reg+6 in
+  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
+  let tc := transf_code (mod_st m) ram (mod_datapath m) (mod_controllogic m) in
+  match mod_ram m with
+  | None =>
+    mkmodule m.(mod_params)
+                 (fst tc)
+                 (snd tc)
+                 (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)
+                 (AssocMap.set u_en (None, VScalar 1)
+                  (AssocMap.set en (None, VScalar 1)
+                   (AssocMap.set wr_en (None, VScalar 1)
+                    (AssocMap.set d_out (None, VScalar 32)
+                     (AssocMap.set d_in (None, VScalar 32)
+                      (AssocMap.set addr (None, VScalar 32) m.(mod_scldecls)))))))
+                       (AssocMap.set m.(mod_stk)
+                                 (None, VArray 32 (2 ^ Nat.log2_up new_size))%nat m.(mod_arrdecls))
+                 (Some ram)
+                 _ (mod_ordering_wf m) _ (mod_params_wf m)
+  | _ => m
+  end).
+  eapply transf_code_wf. apply (mod_wf m). destruct tc eqn:?; simpl.
+  rewrite <- Heqp. intuition.
+  inversion 1; subst. auto using module_ram_wf'.
+Defined.
+
+Definition transf_fundef := transf_fundef transf_module.
+
+Definition transf_program (p : program) :=
+  transform_program transf_fundef p.
+
+Inductive match_assocmaps : positive -> assocmap -> assocmap -> Prop :=
+  match_assocmap: forall p rs rs',
+    (forall r, r < p -> rs!r = rs'!r) ->
+    match_assocmaps p rs rs'.
+
+Inductive match_arrs : assocmap_arr -> assocmap_arr -> Prop :=
+| match_assocmap_arr_intro: forall ar ar',
+    (forall s arr,
+        ar ! s = Some arr ->
+        exists arr',
+          ar' ! s = Some arr'
+          /\ (forall addr,
+                 array_get_error addr arr = array_get_error addr arr')
+          /\ arr_length arr = arr_length arr')%nat ->
+    (forall s, ar ! s = None -> ar' ! s = None) ->
+    match_arrs ar ar'.
+
+Inductive match_arrs_size : assocmap_arr -> assocmap_arr -> Prop :=
+  match_arrs_size_intro :
+    forall nasa basa,
+      (forall s arr,
+          nasa ! s = Some arr ->
+          exists arr',
+            basa ! s = Some arr' /\ arr_length arr = arr_length arr') ->
+      (forall s arr,
+          basa ! s = Some arr ->
+          exists arr',
+            nasa ! s = Some arr' /\ arr_length arr = arr_length arr') ->
+      (forall s, basa ! s = None <-> nasa ! s = None) ->
+      match_arrs_size nasa basa.
+
+Definition match_empty_size (m : module) (ar : assocmap_arr) : Prop :=
+  match_arrs_size (empty_stack m) ar.
+Hint Unfold match_empty_size : mgen.
+
+Definition disable_ram (ram: option ram) (asr : assocmap_reg) : Prop :=
+  match ram with
+  | Some r => Int.eq (asr # ((ram_en r), 32)) (asr # ((ram_u_en r), 32)) = true
+  | None => True
+  end.
+
+Inductive match_stackframes : stackframe -> stackframe -> Prop :=
+  match_stackframe_intro :
+    forall r m pc asr asa asr' asa'
+      (DISABLE_RAM: disable_ram (mod_ram (transf_module m)) asr')
+      (MATCH_ASSOC: match_assocmaps (max_reg_module m + 1) asr asr')
+      (MATCH_ARRS: match_arrs asa asa')
+      (MATCH_EMPT1: match_empty_size m asa)
+      (MATCH_EMPT2: match_empty_size m asa')
+      (MATCH_RES: r < mod_st m),
+      match_stackframes (Stackframe r m pc asr asa)
+                        (Stackframe r (transf_module m) pc asr' asa').
+
+Inductive match_states : state -> state -> Prop :=
+| match_state :
+    forall res res' m st asr asr' asa asa'
+           (ASSOC: match_assocmaps (max_reg_module m + 1) asr asr')
+           (ARRS: match_arrs asa asa')
+           (STACKS: list_forall2 match_stackframes res res')
+           (ARRS_SIZE: match_empty_size m asa)
+           (ARRS_SIZE2: match_empty_size m asa')
+           (DISABLE_RAM: disable_ram (mod_ram (transf_module m)) asr'),
+      match_states (State res m st asr asa)
+                   (State res' (transf_module m) st asr' asa')
+| match_returnstate :
+    forall res res' i
+           (STACKS: list_forall2 match_stackframes res res'),
+      match_states (Returnstate res i) (Returnstate res' i)
+| match_initial_call :
+    forall m,
+      match_states (Callstate nil m nil)
+                   (Callstate nil (transf_module m) nil).
+Hint Constructors match_states : htlproof.
+
+Definition empty_stack_ram r :=
+  AssocMap.set (ram_mem r) (Array.arr_repeat None (ram_size r)) (AssocMap.empty arr).
+
+Definition empty_stack' len st :=
+  AssocMap.set st (Array.arr_repeat None len) (AssocMap.empty arr).
+
+Definition match_empty_size' l s (ar : assocmap_arr) : Prop :=
+  match_arrs_size (empty_stack' l s) ar.
+Hint Unfold match_empty_size : mgen.
+
+Definition merge_reg_assocs r :=
+  Verilog.mkassociations (Verilog.merge_regs (assoc_nonblocking r) (assoc_blocking r)) empty_assocmap.
+
+Definition merge_arr_assocs st len r :=
+  Verilog.mkassociations (Verilog.merge_arrs (assoc_nonblocking r) (assoc_blocking r)) (empty_stack' len st).
+
+Inductive match_reg_assocs : positive -> reg_associations -> reg_associations -> Prop :=
+  match_reg_association:
+    forall p rab rab' ran ran',
+      match_assocmaps p rab rab' ->
+      match_assocmaps p ran ran' ->
+      match_reg_assocs p (mkassociations rab ran) (mkassociations rab' ran').
+
+Inductive match_arr_assocs : arr_associations -> arr_associations -> Prop :=
+  match_arr_association:
+    forall rab rab' ran ran',
+      match_arrs rab rab' ->
+      match_arrs ran ran' ->
+      match_arr_assocs (mkassociations rab ran) (mkassociations rab' ran').
+
+Ltac mgen_crush := crush; eauto with mgen.
+
+Lemma match_assocmaps_equiv : forall p a, match_assocmaps p a a.
+Proof. constructor; auto. Qed.
+Hint Resolve match_assocmaps_equiv : mgen.
+
+Lemma match_arrs_equiv : forall a, match_arrs a a.
+Proof. econstructor; mgen_crush. Qed.
+Hint Resolve match_arrs_equiv : mgen.
+
+Lemma match_reg_assocs_equiv : forall p a, match_reg_assocs p a a.
+Proof. destruct a; constructor; mgen_crush. Qed.
+Hint Resolve match_reg_assocs_equiv : mgen.
+
+Lemma match_arr_assocs_equiv : forall a, match_arr_assocs a a.
+Proof. destruct a; constructor; mgen_crush. Qed.
+Hint Resolve match_arr_assocs_equiv : mgen.
+
+Lemma match_arrs_size_equiv : forall a, match_arrs_size a a.
+Proof. intros; repeat econstructor; eauto. Qed.
+Hint Resolve match_arrs_size_equiv : mgen.
+
+Lemma match_stacks_equiv :
+  forall m s l,
+    mod_stk m = s ->
+    mod_stk_len m = l ->
+    empty_stack' l s = empty_stack m.
+Proof. unfold empty_stack', empty_stack; mgen_crush. Qed.
+Hint Rewrite match_stacks_equiv : mgen.
+
+Lemma match_assocmaps_max1 :
+  forall p p' a b,
+    match_assocmaps (Pos.max p' p) a b ->
+    match_assocmaps p a b.
+Proof.
+  intros. inv H. constructor. intros.
+  apply H0. lia.
+Qed.
+Hint Resolve match_assocmaps_max1 : mgen.
+
+Lemma match_assocmaps_max2 :
+  forall p p' a b,
+    match_assocmaps (Pos.max p p') a b ->
+    match_assocmaps p a b.
+Proof.
+  intros. inv H. constructor. intros.
+  apply H0. lia.
+Qed.
+Hint Resolve match_assocmaps_max2 : mgen.
+
+Lemma match_assocmaps_ge :
+  forall p p' a b,
+    match_assocmaps p' a b ->
+    p <= p' ->
+    match_assocmaps p a b.
+Proof.
+  intros. inv H. constructor. intros.
+  apply H1. lia.
+Qed.
+Hint Resolve match_assocmaps_ge : mgen.
+
+Lemma match_reg_assocs_max1 :
+  forall p p' a b,
+    match_reg_assocs (Pos.max p' p) a b ->
+    match_reg_assocs p a b.
+Proof. intros; inv H; econstructor; mgen_crush. Qed.
+Hint Resolve match_reg_assocs_max1 : mgen.
+
+Lemma match_reg_assocs_max2 :
+  forall p p' a b,
+    match_reg_assocs (Pos.max p p') a b ->
+    match_reg_assocs p a b.
+Proof. intros; inv H; econstructor; mgen_crush. Qed.
+Hint Resolve match_reg_assocs_max2 : mgen.
+
+Lemma match_reg_assocs_ge :
+  forall p p' a b,
+    match_reg_assocs p' a b ->
+    p <= p' ->
+    match_reg_assocs p a b.
+Proof. intros; inv H; econstructor; mgen_crush. Qed.
+Hint Resolve match_reg_assocs_ge : mgen.
+
+Definition forall_ram (P: reg -> Prop) ram :=
+  P (ram_en ram)
+  /\ P (ram_u_en ram)
+  /\ P (ram_addr ram)
+  /\ P (ram_wr_en ram)
+  /\ P (ram_d_in ram)
+  /\ P (ram_d_out ram).
+
+Lemma forall_ram_lt :
+  forall m r,
+    (mod_ram m) = Some r ->
+    forall_ram (fun x => x < max_reg_module m + 1) r.
+Proof.
+  assert (X: forall a b c, a < b + 1 -> a < Pos.max c b + 1) by lia.
+  unfold forall_ram; simplify; unfold max_reg_module; repeat apply X;
+  unfold max_reg_ram; rewrite H; try lia.
+Qed.
+Hint Resolve forall_ram_lt : mgen.
+
+Definition exec_all d_s c_s rs1 ar1 rs3 ar3 :=
+  exists f rs2 ar2,
+    stmnt_runp f rs1 ar1 c_s rs2 ar2
+    /\ stmnt_runp f rs2 ar2 d_s rs3 ar3.
+
+Definition exec_all_ram r d_s c_s rs1 ar1 rs4 ar4 :=
+  exists f rs2 ar2 rs3 ar3,
+    stmnt_runp f rs1 ar1 c_s rs2 ar2
+    /\ stmnt_runp f rs2 ar2 d_s rs3 ar3
+    /\ exec_ram (merge_reg_assocs rs3) (merge_arr_assocs (ram_mem r) (ram_size r) ar3) (Some r) rs4 ar4.
+
+Lemma merge_reg_idempotent :
+  forall rs, merge_reg_assocs (merge_reg_assocs rs) = merge_reg_assocs rs.
+Proof. auto. Qed.
+Hint Rewrite merge_reg_idempotent : mgen.
+
+Lemma merge_arr_idempotent :
+  forall ar st len v v',
+    (assoc_nonblocking ar)!st = Some v ->
+    (assoc_blocking ar)!st = Some v' ->
+    arr_length v' = len ->
+    arr_length v = len ->
+    (assoc_blocking (merge_arr_assocs st len (merge_arr_assocs st len ar)))!st
+    = (assoc_blocking (merge_arr_assocs st len ar))!st
+    /\ (assoc_nonblocking (merge_arr_assocs st len (merge_arr_assocs st len ar)))!st
+       = (assoc_nonblocking (merge_arr_assocs st len ar))!st.
+Proof.
+  split; simplify; eauto.
+  unfold merge_arrs.
+  rewrite AssocMap.gcombine by reflexivity.
+  unfold empty_stack'.
+  rewrite AssocMap.gss.
+  setoid_rewrite merge_arr_empty2; auto.
+  rewrite AssocMap.gcombine by reflexivity.
+  unfold merge_arr, arr.
+  rewrite H. rewrite H0. auto.
+  unfold combine.
+  simplify.
+  rewrite list_combine_length.
+  rewrite (arr_wf v). rewrite (arr_wf v').
+  lia.
+Qed.
+
+Lemma empty_arr :
+  forall m s,
+    (exists l, (empty_stack m) ! s = Some (arr_repeat None l))
+    \/ (empty_stack m) ! s = None.
+Proof.
+  unfold empty_stack. simplify.
+  destruct (Pos.eq_dec s (mod_stk m)); subst.
+  left. eexists. apply AssocMap.gss.
+  right. rewrite AssocMap.gso; auto. apply AssocMap.gempty.
+Qed.
+
+Lemma merge_arr_empty':
+  forall m ar s v,
+    match_empty_size m ar ->
+    (merge_arrs (empty_stack m) ar) ! s = v ->
+    ar ! s = v.
+Proof.
+  inversion 1; subst.
+  pose proof (empty_arr m s).
+  simplify.
+  destruct (merge_arrs (empty_stack m) ar) ! s eqn:?; subst.
+  - inv H3. inv H4.
+    learn H3 as H5. apply H0 in H5. inv H5. simplify.
+    unfold merge_arrs in *. rewrite AssocMap.gcombine in Heqo; auto.
+    rewrite H3 in Heqo. erewrite merge_arr_empty2 in Heqo. auto. eauto.
+    rewrite list_repeat_len in H6. auto.
+    learn H4 as H6. apply H2 in H6.
+    unfold merge_arrs in *. rewrite AssocMap.gcombine in Heqo; auto.
+    rewrite H4 in Heqo. unfold Verilog.arr in *. rewrite H6 in Heqo.
+    discriminate.
+  - inv H3. inv H4. learn H3 as H4. apply H0 in H4. inv H4. simplify.
+    rewrite list_repeat_len in H6.
+    unfold merge_arrs in *. rewrite AssocMap.gcombine in Heqo; auto. rewrite H3 in Heqo.
+    unfold Verilog.arr in *. rewrite H4 in Heqo.
+    discriminate.
+    apply H2 in H4; auto.
+Qed.
+
+Lemma merge_arr_empty :
+  forall m ar ar',
+    match_empty_size m ar ->
+    match_arrs ar ar' ->
+    match_arrs (merge_arrs (empty_stack m) ar) ar'.
+Proof.
+  inversion 1; subst; inversion 1; subst;
+  econstructor; intros; apply merge_arr_empty' in H6; auto.
+Qed.
+Hint Resolve merge_arr_empty : mgen.
+
+Lemma merge_arr_empty'':
+  forall m ar s v,
+    match_empty_size m ar ->
+    ar ! s = v ->
+    (merge_arrs (empty_stack m) ar) ! s = v.
+Proof.
+  inversion 1; subst.
+  pose proof (empty_arr m s).
+  simplify.
+  destruct (merge_arrs (empty_stack m) ar) ! s eqn:?; subst.
+  - inv H3. inv H4.
+    learn H3 as H5. apply H0 in H5. inv H5. simplify.
+    unfold merge_arrs in *. rewrite AssocMap.gcombine in Heqo; auto.
+    rewrite H3 in Heqo. erewrite merge_arr_empty2 in Heqo. auto. eauto.
+    rewrite list_repeat_len in H6. auto.
+    learn H4 as H6. apply H2 in H6.
+    unfold merge_arrs in *. rewrite AssocMap.gcombine in Heqo; auto.
+    rewrite H4 in Heqo. unfold Verilog.arr in *. rewrite H6 in Heqo.
+    discriminate.
+  - inv H3. inv H4. learn H3 as H4. apply H0 in H4. inv H4. simplify.
+    rewrite list_repeat_len in H6.
+    unfold merge_arrs in *. rewrite AssocMap.gcombine in Heqo; auto. rewrite H3 in Heqo.
+    unfold Verilog.arr in *. rewrite H4 in Heqo.
+    discriminate.
+    apply H2 in H4; auto.
+Qed.
+
+Lemma merge_arr_empty_match :
+  forall m ar,
+    match_empty_size m ar ->
+    match_empty_size m (merge_arrs (empty_stack m) ar).
+Proof.
+  inversion 1; subst.
+  constructor; simplify.
+  learn H3 as H4. apply H0 in H4. inv H4. simplify.
+  eexists; split; eauto. apply merge_arr_empty''; eauto.
+  apply merge_arr_empty' in H3; auto.
+  split; simplify.
+  unfold merge_arrs in H3. rewrite AssocMap.gcombine in H3; auto.
+  unfold merge_arr in *.
+  destruct (empty_stack m) ! s eqn:?;
+           destruct ar ! s; try discriminate; eauto.
+  apply merge_arr_empty''; auto. apply H2 in H3; auto.
+Qed.
+Hint Resolve merge_arr_empty_match : mgen.
+
+Definition ram_present {A: Type} ar r v v' :=
+  (assoc_nonblocking ar)!(ram_mem r) = Some v
+  /\ @arr_length A v = ram_size r
+  /\ (assoc_blocking ar)!(ram_mem r) = Some v'
+  /\ arr_length v' = ram_size r.
+
+Lemma find_assoc_get :
+  forall rs r trs,
+    rs ! r = trs ! r ->
+    rs # r = trs # r.
+Proof.
+  intros; unfold find_assocmap, AssocMapExt.get_default; rewrite H; auto.
+Qed.
+Hint Resolve find_assoc_get : mgen.
+
+Lemma find_assoc_get2 :
+  forall rs p r v trs,
+    (forall r, r < p -> rs ! r = trs ! r) ->
+    r < p ->
+    rs # r = v ->
+    trs # r = v.
+Proof.
+  intros; unfold find_assocmap, AssocMapExt.get_default; rewrite <- H; auto.
+Qed.
+Hint Resolve find_assoc_get2 : mgen.
+
+Lemma get_assoc_gt :
+  forall A (rs : AssocMap.t A) p r v trs,
+    (forall r, r < p -> rs ! r = trs ! r) ->
+    r < p ->
+    rs ! r = v ->
+    trs ! r = v.
+Proof. intros. rewrite <- H; auto. Qed.
+Hint Resolve get_assoc_gt : mgen.
+
+Lemma expr_runp_matches :
+  forall f rs ar e v,
+    expr_runp f rs ar e v ->
+    forall trs tar,
+      match_assocmaps (max_reg_expr e + 1) rs trs ->
+      match_arrs ar tar ->
+      expr_runp f trs tar e v.
+Proof.
+  induction 1.
+  - intros. econstructor.
+  - intros. econstructor. inv H0. symmetry.
+    apply find_assoc_get.
+    apply H2. crush.
+  - intros. econstructor. apply IHexpr_runp; eauto.
+    inv H1. constructor. simplify.
+    assert (forall a b c, a < b + 1 -> a < Pos.max c b + 1) by lia.
+    eapply H4 in H1. eapply H3 in H1. auto.
+    inv H2.
+    unfold arr_assocmap_lookup in *.
+    destruct (stack ! r) eqn:?; [|discriminate].
+    inv H1.
+    inv H0.
+    eapply H3 in Heqo. inv Heqo. inv H0.
+    unfold arr in *. rewrite H1. inv H5.
+    rewrite H0. auto.
+  - intros. econstructor; eauto. eapply IHexpr_runp1; eauto.
+    econstructor. inv H2. intros.
+    assert (forall a b c, a < b + 1 -> a < Pos.max b c + 1) by lia.
+    simplify.
+    eapply H5 in H2. apply H4 in H2. auto.
+    apply IHexpr_runp2; eauto.
+    econstructor. inv H2. intros.
+    assert (forall a b c, a < b + 1 -> a < Pos.max c b + 1) by lia.
+    simplify. eapply H5 in H2. apply H4 in H2. auto.
+  - intros. econstructor; eauto.
+  - intros. econstructor; eauto. apply IHexpr_runp1; eauto.
+    constructor. inv H2. intros. simplify.
+    assert (forall a b c, a < b + 1 -> a < Pos.max b c + 1) by lia.
+    eapply H5 in H2. apply H4 in H2. auto.
+    apply IHexpr_runp2; eauto. simplify.
+    assert (forall a b c d, a < b + 1 -> a < Pos.max c (Pos.max b d) + 1) by lia.
+    constructor. intros. eapply H4 in H5. inv H2. apply H6 in H5. auto.
+  - intros. eapply erun_Vternary_false. apply IHexpr_runp1; eauto. constructor. inv H2.
+    intros. simplify. assert (forall a b c, a < b + 1 -> a < Pos.max b c + 1) by lia.
+    eapply H5 in H2. apply H4 in H2. auto.
+    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.
+Qed.
+Hint Resolve expr_runp_matches : mgen.
+
+Lemma expr_runp_matches2 :
+  forall f rs ar e v p,
+    expr_runp f rs ar e v ->
+    max_reg_expr e < p ->
+    forall trs tar,
+      match_assocmaps p rs trs ->
+      match_arrs ar tar ->
+      expr_runp f trs tar e v.
+Proof.
+  intros. eapply expr_runp_matches; eauto.
+  assert (max_reg_expr e + 1 <= p) by lia.
+  mgen_crush.
+Qed.
+Hint Resolve expr_runp_matches2 : mgen.
+
+Lemma match_assocmaps_gss :
+  forall p rab rab' r rhsval,
+    match_assocmaps p rab rab' ->
+    match_assocmaps p rab # r <- rhsval rab' # r <- rhsval.
+Proof.
+  intros. inv H. econstructor.
+  intros.
+  unfold find_assocmap. unfold AssocMapExt.get_default.
+  destruct (Pos.eq_dec r r0); subst.
+  repeat rewrite PTree.gss; auto.
+  repeat rewrite PTree.gso; auto.
+Qed.
+Hint Resolve match_assocmaps_gss : mgen.
+
+Lemma match_assocmaps_gt :
+  forall p s ra ra' v,
+    p <= s ->
+    match_assocmaps p ra ra' ->
+    match_assocmaps p ra (ra' # s <- v).
+Proof.
+  intros. inv H0. constructor.
+  intros. rewrite AssocMap.gso; try lia. apply H1; auto.
+Qed.
+Hint Resolve match_assocmaps_gt : mgen.
+
+Lemma match_reg_assocs_block :
+  forall p rab rab' r rhsval,
+    match_reg_assocs p rab rab' ->
+    match_reg_assocs p (block_reg r rab rhsval) (block_reg r rab' rhsval).
+Proof. inversion 1; econstructor; eauto with mgen. Qed.
+Hint Resolve match_reg_assocs_block : mgen.
+
+Lemma match_reg_assocs_nonblock :
+  forall p rab rab' r rhsval,
+    match_reg_assocs p rab rab' ->
+    match_reg_assocs p (nonblock_reg r rab rhsval) (nonblock_reg r rab' rhsval).
+Proof. inversion 1; econstructor; eauto with mgen. Qed.
+Hint Resolve match_reg_assocs_nonblock : mgen.
+
+Lemma some_inj :
+  forall A (x: A) y,
+    Some x = Some y ->
+    x = y.
+Proof. inversion 1; auto. Qed.
+
+Lemma arrs_present :
+  forall r i v ar arr,
+    (arr_assocmap_set r i v ar) ! r = Some arr ->
+    exists b, ar ! r = Some b.
+Proof.
+  intros. unfold arr_assocmap_set in *.
+  destruct ar!r eqn:?.
+  rewrite AssocMap.gss in H.
+  inv H. eexists. auto. rewrite Heqo in H. discriminate.
+Qed.
+
+Ltac inv_exists :=
+  match goal with
+  | H: exists _, _ |- _ => inv H
+  end.
+
+Lemma array_get_error_bound_gt :
+  forall A i (a : Array A),
+    (i >= arr_length a)%nat ->
+    array_get_error i a = None.
+Proof.
+  intros. unfold array_get_error.
+  apply nth_error_None. destruct a. simplify.
+  lia.
+Qed.
+Hint Resolve array_get_error_bound_gt : mgen.
+
+Lemma array_get_error_each :
+  forall A addr i (v : A) a x,
+    arr_length a = arr_length x ->
+    array_get_error addr a = array_get_error addr x ->
+    array_get_error addr (array_set i v a) = array_get_error addr (array_set i v x).
+Proof.
+  intros.
+  destruct (Nat.eq_dec addr i); subst.
+  destruct (lt_dec i (arr_length a)).
+  repeat rewrite array_get_error_set_bound; auto.
+  rewrite <- H. auto.
+  apply Nat.nlt_ge in n.
+  repeat rewrite array_get_error_bound_gt; auto.
+  rewrite <- array_set_len. rewrite <- H. lia.
+  repeat rewrite array_gso; auto.
+Qed.
+Hint Resolve array_get_error_each : mgen.
+
+Lemma match_arrs_gss :
+  forall ar ar' r v i,
+    match_arrs ar ar' ->
+    match_arrs (arr_assocmap_set r i v ar) (arr_assocmap_set r i v ar').
+Proof.
+  Ltac mag_tac :=
+    match goal with
+    | H: ?ar ! _ = Some _, H2: forall s arr, ?ar ! s = Some arr -> _ |- _ =>
+      let H3 := fresh "H" in
+      learn H as H3; apply H2 in H3; inv_exists; simplify
+    | H: ?ar ! _ = None, H2: forall s, ?ar ! s = None -> _ |- _ =>
+      let H3 := fresh "H" in
+      learn H as H3; apply H2 in H3; inv_exists; simplify
+    | H: ?ar ! _ = _ |- context[match ?ar ! _ with _ => _ end] =>
+      unfold Verilog.arr in *; rewrite H
+    | H: ?ar ! _ = _, H2: context[match ?ar ! _ with _ => _ end] |- _ =>
+      unfold Verilog.arr in *; rewrite H in H2
+    | H: context[(_ # ?s <- _) ! ?s] |- _ => rewrite AssocMap.gss in H
+    | H: context[(_ # ?r <- _) ! ?s], H2: ?r <> ?s |- _ => rewrite AssocMap.gso in H; auto
+    | |- context[(_ # ?s <- _) ! ?s] => rewrite AssocMap.gss
+    | H: ?r <> ?s |- context[(_ # ?r <- _) ! ?s] => rewrite AssocMap.gso; auto
+    end.
+  intros.
+  inv H. econstructor; simplify.
+  destruct (Pos.eq_dec r s); subst.
+  - unfold arr_assocmap_set, Verilog.arr in *.
+    destruct ar!s eqn:?.
+    mag_tac.
+    econstructor; simplify.
+    repeat mag_tac; auto.
+    intros. repeat mag_tac. simplify.
+    apply array_get_error_each; auto.
+    repeat mag_tac; crush.
+    repeat mag_tac; crush.
+  - unfold arr_assocmap_set in *.
+    destruct ar ! r eqn:?. rewrite AssocMap.gso in H; auto.
+    apply H0 in Heqo. apply H0 in H. repeat inv_exists. simplify.
+    econstructor. unfold Verilog.arr in *. rewrite H3. simplify.
+    rewrite AssocMap.gso; auto. eauto. intros. auto. auto.
+    apply H1 in Heqo. apply H0 in H. repeat inv_exists; simplify.
+    econstructor. unfold Verilog.arr in *. rewrite Heqo. simplify; eauto.
+  - destruct (Pos.eq_dec r s); unfold arr_assocmap_set, Verilog.arr in *; simplify; subst.
+    destruct ar!s eqn:?; repeat mag_tac; crush.
+    apply H1 in H. mag_tac; crush.
+    destruct ar!r eqn:?; repeat mag_tac; crush.
+    apply H1 in Heqo. repeat mag_tac; auto.
+Qed.
+Hint Resolve match_arrs_gss : mgen.
+
+Lemma match_arr_assocs_block :
+  forall rab rab' r i rhsval,
+    match_arr_assocs rab rab' ->
+    match_arr_assocs (block_arr r i rab rhsval) (block_arr r i rab' rhsval).
+Proof. inversion 1; econstructor; eauto with mgen. Qed.
+Hint Resolve match_arr_assocs_block : mgen.
+
+Lemma match_arr_assocs_nonblock :
+  forall rab rab' r i rhsval,
+    match_arr_assocs rab rab' ->
+    match_arr_assocs (nonblock_arr r i rab rhsval) (nonblock_arr r i rab' rhsval).
+Proof. inversion 1; econstructor; eauto with mgen. Qed.
+Hint Resolve match_arr_assocs_nonblock : mgen.
+
+Lemma match_states_same :
+  forall f rs1 ar1 c rs2 ar2 p,
+    stmnt_runp f rs1 ar1 c rs2 ar2 ->
+    max_reg_stmnt c < p ->
+    forall trs1 tar1,
+      match_reg_assocs p rs1 trs1 ->
+      match_arr_assocs ar1 tar1 ->
+      exists trs2 tar2,
+        stmnt_runp f trs1 tar1 c trs2 tar2
+        /\ match_reg_assocs p rs2 trs2
+        /\ match_arr_assocs ar2 tar2.
+Proof.
+  Ltac match_states_same_facts :=
+    match goal with
+    | H: match_reg_assocs _ _ _ |- _ =>
+      let H2 := fresh "H" in
+      learn H as H2; inv H2
+    | H: match_arr_assocs _ _ |- _ =>
+      let H2 := fresh "H" in
+      learn H as H2; inv H2
+    | H1: context[exists _, _], H2: context[exists _, _] |- _ =>
+      learn H1; learn H2;
+      exploit H1; mgen_crush; exploit H2; mgen_crush
+    | H1: context[exists _, _] |- _ =>
+      learn H1; exploit H1; mgen_crush
+    end.
+  Ltac match_states_same_tac :=
+    match goal with
+    | |- exists _, _ => econstructor
+    | |- _ < _ => lia
+    | H: context[_ <> _] |- stmnt_runp _ _ _ (Vcase _ (Stmntcons _ _ _) _) _ _ =>
+      eapply stmnt_runp_Vcase_nomatch
+    | |- stmnt_runp _ _ _ (Vcase _ (Stmntcons _ _ _) _) _ _ =>
+      eapply stmnt_runp_Vcase_match
+    | H: valueToBool _ = false |- stmnt_runp _ _ _ _ _ _ =>
+      eapply stmnt_runp_Vcond_false
+    | |- stmnt_runp _ _ _ _ _ _ => econstructor
+    | |- expr_runp _ _ _ _ _ => eapply expr_runp_matches2
+    end; mgen_crush; try lia.
+  induction 1; simplify; repeat match_states_same_facts;
+    try destruct_match; try solve [repeat match_states_same_tac].
+  - inv H. exists (block_reg r {| assoc_blocking := rab'; assoc_nonblocking := ran' |} rhsval);
+      repeat match_states_same_tac; econstructor.
+  - exists (nonblock_reg r {| assoc_blocking := rab'; assoc_nonblocking := ran' |} rhsval);
+      repeat match_states_same_tac; inv H; econstructor.
+  - econstructor. exists (block_arr r i {| assoc_blocking := rab'0; assoc_nonblocking := ran'0 |} rhsval).
+    simplify; repeat match_states_same_tac. inv H. econstructor.
+    repeat match_states_same_tac. eauto. mgen_crush.
+  - econstructor. exists (nonblock_arr r i {| assoc_blocking := rab'0; assoc_nonblocking := ran'0 |} rhsval).
+    simplify; repeat match_states_same_tac. inv H. econstructor.
+    repeat match_states_same_tac. eauto. mgen_crush.
+Qed.
+
+Lemma match_reg_assocs_merge :
+  forall p rs rs',
+    match_reg_assocs p rs rs' ->
+    match_reg_assocs p (merge_reg_assocs rs) (merge_reg_assocs rs').
+Proof.
+  inversion 1.
+  econstructor; econstructor; crush. inv H3.  inv H.
+  inv H7. inv H9.
+  unfold merge_regs.
+  destruct (ran!r) eqn:?; destruct (rab!r) eqn:?.
+  erewrite AssocMapExt.merge_correct_1; eauto.
+  erewrite AssocMapExt.merge_correct_1; eauto.
+  rewrite <- H2; eauto.
+  erewrite AssocMapExt.merge_correct_1; eauto.
+  erewrite AssocMapExt.merge_correct_1; eauto.
+  rewrite <- H2; eauto.
+  erewrite AssocMapExt.merge_correct_2; eauto.
+  erewrite AssocMapExt.merge_correct_2; eauto.
+  rewrite <- H2; eauto.
+  rewrite <- H; eauto.
+  erewrite AssocMapExt.merge_correct_3; eauto.
+  erewrite AssocMapExt.merge_correct_3; eauto.
+  rewrite <- H2; eauto.
+  rewrite <- H; eauto.
+Qed.
+Hint Resolve match_reg_assocs_merge : mgen.
+
+Lemma transf_not_changed :
+  forall state ram n d c i d_s c_s,
+    (forall e1 e2 r, d_s <> Vnonblock (Vvari r e1) e2) ->
+    (forall e1 e2 r, d_s <> Vnonblock e1 (Vvari r e2)) ->
+    d!i = Some d_s ->
+    c!i = Some c_s ->
+    transf_maps state ram (i, n) (d, c) = (d, c).
+Proof. intros; unfold transf_maps; repeat destruct_match; mgen_crush. Qed.
+
+Lemma transf_not_changed_neq :
+  forall state ram n d c d' c' i a d_s c_s,
+    transf_maps state ram (a, n) (d, c) = (d', c') ->
+    d!i = Some d_s ->
+    c!i = Some c_s ->
+    a <> i -> n <> i ->
+    d'!i = Some d_s /\ c'!i = Some c_s.
+Proof.
+  unfold transf_maps; intros; repeat destruct_match; mgen_crush;
+  match goal with [ H: (_, _) = (_, _) |- _ ] => inv H end;
+  repeat (rewrite AssocMap.gso; auto).
+Qed.
+
+Lemma forall_gt :
+  forall l, Forall (Pos.ge (fold_right Pos.max 1 l)) l.
+Proof.
+  induction l; auto.
+  constructor. inv IHl; simplify; lia.
+  simplify. destruct (Pos.max_dec a (fold_right Pos.max 1 l)).
+  rewrite e. apply Pos.max_l_iff in e. apply Pos.le_ge in e.
+  apply Forall_forall. rewrite Forall_forall in IHl.
+  intros.
+  assert (X: forall a b c, a >= c -> c >= b -> a >= b) by lia.
+  apply X with (b := x) in e; auto.
+  rewrite e; auto.
+Qed.
+
+Lemma max_index_list :
+  forall A (l : list (positive * A)) i d_s,
+    In (i, d_s) l ->
+    list_norepet (map fst l) ->
+    i <= fold_right Pos.max 1 (map fst l).
+Proof.
+  induction l; crush.
+  inv H. inv H0. simplify. lia.
+  inv H0.
+  let H := fresh "H" in
+  assert (H: forall a b c, c <= b -> c <= Pos.max a b) by lia;
+  apply H; eapply IHl; eauto.
+Qed.
+
+Lemma max_index :
+  forall A d i (d_s: A), d ! i = Some d_s -> i <= max_pc d.
+Proof.
+  unfold max_pc;
+  eauto using max_index_list,
+  PTree.elements_correct, PTree.elements_keys_norepet.
+Qed.
+
+Lemma max_index_2' :
+  forall l i, i > fold_right Pos.max 1 l -> Forall (Pos.gt i) l.
+Proof. induction l; crush; constructor; [|apply IHl]; lia. Qed.
+
+Lemma max_index_2'' :
+  forall l i, Forall (Pos.gt i) l -> ~ In i l.
+Proof.
+  induction l; crush. unfold not in *.
+  intros. inv H0. inv H. lia. eapply IHl.
+  inv H. apply H4. auto.
+Qed.
+
+Lemma elements_correct_none :
+  forall A am k,
+    ~ List.In k (List.map (@fst _ A) (AssocMap.elements am)) ->
+    AssocMap.get k am = None.
+Proof.
+  intros. apply AssocMapExt.elements_correct' in H. unfold not in *.
+  destruct am ! k eqn:?; auto. exfalso. apply H. eexists. auto.
+Qed.
+Hint Resolve elements_correct_none : assocmap.
+
+Lemma max_index_2 :
+  forall A (d: AssocMap.t A) i, i > max_pc d -> d ! i = None.
+Proof.
+  intros. unfold max_pc in *. apply max_index_2' in H.
+  apply max_index_2'' in H. apply elements_correct_none. auto.
+Qed.
+
+Definition match_prog (p: program) (tp: program) :=
+  Linking.match_program (fun cu f tf => tf = transf_fundef f) eq p tp.
+
+Lemma transf_program_match:
+  forall p, match_prog p (transf_program p).
+Proof.
+  intros. unfold transf_program, match_prog.
+  apply Linking.match_transform_program.
+Qed.
+
+Lemma exec_all_Vskip :
+  forall rs ar,
+    exec_all Vskip Vskip rs ar rs ar.
+Proof.
+  unfold exec_all.
+  intros. repeat econstructor.
+  Unshelve. unfold fext. exact tt.
+Qed.
+
+Lemma match_assocmaps_trans:
+  forall p rs1 rs2 rs3,
+    match_assocmaps p rs1 rs2 ->
+    match_assocmaps p rs2 rs3 ->
+    match_assocmaps p rs1 rs3.
+Proof.
+  intros. inv H. inv H0. econstructor; eauto.
+  intros. rewrite H1 by auto. auto.
+Qed.
+
+Lemma match_reg_assocs_trans:
+  forall p rs1 rs2 rs3,
+    match_reg_assocs p rs1 rs2 ->
+    match_reg_assocs p rs2 rs3 ->
+    match_reg_assocs p rs1 rs3.
+Proof.
+  intros. inv H. inv H0.
+  econstructor; eapply match_assocmaps_trans; eauto.
+Qed.
+
+Lemma empty_arrs_match :
+  forall m,
+    match_arrs (empty_stack m) (empty_stack (transf_module m)).
+Proof.
+  intros;
+  unfold empty_stack, transf_module; repeat destruct_match; mgen_crush.
+Qed.
+Hint Resolve empty_arrs_match : mgen.
+
+Lemma max_module_stmnts :
+  forall m,
+    Pos.max (max_stmnt_tree (mod_controllogic m))
+            (max_stmnt_tree (mod_datapath m)) < max_reg_module m + 1.
+Proof. intros. unfold max_reg_module. lia. Qed.
+Hint Resolve max_module_stmnts : mgen.
+
+Lemma transf_module_code :
+  forall m,
+    mod_ram m = None ->
+    transf_code (mod_st m)
+                {| ram_size := mod_stk_len m;
+                   ram_mem := mod_stk m;
+                   ram_en := max_reg_module m + 2;
+                   ram_addr := max_reg_module m + 1;
+                   ram_wr_en := max_reg_module m + 5;
+                   ram_d_in := max_reg_module m + 3;
+                   ram_d_out := max_reg_module m + 4;
+                   ram_u_en := max_reg_module m + 6;
+                   ram_ordering := ram_wf (max_reg_module m) |}
+                (mod_datapath m) (mod_controllogic m)
+    = ((mod_datapath (transf_module m)), mod_controllogic (transf_module m)).
+Proof. unfold transf_module; intros; repeat destruct_match; crush.
+       apply surjective_pairing. Qed.
+Hint Resolve transf_module_code : mgen.
+
+Lemma transf_module_code_ram :
+  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.
+Proof. intros; unfold max_reg_module; lia. Qed.
+Hint Resolve mod_reset_lt : mgen.
+
+Lemma mod_finish_lt : forall m, mod_finish m < max_reg_module m + 1.
+Proof. intros; unfold max_reg_module; lia. Qed.
+Hint Resolve mod_finish_lt : mgen.
+
+Lemma mod_return_lt : forall m, mod_return m < max_reg_module m + 1.
+Proof. intros; unfold max_reg_module; lia. Qed.
+Hint Resolve mod_return_lt : mgen.
+
+Lemma mod_start_lt : forall m, mod_start m < max_reg_module m + 1.
+Proof. intros; unfold max_reg_module; lia. Qed.
+Hint Resolve mod_start_lt : mgen.
+
+Lemma mod_stk_lt : forall m, mod_stk m < max_reg_module m + 1.
+Proof. intros; unfold max_reg_module; lia. Qed.
+Hint Resolve mod_stk_lt : mgen.
+
+Lemma mod_st_lt : forall m, mod_st m < max_reg_module m + 1.
+Proof. intros; unfold max_reg_module; lia. Qed.
+Hint Resolve mod_st_lt : mgen.
+
+Lemma mod_reset_modify :
+  forall m ar ar' v,
+    match_assocmaps (max_reg_module m + 1) ar ar' ->
+    ar ! (mod_reset m) = Some v ->
+    ar' ! (mod_reset (transf_module m)) = Some v.
+Proof.
+  inversion 1. intros.
+  unfold transf_module; repeat destruct_match; simplify;
+  rewrite <- H0; eauto with mgen.
+Qed.
+Hint Resolve mod_reset_modify : mgen.
+
+Lemma mod_finish_modify :
+  forall m ar ar' v,
+    match_assocmaps (max_reg_module m + 1) ar ar' ->
+    ar ! (mod_finish m) = Some v ->
+    ar' ! (mod_finish (transf_module m)) = Some v.
+Proof.
+  inversion 1. intros.
+  unfold transf_module; repeat destruct_match; simplify;
+  rewrite <- H0; eauto with mgen.
+Qed.
+Hint Resolve mod_finish_modify : mgen.
+
+Lemma mod_return_modify :
+  forall m ar ar' v,
+    match_assocmaps (max_reg_module m + 1) ar ar' ->
+    ar ! (mod_return m) = Some v ->
+    ar' ! (mod_return (transf_module m)) = Some v.
+Proof.
+  inversion 1. intros.
+  unfold transf_module; repeat destruct_match; simplify;
+  rewrite <- H0; eauto with mgen.
+Qed.
+Hint Resolve mod_return_modify : mgen.
+
+Lemma mod_start_modify :
+  forall m ar ar' v,
+    match_assocmaps (max_reg_module m + 1) ar ar' ->
+    ar ! (mod_start m) = Some v ->
+    ar' ! (mod_start (transf_module m)) = Some v.
+Proof.
+  inversion 1. intros.
+  unfold transf_module; repeat destruct_match; simplify;
+  rewrite <- H0; eauto with mgen.
+Qed.
+Hint Resolve mod_start_modify : mgen.
+
+Lemma mod_st_modify :
+  forall m ar ar' v,
+    match_assocmaps (max_reg_module m + 1) ar ar' ->
+    ar ! (mod_st m) = Some v ->
+    ar' ! (mod_st (transf_module m)) = Some v.
+Proof.
+  inversion 1. intros.
+  unfold transf_module; repeat destruct_match; simplify;
+  rewrite <- H0; eauto with mgen.
+Qed.
+Hint Resolve mod_st_modify : mgen.
+
+Lemma match_arrs_read :
+  forall ra ra' addr v mem,
+    arr_assocmap_lookup ra mem addr = Some v ->
+    match_arrs ra ra' ->
+    arr_assocmap_lookup ra' mem addr = Some v.
+Proof.
+  unfold arr_assocmap_lookup. intros. destruct_match; destruct_match; try discriminate.
+  inv H0. eapply H1 in Heqo0. inv Heqo0. simplify. unfold arr in *.
+  rewrite H in Heqo. inv Heqo.
+  rewrite H0. auto.
+  inv H0. eapply H1 in Heqo0. inv Heqo0. inv H0. unfold arr in *.
+  rewrite H3 in Heqo. discriminate.
+Qed.
+Hint Resolve match_arrs_read : mgen.
+
+Lemma match_reg_implies_equal :
+  forall ra ra' p a b c,
+    Int.eq (ra # a) (ra # b) = c ->
+    a < p -> b < p ->
+    match_assocmaps p ra ra' ->
+    Int.eq (ra' # a) (ra' # b) = c.
+Proof.
+  unfold find_assocmap, AssocMapExt.get_default; intros.
+  inv H2. destruct (ra ! a) eqn:?; destruct (ra ! b) eqn:?;
+  repeat rewrite <- H3 by lia; rewrite Heqo; rewrite Heqo0; auto.
+Qed.
+Hint Resolve match_reg_implies_equal : mgen.
+
+Lemma exec_ram_same :
+  forall rs1 ar1 ram rs2 ar2 p,
+    exec_ram rs1 ar1 (Some ram) rs2 ar2 ->
+    forall_ram (fun x => x < p) ram ->
+    forall trs1 tar1,
+      match_reg_assocs p rs1 trs1 ->
+      match_arr_assocs ar1 tar1 ->
+      exists trs2 tar2,
+        exec_ram trs1 tar1 (Some ram) trs2 tar2
+        /\ match_reg_assocs p rs2 trs2
+        /\ match_arr_assocs ar2 tar2.
+Proof.
+  Ltac exec_ram_same_facts :=
+    match goal with
+    | H: match_reg_assocs _ _ _ |- _ => let H2 := fresh "H" in learn H as H2; inv H2
+    | H: match_assocmaps _ _ _ |- _ => let H2 := fresh "H" in learn H as H2; inv H2
+    | H: match_arr_assocs _ _ |- _ => let H2 := fresh "H" in learn H as H2; inv H2
+    | H: match_arrs _ _ |- _ => let H2 := fresh "H" in learn H as H2; inv H2
+    end.
+  inversion 1; subst; destruct ram; unfold forall_ram; simplify; repeat exec_ram_same_facts.
+  - repeat (econstructor; mgen_crush).
+  - do 2 econstructor; simplify;
+      [eapply exec_ram_Some_write; [ apply H1 | apply H2 | | | | | ] | | ];
+      mgen_crush.
+  - do 2 econstructor; simplify; [eapply exec_ram_Some_read | | ];
+      repeat (try econstructor; mgen_crush).
+Qed.
+
+Lemma match_assocmaps_merge :
+  forall p nasr basr nasr' basr',
+    match_assocmaps p nasr nasr' ->
+    match_assocmaps p basr basr' ->
+    match_assocmaps p (merge_regs nasr basr) (merge_regs nasr' basr').
+Proof.
+  unfold merge_regs.
+  intros. inv H. inv H0. econstructor.
+  intros.
+  destruct nasr ! r eqn:?; destruct basr ! r eqn:?.
+  erewrite AssocMapExt.merge_correct_1; mgen_crush.
+  erewrite AssocMapExt.merge_correct_1; mgen_crush.
+  erewrite AssocMapExt.merge_correct_1; mgen_crush.
+  erewrite AssocMapExt.merge_correct_1; mgen_crush.
+  erewrite AssocMapExt.merge_correct_2; mgen_crush.
+  erewrite AssocMapExt.merge_correct_2; mgen_crush.
+  erewrite AssocMapExt.merge_correct_3; mgen_crush.
+  erewrite AssocMapExt.merge_correct_3; mgen_crush.
+Qed.
+Hint Resolve match_assocmaps_merge : mgen.
+
+Lemma list_combine_nth_error1 :
+  forall l l' addr v,
+    length l = length l' ->
+    nth_error l addr = Some (Some v) ->
+    nth_error (list_combine merge_cell l l') addr = Some (Some v).
+Proof. induction l; destruct l'; destruct addr; crush. Qed.
+
+Lemma list_combine_nth_error2 :
+  forall l' l addr v,
+    length l = length l' ->
+    nth_error l addr = Some None ->
+    nth_error l' addr = Some (Some v) ->
+    nth_error (list_combine merge_cell l l') addr = Some (Some v).
+Proof. induction l'; try rewrite nth_error_nil in *; destruct l; destruct addr; crush. Qed.
+
+Lemma list_combine_nth_error3 :
+  forall l l' addr,
+    length l = length l' ->
+    nth_error l addr = Some None ->
+    nth_error l' addr = Some None ->
+    nth_error (list_combine merge_cell l l') addr = Some None.
+Proof. induction l; destruct l'; destruct addr; crush. Qed.
+
+Lemma list_combine_nth_error4 :
+  forall l l' addr,
+    length l = length l' ->
+    nth_error l addr = None ->
+    nth_error (list_combine merge_cell l l') addr = None.
+Proof. induction l; destruct l'; destruct addr; crush. Qed.
+
+Lemma list_combine_nth_error5 :
+  forall l l' addr,
+    length l = length l' ->
+    nth_error l' addr = None ->
+    nth_error (list_combine merge_cell l l') addr = None.
+Proof. induction l; destruct l'; destruct addr; crush. Qed.
+
+Lemma array_get_error_merge1 :
+  forall a a0 addr v,
+    arr_length a = arr_length a0 ->
+    array_get_error addr a = Some (Some v) ->
+    array_get_error addr (combine merge_cell a a0) = Some (Some v).
+Proof.
+  unfold array_get_error, combine in *; intros;
+  apply list_combine_nth_error1; destruct a; destruct a0; crush.
+Qed.
+
+Lemma array_get_error_merge2 :
+  forall a a0 addr v,
+    arr_length a = arr_length a0 ->
+    array_get_error addr a0 = Some (Some v) ->
+    array_get_error addr a = Some None ->
+    array_get_error addr (combine merge_cell a a0) = Some (Some v).
+Proof.
+  unfold array_get_error, combine in *; intros;
+  apply list_combine_nth_error2; destruct a; destruct a0; crush.
+Qed.
+
+Lemma array_get_error_merge3 :
+  forall a a0 addr,
+    arr_length a = arr_length a0 ->
+    array_get_error addr a0 = Some None ->
+    array_get_error addr a = Some None ->
+    array_get_error addr (combine merge_cell a a0) = Some None.
+Proof.
+  unfold array_get_error, combine in *; intros;
+  apply list_combine_nth_error3; destruct a; destruct a0; crush.
+Qed.
+
+Lemma array_get_error_merge4 :
+  forall a a0 addr,
+    arr_length a = arr_length a0 ->
+    array_get_error addr a = None ->
+    array_get_error addr (combine merge_cell a a0) = None.
+Proof.
+  unfold array_get_error, combine in *; intros;
+  apply list_combine_nth_error4; destruct a; destruct a0; crush.
+Qed.
+
+Lemma array_get_error_merge5 :
+  forall a a0 addr,
+    arr_length a = arr_length a0 ->
+    array_get_error addr a0 = None ->
+    array_get_error addr (combine merge_cell a a0) = None.
+Proof.
+  unfold array_get_error, combine in *; intros;
+  apply list_combine_nth_error5; destruct a; destruct a0; crush.
+Qed.
+
+Lemma match_arrs_merge' :
+  forall addr nasa basa arr s x x0 a a0 nasa' basa',
+    (AssocMap.combine merge_arr nasa basa) ! s = Some arr ->
+    nasa ! s = Some a ->
+    basa ! s = Some a0 ->
+    nasa' ! s = Some x0 ->
+    basa' ! s = Some x ->
+    arr_length x = arr_length x0 ->
+    array_get_error addr a0 = array_get_error addr x ->
+    arr_length a0 = arr_length x ->
+    array_get_error addr a = array_get_error addr x0 ->
+    arr_length a = arr_length x0 ->
+    array_get_error addr arr = array_get_error addr (combine merge_cell x0 x).
+Proof.
+  intros. rewrite AssocMap.gcombine in H by auto.
+  unfold merge_arr in H.
+  rewrite H0 in H. rewrite H1 in H. inv H.
+  destruct (array_get_error addr a0) eqn:?; destruct (array_get_error addr a) eqn:?.
+  destruct o; destruct o0.
+  erewrite array_get_error_merge1; eauto. erewrite array_get_error_merge1; eauto.
+  rewrite <- H6 in H4. rewrite <- H8 in H4. auto.
+  erewrite array_get_error_merge2; eauto. erewrite array_get_error_merge2; eauto.
+  rewrite <- H6 in H4. rewrite <- H8 in H4. auto.
+  erewrite array_get_error_merge1; eauto. erewrite array_get_error_merge1; eauto.
+  rewrite <- H6 in H4. rewrite <- H8 in H4. auto.
+  erewrite array_get_error_merge3; eauto. erewrite array_get_error_merge3; eauto.
+  rewrite <- H6 in H4. rewrite <- H8 in H4. auto.
+  erewrite array_get_error_merge4; eauto. erewrite array_get_error_merge4; eauto.
+  rewrite <- H6 in H4. rewrite <- H8 in H4. auto.
+  erewrite array_get_error_merge5; eauto. erewrite array_get_error_merge5; eauto.
+  rewrite <- H6 in H4. rewrite <- H8 in H4. auto.
+  erewrite array_get_error_merge5; eauto. erewrite array_get_error_merge5; eauto.
+  rewrite <- H6 in H4. rewrite <- H8 in H4. auto.
+Qed.
+
+Lemma match_arrs_merge :
+  forall nasa nasa' basa basa',
+    match_arrs_size nasa basa ->
+    match_arrs nasa nasa' ->
+    match_arrs basa basa' ->
+    match_arrs (merge_arrs nasa basa) (merge_arrs nasa' basa').
+Proof.
+  unfold merge_arrs.
+  intros. inv H. inv H0. inv H1. econstructor.
+  - intros. destruct nasa ! s eqn:?; destruct basa ! s eqn:?; unfold Verilog.arr in *.
+    + pose proof Heqo. apply H in Heqo. pose proof Heqo0. apply H0 in Heqo0.
+      repeat inv_exists. simplify.
+      eexists. simplify. rewrite AssocMap.gcombine; eauto.
+      unfold merge_arr. unfold Verilog.arr in *. rewrite H11. rewrite H12. auto.
+      intros. eapply match_arrs_merge'; eauto. eapply H2 in H7; eauto.
+      inv_exists. simplify. congruence.
+      rewrite AssocMap.gcombine in H1; auto. unfold merge_arr in H1.
+      rewrite H7 in H1. rewrite H8 in H1. inv H1.
+      repeat rewrite combine_length; auto.
+      eapply H2 in H7; eauto. inv_exists; simplify; congruence.
+      eapply H2 in H7; eauto. inv_exists; simplify; congruence.
+    + apply H2 in Heqo; inv_exists; crush.
+    + apply H3 in Heqo0; inv_exists; crush.
+    + rewrite AssocMap.gcombine in H1 by auto. unfold merge_arr in *.
+      rewrite Heqo in H1. rewrite Heqo0 in H1. discriminate.
+  - intros. rewrite AssocMap.gcombine in H1 by auto. unfold merge_arr in H1.
+    repeat destruct_match; crush.
+    rewrite AssocMap.gcombine by auto; unfold merge_arr.
+    apply H5 in Heqo. apply H6 in Heqo0.
+    unfold Verilog.arr in *.
+    rewrite Heqo. rewrite Heqo0. auto.
+Qed.
+Hint Resolve match_arrs_merge : mgen.
+
+Lemma match_empty_size_merge :
+  forall nasa2 basa2 m,
+  match_empty_size m nasa2 ->
+  match_empty_size m basa2 ->
+  match_empty_size m (merge_arrs nasa2 basa2).
+Proof.
+  intros. inv H. inv H0. constructor.
+  simplify. unfold merge_arrs. rewrite AssocMap.gcombine by auto.
+  pose proof H0 as H6. apply H1 in H6. inv_exists; simplify.
+  pose proof H0 as H9. apply H in H9. inv_exists; simplify.
+  eexists. simplify. unfold merge_arr. unfold Verilog.arr in *. rewrite H6.
+  rewrite H9. auto. rewrite H8. symmetry. apply combine_length. congruence.
+  intros.
+  destruct (nasa2 ! s) eqn:?; destruct (basa2 ! s) eqn:?.
+  unfold merge_arrs in H0. rewrite AssocMap.gcombine in H0 by auto.
+  unfold merge_arr in *. setoid_rewrite Heqo in H0. setoid_rewrite Heqo0 in H0. inv H0.
+  apply H2 in Heqo. apply H4 in Heqo0. repeat inv_exists; simplify.
+  eexists. simplify. eauto. rewrite list_combine_length.
+  rewrite (arr_wf a). rewrite (arr_wf a0). lia.
+  unfold merge_arrs in H0. rewrite AssocMap.gcombine in H0 by auto.
+  unfold merge_arr in *.  setoid_rewrite Heqo in H0. setoid_rewrite Heqo0 in H0.
+  apply H2 in Heqo. inv_exists; simplify.
+  econstructor; eauto.
+  unfold merge_arrs in H0. rewrite AssocMap.gcombine in H0 by auto.
+  unfold merge_arr in *.  setoid_rewrite Heqo in H0. setoid_rewrite Heqo0 in H0.
+  inv H0. apply H4 in Heqo0. inv_exists; simplify. econstructor; eauto.
+  unfold merge_arrs in H0. rewrite AssocMap.gcombine in H0 by auto.
+  unfold merge_arr in *.  setoid_rewrite Heqo in H0. setoid_rewrite Heqo0 in H0.
+  discriminate.
+  split; intros.
+  unfold merge_arrs in H0. rewrite AssocMap.gcombine in H0 by auto.
+  unfold merge_arr in *. repeat destruct_match; crush. apply H5 in Heqo0; auto.
+  pose proof H0.
+  apply H5 in H0.
+  apply H3 in H6. unfold merge_arrs. rewrite AssocMap.gcombine by auto.
+  setoid_rewrite H0. setoid_rewrite H6. auto.
+Qed.
+Hint Resolve match_empty_size_merge : mgen.
+
+Lemma match_empty_size_match :
+  forall m nasa2 basa2,
+    match_empty_size m nasa2 ->
+    match_empty_size m basa2 ->
+    match_arrs_size nasa2 basa2.
+Proof.
+  Ltac match_empty_size_match_solve :=
+    match goal with
+    | H: context[forall s arr, ?ar ! s = Some arr -> _], H2: ?ar ! _ = Some _ |- _ =>
+      let H3 := fresh "H" in
+      learn H; pose proof H2 as H3; apply H in H3; repeat inv_exists
+    | H: context[forall s, ?ar ! s = None <-> _], H2: ?ar ! _ = None |- _ =>
+      let H3 := fresh "H" in
+      learn H; pose proof H2 as H3; apply H in H3
+    | H: context[forall s, _ <-> ?ar ! s = None], H2: ?ar ! _ = None |- _ =>
+      let H3 := fresh "H" in
+      learn H; pose proof H2 as H3; apply H in H3
+    | |- exists _, _ => econstructor
+    | |- _ ! _ = Some _ => eassumption
+    | |- _ = _ => congruence
+    | |- _ <-> _ => split
+    end; simplify.
+  inversion 1; inversion 1; constructor; simplify; repeat match_empty_size_match_solve.
+Qed.
+Hint Resolve match_empty_size_match : mgen.
+
+Lemma match_get_merge :
+  forall p ran ran' rab rab' s v,
+    s < p ->
+    match_assocmaps p ran ran' ->
+    match_assocmaps p rab rab' ->
+    (merge_regs ran rab) ! s = Some v ->
+    (merge_regs ran' rab') ! s = Some v.
+Proof.
+  intros.
+  assert (X: match_assocmaps p (merge_regs ran rab) (merge_regs ran' rab')) by auto with mgen.
+  inv X. rewrite <- H3; auto.
+Qed.
+Hint Resolve match_get_merge : mgen.
+
+Ltac masrp_tac :=
+  match goal with
+  | H: context[forall s arr, ?ar ! s = Some arr -> _], H2: ?ar ! _ = Some _ |- _ =>
+    let H3 := fresh "H" in
+    learn H; pose proof H2 as H3; apply H in H3; repeat inv_exists
+  | H: context[forall s, ?ar ! s = None <-> _], H2: ?ar ! _ = None |- _ =>
+    let H3 := fresh "H" in
+    learn H; pose proof H2 as H3; apply H in H3
+  | H: context[forall s, _ <-> ?ar ! s = None], H2: ?ar ! _ = None |- _ =>
+    let H3 := fresh "H" in
+    learn H; pose proof H2 as H3; apply H in H3
+  | ra: arr_associations |- _ =>
+    let ra1 := fresh "ran" in let ra2 := fresh "rab" in destruct ra as [ra1 ra2]
+  | |- _ ! _ = _ => solve [mgen_crush]
+  | |- _ = _ => congruence
+  | |- _ <> _ => lia
+  | H: ?ar ! ?s = _ |- context[match ?ar ! ?r with _ => _ end] => learn H; destruct (Pos.eq_dec s r); subst
+  | H: ?ar ! ?s = _ |- context[match ?ar ! ?s with _ => _ end] => setoid_rewrite H
+  | |- context[match ?ar ! ?s with _ => _ end] => destruct (ar ! s) eqn:?
+  | H: ?s <> ?r |- context[(_ # ?r <- _) ! ?s] => rewrite AssocMap.gso
+  | H: ?r <> ?s |- context[(_ # ?r <- _) ! ?s] => rewrite AssocMap.gso
+  | |- context[(_ # ?s <- _) ! ?s] => rewrite AssocMap.gss
+  | H: context[match ?ar ! ?r with _ => _ end ! ?s] |- _ =>
+    destruct (ar ! r) eqn:?; destruct (Pos.eq_dec r s); subst
+  | H: ?ar ! ?s = _, H2: context[match ?ar ! ?s with _ => _ end] |- _ =>
+    setoid_rewrite H in H2
+  | H: context[match ?ar ! ?s with _ => _ end] |- _ => destruct (ar ! s) eqn:?
+  | H: ?s <> ?r, H2: context[(_ # ?r <- _) ! ?s] |- _ => rewrite AssocMap.gso in H2
+  | H: ?r <> ?s, H2: context[(_ # ?r <- _) ! ?s] |- _ => rewrite AssocMap.gso in H2
+  | H: context[(_ # ?s <- _) ! ?s] |- _ => rewrite AssocMap.gss in H
+  | |- context[match_empty_size] => constructor
+  | |- context[arr_assocmap_set] => unfold arr_assocmap_set
+  | H: context[arr_assocmap_set] |- _ => unfold arr_assocmap_set in H
+  | |- exists _, _ => econstructor
+  | |- _ <-> _ => split
+  end; simplify.
+
+Lemma match_empty_assocmap_set :
+  forall m r i rhsval asa,
+    match_empty_size m asa ->
+    match_empty_size m (arr_assocmap_set r i rhsval asa).
+Proof.
+  inversion 1; subst; simplify.
+  constructor. intros.
+  repeat masrp_tac.
+  intros. do 5 masrp_tac; try solve [repeat masrp_tac].
+  apply H1 in H3. inv_exists. simplify.
+  econstructor. simplify. apply H3. congruence.
+  repeat masrp_tac. destruct (Pos.eq_dec r s); subst.
+  rewrite AssocMap.gss in H8. discriminate.
+  rewrite AssocMap.gso in H8; auto. apply H2 in H8. auto.
+  destruct (Pos.eq_dec r s); subst. apply H1 in H5. inv_exists. simplify.
+  rewrite H5 in H8. discriminate.
+  rewrite AssocMap.gso; auto.
+  apply H2 in H5. auto. apply H2 in H5. auto.
+  Unshelve. auto.
+Qed.
+Hint Resolve match_empty_assocmap_set : mgen.
+
+Lemma match_arrs_size_stmnt_preserved :
+  forall m f rs1 ar1 ar2 c rs2,
+    stmnt_runp f rs1 ar1 c rs2 ar2 ->
+    match_empty_size m (assoc_nonblocking ar1) ->
+    match_empty_size m (assoc_blocking ar1) ->
+    match_empty_size m (assoc_nonblocking ar2) /\ match_empty_size m (assoc_blocking ar2).
+Proof.
+  induction 1; inversion 1; inversion 1; eauto; simplify; try solve [repeat masrp_tac].
+  subst. apply IHstmnt_runp2; apply IHstmnt_runp1; auto.
+  apply IHstmnt_runp2; apply IHstmnt_runp1; auto.
+  apply match_empty_assocmap_set. auto.
+  apply match_empty_assocmap_set. auto.
+Qed.
+
+Lemma match_arrs_size_stmnt_preserved2 :
+  forall m f rs1 na ba na' ba' c rs2,
+    stmnt_runp f rs1 {| assoc_nonblocking := na; assoc_blocking := ba |} c rs2
+               {| assoc_nonblocking := na'; assoc_blocking := ba' |} ->
+    match_empty_size m na ->
+    match_empty_size m ba ->
+    match_empty_size m na' /\ match_empty_size m ba'.
+Proof.
+  intros.
+  remember ({| assoc_blocking := ba; assoc_nonblocking := na |}) as ar1.
+  remember ({| assoc_blocking := ba'; assoc_nonblocking := na' |}) as ar2.
+  assert (X1: na' = (assoc_nonblocking ar2)) by (rewrite Heqar2; auto). rewrite X1.
+  assert (X2: ba' = (assoc_blocking ar2)) by (rewrite Heqar2; auto). rewrite X2.
+  assert (X3: na = (assoc_nonblocking ar1)) by (rewrite Heqar1; auto). rewrite X3 in *.
+  assert (X4: ba = (assoc_blocking ar1)) by (rewrite Heqar1; auto). rewrite X4 in *.
+  eapply match_arrs_size_stmnt_preserved; mgen_crush.
+Qed.
+Hint Resolve match_arrs_size_stmnt_preserved2 : mgen.
+
+Lemma match_arrs_size_ram_preserved :
+  forall m rs1 ar1 ar2 ram rs2,
+    exec_ram rs1 ar1 ram rs2 ar2 ->
+    match_empty_size m (assoc_nonblocking ar1) ->
+    match_empty_size m (assoc_blocking ar1) ->
+    match_empty_size m (assoc_nonblocking ar2)
+    /\ match_empty_size m (assoc_blocking ar2).
+Proof.
+  induction 1; inversion 1; inversion 1; subst; simplify; try solve [repeat masrp_tac].
+  masrp_tac. masrp_tac. solve [repeat masrp_tac].
+  masrp_tac. masrp_tac. masrp_tac. masrp_tac. masrp_tac. masrp_tac. masrp_tac.
+  masrp_tac. masrp_tac. masrp_tac. masrp_tac. masrp_tac. masrp_tac. masrp_tac.
+  masrp_tac. apply H8 in H1; inv_exists; simplify. repeat masrp_tac. auto.
+  repeat masrp_tac.
+  repeat masrp_tac.
+  repeat masrp_tac.
+  destruct (Pos.eq_dec (ram_mem r) s); subst; repeat masrp_tac.
+  destruct (Pos.eq_dec (ram_mem r) s); subst; repeat masrp_tac.
+  apply H9 in H17; auto. apply H9 in H17; auto.
+  Unshelve. eauto.
+Qed.
+Hint Resolve match_arrs_size_ram_preserved : mgen.
+
+Lemma match_arrs_size_ram_preserved2 :
+  forall m rs1 na na' ba ba' ram rs2,
+    exec_ram rs1 {| assoc_nonblocking := na; assoc_blocking := ba |} ram rs2
+    {| assoc_nonblocking := na'; assoc_blocking := ba' |} ->
+    match_empty_size m na -> match_empty_size m ba ->
+    match_empty_size m na' /\ match_empty_size m ba'.
+Proof.
+  intros.
+  remember ({| assoc_blocking := ba; assoc_nonblocking := na |}) as ar1.
+  remember ({| assoc_blocking := ba'; assoc_nonblocking := na' |}) as ar2.
+  assert (X1: na' = (assoc_nonblocking ar2)) by (rewrite Heqar2; auto). rewrite X1.
+  assert (X2: ba' = (assoc_blocking ar2)) by (rewrite Heqar2; auto). rewrite X2.
+  assert (X3: na = (assoc_nonblocking ar1)) by (rewrite Heqar1; auto). rewrite X3 in *.
+  assert (X4: ba = (assoc_blocking ar1)) by (rewrite Heqar1; auto). rewrite X4 in *.
+  eapply match_arrs_size_ram_preserved; mgen_crush.
+Qed.
+Hint Resolve match_arrs_size_ram_preserved2 : mgen.
+
+Lemma empty_stack_m :
+  forall m, empty_stack m = empty_stack' (mod_stk_len m) (mod_stk m).
+Proof. unfold empty_stack, empty_stack'; mgen_crush. Qed.
+Hint Rewrite empty_stack_m : mgen.
+
+Ltac clear_forall :=
+  repeat match goal with
+  | H: context[forall _, _] |- _ => clear H
+  end.
+
+Lemma list_combine_none :
+  forall n l,
+    length l = n ->
+    list_combine Verilog.merge_cell (list_repeat None n) l = l.
+Proof.
+  induction n; intros; crush.
+  - symmetry. apply length_zero_iff_nil. auto.
+  - destruct l; crush.
+    rewrite list_repeat_cons.
+    crush. f_equal.
+    eauto.
+Qed.
+
+Lemma combine_none :
+  forall n a,
+    a.(arr_length) = n ->
+    arr_contents (combine Verilog.merge_cell (arr_repeat None n) a) = arr_contents a.
+Proof.
+  intros.
+  unfold combine.
+  crush.
+
+  rewrite <- (arr_wf a) in H.
+  apply list_combine_none.
+  assumption.
+Qed.
+
+Lemma combine_none2 :
+  forall n a addr,
+    arr_length a = n ->
+    array_get_error addr (combine Verilog.merge_cell (arr_repeat None n) a)
+    = array_get_error addr a.
+Proof. intros; auto using array_get_error_equal, combine_none. Qed.
+
+Lemma list_combine_lookup_first :
+  forall l1 l2 n,
+    length l1 = length l2 ->
+    nth_error l1 n = Some None ->
+    nth_error (list_combine Verilog.merge_cell l1 l2) n = nth_error l2 n.
+Proof.
+  induction l1; intros; crush.
+
+  rewrite nth_error_nil in H0.
+  discriminate.
+
+  destruct l2 eqn:EQl2. crush.
+  simpl in H. invert H.
+  destruct n; simpl in *.
+  invert H0. simpl. reflexivity.
+  eauto.
+Qed.
+
+Lemma combine_lookup_first :
+  forall a1 a2 n,
+    a1.(arr_length) = a2.(arr_length) ->
+    array_get_error n a1 = Some None ->
+    array_get_error n (combine Verilog.merge_cell a1 a2) = array_get_error n a2.
+Proof.
+  intros.
+
+  unfold array_get_error in *.
+  apply list_combine_lookup_first; eauto.
+  rewrite a1.(arr_wf). rewrite a2.(arr_wf).
+  assumption.
+Qed.
+
+Lemma list_combine_lookup_second :
+  forall l1 l2 n x,
+    length l1 = length l2 ->
+    nth_error l1 n = Some (Some x) ->
+    nth_error (list_combine Verilog.merge_cell l1 l2) n = Some (Some x).
+Proof.
+  induction l1; intros; crush; auto.
+
+  destruct l2 eqn:EQl2. crush.
+  simpl in H. invert H.
+  destruct n; simpl in *.
+  invert H0. simpl. reflexivity.
+  eauto.
+Qed.
+
+Lemma combine_lookup_second :
+  forall a1 a2 n x,
+    a1.(arr_length) = a2.(arr_length) ->
+    array_get_error n a1 = Some (Some x) ->
+    array_get_error n (combine Verilog.merge_cell a1 a2) = Some (Some x).
+Proof.
+  intros.
+
+  unfold array_get_error in *.
+  apply list_combine_lookup_second; eauto.
+  rewrite a1.(arr_wf). rewrite a2.(arr_wf).
+  assumption.
+Qed.
+
+Lemma match_get_arrs2 :
+  forall a i v l,
+    length a = l ->
+    list_combine merge_cell (list_set i (Some v) (list_repeat None l)) a =
+    list_combine merge_cell (list_repeat None l) (list_set i (Some v) a).
+Proof.
+  induction a; crush; subst.
+  - destruct i. unfold list_repeat. unfold list_repeat'. auto.
+    unfold list_repeat. unfold list_repeat'. auto.
+  - destruct i.
+    rewrite list_repeat_cons. simplify. auto.
+    rewrite list_repeat_cons. simplify. f_equal. apply IHa. auto.
+Qed.
+
+Lemma match_get_arrs :
+  forall addr i v x4 x x3,
+    x4 = arr_length x ->
+    x4 = arr_length x3 ->
+    array_get_error addr (combine merge_cell (array_set i (Some v) (arr_repeat None x4))
+                                  (combine merge_cell x x3))
+    = array_get_error addr (combine merge_cell (arr_repeat None x4)
+                                    (array_set i (Some v) (combine merge_cell x x3))).
+Proof.
+  intros. apply array_get_error_equal. unfold combine. simplify.
+  destruct x; destruct x3; simplify.
+  apply match_get_arrs2. rewrite list_combine_length. subst.
+  rewrite H0. lia.
+Qed.
+
+Lemma combine_array_set' :
+  forall a b i v,
+    length a = length b ->
+    list_combine merge_cell (list_set i (Some v) a) b =
+    list_set i (Some v) (list_combine merge_cell a b).
+Proof.
+  induction a; simplify; crush.
+  - destruct i; crush.
+  - destruct i; destruct b; crush.
+    f_equal. apply IHa. auto.
+Qed.
+
+Lemma combine_array_set :
+  forall a b i v addr,
+    arr_length a = arr_length b ->
+    array_get_error addr (combine merge_cell (array_set i (Some v) a) b)
+    = array_get_error addr (array_set i (Some v) (combine merge_cell a b)).
+Proof.
+  intros. destruct a; destruct b. unfold array_set. simplify.
+  unfold array_get_error. simplify. f_equal.
+  apply combine_array_set'. crush.
+Qed.
+
+Lemma array_get_combine' :
+  forall a b a' b' addr,
+    length a = length b ->
+    length a = length b' ->
+    length a = length a' ->
+    nth_error a addr = nth_error a' addr ->
+    nth_error b addr = nth_error b' addr ->
+    nth_error (list_combine merge_cell a b) addr =
+    nth_error (list_combine merge_cell a' b') addr.
+Proof.
+  induction a; crush.
+  - destruct b; crush; destruct b'; crush; destruct a'; crush.
+  - destruct b; crush; destruct b'; crush; destruct a'; crush;
+    destruct addr; crush; apply IHa.
+Qed.
+
+Lemma array_get_combine :
+  forall a b a' b' addr,
+    arr_length a = arr_length b ->
+    arr_length a = arr_length b' ->
+    arr_length a = arr_length a' ->
+    array_get_error addr a = array_get_error addr a' ->
+    array_get_error addr b = array_get_error addr b' ->
+    array_get_error addr (combine merge_cell a b)
+    = array_get_error addr (combine merge_cell a' b').
+Proof.
+  intros; unfold array_get_error, combine in *; destruct a; destruct b;
+  destruct a'; destruct b'; simplify; apply array_get_combine'; crush.
+Qed.
+
+Lemma match_empty_size_exists_Some :
+  forall m rab s v,
+    match_empty_size m rab ->
+    rab ! s = Some v ->
+    exists v', (empty_stack m) ! s = Some v' /\ arr_length v = arr_length v'.
+Proof. inversion 1; intros; repeat masrp_tac. Qed.
+
+Lemma match_empty_size_exists_None :
+  forall m rab s,
+    match_empty_size m rab ->
+    rab ! s = None ->
+    (empty_stack m) ! s = None.
+Proof. inversion 1; intros; repeat masrp_tac. Qed.
+
+Lemma match_empty_size_exists_None' :
+  forall m rab s,
+    match_empty_size m rab ->
+    (empty_stack m) ! s = None ->
+    rab ! s = None.
+Proof. inversion 1; intros; repeat masrp_tac. Qed.
+
+Lemma match_empty_size_exists_Some' :
+  forall m rab s v,
+    match_empty_size m rab ->
+    (empty_stack m) ! s = Some v ->
+    exists v', rab ! s = Some v' /\ arr_length v = arr_length v'.
+Proof. inversion 1; intros; repeat masrp_tac. Qed.
+
+Lemma match_arrs_Some :
+  forall ra ra' s v,
+    match_arrs ra ra' ->
+    ra ! s = Some v ->
+    exists v', ra' ! s = Some v'
+               /\ (forall addr, array_get_error addr v = array_get_error addr v')
+               /\ arr_length v = arr_length v'.
+Proof. inversion 1; intros; repeat masrp_tac. intros. rewrite H5. auto. Qed.
+
+Lemma match_arrs_None :
+  forall ra ra' s,
+    match_arrs ra ra' ->
+    ra ! s = None ->
+    ra' ! s = None.
+Proof. inversion 1; intros; repeat masrp_tac. Qed.
+
+Ltac learn_next :=
+  match goal with
+  | H: match_empty_size _ ?rab, H2: ?rab ! _ = Some _ |- _ =>
+    let H3 := fresh "H" in
+    learn H2 as H3; eapply match_empty_size_exists_Some in H3;
+    eauto; inv_exists; simplify
+  | H: match_empty_size _ ?rab, H2: ?rab ! _ = None |- _ =>
+    let H3 := fresh "H" in
+    learn H2 as H3; eapply match_empty_size_exists_None in H3; eauto
+  end.
+
+Ltac learn_empty :=
+  match goal with
+  | H: match_empty_size _ _, H2: (empty_stack _) ! _ = Some _ |- _ =>
+    let H3 := fresh "H" in
+    learn H as H3; eapply match_empty_size_exists_Some' in H3;
+    [| eassumption]; inv_exists; simplify
+  | H: match_arrs ?ar _, H2: ?ar ! _ = Some _ |- _ =>
+    let H3 := fresh "H" in
+    learn H as H3; eapply match_arrs_Some in H3;
+    [| eassumption]; inv_exists; simplify
+  | H: match_empty_size _ _, H2: (empty_stack _) ! _ = None |- _ =>
+    let H3 := fresh "H" in
+    learn H as H3; eapply match_empty_size_exists_None' in H3;
+    [| eassumption]; simplify
+  end.
+
+Lemma empty_set_none :
+  forall m ran rab s i v s0,
+    match_empty_size m ran ->
+    match_empty_size m rab ->
+    (arr_assocmap_set s i v ran) ! s0 = None ->
+    (arr_assocmap_set s i v rab) ! s0 = None.
+Proof.
+  unfold arr_assocmap_set; inversion 1; subst; simplify.
+  destruct (Pos.eq_dec s s0); subst.
+  destruct ran ! s0 eqn:?.
+  rewrite AssocMap.gss in H4. inv H4.
+  learn_next. learn_empty. rewrite H6; auto.
+  destruct ran ! s eqn:?. rewrite AssocMap.gso in H4.
+  learn_next. learn_empty. rewrite H6. rewrite AssocMap.gso.
+  repeat match goal with
+  | H: Learnt _ |- _ => clear H
+  end. clear Heqo. clear H5. clear H6.
+  learn_next. repeat learn_empty. auto. auto. auto.
+  pose proof Heqo. learn_next; repeat learn_empty.
+  repeat match goal with
+  | H: Learnt _ |- _ => clear H
+  end.
+  pose proof H4. learn_next; repeat learn_empty.
+  rewrite H7. auto.
+Qed.
+
+Ltac clear_learnt :=
+  repeat match goal with
+  | H: Learnt _ |- _ => clear H
+  end.
+
+Lemma match_arrs_size_assoc :
+  forall a b,
+    match_arrs_size a b ->
+    match_arrs_size b a.
+Proof. inversion 1; constructor; crush; split; apply H2. Qed.
+Hint Resolve match_arrs_size_assoc : mgen.
+
+Lemma match_arrs_merge_set2 :
+  forall rab rab' ran ran' s m i v,
+    match_empty_size m rab ->
+    match_empty_size m ran ->
+    match_empty_size m rab' ->
+    match_empty_size m ran' ->
+    match_arrs rab rab' ->
+    match_arrs ran ran' ->
+    match_arrs (merge_arrs (arr_assocmap_set s i v ran) rab)
+               (merge_arrs (arr_assocmap_set s i v (empty_stack m))
+                           (merge_arrs ran' rab')).
+Proof.
+  simplify.
+  constructor; intros.
+  unfold arr_assocmap_set in *. destruct (Pos.eq_dec s s0); subst.
+  destruct ran ! s0 eqn:?. unfold merge_arrs in *. rewrite AssocMap.gcombine in *; auto.
+  learn_next. repeat learn_empty.
+  econstructor. simplify. rewrite H6. rewrite AssocMap.gcombine by auto.
+  rewrite AssocMap.gss. simplify. setoid_rewrite H9. setoid_rewrite H7. simplify.
+  intros. rewrite AssocMap.gss in H5. setoid_rewrite H13 in H5.
+  simplify. pose proof (empty_arr m s0). inv H5. inv_exists. setoid_rewrite H5 in H6. inv H6.
+  unfold arr_repeat in H8. simplify. rewrite list_repeat_len in H8. rewrite list_repeat_len in H10.
+  rewrite match_get_arrs. crush. rewrite combine_none2. rewrite combine_array_set; try congruence.
+  apply array_get_error_each. rewrite combine_length; try congruence.
+  rewrite combine_length; try congruence.
+  apply array_get_combine; crush.
+  rewrite <- array_set_len. rewrite combine_length; crush. crush. crush.
+  setoid_rewrite H21 in H6; discriminate. rewrite combine_length.
+  rewrite <- array_set_len; crush.
+  unfold merge_arr in *. rewrite AssocMap.gss in H5. setoid_rewrite H13 in H5.
+  inv H5. rewrite combine_length. rewrite <- array_set_len; crush.
+  rewrite <- array_set_len; crush.
+  rewrite combine_length; crush.
+  destruct rab ! s0 eqn:?. learn_next. repeat learn_empty.
+  rewrite H11 in Heqo. discriminate.
+  unfold merge_arrs in H5. rewrite AssocMap.gcombine in H5; auto. rewrite Heqo in H5.
+  rewrite Heqo0 in H5. crush.
+
+  destruct ran ! s eqn:?.
+  learn_next. repeat learn_empty. rewrite H6.
+  unfold merge_arrs in *. rewrite AssocMap.gcombine in H5; auto.
+  rewrite AssocMap.gcombine; auto. rewrite AssocMap.gso in H5; auto.
+  rewrite AssocMap.gso; auto.
+  destruct ran ! s0 eqn:?.
+  learn_next.
+  repeat match goal with
+  | H: Learnt _ |- _ => clear H
+  end.
+  repeat learn_empty.
+  repeat match goal with
+  | H: Learnt _ |- _ => clear H
+  end.
+  rewrite AssocMap.gcombine; auto. setoid_rewrite Heqo0 in H5. setoid_rewrite H29 in H5.
+  simplify.
+  pose proof (empty_arr m s0). inv H5. inv_exists. rewrite H5 in H21. inv H21.
+  econstructor. simplify. setoid_rewrite H23. rewrite H25. setoid_rewrite H5.
+  simplify. intros. rewrite combine_none2. apply array_get_combine; solve [crush].
+  crush. rewrite list_combine_length. rewrite (arr_wf x5). rewrite (arr_wf x6).
+  rewrite <- H26. rewrite <- H28. rewrite list_repeat_len. lia. rewrite list_combine_length.
+  rewrite (arr_wf a). rewrite (arr_wf x7). rewrite combine_length. rewrite arr_repeat_length.
+  rewrite H24. rewrite <- H32. rewrite list_repeat_len. lia.
+  rewrite arr_repeat_length. rewrite combine_length. rewrite <- H26. symmetry. apply list_repeat_len.
+  congruence.
+  rewrite H37 in H21; discriminate.
+  repeat match goal with
+  | H: Learnt _ |- _ => clear H
+  end. eapply match_empty_size_exists_None in H0; eauto.
+  clear H6. repeat learn_empty. setoid_rewrite Heqo0 in H5.
+  setoid_rewrite H29 in H5. discriminate.
+  pose proof (match_arrs_merge ran ran' rab rab').
+  eapply match_empty_size_match in H; [|apply H0].
+  apply H6 in H; auto. inv H. apply H7 in H5. inv_exists. simplify.
+  learn_next. rewrite H9. econstructor. simplify.
+  apply merge_arr_empty''; mgen_crush.
+  auto. auto.
+  unfold merge_arrs in *. rewrite AssocMap.gcombine in H5; auto. rewrite AssocMap.gcombine; auto.
+  destruct (arr_assocmap_set s i v ran) ! s0 eqn:?; destruct rab ! s0 eqn:?; crush.
+  learn_next. repeat learn_empty.
+  repeat match goal with
+  | H: Learnt _ |- _ => clear H
+  end.
+  erewrite empty_set_none. rewrite AssocMap.gcombine; auto.
+  simplify. rewrite H7. rewrite H8. auto. apply H0. mgen_crush. auto.
+Qed.
+
+Definition all_match_empty_size m ar :=
+  match_empty_size m (assoc_nonblocking ar) /\ match_empty_size m (assoc_blocking ar).
+Hint Unfold all_match_empty_size : mgen.
+
+Definition match_module_to_ram m ram :=
+  ram_size ram = mod_stk_len m /\ ram_mem ram = mod_stk m.
+Hint Unfold match_module_to_ram : mgen.
+
+Lemma zip_range_forall_le :
+  forall A (l: list A) n, Forall (Pos.le n) (map snd (zip_range n l)).
+Proof.
+  induction l; crush; constructor; [lia|].
+  assert (forall n x, n+1 <= x -> n <= x) by lia.
+  apply Forall_forall. intros. apply H. generalize dependent x.
+  apply Forall_forall. apply IHl.
+Qed.
+
+Lemma transf_code_fold_correct:
+  forall l m state ram d' c' n,
+    fold_right (transf_maps state ram) (mod_datapath m, mod_controllogic m) l = (d', c') ->
+    Forall (fun x => x < n) (map fst l) ->
+    Forall (Pos.le n) (map snd l) ->
+    list_norepet (map fst l) ->
+    list_norepet (map snd l) ->
+    (forall p i c_s rs1 ar1 rs2 ar2 trs1 tar1 d_s,
+        i < n ->
+        all_match_empty_size m ar1 ->
+        all_match_empty_size m tar1 ->
+        match_module_to_ram m ram ->
+        (mod_datapath m)!i = Some d_s ->
+        (mod_controllogic m)!i = Some c_s ->
+        match_reg_assocs p rs1 trs1 ->
+        match_arr_assocs ar1 tar1 ->
+        max_reg_module m < p ->
+        exec_all d_s c_s rs1 ar1 rs2 ar2 ->
+        exists d_s' c_s' trs2 tar2,
+          d'!i = Some d_s' /\ c'!i = Some c_s'
+          /\ exec_all_ram ram d_s' c_s' trs1 tar1 trs2 tar2
+          /\ match_reg_assocs p (merge_reg_assocs rs2) (merge_reg_assocs trs2)
+          /\ match_arr_assocs (merge_arr_assocs (ram_mem ram) (ram_size ram) ar2)
+                              (merge_arr_assocs (ram_mem ram) (ram_size ram) tar2)).
+Proof.
+  induction l as [| a l IHl]; simplify.
+  - match goal with
+    | H: (_, _) = (_, _) |- _ => inv H
+    end;
+    unfold exec_all in *; repeat inv_exists; simplify.
+    exploit match_states_same;
+    try match goal with
+    | H: stmnt_runp _ _ _ ?c _ _, H2: (mod_controllogic _) ! _ = Some ?c |- _ => apply H
+    end; eauto; mgen_crush;
+    try match goal with
+    | H: (mod_controllogic _) ! _ = Some ?c |- _ =>
+      apply max_reg_stmnt_le_stmnt_tree in H; unfold max_reg_module in *; lia
+    end; intros;
+    exploit match_states_same;
+    try match goal with
+    | H: stmnt_runp _ _ _ ?c _ _, H2: (mod_datapath _) ! _ = Some ?c |- _ => apply H
+    end; eauto; mgen_crush;
+    try match goal with
+    | H: (mod_datapath _) ! _ = Some ?c |- _ =>
+      apply max_reg_stmnt_le_stmnt_tree in H; unfold max_reg_module in *; lia
+    end; intros;
+    repeat match goal with
+    | |- exists _, _ => eexists
+    end; simplify; eauto;
+    unfold exec_all_ram;
+    repeat match goal with
+    | |- exists _, _ => eexists
+    end; simplify; eauto.
+    constructor. admit.
+  Abort.
+
+Lemma empty_stack_transf : forall m, empty_stack (transf_module m) = empty_stack m.
+Proof. unfold empty_stack, transf_module; intros; repeat destruct_match; crush. Qed.
+
+Definition alt_unchanged (d : AssocMap.t stmnt) (c: AssocMap.t stmnt) d' c' i :=
+  d ! i = d' ! i /\ c ! i = c' ! i.
+
+Definition alt_store ram d (c : AssocMap.t stmnt) d' c' i :=
+  exists e1 e2,
+    d' ! i = Some (Vseq (Vnonblock (Vvar (ram_u_en ram)) (Vunop Vnot (Vvar (ram_u_en ram))))
+                        (Vseq (Vnonblock (Vvar (ram_wr_en ram)) (Vlit (ZToValue 1)))
+                              (Vseq (Vnonblock (Vvar (ram_d_in ram)) e2)
+                                    (Vnonblock (Vvar (ram_addr ram)) e1))))
+    /\ c' ! i = c ! i
+    /\ d ! i = Some (Vnonblock (Vvari (ram_mem ram) e1) e2).
+
+Definition alt_load state ram d (c : AssocMap.t stmnt) d' c' i n :=
+  exists ns e1 e2,
+    d' ! i = Some (Vseq (Vnonblock (Vvar (ram_u_en ram)) (Vunop Vnot (Vvar (ram_u_en ram))))
+                        (Vseq (Vnonblock (Vvar (ram_wr_en ram)) (Vlit (ZToValue 0)))
+                              (Vnonblock (Vvar (ram_addr ram)) e2)))
+    /\ d' ! n = Some (Vnonblock (Vvar e1) (Vvar (ram_d_out ram)))
+    /\ 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))
+    /\ 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
+  \/ alt_store ram d c d' c' i
+  \/ alt_load state ram d c d' c' i n.
+
+Lemma transf_alternatives :
+  forall ram n d c state i d' c',
+    transf_maps state ram (i, n) (d, c) = (d', c') ->
+    i <> n ->
+    alternatives state ram d c d' c' i n.
+Proof.
+  intros. unfold transf_maps in *.
+  repeat destruct_match; match goal with
+                         | H: (_, _) = (_, _) |- _ => inv H
+                         end; try solve [left; econstructor; crush]; simplify;
+  repeat match goal with
+  | H: (_ =? _) = true |- _ => apply Peqb_true_eq in H; subst
+  end; unfold alternatives; right;
+  match goal with
+  | H: context[Vnonblock (Vvari _ _) _] |- _ => left
+  | _ => right
+  end; repeat econstructor; simplify;
+  repeat match goal with
+         | |- ( _ # ?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.
+
+Lemma transf_alternatives_neq :
+  forall state ram a n' n d'' c'' d' c' i d c,
+    transf_maps state ram (a, n) (d, c) = (d', c') ->
+    a <> i -> n' <> n -> i <> n' -> a <> n' ->
+    i <> n -> a <> n ->
+    alternatives state ram d'' c'' d c i n' ->
+    alternatives state ram d'' c'' d' c' i n'.
+Proof.
+  unfold alternatives, alt_unchanged, alt_store, alt_load, transf_maps; intros;
+  repeat match goal with H: _ \/ _ |- _ => inv H | H: _ /\ _ |- _ => destruct H end;
+  [left | right; left | right; right];
+  repeat inv_exists; simplify;
+  repeat destruct_match;
+  repeat match goal with
+         | H: (_, _) = (_, _) |- _ => inv H
+         | |- exists _, _ => econstructor
+         end; repeat split; repeat rewrite AssocMap.gso by lia; eauto; lia.
+Qed.
+
+Lemma transf_alternatives_neq2 :
+  forall state ram a n' n d'' c'' d' c' i d c,
+    transf_maps state ram (a, n) (d', c') = (d, c) ->
+    a <> i -> n' <> n -> i <> n' -> a <> n' -> i <> n ->
+    alternatives state ram d c d'' c'' i n' ->
+    alternatives state ram d' c' d'' c'' i n'.
+Proof.
+  unfold alternatives, alt_unchanged, alt_store, alt_load, transf_maps; intros;
+  repeat match goal with H: _ \/ _ |- _ => inv H | H: _ /\ _ |- _ => destruct H end;
+  [left | right; left | right; right];
+  repeat inv_exists; simplify;
+  repeat destruct_match;
+  repeat match goal with
+         | H: (_, _) = (_, _) |- _ => inv H
+         | |- exists _, _ => econstructor
+         end; repeat split; repeat rewrite AssocMap.gso in * by lia; eauto; lia.
+Qed.
+
+Lemma transf_alt_unchanged_neq :
+  forall i c'' d'' d c d' c',
+    alt_unchanged d' c' d'' c'' i ->
+    d' ! i = d ! i ->
+    c' ! i = c ! i ->
+    alt_unchanged d c d'' c'' i.
+Proof. unfold alt_unchanged; simplify; congruence. Qed.
+
+Lemma transf_maps_neq :
+  forall state ram d c i n d' c' i' n' va vb vc vd,
+    transf_maps state ram (i, n) (d, c) = (d', c') ->
+    d ! i' = va -> d ! n' = vb ->
+    c ! i' = vc -> c ! n' = vd ->
+    i <> i' -> i <> n' -> n <> i' -> n <> n' ->
+    d' ! i' = va /\ d' ! n' = vb /\ c' ! i' = vc /\ c' ! n' = vd.
+Proof.
+  unfold transf_maps; intros; repeat destruct_match; simplify;
+  repeat match goal with
+         | H: (_, _) = (_, _) |- _ => inv H
+         | H: (_ =? _) = true |- _ => apply Peqb_true_eq in H; subst
+         | |- context[( _ # ?s <- _ ) ! ?r] => rewrite AssocMap.gso by lia
+         end; crush.
+Qed.
+
+Lemma alternatives_different_map :
+  forall l state ram d c d'' c'' d' c' n i p,
+    i <= p -> n > p ->
+    Forall (Pos.lt p) (map snd l) ->
+    Forall (Pos.ge p) (map fst l) ->
+    ~ In n (map snd l) ->
+    ~ In i (map fst l) ->
+    fold_right (transf_maps state ram) (d, c) l = (d', c') ->
+    alternatives state ram d' c' d'' c'' i n ->
+    alternatives state ram d c d'' c'' i n.
+Proof.
+  Opaque transf_maps.
+  induction l; intros.
+  - crush.
+  - simplify; repeat match goal with
+                     | H: context[_ :: _] |- _ => inv H
+                     | H: transf_maps _ _ _ (fold_right (transf_maps ?s ?r) (?d, ?c) ?l) = (_, _) |- _ =>
+                       let X := fresh "X" in
+                       remember (fold_right (transf_maps s r) (d, c) l) as X
+                     | X: _ * _ |- _ => destruct X
+                     | H: (_, _) = _ |- _ => symmetry in H
+                     end; simplify.
+    remember p0 as i'. symmetry in Heqi'. subst.
+    remember p1 as n'. symmetry in Heqn'. subst.
+    assert (i <> n') by lia.
+    assert (n <> i') by lia.
+    assert (n <> n') by lia.
+    assert (i <> i') by lia.
+    eapply IHl; eauto.
+    eapply transf_alternatives_neq2; eauto; try lia.
+Qed.
+
+Lemma transf_fold_alternatives :
+  forall l state ram d c d' c' i n d_s c_s,
+    fold_right (transf_maps state ram) (d, c) l = (d', c') ->
+    Pos.max (max_pc c) (max_pc d) < n ->
+    Forall (Pos.lt (Pos.max (max_pc c) (max_pc d))) (map snd l) ->
+    Forall (Pos.ge (Pos.max (max_pc c) (max_pc d))) (map fst l) ->
+    list_norepet (map fst l) ->
+    list_norepet (map snd l) ->
+    In (i, n) l ->
+    d ! i = Some d_s ->
+    c ! i = Some c_s ->
+    alternatives state ram d c d' c' i n.
+Proof.
+  Opaque transf_maps.
+  induction l; crush; [].
+  repeat match goal with
+         | H: context[_ :: _] |- _ => inv H
+         | H: transf_maps _ _ _ (fold_right (transf_maps ?s ?r) (?d, ?c) ?l) = (_, _) |- _ =>
+           let X := fresh "X" in
+           remember (fold_right (transf_maps s r) (d, c) l) as X
+         | X: _ * _ |- _ => destruct X
+         | H: (_, _) = _ |- _ => symmetry in H
+         end.
+  inv H5. inv H1. simplify.
+  eapply alternatives_different_map; eauto.
+  simplify; lia. simplify; lia. apply transf_alternatives; auto. lia.
+  simplify.
+  assert (X: In i (map fst l)). { replace i with (fst (i, n)) by auto. apply in_map; auto. }
+  assert (X2: In n (map snd l)). { replace n with (snd (i, n)) by auto. apply in_map; auto. }
+  assert (X3: n <> p0). { destruct (Pos.eq_dec n p0); subst; crush. }
+  assert (X4: i <> p). { destruct (Pos.eq_dec i p); subst; crush. }
+  eapply transf_alternatives_neq; eauto; apply max_index in H7; lia.
+  Transparent transf_maps.
+Qed.
+
+Lemma zip_range_inv :
+  forall A (l: list A) i n,
+    In i l ->
+    exists n', In (i, n') (zip_range n l) /\ n' >= n.
+Proof.
+  induction l; crush.
+  inv H. econstructor.
+  split. left. eauto. lia.
+  eapply IHl in H0. inv H0. inv H.
+  econstructor. split. right. apply H0. lia.
+Qed.
+
+Lemma zip_range_not_in_fst :
+  forall A (l: list A) a n, ~ In a l -> ~ In a (map fst (zip_range n l)).
+Proof. unfold not; induction l; crush; inv H0; firstorder. Qed.
+
+Lemma zip_range_no_repet_fst :
+  forall A (l: list A) a, list_norepet l -> list_norepet (map fst (zip_range a l)).
+Proof.
+  induction l; simplify; constructor; inv H; firstorder;
+  eapply zip_range_not_in_fst; auto.
+Qed.
+
+Lemma transf_code_alternatives :
+  forall state ram d c d' c' i d_s c_s,
+    transf_code state ram d c = (d', c') ->
+    d ! i = Some d_s ->
+    c ! i = Some c_s ->
+    exists n, alternatives state ram d c d' c' i n.
+Proof.
+  unfold transf_code;
+  intros.
+  pose proof H0 as X.
+  apply PTree.elements_correct in X. assert (In i (map fst (PTree.elements d))).
+  { replace i with (fst (i, d_s)) by auto. apply in_map. auto. }
+  exploit zip_range_inv. apply H2. intros. inv H3. simplify.
+  instantiate (1 := (Pos.max (max_pc c) (max_pc d) + 1)) in H3.
+  exists x.
+  eapply transf_fold_alternatives;
+  eauto using forall_gt, PTree.elements_keys_norepet, max_index. lia.
+  assert (Forall (Pos.le (Pos.max (max_pc c) (max_pc d) + 1))
+    (map snd (zip_range (Pos.max (max_pc c) (max_pc d) + 1)
+                        (map fst (PTree.elements d))))) by apply zip_range_forall_le.
+  apply Forall_forall; intros. eapply Forall_forall in H4; eauto. lia.
+  rewrite zip_range_fst_idem. apply Forall_forall; intros.
+  apply AssocMapExt.elements_iff in H4. inv H4. apply max_index in H6. lia.
+  eapply zip_range_no_repet_fst. apply PTree.elements_keys_norepet.
+  eapply zip_range_snd_no_repet.
+Qed.
+
+Lemma max_reg_stmnt_not_modified :
+  forall s f rs ar rs' ar',
+    stmnt_runp f rs ar s rs' ar' ->
+    forall r,
+      max_reg_stmnt s < r ->
+      (assoc_blocking rs) ! r = (assoc_blocking rs') ! r.
+Proof.
+  induction 1; crush;
+  try solve [repeat destruct_match; apply IHstmnt_runp; try lia; auto].
+  assert (X: (assoc_blocking asr1) ! r = (assoc_blocking asr2) ! r) by (apply IHstmnt_runp2; lia).
+  assert (X2: (assoc_blocking asr0) ! r = (assoc_blocking asr1) ! r) by (apply IHstmnt_runp1; lia).
+  congruence.
+  inv H. simplify. rewrite AssocMap.gso by lia; auto.
+Qed.
+
+Lemma max_reg_stmnt_not_modified_nb :
+  forall s f rs ar rs' ar',
+    stmnt_runp f rs ar s rs' ar' ->
+    forall r,
+      max_reg_stmnt s < r ->
+      (assoc_nonblocking rs) ! r = (assoc_nonblocking rs') ! r.
+Proof.
+  induction 1; crush;
+  try solve [repeat destruct_match; apply IHstmnt_runp; try lia; auto].
+  assert (X: (assoc_nonblocking asr1) ! r = (assoc_nonblocking asr2) ! r) by (apply IHstmnt_runp2; lia).
+  assert (X2: (assoc_nonblocking asr0) ! r = (assoc_nonblocking asr1) ! r) by (apply IHstmnt_runp1; lia).
+  congruence.
+  inv H. simplify. rewrite AssocMap.gso by lia; auto.
+Qed.
+
+Lemma int_eq_not_changed :
+  forall ar ar' r r2 b,
+    Int.eq (ar # r) (ar # r2) = b ->
+    ar ! r = ar' ! r ->
+    ar ! r2 = ar' ! r2 ->
+    Int.eq (ar' # r) (ar' # r2) = b.
+Proof.
+  unfold find_assocmap, AssocMapExt.get_default. intros.
+  rewrite <- H0. rewrite <- H1. auto.
+Qed.
+
+Lemma merge_find_assocmap :
+  forall ran rab x,
+    ran ! x = None ->
+    (merge_regs ran rab) # x = rab # x.
+Proof.
+  unfold merge_regs, find_assocmap, AssocMapExt.get_default.
+  intros. destruct (rab ! x) eqn:?.
+  erewrite AssocMapExt.merge_correct_2; eauto.
+  erewrite AssocMapExt.merge_correct_3; eauto.
+Qed.
+
+Lemma max_reg_module_controllogic_gt :
+  forall m i v p,
+    (mod_controllogic m) ! i = Some v ->
+    max_reg_module m < p ->
+    max_reg_stmnt v < p.
+Proof.
+  intros. unfold max_reg_module in *.
+  apply max_reg_stmnt_le_stmnt_tree in H. lia.
+Qed.
+
+Lemma max_reg_module_datapath_gt :
+  forall m i v p,
+    (mod_datapath m) ! i = Some v ->
+    max_reg_module m < p ->
+    max_reg_stmnt v < p.
+Proof.
+  intros. unfold max_reg_module in *.
+  apply max_reg_stmnt_le_stmnt_tree in H. lia.
+Qed.
+
+Lemma merge_arr_empty2 :
+  forall m ar ar',
+    match_empty_size m ar' ->
+    match_arrs ar ar' ->
+    match_arrs ar (merge_arrs (empty_stack m) ar').
+Proof.
+  inversion 1; subst; inversion 1; subst.
+  econstructor; intros. apply H4 in H6; inv_exists. simplify.
+  eapply merge_arr_empty'' in H6; eauto.
+  apply H5 in H6. pose proof H6. apply H2 in H7.
+  unfold merge_arrs. rewrite AssocMap.gcombine; auto. setoid_rewrite H6.
+  setoid_rewrite H7. auto.
+Qed.
+Hint Resolve merge_arr_empty2 : mgen.
+
+Lemma find_assocmap_gso :
+  forall ar x y v, x <> y -> (ar # y <- v) # x = ar # x.
+Proof.
+  unfold find_assocmap, AssocMapExt.get_default; intros; rewrite AssocMap.gso; auto.
+Qed.
+
+Lemma find_assocmap_gss :
+  forall ar x v, (ar # x <- v) # x = v.
+Proof.
+  unfold find_assocmap, AssocMapExt.get_default; intros; rewrite AssocMap.gss; auto.
+Qed.
+
+Lemma expr_lt_max_module_datapath :
+  forall m x,
+    max_reg_stmnt x <= max_stmnt_tree (mod_datapath m) ->
+    max_reg_stmnt x < max_reg_module m + 1.
+Proof. unfold max_reg_module. lia. Qed.
+
+Lemma expr_lt_max_module_controllogic :
+  forall m x,
+    max_reg_stmnt x <= max_stmnt_tree (mod_controllogic m) ->
+    max_reg_stmnt x < max_reg_module m + 1.
+Proof. unfold max_reg_module. lia. Qed.
+
+Lemma int_eq_not :
+  forall x y, Int.eq x y = true -> Int.eq x (Int.not y) = false.
+Proof.
+  intros. pose proof (Int.eq_spec x y). rewrite H in H0. subst.
+  apply int_eq_not_false.
+Qed.
+
+Lemma match_assocmaps_gt2 :
+  forall (p s : positive) (ra ra' : assocmap) (v : value),
+  p <= s -> match_assocmaps p ra ra' -> match_assocmaps p (ra # s <- v) ra'.
+Proof.
+  intros; inv H0; constructor; intros.
+  destruct (Pos.eq_dec r s); subst. lia.
+  rewrite AssocMap.gso by lia. auto.
+Qed.
+
+Lemma match_assocmaps_switch_neq :
+  forall p ra ra' r v' s v,
+    match_assocmaps p ra ((ra' # r <- v') # s <- v) ->
+    s <> r ->
+    match_assocmaps p ra ((ra' # s <- v) # r <- v').
+Proof.
+  inversion 1; constructor; simplify.
+  destruct (Pos.eq_dec r0 s); destruct (Pos.eq_dec r0 r); subst; try lia.
+  rewrite AssocMap.gso by lia. specialize (H0 s). apply H0 in H5.
+  rewrite AssocMap.gss in H5. rewrite AssocMap.gss. auto.
+  rewrite AssocMap.gss. apply H0 in H5. rewrite AssocMap.gso in H5 by lia.
+  rewrite AssocMap.gss in H5. auto.
+  repeat rewrite AssocMap.gso by lia.
+  apply H0 in H5. repeat rewrite AssocMap.gso in H5 by lia.
+  auto.
+Qed.
+
+Lemma match_assocmaps_duplicate :
+  forall p ra ra' v' s v,
+    match_assocmaps p ra (ra' # s <- v) ->
+    match_assocmaps p ra ((ra' # s <- v') # s <- v).
+Proof.
+  inversion 1; constructor; simplify.
+  destruct (Pos.eq_dec r s); subst.
+  rewrite AssocMap.gss. apply H0 in H4. rewrite AssocMap.gss in H4. auto.
+  repeat rewrite AssocMap.gso by lia. apply H0 in H4. rewrite AssocMap.gso in H4 by lia.
+  auto.
+Qed.
+
+Lemma translation_correct :
+  forall m asr nasa1 basa1 nasr1 basr1 basr2 nasr2 nasa2 basa2 nasr3 basr3
+         nasa3 basa3 asr'0 asa'0 res' st tge pstval sf asa ctrl data f,
+    asr ! (mod_reset m) = Some (ZToValue 0) ->
+    asr ! (mod_finish m) = Some (ZToValue 0) ->
+    asr ! (mod_st m) = Some (posToValue st) ->
+    (mod_controllogic m) ! st = Some ctrl ->
+    (mod_datapath m) ! st = Some data ->
+    stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := empty_assocmap |}
+               {| assoc_blocking := asa; assoc_nonblocking := empty_stack m |} ctrl
+               {| assoc_blocking := basr1; assoc_nonblocking := nasr1 |}
+               {| assoc_blocking := basa1; assoc_nonblocking := nasa1 |} ->
+    basr1 ! (mod_st m) = Some (posToValue st) ->
+    stmnt_runp f {| assoc_blocking := basr1; assoc_nonblocking := nasr1 |}
+               {| assoc_blocking := basa1; assoc_nonblocking := nasa1 |} data
+               {| assoc_blocking := basr2; assoc_nonblocking := nasr2 |}
+               {| assoc_blocking := basa2; assoc_nonblocking := nasa2 |} ->
+    exec_ram {| assoc_blocking := merge_regs nasr2 basr2; assoc_nonblocking := empty_assocmap |}
+             {| assoc_blocking := merge_arrs nasa2 basa2; assoc_nonblocking := empty_stack m |} None
+             {| assoc_blocking := basr3; assoc_nonblocking := nasr3 |}
+             {| assoc_blocking := basa3; assoc_nonblocking := nasa3 |} ->
+    (merge_regs nasr3 basr3) ! (mod_st m) = Some (posToValue pstval) ->
+    (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 ->
+    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.
+Proof.
+  Ltac tac0 :=
+    repeat match goal with
+           | H: match_reg_assocs _ _ _ |- _ => inv H
+           | H: match_arr_assocs _ _ |- _ => inv H
+           end.
+  intros.
+  repeat match goal with
+  | H: match_states _ _ |- _ => inv H
+  | H: context[exec_ram] |- _ => inv H
+  | H: mod_ram _ = None |- _ =>
+    let H2 := fresh "TRANSF" in learn H as H2; apply transf_module_code in H2
+  end.
+  eapply transf_code_alternatives in TRANSF; eauto; simplify; unfold alternatives in *.
+  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; 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 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.
+    exploit match_states_same; try solve [eapply H6 | eapply max_stmnt_lt_module; eauto
+                                          | 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; 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 eauto with mgen.
+    do 2 econstructor. apply Smallstep.plus_one. econstructor.
+    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; try discriminate; []. 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.
+    eapply int_eq_not_changed with (ar' := rab'1) in DISABLE_RAM; try congruence.
+    rewrite AssocMap.gempty in R2. rewrite <- R2 in R4.
+    rewrite AssocMap.gempty in R2'. rewrite <- R2' in R4'.
+    eapply int_eq_not_changed in DISABLE_RAM; auto. repeat (rewrite merge_find_assocmap; try congruence).
+    eapply max_reg_module_datapath_gt; eauto; remember (max_reg_module m); lia.
+    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.
+    eapply max_reg_module_datapath_gt; eauto; remember (max_reg_module m); lia.
+    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. 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 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.
+    eapply int_eq_not_changed with (ar' := rab'1) in DISABLE_RAM; try congruence.
+    rewrite AssocMap.gempty in R2. rewrite <- R2 in R4.
+    rewrite AssocMap.gempty in R2'. rewrite <- R2' in R4'.
+    eapply int_eq_not_changed in DISABLE_RAM; auto. repeat (rewrite merge_find_assocmap; try congruence).
+    eapply max_reg_module_datapath_gt; eauto; remember (max_reg_module m); lia.
+    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.
+    eapply max_reg_module_datapath_gt; eauto; remember (max_reg_module m); lia.
+    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 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. 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.
+    auto. auto. auto. econstructor. econstructor. econstructor.
+    econstructor. econstructor. econstructor. econstructor.
+    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. 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.
+
+    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 H12 as X.
+      eapply max_reg_stmnt_not_modified_nb with (r := (max_reg_module m + 2)) 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.
+    }
+    3: {
+      simplify. unfold merge_regs. repeat rewrite AssocMapExt.merge_add_assoc.
+      repeat rewrite AssocMap.gso by lia. apply AssocMap.gss.
+    }
+    { unfold disable_ram in *. unfold transf_module in DISABLE_RAM;
+                               repeat destruct_match; try discriminate.
+      simplify.
+      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.
+      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. 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. simplify. remember (max_reg_module m). lia.
+      apply max_reg_stmnt_le_stmnt_tree in H2.
+      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.
+      repeat rewrite AssocMap.gso by lia. apply AssocMap.gss.
+    }
+    solve [auto].
+    simplify. unfold merge_regs. repeat rewrite AssocMapExt.merge_add_assoc.
+    repeat rewrite AssocMap.gso by lia. apply AssocMap.gss.
+    simplify. unfold merge_regs. repeat rewrite AssocMapExt.merge_add_assoc.
+    repeat rewrite AssocMap.gso by lia. apply AssocMap.gss.
+    simplify. auto.
+    simplify. auto.
+    unfold merge_regs. repeat rewrite AssocMapExt.merge_add_assoc.
+    unfold_merge.
+    assert (mod_st (transf_module m) < max_reg_module m + 1).
+    { unfold max_reg_module, transf_module; repeat destruct_match; try discriminate; simplify; lia. }
+    remember (max_reg_module m).
+    repeat rewrite AssocMap.gso by lia.
+    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 H19 as X.
+    eapply match_assocmaps_merge in X.
+    2: { apply H21. }
+    inv X. rewrite <- H14. eassumption. unfold transf_module in H6; repeat destruct_match;
+                                        try discriminate; simplify.
+    lia. auto.
+
+    econstructor. unfold merge_regs. repeat rewrite AssocMapExt.merge_add_assoc.
+    rewrite AssocMapExt.merge_base_1.
+    remember (max_reg_module m).
+    repeat (apply match_assocmaps_gt; [lia|]).
+    solve [eauto with mgen].
+
+    apply merge_arr_empty. apply match_empty_size_merge.
+    apply match_empty_assocmap_set.
+    eapply match_arrs_size_stmnt_preserved in H4; mgen_crush.
+    eapply match_arrs_size_stmnt_preserved in H4; mgen_crush.
+    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 H12; mgen_crush.
+    rewrite empty_stack_transf. mgen_crush.
+    eapply match_arrs_size_stmnt_preserved in H12; mgen_crush.
+    rewrite empty_stack_transf. mgen_crush.
+    auto.
+    apply merge_arr_empty_match.
+    apply match_empty_size_merge. apply match_empty_assocmap_set.
+    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 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.
+    remember (max_reg_module m).
+    rewrite find_assocmap_gss.
+    repeat rewrite find_assocmap_gso by lia.
+    rewrite find_assocmap_gss. apply Int.eq_true.
+  - unfold alt_load in *; simplify. inv H6.
+    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.
+    solve [eauto with mgen]. econstructor. econstructor. econstructor.
+    econstructor. econstructor. auto. auto. auto.
+    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.
+    2: {
+      unfold merge_regs. unfold_merge. repeat rewrite find_assocmap_gso; try (remember (max_reg_module m); lia).
+      auto. unfold max_reg_module. lia.
+    }
+    2: {
+      unfold merge_regs. unfold_merge. rewrite AssocMap.gso by lia. rewrite AssocMap.gso by lia.
+      rewrite AssocMap.gss. auto.
+    }
+    { unfold disable_ram, transf_module in DISABLE_RAM;
+      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. eassumption. mgen_crush. }
+    { crush. }
+    { crush. }
+    { unfold merge_regs. unfold_merge.
+      unfold transf_module; repeat destruct_match; try discriminate; simplify.
+      assert (mod_st m < max_reg_module m + 1).
+      { unfold max_reg_module; lia. }
+      remember (max_reg_module m). repeat rewrite AssocMap.gso by lia.
+      apply AssocMap.gss.
+    }
+    { auto. }
+
+    { econstructor.
+      { unfold merge_regs. unfold_merge.
+        assert (mod_reset 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_reset m).
+        { 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 <- 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).
+        { 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 <- H19. auto. lia.
+      }
+      { unfold merge_regs. unfold_merge.
+        assert (mod_st m < max_reg_module m + 1).
+        { unfold max_reg_module; lia. }
+        unfold transf_module; repeat destruct_match; try discriminate; simplify.
+        repeat rewrite AssocMap.gso by lia. apply AssocMap.gss.
+      }
+      { eassumption. }
+      { eassumption. }
+      { econstructor. econstructor. simplify. unfold merge_regs. unfold_merge.
+        eapply expr_runp_matches. eassumption.
+        assert (max_reg_expr x0 + 1 <= max_reg_module m + 1).
+        { pose proof H2 as X. apply max_reg_stmnt_le_stmnt_tree in X.
+          apply expr_lt_max_module_controllogic in X. simplify. remember (max_reg_module m). lia. }
+        assert (max_reg_expr x0 + 1 <= mod_st m).
+        { unfold module_ordering in *. simplify.
+          repeat match goal with
+                 | H: context[_ <? _] |- _ => apply Pos.ltb_lt in H
+                 end.
+          pose proof H2 as X. apply max_reg_stmnt_le_stmnt_tree in X.
+          simplify. lia.
+        }
+        remember (max_reg_module m).
+        apply match_assocmaps_gt; [lia|].
+        apply match_assocmaps_gt; [lia|].
+        apply match_assocmaps_gt; [lia|].
+        apply match_assocmaps_gt; [lia|].
+        apply match_assocmaps_gt; [lia|].
+        apply match_assocmaps_gt; [lia|].
+        simplify.
+        eapply match_assocmaps_ge. eauto. lia.
+        mgen_crush.
+      }
+      { simplify. unfold merge_regs. unfold_merge.
+        unfold transf_module; repeat destruct_match; try discriminate; simplify.
+        assert (mod_st m < max_reg_module m + 1).
+        { unfold max_reg_module; lia. }
+        remember (max_reg_module m).
+        repeat rewrite AssocMap.gso by lia. apply AssocMap.gss.
+      }
+      {
+        simplify. econstructor. econstructor. econstructor. simplify.
+        unfold merge_regs; unfold_merge.
+        repeat rewrite find_assocmap_gso by lia. apply find_assocmap_gss.
+      }
+      { simplify. rewrite empty_stack_transf.
+        unfold transf_module; repeat destruct_match; try discriminate; simplify.
+        econstructor. simplify.
+        unfold merge_regs; unfold_merge. simplify.
+        assert (r < max_reg_module m + 1).
+        { pose proof H3 as X. eapply max_reg_module_datapath_gt with (p := max_reg_module m + 1) in X.
+          unfold max_reg_stmnt in X. simplify.
+          lia. lia. }
+        assert (mod_st m < max_reg_module m + 1).
+        { unfold max_reg_module; lia. }
+        repeat rewrite find_assocmap_gso by lia. rewrite find_assocmap_gss.
+        repeat rewrite find_assocmap_gso by lia. rewrite find_assocmap_gss.
+        apply Int.eq_true.
+      }
+      { crush. }
+      { crush. }
+      { unfold merge_regs. unfold_merge. simplify.
+        assert (r < mod_st m).
+        { unfold module_ordering in *. simplify.
+          repeat match goal with
+                 | H: context[_ <? _] |- _ => apply Pos.ltb_lt in H
+                 end.
+          pose proof H3 as X. apply max_reg_stmnt_le_stmnt_tree in X.
+          simplify. lia.
+        }
+        unfold merge_regs in H8. repeat rewrite AssocMapExt.merge_add_assoc in H8.
+        simplify. rewrite AssocMap.gso in H8 by lia. rewrite AssocMap.gss in H8.
+        unfold transf_module; repeat destruct_match; try discriminate; simplify.
+        repeat rewrite AssocMap.gso by lia.
+        apply AssocMap.gss. }
+      { eassumption. }
+    }
+    { eauto. }
+    { econstructor.
+      { unfold merge_regs. unfold_merge. simplify.
+        apply match_assocmaps_gss.
+        unfold merge_regs in H8. repeat rewrite AssocMapExt.merge_add_assoc in H8.
+        rewrite AssocMap.gso in H8. rewrite AssocMap.gss in H8. inv H8.
+        remember (max_reg_module m).
+        assert (mod_st m < max_reg_module m + 1).
+        { unfold max_reg_module; lia. }
+        apply match_assocmaps_switch_neq; [|lia].
+        apply match_assocmaps_gt; [lia|].
+        apply match_assocmaps_switch_neq; [|lia].
+        apply match_assocmaps_gt; [lia|].
+        apply match_assocmaps_switch_neq; [|lia].
+        apply match_assocmaps_gt; [lia|].
+        apply match_assocmaps_switch_neq; [|lia].
+        apply match_assocmaps_gt; [lia|].
+        apply match_assocmaps_switch_neq; [|lia].
+        apply match_assocmaps_gt; [lia|].
+        apply match_assocmaps_duplicate.
+        apply match_assocmaps_gss. auto.
+        assert (r < mod_st m).
+        { unfold module_ordering in *. simplify.
+          repeat match goal with
+                 | H: context[_ <? _] |- _ => apply Pos.ltb_lt in H
+                 end.
+          pose proof H3 as X. apply max_reg_stmnt_le_stmnt_tree in X.
+          simplify. lia.
+        } lia.
+      }
+      {
+        apply merge_arr_empty. mgen_crush.
+        apply merge_arr_empty2. mgen_crush.
+        apply merge_arr_empty2. mgen_crush.
+        apply merge_arr_empty2. mgen_crush.
+        mgen_crush.
+      }
+      { auto. }
+      { mgen_crush. }
+      { mgen_crush. }
+      { unfold disable_ram.
+        unfold transf_module; repeat destruct_match; try discriminate; simplify.
+        unfold merge_regs. unfold_merge. simplify.
+        assert (mod_st m < max_reg_module m + 1).
+        { unfold max_reg_module; lia. }
+        assert (r < max_reg_module m + 1).
+        { pose proof H3 as X. eapply max_reg_module_datapath_gt with (p := max_reg_module m + 1) in X.
+          unfold max_reg_stmnt in X. simplify.
+          lia. lia. }
+        repeat rewrite find_assocmap_gso by lia.
+        rewrite find_assocmap_gss.
+        repeat rewrite find_assocmap_gso by lia.
+        rewrite find_assocmap_gss. apply Int.eq_true.
+      }
+    }
+Qed.
+
+Lemma exec_ram_resets_en :
+  forall rs ar rs' ar' r,
+    exec_ram rs ar (Some r) rs' ar' ->
+    assoc_nonblocking rs = empty_assocmap ->
+    Int.eq ((assoc_blocking (merge_reg_assocs rs')) # (ram_en r, 32))
+           ((assoc_blocking (merge_reg_assocs rs')) # (ram_u_en r, 32)) = true.
+Proof.
+  inversion 1; intros; subst; unfold merge_reg_assocs; simplify.
+  - rewrite H6. mgen_crush.
+  - unfold merge_regs. rewrite H12. unfold_merge.
+    unfold find_assocmap, AssocMapExt.get_default in *.
+    rewrite AssocMap.gss; auto. rewrite AssocMap.gso; auto. setoid_rewrite H4. apply Int.eq_true.
+    pose proof (ram_ordering r); lia.
+  - unfold merge_regs. rewrite H11. unfold_merge.
+    unfold find_assocmap, AssocMapExt.get_default in *.
+    rewrite AssocMap.gss; auto.
+    repeat rewrite AssocMap.gso by (pose proof (ram_ordering r); lia).
+    setoid_rewrite H3. apply Int.eq_true.
+Qed.
+
+Lemma disable_ram_set_gso :
+  forall rs r i v,
+    disable_ram (Some r) rs ->
+    i <> (ram_en r) -> i <> (ram_u_en r) ->
+    disable_ram (Some r) (rs # i <- v).
+Proof.
+  unfold disable_ram, find_assocmap, AssocMapExt.get_default; intros;
+  repeat rewrite AssocMap.gso by lia; auto.
+Qed.
+Hint Resolve disable_ram_set_gso : mgen.
+
+Lemma disable_ram_None rs : disable_ram None rs.
+Proof. unfold disable_ram; auto. Qed.
+Hint Resolve disable_ram_None : mgen.
+
+Lemma init_regs_equal_empty l st :
+  Forall (Pos.gt st) l -> (init_regs nil l) ! st = None.
+Proof. induction l; simplify; apply AssocMap.gempty. Qed.
+
+Lemma forall_lt_num :
+  forall l p p', Forall (Pos.gt p) l -> p < p' -> Forall (Pos.gt p') l.
+Proof. induction l; crush; inv H; constructor; [lia | eauto]. Qed.
+
+Section CORRECTNESS.
+
+  Context (prog tprog: program).
+  Context (TRANSL: match_prog prog tprog).
+
+  Let ge : genv := Genv.globalenv prog.
+  Let tge : genv := Genv.globalenv tprog.
+
+  Lemma symbols_preserved:
+    forall (s: AST.ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
+  Proof using TRANSL. intros. eapply (Genv.find_symbol_match TRANSL). Qed.
+  Hint Resolve symbols_preserved : mgen.
+
+  Lemma function_ptr_translated:
+    forall (b: Values.block) (f: fundef),
+      Genv.find_funct_ptr ge b = Some f ->
+      exists tf,
+        Genv.find_funct_ptr tge b = Some tf /\ transf_fundef f = tf.
+  Proof using TRANSL.
+    intros. exploit (Genv.find_funct_ptr_match TRANSL); eauto.
+    intros (cu & tf & P & Q & R); exists tf; auto.
+  Qed.
+  Hint Resolve function_ptr_translated : mgen.
+
+  Lemma functions_translated:
+    forall (v: Values.val) (f: fundef),
+      Genv.find_funct ge v = Some f ->
+      exists tf,
+        Genv.find_funct tge v = Some tf /\ transf_fundef f = tf.
+  Proof using TRANSL.
+    intros. exploit (Genv.find_funct_match TRANSL); eauto.
+    intros (cu & tf & P & Q & R); exists tf; auto.
+  Qed.
+  Hint Resolve functions_translated : mgen.
+
+  Lemma senv_preserved:
+    Senv.equiv (Genv.to_senv ge) (Genv.to_senv tge).
+  Proof (Genv.senv_transf TRANSL).
+  Hint Resolve senv_preserved : mgen.
+
+  Theorem transf_step_correct:
+    forall (S1 : state) t S2,
+      step ge S1 t S2 ->
+      forall R1,
+        match_states S1 R1 ->
+        exists R2, Smallstep.plus step tge R1 t R2 /\ match_states S2 R2.
+  Proof.
+    Ltac transf_step_correct_assum :=
+      match goal with
+      | H: match_states _ _ |- _ => let H2 := fresh "MATCH" in learn H as H2; inv H2
+      | H: mod_ram ?m = Some ?r |- _ =>
+        let H2 := fresh "RAM" in learn H;
+          pose proof (transf_module_code_ram m r H) as H2
+      | H: mod_ram ?m = None |- _ =>
+        let H2 := fresh "RAM" in learn H;
+          pose proof (transf_module_code m H) as H2
+      end.
+    Ltac transf_step_correct_tac :=
+      match goal with
+      | |- Smallstep.plus _ _ _ _ _ => apply Smallstep.plus_one
+      end.
+    induction 1; destruct (mod_ram m) eqn:RAM; simplify; repeat transf_step_correct_assum;
+      repeat transf_step_correct_tac.
+    - 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).
+      { eapply match_arrs_size_stmnt_preserved2; mgen_crush. } simplify.
+      assert (MATCH_SIZE2: match_empty_size m nasa3 /\ match_empty_size m basa3).
+      { eapply match_arrs_size_ram_preserved2; mgen_crush. } simplify.
+      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 H18. inv H21.
+      exploit match_states_same. apply H6. eauto with mgen.
+      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 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 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.
+      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. }
+      simplify.
+      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_SIZE2': match_empty_size m ran'4 /\ match_empty_size m rab'4).
+      { eapply match_arrs_size_ram_preserved2; mgen_crush.
+        unfold match_empty_size, transf_module, empty_stack.
+        repeat destruct_match; crush. mgen_crush.  }
+      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 H21. unfold merge_reg_assocs in H21.
+      simplify. auto. auto.
+    - 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.
+    - 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).
+      replace (empty_stack (transf_module m)) with (empty_stack m) by (rewrite RAM0; auto).
+      replace (mod_params (transf_module m)) with (mod_params m) by (rewrite RAM0; auto).
+      replace (mod_st (transf_module m)) with (mod_st m) by (rewrite RAM0; auto).
+      repeat econstructor; mgen_crush.
+      unfold disable_ram. unfold transf_module; repeat destruct_match; crush.
+      pose proof (mod_ordering_wf m); unfold module_ordering in *.
+      pose proof (mod_params_wf m).
+      pose proof (mod_ram_wf m r Heqo0).
+      pose proof (ram_ordering r).
+      simplify.
+      repeat rewrite find_assocmap_gso by lia.
+      assert ((init_regs nil (mod_params m)) ! (ram_en r) = None).
+      { 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 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).
+      replace (mod_finish (transf_module m)) with (mod_finish m).
+      replace (empty_stack (transf_module m)) with (empty_stack m).
+      replace (mod_params (transf_module m)) with (mod_params m).
+      replace (mod_st (transf_module m)) with (mod_st m).
+      all: try solve [unfold transf_module; repeat destruct_match; mgen_crush].
+      repeat econstructor; mgen_crush.
+      unfold disable_ram. unfold transf_module; repeat destruct_match; crush.
+      unfold max_reg_module.
+      repeat rewrite find_assocmap_gso by lia.
+      assert (max_reg_module m + 1 > max_list (mod_params m)).
+      { unfold max_reg_module. lia. }
+      apply max_list_correct in H0.
+      unfold find_assocmap, AssocMapExt.get_default.
+      rewrite init_regs_equal_empty. rewrite init_regs_equal_empty. auto.
+      eapply forall_lt_num. eassumption. unfold max_reg_module. lia.
+      eapply forall_lt_num. eassumption. unfold max_reg_module. lia.
+    - inv STACKS. destruct b1; subst.
+      econstructor. econstructor. apply Smallstep.plus_one.
+      econstructor. eauto.
+      clear Learn. inv H0. inv H3. inv STACKS. inv H3. constructor.
+      constructor. intros.
+      rewrite RAM0.
+      destruct (Pos.eq_dec r res); subst.
+      rewrite AssocMap.gss.
+      rewrite AssocMap.gss. auto.
+      rewrite AssocMap.gso; auto.
+      symmetry. rewrite AssocMap.gso; auto.
+      destruct (Pos.eq_dec (mod_st m) r); subst.
+      rewrite AssocMap.gss.
+      rewrite AssocMap.gss. auto.
+      rewrite AssocMap.gso; 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.
+      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). 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.
+    - inv STACKS. destruct b1; subst.
+      econstructor. econstructor. apply Smallstep.plus_one.
+      econstructor. eauto.
+      clear Learn. inv H0. inv H3. inv STACKS. constructor.
+      constructor. intros.
+      unfold transf_module. repeat destruct_match; crush.
+      destruct (Pos.eq_dec r res); subst.
+      rewrite AssocMap.gss.
+      rewrite AssocMap.gss. auto.
+      rewrite AssocMap.gso; auto.
+      symmetry. rewrite AssocMap.gso; auto.
+      destruct (Pos.eq_dec (mod_st m) r); subst.
+      rewrite AssocMap.gss.
+      rewrite AssocMap.gss. auto.
+      rewrite AssocMap.gso; auto.
+      symmetry. rewrite AssocMap.gso; auto. inv MATCH_ASSOC. apply H. auto.
+      auto. auto. auto. auto.
+      Opaque disable_ram.
+      unfold transf_module in *; repeat destruct_match; crush.
+      apply disable_ram_set_gso.
+      apply disable_ram_set_gso.
+      auto.
+      simplify. unfold max_reg_module. lia.
+      simplify. unfold max_reg_module. lia.
+      simplify. unfold max_reg_module. lia.
+      simplify. unfold max_reg_module. lia.
+  Qed.
+  Hint Resolve transf_step_correct : mgen.
+
+  Lemma transf_initial_states :
+    forall s1 : state,
+      initial_state prog s1 ->
+      exists s2 : state,
+        initial_state tprog s2 /\ match_states s1 s2.
+  Proof using TRANSL.
+    simplify. inv H.
+    exploit function_ptr_translated. eauto. intros.
+    inv H. inv H3.
+    econstructor. econstructor. econstructor.
+    eapply (Genv.init_mem_match TRANSL); eauto.
+    setoid_rewrite (Linking.match_program_main TRANSL).
+    rewrite symbols_preserved. eauto.
+    eauto.
+    econstructor.
+  Qed.
+  Hint Resolve transf_initial_states : mgen.
+
+  Lemma transf_final_states :
+    forall (s1 : state)
+           (s2 : state)
+           (r : Int.int),
+      match_states s1 s2 ->
+      final_state s1 r ->
+      final_state s2 r.
+  Proof using TRANSL.
+    intros. inv H0. inv H. inv STACKS. unfold valueToInt. constructor. auto.
+  Qed.
+  Hint Resolve transf_final_states : mgen.
+
+  Theorem transf_program_correct:
+    Smallstep.forward_simulation (semantics prog) (semantics tprog).
+  Proof using TRANSL.
+    eapply Smallstep.forward_simulation_plus; mgen_crush.
+    apply senv_preserved.
+  Qed.
+
+End CORRECTNESS.
diff --git a/src/hls/Partition.ml b/src/hls/Partition.ml
deleted file mode 100644
index 19c6048..0000000
--- a/src/hls/Partition.ml
+++ /dev/null
@@ -1,124 +0,0 @@
- (*
- * Vericert: Verified high-level synthesis.
- * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com>
- *
- * This program is free software: you can redistribute it and/or modify
- * it under the terms of the GNU General Public License as published by
- * the Free Software Foundation, either version 3 of the License, or
- * (at your option) any later version.
- *
- * This program is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with this program.  If not, see <https://www.gnu.org/licenses/>.
- *)
-
-open Printf
-open Clflags
-open Camlcoq
-open Datatypes
-open Coqlib
-open Maps
-open AST
-open Kildall
-open Op
-open RTLBlockInstr
-open RTLBlock
-
-(* Assuming that the nodes of the CFG [code] are numbered in reverse postorder (cf. pass
-   [Renumber]), an edge from [n] to [s] is a normal edge if [s < n] and a back-edge otherwise. *)
-let find_edge i n =
-  let succ = RTL.successors_instr i in
-  let filt = List.filter (fun s -> P.lt n s || P.lt s (P.pred n)) succ in
-  ((match filt with [] -> [] | _ -> [n]), filt)
-
-let find_edges c =
-  PTree.fold (fun l n i ->
-      let f = find_edge i n in
-      (List.append (fst f) (fst l), List.append (snd f) (snd l))) c ([], [])
-
-let prepend_instr i = function
-  | {bb_body = bb; bb_exit = e} -> {bb_body = (i :: bb); bb_exit = e}
-
-let translate_inst = function
-  | RTL.Inop _ -> Some RBnop
-  | RTL.Iop (op, ls, dst, _) -> Some (RBop (None, op, ls, dst))
-  | RTL.Iload (m, addr, ls, dst, _) -> Some (RBload (None, m, addr, ls, dst))
-  | RTL.Istore (m, addr, ls, src, _) -> Some (RBstore (None, m, addr, ls, src))
-  | _ -> None
-
-let translate_cfi = function
-  | RTL.Icall (s, r, ls, dst, n) -> Some (RBcall (s, r, ls, dst, n))
-  | RTL.Itailcall (s, r, ls) -> Some (RBtailcall (s, r, ls))
-  | RTL.Ibuiltin (e, ls, r, n) -> Some (RBbuiltin (e, ls, r, n))
-  | RTL.Icond (c, ls, dst1, dst2) -> Some (RBcond (c, ls, dst1, dst2))
-  | RTL.Ijumptable (r, ls) -> Some (RBjumptable (r, ls))
-  | RTL.Ireturn r -> Some (RBreturn r)
-  | _ -> None
-
-let rec next_bblock_from_RTL is_start e (c : RTL.code) s i =
-  let succ = List.map (fun i -> (i, PTree.get i c)) (RTL.successors_instr i) in
-  let trans_inst = (translate_inst i, translate_cfi i) in
-  match trans_inst, succ with
-  | (None, Some i'), _ ->
-    if List.exists (fun x -> x = s) (snd e) && not is_start then
-      Errors.OK { bb_body = []; bb_exit = RBgoto s }
-    else
-      Errors.OK { bb_body = []; bb_exit = i' }
-  | (Some i', None), (s', Some i_n)::[] ->
-    if List.exists (fun x -> x = s) (fst e) then
-      Errors.OK { bb_body = [i']; bb_exit = RBgoto s' }
-    else if List.exists (fun x -> x = s) (snd e) && not is_start then
-      Errors.OK { bb_body = []; bb_exit = RBgoto s }
-    else begin
-      match next_bblock_from_RTL false e c s' i_n with
-      | Errors.OK bb ->
-        Errors.OK (prepend_instr i' bb)
-      | Errors.Error msg -> Errors.Error msg
-    end
-  | _, _ ->
-    Errors.Error (Errors.msg (coqstring_of_camlstring "next_bblock_from_RTL went wrong."))
-
-let rec traverseacc f l c =
-  match l with
-  | [] -> Errors.OK c
-  | x::xs ->
-    match f x c with
-    | Errors.Error msg -> Errors.Error msg
-    | Errors.OK x' ->
-      match traverseacc f xs x' with
-      | Errors.Error msg -> Errors.Error msg
-      | Errors.OK xs' -> Errors.OK xs'
-
-let rec translate_all edge c s res =
-  let c_bb, translated = res in
-  if List.exists (fun x -> P.eq x s) translated then Errors.OK (c_bb, translated) else
-    (match PTree.get s c with
-     | None -> Errors.Error (Errors.msg (coqstring_of_camlstring "Could not translate all."))
-     | Some i ->
-       match next_bblock_from_RTL true edge c s i with
-       | Errors.Error msg -> Errors.Error msg
-       | Errors.OK {bb_body = bb; bb_exit = e} ->
-         let succ = List.filter (fun x -> P.lt x s) (successors_instr e) in
-         (match traverseacc (translate_all edge c) succ (c_bb, s :: translated) with
-          | Errors.Error msg -> Errors.Error msg
-          | Errors.OK (c', t') ->
-            Errors.OK (PTree.set s {bb_body = bb; bb_exit = e} c', t')))
-
-(* Partition a function and transform it into RTLBlock. *)
-let function_from_RTL f =
-  let e = find_edges f.RTL.fn_code in
-  match translate_all e f.RTL.fn_code f.RTL.fn_entrypoint (PTree.empty, []) with
-  | Errors.Error msg -> Errors.Error msg
-  | Errors.OK (c, _) ->
-    Errors.OK { fn_sig = f.RTL.fn_sig;
-                fn_stacksize = f.RTL.fn_stacksize;
-                fn_params = f.RTL.fn_params;
-                fn_entrypoint = f.RTL.fn_entrypoint;
-                fn_code = c
-              }
-
-let partition = function_from_RTL
diff --git a/src/hls/PrintRTLBlock.ml b/src/hls/PrintRTLBlock.ml
deleted file mode 100644
index 8fef401..0000000
--- a/src/hls/PrintRTLBlock.ml
+++ /dev/null
@@ -1,72 +0,0 @@
-(* *********************************************************************)
-(*                                                                     *)
-(*              The Compcert verified compiler                         *)
-(*                                                                     *)
-(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
-(*                                                                     *)
-(*  Copyright Institut National de Recherche en Informatique et en     *)
-(*  Automatique.  All rights reserved.  This file is distributed       *)
-(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
-(*                                                                     *)
-(* *********************************************************************)
-
-(** Pretty-printers for RTL code *)
-
-open Printf
-open Camlcoq
-open Datatypes
-open Maps
-open AST
-open RTLBlockInstr
-open RTLBlock
-open PrintAST
-open PrintRTLBlockInstr
-
-(* Printing of RTL code *)
-
-let reg pp r =
-  fprintf pp "x%d" (P.to_int r)
-
-let rec regs pp = function
-  | [] -> ()
-  | [r] -> reg pp r
-  | r1::rl -> fprintf pp "%a, %a" reg r1 regs rl
-
-let ros pp = function
-  | Coq_inl r -> reg pp r
-  | Coq_inr s -> fprintf pp "\"%s\"" (extern_atom s)
-
-let print_bblock pp (pc, i) =
-  fprintf pp "%5d:{\n" pc;
-  List.iter (print_bblock_body pp) i.bb_body;
-  print_bblock_exit pp i.bb_exit;
-  fprintf pp "\t}\n\n"
-
-let print_function pp id f =
-  fprintf pp "%s(%a) {\n" (extern_atom id) regs f.fn_params;
-  let instrs =
-    List.sort
-      (fun (pc1, _) (pc2, _) -> compare pc2 pc1)
-      (List.rev_map
-        (fun (pc, i) -> (P.to_int pc, i))
-        (PTree.elements f.fn_code)) in
-  List.iter (print_bblock pp) instrs;
-  fprintf pp "}\n\n"
-
-let print_globdef pp (id, gd) =
-  match gd with
-  | Gfun(Internal f) -> print_function pp id f
-  | _ -> ()
-
-let print_program pp (prog: program) =
-  List.iter (print_globdef pp) prog.prog_defs
-
-let destination : string option ref = ref None
-
-let print_if passno prog =
-  match !destination with
-  | None -> ()
-  | Some f ->
-     let oc = open_out (f ^ "." ^ Z.to_string passno) in
-     print_program oc prog;
-     close_out oc
diff --git a/src/hls/PrintRTLBlockInstr.ml b/src/hls/PrintRTLBlockInstr.ml
deleted file mode 100644
index ba7241b..0000000
--- a/src/hls/PrintRTLBlockInstr.ml
+++ /dev/null
@@ -1,87 +0,0 @@
-open Printf
-open Camlcoq
-open Datatypes
-open Maps
-open AST
-open RTLBlockInstr
-open PrintAST
-
-let reg pp r =
-  fprintf pp "x%d" (P.to_int r)
-
-let pred pp r =
-  fprintf pp "p%d" (Nat.to_int r)
-
-let rec regs pp = function
-  | [] -> ()
-  | [r] -> reg pp r
-  | r1::rl -> fprintf pp "%a, %a" reg r1 regs rl
-
-let ros pp = function
-  | Coq_inl r -> reg pp r
-  | Coq_inr s -> fprintf pp "\"%s\"" (extern_atom s)
-
-let rec print_pred_op pp = function
-  | Pvar p -> pred pp p
-  | Pnot p -> fprintf pp "(~ %a)" print_pred_op p
-  | Pand (p1, p2) -> fprintf pp "(%a & %a)" print_pred_op p1 print_pred_op p2
-  | Por (p1, p2) -> fprintf pp "(%a | %a)" print_pred_op p1 print_pred_op p2
-
-let print_pred_option pp = function
-  | Some x -> fprintf pp "(%a)" print_pred_op x
-  | None -> ()
-
-let print_bblock_body pp i =
-  fprintf pp "\t\t";
-  match i with
-  | RBnop -> fprintf pp "nop\n"
-  | RBop(p, op, ls, dst) ->
-     fprintf pp "%a %a = %a\n"
-       print_pred_option p reg dst (PrintOp.print_operation reg) (op, ls)
-  | RBload(p, chunk, addr, args, dst) ->
-     fprintf pp "%a %a = %s[%a]\n"
-       print_pred_option p reg dst (name_of_chunk chunk)
-       (PrintOp.print_addressing reg) (addr, args)
-  | RBstore(p, chunk, addr, args, src) ->
-     fprintf pp "%a %s[%a] = %a\n"
-       print_pred_option p
-       (name_of_chunk chunk)
-       (PrintOp.print_addressing reg) (addr, args)
-       reg src
-  | RBsetpred (c, args, p) ->
-    fprintf pp "%a = %a\n"
-      pred p
-      (PrintOp.print_condition reg) (c, args)
-
-let rec print_bblock_exit pp i =
-  fprintf pp "\t\t";
-  match i with
-  | RBcall(_, fn, args, res, _) ->
-      fprintf pp "%a = %a(%a)\n"
-        reg res ros fn regs args;
-  | RBtailcall(_, fn, args) ->
-      fprintf pp "tailcall %a(%a)\n"
-        ros fn regs args
-  | RBbuiltin(ef, args, res, _) ->
-      fprintf pp "%a = %s(%a)\n"
-        (print_builtin_res reg) res
-        (name_of_external ef)
-        (print_builtin_args reg) args
-  | RBcond(cond, args, s1, s2) ->
-      fprintf pp "if (%a) goto %d else goto %d\n"
-        (PrintOp.print_condition reg) (cond, args)
-        (P.to_int s1) (P.to_int s2)
-  | RBjumptable(arg, tbl) ->
-      let tbl = Array.of_list tbl in
-      fprintf pp "jumptable (%a)\n" reg arg;
-      for i = 0 to Array.length tbl - 1 do
-        fprintf pp "\tcase %d: goto %d\n" i (P.to_int tbl.(i))
-      done
-  | RBreturn None ->
-      fprintf pp "return\n"
-  | RBreturn (Some arg) ->
-      fprintf pp "return %a\n" reg arg
-  | RBgoto n ->
-     fprintf pp "goto %d\n" (P.to_int n)
-  | RBpred_cf (p, c1, c2) ->
-    fprintf pp "if %a then (%a) else (%a)\n" print_pred_op p print_bblock_exit c1 print_bblock_exit c2
diff --git a/src/hls/PrintVerilog.ml b/src/hls/PrintVerilog.ml
index aeaf75c..a2700a1 100644
--- a/src/hls/PrintVerilog.ml
+++ b/src/hls/PrintVerilog.ml
@@ -118,7 +118,9 @@ let rec pprint_stmnt i =
                                   indent i; "end\n"
                                 ]
   | Vcase (e, es, d) -> concat [ indent i; "case ("; pprint_expr e; ")\n";
-                                 fold_map pprint_case (List.sort compare_expr es |> List.rev);
+                                 fold_map pprint_case (stmnt_to_list es
+                                                       |> List.sort compare_expr
+                                                       |> List.rev);
                                  indent (i+1); "default:;\n";
                                  indent i; "endcase\n"
                                ]
@@ -137,22 +139,22 @@ let pprint_edge_top i = function
   | Valledge -> "@*"
   | Voredge (e1, e2) -> concat ["@("; pprint_edge e1; " or "; pprint_edge e2; ")"]
 
-let declare t =
+let declare (t, i) =
   function (r, sz) ->
     concat [ t; " ["; sprintf "%d" (Nat.to_int sz - 1); ":0] ";
-             register r; ";\n" ]
+             register r; if i then " = 0;\n" else ";\n" ]
 
-let declarearr t =
+let declarearr (t, _) =
   function (r, sz, ln) ->
     concat [ t; " ["; sprintf "%d" (Nat.to_int sz - 1); ":0] ";
              register r;
              " ["; sprintf "%d" (Nat.to_int ln - 1); ":0];\n" ]
 
 let print_io = function
-  | Some Vinput -> "input"
-  | Some Voutput -> "output reg"
-  | Some Vinout -> "inout"
-  | None -> "reg"
+  | Some Vinput -> "input", false
+  | Some Voutput -> "output reg", true
+  | Some Vinout -> "inout", false
+  | None -> "reg", true
 
 let decl i = function
   | Vdecl (io, r, sz) -> concat [indent i; declare (print_io io) (r, sz)]
@@ -162,11 +164,14 @@ let decl i = function
 let pprint_module_item i = function
   | Vdeclaration d -> decl i d
   | Valways (e, s) ->
-    concat [indent i; "always "; pprint_edge_top i e; "\n"; pprint_stmnt (i+1) s]
+    concat [indent i; "always "; pprint_edge_top i e; " begin\n";
+            pprint_stmnt (i+1) s; indent i; "end\n"]
   | Valways_ff (e, s) ->
-    concat [indent i; "always "; pprint_edge_top i e; "\n"; pprint_stmnt (i+1) s]
+    concat [indent i; "always "; pprint_edge_top i e; " begin\n";
+            pprint_stmnt (i+1) s; indent i; "end\n"]
   | Valways_comb (e, s) ->
-    concat [indent i; "always "; pprint_edge_top i e; "\n"; pprint_stmnt (i+1) s]
+    concat [indent i; "always "; pprint_edge_top i e; " begin\n";
+            pprint_stmnt (i+1) s; indent i; "end\n"]
 
 let rec intersperse c = function
   | [] -> []
@@ -245,7 +250,7 @@ let pprint_module debug i n m =
         ];
     concat [ indent i; "module "; (extern_atom n);
              "("; concat (intersperse ", " (List.map register (inputs @ outputs))); ");\n";
-             fold_map (pprint_module_item (i+1)) m.mod_body;
+             fold_map (pprint_module_item (i+1)) (List.rev m.mod_body);
              if !option_initial then print_initial i (Nat.to_int m.mod_stk_len) m.mod_stk else "";
              if debug then debug_always_verbose i m.mod_clk m.mod_st else "";
              indent i; "endmodule\n\n"
diff --git a/src/hls/RTLBlockInstr.v b/src/hls/RTLBlockInstr.v
index 86f8eba..5e123a3 100644
--- a/src/hls/RTLBlockInstr.v
+++ b/src/hls/RTLBlockInstr.v
@@ -211,9 +211,9 @@ Fixpoint trans_pred (bound: nat) (p: pred_op) :
   - apply orb_true_intro.
     apply satFormula_mult2 in H. inv H. apply i in H0. auto.
     apply i0 in H0. auto.
-Admitted.
+Abort.
 
-Definition sat_pred (bound: nat) (p: pred_op) :
+(*Definition sat_pred (bound: nat) (p: pred_op) :
   option ({al : alist | sat_predicate p (interp_alist al) = true}
           + {forall a : asgn, sat_predicate p a = false}).
   refine
@@ -243,7 +243,7 @@ Definition sat_pred_temp (bound: nat) (p: pred_op) :=
   match trans_pred_temp bound p with
   | Some fm => boundedSatSimple bound fm
   | None => None
-  end.
+  end.*)
 
 Inductive instr : Type :=
 | RBnop : instr
diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v
index e2e9a90..5ad3f90 100644
--- a/src/hls/RTLPargen.v
+++ b/src/hls/RTLPargen.v
@@ -473,9 +473,9 @@ Lemma sems_det:
   forall v v' mv mv',
   (sem_value A ge sp st f v /\ sem_value A tge sp st f v' -> v = v') /\
   (sem_mem A ge sp st f mv /\ sem_mem A tge sp st f mv' -> mv = mv').
-Proof. Admitted.
+Proof. Abort.
 
-Lemma sem_value_det:
+(*Lemma sem_value_det:
   forall A ge tge sp st f v v',
   ge_preserved ge tge ->
   sem_value A ge sp st f v ->
@@ -657,7 +657,7 @@ Lemma abstract_execution_correct:
     RTLBlock.step_instr_list ge sp (InstrState rs m) bb (InstrState rs' m') ->
     exists rs'', RTLPar.step_instr_block tge sp (InstrState rs m) bb' (InstrState rs'' m')
                  /\ regs_lessdef rs' rs''.
-Proof. Admitted.
+Proof. Abort.
 
 (*|
 Top-level functions
@@ -689,3 +689,4 @@ Definition transl_fundef := transf_partial_fundef transl_function_temp.
 
 Definition transl_program (p : RTLBlock.program) : Errors.res RTLPar.program :=
   transform_partial_program transl_fundef p.
+*)
diff --git a/src/hls/RTLPargenproof.v b/src/hls/RTLPargenproof.v
index eb7931e..a0c01fa 100644
--- a/src/hls/RTLPargenproof.v
+++ b/src/hls/RTLPargenproof.v
@@ -16,7 +16,7 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-Require Import compcert.backend.Registers.
+(*Require Import compcert.backend.Registers.
 Require Import compcert.common.AST.
 Require Import compcert.common.Errors.
 Require Import compcert.common.Linking.
@@ -286,3 +286,4 @@ Section CORRECTNESS.
   Qed.*)
 
 End CORRECTNESS.
+*)
diff --git a/src/hls/Schedule.ml b/src/hls/Schedule.ml
deleted file mode 100644
index c6c8bf4..0000000
--- a/src/hls/Schedule.ml
+++ /dev/null
@@ -1,801 +0,0 @@
-(*
- * Vericert: Verified high-level synthesis.
- * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com>
- *
- * This program is free software: you can redistribute it and/or modify
- * it under the terms of the GNU General Public License as published by
- * the Free Software Foundation, either version 3 of the License, or
- * (at your option) any later version.
- *
- * This program is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with this program.  If not, see <https://www.gnu.org/licenses/>.
- *)
-
-open Printf
-open Clflags
-open Camlcoq
-open Datatypes
-open Coqlib
-open Maps
-open AST
-open Kildall
-open Op
-open RTLBlockInstr
-open RTLBlock
-open HTL
-open Verilog
-open HTLgen
-open HTLMonad
-open HTLMonadExtra
-
-module SS = Set.Make(P)
-
-type svtype =
-  | BBType of int
-  | VarType of int * int
-
-type sv = {
-  sv_type: svtype;
-  sv_num: int;
-}
-
-let print_sv v =
-  match v with
-  | { sv_type = BBType bbi; sv_num = n } -> sprintf "bb%d_%d" bbi n
-  | { sv_type = VarType (bbi, i); sv_num = n } -> sprintf "var%dn%d_%d" bbi i n
-
-module G = Graph.Persistent.Digraph.ConcreteLabeled(struct
-  type t = sv
-  let compare = compare
-  let equal = (=)
-  let hash = Hashtbl.hash
-end)(struct
-  type t = int
-  let compare = compare
-  let hash = Hashtbl.hash
-  let equal = (=)
-  let default = 0
-end)
-
-module GDot = Graph.Graphviz.Dot(struct
-    let graph_attributes _ = []
-    let default_vertex_attributes _ = []
-    let vertex_name = print_sv
-    let vertex_attributes _ = []
-    let get_subgraph _ = None
-    let default_edge_attributes _ = []
-    let edge_attributes _ = []
-
-    include G
-  end)
-
-module DFG = Graph.Persistent.Digraph.ConcreteLabeled(struct
-  type t = int * instr
-  let compare = compare
-  let equal = (=)
-  let hash = Hashtbl.hash
-end)(struct
-  type t = int
-  let compare = compare
-  let hash = Hashtbl.hash
-  let equal = (=)
-  let default = 0
-end)
-
-let reg r = sprintf "r%d" (P.to_int r)
-let print_pred r = sprintf "p%d" (Nat.to_int r)
-
-let print_instr = function
-  | RBnop -> ""
-  | RBload (_, _, _, _, r) -> sprintf "load(%s)" (reg r)
-  | RBstore (_, _, _, _, r) -> sprintf "store(%s)" (reg r)
-  | RBsetpred (_, _, p) -> sprintf "setpred(%s)" (print_pred p)
-  | RBop (_, op, args, d) ->
-    (match op, args with
-    | Omove, _ -> "mov"
-    | Ointconst n, _ -> sprintf "%s=%ld" (reg d) (camlint_of_coqint n)
-    | Olongconst n, _ -> sprintf "%s=%LdL" (reg d) (camlint64_of_coqint n)
-    | Ofloatconst n, _ -> sprintf "%s=%.15F" (reg d) (camlfloat_of_coqfloat n)
-    | Osingleconst n, _ -> sprintf "%s=%.15Ff" (reg d) (camlfloat_of_coqfloat32 n)
-    | Oindirectsymbol id, _ -> sprintf "%s=&%s" (reg d) (extern_atom id)
-    | Ocast8signed, [r1] -> sprintf "%s=int8signed(%s)" (reg d) (reg r1)
-    | Ocast8unsigned, [r1] -> sprintf "%s=int8unsigned(%s)" (reg d) (reg r1)
-    | Ocast16signed, [r1] -> sprintf "%s=int16signed(%s)" (reg d) (reg r1)
-    | Ocast16unsigned, [r1] -> sprintf "%s=int16unsigned(%s)" (reg d) (reg r1)
-    | Oneg, [r1] -> sprintf "%s=-%s" (reg d) (reg r1)
-    | Osub, [r1;r2] -> sprintf "%s=%s-%s" (reg d) (reg r1) (reg r2)
-    | Omul, [r1;r2] -> sprintf "%s=%s*%s" (reg d) (reg r1) (reg r2)
-    | Omulimm n, [r1] -> sprintf "%s=%s*%ld" (reg d) (reg r1) (camlint_of_coqint n)
-    | Omulhs, [r1;r2] -> sprintf "%s=mulhs(%s,%s)" (reg d) (reg r1) (reg r2)
-    | Omulhu, [r1;r2] -> sprintf "%s=mulhu(%s,%s)" (reg d) (reg r1) (reg r2)
-    | Odiv, [r1;r2] -> sprintf "%s=%s /s %s" (reg d) (reg r1) (reg r2)
-    | Odivu, [r1;r2] -> sprintf "%s=%s /u %s" (reg d) (reg r1) (reg r2)
-    | Omod, [r1;r2] -> sprintf "%s=%s %%s %s" (reg d) (reg r1) (reg r2)
-    | Omodu, [r1;r2] -> sprintf "%s=%s %%u %s" (reg d) (reg r1) (reg r2)
-    | Oand, [r1;r2] -> sprintf "%s=%s & %s" (reg d) (reg r1) (reg r2)
-    | Oandimm n, [r1] -> sprintf "%s=%s & %ld" (reg d) (reg r1) (camlint_of_coqint n)
-    | Oor, [r1;r2] -> sprintf "%s=%s | %s" (reg d) (reg r1) (reg r2)
-    | Oorimm n, [r1] ->  sprintf "%s=%s | %ld" (reg d) (reg r1) (camlint_of_coqint n)
-    | Oxor, [r1;r2] -> sprintf "%s=%s ^ %s" (reg d) (reg r1) (reg r2)
-    | Oxorimm n, [r1] -> sprintf "%s=%s ^ %ld" (reg d) (reg r1) (camlint_of_coqint n)
-    | Onot, [r1] -> sprintf "%s=not(%s)" (reg d) (reg r1)
-    | Oshl, [r1;r2] -> sprintf "%s=%s << %s" (reg d) (reg r1) (reg r2)
-    | Oshlimm n, [r1] -> sprintf "%s=%s << %ld" (reg d) (reg r1) (camlint_of_coqint n)
-    | Oshr, [r1;r2] -> sprintf "%s=%s >>s %s" (reg d) (reg r1) (reg r2)
-    | Oshrimm n, [r1] -> sprintf "%s=%s >>s %ld" (reg d) (reg r1) (camlint_of_coqint n)
-    | Oshrximm n, [r1] -> sprintf "%s=%s >>x %ld" (reg d) (reg r1) (camlint_of_coqint n)
-    | Oshru, [r1;r2] -> sprintf "%s=%s >>u %s" (reg d) (reg r1) (reg r2)
-    | Oshruimm n, [r1] -> sprintf "%s=%s >>u %ld" (reg d) (reg r1) (camlint_of_coqint n)
-    | Ororimm n, [r1] -> sprintf "%s=%s ror %ld" (reg d) (reg r1) (camlint_of_coqint n)
-    | Oshldimm n, [r1;r2] -> sprintf "%s=(%s, %s) << %ld" (reg d) (reg r1) (reg r2) (camlint_of_coqint n)
-    | Olea addr, args -> sprintf "%s=addr" (reg d)
-    | Omakelong, [r1;r2] -> sprintf "%s=makelong(%s,%s)" (reg d) (reg r1) (reg r2)
-    | Olowlong, [r1] -> sprintf "%s=lowlong(%s)" (reg d) (reg r1)
-    | Ohighlong, [r1] -> sprintf "%s=highlong(%s)" (reg d) (reg r1)
-    | Ocast32signed, [r1] -> sprintf "%s=long32signed(%s)" (reg d) (reg r1)
-    | Ocast32unsigned, [r1] -> sprintf "%s=long32unsigned(%s)" (reg d) (reg r1)
-    | Onegl, [r1] -> sprintf "%s=-l %s" (reg d) (reg r1)
-    | Osubl, [r1;r2] -> sprintf "%s=%s -l %s" (reg d) (reg r1) (reg r2)
-    | Omull, [r1;r2] -> sprintf "%s=%s *l %s" (reg d) (reg r1) (reg r2)
-    | Omullimm n, [r1] -> sprintf "%s=%s *l %Ld" (reg d) (reg r1) (camlint64_of_coqint n)
-    | Omullhs, [r1;r2] -> sprintf "%s=mullhs(%s,%s)" (reg d) (reg r1) (reg r2)
-    | Omullhu, [r1;r2] -> sprintf "%s=mullhu(%s,%s)" (reg d) (reg r1) (reg r2)
-    | Odivl, [r1;r2] -> sprintf "%s=%s /ls %s" (reg d) (reg r1) (reg r2)
-    | Odivlu, [r1;r2] -> sprintf "%s=%s /lu %s" (reg d) (reg r1) (reg r2)
-    | Omodl, [r1;r2] -> sprintf "%s=%s %%ls %s" (reg d) (reg r1) (reg r2)
-    | Omodlu, [r1;r2] -> sprintf "%s=%s %%lu %s" (reg d) (reg r1) (reg r2)
-    | Oandl, [r1;r2] -> sprintf "%s=%s &l %s" (reg d) (reg r1) (reg r2)
-    | Oandlimm n, [r1] -> sprintf "%s=%s &l %Ld" (reg d) (reg r1) (camlint64_of_coqint n)
-    | Oorl, [r1;r2] -> sprintf "%s=%s |l %s" (reg d) (reg r1) (reg r2)
-    | Oorlimm n, [r1] ->  sprintf "%s=%s |l %Ld" (reg d) (reg r1) (camlint64_of_coqint n)
-    | Oxorl, [r1;r2] -> sprintf "%s=%s ^l %s" (reg d) (reg r1) (reg r2)
-    | Oxorlimm n, [r1] -> sprintf "%s=%s ^l %Ld" (reg d) (reg r1) (camlint64_of_coqint n)
-    | Onotl, [r1] -> sprintf "%s=notl(%s)" (reg d) (reg r1)
-    | Oshll, [r1;r2] -> sprintf "%s=%s <<l %s" (reg d) (reg r1) (reg r2)
-    | Oshllimm n, [r1] -> sprintf "%s=%s <<l %ld" (reg d) (reg r1) (camlint_of_coqint n)
-    | Oshrl, [r1;r2] -> sprintf "%s=%s >>ls %s" (reg d) (reg r1) (reg r2)
-    | Oshrlimm n, [r1] -> sprintf "%s=%s >>ls %ld" (reg d) (reg r1) (camlint_of_coqint n)
-    | Oshrxlimm n, [r1] -> sprintf "%s=%s >>lx %ld" (reg d) (reg r1) (camlint_of_coqint n)
-    | Oshrlu, [r1;r2] -> sprintf "%s=%s >>lu %s" (reg d) (reg r1) (reg r2)
-    | Oshrluimm n, [r1] -> sprintf "%s=%s >>lu %ld" (reg d) (reg r1) (camlint_of_coqint n)
-    | Ororlimm n, [r1] -> sprintf "%s=%s rorl %ld" (reg d) (reg r1) (camlint_of_coqint n)
-    | Oleal addr, args -> sprintf "%s=addr" (reg d)
-    | Onegf, [r1] -> sprintf "%s=negf(%s)" (reg d) (reg r1)
-    | Oabsf, [r1] -> sprintf "%s=absf(%s)" (reg d) (reg r1)
-    | Oaddf, [r1;r2] -> sprintf "%s=%s +f %s" (reg d) (reg r1) (reg r2)
-    | Osubf, [r1;r2] -> sprintf "%s=%s -f %s" (reg d) (reg r1) (reg r2)
-    | Omulf, [r1;r2] -> sprintf "%s=%s *f %s" (reg d) (reg r1) (reg r2)
-    | Odivf, [r1;r2] -> sprintf "%s=%s /f %s" (reg d) (reg r1) (reg r2)
-    | Onegfs, [r1] -> sprintf "%s=negfs(%s)" (reg d) (reg r1)
-    | Oabsfs, [r1] -> sprintf "%s=absfs(%s)" (reg d) (reg r1)
-    | Oaddfs, [r1;r2] -> sprintf "%s=%s +fs %s" (reg d) (reg r1) (reg r2)
-    | Osubfs, [r1;r2] -> sprintf "%s=%s -fs %s" (reg d) (reg r1) (reg r2)
-    | Omulfs, [r1;r2] -> sprintf "%s=%s *fs %s" (reg d) (reg r1) (reg r2)
-    | Odivfs, [r1;r2] -> sprintf "%s=%s /fs %s" (reg d) (reg r1) (reg r2)
-    | Osingleoffloat, [r1] -> sprintf "%s=singleoffloat(%s)" (reg d) (reg r1)
-    | Ofloatofsingle, [r1] -> sprintf "%s=floatofsingle(%s)" (reg d) (reg r1)
-    | Ointoffloat, [r1] -> sprintf "%s=intoffloat(%s)" (reg d) (reg r1)
-    | Ofloatofint, [r1] -> sprintf "%s=floatofint(%s)" (reg d) (reg r1)
-    | Ointofsingle, [r1] -> sprintf "%s=intofsingle(%s)" (reg d) (reg r1)
-    | Osingleofint, [r1] -> sprintf "%s=singleofint(%s)" (reg d) (reg r1)
-    | Olongoffloat, [r1] -> sprintf "%s=longoffloat(%s)" (reg d) (reg r1)
-    | Ofloatoflong, [r1] -> sprintf "%s=floatoflong(%s)" (reg d) (reg r1)
-    | Olongofsingle, [r1] -> sprintf "%s=longofsingle(%s)" (reg d) (reg r1)
-    | Osingleoflong, [r1] -> sprintf "%s=singleoflong(%s)" (reg d) (reg r1)
-    | Ocmp c, args -> sprintf "%s=cmp" (reg d)
-    | Osel (c, ty), r1::r2::args -> sprintf "%s=sel" (reg d)
-    | _, _ -> sprintf "N/a")
-
-module DFGDot = Graph.Graphviz.Dot(struct
-    let graph_attributes _ = []
-    let default_vertex_attributes _ = []
-    let vertex_name = function (i, instr) -> sprintf "\"%d:%s\"" i (print_instr instr)
-    let vertex_attributes _ = []
-    let get_subgraph _ = None
-    let default_edge_attributes _ = []
-    let edge_attributes _ = []
-
-    include DFG
-  end)
-
-module IMap = Map.Make (struct
-  type t = int
-
-  let compare = compare
-end)
-
-let gen_vertex instrs i = (i, List.nth instrs i)
-
-(** The DFG type defines a list of instructions with their data dependencies as [edges], which are
-   the pairs of integers that represent the index of the instruction in the [nodes].  The edges
-   always point from left to right. *)
-
-let print_list f out_chan a =
-  fprintf out_chan "[ ";
-  List.iter (fprintf out_chan "%a " f) a;
-  fprintf out_chan "]"
-
-let print_tuple out_chan a =
-  let l, r = a in
-  fprintf out_chan "(%d,%d)" l r
-
-(*let print_dfg out_chan dfg =
-  fprintf out_chan "{ nodes = %a, edges = %a }"
-    (print_list PrintRTLBlockInstr.print_bblock_body)
-    dfg.nodes (print_list print_tuple) dfg.edges*)
-
-let print_dfg = DFGDot.output_graph
-
-let read_process command =
-  let buffer_size = 2048 in
-  let buffer = Buffer.create buffer_size in
-  let string = Bytes.create buffer_size in
-  let in_channel = Unix.open_process_in command in
-  let chars_read = ref 1 in
-  while !chars_read <> 0 do
-    chars_read := input in_channel string 0 buffer_size;
-    Buffer.add_substring buffer (Bytes.to_string string) 0 !chars_read
-  done;
-  ignore (Unix.close_process_in in_channel);
-  Buffer.contents buffer
-
-let comb_delay = function
-  | RBnop -> 0
-  | RBop (_, op, _, _) ->
-    (match op with
-     | Omove -> 0
-     | Ointconst _ -> 0
-     | Olongconst _ -> 0
-     | Ocast8signed -> 0
-     | Ocast8unsigned -> 0
-     | Ocast16signed -> 0
-     | Ocast16unsigned -> 0
-     | Oneg -> 0
-     | Onot -> 0
-     | Oor -> 0
-     | Oorimm _ -> 0
-     | Oand -> 0
-     | Oandimm _ -> 0
-     | Oxor -> 0
-     | Oxorimm _ -> 0
-     | Omul -> 8
-     | Omulimm _ -> 8
-     | Omulhs -> 8
-     | Omulhu -> 8
-     | Odiv -> 72
-     | Odivu -> 72
-     | Omod -> 72
-     | Omodu -> 72
-     | _ -> 1)
-  | _ -> 1
-
-let pipeline_stages = function
-  | RBop (_, op, _, _) ->
-    (match op with
-     | Odiv -> 32
-     | Odivu -> 32
-     | Omod -> 32
-     | Omodu -> 32
-     | _ -> 0)
-  | _ -> 0
-
-(** Add a dependency if it uses a register that was written to previously. *)
-let add_dep map i tree dfg curr =
-  match PTree.get curr tree with
-  | None -> dfg
-  | Some ip ->
-    let ipv = (List.nth map ip) in
-    DFG.add_edge_e dfg (ipv, comb_delay (snd ipv), List.nth map i)
-
-(** This function calculates the dependencies of each instruction.  The nodes correspond to previous
-   registers that were allocated and show which instruction caused it.
-
-   This function only gathers the RAW constraints, and will therefore only be active for operations
-   that modify registers, which is this case only affects loads and operations. *)
-let accumulate_RAW_deps map dfg curr =
-  let i, dst_map, graph = dfg in
-  let acc_dep_instruction rs dst =
-    ( i + 1,
-      PTree.set dst i dst_map,
-      List.fold_left (add_dep map i dst_map) graph rs
-    )
-  in
-  let acc_dep_instruction_nodst rs =
-    ( i + 1,
-      dst_map,
-    List.fold_left (add_dep map i dst_map) graph rs)
-  in
-  match curr with
-  | RBop (op, _, rs, dst) -> acc_dep_instruction rs dst
-  | RBload (op, _mem, _addr, rs, dst) -> acc_dep_instruction rs dst
-  | RBstore (op, _mem, _addr, rs, src) -> acc_dep_instruction_nodst (src :: rs)
-  | _ -> (i + 1, dst_map, graph)
-
-(** Finds the next write to the [dst] register.  This is a small optimisation so that only one
-   dependency is generated for a data dependency. *)
-let rec find_next_dst_write i dst i' curr =
-  let check_dst dst' curr' =
-    if dst = dst' then Some (i, i')
-    else find_next_dst_write i dst (i' + 1) curr'
-  in
-  match curr with
-  | [] -> None
-  | RBop (_, _, _, dst') :: curr' -> check_dst dst' curr'
-  | RBload (_, _, _, _, dst') :: curr' -> check_dst dst' curr'
-  | _ :: curr' -> find_next_dst_write i dst (i' + 1) curr'
-
-let rec find_all_next_dst_read i dst i' curr =
-  let check_dst rs curr' =
-    if List.exists (fun x -> x = dst) rs
-    then (i, i') :: find_all_next_dst_read i dst (i' + 1) curr'
-    else find_all_next_dst_read i dst (i' + 1) curr'
-  in
-  match curr with
-  | [] -> []
-  | RBop (_, _, rs, _) :: curr' -> check_dst rs curr'
-  | RBload (_, _, _, rs, _) :: curr' -> check_dst rs curr'
-  | RBstore (_, _, _, rs, src) :: curr' -> check_dst (src :: rs) curr'
-  | RBnop :: curr' -> find_all_next_dst_read i dst (i' + 1) curr'
-  | RBsetpred (_, rs, _) :: curr' -> check_dst rs curr'
-
-let drop i lst =
-  let rec drop' i' lst' =
-    match lst' with
-    | _ :: ls -> if i' = i then ls else drop' (i' + 1) ls
-    | [] -> []
-  in
-  if i = 0 then lst else drop' 1 lst
-
-let take i lst =
-  let rec take' i' lst' =
-    match lst' with
-    | l :: ls -> if i' = i then [ l ] else l :: take' (i' + 1) ls
-    | [] -> []
-  in
-  if i = 0 then [] else take' 1 lst
-
-let rec next_store i = function
-  | [] -> None
-  | RBstore (_, _, _, _, _) :: _ -> Some i
-  | _ :: rst -> next_store (i + 1) rst
-
-let rec next_load i = function
-  | [] -> None
-  | RBload (_, _, _, _, _) :: _ -> Some i
-  | _ :: rst -> next_load (i + 1) rst
-
-let accumulate_RAW_mem_deps instrs dfg curri =
-  let i, curr = curri in
-  match curr with
-  | RBload (_, _, _, _, _) -> (
-      match next_store 0 (take i instrs |> List.rev) with
-      | None -> dfg
-      | Some d -> DFG.add_edge dfg (gen_vertex instrs (i - d - 1)) (gen_vertex instrs i) )
-  | _ -> dfg
-
-let accumulate_WAR_mem_deps instrs dfg curri =
-  let i, curr = curri in
-  match curr with
-  | RBstore (_, _, _, _, _) -> (
-      match next_load 0 (take i instrs |> List.rev) with
-      | None -> dfg
-      | Some d -> DFG.add_edge dfg (gen_vertex instrs (i - d - 1)) (gen_vertex instrs i) )
-  | _ -> dfg
-
-let accumulate_WAW_mem_deps instrs dfg curri =
-  let i, curr = curri in
-  match curr with
-  | RBstore (_, _, _, _, _) -> (
-      match next_store 0 (take i instrs |> List.rev) with
-      | None -> dfg
-      | Some d -> DFG.add_edge dfg (gen_vertex instrs (i - d - 1)) (gen_vertex instrs i) )
-  | _ -> dfg
-
-(** Predicate dependencies. *)
-
-let rec in_predicate p p' =
-  match p' with
-  | Pvar p'' -> Nat.to_int p = Nat.to_int p''
-  | Pnot p'' -> in_predicate p p''
-  | Pand (p1, p2) -> in_predicate p p1 || in_predicate p p2
-  | Por (p1, p2) -> in_predicate p p1 || in_predicate p p2
-
-let get_predicate = function
-  | RBop (p, _, _, _) -> p
-  | RBload (p, _, _, _, _) -> p
-  | RBstore (p, _, _, _, _) -> p
-  | _ -> None
-
-let rec next_setpred p i = function
-  | [] -> None
-  | RBsetpred (_, _, p') :: rst ->
-    if in_predicate p' p then
-      Some i
-    else
-      next_setpred p (i + 1) rst
-  | _ :: rst -> next_setpred p (i + 1) rst
-
-let rec next_preduse p i instr=
-  let next p' rst =
-    if in_predicate p p' then
-      Some i
-    else
-      next_preduse p (i + 1) rst
-  in
-  match instr with
-  | [] -> None
-  | RBload (Some p', _, _, _, _) :: rst -> next p' rst
-  | RBstore (Some p', _, _, _, _) :: rst -> next p' rst
-  | RBop (Some p', _, _, _) :: rst -> next p' rst
-  | _ :: rst -> next_load (i + 1) rst
-
-let accumulate_RAW_pred_deps instrs dfg curri =
-  let i, curr = curri in
-  match get_predicate curr with
-  | Some p -> (
-      match next_setpred p 0 (take i instrs |> List.rev) with
-      | None -> dfg
-      | Some d -> DFG.add_edge dfg (gen_vertex instrs (i - d - 1)) (gen_vertex instrs i) )
-  | _ -> dfg
-
-let accumulate_WAR_pred_deps instrs dfg curri =
-  let i, curr = curri in
-  match curr with
-  | RBsetpred (_, _, p) -> (
-      match next_preduse p 0 (take i instrs |> List.rev) with
-      | None -> dfg
-      | Some d -> DFG.add_edge dfg (gen_vertex instrs (i - d - 1)) (gen_vertex instrs i) )
-  | _ -> dfg
-
-let accumulate_WAW_pred_deps instrs dfg curri =
-  let i, curr = curri in
-  match curr with
-  | RBsetpred (_, _, p) -> (
-      match next_setpred (Pvar p) 0 (take i instrs |> List.rev) with
-      | None -> dfg
-      | Some d -> DFG.add_edge dfg (gen_vertex instrs (i - d - 1)) (gen_vertex instrs i) )
-  | _ -> dfg
-
-(** This function calculates the WAW dependencies, which happen when two writes are ordered one
-   after another and therefore have to be kept in that order.  This accumulation might be redundant
-   if register renaming is done before hand, because then these dependencies can be avoided. *)
-let accumulate_WAW_deps instrs dfg curri =
-  let i, curr = curri in
-  let dst_dep dst =
-    match find_next_dst_write i dst (i + 1) (drop (i + 1) instrs) with
-    | Some (a, b) -> DFG.add_edge dfg (gen_vertex instrs a) (gen_vertex instrs b)
-    | _ -> dfg
-  in
-  match curr with
-  | RBop (_, _, _, dst) -> dst_dep dst
-  | RBload (_, _, _, _, dst) -> dst_dep dst
-  | RBstore (_, _, _, _, _) -> (
-      match next_store (i + 1) (drop (i + 1) instrs) with
-      | None -> dfg
-      | Some i' -> DFG.add_edge dfg (gen_vertex instrs i) (gen_vertex instrs i') )
-  | _ -> dfg
-
-let accumulate_WAR_deps instrs dfg curri =
-  let i, curr = curri in
-  let dst_dep dst =
-    let dep_list = find_all_next_dst_read i dst 0 (take i instrs |> List.rev)
-        |> List.map (function (d, d') -> (i - d' - 1, d))
-    in
-    List.fold_left (fun g ->
-        function (d, d') -> DFG.add_edge g (gen_vertex instrs d) (gen_vertex instrs d')) dfg dep_list
-  in
-  match curr with
-  | RBop (_, _, _, dst) -> dst_dep dst
-  | RBload (_, _, _, _, dst) -> dst_dep dst
-  | _ -> dfg
-
-let assigned_vars vars = function
-  | RBnop -> vars
-  | RBop (_, _, _, dst) -> dst :: vars
-  | RBload (_, _, _, _, dst) -> dst :: vars
-  | RBstore (_, _, _, _, _) -> vars
-  | RBsetpred (_, _, _) -> vars
-
-let get_pred = function
-  | RBnop -> None
-  | RBop (op, _, _, _) -> op
-  | RBload (op, _, _, _, _) -> op
-  | RBstore (op, _, _, _, _) -> op
-  | RBsetpred (_, _, _) -> None
-
-let independant_pred p p' =
-  match sat_pred_temp (Nat.of_int 100000) (Pand (p, p')) with
-  | Some None -> true
-  | _ -> false
-
-let check_dependent op1 op2 =
-  match op1, op2 with
-  | Some p, Some p' -> not (independant_pred p p')
-  | _, _ -> true
-
-let remove_unnecessary_deps graph =
-  let is_dependent v1 v2 g =
-    let (_, instr1) = v1 in
-    let (_, instr2) = v2 in
-    if check_dependent (get_pred instr1) (get_pred instr2)
-    then g
-    else DFG.remove_edge g v1 v2
-  in
-  DFG.fold_edges is_dependent graph graph
-
-(** All the nodes in the DFG have to come after the source of the basic block, and should terminate
-   before the sink of the basic block.  After that, there should be constraints for data
-   dependencies between nodes. *)
-let gather_bb_constraints debug bb =
-  let ibody = List.mapi (fun i a -> (i, a)) bb.bb_body in
-  let dfg = List.fold_left (fun dfg v -> DFG.add_vertex dfg v) DFG.empty ibody in
-  let _, _, dfg' =
-    List.fold_left (accumulate_RAW_deps ibody)
-      (0, PTree.empty, dfg)
-      bb.bb_body
-  in
-  let dfg'' = List.fold_left (fun dfg f -> List.fold_left (f bb.bb_body) dfg ibody) dfg'
-      [ accumulate_WAW_deps;
-        accumulate_WAR_deps;
-        accumulate_RAW_mem_deps;
-        accumulate_WAR_mem_deps;
-        accumulate_WAW_mem_deps;
-        accumulate_RAW_pred_deps;
-        accumulate_WAR_pred_deps;
-        accumulate_WAW_pred_deps
-      ]
-  in
-  let dfg''' = remove_unnecessary_deps dfg'' in
-  (List.length bb.bb_body, dfg''', successors_instr bb.bb_exit)
-
-let encode_var bbn n i = { sv_type = VarType (bbn, n); sv_num = i }
-let encode_bb bbn i = { sv_type = BBType bbn; sv_num = i }
-
-let add_super_nodes n dfg =
-  DFG.fold_vertex (function v1 -> fun g ->
-      (if DFG.in_degree dfg v1 = 0
-       then G.add_edge_e g (encode_bb n 0, 0, encode_var n (fst v1) 0)
-       else g) |>
-      (fun g' ->
-         if DFG.out_degree dfg v1 = 0
-         then G.add_edge_e g' (encode_var n (fst v1) 0, 0, encode_bb n 1)
-         else g')) dfg
-
-let add_data_deps n =
-  DFG.fold_edges_e (function ((i1, _), l, (i2, _)) -> fun g ->
-      G.add_edge_e g (encode_var n i1 0, 0, encode_var n i2 0)
-    )
-
-let add_ctrl_deps n succs constr =
-  List.fold_left (fun g n' ->
-      G.add_edge_e g (encode_bb n 1, -1, encode_bb n' 0)
-    ) constr succs
-
-module BFDFG = Graph.Path.BellmanFord(DFG)(struct
-    include DFG
-    type t = int
-    let weight = DFG.E.label
-    let compare = compare
-    let add = (+)
-    let zero = 0
-  end)
-
-module TopoDFG = Graph.Topological.Make(DFG)
-
-let negate_graph constr =
-  DFG.fold_edges_e (function (v1, e, v2) -> fun g ->
-      DFG.add_edge_e g (v1, -e, v2)
-    ) constr DFG.empty
-
-let add_cycle_constr max n dfg constr =
-  let negated_dfg = negate_graph dfg in
-  let longest_path v = BFDFG.all_shortest_paths negated_dfg v
-                       |> BFDFG.H.to_seq |> List.of_seq in
-  let constrained_paths = List.filter (function (v, m) -> - m > max) in
-  List.fold_left (fun g -> function (v, v', w) ->
-      G.add_edge_e g (encode_var n (fst v) 0,
-                      - (int_of_float (Float.ceil (Float.div (float_of_int w) (float_of_int max))) - 1),
-                      encode_var n (fst v') 0)
-    ) constr (DFG.fold_vertex (fun v l ->
-      List.append l (longest_path v |> constrained_paths
-                     |> List.map (function (v', w) -> (v, v', - w)))
-    ) dfg [])
-
-type resource =
-  | Mem
-  | SDiv
-  | UDiv
-
-type resources = {
-  res_mem: DFG.V.t list;
-  res_udiv: DFG.V.t list;
-  res_sdiv: DFG.V.t list;
-}
-
-let find_resource = function
-  | RBload _ -> Some Mem
-  | RBstore _ -> Some Mem
-  | RBop (_, op, _, _) ->
-    ( match op with
-      | Odiv -> Some SDiv
-      | Odivu -> Some UDiv
-      | Omod -> Some SDiv
-      | Omodu -> Some UDiv
-      | _ -> None )
-  | _ -> None
-
-let add_resource_constr n dfg constr =
-  let res = TopoDFG.fold (function (i, instr) ->
-    function {res_mem = ml; res_sdiv = sdl; res_udiv = udl} as r ->
-    match find_resource instr with
-    | Some SDiv -> {r with res_sdiv = (i, instr) :: sdl}
-    | Some UDiv -> {r with res_udiv = (i, instr) :: udl}
-    | Some Mem -> {r with res_mem = (i, instr) :: ml}
-    | None -> r
-    ) dfg {res_mem = []; res_sdiv = []; res_udiv = []}
-  in
-  let get_constraints l g = List.fold_left (fun gv v' ->
-      match gv with
-      | (g, None) -> (g, Some v')
-      | (g, Some v) ->
-        (G.add_edge_e g (encode_var n (fst v) 0, -1, encode_var n (fst v') 0), Some v')
-    ) (g, None) l |> fst
-  in
-  get_constraints (List.rev res.res_mem) constr
-  |> get_constraints (List.rev res.res_udiv)
-  |> get_constraints (List.rev res.res_sdiv)
-
-let gather_cfg_constraints c constr curr =
-  let (n, dfg) = curr in
-  match PTree.get (P.of_int n) c with
-  | None -> assert false
-  | Some { bb_exit = ctrl; _ } ->
-    add_super_nodes n dfg constr
-    |> add_data_deps n dfg
-    |> add_ctrl_deps n (successors_instr ctrl
-                        |> List.map P.to_int
-                        |> List.filter (fun n' -> n' < n))
-    |> add_cycle_constr 8 n dfg
-    |> add_resource_constr n dfg
-
-let rec intersperse s = function
-  | [] -> []
-  | [ a ] -> [ a ]
-  | x :: xs -> x :: s :: intersperse s xs
-
-let print_objective constr =
-  let vars = G.fold_vertex (fun v1 l ->
-      match v1 with
-      | { sv_type = VarType _; sv_num = 0 } -> print_sv v1 :: l
-      | _ -> l
-    ) constr []
-  in
-  "min: " ^ String.concat "" (intersperse " + " vars) ^ ";\n"
-
-let print_lp constr =
-  print_objective constr ^
-  (G.fold_edges_e (function (e1, w, e2) -> fun s ->
-       s ^ sprintf "%s - %s <= %d;\n" (print_sv e1) (print_sv e2) w
-     ) constr "" |>
-   G.fold_vertex (fun v1 s ->
-       s ^ sprintf "int %s;\n" (print_sv v1)
-     ) constr)
-
-let update_schedule v = function Some l -> Some (v :: l) | None -> Some [ v ]
-
-let parse_soln tree s =
-  let r = Str.regexp "var\\([0-9]+\\)n\\([0-9]+\\)_0[ ]+\\([0-9]+\\)" in
-  if Str.string_match r s 0 then
-    IMap.update
-      (Str.matched_group 1 s |> int_of_string)
-      (update_schedule
-         ( Str.matched_group 2 s |> int_of_string,
-           Str.matched_group 3 s |> int_of_string ))
-      tree
-  else tree
-
-let solve_constraints constr =
-  let oc = open_out "lpsolve.txt" in
-  fprintf oc "%s\n" (print_lp constr);
-  close_out oc;
-
-  Str.split (Str.regexp_string "\n") (read_process "lp_solve lpsolve.txt")
-  |> drop 3
-  |> List.fold_left parse_soln IMap.empty
-
-let subgraph dfg l =
-  let dfg' = List.fold_left (fun g v -> DFG.add_vertex g v) DFG.empty l in
-  List.fold_left (fun g v ->
-      List.fold_left (fun g' v' ->
-          let edges = DFG.find_all_edges dfg v v' in
-          List.fold_left (fun g'' e ->
-              DFG.add_edge_e g'' e
-            ) g' edges
-        ) g l
-    ) dfg' l
-
-let rec all_successors dfg v =
-  List.concat (List.fold_left (fun l v ->
-      all_successors dfg v :: l
-    ) [] (DFG.succ dfg v))
-
-let order_instr dfg =
-  DFG.fold_vertex (fun v li ->
-      if DFG.in_degree dfg v = 0
-      then (List.map snd (v :: all_successors dfg v)) :: li
-      else li
-    ) dfg []
-
-let combine_bb_schedule schedule s =
-  let i, st = s in
-  IMap.update st (update_schedule i) schedule
-
-(** Should generate the [RTLPar] code based on the input [RTLBlock] description. *)
-let transf_rtlpar c c' (schedule : (int * int) list IMap.t) =
-  let f i bb : RTLPar.bblock =
-    match bb with
-    | { bb_body = []; bb_exit = c } -> { bb_body = []; bb_exit = c }
-    | { bb_body = bb_body'; bb_exit = ctrl_flow } ->
-      let dfg = match PTree.get i c' with None -> assert false | Some x -> x in
-      let i_sched = IMap.find (P.to_int i) schedule in
-      let i_sched_tree =
-        List.fold_left combine_bb_schedule IMap.empty i_sched
-      in
-      let body = IMap.to_seq i_sched_tree |> List.of_seq |> List.map snd
-                 |> List.map (List.map (fun x -> (x, List.nth bb_body' x)))
-      in
-      (*let final_body = List.map (fun x -> subgraph dfg x |> order_instr) body in*)
-      let final_body2 = List.map (fun x -> subgraph dfg x
-                                           |> (fun x -> TopoDFG.fold (fun i l -> snd i :: l) x [])
-                                           |> List.rev) body
-      in
-      { bb_body = List.map (fun x -> [x]) final_body2;
-        bb_exit = ctrl_flow
-      }
-  in
-  PTree.map f c
-
-let schedule entry (c : RTLBlock.bb RTLBlockInstr.code) =
-  let debug = true in
-  let transf_graph (_, dfg, _) = dfg in
-  let c' = PTree.map1 (fun x -> gather_bb_constraints false x |> transf_graph) c in
-  (*let _ = if debug then PTree.map (fun r o -> printf "##### %d #####\n%a\n\n" (P.to_int r) print_dfg (second o)) c' else PTree.empty in*)
-  let cgraph = PTree.elements c'
-               |> List.map (function (x, y) -> (P.to_int x, y))
-               |> List.fold_left (gather_cfg_constraints c) G.empty
-  in
-  let graph = open_out "constr_graph.dot" in
-  fprintf graph "%a\n" GDot.output_graph cgraph;
-  close_out graph;
-  let schedule' = solve_constraints cgraph in
-  (**IMap.iter (fun a b -> printf "##### %d #####\n%a\n\n" a (print_list print_tuple) b) schedule';*)
-  (*printf "Schedule: %a\n" (fun a x -> IMap.iter (fun d -> fprintf a "%d: %a\n" d (print_list print_tuple)) x) schedule';*)
-  transf_rtlpar c c' schedule'
-
-let rec find_reachable_states c e =
-  match PTree.get e c with
-  | Some { bb_exit = ex; _ } ->
-    e :: List.fold_left (fun x a -> List.concat [x; find_reachable_states c a]) []
-      (successors_instr ex |> List.filter (fun x -> P.lt x e))
-  | None -> assert false
-
-let add_to_tree c nt i =
-  match PTree.get i c with
-  | Some p -> PTree.set i p nt
-  | None -> assert false
-
-let schedule_fn (f : RTLBlock.coq_function) : RTLPar.coq_function =
-  let scheduled = schedule f.fn_entrypoint f.fn_code in
-  let reachable = find_reachable_states scheduled f.fn_entrypoint
-                  |> List.to_seq |> SS.of_seq |> SS.to_seq |> List.of_seq in
-  { fn_sig = f.fn_sig;
-    fn_params = f.fn_params;
-    fn_stacksize = f.fn_stacksize;
-    fn_code = List.fold_left (add_to_tree scheduled) PTree.empty reachable;
-    fn_entrypoint = f.fn_entrypoint
-  }
diff --git a/src/hls/Verilog.v b/src/hls/Verilog.v
index ca5abd4..0df8b7e 100644
--- a/src/hls/Verilog.v
+++ b/src/hls/Verilog.v
@@ -17,27 +17,33 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-From Coq Require Import
-  Structures.OrderedTypeEx
-  FSets.FMapPositive
-  Program.Basics
-  PeanoNat
-  ZArith
-  Lists.List
-  Program.
+Set Implicit Arguments.
 
-Require Import Lia.
+Require Import Coq.Structures.OrderedTypeEx.
+Require Import Coq.FSets.FMapPositive.
+Require Import Coq.Program.Basics.
+Require Import Coq.Arith.PeanoNat.
+Require Import Coq.ZArith.ZArith.
+Require Import Coq.Lists.List.
+Require Import Coq.Program.Program.
+Require Import Coq.micromega.Lia.
+
+Require compcert.common.Events.
+Require Import compcert.lib.Integers.
+Require Import compcert.common.Errors.
+Require Import compcert.common.Smallstep.
+Require Import compcert.common.Globalenvs.
+
+Require Import vericert.common.Vericertlib.
+Require Import vericert.common.Show.
+Require Import vericert.hls.ValueInt.
+Require Import vericert.hls.AssocMap.
+Require Import vericert.hls.Array.
 
 Import ListNotations.
 
-From vericert Require Import Vericertlib Show ValueInt AssocMap Array.
-From compcert Require Events.
-From compcert Require Import Integers Errors Smallstep Globalenvs.
-
 Local Open Scope assocmap.
 
-Set Implicit Arguments.
-
 Definition reg : Type := positive.
 Definition node : Type := positive.
 Definition szreg : Type := reg * nat.
@@ -76,6 +82,39 @@ Definition merge_arr (new : option arr) (old : option arr) : option arr :=
 Definition merge_arrs (new : assocmap_arr) (old : assocmap_arr) : assocmap_arr :=
   AssocMap.combine merge_arr new old.
 
+Lemma merge_arr_empty':
+  forall l,
+  merge_arr (Some (arr_repeat None (length l))) (Some (make_array l)) = Some (make_array l).
+Proof.
+  induction l; auto.
+  unfold merge_arr.
+  unfold combine, make_array. simplify. rewrite H0.
+  rewrite list_repeat_cons. simplify.
+  rewrite H0; auto.
+Qed.
+
+Lemma merge_arr_empty:
+  forall v l,
+  v = Some (make_array l) ->
+  merge_arr (Some (arr_repeat None (length l))) v = v.
+Proof. intros. rewrite H. apply merge_arr_empty'. Qed.
+
+Lemma merge_arr_empty2:
+  forall v l v',
+  v = Some v' ->
+  l = arr_length v' ->
+  merge_arr (Some (arr_repeat None l)) v = v.
+Proof.
+  intros. subst. destruct v'. simplify.
+  generalize dependent arr_wf. generalize dependent arr_length.
+  induction arr_contents.
+  - simplify; subst; auto.
+  - unfold combine, make_array in *; simplify; subst.
+    rewrite list_repeat_cons; simplify.
+    specialize (IHarr_contents (Datatypes.length arr_contents) eq_refl).
+    inv IHarr_contents. rewrite H0. rewrite H0. auto.
+Qed.
+
 Definition arr_assocmap_lookup (a : assocmap_arr) (r : reg) (i : nat) : option value :=
   match a ! r with
   | None => None
@@ -174,9 +213,12 @@ Inductive stmnt : Type :=
 | Vskip : stmnt
 | Vseq : stmnt -> stmnt -> stmnt
 | Vcond : expr -> stmnt -> stmnt -> stmnt
-| Vcase : expr -> list (expr * stmnt) -> option stmnt -> stmnt
+| Vcase : expr -> stmnt_expr_list -> option stmnt -> stmnt
 | Vblock : expr -> expr -> stmnt
-| Vnonblock : expr -> expr -> stmnt.
+| Vnonblock : expr -> expr -> stmnt
+with stmnt_expr_list : Type :=
+| Stmntnil : stmnt_expr_list
+| Stmntcons : expr -> stmnt -> stmnt_expr_list -> stmnt_expr_list.
 
 (** ** Edges
 
@@ -404,40 +446,6 @@ Definition handle_def {A : Type} (a : A) (val : option A)
 
 Local Open Scope error_monad_scope.
 
-(*Definition access_fext (f : fext) (r : reg) : res value :=
-  match AssocMap.get r f with
-  | Some v => OK v
-  | _ => OK (ZToValue 0)
-  end.*)
-
-(* TODO FIX Vvar case without default *)
-(*Fixpoint expr_run (assoc : assocmap) (e : expr)
-         {struct e} : res value :=
-  match e with
-  | Vlit v => OK v
-  | Vvar r => match s with
-              | State _ assoc _ _ _ => handle_def (ZToValue 32 0) assoc!r
-              | _ => Error (msg "Verilog: Wrong state")
-              end
-  | Vvari _ _ => Error (msg "Verilog: variable indexing not modelled")
-  | Vinputvar r => access_fext s r
-  | Vbinop op l r =>
-    let lv := expr_run s l in
-    let rv := expr_run s r in
-    let oper := binop_run op in
-    do lv' <- lv;
-    do rv' <- rv;
-    handle_opt (msg "Verilog: sizes are not equal")
-               (eq_to_opt lv' rv' (oper lv' rv'))
-  | Vunop op e =>
-    let oper := unop_run op in
-    do ev <- expr_run s e;
-    OK (oper ev)
-  | Vternary c te fe =>
-    do cv <- expr_run s c;
-    if valueToBool cv then expr_run s te else expr_run s fe
-  end.*)
-
 (** Return the location of the lhs of an assignment. *)
 
 Inductive location : Type :=
@@ -450,80 +458,6 @@ Inductive location_is : fext -> assocmap -> assocmap_arr -> expr -> location ->
   expr_runp f asr asa iexp iv ->
   location_is f asr asa (Vvari r iexp) (LocArray r (valueToNat iv)).
 
-(* Definition assign_name (f : fext) (asr: assocmap) (asa : assocmap_l)  (e : expr) : res reg := *)
-(*   match e with *)
-(*   | Vvar r => OK r *)
-(*   | _ => Error (msg "Verilog: expression not supported on lhs of assignment") *)
-(*   end. *)
-
-(*Fixpoint stmnt_height (st : stmnt) {struct st} : nat :=
-  match st with
-  | Vseq s1 s2 => S (stmnt_height s1 + stmnt_height s2)
-  | Vcond _ s1 s2 => S (Nat.max (stmnt_height s1) (stmnt_height s2))
-  | Vcase _ ls (Some st) =>
-    S (fold_right (fun t acc => Nat.max acc (stmnt_height (snd t))) 0%nat ls)
-  | _ => 1
-  end.
-
-Fixpoint find_case_stmnt (s : state) (v : value) (cl : list (expr * stmnt))
-         {struct cl} : option (res stmnt) :=
-  match cl with
-  | (e, st)::xs =>
-    match expr_run s e with
-    | OK v' =>
-      match eq_to_opt v v' (veq v v') with
-      | Some eq => if valueToBool eq then Some (OK st) else find_case_stmnt s v xs
-      | None => Some (Error (msg "Verilog: equality check sizes not equal"))
-      end
-    | Error msg => Some (Error msg)
-    end
-  | _ => None
-  end.
-
-Fixpoint stmnt_run' (n : nat) (s : state) (st : stmnt) {struct n} : res state :=
-  match n with
-  | S n' =>
-    match st with
-    | Vskip => OK s
-    | Vseq s1 s2 =>
-      do s' <- stmnt_run' n' s s1;
-      stmnt_run' n' s' s2
-    | Vcond c st sf =>
-      do cv <- expr_run s c;
-      if valueToBool cv
-      then stmnt_run' n' s st
-      else stmnt_run' n' s sf
-    | Vcase e cl defst =>
-      do v <- expr_run s e;
-      match find_case_stmnt s v cl with
-      | Some (OK st') => stmnt_run' n' s st'
-      | Some (Error msg) => Error msg
-      | None => do s' <- handle_opt (msg "Verilog: no case was matched")
-                                    (option_map (stmnt_run' n' s) defst); s'
-      end
-    | Vblock lhs rhs =>
-      match s with
-      | State m assoc nbassoc f c =>
-        do name <- assign_name lhs;
-        do rhse <- expr_run s rhs;
-        OK (State m (PositiveMap.add name rhse assoc) nbassoc f c)
-      | _ => Error (msg "Verilog: Wrong state")
-      end
-    | Vnonblock lhs rhs =>
-      match s with
-      | State m assoc nbassoc f c =>
-        do name <- assign_name lhs;
-        do rhse <- expr_run s rhs;
-        OK (State m assoc (PositiveMap.add name rhse nbassoc) f c)
-      | _ => Error (msg "Verilog: Wrong state")
-      end
-    end
-  | _ => OK s
-  end.
-
-Definition stmnt_run (s : state) (st : stmnt) : res state :=
-  stmnt_run' (stmnt_height st) s st. *)
-
 Inductive stmnt_runp: fext -> reg_associations -> arr_associations ->
                       stmnt -> reg_associations -> arr_associations -> Prop :=
 | stmnt_runp_Vskip:
@@ -551,19 +485,19 @@ Inductive stmnt_runp: fext -> reg_associations -> arr_associations ->
     expr_runp f asr0.(assoc_blocking) asa0.(assoc_blocking) me mve ->
     mve <> ve ->
     stmnt_runp f asr0 asa0 (Vcase e cs def) asr1 asa1 ->
-    stmnt_runp f asr0 asa0 (Vcase e ((me, sc)::cs) def) asr1 asa1
+    stmnt_runp f asr0 asa0 (Vcase e (Stmntcons me sc cs) def) asr1 asa1
 | stmnt_runp_Vcase_match:
     forall e ve asr0 asa0 f asr1 asa1 me mve sc cs def,
     expr_runp f asr0.(assoc_blocking) asa0.(assoc_blocking) e ve ->
     expr_runp f asr0.(assoc_blocking) asa0.(assoc_blocking) me mve ->
     mve = ve ->
     stmnt_runp f asr0 asa0 sc asr1 asa1 ->
-    stmnt_runp f asr0 asa0 (Vcase e ((me, sc)::cs) def) asr1 asa1
+    stmnt_runp f asr0 asa0 (Vcase e (Stmntcons me sc cs) def) asr1 asa1
 | stmnt_runp_Vcase_default:
     forall asr0 asa0 asr1 asa1 f st e ve,
     expr_runp f asr0.(assoc_blocking) asa0.(assoc_blocking) e ve ->
     stmnt_runp f asr0 asa0 st asr1 asa1 ->
-    stmnt_runp f asr0 asa0 (Vcase e nil (Some st)) asr1 asa1
+    stmnt_runp f asr0 asa0 (Vcase e Stmntnil (Some st)) asr1 asa1
 | stmnt_runp_Vblock_reg:
     forall lhs r rhs rhsval asr asa f,
     location_is f asr.(assoc_blocking) asa.(assoc_blocking) lhs (LocReg r) ->
@@ -594,37 +528,32 @@ Inductive stmnt_runp: fext -> reg_associations -> arr_associations ->
                  asr (nonblock_arr r i asa rhsval).
 Hint Constructors stmnt_runp : verilog.
 
-(*Fixpoint mi_step (s : state) (m : list module_item) {struct m} : res state :=
-  let run := fun st ls =>
-              do s' <- stmnt_run s st;
-              mi_step s' ls
-  in
-  match m with
-  | (Valways _ st)::ls => run st ls
-  | (Valways_ff _ st)::ls => run st ls
-  | (Valways_comb _ st)::ls => run st ls
-  | (Vdecl _ _)::ls => mi_step s ls
-  | (Vdeclarr _ _ _)::ls => mi_step s ls
-  | nil => OK s
-  end.*)
-
 Inductive mi_stepp : fext -> reg_associations -> arr_associations ->
                      module_item -> reg_associations -> arr_associations -> Prop :=
 | mi_stepp_Valways :
     forall f sr0 sa0 st sr1 sa1 c,
     stmnt_runp f sr0 sa0 st sr1 sa1 ->
-    mi_stepp f sr0 sa0 (Valways c st) sr1 sa1
-| mi_stepp_Valways_ff :
-    forall f sr0 sa0 st sr1 sa1 c,
-    stmnt_runp f sr0 sa0 st sr1 sa1 ->
-    mi_stepp f sr0 sa0 (Valways_ff c st) sr1 sa1
-| mi_stepp_Valways_comb :
+    mi_stepp f sr0 sa0 (Valways (Vposedge c) st) sr1 sa1
+| mi_stepp_Valways_ne :
+    forall f sr0 sa0 c st,
+    mi_stepp f sr0 sa0 (Valways (Vnegedge c) st) sr0 sa0
+| mi_stepp_Vdecl :
+    forall f sr0 sa0 d,
+    mi_stepp f sr0 sa0 (Vdeclaration d) sr0 sa0.
+Hint Constructors mi_stepp : verilog.
+
+Inductive mi_stepp_negedge : fext -> reg_associations -> arr_associations ->
+                             module_item -> reg_associations -> arr_associations -> Prop :=
+| mi_stepp_negedge_Valways :
     forall f sr0 sa0 st sr1 sa1 c,
     stmnt_runp f sr0 sa0 st sr1 sa1 ->
-    mi_stepp f sr0 sa0 (Valways_comb c st) sr1 sa1
-| mi_stepp_Vdecl :
-    forall f sr sa d,
-    mi_stepp f sr sa (Vdeclaration d) sr sa.
+    mi_stepp_negedge f sr0 sa0 (Valways (Vnegedge c) st) sr1 sa1
+| mi_stepp_negedge_Valways_ne :
+    forall f sr0 sa0 c st,
+    mi_stepp_negedge f sr0 sa0 (Valways (Vposedge c) st) sr0 sa0
+| mi_stepp_negedge_Vdecl :
+    forall f sr0 sa0 d,
+    mi_stepp_negedge f sr0 sa0 (Vdeclaration d) sr0 sa0.
 Hint Constructors mi_stepp : verilog.
 
 Inductive mis_stepp : fext -> reg_associations -> arr_associations ->
@@ -639,80 +568,20 @@ Inductive mis_stepp : fext -> reg_associations -> arr_associations ->
     mis_stepp f sr sa nil sr sa.
 Hint Constructors mis_stepp : verilog.
 
-(*Definition mi_step_commit (s : state) (m : list module_item) : res state :=
-  match mi_step s m with
-  | OK (State m assoc nbassoc f c) =>
-    OK (State m (merge_assocmap nbassoc assoc) empty_assocmap f c)
-  | Error msg => Error msg
-  | _ => Error (msg "Verilog: Wrong state")
-  end.
-
-Fixpoint mi_run (f : fextclk) (assoc : assocmap) (m : list module_item) (n : nat)
-         {struct n} : res assocmap :=
-  match n with
-  | S n' =>
-    do assoc' <- mi_run f assoc m n';
-    match mi_step_commit (State assoc' empty_assocmap f (Pos.of_nat n')) m with
-    | OK (State assoc _ _ _) => OK assoc
-    | Error m => Error m
-    end
-  | O => OK assoc
-  end.*)
-
-(** Resets the module into a known state, so that it can be executed.  This is
-assumed to be the starting state of the module, and may have to be changed if
-other arguments to the module are also to be supported. *)
-
-(*Definition initial_fextclk (m : module) : fextclk :=
-  fun x => match x with
-           | S O => (AssocMap.set (mod_reset m) (ZToValue 1) empty_assocmap)
-           | _ => (AssocMap.set (mod_reset m) (ZToValue 0) empty_assocmap)
-           end.*)
-
-(*Definition module_run (n : nat) (m : module) : res assocmap :=
-  mi_run (initial_fextclk m) empty_assocmap (mod_body m) n.*)
+Inductive mis_stepp_negedge : fext -> reg_associations -> arr_associations ->
+                      list module_item -> reg_associations -> arr_associations -> Prop :=
+| mis_stepp_negedge_Cons :
+    forall f mi mis sr0 sa0 sr1 sa1 sr2 sa2,
+    mi_stepp_negedge f sr0 sa0 mi sr1 sa1 ->
+    mis_stepp_negedge f sr1 sa1 mis sr2 sa2 ->
+    mis_stepp_negedge f sr0 sa0 (mi :: mis) sr2 sa2
+| mis_stepp_negedge_Nil :
+    forall f sr sa,
+    mis_stepp_negedge f sr sa nil sr sa.
+Hint Constructors mis_stepp : verilog.
 
 Local Close Scope error_monad_scope.
 
-(*Theorem value_eq_size_if_eq:
-  forall lv rv EQ,
-  vsize lv = vsize rv -> value_eq_size lv rv = left EQ.
-Proof. intros. unfold value_eq_size.
-
-Theorem expr_run_same:
-  forall assoc e v, expr_run assoc e = OK v <-> expr_runp assoc e v.
-Proof.
-  split; generalize dependent v; generalize dependent assoc.
-  - induction e.
-    + intros. inversion H. constructor.
-    + intros. inversion H. constructor. assumption.
-    + intros. inversion H. destruct (expr_run assoc e1) eqn:?. destruct (expr_run assoc e2) eqn:?.
-      unfold eq_to_opt in H1. destruct (value_eq_size v0 v1) eqn:?. inversion H1.
-      constructor. apply IHe1. assumption. apply IHe2. assumption. reflexivity. discriminate. discriminate.
-      discriminate.
-    + intros. inversion H. destruct (expr_run assoc e) eqn:?. unfold option_map in H1.
-      inversion H1. constructor. apply IHe. assumption. reflexivity. discriminate.
-    + intros. inversion H. destruct (expr_run assoc e1) eqn:?. destruct (valueToBool v0) eqn:?.
-      eapply erun_Vternary_true. apply IHe1. eassumption. apply IHe2. eassumption. assumption.
-      eapply erun_Vternary_false. apply IHe1. eassumption. apply IHe3. eassumption. assumption.
-      discriminate.
-  - induction e.
-    + intros. inversion H. reflexivity.
-    + intros. inversion H. subst. simpl. assumption.
-    + intros. inversion H. subst. simpl. apply IHe1 in H4. rewrite H4.
-      apply IHe2 in H6. rewrite H6. unfold eq_to_opt. assert (vsize lv = vsize rv).
-      apply EQ. apply (value_eq_size_if_eq lv rv EQ) in H0. rewrite H0. reflexivity.
-    + intros. inversion H. subst. simpl. destruct (expr_run assoc e) eqn:?. simpl.
-      apply IHe in H3. rewrite Heqo in H3.
-      inversion H3. subst. reflexivity. apply IHe in H3. rewrite Heqo in H3. discriminate.
-    + intros. inversion H. subst. simpl. apply IHe1 in H4. rewrite H4. rewrite H7.
-      apply IHe2 in H6. rewrite H6. reflexivity.
-      subst. simpl. apply IHe1 in H4. rewrite H4. rewrite H7. apply IHe3.
-      assumption.
-Qed.
-
- *)
-
 Fixpoint init_params (vl : list value) (rl : list reg) {struct rl} :=
   match rl, vl with
   | r :: rl', v :: vl' => AssocMap.set r v (init_params vl' rl')
@@ -725,18 +594,24 @@ Definition empty_stack (m : module) : assocmap_arr :=
 
 Inductive step : genv -> state -> Events.trace -> state -> Prop :=
   | step_module :
-      forall asr asa asr' asa' basr1 nasr1 basa1 nasa1 f stval pstval m sf st g ist,
+      forall asr asa asr' asa' basr1 nasr1 basa1 nasa1 basr2 nasr2
+             basa2 nasa2 f stval pstval m sf st g ist,
       asr!(m.(mod_reset)) = Some (ZToValue 0) ->
       asr!(m.(mod_finish)) = Some (ZToValue 0) ->
       asr!(m.(mod_st)) = Some ist ->
       valueToPos ist = st ->
       mis_stepp f (mkassociations asr empty_assocmap)
                   (mkassociations asa (empty_stack m))
-                  m.(mod_body)
+                  (mod_body m)
                   (mkassociations basr1 nasr1)
-                  (mkassociations basa1 nasa1)->
-      asr' = merge_regs nasr1 basr1 ->
-      asa' = merge_arrs nasa1 basa1 ->
+                  (mkassociations basa1 nasa1) ->
+      mis_stepp_negedge f (mkassociations (merge_regs nasr1 basr1) empty_assocmap)
+                        (mkassociations (merge_arrs nasa1 basa1) (empty_stack m))
+                        (mod_body m)
+                        (mkassociations basr2 nasr2)
+                        (mkassociations basa2 nasa2) ->
+      asr' = merge_regs nasr2 basr2 ->
+      asa' = merge_arrs nasa2 basa2 ->
       asr'!(m.(mod_st)) = Some stval ->
       valueToPos stval = pstval ->
       step g (State sf m st asr asa) Events.E0 (State sf m pstval asr' asa')
@@ -778,6 +653,18 @@ Definition semantics (m : program) :=
   Smallstep.Semantics step (initial_state m) final_state
                       (Globalenvs.Genv.globalenv m).
 
+Fixpoint list_to_stmnt st :=
+  match st with
+  | (e, s) :: r => Stmntcons e s (list_to_stmnt r)
+  | nil => Stmntnil
+  end.
+
+Fixpoint stmnt_to_list st :=
+  match st with
+  | Stmntcons e s r => (e, s) :: stmnt_to_list r
+  | Stmntnil => nil
+  end.
+
 Lemma expr_runp_determinate :
   forall f e asr asa v,
   expr_runp f asr asa e v ->
@@ -838,8 +725,8 @@ Lemma stmnt_runp_determinate :
              | [ H : stmnt_runp _ _ _ (Vblock _ _) _ _ |- _ ] => invert H
              | [ H : stmnt_runp _ _ _ Vskip _ _ |- _ ] => invert H
              | [ H : stmnt_runp _ _ _ (Vcond _ _ _) _ _ |- _ ] => invert H
-             | [ H : stmnt_runp _ _ _ (Vcase _ (_ :: _) _) _ _ |- _ ] => invert H
-             | [ H : stmnt_runp _ _ _ (Vcase _ []  _) _ _ |- _ ] => invert H
+             | [ H : stmnt_runp _ _ _ (Vcase _ (Stmntcons _ _ _) _) _ _ |- _ ] => invert H
+             | [ H : stmnt_runp _ _ _ (Vcase _ Stmntnil  _) _ _ |- _ ] => invert H
 
              | [ H1 : expr_runp _ ?asr ?asa ?e _,
                  H2 : expr_runp _ ?asr ?asa ?e _ |- _ ] =>
@@ -872,6 +759,22 @@ Proof.
               end; crush).
 Qed.
 
+Lemma mi_stepp_negedge_determinate :
+  forall f asr0 asa0 m asr1 asa1,
+  mi_stepp_negedge f asr0 asa0 m asr1 asa1 ->
+  forall asr1' asa1',
+  mi_stepp_negedge f asr0 asa0 m asr1' asa1' ->
+  asr1' = asr1 /\ asa1' = asa1.
+Proof.
+  intros. destruct m; invert H; invert H0;
+
+  repeat (try match goal with
+              | [ H1 : stmnt_runp _ ?asr0 ?asa0 ?s _ _,
+                  H2 : stmnt_runp _ ?asr0 ?asa0 ?s _ _ |- _ ] =>
+                learn (stmnt_runp_determinate H1 H2)
+              end; crush).
+Qed.
+
 Lemma mis_stepp_determinate :
   forall f asr0 asa0 m asr1 asa1,
   mis_stepp f asr0 asa0 m asr1 asa1 ->
@@ -895,16 +798,77 @@ Proof.
               end; crush).
 Qed.
 
+Lemma mis_stepp_negedge_determinate :
+  forall f asr0 asa0 m asr1 asa1,
+  mis_stepp_negedge f asr0 asa0 m asr1 asa1 ->
+  forall asr1' asa1',
+  mis_stepp_negedge f asr0 asa0 m asr1' asa1' ->
+  asr1' = asr1 /\ asa1' = asa1.
+Proof.
+  induction 1; intros;
+
+  repeat (try match goal with
+              | [ H : mis_stepp_negedge _ _ _ [] _ _ |- _ ] => invert H
+              | [ H : mis_stepp_negedge _ _ _ ( _ :: _ ) _ _ |- _ ] => invert H
+
+              | [ H1 : mi_stepp_negedge _ ?asr0 ?asa0 ?s _ _,
+                  H2 : mi_stepp_negedge _ ?asr0 ?asa0 ?s _ _ |- _ ] =>
+                learn (mi_stepp_negedge_determinate H1 H2)
+
+             | [ H1 : forall asr1 asa1, mis_stepp_negedge _ ?asr0 ?asa0 ?m asr1 asa1 -> _,
+                 H2 : mis_stepp_negedge _ ?asr0 ?asa0 ?m _ _ |- _ ] =>
+               learn (H1 _ _ H2)
+              end; crush).
+Qed.
+
 Lemma semantics_determinate :
   forall (p: program), Smallstep.determinate (semantics p).
 Proof.
   intros. constructor; set (ge := Globalenvs.Genv.globalenv p); simplify.
   - invert H; invert H0; constructor. (* Traces are always empty *)
   - invert H; invert H0; crush. assert (f = f0) by (destruct f; destruct f0; auto); subst.
-    pose proof (mis_stepp_determinate H5 H15).
+    pose proof (mis_stepp_determinate H5 H15). simplify. inv H0. inv H4.
+    pose proof (mis_stepp_negedge_determinate H6 H17).
     crush.
   - constructor. invert H; crush.
   - invert H; invert H0; unfold ge0, ge1 in *; crush.
   - 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/Veriloggen.v b/src/hls/Veriloggen.v
index 7ace6be..1ded68a 100644
--- a/src/hls/Veriloggen.v
+++ b/src/hls/Veriloggen.v
@@ -62,6 +62,9 @@ Section TRANSLATE.
     | _ => Some it
     end.
 
+  Definition mod_body (m : HTL.module) :=
+
+
   (* FIXME Remove the fuel parameter (recursion limit)*)
   Fixpoint transl_module (fuel : nat) (prog : HTL.program) (externclk : option reg) (m : HTL.module) : res Verilog.module :=
     match fuel with
@@ -99,17 +102,33 @@ Section TRANSLATE.
       let local_scldecls := PTree.filter (fun r _ => negb (PTree.contains r externctrl)) (HTL.mod_scldecls m) in
       let scl_decls := scl_to_Vdecls (AssocMap.elements local_scldecls) in
 
-      let body : list Verilog.module_item:=
-          Valways (Vposedge clk) (Vcond (Vbinop Veq (Vvar (HTL.mod_reset m)) (Vlit (ZToValue 1)))
-                                                    (Vseq
-                                                      (Vnonblock (Vvar (HTL.mod_st m)) (Vlit (posToValue (HTL.mod_entrypoint m))))
-                                                      (Vnonblock (Vvar (HTL.mod_finish m)) (Vlit (ZToValue 0))))
-                                                    (Vcase (Vvar (HTL.mod_st m)) case_el_ctrl (Some Vskip)))
-                  :: Valways (Vposedge clk) (Vcase (Vvar (HTL.mod_st m)) case_el_data (Some Vskip))
-                  :: arr_decls
-                  ++ scl_decls
-                  ++ maybe_clk_decl
-                  ++ List.flat_map Verilog.mod_body (List.map snd (PTree.elements cleaned_modules)) in
+      let body : list Verilog.module_item :=
+          match (HTL.mod_ram m) with
+          | Some ram =>
+            Valways (Vposedge clk) (Vcond (Vbinop Veq (Vvar (HTL.mod_reset m)) (Vlit (ZToValue 1)))
+                                          (Vseq
+                                         (Vnonblock (Vvar (HTL.mod_st m)) (Vlit (posToValue (HTL.mod_entrypoint m))))
+                                         (Vnonblock (Vvar (HTL.mod_finish m)) (Vlit (ZToValue 0))))
+                                          (Vcase (Vvar (HTL.mod_st m)) case_el_ctrl (Some Vskip)))
+                    :: Valways (Vposedge clk) (Vcase (Vvar (HTL.mod_st m)) case_el_data (Some Vskip))
+                    :: inst_ram m.(HTL.mod_clk) ram
+                    :: arr_decls
+                    ++ scl_decls
+                    ++ maybe_clk_decl
+                    ++ List.flat_map Verilog.mod_body (List.map snd (PTree.elements cleaned_modules))
+          | Nothing =>
+            Valways (Vposedge clk) (Vcond (Vbinop Veq (Vvar (HTL.mod_reset m)) (Vlit (ZToValue 1)))
+                                          (Vseq
+                                         (Vnonblock (Vvar (HTL.mod_st m)) (Vlit (posToValue (HTL.mod_entrypoint m))))
+                                         (Vnonblock (Vvar (HTL.mod_finish m)) (Vlit (ZToValue 0))))
+                                          (Vcase (Vvar (HTL.mod_st m)) case_el_ctrl (Some Vskip)))
+                    :: Valways (Vposedge clk) (Vcase (Vvar (HTL.mod_st m)) case_el_data (Some Vskip))
+                    :: arr_decls
+                    ++ scl_decls
+                    ++ maybe_clk_decl
+                    ++ List.flat_map Verilog.mod_body (List.map snd (PTree.elements cleaned_modules))
+          end
+      in
 
       OK (Verilog.mkmodule
                (HTL.mod_start m)
diff --git a/src/hls/Veriloggenproof.v b/src/hls/Veriloggenproof.v
index ccb315e..c54f726 100644
--- a/src/hls/Veriloggenproof.v
+++ b/src/hls/Veriloggenproof.v
@@ -264,6 +264,116 @@ Admitted.
 (* Qed. *)
 (* Hint Resolve mis_stepp_decl : verilogproof. *)
 
+Lemma mis_stepp_negedge_decl :
+  forall l asr asa f,
+    mis_stepp_negedge f asr asa (map Vdeclaration l) asr asa.
+Proof.
+  induction l.
+  - intros. constructor.
+  - intros. simplify. econstructor. constructor. auto.
+Qed.
+Hint Resolve mis_stepp_negedge_decl : verilogproof.
+
+Lemma mod_entrypoint_equiv m : mod_entrypoint (transl_module m) = HTL.mod_entrypoint m.
+Proof. unfold transl_module; intros; destruct (HTL.mod_ram m) eqn:?; crush. Qed.
+
+Lemma mod_st_equiv m : mod_st (transl_module m) = HTL.mod_st m.
+Proof. unfold transl_module; intros; destruct (HTL.mod_ram m) eqn:?; crush. Qed.
+
+Lemma mod_stk_equiv m : mod_stk (transl_module m) = HTL.mod_stk m.
+Proof. unfold transl_module; intros; destruct (HTL.mod_ram m) eqn:?; crush. Qed.
+
+Lemma mod_stk_len_equiv m : mod_stk_len (transl_module m) = HTL.mod_stk_len m.
+Proof. unfold transl_module; intros; destruct (HTL.mod_ram m) eqn:?; crush. Qed.
+
+Lemma mod_finish_equiv m : mod_finish (transl_module m) = HTL.mod_finish m.
+Proof. unfold transl_module; intros; destruct (HTL.mod_ram m) eqn:?; crush. Qed.
+
+Lemma mod_reset_equiv m : mod_reset (transl_module m) = HTL.mod_reset m.
+Proof. unfold transl_module; intros; destruct (HTL.mod_ram m) eqn:?; crush. Qed.
+
+Lemma mod_clk_equiv m : mod_clk (transl_module m) = HTL.mod_clk m.
+Proof. unfold transl_module; intros; destruct (HTL.mod_ram m) eqn:?; crush. Qed.
+
+Lemma mod_return_equiv m : mod_return (transl_module m) = HTL.mod_return m.
+Proof. unfold transl_module; intros; destruct (HTL.mod_ram m) eqn:?; crush. Qed.
+
+Lemma mod_params_equiv m : mod_args (transl_module m) = HTL.mod_params m.
+Proof. unfold transl_module; intros; destruct (HTL.mod_ram m) eqn:?; crush. Qed.
+
+Lemma empty_stack_equiv m : empty_stack (transl_module m) = HTL.empty_stack m.
+Proof. unfold transl_module; intros; destruct (HTL.mod_ram m) eqn:?; crush. Qed.
+
+Ltac rewrite_eq := rewrite mod_return_equiv
+                   || rewrite mod_clk_equiv
+                   || rewrite mod_reset_equiv
+                   || rewrite mod_finish_equiv
+                   || rewrite mod_stk_len_equiv
+                   || rewrite mod_stk_equiv
+                   || rewrite mod_st_equiv
+                   || rewrite mod_entrypoint_equiv
+                   || rewrite mod_params_equiv
+                   || rewrite empty_stack_equiv.
+
+Lemma find_assocmap_get r i v : r ! i = Some v -> r # i = v.
+Proof.
+  intros. unfold find_assocmap, AssocMapExt.get_default. rewrite H. auto.
+Qed.
+
+Lemma ram_exec_match :
+  forall f asr asa asr' asa' r clk,
+    HTL.exec_ram asr asa (Some r) asr' asa' ->
+    mi_stepp_negedge f asr asa (inst_ram clk r) asr' asa'.
+Proof.
+  inversion 1; subst; simplify.
+  { unfold inst_ram. econstructor.
+    eapply stmnt_runp_Vcond_false.
+    econstructor. econstructor. econstructor. auto.
+    econstructor. auto.
+    simplify.
+    unfold boolToValue, natToValue, valueToBool.
+    rewrite Int.eq_sym. rewrite H3. simplify.
+    auto. constructor. }
+  { unfold inst_ram. econstructor. econstructor. econstructor.
+    econstructor. econstructor. auto.
+    econstructor. auto.
+    simplify.
+    unfold boolToValue, natToValue, valueToBool.
+    pose proof H4 as X. apply find_assocmap_get in X.
+    rewrite X. rewrite Int.eq_sym. rewrite H1. auto.
+    econstructor. econstructor. econstructor. econstructor.
+    pose proof H5 as X. apply find_assocmap_get in X.
+    rewrite X.
+    unfold valueToBool. unfold ZToValue in *.
+    unfold Int.eq in H2.
+    unfold uvalueToZ.
+    assert (Int.unsigned wr_en =? 0 = false).
+    apply Z.eqb_neq. rewrite Int.unsigned_repr in H2 by (simplify; lia).
+    destruct (zeq (Int.unsigned wr_en) 0); crush.
+    rewrite H0. auto.
+    apply stmnt_runp_Vnonblock_arr. econstructor. econstructor. auto.
+    econstructor. econstructor.
+    apply find_assocmap_get in H9. rewrite H9.
+    apply find_assocmap_get in H6. rewrite H6.
+    repeat econstructor. apply find_assocmap_get; auto.
+  }
+  { econstructor. econstructor. econstructor. econstructor. auto.
+    econstructor. auto.
+    econstructor.
+    unfold boolToValue, natToValue, valueToBool.
+    apply find_assocmap_get in H3. rewrite H3.
+    rewrite Int.eq_sym. rewrite H1. auto.
+    econstructor.
+    eapply stmnt_runp_Vcond_false. econstructor. auto.
+    simplify. apply find_assocmap_get in H4. rewrite H4.
+    auto.
+    repeat (econstructor; auto). apply find_assocmap_get in H5.
+    rewrite H5. eassumption.
+    repeat econstructor. simplify. apply find_assocmap_get; auto.
+  }
+Qed.
+
+
 Section CORRECTNESS.
 
   Variable prog: HTL.program.