From 2850f8883bafe6d3676185cff210a68d640c42ea Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 16 Feb 2018 17:12:32 +0100
Subject: [PATCH] Add first definition of (logically) atomic shifts and triples

---
 _CoqProject                     |  2 ++
 theories/bi/lib/atomic.v        | 14 ++++++++++++++
 theories/program_logic/atomic.v | 14 ++++++++++++++
 3 files changed, 30 insertions(+)
 create mode 100644 theories/bi/lib/atomic.v
 create mode 100644 theories/program_logic/atomic.v

diff --git a/_CoqProject b/_CoqProject
index dc79c329b..799b53c49 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -37,6 +37,7 @@ theories/bi/fixpoint.v
 theories/bi/monpred.v
 theories/bi/embedding.v
 theories/bi/lib/fractional.v
+theories/bi/lib/atomic.v
 theories/base_logic/upred.v
 theories/base_logic/derived.v
 theories/base_logic/base_logic.v
@@ -72,6 +73,7 @@ theories/program_logic/ectx_lifting.v
 theories/program_logic/ownp.v
 theories/program_logic/total_lifting.v
 theories/program_logic/total_ectx_lifting.v
+theories/program_logic/atomic.v
 theories/heap_lang/lang.v
 theories/heap_lang/tactics.v
 theories/heap_lang/lifting.v
diff --git a/theories/bi/lib/atomic.v b/theories/bi/lib/atomic.v
new file mode 100644
index 000000000..4ae20945f
--- /dev/null
+++ b/theories/bi/lib/atomic.v
@@ -0,0 +1,14 @@
+From iris.bi Require Export bi updates.
+From stdpp Require Import coPset.
+From iris.proofmode Require Import classes class_instances.
+Set Default Proof Using "Type".
+
+Definition atomic_shift {PROP: sbi} `{!FUpd PROP} {A B : Type}
+  (α: A → PROP) (* atomic pre-condition *)
+  (β: A → B → PROP) (* atomic post-condition *)
+  (Ei Eo: coPset) (* inside/outside masks *)
+  (Q: A → B → PROP) (* post-condition *)
+  : PROP :=
+    (∃ (F P:PROP), F ∗ ▷ P ∗ □ (▷ P ={Eo, Ei}=∗ ∃ x, α x ∗
+          ((α x ={Ei, Eo}=∗ ▷ P) ∧ (∀ y, β x y ={Ei, Eo}=∗ F -∗ Q x y)))
+    )%I.
diff --git a/theories/program_logic/atomic.v b/theories/program_logic/atomic.v
new file mode 100644
index 000000000..2ee188978
--- /dev/null
+++ b/theories/program_logic/atomic.v
@@ -0,0 +1,14 @@
+From iris.program_logic Require Export weakestpre.
+From iris.proofmode Require Import tactics classes.
+From iris.bi.lib Require Import atomic.
+Set Default Proof Using "Type".
+
+Definition atomic_wp `{irisG Λ Σ} {A B : Type}
+  (e: expr Λ) (* expression *)
+  (α: A → iProp Σ) (* atomic pre-condition *)
+  (β: A → B → iProp Σ) (* atomic post-condition *)
+  (Ei Eo: coPset) (* inside/outside masks *)
+  (f: A → B → val Λ) (* Turn the return data into the return value *)
+  : iProp Σ :=
+    (∀ Φ, atomic_shift α β Ei Eo (λ x y, Φ (f x y)) -∗
+          WP e {{ Φ }})%I.
-- 
GitLab