Finish evaluability proof of RBop

5 files changed, 338 insertions, 210 deletions

diff --git a/src/hls/AbstrSemIdent.v b/src/hls/AbstrSemIdent.v
index 0cc8e9d..36c3ffc 100644
--- a/src/hls/AbstrSemIdent.v
+++ b/src/hls/AbstrSemIdent.v
@@ -96,10 +96,10 @@ Proof.
 
 Lemma sem_pred_expr_app_predicated_false2 :
   forall f_p y x v p ps,
-    sem_pred_expr f_p sem ctx (app_predicated p y x) v ->
+    sem_pred_expr f_p a_sem ctx (app_predicated p y x) v ->
     (forall x, sem_pexpr ctx (get_forest_p' x f_p) (ps !! x)) ->
     eval_predf ps p = false ->
-    sem_pred_expr f_p sem ctx y v.
+    sem_pred_expr f_p a_sem ctx y v.
 Admitted.
 
 Lemma sem_pred_expr_pred_ret :
@@ -601,7 +601,8 @@ Proof.
     rewrite Eapp_right_nil. auto.
 Qed.
 
-Lemma sem_merge_list :          (* [[id:f307d227-d0e9-49a0-823f-2d7e0db76972]] *)
+(* [[id:f307d227-d0e9-49a0-823f-2d7e0db76972]] *)
+Lemma sem_merge_list :
   forall f rs ps m args,
     sem ctx f ((mk_instr_state rs ps m), None) ->
     sem_pred_expr (forest_preds f) sem_val_list ctx
diff --git a/src/hls/GiblePargenproofBackward.v b/src/hls/GiblePargenproofBackward.v
index 718eb66..db0df19 100644
--- a/src/hls/GiblePargenproofBackward.v
+++ b/src/hls/GiblePargenproofBackward.v
@@ -30,6 +30,7 @@ Require Import vericert.hls.GibleSeq.
 Require Import vericert.hls.GiblePar.
 Require Import vericert.hls.Gible.
 Require Import vericert.hls.GiblePargenproofEquiv.
+Require Import vericert.hls.GiblePargenproofCommon.
 Require Import vericert.hls.GiblePargen.
 Require Import vericert.hls.Predicate.
 Require Import vericert.hls.Abstr.
@@ -132,30 +133,55 @@ Lemma evaluable_pred_expr_exists :
   forall sp pr f i0 exit_p exit_p' f' i ti p op args dst,
     (forall x, sem_pexpr (mk_ctx i0 sp ge) (get_forest_p' x f'.(forest_preds)) (pr !! x)) ->
     eval_predf pr exit_p = true ->
+    valid_mem (is_mem i0) (is_mem i) ->
     update (exit_p, f) (RBop p op 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) (RBop p op args dst) (Iexec ti').
+    exists ti',
+      step_instr ge sp (Iexec ti) (RBop p op args dst) (Iexec ti').
 Proof.
-  intros * HPRED HEVAL **. cbn -[seq_app] in H. unfold Option.bind in H. destr. inv H.
+  intros * HPRED HEVAL VALID_MEM **. cbn -[seq_app] in H. unfold Option.bind in H. destr. inv H.
   destruct ti.
   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.
-  assert (eval_predf pr (dfltp p ∧ exit_p') = true) by admit.
-  exploit sem_pred_expr_app_predicated2; eauto; intros.
-  exploit sem_pred_expr_seq_app_val2; eauto; simplify.
-  unfold pred_ret in *. inv H4. inv H12.
-  destruct i. exploit sem_merge_list; eauto; intros.
-  instantiate (1 := args) in H4.
-  eapply sem_pred_expr_ident2 in H4. simplify.
-  exploit sem_pred_expr_ident_det. eapply H5. eapply H4.
-  intros. subst. exploit sem_pred_expr_ident. eapply H5. eapply H8.
-  intros.
-
-  econstructor. econstructor.
-  Admitted.
+  exploit sem_pred_expr_prune_predicated2; eauto; intros. cbn in HPRED.
+  pose proof (truthy_dec pr p) as YH. inversion_clear YH as [YH'|YH'].
+  - assert (eval_predf pr (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.
+    unfold pred_ret in *. inv H4. inv H12.
+    destruct i. exploit sem_merge_list; eauto; intros.
+    instantiate (1 := args) in H4.
+    eapply sem_pred_expr_ident2 in H4. simplify.
+    exploit sem_pred_expr_ident_det. eapply H5. eapply H4.
+    intros. subst. inv H7.
+    eapply sem_val_list_det in H8; eauto; [|reflexivity]. subst.
+    inv H2.
+    econstructor. constructor.
+    + cbn in *. eapply eval_operation_valid_pointer. symmetry; eauto.
+      unfold ctx_mem in H14. cbn in H14. erewrite <- match_states_list; eauto.
+    + inv H0.
+      assert (sem_predset {| ctx_is := i0; ctx_sp := sp; ctx_ge := ge |} f pr)
+        by (now constructor).
+      pose proof (sem_predset_det _ _ ltac:(reflexivity) _ _ _ H0 H17).
+      assert (truthy is_ps0 p).
+      { eapply truthy_match_state; eassumption. }
+      eapply truthy_match_state; eassumption.
+  - inv YH'. cbn -[seq_app] in H.
+    assert (eval_predf pr (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 pr)
+        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 remember_expr_in :
   forall x l f a,
@@ -289,7 +315,7 @@ Proof.
   - cbn in *. inv Y.
     assert (similar {| ctx_is := i0; ctx_sp := sp; ctx_ge := ge |}
                     {| ctx_is := i0; ctx_sp := sp; ctx_ge := ge |})
-      by auto using similar_refl.
+      by reflexivity.
     now eapply sem_det in H; [| eapply Y1 | eapply Y3 ].
   - cbn -[update] in Y.
     pose proof Y as YX.
diff --git a/src/hls/GiblePargenproofCommon.v b/src/hls/GiblePargenproofCommon.v
new file mode 100644
index 0000000..8d8e0a2
--- /dev/null
+++ b/src/hls/GiblePargenproofCommon.v
@@ -0,0 +1,264 @@
+(*
+ * Vericert: Verified high-level synthesis.
+ * Copyright (C) 2023 Yann Herklotz <git@yannherklotz.com>
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <https://www.gnu.org/licenses/>.
+ *)
+
+Require Import compcert.backend.Registers.
+Require Import compcert.common.AST.
+Require Import compcert.common.Errors.
+Require Import compcert.common.Linking.
+Require Import compcert.common.Globalenvs.
+Require Import compcert.common.Memory.
+Require Import compcert.common.Values.
+Require Import compcert.lib.Maps.
+
+Require Import vericert.common.Vericertlib.
+Require Import vericert.hls.GibleSeq.
+Require Import vericert.hls.GiblePar.
+Require Import vericert.hls.Gible.
+Require Import vericert.hls.GiblePargenproofEquiv.
+Require Import vericert.hls.GiblePargen.
+Require Import vericert.hls.Predicate.
+Require Import vericert.hls.Abstr.
+Require Import vericert.hls.AbstrSemIdent.
+Require Import vericert.common.Monad.
+
+Module Import OptionExtra := MonadExtra(Option).
+
+#[local] Open Scope positive.
+#[local] Open Scope forest.
+#[local] Open Scope pred_op.
+
+#[local] Opaque simplify.
+#[local] Opaque deep_simplify.
+
+#[local] Ltac destr := destruct_match; try discriminate; [].
+
+Lemma storev_valid_pointer1 :
+  forall chunk m m' s d b z,
+    Mem.storev chunk m s d = Some m' ->
+    Mem.valid_pointer m b z = true ->
+    Mem.valid_pointer m' b z = true.
+Proof using.
+  intros. unfold Mem.storev in *. destruct_match; try discriminate; subst.
+  apply Mem.valid_pointer_nonempty_perm. apply Mem.valid_pointer_nonempty_perm in H0.
+  eapply Mem.perm_store_1; eauto.
+Qed.
+
+Lemma storev_valid_pointer2 :
+  forall chunk m m' s d b z,
+    Mem.storev chunk m s d = Some m' ->
+    Mem.valid_pointer m' b z = true ->
+    Mem.valid_pointer m b z = true.
+Proof using.
+  intros. unfold Mem.storev in *. destruct_match; try discriminate; subst.
+  apply Mem.valid_pointer_nonempty_perm. apply Mem.valid_pointer_nonempty_perm in H0.
+  eapply Mem.perm_store_2; eauto.
+Qed.
+
+Definition valid_mem m m' :=
+  forall b z, Mem.valid_pointer m b z = Mem.valid_pointer m' b z.
+
+#[global] Program Instance valid_mem_Equivalence : Equivalence valid_mem.
+Next Obligation. unfold valid_mem; auto. Qed. (* Reflexivity *)
+Next Obligation. unfold valid_mem; auto. Qed. (* Symmetry *)
+Next Obligation. unfold valid_mem; eauto. Qed. (* Transitity *)
+
+Lemma storev_valid_pointer :
+  forall chunk m m' s d,
+    Mem.storev chunk m s d = Some m' ->
+    valid_mem m m'.
+Proof using.
+  unfold valid_mem. symmetry.
+  intros. destruct (Mem.valid_pointer m b z) eqn:?;
+                   eauto using storev_valid_pointer1.
+  apply not_true_iff_false.
+  apply not_true_iff_false in Heqb0.
+  eauto using storev_valid_pointer2.
+Qed.
+
+Lemma storev_cmpu_bool :
+  forall m m' c v v0,
+    valid_mem m m' ->
+    Val.cmpu_bool (Mem.valid_pointer m) c v v0 = Val.cmpu_bool (Mem.valid_pointer m') c v v0.
+Proof using.
+  unfold valid_mem.
+  intros. destruct v, v0; crush.
+  { destruct_match; crush.
+    destruct_match; crush.
+    destruct_match; crush.
+    apply orb_true_iff in H1.
+    inv H1. rewrite H in H2. rewrite H2 in Heqb1.
+    simplify. rewrite H0 in Heqb1. crush.
+    rewrite H in H2. rewrite H2 in Heqb1.
+    rewrite H0 in Heqb1. crush.
+    destruct_match; auto. simplify.
+    apply orb_true_iff in H1.
+    inv H1. rewrite <- H in H2. rewrite H2 in Heqb1.
+    simplify. rewrite H0 in Heqb1. crush.
+    rewrite <- H in H2. rewrite H2 in Heqb1.
+    rewrite H0 in Heqb1. crush. }
+
+  { destruct_match; crush.
+    destruct_match; crush.
+    destruct_match; crush.
+    apply orb_true_iff in H1.
+    inv H1. rewrite H in H2. rewrite H2 in Heqb1.
+    simplify. rewrite H0 in Heqb1. crush.
+    rewrite H in H2. rewrite H2 in Heqb1.
+    rewrite H0 in Heqb1. crush.
+    destruct_match; auto. simplify.
+    apply orb_true_iff in H1.
+    inv H1. rewrite <- H in H2. rewrite H2 in Heqb1.
+    simplify. rewrite H0 in Heqb1. crush.
+    rewrite <- H in H2. rewrite H2 in Heqb1.
+    rewrite H0 in Heqb1. crush. }
+
+  { destruct_match; auto. destruct_match; auto; crush.
+    { destruct_match; crush.
+      { destruct_match; crush.
+        setoid_rewrite H in H0; eauto.
+        setoid_rewrite H in H1; eauto.
+        rewrite H0 in Heqb. rewrite H1 in Heqb; crush.
+      }
+      { destruct_match; crush.
+        setoid_rewrite H in Heqb0; eauto.
+        rewrite H0 in Heqb0. rewrite H1 in Heqb0; crush. } }
+    { destruct_match; crush.
+      { destruct_match; crush.
+        setoid_rewrite H in H0; eauto.
+        setoid_rewrite H in H1; eauto.
+        rewrite H0 in Heqb0. rewrite H1 in Heqb0; crush.
+      }
+      { destruct_match; crush.
+        setoid_rewrite H in Heqb0; eauto.
+        rewrite H0 in Heqb0. rewrite H1 in Heqb0; crush. } } }
+Qed.
+
+Lemma storev_eval_condition :
+  forall m m' c rs,
+    valid_mem m m' ->
+    Op.eval_condition c rs m = Op.eval_condition c rs m'.
+Proof using.
+  intros. destruct c; crush.
+  destruct rs; crush.
+  destruct rs; crush.
+  destruct rs; crush.
+  eapply storev_cmpu_bool; eauto.
+  destruct rs; crush.
+  destruct rs; crush.
+  eapply storev_cmpu_bool; eauto.
+Qed.
+
+Lemma eval_operation_valid_pointer :
+  forall A B (ge: Genv.t A B) sp op args m m' v,
+    valid_mem m m' ->
+    Op.eval_operation ge sp op args m' = Some v ->
+    Op.eval_operation ge sp op args m = Some v.
+Proof.
+  intros * VALID OP. destruct op; auto.
+  - destruct cond; auto; cbn in *.
+    + repeat destruct_match; auto. setoid_rewrite <- storev_cmpu_bool in OP; eauto.
+    + repeat destruct_match; auto. setoid_rewrite <- storev_cmpu_bool in OP; eauto.
+  - destruct c; auto; cbn in *.
+    + repeat destruct_match; auto. setoid_rewrite <- storev_cmpu_bool in OP; eauto.
+    + repeat destruct_match; auto. setoid_rewrite <- storev_cmpu_bool in OP; eauto.
+Qed.
+
+Lemma bb_memory_consistency_eval_operation :
+  forall A B (ge: Genv.t A B) sp state i state' args op v,
+    step_instr ge sp (Iexec state) i (Iexec state') ->
+    Op.eval_operation ge sp op args (is_mem state) = Some v ->
+    Op.eval_operation ge sp op args (is_mem state') = Some v.
+Proof.
+  inversion_clear 1; intro EVAL; auto.
+  cbn in *.
+  eapply eval_operation_valid_pointer. unfold valid_mem. symmetry.
+  eapply storev_valid_pointer; eauto.
+  auto.
+Qed.
+
+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 exists_sem_pred :
+  forall A B C (ctx: @ctx A) s pr r v,
+    @sem_pred_expr A B C pr s ctx r v ->
+    exists r',
+      NE.In r' r /\ s ctx (snd r') v.
+Proof.
+  induction r; crush.
+  - inv H. econstructor. split. constructor. auto.
+  - inv H.
+    + econstructor. split. constructor. left; auto. auto.
+    + exploit IHr; eauto. intros HH. inversion_clear HH as [x HH']. inv HH'.
+      econstructor. split. constructor. right. eauto. auto.
+Qed.
+
+Definition predicated_not_inP {A} (p: Gible.predicate) (l: predicated A) :=
+  forall op e, NE.In (op, e) l -> ~ PredIn p op.
+
+Lemma predicated_not_inP_cons :
+  forall A p (a: (pred_op * A)) l,
+    predicated_not_inP p (NE.cons a l) ->
+    predicated_not_inP p l.
+Proof.
+  unfold predicated_not_inP; intros. eapply H. econstructor. right; eauto.
+Qed.
+
+Lemma match_states_list :
+  forall A (rs: Regmap.t A) rs',
+  (forall r, rs !! r = rs' !! r) ->
+  forall l, rs ## l = rs' ## l.
+Proof. induction l; crush. Qed.
+
+Lemma PTree_matches :
+  forall A (v: A) res rs rs',
+  (forall r, rs !! r = rs' !! r) ->
+  forall x, (Regmap.set res v rs) !! x = (Regmap.set res v rs') !! x.
+Proof.
+  intros; destruct (Pos.eq_dec x res); subst;
+  [ repeat rewrite Regmap.gss by auto
+  | repeat rewrite Regmap.gso by auto ]; auto.
+Qed.
+
+Lemma truthy_dec:
+  forall ps a, truthy ps a \/ falsy ps a.
+Proof.
+  destruct a; try case_eq (eval_predf ps p); intuition (constructor; auto).
+Qed.
+
+Lemma truthy_match_state :
+  forall ps ps' p,
+    (forall x, ps !! x = ps' !! x) ->
+    truthy ps p ->
+    truthy ps' p.
+Proof.
+  intros; destruct p; inv H0; constructor; auto.
+  erewrite eval_predf_pr_equiv; eauto.
+Qed.
+
+Lemma falsy_match_state :
+  forall ps ps' p,
+    (forall x, ps !! x = ps' !! x) ->
+    falsy ps p ->
+    falsy ps' p.
+Proof.
+  intros; destruct p; inv H0; constructor; auto.
+  erewrite eval_predf_pr_equiv; eauto.
+Qed.
diff --git a/src/hls/GiblePargenproofEquiv.v b/src/hls/GiblePargenproofEquiv.v
index 5f589a7..b63f2fd 100644
--- a/src/hls/GiblePargenproofEquiv.v
+++ b/src/hls/GiblePargenproofEquiv.v
@@ -342,6 +342,11 @@ Proof.
   - transitivity ist'; auto.
 Qed.
 
+#[global] Instance similar_Equivalence {A} : Equivalence (@similar A A) :=
+  { Equivalence_Reflexive := similar_refl A ;
+    Equivalence_Symmetric := similar_commut A A ;
+    Equivalence_Transitive := @similar_trans A A A ; }.
+
 Module HashExpr' <: MiniDecidableType.
   Definition t := expression.
   Definition eq_dec := expression_dec.
@@ -745,6 +750,27 @@ Section CORRECT.
     - inv H0; inv H1; eauto; exploit sem_pexpr_det; eauto; discriminate.
   Qed.
 
+  Lemma sem_predset_det:
+    forall f ps ps',
+      sem_predset ictx f ps ->
+      sem_predset octx f ps' ->
+      forall x, ps !! x = ps' !! x.
+  Proof.
+    intros. inv H. inv H0. eauto using sem_pexpr_det.
+  Qed.
+
+  Lemma sem_regset_det:
+    forall f rs rs',
+      sem_regset ictx f rs ->
+      sem_regset octx f rs' ->
+      forall x, rs !! x = rs' !! x.
+  Proof.
+    intros. inv H. inv H0.
+    specialize (H1 x). specialize (H x).
+    eapply sem_pred_expr_det in H1; eauto.
+    exact sem_value_det.
+  Qed.
+
   Lemma sem_det :
     forall p i cf i' cf',
       sem ictx p (i, cf) ->
diff --git a/src/hls/GiblePargenproofForward.v b/src/hls/GiblePargenproofForward.v
index 1d59216..bd18855 100644
--- a/src/hls/GiblePargenproofForward.v
+++ b/src/hls/GiblePargenproofForward.v
@@ -30,6 +30,7 @@ Require Import vericert.hls.GibleSeq.
 Require Import vericert.hls.GiblePar.
 Require Import vericert.hls.Gible.
 Require Import vericert.hls.GiblePargenproofEquiv.
+Require Import vericert.hls.GiblePargenproofCommon.
 Require Import vericert.hls.GiblePargen.
 Require Import vericert.hls.Predicate.
 Require Import vericert.hls.Abstr.
@@ -80,22 +81,6 @@ 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 match_states_list :
-  forall A (rs: Regmap.t A) rs',
-  (forall r, rs !! r = rs' !! r) ->
-  forall l, rs ## l = rs' ## l.
-Proof. induction l; crush. Qed.
-
-Lemma PTree_matches :
-  forall A (v: A) res rs rs',
-  (forall r, rs !! r = rs' !! r) ->
-  forall x, (Regmap.set res v rs) !! x = (Regmap.set res v rs') !! x.
-Proof.
-  intros; destruct (Pos.eq_dec x res); subst;
-  [ repeat rewrite Regmap.gss by auto
-  | repeat rewrite Regmap.gso by auto ]; auto.
-Qed.
-
 Section CORRECTNESS.
 
   Context (prog: GibleSeq.program) (tprog : GiblePar.program).
@@ -147,155 +132,6 @@ all be evaluable.
     econstructor; eauto.
   Qed.
 
-  Lemma storev_valid_pointer1 :
-    forall chunk m m' s d b z,
-      Mem.storev chunk m s d = Some m' ->
-      Mem.valid_pointer m b z = true ->
-      Mem.valid_pointer m' b z = true.
-  Proof using.
-    intros. unfold Mem.storev in *. destruct_match; try discriminate; subst.
-    apply Mem.valid_pointer_nonempty_perm. apply Mem.valid_pointer_nonempty_perm in H0.
-    eapply Mem.perm_store_1; eauto.
-  Qed.
-
-  Lemma storev_valid_pointer2 :
-    forall chunk m m' s d b z,
-      Mem.storev chunk m s d = Some m' ->
-      Mem.valid_pointer m' b z = true ->
-      Mem.valid_pointer m b z = true.
-  Proof using.
-    intros. unfold Mem.storev in *. destruct_match; try discriminate; subst.
-    apply Mem.valid_pointer_nonempty_perm. apply Mem.valid_pointer_nonempty_perm in H0.
-    eapply Mem.perm_store_2; eauto.
-  Qed.
-
-  Definition valid_mem m m' :=
-    forall b z, Mem.valid_pointer m b z = Mem.valid_pointer m' b z.
-
-  #[global] Program Instance valid_mem_Equivalence : Equivalence valid_mem.
-  Next Obligation. unfold valid_mem; auto. Qed. (* Reflexivity *)
-  Next Obligation. unfold valid_mem; auto. Qed. (* Symmetry *)
-  Next Obligation. unfold valid_mem; eauto. Qed. (* Transitity *)
-
-  Lemma storev_valid_pointer :
-    forall chunk m m' s d,
-      Mem.storev chunk m s d = Some m' ->
-      valid_mem m m'.
-  Proof using.
-    unfold valid_mem. symmetry.
-    intros. destruct (Mem.valid_pointer m b z) eqn:?;
-                     eauto using storev_valid_pointer1.
-    apply not_true_iff_false.
-    apply not_true_iff_false in Heqb0.
-    eauto using storev_valid_pointer2.
-  Qed.
-
-  Lemma storev_cmpu_bool :
-    forall m m' c v v0,
-      valid_mem m m' ->
-      Val.cmpu_bool (Mem.valid_pointer m) c v v0 = Val.cmpu_bool (Mem.valid_pointer m') c v v0.
-  Proof using.
-    unfold valid_mem.
-    intros. destruct v, v0; crush.
-    { destruct_match; crush.
-      destruct_match; crush.
-      destruct_match; crush.
-      apply orb_true_iff in H1.
-      inv H1. rewrite H in H2. rewrite H2 in Heqb1.
-      simplify. rewrite H0 in Heqb1. crush.
-      rewrite H in H2. rewrite H2 in Heqb1.
-      rewrite H0 in Heqb1. crush.
-      destruct_match; auto. simplify.
-      apply orb_true_iff in H1.
-      inv H1. rewrite <- H in H2. rewrite H2 in Heqb1.
-      simplify. rewrite H0 in Heqb1. crush.
-      rewrite <- H in H2. rewrite H2 in Heqb1.
-      rewrite H0 in Heqb1. crush. }
-
-    { destruct_match; crush.
-      destruct_match; crush.
-      destruct_match; crush.
-      apply orb_true_iff in H1.
-      inv H1. rewrite H in H2. rewrite H2 in Heqb1.
-      simplify. rewrite H0 in Heqb1. crush.
-      rewrite H in H2. rewrite H2 in Heqb1.
-      rewrite H0 in Heqb1. crush.
-      destruct_match; auto. simplify.
-      apply orb_true_iff in H1.
-      inv H1. rewrite <- H in H2. rewrite H2 in Heqb1.
-      simplify. rewrite H0 in Heqb1. crush.
-      rewrite <- H in H2. rewrite H2 in Heqb1.
-      rewrite H0 in Heqb1. crush. }
-
-    { destruct_match; auto. destruct_match; auto; crush.
-      { destruct_match; crush.
-        { destruct_match; crush.
-          setoid_rewrite H in H0; eauto.
-          setoid_rewrite H in H1; eauto.
-          rewrite H0 in Heqb. rewrite H1 in Heqb; crush.
-        }
-        { destruct_match; crush.
-          setoid_rewrite H in Heqb0; eauto.
-          rewrite H0 in Heqb0. rewrite H1 in Heqb0; crush. } }
-      { destruct_match; crush.
-        { destruct_match; crush.
-          setoid_rewrite H in H0; eauto.
-          setoid_rewrite H in H1; eauto.
-          rewrite H0 in Heqb0. rewrite H1 in Heqb0; crush.
-        }
-        { destruct_match; crush.
-          setoid_rewrite H in Heqb0; eauto.
-          rewrite H0 in Heqb0. rewrite H1 in Heqb0; crush. } } }
-  Qed.
-
-  Lemma storev_eval_condition :
-    forall m m' c rs,
-      valid_mem m m' ->
-      Op.eval_condition c rs m = Op.eval_condition c rs m'.
-  Proof using.
-    intros. destruct c; crush.
-    destruct rs; crush.
-    destruct rs; crush.
-    destruct rs; crush.
-    eapply storev_cmpu_bool; eauto.
-    destruct rs; crush.
-    destruct rs; crush.
-    eapply storev_cmpu_bool; eauto.
-  Qed.
-
-  Lemma eval_operation_valid_pointer :
-    forall A B (ge: Genv.t A B) sp op args m m' v,
-      valid_mem m m' ->
-      Op.eval_operation ge sp op args m' = Some v ->
-      Op.eval_operation ge sp op args m = Some v.
-  Proof.
-    intros * VALID OP. destruct op; auto.
-    - destruct cond; auto; cbn in *.
-      + repeat destruct_match; auto. setoid_rewrite <- storev_cmpu_bool in OP; eauto.
-      + repeat destruct_match; auto. setoid_rewrite <- storev_cmpu_bool in OP; eauto.
-    - destruct c; auto; cbn in *.
-      + repeat destruct_match; auto. setoid_rewrite <- storev_cmpu_bool in OP; eauto.
-      + repeat destruct_match; auto. setoid_rewrite <- storev_cmpu_bool in OP; eauto.
-  Qed.
-
-  Lemma bb_memory_consistency_eval_operation :
-    forall A B (ge: Genv.t A B) sp state i state' args op v,
-      step_instr ge sp (Iexec state) i (Iexec state') ->
-      Op.eval_operation ge sp op args (is_mem state) = Some v ->
-      Op.eval_operation ge sp op args (is_mem state') = Some v.
-  Proof.
-    inversion_clear 1; intro EVAL; auto.
-    cbn in *.
-    eapply eval_operation_valid_pointer. unfold valid_mem. symmetry.
-    eapply storev_valid_pointer; eauto.
-    auto.
-  Qed.
-
-  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 sem_update_Istore :
     forall A rs args m v f ps ctx addr a0 chunk m' v',
       Op.eval_addressing (ctx_ge ctx) (ctx_sp ctx) addr rs ## args = Some a0 ->
@@ -393,20 +229,6 @@ all be evaluable.
       + auto.
   Qed.
 
-  Lemma exists_sem_pred :
-    forall A B C (ctx: @ctx A) s pr r v,
-      @sem_pred_expr A B C pr s ctx r v ->
-      exists r',
-        NE.In r' r /\ s ctx (snd r') v.
-  Proof.
-    induction r; crush.
-    - inv H. econstructor. split. constructor. auto.
-    - inv H.
-      + econstructor. split. constructor. left; auto. auto.
-      + exploit IHr; eauto. intros HH. inversion_clear HH as [x HH']. inv HH'.
-        econstructor. split. constructor. right. eauto. auto.
-  Qed.
-
   Lemma sem_update_Istore_top:
     forall A f p p' f' rs m pr res args p0 state addr a chunk m',
       Op.eval_addressing (ctx_ge state) (ctx_sp state) addr rs ## args = Some a ->
@@ -451,17 +273,6 @@ all be evaluable.
     + auto.
   Qed.
 
-  Definition predicated_not_inP {A} (p: Gible.predicate) (l: predicated A) :=
-    forall op e, NE.In (op, e) l -> ~ PredIn p op.
-
-  Lemma predicated_not_inP_cons :
-    forall A p (a: (pred_op * A)) l,
-      predicated_not_inP p (NE.cons a l) ->
-      predicated_not_inP p l.
-  Proof.
-    unfold predicated_not_inP; intros. eapply H. econstructor. right; eauto.
-  Qed.
-
   Lemma sem_pexpr_not_in :
     forall G (ctx: @ctx G) p0 ps p e b,
       ~ PredIn p p0 ->