Fix many more lemmas

4 files changed, 329 insertions, 109 deletions

diff --git a/src/hls/CondElim.v b/src/hls/CondElim.v
index b9bd1e9..9f51053 100644
--- a/src/hls/CondElim.v
+++ b/src/hls/CondElim.v
@@ -28,6 +28,8 @@ Require Import vericert.hls.GibleSeq.
 Require Import vericert.hls.Predicate.
 Require Import vericert.bourdoncle.Bourdoncle.
 
+#[local] Open Scope positive.
+
 Definition elim_cond_s (fresh: predicate) (i: instr) :=
   match i with
   | RBexit p (RBcond c args n1 n2) =>
@@ -61,7 +63,7 @@ Definition elim_cond_fold (state: predicate * PTree.t SeqBB.t) (n: node) (b: Seq
 
 Definition transf_function (f: function) : function :=
   mkfunction f.(fn_sig) f.(fn_params) f.(fn_stacksize)
-             (snd (PTree.fold elim_cond_fold f.(fn_code) (1%positive, PTree.empty _)))
+             (snd (PTree.fold elim_cond_fold f.(fn_code) (max_pred_function f + 1, PTree.empty _)))
              f.(fn_entrypoint).
 
 Definition transf_fundef (fd: fundef) : fundef :=
diff --git a/src/hls/CondElimproof.v b/src/hls/CondElimproof.v
index ecc3538..8b2ce48 100644
--- a/src/hls/CondElimproof.v
+++ b/src/hls/CondElimproof.v
@@ -42,38 +42,53 @@ Require Import vericert.hls.Predicate.
 
 #[local] Open Scope positive.
 
-Lemma cf_in_step :
-  forall A B ge sp is_ is_' bb cf,
-    @SeqBB.step A B ge sp (Iexec is_) bb (Iterm is_' cf) ->
-    exists p, In (RBexit p cf) bb
-              /\ Option.default true (Option.map (eval_predf (is_ps is_')) p) = true.
-  Proof. Admitted.
-
 Lemma forbidden_term_trans :
   forall A B ge sp i c b i' c',
     ~ @SeqBB.step A B ge sp (Iterm i c) b (Iterm i' c').
 Proof. induction b; unfold not; intros; inv H. Qed.
 
-Lemma random1 :
-  forall A B ge sp is_ b is_' cf,
-    @SeqBB.step A B ge sp (Iexec is_) b (Iterm is_' cf) ->
-    exists p b', SeqBB.step ge sp (Iexec is_) (b' ++ (RBexit p cf) :: nil) (Iterm is_' cf)
-                 /\ Forall2 eq (b' ++ (RBexit p cf) :: nil) b.
+Lemma step_instr_false :
+  forall A B ge sp i c a i0,
+    ~ @step_instr A B ge sp (Iterm i c) a (Iexec i0).
+Proof. destruct a; unfold not; intros; inv H. Qed.
+
+Lemma step_list2_false :
+  forall A B ge l0 sp i c i0',
+    ~ step_list2 (@step_instr A B ge) sp (Iterm i c) l0 (Iexec i0').
 Proof.
-Admitted.
+  induction l0; unfold not; intros.
+  inv H. inv H. destruct i1. eapply step_instr_false in H4. auto.
+  eapply IHl0; eauto.
+Qed.
+
+Lemma append' :
+  forall A B l0 cf i0 i1 l1 sp ge i0',
+    step_list2 (@step_instr A B ge) sp (Iexec i0) l0 (Iexec i0') ->
+    @SeqBB.step A B ge sp (Iexec i0') l1 (Iterm i1 cf) ->
+    @SeqBB.step A B ge sp (Iexec i0) (l0 ++ l1) (Iterm i1 cf).
+Proof.
+  induction l0; crush. inv H. eauto. inv H. destruct i3.
+  econstructor; eauto. eapply IHl0; eauto.
+  eapply step_list2_false in H7. exfalso; auto.
+Qed.
 
 Lemma append :
   forall A B cf i0 i1 l0 l1 sp ge,
       (exists i0', step_list2 (@step_instr A B ge) sp (Iexec i0) l0 (Iexec i0') /\
                     @SeqBB.step A B ge sp (Iexec i0') l1 (Iterm i1 cf)) ->
     @SeqBB.step A B ge sp (Iexec i0) (l0 ++ l1) (Iterm i1 cf).
-Proof. Admitted.
+Proof. intros. simplify. eapply append'; eauto. Qed.
 
 Lemma append2 :
-  forall A B cf i0 i1 l0 l1 sp ge,
+  forall A B l0 cf i0 i1 l1 sp ge,
     @SeqBB.step A B ge sp (Iexec i0) l0 (Iterm i1 cf) ->
     @SeqBB.step A B ge sp (Iexec i0) (l0 ++ l1) (Iterm i1 cf).
-Proof. Admitted.
+Proof.
+  induction l0; crush.
+  inv H.
+  inv H. econstructor; eauto. eapply IHl0; eauto.
+  constructor; auto.
+Qed.
 
 Definition to_cf c :=
   match c with | Iterm _ cf => Some cf | _ => None end.
@@ -89,7 +104,7 @@ Variant match_ps : positive -> predset -> predset -> Prop :=
 Lemma eval_pred_under_match:
   forall rs m rs' m' ps tps tps' ps' v p1 rs'' ps'' m'',
     eval_pred (Some p1) (mki rs ps m) (mki rs' ps' m') (mki rs'' ps'' m'') ->
-    max_predicate p1 <= v ->
+    (forall p, In p (predicate_use p1) -> p <= v) ->
     match_ps v ps tps ->
     match_ps v ps' tps' ->
     exists tps'',
@@ -105,10 +120,22 @@ Lemma eval_pred_eq_predset :
     ps' = ps.
 Proof. inversion 1; subst; crush. Qed.
 
+Lemma predicate_lt :
+  forall p p0,
+    In p0 (predicate_use p) -> p0 <= max_predicate p.
+Proof.
+  induction p; crush.
+  - destruct_match. inv H; try lia; contradiction.
+  - eapply Pos.max_le_iff.
+    eapply in_app_or in H. inv H; eauto.
+  - eapply Pos.max_le_iff.
+    eapply in_app_or in H. inv H; eauto.
+Qed.
+
 Lemma elim_cond_s_spec :
   forall A B ge sp rs m rs' m' ps tps ps' p a p0 l v,
     step_instr ge sp (Iexec (mki rs ps m)) a (Iexec (mki rs' ps' m')) ->
-    max_pred_instr v a <= v ->
+    (forall p, In p (pred_uses a) -> p <= v) ->
     match_ps v ps tps ->
     elim_cond_s p a = (p0, l) ->
     exists tps',
@@ -136,14 +163,14 @@ Proof.
     + inv H18. econstructor. split. econstructor. econstructor; eauto. constructor; eauto.
       constructor. auto.
   - inv H2. destruct p'.
-    exploit eval_pred_under_match; eauto. lia. Admitted.
+    exploit eval_pred_under_match; eauto. Admitted.
 
 Definition wf_predicate (v: predicate) (p: predicate) := v < p.
 
 Lemma eval_predf_match_ps :
   forall p p' p0 v,
     match_ps v p p' ->
-    max_predicate p0 <= v ->
+    Forall (fun x => x <= v) (predicate_use p0) ->
     eval_predf p p0 = eval_predf p' p0.
   Admitted.
 
@@ -162,7 +189,8 @@ Proof. inversion 1; subst; simplify; econstructor; eauto. Qed.
 Variant match_stackframe : stackframe -> stackframe -> Prop :=
   | match_stackframe_init :
     forall res f tf sp pc rs p p'
-           (TF: transf_function f = tf),
+           (TF: transf_function f = tf)
+           (PS: match_ps (max_pred_function f) p p'),
       match_stackframe (Stackframe res f sp pc rs p) (Stackframe res tf sp pc rs p').
 
 Variant match_states : state -> state -> Prop :=
@@ -208,7 +236,7 @@ Qed.
 Lemma eval_predf_in_ps :
   forall v ps ps' p1 b p tps,
     eval_predf ps p1 = true ->
-    max_predicate p1 <= v ->
+    Forall (fun x => x <= v) (predicate_use p1) ->
     wf_predicate v p ->
     match_ps v ps ps' ->
     eval_predf tps # p <- b (Pand (Plit (b, p)) p1) = true.
@@ -217,7 +245,7 @@ Admitted.
 Lemma eval_predf_in_ps2 :
   forall v ps ps' p1 b b' p tps,
     eval_predf ps p1 = true ->
-    max_predicate p1 <= v ->
+    Forall (fun x => x <= v) (predicate_use p1) ->
     wf_predicate v p ->
     match_ps v ps ps' ->
     b <> b' ->
@@ -235,13 +263,6 @@ Proof.
   rewrite PMap.gso; auto; lia.
 Qed.
 
-Lemma transf_block_spec :
-  forall f pc b,
-    f.(fn_code) ! pc = Some b ->
-    exists p,
-      (transf_function f).(fn_code) ! pc
-      = Some (snd (replace_section elim_cond_s p b)). Admitted.
-
 Definition match_prog (p: program) (tp: program) :=
   Linking.match_program (fun cu f tf => tf = transf_fundef f) eq p tp.
 
@@ -325,52 +346,6 @@ Section CORRECTNESS.
     inversion 2; crush. subst. inv H. inv STK. econstructor.
   Qed.
 
-  Lemma elim_cond_s_spec2 :
-    forall rs m rs' m' ps tps ps' p a p0 l v cf stk f sp pc t st,
-      step_instr ge sp (Iexec (mki rs ps m)) a (Iterm (mki rs' ps' m') cf) ->
-      step_cf_instr ge (State stk f sp pc rs' ps' m') cf t st ->
-      max_pred_instr v a <= v ->
-      match_ps v ps tps ->
-      wf_predicate v p ->
-      elim_cond_s p a = (p0, l) ->
-      exists tps' cf' st',
-        SeqBB.step tge sp (Iexec (mki rs tps m)) l (Iterm (mki rs' tps' m') cf')
-        /\ match_ps v ps' tps'
-        /\ step_cf_instr tge (State stk f sp pc rs' tps' m') cf' t st'
-        /\ match_states st st'.
-  Proof.
-    inversion 1; subst; simplify.
-    - destruct (eval_predf ps p1) eqn:?; [|discriminate]. inv H2.
-      destruct cf; inv H5;
-        try (do 3 econstructor; simplify;
-             [ constructor; apply step_instr_inv_exit; erewrite <- eval_predf_match_ps; eauto; lia
-             | auto
-             | eauto using step_cf_instr_ps_idem
-             | assert (ps' = ps'') by (eauto using step_cf_instr_ps_const); subst; auto ]).
-      do 3 econstructor; simplify.
-      constructor; apply step_instr_inv_exit; erewrite <- eval_predf_match_ps; eauto; lia.
-      auto.
-      (*inv H0; destruct b.
-      + do 3 econstructor; simplify.
-        econstructor. econstructor; eauto. eapply eval_pred_true.
-        erewrite <- eval_predf_match_ps; eauto. simpl. lia.
-        constructor. apply step_instr_inv_exit. simpl.
-        eapply eval_predf_in_ps; eauto. lia.
-        apply match_ps_set_gt; auto.
-        constructor; auto.
-        apply match_ps_set_gt; auto.
-      + do 3 econstructor; simplify.
-        econstructor. econstructor; eauto. eapply eval_pred_true.
-        erewrite <- eval_predf_match_ps; eauto. simpl. lia.
-        econstructor. apply step_instr_inv_exit2. simpl.
-        eapply eval_predf_in_ps2; eauto. lia.
-        constructor. apply step_instr_inv_exit. simpl.
-        eapply eval_predf_in_ps; eauto; lia.
-        apply match_ps_set_gt; auto.
-        constructor; auto.
-        apply match_ps_set_gt; auto.
-    -*) Admitted.
-
   Lemma eval_op_eq:
     forall (sp0 : Values.val) (op : Op.operation) (vl : list Values.val) m,
       Op.eval_operation ge sp0 op vl m = Op.eval_operation tge sp0 op vl m.
@@ -401,21 +376,35 @@ Section CORRECTNESS.
       try (rewrite <- eval_op_eq; auto); rewrite <- eval_addressing_eq; auto.
   Qed.
 
+  #[local] Hint Resolve eval_builtin_args_preserved : core.
+  #[local] Hint Resolve symbols_preserved : core.
+  #[local] Hint Resolve external_call_symbols_preserved : core.
+  #[local] Hint Resolve senv_preserved : core.
+  #[local] Hint Resolve find_function_translated : core.
+  #[local] Hint Resolve sig_transf_function : core.
+
   Lemma step_cf_instr_ge :
     forall st cf t st' tst,
       step_cf_instr ge st cf t st' ->
       match_states st tst ->
       exists tst', step_cf_instr tge tst cf t tst' /\ match_states st' tst'.
-  Proof.
+  Proof using TRANSL.
+    inversion 1; subst; simplify; clear H;
+      match goal with H: context[match_states] |- _ => inv H end;
+      repeat (econstructor; eauto).
+  Qed.
+
+  Lemma step_cf_instr_det :
+    forall ge st cf t st1 st2,
+      step_cf_instr ge st cf t st1 ->
+      step_cf_instr ge st cf t st2 ->
+      st1 = st2.
+  Proof using TRANSL.
     inversion 1; subst; simplify; clear H;
-      match goal with H: context[match_states] |- _ => inv H end.
-    - do 2 econstructor. rewrite <- sig_transf_function. econstructor; eauto.
-      eauto using find_function_translated. auto.
-      econstructor; auto. repeat (constructor; auto).
-    - do 2 econstructor. econstructor. eauto using find_function_translated.
-      eauto using sig_transf_function. eauto.
-      econstructor; auto.
-    - do 2 econstructor.
+      match goal with H: context[step_cf_instr] |- _ => inv H end; crush;
+    assert (vargs0 = vargs) by eauto using eval_builtin_args_determ; subst;
+    assert (vres = vres0 /\ m' = m'0) by eauto using external_call_deterministic; crush.
+  Qed.
 
   Lemma step_list2_ge :
     forall sp l i i',
@@ -438,33 +427,233 @@ Section CORRECTNESS.
     - eauto using exec_RBterm, step_instr_ge.
   Qed.
 
+  Lemma max_pred_function_use :
+    forall f pc bb i p,
+      f.(fn_code) ! pc = Some bb ->
+      In i bb ->
+      In p (pred_uses i) ->
+      p <= max_pred_function f.
+  Proof. Admitted.
+
+  Lemma elim_cond_s_wf_predicate :
+    forall a p p0 l v,
+      elim_cond_s p a = (p0, l) ->
+      wf_predicate v p ->
+      wf_predicate v p0.
+  Proof using.
+    destruct a; simplify; try match goal with H: (_, _) = (_, _) |- _ => inv H end; auto.
+    destruct c; simplify; try match goal with H: (_, _) = (_, _) |- _ => inv H end; auto.
+    unfold wf_predicate in *; lia.
+  Qed.
+
+  Lemma replace_section_wf_predicate :
+    forall bb v p t0 p0,
+      replace_section elim_cond_s p bb = (p0, t0) ->
+      wf_predicate v p ->
+      wf_predicate v p0.
+  Proof using.
+    induction bb; crush; repeat (destruct_match; crush).
+    inv H.
+    exploit IHbb; eauto; simplify.
+    eapply elim_cond_s_wf_predicate in Heqp2; eauto.
+  Qed.
+
+  Lemma elim_cond_s_spec2 :
+    forall rs m rs' m' ps tps ps' p a p0 l cf stk f sp pc t st tstk,
+      step_instr ge sp (Iexec (mki rs ps m)) a (Iterm (mki rs' ps' m') cf) ->
+      step_cf_instr ge (State stk f sp pc rs' ps' m') cf t st ->
+      Forall (fun p => p <= (max_pred_function f)) (pred_uses a) ->
+      match_ps (max_pred_function f) ps tps ->
+      wf_predicate (max_pred_function f) p ->
+      elim_cond_s p a = (p0, l) ->
+      Forall2 match_stackframe stk tstk ->
+      exists tps' cf' st',
+        SeqBB.step tge sp (Iexec (mki rs tps m)) l (Iterm (mki rs' tps' m') cf')
+        /\ match_ps (max_pred_function f) ps' tps'
+        /\ step_cf_instr tge (State tstk (transf_function f) sp pc rs' tps' m') cf' t st'
+        /\ match_states st st'.
+  Proof using TRANSL.
+    inversion 1; subst; simplify.
+    - destruct (eval_predf ps p1) eqn:?; [|discriminate]. inv H2.
+      destruct cf; inv H5;
+        try (exploit step_cf_instr_ge; eauto; econstructor; eauto; simplify;
+             do 3 econstructor; simplify;
+             [ constructor; apply step_instr_inv_exit; erewrite <- eval_predf_match_ps | | | ]);
+        eauto using step_cf_instr_ps_idem.
+      inv H0; destruct b.
+      + do 3 econstructor; simplify.
+        econstructor. econstructor; eauto. eapply eval_pred_true.
+        erewrite <- eval_predf_match_ps; eauto. simpl.
+        constructor. apply step_instr_inv_exit. simpl.
+        eapply eval_predf_in_ps; eauto.
+        apply match_ps_set_gt; auto.
+        constructor; auto.
+        constructor; auto.
+        apply match_ps_set_gt; auto.
+      + do 3 econstructor; simplify.
+        econstructor. econstructor; eauto. eapply eval_pred_true.
+        erewrite <- eval_predf_match_ps; eauto.
+        econstructor. apply step_instr_inv_exit2. simpl.
+        eapply eval_predf_in_ps2; eauto.
+        constructor. apply step_instr_inv_exit. simpl.
+        eapply eval_predf_in_ps; eauto.
+        apply match_ps_set_gt; auto.
+        constructor; auto.
+        constructor; auto.
+        apply match_ps_set_gt; auto.
+    - destruct cf; inv H4; exploit step_cf_instr_ge; eauto; try solve [econstructor; eauto]; simplify;
+        try (do 3 econstructor; simplify; eauto; eapply exec_RBterm; econstructor; eauto).
+      inv H0. destruct b.
+      + do 3 econstructor; simplify.
+        econstructor. econstructor; eauto. constructor.
+        constructor. apply step_instr_inv_exit. simplify.
+        unfold eval_predf. simplify. rewrite Pos2Nat.id. apply PMap.gss.
+        apply match_ps_set_gt; auto.
+        constructor; auto.
+        constructor; auto.
+        apply match_ps_set_gt; auto.
+      + do 3 econstructor; simplify.
+        econstructor. econstructor; eauto. constructor.
+        econstructor. apply step_instr_inv_exit2. simpl.
+        unfold eval_predf. simplify. rewrite Pos2Nat.id. apply PMap.gss.
+        constructor. apply step_instr_inv_exit. simpl.
+        unfold eval_predf. simplify. rewrite Pos2Nat.id. rewrite PMap.gss. auto.
+        apply match_ps_set_gt; auto.
+        constructor; auto.
+        constructor; auto.
+        apply match_ps_set_gt; auto.
+  Qed.
+
   Lemma replace_section_spec :
-    forall sp bb rs ps m rs' ps' m' stk f t cf pc tps v n p p' bb' st st',
+    forall sp bb rs ps m rs' ps' m' stk f t cf pc tps p p' bb' st tstk,
       SeqBB.step ge sp (Iexec (mki rs ps m)) bb (Iterm (mki rs' ps' m') cf) ->
       step_cf_instr ge (State stk f sp pc rs' ps' m') cf t st ->
-      match_ps v ps tps ->
-      max_pred_block v n bb <= v ->
+      match_ps (max_pred_function f) ps tps ->
+      (forall p i, In i bb -> In p (pred_uses i) -> p <= max_pred_function f) ->
+      wf_predicate (max_pred_function f) p ->
       replace_section elim_cond_s p bb = (p', bb') ->
-      exists tps' cf',
+      Forall2 match_stackframe stk tstk ->
+      exists st' tps' cf',
         SeqBB.step tge sp (Iexec (mki rs tps m)) bb' (Iterm (mki rs' tps' m') cf')
-        /\ match_ps v ps' tps'
-        /\ step_cf_instr tge (State stk f sp pc rs' tps' m') cf' t st'
+        /\ match_ps (max_pred_function f) ps' tps'
+        /\ step_cf_instr tge (State tstk (transf_function f) sp pc rs' tps' m') cf' t st'
         /\ match_states st st'.
-  Proof.
+  Proof using TRANSL.
     induction bb; simplify; inv H.
-    - destruct state'. repeat destruct_match. inv H3.
-      exploit elim_cond_s_spec; eauto. admit. simplify.
-      exploit IHbb; eauto; simplify. admit.
-      do 2 econstructor. simplify.
+    - destruct state'. repeat destruct_match. inv H4.
+      exploit elim_cond_s_spec; eauto. simplify.
+      exploit IHbb; eauto; simplify.
+      do 3 econstructor. simplify.
       eapply append. econstructor; simplify.
       eapply step_list2_ge; eauto. eauto.
       eauto. eauto. eauto.
-    - repeat destruct_match; simplify. inv H3.
-      exploit elim_cond_s_spec2; eauto. admit. admit. simplify.
-      do 3 econstructor; simplify; eauto.
-      eapply append2; eauto using step_list2_ge.
-      Unshelve. exact 1.
-  Admitted.
+    - repeat destruct_match; simplify. inv H4.
+      exploit elim_cond_s_spec2. 6: { eauto. } eauto. eauto.
+      apply Forall_forall. eauto. eauto.
+      eapply replace_section_wf_predicate; eauto. eauto.
+      simplify.
+      exploit step_cf_instr_ge; eauto. constructor; eauto. simplify.
+      exists x1. eexists. exists x0. simplify.
+      eapply append2. eauto using step_list_ge. auto. auto. auto.
+  Qed.
+
+  Definition lt_pred (c: code) (m: positive) :=
+    forall pc bb n,
+      c ! pc = Some bb ->
+      m = max_pred_block m n bb \/ m < max_pred_block 1 n bb.
+
+  Definition lt_pred2 (c: code) (m: positive) :=
+    forall pc bb n,
+      c ! pc = Some bb ->
+      max_pred_block 1 n bb <= m.
+
+  (* Lemma max_pred_block_lt: *)
+  (*   forall v v0 n b k, *)
+  (*     v0 <= b -> *)
+  (*     max_pred_block v0 n v <= max_pred_block b k v. *)
+  (*   Proof. Admitted. *)
+
+  (* Lemma max_block_pred : *)
+  (*   forall f, lt_pred f.(fn_code) (max_pred_function f). *)
+  (* Proof. *)
+  (*   unfold max_pred_function; intros. *)
+  (*   eapply PTree_Properties.fold_ind; unfold lt_pred; intros. *)
+  (*   destruct (max_pred_block 1 n bb); crush. *)
+  (*   destruct (peq pc k); subst; simplify. *)
+  (*   - assert (v0 <= a \/ a < v0) by admit. *)
+  (*     inv H3. left. eapply max_pred_block_lt; eauto. *)
+  (*     right. *)
+  (*     Abort. *)
+
+  Lemma elim_cond_s_lt :
+    forall p a p0 l x,
+      elim_cond_s p a = (p0, l) ->
+      p0 <= x ->
+      p <= x.
+  Proof using.
+    destruct a; crush; destruct c; crush.
+    inv H. lia.
+  Qed.
+
+  Lemma replace_section_lt :
+    forall t p1 p0 t2 x,
+      replace_section elim_cond_s p1 t = (p0, t2) ->
+      p0 <= x ->
+      p1 <= x.
+  Proof using.
+    induction t; crush; repeat destruct_match. inv H.
+    eapply IHt; eauto.
+    eapply elim_cond_s_lt; eauto.
+  Qed.
+
+  Lemma pred_not_in :
+    forall l pc p t p' t' x,
+      ~ In pc (map fst l) ->
+      fold_left (fun a p => elim_cond_fold a (fst p) (snd p)) l (p, t) = (p', t') ->
+      t ! pc = x -> t' ! pc = x.
+  Proof using.
+    induction l; crush.
+    repeat destruct_match.
+    eapply IHl; eauto. rewrite PTree.gso; auto.
+  Qed.
+
+  Lemma pred_greater :
+    forall l pc x v p' t',
+      In (pc, x) l ->
+      list_norepet (map fst l) ->
+      fold_left (fun a p => elim_cond_fold a (fst p) (snd p)) l v = (p', t') ->
+      exists p, t' ! pc = Some (snd (replace_section elim_cond_s p x))
+                /\ (fst v) <= p.
+  Proof.
+    induction l; crush.
+    inv H0. destruct a; simplify. inv H. inv H0.
+    remember (elim_cond_fold v pc x). destruct p.
+    eapply pred_not_in in H1; eauto. symmetry in Heqp.
+    unfold elim_cond_fold in Heqp. repeat destruct_match. inv Heqp0. inv Heqp.
+    simplify. econstructor. split. rewrite PTree.gss in H1.
+    rewrite Heqp1. eauto. lia.
+    remember (elim_cond_fold v p t). destruct p0. symmetry in Heqp0.
+    unfold elim_cond_fold in Heqp0. repeat destruct_match. inv Heqp0.
+    exploit IHl; eauto; simplify.
+    econstructor; simplify. eauto.
+    eapply replace_section_lt; eauto.
+  Qed.
+
+  Lemma transf_block_spec :
+    forall f pc x,
+      f.(fn_code) ! pc = Some x ->
+      forall p' t',
+        PTree.fold elim_cond_fold f.(fn_code) (max_pred_function f + 1, PTree.empty _) = (p', t') ->
+        exists p,
+          t' ! pc = Some (snd (replace_section elim_cond_s p x)) /\ max_pred_function f + 1 <= p.
+  Proof using.
+    intros.
+    replace (max_pred_function f + 1) with (fst (max_pred_function f + 1, PTree.empty SeqBB.t)); auto.
+    eapply pred_greater.
+    eapply PTree.elements_correct; eauto.
+    apply PTree.elements_keys_norepet.
+    rewrite <- PTree.fold_spec. eauto.
+  Qed.
 
   Lemma transf_step_correct:
     forall (s1 : state) (t : trace) (s1' : state),
@@ -472,12 +661,23 @@ Section CORRECTNESS.
       forall s2 : state,
         match_states s1 s2 ->
         exists s2' : state, step tge s2 t s2' /\ match_states s1' s2'.
-  Proof.
+  Proof using TRANSL.
     induction 1; intros.
-    + inv H2. eapply cf_in_step in H0; simplify.
-      exploit transf_block_spec; eauto; simplify.
-      do 2 econstructor. econstructor; eauto.
-      simplify. Admitted.
+    + inv H2.
+      exploit transf_block_spec; eauto.
+      assert (X: forall A B (a: A * B), a = (fst a, snd a)).
+      { destruct a; auto. } eapply X. simplify.
+      remember (replace_section elim_cond_s x bb). destruct p. symmetry in Heqp.
+      exploit replace_section_spec; eauto.
+      solve [eauto using max_pred_function_use].
+      unfold wf_predicate. lia.
+      simplify. econstructor.
+      simplify. econstructor; eauto. auto.
+    + inv H0. econstructor.
+      simplify. econstructor; eauto. constructor; eauto. constructor. auto.
+    + inv H0. do 3 econstructor; eauto.
+    + inv H. inv STK. inv H1. do 3 econstructor; eauto.
+  Qed.
 
   Theorem transf_program_correct:
     forward_simulation (semantics prog) (semantics tprog).
@@ -489,5 +689,4 @@ Section CORRECTNESS.
     + apply transf_step_correct.
   Qed.
 
-
 End CORRECTNESS.
diff --git a/src/hls/Gible.v b/src/hls/Gible.v
index e50fdc0..c51b250 100644
--- a/src/hls/Gible.v
+++ b/src/hls/Gible.v
@@ -613,4 +613,14 @@ type ~genv~ which was declared earlier.
                end
             ) b nil.
 
+    Definition pred_uses i :=
+      match i with
+      | RBop (Some p) _ _ _
+      | RBload (Some p) _ _ _ _
+      | RBstore (Some p) _ _ _ _
+      | RBexit (Some p) _ => predicate_use p
+      | RBsetpred (Some p) _ _ p' => p' :: predicate_use p
+      | _ => nil
+      end.
+
 End Gible.
diff --git a/src/hls/Predicate.v b/src/hls/Predicate.v
index 087b119..7a4ed60 100644
--- a/src/hls/Predicate.v
+++ b/src/hls/Predicate.v
@@ -508,6 +508,15 @@ Fixpoint max_predicate (p: pred_op) : positive :=
   | Por a b => Pos.max (max_predicate a) (max_predicate b)
   end.
 
+Fixpoint predicate_use (p: pred_op) : list positive :=
+  match p with
+  | Plit (b, p) => p :: nil
+  | Ptrue => nil
+  | Pfalse => nil
+  | Pand a b => predicate_use a ++ predicate_use b
+  | Por a b => predicate_use a ++ predicate_use b
+  end.
+
 Definition tseytin (p: pred_op) :
   {fm: formula | forall a,
       sat_predicate p a = true <-> satFormula fm a}.