From 64751fcd846a1a96ea977896a0fa9cc219e7ae43 Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Fri, 9 Dec 2016 10:11:34 +0100
Subject: [PATCH] prove lemma for non-deterministic CAS on locations

---
 theories/lang/derived.v |  2 +-
 theories/lang/heap.v    | 25 ++++++++++++++++++++++++-
 2 files changed, 25 insertions(+), 2 deletions(-)

diff --git a/theories/lang/derived.v b/theories/lang/derived.v
index 0f4519c0..04362d16 100644
--- a/theories/lang/derived.v
+++ b/theories/lang/derived.v
@@ -78,7 +78,7 @@ Proof.
   iNext. iIntros (?? Heval). inversion_clear Heval. done.
 Qed.
 
-(* TODO: Add lemmas for remaining binary operators. *)
+(* TODO: Add lemmas for equality test. *)
 
 Lemma wp_if E (b : bool) e1 e2 Φ :
   (if b then ▷ WP e1 @ E {{ Φ }} else ▷ WP e2 @ E {{ Φ }})%I -∗
diff --git a/theories/lang/heap.v b/theories/lang/heap.v
index a2f0e148..b6250b80 100644
--- a/theories/lang/heap.v
+++ b/theories/lang/heap.v
@@ -608,5 +608,28 @@ Section heap.
     iNext. iExists _, hF. iFrame. eauto using  heap_freeable_rel_stable.
   Qed.
 
-  (* TODO: Add a lemma for non-deterministic CAS on locations. *)
+  Lemma wp_cas_loc_nondet E l l1 e2 l2 ll :
+    ↑heapN ⊆ E → to_val e2 = Some $ LitV $ LitLoc l2 →
+    {{{ heap_ctx ∗ ▷ l ↦ (LitV $ LitLoc ll) }}}
+      CAS (Lit $ LitLoc l) (Lit $ LitLoc l1) e2 @ E
+    {{{ b, RET LitV $ lit_of_bool b;
+        if b is true then l ↦ LitV (LitLoc l2)
+        else ⌜l1 ≠ ll⌝ ∗ l ↦ LitV (LitLoc ll) }}}.
+  Proof.
+    iIntros (? <-%of_to_val?) "[#Hinv >Hv] HΦ".
+    rewrite /heap_ctx /heap_inv heap_mapsto_eq /heap_mapsto_def.
+    iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
+    iDestruct (heap_mapsto_lookup_1 with "Hvalσ Hv") as %?.
+    iApply (wp_cas_pst with "[$Hσ]"); eauto.
+    { destruct (decide (l1 = ll)) as [->|Hne].
+      - left. by constructor.
+      - right. by constructor. }
+    iNext. iIntros ([|]).
+    - iIntros "[_ Hσ]". iMod (heap_write_vs with "[$Hvalσ $Hv]") as "[Hvalσ Hv]"; first done.
+      iMod ("Hclose" with "[-Hv HΦ]"); last by iApply "HΦ"; iFrame.
+      iNext. iExists _, hF. iFrame. eauto using  heap_freeable_rel_stable.
+    - iIntros "[Hneq Hσ]". iDestruct "Hneq" as %Hneq. inversion_clear Hneq.
+      iMod ("Hclose" with "[-Hv HΦ]"); last by iApply ("HΦ" $! false); iFrame.
+      iNext. iExists _, hF. iFrame. eauto using  heap_freeable_rel_stable.
+  Qed.
 End heap.
-- 
GitLab