More work on proof

6 files changed, 676 insertions, 118 deletions

diff --git a/src/hls/DHTL.v b/src/hls/DHTL.v
index b80123c..174b54d 100644
--- a/src/hls/DHTL.v
+++ b/src/hls/DHTL.v
@@ -104,8 +104,8 @@ Fixpoint init_regs (vl : list value) (rl : list reg) {struct rl} :=
   | _, _ => empty_assocmap
   end.
 
-Definition empty_stack (m : module) : Verilog.assocmap_arr :=
-  (AssocMap.set m.(mod_stk) (Array.arr_repeat None m.(mod_stk_len)) (AssocMap.empty Verilog.arr)).
+Definition empty_stack stk stk_len : Verilog.assocmap_arr :=
+  (AssocMap.set stk (Array.arr_repeat None stk_len) (AssocMap.empty Verilog.arr)).
 
 (** * Operational Semantics *)
 
@@ -183,13 +183,13 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop :=
       m.(mod_datapath)!st = Some data ->
       Verilog.stmnt_runp f
         (Verilog.mkassociations asr empty_assocmap)
-        (Verilog.mkassociations asa (empty_stack m))
+        (Verilog.mkassociations asa (empty_stack m.(mod_stk) m.(mod_stk_len)))
         data
         (Verilog.mkassociations basr2 nasr2)
         (Verilog.mkassociations basa2 nasa2) ->
       exec_ram
         (Verilog.mkassociations (Verilog.merge_regs nasr2 basr2) empty_assocmap)
-        (Verilog.mkassociations (Verilog.merge_arrs nasa2 basa2) (empty_stack m))
+        (Verilog.mkassociations (Verilog.merge_arrs nasa2 basa2) (empty_stack m.(mod_stk) m.(mod_stk_len)))
         (mod_ram m)
         (Verilog.mkassociations basr3 nasr3)
         (Verilog.mkassociations basa3 nasa3) ->
@@ -211,7 +211,7 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop :=
               (AssocMap.set (mod_finish m) (ZToValue 0)
                (AssocMap.set (mod_st m) (posToValue m.(mod_entrypoint))
                 (init_regs args m.(mod_params)))))
-             (empty_stack m))
+             (empty_stack m.(mod_stk) m.(mod_stk_len)))
 | step_return :
     forall g m asr asa i r sf pc mst,
       mst = mod_st m ->
diff --git a/src/hls/DMemorygen.v b/src/hls/DMemorygen.v
index c0fc03d..846bfad 100644
--- a/src/hls/DMemorygen.v
+++ b/src/hls/DMemorygen.v
@@ -403,7 +403,7 @@ Inductive match_arrs_size : assocmap_arr -> assocmap_arr -> Prop :=
       match_arrs_size nasa basa.
 
 Definition match_empty_size (m : module) (ar : assocmap_arr) : Prop :=
-  match_arrs_size (empty_stack m) ar.
+  match_arrs_size (empty_stack m.(mod_stk) m.(mod_stk_len)) ar.
 #[local] Hint Unfold match_empty_size : mgen.
 
 Definition disable_ram (ram: option ram) (asr : assocmap_reg) : Prop :=
@@ -501,7 +501,7 @@ Lemma match_stacks_equiv :
   forall m s l,
     mod_stk m = s ->
     mod_stk_len m = l ->
-    empty_stack' l s = empty_stack m.
+    empty_stack' l s = empty_stack m.(mod_stk) m.(mod_stk_len).
 Proof. unfold empty_stack', empty_stack; mgen_crush. Qed.
 #[local] Hint Rewrite match_stacks_equiv : mgen.
 
@@ -638,8 +638,8 @@ Qed.
 
 Lemma empty_arr :
   forall m s,
-    (exists l, (empty_stack m) ! s = Some (arr_repeat None l))
-    \/ (empty_stack m) ! s = None.
+    (exists l, (empty_stack m.(mod_stk) m.(mod_stk_len)) ! s = Some (arr_repeat None l))
+    \/ (empty_stack m.(mod_stk) m.(mod_stk_len)) ! s = None.
 Proof.
   unfold empty_stack. simplify.
   destruct (Pos.eq_dec s (mod_stk m)); subst.
@@ -650,13 +650,13 @@ Qed.
 Lemma merge_arr_empty':
   forall m ar s v,
     match_empty_size m ar ->
-    (merge_arrs (empty_stack m) ar) ! s = v ->
+    (merge_arrs (empty_stack m.(mod_stk) m.(mod_stk_len)) ar) ! s = v ->
     ar ! s = v.
 Proof.
   inversion 1; subst.
   pose proof (empty_arr m s).
   simplify_local.
-  destruct (merge_arrs (empty_stack m) ar) ! s eqn:?; subst.
+  destruct (merge_arrs (empty_stack m.(mod_stk) m.(mod_stk_len)) ar) ! s eqn:?; subst.
   - inv H3. inv H4.
     learn H3 as H5. apply H0 in H5. inv H5. simplify_local.
     unfold merge_arrs in *. rewrite AssocMap.gcombine in Heqo; auto.
@@ -678,7 +678,7 @@ Lemma merge_arr_empty :
   forall m ar ar',
     match_empty_size m ar ->
     match_arrs ar ar' ->
-    match_arrs (merge_arrs (empty_stack m) ar) ar'.
+    match_arrs (merge_arrs (empty_stack m.(mod_stk) m.(mod_stk_len)) ar) ar'.
 Proof.
   inversion 1; subst; inversion 1; subst;
   econstructor; intros; apply merge_arr_empty' in H6; auto.
@@ -689,12 +689,12 @@ Lemma merge_arr_empty'':
   forall m ar s v,
     match_empty_size m ar ->
     ar ! s = v ->
-    (merge_arrs (empty_stack m) ar) ! s = v.
+    (merge_arrs (empty_stack m.(mod_stk) m.(mod_stk_len)) ar) ! s = v.
 Proof.
   inversion 1; subst.
   pose proof (empty_arr m s).
   simplify_local.
-  destruct (merge_arrs (empty_stack m) ar) ! s eqn:?; subst.
+  destruct (merge_arrs (empty_stack m.(mod_stk) m.(mod_stk_len)) ar) ! s eqn:?; subst.
   - inv H3. inv H4.
     learn H3 as H5. apply H0 in H5. inv H5. simplify_local.
     unfold merge_arrs in *. rewrite AssocMap.gcombine in Heqo; auto.
@@ -715,7 +715,7 @@ Qed.
 Lemma merge_arr_empty_match :
   forall m ar,
     match_empty_size m ar ->
-    match_empty_size m (merge_arrs (empty_stack m) ar).
+    match_empty_size m (merge_arrs (empty_stack m.(mod_stk) m.(mod_stk_len)) ar).
 Proof.
   inversion 1; subst.
   constructor; simplify_local.
@@ -725,7 +725,7 @@ Proof.
   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 (empty_stack m.(mod_stk) m.(mod_stk_len)) ! s eqn:?;
            destruct ar ! s; try discriminate; eauto.
   apply merge_arr_empty''; auto. apply H2 in H3; auto.
 Qed.
@@ -1196,7 +1196,7 @@ Qed.
 
 Lemma empty_arrs_match :
   forall m,
-    match_arrs (empty_stack m) (empty_stack (transf_module m)).
+    match_arrs (empty_stack m.(mod_stk) m.(mod_stk_len)) (empty_stack (transf_module m).(mod_stk) (transf_module m).(mod_stk_len)).
 Proof.
   intros;
   unfold empty_stack, transf_module; repeat destruct_match; mgen_crush.
@@ -1764,7 +1764,7 @@ 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).
+  forall m, empty_stack (mod_stk m) (mod_stk_len 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.
 
@@ -1954,27 +1954,27 @@ 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'.
+    exists v', (empty_stack (mod_stk m) (mod_stk_len 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.
+    (empty_stack (mod_stk m) (mod_stk_len 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 ->
+    (empty_stack (mod_stk m) (mod_stk_len 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 ->
+    (empty_stack (mod_stk m) (mod_stk_len m)) ! s = Some v ->
     exists v', rab ! s = Some v' /\ arr_length v = arr_length v'.
 Proof. inversion 1; intros; repeat masrp_tac. Qed.
 
@@ -2007,7 +2007,7 @@ Ltac learn_next :=
 
 Ltac learn_empty :=
   match goal with
-  | H: match_empty_size _ _, H2: (empty_stack _) ! _ = Some _ |- _ =>
+  | 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
@@ -2015,7 +2015,7 @@ Ltac learn_empty :=
     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 |- _ =>
+  | 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
@@ -2068,7 +2068,7 @@ Lemma match_arrs_merge_set2 :
     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 (arr_assocmap_set s i v (empty_stack (mod_stk m) (mod_stk_len m)))
                            (merge_arrs ran' rab')).
 Proof.
   simplify.
@@ -2217,7 +2217,7 @@ Qed.
 (*     constructor. admit. *)
 (*   Abort. *)
 
-Lemma empty_stack_transf : forall m, empty_stack (transf_module m) = empty_stack m.
+Lemma empty_stack_transf : forall m, empty_stack (mod_stk (transf_module m)) (mod_stk_len (transf_module m)) = empty_stack (mod_stk m) (mod_stk_len 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.
@@ -2513,7 +2513,7 @@ 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').
+    match_arrs ar (merge_arrs (empty_stack (mod_stk m) (mod_stk_len m)) ar').
 Proof.
   inversion 1; subst; inversion 1; subst.
   econstructor; intros. apply H4 in H6; inv_exists. simplify_local.
@@ -2630,7 +2630,7 @@ Lemma translation_correct_unchanged :
   (H1 : asr ! (mod_st m) = Some (posToValue st))
   (H2 : (mod_datapath m) ! st = Some data)
   (H3 : stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := empty_assocmap |}
-         {| assoc_blocking := asa; assoc_nonblocking := empty_stack m |} data
+         {| assoc_blocking := asa; assoc_nonblocking := empty_stack (mod_stk m) (mod_stk_len m) |} data
          {| assoc_blocking := basr2; assoc_nonblocking := nasr2 |}
          {| assoc_blocking := basa2; assoc_nonblocking := nasa2 |})
   (H5 : (merge_regs empty_assocmap (merge_regs nasr2 basr2)) ! (mod_st m) = Some (posToValue pstval))
@@ -2649,7 +2649,7 @@ Lemma translation_correct_unchanged :
     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 empty_assocmap (merge_regs nasr2 basr2))
-         (merge_arrs (empty_stack m) (merge_arrs nasa2 basa2))) R2.
+         (merge_arrs (empty_stack (mod_stk m) (mod_stk_len m)) (merge_arrs nasa2 basa2))) R2.
 Proof.
   intros.
   unfold alt_unchanged in *; simplify_local.
@@ -2725,7 +2725,7 @@ Lemma translation_correct_store :
   (H1 : asr ! (mod_st m) = Some (posToValue st))
   (H2 : (mod_datapath m) ! st = Some data)
   (H3 : stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := empty_assocmap |}
-         {| assoc_blocking := asa; assoc_nonblocking := empty_stack m |} data
+         {| assoc_blocking := asa; assoc_nonblocking := empty_stack (mod_stk m) (mod_stk_len m) |} data
          {| assoc_blocking := basr2; assoc_nonblocking := nasr2 |}
          {| assoc_blocking := basa2; assoc_nonblocking := nasa2 |})
   (H5 : (merge_regs empty_assocmap (merge_regs nasr2 basr2)) ! (mod_st m) = Some (posToValue pstval))
@@ -2755,7 +2755,7 @@ Lemma translation_correct_store :
     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 empty_assocmap (merge_regs nasr2 basr2))
-         (merge_arrs (empty_stack m) (merge_arrs nasa2 basa2))) R2.
+         (merge_arrs (empty_stack (mod_stk m) (mod_stk_len m)) (merge_arrs nasa2 basa2))) R2.
 Proof.
   intros.
   unfold alt_store in *; simplify_local. inv H3. inv H17. inv H18. inv H16. simplify_local.
@@ -2999,7 +2999,7 @@ Lemma translation_correct_load :
   (H1 : asr ! (mod_st m) = Some (posToValue st))
   (H2 : (mod_datapath m) ! st = Some data)
   (H3 : stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := empty_assocmap |}
-         {| assoc_blocking := asa; assoc_nonblocking := empty_stack m |} data
+         {| assoc_blocking := asa; assoc_nonblocking := empty_stack (mod_stk m) (mod_stk_len m) |} data
          {| assoc_blocking := basr2; assoc_nonblocking := nasr2 |}
          {| assoc_blocking := basa2; assoc_nonblocking := nasa2 |})
   (H5 : (merge_regs empty_assocmap (merge_regs nasr2 basr2)) ! (mod_st m) = Some (posToValue pstval))
@@ -3029,7 +3029,7 @@ Lemma translation_correct_load :
     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 empty_assocmap (merge_regs nasr2 basr2))
-         (merge_arrs (empty_stack m) (merge_arrs nasa2 basa2))) R2.
+         (merge_arrs (empty_stack (mod_stk m) (mod_stk_len m)) (merge_arrs nasa2 basa2))) R2.
 Proof.
   intros.
   unfold alt_load in *; simplify_local. inv H3. inv H22.
@@ -3206,11 +3206,11 @@ Lemma translation_correct :
     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 := asa; assoc_nonblocking := empty_stack (mod_stk m) (mod_stk_len 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 := merge_arrs nasa2 basa2; assoc_nonblocking := empty_stack (mod_stk m) (mod_stk_len m) |} None
              {| assoc_blocking := basr3; assoc_nonblocking := nasr3 |}
              {| assoc_blocking := basa3; assoc_nonblocking := nasa3 |} ->
     (merge_regs nasr3 basr3) ! (mod_st m) = Some (posToValue pstval) ->
@@ -3388,7 +3388,7 @@ Section CORRECTNESS.
       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 (empty_stack (mod_stk (transf_module m)) (mod_stk_len (transf_module m))) with (empty_stack (mod_stk m) (mod_stk_len 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.
@@ -3408,7 +3408,7 @@ Section CORRECTNESS.
       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 (empty_stack (mod_stk (transf_module m)) (mod_stk_len (transf_module m))) with (empty_stack (mod_stk m) (mod_stk_len 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].
diff --git a/src/hls/DVeriloggenproof.v b/src/hls/DVeriloggenproof.v
index 31cdfca..0d417db 100644
--- a/src/hls/DVeriloggenproof.v
+++ b/src/hls/DVeriloggenproof.v
@@ -262,7 +262,7 @@ Proof. unfold transl_module; intros; destruct (DHTL.mod_ram m) eqn:?; crush. Qed
 Lemma mod_params_equiv m : mod_args (transl_module m) = DHTL.mod_params m.
 Proof. unfold transl_module; intros; destruct (DHTL.mod_ram m) eqn:?; crush. Qed.
 
-Lemma empty_stack_equiv m : empty_stack (transl_module m) = DHTL.empty_stack m.
+Lemma empty_stack_equiv m : empty_stack (transl_module m) = DHTL.empty_stack m.(DHTL.mod_stk) m.(DHTL.mod_stk_len).
 Proof. unfold transl_module; intros; destruct (DHTL.mod_ram m) eqn:?; crush. Qed.
 
 Ltac rewrite_eq := rewrite mod_return_equiv
diff --git a/src/hls/Gible.v b/src/hls/Gible.v
index b8feb37..32aa7bc 100644
--- a/src/hls/Gible.v
+++ b/src/hls/Gible.v
@@ -481,6 +481,90 @@ Inductive step_list {A} (step_i: val -> istate -> A -> istate -> Prop):
     step_i sp (Iexec state) i (Iterm state' cf) ->
     step_list step_i sp (Iexec state) (i :: instrs) (Iterm state' cf).
 
+Inductive step_list_nth {A} (step_i: val -> istate -> A -> istate -> Prop):
+  val -> nat -> istate -> list A -> nat -> istate -> Prop :=
+| exec_RBnth_refl :
+  forall out n instrs sp,
+    step_list_nth step_i sp n out instrs n out
+| exec_RBnth_star :
+  forall state i n out instrs sp m out',
+    nth_error instrs n = Some i ->
+    step_i sp state i out ->
+    step_list_nth step_i sp (S n) out instrs m out' ->
+    (n < m)%nat ->
+    step_list_nth step_i sp n state instrs m out'.
+
+Lemma list_drop_nil :
+  forall A n, @list_drop A n nil = nil.
+Proof. intros. destruct n; auto. Qed.
+
+Lemma list_drop_length :
+  forall A n (l: list A), (length l <= n)%nat -> @list_drop A n l = nil.
+Proof. 
+  induction n; intros.
+  - destruct l; cbn in *; auto. lia.
+  - destruct l; cbn; auto.
+    rewrite IHn; eauto. cbn in *. lia.
+Qed.
+
+Lemma step_list_equiv_nth:
+  forall A (step_i: val -> istate -> A -> istate -> Prop) sp l n m st1 st2,
+    step_list_nth step_i sp n st1 l m st2 ->
+    forall offs l',
+    (forall x e, (n <= x < m)%nat -> nth_error l x = Some e -> nth_error l' (x+offs) = Some e) ->
+    step_list_nth step_i sp (n+offs) st1 l' (m+offs) st2.
+Proof.
+  induction 1. intros. constructor.
+  intros. econstructor; eauto; [|lia].
+  eapply IHstep_list_nth; eauto.
+  intros. eapply H3; auto; lia.
+Qed.
+
+Lemma step_list_nth_cons':
+  forall A (step_i: val -> istate -> A -> istate -> Prop) sp 
+      n m (l: list A) a st1 st2,
+    step_list_nth step_i sp n st1 l m st2 ->
+    step_list_nth step_i sp (S n) st1 (a :: l) (S m) st2.
+Proof.
+  intros * Hstep.
+  assert (Hequiv: forall x e, (n <= x < m)%nat -> nth_error l x = Some e -> nth_error (a :: l) (x+1) = Some e).
+  { intros. replace (a :: l) with ((a :: nil) ++ l) by auto.
+    rewrite nth_error_app2 by (cbn; lia).
+    cbn. now replace ((x + 1 - 1)%nat) with x by lia.
+  }
+  replace (S n) with (n + 1)%nat by lia.
+  replace (S m) with (m + 1)%nat by lia.
+  eapply step_list_equiv_nth; eauto.
+Qed.
+
+Lemma step_list_nth_cons :
+  forall A (step_i: val -> istate -> A -> istate -> Prop) sp 
+      (instrs: list A) (a: A) l st1 st2 st3,
+    step_i sp st1 a st2 ->
+    step_list_nth step_i sp 0 st2 instrs l st3 ->
+    step_list_nth step_i sp 0 st1 (a :: instrs) (S l) st3.
+Proof.
+  intros. econstructor; cbn; eauto; [|lia].
+  replace 1%nat with (0 + 1)%nat at 1 by lia. 
+  now apply step_list_nth_cons'.
+Qed.
+
+Lemma step_list_equiv :
+  forall A step_i sp (instrs: list A) st1 st2,
+    step_list step_i sp st1 instrs st2 ->
+    exists l, step_list_nth step_i sp 0 st1 instrs l st2 
+      /\ (l <= length instrs)%nat.
+Proof.
+  induction instrs.
+  - cbn; intros. inv H.
+  - cbn; intros. inv H.
+    + exploit IHinstrs. eauto. simplify.
+      exists (S x). split; [|lia].
+      eapply step_list_nth_cons; eauto.
+    + exists 1%nat. split; [|lia].
+      econstructor; cbn; eauto. constructor.
+Qed.
+
 Inductive step_list2 {A} (step_i: val -> istate -> A -> istate -> Prop):
   val -> istate -> list A -> istate -> Prop :=
 | exec_RBcons2 :
@@ -504,6 +588,21 @@ Inductive step_list_inter {A} (step_i: val -> istate -> A -> istate -> Prop):
   forall i cf l sp,
     step_list_inter step_i sp (Iterm i cf) l (Iterm i cf).
 
+Inductive step_list_inter_strict {A} (step_i: val -> istate -> A -> istate -> Prop):
+  val -> istate -> list A -> istate -> Prop :=
+| exec_term_strict_RBcons :
+  forall i0 i1 i2 i instrs sp,
+    step_i sp (Iexec i0) i i1 ->
+    step_list_inter_strict step_i sp i1 instrs i2 ->
+    step_list_inter_strict step_i sp (Iexec i0) (i :: instrs) i2
+| exec_term_strict_RBnil :
+  forall sp i, step_list_inter_strict step_i sp i nil i
+| exec_term_strict_RBcons_term :
+  forall i cf instr instrs sp,
+    step_i sp (Iexec i) instr (Iexec i) ->
+    step_list_inter_strict step_i sp (Iexec i) instrs (Iexec i) ->
+    step_list_inter_strict step_i sp (Iterm i cf) (instr :: instrs) (Iterm i cf).
+
 (*|
 Top-Level Type Definitions
 ==========================
diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v
index abdec08..1966ba1 100644
--- a/src/hls/HTLPargen.v
+++ b/src/hls/HTLPargen.v
@@ -81,9 +81,9 @@ Fixpoint pred_expr (p: pred_op) :=
   | Plit (b, pred) =>
     if b
     then Vvar (pred_enc pred)
-    else Vunop Vnot (Vvar (pred_enc pred))
-  | Ptrue => Vlit (ZToValue 1)
-  | Pfalse => Vlit (ZToValue 0)
+    else (Vbinop Veq (Vvar (pred_enc pred)) (Vlit Integers.Int.zero))
+  | Ptrue => Vlit (boolToValue true)
+  | Pfalse => Vlit (boolToValue false)
   | Pand p1 p2 =>
     Vbinop Vand (pred_expr p1) (pred_expr p2)
   | Por p1 p2 =>
@@ -291,23 +291,23 @@ Definition tbl_to_case_expr (st : reg) (ns : list node) : list (expr * stmnt) :=
                   end)
            (enumerate 0 ns).
 
-Definition translate_cfi (fin rtrn state: reg) p (cfi: cf_instr)
+Definition translate_cfi (ctrl: control_regs) p (cfi: cf_instr)
   : Errors.res stmnt :=
   match cfi with
   | RBgoto n' =>
-    Errors.OK (state_goto p state n')
+    Errors.OK (state_goto p ctrl.(ctrl_st) n')
   | RBcond c args n1 n2 =>
     do e <- translate_condition c args;
-    Errors.OK (state_cond p state e n1 n2)
+    Errors.OK (state_cond p ctrl.(ctrl_st) e n1 n2)
   | RBreturn r =>
     match r with
     | Some r' =>
-      Errors.OK (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vvar r')))
+      Errors.OK (Vseq (block ctrl.(ctrl_fin) (Vlit (ZToValue 1%Z))) (block ctrl.(ctrl_return) (Vvar r')))
     | None =>
-      Errors.OK (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vlit (ZToValue 0%Z))))
+      Errors.OK (Vseq (block ctrl.(ctrl_fin) (Vlit (ZToValue 1%Z))) (block ctrl.(ctrl_return) (Vlit (ZToValue 0%Z))))
     end
   | RBjumptable r tbl =>
-    Errors.OK (Vcase (Vvar r) (list_to_stmnt (tbl_to_case_expr state tbl)) (Some Vskip))
+    Errors.OK (Vcase (Vvar r) (list_to_stmnt (tbl_to_case_expr ctrl.(ctrl_st) tbl)) (Some Vskip))
   | RBcall sig ri rl r n =>
     Errors.Error (Errors.msg "HTLPargen: RBcall not supported.")
   | RBtailcall sig ri lr =>
@@ -316,8 +316,7 @@ Definition translate_cfi (fin rtrn state: reg) p (cfi: cf_instr)
     Errors.Error (Errors.msg "HTLPargen: RBbuildin not supported.")
   end.
 
-Definition transf_instr (fin rtrn stack state: reg) 
-           (dc: pred_op * stmnt) (i: instr)
+Definition transf_instr (ctrl: control_regs) (dc: pred_op * stmnt) (i: instr)
            : Errors.res (pred_op * stmnt) :=
   let '(curr_p, d) := dc in
   let npred p := Some (Pand curr_p (dfltp p)) in
@@ -328,11 +327,11 @@ Definition transf_instr (fin rtrn stack state: reg)
     let stmnt := translate_predicate Vblock (npred p) (Vvar dst) instr in
     Errors.OK (curr_p, Vseq d stmnt)
   | RBload p mem addr args dst =>
-    do src <- translate_arr_access mem addr args stack;
+    do src <- translate_arr_access mem addr args ctrl.(ctrl_stack);
     let stmnt := translate_predicate Vblock (npred p) (Vvar dst) src in
     Errors.OK (curr_p, Vseq d stmnt)
   | RBstore p mem addr args src =>
-    do dst <- translate_arr_access mem addr args stack;
+    do dst <- translate_arr_access mem addr args ctrl.(ctrl_stack);
     let stmnt := translate_predicate Vblock (npred p) dst (Vvar src) in
     Errors.OK (curr_p, Vseq d stmnt)
   | RBsetpred p' cond args p =>
@@ -340,50 +339,39 @@ Definition transf_instr (fin rtrn stack state: reg)
     let stmnt := translate_predicate Vblock (npred p') (pred_expr (Plit (true, p))) cond' in
     Errors.OK (curr_p, Vseq d stmnt)
   | RBexit p cf => 
-    do d_stmnt <- translate_cfi fin rtrn state (npred p) cf;
+    do d_stmnt <- translate_cfi ctrl (npred p) cf;
     Errors.OK (Pand curr_p (negate (dfltp p)), Vseq d d_stmnt)
   end.
 
-Definition transf_chained_block (fin rtrn stack state: reg)
-           (dc: @pred_op positive * stmnt)
-           (block: list instr)
+Definition transf_chained_block (ctrl: control_regs) (dc: @pred_op positive * stmnt) (block: list instr)
            : Errors.res (pred_op * stmnt) :=
-  mfold_left (transf_instr fin rtrn stack state) block (ret dc).
+  mfold_left (transf_instr ctrl) block (ret dc).
 
-Definition transf_parallel_block (fin rtrn stack state: reg)
-           (dc: @pred_op positive * stmnt)
-           (block: list (list instr))
+Definition transf_parallel_block (ctrl: control_regs) (dc: @pred_op positive * stmnt) (block: list (list instr))
            : Errors.res (pred_op * stmnt) :=
-  mfold_left (transf_chained_block fin rtrn stack state) block (ret dc).
+  mfold_left (transf_chained_block ctrl) block (ret dc).
 
-Definition transf_parallel_full_block (fin rtrn stack state: reg)
-           (dc: node * @pred_op positive * datapath)
-           (block: list (list instr))
+Definition transf_parallel_full_stmnt ctrl curr_p n block :=
+  do ctrl_init_stmnt <- translate_cfi ctrl (Some curr_p) (RBgoto (n - 1)%positive);
+  transf_parallel_block ctrl (curr_p, ctrl_init_stmnt) block.
+
+Definition transf_parallel_full_block (ctrl: control_regs) (dc: node * @pred_op positive * datapath) (block: list (list instr))
            : Errors.res (node * pred_op * datapath) :=
   let '(n, curr_p, dt) := dc in
   match AssocMap.get n dt with
   | None =>
-    do ctrl_init_stmnt <-
-          translate_cfi fin rtrn state (Some curr_p) (RBgoto (n - 1)%positive);
-    do dc' <- transf_parallel_block fin rtrn stack state (curr_p, ctrl_init_stmnt) block;
-    let '(curr_p', dt_stmnt) := dc' in
+    do (curr_p', dt_stmnt) <- transf_parallel_full_stmnt ctrl curr_p n block;
     Errors.OK ((n - 1)%positive, curr_p', AssocMap.set n dt_stmnt dt)
   | _ => Errors.Error (msg "HtlPargen.transf_parallel_full_block: block not empty")
   end.
 
-Definition transf_seq_block (fin rtrn stack state: reg)
-           (d: datapath) (n: node)
-           (block: list (list (list instr)))
+Definition transf_seq_block (ctrl: control_regs) (d: datapath) (ni: node * ParBB.t)
            : Errors.res datapath :=
-  do res <- mfold_left
-    (transf_parallel_full_block fin rtrn stack state) block (ret (n, Ptrue, d));
+  let (n, block) := ni in
+  do res <- mfold_left (transf_parallel_full_block ctrl) block (ret (n, Ptrue, d));
   let '(_, _, d') := res in
   Errors.OK d'.
 
-Definition transf_seq_blockM (ctrl: control_regs) (d: datapath) (ni: node * ParBB.t): res datapath :=
-    let (n, i) := ni in
-    transf_seq_block ctrl.(ctrl_fin) ctrl.(ctrl_return) ctrl.(ctrl_stack) ctrl.(ctrl_st) d n i.
-
 Definition stack_correct (sz : Z) : bool :=
   (0 <=? sz) && (sz <? Integers.Ptrofs.modulus) && (Z.modulo sz 4 =? 0).
 
@@ -439,7 +427,7 @@ Program Definition transl_module (f: function) : res DHTL.module :=
     let start := Pos.succ stack in
     let rst := Pos.succ start in
     let clk := Pos.succ rst in
-    do _stmnt <- mfold_left (transf_seq_blockM (mk_control_regs st stack fin rtrn)) 
+    do _stmnt <- mfold_left (transf_seq_block (mk_control_regs st stack fin rtrn)) 
                             (Maps.PTree.elements f.(GiblePar.fn_code)) (ret (PTree.empty _));
     match zle (Z.pos (max_pc_map _stmnt)) Integers.Int.max_unsigned,
             decide_order st fin rtrn stack start rst clk,
diff --git a/src/hls/HTLPargenproof.v b/src/hls/HTLPargenproof.v
index 2a582df..04b87f0 100644
--- a/src/hls/HTLPargenproof.v
+++ b/src/hls/HTLPargenproof.v
@@ -69,8 +69,9 @@ Inductive match_arrs (stack_size: Z) (stk: positive) (stk_len: nat) (sp : Values
 | match_arr : forall asa stack,
     asa ! stk = Some stack /\
     stack.(arr_length) = Z.to_nat (stack_size / 4) /\
+    stack.(arr_length) = stk_len /\
     (forall ptr,
-        0 <= ptr < Z.of_nat stk_len ->
+        0 <= ptr < Z.of_nat stack.(arr_length) ->
         opt_val_value_lessdef (Mem.loadv AST.Mint32 mem
                                          (Values.Val.offset_ptr sp (Ptrofs.repr (4 * ptr))))
                               (Option.default (NToValue 0)
@@ -144,6 +145,22 @@ Inductive match_states : GiblePar.state -> DHTL.state -> Prop :=
       match_states (GiblePar.Callstate nil (AST.Internal f) nil m0) (DHTL.Callstate nil m nil).
 #[local] Hint Constructors match_states : htlproof.
 
+Inductive match_states_reduced : nat -> GiblePar.state -> DHTL.state -> Prop :=
+| match_states_reduced_intro : forall asa asr sf f sp sp' rs mem m st res ps n
+    (MASSOC : match_assocmaps (max_reg_function f) (max_pred_function f) rs ps asr)
+    (TF : transl_module f = Errors.OK m)
+    (WF : state_st_wf asr m.(DHTL.mod_st) (Pos.of_nat (Pos.to_nat st - n)%nat))
+    (MF : match_frames sf res)
+    (MARR : match_arrs f.(fn_stacksize) m.(DHTL.mod_stk) m.(DHTL.mod_stk_len) sp mem asa)
+    (SP : sp = Values.Vptr sp' (Ptrofs.repr 0))
+    (RSBP : reg_stack_based_pointers sp' rs)
+    (ASBP : arr_stack_based_pointers sp' mem (f.(GiblePar.fn_stacksize)) sp)
+    (BOUNDS : stack_bounds sp (f.(GiblePar.fn_stacksize)) mem)
+    (CONST : match_constants m.(DHTL.mod_reset) m.(DHTL.mod_finish) asr),
+    (* Add a relation about ps compared with the state register. *)
+    match_states_reduced n (GiblePar.State sf f sp st rs ps mem)
+                 (DHTL.State res m (Pos.of_nat (Pos.to_nat st - n)%nat) asr asa).
+
 Definition match_prog (p: GiblePar.program) (tp: DHTL.program) :=
   Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq p tp /\
   main_is_internal p = true.
@@ -212,11 +229,11 @@ Lemma plt_pred_enc :
   forall a b, Ple a b -> Ple (pred_enc a) (pred_enc b).
 Proof. unfold Ple, reg_enc, pred_enc in *; intros. lia. Qed.
 
-Lemma reg_enc_inj : 
+Lemma reg_enc_inj :
   forall a b, reg_enc a = reg_enc b -> a = b.
 Proof. unfold reg_enc; intros; lia. Qed.
 
-Lemma pred_enc_inj : 
+Lemma pred_enc_inj :
   forall a b, pred_enc a = pred_enc b -> a = b.
 Proof. unfold pred_enc; intros; lia. Qed.
 
@@ -639,7 +656,7 @@ Section CORRECTNESS.
       Forall (fun x => Ple x m) l ->
       In y l ->
       Ple y m.
-  Proof. 
+  Proof.
     intros. eapply Forall_forall in H; eauto.
   Qed.
 
@@ -888,11 +905,11 @@ Section CORRECTNESS.
       val_value_lessdef (Values.Val.add a b) (Int.add a' b').
   Proof.
     intros * HPLE HPLE0.
-    inv HPLE; inv HPLE0; cbn in *; unfold valueToInt; 
+    inv HPLE; inv HPLE0; cbn in *; unfold valueToInt;
     try destruct_match; constructor; auto; unfold valueToPtr;
-    unfold Ptrofs.of_int; apply ptrofs_inj; 
+    unfold Ptrofs.of_int; apply ptrofs_inj;
     rewrite Ptrofs.unsigned_repr by auto with int_ptrofs;
-    [rewrite Int.add_commut|]; apply Ptrofs.agree32_add; auto; 
+    [rewrite Int.add_commut|]; apply Ptrofs.agree32_add; auto;
     rewrite <- Int.repr_unsigned; now apply Ptrofs.agree32_repr.
   Qed.
 
@@ -903,7 +920,7 @@ Section CORRECTNESS.
   Proof.
     intros * HPLE.
     inv HPLE; cbn in *; unfold valueToInt; try destruct_match; try constructor; auto.
-    unfold valueToPtr. apply ptrofs_inj. unfold Ptrofs.of_int. 
+    unfold valueToPtr. apply ptrofs_inj. unfold Ptrofs.of_int.
     rewrite Ptrofs.unsigned_repr by auto with int_ptrofs.
     apply Ptrofs.agree32_add; auto. rewrite <- Int.repr_unsigned.
     apply Ptrofs.agree32_repr; auto.
@@ -924,7 +941,7 @@ Section CORRECTNESS.
     pose proof MSTATE as MSTATE_2. inv MSTATE.
     inv MASSOC. unfold translate_instr in TR_INSTR; repeat (unfold_match TR_INSTR); inv TR_INSTR;
     unfold Op.eval_operation in EVAL; repeat (unfold_match EVAL); inv EVAL;
-    repeat (simplify; eval_correct_tac; unfold valueToInt in *);  
+    repeat (simplify; eval_correct_tac; unfold valueToInt in *);
     repeat (apply Forall_cons_iff in INSTR; destruct INSTR as (?HPLE & INSTR));
       try (apply H in HPLE); try (apply H in HPLE0).
     - do 2 econstructor; eauto. repeat econstructor.
@@ -957,9 +974,9 @@ Section CORRECTNESS.
     - do 2 econstructor; eauto. repeat econstructor. now apply eval_correct_shl'.
     - do 2 econstructor; eauto. repeat econstructor. now apply eval_correct_shr.
     - do 2 econstructor; eauto. repeat econstructor. now apply eval_correct_shr'.
-    - inv H2. rewrite Heqv0 in HPLE. inv HPLE. 
-      assert (0 <= 31 <= Int.max_unsigned). 
-      { pose proof Int.two_wordsize_max_unsigned as Y. 
+    - inv H2. rewrite Heqv0 in HPLE. inv HPLE.
+      assert (0 <= 31 <= Int.max_unsigned).
+      { pose proof Int.two_wordsize_max_unsigned as Y.
         unfold Int.zwordsize, Int.wordsize, Wordsize_32.wordsize in Y. lia. }
       assert (Int.unsigned n <= 30).
       { unfold Int.ltu in Heqb. destruct_match; try discriminate.
@@ -978,7 +995,7 @@ Section CORRECTNESS.
           assert (Int.signed (find_assocmap 32 (reg_enc p) asr) >= 0 -> False) by auto. apply H3. unfold Int.lt in HLT.
           destruct_match; try discriminate. auto. }
         destruct_match; try discriminate.
-        do 2 econstructor; eauto. eapply erun_Vternary_false; repeat econstructor. 
+        do 2 econstructor; eauto. eapply erun_Vternary_false; repeat econstructor.
         now rewrite HLT.
         constructor; cbn. unfold IntExtra.shrx_alt. rewrite Heqs. auto.
     - do 2 econstructor; eauto. repeat econstructor. now apply eval_correct_shru.
@@ -993,12 +1010,12 @@ Section CORRECTNESS.
         apply eval_correct_add; auto. apply eval_correct_add; auto.
         constructor; auto.
       + inv H2. do 2 econstructor; eauto. repeat econstructor. unfold ZToValue.
-        apply eval_correct_add; try constructor; auto. 
-        apply eval_correct_mul; try constructor; auto. 
+        apply eval_correct_add; try constructor; auto.
+        apply eval_correct_mul; try constructor; auto.
       + inv H2. do 2 econstructor; eauto. repeat econstructor. unfold ZToValue.
         apply eval_correct_add; try constructor; auto.
-        apply eval_correct_add; try constructor; auto. 
-        apply eval_correct_mul; try constructor; auto. 
+        apply eval_correct_add; try constructor; auto.
+        apply eval_correct_mul; try constructor; auto.
       + inv H2. do 2 econstructor; eauto. repeat econstructor. unfold ZToValue.
         assert (X: Archi.ptr64 = false) by auto.
         rewrite X in H3. inv H3.
@@ -1045,6 +1062,73 @@ Ltac unfold_merge :=
     rewrite merge_get_default2 by auto. auto.
   Qed.
 
+  Lemma match_constants_merge_empty:
+    forall n m ars,
+      match_constants n m ars ->
+      match_constants n m (AssocMapExt.merge value empty_assocmap ars).
+  Proof.
+    inversion 1. constructor; unfold AssocMapExt.merge.
+    - rewrite PTree.gcombine; auto.
+    - rewrite PTree.gcombine; auto.
+  Qed.
+
+  Lemma match_state_st_wf_empty:
+    forall asr st pc,
+      state_st_wf asr st pc ->
+      state_st_wf (AssocMapExt.merge value empty_assocmap asr) st pc.
+  Proof.
+    unfold state_st_wf; intros.
+    unfold AssocMapExt.merge. rewrite AssocMap.gcombine by auto. rewrite H.
+    rewrite AssocMap.gempty. auto.
+  Qed.
+
+  Lemma match_arrs_merge_empty:
+    forall sz stk stk_len sp mem asa,
+      match_arrs sz stk stk_len sp mem asa ->
+      match_arrs sz stk stk_len sp mem (merge_arrs (DHTL.empty_stack stk stk_len) asa).
+  Proof.
+    inversion 1. inv H0. inv H3. inv H1. destruct stack. econstructor; unfold AssocMapExt.merge.
+    split; [|split]; [| |split]; cbn in *.
+    - unfold merge_arrs in *. rewrite AssocMap.gcombine by auto.
+      setoid_rewrite H2. unfold DHTL.empty_stack. rewrite AssocMap.gss.
+      cbn in *. eauto.
+    - cbn. rewrite list_combine_length. rewrite list_repeat_len. lia.
+    - cbn. rewrite list_combine_length. rewrite list_repeat_len. lia.
+    - cbn; intros.
+      assert ((Datatypes.length (list_combine merge_cell (list_repeat None arr_length) arr_contents)) = arr_length).
+      { rewrite list_combine_length. rewrite list_repeat_len. lia. }
+      rewrite H3 in H1. apply H4 in H1.
+      inv H1; try constructor.
+      assert (array_get_error (Z.to_nat ptr)
+           {| arr_contents := arr_contents; arr_length := Datatypes.length arr_contents; arr_wf := eq_refl |} =
+           (array_get_error (Z.to_nat ptr)
+             (combine merge_cell (arr_repeat None (Datatypes.length arr_contents))
+                {| arr_contents := arr_contents; arr_length := Datatypes.length arr_contents; arr_wf := eq_refl |}))).
+      { apply array_get_error_equal; auto. cbn. now rewrite list_combine_none. }
+      rewrite <- H1. auto.
+  Qed.
+
+  Lemma match_states_merge_empty :
+    forall st f sp pc rs ps m st' modle asr asa,
+      match_states (GiblePar.State st f sp pc rs ps m) (DHTL.State st' modle pc asr asa) ->
+      match_states (GiblePar.State st f sp pc rs ps m) (DHTL.State st' modle pc (AssocMapExt.merge value empty_assocmap asr) asa).
+  Proof.
+    inversion 1; econstructor; eauto using match_assocmaps_merge_empty,
+      match_constants_merge_empty, match_state_st_wf_empty.
+  Qed.
+
+  Lemma match_states_merge_empty_arr :
+    forall st f sp pc rs ps m st' modle asr asa,
+      match_states (GiblePar.State st f sp pc rs ps m) (DHTL.State st' modle pc asr asa) ->
+      match_states (GiblePar.State st f sp pc rs ps m) (DHTL.State st' modle pc asr (merge_arrs (DHTL.empty_stack modle.(DHTL.mod_stk) modle.(DHTL.mod_stk_len)) asa)).
+  Proof. inversion 1; econstructor; eauto using match_arrs_merge_empty. Qed.
+
+  Lemma match_states_merge_empty_all :
+    forall st f sp pc rs ps m st' modle asr asa,
+      match_states (GiblePar.State st f sp pc rs ps m) (DHTL.State st' modle pc asr asa) ->
+      match_states (GiblePar.State st f sp pc rs ps m) (DHTL.State st' modle pc (AssocMapExt.merge value empty_assocmap asr) (merge_arrs (DHTL.empty_stack modle.(DHTL.mod_stk) modle.(DHTL.mod_stk_len)) asa)).
+  Proof. eauto using match_states_merge_empty, match_states_merge_empty_arr. Qed.
+
   Opaque AssocMap.get.
   Opaque AssocMap.set.
   Opaque AssocMapExt.merge.
@@ -1060,25 +1144,12 @@ Ltac unfold_merge :=
     intros * YFRL YFRL2 YMATCH.
     inv YMATCH. constructor; intros x' YPLE.
     unfold "#", AssocMapExt.get_default in *.
-    rewrite <- YFRL by auto.
-    eauto.
-    unfold "#", AssocMapExt.get_default. rewrite <- YFRL2 by auto.
-    eauto.
+    rewrite <- YFRL by auto. eauto.
+    unfold "#", AssocMapExt.get_default. rewrite <- YFRL2 by auto. eauto.
   Qed.
 
   Definition e_assoc asr : reg_associations := mkassociations asr (AssocMap.empty _).
-  Definition e_assoc_arr asr : arr_associations := mkassociations asr (AssocMap.empty _).
-
-  Lemma transl_iop_correct:
-    forall sp max_reg max_pred d d' curr_p next_p fin rtrn stack state rs ps m rs' ps' p op args dst asr arr asr' arr',
-      transf_instr fin rtrn stack state (curr_p, d) (RBop p op args dst) = Errors.OK (next_p, d') ->
-      step_instr ge sp (Iexec (mk_instr_state rs ps m)) (RBop p op args dst) (Iexec (mk_instr_state rs' ps m)) ->
-      stmnt_runp tt (e_assoc asr) (e_assoc_arr arr) d (e_assoc asr') (e_assoc_arr arr') ->
-      match_assocmaps max_reg max_pred rs ps asr' ->
-      exists asr'', stmnt_runp tt (e_assoc asr) (e_assoc_arr arr) d' (e_assoc asr'') (e_assoc_arr arr') 
-        /\ match_assocmaps max_reg max_pred rs' ps' asr''.
-  Proof.
-    Admitted.
+  Definition e_assoc_arr stk stk_len asr : arr_associations := mkassociations asr (DHTL.empty_stack stk stk_len).
 
   Lemma option_inv :
     forall A x y,
@@ -1194,6 +1265,17 @@ Proof.
   now rewrite AssocMap.gempty.
 Qed.
 
+  Lemma transl_iop_correct:
+    forall ctrl sp max_reg max_pred d d' curr_p next_p rs ps m rs' ps' p op args dst asr arr asr' arr' stk stk_len,
+      transf_instr ctrl (curr_p, d) (RBop p op args dst) = Errors.OK (next_p, d') ->
+      step_instr ge sp (Iexec (mk_instr_state rs ps m)) (RBop p op args dst) (Iexec (mk_instr_state rs' ps m)) ->
+      stmnt_runp tt (e_assoc asr) (e_assoc_arr stk stk_len arr) d (e_assoc asr') (e_assoc_arr stk stk_len arr') ->
+      match_assocmaps max_reg max_pred rs ps asr' ->
+      exists asr'', stmnt_runp tt (e_assoc asr) (e_assoc_arr stk stk_len arr) d' (e_assoc asr'') (e_assoc_arr stk stk_len arr')
+        /\ match_assocmaps max_reg max_pred rs' ps' asr''.
+  Proof.
+    Admitted.
+
 Transparent Mem.load.
 Transparent Mem.store.
 Transparent Mem.alloc.
@@ -1215,14 +1297,14 @@ Transparent Mem.alloc.
     econstructor. split. apply Smallstep.plus_one.
     eapply DHTL.step_call.
 
-    unfold transl_module, Errors.bind, Errors.bind2, ret in *. 
+    unfold transl_module, Errors.bind, Errors.bind2, ret in *.
     repeat (destruct_match; try discriminate; []). inv TF. cbn.
     econstructor; eauto; inv MSTATE; inv H1; eauto.
 
     - constructor; intros.
       + pose proof (ple_max_resource_function f r H0) as Hple.
         unfold Ple in *. repeat rewrite assocmap_gso by lia. rewrite init_regs_empty.
-        rewrite dhtl_init_regs_empty. rewrite assocmap_gempty. rewrite Registers.Regmap.gi. 
+        rewrite dhtl_init_regs_empty. rewrite assocmap_gempty. rewrite Registers.Regmap.gi.
         constructor.
       + pose proof (ple_pred_max_resource_function f r H0) as Hple.
         unfold Ple in *. repeat rewrite assocmap_gso by lia.
@@ -1234,8 +1316,9 @@ Transparent Mem.alloc.
     - unfold DHTL.empty_stack. cbn in *. econstructor. repeat split; intros.
       + now rewrite AssocMap.gss.
       + cbn. now rewrite list_repeat_len.
+      + cbn. now rewrite list_repeat_len.
       + destruct (Mem.loadv Mint32 m' (Values.Val.offset_ptr (Values.Vptr stk Ptrofs.zero) (Ptrofs.repr (4 * ptr)))) eqn:Heqn; constructor.
-        unfold Mem.loadv in Heqn. destruct_match; try discriminate. cbn in Heqv0. 
+        unfold Mem.loadv in Heqn. destruct_match; try discriminate. cbn in Heqv0.
         symmetry in Heqv0. inv Heqv0.
         pose proof Mem.load_alloc_same as LOAD_ALLOC.
         pose proof H as ALLOC.
@@ -1256,7 +1339,7 @@ Transparent Mem.alloc.
         destruct_match; auto. unfold Mem.valid_access, Mem.range_perm, Mem.perm, Mem.perm_order' in *.
         clear Heqs2. inv v0. cbn -[Ptrofs.max_unsigned] in *. inv Heqv0. exfalso.
         specialize (H ptr). rewrite ! Ptrofs.add_zero_l in H. rewrite ! Ptrofs.unsigned_repr in H.
-        specialize (H ltac:(lia)). destruct_match; auto. rewrite PMap.gss in Heqo. 
+        specialize (H ltac:(lia)). destruct_match; auto. rewrite PMap.gss in Heqo.
         destruct_match; try discriminate. simplify. apply proj_sumbool_true in H5. lia.
         apply stack_correct_inv in Heqb. lia.
       + unfold Mem.storev. destruct_match; auto.
@@ -1264,7 +1347,7 @@ Transparent Mem.alloc.
         destruct_match; auto. unfold Mem.valid_access, Mem.range_perm, Mem.perm, Mem.perm_order' in *.
         clear Heqs2. inv v0. cbn -[Ptrofs.max_unsigned] in *. inv Heqv0. exfalso.
         specialize (H ptr). rewrite ! Ptrofs.add_zero_l in H. rewrite ! Ptrofs.unsigned_repr in H.
-        specialize (H ltac:(lia)). destruct_match; auto. rewrite PMap.gss in Heqo. 
+        specialize (H ltac:(lia)). destruct_match; auto. rewrite PMap.gss in Heqo.
         destruct_match; try discriminate. simplify. apply proj_sumbool_true in H5. lia.
         apply stack_correct_inv in Heqb. lia.
     - cbn; constructor; repeat rewrite PTree.gso by lia; now rewrite PTree.gss.
@@ -1287,6 +1370,395 @@ Opaque Mem.alloc.
   Qed.
   #[local] Hint Resolve transl_returnstate_correct : htlproof.
 
+  Lemma mfold_left_error:
+    forall A B f l m, @mfold_left A B f l (Error m) = Error m.
+  Proof. now induction l. Qed.
+
+  Lemma transf_block_correct1:
+    forall l ctrl d d' pc bb pbb i,
+      mfold_left (transf_seq_block ctrl) l (OK d) = OK d' ->
+      In (pc, bb) l ->
+      nth_error bb i = Some pbb ->
+      exists curr_p next_p stmnt,
+        d' ! (Pos.of_nat (Pos.to_nat pc - i)%nat) = Some stmnt
+        /\ transf_parallel_full_stmnt ctrl curr_p (Pos.of_nat (Pos.to_nat pc - i)%nat) pbb
+           = OK (next_p, stmnt).
+  Admitted.
+
+  Lemma step_list_inter_not_term :
+    forall A step_i sp i cf l i' cf',
+      @step_list_inter A step_i sp (Iterm i cf) l (Iterm i' cf') ->
+      i = i' /\ cf = cf'.
+  Proof. now inversion 1. Qed.
+
+  Lemma step_list_inter_not_exec :
+    forall A step_i sp i cf l i',
+      ~ @step_list_inter A step_i sp (Iterm i cf) l (Iexec i').
+  Proof. now inversion 1. Qed.
+
+  Lemma step_list_nth_iterm':
+    forall sp n instrs m out1 out2,
+      step_list_nth (ParBB.step_instr_seq ge) sp n out1 instrs m out2 ->
+      forall i cf,
+        out1 = Iterm i cf ->
+        out1 = out2.
+  Proof.
+    induction 1; subst; auto.
+    intros. subst. destruct out.
+    - now apply step_list_inter_not_exec in H0.
+    - apply step_list_inter_not_term in H0. inv H0.
+      now erewrite <- IHstep_list_nth by eauto.
+  Qed.
+
+  Lemma step_list_nth_iterm:
+    forall sp n instrs m out2 i cf,
+      step_list_nth (ParBB.step_instr_seq ge) sp n (Iterm i cf) instrs m out2 ->
+      Iterm i cf = out2.
+  Proof. eauto using step_list_nth_iterm'. Qed.
+
+  Lemma transl_step_state_correct' :
+    forall sp bb pc_final vstep init_state final_state pc_init,
+      step_list_nth vstep sp pc_init init_state bb pc_final final_state ->
+      forall rs rs' m m' pr pr' cf state t pc f s,
+        vstep = (ParBB.step_instr_seq ge) ->
+        init_state = (Iexec {| is_rs := rs; is_ps := pr; is_mem := m |}) ->
+        final_state = (Iterm {| is_rs := rs'; is_ps := pr'; is_mem := m' |} cf) ->
+        (fn_code f) ! pc = Some bb ->
+        (pc_final <= Datatypes.length bb)%nat ->
+        step_cf_instr ge (GiblePar.State s f sp pc rs' pr' m') cf t state ->
+        forall R1 : DHTL.state,
+          match_states_reduced pc_init (GiblePar.State s f sp pc rs pr m) R1 ->
+          exists R2 : DHTL.state, Smallstep.plus DHTL.step tge R1 t R2 /\ match_states state R2.
+  Proof.
+    induction 1; intros * EQ1 EQ2 EQ3 HCODE HBOUND HSTEP R1 HMATCH; subst.
+    - discriminate.
+    - destruct out as [[rs_mid ps_mid m_mid] | [rs_mid ps_mid m_mid] cf_mid].
+      + inv HMATCH. unfold transl_module, Errors.bind, ret in TF.
+        repeat (destruct_match; try discriminate; []).
+        inv TF.
+        exploit transf_block_correct1. eauto. apply PTree.elements_correct. eassumption.
+        eauto.
+        intros (curr_p & next_p & stmnt0 & HIND & HTRANSF).
+        exploit IHstep_list_nth; trivial.
+        * eassumption.
+        * eassumption.
+        * admit.
+        * intros (R2' & HSMALL & HMATCH'). admit.
+      + clear IHstep_list_nth.
+        pose proof (step_list_nth_iterm _ _ _ _ _ _ _ H1) as HITERM. inv HITERM.
+        admit.
+  Admitted.
+
+Inductive match_states_reduced' : GiblePar.state -> DHTL.state -> Prop :=
+| match_states_reduced'_intro : forall asa asr sf f sp sp' rs mem m st res ps n
+    (MASSOC : match_assocmaps (max_reg_function f) (max_pred_function f) rs ps asr)
+    (TF : transl_module f = Errors.OK m)
+    (WF : state_st_wf asr m.(DHTL.mod_st) n)
+    (MF : match_frames sf res)
+    (MARR : match_arrs f.(fn_stacksize) m.(DHTL.mod_stk) m.(DHTL.mod_stk_len) sp mem asa)
+    (SP : sp = Values.Vptr sp' (Ptrofs.repr 0))
+    (RSBP : reg_stack_based_pointers sp' rs)
+    (ASBP : arr_stack_based_pointers sp' mem (f.(GiblePar.fn_stacksize)) sp)
+    (BOUNDS : stack_bounds sp (f.(GiblePar.fn_stacksize)) mem)
+    (CONST : match_constants m.(DHTL.mod_reset) m.(DHTL.mod_finish) asr),
+    (* Add a relation about ps compared with the state register. *)
+    match_states_reduced' (GiblePar.State sf f sp st rs ps mem)
+                 (DHTL.State res m n asr asa).
+
+  Lemma step_cf_instr_pc_ind :
+    forall s f sp rs' pr' m' pc pc' cf t state,
+      step_cf_instr ge (GiblePar.State s f sp pc rs' pr' m') cf t state ->
+      step_cf_instr ge (GiblePar.State s f sp pc' rs' pr' m') cf t state.
+  Proof. destruct cf; intros; inv H; econstructor; eauto. Qed.
+
+  Definition mk_ctrl f := {|
+                 ctrl_st := Pos.succ (max_resource_function f);
+                 ctrl_stack := Pos.succ (Pos.succ (Pos.succ (Pos.succ (max_resource_function f))));
+                 ctrl_fin := Pos.succ (Pos.succ (max_resource_function f));
+                 ctrl_return := Pos.succ (Pos.succ (Pos.succ (max_resource_function f)))
+               |}.
+
+  Lemma transl_step_state_correct_instr :
+    forall s f sp bb hw_pc curr_p next_p rs rs' m m' pr pr' m_ s' stmnt stmnt' asr0 asa0 asr asa,
+      (* (fn_code f) ! pc = Some bb -> *)
+      mfold_left (transf_instr (mk_ctrl f)) bb (OK (curr_p, stmnt)) = OK (next_p, stmnt') ->
+      stmnt_runp tt (e_assoc asr0) (e_assoc_arr (DHTL.mod_stk m_) (DHTL.mod_stk_len m_) asa0) stmnt (e_assoc asr) (e_assoc_arr (DHTL.mod_stk m_) (DHTL.mod_stk_len m_) asa) ->
+      eval_predf pr curr_p = true ->
+      ParBB.step_instr_list ge sp (Iexec {| is_rs := rs; is_ps := pr; is_mem := m |}) bb
+             (Iexec {| is_rs := rs'; is_ps := pr'; is_mem := m' |}) ->
+      match_states (GiblePar.State s f sp hw_pc rs pr m) (DHTL.State s' m_ hw_pc asr asa) ->
+      exists asr' asa',
+        stmnt_runp tt (e_assoc asr0) (e_assoc_arr (DHTL.mod_stk m_) (DHTL.mod_stk_len m_) asa0) stmnt' (e_assoc asr') (e_assoc_arr (DHTL.mod_stk m_) (DHTL.mod_stk_len m_) asa')
+        /\ match_states (GiblePar.State s f sp hw_pc rs' pr' m') (DHTL.State s' m_ hw_pc asr' asa').
+  Proof. Admitted.
+
+  Lemma transl_step_state_correct_chained :
+    forall s f sp bb hw_pc curr_p next_p rs rs' m m' pr pr' m_ s' stmnt stmnt' asr0 asa0 asr asa,
+      (* (fn_code f) ! pc = Some bb -> *)
+      mfold_left (transf_chained_block (mk_ctrl f)) bb (OK (curr_p, stmnt)) = OK (next_p, stmnt') ->
+      stmnt_runp tt (e_assoc asr0) (e_assoc_arr (DHTL.mod_stk m_) (DHTL.mod_stk_len m_) asa0) stmnt (e_assoc asr) (e_assoc_arr (DHTL.mod_stk m_) (DHTL.mod_stk_len m_) asa) ->
+      eval_predf pr curr_p = true ->
+      ParBB.step_instr_seq ge sp (Iexec {| is_rs := rs; is_ps := pr; is_mem := m |}) bb
+             (Iexec {| is_rs := rs'; is_ps := pr'; is_mem := m' |}) ->
+      match_states (GiblePar.State s f sp hw_pc rs pr m) (DHTL.State s' m_ hw_pc asr asa) ->
+      exists asr' asa',
+        stmnt_runp tt (e_assoc asr0) (e_assoc_arr (DHTL.mod_stk m_) (DHTL.mod_stk_len m_) asa0) stmnt' (e_assoc asr') (e_assoc_arr (DHTL.mod_stk m_) (DHTL.mod_stk_len m_) asa')
+        /\ match_states (GiblePar.State s f sp hw_pc rs' pr' m') (DHTL.State s' m_ hw_pc asr' asa').
+  Proof. Admitted.
+
+  Lemma one_ne_zero:
+    Int.repr 1 <> Int.repr 0.
+  Proof.
+    unfold not; intros.
+    assert (Int.unsigned (Int.repr 1) = Int.unsigned (Int.repr 0)) by (now rewrite H).
+    rewrite ! Int.unsigned_repr in H0 by crush. lia.
+  Qed.
+
+  Lemma int_and_boolToValue :
+    forall b1 b2,
+      Int.and (boolToValue b1) (boolToValue b2) = boolToValue (b1 && b2).
+  Proof.
+    destruct b1; destruct b2; cbn; unfold boolToValue; unfold natToValue;
+    replace (Z.of_nat 1) with 1 by auto;
+    replace (Z.of_nat 0) with 0 by auto.
+    - apply Int.and_idem.
+    - apply Int.and_zero.
+    - apply Int.and_zero_l.
+    - apply Int.and_zero.
+  Qed.
+
+  Lemma int_or_boolToValue :
+    forall b1 b2,
+      Int.or (boolToValue b1) (boolToValue b2) = boolToValue (b1 || b2).
+  Proof.
+    destruct b1; destruct b2; cbn; unfold boolToValue; unfold natToValue;
+    replace (Z.of_nat 1) with 1 by auto;
+    replace (Z.of_nat 0) with 0 by auto.
+    - apply Int.or_idem.
+    - apply Int.or_zero.
+    - apply Int.or_zero_l.
+    - apply Int.or_zero_l.
+  Qed.
+
+  Lemma translate_pred_correct :
+    forall curr_p pr asr asa,
+      (forall r, Ple r (max_predicate curr_p) ->
+          find_assocmap 1 (pred_enc r) asr = boolToValue (PMap.get r pr)) ->
+      expr_runp tt asr asa (pred_expr curr_p) (boolToValue (eval_predf pr curr_p)).
+  Proof.
+    induction curr_p.
+    - intros * HFRL. cbn. destruct p as [b p']. destruct b.
+      + constructor. eapply HFRL. cbn. unfold Ple. lia.
+      + econstructor. constructor. eapply HFRL. cbn. unfold Ple; lia.
+        econstructor. cbn. f_equal. unfold boolToValue.
+        f_equal. destruct pr !! p' eqn:?. cbn.
+        rewrite Int.eq_false; auto. unfold natToValue.
+        replace (Z.of_nat 1) with 1 by auto. unfold Int.zero.
+        apply one_ne_zero.
+        cbn. rewrite Int.eq_true; auto.
+    - intros. cbn. constructor.
+    - intros. cbn. constructor.
+    - cbn -[eval_predf]; intros. econstructor. eapply IHcurr_p1. intros. eapply H.
+      unfold Ple in *. lia.
+      eapply IHcurr_p2; intros. eapply H. unfold Ple in *; lia.
+      cbn -[eval_predf]. f_equal. symmetry. apply int_and_boolToValue.
+    - cbn -[eval_predf]; intros. econstructor. eapply IHcurr_p1. intros. eapply H.
+      unfold Ple in *. lia.
+      eapply IHcurr_p2; intros. eapply H. unfold Ple in *; lia.
+      cbn -[eval_predf]. f_equal. symmetry. apply int_or_boolToValue.
+  Qed.
+
+  Lemma max_predicate_deep_simplify' :
+    forall peq curr r,
+      (r <= max_predicate (deep_simplify' peq curr))%positive ->
+      (r <= max_predicate curr)%positive.
+  Proof.
+    destruct curr; cbn -[deep_simplify']; auto.
+    - intros. unfold deep_simplify' in H.
+      destruct curr1; destruct curr2; try (destruct_match; cbn in *); lia.
+    - intros. unfold deep_simplify' in H.
+      destruct curr1; destruct curr2; try (destruct_match; cbn in *); lia.
+  Qed.
+
+  Lemma max_predicate_deep_simplify :
+    forall peq curr r,
+      (r <= max_predicate (deep_simplify peq curr))%positive ->
+      (r <= max_predicate curr)%positive.
+  Proof.
+    induction curr; try solve [cbn; auto]; cbn -[deep_simplify'] in *.
+    - intros. apply max_predicate_deep_simplify' in H. cbn -[deep_simplify'] in *.
+      assert (HX: (r <= max_predicate (deep_simplify peq curr1))%positive \/ (r <= max_predicate (deep_simplify peq curr2))%positive) by lia.
+      inv HX; [eapply IHcurr1 in H0 | eapply IHcurr2 in H0]; lia.
+    - intros. apply max_predicate_deep_simplify' in H. cbn -[deep_simplify'] in *.
+      assert (HX: (r <= max_predicate (deep_simplify peq curr1))%positive \/ (r <= max_predicate (deep_simplify peq curr2))%positive) by lia.
+      inv HX; [eapply IHcurr1 in H0 | eapply IHcurr2 in H0]; lia.
+  Qed.
+
+  Lemma translate_cfi_goto:
+    forall pr curr_p pc s ctrl asr asa,
+      (forall r, Ple r (max_predicate curr_p) ->
+        find_assocmap 1 (pred_enc r) asr = boolToValue (PMap.get r pr)) ->
+      eval_predf pr curr_p = true ->
+      translate_cfi ctrl (Some curr_p) (RBgoto pc) = OK s ->
+      stmnt_runp tt (e_assoc asr) asa s
+        (e_assoc (AssocMap.set ctrl.(ctrl_st) (posToValue pc) asr)) asa.
+  Proof.
+    intros * HPLE HEVAL HTRANSL. unfold translate_cfi in *.
+    inversion_clear HTRANSL as []. destruct_match.
+    - constructor. constructor. econstructor. eapply translate_pred_correct.
+      intros. unfold Ple in *. eapply HPLE.
+      now apply max_predicate_deep_simplify in H.
+      eauto. constructor. rewrite eval_predf_deep_simplify. rewrite HEVAL. auto.
+    - repeat constructor.
+  Qed.
+
+  Lemma translate_cfi_goto_none:
+    forall pc s ctrl asr asa,
+      translate_cfi ctrl None (RBgoto pc) = OK s ->
+      stmnt_runp tt (e_assoc asr) asa s
+        (e_assoc (AssocMap.set ctrl.(ctrl_st) (posToValue pc) asr)) asa.
+  Proof. intros; inversion_clear H as []; repeat constructor. Qed.
+
+  Lemma transl_module_ram_none :
+    forall f m_,
+      transl_module f = OK m_ ->
+      m_.(mod_ram) = None.
+  Proof.
+    unfold transl_module, Errors.bind, Errors.bind2, ret; intros.
+    repeat (destruct_match; try discriminate). inversion_clear H as []. auto.
+  Qed.
+
+  Lemma transl_step_state_correct_ :
+    forall s f sp bb hw_pc curr_p d hw_pc' pc_ind next_p d' rs rs' m m' pr pr' state cf m_ s',
+      (* (fn_code f) ! pc = Some bb -> *)
+      mfold_left (transf_parallel_full_block (mk_ctrl f)) bb (OK (hw_pc, curr_p, d)) = OK (hw_pc', next_p, d') ->
+      (forall x y, d' ! x = Some y -> m_.(mod_datapath) ! x = Some y) ->
+      eval_predf pr curr_p = true ->
+      (max_predicate curr_p <= max_pred_function f)%positive ->
+      ParBB.step ge sp (Iexec {| is_rs := rs; is_ps := pr; is_mem := m |}) bb
+             (Iterm {| is_rs := rs'; is_ps := pr'; is_mem := m' |} cf) ->
+      step_cf_instr ge (GiblePar.State s f sp pc_ind rs' pr' m') cf Events.E0 state ->
+      forall asr asa,
+        match_states (GiblePar.State s f sp hw_pc rs pr m) (DHTL.State s' m_ hw_pc asr asa) ->
+        exists R2 : DHTL.state, Smallstep.plus DHTL.step tge (DHTL.State s' m_ hw_pc asr asa) Events.E0 R2
+        /\ match_states state R2.
+  Proof.
+    induction bb.
+    - cbn; intros * HFOLD HSUB HCURR HMAX HPAR HSTEP * HMATCH. inv HPAR.
+    - intros * HFOLD HSUB HCURR HMAX HPAR HSTEP * HMATCH. inv HPAR.
+      + destruct state' as [rs_mid pr_mid m_mid].
+        cbn -[transf_parallel_full_block] in HFOLD.
+        assert (HTRANSF_EX: exists tres, (transf_parallel_full_block
+           (mk_ctrl f) (hw_pc, curr_p, d) a) = OK tres) by admit.
+        inversion_clear HTRANSF_EX as [[[hw_pc_mid curr_p_mid] d_mid] HTRANSF_EX'].
+        rewrite HTRANSF_EX' in HFOLD.
+        unfold transf_parallel_full_block, Errors.bind2,
+               transf_parallel_full_stmnt, Errors.bind in HTRANSF_EX'.
+        repeat (destruct_match; try discriminate; []). inv Heqp0. inv HTRANSF_EX'.
+        exploit translate_cfi_goto. instantiate (2 := asr). admit. eauto. eauto. intros.
+        instantiate (1 := (e_assoc_arr (DHTL.mod_stk m_) (DHTL.mod_stk_len m_) asa)) in H.
+        exploit transl_step_state_correct_chained; eauto. admit.
+        intros (asr' & asa' & HSTMNT & HMATCH').
+        eapply match_states_merge_empty_all in HMATCH'.
+        eapply match_states_merge_empty_all in HMATCH'.
+        exploit IHbb.
+        * eauto.
+        * eauto.
+        * instantiate (1 := pr_mid). admit.
+        * admit.
+        * eauto.
+        * eauto.
+        * eauto.
+        * intros (R2 & HSEMPLUS & HMATCH'').
+          exists R2; split; auto.
+          eapply Smallstep.plus_left'; eauto.
+          2: { symmetry; eapply Events.E0_right. }
+          inv HMATCH. inv CONST. econstructor.
+          eauto. eauto. eauto. inv WF. eapply HSUB.
+          instantiate (1:=s0). admit.
+          unfold e_assoc, e_assoc_arr in HSTMNT. eauto. rewrite transl_module_ram_none with (f := f) by auto.
+          constructor. auto. auto. admit. admit.
+      + admit.
+  Admitted.
+
+  (* Lemma transl_step_state_correct : *)
+  (*   forall s f sp pc rs rs' m m' bb pr pr' t state cf, *)
+  (*     (fn_code f) ! pc = Some bb -> *)
+  (*     ParBB.step ge sp (Iexec {| is_rs := rs; is_ps := pr; is_mem := m |}) bb *)
+  (*            (Iterm {| is_rs := rs'; is_ps := pr'; is_mem := m' |} cf) -> *)
+  (*     step_cf_instr ge (GiblePar.State s f sp pc rs' pr' m') cf t state -> *)
+  (*       forall R1 : DHTL.state, *)
+  (*         match_states (GiblePar.State s f sp pc rs pr m) R1 -> *)
+  (*         exists R2 : DHTL.state, Smallstep.plus DHTL.step tge R1 Events.E0 R2 /\ match_states state R2. *)
+  (* Proof. *)
+  (*   intros * HCODE HPARBB HSTEP R1 HMATCH.  *)
+  (*   exploit step_list_equiv; eauto. intros (pc_final & HSTEPNTH & HBOUND). *)
+  (*   eapply transl_step_state_correct'; eauto. inv HMATCH. *)
+  (*   replace pc with (Pos.of_nat ((Pos.to_nat pc) - O)%nat) at 2 by lia. *)
+  (*   econstructor; eauto. *)
+  (*   now replace (Pos.of_nat ((Pos.to_nat pc) - O)%nat) with pc by lia. *)
+  (* Qed. *)
+
+  Lemma transf_seq_block_in_const :
+    forall d_init pc bb ctrl l d',
+      mfold_left (transf_seq_block ctrl) l (OK d_init) = OK d' ->
+      d_init ! pc = Some bb ->
+      d' ! pc = Some bb.
+  Proof. Admitted.
+
+  Lemma transf_seq_block_in' :
+    forall d_init pc bb ctrl l d',
+      mfold_left (transf_seq_block ctrl) l (OK d_init) = OK d' ->
+      list_norepet (List.map fst l) ->
+      In (pc, bb) l ->
+      exists d_mid d_mid' n' next_p',
+        (mfold_left (transf_parallel_full_block ctrl) bb (OK (pc, Ptrue, d_mid)) = OK (n', next_p', d_mid'))
+        /\ (forall x y, d_mid' ! x = Some y -> d' ! x = Some y).
+  Proof. Admitted.
+
+  Lemma transf_seq_block_in :
+    forall d_init pc bb ctrl d' d,
+      mfold_left (transf_seq_block ctrl) (PTree.elements d) (OK d_init) = OK d' ->
+      d ! pc = Some bb ->
+      exists d_mid d_mid' n' next_p',
+        (mfold_left (transf_parallel_full_block ctrl) bb (OK (pc, Ptrue, d_mid)) = OK (n', next_p', d_mid'))
+        /\ (forall x y, d_mid' ! x = Some y -> d' ! x = Some y).
+  Proof. 
+    intros. eapply transf_seq_block_in'; eauto.
+    apply PTree.elements_keys_norepet.
+    apply PTree.elements_correct; eassumption.
+  Qed.
+
+  Lemma transl_step_state_correct :
+    forall s f sp pc rs rs' m m' bb pr pr' state cf,
+      (fn_code f) ! pc = Some bb ->
+      ParBB.step ge sp (Iexec {| is_rs := rs; is_ps := pr; is_mem := m |}) bb
+             (Iterm {| is_rs := rs'; is_ps := pr'; is_mem := m' |} cf) ->
+      step_cf_instr ge (GiblePar.State s f sp pc rs' pr' m') cf Events.E0 state ->
+        forall R1 : DHTL.state,
+          match_states (GiblePar.State s f sp pc rs pr m) R1 ->
+          exists R2 : DHTL.state, Smallstep.plus DHTL.step tge R1 Events.E0 R2 /\ match_states state R2.
+  Proof.
+    intros * HCODE HPARBB HSTEP R1 HMATCH.
+    inversion HMATCH. unfold transl_module, Errors.bind, ret in *.
+    repeat (destruct_match; try discriminate; []). inv TF.
+    exploit transf_seq_block_in; eauto.
+    intros (d_mid & d_mid' & n' & next_p' & HFOLD & HIN).
+    eapply transl_step_state_correct_; eauto.
+    cbn; lia.
+  Qed.
+
+  Lemma transl_step_state_correct_final :
+    forall s f sp pc rs rs' m m' bb pr pr' state cf t,
+      (fn_code f) ! pc = Some bb ->
+      ParBB.step ge sp (Iexec {| is_rs := rs; is_ps := pr; is_mem := m |}) bb
+             (Iterm {| is_rs := rs'; is_ps := pr'; is_mem := m' |} cf) ->
+      step_cf_instr ge (GiblePar.State s f sp pc rs' pr' m') cf t state ->
+        forall R1 : DHTL.state,
+          match_states (GiblePar.State s f sp pc rs pr m) R1 ->
+          exists R2 : DHTL.state, Smallstep.plus DHTL.step tge R1 t R2 /\ match_states state R2.
+  Proof. Admitted.
+
   Theorem transl_step_correct:
     forall (S1 : GiblePar.state) t S2,
       GiblePar.step ge S1 t S2 ->
@@ -1295,8 +1767,7 @@ Opaque Mem.alloc.
         exists R2, Smallstep.plus DHTL.step tge R1 t R2 /\ match_states S2 R2.
   Proof.
     induction 1.
-    - inversion 1; subst. unfold transl_module, Errors.bind, Errors.bind2, ret in *. 
-    repeat (destruct_match; try discriminate; []). inv TF. cbn in *.
+    - now (eapply transl_step_state_correct_final; eauto).
     - now apply transl_callstate_correct.
     - inversion 1.
     - now apply transl_returnstate_correct.
@@ -1309,5 +1780,5 @@ Opaque Mem.alloc.
     eapply Smallstep.forward_simulation_plus; eauto with htlproof.
     apply senv_preserved.
   Qed.
-    
+
 End CORRECTNESS.