Add incremental evaluability check

6 files changed, 1127 insertions, 11 deletions

diff --git a/debug/vericertTest.ml b/debug/vericertTest.ml
index 48391db..87c9e60 100644
--- a/debug/vericertTest.ml
+++ b/debug/vericertTest.ml
@@ -26,7 +26,12 @@ let schedule_oracle l bb bbt =
        let (p2, m_expr_t) = p1 in
        let (bbt', reg_expr_t) = p2 in
        printf "F1:\n%a\n" PrintAbstr.print_forest bb';
-       printf "F2:\n%a\n" PrintAbstr.print_forest bbt'; flush stdout;
+       printf "%a\n" PrintAbstr.print_evaluability_list reg_expr;
+       printf "%a\n" PrintAbstr.print_evaluability_list2 m_expr;
+       printf "F2:\n%a\n" PrintAbstr.print_forest bbt';
+       printf "%a\n" PrintAbstr.print_evaluability_list reg_expr_t;
+       printf "%a\n" PrintAbstr.print_evaluability_list2 m_expr_t;
+       flush stdout;
        (&&)
          ((&&) ((&&) (if check l bb' bbt' then true else (Printf.printf "Failed 1\n"; false)) (empty_trees bb bbt))
            (if (check_evaluability1 reg_expr reg_expr_t) then true else (Printf.printf "Failed 12\n"; false)))
@@ -179,12 +184,12 @@ let () =
          seteq None 2 12 13;
          add None 2 1 4;
          mul (Some (Pand (plit false 1, plit false 2))) 3 1 1;
-         mul (Some (Pand (plit false 1, plit false 2))) 5 3 3;
+         mul (Some (Pand (plit false 1, plit false 2))) 3 3 3;
          goto (Some (Pand (plit false 1, plit false 2))) 10;
          mul (Some (Pand (plit false 1, plit true 2))) 3 1 4;
          goto (Some (Pand (plit false 1, plit true 2))) 10;
          add (Some (plit true 1)) 1 2 4;
-         mul (Some (Pand (plit true 1, plit false 2))) 5 3 3;
+         mul (Some (Pand (plit true 1, plit false 2))) 3 3 3;
          goto (Some (Pand (plit true 1, plit false 2))) 10;
          mul (Some (Pand (plit true 1, plit true 2))) 3 1 4;
          goto (Some (Pand (plit true 1, plit true 2))) 10;
@@ -197,8 +202,8 @@ let () =
              add (Some (plit true 1)) 1 2 4;
              mul (Some (Pand (plit false 1, plit true 2))) 3 1 4;
              mul (Some (Pand (plit true 1, plit true 2))) 3 1 4;
-             mul (Some (Pand (plit false 1, plit false 2))) 5 3 3;
-             mul (Some (Pand (plit true 1, plit false 2))) 5 3 3;
+             mul (Some (Pand (plit false 1, plit false 2))) 3 3 3;
+             mul (Some (Pand (plit true 1, plit false 2))) 3 3 3;
              goto None 10;
        ] ] ]
   then Printf.printf "Passed 110\n"
diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v
index 0a83f02..f78b0bd 100644
--- a/src/extraction/Extraction.v
+++ b/src/extraction/Extraction.v
@@ -210,6 +210,7 @@ Separate Extraction
          Bourdoncle.bourdoncle
 
    Smtpredicate.check_smt_total
+   GiblePargen.abstract_sequence_top_inc
 
    Compiler.transf_c_program Compiler.transf_cminor_program
    Cexec.do_initial_state Cexec.do_step Cexec.at_final_state
diff --git a/src/hls/GiblePargen.v b/src/hls/GiblePargen.v
index 4095977..7dd1c97 100644
--- a/src/hls/GiblePargen.v
+++ b/src/hls/GiblePargen.v
@@ -347,13 +347,13 @@ Definition remember_expr_inc (fop : pred_op * forest) (lst: list (resource * pre
   let (pred, f) := fop in
   match i with
   | RBnop => lst
-  | RBop p op rl r => (Reg r, (NE.map (fun x => (dfltp p ∧ pred ∧ fst x, snd x))
-        (seq_app (pred_ret (Eop op)) (merge (list_translation rl f))))) :: lst
-  | RBload p chunk addr rl r => (Reg r, (NE.map (fun x => (dfltp p ∧ pred ∧ fst x, snd x))
+  | RBop p op rl r => (Reg r, (app_predicated (dfltp p ∧ pred) (NE.singleton (Ptrue, Ebase (Reg 1))) (
+        (seq_app (pred_ret (Eop op)) (merge (list_translation rl f)))))) :: lst
+  | RBload p chunk addr rl r => (Reg r, (app_predicated (dfltp p ∧ pred) (NE.singleton (Ptrue, Ebase (Reg 1))) (
         (seq_app
           (seq_app (pred_ret (Eload chunk addr))
             (merge (list_translation rl f)))
-            (f #r Mem)))) :: lst
+            (f #r Mem))))) :: lst
   | RBstore p chunk addr rl r => lst
   | RBsetpred p' c args p =>  lst
   | RBexit p c => lst
@@ -365,7 +365,7 @@ Definition remember_expr_m_inc (fop : pred_op * forest) (lst: list pred_expr) (i
   | RBnop => lst
   | RBop p op rl r => lst
   | RBload  p chunk addr rl r => lst
-  | RBstore p chunk addr rl r => (NE.map (fun x => (dfltp p ∧ pred ∧ fst x, snd x))
+  | RBstore p chunk addr rl r => (app_predicated (dfltp p ∧ pred) (NE.singleton (Ptrue, Ebase Mem))
         (seq_app
           (seq_app
              (flap2 (seq_app (pred_ret Estore)
@@ -490,6 +490,15 @@ Definition schedule_oracle (bb: SeqBB.t) (bbt: ParBB.t) : bool :=
   | _, _ => false
   end.
 
+Definition schedule_oracle_inc (bb: SeqBB.t) (bbt: ParBB.t) : bool :=
+  match abstract_sequence_top_inc bb, abstract_sequence_top_inc (concat (concat bbt)) with
+  | Some (bb', reg_expr, m_expr), Some (bbt', reg_expr_t, m_expr_t) =>
+      check nil bb' bbt' && empty_trees bb bbt
+      && check_evaluability1 reg_expr reg_expr_t
+      && check_evaluability2 m_expr m_expr_t
+  | _, _ => false
+  end.
+
 Definition check_scheduled_trees := beq2 schedule_oracle.
 
 Ltac solve_scheduled_trees_correct :=
diff --git a/src/hls/GiblePargenproof.v b/src/hls/GiblePargenproof.v
index afa554c..1b5e505 100644
--- a/src/hls/GiblePargenproof.v
+++ b/src/hls/GiblePargenproof.v
@@ -57,6 +57,15 @@ Proof.
   inv Heqp1. now inv H.
 Qed.
 
+Lemma equiv_update_top_inc:
+  forall i p f l lm p' f' l' lm',
+    update_top_inc (p, f, l, lm) i = Some (p', f', l', lm') ->
+    update (p, f) i = Some (p', f').
+Proof.
+  intros. unfold update_top_inc, Option.bind2, Option.ret in *. repeat destr.
+  inv Heqp1. now inv H.
+Qed.
+
 Lemma remember_expr_eq :
   forall l i f,
     remember_expr f (map snd l) i = map snd (GiblePargen.remember_expr f l i).
@@ -64,6 +73,14 @@ Proof.
   induction l; destruct i; auto.
 Qed.
 
+Lemma remember_expr_eq_inc :
+  forall l i f,
+    remember_expr_inc f (map snd l) i = map snd (GiblePargen.remember_expr_inc f l i).
+Proof.
+  unfold remember_expr_inc, GiblePargen.remember_expr_inc.
+  induction l; destruct i; cbn; intros; repeat destruct_match; auto.
+Qed.
+
 Lemma equiv_update'_top:
   forall i p f l lm p' f' l' lm',
     update_top (p, f, l, lm) i = Some (p', f', l', lm') ->
@@ -73,6 +90,15 @@ Proof.
   inv Heqp1. inv H. repeat f_equal. apply remember_expr_eq.
 Qed.
 
+Lemma equiv_update'_top_inc:
+  forall i p f l lm p' f' l' lm',
+    update_top_inc (p, f, l, lm) i = Some (p', f', l', lm') ->
+    update'_inc (p, f, map snd l, lm) i = Some (p', f', map snd l', lm').
+Proof.
+  intros. unfold update'_inc, update_top_inc, Option.bind2, Option.ret in *. repeat destr.
+  inv Heqp1. inv H. repeat f_equal. apply remember_expr_eq_inc.
+Qed.
+
 Lemma equiv_fold_update'_top:
   forall i p f l lm p' f' l' lm',
     mfold_left update_top i (Some (p, f, l, lm)) = Some (p', f', l', lm') ->
@@ -86,6 +112,19 @@ Proof.
     intros. rewrite H0. eapply IHi. rewrite HB in H. eauto.
 Qed.
 
+Lemma equiv_fold_update'_top_inc:
+  forall i p f l lm p' f' l' lm',
+    mfold_left update_top_inc i (Some (p, f, l, lm)) = Some (p', f', l', lm') ->
+    mfold_left update'_inc i (Some (p, f, map snd l, lm)) = Some (p', f', map snd l', lm').
+Proof.
+  induction i; cbn -[update_top_inc update'_inc] in *; intros.
+  - inv H; auto.
+  - exploit OptionExtra.mfold_left_Some; eauto;
+      intros [[[[p_mid f_mid] l_mid] lm_mid] HB].
+    exploit equiv_update'_top_inc; try eassumption.
+    intros. rewrite H0. eapply IHi. rewrite HB in H. eauto.
+Qed.
+
 Lemma equiv_fold_update_top:
   forall i p f l lm p' f' l' lm',
     mfold_left update_top i (Some (p, f, l, lm)) = Some (p', f', l', lm') ->
@@ -99,6 +138,19 @@ Proof.
     intros. rewrite H0. eapply IHi. rewrite HB in H. eauto.
 Qed.
 
+Lemma equiv_fold_update_top_inc:
+  forall i p f l lm p' f' l' lm',
+    mfold_left update_top_inc i (Some (p, f, l, lm)) = Some (p', f', l', lm') ->
+    mfold_left update i (Some (p, f)) = Some (p', f').
+Proof.
+  induction i; cbn -[update_top_inc update] in *; intros.
+  - inv H; auto.
+  - exploit OptionExtra.mfold_left_Some; eauto;
+      intros [[[[p_mid f_mid] l_mid] lm_mid] HB].
+    exploit equiv_update_top_inc; try eassumption.
+    intros. rewrite H0. eapply IHi. rewrite HB in H. eauto.
+Qed.
+
 Lemma top_implies_abstract_sequence :
   forall y f l1 l2,
     abstract_sequence_top y = Some (f, l1, l2) ->
@@ -111,6 +163,18 @@ Proof.
   erewrite equiv_fold_update_top by eauto. auto.
 Qed.
 
+Lemma top_implies_abstract_sequence_inc :
+  forall y f l1 l2,
+    abstract_sequence_top_inc y = Some (f, l1, l2) ->
+    abstract_sequence y = Some f.
+Proof.
+  unfold abstract_sequence, abstract_sequence_top_inc; intros.
+  unfold Option.bind in *. repeat destr.
+  inv H.
+  unfold Option.map in *|-. repeat destr. subst. inv Heqo.
+  erewrite equiv_fold_update_top_inc by eauto. auto.
+Qed.
+
 Lemma top_implies_abstract_sequence' :
   forall y f l1 l2,
     abstract_sequence_top y = Some (f, l1, l2) ->
@@ -124,6 +188,19 @@ Proof.
   setoid_rewrite H. cbn. setoid_rewrite Heqm. auto.
 Qed.
 
+Lemma top_implies_abstract_sequence'_inc :
+  forall y f l1 l2,
+    abstract_sequence_top_inc y = Some (f, l1, l2) ->
+    abstract_sequence'_inc y = Some (f, map snd l1, l2).
+Proof.
+  unfold abstract_sequence'_inc, abstract_sequence_top_inc; intros.
+  unfold Option.bind in *|-. repeat destr.
+  inv H.
+  unfold Option.map in *|-. repeat destr. subst. inv Heqo.
+  exploit equiv_fold_update'_top_inc; eauto; intros.
+  setoid_rewrite H. cbn. setoid_rewrite Heqm. auto.
+Qed.
+
 Definition state_lessdef := GiblePargenproofEquiv.match_states.
 
 Definition match_prog (prog : GibleSeq.program) (tprog : GiblePar.program) :=
@@ -537,6 +614,30 @@ it states that we can execute the forest.
       eapply NE.Forall_forall in HFRL; eauto.
   Qed.
 
+  Lemma eval_forest_gather_predicates_fold_inc :
+    forall G A B a_sem i0 sp ge x p f p' f' pe pe_val preds preds' l l_m l' l_m',
+      OptionExtra.mfold_left update_top_inc x (Some (p, f, l, l_m)) = Some (p', f', l', l_m') ->
+      OptionExtra.mfold_left gather_predicates x (Some preds) = Some preds' ->
+      @sem_pred_expr G A B f.(forest_preds) a_sem (mk_ctx i0 sp ge) pe pe_val ->
+      NE.Forall (fun x => forall pred, PredIn pred (fst x) -> preds ! pred = Some tt) pe ->
+      sem_pred_expr f'.(forest_preds) a_sem (mk_ctx i0 sp ge) pe pe_val.
+  Proof.
+    induction x.
+    - intros * HF; cbn in *. now inv HF.
+    - intros * HFOLD1 HFOLD2 HSEM HFRL.
+      cbn -[update] in *.
+      exploit OptionExtra.mfold_left_Some. eapply HFOLD1.
+      intros [[[[p_mid f_mid] l_mid] l_m_mid] HSTATE].
+      rewrite HSTATE in HFOLD1.
+      exploit OptionExtra.mfold_left_Some. eapply HFOLD2.
+      intros [preds_mid HPRED]. rewrite HPRED in HFOLD2.
+      unfold Option.bind2, Option.ret in HSTATE; repeat destr; subst. inv HSTATE.
+      eapply IHx; eauto using eval_forest_gather_predicates.
+      eapply NE.Forall_forall; intros.
+      eapply gather_predicates_in; eauto.
+      eapply NE.Forall_forall in HFRL; eauto.
+  Qed.
+
   Lemma abstract_sequence_evaluable_fold2 :
     forall x sp i i' i0 cf p f l l_m p' f' l' l_m' preds preds',
       sem (mk_ctx i0 sp ge) f (i, Some cf) ->
@@ -648,6 +749,126 @@ it states that we can execute the forest.
           gather_predicates_in_forest, gather_predicates_update_constant.
   Qed.
 
+  Opaque app_predicated.
+
+  Lemma abstract_sequence_evaluable_fold2_inc :
+    forall x sp i i' i0 cf p f l l_m p' f' l' l_m' preds preds',
+      sem (mk_ctx i0 sp ge) f (i, Some cf) ->
+      sem (mk_ctx i0 sp ge) f' (i', Some cf) ->
+      eval_predf (is_ps i) p = false ->
+      mfold_left gather_predicates x (Some preds) = Some preds' ->
+      all_preds_in f preds ->
+      (forall in_pred : Predicate.predicate, PredIn in_pred p -> preds ! in_pred = Some tt) ->
+      OptionExtra.mfold_left update_top_inc x (Some (p, f, l, l_m)) = Some (p', f', l', l_m') ->
+      evaluable_pred_list (mk_ctx i0 sp ge) f'.(forest_preds) (map snd l) ->
+      evaluable_pred_list (mk_ctx i0 sp ge) f'.(forest_preds) (map snd l').
+  Proof.
+    induction x; intros * HSEM HSEM2 HPRED HGATHER HALL HPIN **.
+    - inv H. auto.
+    - exploit abstr_fold_falsy. apply HSEM.
+            eapply equiv_fold_update_top_inc; eauto. eauto. intros HSEM3. cbn -[update] in *. exploit OptionExtra.mfold_left_Some. eassumption.
+      intros [[[[p_mid f_mid] l_mid] l_m_mid] HBIND].
+      rewrite HBIND in H. unfold Option.bind2, Option.ret in HBIND; repeat destr; subst.
+      inv HBIND.
+      exploit OptionExtra.mfold_left_Some. eapply HGATHER.
+      intros [preds_mid HGATHER0]. rewrite HGATHER0 in HGATHER.
+      unfold evaluable_pred_list in *; intros.
+      eapply IHx. 7: { eauto. }
+      + eapply abstr_fold_falsy. eapply HSEM. instantiate (3 := (a :: nil)).
+        cbn -[update]. eauto. auto.
+      + eauto.
+      + destruct i. eapply sem_update_falsy_input; eauto.
+      + eauto.
+      + eapply gather_predicates_in_forest; eauto.
+      + eapply gather_predicates_update_constant; eauto.
+      + intros.
+        { destruct a; cbn -[gather_predicates update seq_app remember_expr_inc remember_expr_m_inc] in *; eauto.
+          - inv H2; eauto. exists (is_rs i0)!!1. inv HSEM3. inv H5.
+            eapply AbstrSemIdent.sem_pred_expr_app_predicated_false. repeat constructor. eauto.
+            rewrite eval_predf_Pand. cbn in *. rewrite HPRED. auto with bool.
+            - inv H2; eauto. exists (is_rs i0)!!1. inv HSEM3. inv H5.
+            eapply AbstrSemIdent.sem_pred_expr_app_predicated_false. repeat constructor. eauto.
+            rewrite eval_predf_Pand. cbn in *. rewrite HPRED. auto with bool.
+        }
+      + eauto.
+  Qed.
+
+  Lemma abstract_sequence_evaluable_fold_inc :
+    forall x sp i i' ti' i0 cf p f l l_m p' f' l' l_m' preds preds',
+      SeqBB.step ge sp (Iexec i) x (Iterm ti' cf) ->
+      state_lessdef i' ti' ->
+      sem (mk_ctx i0 sp ge) f (i, None) ->
+      sem (mk_ctx i0 sp ge) f' (i', Some cf) ->
+      eval_predf (is_ps i) p = true ->
+      GiblePargenproofCommon.valid_mem (is_mem i0) (is_mem i) ->
+      mfold_left gather_predicates x (Some preds) = Some preds' ->
+      all_preds_in f preds ->
+      (forall in_pred : Predicate.predicate, PredIn in_pred p -> preds ! in_pred = Some tt) ->
+      OptionExtra.mfold_left update_top_inc x (Some (p, f, l, l_m)) = Some (p', f', l', l_m') ->
+      evaluable_pred_list (mk_ctx i0 sp ge) f'.(forest_preds) (map snd l) ->
+      evaluable_pred_list (mk_ctx i0 sp ge) f'.(forest_preds) (map snd l').
+  Proof.
+    induction x; cbn -[update seq_app remember_expr_inc remember_expr_m_inc]; intros * ? HLESSDEF HSEM HSEM2 HPRED HVALID_MEM HGATHER HALL HPREDALL **.
+    - inv H0. auto.
+    - exploit OptionExtra.mfold_left_Some. eassumption.
+      intros [[[[p_mid f_mid] l_mid] l_m_mid] HBIND].
+      rewrite HBIND in H0. unfold Option.bind2, Option.ret in HBIND; repeat destr; subst.
+      inv HBIND.
+      exploit OptionExtra.mfold_left_Some. eapply HGATHER.
+      intros [preds_mid HGATHER0]. rewrite HGATHER0 in HGATHER.
+      inv H.
+      + unfold evaluable_pred_list; intros. exploit IHx.
+        eauto. eauto. eapply sem_update_instr; eauto.
+        eauto. eapply eval_predf_update_true; eauto.
+        transitivity (is_mem i); auto. eapply sem_update_valid_mem; eauto.
+        eauto. eapply gather_predicates_in_forest; eauto. eapply gather_predicates_update_constant; eauto.
+        eauto. unfold evaluable_pred_list in *; intros.
+        { destruct a; cbn -[gather_predicates update seq_app remember_expr_inc remember_expr_m_inc] in *; eauto.
+          - inv H2; eauto.
+            exploit sem_update_instr; eauto. intros. inv H2. inv H5. specialize (H2 r).
+            inv HSEM. inv H8.
+            exploit gather_predicates_in_forest; eauto. instantiate (1:=Reg r). intros HPRED_IN.
+            unfold update, Option.bind in Heqo. destruct_match; try discriminate. inv Heqo.
+            rewrite forest_reg_gss in H2.
+            exploit eval_forest_gather_predicates_fold_inc. eauto. eauto. apply H2.
+            eapply NE.Forall_forall; intros.
+            eapply NE.Forall_forall in HPRED_IN; eauto.
+            rewrite forest_reg_gss. auto. intros HSEMEXEC.
+            inv HSEM2. inv H13. exploit AbstrSemIdent.sem_pred_expr_prune_predicated2. eauto.
+            apply HSEMEXEC. eassumption.
+            intros HSEM_APP.
+            case_eq (eval_predf pr'1 (dfltp o ∧ p_mid)); intros.
+            + exists rs'!!r. eapply AbstrSemIdent.sem_pred_expr_app_predicated; eauto.
+              eapply AbstrSemIdent.sem_pred_expr_app_predicated2; eauto.
+            + exists (is_rs i0)!!1. eapply AbstrSemIdent.sem_pred_expr_app_predicated_false; eauto.
+              repeat constructor.
+          - inv H2; eauto.
+            exploit sem_update_instr; eauto. intros. inv H2. inv H5. specialize (H2 r).
+            inv HSEM. inv H8.
+            exploit gather_predicates_in_forest; eauto. instantiate (1:=Reg r). intros HPRED_IN.
+            unfold update, Option.bind in Heqo. destruct_match; try discriminate. inv Heqo.
+            rewrite forest_reg_gss in H2.
+            exploit eval_forest_gather_predicates_fold_inc. eauto. eauto. apply H2.
+            eapply NE.Forall_forall; intros.
+            eapply NE.Forall_forall in HPRED_IN; eauto.
+            rewrite forest_reg_gss. auto. intros HSEMEXEC.
+            inv HSEM2. inv H13. exploit AbstrSemIdent.sem_pred_expr_prune_predicated2. eauto.
+            apply HSEMEXEC. eassumption.
+            intros HSEM_APP.
+            case_eq (eval_predf pr'1 (dfltp o ∧ p_mid)); intros.
+            + exists rs'!!r. eapply AbstrSemIdent.sem_pred_expr_app_predicated; eauto.
+              eapply AbstrSemIdent.sem_pred_expr_app_predicated2; eauto.
+            + exists (is_rs i0)!!1. eapply AbstrSemIdent.sem_pred_expr_app_predicated_false; eauto.
+              repeat constructor.
+        }
+        eauto. auto.
+      + unfold evaluable_pred_list in *; intros.
+        inversion H5; subst.
+        exploit sem_update_instr_term; eauto; intros [HSEM3 HEVAL_PRED].
+        eapply abstract_sequence_evaluable_fold2_inc; eauto using
+          gather_predicates_in_forest, gather_predicates_update_constant.
+  Qed.
+
   Lemma abstract_sequence_evaluable_fold2_m :
     forall x sp i i' i0 cf p f l l_m p' f' l' l_m' preds preds',
       sem (mk_ctx i0 sp ge) f (i, Some cf) ->
@@ -741,6 +962,103 @@ it states that we can execute the forest.
           gather_predicates_in_forest, gather_predicates_update_constant.
 Qed.
 
+  Lemma abstract_sequence_evaluable_fold2_m_inc :
+    forall x sp i i' i0 cf p f l l_m p' f' l' l_m' preds preds',
+      sem (mk_ctx i0 sp ge) f (i, Some cf) ->
+      sem (mk_ctx i0 sp ge) f' (i', Some cf) ->
+      eval_predf (is_ps i) p = false ->
+      mfold_left gather_predicates x (Some preds) = Some preds' ->
+      all_preds_in f preds ->
+      (forall in_pred : Predicate.predicate, PredIn in_pred p -> preds ! in_pred = Some tt) ->
+      OptionExtra.mfold_left update_top_inc x (Some (p, f, l, l_m)) = Some (p', f', l', l_m') ->
+      evaluable_pred_list_m (mk_ctx i0 sp ge) f'.(forest_preds) l_m ->
+      evaluable_pred_list_m (mk_ctx i0 sp ge) f'.(forest_preds) l_m'.
+  Proof.
+    induction x; intros * HSEM HSEM2 HPRED HGATHER HALL HPIN **.
+    - inv H. auto.
+    - exploit abstr_fold_falsy. apply HSEM.
+            eapply equiv_fold_update_top_inc; eauto. eauto. intros HSEM3. cbn -[update] in *. exploit OptionExtra.mfold_left_Some. eassumption.
+      intros [[[[p_mid f_mid] l_mid] l_m_mid] HBIND].
+      rewrite HBIND in H. unfold Option.bind2, Option.ret in HBIND; repeat destr; subst.
+      inv HBIND.
+      exploit OptionExtra.mfold_left_Some. eapply HGATHER.
+      intros [preds_mid HGATHER0]. rewrite HGATHER0 in HGATHER.
+      unfold evaluable_pred_list_m in *; intros.
+      eapply IHx. 7: { eauto. }
+      + eapply abstr_fold_falsy. eapply HSEM. instantiate (3 := (a :: nil)).
+        cbn -[update]. eauto. auto.
+      + eauto.
+      + destruct i. eapply sem_update_falsy_input; eauto.
+      + eauto.
+      + eapply gather_predicates_in_forest; eauto.
+      + eapply gather_predicates_update_constant; eauto.
+      + intros.
+        { destruct a; cbn -[gather_predicates update seq_app remember_expr_inc remember_expr_m_inc] in *; eauto.
+          - inv H2; eauto. exists (is_mem i0). inv HSEM3. inv H5.
+            eapply AbstrSemIdent.sem_pred_expr_app_predicated_false. repeat constructor. eauto.
+            rewrite eval_predf_Pand. cbn in *. rewrite HPRED. auto with bool.
+        }
+      + eauto.
+  Qed.
+
+  Lemma abstract_sequence_evaluable_fold_m_inc :
+    forall x sp i i' ti' i0 cf p f l l_m p' f' l' l_m' preds preds',
+      SeqBB.step ge sp (Iexec i) x (Iterm ti' cf) ->
+      state_lessdef i' ti' ->
+      sem (mk_ctx i0 sp ge) f (i, None) ->
+      sem (mk_ctx i0 sp ge) f' (i', Some cf) ->
+      eval_predf (is_ps i) p = true ->
+      GiblePargenproofCommon.valid_mem (is_mem i0) (is_mem i) ->
+      mfold_left gather_predicates x (Some preds) = Some preds' ->
+      all_preds_in f preds ->
+      (forall in_pred : Predicate.predicate, PredIn in_pred p -> preds ! in_pred = Some tt) ->
+      OptionExtra.mfold_left update_top_inc x (Some (p, f, l, l_m)) = Some (p', f', l', l_m') ->
+      evaluable_pred_list_m (mk_ctx i0 sp ge) f'.(forest_preds) l_m ->
+      evaluable_pred_list_m (mk_ctx i0 sp ge) f'.(forest_preds) l_m'.
+  Proof.
+    induction x; cbn -[update seq_app remember_expr_inc remember_expr_m_inc]; intros * ? HLESSDEF HSEM HSEM2 HPRED HVALID_MEM HGATHER HALL HPREDALL **.
+    - inv H0. auto.
+    - exploit OptionExtra.mfold_left_Some. eassumption.
+      intros [[[[p_mid f_mid] l_mid] l_m_mid] HBIND].
+      rewrite HBIND in H0. unfold Option.bind2, Option.ret in HBIND; repeat destr; subst.
+      inv HBIND.
+      exploit OptionExtra.mfold_left_Some. eapply HGATHER.
+      intros [preds_mid HGATHER0]. rewrite HGATHER0 in HGATHER.
+      inv H.
+      + unfold evaluable_pred_list_m; intros. exploit IHx.
+        eauto. eauto. eapply sem_update_instr; eauto.
+        eauto. eapply eval_predf_update_true; eauto.
+        transitivity (is_mem i); auto. eapply sem_update_valid_mem; eauto.
+        eauto. eapply gather_predicates_in_forest; eauto. eapply gather_predicates_update_constant; eauto.
+        eauto. unfold evaluable_pred_list_m in *; intros.
+        { destruct a; cbn -[gather_predicates update seq_app remember_expr_inc remember_expr_m_inc] in *; eauto.
+          - inv H2; eauto.
+            exploit sem_update_instr; eauto. intros. inv H2. inv H5. specialize (H2 r).
+            inv HSEM. inv H8.
+            exploit gather_predicates_in_forest; eauto. instantiate (1:=Mem). intros HPRED_IN.
+            unfold update, Option.bind in Heqo. destruct_match; try discriminate. inv Heqo.
+            rewrite forest_reg_gss in H11.
+            exploit eval_forest_gather_predicates_fold_inc. eauto. eauto. apply H11.
+            eapply NE.Forall_forall; intros.
+            eapply NE.Forall_forall in HPRED_IN; eauto.
+            rewrite forest_reg_gss. auto. intros HSEMEXEC.
+            inv HSEM2. inv H13. exploit AbstrSemIdent.sem_pred_expr_prune_predicated2. eauto.
+            apply HSEMEXEC. eassumption.
+            intros HSEM_APP.
+            case_eq (eval_predf pr'1 (dfltp o ∧ p_mid)); intros.
+            + exists m'. eapply AbstrSemIdent.sem_pred_expr_app_predicated; eauto.
+              eapply AbstrSemIdent.sem_pred_expr_app_predicated2; eauto.
+            + exists (is_mem i0). eapply AbstrSemIdent.sem_pred_expr_app_predicated_false; eauto.
+              repeat constructor.
+        }
+        eauto. auto.
+      + unfold evaluable_pred_list in *; intros.
+        inversion H5; subst.
+        exploit sem_update_instr_term; eauto; intros [HSEM3 HEVAL_PRED].
+        eapply abstract_sequence_evaluable_fold2_m_inc; eauto using
+          gather_predicates_in_forest, gather_predicates_update_constant.
+  Qed.
+
 (*|
 Proof sketch: If I can execute the list of instructions, then every single
 forest element that is added to the forest will be evaluable too.  This then
@@ -767,6 +1085,25 @@ have been evaluable.
     - cbn; unfold evaluable_pred_list; inversion 1.
   Qed.
 
+  Lemma abstract_sequence_evaluable_inc :
+    forall sp x i i' ti' cf f l0 l,
+      SeqBB.step ge sp (Iexec i) x (Iterm ti' cf) ->
+      state_lessdef i' ti' ->
+      sem {| ctx_is := i; ctx_sp := sp; ctx_ge := ge |} f (i', Some cf) ->
+      abstract_sequence_top_inc x = Some (f, l0, l) ->
+      evaluable_pred_list (mk_ctx i sp ge) f.(forest_preds) (map snd l0).
+  Proof.
+    intros * ? HLESSDEF **. unfold abstract_sequence_top_inc in *.
+    unfold Option.bind, Option.map in H1; repeat destr.
+    inv H1. inv Heqo.
+    eapply abstract_sequence_evaluable_fold_inc; eauto; auto.
+    - apply sem_empty.
+    - reflexivity.
+    - apply all_preds_in_empty.
+    - inversion 1.
+    - cbn; unfold evaluable_pred_list; inversion 1.
+  Qed.
+
   Lemma abstract_sequence_evaluable_m :
     forall sp x i i' ti' cf f l0 l,
       SeqBB.step ge sp (Iexec i) x (Iterm ti' cf) ->
@@ -786,6 +1123,25 @@ have been evaluable.
     - cbn; unfold evaluable_pred_list; inversion 1.
   Qed.
 
+  Lemma abstract_sequence_evaluable_m_inc :
+    forall sp x i i' ti' cf f l0 l,
+      SeqBB.step ge sp (Iexec i) x (Iterm ti' cf) ->
+      state_lessdef i' ti' ->
+      sem {| ctx_is := i; ctx_sp := sp; ctx_ge := ge |} f (i', Some cf) ->
+      abstract_sequence_top_inc x = Some (f, l0, l) ->
+      evaluable_pred_list_m (mk_ctx i sp ge) f.(forest_preds) l.
+  Proof.
+    intros * ? HLESSDEF **. unfold abstract_sequence_top_inc in *.
+    unfold Option.bind, Option.map in H1; repeat destr.
+    inv H1. inv Heqo.
+    eapply abstract_sequence_evaluable_fold_m_inc; eauto; auto.
+    - apply sem_empty.
+    - reflexivity.
+    - apply all_preds_in_empty.
+    - inversion 1.
+    - cbn; unfold evaluable_pred_list; inversion 1.
+  Qed.
+
   Lemma check_evaluability1_evaluable :
     forall G (ctx: @Abstr.ctx G) l1 l2 f ps,
       (forall x : positive, sem_pexpr ctx (get_forest_p' x f) ps !! x) ->
@@ -936,6 +1292,50 @@ have been evaluable.
     etransitivity; eauto.
   Qed.
 
+  Lemma schedule_oracle_correct_inc:
+    forall x y sp i i' ti cf,
+      schedule_oracle_inc x y = true ->
+      SeqBB.step ge sp (Iexec i) x (Iterm i' cf) ->
+      state_lessdef i ti ->
+      exists ti', ParBB.step tge sp (Iexec ti) y (Iterm ti' cf)
+             /\ state_lessdef i' ti'.
+  Proof.
+    unfold schedule_oracle_inc; intros. repeat (destruct_match; try discriminate). simplify.
+    exploit top_implies_abstract_sequence_inc; [eapply Heqo|]; intros.
+    exploit top_implies_abstract_sequence'_inc; eauto; intros.
+    exploit abstr_sequence_correct; eauto; simplify.
+    exploit local_abstr_check_correct2; eauto.
+    { constructor. eapply ge_preserved_refl. reflexivity. }
+(*    { inv H. inv H8. exists pr'. intros x0. specialize (H x0). auto. } *)
+    simplify.
+    exploit abstr_seq_reverse_correct_inc; eauto.
+    { inv H8. inv H14.
+      eapply check_evaluability1_evaluable.
+      eauto. eauto.
+      eapply evaluable_same_preds. unfold check in *. simplify. eauto.
+      eapply evaluable_same_state; eauto.
+      eapply abstract_sequence_evaluable_inc. eauto. symmetry; eauto.
+      eapply sem_correct; eauto.
+      { constructor. constructor; auto. symmetry; auto. }
+      eauto.
+    }
+    { inv H8. inv H14.
+      eapply check_evaluability2_evaluable.
+      eauto. eauto.
+      eapply evaluable_same_preds_m. unfold check in *. simplify. eauto.
+      eapply evaluable_same_state_m; eauto.
+      eapply abstract_sequence_evaluable_m_inc. eauto. symmetry; eauto.
+      eapply sem_correct; eauto.
+      { constructor. constructor; auto. symmetry; auto. }
+      eauto.
+    }
+    reflexivity. simplify.
+    exploit seqbb_step_parbb_step; eauto; intros.
+    econstructor; split; eauto.
+    etransitivity; eauto.
+    etransitivity; eauto.
+  Qed.
+
   Lemma step_cf_correct :
     forall cf ts s s' t,
       GibleSeq.step_cf_instr ge s cf t s' ->
diff --git a/src/hls/GiblePargenproofBackward.v b/src/hls/GiblePargenproofBackward.v
index 43e97a6..659a683 100644
--- a/src/hls/GiblePargenproofBackward.v
+++ b/src/hls/GiblePargenproofBackward.v
@@ -76,16 +76,42 @@ Definition remember_expr (f : forest) (lst: list pred_expr) (i : instr): list pr
   | RBexit p c => lst
   end.
 
+Definition remember_expr_inc (fop : pred_op * forest) (lst: list pred_expr) (i : instr): list pred_expr :=
+  let (pred, f) := fop in
+  match i with
+  | RBnop => lst
+  | RBop p op rl r => (app_predicated (dfltp p ∧ pred) (NE.singleton (Ptrue, Ebase (Reg 1))) (
+        (seq_app (pred_ret (Eop op)) (merge (list_translation rl f))))) :: lst
+  | RBload p chunk addr rl r => (app_predicated (dfltp p ∧ pred) (NE.singleton (Ptrue, Ebase (Reg 1))) (
+        (seq_app
+          (seq_app (pred_ret (Eload chunk addr))
+            (merge (list_translation rl f)))
+            (f #r Mem)))) :: lst
+  | RBstore p chunk addr rl r => lst
+  | RBsetpred p' c args p =>  lst
+  | RBexit p c => lst
+  end.
+
 Definition update' (s: pred_op * forest * list pred_expr * list pred_expr) (i: instr): option (pred_op * forest * list pred_expr * list pred_expr) :=
   let '(p, f, l, lm) := s in
   Option.bind2 (fun p' f' => Option.ret (p', f', remember_expr f l i, remember_expr_m f lm i)) (update (p, f) i).
 
+Definition update'_inc (s: pred_op * forest * list pred_expr * list pred_expr) (i: instr): option (pred_op * forest * list pred_expr * list pred_expr) :=
+  let '(p, f, l, lm) := s in
+  Option.bind2 (fun p' f' => Option.ret (p', f', remember_expr_inc (p, f) l i, remember_expr_m_inc (p, f) lm i)) (update (p, f) i).
+
 Definition abstract_sequence' (b : list instr) : option (forest * list pred_expr * list pred_expr) :=
   Option.bind (fun x => Option.bind (fun _ => Some x)
     (mfold_left gather_predicates b (Some (PTree.empty _))))
       (Option.map (fun x => let '(_, y, z, zm) := x in (y, z, zm))
         (mfold_left update' b (Some (Ptrue, empty, nil, nil)))).
 
+Definition abstract_sequence'_inc (b : list instr) : option (forest * list pred_expr * list pred_expr) :=
+  Option.bind (fun x => Option.bind (fun _ => Some x)
+    (mfold_left gather_predicates b (Some (PTree.empty _))))
+      (Option.map (fun x => let '(_, y, z, zm) := x in (y, z, zm))
+        (mfold_left update'_inc b (Some (Ptrue, empty, nil, nil)))).
+
 Section CORRECTNESS.
 
 Context (prog: GibleSeq.program) (tprog : GiblePar.program).
@@ -106,6 +132,19 @@ Proof.
     eapply IHi; eauto.
 Qed.
 
+Lemma equiv_update_inc:
+  forall i p f l lm p' f' l' lm',
+    mfold_left update'_inc i (Some (p, f, l, lm)) = Some (p', f', l', lm') ->
+    mfold_left update i (Some (p, f)) = Some (p', f').
+Proof.
+  induction i; cbn -[update] in *; intros.
+  - inv H; auto.
+  - exploit OptionExtra.mfold_left_Some; eauto;
+      intros [[[[p_mid f_mid] l_mid] lm_mid] HB].
+    unfold Option.bind2, Option.ret in HB; repeat destr. inv Heqp1.
+    eapply IHi; eauto.
+Qed.
+
 Lemma equiv_update1:
   forall i p f l lm p' f' l' lm',
     update' (p, f, l, lm) i = Some (p', f', l', lm') ->
@@ -115,6 +154,15 @@ Proof.
   now inv H.
 Qed.
 
+Lemma equiv_update1_inc:
+  forall i p f l lm p' f' l' lm',
+    update'_inc (p, f, l, lm) i = Some (p', f', l', lm') ->
+    update (p, f) i = Some (p', f').
+Proof.
+  intros. unfold update'_inc, Option.bind2, Option.ret in *. repeat destr.
+  now inv H.
+Qed.
+
 Lemma equiv_update1'':
   forall i p f l lm p' f' l' lm' lp lp',
     update'' (p, f, l, lm, lp) i = Some (p', f', l', lm', lp') ->
@@ -148,6 +196,18 @@ Definition evaluable_pred_expr {G} (ctx: @Abstr.ctx G) pr p :=
 Definition evaluable_pred_expr_m {G} (ctx: @Abstr.ctx G) pr p :=
   exists r, sem_pred_expr pr sem_mem ctx p r.
 
+Definition cond_evaluable_pred_expr {G} (ctx: @Abstr.ctx G) pr ps cond p :=
+  eval_predf ps cond = true ->
+  exists r, sem_pred_expr pr sem_value ctx p r.
+
+Definition cond_evaluable_pred_expr_m {G} (ctx: @Abstr.ctx G) pr ps cond p :=
+  eval_predf ps cond = true ->
+  exists r, sem_pred_expr pr sem_mem ctx p r.
+
+Definition evaluable_forest {G} (ctx: @Abstr.ctx G) pr f := 
+  (forall x, evaluable_pred_expr ctx pr (f #r (Reg x)))
+  /\ evaluable_pred_expr_m ctx pr (f #r Mem).
+
 Definition evaluable_pred_list {G} ctx pr l :=
   forall p,
     In p l ->
@@ -472,11 +532,25 @@ Proof.
   unfold remember_expr; destruct a; eauto using in_cons.
 Qed.
 
+Lemma remember_expr_in_inc :
+  forall x l f a,
+    In x l -> In x (remember_expr_inc f l a).
+Proof.
+  unfold remember_expr_inc; destruct a; repeat destruct_match; eauto using in_cons.
+Qed.
+
 Lemma remember_expr_in_m :
   forall x l f a,
     In x l -> In x (remember_expr_m f l a).
 Proof.
-  unfold remember_expr; destruct a; eauto using in_cons.
+  unfold remember_expr_m; destruct a; eauto using in_cons.
+Qed.
+
+Lemma remember_expr_in_m_inc :
+  forall x l f a,
+    In x l -> In x (remember_expr_m_inc f l a).
+Proof.
+  unfold remember_expr_m_inc; destruct a; repeat destruct_match; eauto using in_cons.
 Qed.
 
 Lemma in_mfold_left_abstr :
@@ -495,6 +569,22 @@ Proof.
     auto using remember_expr_in.
 Qed.
 
+Lemma in_mfold_left_abstr_inc :
+  forall instrs p f l p' f' l' x lm lm',
+    mfold_left update'_inc instrs (Some (p, f, l, lm)) = Some (p', f', l', lm') ->
+    In x l -> In x l'.
+Proof.
+  induction instrs; intros.
+  - cbn in *; now inv H.
+  - cbn -[update] in *.
+    pose proof H as Y.
+    apply OptionExtra.mfold_left_Some in Y. inv Y.
+    rewrite H1 in H. destruct x0 as (((p_int & f_int) & l_int) & lm_int).
+    exploit IHinstrs; eauto.
+    unfold Option.bind2, Option.ret in H1; repeat destr. inv H1.
+    destruct a; auto; apply in_cons; auto.
+Qed.
+
 Lemma in_mfold_left_abstr_m :
   forall instrs p f l p' f' l' x lm lm',
     mfold_left update' instrs (Some (p, f, l, lm)) = Some (p', f', l', lm') ->
@@ -511,6 +601,22 @@ Proof.
     auto using remember_expr_in_m.
 Qed.
 
+Lemma in_mfold_left_abstr_m_inc:
+  forall instrs p f l p' f' l' x lm lm',
+    mfold_left update'_inc instrs (Some (p, f, l, lm)) = Some (p', f', l', lm') ->
+    In x lm -> In x lm'.
+Proof.
+  induction instrs; intros.
+  - cbn in *; now inv H.
+  - cbn -[update remember_expr_inc remember_expr_m_inc] in *.
+    pose proof H as Y.
+    apply OptionExtra.mfold_left_Some in Y. inv Y.
+    rewrite H1 in H. destruct x0 as (((p_int & f_int) & l_int) & lm_int).
+    exploit IHinstrs; eauto.
+    unfold Option.bind, Option.bind2, Option.ret in *; repeat destr. inv H1.
+    destruct a; auto. apply in_cons; auto.
+Qed.
+
 Lemma not_remembered_in_forest :
   forall a p f p_mid f_mid l x,
     update (p, f) a = Some (p_mid, f_mid) ->
@@ -615,6 +721,34 @@ Proof.
   unfold evaluable_pred_expr_m. eauto.
 Qed.
 
+(* Lemma in_forest_evaluable_inc : *)
+(*   forall G sp ge i' cf instrs p f l p' f' l' x i0 lm lm', *)
+(*     mfold_left update'_inc instrs (Some (p, f, l, lm)) = Some (p', f', l', lm') -> *)
+(*     sem (mk_ctx i0 sp ge) f' (i', cf) -> *)
+(*     @evaluable_pred_list G (mk_ctx i0 sp ge) f'.(forest_preds) l' -> *)
+(*     evaluable_pred_expr (mk_ctx i0 sp ge) f'.(forest_preds) (f #r (Reg x)). *)
+(* Proof. *)
+(*   intros. *)
+(*   pose proof H as Y. apply in_forest_or_remembered with (x := x) in Y. *)
+(*   inv Y; eauto. *)
+(*   inv H0. inv H5. rewrite H2. *)
+(*   unfold evaluable_pred_expr. eauto. *)
+(* Qed. *)
+
+(* Lemma in_forest_evaluable_m_inc : *)
+(*   forall G sp ge i' cf instrs p f l p' f' l' i0 lm lm', *)
+(*     mfold_left update'_inc instrs (Some (p, f, l, lm)) = Some (p', f', l', lm') -> *)
+(*     sem (mk_ctx i0 sp ge) f' (i', cf) -> *)
+(*     @evaluable_pred_list_m G (mk_ctx i0 sp ge) f'.(forest_preds) lm' -> *)
+(*     evaluable_pred_expr_m (mk_ctx i0 sp ge) f'.(forest_preds) (f #r Mem). *)
+(* Proof. *)
+(*   intros. *)
+(*   pose proof H as Y. apply in_forest_or_remembered_m in Y. *)
+(*   inv Y; eauto. *)
+(*   inv H0. inv H5. rewrite H2. *)
+(*   unfold evaluable_pred_expr_m. eauto. *)
+(* Qed. *)
+
 Definition pe_preds_in {A} (x: predicated A) preds :=
   NE.Forall (fun x => forall pred, PredIn pred (fst x)
                -> PTree.get pred preds = Some tt) x.
@@ -1346,6 +1480,20 @@ Proof.
   eapply abstr_seq_revers_correct_fold_sem_pexpr_eval3''; eauto.
 Qed.
 
+Lemma abstr_seq_revers_correct_fold_sem_pexpr_eval3'_inc :
+  forall A B G a_sem instrs p f p' f' i0 sp ge preds preds' pe pe_val l l' lm lm',
+    update'_inc (p, f, l, lm) instrs = Some (p', f', l', lm') ->
+    gather_predicates preds instrs = Some preds' ->
+    @sem_pred_expr G A B f'.(forest_preds) a_sem (mk_ctx i0 sp ge) pe pe_val ->
+    NE.Forall (fun x => forall pred, PredIn pred (fst x) -> preds ! pred = Some tt) pe ->
+    sem_pred_expr f.(forest_preds) a_sem (mk_ctx i0 sp ge) pe pe_val.
+Proof.
+  intros.
+  unfold update'_inc, Option.bind2, Option.ret in H; repeat destr.
+  inversion H; subst.
+  eapply abstr_seq_revers_correct_fold_sem_pexpr_eval3''; eauto.
+Qed.
+
 Lemma abstr_seq_revers_correct_fold_sem_pexpr_eval3 :
   forall A B G a_sem instrs p f l p' f' l' i0 sp ge preds preds' pe pe_val lm lm',
     mfold_left update' instrs (Some (p, f, l, lm)) = Some (p', f', l', lm') ->
@@ -1369,6 +1517,29 @@ Proof.
   eapply abstr_seq_revers_correct_fold_sem_pexpr_eval3'; eauto.
 Qed.
 
+Lemma abstr_seq_revers_correct_fold_sem_pexpr_eval3_inc :
+  forall A B G a_sem instrs p f l p' f' l' i0 sp ge preds preds' pe pe_val lm lm',
+    mfold_left update'_inc instrs (Some (p, f, l, lm)) = Some (p', f', l', lm') ->
+    mfold_left gather_predicates instrs (Some preds) = Some preds' ->
+    @sem_pred_expr G A B f'.(forest_preds) a_sem (mk_ctx i0 sp ge) pe pe_val ->
+    NE.Forall (fun x => forall pred, PredIn pred (fst x) -> preds ! pred = Some tt) pe ->
+    sem_pred_expr f.(forest_preds) a_sem (mk_ctx i0 sp ge) pe pe_val.
+Proof.
+  induction instrs; [crush|].
+  intros. cbn -[update remember_expr_inc remember_expr_m_inc] in H,H0.
+  exploit OptionExtra.mfold_left_Some. eapply H. intros [[[[p_mid f_mid] l_mid] lm_mid] HBind].
+  rewrite HBind in H.
+  exploit OptionExtra.mfold_left_Some. eapply H0. intros [preds_mid HGATHER].
+  rewrite HGATHER in H0.
+  exploit IHinstrs; eauto.
+  apply NE.Forall_forall. intros [p_op aval] YIN ypred YPREDIN.
+  apply NE.Forall_forall with (x:=(p_op, aval)) in H2; auto. cbn [fst snd] in *.
+  specialize (H2 ypred YPREDIN).
+  eapply gather_predicates_in; eassumption.
+  intros HSEM.
+  eapply abstr_seq_revers_correct_fold_sem_pexpr_eval3'_inc; eauto.
+Qed.
+
 Lemma abstr_seq_revers_correct_fold_sem_pexpr_eval2 :
   forall G instrs p f l p' f' l' i0 sp ge preds preds' pe lm lm',
     mfold_left update' instrs (Some (p, f, l, lm)) = Some (p', f', l', lm') ->
@@ -1383,6 +1554,20 @@ Proof.
   eapply abstr_seq_revers_correct_fold_sem_pexpr_eval3; eauto.
 Qed.
 
+Lemma abstr_seq_revers_correct_fold_sem_pexpr_eval2_inc :
+  forall G instrs p f l p' f' l' i0 sp ge preds preds' pe lm lm',
+    mfold_left update'_inc instrs (Some (p, f, l, lm)) = Some (p', f', l', lm') ->
+    mfold_left gather_predicates instrs (Some preds) = Some preds' ->
+    @evaluable_pred_expr G (mk_ctx i0 sp ge) f'.(forest_preds) pe ->
+    NE.Forall (fun x => forall pred, PredIn pred (fst x)
+                 -> PTree.get pred preds = Some tt) pe ->
+    evaluable_pred_expr (mk_ctx i0 sp ge) f.(forest_preds) pe.
+Proof.
+  unfold evaluable_pred_expr in *.
+  intros. inv H1. exists x.
+  eapply abstr_seq_revers_correct_fold_sem_pexpr_eval3_inc; eauto.
+Qed.
+
 Lemma abstr_seq_revers_correct_fold_sem_pexpr_eval4 :
   forall G instrs p f l p' f' l' i0 sp ge preds preds' pe lm lm',
     mfold_left update' instrs (Some (p, f, l, lm)) = Some (p', f', l', lm') ->
@@ -1397,6 +1582,20 @@ Proof.
   eapply abstr_seq_revers_correct_fold_sem_pexpr_eval3; eauto.
 Qed.
 
+Lemma abstr_seq_revers_correct_fold_sem_pexpr_eval4_inc :
+  forall G instrs p f l p' f' l' i0 sp ge preds preds' pe lm lm',
+    mfold_left update'_inc instrs (Some (p, f, l, lm)) = Some (p', f', l', lm') ->
+    mfold_left gather_predicates instrs (Some preds) = Some preds' ->
+    @evaluable_pred_expr_m G (mk_ctx i0 sp ge) f'.(forest_preds) pe ->
+    NE.Forall (fun x => forall pred, PredIn pred (fst x)
+                 -> PTree.get pred preds = Some tt) pe ->
+    evaluable_pred_expr_m (mk_ctx i0 sp ge) f.(forest_preds) pe.
+Proof.
+  unfold evaluable_pred_expr in *.
+  intros. inv H1. exists x.
+  eapply abstr_seq_revers_correct_fold_sem_pexpr_eval3_inc; eauto.
+Qed.
+
 Lemma state_lessdef_state_equiv :
   forall x y, state_lessdef x y <-> state_equiv x y.
 Proof. split; intros; inv H; constructor; auto. Qed.
@@ -1419,6 +1618,24 @@ Proof.
   unfold Option.bind2, Option.ret in *. repeat destr. inv Heqp1. inv HBIND. eauto.
 Qed.
 
+Lemma abstr_seq_revers_correct_fold_sem_pexpr_inc :
+  forall instrs p f l p' f' l' preds preds' lm lm',
+    mfold_left update'_inc instrs (Some (p, f, l, lm)) = Some (p', f', l', lm') ->
+    mfold_left gather_predicates instrs (Some preds) = Some preds' ->
+    forall pred, preds ! pred = Some tt ->
+      f #p pred = f' #p pred.
+Proof.
+  induction instrs; try solve [crush].
+  intros. cbn -[update] in *.
+  exploit OptionExtra.mfold_left_Some. apply H. intros [[[[p_mid f_mid] l_mid] lm_mid] HBIND].
+  exploit OptionExtra.mfold_left_Some. apply H0. intros [ptree_mid HGATHER].
+  rewrite HBIND in H. rewrite HGATHER in H0.
+  exploit IHinstrs; eauto. eapply gather_predicates_in; eauto.
+  intros. rewrite <- H2.
+  unfold "#p". unfold get_forest_p'. erewrite abstr_seq_revers_correct_fold_sem_pexpr_sem2; eauto.
+  unfold Option.bind2, Option.ret in *. repeat destr. inv Heqp1. inv HBIND. eauto.
+Qed.
+
 (*|
 This lemma states that predicates are always evaluable, given that the output
 forest is also evaluable.  This is true because gather_predicates ensures that
@@ -1482,6 +1699,60 @@ Proof.
     eauto. inv H1; eauto.
 Qed.
 
+Lemma update_rev_gather_constant_inc:
+  forall G i preds i0 sp ge f p l lm p' f' l' lm' preds' ps,
+    (forall p, preds ! p = None -> @sem_pexpr G (mk_ctx i0 sp ge) (f #p p) (ps !! p)) ->
+    update'_inc (p, f, l, lm) i = Some (p', f', l', lm') ->
+    gather_predicates preds i = Some preds' ->
+    (forall p, preds' ! p = None -> sem_pexpr (mk_ctx i0 sp ge) (f' #p p) (ps !! p)).
+Proof.
+  unfold update'_inc, gather_predicates; destruct i; intros; unfold Option.bind, Option.bind2, Option.ret in *;
+    repeat destr.
+  - inv H0. inv H1. inv Heqo. eauto.
+  - inv H0. cbn in *. unfold Option.bind, Option.bind2, Option.ret in *;
+    repeat destr; inv Heqo1; inv H4. destruct o. inv H1. eapply gather_predicates_fold3 in H2. eauto. inv H1; eauto.
+  - inv H0. cbn in *. unfold Option.bind, Option.bind2, Option.ret in *;
+    repeat destr; inv Heqo1; inv H4. inv Heqo0. destruct o. inv H1. eapply gather_predicates_fold3 in H2.
+    eauto. inv H1; eauto.
+  - inv H0. cbn in *. unfold Option.bind, Option.bind2, Option.ret in *;
+    repeat destr; inv Heqo1; inv H4. inv Heqo0. destruct o. inv H1. eapply gather_predicates_fold3 in H2.
+    eauto. inv H1; eauto.
+  - inv H0. cbn in *. unfold Option.bind, Option.bind2, Option.ret in *. repeat destr. inv Heqo1. inv H4.
+    destruct (peq p1 p); subst. inv H1. rewrite PTree.gss in H2. discriminate.
+    rewrite forest_pred_gso by auto. inv H1. rewrite PTree.gso in H2 by auto.
+    destruct o. eapply gather_predicates_fold3 in H2. eauto. eauto.
+  - inv H0. cbn in *. unfold Option.bind, Option.bind2, Option.ret in *;
+    repeat destr; inv Heqo1; inv H4. inv Heqo0. destruct o. inv H1. eapply gather_predicates_fold3 in H2.
+    eauto. inv H1; eauto.
+Qed.
+
+Lemma update_rev_gather_constant2_inc:
+  forall G i preds i0 sp ge f p l lm p' f' l' lm' preds' ps,
+    (forall p, preds ! p = None -> @sem_pexpr G (mk_ctx i0 sp ge) (f #p p) ps) ->
+    update'_inc (p, f, l, lm) i = Some (p', f', l', lm') ->
+    gather_predicates preds i = Some preds' ->
+    (forall p, preds' ! p = None -> sem_pexpr (mk_ctx i0 sp ge) (f' #p p) ps).
+Proof.
+  unfold update'_inc, gather_predicates; destruct i; intros; unfold Option.bind, Option.bind2, Option.ret in *;
+    repeat destr.
+  - inv H0. inv H1. inv Heqo. eauto.
+  - inv H0. cbn in *. unfold Option.bind, Option.bind2, Option.ret in *;
+    repeat destr; inv Heqo1; inv H4. destruct o. inv H1. eapply gather_predicates_fold3 in H2. eauto. inv H1; eauto.
+  - inv H0. cbn in *. unfold Option.bind, Option.bind2, Option.ret in *;
+    repeat destr; inv Heqo1; inv H4. inv Heqo0. destruct o. inv H1. eapply gather_predicates_fold3 in H2.
+    eauto. inv H1; eauto.
+  - inv H0. cbn in *. unfold Option.bind, Option.bind2, Option.ret in *;
+    repeat destr; inv Heqo1; inv H4. inv Heqo0. destruct o. inv H1. eapply gather_predicates_fold3 in H2.
+    eauto. inv H1; eauto.
+  - inv H0. cbn in *. unfold Option.bind, Option.bind2, Option.ret in *. repeat destr. inv Heqo1. inv H4.
+    destruct (peq p1 p); subst. inv H1. rewrite PTree.gss in H2. discriminate.
+    rewrite forest_pred_gso by auto. inv H1. rewrite PTree.gso in H2 by auto.
+    destruct o. eapply gather_predicates_fold3 in H2. eauto. eauto.
+  - inv H0. cbn in *. unfold Option.bind, Option.bind2, Option.ret in *;
+    repeat destr; inv Heqo1; inv H4. inv Heqo0. destruct o. inv H1. eapply gather_predicates_fold3 in H2.
+    eauto. inv H1; eauto.
+Qed.
+
 Definition PMapmap {A} (f: positive -> A -> A) (m: PMap.t A): PMap.t A :=
   (fst m, PTree.map f (snd m)).
 
@@ -1607,6 +1878,57 @@ Proof.
       econstructor. constructor; eauto.
 Qed.
 
+Lemma abstr_seq_revers_correct_fold_sem_pexpr_eval_inc :
+  forall G instrs p f l p' f' l' i0 sp ge preds preds' ps' lm lm',
+    (forall p, preds ! p = None -> sem_pexpr (mk_ctx i0 sp ge) (f #p p) ((is_ps i0) !! p)) ->
+    mfold_left update'_inc instrs (Some (p, f, l, lm)) = Some (p', f', l', lm') ->
+    mfold_left gather_predicates instrs (Some preds) = Some preds' ->
+    sem_predset (@mk_ctx G i0 sp ge) f' ps' ->
+    exists ps, sem_predset (mk_ctx i0 sp ge) f ps.
+Proof.
+  induction instrs.
+  - intros * YH **. cbn in *. inv H. inv H0. eauto.
+  - intros * YH **. cbn -[update remember_expr_inc remember_expr_m_inc] in *.
+    exploit OptionExtra.mfold_left_Some. apply H. intros [[[[p_mid f_mid] l_mid] lm_mid] HBIND].
+    exploit OptionExtra.mfold_left_Some. apply H0. intros [ptree_mid HGATHER].
+    rewrite HBIND in H. rewrite HGATHER in H0.
+    exploit IHinstrs. 3: { eauto. } 3: { eauto. } eapply update_rev_gather_constant_inc; eauto.
+    eauto. eauto.
+    intros [ps_mid HSEM_MID].
+    (* destruct (preds ! p0) eqn:?. destruct u. eapply gather_predicates_in in HGATHER; eauto. *)
+    (* rewrite HGATHER in H2. discriminate. *)
+    unfold Option.bind2, Option.bind, Option.ret in *; repeat destr. inv HBIND.
+    destruct a; cbn in *.
+    + inv Heqo. inv HGATHER. eauto.
+    + unfold Option.bind2, Option.bind, Option.ret in *; repeat destr.
+      generalize dependent Heqo; repeat destr; intros Heqo; inv Heqo.
+      inv HSEM_MID.
+      econstructor. constructor; eauto.
+    + unfold Option.bind2, Option.bind, Option.ret in *; repeat destr.
+      generalize dependent Heqo; repeat destr; intros Heqo; inv Heqo.
+      inv HSEM_MID.
+      econstructor. constructor; eauto.
+    + unfold Option.bind2, Option.bind, Option.ret in *; repeat destr.
+      generalize dependent Heqo; repeat destr; intros Heqo; inv Heqo.
+      inv HSEM_MID.
+      econstructor. constructor; eauto.
+    + unfold Option.bind2, Option.bind, Option.ret in *; repeat destr. inv HGATHER.
+      generalize dependent Heqo; repeat destr; intros Heqo; inv Heqo.
+      exists (mask_pred_map preds (is_ps i0) ps_mid).
+      econstructor; intros.
+      destruct (peq x p0); subst.
+      * destruct o; [assert (YX: preds ! p0 = None) by (eapply gather_predicates_fold3; eauto)|];
+          rewrite mask_pred_map_not_in_pred; auto.
+      * inv HSEM_MID. specialize (H2 x). rewrite forest_pred_gso in H2 by auto.
+        destruct (preds ! x) eqn:HDESTR.
+        -- destruct u3. now rewrite mask_pred_map_in_pred.
+        -- rewrite mask_pred_map_not_in_pred; auto.
+    + unfold Option.bind2, Option.bind, Option.ret in *; repeat destr.
+      generalize dependent Heqo; repeat destr; intros Heqo; inv Heqo.
+      inv HSEM_MID.
+      econstructor. constructor; eauto.
+Qed.
+
 (* [[id:5e6486bb-fda2-4558-aed8-243a9698de85]] *)
 Lemma abstr_seq_reverse_correct_fold :
   forall sp instrs i0 i i' ti cf f' l p p' l' f preds preds' lm lm' ps',
@@ -1795,6 +2117,346 @@ Proof.
         Unshelve. all: exact nil.
 Qed.
 
+Lemma eval_app_predicated :
+  forall G (ctx: @Abstr.ctx G) (a b: predicated expression) p f_p ps c,
+    (forall x0 : positive, sem_pexpr ctx (get_forest_p' x0 f_p) ps !! x0) ->
+    evaluable_pred_expr ctx f_p (app_predicated p c a) ->
+    evaluable_pred_expr ctx f_p b ->
+    evaluable_pred_expr ctx f_p (app_predicated p b a).
+Proof.
+  intros * HPred HEvalR HEvalL.
+  inv HEvalR. inv HEvalL.
+  case_eq (eval_predf ps p); intros.
+  - exists x. apply sem_pred_expr_app_predicated with (ps:=ps); auto.
+    eapply sem_pred_expr_app_predicated2; eauto.
+  - exists x0. apply sem_pred_expr_app_predicated_false with (ps:=ps); auto.
+Qed.
+
+Lemma eval_prune_predicated :
+  forall G (ctx: @Abstr.ctx G) (a b: predicated expression) f_p ps,
+    (forall x0 : positive, sem_pexpr ctx (get_forest_p' x0 f_p) ps !! x0) ->
+    prune_predicated a = Some b ->
+    evaluable_pred_expr ctx f_p a ->
+    evaluable_pred_expr ctx f_p b.
+Proof.
+  intros * HPred Hprune HEval. inv HEval.
+  exists x. eapply sem_pred_expr_prune_predicated; eauto.
+Qed.
+
+Lemma eval_app_predicated_m :
+  forall G (ctx: @Abstr.ctx G) (a b: predicated expression) p f_p ps c,
+    (forall x0 : positive, sem_pexpr ctx (get_forest_p' x0 f_p) ps !! x0) ->
+    evaluable_pred_expr_m ctx f_p (app_predicated p c a) ->
+    evaluable_pred_expr_m ctx f_p b ->
+    evaluable_pred_expr_m ctx f_p (app_predicated p b a).
+Proof.
+  intros * HPred HEvalR HEvalL.
+  inv HEvalR. inv HEvalL.
+  case_eq (eval_predf ps p); intros.
+  - exists x. apply sem_pred_expr_app_predicated with (ps:=ps); auto.
+    eapply sem_pred_expr_app_predicated2; eauto.
+  - exists x0. apply sem_pred_expr_app_predicated_false with (ps:=ps); auto.
+Qed.
+
+Lemma eval_prune_predicated_m :
+  forall G (ctx: @Abstr.ctx G) (a b: predicated expression) f_p ps,
+    (forall x0 : positive, sem_pexpr ctx (get_forest_p' x0 f_p) ps !! x0) ->
+    prune_predicated a = Some b ->
+    evaluable_pred_expr_m ctx f_p a ->
+    evaluable_pred_expr_m ctx f_p b.
+Proof.
+  intros * HPred Hprune HEval. inv HEval.
+  exists x. eapply sem_pred_expr_prune_predicated; eauto.
+Qed.
+
+Lemma eval_forest_update_inc :
+  forall sp i i0 p p' f f' l l' lm lm' f_p ps,
+    (forall x0 : positive, sem_pexpr (mk_ctx i0 sp ge) (get_forest_p' x0 f_p) ps !! x0) ->
+    update'_inc (p, f, l, lm) i = Some (p', f', l', lm') ->
+    evaluable_pred_list (mk_ctx i0 sp ge) f_p l' ->
+    evaluable_pred_list_m (mk_ctx i0 sp ge) f_p lm' ->
+    evaluable_forest (mk_ctx i0 sp ge) f_p f ->
+    evaluable_forest (mk_ctx i0 sp ge) f_p f'.
+Proof.
+  destruct i; intros * Hpred **; cbn -[app_predicated seq_app] in *; unfold Option.ret, Option.bind2, Option.bind in *; repeat (destruct_match; try easy; []).
+  - inv H; auto.
+  - inv H. inv Heqo1. inv H2.
+    constructor.
+    2: {
+      inv H3. exists x. rewrite forest_reg_gso by discriminate. auto.
+    }
+    intro x. destruct (peq x r); subst.
+    2: {
+      rewrite forest_reg_gso; auto. unfold not; intros. inv H2. contradiction.
+    }
+    rewrite forest_reg_gss.
+    unfold evaluable_pred_list in *.
+    exploit eval_app_predicated. eauto. eapply H0. constructor. eauto.
+    eapply H. instantiate (1:=r). intros.
+    eapply eval_prune_predicated; eauto.
+  - inv H. inv Heqo0. inv H2.
+    constructor.
+    2: {
+      inv H3. exists x. rewrite forest_reg_gso by discriminate. auto.
+    }
+    intro x. destruct (peq x r); subst.
+    2: {
+      rewrite forest_reg_gso; auto. unfold not; intros. inv H2. contradiction.
+    }
+    rewrite forest_reg_gss.
+    unfold evaluable_pred_list in *.
+    exploit eval_app_predicated. eauto. eapply H0. constructor. eauto.
+    eapply H. instantiate (1:=r). intros.
+    eapply eval_prune_predicated; eauto.
+  - inv Heqo0. inv H. inv H2.
+    constructor; intros.
+    rewrite forest_reg_gso by discriminate. auto.
+    rewrite forest_reg_gss. 
+    exploit eval_app_predicated_m. eauto. apply H1. constructor. eauto.
+    apply H3.
+    intros. eapply eval_prune_predicated_m; eauto.
+  - inv Heqo0. inv H. inv H2. constructor; intros; rewrite forest_pred_reg; eauto.
+  - inv Heqo0. inv H. inv H2. constructor; intros; rewrite forest_exit_regs; auto.
+Qed.
+
+Lemma abstr_seq_reverse_correct_fold_inc :
+  forall sp instrs i0 i i' ti cf f' l p p' l' f preds preds' lm lm' ps',
+    (forall in_pred, PredIn in_pred p -> preds ! in_pred = Some tt) ->
+    (forall p : positive, preds ! p = None -> sem_pexpr (mk_ctx i0 sp ge) f #p p (is_ps i0) !! p) ->
+    valid_mem (is_mem i0) (is_mem i) ->
+    all_preds_in f preds ->
+    eval_predf (is_ps i) p = true ->
+    sem (mk_ctx i0 sp ge) f (i, None) ->
+    mfold_left update'_inc instrs (Some (p, f, l, lm)) = Some (p', f', l', lm') ->
+    mfold_left gather_predicates instrs (Some preds) = Some preds' ->
+    evaluable_pred_list (mk_ctx i0 sp ge) f'.(forest_preds) l' ->
+    evaluable_pred_list_m (mk_ctx i0 sp ge) f'.(forest_preds) lm' ->
+    sem_predset (mk_ctx i0 sp ge) f' ps' ->
+    sem (mk_ctx i0 sp ge) f' (i', Some cf) ->
+    state_lessdef i ti ->
+    evaluable_forest (mk_ctx i0 sp ge) f'.(forest_preds) f ->
+    exists ti',
+      SeqBB.step ge sp (Iexec ti) instrs (Iterm ti' cf)
+      /\ state_lessdef i' ti'.
+Proof.
+  induction instrs; intros * YPREDSIN YPREDNONE YVALID YALL YEVAL Y3 Y YGATHER Y0 YEVALUABLE YSEM_FINAL Y1 Y2 HEval.
+  - cbn in *. inv Y.
+    assert (X: similar {| ctx_is := i0; ctx_sp := sp; ctx_ge := ge |}
+                       {| ctx_is := i0; ctx_sp := sp; ctx_ge := ge |})
+      by reflexivity.
+    now eapply sem_det in X; [| exact Y1 | exact Y3 ].
+  - cbn -[update'_inc] in Y.
+    pose proof Y as YX.
+    apply OptionExtra.mfold_left_Some in YX. inv YX.
+    cbn in YGATHER.
+    pose proof YGATHER as YX.
+    apply OptionExtra.mfold_left_Some in YX. inv YX. rewrite H0 in YGATHER.
+    pose proof H0 as YGATHER_SINGLE. clear H0.
+    rewrite H in Y.
+    destruct x as ((p_mid & f_mid) & l_mid).
+    pose proof H as Hupdate'_inc.
+    unfold update'_inc, Option.bind2, Option.ret in H. repeat destr.
+    inv H.
+
+    destruct a.
+    + cbn in Heqo. inv Heqo. cbn in YGATHER_SINGLE. inv YGATHER_SINGLE.
+      exploit IHinstrs; eauto; simplify.
+      exists x; split; auto. econstructor. constructor. auto.
+    + exploit evaluable_pred_expr_exists_RBop; eauto.
+      eapply abstr_seq_revers_correct_fold_sem_pexpr_eval2_inc; eauto.
+      (* unfold evaluable_pred_list in Y0. eapply in_forest_evaluable; eauto. *)
+      inv YSEM_FINAL.
+      eapply eval_forest_update_inc; eauto.
+      unfold evaluable_pred_list. intros. eapply Y0.
+      eapply in_mfold_left_abstr_inc; eauto.
+      unfold evaluable_pred_list_m. intros. eapply YEVALUABLE.
+      eapply in_mfold_left_abstr_m_inc; eauto.
+      eapply gather_predicates_in_forest in YALL; eauto.
+      unfold all_preds_in in YALL. eauto.
+      intros [ti_mid HSTEP].
+
+      pose proof Y3 as YH.
+      pose proof HSTEP as YHSTEP.
+      pose proof Y2 as Y2SPLIT; inv Y2SPLIT.
+      eapply step_exists in YHSTEP.
+      2: { symmetry. econstructor; try eassumption; auto. }
+      inv YHSTEP. inv H1.
+      exploit sem_update_instr. auto. eauto. eauto. eauto. eauto. auto. intros.
+      exploit IHinstrs. 6: { eauto. } eapply gather_predicates_update_constant; eauto.
+      eapply update_rev_gather_constant; eauto.
+      unfold update', Option.bind2, Option.ret. rewrite Heqo; auto.
+      cbn in YVALID. transitivity m'; auto.
+      replace m' with (is_mem {| is_rs := rs; Gible.is_ps := ps; Gible.is_mem := m' |}) by auto.
+      eapply sem_update_valid_mem; eauto.
+      eapply gather_predicates_in_forest; eauto.
+      eapply eval_predf_update_true; eauto.
+      eauto. eauto. eauto. eauto. eauto. eauto. symmetry.
+      eapply state_lessdef_state_equiv; eauto.
+      inv YSEM_FINAL. eapply eval_forest_update_inc; eauto.
+      unfold evaluable_pred_list. intros. eapply Y0.
+      eapply in_mfold_left_abstr_inc; eauto.
+      unfold evaluable_pred_list_m. intros. eapply YEVALUABLE.
+      eapply in_mfold_left_abstr_m_inc; eauto.
+      intros [ti' [YHH HLD]].
+      exists ti'; split; eauto. econstructor; eauto.
+    + exploit evaluable_pred_expr_exists_RBload; eauto.
+      eapply abstr_seq_revers_correct_fold_sem_pexpr_eval2_inc; eauto.
+      inv YSEM_FINAL.
+      eapply eval_forest_update_inc; eauto.
+      unfold evaluable_pred_list. intros. eapply Y0.
+      eapply in_mfold_left_abstr_inc; eauto.
+      unfold evaluable_pred_list_m. intros. eapply YEVALUABLE.
+      eapply in_mfold_left_abstr_m_inc; eauto.
+      eapply gather_predicates_in_forest in YALL; eauto.
+      unfold all_preds_in in YALL. eauto.
+      intros [ti_mid HSTEP].
+
+      pose proof Y3 as YH.
+      pose proof HSTEP as YHSTEP.
+      pose proof Y2 as Y2SPLIT; inv Y2SPLIT.
+      eapply step_exists in YHSTEP.
+      2: { symmetry. econstructor; try eassumption; auto. }
+      inv YHSTEP. inv H1.
+      exploit sem_update_instr. auto. eauto. eauto. eauto. eauto. auto. intros.
+      exploit IHinstrs. 6: { eauto. } eapply gather_predicates_update_constant; eauto.
+      eapply update_rev_gather_constant; eauto.
+      unfold update', Option.bind2, Option.ret. rewrite Heqo; auto.
+      cbn in YVALID. transitivity m'; auto.
+      replace m' with (is_mem {| is_rs := rs; Gible.is_ps := ps; Gible.is_mem := m' |}) by auto.
+      eapply sem_update_valid_mem; eauto.
+      eapply gather_predicates_in_forest; eauto.
+      eapply eval_predf_update_true; eauto.
+      eauto. eauto. eauto. eauto. eauto. eauto. symmetry.
+      eapply state_lessdef_state_equiv; eauto.
+      inv YSEM_FINAL. eapply eval_forest_update_inc; eauto.
+      unfold evaluable_pred_list. intros. eapply Y0.
+      eapply in_mfold_left_abstr_inc; eauto.
+      unfold evaluable_pred_list_m. intros. eapply YEVALUABLE.
+      eapply in_mfold_left_abstr_m_inc; eauto.
+      intros [ti' [YHH HLD]].
+      exists ti'; split; eauto. econstructor; eauto.
+    + exploit evaluable_pred_expr_exists_RBstore; eauto.
+      eapply abstr_seq_revers_correct_fold_sem_pexpr_eval4_inc; eauto.
+
+      inv YSEM_FINAL.
+      eapply eval_forest_update_inc; eauto.
+      unfold evaluable_pred_list. intros. eapply Y0.
+      eapply in_mfold_left_abstr_inc; eauto.
+      unfold evaluable_pred_list_m. intros. eapply YEVALUABLE.
+      eapply in_mfold_left_abstr_m_inc; eauto.
+
+      eapply gather_predicates_in_forest in YALL; eauto.
+      unfold all_preds_in in YALL. eauto.
+      intros [ti_mid HSTEP].
+
+      pose proof Y3 as YH.
+      pose proof HSTEP as YHSTEP.
+      pose proof Y2 as Y2SPLIT; inv Y2SPLIT.
+      eapply step_exists in YHSTEP.
+      2: { symmetry. econstructor; try eassumption; auto. }
+      inv YHSTEP. inv H1.
+      exploit sem_update_instr. auto. eauto. eauto. eauto. eauto. auto. intros.
+      exploit IHinstrs. 6: { eauto. } eapply gather_predicates_update_constant; eauto.
+      eapply update_rev_gather_constant; eauto.
+      unfold update', Option.bind2, Option.ret. rewrite Heqo; auto.
+      cbn in YVALID. transitivity m'; auto.
+      replace m' with (is_mem {| is_rs := rs; Gible.is_ps := ps; Gible.is_mem := m' |}) by auto.
+      eapply sem_update_valid_mem; eauto.
+      eapply gather_predicates_in_forest; eauto.
+      eapply eval_predf_update_true; eauto.
+      eauto. eauto. eauto. eauto. eauto. eauto. symmetry.
+      eapply state_lessdef_state_equiv; eauto.
+
+      inv YSEM_FINAL. eapply eval_forest_update_inc; eauto.
+      unfold evaluable_pred_list. intros. eapply Y0.
+      eapply in_mfold_left_abstr_inc; eauto.
+      unfold evaluable_pred_list_m. intros. eapply YEVALUABLE.
+      eapply in_mfold_left_abstr_m_inc; eauto.
+
+      intros [ti' [YHH HLD]].
+      exists ti'; split; eauto. econstructor; eauto.
+    + exploit abstr_seq_revers_correct_fold_sem_pexpr_eval_inc.
+      2: { eauto. }
+      eapply update_rev_gather_constant; eauto.
+      unfold update', Option.bind2, Option.ret. rewrite Heqo; auto.
+      eauto.
+      eauto.
+      intros [ps_mid HPRED2].
+      exploit evaluable_pred_expr_exists_RBsetpred; eauto.
+      intros [ti_mid HSTEP].
+
+      pose proof Y3 as YH.
+      pose proof HSTEP as YHSTEP.
+      pose proof Y2 as Y2SPLIT; inv Y2SPLIT.
+      eapply step_exists in YHSTEP.
+      2: { symmetry. econstructor; try eassumption; auto. }
+      inv YHSTEP. inv H1.
+      exploit sem_update_instr. auto. eauto. eauto. eauto. eauto. auto. intros.
+      exploit IHinstrs. 6: { eauto. } eapply gather_predicates_update_constant; eauto.
+      eapply update_rev_gather_constant; eauto.
+      unfold update', Option.bind2, Option.ret. rewrite Heqo; auto.
+      cbn in YVALID. transitivity m'; auto.
+      replace m' with (is_mem {| is_rs := rs; Gible.is_ps := ps; Gible.is_mem := m' |}) by auto.
+      eapply sem_update_valid_mem; eauto.
+      eapply gather_predicates_in_forest; eauto.
+      eapply eval_predf_update_true; eauto.
+      eauto. eauto. eauto. eauto. eauto. eauto. symmetry.
+      eapply state_lessdef_state_equiv; eauto.
+
+      inv YSEM_FINAL. eapply eval_forest_update_inc; eauto.
+      unfold evaluable_pred_list. intros. eapply Y0.
+      eapply in_mfold_left_abstr_inc; eauto.
+      unfold evaluable_pred_list_m. intros. eapply YEVALUABLE.
+      eapply in_mfold_left_abstr_m_inc; eauto.
+
+      intros [ti' [YHH HLD]].
+      exists ti'; split; eauto. econstructor; eauto.
+    + case_eq (eval_predf (is_ps i) (dfltp o)); intros.
+      * exploit evaluable_pred_expr_exists_RBexit2; eauto; intros HSTEP.
+        instantiate (1:=c) in HSTEP.
+        instantiate (1:=sp) in HSTEP.
+        exploit evaluable_pred_expr_exists_RBexit3. eauto. eauto. intros.
+        pose proof (state_lessdef_state_equiv i ti). inv H1.
+        specialize (H2 Y2).
+        pose proof (step_exists_Iterm ge sp ti _ i _ HSTEP
+                      ltac:(symmetry; assumption)).
+        exploit sem_update_instr_term; eauto; intros. inv H4.
+        exploit abstr_fold_falsy; auto. eauto. eapply equiv_update_inc; eauto. cbn. auto.
+        intros. eapply sem_det in Y1; eauto. inv Y1. inv H7.
+        eexists. split. constructor. eauto. transitivity i.
+        symmetry; auto. auto. reflexivity.
+      * exploit evaluable_pred_expr_exists_RBexit; eauto; intros HSTEP.
+        instantiate (1:=c) in HSTEP. instantiate (1:=sp) in HSTEP.
+        pose proof Y3 as YH.
+        pose proof HSTEP as YHSTEP.
+        pose proof Y2 as Y2SPLIT; inv Y2SPLIT.
+        eapply step_exists in YHSTEP.
+        2: { symmetry. econstructor; try eassumption; auto. }
+        inv YHSTEP. inv H2.
+        exploit sem_update_instr. auto. eauto. eauto. eauto. eapply Heqo. eauto. auto. intros.
+        exploit IHinstrs. 6: { eauto. } eapply gather_predicates_update_constant; eauto.
+        eapply update_rev_gather_constant; eauto.
+        unfold update', Option.bind2, Option.ret. rewrite Heqo; auto.
+        cbn in YVALID. transitivity m'; auto.
+        replace m' with (is_mem {| is_rs := rs; Gible.is_ps := ps; Gible.is_mem := m' |}) by auto.
+        cbn. inv H4.
+        reflexivity.
+        eapply gather_predicates_in_forest; eauto.
+        eapply eval_predf_update_true; eauto.
+        eauto. eauto. eauto. eauto. eauto. eauto. symmetry.
+        eapply state_lessdef_state_equiv; eauto.
+
+      inv YSEM_FINAL. eapply eval_forest_update_inc; eauto.
+      unfold evaluable_pred_list. intros. eapply Y0.
+      eapply in_mfold_left_abstr_inc; eauto.
+      unfold evaluable_pred_list_m. intros. eapply YEVALUABLE.
+      eapply in_mfold_left_abstr_m_inc; eauto.
+
+        intros [ti' [YHH HLD]].
+        exists ti'; split; eauto. econstructor; eauto.
+        Unshelve. all: exact nil.
+Qed.
+
 Lemma sem_empty :
   forall G (ctx: @Abstr.ctx G),
     sem ctx empty (ctx_is ctx, None).
@@ -1834,6 +2496,32 @@ Proof.
   intros; repeat constructor.
 Qed.
 
+Lemma abstr_seq_reverse_correct_inc:
+  forall sp x i i' ti cf x' l lm,
+    abstract_sequence'_inc x = Some (x', l, lm) ->
+    evaluable_pred_list (mk_ctx i sp ge) x'.(forest_preds) l ->
+    evaluable_pred_list_m (mk_ctx i sp ge) x'.(forest_preds) lm ->
+    sem (mk_ctx i sp ge) x' (i', (Some cf)) ->
+    state_lessdef i ti ->
+   exists ti', SeqBB.step ge sp (Iexec ti) x (Iterm ti' cf)
+           /\ state_lessdef i' ti'.
+Proof.
+  intros. unfold abstract_sequence'_inc in H.
+  unfold Option.map, Option.bind in H. repeat destr. inv H. inv Heqo.
+  pose proof H2 as X. inv X.
+  eapply abstr_seq_reverse_correct_fold_inc;
+    try eassumption; try reflexivity; auto using sem_empty, all_preds_in_empty.
+  inversion 1.
+  intros; repeat constructor.
+  unfold evaluable_forest; split.
+  - intros. unfold "#r". cbn. rewrite RTree.gempty. 
+    unfold evaluable_pred_expr. eexists. constructor. constructor.
+    constructor.
+  - intros. unfold "#r". cbn. rewrite RTree.gempty. 
+    unfold evaluable_pred_expr_m. eexists. constructor. constructor.
+    constructor.
+Qed.
+
 (*|
 Proof Sketch:
 
diff --git a/src/hls/PrintAbstr.ml b/src/hls/PrintAbstr.ml
index e1341b1..857b89c 100644
--- a/src/hls/PrintAbstr.ml
+++ b/src/hls/PrintAbstr.ml
@@ -81,9 +81,22 @@ let print_forest_exit pp f =
   fprintf pp "------------------- Exit  -------------------\n";
   print_predicated_exit pp f
 
+let print_evaluability_list pp = function
+  | [] -> ()
+  | r -> (fprintf pp "------------------- Eval  -------------------\n";
+          fprintf pp "["; List.iter (fun x -> fprintf pp "%a = %a\n" res (fst x) print_predicated (snd x)) r; fprintf pp "]";
+         )
+
+let print_evaluability_list2 pp = function
+  | [] -> ()
+  | r -> (fprintf pp "------------------- Eval2 -------------------\n";
+          fprintf pp "["; List.iter (fun x -> fprintf pp "%a\n" print_predicated x) r; fprintf pp "]";
+         )
+
 let print_forest pp f =
   fprintf pp "#############################################\n";
   fprintf pp "%a\n%a\n%a\n"
     print_forest_regs f.forest_regs
     print_forest_preds f.forest_preds
     print_forest_exit f.forest_exit
+