Split proof up into more files

1 files changed, 79 insertions, 2006 deletions

diff --git a/src/hls/GiblePargenproof.v b/src/hls/GiblePargenproof.v
index 0b9bd78..9e58e03 100644
--- a/src/hls/GiblePargenproof.v
+++ b/src/hls/GiblePargenproof.v
@@ -1,6 +1,6 @@
 (*
  * Vericert: Verified high-level synthesis.
- * Copyright (C) 2020-2023 Yann Herklotz <yann@yannherklotz.com>
+ * Copyright (C) 2020-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
@@ -29,10 +29,12 @@ 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.common.Monad.
+Require Import vericert.hls.GiblePargenproofForward.
 
 Module Import OptionExtra := MonadExtra(Option).
 
@@ -45,168 +47,7 @@ Module Import OptionExtra := MonadExtra(Option).
 
 Ltac destr := destruct_match; try discriminate; [].
 
-(*|
-==============
-RTLPargenproof
-==============
-
-RTLBlock to abstract translation
-================================
-
-Correctness of translation from RTLBlock to the abstract interpretation
-language.
-|*)
-
-Definition is_regs i := match i with mk_instr_state rs _ _ => rs end.
-Definition is_mem i := match i with mk_instr_state _ _ m => m end.
-Definition is_ps i := match i with mk_instr_state _ p _ => p end.
-
-Definition evaluable {A B C} (sem: ctx -> B -> C -> Prop) (ctx: @ctx A) p := exists b, sem ctx p b.
-
-Definition p_evaluable {A} := @evaluable A _ _ sem_pexpr.
-
-Definition evaluable_expr {A} := @evaluable A _ _ sem_pred.
-
-Definition all_evaluable {A B} (ctx: @ctx A) f_p (l: predicated B) :=
-  forall p y, NE.In (p, y) l -> p_evaluable ctx (from_pred_op f_p p).
-
-Definition all_evaluable2 {A B C} (ctx: @ctx A) (sem: Abstr.ctx -> B -> C -> Prop) (l: predicated B) :=
-  forall p y, NE.In (p, y) l -> evaluable sem ctx y.
-
-Definition pred_forest_evaluable {A} (ctx: @ctx A) (ps: PTree.t pred_pexpr) :=
-  forall i p, ps ! i = Some p -> p_evaluable ctx p.
-
-Definition forest_evaluable {A} (ctx: @ctx A) (f: forest) :=
-  pred_forest_evaluable ctx f.(forest_preds).
-
-(* Lemma all_evaluable2_NEmap : *)
-(*   forall G A (ctx: @ctx G) (f: (pred_op * A) -> (pred_op * pred_expression)) (x: predicated A), *)
-(*     all_evaluable2 ctx sem_pred (NE.map f x). *)
-(* Proof. *)
-(*   induction x. *)
-
-Lemma all_evaluable_cons :
-  forall A B pr ctx b a,
-    all_evaluable ctx pr (NE.cons a b) ->
-    @all_evaluable A B ctx pr b.
-Proof.
-  unfold all_evaluable; intros.
-  enough (NE.In (p, y) (NE.cons a b)); eauto.
-  constructor; tauto.
-Qed.
-
-Lemma all_evaluable2_cons :
-  forall A B C sem ctx b a,
-    all_evaluable2 ctx sem (NE.cons a b) ->
-    @all_evaluable2 A B C ctx sem b.
-Proof.
-  unfold all_evaluable2; intros.
-  enough (NE.In (p, y) (NE.cons a b)); eauto.
-  constructor; tauto.
-Qed.
-
-Lemma all_evaluable_cons2 :
-  forall A B pr ctx b a p,
-    @all_evaluable A B ctx pr (NE.cons (p, a) b) ->
-    p_evaluable ctx (from_pred_op pr p).
-Proof.
-  unfold all_evaluable; intros.
-  eapply H. constructor; eauto.
-Qed.
-
-Lemma all_evaluable2_cons2 :
-  forall A B C sem ctx b a p,
-    @all_evaluable2 A B C ctx sem (NE.cons (p, a) b) ->
-    evaluable sem ctx a.
-Proof.
-  unfold all_evaluable; intros.
-  eapply H. constructor; eauto.
-Qed.
-
-Lemma all_evaluable_cons3 :
-  forall A B pr ctx b p a,
-    all_evaluable ctx pr b ->
-    p_evaluable ctx (from_pred_op pr p) ->
-    @all_evaluable A B ctx pr (NE.cons (p, a) b).
-Proof.
-  unfold all_evaluable; intros. inv H1. inv H3. inv H1. auto.
-  eauto.
-Qed.
-
-Lemma all_evaluable_singleton :
-  forall A B pr ctx b p,
-    @all_evaluable A B ctx pr (NE.singleton (p, b)) ->
-    p_evaluable ctx (from_pred_op pr p).
-Proof.
-  unfold all_evaluable; intros. eapply H. constructor.
-Qed.
-
-Lemma get_forest_p_evaluable :
-  forall A (ctx: @ctx A) f r,
-    forest_evaluable ctx f ->
-    p_evaluable ctx (f #p r).
-Proof.
-  intros. unfold "#p", get_forest_p'.
-  destruct_match. unfold forest_evaluable in *.
-  unfold pred_forest_evaluable in *. eauto.
-  unfold p_evaluable, evaluable. eexists.
-  constructor. constructor.
-Qed.
-
-Lemma set_forest_p_evaluable :
-  forall A (ctx: @ctx A) f r p,
-    forest_evaluable ctx f ->
-    p_evaluable ctx p ->
-    forest_evaluable ctx (f #p r <- p).
-Proof.
-  unfold forest_evaluable, pred_forest_evaluable; intros.
-  destruct (peq i r); subst.
-  - rewrite forest_pred_gss2 in H1. now inv H1.
-  - rewrite forest_pred_gso2 in H1 by auto; eauto.
-Qed.
-
-Definition check_dest i r' :=
-  match i with
-  | RBop p op rl r => (r =? r')%positive
-  | RBload p chunk addr rl r => (r =? r')%positive
-  | _ => false
-  end.
-
-Lemma check_dest_dec i r :
-  {check_dest i r = true} + {check_dest i r = false}.
-Proof. destruct (check_dest i r); tauto. Qed.
-
-Fixpoint check_dest_l l r :=
-  match l with
-  | nil => false
-  | a :: b => check_dest a r || check_dest_l b r
-  end.
-
-Lemma check_dest_l_forall :
-  forall l r,
-  check_dest_l l r = false ->
-  Forall (fun x => check_dest x r = false) l.
-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 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.
+Definition state_lessdef := GiblePargenproofEquiv.match_states.
 
 Definition match_prog (prog : GibleSeq.program) (tprog : GiblePar.program) :=
   match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq prog tprog.
@@ -355,13 +196,80 @@ Section CORRECTNESS.
   Qed.
   Hint Resolve eval_addressing_eq : rtlgp.
 
-  Lemma ge_preserved_lem:
+(*|
+==============
+RTLPargenproof
+==============
+
+RTLBlock to abstract translation
+================================
+
+Correctness of translation from RTLBlock to the abstract interpretation
+language.
+|*)
+
+  Lemma abstr_seq_reverse_correct :
+    forall sp x i i' ti cf x',
+      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)
+             /\ state_lessdef i' ti'.
+  Proof.
+
+(*|
+Proof Sketch:
+
+We do an induction over the list of instructions ``x``.  This is trivial for the
+empty case and then for the inductive case we know that there exists an
+execution that matches the abstract execution, so we need to know that adding
+another instructions to it will still mean that the execution will result in the
+same value.
+
+Arithmetic operations will be a problem because we will have to show that these
+can be executed.  However, this should mostly be a problem in the abstract state
+comparison, because there two abstract states can be equal without one being
+evaluable.
+|*)
+
+  Admitted.
+
+(*|
+This is the top-level lemma which uses the following proofs to complete the
+square:
+
+- ``abstr_sequence_correct``: This is the lemma that states the forward
+  translation form ``GibleSeq`` to ``Abstr`` was correct.
+- ``abstr_check_correct``: This is the lemma that states that if a check between
+  two ``Abstr`` programs succeeds, that they will also behave the same.  This
+  depends on the SAT solver correctness, as the predicates might be
+  syntactically different to each other.
+- ``abstr_seq_reverse_correct``: This is the lemma that shows that the backwards
+  simulation between the abstract translation and the concrete execution also
+  holds.  We only have a translation from the concrete into the abstract, but
+  then prove that if we have an execution in the abstract, we can observe that
+  same execution in the concrete.
+- ``seqbb_step_parbb_step``: Finally, this lemma states that the parallel
+  execution of the basic block is equivalent to the sequential execution of the
+  concatenation of that parallel block.  This is because even in the translation
+  to HTL, the Verilog semantics are sequential within a clock cycle, but will
+  then be parallelised by the synthesis tool.  The argument for why this is
+  still useful is because we are identifying and scheduling instructions into
+  clock cycles.
+|*)
+
+  Definition local_abstr_check_correct :=
+    @abstr_check_correct GibleSeq.fundef GiblePar.fundef.
+
+  Definition local_abstr_check_correct2 :=
+    @abstr_check_correct GibleSeq.fundef GibleSeq.fundef.
+
+  Lemma ge_preserved_local :
     ge_preserved ge tge.
-  Proof using TRANSL.
-    unfold ge_preserved.
-    eauto with rtlgp.
+  Proof.
+    unfold ge_preserved; 
+    eauto using eval_op_eq, eval_addressing_eq.
   Qed.
-  Hint Resolve ge_preserved_lem : rtlgp.
 
   Lemma lessdef_regmap_optget:
     forall or rs rs',
@@ -533,1848 +441,13 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed.
     eapply IHx; eauto.
   Qed.
 
-  Lemma eval_predf_negate :
-    forall ps p,
-      eval_predf ps (negate p) = negb (eval_predf ps p).
-  Proof.
-    unfold eval_predf; intros. rewrite negate_correct. auto.
-  Qed.
-
-  Lemma is_truthy_negate :
-    forall ps p pred,
-      truthy ps p ->
-      falsy ps (combine_pred (Some (negate (Option.default T p))) pred).
-  Proof.
-    inversion 1; subst; simplify.
-    - destruct pred; constructor; auto.
-    - destruct pred; constructor.
-      rewrite eval_predf_Pand. rewrite eval_predf_negate. rewrite H0. auto.
-      rewrite eval_predf_negate. rewrite H0. auto.
-  Qed.
-
-  Lemma sem_pred_expr_NEapp :
-    forall A B C sem f_p ctx a b v,
-      sem_pred_expr f_p sem ctx a v ->
-      @sem_pred_expr A B C f_p sem ctx (NE.app a b) v.
-  Proof.
-    induction a; crush.
-    - inv H. constructor; auto.
-    - inv H. constructor; eauto.
-      eapply sem_pred_expr_cons_false; eauto.
-  Qed.
-
-  Lemma sem_pred_expr_NEapp2 :
-    forall A B C sem f_p ctx a b v ps,
-      (forall x, sem_pexpr ctx (get_forest_p' x f_p) (ps !! x)) ->
-      (forall x, NE.In x a -> eval_predf ps (fst x) = false) ->
-      sem_pred_expr f_p sem ctx b v ->
-      @sem_pred_expr A B C f_p sem ctx (NE.app a b) v.
-  Proof.
-    induction a; crush.
-    - assert (IN: NE.In a (NE.singleton a)) by constructor.
-      specialize (H0 _ IN). destruct a.
-      eapply sem_pred_expr_cons_false; eauto. cbn [fst] in *.
-      eapply sem_pexpr_eval; eauto.
-    - assert (NE.In a (NE.cons a a0)) by (constructor; tauto).
-      apply H0 in H2.
-      destruct a. cbn [fst] in *.
-      eapply sem_pred_expr_cons_false.
-      eapply sem_pexpr_eval; eauto. eapply IHa; eauto.
-      intros. eapply H0. constructor; tauto.
-  Qed.
-
-  Lemma sem_pred_expr_NEapp3 :
-    forall A B C sem f_p ctx (a b: predicated B) v,
-      (forall x, NE.In x a -> sem_pexpr ctx (from_pred_op f_p (fst x)) false) ->
-      sem_pred_expr f_p sem ctx b v ->
-      @sem_pred_expr A B C f_p sem ctx (NE.app a b) v.
-  Proof.
-    induction a; crush.
-    - assert (IN: NE.In a (NE.singleton a)) by constructor.
-      specialize (H _ IN). destruct a.
-      eapply sem_pred_expr_cons_false; eauto.
-    - assert (NE.In a (NE.cons a a0)) by (constructor; tauto).
-      apply H in H1.
-      destruct a. cbn [fst] in *.
-      eapply sem_pred_expr_cons_false; auto.
-      eapply IHa; eauto.
-      intros. eapply H. constructor; tauto.
-  Qed.
-
-  Lemma sem_pred_expr_map_not :
-    forall A p ps y x0,
-      eval_predf ps p = false ->
-      NE.In x0 (NE.map (fun x => (p ∧ fst x, snd x)) y) ->
-      eval_predf ps (@fst _ A x0) = false.
-  Proof.
-    induction y; crush.
-    - inv H0. simplify. rewrite eval_predf_Pand. rewrite H. auto.
-    - inv H0. inv H2. cbn -[eval_predf]. rewrite eval_predf_Pand.
-      rewrite H. auto. eauto.
-  Qed.
-
-  Lemma sem_pred_expr_map_Pand :
-    forall A B C sem ctx f_p ps x v p,
-      (forall x : positive, sem_pexpr ctx (get_forest_p' x f_p) ps !! x) ->
-      eval_predf ps p = true ->
-      sem_pred_expr f_p sem ctx x v ->
-      @sem_pred_expr A B C f_p sem ctx
-        (NE.map (fun x0 => (p ∧ fst x0, snd x0)) x) v.
-  Proof.
-    induction x; crush.
-    inv H1. simplify. constructor; eauto.
-    simplify. replace true with (true && true) by auto.
-    constructor; auto.
-    eapply sem_pexpr_eval; eauto.
-    inv H1. simplify. constructor; eauto.
-    simplify. replace true with (true && true) by auto.
-    constructor; auto.
-    eapply sem_pexpr_eval; eauto.
-    eapply sem_pred_expr_cons_false. cbn.
-    replace false with (true && false) by auto. apply sem_pexpr_Pand; auto.
-    eapply sem_pexpr_eval; eauto. eauto.
-  Qed.
-
-  Lemma sem_pred_expr_app_predicated :
-    forall A B C sem ctx f_p y x v p ps,
-      sem_pred_expr f_p sem ctx x v ->
-      (forall x, sem_pexpr ctx (get_forest_p' x f_p) (ps !! x)) ->
-      eval_predf ps p = true ->
-      @sem_pred_expr A B C f_p sem ctx (app_predicated p y x) v.
-  Proof.
-    intros * SEM PS EVAL. unfold app_predicated.
-    eapply sem_pred_expr_NEapp2; eauto.
-    intros. eapply sem_pred_expr_map_not; eauto.
-    rewrite eval_predf_negate. rewrite EVAL. auto.
-    eapply sem_pred_expr_map_Pand; eauto.
-  Qed.
-
-  Lemma sem_pred_expr_app_predicated_false :
-    forall A B C sem ctx f_p y x v p ps,
-      sem_pred_expr f_p sem ctx y v ->
-      (forall x, sem_pexpr ctx (get_forest_p' x f_p) (ps !! x)) ->
-      eval_predf ps p = false ->
-      @sem_pred_expr A B C f_p sem ctx (app_predicated p y x) v.
-  Admitted.
-
-  Lemma sem_pred_expr_prune_predicated :
-    forall A B C sem ctx f_p y x v,
-      sem_pred_expr f_p sem ctx x v ->
-      prune_predicated x = Some y ->
-      @sem_pred_expr A B C f_p sem ctx y v.
-  Proof.
-    intros * SEM PRUNE. unfold prune_predicated in *.
-    Admitted.
-
-  Inductive sem_ident {B A: Type} (c: @ctx B) (a: A): A -> Prop :=
-  | sem_ident_intro : sem_ident c a a.
-
-  Lemma sem_pred_expr_pred_ret :
-    forall G A (ctx: @Abstr.ctx G) (i: A) ps,
-      sem_pred_expr ps sem_ident ctx (pred_ret i) i.
-  Proof. intros; constructor; constructor. Qed.
-
-  Lemma sem_pred_expr_ident :
-    forall G A B ps (ctx: @Abstr.ctx G) (l: predicated A) (s: @Abstr.ctx G -> A -> B -> Prop) l_,
-      sem_pred_expr ps sem_ident ctx l l_ ->
-      forall (v: B),
-        s ctx l_ v ->
-        sem_pred_expr ps s ctx l v.
-  Proof.
-    induction 1.
-    - intros. constructor; auto. inv H0. auto.
-    - intros. apply sem_pred_expr_cons_false; auto.
-    - intros. inv H0. constructor; auto.
-  Qed.
-
-  Lemma sem_pred_expr_ident2 :
-    forall G A B ps (ctx: @Abstr.ctx G) (l: predicated A) (s: @Abstr.ctx G -> A -> B -> Prop) (v: B),
-        sem_pred_expr ps s ctx l v ->
-        exists l_, sem_pred_expr ps sem_ident ctx l l_ /\ s ctx l_ v.
-  Proof.
-    induction 1.
-    - exists e; split; auto. constructor; auto. constructor.
-    - inversion_clear IHsem_pred_expr as [x IH].
-      inversion_clear IH as [SEM EVALS].
-      exists x; split; auto. apply sem_pred_expr_cons_false; auto.
-    - exists e; split; auto; constructor; auto; constructor.
-  Qed.
-
-  Fixpoint of_elist (e: expression_list): list expression :=
-    match e with
-    | Econs a b => a :: of_elist b
-    | Enil => nil
-    end.
-
-  Fixpoint to_elist (e: list expression): expression_list :=
-    match e with
-    | a :: b => Econs a (to_elist b)
-    | nil => Enil
-    end.
-
-  Lemma sem_val_list_elist :
-    forall G (ctx: @Abstr.ctx G) l j,
-      sem_val_list ctx (to_elist l) j ->
-      Forall2 (sem_value ctx) l j.
-  Proof. induction l; intros; cbn in *; inversion H; constructor; eauto. Qed.
-
-  Lemma sem_val_list_elist2 :
-    forall G (ctx: @Abstr.ctx G) l j,
-      Forall2 (sem_value ctx) l j ->
-      sem_val_list ctx (to_elist l) j.
-  Proof. induction l; intros; cbn in *; inversion H; constructor; eauto. Qed.
-
-  Lemma sem_val_list_elist3 :
-    forall G (ctx: @Abstr.ctx G) l j,
-      sem_val_list ctx l j ->
-      Forall2 (sem_value ctx) (of_elist l) j.
-  Proof. induction l; intros; cbn in *; inversion H; constructor; eauto. Qed.
-
-  Lemma sem_val_list_elist4 :
-    forall G (ctx: @Abstr.ctx G) l j,
-      Forall2 (sem_value ctx) (of_elist l) j ->
-      sem_val_list ctx l j.
-  Proof. induction l; intros; cbn in *; inversion H; constructor; eauto. Qed.
-
-  Lemma sem_pred_expr_predicated_map :
-    forall A B C pr (f: C -> B) ctx (pred: predicated C) (pred': C),
-      sem_pred_expr pr sem_ident ctx pred pred' ->
-      @sem_pred_expr A _ _ pr sem_ident ctx (predicated_map f pred) (f pred').
-  Proof.
-    induction pred; unfold predicated_map; intros.
-    - inv H. inv H3. constructor; eauto. constructor.
-    - inv H. inv H5. constructor; eauto. constructor.
-      eapply sem_pred_expr_cons_false; eauto.
-  Qed.
-
-  Lemma NEapp_NEmap :
-    forall A B (f: A -> B) a b,
-      NE.map f (NE.app a b) = NE.app (NE.map f a) (NE.map f b).
-  Proof. induction a; crush. Qed.
-
-  Lemma sem_pred_expr_predicated_prod :
-    forall A B C pr ctx (a: predicated C) (b: predicated B) a' b',
-      sem_pred_expr pr sem_ident ctx a a' ->
-      sem_pred_expr pr sem_ident ctx b b' ->
-      @sem_pred_expr A _ _ pr sem_ident ctx (predicated_prod a b) (a', b').
-  Proof.
-    induction a; intros.
-    - inv H. inv H4. unfold predicated_prod.
-      generalize dependent b. induction b; intros.
-      + cbn. destruct_match. inv Heqp. inv H0. inv H6.
-        constructor. simplify. replace true with (true && true) by auto.
-        eapply sem_pexpr_Pand; eauto. constructor.
-      + inv H0. inv H6. cbn. constructor; cbn.
-        replace true with (true && true) by auto.
-        constructor; auto. constructor.
-        eapply sem_pred_expr_cons_false; eauto. cbn.
-        replace false with (true && false) by auto.
-        apply sem_pexpr_Pand; auto.
-    - unfold predicated_prod. simplify.
-      rewrite NEapp_NEmap.
-      inv H. eapply sem_pred_expr_NEapp.
-      { induction b; crush.
-        destruct a. inv H0. constructor.
-        replace true with (true && true) by auto.
-        eapply sem_pexpr_Pand; auto. inv H6. inv H7.
-        constructor.
-
-        destruct a. inv H0. constructor.
-        replace true with (true && true) by auto.
-        constructor; auto. inv H8. inv H6. constructor.
-
-        specialize (IHb H8). eapply sem_pred_expr_cons_false; auto.
-        replace false with (true && false) by auto.
-        apply sem_pexpr_Pand; auto.
-      }
-      { exploit IHa. eauto. eauto. intros.
-        unfold predicated_prod in *.
-        eapply sem_pred_expr_NEapp3; eauto; [].
-        clear H. clear H0.
-        induction b.
-        { intros. inv H. destruct a. simpl.
-          constructor; tauto. }
-        { intros. inv H. inv H1. destruct a. simpl.
-          constructor; tauto. eauto. } }
-  Qed.
-
-  Lemma sem_pred_expr_seq_app :
-    forall G A B (f: predicated (A -> B))
-        ps (ctx: @ctx G) l f_ l_,
-      sem_pred_expr ps sem_ident ctx l l_ ->
-      sem_pred_expr ps sem_ident ctx f f_ ->
-      sem_pred_expr ps sem_ident ctx (seq_app f l) (f_ l_).
-  Proof.
-    unfold seq_app; intros.
-    remember (fun x : (A -> B) * A => fst x (snd x)) as app.
-    replace (f_ l_) with (app (f_, l_)) by (rewrite Heqapp; auto).
-    eapply sem_pred_expr_predicated_map. eapply sem_pred_expr_predicated_prod; auto.
-  Qed.
-
-  Lemma sem_pred_expr_map :
-    forall A B C (ctx: @ctx A) ps (f: B -> C) y v,
-      sem_pred_expr ps sem_ident ctx y v ->
-      sem_pred_expr ps sem_ident ctx (NE.map (fun x => (fst x, f (snd x))) y) (f v).
-  Proof.
-    induction y; crush. inv H. constructor; crush. inv H3. constructor.
-    inv H. inv H5. constructor; eauto. constructor.
-    eapply sem_pred_expr_cons_false; eauto.
-  Qed.
-
-  Lemma sem_pred_expr_flap :
-    forall G A B C (f: predicated (A -> B -> C))
-        ps (ctx: @ctx G) l f_,
-      sem_pred_expr ps sem_ident ctx f f_ ->
-      sem_pred_expr ps sem_ident ctx (flap f l) (f_ l).
-  Proof.
-    induction f. unfold flap2; intros. inv H. inv H3.
-    constructor; eauto. constructor.
-    intros. inv H. cbn.
-    constructor; eauto. inv H5. constructor.
-    eapply sem_pred_expr_cons_false; eauto.
-   Qed.
-
-  Lemma sem_pred_expr_flap2 :
-    forall G A B C (f: predicated (A -> B -> C))
-        ps (ctx: @ctx G) l1 l2 f_,
-      sem_pred_expr ps sem_ident ctx f f_ ->
-      sem_pred_expr ps sem_ident ctx (flap2 f l1 l2) (f_ l1 l2).
-  Proof.
-    induction f. unfold flap2; intros. inv H. inv H3.
-    constructor; eauto. constructor.
-    intros. inv H. cbn.
-    constructor; eauto. inv H5. constructor.
-    eapply sem_pred_expr_cons_false; eauto.
-  Qed.
-
-  Lemma sem_pred_expr_seq_app_val :
-    forall G A B V (s: @Abstr.ctx G -> B -> V -> Prop)
-        (f: predicated (A -> B))
-        ps ctx l v f_ l_,
-      sem_pred_expr ps sem_ident ctx l l_ ->
-      sem_pred_expr ps sem_ident ctx f f_ ->
-      s ctx (f_ l_) v ->
-      sem_pred_expr ps s ctx (seq_app f l) v.
-  Proof.
-    intros. eapply sem_pred_expr_ident; [|eassumption].
-    eapply sem_pred_expr_seq_app; eauto.
-  Qed.
-
-  Fixpoint Eapp a b :=
-    match a with
-    | Enil => b
-    | Econs ax axs => Econs ax (Eapp axs b)
-    end.
-
-  Lemma Eapp_right_nil :
-    forall a, Eapp a Enil = a.
-  Proof. induction a; cbn; try rewrite IHa; auto. Qed.
-
-  Lemma Eapp_left_nil :
-    forall a, Eapp Enil a = a.
-  Proof. auto. Qed.
-
-  Lemma sem_pred_expr_cons_pred_expr :
-    forall A (ctx: @ctx A) pr s s' a e,
-      sem_pred_expr pr sem_ident ctx s s' ->
-      sem_pred_expr pr sem_ident ctx a e ->
-      sem_pred_expr pr sem_ident ctx (cons_pred_expr a s) (Econs e s').
-  Proof.
-    intros. unfold cons_pred_expr.
-    replace (Econs e s') with ((uncurry Econs) (e, s')) by auto.
-    eapply sem_pred_expr_predicated_map.
-    eapply sem_pred_expr_predicated_prod; eauto.
-  Qed.
-
-  Lemma evaluable_singleton :
-    forall A B ctx fp r,
-      @all_evaluable A B ctx fp (NE.singleton (T, r)).
-  Proof.
-    unfold all_evaluable, evaluable; intros.
-    inv H. simpl. exists true. constructor.
-  Qed.
-
-Lemma evaluable_negate :
-  forall G (ctx: @ctx G) p,
-    p_evaluable ctx p ->
-    p_evaluable ctx (¬ p).
-Proof.
-  unfold p_evaluable, evaluable in *; intros.
-  inv H. eapply sem_pexpr_negate in H0. econstructor; eauto.
-Qed.
-
-Lemma predicated_evaluable :
-  forall G (ctx: @ctx G) ps (p: pred_op),
-    pred_forest_evaluable ctx ps ->
-    p_evaluable ctx (from_pred_op ps p).
-Proof.
-  unfold pred_forest_evaluable; intros. induction p; intros; cbn.
-  - repeat destruct_match; subst; unfold get_forest_p'.
-    destruct_match. eapply H; eauto. econstructor. constructor. constructor.
-    eapply evaluable_negate.
-    destruct_match. eapply H; eauto. econstructor. constructor. constructor.
-  - repeat econstructor.
-  - repeat econstructor.
-  - inv IHp1. inv IHp2. econstructor. apply sem_pexpr_Pand; eauto.
-  - inv IHp1. inv IHp2. econstructor. apply sem_pexpr_Por; eauto.
-Qed.
-
-Lemma predicated_evaluable_all :
-  forall A G (ctx: @ctx G) ps (p: predicated A),
-    pred_forest_evaluable ctx ps ->
-    all_evaluable ctx ps p.
-Proof.
-  unfold all_evaluable; intros.
-  eapply predicated_evaluable. eauto.
-Qed.
-
-Lemma predicated_evaluable_all_list :
-  forall A G (ctx: @ctx G) ps (p: list (predicated A)),
-    pred_forest_evaluable ctx ps ->
-    Forall (all_evaluable ctx ps) p.
-Proof.
-  induction p.
-  - intros. constructor.
-  - intros. constructor; eauto. apply predicated_evaluable_all; auto.
-Qed.
-
-Hint Resolve evaluable_singleton : core.
-Hint Resolve predicated_evaluable : core.
-Hint Resolve predicated_evaluable_all : core.
-Hint Resolve predicated_evaluable_all_list : core.
-
-  Lemma sem_pred_expr_fold_right :
-    forall A pr ctx s a a' s',
-      sem_pred_expr pr sem_ident ctx s s' ->
-      Forall2 (sem_pred_expr pr sem_ident ctx) (NE.to_list a) (of_elist a') ->
-      @sem_pred_expr A _ _ pr sem_ident ctx (NE.fold_right cons_pred_expr s a) (Eapp a' s').
-  Proof.
-    induction a; crush. inv H0. inv H5. destruct a'; crush. destruct a'; crush.
-    inv H3. eapply sem_pred_expr_cons_pred_expr; eauto.
-    inv H0. destruct a'; crush. inv H3.
-    eapply sem_pred_expr_cons_pred_expr; eauto.
-  Qed.
-
-  Lemma sem_pred_expr_fold_right2 :
-    forall A pr ctx s a a' s',
-      sem_pred_expr pr sem_ident ctx s s' ->
-      @sem_pred_expr A _ _ pr sem_ident ctx (NE.fold_right cons_pred_expr s a) (Eapp a' s') ->
-      Forall2 (sem_pred_expr pr sem_ident ctx) (NE.to_list a) (of_elist a').
-  Proof.
-    induction a. Admitted.
-
-  Lemma NEof_list_some :
-    forall A a a' (e: A),
-      NE.of_list a = Some a' ->
-      NE.of_list (e :: a) = Some (NE.cons e a').
-  Proof.
-    induction a; [crush|].
-    intros.
-    cbn in H. destruct a0. inv H. auto.
-    destruct_match; [|discriminate].
-    inv H. specialize (IHa n a ltac:(trivial)).
-    cbn. destruct_match. unfold NE.of_list in IHa.
-    fold (@NE.of_list A) in IHa. rewrite IHa in Heqo0. inv Heqo0. auto.
-    unfold NE.of_list in IHa. fold (@NE.of_list A) in IHa. rewrite IHa in Heqo0. inv Heqo0.
-  Qed.
-
-  Lemma NEof_list_contra :
-    forall A b (a: A),
-      ~ NE.of_list (a :: b) = None.
-  Proof.
-    induction b; try solve [crush].
-    intros.
-    specialize (IHb a).
-    enough (X: exists x, NE.of_list (a :: b) = Some x).
-    inversion_clear X as [x X'].
-    erewrite NEof_list_some; eauto; discriminate.
-    destruct (NE.of_list (a :: b)) eqn:?; [eauto|contradiction].
-  Qed.
-
-  Lemma NEof_list_exists :
-    forall A b (a: A),
-      exists x, NE.of_list (a :: b) = Some x.
-  Proof.
-    intros. pose proof (NEof_list_contra _ b a).
-    destruct (NE.of_list (a :: b)); try contradiction.
-    eauto.
-  Qed.
-
-  Lemma NEof_list_exists2 :
-    forall A b (a c: A),
-      exists x,
-        NE.of_list (c :: a :: b) = Some (NE.cons c x)
-        /\ NE.of_list (a :: b) = Some x.
-  Proof.
-    intros. pose proof (NEof_list_exists _ b a).
-    inversion_clear H as [x B].
-    econstructor; split; eauto.
-    eapply NEof_list_some; eauto.
-  Qed.
-
-  Lemma NEof_list_to_list :
-    forall A (x: list A) y,
-      NE.of_list x = Some y ->
-      NE.to_list y = x.
-  Proof.
-    induction x; [crush|].
-    intros. destruct x; [crush|].
-    pose proof (NEof_list_exists2 _ x a0 a).
-    inversion_clear H0 as [x0 [HN1 HN2]]. rewrite HN1 in H. inv H.
-    cbn. f_equal. eauto.
-  Qed.
-
-  Lemma sem_pred_expr_merge :
-    forall G (ctx: @Abstr.ctx G) ps l args,
-      Forall2 (sem_pred_expr ps sem_ident ctx) args l ->
-      sem_pred_expr ps sem_ident ctx (merge args) (to_elist l).
-  Proof.
-    induction l; intros.
-    - inv H. cbn; repeat constructor.
-    - inv H. cbn. unfold merge. Admitted.
-
-  Lemma sem_pred_expr_merge2 :
-    forall A (ctx: @ctx A) pr l l',
-      sem_pred_expr pr sem_ident ctx (merge l) l' ->
-      Forall2 (sem_pred_expr pr sem_ident ctx) l (of_elist l').
-  Proof.
-    induction l; crush.
-    - unfold merge in *; cbn in *.
-      inv H. inv H5. constructor.
-    - unfold merge in H.
-      pose proof (NEof_list_exists _ l a) as Y.
-      inversion_clear Y as [x HNE]. rewrite HNE in H.
-      erewrite <- (NEof_list_to_list _ (a :: l)) by eassumption.
-      apply sem_pred_expr_fold_right2 with (s := (NE.singleton (T, Enil))) (s' := Enil).
-      repeat constructor.
-      rewrite Eapp_right_nil. auto.
-  Qed.
-
-  Lemma sem_merge_list :
-    forall A ctx f rs ps m args,
-      sem ctx f ((mk_instr_state rs ps m), None) ->
-      @sem_pred_expr A _ _ (forest_preds f) sem_val_list ctx
-        (merge (list_translation args f)) (rs ## args).
-  Proof.
-    induction args; crush. cbn. constructor; constructor.
-    unfold merge. specialize (IHargs H).
-    eapply sem_pred_expr_ident2 in IHargs.
-    inversion_clear IHargs as [l_ [HSEM HVAL]].
-    destruct_match; [|exfalso; eapply NEof_list_contra; eauto].
-    destruct args; cbn -[NE.of_list] in *.
-    - unfold merge in *. simplify.
-      inv H. inv H6. specialize (H a).
-      eapply sem_pred_expr_ident2 in H.
-      inversion_clear H as [l_2 [HSEM2 HVAL2]].
-      unfold cons_pred_expr.
-      eapply sem_pred_expr_ident.
-      eapply sem_pred_expr_predicated_map.
-      eapply sem_pred_expr_predicated_prod; [eassumption|repeat constructor].
-      repeat constructor; auto.
-    - pose proof (NEof_list_exists2 _ (list_translation args f) (f #r (Reg r)) (f #r (Reg a))) as Y.
-      inversion_clear Y as [x [Y1 Y2]]. rewrite Heqo in Y1. inv Y1.
-      inversion_clear H as [? ? ? ? ? ? REG PRED MEM EXIT].
-      inversion_clear REG as [? ? ? REG'].
-      inversion_clear PRED as [? ? ? PRED'].
-      pose proof (REG' a) as REGa. pose proof (REG' r) as REGr.
-      exploit sem_pred_expr_ident2; [exact REGa|].
-      intro REGI'; inversion_clear REGI' as [a' [SEMa SEMa']].
-      exploit sem_pred_expr_ident2; [exact REGr|].
-      intro REGI'; inversion_clear REGI' as [r' [SEMr SEMr']].
-      apply sem_pred_expr_ident with (l_ := Econs a' l_); [|constructor; auto].
-      replace (Econs a' l_) with (Eapp (Econs a' l_) Enil) by (now apply Eapp_right_nil).
-      apply sem_pred_expr_fold_right; eauto.
-      repeat constructor.
-      constructor; eauto.
-      erewrite NEof_list_to_list; eauto.
-      eapply sem_pred_expr_merge2; auto.
-  Qed.
-
-  Lemma sem_pred_expr_list_translation :
-    forall G ctx args f i,
-      @sem G ctx f (i, None) ->
-      exists l,
-        Forall2 (sem_pred_expr (forest_preds f) sem_ident ctx) (list_translation args f) l
-        /\ sem_val_list ctx (to_elist l) ((is_rs i)##args).
-  Proof.
-    induction args; intros.
-    - exists nil; cbn; split; auto; constructor.
-    - exploit IHargs; try eassumption; intro EX.
-      inversion_clear EX as [l [FOR SEM]].
-      destruct i as [rs' m' ps'].
-      inversion_clear H as [? ? ? ? ? ? REGSET PREDSET MEM EXIT].
-      inversion_clear REGSET as [? ? ? REG].
-      pose proof (REG a).
-      exploit sem_pred_expr_ident2; eauto; intro IDENT.
-      inversion_clear IDENT as [l_ [SEMP SV]].
-      exists (l_ :: l). split. constructor; auto.
-      cbn; constructor; auto.
-  Qed.
-
-Lemma evaluable_and_true :
-  forall G (ctx: @ctx G) ps p,
-    p_evaluable ctx (from_pred_op ps p) ->
-    p_evaluable ctx (from_pred_op ps (p ∧ T)).
-Proof.
-  intros. unfold evaluable in *. inv H. exists (x && true). cbn.
-  apply sem_pexpr_Pand; auto. constructor.
-Qed.
-
-Lemma NEin_map :
-  forall A B p y (f: A -> B) a,
-    NE.In (p, y) (predicated_map f a) ->
-    exists x, NE.In (p, x) a /\ y = f x.
-Proof.
-  induction a; intros.
-  - inv H. destruct a. econstructor. split; eauto. constructor.
-  - inv H. inv H1. inv H. destruct a. cbn in *. econstructor; econstructor; eauto.
-    constructor; tauto.
-    specialize (IHa H). inv IHa. inv H0.
-    econstructor; econstructor; eauto. constructor; tauto.
-Qed.
-
-Lemma NEin_map2 :
-  forall A B (f: A -> B) a p y,
-    NE.In (p, y) a ->
-    NE.In (p, f y) (predicated_map f a).
-Proof.
-  induction a; crush.
-  inv H. constructor.
-  inv H. inv H1.
-  - constructor; auto.
-  - constructor; eauto.
-Qed.
-
-Lemma all_evaluable_predicated_map :
-  forall A B G (ctx: @ctx G) ps (f: A -> B) p,
-    all_evaluable ctx ps p ->
-    all_evaluable ctx ps (predicated_map f p).
-Proof.
-  induction p.
-  - unfold all_evaluable; intros.
-    exploit NEin_map; eauto; intros. inv H1. inv H2.
-    eapply H; eauto.
-  - intros. cbn.
-    eapply all_evaluable_cons3. eapply IHp. eapply all_evaluable_cons; eauto.
-    cbn. destruct a. cbn in *. eapply all_evaluable_cons2; eauto.
-Qed.
-
-Lemma all_evaluable_predicated_map2 :
-  forall A B G (ctx: @ctx G) ps (f: A -> B) p,
-    all_evaluable ctx ps (predicated_map f p) ->
-    all_evaluable ctx ps p.
-Proof.
-  induction p.
-  - unfold all_evaluable in *; intros.
-    eapply H. eapply NEin_map2; eauto.
-  - intros. cbn. destruct a.
-    cbn in H. pose proof H. eapply all_evaluable_cons in H; eauto.
-    eapply all_evaluable_cons2 in H0; eauto.
-    unfold all_evaluable. specialize (IHp H).
-    unfold all_evaluable in IHp.
-    intros. inv H1. inv H3. inv H1; eauto.
-    specialize (IHp _ _ H1). eauto.
-Qed.
-
-Lemma all_evaluable_map_and :
-  forall A B G (ctx: @ctx G) ps (a: NE.non_empty ((pred_op * A) * (pred_op * B))),
-    (forall p1 x p2 y,
-       NE.In ((p1, x), (p2, y)) a ->
-            p_evaluable ctx (from_pred_op ps p1)
-            /\ p_evaluable ctx (from_pred_op ps p2)) ->
-    all_evaluable ctx ps (NE.map (fun x => match x with ((a, b), (c, d)) => (Pand a c, (b, d)) end) a).
-Proof.
-  induction a.
-  - intros. cbn. repeat destruct_match. inv Heqp.
-    unfold all_evaluable; intros. inv H0.
-    unfold evaluable.
-    exploit H. constructor.
-    intros [Ha Hb]. inv Ha. inv Hb.
-    exists (x && x0). apply sem_pexpr_Pand; auto.
-  - intros. unfold all_evaluable; cbn; intros. inv H0. inv H2.
-    + repeat destruct_match. inv Heqp0. inv H0.
-      specialize (H p2 a1 p3 b ltac:(constructor; eauto)).
-      inv H. inv H0. inv H1. exists (x && x0).
-      apply sem_pexpr_Pand; eauto.
-    + eapply IHa; intros. eapply H. econstructor. right. eauto.
-      eauto.
-Qed.
-
-Lemma all_evaluable_map_add :
-  forall A B G (ctx: @ctx G) ps (a: pred_op * A) (b: predicated B) p1 x p2 y,
-    p_evaluable ctx (from_pred_op ps (fst a)) ->
-    all_evaluable ctx ps b ->
-    NE.In (p1, x, (p2, y)) (NE.map (fun x : pred_op * B => (a, x)) b) ->
-    p_evaluable ctx (from_pred_op ps p1) /\ p_evaluable ctx (from_pred_op ps p2).
-Proof.
-  induction b; intros.
-  - cbn in *. inv H1. unfold all_evaluable in *. specialize (H0 _ _ ltac:(constructor)).
-    auto.
-  - cbn in *. inv H1. inv H3.
-    + inv H1. unfold all_evaluable in H0. specialize (H0 _ _ ltac:(constructor; eauto)); auto.
-    + eapply all_evaluable_cons in H0. specialize (IHb _ _ _ _ H H0 H1). auto.
-Qed.
-
-Lemma NEin_NEapp5 :
-  forall A (a: A) x y,
-    NE.In a (NE.app x y) ->
-    NE.In a x \/ NE.In a y.
-Proof.
-  induction x; crush.
-  - inv H. inv H1. left. constructor. tauto.
-  - inv H. inv H1. left. constructor; tauto.
-    exploit IHx; eauto; intros. inv H0.
-    left. constructor; tauto. tauto.
-Qed.
-
-Lemma all_evaluable_non_empty_prod :
-  forall A B G (ctx: @ctx G) ps p1 x p2 y (a: predicated A) (b: predicated B),
-    all_evaluable ctx ps a ->
-    all_evaluable ctx ps b ->
-    NE.In ((p1, x), (p2, y)) (NE.non_empty_prod a b) ->
-    p_evaluable ctx (from_pred_op ps p1)
-    /\ p_evaluable ctx (from_pred_op ps p2).
-Proof.
-  induction a; intros.
-  - cbn in *. eapply all_evaluable_map_add; eauto. destruct a; cbn in *. eapply H; constructor.
-  - cbn in *. eapply NEin_NEapp5 in H1. inv H1. eapply all_evaluable_map_add; eauto.
-    destruct a; cbn in *. eapply all_evaluable_cons2; eauto.
-    eapply all_evaluable_cons in H. eauto.
-Qed.
-
-Lemma all_evaluable_predicated_prod :
-  forall A B G (ctx: @ctx G) ps (a: predicated A) (b: predicated B),
-    all_evaluable ctx ps a ->
-    all_evaluable ctx ps b ->
-    all_evaluable ctx ps (predicated_prod a b).
-Proof.
-  intros. unfold all_evaluable; intros.
-  unfold predicated_prod in *. exploit all_evaluable_map_and.
-  2: { eauto. }
-  intros. 2: { eauto. }
-Admitted. (* Requires simple lemma to prove, but this lemma is not needed. *)
-
-Lemma cons_pred_expr_evaluable :
-  forall G (ctx: @ctx G) ps a b,
-    all_evaluable ctx ps a ->
-    all_evaluable ctx ps b ->
-    all_evaluable ctx ps (cons_pred_expr a b).
-Proof.
-  unfold cons_pred_expr; intros.
-  apply all_evaluable_predicated_map.
-  now apply all_evaluable_predicated_prod.
-Qed.
-
-Lemma fold_right_all_evaluable :
-  forall G (ctx: @ctx G) ps n,
-    Forall (all_evaluable ctx ps) (NE.to_list n) ->
-    all_evaluable ctx ps (NE.fold_right cons_pred_expr (NE.singleton (T, Enil)) n).
-Proof.
-  induction n; cbn in *; intros.
-  - unfold cons_pred_expr. eapply all_evaluable_predicated_map. eapply all_evaluable_predicated_prod.
-    inv H. auto. unfold all_evaluable; intros. inv H0. exists true. constructor.
-  - inv H. specialize (IHn H3). now eapply cons_pred_expr_evaluable.
-Qed.
-
-Lemma merge_all_evaluable :
-  forall G (ctx: @ctx G) ps,
-    pred_forest_evaluable ctx ps ->
-    forall f args,
-      all_evaluable ctx ps (merge (list_translation args f)).
-Proof.
-  intros. eapply predicated_evaluable_all. eauto.
-Qed.
-
-(*|
-Here we can finally assume that everything in the forest is evaluable, which
-will allow us to prove that translating the list of register accesses will also
-all be evaluable.
-|*)
-
-  Lemma sem_update_Iop :
-    forall A op rs args m v f ps ctx,
-      Op.eval_operation (ctx_ge ctx) (ctx_sp ctx) op rs ## args (is_mem (ctx_is ctx)) = Some v ->
-      sem ctx f ((mk_instr_state rs ps m), None) ->
-      @sem_pred_expr A _ _ (forest_preds f) sem_value ctx
-        (seq_app (pred_ret (Eop op)) (merge (list_translation args f))) v.
-  Proof.
-    intros * EVAL SEM.
-    exploit sem_pred_expr_list_translation; try eassumption.
-    intro H; inversion_clear H as [x [HS HV]].
-    eapply sem_pred_expr_seq_app_val.
-    - cbn in *; eapply sem_pred_expr_merge; eauto.
-    - apply sem_pred_expr_pred_ret.
-    - econstructor; [eauto|]; auto.
-  Qed.
-
-  Lemma sem_update_Iload :
-    forall A rs args m v f ps ctx addr a0 chunk,
-      Op.eval_addressing (ctx_ge ctx) (ctx_sp ctx) addr rs ## args = Some a0 ->
-      Mem.loadv chunk m a0 = Some v ->
-      sem ctx f ((mk_instr_state rs ps m), None) ->
-      @sem_pred_expr A _ _ (forest_preds f) sem_value ctx
-        (seq_app (seq_app (pred_ret (Eload chunk addr)) (merge (list_translation args f))) (f #r Mem)) v.
-  Proof.
-    intros * EVAL MEM SEM.
-    exploit sem_pred_expr_list_translation; try eassumption.
-    intro H; inversion_clear H as [x [HS HV]].
-    inversion SEM as [? ? ? ? ? ? REG PRED HMEM EXIT]; subst.
-    exploit sem_pred_expr_ident2; [eapply HMEM|].
-    intros H; inversion_clear H as [x' [HS' HV']].
-    eapply sem_pred_expr_seq_app_val; eauto.
-    { eapply sem_pred_expr_seq_app; eauto.
-      - eapply sem_pred_expr_merge; eauto.
-      - apply sem_pred_expr_pred_ret.
-    }
-    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'
-      (EVALF: forest_evaluable ctx f),
-      Op.eval_addressing (ctx_ge ctx) (ctx_sp ctx) addr rs ## args = Some a0 ->
-      Mem.storev chunk m a0 v' = Some m' ->
-      sem_value ctx v v' ->
-      sem ctx f ((mk_instr_state rs ps m), None) ->
-      @sem_pred_expr A _ _ (forest_preds f) sem_mem ctx
-        (seq_app (seq_app (pred_ret (Estore v chunk addr))
-          (merge (list_translation args f))) (f #r Mem)) m'.
-  Proof.
-    intros * EVALF EVAL STOREV SEMVAL SEM.
-    exploit sem_merge_list; try eassumption.
-    intro MERGE. exploit sem_pred_expr_ident2; eauto.
-    intro TMP; inversion_clear TMP as [x [HS HV]].
-    inversion_clear SEM as [? ? ? ? ? ? REG PRED HMEM EXIT].
-    exploit sem_pred_expr_ident2; [eapply HMEM|].
-    intros TMP; inversion_clear TMP as [x' [HS' HV']].
-    eapply sem_pred_expr_ident.
-    eapply sem_pred_expr_seq_app; eauto.
-    eapply sem_pred_expr_seq_app; eauto.
-    eapply sem_pred_expr_pred_ret.
-    econstructor; eauto.
-  Qed.
-
-  Lemma sem_update_Iop_top:
-    forall A f p p' f' rs m pr op res args p0 v state,
-      Op.eval_operation (ctx_ge state) (ctx_sp state) op rs ## args m = Some v ->
-      truthy pr p0 ->
-      valid_mem (is_mem (ctx_is state)) m ->
-      sem state f ((mk_instr_state rs pr m), None) ->
-      update (p, f) (RBop p0 op args res) = Some (p', f') ->
-      eval_predf pr p = true ->
-      @sem A state f' (mk_instr_state (rs # res <- v) pr m, None).
-    Proof.
-      intros * EVAL_OP TRUTHY VALID SEM UPD EVAL_PRED.
-      pose proof SEM as SEM2.
-      inversion UPD as [PRUNE]. unfold Option.bind in PRUNE.
-      destr. inversion_clear PRUNE.
-      rename Heqo into PRUNE.
-      inversion_clear SEM as [? ? ? ? ? ? REG PRED MEM EXIT].
-      cbn [is_ps] in *. constructor.
-      + constructor; intro x. inversion_clear REG as [? ? ? REG']. specialize (REG' x).
-        destruct f as [fr fp fe]. cbn [forest_preds set_forest] in *.
-        destruct (peq x res); subst.
-        * rewrite forest_reg_gss in *. rewrite Regmap.gss in *.
-          eapply sem_pred_expr_prune_predicated; eauto.
-          eapply sem_pred_expr_app_predicated; [| |eauto].
-          replace fp with (forest_preds {| forest_regs := fr; forest_preds := fp; forest_exit := fe |}) by auto.
-          eapply sem_update_Iop; eauto. cbn in *.
-          eapply eval_operation_valid_pointer; eauto.
-          inversion_clear SEM2 as [? ? ? ? ? ? REG2 PRED2 MEM2 EXIT2].
-          inversion_clear PRED2; eauto.
-          cbn -[eval_predf]. rewrite eval_predf_Pand.
-          rewrite EVAL_PRED. rewrite truthy_dflt; auto.
-        * rewrite forest_reg_gso. rewrite Regmap.gso; auto.
-          unfold not in *; intros. apply n0. inv H; auto.
-      + constructor; intros. inv PRED. rewrite forest_reg_pred. auto.
-      + rewrite forest_reg_gso; auto; discriminate.
-      + auto.
-  Qed.
-
-  Lemma sem_update_Iload_top:
-    forall A f p p' f' rs m pr res args p0 v state addr a chunk,
-      Op.eval_addressing (ctx_ge state) (ctx_sp state) addr rs ## args = Some a ->
-      Mem.loadv chunk m a = Some v ->
-      truthy pr p0 ->
-      valid_mem (is_mem (ctx_is state)) m ->
-      sem state f ((mk_instr_state rs pr m), None) ->
-      update (p, f) (RBload p0 chunk addr args res) = Some (p', f') ->
-      eval_predf pr p = true ->
-      @sem A state f' (mk_instr_state (rs # res <- v) pr m, None).
-    Proof.
-      intros * EVAL_OP LOAD TRUTHY VALID SEM UPD EVAL_PRED.
-      pose proof SEM as SEM2.
-      inversion UPD as [PRUNE]. unfold Option.bind in PRUNE. destr.
-      inversion_clear PRUNE.
-      rename Heqo into PRUNE.
-      inversion_clear SEM as [? ? ? ? ? ? REG PRED MEM EXIT].
-      cbn [is_ps] in *. constructor.
-      + constructor; intro x. inversion_clear REG as [? ? ? REG']. specialize (REG' x).
-        destruct f as [fr fp fe]. cbn [forest_preds set_forest] in *.
-        destruct (peq x res); subst.
-        * rewrite forest_reg_gss in *. rewrite Regmap.gss in *.
-          eapply sem_pred_expr_prune_predicated; eauto.
-          eapply sem_pred_expr_app_predicated; [| |eauto].
-          replace fp with (forest_preds {| forest_regs := fr; forest_preds := fp; forest_exit := fe |}) by auto.
-          eapply sem_update_Iload; eauto.
-          inversion_clear PRED; eauto.
-          cbn -[eval_predf]. rewrite eval_predf_Pand.
-          rewrite EVAL_PRED. rewrite truthy_dflt; auto.
-        * rewrite forest_reg_gso. rewrite Regmap.gso; auto.
-          unfold not in *; intros. apply n0. inv H; auto.
-      + constructor; intros. inv PRED. rewrite forest_reg_pred. auto.
-      + rewrite forest_reg_gso; auto; discriminate.
-      + 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 ->
-      Mem.storev chunk m a rs !! res = Some m' ->
-      truthy pr p0 ->
-      valid_mem (is_mem (ctx_is state)) m ->
-      sem state f ((mk_instr_state rs pr m), None) ->
-      update (p, f) (RBstore p0 chunk addr args res) = Some (p', f') ->
-      eval_predf pr p = true ->
-      @sem A state f' (mk_instr_state rs pr m', None).
-  Proof.
-    intros * EVAL_OP STORE TRUTHY VALID SEM UPD EVAL_PRED.
-    pose proof SEM as SEM2.
-    inversion UPD as [PRUNE]. unfold Option.bind in PRUNE. destr.
-    inversion_clear PRUNE.
-    rename Heqo into PRUNE.
-    inversion_clear SEM as [? ? ? ? ? ? REG PRED MEM EXIT].
-    cbn [is_ps] in *. constructor.
-    + constructor; intros. inv REG. rewrite forest_reg_gso; eauto. discriminate.
-    + constructor; intros. inv PRED. rewrite forest_reg_pred. auto.
-    + destruct f as [fr fp fm]; cbn -[seq_app] in *.
-      rewrite forest_reg_gss.
-      exploit sem_pred_expr_ident2; [exact MEM|]; intro HSEM_;
-        inversion_clear HSEM_ as [x [HSEM1 HSEM2]].
-      inv REG. specialize (H res).
-      pose proof H as HRES.
-      eapply sem_pred_expr_ident2 in HRES.
-      inversion_clear HRES as [r2 [HRES1 HRES2]].
-      apply exists_sem_pred in H. inversion_clear H as [r' [HNE HVAL]].
-      exploit sem_merge_list. eapply SEM2. instantiate (2 := args). intro HSPE. eapply sem_pred_expr_ident2 in HSPE.
-      inversion_clear HSPE as [l_ [HSPE1 HSPE2]].
-      eapply sem_pred_expr_prune_predicated; eauto.
-      eapply sem_pred_expr_app_predicated.
-      eapply sem_pred_expr_seq_app_val; [solve [eauto]| |].
-      eapply sem_pred_expr_seq_app; [solve [eauto]|].
-      eapply sem_pred_expr_flap2.
-      eapply sem_pred_expr_seq_app; [solve [eauto]|].
-      eapply sem_pred_expr_pred_ret. econstructor. eauto. 3: { eauto. }
-      eauto. auto. eauto. inv PRED. eauto.
-      rewrite eval_predf_Pand. rewrite EVAL_PRED.
-      rewrite truthy_dflt. auto. auto.
-    + 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 ->
-      sem_pexpr ctx (from_pred_op ps p0) b ->
-      sem_pexpr ctx (from_pred_op (PTree.set p e ps) p0) b.
-  Proof.
-    induction p0; auto; intros.
-    - cbn. destruct p. unfold get_forest_p'.
-      assert (p0 <> p) by
-        (unfold not; intros; apply H; subst; constructor).
-      rewrite PTree.gso; auto.
-    - cbn in *.
-      assert (X: ~ PredIn p p0_1 /\ ~ PredIn p p0_2) by
-        (split; unfold not; intros; apply H; constructor; tauto).
-      inversion_clear X as [X1 X2].
-      inv H0. inv H4.
-      specialize (IHp0_1 _ p e _ X1 H0). constructor. tauto.
-      specialize (IHp0_2 _ p e _ X2 H0). constructor. tauto.
-      constructor; auto.
-    - cbn in *.
-      assert (X: ~ PredIn p p0_1 /\ ~ PredIn p p0_2) by
-        (split; unfold not; intros; apply H; constructor; tauto).
-      inversion_clear X as [X1 X2].
-      inv H0. inv H4.
-      specialize (IHp0_1 _ p e _ X1 H0). constructor. tauto.
-      specialize (IHp0_2 _ p e _ X2 H0). constructor. tauto.
-      constructor; auto.
-  Qed.
-
-  Lemma sem_pred_not_in :
-    forall A B G (ctx: @ctx G) (s: @Abstr.ctx G -> A -> B -> Prop) l v p e ps,
-      sem_pred_expr ps s ctx l v ->
-      predicated_not_inP p l ->
-      sem_pred_expr (PTree.set p e ps) s ctx l v.
-  Proof.
-    induction l.
-    - intros. unfold predicated_not_inP in H0.
-      destruct a. constructor. apply sem_pexpr_not_in.
-      eapply H0. econstructor. inv H. auto. inv H. auto.
-    - intros. inv H. constructor. unfold predicated_not_inP in H0.
-      eapply sem_pexpr_not_in. eapply H0. constructor. left. eauto.
-      auto. auto.
-      apply sem_pred_expr_cons_false. apply sem_pexpr_not_in. eapply H0.
-      constructor. tauto. auto. auto.
-      eapply IHl. eauto. eapply predicated_not_inP_cons; eauto.
-  Qed.
-
-  Lemma pred_not_in_forestP :
-    forall pred f,
-      predicated_not_in_forest pred f = true ->
-      forall x, predicated_not_inP pred (f #r x).
-  Proof. Admitted.
-
-  Lemma pred_not_in_forest_exitP :
-    forall pred f,
-      predicated_not_in_forest pred f = true ->
-      predicated_not_inP pred (forest_exit f).
-  Proof. Admitted.
-
-  Lemma from_predicated_sem_pred_expr :
-    forall A (ctx: @ctx A) preds pe b,
-      sem_pred_expr preds sem_pred ctx pe b ->
-      sem_pexpr ctx (from_predicated true preds pe) b.
-  Proof. Admitted.
-
-  Lemma sem_update_Isetpred:
-    forall A (ctx: @ctx A) f pr p0 c args b rs m,
-      valid_mem (ctx_mem ctx) m ->
-      sem ctx f (mk_instr_state rs pr m, None) ->
-      Op.eval_condition c rs ## args m = Some b ->
-      truthy pr p0 ->
-      sem_pexpr ctx
-      (from_predicated true (forest_preds f) (seq_app (pred_ret (PEsetpred c)) (merge (list_translation args f)))) b.
-  Proof.
-    intros. eapply from_predicated_sem_pred_expr.
-    pose proof (sem_merge_list _ ctx f rs pr m args H0).
-    apply sem_pred_expr_ident2 in H3; simplify.
-    eapply sem_pred_expr_seq_app_val; [eauto| |].
-    constructor. constructor. constructor.
-    econstructor; eauto.
-    erewrite storev_eval_condition; eauto.
-  Qed.
-
-  Lemma sem_update_Isetpred_top:
-    forall A f p p' f' rs m pr args p0 state c pred b,
-      Op.eval_condition c rs ## args m = Some b ->
-      truthy pr p0 ->
-      valid_mem (is_mem (ctx_is state)) m ->
-      sem state f ((mk_instr_state rs pr m), None) ->
-      update (p, f) (RBsetpred p0 c args pred) = Some (p', f') ->
-      eval_predf pr p = true ->
-      @sem A state f' (mk_instr_state rs (pr # pred <- b) m, None).
-  Proof.
-    intros * EVAL_OP TRUTHY VALID SEM UPD EVAL_PRED.
-    pose proof SEM as SEM2.
-    inversion UPD as [PRUNE]. unfold Option.bind in PRUNE. destr. destr.
-    inversion_clear PRUNE.
-    rename Heqo into PRUNE.
-    inversion_clear SEM as [? ? ? ? ? ? REG PRED MEM EXIT].
-    cbn [is_ps] in *. constructor.
-    + constructor. intros. apply sem_pred_not_in. rewrite forest_pred_reg.
-      inv REG. auto. rewrite forest_pred_reg. apply pred_not_in_forestP.
-      unfold assert_ in *. repeat (destruct_match; try discriminate); auto.
-    + constructor; intros. destruct (peq x pred); subst.
-      * rewrite Regmap.gss.
-        rewrite forest_pred_gss.
-        cbn [update] in *. unfold Option.bind in *. destr. destr. inv UPD.
-        replace b with (b && true) by eauto with bool.
-        apply sem_pexpr_Pand.
-        destruct b. constructor. right.
-        eapply sem_update_Isetpred; eauto.
-        constructor. constructor. replace false with (negb true) by auto.
-        apply sem_pexpr_negate. inv TRUTHY. constructor.
-        cbn. eapply sem_pexpr_eval. inv PRED. eauto. auto.
-        replace false with (negb true) by auto.
-        apply sem_pexpr_negate.
-        eapply sem_pexpr_eval. inv PRED. eauto. auto.
-        eapply sem_update_Isetpred; eauto.
-        constructor. constructor. constructor.
-        replace true with (negb false) by auto. apply sem_pexpr_negate.
-        eapply sem_pexpr_eval. inv PRED. eauto. inv TRUTHY. auto. cbn -[eval_predf].
-        rewrite eval_predf_negate. rewrite H; auto.
-        replace true with (negb false) by auto. apply sem_pexpr_negate.
-        eapply sem_pexpr_eval. inv PRED. eauto. rewrite eval_predf_negate.
-        rewrite EVAL_PRED. auto.
-      * rewrite Regmap.gso by auto. inv PRED. specialize (H x).
-        rewrite forest_pred_gso by auto; auto.
-    + rewrite forest_pred_reg. apply sem_pred_not_in. auto. apply pred_not_in_forestP.
-      unfold assert_ in *. now repeat (destruct_match; try discriminate).
-    + cbn -[from_predicated from_pred_op seq_app]. apply sem_pred_not_in; auto.
-      apply pred_not_in_forest_exitP.
-      unfold assert_ in *. now repeat (destruct_match; try discriminate).
-  Qed.
-
-  Lemma sem_pexpr_impl :
-    forall A (state: @ctx A) a b res,
-      sem_pexpr state b res ->
-      sem_pexpr state a true ->
-      sem_pexpr state (a → b) res.
-  Proof.
-    intros. destruct res.
-    constructor; tauto.
-    constructor; auto. replace false with (negb true) by auto.
-    now apply sem_pexpr_negate.
-  Qed.
-
-  Lemma eval_predf_simplify :
-    forall ps x,
-      eval_predf ps (simplify x) = eval_predf ps x.
-  Proof.
-    unfold eval_predf; intros.
-    rewrite simplify_correct. auto.
-  Qed.
-
-  Lemma sem_update_falsy:
-    forall A state f f' rs ps m p a p',
-      instr_falsy ps a ->
-      update (p, f) a = Some (p', f') ->
-      sem state f (mk_instr_state rs ps m, None) ->
-      @sem A state f' (mk_instr_state rs ps m, None).
-  Proof.
-    inversion 1; cbn [update] in *; intros.
-    - unfold Option.bind in *. destr. inv H2.
-      constructor.
-      * constructor. intros. destruct (peq x res); subst.
-        rewrite forest_reg_gss. cbn.
-        eapply sem_pred_expr_prune_predicated; eauto.
-        eapply sem_pred_expr_app_predicated_false. inv H3. inv H8. auto.
-        inv H3. inv H9. eauto. rewrite eval_predf_Pand. cbn -[eval_predf].
-        rewrite H0. auto. 
-        rewrite forest_reg_gso. inv H3. inv H8. auto.
-        unfold not; intros; apply n0. now inv H1.
-      * constructor; intros. rewrite forest_reg_pred. inv H3. inv H9. auto.
-      * rewrite forest_reg_gso. inv H3. auto. unfold not; intros. inversion H1.
-      * inv H3. auto.
-    - unfold Option.bind in *. destr. inv H2.
-      constructor.
-      * constructor. intros. destruct (peq x dst); subst.
-        rewrite forest_reg_gss. cbn.
-        eapply sem_pred_expr_prune_predicated; eauto.
-        eapply sem_pred_expr_app_predicated_false. inv H3. inv H8. auto.
-        inv H3. inv H9. eauto. rewrite eval_predf_Pand. cbn -[eval_predf].
-        rewrite H0. auto. 
-        rewrite forest_reg_gso. inv H3. inv H8. auto.
-        unfold not; intros; apply n0. now inv H1.
-      * constructor; intros. rewrite forest_reg_pred. inv H3. inv H9. auto.
-      * rewrite forest_reg_gso. inv H3. auto. unfold not; intros. inversion H1.
-      * inv H3. auto.
-    - unfold Option.bind in *. destr. inv H2.
-      constructor.
-      * constructor. intros. rewrite forest_reg_gso by discriminate. inv H3. inv H8. auto.
-      * constructor; intros. rewrite forest_reg_pred. inv H3. inv H9. auto.
-      * rewrite forest_reg_gss. cbn. eapply sem_pred_expr_prune_predicated; eauto.
-        eapply sem_pred_expr_app_predicated_false. inv H3. auto. inv H3. inv H9. eauto.
-        rewrite eval_predf_Pand. cbn -[eval_predf]. rewrite H0. auto.
-      * inv H3. auto.
-    - unfold Option.bind in *. destr. destr. inv H2.
-      constructor.
-      * constructor; intros. rewrite forest_pred_reg. apply sem_pred_not_in.
-        inv H3. inv H8. auto. apply pred_not_in_forestP. unfold assert_ in Heqo. now destr.
-      * constructor. intros. destruct (peq x pred); subst.
-        rewrite forest_pred_gss. replace (ps !! pred) with (true && ps !! pred) by auto.
-        assert (sem_pexpr state0 (¬ (from_pred_op (forest_preds f) p0 ∧ from_pred_op (forest_preds f) p')) true).
-        { replace true with (negb false) by auto. apply sem_pexpr_negate.
-          constructor. left. eapply sem_pexpr_eval. inv H3. inv H9. eauto.
-          auto.
-        }
-        apply sem_pexpr_Pand. constructor; tauto.
-        apply sem_pexpr_impl. inv H3. inv H10. eauto.
-        { constructor. left. eapply sem_pexpr_eval. inv H3. inv H10. eauto.
-          rewrite eval_predf_negate. rewrite H0. auto.
-        }
-        rewrite forest_pred_gso by auto. inv H3. inv H9. auto.
-      * rewrite forest_pred_reg. apply sem_pred_not_in. inv H3. auto.
-        apply pred_not_in_forestP. unfold assert_ in Heqo. now destr.
-      * apply sem_pred_not_in. inv H3; auto. cbn.
-        apply pred_not_in_forest_exitP. unfold assert_ in Heqo. now destr.
-    - unfold Option.bind in *. destr. inv H2. inv H3. constructor.
-      * constructor. inv H8. auto.
-      * constructor. intros. inv H9. eauto.
-      * auto.
-      * cbn. eapply sem_pred_expr_prune_predicated; [|eauto].
-        eapply sem_pred_expr_app_predicated_false; auto.
-        inv H9. eauto.
-        rewrite eval_predf_Pand. cbn -[eval_predf]. rewrite H0. auto.
-  Qed.
-
-  Lemma sem_update_falsy_input:
-    forall A state f f' rs ps m p a p' exitcf,
-      eval_predf ps p = false ->
-      update (p, f) a = Some (p', f') ->
-      sem state f (mk_instr_state rs ps m, exitcf) ->
-      @sem A state f' (mk_instr_state rs ps m, exitcf)
-        /\ eval_predf ps p' = false.
-  Proof.
-    intros; destruct a; cbn [update] in *; intros.
-    - inv H0. auto.
-    - unfold Option.bind in *. destr. inv H0. split; [|solve [auto]].
-      constructor.
-      * constructor. intros. destruct (peq x r); subst.
-        rewrite forest_reg_gss. cbn.
-        eapply sem_pred_expr_prune_predicated; eauto.
-        eapply sem_pred_expr_app_predicated_false. inv H1. inv H7. auto.
-        inv H1. inv H8. eauto. rewrite eval_predf_Pand.
-        rewrite H. eauto with bool.
-        rewrite forest_reg_gso. inv H1. inv H7. auto.
-        unfold not; intros; apply n0. now inv H0.
-      * constructor; intros. rewrite forest_reg_pred. inv H1. inv H8. auto.
-      * rewrite forest_reg_gso. inv H1. auto. unfold not; intros. inversion H0.
-      * inv H1. auto.
-    - unfold Option.bind in *. destr. inv H0. split; [|solve [auto]].
-      constructor.
-      * constructor. intros. destruct (peq x r); subst.
-        rewrite forest_reg_gss. cbn.
-        eapply sem_pred_expr_prune_predicated; eauto.
-        eapply sem_pred_expr_app_predicated_false. inv H1. inv H7. auto.
-        inv H1. inv H8. eauto. rewrite eval_predf_Pand. cbn -[eval_predf].
-        rewrite H. eauto with bool.
-        rewrite forest_reg_gso. inv H1. inv H7. auto.
-        unfold not; intros; apply n0. now inv H0.
-      * constructor; intros. rewrite forest_reg_pred. inv H1. inv H8. auto.
-      * rewrite forest_reg_gso. inv H1. auto. unfold not; intros. inversion H0.
-      * inv H1. auto.
-    - unfold Option.bind in *. destr. inv H0. split; [|solve [auto]].
-      constructor.
-      * constructor. intros. rewrite forest_reg_gso by discriminate. inv H1. inv H7. auto.
-      * constructor; intros. rewrite forest_reg_pred. inv H1. inv H8. auto.
-      * rewrite forest_reg_gss. cbn. eapply sem_pred_expr_prune_predicated; eauto.
-        eapply sem_pred_expr_app_predicated_false. inv H1. auto. inv H1. inv H8. eauto.
-        rewrite eval_predf_Pand. cbn -[eval_predf]. rewrite H. eauto with bool.
-      * inv H1. auto.
-    - unfold Option.bind in *. destr. destr. inv H0. split; [|solve [auto]].
-      constructor.
-      * constructor; intros. rewrite forest_pred_reg. apply sem_pred_not_in.
-        inv H1. inv H7. auto. apply pred_not_in_forestP. unfold assert_ in Heqo0. now destr.
-      * constructor. intros. destruct (peq x p0); subst.
-        rewrite forest_pred_gss. replace (ps !! p0) with (true && ps !! p0) by auto.
-        assert (sem_pexpr state0 (¬ (from_pred_op (forest_preds f) (dfltp o) ∧ from_pred_op (forest_preds f) p')) true).
-        { replace true with (negb false) by auto. apply sem_pexpr_negate.
-          constructor. right. eapply sem_pexpr_eval. inv H1. inv H8. eauto.
-          auto.
-        }
-        apply sem_pexpr_Pand. constructor; tauto.
-        apply sem_pexpr_impl. inv H1. inv H9. eauto.
-        { constructor. right. eapply sem_pexpr_eval. inv H1. inv H9. eauto.
-          rewrite eval_predf_negate. rewrite H. auto.
-        }
-        rewrite forest_pred_gso by auto. inv H1. inv H8. auto.
-      * rewrite forest_pred_reg. apply sem_pred_not_in. inv H1. auto.
-        apply pred_not_in_forestP. unfold assert_ in Heqo0. now destr.
-      * apply sem_pred_not_in. inv H1; auto. cbn.
-        apply pred_not_in_forest_exitP. unfold assert_ in Heqo0. now destr.
-    - unfold Option.bind in *. destr. inv H0. inv H1. split.
-      -- constructor.
-         * constructor. inv H7. auto.
-         * constructor. intros. inv H8. eauto.
-         * auto.
-         * cbn. eapply sem_pred_expr_prune_predicated; [|eauto].
-           eapply sem_pred_expr_app_predicated_false; auto.
-           inv H8. eauto.
-           rewrite eval_predf_Pand. cbn -[eval_predf]. rewrite H. eauto with bool.
-      -- rewrite eval_predf_simplify. rewrite eval_predf_Pand. rewrite H. eauto with bool.
-  Qed.
-
-  Definition setpred_wf (i: instr): bool :=
-    match i with
-    | RBsetpred (Some op) _ _ p => negb (predin peq p op)
-    | _ => true
-    end.
-
-  Lemma sem_update_instr :
-    forall f i' i'' a sp p i p' f',
-      step_instr ge sp (Iexec i') a (Iexec i'') ->
-      valid_mem (is_mem i) (is_mem i') ->
-      sem (mk_ctx i sp ge) f (i', None) ->
-      update (p, f) a = Some (p', f') ->
-      eval_predf (is_ps i') p = true ->
-      sem (mk_ctx i sp ge) f' (i'', None).
-  Proof.
-    inversion 1; subst; clear H; intros VALID SEM UPD EVAL_PRED; pose proof SEM as SEM2.
-    - inv UPD; auto.
-    - eauto using sem_update_Iop_top.
-    - eauto using sem_update_Iload_top.
-    - eauto using sem_update_Istore_top.
-    - eauto using sem_update_Isetpred_top.
-    - destruct i''. eauto using sem_update_falsy.
-  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 Pand_true_right :
-    forall ps a b,
-      eval_predf ps b = false ->
-      eval_predf ps (a ∧ b) = false.
-  Proof.
-    intros.
-    rewrite eval_predf_Pand. rewrite H.
-    eauto with bool.
-  Qed.
-
-  Lemma sem_update_instr_term :
-    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) (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.
-  Proof.
-    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.
-    constructor. inv H9. intros. cbn. eauto.
-    inv H10. constructor; intros. eauto.
-    cbn.
-    eapply sem_pred_expr_prune_predicated; eauto.
-    eapply sem_pred_expr_app_predicated.
-    constructor. constructor. constructor.
-    inv H10. eauto. cbn -[eval_predf] in *.
-    rewrite eval_predf_Pand. rewrite H2. now rewrite H6.
-  Qed.
-
-  Lemma step_instr_lessdef_term :
-    forall sp a i i' ti cf,
-      step_instr ge sp (Iexec i) a (Iterm i' cf) ->
-      Abstr.match_states i ti ->
-      exists ti', step_instr ge sp (Iexec ti) a (Iterm ti' cf) /\ Abstr.match_states i' ti'.
-  Proof.
-    inversion 1; intros; subst.
-    econstructor. split; eauto. constructor.
-    destruct p. constructor. erewrite eval_predf_pr_equiv. inv H4.
-    eauto. inv H6. eauto. constructor.
-  Qed.
-
-  Lemma combined_falsy :
-    forall i o1 o,
-      falsy i o1 ->
-      falsy i (combine_pred o o1).
-  Proof.
-    inversion 1; subst; crush. destruct o; simplify.
-    constructor. rewrite eval_predf_Pand. rewrite H0. crush.
-    constructor. auto.
-  Qed.
-
-  Lemma Abstr_match_states_sem :
-    forall i sp f i' ti cf,
-      sem (mk_ctx i sp ge) f (i', cf) ->
-      Abstr.match_states i ti ->
-      exists ti', sem (mk_ctx ti sp ge) f (ti', cf) /\ Abstr.match_states i' ti'.
-  Proof. Admitted. (* This needs a bit more in Abstr.v *)
-
-  Lemma mfold_left_update_Some :
-    forall xs x v,
-      mfold_left update xs x = Some v ->
-      exists y, x = Some y.
-  Proof.
-    induction xs; intros.
-    { cbn in *. inv H. eauto. }
-    cbn in *. unfold Option.bind in *. exploit IHxs; eauto.
-    intros. simplify. destruct x; crush.
-    eauto.
-  Qed.
-
-  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 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. destr. inv UPD. inv STEP; auto. cbn [is_ps] in *.
-      unfold is_initial_pred_and_notin in Heqo1. unfold assert_ in Heqo1. destr. destr.
-      destr. destr. destr. destr. subst. assert (~ PredIn p2 next_p).
-      unfold not; intros. apply negb_true_iff in Heqb0. apply not_true_iff_false in Heqb0.
-      apply Heqb0. now apply predin_PredIn. rewrite eval_predf_not_PredIn; auto.
-    - unfold Option.bind in *. destr. inv UPD. inv STEP. inv H3. cbn.
-      rewrite eval_predf_simplify. rewrite eval_predf_Pand. rewrite eval_predf_negate.
-      destruct i'; cbn in *. rewrite H0. auto.
-  Qed.
-
-  Lemma forest_evaluable_regset :
-    forall A f (ctx: @ctx A) n x,
-      forest_evaluable ctx f ->
-      forest_evaluable ctx f #r x <- n.
-  Proof.
-    unfold forest_evaluable, pred_forest_evaluable; intros.
-    eapply H. eauto.
-  Qed.
-
-  Lemma evaluable_impl :
-    forall A (ctx: @ctx A) a b,
-      p_evaluable ctx a ->
-      p_evaluable ctx b ->
-      p_evaluable ctx (a → b).
-  Proof.
-    unfold evaluable.
-    inversion_clear 1 as [b1 SEM1].
-    inversion_clear 1 as [b2 SEM2].
-    unfold Pimplies.
-    econstructor. apply sem_pexpr_Por;
-    eauto using sem_pexpr_negate.
-  Qed.
-
-  Lemma parts_evaluable :
-    forall A (ctx: @ctx A) b p0,
-      evaluable sem_pred ctx p0 ->
-      evaluable sem_pexpr ctx (Plit (b, p0)).
-  Proof.
-    intros. unfold evaluable in *. inv H.
-    destruct b. do 2 econstructor. eauto.
-    exists (negb x). constructor. rewrite negb_involutive. auto.
-  Qed.
-
-  Lemma p_evaluable_Pand :
-    forall A (ctx: @ctx A) a b,
-      p_evaluable ctx a ->
-      p_evaluable ctx b ->
-      p_evaluable ctx (a ∧ b).
-  Proof.
-    intros. inv H. inv H0.
-    econstructor. apply sem_pexpr_Pand; eauto.
-  Qed.
-
-  Lemma from_predicated_evaluable :
-    forall A (ctx: @ctx A) f b a,
-      pred_forest_evaluable ctx f ->
-      all_evaluable2 ctx sem_pred a ->
-      p_evaluable ctx (from_predicated b f a).
-  Proof.
-    induction a.
-    cbn. destruct_match; intros.
-    eapply evaluable_impl.
-    eauto using predicated_evaluable.
-    unfold all_evaluable2 in H0. unfold p_evaluable.
-    eapply parts_evaluable. eapply H0. econstructor.
-
-    intros. cbn. destruct_match.
-    eapply p_evaluable_Pand.
-    eapply all_evaluable2_cons2 in H0.
-    eapply evaluable_impl.
-    eauto using predicated_evaluable.
-    unfold all_evaluable2 in H0. unfold p_evaluable.
-    eapply parts_evaluable. eapply H0.
-    eapply all_evaluable2_cons in H0. eauto.
-  Qed.
-
-  Lemma seq_app_cons :
-    forall A B  f a l p0 p1,
-      @seq_app A B (pred_ret f) (NE.cons a l) = NE.cons p0 p1 ->
-      @seq_app A B (pred_ret f) l = p1.
-  Proof. intros. cbn in *. inv H. eauto. Qed.
-
-  Lemma p_evaluable_imp :
-    forall A (ctx: @ctx A) a b,
-      sem_pexpr ctx a false ->
-      p_evaluable ctx (a → b).
-  Proof.
-    intros. unfold "→".
-    unfold p_evaluable, evaluable. exists true.
-    constructor. replace true with (negb false) by trivial. left.
-    now apply sem_pexpr_negate.
-  Qed.
-
-  Lemma sem_update_valid_mem :
-    forall i i' i'' curr_p next_p f f_next instr sp,
-      step_instr ge sp (Iexec i') instr (Iexec i'') ->
-      update (curr_p, f) instr = Some (next_p, f_next) ->
-      sem (mk_ctx i sp ge) f (i', None) ->
-      valid_mem (is_mem i') (is_mem i'').
-  Proof.
-    inversion 1; crush.
-    unfold Option.bind in *. destr. inv H7.
-    eapply storev_valid_pointer; eauto.
-  Qed.
-
-  Lemma eval_predf_lessdef :
-    forall p a b,
-      Abstr.match_states 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.
-
-(*|
-``abstr_fold_falsy``: This lemma states that when we are at the end of an
-execution, the values in the register map do not continue to change.
-|*)
-
-  Lemma abstr_fold_falsy :
-    forall A ilist i sp ge f res p f' p',
-      @sem A (mk_ctx i sp ge) f res ->
-      mfold_left update ilist (Some (p, f)) = Some (p', f') ->
-      eval_predf (is_ps (fst res)) p = false ->
-      sem (mk_ctx i sp ge) f' res.
-  Proof.
-    induction ilist.
-    - intros. cbn in *. inv H0. auto.
-    - intros. cbn -[update] in H0.
-      exploit mfold_left_update_Some. eauto. intros. inv H2.
-      rewrite H3 in H0. destruct x.
-      destruct res. destruct i0.
-      exploit sem_update_falsy_input; try eassumption; intros.
-      inversion_clear H2.
-      eapply IHilist; eassumption.
-  Qed.
-
-  Lemma abstr_fold_correct :
-    forall sp x i i' i'' cf f p f' curr_p
-        (VALID: valid_mem (is_mem i) (is_mem i')),
-      SeqBB.step ge sp (Iexec i') x (Iterm i'' cf) ->
-      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,
-        Abstr.match_states i ti ->
-        exists ti', sem (mk_ctx ti sp ge) f' (ti', Some cf)
-               /\ Abstr.match_states i'' ti'
-               /\ valid_mem (is_mem i) (is_mem i'').
-  Proof.
-    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; cbn [fst snd] in *.
-      eauto.
-      transitivity (is_mem i'); auto.
-      eapply sem_update_valid_mem; eauto.
-      eauto.
-      eapply sem_update_instr; eauto. eauto. 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 Abstr_match_states_sem; (* TODO *)
-      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.
-      exploit abstr_fold_falsy.
-      apply A.
-      eassumption. auto. cbn. inversion Hi2; subst. auto. intros.
-      split; auto. split; auto.
-      inversion H7; subst; auto.
-  Qed.
-
-  Lemma sem_regset_empty :
-    forall A ctx, @sem_regset A ctx empty (ctx_rs ctx).
-  Proof using.
-    intros; constructor; intros.
-    constructor; auto. constructor.
-    constructor.
-  Qed.
-
-  Lemma sem_predset_empty :
-    forall A ctx, @sem_predset A ctx empty (ctx_ps ctx).
-  Proof using.
-    intros; constructor; intros.
-    constructor; auto. constructor.
-  Qed.
-
-  Lemma sem_empty :
-    forall A ctx, @sem A ctx empty (ctx_is ctx, None).
-  Proof using.
-    intros. destruct ctx. destruct ctx_is.
-    constructor; try solve [constructor; constructor; crush].
-    eapply sem_regset_empty.
-    eapply sem_predset_empty.
-  Qed.
-
-  Lemma abstr_sequence_correct :
-    forall sp x i i'' cf x',
-      SeqBB.step ge sp (Iexec i) x (Iterm i'' cf) ->
-      abstract_sequence x = Some x' ->
-      forall ti,
-        Abstr.match_states i ti ->
-        exists ti', sem (mk_ctx ti sp ge) x' (ti', Some cf)
-               /\ Abstr.match_states i'' ti'.
-  Proof.
-    unfold abstract_sequence. intros. unfold Option.map in H0.
-    destruct_match; try easy.
-    destruct p as [p TMP]; simplify.
-    exploit abstr_fold_correct; eauto; crush.
-    { apply sem_empty. }
-    exists x0. auto.
-  Qed.
-
-  Lemma abstr_seq_reverse_correct :
-    forall sp x i i' ti cf x',
-      abstract_sequence x = Some x' ->
-      sem (mk_ctx i sp ge) x' (i', (Some cf)) ->
-      Abstr.match_states i ti ->
-     exists ti', SeqBB.step ge sp (Iexec ti) x (Iterm ti' cf)
-             /\ Abstr.match_states i' ti'.
-  Proof.
-
-(*|
-Proof Sketch:
-
-We do an induction over the list of instructions ``x``.  This is trivial for the
-empty case and then for the inductive case we know that there exists an
-execution that matches the abstract execution, so we need to know that adding
-another instructions to it will still mean that the execution will result in the
-same value.
-
-Arithmetic operations will be a problem because we will have to show that these
-can be executed.  However, this should mostly be a problem in the abstract state
-comparison, because there two abstract states can be equal without one being
-evaluable.
-|*)
-
-  Admitted.
-
-(*|
-This is the top-level lemma which uses the following proofs to complete the
-square:
-
-- ``abstr_sequence_correct``: This is the lemma that states the forward
-  translation form ``GibleSeq`` to ``Abstr`` was correct.
-- ``abstr_check_correct``: This is the lemma that states that if a check between
-  two ``Abstr`` programs succeeds, that they will also behave the same.  This
-  depends on the SAT solver correctness, as the predicates might be
-  syntactically different to each other.
-- ``abstr_seq_reverse_correct``: This is the lemma that shows that the backwards
-  simulation between the abstract translation and the concrete execution also
-  holds.  We only have a translation from the concrete into the abstract, but
-  then prove that if we have an execution in the abstract, we can observe that
-  same execution in the concrete.
-- ``seqbb_step_parbb_step``: Finally, this lemma states that the parallel
-  execution of the basic block is equivalent to the sequential execution of the
-  concatenation of that parallel block.  This is because even in the translation
-  to HTL, the Verilog semantics are sequential within a clock cycle, but will
-  then be parallelised by the synthesis tool.  The argument for why this is
-  still useful is because we are identifying and scheduling instructions into
-  clock cycles.
-|*)
-
-  Definition local_abstr_check_correct :=
-    @abstr_check_correct GibleSeq.fundef GiblePar.fundef.
-
-  Definition local_abstr_check_correct2 :=
-    @abstr_check_correct GibleSeq.fundef GibleSeq.fundef.
-
-  Lemma ge_preserved_local :
-    ge_preserved ge tge.
-  Proof.
-    unfold ge_preserved; 
-    eauto using Op.eval_operation_preserved, Op.eval_addressing_preserved.
-  Qed.
-
   Lemma schedule_oracle_correct :
     forall x y sp i i' ti cf,
       schedule_oracle x y = true ->
       SeqBB.step ge sp (Iexec i) x (Iterm i' cf) ->
-      Abstr.match_states i ti ->
+      state_lessdef i ti ->
       exists ti', ParBB.step tge sp (Iexec ti) y (Iterm ti' cf)
-             /\ Abstr.match_states i' ti'.
+             /\ state_lessdef i' ti'.
   Proof.
     unfold schedule_oracle; intros. repeat (destruct_match; try discriminate). simplify.
     exploit abstr_sequence_correct; eauto; simplify.
@@ -2406,7 +479,7 @@ Proof Sketch:  Trivial because of structural equality.
   Lemma match_states_stepBB :
     forall s f sp pc rs pr m sf' f' trs tps tm rs' pr' m' trs' tpr' tm',
       match_states (GibleSeq.State s f sp pc rs pr m) (State sf' f' sp pc trs tps tm) ->
-      Abstr.match_states (mk_instr_state rs' pr' m') (mk_instr_state trs' tpr' tm') ->
+      state_lessdef (mk_instr_state rs' pr' m') (mk_instr_state trs' tpr' tm') ->
       match_states (GibleSeq.State s f sp pc rs' pr' m') (State sf' f' sp pc trs' tpr' tm').
   Proof.
     inversion 1; subst; simplify.