Prove evaluable_pred_expr_exists_RBsetpred

1 files changed, 474 insertions, 83 deletions

diff --git a/src/hls/GiblePargenproofBackward.v b/src/hls/GiblePargenproofBackward.v
index b6e79a1..911cd9b 100644
--- a/src/hls/GiblePargenproofBackward.v
+++ b/src/hls/GiblePargenproofBackward.v
@@ -89,13 +89,55 @@ Lemma sem_exists_execution :
     exists ti', SeqBB.step ge sp (Iexec ti) x (Iterm ti' cf).
 Proof. Admitted. *)
 
-Definition update' (s: pred_op * forest * list pred_expr) (i: instr): option (pred_op * forest * list pred_expr) :=
-  let '(p, f, l) := s in
-  Option.bind2 (fun p' f' => Option.ret (p', f', remember_expr f l i)) (update (p, f) i).
+Definition remember_expr (f : forest) (lst: list pred_expr) (i : instr): list pred_expr :=
+  match i with
+  | RBnop => lst
+  | RBop p op rl r => (f #r (Reg r)) :: lst
+  | RBload  p chunk addr rl r => (f #r (Reg r)) :: lst
+  | RBstore p chunk addr rl r => lst
+  | RBsetpred p' c args p => lst
+  | RBexit p c => lst
+  end.
 
-Definition abstract_sequence' (b : list instr) : option (forest * list pred_expr) :=
-  Option.map (fun x => let '(_, y, z) := x in (y, z))
-    (mfold_left update' b (Some (Ptrue, empty, nil))).
+Definition remember_expr_m (f : forest) (lst: list pred_expr) (i : instr): list pred_expr :=
+  match i with
+  | RBnop => lst
+  | RBop p op rl r => lst
+  | RBload  p chunk addr rl r => lst
+  | RBstore p chunk addr rl r => (f #r Mem) :: 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 gather_predicates (preds : PTree.t unit) (i : instr): option (PTree.t unit) :=
+  match i with
+  | RBop (Some p) _ _ _
+  | RBload (Some p) _ _ _ _
+  | RBstore (Some p) _ _ _ _
+  | RBexit (Some p) _ =>
+    Some (fold_right (fun x => PTree.set x tt) preds (predicate_use p))
+  | RBsetpred p' c args p =>
+    let preds' := match p' with
+                  | Some p'' => fold_right (fun x => PTree.set x tt) preds (predicate_use p'')
+                  | None => preds
+                  end
+    in
+    match preds' ! p with
+    | Some _ => None
+    | None => Some preds'
+    end
+  | _ => Some preds
+  end.
+
+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 i_state (s: istate): instr_state :=
   match s with
@@ -110,14 +152,21 @@ Definition cf_state (s: istate): option cf_instr :=
   end.
 
 Definition evaluable_pred_expr {G} (ctx: @Abstr.ctx G) pr p :=
-  exists r,
-      sem_pred_expr pr sem_value ctx p r.
+  exists r, sem_pred_expr pr sem_value ctx p r.
+
+Definition evaluable_pred_expr_m {G} (ctx: @Abstr.ctx G) pr p :=
+  exists r, sem_pred_expr pr sem_mem ctx p r.
 
 Definition evaluable_pred_list {G} ctx pr l :=
   forall p,
     In p l ->
     @evaluable_pred_expr G ctx pr p.
 
+Definition evaluable_pred_list_m {G} ctx pr l :=
+  forall p,
+    In p l ->
+    @evaluable_pred_expr_m G ctx pr p.
+
 (* Lemma evaluable_pred_expr_exists : *)
 (*   forall sp pr f i0 exit_p exit_p' f' cf i ti p op args dst, *)
 (*     update (exit_p, f) (RBop p op args dst) = Some (exit_p', f') -> *)
@@ -130,7 +179,7 @@ Definition evaluable_pred_list {G} ctx pr l :=
 (*   destruct ti. econstructor. econstructor. *)
 (*   unfold evaluable_pred_expr in H1. Admitted. *)
 
-Lemma evaluable_pred_expr_exists :
+Lemma evaluable_pred_expr_exists_RBop :
   forall sp f i0 exit_p exit_p' f' i ti p op args dst,
     eval_predf (is_ps i) exit_p = true ->
     valid_mem (is_mem i0) (is_mem i) ->
@@ -186,6 +235,209 @@ Proof.
     now erewrite <- eval_predf_pr_equiv by exact H0.
 Qed.
 
+Lemma evaluable_pred_expr_exists_RBload :
+  forall sp f i0 exit_p exit_p' f' i ti p chunk addr args dst,
+    eval_predf (is_ps i) exit_p = true ->
+    valid_mem (is_mem i0) (is_mem i) ->
+    update (exit_p, f) (RBload p chunk addr args dst) = Some (exit_p', f') ->
+    sem (mk_ctx i0 sp ge) f (i, None) ->
+    evaluable_pred_expr (mk_ctx i0 sp ge) f'.(forest_preds) (f' #r (Reg dst)) ->
+    state_lessdef i ti ->
+    exists ti',
+      step_instr ge sp (Iexec ti) (RBload p chunk addr args dst) (Iexec ti').
+Proof.
+  intros * HEVAL VALID_MEM **. cbn -[seq_app] in H. unfold Option.bind in H. destr. inv H.
+  assert (HPRED': sem_predset {| ctx_is := i0; ctx_sp := sp; ctx_ge := ge |} f (is_ps i))
+    by now inv H0.
+  inversion_clear HPRED' as [? ? ? HPRED].
+  destruct ti as [is_trs is_tps is_tm].
+  unfold evaluable_pred_expr in H1. destruct H1 as (r & Heval).
+  rewrite forest_reg_gss in Heval.
+  exploit sem_pred_expr_prune_predicated2; eauto; intros.
+  pose proof (truthy_dec (is_ps i) p) as YH. inversion_clear YH as [YH'|YH'].
+  - assert (eval_predf (is_ps i) (dfltp p ∧ exit_p') = true).
+    { pose proof (truthy_dflt _ _ YH'). rewrite eval_predf_Pand.
+      rewrite H1. now rewrite HEVAL. }
+    exploit sem_pred_expr_app_predicated2; eauto; intros.
+    exploit sem_pred_expr_seq_app_val2; eauto; simplify.
+    exploit sem_pred_expr_seq_app_val2; eauto; simplify.
+    unfold pred_ret in *. inv H6. inv H15. clear H13. inv H10.
+    destruct i as [is_rs_1 is_ps_1 is_m_1]. exploit sem_merge_list; eauto; intros.
+    instantiate (1 := args) in H6.
+    eapply sem_pred_expr_ident2 in H6. simplify.
+    exploit sem_pred_expr_ident_det. eapply H8. eapply H6.
+    intros. subst. inv H7.
+    eapply sem_val_list_det in H10; eauto; [|reflexivity]. subst.
+    cbn in *. inv H2.
+    econstructor. econstructor; eauto.
+    + erewrite <- match_states_list; eauto.
+    + inv H0. exploit sem_pred_expr_ident. eapply H5. eapply H15. intros.
+      eapply sem_pred_expr_det in H0. rewrite H0. eassumption.
+      reflexivity. eapply sem_mem_det. reflexivity. auto.
+    + inv H0.
+      assert (sem_predset {| ctx_is := i0; ctx_sp := sp; ctx_ge := ge |} f (is_ps_1))
+        by (now constructor).
+      pose proof (sem_predset_det _ _ ltac:(reflexivity) _ _ _ H0 H20).
+      assert (truthy is_ps_1 p).
+      { eapply truthy_match_state; eassumption. }
+      eapply truthy_match_state; eassumption.
+  - inv YH'. cbn -[seq_app] in H.
+    assert (eval_predf (is_ps i) (p0 ∧ exit_p') = false).
+    { rewrite eval_predf_Pand. now rewrite H1. }
+    eapply sem_pred_expr_app_predicated_false2 in H; eauto.
+    eexists. eapply exec_RB_falsy. constructor. auto. cbn.
+    assert (sem_predset {| ctx_is := i0; ctx_sp := sp; ctx_ge := ge |} f (is_ps i))
+        by (now constructor).
+    inv H0. pose proof (sem_predset_det _ _ ltac:(reflexivity) _ _ _ H4 H8).
+    inv H2.
+    erewrite <- eval_predf_pr_equiv by exact H16.
+    now erewrite <- eval_predf_pr_equiv by exact H0.
+Qed.
+
+Lemma evaluable_pred_expr_exists_RBstore :
+  forall sp f i0 exit_p exit_p' f' i ti p chunk addr args src,
+    eval_predf (is_ps i) exit_p = true ->
+    valid_mem (is_mem i0) (is_mem i) ->
+    update (exit_p, f) (RBstore p chunk addr args src) = Some (exit_p', f') ->
+    sem (mk_ctx i0 sp ge) f (i, None) ->
+    evaluable_pred_expr_m (mk_ctx i0 sp ge) f'.(forest_preds) (f' #r Mem) ->
+    state_lessdef i ti ->
+    exists ti',
+      step_instr ge sp (Iexec ti) (RBstore p chunk addr args src) (Iexec ti').
+Proof.
+  intros * HEVAL VALID_MEM **. cbn -[seq_app] in H. unfold Option.bind in H. destr. inv H.
+  assert (HPRED': sem_predset {| ctx_is := i0; ctx_sp := sp; ctx_ge := ge |} f (is_ps i))
+    by now inv H0.
+  inversion_clear HPRED' as [? ? ? HPRED].
+  destruct ti as [is_trs is_tps is_tm].
+  unfold evaluable_pred_expr in H1. destruct H1 as (r & Heval).
+  rewrite forest_reg_gss in Heval.
+  exploit sem_pred_expr_prune_predicated2; eauto; intros.
+  pose proof (truthy_dec (is_ps i) p) as YH. inversion_clear YH as [YH'|YH'].
+  - assert (eval_predf (is_ps i) (dfltp p ∧ exit_p') = true).
+    { pose proof (truthy_dflt _ _ YH'). rewrite eval_predf_Pand.
+      rewrite H1. now rewrite HEVAL. }
+    exploit sem_pred_expr_app_predicated2; eauto; intros.
+    exploit sem_pred_expr_seq_app_val2; eauto; simplify.
+    exploit sem_pred_expr_seq_app_val2; eauto; simplify.
+    exploit sem_pred_expr_flap2_2; eauto; simplify.
+    exploit sem_pred_expr_seq_app_val2; eauto; simplify.
+    unfold pred_ret in *. inv H14. inv H11. inv H18. clear H16. inv H10. inv H7.
+    destruct i as [is_rs_1 is_ps_1 is_m_1]. exploit sem_merge_list; eauto; intros.
+    instantiate (1 := args) in H7.
+    eapply sem_pred_expr_ident2 in H7. simplify.
+    exploit sem_pred_expr_ident_det. eapply H8. eapply H7.
+    intros. subst.
+    eapply sem_val_list_det in H20; eauto; [|reflexivity]. subst.
+    cbn in *. inv H2. inv H0. inv H20. pose proof H0 as YH0. specialize (YH0 src).
+    exploit sem_pred_expr_ident. eapply H5. eauto. intros.
+    exploit sem_pred_expr_ident. eapply H12. eauto. intros.
+    eapply sem_pred_expr_det in H25; eauto; [|reflexivity|eapply sem_mem_det; reflexivity].
+    eapply sem_pred_expr_det in YH0; eauto; [|reflexivity|eapply sem_value_det; reflexivity].
+    subst.
+    econstructor. econstructor; eauto.
+    + erewrite <- match_states_list; eauto.
+    + rewrite <- H16. eassumption.
+    + assert (sem_predset {| ctx_is := i0; ctx_sp := sp; ctx_ge := ge |} f (is_ps_1))
+        by (now constructor).
+      pose proof (sem_predset_det _ _ ltac:(reflexivity) _ _ _ H24 H13).
+      assert (truthy is_ps_1 p).
+      { eapply truthy_match_state; eassumption. }
+      eapply truthy_match_state; eassumption.
+  - inv YH'. cbn -[seq_app] in H.
+    assert (eval_predf (is_ps i) (p0 ∧ exit_p') = false).
+    { rewrite eval_predf_Pand. now rewrite H1. }
+    eapply sem_pred_expr_app_predicated_false2 in H; eauto.
+    eexists. eapply exec_RB_falsy. constructor. auto. cbn.
+    assert (sem_predset {| ctx_is := i0; ctx_sp := sp; ctx_ge := ge |} f (is_ps i))
+        by (now constructor).
+    inv H0. pose proof (sem_predset_det _ _ ltac:(reflexivity) _ _ _ H4 H8).
+    inv H2.
+    erewrite <- eval_predf_pr_equiv by exact H16.
+    now erewrite <- eval_predf_pr_equiv by exact H0.
+Qed.
+
+Lemma evaluable_pred_expr_exists_RBsetpred :
+  forall sp f i0 exit_p exit_p' f' i ti p c args src ps',
+    eval_predf (is_ps i) exit_p = true ->
+    valid_mem (is_mem i0) (is_mem i) ->
+    update (exit_p, f) (RBsetpred p c args src) = Some (exit_p', f') ->
+    sem (mk_ctx i0 sp ge) f (i, None) ->
+    sem_predset (mk_ctx i0 sp ge) f' ps' ->
+    state_lessdef i ti ->
+    exists ti',
+      step_instr ge sp (Iexec ti) (RBsetpred p c args src) (Iexec ti').
+Proof.
+  intros * HEVAL VALID_MEM **. cbn -[seq_app] in H. unfold Option.bind in H. destr. inv H.
+  assert (HPRED': sem_predset {| ctx_is := i0; ctx_sp := sp; ctx_ge := ge |} f (is_ps i))
+    by now inv H0.
+  inversion_clear HPRED' as [? ? ? HPRED].
+  destruct ti as [is_trs is_tps is_tm]. destr. inv H4. inv H1.
+  pose proof H as YH. specialize (YH src). rewrite forest_pred_gss in YH.
+  inv YH; try inv H3.
+  + inv H1. inv H6. replace false with (negb true) in H4 by auto.
+    replace false with (negb true) in H8 by auto.
+    eapply sem_pexpr_negate2 in H4. eapply sem_pexpr_negate2 in H8.
+    destruct i.
+    exploit from_predicated_sem_pred_expr2; eauto; intros.
+    exploit sem_pred_expr_seq_app_val2. eapply HPRED. eauto. simplify.
+    inv H3. inv H15. clear H13.
+    exploit sem_merge_list; eauto; intros. instantiate (1:=args) in H3.
+    eapply sem_pred_expr_ident2 in H3; simplify. exploit sem_pred_expr_ident_det.
+    eapply H6. eauto. intros. subst.
+    intros. inv H10. eapply sem_val_list_det in H11; eauto. subst.
+    inv H2.
+    econstructor. econstructor. erewrite <- match_states_list; eauto.
+    erewrite <- storev_eval_condition; eauto.
+    assert (truthy is_ps p).
+    { destruct p. cbn in H4. constructor.
+      eapply sem_pexpr_forward_eval; eauto. constructor.
+    }
+    eapply truthy_match_state; eassumption.
+    reflexivity.
+  + inv H1. inv H6. inv H3.
+    * replace false with (negb true) in H1 by auto. eapply sem_pexpr_negate2 in H1.
+      eapply sem_pexpr_forward_eval in H1; eauto. rewrite eval_predf_negate in H1.
+      assert ((eval_predf (is_ps i) (dfltp p)) = false).
+      { replace false with (negb true) by auto. rewrite <- H1. now rewrite negb_involutive. }
+      econstructor. apply exec_RB_falsy. cbn. destruct p. constructor; auto. inv H2.
+      erewrite <- eval_predf_pr_equiv; eauto. now cbn in H3.
+    * replace false with (negb true) in H1 by auto. eapply sem_pexpr_negate2 in H1.
+      eapply sem_pexpr_forward_eval in H1; eauto. rewrite eval_predf_negate in H1.
+      now rewrite HEVAL in H1.
+  + inv H5. inv H3.
+    * inv H1. inv H5.
+      -- replace true with (negb false) in H1 by auto. eapply sem_pexpr_negate2 in H1.
+         eapply sem_pexpr_forward_eval in H1; eauto.
+         econstructor. apply exec_RB_falsy. cbn. destruct p. constructor; auto. inv H2.
+         erewrite <- eval_predf_pr_equiv; eauto. now cbn in H1.
+      -- replace true with (negb false) in H1 by auto. eapply sem_pexpr_negate2 in H1.
+         eapply sem_pexpr_forward_eval in H1; eauto. now rewrite HEVAL in H1.
+    * case_eq (eval_predf (is_ps i) (dfltp p)); intros.
+      -- eapply sem_pexpr_eval in H3; eauto.
+         destruct i.
+         exploit from_predicated_sem_pred_expr2; eauto; intros.
+         exploit sem_pred_expr_seq_app_val2. eapply HPRED. eauto. simplify.
+         inv H7. inv H15. clear H13.
+         exploit sem_merge_list; eauto; intros. instantiate (1:=args) in H7.
+         eapply sem_pred_expr_ident2 in H7; simplify. exploit sem_pred_expr_ident_det.
+         eapply H8. eauto. intros. subst.
+         inv H10. clear H8. eapply sem_val_list_det in H11; eauto. subst.
+         inv H2.
+         econstructor. econstructor. erewrite <- match_states_list; eauto.
+         erewrite <- storev_eval_condition; eauto.
+         assert (truthy is_ps p).
+         { destruct p. cbn in H4. constructor.
+           eapply sem_pexpr_forward_eval; eauto.
+           constructor.
+         }
+         eapply truthy_match_state; eassumption.
+         reflexivity.
+      -- econstructor. apply exec_RB_falsy.
+         destruct p. constructor. inv H2. erewrite <- eval_predf_pr_equiv; eauto.
+         easy.
+Qed.
+
 Lemma remember_expr_in :
   forall x l f a,
     In x l -> In x (remember_expr f l a).
@@ -193,9 +445,16 @@ Proof.
   unfold remember_expr; destruct a; 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.
+Qed.
+
 Lemma in_mfold_left_abstr :
-  forall instrs p f l p' f' l' x,
-    mfold_left update' instrs (Some (p, f, l)) = Some (p', f', l') ->
+  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') ->
     In x l -> In x l'.
 Proof.
   induction instrs; intros.
@@ -203,12 +462,28 @@ Proof.
   - 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).
+    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.
     auto using remember_expr_in.
 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') ->
+    In x lm -> In x lm'.
+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.
+    auto using remember_expr_in_m.
+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) ->
@@ -229,9 +504,23 @@ Proof.
     now rewrite forest_reg_gso by auto.
 Qed.
 
+Lemma not_remembered_in_forest_m :
+  forall a p f p_mid f_mid l,
+    update (p, f) a = Some (p_mid, f_mid) ->
+    ~ In f #r Mem (remember_expr_m f l a) ->
+    f #r Mem = f_mid #r Mem.
+Proof.
+  intros; destruct a; cbn in *;
+    unfold Option.bind in H; repeat destr; inv H; try easy.
+  - rewrite forest_reg_gso; auto. easy.
+  - rewrite forest_reg_gso; auto. easy.
+  - assert (~ (f #r Mem = f #r Mem) /\ ~ (In f #r Mem l)) by tauto. inv H.
+    contradiction.
+Qed.
+
 Lemma in_forest_or_remembered :
-  forall instrs p f l p' f' l',
-    mfold_left update' instrs (Some (p, f, l)) = Some (p', f', l') ->
+  forall instrs p f l p' f' l' lm lm',
+    mfold_left update' instrs (Some (p, f, l, lm)) = Some (p', f', l', lm') ->
     forall x, In (f #r (Reg x)) l' \/ f #r (Reg x) = f' #r (Reg x).
 Proof.
   induction instrs; try solve [crush]; []; intros.
@@ -239,8 +528,8 @@ Proof.
   pose proof H as YX.
   apply OptionExtra.mfold_left_Some in YX. inv YX.
   rewrite H0 in H.
-  destruct x0 as ((p_mid & f_mid) & l_mid).
-  pose proof (IHinstrs _ _ _ _ _ _ H).
+  destruct x0 as (((p_mid & f_mid) & l_mid) & lm_mid).
+  pose proof (IHinstrs _ _ _ _ _ _ _ _ H).
   unfold Option.bind2, Option.ret in H0; cbn -[update] in H0; repeat destr.
   inv H0. specialize (H1 x).
   pose proof H as Y.
@@ -250,9 +539,30 @@ Proof.
     rewrite n in *; tauto.
 Qed.
 
+Lemma in_forest_or_remembered_m :
+  forall instrs p f l p' f' l' lm lm',
+    mfold_left update' instrs (Some (p, f, l, lm)) = Some (p', f', l', lm') ->
+    In (f #r Mem) lm' \/ f #r Mem = f' #r Mem.
+Proof.
+  induction instrs; try solve [crush]; []; intros.
+  cbn -[update] in H.
+  pose proof H as YX.
+  apply OptionExtra.mfold_left_Some in YX. inv YX.
+  rewrite H0 in H.
+  destruct x as (((p_mid & f_mid) & l_mid) & lm_mid).
+  pose proof (IHinstrs _ _ _ _ _ _ _ _ H).
+  unfold Option.bind2, Option.ret in H0; cbn -[update] in H0; repeat destr.
+  inv H0.
+  pose proof H as Y.
+  destruct (in_dec pred_expr_eqb (f #r Mem) (remember_expr_m f lm a));
+    eauto using in_mfold_left_abstr_m.
+  inv H1; eapply not_remembered_in_forest_m with (f_mid := f_mid) in n; eauto;
+    rewrite n in *; tauto.
+Qed.
+
 Lemma in_forest_evaluable :
-  forall G sp ge i' cf instrs p f l p' f' l' x i0,
-    mfold_left update' instrs (Some (p, f, l)) = Some (p', f', l') ->
+  forall G sp ge i' cf instrs p f l p' f' l' x i0 lm lm',
+    mfold_left update' 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)).
@@ -264,37 +574,31 @@ Proof.
   unfold evaluable_pred_expr. eauto.
 Qed.
 
-Definition gather_predicates (preds : PTree.t unit) (i : instr): option (PTree.t unit) :=
-  match i with
-  | RBop (Some p) _ _ _
-  | RBload (Some p) _ _ _ _
-  | RBstore (Some p) _ _ _ _
-  | RBexit (Some p) _ =>
-    Some (fold_right (fun x => PTree.set x tt) preds (predicate_use p))
-  | RBsetpred p' c args p =>
-    let preds' := match p' with
-                  | Some p'' => fold_right (fun x => PTree.set x tt) preds (predicate_use p'')
-                  | None => preds
-                  end
-    in
-    match preds' ! p with
-    | Some _ => None
-    | None => Some preds'
-    end
-  | _ => Some preds
-  end.
+Lemma in_forest_evaluable_m :
+  forall G sp ge i' cf instrs p f l p' f' l' i0 lm lm',
+    mfold_left update' 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.
 
 Lemma abstr_seq_revers_correct_fold_sem_pexpr :
-  forall instrs p f l p' f' l' preds preds',
-    mfold_left update' instrs (Some (p, f, l)) = Some (p', f', l') ->
+  forall instrs p f l p' f' l' preds preds' lm lm',
+    mfold_left update' 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. Admitted.
 
 Lemma abstr_seq_revers_correct_fold_sem_pexpr_eval :
-  forall G instrs p f l p' f' l' i0 sp ge ps preds preds' ps',
-    mfold_left update' instrs (Some (p, f, l)) = Some (p', f', l') ->
+  forall G instrs p f l p' f' l' i0 sp ge ps preds preds' ps' lm lm',
+    mfold_left update' 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 ->
       sem_predset (mk_ctx i0 sp ge) f ps ->
@@ -302,9 +606,23 @@ Lemma abstr_seq_revers_correct_fold_sem_pexpr_eval :
       ps !! pred = ps' !! pred.
 Proof. Admitted.
 
+Definition all_preds_in f preds :=
+  (forall x, NE.Forall (fun x => forall pred, PredIn pred (fst x)
+                       -> PTree.get pred preds = Some tt) (f #r x))
+  /\ NE.Forall (fun x => forall pred, PredIn pred (fst x)
+                 -> PTree.get pred preds = Some tt) f.(forest_exit).
+
+Lemma gather_predicates_in_forest :
+  forall p i f p' f' preds preds',
+    update (p, f) i = Some (p', f') ->
+    gather_predicates preds i = Some preds' ->
+    all_preds_in f preds ->
+    all_preds_in f' preds'.
+Proof. Admitted.
+
 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,
-    mfold_left update' instrs (Some (p, f, l)) = Some (p', f', l') ->
+  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') ->
     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)
@@ -314,7 +632,7 @@ Proof.
   induction instrs; try solve [crush]; intros.
   cbn -[update] in *.
   exploit OptionExtra.mfold_left_Some. eapply H.
-  intros [[[p_mid f_mid] l_mid] HBind]. rewrite HBind in 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. eassumption. eassumption. eassumption. admit.
@@ -324,8 +642,8 @@ Proof.
 (*   intros [[p_val e_val] [HIN HSEM]]. *)
 
 Lemma abstr_seq_revers_correct_fold_sem_pexpr_eval2 :
-  forall G instrs p f l p' f' l' i0 sp ge preds preds' pe,
-    mfold_left update' instrs (Some (p, f, l)) = Some (p', f', l') ->
+  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') ->
     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)
@@ -337,21 +655,42 @@ Proof.
   eapply abstr_seq_revers_correct_fold_sem_pexpr_eval3; 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') ->
+    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; 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.
+
 (* [[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,
+  forall sp instrs i0 i i' ti cf f' l p p' l' f preds preds' lm lm',
     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' instrs (Some (p, f, l)) = Some (p', f', l') ->
+    mfold_left update' 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 (mk_ctx i0 sp ge) f' (i', Some cf) ->
     state_lessdef i ti ->
     exists ti',
       SeqBB.step ge sp (Iexec ti) instrs (Iterm ti' cf)
       /\ state_lessdef i' ti'.
 Proof.
-  induction instrs; intros * YVALID YEVAL Y3 Y Y0 Y1 Y2.
+  induction instrs; intros * YVALID YALL YEVAL Y3 Y YGATHER Y0 YEVALUABLE Y1 Y2.
   - 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 |})
@@ -360,36 +699,93 @@ Proof.
   - cbn -[update] 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).
     unfold Option.bind2, Option.ret in H. repeat destr.
     inv H.
 
-    (* Assume we are in RBop for now*)
-    assert (exists pred op args dst, a = RBop pred op args dst)
-      by admit; destruct H as (pred & op & args & dst & EQ); subst a.
-
-    exploit evaluable_pred_expr_exists; eauto.
-    eapply abstr_seq_revers_correct_fold_sem_pexpr_eval2; eauto. admit. admit.
-    admit.
-    
-    (* I have the pred already from sem. *)
-    intros [ti_mid HSTEP].
-    (* unfold evaluable_pred_list in Y0. *)
-    (* instantiate (1 := forest_preds f'). *)
-    (* eapply in_forest_evaluable; eauto. *)
-    (* (* provable using evaluability in list *) intros [t step]. *)
-
-    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. 3: { eauto. } admit. admit. eauto. admit. eauto. symmetry.
-    instantiate (1:=ti_mid). admit. intros [ti' [YHH HLD]].
-    exists ti'; split; eauto. econstructor; eauto.
+    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; eauto.
+      unfold evaluable_pred_list in Y0. eapply in_forest_evaluable; eauto.
+      eapply gather_predicates_in_forest in YALL; eauto.
+      unfold all_preds_in in YALL. inv 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. 4: { eauto. }
+      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. symmetry.
+      eapply state_lessdef_state_equiv; 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; eauto.
+      unfold evaluable_pred_list in Y0. eapply in_forest_evaluable; eauto.
+      eapply gather_predicates_in_forest in YALL; eauto.
+      unfold all_preds_in in YALL. inv 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. 4: { eauto. }
+      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. symmetry.
+      eapply state_lessdef_state_equiv; 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; eauto.
+      unfold evaluable_pred_list in Y0. eapply in_forest_evaluable_m; eauto.
+      eapply gather_predicates_in_forest in YALL; eauto.
+      unfold all_preds_in in YALL. inv 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. 4: { eauto. }
+      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. symmetry.
+      eapply state_lessdef_state_equiv; eauto.
+      intros [ti' [YHH HLD]].
+      exists ti'; split; eauto. econstructor; eauto.
+    + admit.
+    + admit.
 Admitted.
 
 Lemma sem_empty :
@@ -408,21 +804,16 @@ Qed.
 Lemma abstr_seq_reverse_correct:
   forall sp x i i' ti cf x' l,
     abstract_sequence' x = Some (x', l) ->
-    (forall p, In p l -> exists r, sem_pred_expr x'.(forest_preds) sem_value (mk_ctx i sp ge) p r) ->
+    evaluable_pred_list (mk_ctx i sp ge) x'.(forest_preds) l ->
     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. exploit sem_exists_execution; eauto; simplify.
-  eauto using sem_equiv_execution.
-Qed. *)
   intros. unfold abstract_sequence' in H.
-  unfold Option.map in H. repeat destr. inv H.
-  eapply  abstr_seq_reverse_correct_fold.
-  2: {  eauto. }
-  all: eauto.
-  apply sem_empty.
+  unfold Option.map, Option.bind in H. repeat destr. inv H. inv Heqo.
+  eapply abstr_seq_reverse_correct_fold;
+    try eassumption; try reflexivity; apply sem_empty.
 Qed.
 
 (*|