diff --git a/tests/atomic.ref b/tests/atomic.ref
new file mode 100644
index 0000000000000000000000000000000000000000..864ff13700f6a594c1fc9049be4ba2fd06b537a5
--- /dev/null
+++ b/tests/atomic.ref
@@ -0,0 +1,340 @@
+1 subgoal
+
+ Σ : gFunctors
+ heapG0 : heapG Σ
+ P : val → iProp Σ
+ ============================
+ <<< ∀ x : val, P x >>> code @ ⊤ <<< ∃ y : val, P y, RET #() >>>
+1 subgoal
+
+ Σ : gFunctors
+ heapG0 : heapG Σ
+ P : val → iProp Σ
+ Q : iPropI Σ
+ Φ : language.val heap_lang → iProp Σ
+ ============================
+ _ : Q
+ "AU" : AU << ∀ x : val, P x >> @ ⊤, ∅ << ∃ y : val, P y, COMM Q -∗ Φ #() >>
+ --------------------------------------∗
+ WP code {{ v, Φ v }}
+
+1 subgoal
+
+ Σ : gFunctors
+ heapG0 : heapG Σ
+ P : val → iProp Σ
+ Q : iPropI Σ
+ Φ : language.val heap_lang → iProp Σ
+ ============================
+ _ : Q
+ _ : AACC << ∀ x : val, P x
+ ABORT AU << ∀ x : val, P x >> @ ⊤, ∅
+ << ∃ y : val, P y, COMM Q -∗ Φ #() >> >> @ ⊤, ∅
+ << ∃ y : val, P y, COMM Q -∗ Φ #() >>
+ --------------------------------------∗
+ WP code {{ v, Φ v }}
+
+1 subgoal
+
+ Σ : gFunctors
+ heapG0 : heapG Σ
+ l : loc
+ ============================
+ <<< ∀ x : val, l ↦ x >>> code @ ⊤ <<< l ↦ x, RET #() >>>
+1 subgoal
+
+ Σ : gFunctors
+ heapG0 : heapG Σ
+ l : loc
+ Q : iPropI Σ
+ Φ : language.val heap_lang → iProp Σ
+ ============================
+ _ : Q
+ "AU" : AU << ∀ x : val, l ↦ x >> @ ⊤, ∅ << l ↦ x, COMM Q -∗ Φ #() >>
+ --------------------------------------∗
+ WP code {{ v, Φ v }}
+
+1 subgoal
+
+ Σ : gFunctors
+ heapG0 : heapG Σ
+ l : loc
+ Q : iPropI Σ
+ Φ : language.val heap_lang → iProp Σ
+ ============================
+ _ : Q
+ _ : AACC << ∀ x : val, l ↦ x
+ ABORT AU << ∀ x : val, l ↦ x >> @ ⊤, ∅
+ << l ↦ x, COMM Q -∗ Φ #() >> >> @ ⊤, ∅
+ << l ↦ x, COMM Q -∗ Φ #() >>
+ --------------------------------------∗
+ WP code {{ v, Φ v }}
+
+1 subgoal
+
+ Σ : gFunctors
+ heapG0 : heapG Σ
+ l : loc
+ ============================
+ <<< l ↦ #() >>> code @ ⊤ <<< ∃ y : val, l ↦ y, RET #() >>>
+1 subgoal
+
+ Σ : gFunctors
+ heapG0 : heapG Σ
+ l : loc
+ Q : iPropI Σ
+ Φ : language.val heap_lang → iProp Σ
+ ============================
+ _ : Q
+ "AU" : AU << l ↦ #() >> @ ⊤, ∅ << ∃ y : val, l ↦ y, COMM Q -∗ Φ #() >>
+ --------------------------------------∗
+ WP code {{ v, Φ v }}
+
+1 subgoal
+
+ Σ : gFunctors
+ heapG0 : heapG Σ
+ l : loc
+ Q : iPropI Σ
+ Φ : language.val heap_lang → iProp Σ
+ ============================
+ _ : Q
+ _ : AACC << l ↦ #()
+ ABORT AU << l ↦ #() >> @ ⊤, ∅
+ << ∃ y : val, l ↦ y, COMM Q -∗ Φ #() >> >> @ ⊤, ∅
+ << ∃ y : val, l ↦ y, COMM Q -∗ Φ #() >>
+ --------------------------------------∗
+ WP code {{ v, Φ v }}
+
+1 subgoal
+
+ Σ : gFunctors
+ heapG0 : heapG Σ
+ l : loc
+ ============================
+ <<< l ↦ #() >>> code @ ⊤ <<< l ↦ #(), RET #() >>>
+1 subgoal
+
+ Σ : gFunctors
+ heapG0 : heapG Σ
+ l : loc
+ Q : iPropI Σ
+ Φ : language.val heap_lang → iProp Σ
+ ============================
+ _ : Q
+ "AU" : AU << l ↦ #() >> @ ⊤, ∅ << l ↦ #(), COMM Q -∗ Φ #() >>
+ --------------------------------------∗
+ WP code {{ v, Φ v }}
+
+1 subgoal
+
+ Σ : gFunctors
+ heapG0 : heapG Σ
+ l : loc
+ Q : iPropI Σ
+ Φ : language.val heap_lang → iProp Σ
+ ============================
+ _ : Q
+ _ : AACC << l ↦ #()
+ ABORT AU << l ↦ #() >> @ ⊤, ∅ << l ↦ #(), COMM Q -∗ Φ #() >> >>
+ @ ⊤, ∅ << l ↦ #(), COMM Q -∗ Φ #() >>
+ --------------------------------------∗
+ WP code {{ v, Φ v }}
+
+"Now come the long pre/post tests"
+ : string
+1 subgoal
+
+ Σ : gFunctors
+ heapG0 : heapG Σ
+ l : loc
+ ============================
+ <<< ∀ x : val, l ↦ x ∗ l ↦ x >>> code @ ⊤ <<< ∃ y : val, l ↦ y, RET #() >>>
+1 subgoal
+
+ Σ : gFunctors
+ heapG0 : heapG Σ
+ l : loc
+ Q : iPropI Σ
+ Φ : language.val heap_lang → iProp Σ
+ ============================
+ _ : Q
+ "AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x >> @ ⊤, ∅
+ << ∃ y : val, l ↦ y, COMM Q -∗ Φ #() >>
+ --------------------------------------∗
+ WP code {{ v, Φ v }}
+
+1 subgoal
+
+ Σ : gFunctors
+ heapG0 : heapG Σ
+ l : loc
+ ============================
+ <<< ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
+ code @ ⊤
+ <<< ∃ y : val, l ↦ y, RET #() >>>
+1 subgoal
+
+ Σ : gFunctors
+ heapG0 : heapG Σ
+ l : loc
+ Q : iPropI Σ
+ Φ : language.val heap_lang → iProp Σ
+ ============================
+ _ : Q
+ "AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>
+ @ ⊤, ∅ << ∃ y : val, l ↦ y, COMM Q -∗ Φ #() >>
+ --------------------------------------∗
+ WP code {{ v, Φ v }}
+
+1 subgoal
+
+ Σ : gFunctors
+ heapG0 : heapG Σ
+ l : loc
+ ============================
+ <<< ∀ xx : val, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
+ code @ ⊤
+ <<< ∃ yyyy : val, l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
+ RET #() >>>
+1 subgoal
+
+ Σ : gFunctors
+ heapG0 : heapG Σ
+ l : loc
+ Q : iPropI Σ
+ Φ : language.val heap_lang → iProp Σ
+ ============================
+ _ : Q
+ _ : AU << ∀ xx : val, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >> @ ⊤, ∅
+ << ∃ yyyy : val, l ↦ yyyy
+ ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
+ COMM Q -∗ Φ #() >>
+ --------------------------------------∗
+ WP code {{ v, Φ v }}
+
+1 subgoal
+
+ Σ : gFunctors
+ heapG0 : heapG Σ
+ l : loc
+ ============================
+ <<< ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
+ code @ ⊤
+ <<< l ↦ x, RET #() >>>
+1 subgoal
+
+ Σ : gFunctors
+ heapG0 : heapG Σ
+ l : loc
+ Q : iPropI Σ
+ Φ : language.val heap_lang → iProp Σ
+ ============================
+ _ : Q
+ "AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >> @ ⊤, ∅
+ << l ↦ x, COMM Q -∗ Φ #() >>
+ --------------------------------------∗
+ WP code {{ v, Φ v }}
+
+1 subgoal
+
+ Σ : gFunctors
+ heapG0 : heapG Σ
+ l : loc
+ x : val
+ ============================
+ <<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
+ code @ ⊤
+ <<< ∃ y : val, l ↦ y, RET #() >>>
+1 subgoal
+
+ Σ : gFunctors
+ heapG0 : heapG Σ
+ l : loc
+ x : val
+ Q : iPropI Σ
+ Φ : language.val heap_lang → iProp Σ
+ ============================
+ _ : Q
+ "AU" : AU << l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >> @ ⊤, ∅
+ << ∃ y : val, l ↦ y, COMM Q -∗ Φ #() >>
+ --------------------------------------∗
+ WP code {{ v, Φ v }}
+
+1 subgoal
+
+ Σ : gFunctors
+ heapG0 : heapG Σ
+ l : loc
+ x : val
+ ============================
+ <<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
+ code @ ⊤
+ <<< l ↦ #(), RET #() >>>
+1 subgoal
+
+ Σ : gFunctors
+ heapG0 : heapG Σ
+ l : loc
+ x : val
+ Q : iPropI Σ
+ Φ : language.val heap_lang → iProp Σ
+ ============================
+ _ : Q
+ "AU" : AU << l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >> @ ⊤, ∅
+ << l ↦ #(), COMM Q -∗ Φ #() >>
+ --------------------------------------∗
+ WP code {{ v, Φ v }}
+
+1 subgoal
+
+ Σ : gFunctors
+ heapG0 : heapG Σ
+ l : loc
+ xx, yyyy : val
+ ============================
+ <<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
+ code @ ⊤
+ <<< l ↦ yyyy, RET #() >>>
+1 subgoal
+
+ Σ : gFunctors
+ heapG0 : heapG Σ
+ l : loc
+ xx, yyyy : val
+ Q : iPropI Σ
+ Φ : language.val heap_lang → iProp Σ
+ ============================
+ _ : Q
+ "AU" : AU << l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>
+ @ ⊤, ∅ << l ↦ yyyy, COMM Q -∗ Φ #() >>
+ --------------------------------------∗
+ WP code {{ v, Φ v }}
+
+1 subgoal
+
+ Σ : gFunctors
+ heapG0 : heapG Σ
+ l : loc
+ xx, yyyy : val
+ ============================
+ <<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
+ code @ ⊤
+ <<< l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
+ RET #() >>>
+1 subgoal
+
+ Σ : gFunctors
+ heapG0 : heapG Σ
+ l : loc
+ xx, yyyy : val
+ Q : iPropI Σ
+ Φ : language.val heap_lang → iProp Σ
+ ============================
+ _ : Q
+ "AU" : AU << l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >> @ ⊤, ∅
+ << l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
+ COMM Q -∗ Φ #() >>
+ --------------------------------------∗
+ WP code {{ v, Φ v }}
+
diff --git a/tests/atomic.v b/tests/atomic.v
new file mode 100644
index 0000000000000000000000000000000000000000..87efeb553794d71993524d191bd6af104b71d721
--- /dev/null
+++ b/tests/atomic.v
@@ -0,0 +1,91 @@
+From iris.heap_lang Require Export lifting notation.
+From iris.program_logic Require Export atomic.
+From iris.proofmode Require Import tactics.
+From iris.heap_lang Require Import proofmode notation.
+Set Default Proof Using "Type".
+
+(* Test if AWP and the AU obtained from AWP print. *)
+Section printing.
+ Context `{!heapG Σ}.
+
+ Definition code : expr := #().
+
+ Lemma print_both_quant (P : val → iProp Σ) :
+ <<< ∀ x, P x >>> code @ ⊤ <<< ∃ y, P y, RET #() >>>.
+ Proof.
+ Show. iIntros (Q Φ) "? AU". Show.
+ iPoseProof (aupd_aacc with "AU") as "?". Show.
+ Abort.
+
+ Lemma print_first_quant l :
+ <<< ∀ x, l ↦ x >>> code @ ⊤ <<< l ↦ x, RET #() >>>.
+ Proof.
+ Show. iIntros (Q Φ) "? AU". Show.
+ iPoseProof (aupd_aacc with "AU") as "?". Show.
+ Abort.
+
+ Lemma print_second_quant l :
+ <<< l ↦ #() >>> code @ ⊤ <<< ∃ y, l ↦ y, RET #() >>>.
+ Proof.
+ Show. iIntros (Q Φ) "? AU". Show.
+ iPoseProof (aupd_aacc with "AU") as "?". Show.
+ Abort.
+
+ Lemma print_no_quant l :
+ <<< l ↦ #() >>> code @ ⊤ <<< l ↦ #(), RET #() >>>.
+ Proof.
+ Show. iIntros (Q Φ) "? AU". Show.
+ iPoseProof (aupd_aacc with "AU") as "?". Show.
+ Abort.
+
+ Check "Now come the long pre/post tests".
+
+ Lemma print_both_quant_long l :
+ <<< ∀ x, l ↦ x ∗ l ↦ x >>> code @ ⊤ <<< ∃ y, l ↦ y, RET #() >>>.
+ Proof.
+ Show. iIntros (Q Φ) "? AU". Show.
+ Abort.
+
+ Lemma print_both_quant_longpre l :
+ <<< ∀ x, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>> code @ ⊤ <<< ∃ y, l ↦ y, RET #() >>>.
+ Proof.
+ Show. iIntros (Q Φ) "? AU". Show.
+ Abort.
+
+ Lemma print_both_quant_longpost l :
+ <<< ∀ xx, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>> code @ ⊤ <<< ∃ yyyy, l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx, RET #() >>>.
+ Proof.
+ Show. iIntros (Q Φ) "? ?". Show.
+ Abort.
+
+ Lemma print_first_quant_long l :
+ <<< ∀ x, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>> code @ ⊤ <<< l ↦ x, RET #() >>>.
+ Proof.
+ Show. iIntros (Q Φ) "? AU". Show.
+ Abort.
+
+ Lemma print_second_quant_long l x :
+ <<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>> code @ ⊤ <<< ∃ y, l ↦ y, RET #() >>>.
+ Proof.
+ Show. iIntros (Q Φ) "? AU". Show.
+ Abort.
+
+ Lemma print_no_quant_long l x :
+ <<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>> code @ ⊤ <<< l ↦ #(), RET #() >>>.
+ Proof.
+ Show. iIntros (Q Φ) "? AU". Show.
+ Abort.
+
+ Lemma print_no_quant_longpre l xx yyyy :
+ <<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>> code @ ⊤ <<< l ↦ yyyy, RET #() >>>.
+ Proof.
+ Show. iIntros (Q Φ) "? AU". Show.
+ Abort.
+
+ Lemma print_no_quant_longpost l xx yyyy :
+ <<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>> code @ ⊤ <<< l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx, RET #() >>>.
+ Proof.
+ Show. iIntros (Q Φ) "? AU". Show.
+ Abort.
+
+End printing.
diff --git a/theories/bi/lib/atomic.v b/theories/bi/lib/atomic.v
index 09b9ec49ce2c4b107f3732810cc774f7843df175..3ee47bfb0f10482961e6a91162d53c83a79e1161 100644
--- a/theories/bi/lib/atomic.v
+++ b/theories/bi/lib/atomic.v
@@ -9,24 +9,24 @@ Local Tactic Notation "iSplitWith" constr(H) :=
iApply (bi.and_parallel with H); iSplit; iIntros H.
Section definition.
- Context `{BiFUpd PROP} {A B : Type}.
+ Context `{BiFUpd PROP} {TA TB : tele}.
Implicit Types
- (Eo Em Ei : coPset) (* outside/module/inner masks *)
- (α : A → PROP) (* atomic pre-condition *)
+ (Eo Ei : coPset) (* outer/inner masks *)
+ (α : TA → PROP) (* atomic pre-condition *)
(P : PROP) (* abortion condition *)
- (β : A → B → PROP) (* atomic post-condition *)
- (Φ : A → B → PROP) (* post-condition *)
+ (β : TA → TB → PROP) (* atomic post-condition *)
+ (Φ : TA → TB → PROP) (* post-condition *)
.
(** atomic_acc as the "introduction form" of atomic updates: An accessor
that can be aborted back to [P]. *)
Definition atomic_acc Eo Ei α P β Φ : PROP :=
- (|={Eo, Ei}=> ∃ x, α x ∗
- ((α x ={Ei, Eo}=∗ P) ∧ (∀ y, β x y ={Ei, Eo}=∗ Φ x y))
+ (|={Eo, Ei}=> ∃.. x, α x ∗
+ ((α x ={Ei, Eo}=∗ P) ∧ (∀.. y, β x y ={Ei, Eo}=∗ Φ x y))
)%I.
Lemma atomic_acc_wand Eo Ei α P1 P2 β Φ1 Φ2 :
- ((P1 -∗ P2) ∧ (∀ x y, Φ1 x y -∗ Φ2 x y)) -∗
+ ((P1 -∗ P2) ∧ (∀.. x y, Φ1 x y -∗ Φ2 x y)) -∗
(atomic_acc Eo Ei α P1 β Φ1 -∗ atomic_acc Eo Ei α P2 β Φ2).
Proof.
iIntros "HP12 AS". iMod "AS" as (x) "[Hα Hclose]".
@@ -37,8 +37,8 @@ Section definition.
iApply "HP12". iApply "Hclose". done.
Qed.
- Lemma atomic_acc_mask Eo Em α P β Φ :
- atomic_acc Eo (Eo∖Em) α P β Φ ⊣⊢ ∀ E, ⌜Eo ⊆ E⌠→ atomic_acc E (E∖Em) α P β Φ.
+ Lemma atomic_acc_mask Eo Ed α P β Φ :
+ atomic_acc Eo (Eo∖Ed) α P β Φ ⊣⊢ ∀ E, ⌜Eo ⊆ E⌠→ atomic_acc E (E∖Ed) α P β Φ.
Proof.
iSplit; last first.
{ iIntros "Hstep". iApply ("Hstep" with "[% //]"). }
@@ -51,15 +51,27 @@ Section definition.
- iIntros (y) "Hβ". iApply "Hclose'". iApply "Hclose". done.
Qed.
+ Lemma atomic_acc_mask_weaken Eo1 Eo2 Ei α P β Φ :
+ Eo1 ⊆ Eo2 →
+ atomic_acc Eo1 Ei α P β Φ -∗ atomic_acc Eo2 Ei α P β Φ.
+ Proof.
+ iIntros (HE) "Hstep".
+ iMod fupd_intro_mask' as "Hclose1"; first done.
+ iMod "Hstep" as (x) "[Hα Hclose2]". iIntros "!>". iExists x.
+ iFrame. iSplitWith "Hclose2".
+ - iIntros "Hα". iMod ("Hclose2" with "Hα") as "$". done.
+ - iIntros (y) "Hβ". iMod ("Hclose2" with "Hβ") as "$". done.
+ Qed.
+
(** atomic_update as a fixed-point of the equation
AU = ∃ P. ▷ P ∗ □ (▷ P ==∗ α ∗ (α ==∗ AU) ∧ (β ==∗ Q))
= ∃ P. ▷ P ∗ □ (▷ P -∗ atomic_acc α AU β Q)
*)
- Context Eo Em α β Φ.
+ Context Eo Ei α β Φ.
Definition atomic_update_pre (Ψ : () → PROP) (_ : ()) : PROP :=
(∃ (P : PROP), ▷ P ∗
- □ (▷ P -∗ atomic_acc Eo (Eo∖Em) α (Ψ ()) β Φ))%I.
+ □ (▷ P -∗ atomic_acc Eo Ei α (Ψ ()) β Φ))%I.
Local Instance atomic_update_pre_mono : BiMonoPred atomic_update_pre.
Proof.
@@ -78,53 +90,177 @@ End definition.
(** Seal it *)
Definition atomic_update_aux : seal (@atomic_update_def). by eexists. Qed.
-Definition atomic_update `{BiFUpd PROP} {A B : Type} := atomic_update_aux.(unseal) PROP _ A B.
+Definition atomic_update `{BiFUpd PROP} {TA TB : tele} := atomic_update_aux.(unseal) PROP _ TA TB.
Definition atomic_update_eq :
@atomic_update = @atomic_update_def := atomic_update_aux.(seal_eq).
+Arguments atomic_acc {PROP _ TA TB} Eo Ei _ _ _ _ : simpl never.
+Arguments atomic_update {PROP _ TA TB} Eo Ei _ _ _ : simpl never.
+
+(** Notation: Atomic updates *)
+Notation "'AU' '<<' ∀ x1 .. xn , α '>>' @ Eo , Ei '<<' ∃ y1 .. yn , β , 'COMM' Φ '>>'" :=
+ (atomic_update (TA:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
+ (TB:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
+ Eo Ei
+ (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
+ λ x1, .. (λ xn, α%I) ..)
+ (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
+ λ x1, .. (λ xn,
+ tele_app (TT:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
+ (λ y1, .. (λ yn, β%I) .. )
+ ) .. )
+ (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
+ λ x1, .. (λ xn,
+ tele_app (TT:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
+ (λ y1, .. (λ yn, Φ%I) .. )
+ ) .. )
+ )
+ (at level 20, Eo, Ei, α, β, Φ at level 200, x1 binder, xn binder, y1 binder, yn binder,
+ format "'[ ' 'AU' '<<' ∀ x1 .. xn , α '>>' '/' @ Eo , Ei '/' '[ ' '<<' ∃ y1 .. yn , β , '/' COMM Φ '>>' ']' ']'") : bi_scope.
+
+Notation "'AU' '<<' ∀ x1 .. xn , α '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" :=
+ (atomic_update (TA:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
+ (TB:=TeleO)
+ Eo Ei
+ (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
+ λ x1, .. (λ xn, α%I) ..)
+ (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
+ λ x1, .. (λ xn, tele_app (TT:=TeleO) β%I) .. )
+ (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
+ λ x1, .. (λ xn, tele_app (TT:=TeleO) Φ%I) .. )
+ )
+ (at level 20, Eo, Ei, α, β, Φ at level 200, x1 binder, xn binder,
+ format "'[ ' 'AU' '<<' ∀ x1 .. xn , α '>>' '/' @ Eo , Ei '/' '[ ' '<<' β , '/' COMM Φ '>>' ']' ']'") : bi_scope.
+
+Notation "'AU' '<<' α '>>' @ Eo , Ei '<<' ∃ y1 .. yn , β , 'COMM' Φ '>>'" :=
+ (atomic_update (TA:=TeleO)
+ (TB:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
+ Eo Ei
+ (tele_app (TT:=TeleO) α%I)
+ (tele_app (TT:=TeleO) $
+ tele_app (TT:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
+ (λ y1, .. (λ yn, β%I) ..))
+ (tele_app (TT:=TeleO) $
+ tele_app (TT:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
+ (λ y1, .. (λ yn, Φ%I) ..))
+ )
+ (at level 20, Eo, Ei, α, β, Φ at level 200, y1 binder, yn binder,
+ format "'[ ' 'AU' '<<' α '>>' '/' @ Eo , Ei '/' '[ ' '<<' ∃ y1 .. yn , β , '/' COMM Φ '>>' ']' ']'") : bi_scope.
+
+Notation "'AU' '<<' α '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" :=
+ (atomic_update (TA:=TeleO) (TB:=TeleO) Eo Ei
+ (tele_app (TT:=TeleO) α%I)
+ (tele_app (TT:=TeleO) $ tele_app (TT:=TeleO) β%I)
+ (tele_app (TT:=TeleO) $ tele_app (TT:=TeleO) Φ%I)
+ )
+ (at level 20, Eo, Ei, α, β, Φ at level 200,
+ format "'[ ' 'AU' '<<' α '>>' '/' @ Eo , Ei '/' '[ ' '<<' β , '/' COMM Φ '>>' ']' ']'") : bi_scope.
+
+(** Notation: Atomic accessors *)
+Notation "'AACC' '<<' ∀ x1 .. xn , α 'ABORT' P '>>' @ Eo , Ei '<<' ∃ y1 .. yn , β , 'COMM' Φ '>>'" :=
+ (atomic_acc (TA:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
+ (TB:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
+ Eo Ei
+ (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
+ λ x1, .. (λ xn, α%I) ..)
+ P%I
+ (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
+ λ x1, .. (λ xn,
+ tele_app (TT:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
+ (λ y1, .. (λ yn, β%I) .. )
+ ) .. )
+ (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
+ λ x1, .. (λ xn,
+ tele_app (TT:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
+ (λ y1, .. (λ yn, Φ%I) .. )
+ ) .. )
+ )
+ (at level 20, Eo, Ei, α, P, β, Φ at level 200, x1 binder, xn binder, y1 binder, yn binder,
+ format "'[ ' 'AACC' '[ ' '<<' ∀ x1 .. xn , α '/' ABORT P '>>' ']' '/' @ Eo , Ei '/' '[ ' '<<' ∃ y1 .. yn , β , '/' COMM Φ '>>' ']' ']'") : bi_scope.
+
+Notation "'AACC' '<<' ∀ x1 .. xn , α 'ABORT' P '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" :=
+ (atomic_acc (TA:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
+ (TB:=TeleO)
+ Eo Ei
+ (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
+ λ x1, .. (λ xn, α%I) ..)
+ P%I
+ (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
+ λ x1, .. (λ xn, tele_app (TT:=TeleO) β%I) .. )
+ (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
+ λ x1, .. (λ xn, tele_app (TT:=TeleO) Φ%I) .. )
+ )
+ (at level 20, Eo, Ei, α, P, β, Φ at level 200, x1 binder, xn binder,
+ format "'[ ' 'AACC' '[ ' '<<' ∀ x1 .. xn , α '/' ABORT P '>>' ']' '/' @ Eo , Ei '/' '[ ' '<<' β , '/' COMM Φ '>>' ']' ']'") : bi_scope.
+
+Notation "'AACC' '<<' α 'ABORT' P '>>' @ Eo , Ei '<<' ∃ y1 .. yn , β , 'COMM' Φ '>>'" :=
+ (atomic_acc (TA:=TeleO)
+ (TB:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
+ Eo Ei
+ (tele_app (TT:=TeleO) α%I)
+ P%I
+ (tele_app (TT:=TeleO) $
+ tele_app (TT:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
+ (λ y1, .. (λ yn, β%I) ..))
+ (tele_app (TT:=TeleO) $
+ tele_app (TT:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
+ (λ y1, .. (λ yn, Φ%I) ..))
+ )
+ (at level 20, Eo, Ei, α, P, β, Φ at level 200, y1 binder, yn binder,
+ format "'[ ' 'AACC' '[ ' '<<' α '/' ABORT P '>>' ']' '/' @ Eo , Ei '/' '[ ' '<<' ∃ y1 .. yn , β , '/' COMM Φ '>>' ']' ']'") : bi_scope.
+
+Notation "'AACC' '<<' α 'ABORT' P '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" :=
+ (atomic_acc (TA:=TeleO)
+ (TB:=TeleO)
+ Eo Ei
+ (tele_app (TT:=TeleO) α%I)
+ P%I
+ (tele_app (TT:=TeleO) $ tele_app (TT:=TeleO) β%I)
+ (tele_app (TT:=TeleO) $ tele_app (TT:=TeleO) Φ%I)
+ )
+ (at level 20, Eo, Ei, α, P, β, Φ at level 200,
+ format "'[ ' 'AACC' '[ ' '<<' α '/' ABORT P '>>' ']' '/' @ Eo , Ei '/' '[ ' '<<' β , '/' COMM Φ '>>' ']' ']'") : bi_scope.
+
(** Lemmas about AU *)
Section lemmas.
- Context `{BiFUpd PROP} {A B : Type}.
- Implicit Types (α : A → PROP) (β Φ : A → B → PROP) (P : PROP).
+ Context `{BiFUpd PROP} {TA TB : tele}.
+ Implicit Types (α : TA → PROP) (β Φ : TA → TB → PROP) (P : PROP).
Local Existing Instance atomic_update_pre_mono.
- Global Instance atomic_acc_ne Eo Em n :
+ Global Instance atomic_acc_ne Eo Ei n :
Proper (
- pointwise_relation A (dist n) ==>
+ pointwise_relation TA (dist n) ==>
dist n ==>
- pointwise_relation A (pointwise_relation B (dist n)) ==>
- pointwise_relation A (pointwise_relation B (dist n)) ==>
+ pointwise_relation TA (pointwise_relation TB (dist n)) ==>
+ pointwise_relation TA (pointwise_relation TB (dist n)) ==>
dist n
- ) (atomic_acc (PROP:=PROP) Eo Em).
+ ) (atomic_acc (PROP:=PROP) Eo Ei).
Proof. solve_proper. Qed.
- Global Instance atomic_update_ne Eo Em n :
+ Global Instance atomic_update_ne Eo Ei n :
Proper (
- pointwise_relation A (dist n) ==>
- pointwise_relation A (pointwise_relation B (dist n)) ==>
- pointwise_relation A (pointwise_relation B (dist n)) ==>
+ pointwise_relation TA (dist n) ==>
+ pointwise_relation TA (pointwise_relation TB (dist n)) ==>
+ pointwise_relation TA (pointwise_relation TB (dist n)) ==>
dist n
- ) (atomic_update (PROP:=PROP) Eo Em).
+ ) (atomic_update (PROP:=PROP) Eo Ei).
Proof.
rewrite atomic_update_eq /atomic_update_def /atomic_update_pre. solve_proper.
Qed.
- (** The ellimination form: an accessor *)
- Lemma aupd_acc Eo Em E α β Φ :
- Eo ⊆ E →
- atomic_update Eo Em α β Φ -∗
- atomic_acc E (E∖Em) α (atomic_update Eo Em α β Φ) β Φ.
+ (** The ellimination form: an atomic accessor *)
+ Lemma aupd_aacc Eo Ei α β Φ :
+ atomic_update Eo Ei α β Φ -∗
+ atomic_acc Eo Ei α (atomic_update Eo Ei α β Φ) β Φ.
Proof using Type*.
- rewrite atomic_update_eq {1}/atomic_update_def /=. iIntros (HE) "HUpd".
+ rewrite atomic_update_eq {1}/atomic_update_def /=. iIntros "HUpd".
iPoseProof (greatest_fixpoint_unfold_1 with "HUpd") as "HUpd".
- iDestruct "HUpd" as (P) "(HP & Hshift)".
- iRevert (E HE). iApply atomic_acc_mask.
- iApply "Hshift". done.
+ iDestruct "HUpd" as (P) "(HP & Hshift)". by iApply "Hshift".
Qed.
- Global Instance aupd_laterable Eo Em α β Φ :
- Laterable (atomic_update Eo Em α β Φ).
+ Global Instance aupd_laterable Eo Ei α β Φ :
+ Laterable (atomic_update Eo Ei α β Φ).
Proof.
rewrite /Laterable atomic_update_eq {1}/atomic_update_def /=. iIntros "AU".
iPoseProof (greatest_fixpoint_unfold_1 with "AU") as (P) "[HP #AS]".
@@ -132,10 +268,10 @@ Section lemmas.
iApply greatest_fixpoint_unfold_2. iExists P. iFrame "#∗".
Qed.
- Lemma aupd_intro P Q α β Eo Em Φ :
+ Lemma aupd_intro P Q α β Eo Ei Φ :
Affine P → Persistent P → Laterable Q →
- (P ∗ Q -∗ atomic_acc Eo (Eo∖Em) α Q β Φ) →
- P ∗ Q -∗ atomic_update Eo Em α β Φ.
+ (P ∗ Q -∗ atomic_acc Eo Ei α Q β Φ) →
+ P ∗ Q -∗ atomic_update Eo Ei α β Φ.
Proof.
rewrite atomic_update_eq {1}/atomic_update_def /=.
iIntros (??? HAU) "[#HP HQ]".
@@ -145,12 +281,12 @@ Section lemmas.
iApply HAU. by iFrame.
Qed.
- Lemma aacc_intro x Eo Ei α P β Φ :
- Ei ⊆ Eo → α x -∗
- ((α x ={Eo}=∗ P) ∧ (∀ y, β x y ={Eo}=∗ Φ x y)) -∗
- atomic_acc Eo Ei α P β Φ.
+ Lemma aacc_intro Eo Ei α P β Φ :
+ Ei ⊆ Eo → (∀.. x, α x -∗
+ ((α x ={Eo}=∗ P) ∧ (∀.. y, β x y ={Eo}=∗ Φ x y)) -∗
+ atomic_acc Eo Ei α P β Φ)%I.
Proof.
- iIntros (?) "Hα Hclose".
+ iIntros (? x) "Hα Hclose".
iMod fupd_intro_mask' as "Hclose'"; last iModIntro; first set_solver.
iExists x. iFrame. iSplitWith "Hclose".
- iIntros "Hα". iMod "Hclose'" as "_". iApply "Hclose". done.
@@ -161,7 +297,8 @@ Section lemmas.
ElimAcc (X:=X) (fupd E1 E2) (fupd E2 E1) α' β' γ'
(atomic_acc E1 Ei α Pas β Φ)
(λ x', atomic_acc E2 Ei α (β' x' ∗ (γ' x' -∗? Pas))%I β
- (λ x y, β' x' ∗ (γ' x' -∗? Φ x y)))%I.
+ (λ.. x y, β' x' ∗ (γ' x' -∗? Φ x y))
+ )%I.
Proof.
rewrite /ElimAcc.
(* FIXME: Is there any way to prevent maybe_wand from unfolding?
@@ -176,21 +313,24 @@ Section lemmas.
iMod ("Hclose" with "Hβ'") as "Hγ'".
iModIntro. destruct (γ' x'); iApply "HPas"; done.
- iIntros (y) "Hβ". iMod "Hclose''" as "_".
- iMod ("Hclose'" with "Hβ") as "[Hβ' HΦ]".
+ iMod ("Hclose'" with "Hβ") as "Hβ'".
+ rewrite ->!tele_app_bind. iDestruct "Hβ'" as "[Hβ' HΦ]".
iMod ("Hclose" with "Hβ'") as "Hγ'".
iModIntro. destruct (γ' x'); iApply "HΦ"; done.
Qed.
- Lemma aacc_aacc {A' B'} E1 E2 E3
+ Lemma aacc_aacc {TA' TB' : tele} E1 E1' E2 E3
α P β Φ
- (α' : A' → PROP) P' (β' Φ' : A' → B' → PROP) :
- atomic_acc E1 E2 α P β Φ -∗
- (∀ x, α x -∗ atomic_acc E2 E3 α' (α x ∗ (P ={E1}=∗ P')) β'
- (λ x' y', (α x ∗ (P ={E1}=∗ Φ' x' y'))
- ∨ ∃ y, β x y ∗ (Φ x y ={E1}=∗ Φ' x' y'))) -∗
+ (α' : TA' → PROP) P' (β' Φ' : TA' → TB' → PROP) :
+ E1' ⊆ E1 →
+ atomic_acc E1' E2 α P β Φ -∗
+ (∀.. x, α x -∗ atomic_acc E2 E3 α' (α x ∗ (P ={E1}=∗ P')) β'
+ (λ.. x' y', (α x ∗ (P ={E1}=∗ Φ' x' y'))
+ ∨ ∃.. y, β x y ∗ (Φ x y ={E1}=∗ Φ' x' y'))) -∗
atomic_acc E1 E3 α' P' β' Φ'.
Proof.
- iIntros "Hupd Hstep". iMod ("Hupd") as (x) "[Hα Hclose]".
+ iIntros (?) "Hupd Hstep".
+ iMod (atomic_acc_mask_weaken with "Hupd") as (x) "[Hα Hclose]"; first done.
iMod ("Hstep" with "Hα") as (x') "[Hα' Hclose']".
iModIntro. iExists x'. iFrame "Hα'". iSplit.
- iIntros "Hα'". iDestruct "Hclose'" as "[Hclose' _]".
@@ -198,7 +338,8 @@ Section lemmas.
iDestruct "Hclose" as "[Hclose _]".
iMod ("Hclose" with "Hα"). iApply "Hupd". auto.
- iIntros (y') "Hβ'". iDestruct "Hclose'" as "[_ Hclose']".
- iMod ("Hclose'" with "Hβ'") as "[[Hα HΦ']|Hcont]".
+ iMod ("Hclose'" with "Hβ'") as "Hres".
+ rewrite ->!tele_app_bind. iDestruct "Hres" as "[[Hα HΦ']|Hcont]".
+ (* Abort the step we are eliminating *)
iDestruct "Hclose" as "[Hclose _]".
iMod ("Hclose" with "Hα") as "HP".
@@ -210,64 +351,63 @@ Section lemmas.
iApply "HΦ'". done.
Qed.
- Lemma aacc_aupd {A' B'} E1 E2 Eo Em
+ Lemma aacc_aupd {TA' TB' : tele} E1 E1' E2 E3
α β Φ
- (α' : A' → PROP) P' (β' Φ' : A' → B' → PROP) :
- Eo ⊆ E1 →
- atomic_update Eo Em α β Φ -∗
- (∀ x, α x -∗ atomic_acc (E1∖Em) E2 α' (α x ∗ (atomic_update Eo Em α β Φ ={E1}=∗ P')) β'
- (λ x' y', (α x ∗ (atomic_update Eo Em α β Φ ={E1}=∗ Φ' x' y'))
- ∨ ∃ y, β x y ∗ (Φ x y ={E1}=∗ Φ' x' y'))) -∗
- atomic_acc E1 E2 α' P' β' Φ'.
+ (α' : TA' → PROP) P' (β' Φ' : TA' → TB' → PROP) :
+ E1' ⊆ E1 →
+ atomic_update E1' E2 α β Φ -∗
+ (∀.. x, α x -∗ atomic_acc E2 E3 α' (α x ∗ (atomic_update E1' E2 α β Φ ={E1}=∗ P')) β'
+ (λ.. x' y', (α x ∗ (atomic_update E1' E2 α β Φ ={E1}=∗ Φ' x' y'))
+ ∨ ∃.. y, β x y ∗ (Φ x y ={E1}=∗ Φ' x' y'))) -∗
+ atomic_acc E1 E3 α' P' β' Φ'.
Proof.
- iIntros (?) "Hupd Hstep". iApply (aacc_aacc with "[Hupd] Hstep").
- iApply aupd_acc; done.
+ iIntros (?) "Hupd Hstep". iApply (aacc_aacc with "[Hupd] Hstep"); first done.
+ iApply aupd_aacc; done.
Qed.
- Lemma aacc_aupd_commit {A' B'} E1 E2 Eo Em
+ Lemma aacc_aupd_commit {TA' TB' : tele} E1 E1' E2 E3
α β Φ
- (α' : A' → PROP) P' (β' Φ' : A' → B' → PROP) :
- Eo ⊆ E1 →
- atomic_update Eo Em α β Φ -∗
- (∀ x, α x -∗ atomic_acc (E1∖Em) E2 α' (α x ∗ (atomic_update Eo Em α β Φ ={E1}=∗ P')) β'
- (λ x' y', ∃ y, β x y ∗ (Φ x y ={E1}=∗ Φ' x' y'))) -∗
- atomic_acc E1 E2 α' P' β' Φ'.
+ (α' : TA' → PROP) P' (β' Φ' : TA' → TB' → PROP) :
+ E1' ⊆ E1 →
+ atomic_update E1' E2 α β Φ -∗
+ (∀.. x, α x -∗ atomic_acc E2 E3 α' (α x ∗ (atomic_update E1' E2 α β Φ ={E1}=∗ P')) β'
+ (λ.. x' y', ∃.. y, β x y ∗ (Φ x y ={E1}=∗ Φ' x' y'))) -∗
+ atomic_acc E1 E3 α' P' β' Φ'.
Proof.
iIntros (?) "Hupd Hstep". iApply (aacc_aupd with "Hupd"); first done.
iIntros (x) "Hα". iApply atomic_acc_wand; last first.
{ iApply "Hstep". done. }
- iSplit; first by eauto. iIntros (??) "?". by iRight.
+ iSplit; first by eauto. iIntros (??) "?". rewrite ->!tele_app_bind. by iRight.
Qed.
- Lemma aacc_aupd_abort {A' B'} E1 E2 Eo Em
+ Lemma aacc_aupd_abort {TA' TB' : tele} E1 E1' E2 E3
α β Φ
- (α' : A' → PROP) P' (β' Φ' : A' → B' → PROP) :
- Eo ⊆ E1 →
- atomic_update Eo Em α β Φ -∗
- (∀ x, α x -∗ atomic_acc (E1∖Em) E2 α' (α x ∗ (atomic_update Eo Em α β Φ ={E1}=∗ P')) β'
- (λ x' y', α x ∗ (atomic_update Eo Em α β Φ ={E1}=∗ Φ' x' y'))) -∗
- atomic_acc E1 E2 α' P' β' Φ'.
+ (α' : TA' → PROP) P' (β' Φ' : TA' → TB' → PROP) :
+ E1' ⊆ E1 →
+ atomic_update E1' E2 α β Φ -∗
+ (∀.. x, α x -∗ atomic_acc E2 E3 α' (α x ∗ (atomic_update E1' E2 α β Φ ={E1}=∗ P')) β'
+ (λ.. x' y', α x ∗ (atomic_update E1' E2 α β Φ ={E1}=∗ Φ' x' y'))) -∗
+ atomic_acc E1 E3 α' P' β' Φ'.
Proof.
iIntros (?) "Hupd Hstep". iApply (aacc_aupd with "Hupd"); first done.
iIntros (x) "Hα". iApply atomic_acc_wand; last first.
{ iApply "Hstep". done. }
- iSplit; first by eauto. iIntros (??) "?". by iLeft.
+ iSplit; first by eauto. iIntros (??) "?". rewrite ->!tele_app_bind. by iLeft.
Qed.
End lemmas.
(** ProofMode support for atomic updates *)
-
Section proof_mode.
- Context `{BiFUpd PROP} {A B : Type}.
- Implicit Types (α : A → PROP) (β Φ : A → B → PROP) (P : PROP).
+ Context `{BiFUpd PROP} {TA TB : tele}.
+ Implicit Types (α : TA → PROP) (β Φ : TA → TB → PROP) (P : PROP).
- Lemma tac_aupd_intro Γp Γs n α β Eo Em Φ P :
+ Lemma tac_aupd_intro Γp Γs n α β Eo Ei Φ P :
Timeless (PROP:=PROP) emp →
TCForall Laterable (env_to_list Γs) →
P = prop_of_env Γs →
- envs_entails (Envs Γp Γs n) (atomic_acc Eo (Eo∖Em) α P β Φ) →
- envs_entails (Envs Γp Γs n) (atomic_update Eo Em α β Φ).
+ envs_entails (Envs Γp Γs n) (atomic_acc Eo Ei α P β Φ) →
+ envs_entails (Envs Γp Γs n) (atomic_update Eo Ei α β Φ).
Proof.
intros ? HΓs ->. rewrite envs_entails_eq of_envs_eq' /atomic_acc /=.
setoid_rewrite prop_of_env_sound =>HAU.
diff --git a/theories/heap_lang/lib/atomic_heap.v b/theories/heap_lang/lib/atomic_heap.v
index ad3f079a38ab3281c597ca7b9ed075d1ccbbcd12..33871ee90fda5cbc310a6ee80cede02c443ba485 100644
--- a/theories/heap_lang/lib/atomic_heap.v
+++ b/theories/heap_lang/lib/atomic_heap.v
@@ -21,29 +21,20 @@ Structure atomic_heap {Σ} `{!heapG Σ} := AtomicHeap {
alloc_spec v :
{{{ True }}} alloc v {{{ l, RET #l; mapsto l 1 v }}};
load_spec (l : loc) :
- atomic_wp (load #l)%E
- ⊤ ⊤
- (λ '(v, q), mapsto l q v)
- (λ '(v, q) (_:()), mapsto l q v)
- (λ '(v, q) _, v);
+ <<< ∀ (v : val) q, mapsto l q v >>> load #l @ ⊤ <<< mapsto l q v, RET v >>>;
store_spec (l : loc) (e : expr) (w : val) :
IntoVal e w →
- atomic_wp (store (#l, e))%E
- ⊤ ⊤
- (λ v, mapsto l 1 v)
- (λ v (_:()), mapsto l 1 w)
- (λ _ _, #()%V);
+ <<< ∀ v, mapsto l 1 v >>> store (#l, e) @ ⊤
+ <<< mapsto l 1 w, RET #() >>>;
(* This spec is slightly weaker than it could be: It is sufficient for [w1]
*or* [v] to be unboxed. However, by writing it this way the [val_is_unboxed]
is outside the atomic triple, which makes it much easier to use -- and the
spec is still good enough for all our applications. *)
cas_spec (l : loc) (e1 e2 : expr) (w1 w2 : val) :
IntoVal e1 w1 → IntoVal e2 w2 → val_is_unboxed w1 →
- atomic_wp (cas (#l, e1, e2))%E
- ⊤ ⊤
- (λ v, mapsto l 1 v)%I
- (λ v (_:()), if decide (v = w1) then mapsto l 1 w2 else mapsto l 1 v)
- (λ v _, #(if decide (v = w1) then true else false)%V);
+ <<< ∀ v, mapsto l 1 v >>> cas (#l, e1, e2) @ ⊤
+ <<< if decide (v = w1) then mapsto l 1 w2 else mapsto l 1 v,
+ RET #(if decide (v = w1) then true else false) >>>;
}.
Arguments atomic_heap _ {_}.
@@ -67,42 +58,35 @@ Section proof.
Qed.
Lemma primitive_load_spec (l : loc) :
- atomic_wp (primitive_load #l)%E
- ⊤ ⊤
- (λ '(v, q), l ↦{q} v)%I
- (λ '(v, q) (_:()), l ↦{q} v)%I
- (λ '(v, q) _, v).
+ <<< ∀ (v : val) q, l ↦{q} v >>> primitive_load #l @ ⊤
+ <<< l ↦{q} v, RET v >>>.
Proof.
iIntros (Q Φ) "? AU". wp_let.
- iMod (aupd_acc with "AU") as ((v, q)) "[H↦ [_ Hclose]]"; first solve_ndisj.
- wp_load. iMod ("Hclose" $! () with "H↦") as "HΦ". by iApply "HΦ".
+ iMod (aupd_aacc with "AU") as (v q) "[H↦ [_ Hclose]]".
+ wp_load. iMod ("Hclose" with "H↦") as "HΦ". by iApply "HΦ".
Qed.
Lemma primitive_store_spec (l : loc) (e : expr) (w : val) :
IntoVal e w →
- atomic_wp (primitive_store (#l, e))%E
- ⊤ ⊤
- (λ v, l ↦ v)%I
- (λ v (_:()), l ↦ w)%I
- (λ _ _, #()%V).
+ <<< ∀ v, l ↦ v >>> primitive_store (#l, e) @ ⊤
+ <<< l ↦ w, RET #() >>>.
Proof.
iIntros (<- Q Φ) "? AU". wp_let. wp_proj. wp_proj.
- iMod (aupd_acc with "AU") as (v) "[H↦ [_ Hclose]]"; first solve_ndisj.
- wp_store. iMod ("Hclose" $! () with "H↦") as "HΦ". by iApply "HΦ".
+ iMod (aupd_aacc with "AU") as (v) "[H↦ [_ Hclose]]".
+ wp_store. iMod ("Hclose" with "H↦") as "HΦ". by iApply "HΦ".
Qed.
Lemma primitive_cas_spec (l : loc) e1 e2 (w1 w2 : val) :
IntoVal e1 w1 → IntoVal e2 w2 → val_is_unboxed w1 →
- atomic_wp (primitive_cas (#l, e1, e2))%E
- ⊤ ⊤
- (λ v, l ↦ v)%I
- (λ v (_:()), if decide (v = w1) then l ↦ w2 else l ↦ v)%I
- (λ v _, #(if decide (v = w1) then true else false)%V).
+ <<< ∀ (v : val), l ↦ v >>>
+ primitive_cas (#l, e1, e2) @ ⊤
+ <<< if decide (v = w1) then l ↦ w2 else l ↦ v,
+ RET #(if decide (v = w1) then true else false) >>>.
Proof.
iIntros (<- <- ? Q Φ) "? AU". wp_let. repeat wp_proj.
- iMod (aupd_acc with "AU") as (v) "[H↦ [_ Hclose]]"; first solve_ndisj.
+ iMod (aupd_aacc with "AU") as (v) "[H↦ [_ Hclose]]".
destruct (decide (v = w1)) as [<-|Hv]; [wp_cas_suc|wp_cas_fail];
- iMod ("Hclose" $! () with "H↦") as "HΦ"; by iApply "HΦ".
+ iMod ("Hclose" with "H↦") as "HΦ"; by iApply "HΦ".
Qed.
Definition primitive_atomic_heap : atomic_heap Σ :=
diff --git a/theories/heap_lang/lib/increment.v b/theories/heap_lang/lib/increment.v
index 4640f7c0167214e2bc091b1c408e6280dae655ae..8f6d9b12c7045bfa0be805b3f807018ec1d81038 100644
--- a/theories/heap_lang/lib/increment.v
+++ b/theories/heap_lang/lib/increment.v
@@ -19,31 +19,32 @@ Section increment.
else "incr" "l".
Lemma incr_spec (l: loc) :
- atomic_wp (incr #l)
- ⊤ ⊤
- (λ (v: Z), aheap.(mapsto) l 1 #v)%I
- (λ v (_:()), aheap.(mapsto) l 1 #(v + 1))%I
- (λ v _, #v).
+ <<< ∀ (v : Z), aheap.(mapsto) l 1 #v >>> incr #l @ ⊤
+ <<< aheap.(mapsto) l 1 #(v + 1), RET #v >>>.
Proof.
iIntros (Q Φ) "HQ AU". iLöb as "IH". wp_let.
wp_apply (load_spec with "[HQ]"); first by iAccu.
(* Prove the atomic shift for load *)
iAuIntro. iApply (aacc_aupd_abort with "AU"); first done.
iIntros (x) "H↦".
- iApply (aacc_intro (_, _) with "[H↦]"); [solve_ndisj|done|iSplit].
+ (* FIXME: Oh wow this is bad. *)
+ iApply (aacc_intro $! ([tele_arg _; _] : [tele (_:val) (_:Qp)]) with "[H↦]"); [solve_ndisj|done|iSplit].
{ iIntros "$ !> $ !> //". }
- iIntros ([]) "$ !> AU !> HQ".
+ iIntros "$ !> AU !> HQ".
(* Now go on *)
wp_let. wp_op. wp_bind (aheap.(cas) _)%I.
- wp_apply (cas_spec with "[HQ]"); first done; first by iAccu.
+ wp_apply (cas_spec with "[HQ]"); [done|iAccu|].
(* Prove the atomic shift for CAS *)
iAuIntro. iApply (aacc_aupd with "AU"); first done.
iIntros (x') "H↦".
- iApply (aacc_intro with "[H↦]"); [solve_ndisj|done|iSplit].
+ (* FIXME: Oh wow this is bad. *)
+ iApply (aacc_intro $! ([tele_arg _] : [tele (_:val)]) with "[H↦]"); [solve_ndisj|simpl; by auto with iFrame|iSplit].
{ eauto 10 with iFrame. }
- iIntros ([]) "H↦ !>".
+ (* FIXME: Manual reduction should not be needed. *)
+ reduction.pm_reduce.
+ iIntros "H↦ !>".
destruct (decide (#x' = #x)) as [[= ->]|Hx].
- - iRight. iExists (). iFrame. iIntros "HΦ !> HQ".
+ - iRight. iFrame. iIntros "HΦ !> HQ".
wp_if. by iApply "HΦ".
- iLeft. iFrame. iIntros "AU !> HQ".
wp_if. iApply ("IH" with "HQ"). done.
@@ -69,9 +70,10 @@ Section increment_client.
iAssert (â–¡ WP incr primitive_atomic_heap #l {{ _, True }})%I as "#Aupd".
{ iAlways. wp_apply (incr_spec with "[]"); first by iAccu. clear x.
iAuIntro. iInv nroot as (x) ">H↦".
- iApply (aacc_intro with "[H↦]"); [solve_ndisj|done|iSplit].
+ (* FIXME: Oh wow this is bad. *)
+ iApply (aacc_intro $! ([tele_arg _] : [tele (_:Z)]) with "[H↦]"); [solve_ndisj|done|iSplit].
{ by eauto 10. }
- iIntros ([]) "H↦ !>". iSplitL "H↦"; first by eauto 10.
+ iIntros "H↦ !>". iSplitL "H↦"; first by eauto 10.
(* The continuation: From after the atomic triple to the postcondition of the WP *)
done.
}
diff --git a/theories/program_logic/atomic.v b/theories/program_logic/atomic.v
index b8a395fc27f0fec783b494f375b851fae292c7d5..75d33c76346e46c39763312591e634234450a102 100644
--- a/theories/program_logic/atomic.v
+++ b/theories/program_logic/atomic.v
@@ -1,16 +1,92 @@
From iris.program_logic Require Export weakestpre.
From iris.proofmode Require Import tactics classes.
From iris.bi.lib Require Export atomic.
+From iris.bi Require Import telescopes.
Set Default Proof Using "Type".
-Definition atomic_wp `{irisG Λ Σ} {A B : Type}
+(* This hard-codes the inner mask to be empty, because we have yet to find an
+example where we want it to be anything else. *)
+Definition atomic_wp `{irisG Λ Σ} {TA TB : tele}
(e: expr Λ) (* expression *)
- (Eo Em : coPset) (* outside/module masks *)
- (α: A → iProp Σ) (* atomic pre-condition *)
- (β: A → B → iProp Σ) (* atomic post-condition *)
- (f: A → B → val Λ) (* Turn the return data into the return value *)
+ (Eo : coPset) (* (outer) mask *)
+ (α: TA → iProp Σ) (* atomic pre-condition *)
+ (β: TA → TB → iProp Σ) (* atomic post-condition *)
+ (f: TA → TB → val Λ) (* Turn the return data into the return value *)
: iProp Σ :=
- (∀ Q Φ, Q -∗ atomic_update Eo Em α β (λ x y, Q -∗ Φ (f x y)) -∗
+ (∀ Q (Φ : val Λ → iProp Σ), Q -∗
+ atomic_update Eo ∅ α β (λ.. x y, Q -∗ Φ (f x y)) -∗
WP e {{ Φ }})%I.
(* Note: To add a private postcondition, use
- atomic_update α β Eo Em (λ x y, POST x y -∗ Φ (f x y)) *)
+ atomic_update α β Eo Ei (λ x y, POST x y -∗ Φ (f x y)) *)
+
+Notation "'<<<' ∀ x1 .. xn , α '>>>' e @ Eo '<<<' ∃ y1 .. yn , β , 'RET' v '>>>'" :=
+ (atomic_wp (TA:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
+ (TB:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
+ e%E
+ Eo
+ (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
+ λ x1, .. (λ xn, α%I) ..)
+ (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
+ λ x1, .. (λ xn,
+ tele_app (TT:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
+ (λ y1, .. (λ yn, β%I) .. )
+ ) .. )
+ (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
+ λ x1, .. (λ xn,
+ tele_app (TT:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
+ (λ y1, .. (λ yn, v%V) .. )
+ ) .. )
+ )
+ (at level 20, Eo, α, β, v at level 200, x1 binder, xn binder, y1 binder, yn binder,
+ format "'[hv' '<<<' ∀ x1 .. xn , α '>>>' '/ ' e @ Eo '/' '[ ' '<<<' ∃ y1 .. yn , β , '/' 'RET' v '>>>' ']' ']'")
+ : stdpp_scope.
+
+Notation "'<<<' ∀ x1 .. xn , α '>>>' e @ Eo '<<<' β , 'RET' v '>>>'" :=
+ (atomic_wp (TA:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
+ (TB:=TeleO)
+ e%E
+ Eo
+ (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
+ λ x1, .. (λ xn, α%I) ..)
+ (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
+ λ x1, .. (λ xn,
+ tele_app (TT:=TeleO) β%I
+ ) .. )
+ (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
+ λ x1, .. (λ xn,
+ tele_app (TT:=TeleO) v%V
+ ) .. )
+ )
+ (at level 20, Eo, α, β, v at level 200, x1 binder, xn binder,
+ format "'[hv' '<<<' ∀ x1 .. xn , α '>>>' '/ ' e @ Eo '/' '[ ' '<<<' β , '/' 'RET' v '>>>' ']' ']'")
+ : stdpp_scope.
+
+Notation "'<<<' α '>>>' e @ Eo '<<<' ∃ y1 .. yn , β , 'RET' v '>>>'" :=
+ (atomic_wp (TA:=TeleO)
+ (TB:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
+ e%E
+ Eo
+ (tele_app (TT:=TeleO) α%I)
+ (tele_app (TT:=TeleO) $
+ tele_app (TT:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
+ (λ y1, .. (λ yn, β%I) .. ))
+ (tele_app (TT:=TeleO) $
+ tele_app (TT:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
+ (λ y1, .. (λ yn, v%V) .. ))
+ )
+ (at level 20, Eo, α, β, v at level 200, y1 binder, yn binder,
+ format "'[hv' '<<<' α '>>>' '/ ' e @ Eo '/' '[ ' '<<<' ∃ y1 .. yn , β , '/' 'RET' v '>>>' ']' ']'")
+ : stdpp_scope.
+
+Notation "'<<<' α '>>>' e @ Eo '<<<' β , 'RET' v '>>>'" :=
+ (atomic_wp (TA:=TeleO)
+ (TB:=TeleO)
+ e%E
+ Eo
+ (tele_app (TT:=TeleO) α%I)
+ (tele_app (TT:=TeleO) $ tele_app (TT:=TeleO) β%I)
+ (tele_app (TT:=TeleO) $ tele_app (TT:=TeleO) v%V)
+ )
+ (at level 20, Eo, α, β, v at level 200,
+ format "'[hv' '<<<' α '>>>' '/ ' e @ Eo '/' '[ ' '<<<' β , '/' 'RET' v '>>>' ']' ']'")
+ : stdpp_scope.