_CoqProject

@@ -115,6 +115,7 @@ theories/heap_lang/lib/lazy_coin.v
 theories/heap_lang/lib/counter.v
 theories/heap_lang/lib/atomic_heap.v
 theories/heap_lang/lib/increment.v
+theories/heap_lang/lib/compare_and_set.v
 theories/proofmode/base.v
 theories/proofmode/tokens.v
 theories/proofmode/coq_tactics.v

tests/heap_lang_proph.v

@@ -8,38 +8,10 @@ Section tests.
   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) :
-    val_for_compare v' ≠ val_for_compare 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.
+    WP Resolve (CAS #l #n (#n + #1)) #p v @ E {{ v, ⌜v = #n⌝ ∗ ∃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.

tests/ipm_paper.v

@@ -121,7 +121,7 @@ Definition newcounter : val := λ: <>, ref #0.
 Definition incr : val :=
   rec: "incr" "l" :=
     let: "n" := !"l" in
-    if: CAS "l" "n" (#1 + "n") then #() else "incr" "l".
+    if: CAS "l" "n" (#1 + "n") = "n" then #() else "incr" "l".
 Definition read : val := λ: "l", !"l".
 
 (** The CMRA we need. *)
@@ -231,10 +231,11 @@ Section counter_proof.
       rewrite (auth_frag_op (S n) (S c)); last lia; iDestruct "Hγ" as "[Hγ Hγf]".
       wp_cas_suc. iSplitL "Hl Hγ".
       { iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
-      wp_if. rewrite {3}/C; eauto 10.
-    - wp_cas_fail; first (intros [=]; abstract omega).
+      wp_op. rewrite bool_decide_true //. wp_if. rewrite {3}/C; eauto 10.
+    - assert (#c ≠ #c') by (intros [=]; abstract omega). wp_cas_fail.
       iSplitL "Hl Hγ"; [iNext; iExists c'; by iFrame|].
-      wp_if. iApply ("IH" with "[Hγf]"). rewrite {3}/C; eauto 10.
+      wp_op. rewrite bool_decide_false //. wp_if.
+      iApply ("IH" with "[Hγf]"). rewrite {3}/C; eauto 10.
   Qed.
 
   Check "read_spec".

tests/one_shot.v

@@ -9,7 +9,7 @@ Set Default Proof Using "Type".
 Definition one_shot_example : val := λ: <>,
   let: "x" := ref NONE in (
   (* tryset *) (λ: "n",
-    CAS "x" NONE (SOME "n")),
+    CAS "x" NONE (SOME "n") = NONE),
   (* check  *) (λ: <>,
     let: "y" := !"x" in λ: <>,
     match: "y" with
@@ -49,13 +49,15 @@ Proof.
   iMod (inv_alloc N _ (one_shot_inv γ l) with "[Hl Hγ]") as "#HN".
   { iNext. iLeft. by iSplitL "Hl". }
   wp_pures. iModIntro. iApply "Hf"; iSplit.
-  - iIntros (n) "!#". wp_lam. wp_pures.
+  - iIntros (n) "!#". wp_lam. wp_pures. wp_bind (CAS _ _ _).
     iInv N as ">[[Hl Hγ]|H]"; last iDestruct "H" as (m) "[Hl Hγ]".
     + iMod (own_update with "Hγ") as "Hγ".
       { by apply cmra_update_exclusive with (y:=Shot n). }
-      wp_cas_suc. iSplitL; last eauto.
-      iModIntro. iNext; iRight; iExists n; by iFrame.
-    + wp_cas_fail. iSplitL; last eauto.
+      wp_cas_suc. iSplitL; iModIntro; last first.
+      { wp_pures. eauto. }
+      iNext; iRight; iExists n; by iFrame.
+    + wp_cas_fail. iSplitL; iModIntro; last first.
+      { wp_pures. eauto. }
       rewrite /one_shot_inv; eauto 10.
   - iIntros "!# /=". wp_lam. wp_bind (! _)%E.
     iInv N as ">Hγ".

theories/heap_lang/lang.v

@@ -97,8 +97,8 @@ Inductive expr :=
   | AllocN (e1 e2 : expr) (* array length (positive number), initial value *)
   | Load (e : expr)
   | Store (e1 : expr) (e2 : expr)
-  | CAS (e0 : expr) (e1 : expr) (e2 : expr)
-  | FAA (e1 : expr) (e2 : expr)
+  | CAS (e0 : expr) (e1 : expr) (e2 : expr) (* Compare-and-swap (NOT compare-and-set!) *)
+  | FAA (e1 : expr) (e2 : expr) (* Fetch-and-add *)
   (* Prophecy *)
   | NewProph
   | Resolve (e0 : expr) (e1 : expr) (e2 : expr) (* wrapped expr, proph, val *)
@@ -518,6 +518,7 @@ Definition bin_op_eval_bool (op : bin_op) (b1 b2 : bool) : option base_lit :=
 
 Definition bin_op_eval (op : bin_op) (v1 v2 : val) : option val :=
   if decide (op = EqOp) then
+    (* Crucially, this compares the same way as [CAS]! *)
     Some $ LitV $ LitBool $ bool_decide (val_for_compare v1 = val_for_compare v2)
   else
     match v1, v2 with
@@ -633,19 +634,13 @@ Inductive head_step : expr → state → list observation → expr → state →
                []
                (Val $ LitV LitUnit) (state_upd_heap <[l:=v]> σ)
                []
-  | CasFailS l v1 v2 vl σ :
+  | CasS l v1 v2 vl σ :
      vals_cas_compare_safe vl v1 →
      σ.(heap) !! l = Some vl →
-     val_for_compare vl ≠ val_for_compare v1 →
-     head_step (CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2)) σ []
-               (Val $ LitV $ LitBool false) σ []
-  | CasSucS l v1 v2 vl σ :
-     vals_cas_compare_safe vl v1 →
-     σ.(heap) !! l = Some vl →
-     val_for_compare vl = val_for_compare v1 →
      head_step (CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2)) σ
                []
-               (Val $ LitV $ LitBool true) (state_upd_heap <[l:=v2]> σ)
+               (* Crucially, this compares the same way as [EqOp]! *)
+               (Val vl) (if decide (val_for_compare vl = val_for_compare v1) then state_upd_heap <[l:=v2]> σ else σ)
                []
   | FaaS l i1 i2 σ :
      σ.(heap) !! l = Some (LitV (LitInt i1)) →

theories/heap_lang/lib/atomic_heap.v

@@ -36,7 +36,7 @@ Class atomic_heap {Σ} `{!heapG Σ} := AtomicHeap {
     val_is_unboxed w1 →
     <<< ∀ v, mapsto l 1 v >>> cas #l w1 w2 @ ⊤
     <<< if decide (val_for_compare v = val_for_compare w1) then mapsto l 1 w2 else mapsto l 1 v,
-        RET #(if decide (val_for_compare v = val_for_compare w1) then true else false) >>>;
+        RET v >>>;
 }.
 Arguments atomic_heap _ {_}.
 
@@ -100,7 +100,7 @@ Section proof.
     <<< ∀ (v : val), l ↦ v >>>
       primitive_cas #l w1 w2 @ ⊤
     <<< if decide (val_for_compare v = val_for_compare w1) then l ↦ w2 else l ↦ v,
-        RET #(if decide (val_for_compare v = val_for_compare w1) then true else false) >>>.
+        RET v >>>.
   Proof.
     iIntros (? Φ) "AU". wp_lam. wp_let. wp_let.
     iMod "AU" as (v) "[H↦ [_ Hclose]]".

theories/heap_lang/lib/compare_and_set.v

+From iris.heap_lang Require Export lifting notation.
+From iris.program_logic Require Export atomic.
+From iris.heap_lang Require Import proofmode notation.
+Set Default Proof Using "Type".
+
+(* Defines compare-and-set (CASet) on top of compare-and-swap (CAS). *)
+
+Definition compare_and_set : val :=
+  λ: "l" "v1" "v2", CAS "l" "v1" "v2" = "v1".
+
+Section proof.
+  Context `{!heapG Σ}.
+
+  (* This is basically a logically atomic spec, but stronger and hence easier to apply. *)
+  Lemma caset_spec (l : loc) (v1 v2 : val) Φ E :
+    val_is_unboxed v1 →
+    (|={⊤,E}=> ∃ v, l ↦ v ∗ let b := bool_decide (val_for_compare v = val_for_compare v1) in
+        (l ↦ (if b then v2 else v) ={E,⊤}=∗ Φ #b) ) -∗
+    WP compare_and_set #l v1 v2 @ ⊤ {{ Φ }}.
+  Proof.
+    iIntros (?) "AU". wp_lam. wp_pures. wp_bind (CAS _ _ _).
+    iMod "AU" as (v) "[H↦ Hclose]". case_bool_decide.
+    - wp_cas_suc. iMod ("Hclose" with "H↦"). iModIntro. wp_op.
+      rewrite bool_decide_true //.
+    - wp_cas_fail. iMod ("Hclose" with "H↦"). iModIntro. wp_op.
+      rewrite bool_decide_false //.
+  Qed.
+End proof.

theories/heap_lang/lib/counter.v

@@ -3,13 +3,13 @@ From iris.base_logic.lib Require Export invariants.
 From iris.heap_lang Require Export lang.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import frac_auth auth.
-From iris.heap_lang Require Import proofmode notation.
+From iris.heap_lang Require Import proofmode notation lib.compare_and_set.
 Set Default Proof Using "Type".
 
 Definition newcounter : val := λ: <>, ref #0.
 Definition incr : val := rec: "incr" "l" :=
     let: "n" := !"l" in
-    if: CAS "l" "n" (#1 + "n") then #() else "incr" "l".
+    if: compare_and_set "l" "n" (#1 + "n") then #() else "incr" "l".
 Definition read : val := λ: "l", !"l".
 
 (** Monotone counter *)
@@ -50,22 +50,25 @@ Section mono_proof.
     iDestruct "Hl" as (γ) "[#? Hγf]".
     wp_bind (! _)%E. iInv N as (c) ">[Hγ Hl]".
     wp_load. iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
-    wp_pures.
-    wp_bind (CAS _ _ _). iInv N as (c') ">[Hγ Hl]".
+    wp_pures. wp_apply caset_spec; first done.
+    iInv N as (c') ">[Hγ Hl]" "Hclose".
     destruct (decide (c' = c)) as [->|].
     - iDestruct (own_valid_2 with "Hγ Hγf")
         as %[?%mnat_included _]%auth_both_valid.
       iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]".
       { apply auth_update, (mnat_local_update _ _ (S c)); auto. }
-      wp_cas_suc. iModIntro. iSplitL "Hl Hγ".
-      { iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
-      wp_if. iApply "HΦ"; iExists γ; repeat iSplit; eauto.
+      iExists _; iFrame "Hl". iIntros "!> Hl".
+      rewrite bool_decide_true //. iMod ("Hclose" with "[Hl Hγ]") as "_".
+      { iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. iFrame. }
+      iModIntro. wp_if.
+      iApply "HΦ"; iExists γ; repeat iSplit; eauto.
       iApply (own_mono with "Hγf").
       (* FIXME: FIXME(Coq #6294): needs new unification *)
       apply: auth_frag_mono. by apply mnat_included, le_n_S.
-    - wp_cas_fail; first (by intros [= ?%Nat2Z.inj]). iModIntro.
-      iSplitL "Hl Hγ"; [iNext; iExists c'; by iFrame|].
-      wp_if. iApply ("IH" with "[Hγf] [HΦ]"); last by auto.
+    - iExists _; iFrame "Hl". iIntros "!> Hl".
+      rewrite bool_decide_false; last by intros [= ?%Nat2Z.inj].
+      iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c'; by iFrame|].
+      iModIntro. wp_if. iApply ("IH" with "[Hγf] [HΦ]"); last by auto.
       rewrite {3}/mcounter; eauto 10.
   Qed.
 
@@ -129,17 +132,19 @@ Section contrib_spec.
     iIntros (Φ) "[#? Hγf] HΦ". iLöb as "IH". wp_rec.
     wp_bind (! _)%E. iInv N as (c) ">[Hγ Hl]".
     wp_load. iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
-    wp_pures.
-    wp_bind (CAS _ _ _). iInv N as (c') ">[Hγ Hl]".
+    wp_pures. wp_apply caset_spec; first done.
+    iInv N as (c') ">[Hγ Hl]" "Hclose".
     destruct (decide (c' = c)) as [->|].
     - iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]".
       { apply frac_auth_update, (nat_local_update _ _ (S c) (S n)); lia. }
-      wp_cas_suc. iModIntro. iSplitL "Hl Hγ".
+      iExists _; iFrame "Hl". iIntros "!> Hl".
+      rewrite bool_decide_true //. iMod ("Hclose" with "[Hl Hγ]") as "_".
       { iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
-      wp_if. by iApply "HΦ".
-    - wp_cas_fail; first (by intros [= ?%Nat2Z.inj]).
-      iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c'; by iFrame|].
-      wp_if. by iApply ("IH" with "[Hγf] [HΦ]"); auto.
+      iModIntro. wp_if. by iApply "HΦ".
+    - iExists _; iFrame "Hl". iIntros "!> Hl".
+      rewrite bool_decide_false; last by intros [= ?%Nat2Z.inj].
+      iMod ("Hclose" with "[Hl Hγ]"); [iNext; iExists c'; by iFrame|].
+      iModIntro. wp_if. by iApply ("IH" with "[Hγf] [HΦ]"); auto.
   Qed.
 
   Lemma read_contrib_spec γ l q n :

theories/heap_lang/lib/increment.v

@@ -16,7 +16,7 @@ Section increment_physical.
   Definition incr_phy : val :=
     rec: "incr" "l" :=
        let: "oldv" := !"l" in
-       if: CAS "l" "oldv" ("oldv" + #1)
+       if: CAS "l" "oldv" ("oldv" + #1) = "oldv"
          then "oldv" (* return old value if success *)
          else "incr" "l".
 
@@ -29,9 +29,9 @@ Section increment_physical.
     wp_pures. wp_bind (CAS _ _ _)%E. iMod "AU" as (w) "[Hl Hclose]".
     destruct (decide (#v = #w)) as [[= ->]|Hx].
     - wp_cas_suc. iDestruct "Hclose" as "[_ Hclose]". iMod ("Hclose" with "Hl") as "HΦ".
-      iModIntro. wp_if. done.
+      iModIntro. wp_op. rewrite bool_decide_true //. wp_if. done.
     - wp_cas_fail. iDestruct "Hclose" as "[Hclose _]". iMod ("Hclose" with "Hl") as "AU".
-      iModIntro. wp_if. iApply "IH". done.
+      iModIntro. wp_op. rewrite bool_decide_false //. wp_if. iApply "IH". done.
   Qed.
 End increment_physical.
 
@@ -45,7 +45,7 @@ Section increment.
   Definition incr : val :=
     rec: "incr" "l" :=
        let: "oldv" := !"l" in
-       if: CAS "l" "oldv" ("oldv" + #1)
+       if: CAS "l" "oldv" ("oldv" + #1) = "oldv"
          then "oldv" (* return old value if success *)
          else "incr" "l".
 
@@ -70,9 +70,9 @@ Section increment.
     { (* abort case *) iDestruct "Hclose" as "[? _]". done. }
     iIntros "Hl". simpl. destruct (decide (#w = #v)) as [[= ->]|Hx].
     - iDestruct "Hclose" as "[_ Hclose]". iMod ("Hclose" with "Hl") as "HΦ".
-      iIntros "!>". wp_if. by iApply "HΦ".
+      iIntros "!>". wp_op. rewrite bool_decide_true //. wp_if. by iApply "HΦ".
     - iDestruct "Hclose" as "[Hclose _]". iMod ("Hclose" with "Hl") as "AU".
-      iIntros "!>". wp_if. iApply "IH". done.
+      iIntros "!>". wp_op. rewrite bool_decide_false //. wp_if. iApply "IH". done.
   Qed.
 
   (** A proof of the incr specification that uses lemmas to avoid reasining
@@ -94,9 +94,9 @@ Section increment.
     iIntros "H↦ !>".
     simpl. destruct (decide (#x' = #x)) as [[= ->]|Hx].
     - iRight. iFrame. iIntros "HΦ !>".
-      wp_if. by iApply "HΦ".
+      wp_op. rewrite bool_decide_true //. wp_if. by iApply "HΦ".
     - iLeft. iFrame. iIntros "AU !>".
-      wp_if. iApply "IH". done.
+      wp_op. rewrite bool_decide_false //. wp_if. iApply "IH". done.
   Qed.
 
   (** A "weak increment": assumes that there is no race *)

theories/heap_lang/lib/spin_lock.v

@@ -7,7 +7,7 @@ From iris.heap_lang.lib Require Import lock.
 Set Default Proof Using "Type".
 
 Definition newlock : val := λ: <>, ref #false.
-Definition try_acquire : val := λ: "l", CAS "l" #false #true.
+Definition try_acquire : val := λ: "l", CAS "l" #false #true = #false.
 Definition acquire : val :=
   rec: "acquire" "l" := if: try_acquire "l" then #() else "acquire" "l".
 Definition release : val := λ: "l", "l" <- #false.
@@ -61,12 +61,12 @@ Section proof.
     {{{ b, RET #b; if b is true then locked γ ∗ R else True }}}.
   Proof.
     iIntros (Φ) "#Hl HΦ". iDestruct "Hl" as (l ->) "#Hinv".
-    wp_rec. iInv N as ([]) "[Hl HR]".
+    wp_rec. wp_bind (CAS _ _ _). iInv N as ([]) "[Hl HR]".
     - wp_cas_fail. iModIntro. iSplitL "Hl"; first (iNext; iExists true; eauto).
-      iApply ("HΦ" $! false). done.
+      wp_pures. iApply ("HΦ" $! false). done.
     - wp_cas_suc. iDestruct "HR" as "[Hγ HR]".
       iModIntro. iSplitL "Hl"; first (iNext; iExists true; eauto).
-      rewrite /locked. by iApply ("HΦ" $! true with "[$Hγ $HR]").
+      rewrite /locked. wp_pures. by iApply ("HΦ" $! true with "[$Hγ $HR]").
   Qed.
 
   Lemma acquire_spec γ lk R :

theories/heap_lang/lib/ticket_lock.v

@@ -20,7 +20,7 @@ Definition newlock : val :=
 Definition acquire : val :=
   rec: "acquire" "lk" :=
     let: "n" := !(Snd "lk") in
-    if: CAS (Snd "lk") "n" ("n" + #1)
+    if: CAS (Snd "lk") "n" ("n" + #1) = "n"
       then wait_loop "n" "lk"
       else "acquire" "lk".
 
@@ -122,14 +122,14 @@ Section proof.
       wp_cas_suc. iModIntro. iSplitL "Hlo' Hln' Haown Hauth".
       { iNext. iExists o', (S n).
         rewrite Nat2Z.inj_succ -Z.add_1_r. by iFrame. }
-      wp_if.
+      wp_op. rewrite bool_decide_true //. wp_if.
       iApply (wait_loop_spec γ (#lo, #ln) with "[-HΦ]").
       + iFrame. rewrite /is_lock; eauto 10.
       + by iNext.
     - wp_cas_fail. iModIntro.
       iSplitL "Hlo' Hln' Hauth Haown".
       { iNext. iExists o', n'. by iFrame. }
-      wp_if. by iApply "IH"; auto.
+      wp_op. rewrite bool_decide_false //. wp_if. by iApply "IH"; auto.
   Qed.
 
   Lemma release_spec γ lk R :

theories/heap_lang/lifting.v

@@ -56,8 +56,7 @@ Local Hint Extern 0 (head_reducible_no_obs _ _) => eexists _, _, _; simpl : core
 
 (* [simpl apply] is too stupid, so we need extern hints here. *)
 Local Hint Extern 1 (head_step _ _ _ _ _ _) => econstructor : core.
-Local Hint Extern 0 (head_step (CAS _ _ _) _ _ _ _ _) => eapply CasSucS : core.
-Local Hint Extern 0 (head_step (CAS _ _ _) _ _ _ _ _) => eapply CasFailS : core.
+Local Hint Extern 0 (head_step (CAS _ _ _) _ _ _ _ _) => eapply CasS : core.
 Local Hint Extern 0 (head_step (AllocN _ _) _ _ _ _ _) => apply alloc_fresh : core.
 Local Hint Extern 0 (head_step NewProph _ _ _ _ _) => apply new_proph_id_fresh : core.
 Local Hint Resolve to_of_val : core.
@@ -355,7 +354,7 @@ Qed.
 Lemma wp_cas_fail s E l q v' v1 v2 :
   val_for_compare v' ≠ val_for_compare v1 → vals_cas_compare_safe v' v1 →
   {{{ ▷ l ↦{q} v' }}} CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
-  {{{ RET LitV (LitBool false); l ↦{q} v' }}}.
+  {{{ RET v'; l ↦{q} v' }}}.
 Proof.
   iIntros (?? Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1 κ κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
@@ -365,7 +364,7 @@ Qed.
 Lemma twp_cas_fail s E l q v' v1 v2 :
   val_for_compare v' ≠ val_for_compare v1 → vals_cas_compare_safe v' v1 →
   [[{ l ↦{q} v' }]] CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
-  [[{ RET LitV (LitBool false); l ↦{q} v' }]].
+  [[{ RET v'; l ↦{q} v' }]].
 Proof.
   iIntros (?? Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
@@ -376,7 +375,7 @@ Qed.
 Lemma wp_cas_suc s E l v1 v2 v' :
   val_for_compare v' = val_for_compare v1 → vals_cas_compare_safe v' v1 →
   {{{ ▷ l ↦ v' }}} CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
-  {{{ RET LitV (LitBool true); l ↦ v2 }}}.
+  {{{ RET v'; l ↦ v2 }}}.
 Proof.
   iIntros (?? Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1 κ κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
@@ -387,7 +386,7 @@ Qed.
 Lemma twp_cas_suc s E l v1 v2 v' :
   val_for_compare v' = val_for_compare v1 → vals_cas_compare_safe v' v1 →
   [[{ l ↦ v' }]] CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
-  [[{ RET LitV (LitBool true); l ↦ v2 }]].
+  [[{ RET v'; l ↦ v2 }]].
 Proof.
   iIntros (?? Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
@@ -496,6 +495,7 @@ Proof.
     iMod "HΦ". iModIntro. by iApply "HΦ".
 Qed.
 
+(** Lemmas for some particular expression inside the [Resolve]. *)
 Lemma wp_resolve_proph s E p vs v :
   {{{ proph p vs }}}
     ResolveProph (Val $ LitV $ LitProphecy p) (Val v) @ s; E
@@ -506,4 +506,29 @@ Proof.
   iIntros "!>" (vs') "HEq Hp". iApply "HΦ". iFrame.
 Qed.
 
+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 }}}
+    Resolve (CAS #l v1 v2) #p v @ s; E
+  {{{ RET v1 ; ∃ vs', ⌜vs = (v1, v)::vs'⌝ ∗ proph p vs' ∗ l ↦ v2 }}}.
+Proof.
+  iIntros (Hcmp Φ) "[Hp Hl] HΦ".
+  iApply (wp_resolve with "Hp"); first done.
+  assert (val_is_unboxed v1) as Hv1; first by destruct Hcmp.
+  iApply (wp_cas_suc with "Hl"); [done..|]. iIntros "!> Hl".
+  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)) q (v' v1 v2 v : val) :
+  val_for_compare v' ≠ val_for_compare v1 → vals_cas_compare_safe v' v1 →
+  {{{ proph p vs ∗ ▷ l ↦{q} v' }}}
+    Resolve (CAS #l v1 v2) #p v @ s; E
+  {{{ RET v' ; ∃ vs', ⌜vs = (v', v)::vs'⌝ ∗ proph p vs' ∗ l ↦{q} v' }}}.
+Proof.
+  iIntros (NEq Hcmp Φ) "[Hp Hl] HΦ".
+  iApply (wp_resolve with "Hp"); first done.
+  iApply (wp_cas_fail with "Hl"); [done..|]. iIntros "!> Hl".
+  iIntros (vs' ->) "Hp". iApply "HΦ". eauto with iFrame.
+Qed.
+
 End lifting.

theories/heap_lang/metatheory.v

@@ -135,6 +135,7 @@ Proof.
   - unfold un_op_eval in *. repeat case_match; naive_solver.
   - eapply bin_op_eval_closed; eauto; naive_solver.
   - by apply heap_closed_alloc.
+  - case_match; try apply map_Forall_insert_2; by naive_solver.
 Qed.
 
 (* Parallel substitution with maps of values indexed by strings *)

theories/heap_lang/proofmode.v

@@ -284,9 +284,9 @@ Lemma tac_wp_cas Δ Δ' Δ'' s E i K l v v1 v2 Φ :
   envs_simple_replace i false (Esnoc Enil i (l ↦ v2)) Δ' = Some Δ'' →
   vals_cas_compare_safe v v1 →
   (val_for_compare v = val_for_compare v1 →
-   envs_entails Δ'' (WP fill K (Val $ LitV true) @ s; E {{ Φ }})) →
+   envs_entails Δ'' (WP fill K (Val v) @ s; E {{ Φ }})) →
   (val_for_compare v ≠ val_for_compare v1 →
-   envs_entails Δ' (WP fill K (Val $ LitV false) @ s; E {{ Φ }})) →
+   envs_entails Δ' (WP fill K (Val v) @ s; E {{ Φ }})) →
   envs_entails Δ (WP fill K (CAS (LitV l) (Val v1) (Val v2)) @ s; E {{ Φ }}).
 Proof.
   rewrite envs_entails_eq=> ???? Hsuc Hfail.
@@ -305,9 +305,9 @@ Lemma tac_twp_cas Δ Δ' s E i K l v v1 v2 Φ :
   envs_simple_replace i false (Esnoc Enil i (l ↦ v2)) Δ = Some Δ' →
   vals_cas_compare_safe v v1 →
   (val_for_compare v = val_for_compare v1 →
-   envs_entails Δ' (WP fill K (Val $ LitV true) @ s; E [{ Φ }])) →
+   envs_entails Δ' (WP fill K (Val v) @ s; E [{ Φ }])) →
   (val_for_compare v ≠ val_for_compare v1 →
-   envs_entails Δ (WP fill K (Val $ LitV false) @ s; E [{ Φ }])) →
+   envs_entails Δ (WP fill K (Val v) @ s; E [{ Φ }])) →
   envs_entails Δ (WP fill K (CAS (LitV l) v1 v2) @ s; E [{ Φ }]).
 Proof.
   rewrite envs_entails_eq=> ??? Hsuc Hfail.
@@ -326,7 +326,7 @@ Lemma tac_wp_cas_fail Δ Δ' s E i K l q v v1 v2 Φ :
   MaybeIntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦{q} v)%I →
   val_for_compare v ≠ val_for_compare v1 → vals_cas_compare_safe v v1 →
-  envs_entails Δ' (WP fill K (Val $ LitV false) @ s; E {{ Φ }}) →
+  envs_entails Δ' (WP fill K (Val v) @ s; E {{ Φ }}) →
   envs_entails Δ (WP fill K (CAS (LitV l) v1 v2) @ s; E {{ Φ }}).
 Proof.
   rewrite envs_entails_eq=> ?????.
@@ -337,7 +337,7 @@ Qed.
 Lemma tac_twp_cas_fail Δ s E i K l q v v1 v2 Φ :
   envs_lookup i Δ = Some (false, l ↦{q} v)%I →
   val_for_compare v ≠ val_for_compare v1 → vals_cas_compare_safe v v1 →
-  envs_entails Δ (WP fill K (Val $ LitV false) @ s; E [{ Φ }]) →
+  envs_entails Δ (WP fill K (Val v) @ s; E [{ Φ }]) →
   envs_entails Δ (WP fill K (CAS (LitV l) v1 v2) @ s; E [{ Φ }]).
 Proof.
   rewrite envs_entails_eq. intros. rewrite -twp_bind.
@@ -350,7 +350,7 @@ Lemma tac_wp_cas_suc Δ Δ' Δ'' s E i K l v v1 v2 Φ :
   envs_lookup i Δ' = Some (false, l ↦ v)%I →
   envs_simple_replace i false (Esnoc Enil i (l ↦ v2)) Δ' = Some Δ'' →
   val_for_compare v = val_for_compare v1 → vals_cas_compare_safe v v1 →
-  envs_entails Δ'' (WP fill K (Val $ LitV true) @ s; E {{ Φ }}) →
+  envs_entails Δ'' (WP fill K (Val v) @ s; E {{ Φ }}) →
   envs_entails Δ (WP fill K (CAS (LitV l) v1 v2) @ s; E {{ Φ }}).
 Proof.
   rewrite envs_entails_eq=> ??????; subst.
@@ -363,7 +363,7 @@ Lemma tac_twp_cas_suc Δ Δ' s E i K l v v1 v2 Φ :
   envs_lookup i Δ = Some (false, l ↦ v)%I →
   envs_simple_replace i false (Esnoc Enil i (l ↦ v2)) Δ = Some Δ' →
   val_for_compare v = val_for_compare v1 → vals_cas_compare_safe v v1 →
-  envs_entails Δ' (WP fill K (Val $ LitV true) @ s; E [{ Φ }]) →
+  envs_entails Δ' (WP fill K (Val v) @ s; E [{ Φ }]) →
   envs_entails Δ (WP fill K (CAS (LitV l) v1 v2) @ s; E [{ Φ }]).
 Proof.
   rewrite envs_entails_eq=>?????; subst.
@@ -621,7 +621,7 @@ Tactic Notation "wp_faa" :=
   | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
     first
       [reshape_expr e ltac:(fun K e' => eapply (tac_wp_faa _ _ _ _ _ _ K))
-      |fail 1 "wp_faa: cannot find 'CAS' in" e];
+      |fail 1 "wp_faa: cannot find 'FAA' in" e];
     [iSolveTC
     |solve_mapsto ()
     |pm_reflexivity
@@ -629,7 +629,7 @@ Tactic Notation "wp_faa" :=
   | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
     first
       [reshape_expr e ltac:(fun K e' => eapply (tac_twp_faa _ _ _ _ _ K))
-      |fail 1 "wp_faa: cannot find 'CAS' in" e];
+      |fail 1 "wp_faa: cannot find 'FAA' in" e];
     [solve_mapsto ()
     |pm_reflexivity
     |wp_finish]