Remove RTLParFu and fix DMemorygen.v

5 files changed, 1949 insertions, 1974 deletions

diff --git a/src/hls/AssocMap.v b/src/hls/AssocMap.v
index 0c9242c..18b1bc0 100644
--- a/src/hls/AssocMap.v
+++ b/src/hls/AssocMap.v
@@ -256,3 +256,51 @@ Lemma find_get_assocmap :
   assoc ! r = Some v ->
   assoc # r = v.
 Proof. intros. unfold find_assocmap, AssocMapExt.get_default. rewrite H. trivial. Qed.
+
+Lemma merge_get_default :
+  forall ars ars' r x,
+    ars ! r = Some x ->
+    (AssocMapExt.merge _ ars ars') # r = x.
+Proof.
+  unfold AssocMapExt.merge; intros.
+  unfold "#", AssocMapExt.get_default.
+  rewrite AssocMap.gcombine by auto.
+  unfold AssocMapExt.merge_atom.
+  now rewrite !H.
+Qed.
+
+Lemma merge_get_default2 :
+  forall ars ars' r,
+    ars ! r = None ->
+    (AssocMapExt.merge _ ars ars') # r = ars' # r.
+Proof.
+  unfold AssocMapExt.merge; intros.
+  unfold "#", AssocMapExt.get_default.
+  rewrite AssocMap.gcombine by auto.
+  unfold AssocMapExt.merge_atom.
+  now rewrite !H.
+Qed.
+
+Lemma merge_get_default3 :
+  forall A ars ars' r,
+    ars ! r = None ->
+    (AssocMapExt.merge A ars ars') ! r = ars' ! r.
+Proof.
+  unfold AssocMapExt.merge; intros.
+  unfold "#", AssocMapExt.get_default.
+  rewrite AssocMap.gcombine by auto.
+  unfold AssocMapExt.merge_atom.
+  now rewrite !H.
+Qed.
+
+Lemma merge_get_default4 :
+  forall A ars ars' r x,
+    ars ! r = Some x ->
+    (AssocMapExt.merge A ars ars') ! r = Some x.
+Proof.
+  unfold AssocMapExt.merge; intros.
+  unfold "#", AssocMapExt.get_default.
+  rewrite AssocMap.gcombine by auto.
+  unfold AssocMapExt.merge_atom.
+  now rewrite !H.
+Qed.
diff --git a/src/hls/DMemorygen.v b/src/hls/DMemorygen.v
index 6251162..3f6ee5e 100644
--- a/src/hls/DMemorygen.v
+++ b/src/hls/DMemorygen.v
@@ -99,7 +99,7 @@ Fixpoint expr_eqb (e1 e2: expr): bool :=
   | Vlit v, Vlit v' => Int.eq v v'
   | Vvar r, Vvar r' => Pos.eqb r r'
   | Vvari r e, Vvari r' e' => Pos.eqb r r' && expr_eqb e e'
-  | Vrange r e1 e2, Vrange r' e1' e2' => 
+  | Vrange r e1 e2, Vrange r' e1' e2' =>
     Pos.eqb r r' && expr_eqb e1 e1' && expr_eqb e2 e2'
   | Vinputvar r, Vinputvar r' => Pos.eqb r r'
   | Vbinop b e1 e2, Vbinop b' e1' e2' =>
@@ -115,7 +115,7 @@ Fixpoint stmnt_eqb (s1 s2: stmnt): bool :=
   match s1, s2 with
   | Vskip, Vskip => true
   | Vseq s1 s2, Vseq s1' s2' => stmnt_eqb s1 s1' && stmnt_eqb s2 s2'
-  | Vcond e st sf, Vcond e' st' sf' => 
+  | Vcond e st sf, Vcond e' st' sf' =>
     expr_eqb e e'
     && stmnt_eqb st st'
     && stmnt_eqb sf sf'
@@ -130,7 +130,7 @@ Fixpoint stmnt_eqb (s1 s2: stmnt): bool :=
   | _, _ => false
   end
 with stmnt_expr_list_eqb (s1 s2: stmnt_expr_list): bool :=
-  match s1, s2 with 
+  match s1, s2 with
   | Stmntnil, Stmntnil => true
   | Stmntcons e s sl, Stmntcons e' s' sl' =>
     expr_eqb e e'
@@ -141,7 +141,7 @@ with stmnt_expr_list_eqb (s1 s2: stmnt_expr_list): bool :=
 
 Fixpoint replace_stmnt (base r b: stmnt): stmnt :=
   match base with
-  | Vskip as st | Vblock _ _ as st | Vnonblock _ _ as st => 
+  | Vskip as st | Vblock _ _ as st | Vnonblock _ _ as st =>
     if stmnt_eqb st r then b else st
   | Vseq s1 s2 =>
     Vseq (replace_stmnt s1 r b) (replace_stmnt s2 r b)
@@ -155,7 +155,7 @@ Fixpoint replace_stmnt (base r b: stmnt): stmnt :=
 with replace_stmnt_expr_list (base: stmnt_expr_list) (r b: stmnt) :=
   match base with
   | Stmntnil => Stmntnil
-  | Stmntcons e s sl => 
+  | Stmntcons e s sl =>
     Stmntcons e (replace_stmnt s r b) (replace_stmnt_expr_list sl r b)
   end.
 
@@ -205,34 +205,19 @@ Proof.
   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.
+  apply AssocMapExt.elements_iff in H0. inv H0.
+  rewrite AssocMap.gss in H3. inv H3; auto.
+  apply AssocMapExt.elements_iff in H0. inv H0.
+  repeat rewrite AssocMap.gso in H3 by lia. unfold map_well_formed in H.
+  eapply H. eapply AssocMapExt.elements_iff; eauto.
+  unfold map_well_formed in *; intros.
+  apply AssocMapExt.elements_iff in H0. inv H0.
+  destruct (peq p p1); subst.
+  + rewrite PTree.gss in H1.
+    eapply H. eapply AssocMapExt.elements_iff; eauto.
+  + rewrite PTree.gso in H1 by auto. eapply H.
+    eapply AssocMapExt.elements_iff; eauto.
+Qed.
 
 Definition max_pc {A: Type} (m: PTree.t A) :=
   fold_right Pos.max 1%positive (map fst (PTree.elements m)).
@@ -294,9 +279,9 @@ Lemma transf_code_wf' :
     map_well_formed d'.
 Proof.
   induction l; intros; simpl in *. inv H0; auto.
-  remember (fold_right (transf_maps state ram) d l). (* destruct p. *)
-(*   apply transf_maps_wf in H0. auto. eapply IHl; eauto. *)
-(* Qed. *) Admitted.
+  remember (fold_right (transf_maps state ram) d l).
+  apply transf_maps_wf in H0. auto. eapply IHl; eauto.
+Qed.
 
 Lemma transf_code_wf :
   forall d state ram d',
@@ -564,9 +549,9 @@ Lemma forall_ram_lt :
     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 HTL.max_reg_module; repeat apply X; *)
-  (* unfold HTL.max_reg_ram; rewrite H; try lia. *)
-Admitted.
+  unfold forall_ram; simplify; unfold DHTL.max_reg_module; repeat apply X;
+  unfold DHTL.max_reg_ram; rewrite H; try lia.
+Qed.
 #[local] Hint Resolve forall_ram_lt : mgen.
 
 Definition exec_all d_s c_s rs1 ar1 rs3 ar3 :=
@@ -580,12 +565,27 @@ Definition exec_all_ram r d_s c_s rs1 ar1 rs4 ar4 :=
     /\ 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.
 
+(* This is not actually correct. *)
 (* Lemma merge_reg_idempotent : *)
 (*   forall rs p,  *)
 (*     match_reg_assocs p (merge_reg_assocs (merge_reg_assocs rs)) (merge_reg_assocs rs). *)
 (* Proof. intros. unfold merge_reg_assocs. cbn. unfold merge_regs.  *)
 (* #[global] Hint Rewrite merge_reg_idempotent : mgen. *)
 
+Ltac simplify_local := intros; unfold_constants; cbn in *;
+                         repeat (nicify_hypotheses; nicify_goals; kill_bools; substpp);
+                         cbn in *.
+
+Ltac simplify_val := repeat (simplify_local; unfold uvalueToZ, valueToPtr, Ptrofs.of_int, valueToInt, intToValue,
+                               ptrToValue in *).
+
+Ltac crush_val := simplify_val; try discriminate; try congruence; try lia; liapp; try assumption.
+
+Ltac crush_local := simplify_local; try discriminate; try congruence; try lia; liapp;
+              try assumption; auto.
+
+Ltac mgen_crush_local := crush_local; eauto with mgen.
+
 Lemma merge_arr_idempotent :
   forall ar st len v v',
     (assoc_nonblocking ar)!st = Some v ->
@@ -597,21 +597,21 @@ Lemma merge_arr_idempotent :
     /\ (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.
+  split; simplify_local; 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. *) Admitted.
+  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_local.
+  rewrite list_combine_length.
+  rewrite (arr_wf v). rewrite (arr_wf v').
+  lia.
+Qed.
 
 Lemma empty_arr :
   forall m s,
@@ -632,24 +632,24 @@ Lemma merge_arr_empty':
 Proof.
   inversion 1; subst.
   pose proof (empty_arr m s).
-  simplify.
+  simplify_local.
   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. *) Admitted.
+    learn H3 as H5. apply H0 in H5. inv H5. simplify_local.
+    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_local.
+    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',
@@ -670,24 +670,24 @@ Lemma merge_arr_empty'':
 Proof.
   inversion 1; subst.
   pose proof (empty_arr m s).
-  simplify.
+  simplify_local.
   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. *) Admitted.
+    learn H3 as H5. apply H0 in H5. inv H5. simplify_local.
+    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_local.
+    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,
@@ -695,17 +695,17 @@ Lemma merge_arr_empty_match :
     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.
+  constructor; simplify_local.
+  learn H3 as H4. apply H0 in H4. inv H4. simplify_local.
   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. *) Admitted.
+  split; simplify_local.
+  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.
 #[local] Hint Resolve merge_arr_empty_match : mgen.
 
 Definition ram_present {A: Type} ar r v v' :=
@@ -1044,89 +1044,87 @@ Qed.
 
 Lemma transf_not_changed :
   forall state ram n d i d_s,
-    (forall e1 e2 r, d_s <> Vnonblock (Vvari r e1) e2) ->
-    (forall e1 e2 r, d_s <> Vnonblock e1 (Vvari r e2)) ->
+    (forall e1 e2 e3 e4 r, d_s <> (Vseq (Vblock (Vvar e1) e2) (Vblock (Vvari r e3) e4))) ->
+    (forall e1 e2 e3 e4 r, d_s <> (Vseq (Vblock (Vvar e1) e2) (Vblock e3 (Vvari r e4)))) ->
     d!i = Some d_s ->
     transf_maps state ram (i, n) d = d.
-Proof. intros; unfold transf_maps; repeat destruct_match; mgen_crush. Admitted.
-
-(* 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. *)
+Proof. intros; unfold transf_maps; repeat destruct_match; mgen_crush. 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 transf_not_changed_neq :
+  forall state ram n d d' i a d_s,
+    transf_maps state ram (a, n) d = d' ->
+    d!i = Some d_s ->
+    a <> i -> n <> i ->
+    d'!i = Some d_s.
+Proof.
+  unfold transf_maps; intros; repeat destruct_match; subst; mgen_crush;
+  repeat (rewrite AssocMap.gso; auto).
+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 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_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. *)
-(* #[local] Hint Resolve elements_correct_none : assocmap. *)
+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_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. *)
+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.
+#[local] 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.
@@ -1176,965 +1174,963 @@ Proof.
 Qed.
 #[local] 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. *)
-(* #[local] 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. *)
-(* #[local] 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. *)
-(* #[local] 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. *)
-(* #[local] 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. *)
-(* #[local] 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. *)
-(* #[local] 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. *)
-(* #[local] 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. *)
-(* #[local] 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. *)
-(* #[local] 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. *)
-(* #[local] 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. *)
-(* #[local] 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. *)
-(* #[local] 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. *)
-(* #[local] 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. *)
-(* #[local] 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. *)
-(* #[local] 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. *)
-(* #[local] 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. *)
-(* #[local] 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. *)
-(* #[local] 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. *)
-(* #[local] 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. *)
-(* #[local] 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. *)
-(* #[local] 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. *)
-(* #[local] 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. *)
-(* #[local] 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. *)
-(* #[local] 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. *)
-(* #[local] 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. *)
-(* #[local] Hint Rewrite empty_stack_m : mgen. *)
-
-(* Ltac clear_forall := *)
-(*   repeat match goal with *)
-(*   | H: context[forall _, _] |- _ => clear H *)
-(*   end. *)
+Lemma max_module_stmnts :
+  forall m,
+    max_stmnt_tree (mod_datapath m) < max_reg_module m + 1.
+Proof. intros. unfold max_reg_module. lia. Qed.
+#[local] Hint Resolve max_module_stmnts : mgen.
 
-(* 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. inv H. *)
-(*   destruct n; simpl in *. *)
-(*   inv 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. *)
+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_datapath (transf_module m))).
+Proof. unfold transf_module; intros; repeat destruct_match; crush. Qed.
+#[local] 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.
+#[local] 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.
+#[local] 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.
+#[local] 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.
+#[local] 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.
+#[local] 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.
+#[local] 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.
+#[local] 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.
+#[local] Hint Resolve mod_reset_modify : mgen.
 
-(*   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. inv H. *)
-(*   destruct n; simpl in *. *)
-(*   inv 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. *)
+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.
+#[local] Hint Resolve mod_finish_modify : mgen.
 
-(*   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. *)
+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.
+#[local] Hint Resolve mod_return_modify : mgen.
 
-(* 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 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.
+#[local] Hint Resolve mod_start_modify : mgen.
 
-(* 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. *)
+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.
+#[local] Hint Resolve mod_st_modify : mgen.
 
-(* Ltac clear_learnt := *)
-(*   repeat match goal with *)
-(*   | H: Learnt _ |- _ => clear H *)
-(*   end. *)
+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.
+#[local] Hint Resolve match_arrs_read : mgen.
 
-(* 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. *)
-(* #[local] 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. *)
+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.
+#[local] Hint Resolve match_reg_implies_equal : mgen.
 
-(* Definition all_match_empty_size m ar := *)
-(*   match_empty_size m (assoc_nonblocking ar) /\ match_empty_size m (assoc_blocking ar). *)
-(* #[local] Hint Unfold all_match_empty_size : 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.
 
-(* Definition match_module_to_ram m ram := *)
-(*   ram_size ram = mod_stk_len m /\ ram_mem ram = mod_stk m. *)
-(* #[local] Hint Unfold match_module_to_ram : mgen. *)
+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.
+#[local] 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 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 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.
+#[local] 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.
+#[local] 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.
+#[local] 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.
+#[local] 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.
+#[local] 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.
+#[local] 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.
+#[local] 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.
+#[local] 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.
+#[local] 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. inv H.
+  destruct n; simpl in *.
+  inv 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. inv H.
+  destruct n; simpl in *.
+  inv 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.
+#[local] 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).
+#[local] 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.
+#[local] 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, *)
@@ -2192,348 +2188,330 @@ Qed.
 (*     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. *) Admitted. *)
-(* #[local] Hint Resolve merge_arr_empty2 : mgen. *)
+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 d': AssocMap.t stmnt) i := d ! i = d' ! i.
+
+Definition alt_store ram (d d': AssocMap.t stmnt) i :=
+  exists e1 e2 rest,
+    d' ! i = Some (Vseq rest (Vseq (Vblock (Vvar (ram_u_en ram)) (Vunop Vnot (Vvar (ram_u_en ram))))
+                        (Vseq (Vblock (Vvar (ram_wr_en ram)) (Vlit (ZToValue 1)))
+                              (Vseq (Vblock (Vvar (ram_d_in ram)) e2)
+                                    (Vblock (Vvar (ram_addr ram)) e1)))))
+    /\ d ! i = Some (Vseq rest (Vblock (Vvari (ram_mem ram) e1) e2)).
+
+Definition alt_load state ram (d d': AssocMap.t stmnt) i n :=
+  exists ns e1 e2,
+    d' ! i = Some (Vseq (Vblock (Vvar state) (Vlit (posToValue n))) (Vseq (Vblock (Vvar (ram_u_en ram)) (Vunop Vnot (Vvar (ram_u_en ram))))
+                        (Vseq (Vblock (Vvar (ram_wr_en ram)) (Vlit (ZToValue 0)))
+                              (Vblock (Vvar (ram_addr ram)) e2))))
+    /\ d' ! n = Some (Vseq (Vblock (Vvar state) ns) (Vblock (Vvar e1) (Vvar (ram_d_out ram))))
+    /\ d ! i = Some (Vseq (Vblock (Vvar state) ns) (Vblock (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 d' i n :=
+  alt_unchanged d d' i
+  \/ alt_store ram d d' i
+  \/ alt_load state ram d d' i n.
+
+Lemma transf_alternatives :
+  forall ram n d state i d',
+    transf_maps state ram (i, n) d = d' ->
+    i <> n ->
+    alternatives state ram d d' i n.
+Proof.
+  intros. unfold transf_maps in *.
+  repeat destruct_match; subst; try 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[Vblock (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 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 transf_alternatives_neq :
+  forall state ram a n' n d'' d' i d,
+    transf_maps state ram (a, n) d = d' ->
+    a <> i -> n' <> n -> i <> n' -> a <> n' ->
+    i <> n -> a <> n ->
+    alternatives state ram d'' d i n' ->
+    alternatives state ram d'' d' 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 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 transf_alternatives_neq2 :
+  forall state ram a n' n d'' d' i d,
+    transf_maps state ram (a, n) d' = d ->
+    a <> i -> n' <> n -> i <> n' -> a <> n' -> i <> n ->
+    alternatives state ram d d'' i n' ->
+    alternatives state ram d' d'' 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 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 transf_alt_unchanged_neq :
+  forall i d'' d d',
+    alt_unchanged d' d'' i ->
+    d' ! i = d ! i ->
+    alt_unchanged d d'' i.
+Proof. unfold alt_unchanged; simplify; congruence. Qed.
+
+Lemma transf_maps_neq :
+  forall state ram d i n d' i' n' va vb,
+    transf_maps state ram (i, n) d = d' ->
+    d ! i' = va -> d ! n' = vb ->
+    i <> i' -> i <> n' -> n <> i' -> n <> n' ->
+    d' ! i' = va /\ d' ! n' = vb.
+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 d'' d' 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 l = d' ->
+    alternatives state ram d' d'' i n ->
+    alternatives state ram d d'' 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 d' i n d_s,
+    fold_right (transf_maps state ram) d l = d' ->
+    max_pc d < n ->
+    Forall (Pos.lt (max_pc d)) (map snd l) ->
+    Forall (Pos.ge (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 ->
+    alternatives state ram d d' 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 ?l) = (_, _) |- _ =>
+           let X := fresh "X" in
+           remember (fold_right (transf_maps s r) d l) as X
+         | X: _ * _ |- _ => destruct X
+         | H: (_, _) = _ |- _ => symmetry in H
+         end; subst.
+  match goal with H: _ \/ _ |- _ => inv H end.
+  match goal with H: (_, _) = (_, _) |- _ => inv H end. 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 H6; 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 d' i d_s,
+    transf_code state ram d = d' ->
+    d ! i = Some d_s ->
+    exists n, alternatives state ram d d' 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 H1. intros. inv H2. simplify.
+  instantiate (1 := (max_pc d + 1)) in H2.
+  exists x.
+  eapply transf_fold_alternatives;
+  eauto using forall_gt, PTree.elements_keys_norepet, max_index. lia.
+  assert (Forall (Pos.le ((max_pc d) + 1))
+    (map snd (zip_range ((max_pc d) + 1)
+                        (map fst (PTree.elements d))))) by apply zip_range_forall_le.
+  apply Forall_forall; intros. eapply Forall_forall in H3; eauto. lia.
+  rewrite zip_range_fst_idem. apply Forall_forall; intros.
+  apply AssocMapExt.elements_iff in H3. inv H3. apply max_index in H4. 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_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_local.
+  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.
+#[local] 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, *)
@@ -2541,85 +2519,79 @@ Qed.
 (*     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 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. *)
+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 basr2 nasr2 nasa2 basa2 nasr3 basr3
+         nasa3 basa3 asr'0 asa'0 res' st tge pstval sf asa data f,
+    asr ! (mod_reset m) = Some (ZToValue 0) ->
+    asr ! (mod_finish m) = Some (ZToValue 0) ->
+    asr ! (mod_st m) = Some (posToValue st) ->
+    (mod_datapath m) ! st = Some data ->
+    stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := empty_assocmap |}
+               {| assoc_blocking := asa; assoc_nonblocking := empty_stack m |} 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. Admitted.
+  (* 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 *)
@@ -3019,48 +2991,51 @@ Qed.
 (* (*     } *) *)
 (* (* Qed. *) Admitted. *)
 
-(* 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. *) Admitted. *)
+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_local.
+  - rewrite H6. repeat rewrite merge_get_default2 by auto. auto.
+  - unfold merge_regs. rewrite H12. pose proof (ram_ordering r).
+    erewrite 1 ! merge_get_default; [erewrite 1 ! merge_get_default2|];
+      [| rewrite AssocMap.gso by lia | rewrite AssocMap.gss ]; auto.
+    unfold "#", AssocMapExt.get_default. rewrite H4.
+    apply Int.eq_true.
+  - unfold merge_regs. rewrite H11.
+    pose proof (ram_ordering r).
+    erewrite 1 ! merge_get_default;
+      [erewrite 1 ! merge_get_default2|];
+      [| now repeat rewrite AssocMap.gso by lia | now rewrite AssocMap.gss].
+    unfold "#", AssocMapExt.get_default. 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. *)
-(* #[local] Hint Resolve disable_ram_set_gso : mgen. *)
+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.
+#[local] Hint Resolve disable_ram_set_gso : mgen.
 
-(* Lemma disable_ram_None rs : disable_ram None rs. *)
-(* Proof. unfold disable_ram; auto. Qed. *)
-(* #[local] Hint Resolve disable_ram_None : mgen. *)
+Lemma disable_ram_None rs : disable_ram None rs.
+Proof. unfold disable_ram; auto. Qed.
+#[local] 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 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. *)
+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.
 
@@ -3102,207 +3077,207 @@ Section CORRECTNESS.
   Proof (Genv.senv_transf TRANSL).
   #[local] 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. *)
-  (* #[local] 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. *)
-  (* #[local] 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. *)
-  (* #[local] Hint Resolve transf_final_states : 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. *) admit.
+    - eapply translation_correct; eauto.
+    - do 2 econstructor. apply Smallstep.plus_one.
+      apply step_finish; mgen_crush. constructor; eauto.
+    - do 2 econstructor. apply Smallstep.plus_one.
+      apply step_finish; mgen_crush. econstructor; eauto.
+    - 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.
+  Admitted.
+  #[local] 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.
+  #[local] 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.
+  #[local] 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. *) Admitted.
+    eapply Smallstep.forward_simulation_plus; mgen_crush.
+    apply senv_preserved.
+  Qed.
 
 End CORRECTNESS.
diff --git a/src/hls/HTLgenproof.v b/src/hls/HTLgenproof.v
index 75ee2fb..1668580 100644
--- a/src/hls/HTLgenproof.v
+++ b/src/hls/HTLgenproof.v
@@ -1083,54 +1083,6 @@ Ltac unfold_merge :=
   Ltac small_tac := repeat (crush_val; try array; try ptrofs); crush_val; auto.
   Ltac big_tac := repeat (crush_val; try array; try ptrofs; try tac0); crush_val; auto.
 
-  Lemma merge_get_default :
-    forall ars ars' r x,
-      ars ! r = Some x ->
-      (AssocMapExt.merge _ ars ars') # r = x.
-  Proof.
-    unfold AssocMapExt.merge; intros.
-    unfold "#", AssocMapExt.get_default.
-    rewrite AssocMap.gcombine by auto.
-    unfold AssocMapExt.merge_atom. 
-    now rewrite !H.
-  Qed.
-
-  Lemma merge_get_default2 :
-    forall ars ars' r,
-      ars ! r = None ->
-      (AssocMapExt.merge _ ars ars') # r = ars' # r.
-  Proof.
-    unfold AssocMapExt.merge; intros.
-    unfold "#", AssocMapExt.get_default.
-    rewrite AssocMap.gcombine by auto.
-    unfold AssocMapExt.merge_atom. 
-    now rewrite !H.
-  Qed.
-
-  Lemma merge_get_default3 :
-    forall A ars ars' r,
-      ars ! r = None ->
-      (AssocMapExt.merge A ars ars') ! r = ars' ! r.
-  Proof.
-    unfold AssocMapExt.merge; intros.
-    unfold "#", AssocMapExt.get_default.
-    rewrite AssocMap.gcombine by auto.
-    unfold AssocMapExt.merge_atom.
-    now rewrite !H.
-  Qed.
-
-  Lemma merge_get_default4 :
-    forall A ars ars' r x,
-      ars ! r = Some x ->
-      (AssocMapExt.merge A ars ars') ! r = Some x.
-  Proof.
-    unfold AssocMapExt.merge; intros.
-    unfold "#", AssocMapExt.get_default.
-    rewrite AssocMap.gcombine by auto.
-    unfold AssocMapExt.merge_atom. 
-    now rewrite !H.
-  Qed.
-
   Lemma match_assocmaps_merge_empty:
     forall f rs ars,
       match_assocmaps f rs ars ->
@@ -1154,7 +1106,7 @@ Ltac unfold_merge :=
   Proof.
     intros * YFRL YMATCH.
     inv YMATCH. constructor; intros x' YPLE.
-    unfold "#", AssocMapExt.get_default in *. 
+    unfold "#", AssocMapExt.get_default in *.
     rewrite <- YFRL by auto.
     eauto.
   Qed.
@@ -1177,7 +1129,7 @@ Ltac unfold_merge :=
     apply Smallstep.plus_one.
     eapply HTL.step_module; eauto.
     inv CONST; assumption.
-    inv CONST; assumption. 
+    inv CONST; assumption.
     (* processing of state *)
     econstructor.
     crush.
@@ -1199,7 +1151,7 @@ Ltac unfold_merge :=
       rewrite !AssocMap.gcombine by auto. rewrite !AssocMap.gss.
       setoid_rewrite H1.
       repeat erewrite Verilog.merge_arr_empty2; eauto.
-    - inv CONST; cbn in *. constructor; cbn in *. 
+    - inv CONST; cbn in *. constructor; cbn in *.
       + repeat unfold_merge. rewrite AssocMap.gso by lia.
         unfold_merge; auto.
       + repeat unfold_merge. rewrite AssocMap.gso by lia.
@@ -2683,7 +2635,7 @@ Ltac unfold_merge :=
   (*         Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ match_states (RTL.State s f sp pc' rs m) R2. *)
   (* Proof. *)
   (*   intros s f sp pc rs m arg tbl n pc' H H0 H1 R1 MSTATE. *)
-  
+
   (* #[local] Hint Resolve transl_ijumptable_correct : htlproof.*)
 
   Lemma transl_ireturn_correct:
diff --git a/src/hls/RTLParFU.v b/src/hls/RTLParFU.v
index b28c0ee..f97ed95 100644
--- a/src/hls/RTLParFU.v
+++ b/src/hls/RTLParFU.v
@@ -378,14 +378,14 @@ Definition max_reg_bblock (m : positive) (pc : node) (bb : bblock) :=
   let max_body := fold_left (fun x l => fold_left (fun x' l' => fold_left max_reg_instr l' x') l x) bb.(bb_body) m in
   max_reg_cfi max_body bb.(bb_exit).
 
-Definition max_reg_function (f: function) :=
-  Pos.max
-    (PTree.fold max_reg_bblock f.(fn_code) 1%positive)
-    (Pos.max (fold_left Pos.max f.(fn_params) 1%positive)
-             (max_reg_resources f.(fn_funct_units))).
-
-Definition max_pc_function (f: function) : positive :=
-  PTree.fold (fun m pc i => (Pos.max m
-                                     (pc + match Zlength i.(bb_body)
-                                           with Z.pos p => p | _ => 1 end))%positive)
-             f.(fn_code) 1%positive.
+(* Definition max_reg_function (f: function) := *)
+(*   Pos.max *)
+(*     (PTree.fold max_reg_bblock f.(fn_code) 1%positive) *)
+(*     (Pos.max (fold_left Pos.max f.(fn_params) 1%positive) *)
+(*              (max_reg_resources f.(fn_funct_units))). *)
+
+(* Definition max_pc_function (f: function) : positive := *)
+(*   PTree.fold (fun m pc i => (Pos.max m *)
+(*                                      (pc + match Zlength i.(bb_body) *)
+(*                                            with Z.pos p => p | _ => 1 end))%positive) *)
+(*              f.(fn_code) 1%positive. *)
diff --git a/src/hls/RTLParFUgen.v b/src/hls/RTLParFUgen.v
index a15be1c..f1b3ba6 100644
--- a/src/hls/RTLParFUgen.v
+++ b/src/hls/RTLParFUgen.v
@@ -35,143 +35,143 @@ Require Import vericert.hls.GiblePar.
 Require Import vericert.hls.RTLParFU.
 Require Import vericert.hls.FunctionalUnits.
 
-#[local] Open Scope error_monad_scope.
-
-Definition update {A: Type} (i: positive) (f: option A -> A) (pt: PTree.t A) :=
-  PTree.set i (f (pt ! i)) pt.
-
-Definition add_instr (instr_: instr) x :=
-  match x with Some i => instr_ :: i | None => instr_ :: nil end.
-
-Definition transl_instr (res: resources) (cycle: positive) (i: Gible.instr)
-           (li: Errors.res (list instr * PTree.t (list instr))):
-  Errors.res (list instr * PTree.t (list instr)) :=
-  do (instr_list, d_tree) <- li;
-  match i with
-  | RBnop => Errors.OK (FUnop :: instr_list, d_tree)
-  | RBop po op args d => Errors.OK (FUop po op args d :: instr_list, d_tree)
-  | RBload po chunk addr args d =>
-      match get_ram 0 res with
-      | Some (ri, r) =>
-          Errors.OK (FUop po Op.Onot (ram_u_en r::nil) (ram_u_en r)
-                          :: FUop po (Op.Ointconst (Int.repr 0)) nil (ram_wr_en r)
-                          :: FUop po (Op.Olea addr) args (ram_addr r)
-                          :: FUop po (Op.Oshruimm (Int.repr 2)) ((ram_addr r)::nil) (ram_addr r)
-                          :: instr_list, update (Pos.pred cycle)
-                                                (add_instr (FUop po Op.Omove (ram_d_out r::nil) d))
-                                                d_tree)
-      | _ => Errors.Error (Errors.msg "Could not find RAM")
-      end
-  | RBstore po chunk addr args d =>
-      match get_ram 0 res with
-      | Some (ri, r) =>
-          Errors.OK (FUop po Op.Onot (ram_u_en r::nil) (ram_u_en r)
-                          :: FUop po (Op.Ointconst (Int.repr 1)) nil (ram_wr_en r)
-                          :: FUop po Op.Omove (d::nil) (ram_d_in r)
-                          :: FUop po (Op.Olea addr) args (ram_addr r)
-                          :: FUop po (Op.Oshruimm (Int.repr 2)) ((ram_addr r)::nil) (ram_addr r)
-                          :: instr_list, d_tree)
-      | _ => Errors.Error (Errors.msg "Could not find RAM")
-      end
-  | RBsetpred op c args p => Errors.OK (FUsetpred op c args p :: instr_list, d_tree)
-  | RBexit po cf => Errors.Error (Errors.msg "Wrong.")
-  end.
-
-Definition transl_cf_instr (i: Gible.cf_instr): RTLParFU.cf_instr :=
-  match i with
-  | RBcall sig r args d n => FUcall sig r args d n
-  | RBtailcall sig r args => FUtailcall sig r args
-  | RBbuiltin ef args r n => FUbuiltin ef args r n
-  | RBcond c args n1 n2 => FUcond c args n1 n2
-  | RBjumptable r ns => FUjumptable r ns
-  | RBreturn r => FUreturn r
-  | RBgoto n => FUgoto n
-  end.
-
-Definition list_split {A:Type} (l: list (Z * A)) : (list (Z * A)) * (list (Z * A)) :=
-  (filter (fun x => Z.eqb 0 (fst x)) l,
-    map (fun x => (Z.pred (fst x), snd x)) (filter (fun x => negb (Z.eqb 0 (fst x))) l)).
-
-Fixpoint map_error {A B : Type} (f : A -> res B) (l : list A) {struct l} : res (list B) :=
-  match l with
-  | nil => OK nil
-  | x::xs =>
-    do y <- f x ;
-    do ys <- map_error f xs ;
-    OK (y::ys)
-  end.
-
-Definition transl_op_chain_block (res: resources) (cycle: positive) (instrs: list Gible.instr)
-           (state: Errors.res (list (list instr) * PTree.t (list instr)))
-  : Errors.res (list (list instr) * PTree.t (list instr)) :=
-  do (li, tr) <- state;
-  do (li', tr') <- fold_right (transl_instr res cycle) (OK (nil, tr)) instrs;
-  OK (li' :: li, tr').
-
-(*Compute transl_op_chain_block initial_resources 10%nat (RBop None (Op.Ointconst (Int.repr 1)) nil 1%positive::RBnop::RBnop::RBnop::nil) (OK (nil, PTree.empty _)).*)
-
-Definition transl_par_block (res: resources) (cycle: positive) (instrs: list (list Gible.instr))
-           (state: Errors.res (list (list (list instr)) * PTree.t (list instr)))
-  : Errors.res (list (list (list instr)) * PTree.t (list instr)) :=
-  do (li, tr) <- state;
-  do (li', tr') <- fold_right (transl_op_chain_block res cycle) (OK (nil, tr)) instrs;
-  OK (li' :: li, tr').
-
-(*Compute transl_par_block initial_resources 10%nat ((RBop None (Op.Ointconst (Int.repr 1)) nil 1%positive::RBnop::nil)::(RBop None (Op.Ointconst (Int.repr 2)) nil 2%positive::RBnop::nil)::nil) (OK (((FUnop::nil)::nil)::nil, PTree.empty _)).*)
-
-Definition transl_seq_block (res: resources) (b: list (list Gible.instr))
-           (a: Errors.res (list (list (list instr)) * PTree.t (list instr) * positive)) :=
-  do (litr, n) <- a;
-  let (li, tr) := litr in
-  do (li', tr') <- transl_par_block res n b (OK (li, tr));
-  OK (li', tr', (n+1)%positive).
-
-Definition insert_extra (pt: PTree.t (list instr)) (curr: list (list instr))
-         (cycle_bb: (positive * list (list (list instr)))) :=
-  let (cycle, bb) := cycle_bb in
-  match pt ! cycle with
-  | Some instrs => ((cycle + 1)%positive, (curr ++ (map (fun x => x :: nil) instrs)) :: bb)
-  | None => ((cycle + 1)%positive, curr :: bb)
-  end.
-
-Definition transl_bb (res: resources) (bb: ParBB.t): Errors.res RTLParFU.bblock_body :=
-  do (litr, n) <- fold_right (transl_seq_block res) (OK (nil, PTree.empty _, 1%positive)) bb;
-  let (li, tr) := litr in
-  OK (snd (fold_right (insert_extra tr) (1%positive, nil) li)).
-
-(*Definition transl_bblock (res: resources) (bb: ParBB.t): Errors.res ParBB.t :=
-  transl_bb res bb.
-
-Definition error_map_ptree {A B: Type} (f: positive -> A -> res B) (pt: PTree.t A) :=
-  do ptl' <- map_error (fun x => do x' <- uncurry f x; OK (fst x, x')) (PTree.elements pt);
-  OK (PTree_Properties.of_list ptl').
-
-Definition transl_code (fu: resources) (c: RTLPar.code): res code :=
-   error_map_ptree (fun _ => transl_bblock fu) c.
-
-Definition transl_function (f: RTLPar.function): Errors.res RTLParFU.function :=
-  let max := RTLPar.max_reg_function f in
-  let fu := set_res (Ram (mk_ram
-                            (Z.to_nat (RTLBlockInstr.fn_stacksize f))
-                            (max+1)%positive
-                            (max+3)%positive
-                            (max+7)%positive
-                            (max+2)%positive
-                            (max+6)%positive
-                            (max+4)%positive
-                            (max+5)%positive
-                    )) initial_resources in
-  do c' <- transl_code fu (RTLBlockInstr.fn_code f);
-  Errors.OK (mkfunction (RTLBlockInstr.fn_sig f)
-                        (RTLBlockInstr.fn_params f)
-                        (RTLBlockInstr.fn_stacksize f)
-                        c'
-                        fu
-                        (RTLBlockInstr.fn_entrypoint f)).
-
-Definition transl_fundef p :=
-  transf_partial_fundef transl_function p.
-
-Definition transl_program (p : RTLPar.program) : Errors.res RTLParFU.program :=
-  transform_partial_program transl_fundef p.
-*)
+(* #[local] Open Scope error_monad_scope. *)
+
+(* Definition update {A: Type} (i: positive) (f: option A -> A) (pt: PTree.t A) := *)
+(*   PTree.set i (f (pt ! i)) pt. *)
+
+(* Definition add_instr (instr_: instr) x := *)
+(*   match x with Some i => instr_ :: i | None => instr_ :: nil end. *)
+
+(* Definition transl_instr (res: resources) (cycle: positive) (i: Gible.instr) *)
+(*            (li: Errors.res (list instr * PTree.t (list instr))): *)
+(*   Errors.res (list instr * PTree.t (list instr)) := *)
+(*   do (instr_list, d_tree) <- li; *)
+(*   match i with *)
+(*   | RBnop => Errors.OK (FUnop :: instr_list, d_tree) *)
+(*   | RBop po op args d => Errors.OK (FUop po op args d :: instr_list, d_tree) *)
+(*   | RBload po chunk addr args d => *)
+(*       match get_ram 0 res with *)
+(*       | Some (ri, r) => *)
+(*           Errors.OK (FUop po Op.Onot (ram_u_en r::nil) (ram_u_en r) *)
+(*                           :: FUop po (Op.Ointconst (Int.repr 0)) nil (ram_wr_en r) *)
+(*                           :: FUop po (Op.Olea addr) args (ram_addr r) *)
+(*                           :: FUop po (Op.Oshruimm (Int.repr 2)) ((ram_addr r)::nil) (ram_addr r) *)
+(*                           :: instr_list, update (Pos.pred cycle) *)
+(*                                                 (add_instr (FUop po Op.Omove (ram_d_out r::nil) d)) *)
+(*                                                 d_tree) *)
+(*       | _ => Errors.Error (Errors.msg "Could not find RAM") *)
+(*       end *)
+(*   | RBstore po chunk addr args d => *)
+(*       match get_ram 0 res with *)
+(*       | Some (ri, r) => *)
+(*           Errors.OK (FUop po Op.Onot (ram_u_en r::nil) (ram_u_en r) *)
+(*                           :: FUop po (Op.Ointconst (Int.repr 1)) nil (ram_wr_en r) *)
+(*                           :: FUop po Op.Omove (d::nil) (ram_d_in r) *)
+(*                           :: FUop po (Op.Olea addr) args (ram_addr r) *)
+(*                           :: FUop po (Op.Oshruimm (Int.repr 2)) ((ram_addr r)::nil) (ram_addr r) *)
+(*                           :: instr_list, d_tree) *)
+(*       | _ => Errors.Error (Errors.msg "Could not find RAM") *)
+(*       end *)
+(*   | RBsetpred op c args p => Errors.OK (FUsetpred op c args p :: instr_list, d_tree) *)
+(*   | RBexit po cf => Errors.Error (Errors.msg "Wrong.") *)
+(*   end. *)
+
+(* Definition transl_cf_instr (i: Gible.cf_instr): RTLParFU.cf_instr := *)
+(*   match i with *)
+(*   | RBcall sig r args d n => FUcall sig r args d n *)
+(*   | RBtailcall sig r args => FUtailcall sig r args *)
+(*   | RBbuiltin ef args r n => FUbuiltin ef args r n *)
+(*   | RBcond c args n1 n2 => FUcond c args n1 n2 *)
+(*   | RBjumptable r ns => FUjumptable r ns *)
+(*   | RBreturn r => FUreturn r *)
+(*   | RBgoto n => FUgoto n *)
+(*   end. *)
+
+(* Definition list_split {A:Type} (l: list (Z * A)) : (list (Z * A)) * (list (Z * A)) := *)
+(*   (filter (fun x => Z.eqb 0 (fst x)) l, *)
+(*     map (fun x => (Z.pred (fst x), snd x)) (filter (fun x => negb (Z.eqb 0 (fst x))) l)). *)
+
+(* Fixpoint map_error {A B : Type} (f : A -> res B) (l : list A) {struct l} : res (list B) := *)
+(*   match l with *)
+(*   | nil => OK nil *)
+(*   | x::xs => *)
+(*     do y <- f x ; *)
+(*     do ys <- map_error f xs ; *)
+(*     OK (y::ys) *)
+(*   end. *)
+
+(* Definition transl_op_chain_block (res: resources) (cycle: positive) (instrs: list Gible.instr) *)
+(*            (state: Errors.res (list (list instr) * PTree.t (list instr))) *)
+(*   : Errors.res (list (list instr) * PTree.t (list instr)) := *)
+(*   do (li, tr) <- state; *)
+(*   do (li', tr') <- fold_right (transl_instr res cycle) (OK (nil, tr)) instrs; *)
+(*   OK (li' :: li, tr'). *)
+
+(* (*Compute transl_op_chain_block initial_resources 10%nat (RBop None (Op.Ointconst (Int.repr 1)) nil 1%positive::RBnop::RBnop::RBnop::nil) (OK (nil, PTree.empty _)).*) *)
+
+(* Definition transl_par_block (res: resources) (cycle: positive) (instrs: list (list Gible.instr)) *)
+(*            (state: Errors.res (list (list (list instr)) * PTree.t (list instr))) *)
+(*   : Errors.res (list (list (list instr)) * PTree.t (list instr)) := *)
+(*   do (li, tr) <- state; *)
+(*   do (li', tr') <- fold_right (transl_op_chain_block res cycle) (OK (nil, tr)) instrs; *)
+(*   OK (li' :: li, tr'). *)
+
+(* (*Compute transl_par_block initial_resources 10%nat ((RBop None (Op.Ointconst (Int.repr 1)) nil 1%positive::RBnop::nil)::(RBop None (Op.Ointconst (Int.repr 2)) nil 2%positive::RBnop::nil)::nil) (OK (((FUnop::nil)::nil)::nil, PTree.empty _)).*) *)
+
+(* Definition transl_seq_block (res: resources) (b: list (list Gible.instr)) *)
+(*            (a: Errors.res (list (list (list instr)) * PTree.t (list instr) * positive)) := *)
+(*   do (litr, n) <- a; *)
+(*   let (li, tr) := litr in *)
+(*   do (li', tr') <- transl_par_block res n b (OK (li, tr)); *)
+(*   OK (li', tr', (n+1)%positive). *)
+
+(* Definition insert_extra (pt: PTree.t (list instr)) (curr: list (list instr)) *)
+(*          (cycle_bb: (positive * list (list (list instr)))) := *)
+(*   let (cycle, bb) := cycle_bb in *)
+(*   match pt ! cycle with *)
+(*   | Some instrs => ((cycle + 1)%positive, (curr ++ (map (fun x => x :: nil) instrs)) :: bb) *)
+(*   | None => ((cycle + 1)%positive, curr :: bb) *)
+(*   end. *)
+
+(* Definition transl_bb (res: resources) (bb: ParBB.t): Errors.res RTLParFU.bblock_body := *)
+(*   do (litr, n) <- fold_right (transl_seq_block res) (OK (nil, PTree.empty _, 1%positive)) bb; *)
+(*   let (li, tr) := litr in *)
+(*   OK (snd (fold_right (insert_extra tr) (1%positive, nil) li)). *)
+
+(* (*Definition transl_bblock (res: resources) (bb: ParBB.t): Errors.res ParBB.t := *)
+(*   transl_bb res bb. *)
+
+(* Definition error_map_ptree {A B: Type} (f: positive -> A -> res B) (pt: PTree.t A) := *)
+(*   do ptl' <- map_error (fun x => do x' <- uncurry f x; OK (fst x, x')) (PTree.elements pt); *)
+(*   OK (PTree_Properties.of_list ptl'). *)
+
+(* Definition transl_code (fu: resources) (c: RTLPar.code): res code := *)
+(*    error_map_ptree (fun _ => transl_bblock fu) c. *)
+
+(* Definition transl_function (f: RTLPar.function): Errors.res RTLParFU.function := *)
+(*   let max := RTLPar.max_reg_function f in *)
+(*   let fu := set_res (Ram (mk_ram *)
+(*                             (Z.to_nat (RTLBlockInstr.fn_stacksize f)) *)
+(*                             (max+1)%positive *)
+(*                             (max+3)%positive *)
+(*                             (max+7)%positive *)
+(*                             (max+2)%positive *)
+(*                             (max+6)%positive *)
+(*                             (max+4)%positive *)
+(*                             (max+5)%positive *)
+(*                     )) initial_resources in *)
+(*   do c' <- transl_code fu (RTLBlockInstr.fn_code f); *)
+(*   Errors.OK (mkfunction (RTLBlockInstr.fn_sig f) *)
+(*                         (RTLBlockInstr.fn_params f) *)
+(*                         (RTLBlockInstr.fn_stacksize f) *)
+(*                         c' *)
+(*                         fu *)
+(*                         (RTLBlockInstr.fn_entrypoint f)). *)
+
+(* Definition transl_fundef p := *)
+(*   transf_partial_fundef transl_function p. *)
+
+(* Definition transl_program (p : RTLPar.program) : Errors.res RTLParFU.program := *)
+(*   transform_partial_program transl_fundef p. *)
+(* *) *)