From f7f8a06902c4591688285be5045ecebf5313ff34 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Thu, 25 Jun 2020 16:15:33 +0200
Subject: [PATCH] add rel_resolveatomic_l

---
 theories/logic/rules.v | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

diff --git a/theories/logic/rules.v b/theories/logic/rules.v
index 98df0d5..e39b094 100644
--- a/theories/logic/rules.v
+++ b/theories/logic/rules.v
@@ -358,6 +358,23 @@ Section rules.
     iNext. iIntros (vs'). by rewrite -bi.wand_curry.
   Qed.
 
+  Lemma refines_resolveatomic_l K E (p : proph_id) e w t A :
+    Atomic StronglyAtomic e →
+    to_val e = None →
+    (|={⊤,E}=> ∃ vs,
+           ▷ (proph p vs) ∗
+           WP e @ E {{ v, ∀ (vs' : list (val*val)), ⌜vs = (v,w)::vs'⌝ -∗
+                  proph p vs' -∗
+                  REL fill K (of_val v) << t @ E : A }})%I
+    -∗ REL fill K (Resolve e #p w) << t : A.
+  Proof.
+    iIntros (??) "Hlog".
+    iApply refines_atomic_l; auto.
+    { apply strongly_atomic_atomic. apply _. }
+    iMod "Hlog" as (vs) "[>Hp Hlog]". iModIntro.
+    iApply (wp_resolve with "Hp"); auto.
+  Qed.
+
   Lemma refines_load_l K E l q t A :
     (|={⊤,E}=> ∃ v',
       ▷(l ↦{q} v') ∗
-- 
GitLab