[sched] Remove some unprovable lemmas

1 files changed, 113 insertions, 842 deletions

diff --git a/src/hls/GiblePargenproof.v b/src/hls/GiblePargenproof.v
index bcc3fd0..05467ed 100644
--- a/src/hls/GiblePargenproof.v
+++ b/src/hls/GiblePargenproof.v
@@ -41,6 +41,9 @@ Import OptionExtra.
 #[local] Open Scope forest.
 #[local] Open Scope pred_op.
 
+#[local] Opaque simplify.
+#[local] Opaque deep_simplify.
+
 (*|
 ==============
 RTLPargenproof
@@ -110,457 +113,6 @@ Proof. induction l; crush. Qed.
 Lemma check_dest_l_dec i r : {check_dest_l i r = true} + {check_dest_l i r = false}.
 Proof. destruct (check_dest_l i r); tauto. Qed.
 
-(* Lemma check_dest_update : *)
-(*   forall f f' i r, *)
-(*   check_dest i r = false -> *)
-(*   update (Some f) i = Some f' -> *)
-(*   (snd f') # (Reg r) = (snd f) # (Reg r). *)
-(* Proof. *)
-(*   destruct i; crush; try apply Pos.eqb_neq in H; unfold update; destruct_match; crush. *)
-(*   inv Heqp. *)
-(*   Admitted. *)
-
-(* Lemma check_dest_l_forall2 : *)
-(*   forall l r, *)
-(*   Forall (fun x => check_dest x r = false) l -> *)
-(*   check_dest_l l r = false. *)
-(* Proof. *)
-(*   induction l; crush. *)
-(*   inv H. apply orb_false_intro; crush. *)
-(* Qed. *)
-
-(* Lemma check_dest_l_ex2 : *)
-(*   forall l r, *)
-(*   (exists a, In a l /\ check_dest a r = true) -> *)
-(*   check_dest_l l r = true. *)
-(* Proof. *)
-(*   induction l; crush. *)
-(*   specialize (IHl r). inv H. *)
-(*   apply orb_true_intro; crush. *)
-(*   apply orb_true_intro; crush. *)
-(*   right. apply IHl. exists x. auto. *)
-(* Qed. *)
-
-(* Lemma check_list_l_false : *)
-(*   forall l x r, *)
-(*   check_dest_l (l ++ x :: nil) r = false -> *)
-(*   check_dest_l l r = false /\ check_dest x r = false. *)
-(* Proof. *)
-(*   simplify. *)
-(*   apply check_dest_l_forall in H. apply Forall_app in H. *)
-(*   simplify. apply check_dest_l_forall2; auto. *)
-(*   apply check_dest_l_forall in H. apply Forall_app in H. *)
-(*   simplify. inv H1. auto. *)
-(* Qed. *)
-
-(* Lemma check_dest_l_ex : *)
-(*   forall l r, *)
-(*   check_dest_l l r = true -> *)
-(*   exists a, In a l /\ check_dest a r = true. *)
-(* Proof. *)
-(*   induction l; crush. *)
-(*   destruct (check_dest a r) eqn:?; try solve [econstructor; crush]. *)
-(*   simplify. *)
-(*   exploit IHl. apply H. simplify. econstructor. simplify. right. eassumption. *)
-(*   auto. *)
-(* Qed. *)
-
-(* Lemma check_list_l_true : *)
-(*   forall l x r, *)
-(*   check_dest_l (l ++ x :: nil) r = true -> *)
-(*   check_dest_l l r = true \/ check_dest x r = true. *)
-(* Proof. *)
-(*   simplify. *)
-(*   apply check_dest_l_ex in H; simplify. *)
-(*   apply in_app_or in H. inv H. left. *)
-(*   apply check_dest_l_ex2. exists x0. auto. *)
-(*   inv H0; auto. *)
-(* Qed. *)
-
-(* Lemma check_dest_l_dec2 l r : *)
-(*   {Forall (fun x => check_dest x r = false) l} *)
-(*   + {exists a, In a l /\ check_dest a r = true}. *)
-(* Proof. *)
-(*   destruct (check_dest_l_dec l r); [right | left]; *)
-(*   auto using check_dest_l_ex, check_dest_l_forall. *)
-(* Qed. *)
-
-(* Lemma abstr_comp : *)
-(*   forall l i f x x0, *)
-(*   fold_left update (l ++ i :: nil) f = x -> *)
-(*   fold_left update l f = x0 -> *)
-(*   x = update x0 i. *)
-(* Proof. induction l; intros; crush; eapply IHl; eauto. Qed. *)
-
-(*
-
-Lemma gen_list_base:
-  forall FF ge sp l rs exps st1,
-  (forall x, @sem_value FF ge sp st1 (exps # (Reg x)) (rs !! x)) ->
-  sem_val_list ge sp st1 (list_translation l exps) rs ## l.
-Proof.
-  induction l.
-  intros. simpl. constructor.
-  intros. simpl. eapply Scons; eauto.
-Qed.
-
-Lemma check_dest_update2 :
-  forall f r rl op p,
-  (update f (RBop p op rl r)) # (Reg r) = Eop op (list_translation rl f) (f # Mem).
-Proof. crush; rewrite map2; auto. Qed.
-
-Lemma check_dest_update3 :
-  forall f r rl p addr chunk,
-  (update f (RBload p chunk addr rl r)) # (Reg r) = Eload chunk addr (list_translation rl f) (f # Mem).
-Proof. crush; rewrite map2; auto. Qed.
-
-Lemma abstract_seq_correct_aux:
-  forall FF ge sp i st1 st2 st3 f,
-    @step_instr FF ge sp st3 i st2 ->
-    sem ge sp st1 f st3 ->
-    sem ge sp st1 (update f i) st2.
-Proof.
-  intros; inv H; simplify.
-  { simplify; eauto. } (*apply match_states_refl. }*)
-  { inv H0. inv H6. destruct st1. econstructor. simplify.
-    constructor. intros.
-    destruct (resource_eq (Reg res) (Reg x)). inv e.
-    rewrite map2. econstructor. eassumption. apply gen_list_base; eauto.
-    rewrite Regmap.gss. eauto.
-    assert (res <> x). { unfold not in *. intros. apply n. rewrite H0. auto. }
-    rewrite Regmap.gso by auto.
-    rewrite genmap1 by auto. auto.
-
-    rewrite genmap1; crush. }
-  { inv H0. inv H7. constructor. constructor. intros.
-    destruct (Pos.eq_dec dst x); subst.
-    rewrite map2. econstructor; eauto.
-    apply gen_list_base. auto. rewrite Regmap.gss. auto.
-    rewrite genmap1. rewrite Regmap.gso by auto. auto.
-    unfold not in *; intros. inv H0. auto.
-    rewrite genmap1; crush.
-  }
-  { inv H0. inv H7. constructor. constructor; intros.
-    rewrite genmap1; crush.
-    rewrite map2. econstructor; eauto.
-    apply gen_list_base; auto.
-  }
-Qed.
-
-Lemma regmap_list_equiv :
-  forall A (rs1: Regmap.t A) rs2,
-    (forall x, rs1 !! x = rs2 !! x) ->
-    forall rl, rs1##rl = rs2##rl.
-Proof. induction rl; crush. Qed.
-
-Lemma sem_update_Op :
-  forall A ge sp st f st' r l o0 o m rs v,
-  @sem A ge sp st f st' ->
-  Op.eval_operation ge sp o0 rs ## l m = Some v ->
-  match_states st' (mk_instr_state rs m) ->
-  exists tst,
-  sem ge sp st (update f (RBop o o0 l r)) tst /\ match_states (mk_instr_state (Regmap.set r v rs) m) tst.
-Proof.
-  intros. inv H1. simplify.
-  destruct st.
-  econstructor. simplify.
-  { constructor.
-    { constructor. intros. destruct (Pos.eq_dec x r); subst.
-      { pose proof (H5 r). rewrite map2. pose proof H. inv H. econstructor; eauto.
-        { inv H9. eapply gen_list_base; eauto. }
-        { instantiate (1 := (Regmap.set r v rs0)). rewrite Regmap.gss. erewrite regmap_list_equiv; eauto. } }
-      { rewrite Regmap.gso by auto. rewrite genmap1; crush. inv H. inv H7; eauto. } }
-    { inv H. rewrite genmap1; crush. eauto. } }
-  { constructor; eauto. intros.
-    destruct (Pos.eq_dec r x);
-    subst; [repeat rewrite Regmap.gss | repeat rewrite Regmap.gso]; auto. }
-Qed.
-
-Lemma sem_update_load :
-  forall A ge sp st f st' r o m a l m0 rs v a0,
-  @sem A ge sp st f st' ->
-  Op.eval_addressing ge sp a rs ## l = Some a0 ->
-  Mem.loadv m m0 a0 = Some v ->
-  match_states st' (mk_instr_state rs m0) ->
-  exists tst : instr_state,
-    sem ge sp st (update f (RBload o m a l r)) tst
-    /\ match_states (mk_instr_state (Regmap.set r v rs) m0) tst.
-Proof.
-  intros. inv H2. pose proof H. inv H. inv H9.
-  destruct st.
-  econstructor; simplify.
-  { constructor.
-    { constructor. intros.
-      destruct (Pos.eq_dec x r); subst.
-      { rewrite map2. econstructor; eauto. eapply gen_list_base. intros.
-        rewrite <- H6. eauto.
-        instantiate (1 := (Regmap.set r v rs0)). rewrite Regmap.gss. auto. }
-      { rewrite Regmap.gso by auto. rewrite genmap1; crush. } }
-    { rewrite genmap1; crush. eauto. } }
-  { constructor; auto; intros. destruct (Pos.eq_dec r x);
-    subst; [repeat rewrite Regmap.gss | repeat rewrite Regmap.gso]; auto. }
-Qed.
-
-Lemma sem_update_store :
-  forall A ge sp a0 m a l r o f st m' rs m0 st',
-  @sem A ge sp st f st' ->
-  Op.eval_addressing ge sp a rs ## l = Some a0 ->
-  Mem.storev m m0 a0 rs !! r = Some m' ->
-  match_states st' (mk_instr_state rs m0) ->
-  exists tst, sem ge sp st (update f (RBstore o m a l r)) tst
-              /\ match_states (mk_instr_state rs m') tst.
-Proof.
-  intros. inv H2. pose proof H. inv H. inv H9.
-  destruct st.
-  econstructor; simplify.
-  { econstructor.
-    { econstructor; intros. rewrite genmap1; crush. }
-    { rewrite map2. econstructor; eauto. eapply gen_list_base. intros. rewrite <- H6.
-      eauto. specialize (H6 r). rewrite H6. eauto. } }
-  { econstructor; eauto. }
-Qed.
-
-Lemma sem_update :
-  forall A ge sp st x st' st'' st''' f,
-  sem ge sp st f st' ->
-  match_states st' st''' ->
-  @step_instr A ge sp st''' x st'' ->
-  exists tst, sem ge sp st (update f x) tst /\ match_states st'' tst.
-Proof.
-  intros. destruct x; inv H1.
-  { econstructor. split.
-    apply sem_update_RBnop. eassumption.
-    apply match_states_commut. auto. }
-  { eapply sem_update_Op; eauto. }
-  { eapply sem_update_load; eauto. }
-  { eapply sem_update_store; eauto. }
-Qed.
-
-Lemma sem_update2_Op :
-  forall A ge sp st f r l o0 o m rs v,
-  @sem A ge sp st f (mk_instr_state rs m) ->
-  Op.eval_operation ge sp o0 rs ## l m = Some v ->
-  sem ge sp st (update f (RBop o o0 l r)) (mk_instr_state (Regmap.set r v rs) m).
-Proof.
-  intros. destruct st. constructor.
-  inv H. inv H6.
-  { constructor; intros. simplify.
-    destruct (Pos.eq_dec r x); subst.
-    { rewrite map2. econstructor. eauto.
-      apply gen_list_base. eauto.
-      rewrite Regmap.gss. auto. }
-    { rewrite genmap1; crush. rewrite Regmap.gso; auto.  } }
-  { simplify. rewrite genmap1; crush. inv H. eauto. }
-Qed.
-
-Lemma sem_update2_load :
-  forall A ge sp st f r o m a l m0 rs v a0,
-    @sem A ge sp st f (mk_instr_state rs m0) ->
-    Op.eval_addressing ge sp a rs ## l = Some a0 ->
-    Mem.loadv m m0 a0 = Some v ->
-    sem ge sp st (update f (RBload o m a l r)) (mk_instr_state (Regmap.set r v rs) m0).
-Proof.
-  intros. simplify. inv H. inv H7. constructor.
-  { constructor; intros. destruct (Pos.eq_dec r x); subst.
-    { rewrite map2. rewrite Regmap.gss. econstructor; eauto.
-      apply gen_list_base; eauto. }
-    { rewrite genmap1; crush. rewrite Regmap.gso; eauto. }
-  }
-  { simplify. rewrite genmap1; crush. }
-Qed.
-
-Lemma sem_update2_store :
-  forall A ge sp a0 m a l r o f st m' rs m0,
-    @sem A ge sp st f (mk_instr_state rs m0) ->
-    Op.eval_addressing ge sp a rs ## l = Some a0 ->
-    Mem.storev m m0 a0 rs !! r = Some m' ->
-    sem ge sp st (update f (RBstore o m a l r)) (mk_instr_state rs m').
-Proof.
-  intros. simplify. inv H. inv H7. constructor; simplify.
-  { econstructor; intros. rewrite genmap1; crush. }
-  { rewrite map2. econstructor; eauto. apply gen_list_base; eauto. }
-Qed.
-
-Lemma sem_update2 :
-  forall A ge sp st x st' st'' f,
-  sem ge sp st f st' ->
-  @step_instr A ge sp st' x st'' ->
-  sem ge sp st (update f x) st''.
-Proof.
-  intros.
-  destruct x; inv H0;
-  eauto using sem_update_RBnop, sem_update2_Op, sem_update2_load, sem_update2_store.
-Qed.
-
-Lemma abstr_sem_val_mem :
-  forall A B ge tge st tst sp a,
-    ge_preserved ge tge ->
-    forall v m,
-    (@sem_mem A ge sp st a m /\ match_states st tst -> @sem_mem B tge sp tst a m) /\
-    (@sem_value A ge sp st a v /\ match_states st tst -> @sem_value B tge sp tst a v).
-Proof.
-  intros * H.
-  apply expression_ind2 with
-
-    (P := fun (e1: expression) =>
-    forall v m,
-    (@sem_mem A ge sp st e1 m /\ match_states st tst -> @sem_mem B tge sp tst e1 m) /\
-    (@sem_value A ge sp st e1 v /\ match_states st tst -> @sem_value B tge sp tst e1 v))
-
-    (P0 := fun (e1: expression_list) =>
-    forall lv, @sem_val_list A ge sp st e1 lv /\ match_states st tst -> @sem_val_list B tge sp tst e1 lv);
-  simplify; intros; simplify.
-  { inv H1. inv H2. constructor. }
-  { inv H2. inv H1. rewrite H0. constructor. }
-  { inv H3. }
-  { inv H3. inv H4. econstructor. apply H1; auto. simplify. eauto. constructor. auto. auto.
-    apply H0; simplify; eauto. constructor; eauto.
-    unfold ge_preserved in *. simplify. rewrite <- H2. auto.
-  }
-  { inv H3. }
-  { inv H3. inv H4. econstructor. apply H1; eauto; simplify; eauto. constructor; eauto.
-    apply H0; simplify; eauto. constructor; eauto.
-    inv H. rewrite <- H4. eauto.
-    auto.
-  }
-  { inv H4. inv H5. econstructor. apply H0; eauto. simplify; eauto. constructor; eauto.
-    apply H2; eauto. simplify; eauto. constructor; eauto.
-    apply H1; eauto. simplify; eauto. constructor; eauto.
-    inv H. rewrite <- H5. eauto. auto.
-  }
-  { inv H4. }
-  { inv H1. constructor. }
-  { inv H3. constructor; auto. apply H0; eauto. apply Mem.empty. }
-Qed.
-
-Lemma abstr_sem_value :
-  forall a A B ge tge sp st tst v,
-    @sem_value A ge sp st a v ->
-    ge_preserved ge tge ->
-    match_states st tst ->
-    @sem_value B tge sp tst a v.
-Proof. intros; eapply abstr_sem_val_mem; eauto; apply Mem.empty. Qed.
-
-Lemma abstr_sem_mem :
-  forall a A B ge tge sp st tst v,
-    @sem_mem A ge sp st a v ->
-    ge_preserved ge tge ->
-    match_states st tst ->
-    @sem_mem B tge sp tst a v.
-Proof. intros; eapply abstr_sem_val_mem; eauto. Qed.
-
-Lemma abstr_sem_regset :
-  forall a a' A B ge tge sp st tst rs,
-    @sem_regset A ge sp st a rs ->
-    ge_preserved ge tge ->
-    (forall x, a # x = a' # x) ->
-    match_states st tst ->
-    exists rs', @sem_regset B tge sp tst a' rs' /\ (forall x, rs !! x = rs' !! x).
-Proof.
-  inversion 1; intros.
-  inv H7.
-  econstructor. simplify. econstructor. intros.
-  eapply abstr_sem_value; eauto. rewrite <- H6.
-  eapply H0. constructor; eauto.
-  auto.
-Qed.
-
-Lemma abstr_sem :
-  forall a a' A B ge tge sp st tst st',
-    @sem A ge sp st a st' ->
-    ge_preserved ge tge ->
-    (forall x, a # x = a' # x) ->
-    match_states st tst ->
-    exists tst', @sem B tge sp tst a' tst' /\ match_states st' tst'.
-Proof.
-  inversion 1; subst; intros.
-  inversion H4; subst.
-  exploit abstr_sem_regset; eauto; inv_simp.
-  do 3 econstructor; eauto.
-  rewrite <- H3.
-  eapply abstr_sem_mem; eauto.
-Qed.
-
-Lemma abstract_execution_correct':
-  forall A B ge tge sp st' a a' st tst,
-  @sem A ge sp st a st' ->
-  ge_preserved ge tge ->
-  check a a' = true ->
-  match_states st tst ->
-  exists tst', @sem B tge sp tst a' tst' /\ match_states st' tst'.
-Proof.
-  intros;
-  pose proof (check_correct a a' H1);
-  eapply abstr_sem; eauto.
-Qed.
-
-Lemma states_match :
-  forall st1 st2 st3 st4,
-  match_states st1 st2 ->
-  match_states st2 st3 ->
-  match_states st3 st4 ->
-  match_states st1 st4.
-Proof.
-  intros * H1 H2 H3; destruct st1; destruct st2; destruct st3; destruct st4.
-  inv H1. inv H2. inv H3; constructor.
-  unfold regs_lessdef in *. intros.
-  repeat match goal with
-         | H: forall _, _, r : positive |- _ => specialize (H r)
-         end.
-  congruence.
-  auto.
-Qed.
-
-Lemma step_instr_block_same :
-  forall ge sp st st',
-  step_instr_block ge sp st nil st' ->
-  st = st'.
-Proof. inversion 1; auto. Qed.
-
-Lemma step_instr_seq_same :
-  forall ge sp st st',
-  step_instr_seq ge sp st nil st' ->
-  st = st'.
-Proof. inversion 1; auto. Qed.
-
-Lemma sem_update' :
-  forall A ge sp st a x st',
-  sem ge sp st (update (abstract_sequence empty a) x) st' ->
-  exists st'',
-  @step_instr A ge sp st'' x st' /\
-  sem ge sp st (abstract_sequence empty a) st''.
-Proof.
-  Admitted.
-
-Lemma rtlpar_trans_correct :
-  forall bb ge sp sem_st' sem_st st,
-  sem ge sp sem_st (abstract_sequence empty (concat (concat bb))) sem_st' ->
-  match_states sem_st st ->
-  exists st', RTLPar.step_instr_block ge sp st bb st'
-              /\ match_states sem_st' st'.
-Proof.
-  induction bb using rev_ind.
-  { repeat econstructor. eapply abstract_interp_empty3 in H.
-    inv H. inv H0. constructor; congruence. }
-  { simplify. inv H0. repeat rewrite concat_app in H. simplify.
-    rewrite app_nil_r in H.
-    exploit sem_separate; eauto; inv_simp.
-    repeat econstructor. admit. admit.
-  }
-Admitted.
-
-(*Lemma abstract_execution_correct_ld:
-  forall bb bb' cfi ge tge sp st st' tst,
-    RTLBlock.step_instr_list ge sp st bb st' ->
-    ge_preserved ge tge ->
-    schedule_oracle (mk_bblock bb cfi) (mk_bblock bb' cfi) = true ->
-    match_states_ld st tst ->
-    exists tst', RTLPar.step_instr_block tge sp tst bb' tst'
-                 /\ match_states st' tst'.
-Proof.
-  intros.*)
-*)
-
 Lemma match_states_list :
   forall A (rs: Regmap.t A) rs',
   (forall r, rs !! r = rs' !! r) ->
@@ -577,245 +129,6 @@ Proof.
   | repeat rewrite Regmap.gso by auto ]; auto.
 Qed.
 
-(*Lemma abstract_interp_empty3 :
-  forall A ctx st',
-    @sem A ctx empty st' -> match_states (ctx_is ctx) st'.
-Proof.
-  inversion 1; subst; simplify. destruct ctx.
-  destruct ctx_is.
-  constructor; intros.
-  - inv H0. specialize (H3 x). inv H3. inv H8. reflexivity.
-  - inv H1. specialize (H3 x). inv H3. inv H8. reflexivity.
-  - inv H2. inv H8. reflexivity.
-Qed.
-
-Lemma step_instr_matches :
-  forall A a ge sp st st',
-    @step_instr A ge sp st a st' ->
-    forall tst,
-      match_states st tst ->
-      exists tst', step_instr ge sp tst a tst'
-                   /\ match_states st' tst'.
-Proof.
-  induction 1; simplify;
-  match goal with H: match_states _ _ |- _ => inv H end;
-  try solve [repeat econstructor; try erewrite match_states_list;
-  try apply PTree_matches; eauto;
-  match goal with
-    H: forall _, _ |- context[Mem.storev] => erewrite <- H; eauto
-  end].
-  - destruct p. match goal with H: eval_pred _ _ _ _ |- _ => inv H end.
-    repeat econstructor; try erewrite match_states_list; eauto.
-    erewrite <- eval_predf_pr_equiv; eassumption.
-    apply PTree_matches; assumption.
-    repeat (econstructor; try apply eval_pred_false); eauto. try erewrite match_states_list; eauto.
-    erewrite <- eval_predf_pr_equiv; eassumption.
-    econstructor; auto.
-    match goal with H: eval_pred _ _ _ _ |- _ => inv H end.
-    repeat econstructor; try erewrite match_states_list; eauto.
-  (*- destruct p. match goal with H: eval_pred _ _ _ _ |- _ => inv H end.
-    repeat econstructor; try erewrite match_states_list; eauto.
-    erewrite <- eval_predf_pr_equiv; eassumption.
-    apply PTree_matches; assumption.
-    repeat (econstructor; try apply eval_pred_false); eauto. try erewrite match_states_list; eauto.
-    erewrite <- eval_predf_pr_equiv; eassumption.
-    econstructor; auto.
-    match goal with H: eval_pred _ _ _ _ |- _ => inv H end.
-    repeat econstructor; try erewrite match_states_list; eauto.
-  - destruct p. match goal with H: eval_pred _ _ _ _ |- _ => inv H end.
-    repeat econstructor; try erewrite match_states_list; eauto.
-    match goal with
-    H: forall _, _ |- context[Mem.storev] => erewrite <- H; eauto
-    end.
-    erewrite <- eval_predf_pr_equiv; eassumption.
-    repeat (econstructor; try apply eval_pred_false); eauto. try erewrite match_states_list; eauto.
-    match goal with
-    H: forall _, _ |- context[Mem.storev] => erewrite <- H; eauto
-    end.
-    erewrite <- eval_predf_pr_equiv; eassumption.
-    match goal with H: eval_pred _ _ _ _ |- _ => inv H end.
-    repeat econstructor; try erewrite match_states_list; eauto.
-    match goal with
-    H: forall _, _ |- context[Mem.storev] => erewrite <- H; eauto
-    end.
-  - admit.*) Admitted.
-
-Lemma step_instr_list_matches :
-  forall a ge sp st st',
-  step_instr_list ge sp st a st' ->
-  forall tst, match_states st tst ->
-              exists tst', step_instr_list ge sp tst a tst'
-                           /\ match_states st' tst'.
-Proof.
-  induction a; intros; inv H;
-  try (exploit step_instr_matches; eauto; []; simplify;
-       exploit IHa; eauto; []; simplify); repeat econstructor; eauto.
-Qed.
-
-Lemma step_instr_seq_matches :
-  forall a ge sp st st',
-   step_instr_seq ge sp st a st' ->
-  forall tst, match_states st tst ->
-              exists tst', step_instr_seq ge sp tst a tst'
-                           /\ match_states st' tst'.
-Proof.
-  induction a; intros; inv H;
-  try (exploit step_instr_list_matches; eauto; []; simplify;
-       exploit IHa; eauto; []; simplify); repeat econstructor; eauto.
-Qed.
-
-Lemma step_instr_block_matches :
-  forall bb ge sp st st',
-  step_instr_block ge sp st bb st' ->
-  forall tst, match_states st tst ->
-              exists tst', step_instr_block ge sp tst bb tst'
-                           /\ match_states st' tst'.
-Proof.
-  induction bb; intros; inv H;
-  try (exploit step_instr_seq_matches; eauto; []; simplify;
-       exploit IHbb; eauto; []; simplify); repeat econstructor; eauto.
-Qed.
-
-Lemma rtlblock_trans_correct' :
-  forall bb ge sp st x st'',
-  RTLBlock.step_instr_list ge sp st (bb ++ x :: nil) st'' ->
-  exists st', RTLBlock.step_instr_list ge sp st bb st'
-              /\ step_instr ge sp st' x st''.
-Proof.
-  induction bb.
-  crush. exists st.
-  split. constructor. inv H. inv H6. auto.
-  crush. inv H. exploit IHbb. eassumption. simplify.
-  econstructor. split.
-  econstructor; eauto. eauto.
-Qed.
-
-Lemma abstract_interp_empty A st : @sem A st empty (ctx_is st).
-Proof. destruct st, ctx_is. simpl. repeat econstructor. Qed.
-
-Lemma abstract_seq :
-  forall l f i,
-    abstract_sequence f (l ++ i :: nil) = update (abstract_sequence f l) i.
-Proof. induction l; crush. Qed.
-
-Lemma abstract_sequence_update :
-  forall l r f,
-  check_dest_l l r = false ->
-  (abstract_sequence f l) # (Reg r) = f # (Reg r).
-Proof.
-  induction l using rev_ind; crush.
-  rewrite abstract_seq. rewrite check_dest_update. apply IHl.
-  apply check_list_l_false in H. tauto.
-  apply check_list_l_false in H. tauto.
-Qed.
-
-(*Lemma sem_separate :
-  forall A ctx b a st',
-    sem ctx (abstract_sequence empty (a ++ b)) st' ->
-    exists st'',
-         @sem A ctx (abstract_sequence empty a) st''
-      /\ @sem A (mk_ctx st'' (ctx_sp ctx) (ctx_ge ctx)) (abstract_sequence empty b) st'.
-Proof.
-  induction b using rev_ind; simplify.
-  { econstructor. simplify. rewrite app_nil_r in H. eauto. apply abstract_interp_empty. }
-  { simplify. rewrite app_assoc in H. rewrite abstract_seq in H.
-    exploit sem_update'; eauto; simplify.
-    exploit IHb; eauto; inv_simp.
-    econstructor; split; eauto.
-    rewrite abstract_seq.
-    eapply sem_update2; eauto.
-  }
-Qed.*)
-
-Lemma sem_update_RBnop :
-  forall A ctx f st',
-  @sem A ctx f st' -> sem ctx (update f RBnop) st'.
-Proof. auto. Qed.
-
-Lemma sem_update_Op :
-  forall A ge sp ist f st' r l o0 o m rs v ps,
-  @sem A (mk_ctx ist sp ge) f st' ->
-  eval_predf ps o = true ->
-  Op.eval_operation ge sp o0 (rs ## l) m = Some v ->
-  match_states st' (mk_instr_state rs ps m) ->
-  exists tst,
-  sem (mk_ctx ist sp ge) (update f (RBop (Some o) o0 l r)) tst
-  /\ match_states (mk_instr_state (Regmap.set r v rs) ps m) tst.
-Proof.
-  intros. inv H1. inv H. inv H1. inv H3. simplify.
-  econstructor. simplify.
-  { constructor; try constructor; intros; try solve [rewrite genmap1; now eauto].
-    destruct (Pos.eq_dec x r); subst.
-    { rewrite map2. specialize (H1 r). inv H1.
-(*}
-  }
-  destruct st.
-  econstructor. simplify.
-  { constructor.
-    { constructor. intros. destruct (Pos.eq_dec x r); subst.
-      { pose proof (H5 r). rewrite map2. pose proof H. inv H. econstructor; eauto.
-        { inv H9. eapply gen_list_base; eauto. }
-        { instantiate (1 := (Regmap.set r v rs0)). rewrite Regmap.gss. erewrite regmap_list_equiv; eauto. } }
-      { rewrite Regmap.gso by auto. rewrite genmap1; crush. inv H. inv H7; eauto. } }
-    { inv H. rewrite genmap1; crush. eauto. } }
-  { constructor; eauto. intros.
-    destruct (Pos.eq_dec r x);
-    subst; [repeat rewrite Regmap.gss | repeat rewrite Regmap.gso]; auto. }
-Qed.*) Admitted.
-
-Lemma sem_update :
-  forall A ge sp st x st' st'' st''' f,
-  sem (mk_ctx st sp ge) f st' ->
-  match_states st' st''' ->
-  @step_instr A ge sp st''' x st'' ->
-  exists tst, sem (mk_ctx st sp ge) (update f x) tst /\ match_states st'' tst.
-Proof.
-  intros. destruct x.
-  - inv H1. econstructor. simplify. eauto. symmetry; auto.
-  - inv H1. inv H0. econstructor.
-    Admitted.
-
-Lemma rtlblock_trans_correct :
-  forall bb ge sp st st',
-    RTLBlock.step_instr_list ge sp st bb st' ->
-    forall tst,
-      match_states st tst ->
-      exists tst', sem (mk_ctx tst sp ge) (abstract_sequence empty bb) tst'
-                   /\ match_states st' tst'.
-Proof.
-  induction bb using rev_ind; simplify.
-  { econstructor. simplify. apply abstract_interp_empty.
-    inv H. auto. }
-  { apply rtlblock_trans_correct' in H. simplify.
-    rewrite abstract_seq.
-    exploit IHbb; try eassumption; []; simplify.
-    exploit sem_update. apply H1. symmetry; eassumption.
-    eauto. simplify. econstructor. split. apply H3.
-    auto. }
-Qed.
-
-Lemma abstract_execution_correct:
-  forall bb bb' cfi cfi' ge tge sp st st' tst,
-    RTLBlock.step_instr_list ge sp st bb st' ->
-    ge_preserved ge tge ->
-    schedule_oracle (mk_bblock bb cfi) (mk_bblock bb' cfi') = true ->
-    match_states st tst ->
-    exists tst', RTLPar.step_instr_block tge sp tst bb' tst'
-                 /\ match_states st' tst'.
-Proof.
-  intros.
-  unfold schedule_oracle in *. simplify. unfold empty_trees in H4.
-  exploit rtlblock_trans_correct; try eassumption; []; simplify.
-(*)  exploit abstract_execution_correct';
-  try solve [eassumption | apply state_lessdef_match_sem; eassumption].
-  apply match_states_commut. eauto. inv_simp.
-  exploit rtlpar_trans_correct; try eassumption; []; inv_simp.
-  exploit step_instr_block_matches; eauto. apply match_states_commut; eauto. inv_simp.
-  repeat match goal with | H: match_states _ _ |- _ => inv H end.
-  do 2 econstructor; eauto.
-  econstructor; congruence.
-Qed.*)Admitted.*)
-
 Definition match_prog (prog : GibleSeq.program) (tprog : GiblePar.program) :=
   match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq prog tprog.
 
@@ -1168,23 +481,45 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed.
       sem (mk_ctx i sp ge) f' (i'', None).
   Proof. Admitted.
 
+  Lemma truthy_dflt :
+    forall ps p,
+      truthy ps p -> eval_predf ps (dfltp p) = true.
+  Proof. intros. destruct p; cbn; inv H; auto. Qed.
+
+  Lemma Pand_true_left :
+    forall ps a b,
+      eval_predf ps a = false ->
+      eval_predf ps (a ∧ b) = false.
+  Proof.
+    intros.
+    rewrite eval_predf_Pand. now rewrite H.
+  Qed.
+
+  Lemma eval_predf_simplify :
+    forall ps x,
+      eval_predf ps (simplify x) = eval_predf ps x.
+  Proof. Admitted.
 
   Lemma sem_update_instr_term :
-    forall f i' i'' a sp i cf p p' p'' f',
+    forall f i' i'' sp i cf p p' p'' f',
       sem (mk_ctx i sp ge) f (i', None) ->
       step_instr ge sp (Iexec i') (RBexit p cf) (Iterm i'' cf) ->
-      update (p', f) a = Some (p'', f') ->
+      update (p', f) (RBexit p cf) = Some (p'', f') ->
+      eval_predf (is_ps i') p' = true ->
       sem (mk_ctx i sp ge) f' (i'', Some cf)
-           /\ eval_predf (is_ps i) p'' = false.
+           /\ eval_predf (is_ps i') p'' = false.
   Proof.
-    Admitted.
-
-  (* Lemma step_instr_lessdef : *)
-  (*   forall sp a i i' ti, *)
-  (*     step_instr ge sp (Iexec i) a (Iexec i') -> *)
-  (*     state_lessdef i ti -> *)
-  (*     exists ti', step_instr ge sp (Iexec ti) a (Iexec ti') /\ state_lessdef i' ti'. *)
-  (* Proof. Admitted. *)
+    intros. inv H0. simpl in *.
+    unfold Option.bind in *. destruct_match; try discriminate.
+    apply truthy_dflt in H6. inv H1.
+    assert (eval_predf (Gible.is_ps i'') (¬ dfltp p) = false).
+    { rewrite eval_predf_negate. now rewrite negb_false_iff. }
+    apply Pand_true_left with (b := p') in H0.
+    rewrite <- eval_predf_simplify in H0. split; auto.
+    unfold "<-e".
+    destruct i''.
+    inv H. constructor; auto. admit. admit. simplify.
+  Admitted.
 
   Lemma step_instr_lessdef_term :
     forall sp a i i' ti cf,
@@ -1193,36 +528,6 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed.
       exists ti', step_instr ge sp (Iexec ti) a (Iterm ti' cf) /\ state_lessdef i' ti'.
   Proof. Admitted.
 
-(*  Lemma app_predicated_semregset :
-    forall A ctx o f res r y,
-      @sem_regset A ctx f res ->
-      falsy (ctx_ps ctx) o ->
-      @sem_regset A ctx f # r <- (app_predicated o f#r y) res.
-  Proof.
-    inversion 1; subst; crush.
-    constructor; intros.
-    destruct (resource_eq r (Reg x)); subst.
-    + rewrite map2; eauto. unfold app_predicated. inv H1. admit.
-    + rewrite genmap1; auto.
-  Admitted.
-
-  Lemma app_predicated_sempredset :
-    forall A ctx o f rs r y ps,
-      @sem_predset A ctx f rs ->
-      falsy ps o ->
-      @sem_predset A ctx f # r <- (app_predicated o f#r y) rs.
-  Proof. Admitted.
-
-  Lemma app_predicated_sem :
-    forall A ctx o f i cf r y,
-      @sem A ctx f (i, cf) ->
-      falsy (is_ps i) o ->
-      @sem A ctx f # r <- (app_predicated o f#r y) (i, cf).
-  Proof.
-    inversion 1; subst; crush.
-    constructor.
-  Admitted.*)
-
   Lemma combined_falsy :
     forall i o1 o,
       falsy i o1 ->
@@ -1233,99 +538,6 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed.
     constructor. auto.
   Qed.
 
-  (* Inductive is_predicate_expr: expression -> Prop := *)
-  (* | is_predicate_expr_Epredset : *)
-  (*   forall c a, is_predicate_expr (Esetpred c a) *)
-  (* | is_predicate_expr_Ebase : *)
-  (*   forall p, is_predicate_expr (Ebase (Pred p)). *)
-
-  (* Inductive apred_wf: apred_op -> Prop := *)
-  (* | apred_wf_Plit: forall b p, *)
-  (*     is_predicate_expr p -> *)
-  (*     apred_wf (Plit (b, p)) *)
-  (* | apred_wf_Ptrue: apred_wf Ptrue *)
-  (* | apred_wf_Pfalse: apred_wf Pfalse *)
-  (* | apred_wf_Pand: forall a b, *)
-  (*   apred_wf a -> apred_wf b -> apred_wf (a ∧ b) *)
-  (* | apred_wf_Por: forall a b, *)
-  (*   apred_wf a -> apred_wf b -> apred_wf (a ∨ b). *)
-
-  (* Lemma apred_and_false1 : *)
-  (*   forall A ctx a b c, *)
-  (*     @eval_apred A ctx a false -> *)
-  (*     @eval_apred A ctx b c -> *)
-  (*     eval_apred ctx (a ∧ b) false. *)
-  (* Proof. *)
-  (*   intros. *)
-  (*   replace false with (false && c) by auto. *)
-  (*   constructor; auto. *)
-  (* Qed. *)
-
-  (* Lemma apred_and_false2 : *)
-  (*   forall A ctx a b c, *)
-  (*     @eval_apred A ctx a c -> *)
-  (*     eval_apred ctx b false -> *)
-  (*     eval_apred ctx (a ∧ b) false. *)
-  (* Proof. *)
-  (*   intros. *)
-  (*   replace false with (c && false) by eauto with bool. *)
-  (*   constructor; auto. *)
-  (* Qed. *)
-
-  (* #[local] Opaque simplify. *)
-
-  (* Lemma apred_simplify: *)
-  (*   forall A ctx a b, *)
-  (*     @eval_apred A ctx a b -> *)
-  (*     @eval_apred A ctx (simplify a) b. *)
-  (* Proof. Admitted. *)
-
-  (* Lemma exists_get_pred_eval : *)
-  (*   forall A ctx f p, *)
-  (*   exists c, @eval_apred A ctx (get_pred' f p) c. *)
-  (* Proof. *)
-  (*   induction p; crush; try solve [econstructor; constructor; eauto]. *)
-  (*   destruct_match. inv Heqp0. econstructor. *)
-  (*   unfold apredicated_to_apred_op. *)
-  (*   Admitted. (*probably not provable.*) *)
-
-  (* Lemma falsy_update : *)
-  (*   forall A f a ctx p f', *)
-  (*     @eval_apred A ctx (fst f) false -> *)
-  (*     update (Some f) a = Some (p, f') -> *)
-  (*     eval_apred ctx p false. *)
-  (* Proof. *)
-  (*   destruct f; destruct a; inversion 1; subst; crush; *)
-  (*   destruct_match; simplify; auto; *)
-  (*   unfold Option.bind, Option.bind2 in *; *)
-  (*   repeat (destruct_match; try discriminate; []); simplify; auto. *)
-  (*   apply apred_simplify. eapply apred_and_false2; eauto. admit. *)
-  (*   apply apred_simplify. eapply apred_and_false2; eauto. admit. *)
-  (*   constructor; auto. *)
-  (*   constructor; auto. *)
-  (*   constructor; auto. *)
-  (*   constructor; auto. *)
-  (*   constructor; auto. *)
-  (*   rewrite H2. *)
-  (*   apply apred_simplify. eapply apred_and_false2; eauto. admit. *)
-  (*   apply apred_simplify. eapply apred_and_false2; eauto. admit. *)
-  (*   Unshelve. all: exact true. *)
-  (* Admitted. *)
-
-  (* Lemma abstr_fold_falsy : *)
-  (*   forall x i0 sp cf i f p p' f', *)
-  (*   sem (mk_ctx i0 sp ge) f (i, cf) -> *)
-  (*   eval_apred (mk_ctx i0 sp ge) p false -> *)
-  (*   fold_left update x (Some (p, f)) =  Some (p', f') -> *)
-  (*   sem (mk_ctx i0 sp ge) f' (i, cf). *)
-  (* Proof. *)
-  (*   induction x; crush. *)
-  (*   eapply IHx. *)
-  (*   destruct a; destruct f; crush; *)
-  (*     try solve [eapply app_predicated_sem; eauto; apply combined_falsy; auto]. *)
-  (*   (* now apply falsy_update. *) *)
-  (* (* Qed. *) Admitted. *)
-
   Lemma state_lessdef_sem :
     forall i sp f i' ti cf,
       sem (mk_ctx i sp ge) f (i', cf) ->
@@ -1335,29 +547,88 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed.
 
   (* #[local] Opaque update. *)
 
+  Lemma mfold_left_update_Some :
+    forall xs x v,
+      mfold_left update xs x = Some v ->
+      exists y, x = Some y.
+  Proof. Admitted.
+
+  Lemma step_instr_term_exists :
+    forall A B ge sp v x v2 cf,
+      @step_instr A B ge sp (Iexec v) x (Iterm v2 cf) ->
+      exists p, x = RBexit p cf.
+  Proof using. inversion 1; eauto. Qed.
+
+  Lemma abstr_fold_falsy :
+    forall A i sp ge f i' cf p f' ilist p',
+      @sem A (mk_ctx i sp ge) f (i', cf) ->
+      mfold_left update ilist (Some (p, f)) = Some (p', f') ->
+      eval_predf (is_ps i') p = false ->
+      sem (mk_ctx i sp ge) f' (i', cf).
+  Proof. Admitted.
+
+  Ltac destr := destruct_match; try discriminate; [].
+
+  Lemma eval_predf_update_true :
+    forall i i' curr_p next_p f f_next instr sp,
+      update (curr_p, f) instr = Some (next_p, f_next) ->
+      step_instr ge sp (Iexec i) instr (Iexec i') ->
+      eval_predf (is_ps i) curr_p = true ->
+      eval_predf (is_ps i') next_p = true.
+  Proof.
+    intros * UPD STEP EVAL. destruct instr; cbn [update] in UPD;
+      try solve [unfold Option.bind in *; try destr; inv UPD; inv STEP; auto].
+    - unfold Option.bind in *. destr. inv UPD. inv STEP; auto. cbn [is_ps] in *.
+      admit.
+    - unfold Option.bind in *. destr. inv UPD. inv STEP. inv H3. admit.
+  Admitted. (* This only needs the addition of the property that any setpreds will not contain the
+  predicate in the name. *)
+
+  Lemma eval_predf_lessdef :
+    forall p a b,
+      state_lessdef a b ->
+      eval_predf (is_ps a) p = eval_predf (is_ps b) p.
+  Proof using.
+    induction p; crush.
+    - inv H. simpl. unfold eval_predf. simpl.
+      repeat destr. inv Heqp0. rewrite H1. auto.
+    - rewrite !eval_predf_Pand.
+      erewrite IHp1 by eassumption.
+      now erewrite IHp2 by eassumption.
+    - rewrite !eval_predf_Por.
+      erewrite IHp1 by eassumption.
+      now erewrite IHp2 by eassumption.
+  Qed.
+
   Lemma abstr_fold_correct :
-    forall sp x i i' i'' cf f p f',
+    forall sp x i i' i'' cf f p f' curr_p,
       SeqBB.step ge sp (Iexec i') x (Iterm i'' cf) ->
-      sem (mk_ctx i sp ge) (snd f) (i', None) ->
-      mfold_left update x (Some f) = Some (p, f') ->
+      sem (mk_ctx i sp ge) f (i', None) ->
+      eval_predf (is_ps i') curr_p = true ->
+      mfold_left update x (Some (curr_p, f)) = Some (p, f') ->
       forall ti,
         state_lessdef i ti ->
         exists ti', sem (mk_ctx ti sp ge) f' (ti', Some cf)
                /\ state_lessdef i'' ti'.
   Proof.
-    induction x; simplify; inv H.
-    - destruct f. (*  exploit update_Some; eauto; intros. simplify. *)
-    (*   rewrite H3 in H1. destruct x0. *)
-    (*   exploit IHx; eauto. eapply sem_update_instr; eauto. *)
-    (* - destruct f. *)
-    (*   exploit state_lessdef_sem; eauto; intros. simplify. *)
-    (*   exploit step_instr_lessdef_term; eauto; intros. simplify. *)
-    (*   inv H6. exploit update_Some; eauto; simplify. destruct x2. *)
-      (* exploit sem_update_instr_term; eauto; simplify. *)
-      (* eexists; split. *)
-      (* eapply abstr_fold_falsy; eauto. *)
-      (* rewrite H6 in H1. eauto. auto. *)
-  (* Qed. *) Admitted.
+    induction x as [| x xs IHx ]; intros; cbn -[update] in *; inv H; cbn [fst snd] in *.
+    - (* inductive case *)
+      exploit mfold_left_update_Some; eauto; intros Hexists;
+        inversion Hexists as [[curr_p_inter f_inter] EXEQ]; clear Hexists.
+        exploit eval_predf_update_true; eauto; intros EVALTRUE.
+      rewrite EXEQ in H2. eapply IHx in H2; eauto; cbn [fst snd] in *.
+      eapply sem_update_instr; eauto.
+    - (* terminal case *)
+      exploit mfold_left_update_Some; eauto; intros Hexists;
+        inversion Hexists as [[curr_p_inter f_inter] EXEQ]; clear Hexists. rewrite EXEQ in H2.
+      exploit state_lessdef_sem; eauto; intros H; inversion H as [v [Hi LESSDEF]]; clear H.
+      exploit step_instr_lessdef_term; eauto; intros H; inversion H as [v2 [Hi2 LESSDEF2]]; clear H.
+      exploit step_instr_term_exists; eauto; inversion 1 as [? ?]; subst; clear H.
+      erewrite eval_predf_lessdef in H1 by eassumption.
+      exploit sem_update_instr_term; eauto; intros [A B].
+      exists v2. split. inv Hi2.
+      eapply abstr_fold_falsy; try eassumption. auto.
+  Qed.
 
   Lemma sem_regset_empty :
     forall A ctx, @sem_regset A ctx empty (ctx_rs ctx).
@@ -1396,7 +667,7 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed.
     destruct_match; try easy.
     destruct p; simplify.
     eapply abstr_fold_correct; eauto.
-    simplify. eapply sem_empty.
+    simplify. eapply sem_empty. auto.
   Qed.
 
   Lemma abstr_check_correct :
@@ -1413,7 +684,7 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed.
       abstract_sequence x = Some x' ->
       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)
+     exists ti', SeqBB.step ge sp (Iexec ti) x (Iterm ti' cf)
              /\ state_lessdef i' ti'.
   Proof. Admitted.