Resolution of prophecy variables can be attached to atomic expressions

tests/heap_lang_proph.v

+From iris.program_logic Require Export weakestpre total_weakestpre.
+From iris.heap_lang Require Import lang adequacy proofmode notation.
+From iris.heap_lang Require Import lang.
+Set Default Proof Using "Type".
+
+Section tests.
+  Context `{!heapG Σ}.
+  Implicit Types P Q : iProp Σ.
+  Implicit Types Φ : val → iProp Σ.
+
+  Definition CAS_resolve e1 e2 e3 p v :=
+    Resolve (CAS e1 e2 e3) p v.
+
+  Lemma wp_cas_suc_resolve s E (l : loc) (p : proph_id) (vs : list (val * val)) (v1 v2 v : val) :
+    vals_cas_compare_safe v1 v1 →
+    {{{ proph p vs ∗ ▷ l ↦ v1 }}}
+      CAS_resolve #l v1 v2 #p v @ s; E
+    {{{ RET #true ; ∃ vs', ⌜vs = (#true, v)::vs'⌝ ∗ proph p vs' ∗ l ↦ v2 }}}.
+  Proof.
+    iIntros (Hcmp Φ) "[Hp Hl] HΦ".
+    wp_apply (wp_resolve with "Hp"); first done.
+    assert (val_is_unboxed v1) as Hv1; first by destruct Hcmp.
+    wp_cas_suc. iIntros (vs' ->) "Hp".
+    iApply "HΦ". eauto with iFrame.
+  Qed.
+
+  Lemma wp_cas_fail_resolve s E (l : loc) (p : proph_id) (vs : list (val * val)) (v' v1 v2 v : val) :
+    v' ≠ v1 → vals_cas_compare_safe v' v1 →
+    {{{ proph p vs ∗ ▷ l ↦ v' }}}
+      CAS_resolve #l v1 v2 #p v @ s; E
+    {{{ RET #false ; ∃ vs', ⌜vs = (#false, v)::vs'⌝ ∗ proph p vs' ∗ l ↦ v' }}}.
+  Proof.
+    iIntros (NEq Hcmp Φ) "[Hp Hl] HΦ".
+    wp_apply (wp_resolve with "Hp"); first done.
+    wp_cas_fail. iIntros (vs' ->) "Hp".
+    iApply "HΦ". eauto with iFrame.
+  Qed.
+
+  Lemma test_resolve1 E (l : loc) (n : Z) (p : proph_id) (vs : list (val * val)) (v : val) :
+    l ↦ #n -∗
+    proph p vs -∗
+    WP Resolve (CAS #l #n (#n + #1)) #p v @ E {{ v, ⌜v = #true⌝ ∗ ∃vs, proph p vs ∗ l ↦ #(n+1) }}%I.
+  Proof.
+    iIntros "Hl Hp". wp_pures. wp_apply (wp_resolve with "Hp"); first done.
+    wp_cas_suc. iIntros (ws ->) "Hp". eauto with iFrame.
+  Qed.
+
+  Lemma test_resolve2 E (l : loc) (n m : Z) (p : proph_id) (vs : list (val * val)) :
+    proph p vs -∗
+    WP Resolve (#n + #m - (#n + #m)) #p #() @ E {{ v, ⌜v = #0⌝ ∗ ∃vs, proph p vs }}%I.
+  Proof.
+    iIntros "Hp". wp_pures. wp_apply (wp_resolve with "Hp"); first done.
+    wp_pures. iIntros (ws ->) "Hp". rewrite Z.sub_diag. eauto with iFrame.
+  Qed.
+
+  Lemma test_resolve3 s E (p1 p2 : proph_id) (vs1 vs2 : list (val * val)) (n : Z) :
+    {{{ proph p1 vs1 ∗ proph p2 vs2 }}}
+      Resolve (Resolve (#n - #n) #p2 #2) #p1 #1 @ s; E
+    {{{ RET #0 ; ∃ vs1' vs2', ⌜vs1 = (#0, #1)::vs1' ∧ vs2 = (#0, #2)::vs2'⌝ ∗ proph p1 vs1' ∗ proph p2 vs2' }}}.
+  Proof.
+    iIntros (Φ) "[Hp1 Hp2] HΦ".
+    wp_apply (wp_resolve with "Hp1"); first done.
+    wp_apply (wp_resolve with "Hp2"); first done.
+    wp_op.
+    iIntros (vs2' ->) "Hp2". iIntros (vs1' ->) "Hp1". rewrite Z.sub_diag.
+    iApply "HΦ". iExists vs1', vs2'. eauto with iFrame.
+  Qed.
+
+  Lemma test_resolve4 s E (p1 p2 : proph_id) (vs1 vs2 : list (val * val)) (n : Z) :
+    {{{ proph p1 vs1 ∗ proph p2 vs2 }}}
+      Resolve (Resolve (#n - #n) ((λ: "x", "x") #p2) (#0 + #2)) ((λ: "x", "x") #p1) (#0 + #1) @ s; E
+    {{{ RET #0 ; ∃ vs1' vs2', ⌜vs1 = (#0, #1)::vs1' ∧ vs2 = (#0, #2)::vs2'⌝ ∗ proph p1 vs1' ∗ proph p2 vs2' }}}.
+  Proof.
+    iIntros (Φ) "[Hp1 Hp2] HΦ".
+    wp_apply (wp_resolve with "Hp1"); first done.
+    wp_apply (wp_resolve with "Hp2"); first done.
+    wp_op.
+    iIntros (vs2' ->) "Hp2". iIntros (vs1' ->) "Hp1". rewrite Z.sub_diag.
+    iApply "HΦ". iExists vs1', vs2'. eauto with iFrame.
+  Qed.
+
+End tests.

theories/heap_lang/adequacy.v

@@ -8,10 +8,10 @@ Set Default Proof Using "Type".
 Class heapPreG Σ := HeapPreG {
   heap_preG_iris :> invPreG Σ;
   heap_preG_heap :> gen_heapPreG loc val Σ;
-  heap_preG_proph :> proph_mapPreG proph_id val Σ
+  heap_preG_proph :> proph_mapPreG proph_id (val * val) Σ
 }.
 
-Definition heapΣ : gFunctors := #[invΣ; gen_heapΣ loc val; proph_mapΣ proph_id val].
+Definition heapΣ : gFunctors := #[invΣ; gen_heapΣ loc val; proph_mapΣ proph_id (val * val)].
 Instance subG_heapPreG {Σ} : subG heapΣ Σ → heapPreG Σ.
 Proof. solve_inG. Qed.
 

theories/heap_lang/lang.v

@@ -14,13 +14,42 @@ Set Default Proof Using "Type".
   useless unless the user let-expands [b].
 
 - For prophecy variables, we annotate the reduction steps with an "observation"
-  and tweak adequacy such that WP knows all future observations.  There is
+  and tweak adequacy such that WP knows all future observations. There is
   another possible choice: Use non-deterministic choice when creating a prophecy
-  variable ([NewProph]), and when resolving it ([ResolveProph]) make the
-  program diverge unless the variable matches.  That, however, requires an
+  variable ([NewProph]), and when resolving it ([Resolve]) make the
+  program diverge unless the variable matches. That, however, requires an
   erasure proof that this endless loop does not make specifications useless.
 
-*)
+The expression [Resolve e p v] attaches a prophecy resolution (for prophecy
+variable [p] to value [v]) to the top-level head-reduction step of [e]. The
+prophecy resolution happens simultaneously with the head-step being taken.
+Furthermore, it is required that the head-step produces a value (otherwise
+the [Resolve] is stuck), and this value is also attached to the resolution.
+A prophecy variable is thus resolved to a pair containing (1) the result
+value of the wrapped expression (called [e] above), and (2) the value that
+was attached by the [Resolve] (called [v] above). This allows, for example,
+to distinguish a resolution originating from a successful [CAS] from one
+originating from a failing [CAS]. For example:
+ - [Resolve (CAS #l #n #(n+1)) #p v] will behave as [CAS #l #n #(n+1)],
+   which means step to a boolean [b] while updating the heap, but in the
+   meantime the prophecy variable [p] will be resolved to [(#b, v)].
+ - [Resolve (! #l) #p v] will behave as [! #l], that is return the value
+   [w] pointed to by [l] on the heap (assuming it was allocated properly),
+   but it will additionally resolve [p] to the pair [(w,v)].
+
+Note that the sub-expressions of [Resolve e p v] (i.e., [e], [p] and [v])
+are reduced as usual, from right to left. However, the evaluation of [e]
+is restricted so that the head-step to which the resolution is attached
+cannot be taken by the context. For example:
+ - [Resolve (CAS #l #n (#n + #1)) #p v] will first be reduced (with by a
+   context-step) to [Resolve (CAS #l #n #(n+1) #p v], and then behave as
+   described above.
+ - However, [Resolve ((λ: "n", CAS #l "n" ("n" + #1)) #n) #p v] is stuck.
+   Indeed, it can only be evaluated using a head-step (it is a β-redex),
+   but the process does not yield a value.
+
+The mechanism described above supports nesting [Resolve] expressions to
+attach several prophecy resolutions to a head-redex. *)
 
 Delimit Scope expr_scope with E.
 Delimit Scope val_scope with V.
@@ -72,7 +101,7 @@ Inductive expr :=
   | FAA (e1 : expr) (e2 : expr)
   (* Prophecy *)
   | NewProph
-  | ResolveProph (e1 : expr) (e2 : expr)
+  | Resolve (e0 : expr) (e1 : expr) (e2 : expr) (* wrapped expr, proph, val *)
 with val :=
   | LitV (l : base_lit)
   | RecV (f x : binder) (e : expr)
@@ -83,7 +112,12 @@ with val :=
 Bind Scope expr_scope with expr.
 Bind Scope val_scope with val.
 
-Definition observation : Set := proph_id * val.
+(** An observation associates a prophecy variable (identifier) to a pair of
+values. The first value is the one that was returned by the (atomic) operation
+during which the prophecy resolution happened (typically, a boolean when the
+wrapped operation is a CAS). The second value is the one that the prophecy
+variable was actually resolved to. *)
+Definition observation : Set := proph_id * (val * val).
 
 Notation of_val := Val (only parsing).
 
@@ -181,8 +215,8 @@ Proof.
      | FAA e1 e2, FAA e1' e2' =>
         cast_if_and (decide (e1 = e1')) (decide (e2 = e2'))
      | NewProph, NewProph => left _
-     | ResolveProph e1 e2, ResolveProph e1' e2' =>
-        cast_if_and (decide (e1 = e1')) (decide (e2 = e2'))
+     | Resolve e0 e1 e2, Resolve e0' e1' e2' =>
+        cast_if_and3 (decide (e0 = e0')) (decide (e1 = e1')) (decide (e2 = e2'))
      | _, _ => right _
      end
    with gov (v1 v2 : val) {struct v1} : Decision (v1 = v2) :=
@@ -255,7 +289,7 @@ Proof.
      | CAS e0 e1 e2 => GenNode 16 [go e0; go e1; go e2]
      | FAA e1 e2 => GenNode 17 [go e1; go e2]
      | NewProph => GenNode 18 []
-     | ResolveProph e1 e2 => GenNode 19 [go e1; go e2]
+     | Resolve e0 e1 e2 => GenNode 19 [go e0; go e1; go e2]
      end
    with gov v :=
      match v with
@@ -290,7 +324,7 @@ Proof.
      | GenNode 16 [e0; e1; e2] => CAS (go e0) (go e1) (go e2)
      | GenNode 17 [e1; e2] => FAA (go e1) (go e2)
      | GenNode 18 [] => NewProph
-     | GenNode 19 [e1; e2] => ResolveProph (go e1) (go e2)
+     | GenNode 19 [e0; e1; e2] => Resolve (go e0) (go e1) (go e2)
      | _ => Val $ LitV LitUnit (* dummy *)
      end
    with gov v :=
@@ -347,10 +381,18 @@ Inductive ectx_item :=
   | CasRCtx (e0 : expr) (e1 : expr)
   | FaaLCtx (v2 : val)
   | FaaRCtx (e1 : expr)
-  | ProphLCtx (v2 : val)
-  | ProphRCtx (e1 : expr).
-
-Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
+  | ResolveLCtx (ctx : ectx_item) (v1 : val) (v2 : val)
+  | ResolveMCtx (e0 : expr) (v2 : val)
+  | ResolveRCtx (e0 : expr) (e1 : expr).
+
+(** Contextual closure will only reduce [e] in [Resolve e (Val _) (Val _)] if
+the local context of [e] is non-empty. As a consequence, the first argument of
+[Resolve] is not completely evaluated (down to a value) by contextual closure:
+no head steps (i.e., surface reductions) are taken. This means that contextual
+closure will reduce [Resolve (CAS #l #n (#n + #1)) #p #v] into [Resolve (CAS
+#l #n #(n+1)) #p #v], but it cannot context-step any further. *)
+
+Fixpoint fill_item (Ki : ectx_item) (e : expr) : expr :=
   match Ki with
   | AppLCtx v2 => App e (of_val v2)
   | AppRCtx e1 => App e1 e
@@ -375,8 +417,9 @@ Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
   | CasRCtx e0 e1 => CAS e0 e1 e
   | FaaLCtx v2 => FAA e (Val v2)
   | FaaRCtx e1 => FAA e1 e
-  | ProphLCtx v2 => ResolveProph e (of_val v2)
-  | ProphRCtx e1 => ResolveProph e1 e
+  | ResolveLCtx K v1 v2 => Resolve (fill_item K e) (Val v1) (Val v2)
+  | ResolveMCtx ex v2 => Resolve ex e (Val v2)
+  | ResolveRCtx ex e1 => Resolve ex e1 e
   end.
 
 (** Substitution *)
@@ -403,7 +446,7 @@ Fixpoint subst (x : string) (v : val) (e : expr)  : expr :=
   | CAS e0 e1 e2 => CAS (subst x v e0) (subst x v e1) (subst x v e2)
   | FAA e1 e2 => FAA (subst x v e1) (subst x v e2)
   | NewProph => NewProph
-  | ResolveProph e1 e2 => ResolveProph (subst x v e1) (subst x v e2)
+  | Resolve ex e1 e2 => Resolve (subst x v ex) (subst x v e1) (subst x v e2)
   end.
 
 Definition subst' (mx : binder) (v : val) : expr → expr :=
@@ -595,30 +638,30 @@ Inductive head_step : expr → state → list observation → expr → state →
                []
                (Val $ LitV $ LitProphecy p) (state_upd_used_proph_id ({[ p ]} ∪) σ)
                []
-  | ResolveProphS p v σ :
-     head_step (ResolveProph (Val $ LitV $ LitProphecy p) (Val v)) σ
-               [(p, v)]
-               (Val $ LitV LitUnit) σ [].
+  | ResolveS p v e σ w σ' κs ts :
+     head_step e σ κs (Val v) σ' ts →
+     head_step (Resolve e (Val $ LitV $ LitProphecy p) (Val w)) σ
+               (κs ++ [(p, (v, w))]) (Val v) σ' ts.
 
 (** Basic properties about the language *)
 Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
-Proof. destruct Ki; intros ???; simplify_eq/=; auto with f_equal. Qed.
+Proof. induction Ki; intros ???; simplify_eq/=; auto with f_equal. Qed.
 
 Lemma fill_item_val Ki e :
   is_Some (to_val (fill_item Ki e)) → is_Some (to_val e).
-Proof. intros [v ?]. destruct Ki; simplify_option_eq; eauto. Qed.
+Proof. intros [v ?]. induction Ki; simplify_option_eq; eauto. Qed.
 
 Lemma val_head_stuck e1 σ1 κ e2 σ2 efs : head_step e1 σ1 κ e2 σ2 efs → to_val e1 = None.
 Proof. destruct 1; naive_solver. Qed.
 
 Lemma head_ctx_step_val Ki e σ1 κ e2 σ2 efs :
   head_step (fill_item Ki e) σ1 κ e2 σ2 efs → is_Some (to_val e).
-Proof. destruct Ki; inversion_clear 1; simplify_option_eq; by eauto. Qed.
+Proof. revert κ e2. induction Ki; inversion_clear 1; simplify_option_eq; eauto. Qed.
 
 Lemma fill_item_no_val_inj Ki1 Ki2 e1 e2 :
   to_val e1 = None → to_val e2 = None →
   fill_item Ki1 e1 = fill_item Ki2 e2 → Ki1 = Ki2.
-Proof. destruct Ki1, Ki2; intros; by simplify_eq. Qed.
+Proof. revert Ki1. induction Ki2, Ki1; naive_solver eauto with f_equal. Qed.
 
 Lemma alloc_fresh v n σ :
   let l := fresh_locs (dom (gset loc) σ.(heap)) n in
@@ -652,6 +695,47 @@ Canonical Structure heap_lang := LanguageOfEctx heap_ectx_lang.
 (* Prefer heap_lang names over ectx_language names. *)
 Export heap_lang.
 
+(* The following lemma is not provable using the axioms of [ectxi_language].
+The proof requires a case analysis over context items ([destruct i] on the
+last line), which in all cases yields a non-value. To prove this lemma for
+[ectxi_language] in general, we would require that a term of the form
+[fill_item i e] is never a value. *)
+Lemma to_val_fill_some K e v : to_val (fill K e) = Some v → K = [] ∧ e = Val v.
+Proof.
+  intro H. destruct K as [|Ki K]; first by apply of_to_val in H. exfalso.
+  assert (to_val e ≠ None) as He.
+  { intro A. by rewrite fill_not_val in H. }
+  assert (∃ w, e = Val w) as [w ->].
+  { destruct e; try done; eauto. }
+  assert (to_val (fill (Ki :: K) (Val w)) = None).
+  { destruct Ki; simpl; apply fill_not_val; done. }
+  by simplify_eq.
+Qed.
+
+Lemma prim_step_to_val_is_head_step e σ1 κs w σ2 efs :
+  prim_step e σ1 κs (Val w) σ2 efs → head_step e σ1 κs (Val w) σ2 efs.
+Proof.
+  intro H. destruct H as [K e1 e2 H1 H2].
+  assert (to_val (fill K e2) = Some w) as H3; first by rewrite -H2.
+  apply to_val_fill_some in H3 as [-> ->]. subst e. done.
+Qed.
+
+Lemma irreducible_resolve e v1 v2 σ :
+  irreducible e σ → irreducible (Resolve e (Val v1) (Val v2)) σ.
+Proof.
+  intros H κs ** [Ks e1' e2' Hfill -> step]. simpl in *.
+  induction Ks as [|K Ks _] using rev_ind; simpl in Hfill.
+  - subst e1'. inversion step. eapply H. by apply head_prim_step.
+  - rewrite fill_app /= in Hfill.
+    destruct K; (inversion Hfill; subst; clear Hfill; try
+      match goal with | H : Val ?v = fill Ks ?e |- _ =>
+        (assert (to_val (fill Ks e) = Some v) as HEq by rewrite -H //);
+        apply to_val_fill_some in HEq; destruct HEq as [-> ->]; inversion step
+      end).
+    apply (H κs (fill_item K (foldl (flip fill_item) e2' Ks)) σ' efs).
+    econstructor 1 with (K := Ks ++ [K]); last done; simpl; by rewrite fill_app.
+Qed.
+
 (** Define some derived forms. *)
 Notation Lam x e := (Rec BAnon x e) (only parsing).
 Notation Let x e1 e2 := (App (Lam x e2) e1) (only parsing).
@@ -665,3 +749,5 @@ Notation Alloc e := (AllocN (Val $ LitV $ LitInt 1) e) (only parsing).
 (* Skip should be atomic, we sometimes open invariants around
    it. Hence, we need to explicitly use LamV instead of e.g., Seq. *)
 Notation Skip := (App (Val $ LamV BAnon (Val $ LitV LitUnit)) (Val $ LitV LitUnit)).
+
+Notation ResolveProph e1 e2 := (Resolve Skip e1 e2) (only parsing).

theories/heap_lang/lib/coin_flip.v

@@ -61,10 +61,10 @@ Section coinflip.
     iModIntro. wp_seq. done.
   Qed.
 
-  Definition val_list_to_bool (v : list val) : bool :=
-    match v with
-    | LitV (LitBool b) :: _ => b
-    | _                     => true
+  Definition extract_bool (l : list (val * val)) : bool :=
+    match l with
+    | (_, LitV (LitBool b)) :: _ => b
+    | _                          => true
     end.
 
   Lemma lateChoice_spec (x: loc) :
@@ -81,7 +81,7 @@ Section coinflip.
     iMod "AU" as "[Hl [_ Hclose]]".
     iDestruct "Hl" as (v') "Hl".
     wp_store.
-    iMod ("Hclose" $! (val_list_to_bool v) with "[Hl]") as "HΦ"; first by eauto.
+    iMod ("Hclose" $! (extract_bool v) with "[Hl]") as "HΦ"; first by eauto.
     iModIntro. wp_apply rand_spec; try done.
     iIntros (b') "_".
     wp_apply (wp_resolve_proph with "Hp").

theories/heap_lang/lifting.v

+From Coq.Lists Require Import List. (* used for lemma "exists_last" *)
 From iris.algebra Require Import auth gmap.
 From iris.base_logic Require Export gen_heap.
 From iris.base_logic.lib Require Export proph_map.
@@ -12,7 +13,7 @@ Set Default Proof Using "Type".
 Class heapG Σ := HeapG {
   heapG_invG : invG Σ;
   heapG_gen_heapG :> gen_heapG loc val Σ;
-  heapG_proph_mapG :> proph_mapG proph_id val Σ
+  heapG_proph_mapG :> proph_mapG proph_id (val * val) Σ
 }.
 
 Instance heapG_irisG `{!heapG Σ} : irisG heap_lang Σ := {
@@ -83,9 +84,31 @@ Instance skip_atomic s  : Atomic s Skip.
 Proof. solve_atomic. Qed.
 Instance new_proph_atomic s : Atomic s NewProph.
 Proof. solve_atomic. Qed.
-Instance resolve_proph_atomic s v1 v2 : Atomic s (ResolveProph (Val v1) (Val v2)).
+Instance binop_atomic s op v1 v2 : Atomic s (BinOp op (Val v1) (Val v2)).
 Proof. solve_atomic. Qed.
 
+Instance proph_resolve_atomic s e v1 v2 :
+  Atomic s e → Atomic s (Resolve e (Val v1) (Val v2)).
+Proof.
+  rename e into e1. intros H σ1 e2 κ σ2 efs [Ks e1' e2' Hfill -> step].
+  simpl in *. induction Ks as [|K Ks _] using rev_ind; simpl in Hfill.
+  - subst. inversion_clear step. by apply (H σ1 (Val v) κs σ2 efs), head_prim_step.
+  - rewrite fill_app. rewrite fill_app in Hfill.
+    assert (∀ v, Val v = fill Ks e1' → False) as fill_absurd.
+    { intros v Hv. assert (to_val (fill Ks e1') = Some v) as Htv by by rewrite -Hv.
+      apply to_val_fill_some in Htv. destruct Htv as [-> ->]. inversion step. }
+    destruct K; (inversion Hfill; clear Hfill; subst; try
+      match goal with | H : Val ?v = fill Ks e1' |- _ => by apply fill_absurd in H end).
+    refine (_ (H σ1 (fill (Ks ++ [K]) e2') _ σ2 efs _)).
+    + destruct s; intro Hs; simpl in *.
+      * destruct Hs as [v Hs]. apply to_val_fill_some in Hs. by destruct Hs, Ks.
+      * apply irreducible_resolve. by rewrite fill_app in Hs.
+    + econstructor 1 with (K := Ks ++ [K]); try done. simpl. by rewrite fill_app.
+Qed.
+
+Instance resolve_proph_atomic s v1 v2 : Atomic s (ResolveProph (Val v1) (Val v2)).
+Proof. by apply proph_resolve_atomic, skip_atomic. Qed.
+
 Local Ltac solve_exec_safe := intros; subst; do 3 eexists; econstructor; eauto.
 Local Ltac solve_exec_puredet := simpl; intros; by inv_head_step.
 Local Ltac solve_pure_exec :=
@@ -396,18 +419,88 @@ Proof.
   iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
 Qed.
 
+(* In the following, strong atomicity is required due to the fact that [e] must
+be able to make a head step for [Resolve e _ _] not to be (head) stuck. *)
+
+Lemma resolve_reducible e σ p v :
+  Atomic StronglyAtomic e → reducible e σ →
+  reducible (Resolve e (Val (LitV (LitProphecy p))) (Val v)) σ.
+Proof.
+  intros A (κ & e' & σ' & efs & H).
+  exists (κ ++ [(p, (default v (to_val e'), v))]), e', σ', efs.
+  eapply Ectx_step with (K:=[]); try done.
+  assert (∃w, Val w = e') as [w <-].
+  { unfold Atomic in A. apply (A σ e' κ σ' efs) in H. unfold is_Some in H.
+    destruct H as [w H]. exists w. simpl in H. by apply (of_to_val _ _ H). }
+  simpl. constructor. by apply prim_step_to_val_is_head_step.
+Qed.
+
+Lemma step_resolve e p v σ1 κ e2 σ2 efs :
+  Atomic StronglyAtomic e →
+  prim_step (Resolve e (Val p) (Val v)) σ1 κ e2 σ2 efs →
+  head_step (Resolve e (Val p) (Val v)) σ1 κ e2 σ2 efs.
+Proof.
+  intros A [Ks e1' e2' Hfill -> step]. simpl in *.
+  induction Ks as [|K Ks _] using rev_ind.
+  + simpl in *. subst. inversion step. by constructor.
+  + rewrite fill_app /= in Hfill. destruct K; inversion Hfill; subst; clear Hfill.
+    - assert (fill_item K (fill Ks e1') = fill (Ks ++ [K]) e1') as Eq1;
+        first by rewrite fill_app.
+      assert (fill_item K (fill Ks e2') = fill (Ks ++ [K]) e2') as Eq2;
+        first by rewrite fill_app.
+      rewrite fill_app /=. rewrite Eq1 in A.
+      assert (is_Some (to_val (fill (Ks ++ [K]) e2'))) as H.
+      { apply (A σ1 _ κ σ2 efs). eapply Ectx_step with (K0 := Ks ++ [K]); done. }
+      destruct H as [v H]. apply to_val_fill_some in H. by destruct H, Ks.
+    - assert (to_val (fill Ks e1') = Some p); first by rewrite -H1 //.
+      apply to_val_fill_some in H. destruct H as [-> ->]. inversion step.
+    - assert (to_val (fill Ks e1') = Some v); first by rewrite -H2 //.
+      apply to_val_fill_some in H. destruct H as [-> ->]. inversion step.
+Qed.
+
+Lemma wp_resolve s E e Φ p v vs :
+  Atomic StronglyAtomic e →
+  to_val e = None →
+  proph p vs -∗
+  WP e @ s; E {{ r, ∀ vs', ⌜vs = (r, v)::vs'⌝ -∗ proph p vs' -∗ Φ r }} -∗
+  WP Resolve e (Val $ LitV $ LitProphecy p) (Val v) @ s; E {{ Φ }}.
+Proof.
+  (* TODO we should try to use a generic lifting lemma (and avoid [wp_unfold])
+     here, since this breaks the WP abstraction. *)
+  iIntros (A He) "Hp WPe". rewrite !wp_unfold /wp_pre /= He. simpl in *.
+  iIntros (σ1 κ κs n) "[Hσ Hκ]". destruct (decide (κ = [])) as [->|HNeq].
+  - iMod ("WPe" $! σ1 [] κs n with "[$Hσ $Hκ]") as "[Hs WPe]". iModIntro. iSplit.
+    { iDestruct "Hs" as "%". iPureIntro. destruct s; [ by apply resolve_reducible | done]. }
+    iIntros (e2 σ2 efs step). exfalso. apply step_resolve in step; last done.
+    inversion step. match goal with H: ?κs ++ [_] = [] |- _ => by destruct κs end.
+  - apply exists_last in HNeq as [κ' [[p' [w' v']] ->]]. rewrite -app_assoc.
+    iMod ("WPe" $! σ1 _ _ n with "[$Hσ $Hκ]") as "[Hs WPe]". iModIntro. iSplit.
+    { iDestruct "Hs" as "%". iPureIntro. destruct s; [ by apply resolve_reducible | done]. }
+    iIntros (e2 σ2 efs step). apply step_resolve in step; last done. inversion step.
+    match goal with H: _ ++ _ = _ ++ _ |- _ =>
+      apply app_inj_2 in H; last done; destruct H as [-> [=-> -> ->]] end. subst.
+    iMod ("WPe" $! (Val w') σ2 efs with "[%]") as "WPe". { eexists [] _ _; try done. }
+    iModIntro. iNext. iMod "WPe" as "[[$ Hκ] WPe]".
+    iMod (proph_map_resolve_proph p' (w',v') κs with "[$Hκ $Hp]") as (vs' ->) "[$ HPost]".
+    iModIntro. rewrite !wp_unfold /wp_pre /=. iDestruct "WPe" as "[HΦ $]".
+    iMod "HΦ". iModIntro. iApply "HΦ"; [ done | iFrame ].
+Qed.
+
+Lemma wp_skip s E Φ : ▷ Φ (LitV LitUnit) -∗ WP Skip @ s; E {{ Φ }}.
+Proof.
+  iIntros "HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
+  iIntros (σ1 κ κs n) "Hσ". iModIntro. iSplit.
+  - iPureIntro. eexists _, _, _, _. by constructor.
+  - iIntros (e2 σ2 efs step) "!>". inversion step. simplify_eq. by iFrame.
+Qed.
+
 Lemma wp_resolve_proph s E p vs v :
   {{{ proph p vs }}}
     ResolveProph (Val $ LitV $ LitProphecy p) (Val v) @ s; E
-  {{{ vs', RET (LitV LitUnit); ⌜vs = v::vs'⌝ ∗ proph p vs' }}}.
+  {{{ vs', RET (LitV LitUnit); ⌜vs = (LitV LitUnit, v)::vs'⌝ ∗ proph p vs' }}}.
 Proof.
-  iIntros (Φ) "Hp HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
-  iIntros (σ1 κ κs n) "[Hσ HR] !>". iSplit; first by eauto.
-  iNext; iIntros (v2 σ2 efs Hstep). inv_head_step.
-  iMod (proph_map_resolve_proph p v κs with "[HR Hp]") as "HPost"; first by iFrame.
-  iModIntro. iFrame. iSplitR; first done.
-  iDestruct "HPost" as (vs') "[HEq [HR Hp]]". iFrame.
-  iApply "HΦ". iFrame.
+  iIntros (Φ) "Hp HΦ". iApply (wp_resolve with "Hp"); first done.
+  iApply wp_skip. iNext. iIntros (vs') "HEq Hp". iApply "HΦ". iFrame.
 Qed.
 
 End lifting.

theories/heap_lang/metatheory.v

@@ -12,10 +12,9 @@ Fixpoint is_closed_expr (X : list string) (e : expr) : bool :=
   | Rec f x e => is_closed_expr (f :b: x :b: X) e
   | UnOp _ e | Fst e | Snd e | InjL e | InjR e | Fork e | Load e =>
      is_closed_expr X e
-  | App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | AllocN e1 e2 | Store e1 e2 | FAA e1 e2
-  | ResolveProph e1 e2 =>
+  | App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | AllocN e1 e2 | Store e1 e2 | FAA e1 e2 =>
      is_closed_expr X e1 && is_closed_expr X e2
-  | If e0 e1 e2 | Case e0 e1 e2 | CAS e0 e1 e2 =>
+  | If e0 e1 e2 | Case e0 e1 e2 | CAS e0 e1 e2 | Resolve e0 e1 e2 =>
      is_closed_expr X e0 && is_closed_expr X e1 && is_closed_expr X e2
   | NewProph => true
   end
@@ -130,7 +129,7 @@ Lemma head_step_is_closed e1 σ1 obs e2 σ2 es :
   map_Forall (λ _ v, is_closed_val v) σ2.(heap).
 Proof.
   intros Cl1 Clσ1 STEP.
-  destruct STEP; simpl in *; split_and!;
+  induction STEP; simpl in *; split_and!;
     try apply map_Forall_insert_2; try by naive_solver.
   - subst. repeat apply is_closed_subst'; naive_solver.
   - unfold un_op_eval in *. repeat case_match; naive_solver.
@@ -173,7 +172,7 @@ Fixpoint subst_map (vs : gmap string val) (e : expr) : expr :=
   | CAS e0 e1 e2 => CAS (subst_map vs e0) (subst_map vs e1) (subst_map vs e2)
   | FAA e1 e2 => FAA (subst_map vs e1) (subst_map vs e2)
   | NewProph => NewProph
-  | ResolveProph e1 e2 => ResolveProph (subst_map vs e1) (subst_map vs e2)
+  | Resolve e0 e1 e2 => Resolve (subst_map vs e0) (subst_map vs e1) (subst_map vs e2)
   end.
 
 Lemma subst_map_empty e : subst_map ∅ e = e.

theories/heap_lang/tactics.v

@@ -6,32 +6,48 @@ Import heap_lang.
 evaluation context [K] and a subexpression [e']. It calls the tactic [tac K e']
 for each possible decomposition until [tac] succeeds. *)
 Ltac reshape_expr e tac :=
-  let rec go K e :=
-  match e with
-  | _ => tac K e
-  | App ?e (Val ?v) => go (AppLCtx v :: K) e
-  | App ?e1 ?e2 => go (AppRCtx e1 :: K) e2
-  | UnOp ?op ?e => go (UnOpCtx op :: K) e
-  | BinOp ?op ?e (Val ?v) => go (BinOpLCtx op v :: K) e
-  | BinOp ?op ?e1 ?e2 => go (BinOpRCtx op e1 :: K) e2
-  | If ?e0 ?e1 ?e2 => go (IfCtx e1 e2 :: K) e0
-  | Pair ?e (Val ?v) => go (PairLCtx v :: K) e
-  | Pair ?e1 ?e2 => go (PairRCtx e1 :: K) e2
-  | Fst ?e => go (FstCtx :: K) e
-  | Snd ?e => go (SndCtx :: K) e
-  | InjL ?e => go (InjLCtx :: K) e
-  | InjR ?e => go (InjRCtx :: K) e
-  | Case ?e0 ?e1 ?e2 => go (CaseCtx e1 e2 :: K) e0
-  | AllocN ?e (Val ?v) => go (AllocNLCtx v :: K) e
-  | AllocN ?e1 ?e2 => go (AllocNRCtx e1 :: K) e2
-  | Load ?e => go (LoadCtx :: K) e
-  | Store ?e (Val ?v) => go (StoreLCtx v :: K) e
-  | Store ?e1 ?e2 => go (StoreRCtx e1 :: K) e2
-  | CAS ?e0 (Val ?v1) (Val ?v2) => go (CasLCtx v1 v2 :: K) e0
-  | CAS ?e0 ?e1 (Val ?v2) => go (CasMCtx e0 v2 :: K) e1
-  | CAS ?e0 ?e1 ?e2 => go (CasRCtx e0 e1 :: K) e2
-  | FAA ?e (Val ?v) => go (FaaLCtx v :: K) e
-  | FAA ?e1 ?e2 => go (FaaRCtx e1 :: K) e2
-  | ResolveProph ?e (Val ?v) => go (ProphLCtx v :: K) e
-  | ResolveProph ?e1 ?e2 => go (ProphRCtx e1 :: K) e2
-  end in go (@nil ectx_item) e.
+  (* Note that the current context is spread into a list of fully-constructed
+     items [K], and a list of pairs of values [vs] (prophecy identifier and
+     resolution value) that is only non-empty if a [ResolveLCtx] item (maybe
+     having several levels) is in the process of being constructed. Note that
+     a fully-constructed item is inserted into [K] by calling [add_item], and
+     that is only the case when a non-[ResolveLCtx] item is built. When [vs]
+     is non-empty, [add_item] also wraps the item under several [ResolveLCtx]
+     constructors: one for each pair in [vs]. *)
+  let rec go K vs e :=
+    match e with
+    | _                               => lazymatch vs with [] => tac K e | _ => fail end
+    | App ?e (Val ?v)                 => add_item (AppLCtx v) vs K e
+    | App ?e1 ?e2                     => add_item (AppRCtx e1) vs K e2
+    | UnOp ?op ?e                     => add_item (UnOpCtx op) vs K e
+    | BinOp ?op ?e (Val ?v)           => add_item (BinOpLCtx op v) vs K e
+    | BinOp ?op ?e1 ?e2               => add_item (BinOpRCtx op e1) vs K e2
+    | If ?e0 ?e1 ?e2                  => add_item (IfCtx e1 e2) vs K e0
+    | Pair ?e (Val ?v)                => add_item (PairLCtx v) vs K e
+    | Pair ?e1 ?e2                    => add_item (PairRCtx e1) vs K e2
+    | Fst ?e                          => add_item FstCtx vs K e
+    | Snd ?e                          => add_item SndCtx vs K e
+    | InjL ?e                         => add_item InjLCtx vs K e
+    | InjR ?e                         => add_item InjRCtx vs K e
+    | Case ?e0 ?e1 ?e2                => add_item (CaseCtx e1 e2) vs K e0
+    | AllocN ?e (Val ?v)              => add_item (AllocNLCtx v) vs K e
+    | AllocN ?e1 ?e2                  => add_item (AllocNRCtx e1) vs K e2
+    | Load ?e                         => add_item LoadCtx vs K e
+    | Store ?e (Val ?v)               => add_item (StoreLCtx v) vs K e
+    | Store ?e1 ?e2                   => add_item (StoreRCtx e1) vs K e2
+    | CAS ?e0 (Val ?v1) (Val ?v2)     => add_item (CasLCtx v1 v2) vs K e0
+    | CAS ?e0 ?e1 (Val ?v2)           => add_item (CasMCtx e0 v2) vs K e1
+    | CAS ?e0 ?e1 ?e2                 => add_item (CasRCtx e0 e1) vs K e2
+    | FAA ?e (Val ?v)                 => add_item (FaaLCtx v) vs K e
+    | FAA ?e1 ?e2                     => add_item (FaaRCtx e1) vs K e2
+    | Resolve ?ex (Val ?v1) (Val ?v2) => go K ((v1,v2) :: vs) ex
+    | Resolve ?ex ?e1 (Val ?v2)       => add_item (ResolveMCtx ex v2) vs K e1
+    | Resolve ?ex ?e1 ?e2             => add_item (ResolveRCtx ex e1) vs K e2
+    end
+  with add_item Ki vs K e :=
+    lazymatch vs with
+    | []               => go (Ki :: K) (@nil (val * val)) e
+    | (?v1,?v2) :: ?vs => add_item (ResolveLCtx Ki v1 v2) vs K e
+    end
+  in
+  go (@nil ectx_item) (@nil (val * val)) e.