Fix HTLgenspec.

2 files changed, 467 insertions, 476 deletions

diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v
index 995977c..09af28a 100644
--- a/src/translation/HTLgen.v
+++ b/src/translation/HTLgen.v
@@ -414,21 +414,19 @@ Definition tbl_to_case_expr (st : reg) (ns : list node) : list (expr * stmnt) :=
                   end)
            (enumerate 0 ns).
 
-Definition add_single_cycle_load (n n' : node) (stack : reg) (addr : expr) (dst : reg) : mon unit :=
+Definition create_single_cycle_load (stack : reg) (addr : expr) (dst : reg) : stmnt :=
   let l0   := Vnonblock (Vvarb0 dst) (Vvari stack addr) in
   let l1   := Vnonblock (Vvarb1 dst) (Vvari stack $ Vbinop Vadd addr (Vlit $ ZToValue 1)) in
   let l2   := Vnonblock (Vvarb2 dst) (Vvari stack $ Vbinop Vadd addr (Vlit $ ZToValue 2)) in
-  let l3   := Vnonblock (Vvarb3 dst) (Vvari stack $ Vbinop Vadd addr (Vlit $ ZToValue 2)) in
-  let instr := Vseq l0 $ Vseq l1 $ Vseq l2 $ l3
-  in add_instr n n' instr.
+  let l3   := Vnonblock (Vvarb3 dst) (Vvari stack $ Vbinop Vadd addr (Vlit $ ZToValue 2))
+  in Vseq l0 $ Vseq l1 $ Vseq l2 $ l3.
 
-Definition add_single_cycle_store (n n' : node) (stack : reg) (addr : expr) (src : reg) : mon unit :=
+Definition create_single_cycle_store (stack : reg) (addr : expr) (src : reg) : stmnt :=
   let l0   := Vnonblock (Vvari stack addr) (Vvarb0 src) in
   let l1   := Vnonblock (Vvari stack $ Vbinop Vadd addr (Vlit $ ZToValue 1)) (Vvarb1 src) in
   let l2   := Vnonblock (Vvari stack $ Vbinop Vadd addr (Vlit $ ZToValue 2)) (Vvarb2 src) in
-  let l3   := Vnonblock (Vvari stack $ Vbinop Vadd addr (Vlit $ ZToValue 2)) (Vvarb3 src) in
-  let instr := Vseq l0 $ Vseq l1 $ Vseq l2 $ l3
-  in add_instr n n' instr.
+  let l3   := Vnonblock (Vvari stack $ Vbinop Vadd addr (Vlit $ ZToValue 2)) (Vvarb3 src)
+  in Vseq l0 $ Vseq l1 $ Vseq l2 $ l3.
 
 Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon unit :=
   match ni with
@@ -442,10 +440,10 @@ Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon uni
     | Iload mem addr args dst n' =>
       do addr' <- translate_eff_addressing addr args;
       do _ <- declare_reg None dst 32;
-      add_single_cycle_load n n' stack addr' dst
+      add_instr n n' $ create_single_cycle_load stack addr' dst
     | Istore mem addr args src n' =>
       do addr' <- translate_eff_addressing addr args;
-      add_single_cycle_store n n' stack addr' src
+      add_instr n n' $ create_single_cycle_store stack addr' src
     | Icall _ _ _ _ _ => error (Errors.msg "Calls are not implemented.")
     | Itailcall _ _ _ => error (Errors.msg "Tailcalls are not implemented.")
     | Ibuiltin _ _ _ _ => error (Errors.msg "Builtin functions not implemented.")
diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v
index 4662cf4..bbcde14 100644
--- a/src/translation/HTLgenspec.v
+++ b/src/translation/HTLgenspec.v
@@ -134,476 +134,469 @@ Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> stmnt -> stmnt -
       tr_instr fin rtrn st stk (RTL.Ireturn (Some r))
                (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vvar r))) Vskip
 | tr_instr_Iload :
-    forall mem addr args s s' i c dst n,
-      translate_arr_access mem addr args stk s = OK c s' i ->
-      tr_instr fin rtrn st stk (RTL.Iload mem addr args dst n) (nonblock dst c) (state_goto st n)
+    forall mem addr args s s' i e dst n,
+      translate_eff_addressing addr args s = OK e s' i ->
+      tr_instr fin rtrn st stk (RTL.Iload mem addr args dst n)
+                               (create_single_cycle_load stk e dst) (state_goto st n)
 | tr_instr_Istore :
-    forall mem addr args s s' i c src n,
-      translate_arr_access mem addr args stk s = OK c s' i ->
-      tr_instr fin rtrn st stk (RTL.Istore mem addr args src n) (Vnonblock c (Vvar src))
-               (state_goto st n)
+    forall mem addr args s s' i e src n,
+      translate_eff_addressing addr args s = OK e s' i ->
+      tr_instr fin rtrn st stk (RTL.Istore mem addr args src n)
+                               (create_single_cycle_store stk e src) (state_goto st n)
 | tr_instr_Ijumptable :
     forall cexpr tbl r,
     cexpr = tbl_to_case_expr st tbl ->
     tr_instr fin rtrn st stk (RTL.Ijumptable r tbl) (Vskip) (Vcase (Vvar r) cexpr (Some Vskip)).
 Hint Constructors tr_instr : htlspec.
 
-(* Inductive tr_code (c : RTL.code) (pc : RTL.node) (i : RTL.instruction) (stmnts trans : PTree.t stmnt) *)
-(*           (fin rtrn st stk : reg) : Prop := *)
-(*   tr_code_intro : *)
-(*     forall s t, *)
-(*       c!pc = Some i -> *)
-(*       stmnts!pc = Some s -> *)
-(*       trans!pc = Some t -> *)
-(*       tr_instr fin rtrn st stk i s t -> *)
-(*       tr_code c pc i stmnts trans fin rtrn st stk. *)
-(* Hint Constructors tr_code : htlspec. *)
-
-(* Inductive tr_module (f : RTL.function) : module -> Prop := *)
-(*   tr_module_intro : *)
-(*     forall data control fin rtrn st stk stk_len m start rst clk scldecls arrdecls wf, *)
-(*       m = (mkmodule f.(RTL.fn_params) *)
-(*                         data *)
-(*                         control *)
-(*                         f.(RTL.fn_entrypoint) *)
-(*                         st stk stk_len fin rtrn start rst clk scldecls arrdecls wf) -> *)
-(*       (forall pc i, Maps.PTree.get pc f.(RTL.fn_code) = Some i -> *)
-(*                tr_code f.(RTL.fn_code) pc i data control fin rtrn st stk) -> *)
-(*       stk_len = Z.to_nat (f.(RTL.fn_stacksize) / 4) -> *)
-(*       Z.modulo (f.(RTL.fn_stacksize)) 4 = 0 -> *)
-(*       0 <= f.(RTL.fn_stacksize) < Integers.Ptrofs.modulus -> *)
-(*       st = ((RTL.max_reg_function f) + 1)%positive -> *)
-(*       fin = ((RTL.max_reg_function f) + 2)%positive -> *)
-(*       rtrn = ((RTL.max_reg_function f) + 3)%positive -> *)
-(*       stk = ((RTL.max_reg_function f) + 4)%positive -> *)
-(*       start = ((RTL.max_reg_function f) + 5)%positive -> *)
-(*       rst = ((RTL.max_reg_function f) + 6)%positive -> *)
-(*       clk = ((RTL.max_reg_function f) + 7)%positive -> *)
-(*       tr_module f m. *)
-(* Hint Constructors tr_module : htlspec. *)
-
-(* Lemma create_reg_datapath_trans : *)
-(*   forall sz s s' x i iop, *)
-(*     create_reg iop sz s = OK x s' i -> *)
-(*     s.(st_datapath) = s'.(st_datapath). *)
-(* Proof. intros. monadInv H. trivial. Qed. *)
-(* Hint Resolve create_reg_datapath_trans : htlspec. *)
-
-(* Lemma create_reg_controllogic_trans : *)
-(*   forall sz s s' x i iop, *)
-(*     create_reg iop sz s = OK x s' i -> *)
-(*     s.(st_controllogic) = s'.(st_controllogic). *)
-(* Proof. intros. monadInv H. trivial. Qed. *)
-(* Hint Resolve create_reg_controllogic_trans : htlspec. *)
-
-(* Lemma declare_reg_datapath_trans : *)
-(*   forall sz s s' x i iop r, *)
-(*     declare_reg iop r sz s = OK x s' i -> *)
-(*     s.(st_datapath) = s'.(st_datapath). *)
-(* Proof. intros. monadInv H. trivial. Qed. *)
-(* Hint Resolve create_reg_datapath_trans : htlspec. *)
-
-(* Lemma declare_reg_controllogic_trans : *)
-(*   forall sz s s' x i iop r, *)
-(*     declare_reg iop r sz s = OK x s' i -> *)
-(*     s.(st_controllogic) = s'.(st_controllogic). *)
-(* Proof. intros. monadInv H. trivial. Qed. *)
-(* Hint Resolve create_reg_controllogic_trans : htlspec. *)
-
-(* Lemma declare_reg_freshreg_trans : *)
-(*   forall sz s s' x i iop r, *)
-(*     declare_reg iop r sz s = OK x s' i -> *)
-(*     s.(st_freshreg) = s'.(st_freshreg). *)
-(* Proof. inversion 1; auto. Qed. *)
-(* Hint Resolve declare_reg_freshreg_trans : htlspec. *)
-
-(* Lemma create_arr_datapath_trans : *)
-(*   forall sz ln s s' x i iop, *)
-(*     create_arr iop sz ln s = OK x s' i -> *)
-(*     s.(st_datapath) = s'.(st_datapath). *)
-(* Proof. intros. monadInv H. trivial. Qed. *)
-(* Hint Resolve create_arr_datapath_trans : htlspec. *)
-
-(* Lemma create_arr_controllogic_trans : *)
-(*   forall sz ln s s' x i iop, *)
-(*     create_arr iop sz ln s = OK x s' i -> *)
-(*     s.(st_controllogic) = s'.(st_controllogic). *)
-(* Proof. intros. monadInv H. trivial. Qed. *)
-(* Hint Resolve create_arr_controllogic_trans : htlspec. *)
-
-(* Lemma get_refl_x : *)
-(*   forall s s' x i, *)
-(*     get s = OK x s' i -> *)
-(*     s = x. *)
-(* Proof. inversion 1. trivial. Qed. *)
-(* Hint Resolve get_refl_x : htlspec. *)
-
-(* Lemma get_refl_s : *)
-(*   forall s s' x i, *)
-(*     get s = OK x s' i -> *)
-(*     s = s'. *)
-(* Proof. inversion 1. trivial. Qed. *)
-(* Hint Resolve get_refl_s : htlspec. *)
-
-(* Ltac inv_incr := *)
-(*   repeat match goal with *)
-(*   | [ H: create_reg _ _ ?s = OK _ ?s' _ |- _ ] => *)
-(*     let H1 := fresh "H" in *)
-(*     assert (H1 := H); eapply create_reg_datapath_trans in H; *)
-(*     eapply create_reg_controllogic_trans in H1 *)
-(*   | [ H: create_arr _ _ _ ?s = OK _ ?s' _ |- _ ] => *)
-(*     let H1 := fresh "H" in *)
-(*     assert (H1 := H); eapply create_arr_datapath_trans in H; *)
-(*     eapply create_arr_controllogic_trans in H1 *)
-(*   | [ H: get ?s = OK _ _ _ |- _ ] => *)
-(*     let H1 := fresh "H" in *)
-(*     assert (H1 := H); apply get_refl_x in H; apply get_refl_s in H1; *)
-(*     subst *)
-(*   | [ H: st_prop _ _ |- _ ] => unfold st_prop in H; destruct H *)
-(*   | [ H: st_incr _ _ |- _ ] => destruct st_incr *)
-(*   end. *)
-
-(* Lemma collect_controllogic_trans : *)
-(*   forall A f l cs cs' ci, *)
-(*   (forall s s' x i y, f y s = OK x s' i -> s.(st_controllogic) = s'.(st_controllogic)) -> *)
-(*   @HTLMonadExtra.collectlist A f l cs = OK tt cs' ci -> cs.(st_controllogic) = cs'.(st_controllogic). *)
-(* Proof. *)
-(*   induction l; intros; monadInv H0. *)
-(*   - trivial. *)
-(*   - apply H in EQ. rewrite EQ. eauto. *)
-(* Qed. *)
-
-(* Lemma collect_datapath_trans : *)
-(*   forall A f l cs cs' ci, *)
-(*   (forall s s' x i y, f y s = OK x s' i -> s.(st_datapath) = s'.(st_datapath)) -> *)
-(*   @HTLMonadExtra.collectlist A f l cs = OK tt cs' ci -> cs.(st_datapath) = cs'.(st_datapath). *)
-(* Proof. *)
-(*   induction l; intros; monadInv H0. *)
-(*   - trivial. *)
-(*   - apply H in EQ. rewrite EQ. eauto. *)
-(* Qed. *)
-
-(* Lemma collect_freshreg_trans : *)
-(*   forall A f l cs cs' ci, *)
-(*   (forall s s' x i y, f y s = OK x s' i -> s.(st_freshreg) = s'.(st_freshreg)) -> *)
-(*   @HTLMonadExtra.collectlist A f l cs = OK tt cs' ci -> cs.(st_freshreg) = cs'.(st_freshreg). *)
-(* Proof. *)
-(*   induction l; intros; monadInv H0. *)
-(*   - trivial. *)
-(*   - apply H in EQ. rewrite EQ. eauto. *)
-(* Qed. *)
-
-(* Lemma collect_declare_controllogic_trans : *)
-(*   forall io n l s s' i, *)
-(*   HTLMonadExtra.collectlist (fun r : reg => declare_reg io r n) l s = OK tt s' i -> *)
-(*   s.(st_controllogic) = s'.(st_controllogic). *)
-(* Proof. *)
-(*   intros. eapply collect_controllogic_trans; try eassumption. *)
-(*   intros. eapply declare_reg_controllogic_trans. simpl in H0. eassumption. *)
-(* Qed. *)
-
-(* Lemma collect_declare_datapath_trans : *)
-(*   forall io n l s s' i, *)
-(*   HTLMonadExtra.collectlist (fun r : reg => declare_reg io r n) l s = OK tt s' i -> *)
-(*   s.(st_datapath) = s'.(st_datapath). *)
-(* Proof. *)
-(*   intros. eapply collect_datapath_trans; try eassumption. *)
-(*   intros. eapply declare_reg_datapath_trans. simpl in H0. eassumption. *)
-(* Qed. *)
-
-(* Lemma collect_declare_freshreg_trans : *)
-(*   forall io n l s s' i, *)
-(*   HTLMonadExtra.collectlist (fun r : reg => declare_reg io r n) l s = OK tt s' i -> *)
-(*   s.(st_freshreg) = s'.(st_freshreg). *)
-(* Proof. *)
-(*   intros. eapply collect_freshreg_trans; try eassumption. *)
-(*   inversion 1. auto. *)
-(* Qed. *)
-
-(* Ltac unfold_match H := *)
-(*   match type of H with *)
-(*   | context[match ?g with _ => _ end] => destruct g eqn:?; try discriminate *)
-(*   end. *)
-
-(* Lemma translate_eff_addressing_freshreg_trans : *)
-(*   forall op args s r s' i, *)
-(*   translate_eff_addressing op args s = OK r s' i -> *)
-(*   s.(st_freshreg) = s'.(st_freshreg). *)
-(* Proof. *)
-(*   destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto. *)
-(* Qed. *)
-(* Hint Resolve translate_eff_addressing_freshreg_trans : htlspec. *)
-
-(* Lemma translate_comparison_freshreg_trans : *)
-(*   forall op args s r s' i, *)
-(*   translate_comparison op args s = OK r s' i -> *)
-(*   s.(st_freshreg) = s'.(st_freshreg). *)
-(* Proof. *)
-(*   destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto. *)
-(* Qed. *)
-(* Hint Resolve translate_comparison_freshreg_trans : htlspec. *)
-
-(* Lemma translate_comparison_imm_freshreg_trans : *)
-(*   forall op args s r s' i n, *)
-(*   translate_comparison_imm op args n s = OK r s' i -> *)
-(*   s.(st_freshreg) = s'.(st_freshreg). *)
-(* Proof. *)
-(*   destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto. *)
-(* Qed. *)
-(* Hint Resolve translate_comparison_imm_freshreg_trans : htlspec. *)
-
-(* Lemma translate_condition_freshreg_trans : *)
-(*   forall op args s r s' i, *)
-(*   translate_condition op args s = OK r s' i -> *)
-(*   s.(st_freshreg) = s'.(st_freshreg). *)
-(* Proof. *)
-(*   destruct op; intros; simpl in *; repeat (unfold_match H); inv H; eauto with htlspec. *)
-(* Qed. *)
-(* Hint Resolve translate_condition_freshreg_trans : htlspec. *)
-
-(* Lemma translate_instr_freshreg_trans : *)
-(*   forall op args s r s' i, *)
-(*   translate_instr op args s = OK r s' i -> *)
-(*   s.(st_freshreg) = s'.(st_freshreg). *)
-(* Proof. *)
-(*   destruct op; intros; simpl in *; repeat (unfold_match H); inv H; eauto with htlspec. *)
-(*   monadInv H1. eauto with htlspec. *)
-(* Qed. *)
-(* Hint Resolve translate_instr_freshreg_trans : htlspec. *)
-
-(* Lemma translate_arr_access_freshreg_trans : *)
-(*   forall mem addr args st s r s' i, *)
-(*   translate_arr_access mem addr args st s = OK r s' i -> *)
-(*   s.(st_freshreg) = s'.(st_freshreg). *)
-(* Proof. *)
-(*   intros. unfold translate_arr_access in H. repeat (unfold_match H); inv H; eauto with htlspec. *)
-(* Qed. *)
-(* Hint Resolve translate_arr_access_freshreg_trans : htlspec. *)
-
-(* Lemma add_instr_freshreg_trans : *)
-(*   forall n n' st s r s' i, *)
-(*   add_instr n n' st s = OK r s' i -> *)
-(*   s.(st_freshreg) = s'.(st_freshreg). *)
-(* Proof. intros. unfold add_instr in H. repeat (unfold_match H). inv H. auto. Qed. *)
-(* Hint Resolve add_instr_freshreg_trans : htlspec. *)
-
-(* Lemma add_branch_instr_freshreg_trans : *)
-(*   forall n n0 n1 e s r s' i, *)
-(*   add_branch_instr e n n0 n1 s = OK r s' i -> *)
-(*   s.(st_freshreg) = s'.(st_freshreg). *)
-(* Proof. intros. unfold add_branch_instr in H. repeat (unfold_match H). inv H. auto. Qed. *)
-(* Hint Resolve add_branch_instr_freshreg_trans : htlspec. *)
-
-(* Lemma add_node_skip_freshreg_trans : *)
-(*   forall n1 n2 s r s' i, *)
-(*   add_node_skip n1 n2 s = OK r s' i -> *)
-(*   s.(st_freshreg) = s'.(st_freshreg). *)
-(* Proof. intros. unfold add_node_skip in H. repeat (unfold_match H). inv H. auto. Qed. *)
-(* Hint Resolve add_node_skip_freshreg_trans : htlspec. *)
-
-(* Lemma add_instr_skip_freshreg_trans : *)
-(*   forall n1 n2 s r s' i, *)
-(*   add_instr_skip n1 n2 s = OK r s' i -> *)
-(*   s.(st_freshreg) = s'.(st_freshreg). *)
-(* Proof. intros. unfold add_instr_skip in H. repeat (unfold_match H). inv H. auto. Qed. *)
-(* Hint Resolve add_instr_skip_freshreg_trans : htlspec. *)
-
-(* Lemma transf_instr_freshreg_trans : *)
-(*   forall fin ret st instr s v s' i, *)
-(*     transf_instr fin ret st instr s = OK v s' i -> *)
-(*     s.(st_freshreg) = s'.(st_freshreg). *)
-(* Proof. *)
-(*   intros. destruct instr eqn:?. subst. unfold transf_instr in H. *)
-(*   destruct i0; try (monadInv H); try (unfold_match H); eauto with htlspec. *)
-(*   - apply add_instr_freshreg_trans in EQ2. apply translate_instr_freshreg_trans in EQ. *)
-(*     apply declare_reg_freshreg_trans in EQ1. congruence. *)
-(*   - apply add_instr_freshreg_trans in EQ2. apply translate_arr_access_freshreg_trans in EQ. *)
-(*     apply declare_reg_freshreg_trans in EQ1. congruence. *)
-(*   - apply add_instr_freshreg_trans in EQ0. apply translate_arr_access_freshreg_trans in EQ. congruence. *)
-(*   - apply translate_condition_freshreg_trans in EQ. apply add_branch_instr_freshreg_trans in EQ0. *)
-(*     congruence. *)
-(*   - inv EQ. apply add_node_skip_freshreg_trans in EQ0. congruence. *)
-(* Qed. *)
-(* Hint Resolve transf_instr_freshreg_trans : htlspec. *)
-
-(* Lemma collect_trans_instr_freshreg_trans : *)
-(*   forall fin ret st l s s' i, *)
-(*   HTLMonadExtra.collectlist (transf_instr fin ret st) l s = OK tt s' i -> *)
-(*   s.(st_freshreg) = s'.(st_freshreg). *)
-(* Proof. *)
-(*   intros. eapply collect_freshreg_trans; try eassumption. *)
-(*   eauto with htlspec. *)
-(* Qed. *)
-
-(* Ltac rewrite_states := *)
-(*   match goal with *)
-(*   | [ H: ?x ?s = ?x ?s' |- _ ] => *)
-(*     let c1 := fresh "c" in *)
-(*     let c2 := fresh "c" in *)
-(*     remember (?x ?s) as c1; remember (?x ?s') as c2; try subst *)
-(*   end. *)
-
-(* Ltac inv_add_instr' H := *)
-(*   match type of H with *)
-(*   | ?f _ _ _ = OK _ _ _ => unfold f in H *)
-(*   | ?f _ _ _ _ = OK _ _ _ => unfold f in H *)
-(*   | ?f _ _ _ _ _ = OK _ _ _ => unfold f in H *)
-(*   end; repeat unfold_match H; inversion H. *)
-
-(* Ltac inv_add_instr := *)
-(*   lazymatch goal with *)
-(*   | H: context[add_instr_skip _ _ _] |- _ => *)
-(*     inv_add_instr' H *)
-(*   | H: context[add_instr_skip _ _] |- _ => *)
-(*     monadInv H; inv_incr; inv_add_instr *)
-(*   | H: context[add_instr _ _ _ _] |- _ => *)
-(*     inv_add_instr' H *)
-(*   | H: context[add_instr _ _ _] |- _ => *)
-(*     monadInv H; inv_incr; inv_add_instr *)
-(*   | H: context[add_branch_instr _ _ _ _ _] |- _ => *)
-(*     inv_add_instr' H *)
-(*   | H: context[add_branch_instr _ _ _ _] |- _ => *)
-(*     monadInv H; inv_incr; inv_add_instr *)
-(*   | H: context[add_node_skip _ _ _] |- _ => *)
-(*     inv_add_instr' H *)
-(*   | H: context[add_node_skip _ _] |- _ => *)
-(*     monadInv H; inv_incr; inv_add_instr *)
-(*   end. *)
-
-(* Ltac destruct_optional := *)
-(*   match goal with H: option ?r |- _ => destruct H end. *)
-
-(* Lemma iter_expand_instr_spec : *)
-(*   forall l fin rtrn stack s s' i x c, *)
-(*     HTLMonadExtra.collectlist (transf_instr fin rtrn stack) l s = OK x s' i -> *)
-(*     list_norepet (List.map fst l) -> *)
-(*     (forall pc instr, In (pc, instr) l -> c!pc = Some instr) -> *)
-(*     (forall pc instr, In (pc, instr) l -> *)
-(*                       c!pc = Some instr -> *)
-(*                       tr_code c pc instr s'.(st_datapath) s'.(st_controllogic) fin rtrn s'.(st_st) stack). *)
-(* Proof. *)
-(*   induction l; simpl; intros; try contradiction. *)
-(*   destruct a as [pc1 instr1]; simpl in *. inv H0. monadInv H. inv_incr. *)
-(*   destruct (peq pc pc1). *)
-(*   - subst. *)
-(*     destruct instr1 eqn:?; try discriminate; *)
-(*       try destruct_optional; inv_add_instr; econstructor; try assumption. *)
-(*     + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. *)
-(*     + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. *)
-(*     + inversion H2. inversion H9. rewrite H. apply tr_instr_Inop. *)
-(*       eapply in_map with (f := fst) in H9. contradiction. *)
-
-(*     + destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. *)
-(*     + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. *)
-(*     + inversion H2. inversion H14. unfold nonblock. replace (st_st s4) with (st_st s2) by congruence. *)
-(*       econstructor. apply EQ1. eapply in_map with (f := fst) in H14. contradiction. *)
-
-(*     + destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. *)
-(*     + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. *)
-(*     + inversion H2. inversion H14. rewrite <- e2. replace (st_st s2) with (st_st s0) by congruence. *)
-(*       econstructor. apply EQ1. eapply in_map with (f := fst) in H14. contradiction. *)
-
-(*     + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. *)
-(*     + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. *)
-(*     + destruct H2. *)
-(*       * inversion H2. *)
-(*         replace (st_st s2) with (st_st s0) by congruence. *)
-(*         eauto with htlspec. *)
-(*       * apply in_map with (f := fst) in H2. contradiction. *)
-
-(*     + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. *)
-(*     + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. *)
-(*     + destruct H2. *)
-(*       * inversion H2. *)
-(*         replace (st_st s2) with (st_st s0) by congruence. *)
-(*         eauto with htlspec. *)
-(*       * apply in_map with (f := fst) in H2. contradiction. *)
-
-(*     + destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. *)
-(*     + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. *)
-(*     + inversion H2. *)
-(*       * inversion H14. constructor. congruence. *)
-(*       * apply in_map with (f := fst) in H14. contradiction. *)
-
-(*     + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. *)
-(*     + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. *)
-(*     + inversion H2. *)
-(*       * inversion H9. *)
-(*         replace (st_st s2) with (st_st s0) by congruence. *)
-(*         eauto with htlspec. *)
-(*       * apply in_map with (f := fst) in H9. contradiction. *)
-
-(*     + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. *)
-(*     + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. *)
-(*     + inversion H2. *)
-(*       * inversion H9. *)
-(*         replace (st_st s2) with (st_st s0) by congruence. *)
-(*         eauto with htlspec. *)
-(*       * apply in_map with (f := fst) in H9. contradiction. *)
-
-(*   - eapply IHl. apply EQ0. assumption. *)
-(*     destruct H2. inversion H2. subst. contradiction. *)
-(*     intros. specialize H1 with pc0 instr0. destruct H1. tauto. trivial. *)
-(*     destruct H2. inv H2. contradiction. assumption. assumption. *)
-(* Qed. *)
-(* Hint Resolve iter_expand_instr_spec : htlspec. *)
-
-(* Lemma create_arr_inv : forall w x y z a b c d, *)
-(*     create_arr w x y z = OK (a, b) c d -> *)
-(*     y = b /\ a = z.(st_freshreg) /\ c.(st_freshreg) = Pos.succ (z.(st_freshreg)). *)
-(* Proof. *)
-(*   inversion 1; split; auto. *)
-(* Qed. *)
-
-(* Lemma create_reg_inv : forall a b s r s' i, *)
-(*     create_reg a b s = OK r s' i -> *)
-(*     r = s.(st_freshreg) /\ s'.(st_freshreg) = Pos.succ (s.(st_freshreg)). *)
-(* Proof. *)
-(*   inversion 1; auto. *)
-(* Qed. *)
-
-(* Theorem transl_module_correct : *)
-(*   forall f m, *)
-(*     transl_module f = Errors.OK m -> tr_module f m. *)
-(* Proof. *)
-(*   intros until m. *)
-(*   unfold transl_module. *)
-(*   unfold run_mon. *)
-(*   destruct (transf_module f (max_state f)) eqn:?; try discriminate. *)
-(*   intros. inv H. *)
-(*   inversion s; subst. *)
-
-(*   unfold transf_module in *. *)
-(*   unfold stack_correct in *. *)
-(*   destruct (0 <=? RTL.fn_stacksize f) eqn:STACK_BOUND_LOW; *)
-(*     destruct (RTL.fn_stacksize f <? Integers.Ptrofs.modulus) eqn:STACK_BOUND_HIGH; *)
-(*     destruct (RTL.fn_stacksize f mod 4 =? 0) eqn:STACK_ALIGN; *)
-(*     crush; *)
-(*     monadInv Heqr. *)
-
-(*   repeat unfold_match EQ9. monadInv EQ9. *)
-
-(*   (* TODO: We should be able to fold this into the automation. *) *)
-(*   pose proof (create_arr_inv _ _ _ _ _ _ _ _ EQ0) as STK_LEN. inv STK_LEN. inv H5. *)
-(*   pose proof (create_reg_inv _ _ _ _ _ _ EQ) as FIN_VAL. inv FIN_VAL. *)
-(*   pose proof (create_reg_inv _ _ _ _ _ _ EQ1) as RET_VAL. inv RET_VAL. *)
-(*   destruct x3. destruct x4. *)
-(*   pose proof (collect_trans_instr_freshreg_trans _ _ _ _ _ _ _ EQ2) as TR_INSTR. *)
-(*   pose proof (collect_declare_freshreg_trans _ _ _ _ _ _ EQ3) as TR_DEC. *)
-(*   pose proof (create_reg_inv _ _ _ _ _ _ EQ4) as START_VAL. inv START_VAL. *)
-(*   pose proof (create_reg_inv _ _ _ _ _ _ EQ5) as RESET_VAL. inv RESET_VAL. *)
-(*   pose proof (create_reg_inv _ _ _ _ _ _ EQ6) as CLK_VAL. inv CLK_VAL. *)
-(*   rewrite H9 in *. rewrite H8 in *. replace (st_freshreg s4) with (st_freshreg s2) in * by congruence. *)
-(*   rewrite H6 in *. rewrite H7 in *. rewrite H5 in *. simpl in *. *)
-(*   inv_incr. *)
-(*   econstructor; simpl; auto; try lia. *)
-(*   intros. *)
-(*   assert (EQ3D := EQ3). *)
-(*   apply collect_declare_datapath_trans in EQ3. *)
-(*   apply collect_declare_controllogic_trans in EQ3D. *)
-(*   replace (st_controllogic s10) with (st_controllogic s3) by congruence. *)
-(*   replace (st_datapath s10) with (st_datapath s3) by congruence. *)
-(*   replace (st_st s10) with (st_st s3) by congruence. *)
-(*   eapply iter_expand_instr_spec; eauto with htlspec. *)
-(*   apply PTree.elements_complete. *)
-(* Qed. *)
+Inductive tr_code (c : RTL.code) (pc : RTL.node) (i : RTL.instruction) (stmnts trans : PTree.t stmnt)
+          (fin rtrn st stk : reg) : Prop :=
+  tr_code_intro :
+    forall s t,
+      c!pc = Some i ->
+      stmnts!pc = Some s ->
+      trans!pc = Some t ->
+      tr_instr fin rtrn st stk i s t ->
+      tr_code c pc i stmnts trans fin rtrn st stk.
+Hint Constructors tr_code : htlspec.
+
+Inductive tr_module (f : RTL.function) : module -> Prop :=
+  tr_module_intro :
+    forall data control fin rtrn st stk stk_len m start rst clk scldecls arrdecls wf,
+      m = (mkmodule f.(RTL.fn_params)
+                        data
+                        control
+                        f.(RTL.fn_entrypoint)
+                        st stk stk_len fin rtrn start rst clk scldecls arrdecls wf) ->
+      (forall pc i, Maps.PTree.get pc f.(RTL.fn_code) = Some i ->
+               tr_code f.(RTL.fn_code) pc i data control fin rtrn st stk) ->
+      stk_len = Z.to_nat f.(RTL.fn_stacksize) ->
+      Z.modulo (f.(RTL.fn_stacksize)) 4 = 0 ->
+      0 <= f.(RTL.fn_stacksize) < Integers.Ptrofs.modulus ->
+      st = ((RTL.max_reg_function f) + 1)%positive ->
+      fin = ((RTL.max_reg_function f) + 2)%positive ->
+      rtrn = ((RTL.max_reg_function f) + 3)%positive ->
+      stk = ((RTL.max_reg_function f) + 4)%positive ->
+      start = ((RTL.max_reg_function f) + 5)%positive ->
+      rst = ((RTL.max_reg_function f) + 6)%positive ->
+      clk = ((RTL.max_reg_function f) + 7)%positive ->
+      tr_module f m.
+Hint Constructors tr_module : htlspec.
+
+Lemma create_reg_datapath_trans :
+  forall sz s s' x i iop,
+    create_reg iop sz s = OK x s' i ->
+    s.(st_datapath) = s'.(st_datapath).
+Proof. intros. monadInv H. trivial. Qed.
+Hint Resolve create_reg_datapath_trans : htlspec.
+
+Lemma create_reg_controllogic_trans :
+  forall sz s s' x i iop,
+    create_reg iop sz s = OK x s' i ->
+    s.(st_controllogic) = s'.(st_controllogic).
+Proof. intros. monadInv H. trivial. Qed.
+Hint Resolve create_reg_controllogic_trans : htlspec.
+
+Lemma declare_reg_datapath_trans :
+  forall sz s s' x i iop r,
+    declare_reg iop r sz s = OK x s' i ->
+    s.(st_datapath) = s'.(st_datapath).
+Proof. intros. monadInv H. trivial. Qed.
+Hint Resolve create_reg_datapath_trans : htlspec.
+
+Lemma declare_reg_controllogic_trans :
+  forall sz s s' x i iop r,
+    declare_reg iop r sz s = OK x s' i ->
+    s.(st_controllogic) = s'.(st_controllogic).
+Proof. intros. monadInv H. trivial. Qed.
+Hint Resolve create_reg_controllogic_trans : htlspec.
+
+Lemma declare_reg_freshreg_trans :
+  forall sz s s' x i iop r,
+    declare_reg iop r sz s = OK x s' i ->
+    s.(st_freshreg) = s'.(st_freshreg).
+Proof. inversion 1; auto. Qed.
+Hint Resolve declare_reg_freshreg_trans : htlspec.
+
+Lemma create_arr_datapath_trans :
+  forall sz ln s s' x i iop,
+    create_arr iop sz ln s = OK x s' i ->
+    s.(st_datapath) = s'.(st_datapath).
+Proof. intros. monadInv H. trivial. Qed.
+Hint Resolve create_arr_datapath_trans : htlspec.
+
+Lemma create_arr_controllogic_trans :
+  forall sz ln s s' x i iop,
+    create_arr iop sz ln s = OK x s' i ->
+    s.(st_controllogic) = s'.(st_controllogic).
+Proof. intros. monadInv H. trivial. Qed.
+Hint Resolve create_arr_controllogic_trans : htlspec.
+
+Lemma get_refl_x :
+  forall s s' x i,
+    get s = OK x s' i ->
+    s = x.
+Proof. inversion 1. trivial. Qed.
+Hint Resolve get_refl_x : htlspec.
+
+Lemma get_refl_s :
+  forall s s' x i,
+    get s = OK x s' i ->
+    s = s'.
+Proof. inversion 1. trivial. Qed.
+Hint Resolve get_refl_s : htlspec.
+
+Ltac inv_incr :=
+  repeat match goal with
+  | [ H: create_reg _ _ ?s = OK _ ?s' _ |- _ ] =>
+    let H1 := fresh "H" in
+    assert (H1 := H); eapply create_reg_datapath_trans in H;
+    eapply create_reg_controllogic_trans in H1
+  | [ H: create_arr _ _ _ ?s = OK _ ?s' _ |- _ ] =>
+    let H1 := fresh "H" in
+    assert (H1 := H); eapply create_arr_datapath_trans in H;
+    eapply create_arr_controllogic_trans in H1
+  | [ H: get ?s = OK _ _ _ |- _ ] =>
+    let H1 := fresh "H" in
+    assert (H1 := H); apply get_refl_x in H; apply get_refl_s in H1;
+    subst
+  | [ H: st_prop _ _ |- _ ] => unfold st_prop in H; destruct H
+  | [ H: st_incr _ _ |- _ ] => destruct st_incr
+  end.
+
+Lemma collect_controllogic_trans :
+  forall A f l cs cs' ci,
+  (forall s s' x i y, f y s = OK x s' i -> s.(st_controllogic) = s'.(st_controllogic)) ->
+  @HTLMonadExtra.collectlist A f l cs = OK tt cs' ci -> cs.(st_controllogic) = cs'.(st_controllogic).
+Proof.
+  induction l; intros; monadInv H0.
+  - trivial.
+  - apply H in EQ. rewrite EQ. eauto.
+Qed.
+
+Lemma collect_datapath_trans :
+  forall A f l cs cs' ci,
+  (forall s s' x i y, f y s = OK x s' i -> s.(st_datapath) = s'.(st_datapath)) ->
+  @HTLMonadExtra.collectlist A f l cs = OK tt cs' ci -> cs.(st_datapath) = cs'.(st_datapath).
+Proof.
+  induction l; intros; monadInv H0.
+  - trivial.
+  - apply H in EQ. rewrite EQ. eauto.
+Qed.
+
+Lemma collect_freshreg_trans :
+  forall A f l cs cs' ci,
+  (forall s s' x i y, f y s = OK x s' i -> s.(st_freshreg) = s'.(st_freshreg)) ->
+  @HTLMonadExtra.collectlist A f l cs = OK tt cs' ci -> cs.(st_freshreg) = cs'.(st_freshreg).
+Proof.
+  induction l; intros; monadInv H0.
+  - trivial.
+  - apply H in EQ. rewrite EQ. eauto.
+Qed.
+
+Lemma collect_declare_controllogic_trans :
+  forall io n l s s' i,
+  HTLMonadExtra.collectlist (fun r : reg => declare_reg io r n) l s = OK tt s' i ->
+  s.(st_controllogic) = s'.(st_controllogic).
+Proof.
+  intros. eapply collect_controllogic_trans; try eassumption.
+  intros. eapply declare_reg_controllogic_trans. simpl in H0. eassumption.
+Qed.
+
+Lemma collect_declare_datapath_trans :
+  forall io n l s s' i,
+  HTLMonadExtra.collectlist (fun r : reg => declare_reg io r n) l s = OK tt s' i ->
+  s.(st_datapath) = s'.(st_datapath).
+Proof.
+  intros. eapply collect_datapath_trans; try eassumption.
+  intros. eapply declare_reg_datapath_trans. simpl in H0. eassumption.
+Qed.
+
+Lemma collect_declare_freshreg_trans :
+  forall io n l s s' i,
+  HTLMonadExtra.collectlist (fun r : reg => declare_reg io r n) l s = OK tt s' i ->
+  s.(st_freshreg) = s'.(st_freshreg).
+Proof.
+  intros. eapply collect_freshreg_trans; try eassumption.
+  inversion 1. auto.
+Qed.
+
+Ltac unfold_match H :=
+  match type of H with
+  | context[match ?g with _ => _ end] => destruct g eqn:?; try discriminate
+  end.
+
+Lemma translate_eff_addressing_freshreg_trans :
+  forall op args s r s' i,
+  translate_eff_addressing op args s = OK r s' i ->
+  s.(st_freshreg) = s'.(st_freshreg).
+Proof.
+  destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto.
+Qed.
+Hint Resolve translate_eff_addressing_freshreg_trans : htlspec.
+
+Lemma translate_comparison_freshreg_trans :
+  forall op args s r s' i,
+  translate_comparison op args s = OK r s' i ->
+  s.(st_freshreg) = s'.(st_freshreg).
+Proof.
+  destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto.
+Qed.
+Hint Resolve translate_comparison_freshreg_trans : htlspec.
+
+Lemma translate_comparison_imm_freshreg_trans :
+  forall op args s r s' i n,
+  translate_comparison_imm op args n s = OK r s' i ->
+  s.(st_freshreg) = s'.(st_freshreg).
+Proof.
+  destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto.
+Qed.
+Hint Resolve translate_comparison_imm_freshreg_trans : htlspec.
+
+Lemma translate_condition_freshreg_trans :
+  forall op args s r s' i,
+  translate_condition op args s = OK r s' i ->
+  s.(st_freshreg) = s'.(st_freshreg).
+Proof.
+  destruct op; intros; simpl in *; repeat (unfold_match H); inv H; eauto with htlspec.
+Qed.
+Hint Resolve translate_condition_freshreg_trans : htlspec.
+
+Lemma translate_instr_freshreg_trans :
+  forall op args s r s' i,
+  translate_instr op args s = OK r s' i ->
+  s.(st_freshreg) = s'.(st_freshreg).
+Proof.
+  destruct op; intros; simpl in *; repeat (unfold_match H); inv H; eauto with htlspec.
+  monadInv H1. eauto with htlspec.
+Qed.
+Hint Resolve translate_instr_freshreg_trans : htlspec.
+
+Lemma add_instr_freshreg_trans :
+  forall n n' st s r s' i,
+  add_instr n n' st s = OK r s' i ->
+  s.(st_freshreg) = s'.(st_freshreg).
+Proof. intros. unfold add_instr in H. repeat (unfold_match H). inv H. auto. Qed.
+Hint Resolve add_instr_freshreg_trans : htlspec.
+
+Lemma add_branch_instr_freshreg_trans :
+  forall n n0 n1 e s r s' i,
+  add_branch_instr e n n0 n1 s = OK r s' i ->
+  s.(st_freshreg) = s'.(st_freshreg).
+Proof. intros. unfold add_branch_instr in H. repeat (unfold_match H). inv H. auto. Qed.
+Hint Resolve add_branch_instr_freshreg_trans : htlspec.
+
+Lemma add_node_skip_freshreg_trans :
+  forall n1 n2 s r s' i,
+  add_node_skip n1 n2 s = OK r s' i ->
+  s.(st_freshreg) = s'.(st_freshreg).
+Proof. intros. unfold add_node_skip in H. repeat (unfold_match H). inv H. auto. Qed.
+Hint Resolve add_node_skip_freshreg_trans : htlspec.
+
+Lemma add_instr_skip_freshreg_trans :
+  forall n1 n2 s r s' i,
+  add_instr_skip n1 n2 s = OK r s' i ->
+  s.(st_freshreg) = s'.(st_freshreg).
+Proof. intros. unfold add_instr_skip in H. repeat (unfold_match H). inv H. auto. Qed.
+Hint Resolve add_instr_skip_freshreg_trans : htlspec.
+
+Lemma transf_instr_freshreg_trans :
+  forall fin ret st instr s v s' i,
+    transf_instr fin ret st instr s = OK v s' i ->
+    s.(st_freshreg) = s'.(st_freshreg).
+Proof.
+  intros. destruct instr eqn:?. subst. unfold transf_instr in H.
+  destruct i0; try (monadInv H); try (unfold_match H); eauto with htlspec.
+  - apply add_instr_freshreg_trans in EQ2. apply translate_instr_freshreg_trans in EQ.
+    apply declare_reg_freshreg_trans in EQ1. congruence.
+  - apply add_instr_freshreg_trans in EQ2. apply translate_eff_addressing_freshreg_trans in EQ.
+    apply declare_reg_freshreg_trans in EQ1. congruence.
+  - apply add_instr_freshreg_trans in EQ0. apply translate_eff_addressing_freshreg_trans in EQ.
+    congruence.
+  - apply translate_condition_freshreg_trans in EQ. apply add_branch_instr_freshreg_trans in EQ0.
+    congruence.
+  - inv EQ. apply add_node_skip_freshreg_trans in EQ0. congruence.
+Qed.
+Hint Resolve transf_instr_freshreg_trans : htlspec.
+
+Lemma collect_trans_instr_freshreg_trans :
+  forall fin ret st l s s' i,
+  HTLMonadExtra.collectlist (transf_instr fin ret st) l s = OK tt s' i ->
+  s.(st_freshreg) = s'.(st_freshreg).
+Proof.
+  intros. eapply collect_freshreg_trans; try eassumption.
+  eauto with htlspec.
+Qed.
+
+Ltac rewrite_states :=
+  match goal with
+  | [ H: ?x ?s = ?x ?s' |- _ ] =>
+    let c1 := fresh "c" in
+    let c2 := fresh "c" in
+    remember (?x ?s) as c1; remember (?x ?s') as c2; try subst
+  end.
+
+Ltac inv_add_instr' H :=
+  match type of H with
+  | ?f _ _ _ = OK _ _ _ => unfold f in H
+  | ?f _ _ _ _ = OK _ _ _ => unfold f in H
+  | ?f _ _ _ _ _ = OK _ _ _ => unfold f in H
+  end; repeat unfold_match H; inversion H.
+
+Ltac inv_add_instr :=
+  lazymatch goal with
+  | H: context[add_instr_skip _ _ _] |- _ =>
+    inv_add_instr' H
+  | H: context[add_instr_skip _ _] |- _ =>
+    monadInv H; inv_incr; inv_add_instr
+  | H: context[add_instr _ _ _ _] |- _ =>
+    inv_add_instr' H
+  | H: context[add_instr _ _ _] |- _ =>
+    monadInv H; inv_incr; inv_add_instr
+  | H: context[add_branch_instr _ _ _ _ _] |- _ =>
+    inv_add_instr' H
+  | H: context[add_branch_instr _ _ _ _] |- _ =>
+    monadInv H; inv_incr; inv_add_instr
+  | H: context[add_node_skip _ _ _] |- _ =>
+    inv_add_instr' H
+  | H: context[add_node_skip _ _] |- _ =>
+    monadInv H; inv_incr; inv_add_instr
+  end.
+
+Ltac destruct_optional :=
+  match goal with H: option ?r |- _ => destruct H end.
+
+Lemma iter_expand_instr_spec :
+  forall l fin rtrn stack s s' i x c,
+    HTLMonadExtra.collectlist (transf_instr fin rtrn stack) l s = OK x s' i ->
+    list_norepet (List.map fst l) ->
+    (forall pc instr, In (pc, instr) l -> c!pc = Some instr) ->
+    (forall pc instr, In (pc, instr) l ->
+                      c!pc = Some instr ->
+                      tr_code c pc instr s'.(st_datapath) s'.(st_controllogic) fin rtrn s'.(st_st) stack).
+Proof.
+  induction l; simpl; intros; try contradiction.
+  destruct a as [pc1 instr1]; simpl in *. inv H0. monadInv H. inv_incr.
+  destruct (peq pc pc1).
+  - subst.
+    destruct instr1 eqn:?; try discriminate;
+      try destruct_optional; inv_add_instr; econstructor; try assumption.
+    + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence.
+    + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence.
+    + inversion H2. inversion H9. rewrite H. apply tr_instr_Inop.
+      eapply in_map with (f := fst) in H9. contradiction.
+
+    + destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence.
+    + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence.
+    + inversion H2. inversion H14. unfold nonblock. replace (st_st s4) with (st_st s2) by congruence.
+      econstructor. apply EQ1. eapply in_map with (f := fst) in H14. contradiction.
+
+    + destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence.
+    + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence.
+    + inversion H2. inversion H14. rewrite <- e2. replace (st_st s2) with (st_st s0) by congruence.
+      econstructor. apply EQ1. eapply in_map with (f := fst) in H14. contradiction.
+
+    + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence.
+    + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence.
+    + destruct H2.
+      * inversion H2.
+        replace (st_st s2) with (st_st s0) by congruence.
+        eauto with htlspec.
+      * apply in_map with (f := fst) in H2. contradiction.
+
+    + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence.
+    + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence.
+    + destruct H2.
+      * inversion H2.
+        replace (st_st s2) with (st_st s0) by congruence.
+        eauto with htlspec.
+      * apply in_map with (f := fst) in H2. contradiction.
+
+    + destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence.
+    + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence.
+    + inversion H2.
+      * inversion H14. constructor. congruence.
+      * apply in_map with (f := fst) in H14. contradiction.
+
+    + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence.
+    + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence.
+    + inversion H2.
+      * inversion H9.
+        replace (st_st s2) with (st_st s0) by congruence.
+        eauto with htlspec.
+      * apply in_map with (f := fst) in H9. contradiction.
+
+    + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence.
+    + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence.
+    + inversion H2.
+      * inversion H9.
+        replace (st_st s2) with (st_st s0) by congruence.
+        eauto with htlspec.
+      * apply in_map with (f := fst) in H9. contradiction.
+
+  - eapply IHl. apply EQ0. assumption.
+    destruct H2. inversion H2. subst. contradiction.
+    intros. specialize H1 with pc0 instr0. destruct H1. tauto. trivial.
+    destruct H2. inv H2. contradiction. assumption. assumption.
+Qed.
+Hint Resolve iter_expand_instr_spec : htlspec.
+
+Lemma create_arr_inv : forall w x y z a b c d,
+    create_arr w x y z = OK (a, b) c d ->
+    y = b /\ a = z.(st_freshreg) /\ c.(st_freshreg) = Pos.succ (z.(st_freshreg)).
+Proof.
+  inversion 1; split; auto.
+Qed.
+
+Lemma create_reg_inv : forall a b s r s' i,
+    create_reg a b s = OK r s' i ->
+    r = s.(st_freshreg) /\ s'.(st_freshreg) = Pos.succ (s.(st_freshreg)).
+Proof.
+  inversion 1; auto.
+Qed.
+
+Theorem transl_module_correct :
+  forall f m,
+    transl_module f = Errors.OK m -> tr_module f m.
+Proof.
+  intros until m.
+  unfold transl_module.
+  unfold run_mon.
+  destruct (transf_module f (max_state f)) eqn:?; try discriminate.
+  intros. inv H.
+  inversion s; subst.
+
+  unfold transf_module in *.
+  unfold stack_correct in *.
+  destruct (0 <=? RTL.fn_stacksize f) eqn:STACK_BOUND_LOW;
+    destruct (RTL.fn_stacksize f <? Integers.Ptrofs.modulus) eqn:STACK_BOUND_HIGH;
+    destruct (RTL.fn_stacksize f mod 4 =? 0) eqn:STACK_ALIGN;
+    crush;
+    monadInv Heqr.
+
+  repeat unfold_match EQ9. monadInv EQ9.
+
+  (* TODO: We should be able to fold this into the automation. *)
+  pose proof (create_arr_inv _ _ _ _ _ _ _ _ EQ0) as STK_LEN. inv STK_LEN. inv H5.
+  pose proof (create_reg_inv _ _ _ _ _ _ EQ) as FIN_VAL. inv FIN_VAL.
+  pose proof (create_reg_inv _ _ _ _ _ _ EQ1) as RET_VAL. inv RET_VAL.
+  destruct x3. destruct x4.
+  pose proof (collect_trans_instr_freshreg_trans _ _ _ _ _ _ _ EQ2) as TR_INSTR.
+  pose proof (collect_declare_freshreg_trans _ _ _ _ _ _ EQ3) as TR_DEC.
+  pose proof (create_reg_inv _ _ _ _ _ _ EQ4) as START_VAL. inv START_VAL.
+  pose proof (create_reg_inv _ _ _ _ _ _ EQ5) as RESET_VAL. inv RESET_VAL.
+  pose proof (create_reg_inv _ _ _ _ _ _ EQ6) as CLK_VAL. inv CLK_VAL.
+  rewrite H9 in *. rewrite H8 in *. replace (st_freshreg s4) with (st_freshreg s2) in * by congruence.
+  rewrite H6 in *. rewrite H7 in *. rewrite H5 in *. simpl in *.
+  inv_incr.
+  econstructor; simpl; auto; try lia.
+  intros.
+  assert (EQ3D := EQ3).
+  apply collect_declare_datapath_trans in EQ3.
+  apply collect_declare_controllogic_trans in EQ3D.
+  replace (st_controllogic s10) with (st_controllogic s3) by congruence.
+  replace (st_datapath s10) with (st_datapath s3) by congruence.
+  replace (st_st s10) with (st_st s3) by congruence.
+  eapply iter_expand_instr_spec; eauto with htlspec.
+  apply PTree.elements_complete.
+Qed.