From 934f529d9c36f4cbb7b03d016bf154bf77eee20d Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 26 Jul 2023 13:42:28 +0200
Subject: [PATCH] atomic: make no-private-post notation consistent with
 private-post notation

---
 iris/program_logic/atomic.v       | 71 ++++++++++++++++++++++++-------
 iris_heap_lang/lib/atomic_heap.v  | 22 +++++-----
 iris_heap_lang/lib/increment.v    |  9 ++--
 iris_heap_lang/lib/logatom_lock.v |  4 +-
 tests/atomic.ref                  | 37 +++++++++-------
 tests/atomic.v                    | 26 +++++------
 6 files changed, 108 insertions(+), 61 deletions(-)

diff --git a/iris/program_logic/atomic.v b/iris/program_logic/atomic.v
index ed2e65f0b..fc581240e 100644
--- a/iris/program_logic/atomic.v
+++ b/iris/program_logic/atomic.v
@@ -1,3 +1,47 @@
+(** This file declares notation for logically atomic Hoare triples, and some
+generic lemmas about them. To enable the definition of a shared theory applying
+to triples with any number of binders, the triples themselves are defined via telescopes, but as a user
+you need not be concerned with that. You can just use the following notation:
+
+  <<< ∀∀ x, atomic_precondition >>>
+    code @ E
+  <<< ∃∃ y, atomic_postcondition >>>
+  {{{ z, RET return_value; private_postcondition }}}
+
+Here, [x] (which can be any number of binders, including 0) is bound in all of
+the atomic pre- and postcondition and the private (non-atomic) postcondition and
+the return value, [y] (which can be any number of binders, including 0) is bound
+in both postconditions and the return value, and [z] (which can be any number of
+binders, including 0) is bound in the return value and the private
+postcondition.
+
+Note that atomic triples are *not* implicitly persistent, unlike Texan triples.
+If you need a private (non-atomic) precondition, you can use a magic wand:
+
+  private_precondition -∗
+  <<< ∀∀ x, atomic_precondition >>>
+    code @ E
+  <<< ∃∃ y, atomic_postcondition >>>
+  {{{ z, RET return_value; private_postcondition }}}
+
+If you don't need a private postcondition, you can leave it away, e.g.:
+
+  <<< ∀∀ x, atomic_precondition >>>
+    code @ E
+  <<< ∃∃ y, atomic_postcondition >>>
+  {{{ RET return_value }}}
+
+Note that due to combinatorial explosion and because Coq does not have a
+facility to declare such notation in a compositional way, not *all* variants of
+this notation exist: if you have binders before the [RET] (which is very
+uncommon), you must have a private postcondition (it can be [True]), and you
+must have [∀∀] and [∃∃] binders (they can be [_unused: ()]).
+
+For an example for how to prove and use logically atomic specifications, see
+[iris_heap_lang/lib/increment.v].
+
+*)
+
 From stdpp Require Import namespaces.
 From iris.bi Require Import telescopes.
 From iris.bi.lib Require Export atomic.
@@ -11,7 +55,6 @@ example where we want it to be anything else. *)
 Definition atomic_wp `{!irisGS_gen hlc Λ Σ} {TA TB TP : tele}
   (e: expr Λ) (* expression *)
   (E : coPset) (* *implementation* mask *)
-  (* no non-atomic preconditiopn, just use [PRE -∗ atomic_wp] for that *)
   (α: TA → iProp Σ) (* atomic pre-condition *)
   (β: TA → TB → iProp Σ) (* atomic post-condition *)
   (POST: TA → TB → TP → option (iProp Σ)) (* non-atomic post-condition *)
@@ -56,13 +99,9 @@ Notation "'<<<' ∀∀ x1 .. xn , α '>>>' e @ E '<<<' ∃∃ y1 .. yn , β '>>>
 - with and without RET binders
 - with and without POST
 
-The variants with RET binders but without POST are unlikely to be useful (no
-predicate can constrain the values that are bound in RET then). But that still
-leaves 12 variants. To keep our sanity we don't have them all here. Please ping
-us if you need another variant.
-
-Also, for historic reasons the no-POST notations have the RET inside the private
-postcondition angle brackets, rather than a separate set of curly braces. *)
+However we don't support the case where RET binders are present but anything
+else is missing. Below we declare the 8 notations that involve no RET binders.
+*)
 
 (* No RET binders *)
 Notation "'<<<' ∀∀ x1 .. xn , α '>>>' e @ E '<<<' ∃∃ y1 .. yn , β '>>>' '{{{' 'RET' v ; POST } } }" :=
@@ -139,7 +178,7 @@ Notation "'<<<' α '>>>' e @ E '<<<' β '>>>' '{{{' 'RET' v ; POST } } }" :=
   : bi_scope.
 
 (* No RET binders, no POST *)
-Notation "'<<<' ∀∀ x1 .. xn , α '>>>' e @ E '<<<' ∃∃ y1 .. yn , β , 'RET' v '>>>'" :=
+Notation "'<<<' ∀∀ x1 .. xn , α '>>>' e @ E '<<<' ∃∃ y1 .. yn , β '>>>' '{{{' 'RET' v } } }" :=
   (atomic_wp (TA:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
              (TB:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
              (TP:=TeleO)
@@ -157,11 +196,11 @@ Notation "'<<<' ∀∀ x1 .. xn , α '>>>' e @ E '<<<' ∃∃ y1 .. yn , β , 'R
                         ) .. )
   )
   (at level 20, E, α, β, v at level 200, x1 binder, xn binder, y1 binder, yn binder,
-   format "'[hv' '<<<'  '[' ∀∀  x1  ..  xn ,  '/' α  ']' '>>>'  '/  ' e  @  E  '/' '<<<'  '[' ∃∃  y1  ..  yn ,  '/' β ,  '/' 'RET'  v  ']' '>>>' ']'")
+   format "'[hv' '<<<'  '[' ∀∀  x1  ..  xn ,  '/' α  ']' '>>>'  '/  ' e  @  E  '/' '<<<'  '[' ∃∃  y1  ..  yn ,  '/' β  ']' '>>>'  '/' {{{  '[' RET  v  ']' } } } ']'")
   : bi_scope.
 
 (* No ∃∃ binders, no RET binders, no POST *)
-Notation "'<<<' ∀∀ x1 .. xn , α '>>>' e @ E '<<<' β , 'RET' v '>>>'" :=
+Notation "'<<<' ∀∀ x1 .. xn , α '>>>' e @ E '<<<' β '>>>' '{{{' 'RET' v } } }" :=
   (atomic_wp (TA:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
              (TB:=TeleO)
              (TP:=TeleO)
@@ -173,11 +212,11 @@ Notation "'<<<' ∀∀ x1 .. xn , α '>>>' e @ E '<<<' β , 'RET' v '>>>'" :=
              (tele_app $ λ x1, .. (λ xn, tele_app $ tele_app v%V) .. )
   )
   (at level 20, E, α, β, v at level 200, x1 binder, xn binder,
-   format "'[hv' '<<<'  '[' ∀∀  x1  ..  xn ,  '/' α  ']' '>>>'  '/  ' e  @  E  '/' '<<<'  '[' β ,  '/' 'RET'  v  ']' '>>>' ']'")
+   format "'[hv' '<<<'  '[' ∀∀  x1  ..  xn ,  '/' α  ']' '>>>'  '/  ' e  @  E  '/' '<<<'  '[' β  ']' '>>>'  '/' {{{  '[' RET  v  ']' } } } ']'")
   : bi_scope.
 
 (* No ∀∀ binders, no RET binders, no POST *)
-Notation "'<<<' α '>>>' e @ E '<<<' ∃∃ y1 .. yn , β , 'RET' v '>>>'" :=
+Notation "'<<<' α '>>>' e @ E '<<<' ∃∃ y1 .. yn , β '>>>' '{{{' 'RET' v } } }" :=
   (atomic_wp (TA:=TeleO)
              (TB:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
              (TP:=TeleO)
@@ -189,11 +228,11 @@ Notation "'<<<' α '>>>' e @ E '<<<' ∃∃ y1 .. yn , β , 'RET' v '>>>'" :=
              (tele_app $ tele_app $ λ y1, .. (λ yn, tele_app v%V) .. )
   )
   (at level 20, E, α, β, v at level 200, y1 binder, yn binder,
-   format "'[hv' '<<<'  '[' α  ']' '>>>'  '/  ' e  @  E  '/' '<<<'  '[' ∃∃  y1  ..  yn ,  '/' β ,  '/' 'RET'  v  ']' '>>>' ']'")
+   format "'[hv' '<<<'  '[' α  ']' '>>>'  '/  ' e  @  E  '/' '<<<'  '[' ∃∃  y1  ..  yn ,  '/' β  ']' '>>>'  '/' {{{  '[' RET  v  ']' } } } ']'")
   : bi_scope.
 
 (* No ∀∀ binders, no ∃∃ binders, no RET binders, no POST *)
-Notation "'<<<' α '>>>' e @ E '<<<' β , 'RET' v '>>>'" :=
+Notation "'<<<' α '>>>' e @ E '<<<' β '>>>' '{{{' 'RET' v } } }" :=
   (atomic_wp (TA:=TeleO)
              (TB:=TeleO)
              (TP:=TeleO)
@@ -205,7 +244,7 @@ Notation "'<<<' α '>>>' e @ E '<<<' β , 'RET' v '>>>'" :=
              (tele_app $ tele_app $ tele_app v%V)
   )
   (at level 20, E, α, β, v at level 200,
-   format "'[hv' '<<<'  '[' α  ']' '>>>'  '/  ' e  @  E  '/' '<<<'  '[' β ,  '/' 'RET'  v  ']' '>>>' ']'")
+   format "'[hv' '<<<'  '[' α  ']' '>>>'  '/  ' e  @  E  '/' '<<<'  '[' β  ']' '>>>'  '/' {{{  '[' RET  v  ']' } } } ']'")
   : bi_scope.
 
 (** Theory *)
diff --git a/iris_heap_lang/lib/atomic_heap.v b/iris_heap_lang/lib/atomic_heap.v
index b356f550a..4dd9e52a3 100644
--- a/iris_heap_lang/lib/atomic_heap.v
+++ b/iris_heap_lang/lib/atomic_heap.v
@@ -56,10 +56,10 @@ Class atomic_heap := AtomicHeap {
   free_spec `{!heapGS_gen hlc Σ} {H : atomic_heapGS Σ} (l : loc) (v : val) :
     {{{ mapsto (H:=H) l (DfracOwn 1) v }}} free #l {{{ l, RET #l; True }}};
   load_spec `{!heapGS_gen hlc Σ} {H : atomic_heapGS Σ} (l : loc) :
-    ⊢ <<< ∀∀ (v : val) q, mapsto (H:=H) l q v >>> load #l @ ∅ <<< mapsto (H:=H) l q v, RET v >>>;
+    ⊢ <<< ∀∀ (v : val) q, mapsto (H:=H) l q v >>> load #l @ ∅ <<< mapsto (H:=H) l q v >>> {{{ RET v }}};
   store_spec `{!heapGS_gen hlc Σ} {H : atomic_heapGS Σ} (l : loc) (w : val) :
     ⊢ <<< ∀∀ v, mapsto (H:=H) l (DfracOwn 1) v >>> store #l w @ ∅
-      <<< mapsto (H:=H) l (DfracOwn 1) w, RET #() >>>;
+      <<< mapsto (H:=H) l (DfracOwn 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
@@ -70,8 +70,8 @@ Class atomic_heap := AtomicHeap {
     val_is_unboxed w1 →
     ⊢ <<< ∀∀ v, mapsto (H:=H) l (DfracOwn 1) v >>> cmpxchg #l w1 w2 @ ∅
       <<< if decide (v = w1)
-          then mapsto (H:=H) l (DfracOwn 1) w2 else mapsto (H:=H) l (DfracOwn 1) v,
-        RET (v, #if decide (v = w1) then true else false) >>>;
+          then mapsto (H:=H) l (DfracOwn 1) w2 else mapsto (H:=H) l (DfracOwn 1) v >>>
+      {{{ RET (v, #if decide (v = w1) then true else false) }}};
 }.
 
 Global Arguments alloc : simpl never.
@@ -115,8 +115,8 @@ Section derived.
     ⊢ <<< ∀∀ v, mapsto l (DfracOwn 1) v >>>
       CAS #l w1 w2 @ ∅
     <<< if decide (v = w1)
-        then mapsto l (DfracOwn 1) w2 else mapsto l (DfracOwn 1) v,
-      RET #if decide (v = w1) then true else false >>>.
+        then mapsto l (DfracOwn 1) w2 else mapsto l (DfracOwn 1) v >>>
+    {{{ RET #if decide (v = w1) then true else false }}}.
   Proof.
     iIntros (? Φ) "AU". awp_apply cmpxchg_spec; first done.
     iApply (aacc_aupd_commit with "AU"); first done.
@@ -127,7 +127,7 @@ Section derived.
   Lemma faa_spec (l : loc) (i2 : Z) :
     ⊢ <<< ∀∀ i1 : Z, mapsto l (DfracOwn 1) #i1 >>>
       FAA #l #i2 @ ∅
-    <<< mapsto l (DfracOwn 1) #(i1 + i2), RET #i1 >>>.
+    <<< mapsto l (DfracOwn 1) #(i1 + i2) >>> {{{ RET #i1 }}}.
   Proof.
     iIntros (Φ) "AU". rewrite /faa_atomic. iLöb as "IH".
     wp_pures. awp_apply load_spec.
@@ -175,7 +175,7 @@ Section proof.
 
   Lemma primitive_load_spec (l : loc) :
     ⊢ <<< ∀∀ (v : val) q, l ↦{q} v >>> primitive_load #l @ ∅
-    <<< l ↦{q} v, RET v >>>.
+      <<< l ↦{q} v >>> {{{ RET v }}}.
   Proof.
     iIntros (Φ) "AU". wp_lam.
     iMod "AU" as (v q) "[H↦ [_ Hclose]]".
@@ -184,7 +184,7 @@ Section proof.
 
   Lemma primitive_store_spec (l : loc) (w : val) :
     ⊢ <<< ∀∀ v, l ↦ v >>> primitive_store #l w @ ∅
-    <<< l ↦ w, RET #() >>>.
+      <<< l ↦ w >>> {{{ RET #() }}}.
   Proof.
     iIntros (Φ) "AU". wp_lam. wp_let.
     iMod "AU" as (v) "[H↦ [_ Hclose]]".
@@ -195,8 +195,8 @@ Section proof.
     val_is_unboxed w1 →
     ⊢ <<< ∀∀ (v : val), l ↦ v >>>
       primitive_cmpxchg #l w1 w2 @ ∅
-    <<< if decide (v = w1) then l ↦ w2 else l ↦ v,
-        RET (v, #if decide (v = w1) then true else false) >>>.
+    <<< if decide (v = w1) then l ↦ w2 else l ↦ v >>>
+    {{{ RET (v, #if decide (v = w1) then true else false) }}}.
   Proof.
     iIntros (? Φ) "AU". wp_lam. wp_pures.
     iMod "AU" as (v) "[H↦ [_ Hclose]]".
diff --git a/iris_heap_lang/lib/increment.v b/iris_heap_lang/lib/increment.v
index b8c82febf..23bc96c7b 100644
--- a/iris_heap_lang/lib/increment.v
+++ b/iris_heap_lang/lib/increment.v
@@ -21,7 +21,7 @@ Section increment_physical.
          else "incr" "l".
 
   Lemma incr_phy_spec (l: loc) :
-    ⊢ <<< ∀∀ (v : Z), l ↦ #v >>> incr_phy #l @ ∅ <<< l ↦ #(v + 1), RET #v >>>.
+    ⊢ <<< ∀∀ (v : Z), l ↦ #v >>> incr_phy #l @ ∅ <<< l ↦ #(v + 1) >>> {{{ RET #v }}}.
   Proof.
     iIntros (Φ) "AU". iLöb as "IH". wp_lam.
     wp_bind (!_)%E. iMod "AU" as (v) "[Hl [Hclose _]]".
@@ -54,7 +54,7 @@ Section increment.
   (** A proof of the incr specification that unfolds the definition of atomic
       accessors.  This is the style that most logically atomic proofs take. *)
   Lemma incr_spec_direct (l: loc) :
-    ⊢ <<< ∀∀ (v : Z), l ↦ #v >>> incr #l @ ∅ <<< l ↦ #(v + 1), RET #v >>>.
+    ⊢ <<< ∀∀ (v : Z), l ↦ #v >>> incr #l @ ∅ <<< l ↦ #(v + 1) >>> {{{ RET #v }}}.
   Proof.
     iIntros (Φ) "AU". iLöb as "IH". wp_lam.
     awp_apply load_spec.
@@ -93,7 +93,7 @@ Section increment.
       prove are in 1:1 correspondence; most logically atomic proofs will not be
       able to use them. *)
   Lemma incr_spec (l: loc) :
-    ⊢ <<< ∀∀ (v : Z), l ↦ #v >>> incr #l @ ∅ <<< l ↦ #(v + 1), RET #v >>>.
+    ⊢ <<< ∀∀ (v : Z), l ↦ #v >>> incr #l @ ∅ <<< l ↦ #(v + 1) >>> {{{ RET #v }}}.
   Proof.
     iIntros (Φ) "AU". iLöb as "IH". wp_lam.
     awp_apply load_spec.
@@ -129,7 +129,8 @@ Section increment.
     l ↦{#1/2} #v -∗
     <<< ∀∀ (v' : Z), l ↦{#1/2} #v' >>>
       weak_incr #l @ ∅
-    <<< ⌜v = v'⌝ ∗ l ↦ #(v + 1), RET #v >>>.
+    <<< ⌜v = v'⌝ ∗ l ↦ #(v + 1) >>>
+    {{{ RET #v }}}.
   Proof.
     iIntros "Hl" (Φ) "AU". wp_lam.
     wp_apply (atomic_wp_seq $! (load_spec _) with "Hl") as "Hl".
diff --git a/iris_heap_lang/lib/logatom_lock.v b/iris_heap_lang/lib/logatom_lock.v
index 859fea3d5..7d7301fb9 100644
--- a/iris_heap_lang/lib/logatom_lock.v
+++ b/iris_heap_lang/lib/logatom_lock.v
@@ -73,7 +73,7 @@ Section tada.
     tada_is_lock γ lk -∗
     <<< ∀∀ s, tada_lock_state γ s >>>
       acquire lk @ ∅
-    <<< ⌜ s = Free ⌝ ∗ tada_lock_state γ Locked, RET #() >>>.
+    <<< ⌜ s = Free ⌝ ∗ tada_lock_state γ Locked >>> {{{ RET #() }}}.
   Proof.
     iIntros "#Hislock %Φ AU". iApply wp_fupd.
     wp_apply (acquire_spec with "Hislock") as "[Hlocked Hvar1]".
@@ -88,7 +88,7 @@ Section tada.
     tada_is_lock γ lk -∗
     <<< tada_lock_state γ Locked >>>
       release lk @ ∅
-    <<< 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/tests/atomic.ref b/tests/atomic.ref
index 7021d20e9..6180598de 100644
--- a/tests/atomic.ref
+++ b/tests/atomic.ref
@@ -40,7 +40,7 @@
   heapGS0 : heapGS Σ
   P : val → iProp Σ
   ============================
-  ⊢ <<< ∀∀ x : val, P x >>> code @ ∅ <<< ∃∃ y : val, P y, RET #() >>>
+  ⊢ <<< ∀∀ x : val, P x >>> code @ ∅ <<< ∃∃ y : val, P y >>> {{{ RET #() }}}
 1 goal
   
   Σ : gFunctors
@@ -72,7 +72,7 @@
   heapGS0 : heapGS Σ
   l : loc
   ============================
-  ⊢ <<< ∀∀ x : val, l ↦ x >>> code @ ∅ <<< l ↦ x, RET #() >>>
+  ⊢ <<< ∀∀ x : val, l ↦ x >>> code @ ∅ <<< l ↦ x >>> {{{ RET #() }}}
 1 goal
   
   Σ : gFunctors
@@ -104,7 +104,7 @@
   heapGS0 : heapGS Σ
   l : loc
   ============================
-  ⊢ <<< l ↦ #() >>> code @ ∅ <<< ∃∃ y : val, l ↦ y, RET #() >>>
+  ⊢ <<< l ↦ #() >>> code @ ∅ <<< ∃∃ y : val, l ↦ y >>> {{{ RET #() }}}
 1 goal
   
   Σ : gFunctors
@@ -136,7 +136,7 @@
   heapGS0 : heapGS Σ
   l : loc
   ============================
-  ⊢ <<< l ↦ #() >>> code @ ∅ <<< l ↦ #(), RET #() >>>
+  ⊢ <<< l ↦ #() >>> code @ ∅ <<< l ↦ #() >>> {{{ RET #() }}}
 1 goal
   
   Σ : gFunctors
@@ -170,7 +170,8 @@
   ============================
   ⊢ <<< ∀∀ x : val, l ↦ x ∗ l ↦ x >>>
       code @ ∅
-    <<< ∃ y : val, l ↦ y, RET #() >>>
+    <<< ∃ y : val, l ↦ y >>>
+    {{{ RET #() }}}
 1 goal
   
   Σ : gFunctors
@@ -191,7 +192,8 @@
   ============================
   ⊢ <<< ∀∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
       code @ ∅
-    <<< ∃∃ y : val, l ↦ y, RET #() >>>
+    <<< ∃∃ y : val, l ↦ y >>>
+    {{{ RET #() }}}
 1 goal
   
   Σ : gFunctors
@@ -212,8 +214,9 @@
   ============================
   ⊢ <<< ∀∀ xx : val, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
       code @ ∅
-    <<< ∃∃ yyyy : val, l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
-        RET #() >>>
+    <<< ∃∃ yyyy : val, l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗
+        l ↦ xx ∗ l ↦ xx >>>
+    {{{ RET #() }}}
 1 goal
   
   Σ : gFunctors
@@ -224,7 +227,7 @@
   _ : AU << ∃∃ xx : val, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>
          @ ⊤ ∖ ∅, ∅
          << ∀∀ yyyy : val, l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗
-            l ↦ xx, COMM Φ #() >>
+            l ↦ xx ∗ l ↦ xx, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
 1 goal
@@ -235,7 +238,8 @@
   ============================
   ⊢ <<< ∀∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
       code @ ∅
-    <<< l ↦ x, RET #() >>>
+    <<< l ↦ x >>>
+    {{{ RET #() }}}
 1 goal
   
   Σ : gFunctors
@@ -257,7 +261,8 @@
   ============================
   ⊢ <<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
       code @ ∅
-    <<< ∃∃ y : val, l ↦ y, RET #() >>>
+    <<< ∃∃ y : val, l ↦ y >>>
+    {{{ RET #() }}}
 1 goal
   
   Σ : gFunctors
@@ -280,7 +285,8 @@
   ============================
   ⊢ <<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
       code @ ∅
-    <<< l ↦ #(), RET #() >>>
+    <<< l ↦ #() >>>
+    {{{ RET #() }}}
 1 goal
   
   Σ : gFunctors
@@ -303,7 +309,8 @@
   ============================
   ⊢ <<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
       code @ ∅
-    <<< l ↦ yyyy, RET #() >>>
+    <<< l ↦ yyyy >>>
+    {{{ RET #() }}}
 1 goal
   
   Σ : gFunctors
@@ -326,8 +333,8 @@
   ============================
   ⊢ <<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
       code @ ∅
-    <<< l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
-        RET #() >>>
+    <<< l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
+    {{{ RET #() }}}
 1 goal
   
   Σ : gFunctors
diff --git a/tests/atomic.v b/tests/atomic.v
index 7b2cdffd9..67854178a 100644
--- a/tests/atomic.v
+++ b/tests/atomic.v
@@ -51,28 +51,28 @@ Section printing.
 
   (* Without private postcondition or RET binders *)
   Lemma print_both_quant (P : val → iProp Σ) :
-    ⊢ <<< ∀∀ x, P x >>> code @ ∅ <<< ∃∃ y, P y, RET #() >>>.
+    ⊢ <<< ∀∀ x, P x >>> code @ ∅ <<< ∃∃ y, P y >>> {{{ RET #() }}}.
   Proof.
     Show. iIntros (Φ) "AU". rewrite difference_empty_L. Show.
     iPoseProof (aupd_aacc with "AU") as "?". Show.
   Abort.
 
   Lemma print_first_quant l :
-    ⊢ <<< ∀∀ x, l ↦ x >>> code @ ∅ <<< l ↦ x, RET #() >>>.
+    ⊢ <<< ∀∀ x, l ↦ x >>> code @ ∅ <<< l ↦ x >>> {{{ RET #() }}}.
   Proof.
     Show. iIntros (Φ) "AU". Show.
     iPoseProof (aupd_aacc with "AU") as "?". Show.
   Abort.
 
   Lemma print_second_quant l :
-    ⊢ <<< l ↦ #() >>> code @ ∅ <<< ∃∃ y, l ↦ y, RET #() >>>.
+    ⊢ <<< l ↦ #() >>> code @ ∅ <<< ∃∃ y, l ↦ y >>> {{{ RET #() }}}.
   Proof.
     Show. iIntros (Φ) "AU". Show.
     iPoseProof (aupd_aacc with "AU") as "?". Show.
   Abort.
 
   Lemma print_no_quant l :
-    ⊢ <<< l ↦ #() >>> code @ ∅ <<< l ↦ #(), RET #() >>>.
+    ⊢ <<< l ↦ #() >>> code @ ∅ <<< l ↦ #() >>> {{{ RET #() }}}.
   Proof.
     Show. iIntros (Φ) "AU". Show.
     iPoseProof (aupd_aacc with "AU") as "?". Show.
@@ -81,49 +81,49 @@ Section printing.
   Check "Now come the long pre/post tests".
 
   Lemma print_both_quant_long l :
-    ⊢ <<< ∀∀ x, l ↦ x ∗ l ↦ x >>> code @ ∅ <<< ∃ y, l ↦ y, RET #() >>>.
+    ⊢ <<< ∀∀ x, l ↦ x ∗ l ↦ x >>> code @ ∅ <<< ∃ y, l ↦ y >>> {{{ RET #() }}}.
   Proof.
     Show. iIntros (Φ) "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 #() >>>.
+    ⊢ <<< ∀∀ x, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>> code @ ∅ <<< ∃∃ y, l ↦ y >>> {{{ RET #() }}}.
   Proof.
     Show. iIntros (Φ) "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 #() >>>.
+    ⊢ <<< ∀∀ xx, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>> code @ ∅ <<< ∃∃ yyyy, l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>> {{{ RET #() }}}.
   Proof.
     Show. iIntros (Φ) "?". Show.
   Abort.
 
   Lemma print_first_quant_long l :
-    ⊢ <<< ∀∀ x, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>> code @ ∅ <<< l ↦ x, RET #() >>>.
+    ⊢ <<< ∀∀ x, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>> code @ ∅ <<< l ↦ x >>> {{{ RET #() }}}.
   Proof.
     Show. iIntros (Φ) "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 #() >>>.
+    ⊢ <<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>> code @ ∅ <<< ∃∃ y, l ↦ y >>> {{{ RET #() }}}.
   Proof.
     Show. iIntros (Φ) "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 #() >>>.
+    ⊢ <<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>> code @ ∅ <<< l ↦ #() >>> {{{ RET #() }}}.
   Proof.
     Show. iIntros (Φ) "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 #() >>>.
+    ⊢ <<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>> code @ ∅ <<< l ↦ yyyy >>> {{{ RET #() }}}.
   Proof.
     Show. iIntros (Φ) "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 #() >>>.
+    ⊢ <<< 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 (Φ) "AU". Show.
   Abort.
@@ -154,7 +154,7 @@ Section printing.
   Check "Prettification".
 
   Lemma iMod_prettify (P : val → iProp Σ) :
-    ⊢ <<< ∀∀ x, P x >>> !#0 @ ∅ <<< ∃∃ y, P y, RET #() >>>.
+    ⊢ <<< ∀∀ x, P x >>> !#0 @ ∅ <<< ∃∃ y, P y >>> {{{ RET #() }}}.
   Proof.
     iIntros (Φ) "AU". iMod "AU". Show.
   Abort.
-- 
GitLab