Adding support for prophecy variables to heap_lang

_CoqProject

@@ -87,6 +87,7 @@ theories/heap_lang/notation.v
 theories/heap_lang/proofmode.v
 theories/heap_lang/adequacy.v
 theories/heap_lang/total_adequacy.v
+theories/heap_lang/proph_map.v
 theories/heap_lang/prophecy.v
 theories/heap_lang/lib/spawn.v
 theories/heap_lang/lib/par.v

theories/heap_lang/adequacy.v

 From iris.program_logic Require Export weakestpre adequacy.
 From iris.algebra Require Import auth.
-From iris.heap_lang Require Import proofmode notation.
+From iris.heap_lang Require Import proofmode notation proph_map.
 From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 
-Class heapPreG Σ := HeapPreG {
-  heap_preG_iris :> invPreG Σ;
-  heap_preG_heap :> gen_heapPreG loc val Σ
+Class heap_prophPreG Σ := HeapProphPreG {
+  heap_proph_preG_iris :> invPreG Σ;
+  heap_proph_preG_heap :> gen_heapPreG loc val Σ;
+  heap_proph_preG_proph :> proph_mapPreG proph val Σ
 }.
 
-Definition heapΣ : gFunctors := #[invΣ; gen_heapΣ loc val].
-Instance subG_heapPreG {Σ} : subG heapΣ Σ → heapPreG Σ.
+Definition heapΣ : gFunctors := #[invΣ; gen_heapΣ loc val; proph_mapΣ proph val].
+Instance subG_heapPreG {Σ} : subG heapΣ Σ → heap_prophPreG Σ.
 Proof. solve_inG. Qed.
 
-Definition heap_adequacy Σ `{heapPreG Σ} s e σ φ :
+Definition heap_adequacy Σ `{heap_prophPreG Σ} s e σ φ :
   (∀ `{heapG Σ}, WP e @ s; ⊤ {{ v, ⌜φ v⌝ }}%I) →
   adequate s e σ (λ v _, φ v).
 Proof.
   intros Hwp; eapply (wp_adequacy _ _); iIntros (??) "".
-  iMod (gen_heap_init σ) as (?) "Hh".
-  iModIntro. iExists (fun σ _ => gen_heap_ctx σ). iFrame "Hh".
-  iApply (Hwp (HeapG _ _ _)).
+  iMod (gen_heap_init σ.1) as (?) "Hh".
+  iMod (proph_map_init κs σ.2) as (?) "Hp".
+  iModIntro.
+  iExists (fun σ κs => (gen_heap_ctx σ.1 ∗ proph_map_ctx κs σ.2)%I). iFrame.
+  iApply (Hwp (HeapG _ _ _ _)).
 Qed.

theories/heap_lang/lang.v

@@ -76,7 +76,10 @@ Inductive expr :=
   | Load (e : expr)
   | Store (e1 : expr) (e2 : expr)
   | CAS (e0 : expr) (e1 : expr) (e2 : expr)
-  | FAA (e1 : expr) (e2 : expr).
+  | FAA (e1 : expr) (e2 : expr)
+  (* Prophecy *)
+  | NewProph
+  | ResolveProph (e1 : expr) (e2 : expr).
 
 Bind Scope expr_scope with expr.
 
@@ -84,10 +87,10 @@ Fixpoint is_closed (X : list string) (e : expr) : bool :=
   match e with
   | Var x => bool_decide (x ∈ X)
   | Rec f x e => is_closed (f :b: x :b: X) e
-  | Lit _ => true
+  | Lit _ | NewProph => true
   | UnOp _ e | Fst e | Snd e | InjL e | InjR e | Fork e | Alloc e | Load e =>
      is_closed X e
-  | App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | Store e1 e2 | FAA e1 e2 =>
+  | App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | Store e1 e2 | FAA e1 e2 | ResolveProph e1 e2 =>
      is_closed X e1 && is_closed X e2
   | If e0 e1 e2 | Case e0 e1 e2 | CAS e0 e1 e2 =>
      is_closed X e0 && is_closed X e1 && is_closed X e2
@@ -108,7 +111,7 @@ Inductive val :=
 
 Bind Scope val_scope with val.
 
-Definition observation := Empty val.
+Definition observation : Set := proph * val.
 
 Fixpoint of_val (v : val) : expr :=
   match v with
@@ -163,7 +166,7 @@ Definition val_is_unboxed (v : val) : Prop :=
   end.
 
 (** The state: heaps of vals. *)
-Definition state := gmap loc val.
+Definition state : Type := gmap loc val * gset proph.
 
 (** Equality and other typeclass stuff *)
 Lemma to_of_val v : to_val (of_val v) = Some v.
@@ -230,12 +233,12 @@ Instance expr_countable : Countable expr.
 Proof.
  set (enc := fix go e :=
   match e with
-  | Var x => GenLeaf (inl (inl x))
-  | Rec f x e => GenNode 0 [GenLeaf (inl (inr f)); GenLeaf (inl (inr x)); go e]
+  | Var x => GenLeaf (Some (inl (inl x)))
+  | Rec f x e => GenNode 0 [GenLeaf (Some ((inl (inr f)))); GenLeaf (Some (inl (inr x))); go e]
   | App e1 e2 => GenNode 1 [go e1; go e2]
-  | Lit l => GenLeaf (inr (inl l))
-  | UnOp op e => GenNode 2 [GenLeaf (inr (inr (inl op))); go e]
-  | BinOp op e1 e2 => GenNode 3 [GenLeaf (inr (inr (inr op))); go e1; go e2]
+  | Lit l => GenLeaf (Some (inr (inl l)))
+  | UnOp op e => GenNode 2 [GenLeaf (Some (inr (inr (inl op)))); go e]
+  | BinOp op e1 e2 => GenNode 3 [GenLeaf (Some (inr (inr (inr op)))); go e1; go e2]
   | If e0 e1 e2 => GenNode 4 [go e0; go e1; go e2]
   | Pair e1 e2 => GenNode 5 [go e1; go e2]
   | Fst e => GenNode 6 [go e]
@@ -249,15 +252,17 @@ Proof.
   | Store e1 e2 => GenNode 14 [go e1; go e2]
   | CAS e0 e1 e2 => GenNode 15 [go e0; go e1; go e2]
   | FAA e1 e2 => GenNode 16 [go e1; go e2]
+  | NewProph => GenLeaf None
+  | ResolveProph e1 e2 => GenNode 17 [go e1; go e2]
   end).
  set (dec := fix go e :=
   match e with
-  | GenLeaf (inl (inl x)) => Var x
-  | GenNode 0 [GenLeaf (inl (inr f)); GenLeaf (inl (inr x)); e] => Rec f x (go e)
+  | GenLeaf (Some(inl (inl x))) => Var x
+  | GenNode 0 [GenLeaf (Some (inl (inr f))); GenLeaf (Some (inl (inr x))); e] => Rec f x (go e)
   | GenNode 1 [e1; e2] => App (go e1) (go e2)
-  | GenLeaf (inr (inl l)) => Lit l
-  | GenNode 2 [GenLeaf (inr (inr (inl op))); e] => UnOp op (go e)
-  | GenNode 3 [GenLeaf (inr (inr (inr op))); e1; e2] => BinOp op (go e1) (go e2)
+  | GenLeaf (Some (inr (inl l))) => Lit l
+  | GenNode 2 [GenLeaf (Some (inr (inr (inl op)))); e] => UnOp op (go e)
+  | GenNode 3 [GenLeaf (Some (inr (inr (inr op)))); e1; e2] => BinOp op (go e1) (go e2)
   | GenNode 4 [e0; e1; e2] => If (go e0) (go e1) (go e2)
   | GenNode 5 [e1; e2] => Pair (go e1) (go e2)
   | GenNode 6 [e] => Fst (go e)
@@ -271,6 +276,8 @@ Proof.
   | GenNode 14 [e1; e2] => Store (go e1) (go e2)
   | GenNode 15 [e0; e1; e2] => CAS (go e0) (go e1) (go e2)
   | GenNode 16 [e1; e2] => FAA (go e1) (go e2)
+  | GenLeaf None => NewProph
+  | GenNode 17 [e1; e2] => ResolveProph (go e1) (go e2)
   | _ => Lit LitUnit (* dummy *)
   end).
  refine (inj_countable' enc dec _). intros e. induction e; f_equal/=; auto.
@@ -308,7 +315,9 @@ Inductive ectx_item :=
   | CasMCtx (e0 : expr) (v2 : val)
   | CasRCtx (e0 : expr) (e1 : expr)
   | FaaLCtx (v2 : val)
-  | FaaRCtx (e1 : expr).
+  | FaaRCtx (e1 : expr)
+  | ProphLCtx (v2 : val)
+  | ProphRCtx (e1 : expr).
 
 Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
   match Ki with
@@ -334,6 +343,8 @@ Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
   | CasRCtx e0 e1 => CAS e0 e1 e
   | FaaLCtx v2 => FAA e (of_val v2)
   | FaaRCtx e1 => FAA e1 e
+  | ProphLCtx v2 => ResolveProph e (of_val v2)
+  | ProphRCtx e1 => ResolveProph e1 e
   end.
 
 (** Substitution *)
@@ -359,6 +370,8 @@ Fixpoint subst (x : string) (es : expr) (e : expr)  : expr :=
   | Store e1 e2 => Store (subst x es e1) (subst x es e2)
   | CAS e0 e1 e2 => CAS (subst x es e0) (subst x es e1) (subst x es e2)
   | FAA e1 e2 => FAA (subst x es e1) (subst x es e2)
+  | NewProph => NewProph
+  | ResolveProph e1 e2 => ResolveProph (subst x es e1) (subst x es e2)
   end.
 
 Definition subst' (mx : binder) (es : expr) : expr → expr :=
@@ -450,28 +463,35 @@ Inductive head_step : expr → state → option observation -> expr → state
   | ForkS e σ:
      head_step (Fork e) σ None (Lit LitUnit) σ [e]
   | AllocS e v σ l :
-     to_val e = Some v → σ !! l = None →
-     head_step (Alloc e) σ None (Lit $ LitLoc l) (<[l:=v]>σ) []
+     to_val e = Some v → σ.1 !! l = None →
+     head_step (Alloc e) σ None (Lit $ LitLoc l) (<[l:=v]>σ.1, σ.2) []
   | LoadS l v σ :
-     σ !! l = Some v →
+     σ.1 !! l = Some v →
      head_step (Load (Lit $ LitLoc l)) σ None (of_val v) σ []
   | StoreS l e v σ :
-     to_val e = Some v → is_Some (σ !! l) →
-     head_step (Store (Lit $ LitLoc l) e) σ None (Lit LitUnit) (<[l:=v]>σ) []
+     to_val e = Some v → is_Some (σ.1 !! l) →
+     head_step (Store (Lit $ LitLoc l) e) σ None (Lit LitUnit) (<[l:=v]>σ.1, σ.2) []
   | CasFailS l e1 v1 e2 v2 vl σ :
      to_val e1 = Some v1 → to_val e2 = Some v2 →
-     σ !! l = Some vl → vl ≠ v1 →
+     σ.1 !! l = Some vl → vl ≠ v1 →
      vals_cas_compare_safe vl v1 →
      head_step (CAS (Lit $ LitLoc l) e1 e2) σ None (Lit $ LitBool false) σ []
   | CasSucS l e1 v1 e2 v2 σ :
      to_val e1 = Some v1 → to_val e2 = Some v2 →
-     σ !! l = Some v1 →
+     σ.1 !! l = Some v1 →
      vals_cas_compare_safe v1 v1 →
-     head_step (CAS (Lit $ LitLoc l) e1 e2) σ None (Lit $ LitBool true) (<[l:=v2]>σ) []
+     head_step (CAS (Lit $ LitLoc l) e1 e2) σ None (Lit $ LitBool true) (<[l:=v2]>σ.1, σ.2) []
   | FaaS l i1 e2 i2 σ :
      to_val e2 = Some (LitV (LitInt i2)) →
-     σ !! l = Some (LitV (LitInt i1)) →
-     head_step (FAA (Lit $ LitLoc l) e2) σ None (Lit $ LitInt i1) (<[l:=LitV (LitInt (i1 + i2))]>σ) [].
+     σ.1 !! l = Some (LitV (LitInt i1)) →
+     head_step (FAA (Lit $ LitLoc l) e2) σ None (Lit $ LitInt i1) (<[l:=LitV (LitInt (i1 + i2))]>σ.1, σ.2) []
+  | NewProphS σ p :
+     p ∉ σ.2 →
+     head_step NewProph σ None (Lit $ LitProphecy p) (σ.1, {[ p ]} ∪ σ.2) []
+  | ResolveProphS e1 p e2 v σ :
+     to_val e1 = Some (LitV $ LitProphecy p) →
+     to_val e2 = Some v →
+     head_step (ResolveProph e1 e2) σ (Some (p, v)) (Lit LitUnit) σ [].
 
 (** Basic properties about the language *)
 Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
@@ -499,10 +519,15 @@ Proof.
 Qed.
 
 Lemma alloc_fresh e v σ :
-  let l := fresh (dom (gset loc) σ) in
-  to_val e = Some v → head_step (Alloc e) σ None (Lit (LitLoc l)) (<[l:=v]>σ) [].
+  let l := fresh (dom (gset loc) σ.1) in
+  to_val e = Some v → head_step (Alloc e) σ None (Lit (LitLoc l)) (<[l:=v]>σ.1, σ.2) [].
 Proof. by intros; apply AllocS, (not_elem_of_dom (D:=gset loc)), is_fresh. Qed.
 
+Lemma new_proph_fresh σ :
+  let p := fresh σ.2 in
+  head_step NewProph σ None (Lit $ LitProphecy p) (σ.1, {[ p ]} ∪ σ.2) [].
+Proof. constructor. apply is_fresh. Qed.
+
 (* Misc *)
 Lemma to_val_rec f x e `{!Closed (f :b: x :b: []) e} :
   to_val (Rec f x e) = Some (RecV f x e).

theories/heap_lang/lifting.v

+From iris.algebra Require Import auth gmap.
 From iris.base_logic Require Export gen_heap.
 From iris.program_logic Require Export weakestpre.
 From iris.program_logic Require Import ectx_lifting total_ectx_lifting.
-From iris.heap_lang Require Export lang.
+From iris.heap_lang Require Export lang proph_map.
 From iris.heap_lang Require Import tactics.
 From iris.proofmode Require Import tactics.
 From stdpp Require Import fin_maps.
@@ -9,12 +10,14 @@ Set Default Proof Using "Type".
 
 Class heapG Σ := HeapG {
   heapG_invG : invG Σ;
-  heapG_gen_heapG :> gen_heapG loc val Σ
+  heapG_gen_heapG :> gen_heapG loc val Σ;
+  heapG_proph_mapG :> proph_mapG proph val Σ
 }.
 
 Instance heapG_irisG `{heapG Σ} : irisG heap_lang Σ := {
   iris_invG := heapG_invG;
-  state_interp σ κs := gen_heap_ctx σ
+  state_interp σ κs :=
+    (gen_heap_ctx σ.1 ∗ proph_map_ctx κs σ.2)%I
 }.
 
 (** Override the notations so that scopes and coercions work out *)
@@ -26,6 +29,9 @@ Notation "l ↦{ q } -" := (∃ v, l ↦{q} v)%I
   (at level 20, q at level 50, format "l  ↦{ q }  -") : bi_scope.
 Notation "l ↦ -" := (l ↦{1} -)%I (at level 20) : bi_scope.
 
+Notation "p ⥱ v" := (p_mapsto p v) (at level 20, format "p ⥱ v") : bi_scope.
+Notation "p ⥱ -" := (∃ v, p ⥱ v)%I (at level 20) : bi_scope.
+
 (** The tactic [inv_head_step] performs inversion on hypotheses of the shape
 [head_step]. The tactic will discharge head-reductions starting from values, and
 simplifies hypothesis related to conversions from and to values, and finite map
@@ -127,7 +133,9 @@ Lemma wp_alloc s E e v :
   {{{ True }}} Alloc e @ s; E {{{ l, RET LitV (LitLoc l); l ↦ v }}}.
 Proof.
   iIntros (<- Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
-  iIntros (σ1 κs) "Hσ !>"; iSplit; first by eauto.
+  iIntros (σ1 κs) "[Hσ Hκs] !>"; iSplit.
+  (* TODO (MR) this used to be done by eauto. Why does it not work any more? *)
+  { iPureIntro. repeat eexists. by apply alloc_fresh. }
   iNext; iIntros (κ κs' v2 σ2 efs [Hstep ->]); inv_head_step.
   iMod (@gen_heap_alloc with "Hσ") as "[Hσ Hl]"; first done.
   iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
@@ -137,7 +145,9 @@ Lemma twp_alloc s E e v :
   [[{ True }]] Alloc e @ s; E [[{ l, RET LitV (LitLoc l); l ↦ v }]].
 Proof.
   iIntros (<- Φ) "_ HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
-  iIntros (σ1 κs) "Hσ !>"; iSplit; first by eauto.
+  iIntros (σ1 κs) "[Hσ Hκs] !>"; iSplit.
+  (* TODO (MR) this used to be done by eauto. Why does it not work any more? *)
+  { iPureIntro. repeat eexists. by apply alloc_fresh. }
   iIntros (κ κs' v2 σ2 efs [Hstep ->]); inv_head_step.
   iMod (@gen_heap_alloc with "Hσ") as "[Hσ Hl]"; first done.
   iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
@@ -147,7 +157,7 @@ Lemma wp_load s E l q v :
   {{{ ▷ l ↦{q} v }}} Load (Lit (LitLoc l)) @ s; E {{{ RET v; l ↦{q} v }}}.
 Proof.
   iIntros (Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
-  iIntros (σ1 κs) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
+  iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
   iSplit; first by eauto.
   iNext; iIntros (κ κs' v2 σ2 efs [Hstep ->]); inv_head_step.
   iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
@@ -156,7 +166,7 @@ Lemma twp_load s E l q v :
   [[{ l ↦{q} v }]] Load (Lit (LitLoc l)) @ s; E [[{ RET v; l ↦{q} v }]].
 Proof.
   iIntros (Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
-  iIntros (σ1 κs) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
+  iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
   iSplit; first by eauto.
   iIntros (κ κs' v2 σ2 efs [Hstep ->]); inv_head_step.
   iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
@@ -168,10 +178,13 @@ Lemma wp_store s E l v' e v :
 Proof.
   iIntros (<- Φ) ">Hl HΦ".
   iApply wp_lift_atomic_head_step_no_fork; auto.
-  iIntros (σ1 κs) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
-  iSplit; first by eauto 6. iNext; iIntros (κ κs' v2 σ2 efs [Hstep ->]); inv_head_step.
+  iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
+  iSplit.
+  (* TODO (MR) this used to be done by eauto. Why does it not work any more? *)
+  { iPureIntro. repeat eexists. constructor; eauto. }
+  iNext; iIntros (κ κs' v2 σ2 efs [Hstep ->]); inv_head_step.
   iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
-  iModIntro. iSplit=>//. by iApply "HΦ".
+  iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
 Qed.
 Lemma twp_store s E l v' e v :
   IntoVal e v →
@@ -179,10 +192,13 @@ Lemma twp_store s E l v' e v :
 Proof.
   iIntros (<- Φ) "Hl HΦ".
   iApply twp_lift_atomic_head_step_no_fork; auto.
-  iIntros (σ1 κs) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
-  iSplit; first by eauto 6. iIntros (κ κs' v2 σ2 efs [Hstep ->]); inv_head_step.
+  iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
+  iSplit.
+  (* TODO (MR) this used to be done by eauto. Why does it not work any more? *)
+  { iPureIntro. repeat eexists. constructor; eauto. }
+  iIntros (κ κs' v2 σ2 efs [Hstep ->]); inv_head_step.
   iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
-  iModIntro. iSplit=>//. by iApply "HΦ".
+  iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
 Qed.
 
 Lemma wp_cas_fail s E l q v' e1 v1 e2 :
@@ -192,7 +208,7 @@ Lemma wp_cas_fail s E l q v' e1 v1 e2 :
 Proof.
   iIntros (<- [v2 <-] ?? Φ) ">Hl HΦ".
   iApply wp_lift_atomic_head_step_no_fork; auto.
-  iIntros (σ1 κs) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
+  iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
   iSplit; first by eauto. iNext; iIntros (κ κs' v2' σ2 efs [Hstep ->]); inv_head_step.
   iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
 Qed.
@@ -203,7 +219,7 @@ Lemma twp_cas_fail s E l q v' e1 v1 e2 :
 Proof.
   iIntros (<- [v2 <-] ?? Φ) "Hl HΦ".
   iApply twp_lift_atomic_head_step_no_fork; auto.
-  iIntros (σ1 κs) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
+  iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
   iSplit; first by eauto. iIntros (κ κs' v2' σ2 efs [Hstep ->]); inv_head_step.
   iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
 Qed.
@@ -215,10 +231,13 @@ Lemma wp_cas_suc s E l e1 v1 e2 v2 :
 Proof.
   iIntros (<- <- ? Φ) ">Hl HΦ".
   iApply wp_lift_atomic_head_step_no_fork; auto.
-  iIntros (σ1 κs) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
-  iSplit; first by eauto. iNext; iIntros (κ κs' v2' σ2 efs [Hstep ->]); inv_head_step.
+  iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
+  iSplit.
+  (* TODO (MR) this used to be done by eauto. Why does it not work any more? *)
+  { iPureIntro. repeat eexists. by econstructor. }
+  iNext; iIntros (κ κs' v2' σ2 efs [Hstep ->]); inv_head_step.
   iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
-  iModIntro. iSplit=>//. by iApply "HΦ".
+  iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
 Qed.
 Lemma twp_cas_suc s E l e1 v1 e2 v2 :
   IntoVal e1 v1 → IntoVal e2 v2 → vals_cas_compare_safe v1 v1 →
@@ -227,10 +246,13 @@ Lemma twp_cas_suc s E l e1 v1 e2 v2 :
 Proof.
   iIntros (<- <- ? Φ) "Hl HΦ".
   iApply twp_lift_atomic_head_step_no_fork; auto.
-  iIntros (σ1 κs) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
-  iSplit; first by eauto. iIntros (κ κs' v2' σ2 efs [Hstep ->]); inv_head_step.
+  iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
+  iSplit.
+  (* TODO (MR) this used to be done by eauto. Why does it not work any more? *)
+  { iPureIntro. repeat eexists. by econstructor. }
+  iIntros (κ κs' v2' σ2 efs [Hstep ->]); inv_head_step.
   iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
-  iModIntro. iSplit=>//. by iApply "HΦ".
+  iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
 Qed.
 
 Lemma wp_faa s E l i1 e2 i2 :
@@ -240,10 +262,13 @@ Lemma wp_faa s E l i1 e2 i2 :
 Proof.
   iIntros (<- Φ) ">Hl HΦ".
   iApply wp_lift_atomic_head_step_no_fork; auto.
-  iIntros (σ1 κs) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
-  iSplit; first by eauto. iNext; iIntros (κ κs' v2' σ2 efs [Hstep ->]); inv_head_step.
+  iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
+  iSplit.
+  (* TODO (MR) this used to be done by eauto. Why does it not work any more? *)
+  { iPureIntro. repeat eexists. by constructor. }
+  iNext; iIntros (κ κs' v2' σ2 efs [Hstep ->]); inv_head_step.
   iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
-  iModIntro. iSplit=>//. by iApply "HΦ".
+  iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
 Qed.
 Lemma twp_faa s E l i1 e2 i2 :
   IntoVal e2 (LitV (LitInt i2)) →
@@ -252,9 +277,53 @@ Lemma twp_faa s E l i1 e2 i2 :
 Proof.
   iIntros (<- Φ) "Hl HΦ".
   iApply twp_lift_atomic_head_step_no_fork; auto.
-  iIntros (σ1 κs) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
-  iSplit; first by eauto. iIntros (κ κs' v2' σ2 efs [Hstep ->]); inv_head_step.
+  iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
+  iSplit.
+  (* TODO (MR) this used to be done by eauto. Why does it not work any more? *)
+  { iPureIntro. repeat eexists. by constructor. }
+  iIntros (κ κs' v2' σ2 efs [Hstep ->]); inv_head_step.
   iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
-  iModIntro. iSplit=>//. by iApply "HΦ".
+  iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
 Qed.
+
+(** Lifting lemmas for creating and resolving prophecy variables *)
+Lemma wp_new_proph :
+  {{{ True }}} NewProph {{{ (p : proph), RET (LitV (LitProphecy p)); p ⥱ - }}}.
+Proof.
+  iIntros (Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
+  iIntros (σ1 κs) "[Hσ HR] !>". iDestruct "HR" as (R [Hfr Hdom]) "HR". iSplit.
+  (* TODO (MR) this used to be done by eauto. Why does it not work any more? *)
+  { iPureIntro. repeat eexists. by apply new_proph_fresh. }
+  unfold cons_obs. simpl.
+  iNext; iIntros (κ κs' v2 σ2 efs [Hstep ->]). inv_head_step.
+  iMod ((@proph_map_alloc _ _ _ _ _ _ _ p) with "HR") as "[HR Hp]".
+  { intro Hin. apply (iffLR (elem_of_subseteq _ _) Hdom) in Hin. done. }
+  iModIntro; iSplit=> //. iFrame. iSplitL "HR".
+  - iExists _. iSplit; last done.
+    iPureIntro. split.
+    + apply first_resolve_insert; auto.
+    + rewrite dom_insert_L. by apply union_mono_l.
+  - iApply "HΦ". by iExists _.
+Qed.
+
+Lemma wp_resolve_proph e1 e2 p v w:
+  IntoVal e1 (LitV (LitProphecy p)) →
+  IntoVal e2 w →
+  {{{ p ⥱ v }}} ResolveProph e1 e2 {{{ RET (LitV LitUnit); ⌜v = Some w⌝ }}}.
+Proof.
+  iIntros (<- <- Φ) "Hp HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
+  iIntros (σ1 κs) "[Hσ HR] !>". iDestruct "HR" as (R [Hfr Hdom]) "HR".
+  iDestruct (@proph_map_valid with "HR Hp") as %Hlookup. iSplit.
+  (* TODO (MR) this used to be done by eauto. Why does it not work any more? *)
+  { iPureIntro. repeat eexists. by constructor. }
+  unfold cons_obs. simpl.
+  iNext; iIntros (κ κs' v2 σ2 efs [Hstep ->]); inv_head_step. iApply fupd_frame_l.
+  iSplit=> //. iFrame.
+  iMod ((@proph_map_remove _ _ _ _ _ _ _ p0) with "HR Hp") as "Hp". iModIntro.
+  iSplitR "HΦ".
+  - iExists _. iFrame. iPureIntro. split; first by eapply first_resolve_delete.
+    rewrite dom_delete. rewrite <- difference_empty_L. by eapply difference_mono.
+  - iApply "HΦ". iPureIntro. by eapply first_resolve_eq.
+Qed.
+
 End lifting.

theories/heap_lang/proph_map.v

+From iris.algebra Require Import auth gmap.
+From iris.base_logic.lib Require Export own.
+From iris.proofmode Require Import tactics.
+Set Default Proof Using "Type".
+Import uPred.
+
+Definition proph_map (P V : Type) `{Countable P} := gmap P (option V).
+Definition proph_val_list (P V : Type) := list (P * V).
+
+Section first_resolve.
+
+  Context {P V : Type} `{Countable P}.
+  Implicit Type pvs : proph_val_list P V.
+  Implicit Type p : P.
+  Implicit Type v : V.
+  Implicit Type R : proph_map P V.
+
+  (** The first resolve for [p] in [pvs] *)
+  Definition first_resolve pvs p :=
+    (map_of_list pvs : gmap P V) !! p.
+
+  Definition first_resolve_in_list R pvs :=
+    forall p v, p ∈ dom (gset _) R →
+           first_resolve pvs p = Some v →
+           R !! p = Some (Some v).
+
+  Lemma first_resolve_insert pvs p R :
+    first_resolve_in_list R pvs →
+    p ∉ dom (gset _) R →
+    first_resolve_in_list (<[p := first_resolve pvs p]> R) pvs.
+  Proof.
+    intros Hf Hnotin p' v' Hp'. rewrite (dom_insert_L R p) in Hp'.
+    erewrite elem_of_union in Hp'. destruct Hp' as [->%elem_of_singleton | Hin] => [->].
+    - by rewrite lookup_insert.
+    - rewrite lookup_insert_ne; first auto. by intros ->.
+  Qed.
+
+  Lemma first_resolve_delete pvs p v R :
+    first_resolve_in_list R ((p, v) :: pvs) →
+    first_resolve_in_list (delete p R) pvs.
+  Proof.
+    intros Hfr p' v' Hpin Heq. rewrite dom_delete_L in Hpin. rewrite /first_resolve in Heq.
+    apply elem_of_difference in Hpin as [Hpin Hne%not_elem_of_singleton].
+    erewrite <- lookup_insert_ne in Heq; last done. rewrite lookup_delete_ne; eauto.
+  Qed.
+
+  Lemma first_resolve_eq R p v w pvs :
+    first_resolve_in_list R ((p, v) :: pvs) →
+    R !! p = Some w →
+    w = Some v.
+  Proof.
+    intros Hfr Hlookup. specialize (Hfr p v (elem_of_dom_2 _ _ _ Hlookup)).
+    rewrite /first_resolve lookup_insert in Hfr. rewrite Hfr in Hlookup; last done.
+    inversion Hlookup. done.
+  Qed.
+
+End first_resolve.
+
+Definition proph_mapUR (P V : Type) `{Countable P} : ucmraT :=
+  gmapUR P $ exclR $ optionC $ leibnizC V.
+
+Definition to_proph_map {P V} `{Countable P} (pvs : proph_map P V) : proph_mapUR P V :=
+  fmap (λ v, Excl (v : option (leibnizC V))) pvs.
+
+(** The CMRA we need. *)
+Class proph_mapG (P V : Type) (Σ : gFunctors) `{Countable P