prove wp_cas_loc_nondet

theories/lang/lifting.v

@@ -396,24 +396,34 @@ Proof.
   iApply "HΦ". iFrame "Hl Hl' Hl1 Hstk".
 Qed.
 
-(* Lemma wp_cas_loc_nondet E l tg l1 tg1 e2 l2 tg2 ll tgl : *)
-(*   IntoVal e2 (LitV $ LitLoc l2 tg2) → ↑stborN ⊆ E → *)
-(*   {{{ ▷ l ↦ LitV (LitLoc ll tgl) }}} *)
-(*     CAS (Lit $ LitLoc l tg) (Lit $ LitLoc l1 tg1) e2 @ E *)
-(*   {{{ b, RET LitV (lit_of_bool b); *)
-(*       if b is true then l ↦ LitV (LitLoc l2 tg2) *)
-(*       else ⌜l1 ≠ ll⌝ ∗ l ↦ LitV (LitLoc ll tgl) }}}. *)
-(* Proof. *)
-(*   iIntros (<- Φ) ">Hv HΦ". *)
-(*   iApply wp_lift_atomic_head_step_no_fork; auto. *)
-(*   iIntros ([σ1 stbor] ???) "[Hσ Hstbor]". iDestruct (heap_read_1 with "Hσ Hv") as %?. *)
-(*   iModIntro; iSplit; first (destruct (decide (ll = l1)) as [->|]; by eauto). *)
-(*   iNext; iIntros (v2 σ2 efs Hstep); inv_head_step; last lia. *)
-(*   - inv_lit. iModIntro; iSplit; [done|]; iFrame "Hσ Hstbor". *)
-(*     iApply "HΦ"; simpl; auto. *)
-(*   - iMod (heap_write with "Hσ Hv") as "[$ Hv]". iFrame "Hstbor". *)
-(*     iModIntro; iSplit; [done|]. iApply "HΦ"; iFrame. *)
-(* Qed. *)
+Lemma wp_cas_loc_nondet E l tg l1 tg1 e2 l2 tg2 ll tgl q gstk :
+  IntoVal e2 (LitV $ LitLoc l2 tg2) → ↑stborN ⊆ E →
+  ghost_grants_write gstk tg -∗
+  {{{ ▷ l ↦ LitV (LitLoc ll tgl) ∗ ▷ stbor_active l q gstk }}}
+    CAS (Lit $ LitLoc l tg) (Lit $ LitLoc l1 tg1) e2 @ E
+  {{{ b, RET LitV (lit_of_bool b);
+      if b is true then l ↦ LitV (LitLoc l2 tg2) ∗ ▷ stbor_active l q gstk
+      else ⌜l1 ≠ ll⌝ ∗ l ↦ LitV (LitLoc ll tgl) ∗ ▷ stbor_active l q gstk }}}.
+Proof.
+  iIntros (<- ?) "#Hgrantsw !>". iIntros (Φ) "[>Hv >Hstk] HΦ".
+  iDestruct (ghost_grants_write_to_read with "Hgrantsw") as "#Hgrantsr".
+  iApply wp_lift_atomic_head_step_no_fork; auto.
+  iIntros ([σ1 stbor] ???) "(Hσ & Hstbor & #BOR)".
+  iDestruct (heap_read_1 with "Hσ Hv") as %?.
+  iMod (stbor_inv_set stbor with "BOR Hstbor") as "(Hctx & Hstbor & Hclose)"; first done.
+  iDestruct (stbor_read_ctx_1 with "Hgrantsr Hctx Hstk") as %[? Hstborstepr].
+  iDestruct (stbor_write_ctx_1 with "Hgrantsw Hctx Hstk") as %[? Hstborstepw].
+  iMod ("Hclose" with "Hctx") as "_".
+  iModIntro; iSplit; first (destruct (decide (ll = l1)) as [->|]; by eauto).
+  iNext; iIntros (v2 σ2 efs Hstep); inv_head_step; last lia.
+  - inv_lit.
+    iMod (stbor_read with "BOR Hgrantsr Hstbor Hstk") as "[Hstbor Hstk]"; [done|done|].
+    iModIntro; iSplit; [done|]; iFrame "Hσ Hstbor BOR". iApply "HΦ"; simpl; iFrame "Hv Hstk"; auto.
+  - iMod (heap_write with "Hσ Hv") as "[$ Hv]".
+    iMod (stbor_write with "BOR Hgrantsw Hstbor Hstk") as "[Hstbor Hstk]"; [done|done|].
+    iFrame "Hstbor BOR".
+    iModIntro; iSplit; [done|]. iApply "HΦ"; iFrame.
+Qed.
 
 Lemma wp_eq_loc E (l1 : loc) (l2: loc) tg1 tg2 q1 q2 v1 v2 P Φ :
   (P -∗ ▷ l1 ↦{q1} v1) →

theories/lang/stbor/stbor_ghost.v

@@ -308,6 +308,15 @@ Section defs.
   Global Instance ghost_grants_read_pers gstk tg : Persistent (ghost_grants_read gstk tg).
   Proof. induction gstk as [|[| |]]; apply _. Qed.
 
+  Lemma ghost_grants_write_to_read tg gstk :
+    ghost_grants_write gstk tg -∗
+    ghost_grants_read gstk tg.
+  Proof.
+    iIntros "#Hwrite".
+    destruct gstk as [|[| |] gstk]; try done.
+    iLeft. iFrame "Hwrite".
+  Qed.
+
   Lemma ghost_grants_write_log tg gstk stklog :
     ghost_grants_write gstk tg -∗
     stbor_ghost_stack stklog gstk -∗