From 6b0f9e9a610eea84421816e7b86e1d15cedc125a Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 26 Sep 2023 14:24:50 +0200
Subject: [PATCH] update dependencies (logatom changes)

---
 coq-iris-examples.opam                             |  2 +-
 .../locks/freeable_lock/freeable_logatom_lock.v    | 12 ++++++------
 theories/logatom/conditional_increment/cinc.v      | 12 ++++++------
 theories/logatom/conditional_increment/spec.v      |  8 ++++----
 .../logatom/counter_with_backup/counter_proof.v    | 14 +++++++-------
 .../logatom/counter_with_backup/counter_spec.v     | 14 +++++++-------
 theories/logatom/elimination_stack/hocap_spec.v    | 10 +++++-----
 theories/logatom/elimination_stack/spec.v          | 10 +++++-----
 theories/logatom/elimination_stack/stack.v         | 12 ++++++------
 theories/logatom/flat_combiner/atomic_sync.v       |  2 +-
 theories/logatom/herlihy_wing_queue/hwq.v          | 12 ++++++------
 theories/logatom/herlihy_wing_queue/spec.v         |  8 ++++----
 theories/logatom/rdcss/rdcss.v                     | 14 +++++++-------
 theories/logatom/rdcss/spec.v                      |  8 ++++----
 theories/logatom/snapshot/atomic_snapshot.v        | 12 ++++++------
 theories/logatom/snapshot/spec.v                   | 12 ++++++------
 theories/logatom/treiber.v                         | 12 ++++++------
 theories/logatom/treiber2.v                        | 10 +++++-----
 18 files changed, 92 insertions(+), 92 deletions(-)

diff --git a/coq-iris-examples.opam b/coq-iris-examples.opam
index 6faabec4..53540573 100644
--- a/coq-iris-examples.opam
+++ b/coq-iris-examples.opam
@@ -8,7 +8,7 @@ dev-repo: "git+https://gitlab.mpi-sws.org/iris/examples.git"
 synopsis: "A collection of case studies for Iris -- not meant to be used as a dependency of anything"
 
 depends: [
-  "coq-iris-heap-lang" { (= "dev.2023-09-14.3.60632dd7") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2023-09-26.0.32e79061") | (= "dev") }
   "coq-autosubst" { = "dev" }
 ]
 
diff --git a/theories/locks/freeable_lock/freeable_logatom_lock.v b/theories/locks/freeable_lock/freeable_logatom_lock.v
index e650008a..97e795fb 100644
--- a/theories/locks/freeable_lock/freeable_logatom_lock.v
+++ b/theories/locks/freeable_lock/freeable_logatom_lock.v
@@ -44,9 +44,9 @@ Section tada.
     else True.
 
   Local Definition acquire_AU γ (Q : iProp Σ) : iProp Σ :=
-    AU << ∃∃ s : state, tada_lock_state γ s >>
+    AU <{ ∃∃ s : state, tada_lock_state γ s }>
        @ ⊤ ∖ ↑N, ∅
-       << tada_lock_state γ Locked, COMM Q >>.
+       <{ tada_lock_state γ Locked, COMM Q }>.
 
   Local Instance acquire_AU_proper γ :
     NonExpansive (acquire_AU γ).
@@ -197,9 +197,9 @@ Section tada.
   Lemma acquire_tada_spec γ lk :
     tada_is_lock γ lk -∗
     £2 -∗
-    <<< ∀∀ s, tada_lock_state γ s >>>
+    <<{ ∀∀ s, tada_lock_state γ s }>>
       l.(acquire) lk @ ↑N
-    <<< tada_lock_state γ Locked, RET #() >>>.
+    <<{ tada_lock_state γ Locked | RET #() }>>.
   Proof.
     iIntros "[#Hislock #Hinv] [Hlc1 Hlc2] %Φ AU".
     iMod (register_lock_acquire with "Hinv AU") as (q) "[Hown Hloan]".
@@ -218,9 +218,9 @@ Section tada.
 
   Lemma release_tada_spec γ lk :
     tada_is_lock γ lk -∗
-    <<< tada_lock_state γ Locked >>>
+    <<{ tada_lock_state γ Locked }>>
       l.(release) lk @ ↑N
-    <<< tada_lock_state γ Free, RET #() >>>.
+    <<{ tada_lock_state γ Free | RET #() }>>.
   Proof.
     iIntros "[#Hislock _] %Φ AU". iApply fupd_wp.
     iMod "AU" as "[[Hvar1 [Hlocked Hvar2]] [_ Hclose]]".
diff --git a/theories/logatom/conditional_increment/cinc.v b/theories/logatom/conditional_increment/cinc.v
index c16e6482..4c65e63e 100644
--- a/theories/logatom/conditional_increment/cinc.v
+++ b/theories/logatom/conditional_increment/cinc.v
@@ -184,9 +184,9 @@ Section conditional_counter.
        ∨ own γ_s (Cinr $ to_agree ()) ∗ done_state Q l l_ghost_winner γ_t))%I.
 
   Local Definition cinc_au Q γs f :=
-    (AU << ∃∃ (b : bool) (n : Z), counter_content γs n ∗ f ↦_(λ _, True) #b >>
+    (AU <{ ∃∃ (b : bool) (n : Z), counter_content γs n ∗ f ↦_(λ _, True) #b }>
            @ ⊤∖(↑N ∪ ↑inv_heapN), ∅
-        << counter_content γs (if b then n + 1 else n)%Z ∗ f ↦_(λ _, True) #b, COMM Q >>)%I.
+        <{ counter_content γs (if b then n + 1 else n)%Z ∗ f ↦_(λ _, True) #b, COMM Q }>)%I.
 
   Definition counter_inv γ_n c :=
     (∃ (l : loc) (q : Qp) (s : abstract_state),
@@ -432,9 +432,9 @@ Section conditional_counter.
 
   Lemma cinc_spec γs v (f: loc) :
     is_counter γs v -∗
-    <<< ∀∀ (b : bool) (n : Z), counter_content γs n ∗ f ↦_(λ _, True) #b >>>
+    <<{ ∀∀ (b : bool) (n : Z), counter_content γs n ∗ f ↦_(λ _, True) #b }>>
         cinc v #f @ (↑N ∪ ↑inv_heapN)
-    <<< counter_content γs (if b then n + 1 else n)%Z ∗ f ↦_(λ _, True) #b, RET #() >>>.
+    <<{ counter_content γs (if b then n + 1 else n)%Z ∗ f ↦_(λ _, True) #b | RET #() }>>.
   Proof.
     iIntros "#InvC". iDestruct "InvC" as (c_l [-> ?]) "[#GC #InvC]".
     iIntros (Φ) "AU". iLöb as "IH".
@@ -515,9 +515,9 @@ Section conditional_counter.
 
   Lemma get_spec γs v :
     is_counter γs v -∗
-    <<< ∀∀ (n : Z), counter_content γs n >>>
+    <<{ ∀∀ (n : Z), counter_content γs n }>>
         get v @ (↑N ∪ ↑inv_heapN)
-    <<< counter_content γs n, RET #n >>>.
+    <<{ counter_content γs n | RET #n }>>.
   Proof.
     iIntros "#InvC" (Φ) "AU". iDestruct "InvC" as (c_l [-> ?]) "[GC InvC]".
     iLöb as "IH". wp_lam. wp_bind (! _)%E.
diff --git a/theories/logatom/conditional_increment/spec.v b/theories/logatom/conditional_increment/spec.v
index 501a3e18..15a03266 100644
--- a/theories/logatom/conditional_increment/spec.v
+++ b/theories/logatom/conditional_increment/spec.v
@@ -31,14 +31,14 @@ Record atomic_cinc {Σ} `{!heapGS Σ} := AtomicCinc {
     {{{ ctr γs, RET ctr ; is_counter N γs ctr ∗ counter_content γs 0 }}};
   cinc_spec N γs v (f : loc) :
     is_counter N γs v -∗
-    <<< ∀∀ (b : bool) (n : Z), counter_content γs n ∗ f ↦_(λ _, True) #b >>>
+    <<{ ∀∀ (b : bool) (n : Z), counter_content γs n ∗ f ↦_(λ _, True) #b }>>
         cinc v #f @ ↑N ∪ ↑inv_heapN
-    <<< counter_content γs (if b then n + 1 else n)%Z ∗ f ↦_(λ _, True) #b, RET #() >>>;
+    <<{ counter_content γs (if b then n + 1 else n)%Z ∗ f ↦_(λ _, True) #b | RET #() }>>;
   get_spec N γs v:
     is_counter N γs v -∗
-    <<< ∀∀ (n : Z), counter_content γs n >>>
+    <<{ ∀∀ (n : Z), counter_content γs n }>>
         get v @ ↑N ∪ ↑inv_heapN
-    <<< counter_content γs n, RET #n >>>;
+    <<{ counter_content γs n | RET #n }>>;
 }.
 Global Arguments atomic_cinc _ {_}.
 
diff --git a/theories/logatom/counter_with_backup/counter_proof.v b/theories/logatom/counter_with_backup/counter_proof.v
index 40c10008..7c1ec6cb 100644
--- a/theories/logatom/counter_with_backup/counter_proof.v
+++ b/theories/logatom/counter_with_backup/counter_proof.v
@@ -105,12 +105,12 @@ Section counter_proof.
 
   (** Invariant for transfer of atomic update (helping) of [get] *)
   Definition get_inv γs (γ1 γ2 : gname) (n : nat) (Φ : val → iProp Σ) : iProp Σ :=
-    ((AU << ∃∃ n: nat, value γs n >> @ ⊤ ∖ ↑N, ∅ << value γs n, COMM (Φ #n) >> ∗ ghost_var γ1 (1/2) true ∗ £ 1) ∨
+    ((AU <{ ∃∃ n: nat, value γs n }> @ ⊤ ∖ ↑N, ∅ <{ value γs n, COMM (Φ #n) }> ∗ ghost_var γ1 (1/2) true ∗ £ 1) ∨
      (ghost_var γ1 (1/2) false ∗ Φ #n) ∨ (ghost_var γ1 (1/2) false ∗ own γ2 (Excl ()))).
 
   (** Invariant for transfer of atomic update (helping) of [put] *)
   Definition put_inv γs (γ1 γ2 : gname) (n : nat) (Φ : val → iProp Σ): iProp Σ :=
-    ((AU  << ∃∃ n: nat, value γs n >> @ ⊤ ∖ ↑N, ∅ << value γs (n + 1), COMM (Φ #n) >> ∗ ghost_var γ1 (1/2) true ∗ £ 1) ∨
+    ((AU <{ ∃∃ n: nat, value γs n }> @ ⊤ ∖ ↑N, ∅ <{ value γs (n + 1), COMM (Φ #n) }> ∗ ghost_var γ1 (1/2) true ∗ £ 1) ∨
      (ghost_var γ1 (1/2) false ∗ Φ #n) ∨ (ghost_var γ1 (1/2) false ∗ own γ2 (Excl ()))).
 
   (** The part of the main counter invariant that controls execution of [put]s *)
@@ -307,7 +307,7 @@ Section counter_proof.
 
   Lemma counter_inv_inner_register_get Φ E γs γ_prim γ_get γ_put γ b p G P n_b n_p :
     n_b < n_p →
-    AU << ∃∃ n: nat, value γs n >> @ ⊤ ∖ ↑N, ∅ << value γs n, COMM (Φ #n) >> -∗
+    AU <{ ∃∃ n: nat, value γs n }> @ ⊤ ∖ ↑N, ∅ <{ value γs n, COMM (Φ #n) }> -∗
     £ 1 -∗
     n_p ↪[ γ_get ]□ γ -∗
     counter_inv_inner γs γ_prim γ_get γ_put b p G P n_b n_p ={E}=∗
@@ -348,7 +348,7 @@ Section counter_proof.
 
   Lemma counter_inv_inner_register_put Φ E γs γ_prim γ_get γ_put b p G P n_b n_p :
     n_b ≤ n_p →
-    AU << ∃∃ n: nat, value γs n >> @ ⊤ ∖ ↑N, ∅ << value γs (n + 1), COMM (Φ #n) >> -∗
+    AU <{ ∃∃ n: nat, value γs n }> @ ⊤ ∖ ↑N, ∅ <{ value γs (n + 1), COMM (Φ #n) }> -∗
     £ 1 -∗
     b ↦ #n_b -∗
     p ↦ #(S n_p) -∗
@@ -530,7 +530,7 @@ Section counter_proof.
 
   (** *** Proof of [get] *)
   Lemma get_spec γs (c : val) :
-    is_counter γs c -∗ <<< ∀∀ (n : nat), value γs n >>> (get c) @ ↑N <<< value γs n, RET #n>>>.
+    is_counter γs c -∗ <<{ ∀∀ (n : nat), value γs n }>> (get c) @ ↑N <<{ value γs n | RET #n}>>.
   Proof.
     iIntros "Counter". iIntros (Φ) "AU". destruct γs as [γ_cnt γ_ex].
     iDestruct "Counter" as (b p γ_prim γ_get γ_put) "(-> & #I)".
@@ -568,7 +568,7 @@ Section counter_proof.
 
   (** *** Proof of [get_backup] *)
   Lemma get_backup_spec γs (c: val) :
-    is_counter γs c -∗ <<< ∀∀ (n: nat), value γs n >>> (get_backup c) @ ↑N <<< value γs n, RET #n>>>.
+    is_counter γs c -∗ <<{ ∀∀ (n: nat), value γs n }>> (get_backup c) @ ↑N <<{ value γs n | RET #n}>>.
   Proof.
     iIntros "Counter". iIntros (Φ) "AU". destruct γs as [γ_cnt γ_ex].
     iDestruct "Counter" as (b p γ_prim γ_get γ_put) "(-> & #I)".
@@ -589,7 +589,7 @@ Section counter_proof.
 
   (** *** Proof of [increment] *)
   Lemma increment_spec γs (c: val) :
-    is_counter γs c -∗ <<< ∀∀ (n: nat), value γs n >>> (increment c) @ ↑N <<< value γs (n + 1), RET #n>>>.
+    is_counter γs c -∗ <<{ ∀∀ (n: nat), value γs n }>> (increment c) @ ↑N <<{ value γs (n + 1) | RET #n}>>.
   Proof.
     iIntros "Counter". iIntros (Φ) "AU". destruct γs as [γ_cnt γ_ex].
     iDestruct "Counter" as (b p γ_prim γ_get γ_put) "(-> & #I)".
diff --git a/theories/logatom/counter_with_backup/counter_spec.v b/theories/logatom/counter_with_backup/counter_spec.v
index 4ded0004..d7936969 100644
--- a/theories/logatom/counter_with_backup/counter_spec.v
+++ b/theories/logatom/counter_with_backup/counter_spec.v
@@ -24,22 +24,22 @@ Record atomic_counter {Σ} `{!heapGS Σ} := AtomicCounter {
   (* -- operation specs -- *)
   new_counter_spec N :
     {{{ True }}} new_counter #() {{{ c γs, RET c; is_counter N γs c ∗ value γs 0 }}};
-  (* the following specs are logically atomic, using logically-atomic triples <<< x. P >>> e <<< y. Q >>> *)
+  (* the following specs are logically atomic, using logically-atomic triples <<{ x. P }>> e <<{ y. Q }>> *)
   (* note that the [RET] clause _specifies_ that the return value is [n], and hence we do not need to introduce a separate binder [m] as is done in the formulation shown in the paper *)
   increment_spec N γs c :
     is_counter N γs c -∗
-    <<< ∀∀ n: nat, value γs n >>>
+    <<{ ∀∀ n: nat, value γs n }>>
       increment c @ ↑N
-    <<< value γs (n + 1), RET #n >>>;
+    <<{ value γs (n + 1) | RET #n }>>;
   get_spec N γs c :
     is_counter N γs c -∗
-    <<< ∀∀ n: nat, value γs n >>>
+    <<{ ∀∀ n: nat, value γs n }>>
       get c @ ↑N
-    <<< value γs n, RET #n >>>;
+    <<{ value γs n | RET #n }>>;
   get_backup_spec N γs c :
     is_counter N γs c -∗
-    <<< ∀∀ n: nat, value γs n >>>
+    <<{ ∀∀ n: nat, value γs n }>>
       get_backup c @ ↑N
-    <<< value γs n, RET #n >>>;
+    <<{ value γs n | RET #n }>>;
 }.
 Global Arguments atomic_counter _ {_}.
diff --git a/theories/logatom/elimination_stack/hocap_spec.v b/theories/logatom/elimination_stack/hocap_spec.v
index d476906e..b08dbe29 100644
--- a/theories/logatom/elimination_stack/hocap_spec.v
+++ b/theories/logatom/elimination_stack/hocap_spec.v
@@ -166,9 +166,9 @@ Section hocap_auth_tada.
 
   Lemma tada_push N γs s (v : val) :
     stack.(hocap_auth.is_stack) N γs s -∗
-    <<< ∀∀ l : list val, stack.(hocap_auth.stack_content_frag) γs l >>>
+    <<{ ∀∀ l : list val, stack.(hocap_auth.stack_content_frag) γs l }>>
       stack.(hocap_auth.push) s v @ ↑N
-    <<< stack.(hocap_auth.stack_content_frag) γs (v::l), RET #() >>>.
+    <<{ stack.(hocap_auth.stack_content_frag) γs (v::l) | RET #() }>>.
   Proof.
     iIntros "Hstack". iIntros (Φ) "HΦ".
     iApply (hocap_auth.push_spec with "Hstack").
@@ -181,10 +181,10 @@ Section hocap_auth_tada.
 
   Lemma tada_pop N γs (s : val) :
     stack.(hocap_auth.is_stack) N γs s -∗
-    <<< ∀∀ l : list val, stack.(hocap_auth.stack_content_frag) γs l >>>
+    <<{ ∀∀ l : list val, stack.(hocap_auth.stack_content_frag) γs l }>>
       stack.(hocap_auth.pop) s @ ↑N
-    <<< stack.(hocap_auth.stack_content_frag) γs (tail l),
-        RET match l with [] => NONEV | v :: _ => SOMEV v end >>>.
+    <<{ stack.(hocap_auth.stack_content_frag) γs (tail l)
+      | RET match l with [] => NONEV | v :: _ => SOMEV v end }>>.
   Proof.
     iIntros "Hstack". iIntros (Φ) "HΦ".
     iApply (hocap_auth.pop_spec with "Hstack").
diff --git a/theories/logatom/elimination_stack/spec.v b/theories/logatom/elimination_stack/spec.v
index 3ae43c10..063eec67 100644
--- a/theories/logatom/elimination_stack/spec.v
+++ b/theories/logatom/elimination_stack/spec.v
@@ -25,15 +25,15 @@ Record atomic_stack {Σ} `{!heapGS Σ} := AtomicStack {
     {{{ True }}} new_stack #() {{{ γs s, RET s; is_stack N γs s ∗ stack_content γs [] }}};
   push_spec N γs s (v : val) :
     is_stack N γs s -∗
-    <<< ∀∀ l : list val, stack_content γs l >>>
+    <<{ ∀∀ l : list val, stack_content γs l }>>
       push s v @ ↑N
-    <<< stack_content γs (v::l), RET #() >>>;
+    <<{ stack_content γs (v::l) | RET #() }>>;
   pop_spec N γs s :
     is_stack N γs s -∗
-    <<< ∀∀ l : list val, stack_content γs l >>>
+    <<{ ∀∀ l : list val, stack_content γs l }>>
       pop s @ ↑N
-    <<< stack_content γs (tail l),
-        RET match l with [] => NONEV | v :: _ => SOMEV v end >>>;
+    <<{ stack_content γs (tail l)
+      | RET match l with [] => NONEV | v :: _ => SOMEV v end }>>;
 }.
 Global Arguments atomic_stack _ {_}.
 
diff --git a/theories/logatom/elimination_stack/stack.v b/theories/logatom/elimination_stack/stack.v
index d48aa0bc..72bf3df9 100644
--- a/theories/logatom/elimination_stack/stack.v
+++ b/theories/logatom/elimination_stack/stack.v
@@ -142,7 +142,7 @@ Section stack.
   Local Hint Extern 0 (environments.envs_entails _ (offer_inv _ _ _ _)) => unfold offer_inv : core.
 
   Definition stack_push_au γs v Q : iProp :=
-    AU << ∃∃ l, stack_content γs l >> @ ⊤∖↑N, ∅ << stack_content γs (v::l), COMM Q >>.
+    AU <{ ∃∃ l, stack_content γs l }> @ ⊤∖↑N, ∅ <{ stack_content γs (v::l), COMM Q }>.
 
   Definition is_offer (γs : gname) (offer_rep : option (val * loc)) :=
     match offer_rep with
@@ -187,9 +187,9 @@ Section stack.
 
   Lemma push_spec γs s (v : val) :
     is_stack γs s -∗
-    <<< ∀∀ l : list val, stack_content γs l >>>
+    <<{ ∀∀ l : list val, stack_content γs l }>>
       push s v @ ↑N
-    <<< stack_content γs (v::l), RET #() >>>.
+    <<{ stack_content γs (v::l) | RET #() }>>.
   Proof.
     iIntros "#Hinv". iIntros (Φ) "AU".
     iDestruct "Hinv" as (head offer) "[% #Hinv]". subst s.
@@ -270,10 +270,10 @@ Section stack.
 
   Lemma pop_spec γs (s : val) :
     is_stack γs s -∗
-    <<< ∀∀ l, stack_content γs l >>>
+    <<{ ∀∀ l, stack_content γs l }>>
       pop s @ ↑N
-    <<< stack_content γs (tail l),
-        RET match l with [] => NONEV | v :: _ => SOMEV v end >>>.
+    <<{ stack_content γs (tail l)
+      | RET match l with [] => NONEV | v :: _ => SOMEV v end }>>.
   Proof.
     iIntros "#Hinv". iIntros (Φ) "AU".
     iDestruct "Hinv" as (head offer) "[% #Hinv]". subst s.
diff --git a/theories/logatom/flat_combiner/atomic_sync.v b/theories/logatom/flat_combiner/atomic_sync.v
index 8b423c72..d67e510c 100644
--- a/theories/logatom/flat_combiner/atomic_sync.v
+++ b/theories/logatom/flat_combiner/atomic_sync.v
@@ -29,7 +29,7 @@ Section atomic_sync.
   (* TODO: Provide better masks. ∅ as inner mask is pretty weak. *)
   Definition atomic_synced (ϕ: A → iProp Σ) γ (f f': val) :=
     (□ ∀ α β (x: val), atomic_seq_spec ϕ α β f x →
-       <<< ∀∀ g, gHalf γ g ∗ □ α g >>> f' x @ ∅ <<< ∃∃ v g', gHalf γ g' ∗ β g g' v, RET v >>>)%I.
+       <<{ ∀∀ g, gHalf γ g ∗ □ α g }>> f' x @ ∅ <<{ ∃∃ v g', gHalf γ g' ∗ β g g' v | RET v }>>)%I.
 
   (* TODO: Use our usual style with a generic post-condition. *)
   (* TODO: We could get rid of the x, and hard-code a unit. That would
diff --git a/theories/logatom/herlihy_wing_queue/hwq.v b/theories/logatom/herlihy_wing_queue/hwq.v
index caee2fbc..3b463cdb 100644
--- a/theories/logatom/herlihy_wing_queue/hwq.v
+++ b/theories/logatom/herlihy_wing_queue/hwq.v
@@ -1208,8 +1208,8 @@ Qed.
 
 (** Atomic update for the insertion of [l], with post-condition [Q]. *)
 Definition enqueue_AU γe l Q :=
-  (AU << ∃∃ ls : list loc, hwq_cont γe ls >> @ ⊤ ∖ ↑N, ∅
-      << hwq_cont γe (ls ++ [l]), COMM Q >>)%I.
+  (AU <{ ∃∃ ls : list loc, hwq_cont γe ls }> @ ⊤ ∖ ↑N, ∅
+      <{ hwq_cont γe (ls ++ [l]), COMM Q }>)%I.
 
 (*
 When a contradiction is going on, we have [cont = WithCont i1 i2] where:
@@ -1528,9 +1528,9 @@ Qed.
 
 Lemma enqueue_spec sz γe (q : val) (l : loc) :
   is_hwq sz γe q -∗
-  <<< ∀∀ (ls : list loc), hwq_cont γe ls >>>
+  <<{ ∀∀ (ls : list loc), hwq_cont γe ls }>>
     enqueue q #l @ ↑N
-  <<< hwq_cont γe (ls ++ [l]), RET #() >>>.
+  <<{ hwq_cont γe (ls ++ [l]) | RET #() }>>.
 Proof.
   iIntros "Hq" (Φ) "AU".
   iDestruct "Hq" as (γb γi γc γs ℓ_ar ℓ_back p ->) "#Inv".
@@ -2497,9 +2497,9 @@ Qed.
 
 Lemma dequeue_spec sz γe (q : val) :
   is_hwq sz γe q -∗
-  <<< ∀∀ (ls : list loc), hwq_cont γe ls >>>
+  <<{ ∀∀ (ls : list loc), hwq_cont γe ls }>>
     dequeue q @ ↑N
-  <<< ∃∃ (l : loc) ls', ⌜ls = l :: ls'⌝ ∗ hwq_cont γe ls', RET #l >>>.
+  <<{ ∃∃ (l : loc) ls', ⌜ls = l :: ls'⌝ ∗ hwq_cont γe ls' | RET #l }>>.
 Proof.
   iIntros "Hq" (Φ) "AU". iLöb as "IH".
   iDestruct "Hq" as (γb γi γc γs ℓ_ar ℓ_back p ->) "#Inv".
diff --git a/theories/logatom/herlihy_wing_queue/spec.v b/theories/logatom/herlihy_wing_queue/spec.v
index ec760f43..88cbb80f 100644
--- a/theories/logatom/herlihy_wing_queue/spec.v
+++ b/theories/logatom/herlihy_wing_queue/spec.v
@@ -28,14 +28,14 @@ Record atomic_hwq {Σ} `{!heapGS Σ} := AtomicHWQ {
     {{{ v γ, RET v; is_hwq N sz γ v ∗ hwq_content γ [] }}};
   enqueue_spec N (sz : nat) (γ : name) (q : val) (l : loc) :
     is_hwq N sz γ q -∗
-    <<< ∀∀ (ls : list loc), hwq_content γ ls >>>
+    <<{ ∀∀ (ls : list loc), hwq_content γ ls }>>
       enqueue q #l @ ↑N
-    <<< hwq_content γ (ls ++ [l]), RET #() >>>;
+    <<{ hwq_content γ (ls ++ [l]) | RET #() }>>;
   dequeue_spec N (sz : nat) (γ : name) (q : val) :
     is_hwq N sz γ q -∗
-    <<< ∀∀ (ls : list loc), hwq_content γ ls >>>
+    <<{ ∀∀ (ls : list loc), hwq_content γ ls }>>
       dequeue q @ ↑N
-    <<< ∃∃ (l : loc) ls', ⌜ls = l :: ls'⌝ ∗ hwq_content γ ls', RET #l >>>;
+    <<{ ∃∃ (l : loc) ls', ⌜ls = l :: ls'⌝ ∗ hwq_content γ ls' | RET #l }>>;
 }.
 Global Arguments atomic_hwq _ {_}.
 
diff --git a/theories/logatom/rdcss/rdcss.v b/theories/logatom/rdcss/rdcss.v
index 4050d8bc..f18b0726 100644
--- a/theories/logatom/rdcss/rdcss.v
+++ b/theories/logatom/rdcss/rdcss.v
@@ -285,10 +285,10 @@ Section rdcss.
   Local Hint Extern 0 (environments.envs_entails _ (descr_inv _ _ _ _ _ _ _ _ _ _)) => unfold descr_inv : core.
 
   Definition rdcss_au Q l_n l_m m1 n1 n2 :=
-    (AU << ∃∃ (m n : val), (l_m ↦_(λ _, True) m) ∗ rdcss_state l_n n >>
+    (AU <{ ∃∃ (m n : val), (l_m ↦_(λ _, True) m) ∗ rdcss_state l_n n }>
          @ ⊤∖(↑N ∪ ↑inv_heapN), ∅
-        << (l_m ↦_(λ _, True) m) ∗ (rdcss_state l_n (if (decide ((m = m1) ∧ (n = n1))) then n2 else n)),
-           COMM Q n >>)%I.
+        <{ (l_m ↦_(λ _, True) m) ∗ (rdcss_state l_n (if (decide ((m = m1) ∧ (n = n1))) then n2 else n)),
+           COMM Q n }>)%I.
 
   Definition rdcss_inv l_n :=
     (∃ (s : abstract_state),
@@ -556,9 +556,9 @@ Section rdcss.
     val_is_unboxed m1 →
     val_is_unboxed (InjLV n1) →
     is_rdcss l_n -∗
-    <<< ∀∀ (m n: val), l_m ↦_(λ _, True) m ∗ rdcss_state l_n n >>>
+    <<{ ∀∀ (m n: val), l_m ↦_(λ _, True) m ∗ rdcss_state l_n n }>>
         rdcss #l_m #l_n m1 n1 n2 @ ↑N ∪ ↑inv_heapN
-    <<< l_m ↦_(λ _, True) m ∗ rdcss_state l_n (if decide (m = m1 ∧ n = n1) then n2 else n), RET n >>>.
+    <<{ l_m ↦_(λ _, True) m ∗ rdcss_state l_n (if decide (m = m1 ∧ n = n1) then n2 else n) | RET n }>>.
   Proof.
     iIntros (Hm1_unbox Hn1_unbox) "(#InvR & #InvGC & %)". iIntros (Φ) "AU".
     (* allocate fresh descriptor *)
@@ -654,9 +654,9 @@ Section rdcss.
   (** ** Proof of [get] *)
   Lemma get_spec l_n :
     is_rdcss l_n -∗
-    <<< ∀∀ (n : val), rdcss_state l_n n >>>
+    <<{ ∀∀ (n : val), rdcss_state l_n n }>>
         get #l_n @↑N
-    <<< rdcss_state l_n n, RET n >>>.
+    <<{ rdcss_state l_n n | RET n }>>.
   Proof.
     iIntros "(#InvR & #InvGC & %)" (Φ) "AU". iLöb as "IH".
     wp_lam. wp_bind (! _)%E. iInv rdcssN as (s) "(>Hln & Hrest)". wp_load.
diff --git a/theories/logatom/rdcss/spec.v b/theories/logatom/rdcss/spec.v
index ddb035bf..587ad42a 100644
--- a/theories/logatom/rdcss/spec.v
+++ b/theories/logatom/rdcss/spec.v
@@ -37,14 +37,14 @@ Record atomic_rdcss {Σ} `{!heapGS Σ} := AtomicRdcss {
     val_is_unboxed m1 →
     val_is_unboxed (InjLV n1) →
     is_rdcss N l_n -∗
-    <<< ∀∀ (m n: val), l_m ↦_(λ _, True) m ∗ rdcss_state N l_n n >>>
+    <<{ ∀∀ (m n: val), l_m ↦_(λ _, True) m ∗ rdcss_state N l_n n }>>
         rdcss #l_m #l_n m1 n1 n2 @ ↑N ∪ ↑inv_heapN
-    <<< l_m ↦_(λ _, True) m ∗ rdcss_state N l_n (if decide (m = m1 ∧ n = n1) then n2 else n), RET n >>>;
+    <<{ l_m ↦_(λ _, True) m ∗ rdcss_state N l_n (if decide (m = m1 ∧ n = n1) then n2 else n) | RET n }>>;
   get_spec N (l_n : loc):
     is_rdcss N l_n -∗
-    <<< ∀∀ (n : val), rdcss_state N l_n n >>>
+    <<{ ∀∀ (n : val), rdcss_state N l_n n }>>
         get #l_n @ ↑N
-    <<< rdcss_state N l_n n, RET n >>>;
+    <<{ rdcss_state N l_n n | RET n }>>;
 }.
 Global Arguments atomic_rdcss _ {_}.
 
diff --git a/theories/logatom/snapshot/atomic_snapshot.v b/theories/logatom/snapshot/atomic_snapshot.v
index 9152f90d..e9d22924 100644
--- a/theories/logatom/snapshot/atomic_snapshot.v
+++ b/theories/logatom/snapshot/atomic_snapshot.v
@@ -208,9 +208,9 @@ Section atomic_snapshot.
 
   Lemma write_spec γ (x2: val) p :
       is_snapshot γ p  -∗
-      <<< ∀∀ x : val, snapshot_content γ x >>>
+      <<{ ∀∀ x : val, snapshot_content γ x }>>
         write p x2 @ ↑N
-      <<< snapshot_content γ x2, RET #() >>>.
+      <<{ snapshot_content γ x2 | RET #() }>>.
   Proof.
     iIntros "Hx". iIntros (Φ) "AU". iLöb as "IH".
     iDestruct "Hx" as (l1 ->) "#Hinv". wp_pures. wp_lam. wp_pures.
@@ -267,9 +267,9 @@ Section atomic_snapshot.
 
   Lemma read_spec γ p :
     is_snapshot γ p -∗
-    <<< ∀∀ v : val, snapshot_content γ v >>>
+    <<{ ∀∀ v : val, snapshot_content γ v }>>
       read p @ ↑N
-    <<< snapshot_content γ v, RET v >>>.
+    <<{ snapshot_content γ v | RET v }>>.
   Proof.
     iIntros "Hx". iIntros (Φ) "AU".
     iDestruct "Hx" as (l1 ->) "#Hinv".
@@ -295,9 +295,9 @@ Section atomic_snapshot.
 
   Lemma read_with_spec γ p (l : loc) :
     is_snapshot γ p -∗
-    <<< ∀∀ v1 v2 : val, snapshot_content γ v1 ∗ l ↦ v2 >>>
+    <<{ ∀∀ v1 v2 : val, snapshot_content γ v1 ∗ l ↦ v2 }>>
        read_with_proph p #l @ ↑N
-    <<< snapshot_content γ v1 ∗ l ↦ v2, RET (v1, v2) >>>.
+    <<{ snapshot_content γ v1 ∗ l ↦ v2 | RET (v1, v2) }>>.
   Proof.
     iIntros "Hx". iIntros (Φ) "AU". iLöb as "IH". wp_lam. wp_pures.
     (* ************ new prophecy ********** *)
diff --git a/theories/logatom/snapshot/spec.v b/theories/logatom/snapshot/spec.v
index 1f11f61d..6f8f64cd 100644
--- a/theories/logatom/snapshot/spec.v
+++ b/theories/logatom/snapshot/spec.v
@@ -27,19 +27,19 @@ Record atomic_snapshot {Σ} `{!heapGS Σ} := AtomicSnapshot {
       {{{ True }}} new_snapshot v {{{ γ p, RET p; is_snapshot N γ p ∗ snapshot_content γ v }}};
     read_spec N γ p :
       is_snapshot N γ p -∗
-      <<< ∀∀ v : val, snapshot_content γ v  >>>
+      <<{ ∀∀ v : val, snapshot_content γ v  }>>
         read p @ ↑N
-      <<< snapshot_content γ v, RET v >>>;
+      <<{ snapshot_content γ v | RET v }>>;
     write_spec N γ (v: val) p :
       is_snapshot N γ p -∗
-      <<< ∀∀ w : val, snapshot_content γ w  >>>
+      <<{ ∀∀ w : val, snapshot_content γ w  }>>
         write p v @ ↑N
-      <<< snapshot_content γ v, RET #() >>>;
+      <<{ snapshot_content γ v | RET #() }>>;
     read_with_spec N γ p (l : loc) :
       is_snapshot N γ p -∗
-      <<< ∀∀ v w : val, snapshot_content γ v ∗ l ↦ w >>>
+      <<{ ∀∀ v w : val, snapshot_content γ v ∗ l ↦ w }>>
         read_with p #l @ ↑N
-      <<< snapshot_content γ v ∗ l ↦ w, RET (v, w) >>>;
+      <<{ snapshot_content γ v ∗ l ↦ w | RET (v, w) }>>;
 }.
 Global Arguments atomic_snapshot _ {_}.
 
diff --git a/theories/logatom/treiber.v b/theories/logatom/treiber.v
index 44060156..5e2d9e3a 100644
--- a/theories/logatom/treiber.v
+++ b/theories/logatom/treiber.v
@@ -83,9 +83,9 @@ Section proof.
   Qed.
 
   Lemma push_atomic_spec (s: loc) (x: val) :
-    ⊢ <<< ∀∀ (xs : list val), is_stack s xs >>>
+    ⊢ <<{ ∀∀ (xs : list val), is_stack s xs }>>
         push #s x @ ∅
-      <<< is_stack s (x::xs), RET #() >>>.
+      <<{ is_stack s (x::xs) | RET #() }>>.
   Proof.
     unfold is_stack.
     iIntros (Φ) "HP". iLöb as "IH". wp_rec.
@@ -110,11 +110,11 @@ Section proof.
   Qed.
 
   Lemma pop_atomic_spec (s: loc) :
-    ⊢ <<< ∀∀ (xs : list val), is_stack s xs >>>
+    ⊢ <<{ ∀∀ (xs : list val), is_stack s xs }>>
         pop #s @ ∅
-      <<< match xs with [] => is_stack s []
-                  | x::xs' => is_stack s xs' end,
-      RET match xs with [] => NONEV | x :: _ => SOMEV x end >>>.
+      <<{ match xs with [] => is_stack s []
+                  | x::xs' => is_stack s xs' end
+        | RET match xs with [] => NONEV | x :: _ => SOMEV x end }>>.
   Proof.
     unfold is_stack.
     iIntros (Φ) "HP". iLöb as "IH". wp_rec.
diff --git a/theories/logatom/treiber2.v b/theories/logatom/treiber2.v
index d67cd99a..d383d96e 100644
--- a/theories/logatom/treiber2.v
+++ b/theories/logatom/treiber2.v
@@ -238,9 +238,9 @@ Qed.
     the possibility of accessing the precondition again, unlike with abort. *)
 Lemma push_stack_spec (ℓ : loc) (γ : gname) (v : val) :
   is_stack ℓ γ -∗
-  <<< ∀∀ (xs : list val), stack_cont γ xs >>>
+  <<{ ∀∀ (xs : list val), stack_cont γ xs }>>
     push_stack v #ℓ @ ↑N
-  <<< stack_cont γ (v :: xs) , RET #() >>>.
+  <<{ stack_cont γ (v :: xs)  | RET #() }>>.
 Proof.
   (* Introduce things into the Coq and Iris contexts, and use induction. *)
   iIntros "#HInv" (Φ) "AU". iLöb as "IH".
@@ -290,10 +290,10 @@ Qed.
     the postcondition also depends on the emptiness of the stack. *)
 Lemma pop_stack_spec (ℓ : loc) (γ : gname) :
   is_stack ℓ γ -∗
-  <<< ∀∀ (xs : list val), stack_cont γ xs >>>
+  <<{ ∀∀ (xs : list val), stack_cont γ xs }>>
     pop_stack #ℓ @ ↑N
-  <<< stack_cont γ (match xs with [] => [] | _::xs => xs end)
-    , RET (match xs with [] => NONEV | v::_ => SOMEV v end) >>>.
+  <<{ stack_cont γ (match xs with [] => [] | _::xs => xs end)
+    | RET (match xs with [] => NONEV | v::_ => SOMEV v end) }>>.
 Proof.
   (* As for [push_stack], we need to use induction and the focus on a load. *)
   iIntros "#HInv" (Φ) "AU". iLöb as "IH". wp_lam. wp_bind (! _)%E.
-- 
GitLab