From 387011bf4428bf28eb6e460a9e587cf70291d0e9 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 26 Jul 2023 12:25:20 +0200
Subject: [PATCH] atomic: add support for private postcondition

---
 iris/program_logic/atomic.v | 202 +++++++++++++++++++++++++++++-------
 tests/atomic.ref            |  41 ++++++++
 tests/atomic.v              |  27 ++++-
 3 files changed, 232 insertions(+), 38 deletions(-)

diff --git a/iris/program_logic/atomic.v b/iris/program_logic/atomic.v
index f4f967d60..ed2e65f0b 100644
--- a/iris/program_logic/atomic.v
+++ b/iris/program_logic/atomic.v
@@ -8,74 +8,201 @@ From iris.prelude Require Import options.
 
 (* 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 `{!irisGS_gen hlc Λ Σ} {TA TB : tele}
+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 *)
-  (f: TA → TB → val Λ) (* Turn the return data into the return value *)
+  (POST: TA → TB → TP → option (iProp Σ)) (* non-atomic post-condition *)
+  (f: TA → TB → TP → val Λ) (* Turn the return data into the return value *)
   : iProp Σ :=
     ∀ (Φ : val Λ → iProp Σ),
             (* The (outer) user mask is what is left after the implementation
             opened its things. *)
-            atomic_update (⊤∖E) ∅ α β (λ.. x y, Φ (f x y)) -∗
+            atomic_update (⊤∖E) ∅ α β (λ.. x y, ∀.. z, POST x y z -∗? Φ (f x y z)) -∗
             WP e {{ Φ }}.
-(* Note: To add a private postcondition, use
-   atomic_update α β Eo Ei (λ x y, POST x y -∗ Φ (f x y)) *)
 
 (* The way to read the [tele_app foo] here is that they convert the n-ary
 function [foo] into a unary function taking a telescope as the argument. *)
+Notation "'<<<' ∀∀ x1 .. xn , α '>>>' e @ E '<<<' ∃∃ y1 .. yn , β '>>>' '{{{' z1 .. zn , 'RET' v ; POST } } }" :=
+  (atomic_wp (TA:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
+             (TB:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
+             (TP:=TeleS (λ z1, .. (TeleS (λ zn, TeleO)) .. ))
+             e%E
+             E
+             (tele_app $ λ x1, .. (λ xn, α%I) ..)
+             (tele_app $ λ x1, .. (λ xn,
+                         tele_app $ λ y1, .. (λ yn, β%I) ..
+                        ) .. )
+             (tele_app $ λ x1, .. (λ xn,
+                         tele_app $ λ y1, .. (λ yn,
+                                   tele_app $ λ z1, .. (λ zn, Some POST%I) ..
+                                  ) ..
+                        ) .. )
+             (tele_app $ λ x1, .. (λ xn,
+                         tele_app $ λ y1, .. (λ yn,
+                                   tele_app $ λ z1, .. (λ zn, v%V) ..
+                                  ) ..
+                        ) .. )
+  )
+  (at level 20, E, α, β, v at level 200, x1 binder, xn binder, y1 binder, yn binder, z1 binder, zn binder,
+   format "'[hv' '<<<'  '[' ∀∀  x1  ..  xn ,  '/' α  ']' '>>>'  '/  ' e  @  E  '/' '<<<'  '[' ∃∃  y1  ..  yn ,  '/' β  ']' '>>>'  '/' {{{  '[' z1  ..  zn ,  RET  v ;  '/' POST  ']' } } } ']'")
+  : bi_scope.
+
+(* There are overall 16 of possible variants of this notation:
+- with and without ∀∀ binders
+- with and without ∃∃ binders
+- 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. *)
+
+(* No RET binders *)
+Notation "'<<<' ∀∀ x1 .. xn , α '>>>' e @ E '<<<' ∃∃ y1 .. yn , β '>>>' '{{{' 'RET' v ; POST } } }" :=
+  (atomic_wp (TA:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
+             (TB:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
+             (TP:=TeleO)
+             e%E
+             E
+             (tele_app $ λ x1, .. (λ xn, α%I) ..)
+             (tele_app $ λ x1, .. (λ xn,
+                         tele_app $ λ y1, .. (λ yn, β%I) ..
+                        ) .. )
+             (tele_app $ λ x1, .. (λ xn,
+                         tele_app $ λ y1, .. (λ yn, tele_app $ Some POST%I) ..
+                        ) .. )
+             (tele_app $ λ x1, .. (λ xn,
+                         tele_app $ λ y1, .. (λ yn, tele_app $ v%V) ..
+                        ) .. )
+  )
+  (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 ;  '/' POST  ']' } } } ']'")
+  : bi_scope.
+
+(* No ∃∃ binders, no RET binders *)
+Notation "'<<<' ∀∀ x1 .. xn , α '>>>' e @ E '<<<' β '>>>' '{{{' 'RET' v ; POST } } }" :=
+  (atomic_wp (TA:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
+             (TB:=TeleO)
+             (TP:=TeleO)
+             e%E
+             E
+             (tele_app $ λ x1, .. (λ xn, α%I) ..)
+             (tele_app $ λ x1, .. (λ xn, tele_app β%I) .. )
+             (tele_app $ λ x1, .. (λ xn,
+                         tele_app $ tele_app $ Some POST%I
+                        ) .. )
+             (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 ;  '/' POST  ']' } } } ']'")
+  : bi_scope.
+
+(* No ∀∀ binders, no RET binders *)
+Notation "'<<<' α '>>>' e @ E '<<<' ∃∃ y1 .. yn , β '>>>' '{{{' 'RET' v ; POST } } }" :=
+  (atomic_wp (TA:=TeleO)
+             (TB:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
+             (TP:=TeleO)
+             e%E
+             E
+             (tele_app $ α%I)
+             (tele_app $ tele_app $ λ y1, .. (λ yn, β%I) .. )
+             (tele_app $ tele_app $ λ y1, .. (λ yn, tele_app $ Some POST%I) .. )
+             (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 ;  '/' POST  ']' } } } ']'")
+  : bi_scope.
+
+(* No ∀∀ binders, no ∃∃ binders, no RET binders *)
+Notation "'<<<' α '>>>' e @ E '<<<' β '>>>' '{{{' 'RET' v ; POST } } }" :=
+  (atomic_wp (TA:=TeleO)
+             (TB:=TeleO)
+             (TP:=TeleO)
+             e%E
+             E
+             (tele_app $ α%I)
+             (tele_app $ tele_app β%I)
+             (tele_app $ tele_app $ tele_app $ Some POST%I)
+             (tele_app $ tele_app $ tele_app $ v%V)
+  )
+  (at level 20, E, α, β, v at level 200,
+   format "'[hv' '<<<'  '[' α  ']' '>>>'  '/  ' e  @  E  '/' '<<<'  '[' β  ']' '>>>'  '/' {{{  '[' RET  v ;  '/' POST  ']' } } } ']'")
+  : bi_scope.
+
+(* No RET binders, no POST *)
 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)
              e%E
              E
              (tele_app $ λ x1, .. (λ xn, α%I) ..)
              (tele_app $ λ x1, .. (λ xn,
-                         tele_app (λ y1, .. (λ yn, β%I) .. )
+                         tele_app $ λ y1, .. (λ yn, β%I) ..
+                        ) .. )
+             (tele_app $ λ x1, .. (λ xn,
+                         tele_app $ λ y1, .. (λ yn, tele_app None) ..
                         ) .. )
              (tele_app $ λ x1, .. (λ xn,
-                         tele_app (λ y1, .. (λ yn, v%V) .. )
+                         tele_app $ λ y1, .. (λ yn, tele_app v%V) ..
                         ) .. )
   )
   (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  ']' '>>>' ']'")
   : bi_scope.
 
+(* No ∃∃ binders, no RET binders, no POST *)
 Notation "'<<<' ∀∀ x1 .. xn , α '>>>' e @ E '<<<' β , 'RET' v '>>>'" :=
   (atomic_wp (TA:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
              (TB:=TeleO)
+             (TP:=TeleO)
              e%E
              E
              (tele_app $ λ x1, .. (λ xn, α%I) ..)
              (tele_app $ λ x1, .. (λ xn, tele_app β%I) .. )
-             (tele_app $ λ x1, .. (λ xn, tele_app v%V) .. )
+             (tele_app $ λ x1, .. (λ xn, tele_app $ tele_app None) .. )
+             (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  ']' '>>>' ']'")
   : bi_scope.
 
+(* No ∀∀ binders, no RET binders, no POST *)
 Notation "'<<<' α '>>>' e @ E '<<<' ∃∃ y1 .. yn , β , 'RET' v '>>>'" :=
   (atomic_wp (TA:=TeleO)
              (TB:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
+             (TP:=TeleO)
              e%E
              E
              (tele_app α%I)
-             (tele_app $ tele_app (λ y1, .. (λ yn, β%I) .. ))
-             (tele_app $ tele_app (λ y1, .. (λ yn, v%V) .. ))
+             (tele_app $ tele_app $ λ y1, .. (λ yn, β%I) .. )
+             (tele_app $ tele_app $ λ y1, .. (λ yn, tele_app None) .. )
+             (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  ']' '>>>' ']'")
   : bi_scope.
 
+(* No ∀∀ binders, no ∃∃ binders, no RET binders, no POST *)
 Notation "'<<<' α '>>>' e @ E '<<<' β , 'RET' v '>>>'" :=
   (atomic_wp (TA:=TeleO)
              (TB:=TeleO)
+             (TP:=TeleO)
              e%E
              E
              (tele_app α%I)
              (tele_app $ tele_app β%I)
-             (tele_app $ tele_app v%V)
+             (tele_app $ tele_app $ tele_app None)
+             (tele_app $ tele_app $ tele_app v%V)
   )
   (at level 20, E, α, β, v at level 200,
    format "'[hv' '<<<'  '[' α  ']' '>>>'  '/  ' e  @  E  '/' '<<<'  '[' β ,  '/' 'RET'  v  ']' '>>>' ']'")
@@ -83,64 +210,65 @@ Notation "'<<<' α '>>>' e @ E '<<<' β , 'RET' v '>>>'" :=
 
 (** Theory *)
 Section lemmas.
-  Context `{!irisGS_gen hlc Λ Σ} {TA TB : tele}.
+  Context `{!irisGS_gen hlc Λ Σ} {TA TB TP : tele}.
   Notation iProp := (iProp Σ).
-  Implicit Types (α : TA → iProp) (β : TA → TB → iProp) (f : TA → TB → val Λ).
+  Implicit Types (α : TA → iProp) (β : TA → TB → iProp) (POST : TA → TB → TP → option iProp) (f : TA → TB → TP → val Λ).
 
   (* Atomic triples imply sequential triples. *)
-  Lemma atomic_wp_seq e E α β f :
-    atomic_wp e E α β f -∗
-    ∀ Φ, ∀.. x, α x -∗ (∀.. y, β x y -∗ Φ (f x y)) -∗ WP e {{ Φ }}.
+  Lemma atomic_wp_seq e E α β POST f :
+    atomic_wp e E α β POST f -∗
+    ∀ Φ, ∀.. x, α x -∗ (∀.. y, β x y -∗ ∀.. z, POST x y z -∗? Φ (f x y z)) -∗ WP e {{ Φ }}.
   Proof.
     iIntros "Hwp" (Φ x) "Hα HΦ".
     iApply (wp_frame_wand with "HΦ"). iApply "Hwp".
     iAuIntro. iAaccIntro with "Hα"; first by eauto. iIntros (y) "Hβ !>".
     (* FIXME: Using ssreflect rewrite does not work, see Coq bug #7773. *)
-    rewrite ->!tele_app_bind. iIntros "HΦ". iApply "HΦ". done.
+    rewrite ->!tele_app_bind. iIntros (z) "Hpost HΦ". iApply ("HΦ" with "Hβ Hpost").
   Qed.
 
   (** This version matches the Texan triple, i.e., with a later in front of the
   [(∀.. y, β x y -∗ Φ (f x y))]. *)
-  Lemma atomic_wp_seq_step e E α β f :
+  Lemma atomic_wp_seq_step e E α β POST f :
     TCEq (to_val e) None →
-    atomic_wp e E α β f -∗
-    ∀ Φ, ∀.. x, α x -∗ ▷ (∀.. y, β x y -∗ Φ (f x y)) -∗ WP e {{ Φ }}.
+    atomic_wp e E α β POST f -∗
+    ∀ Φ, ∀.. x, α x -∗ ▷ (∀.. y, β x y -∗ ∀.. z, POST x y z -∗? Φ (f x y z)) -∗ WP e {{ Φ }}.
   Proof.
     iIntros (?) "H"; iIntros (Φ x) "Hα HΦ".
-    iApply (wp_step_fupd _ _ ⊤ _ (∀.. y : TB, β x y -∗ Φ (f x y))
+    iApply (wp_step_fupd _ _ ⊤ _ (∀.. y : TB, _)
       with "[$HΦ //]"); first done.
     iApply (atomic_wp_seq with "H Hα").
-    iIntros (y) "Hβ HΦ". by iApply "HΦ".
+    iIntros "%y Hβ %z Hpost HΦ". iApply ("HΦ" with "Hβ Hpost").
   Qed.
 
   (* Sequential triples with the empty mask for a physically atomic [e] are atomic. *)
-  Lemma atomic_seq_wp_atomic e E α β f `{!Atomic WeaklyAtomic e} :
-    (∀ Φ, ∀.. x, α x -∗ (∀.. y, β x y -∗ Φ (f x y)) -∗ WP e @ ∅ {{ Φ }}) -∗
-    atomic_wp e E α β f.
+  Lemma atomic_seq_wp_atomic e E α β POST f `{!Atomic WeaklyAtomic e} :
+    (∀ Φ, ∀.. x, α x -∗ (∀.. y, β x y -∗ ∀.. z, POST x y z -∗? Φ (f x y z)) -∗ WP e @ ∅ {{ Φ }}) -∗
+    atomic_wp e E α β POST f.
   Proof.
     iIntros "Hwp" (Φ) "AU". iMod "AU" as (x) "[Hα [_ Hclose]]".
-    iApply ("Hwp" with "Hα"). iIntros (y) "Hβ".
+    iApply ("Hwp" with "Hα"). iIntros "%y Hβ %z Hpost".
     iMod ("Hclose" with "Hβ") as "HΦ".
-    rewrite ->!tele_app_bind. iApply "HΦ".
+    rewrite ->!tele_app_bind. iApply "HΦ". done.
   Qed.
 
   (** Sequential triples with a persistent precondition and no initial quantifier
   are atomic. *)
   Lemma persistent_seq_wp_atomic e E (α : [tele] → iProp) (β : [tele] → TB → iProp)
-        (f : [tele] → TB → val Λ) {HP : Persistent (α [tele_arg])} :
-    (∀ Φ, α [tele_arg] -∗ (∀.. y, β [tele_arg] y -∗ Φ (f [tele_arg] y)) -∗ WP e {{ Φ }}) -∗
-    atomic_wp e E α β f.
+      (POST : [tele] → TB → TP → option iProp) (f : [tele] → TB → TP → val Λ)
+      {HP : Persistent (α [tele_arg])} :
+    (∀ Φ, α [tele_arg] -∗ (∀.. y, β [tele_arg] y -∗ ∀.. z, POST [tele_arg] y z -∗? Φ (f [tele_arg] y z)) -∗ WP e {{ Φ }}) -∗
+    atomic_wp e E α β POST f.
   Proof.
     simpl in HP. iIntros "Hwp" (Φ) "HΦ". iApply fupd_wp.
     iMod ("HΦ") as "[#Hα [Hclose _]]". iMod ("Hclose" with "Hα") as "HΦ".
-    iApply wp_fupd. iApply ("Hwp" with "Hα"). iIntros "!>" (y) "Hβ".
+    iApply wp_fupd. iApply ("Hwp" with "Hα"). iIntros "!> %y Hβ %z Hpost".
     iMod ("HΦ") as "[_ [_ Hclose]]". iMod ("Hclose" with "Hβ") as "HΦ".
     (* FIXME: Using ssreflect rewrite does not work, see Coq bug #7773. *)
-    rewrite ->!tele_app_bind. done.
+    rewrite ->!tele_app_bind. iApply "HΦ". done.
   Qed.
 
-  Lemma atomic_wp_mask_weaken e E1 E2 α β f :
-    E1 ⊆ E2 → atomic_wp e E1 α β f -∗ atomic_wp e E2 α β f.
+  Lemma atomic_wp_mask_weaken e E1 E2 α β POST f :
+    E1 ⊆ E2 → atomic_wp e E1 α β POST f -∗ atomic_wp e E2 α β POST f.
   Proof.
     iIntros (HE) "Hwp". iIntros (Φ) "AU". iApply "Hwp".
     iApply atomic_update_mask_weaken; last done. set_solver.
@@ -148,10 +276,10 @@ Section lemmas.
 
   (** We can open invariants around atomic triples.
       (Just for demonstration purposes; we always use [iInv] in proofs.) *)
-  Lemma atomic_wp_inv e E α β f N I :
+  Lemma atomic_wp_inv e E α β POST f N I :
     ↑N ⊆ E →
-    atomic_wp e (E ∖ ↑N) (λ.. x, ▷ I ∗ α x) (λ.. x y, ▷ I ∗ β x y) f -∗
-    inv N I -∗ atomic_wp e E α β f.
+    atomic_wp e (E ∖ ↑N) (λ.. x, ▷ I ∗ α x) (λ.. x y, ▷ I ∗ β x y) POST f -∗
+    inv N I -∗ atomic_wp e E α β POST f.
   Proof.
     intros ?. iIntros "Hwp #Hinv" (Φ) "AU". iApply "Hwp". iAuIntro.
     iInv N as "HI". iApply (aacc_aupd with "AU"); first solve_ndisj.
diff --git a/tests/atomic.ref b/tests/atomic.ref
index 131326ff0..7021d20e9 100644
--- a/tests/atomic.ref
+++ b/tests/atomic.ref
@@ -342,6 +342,47 @@
                l ↦ xx, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
+1 goal
+  
+  Σ : gFunctors
+  heapGS0 : heapGS Σ
+  P : val → iProp Σ
+  ============================
+  ⊢ <<< ∀∀ x : val, P x >>>
+      code @ ∅
+    <<< ∃∃ y : val, P y >>>
+    {{{ z : val, RET z; P z }}}
+1 goal
+  
+  Σ : gFunctors
+  heapGS0 : heapGS Σ
+  P : val → iProp Σ
+  ============================
+  ⊢ <<< ∀∀ x : val, P x >>>
+      code @ ∅
+    <<< ∃∃ y : val, P y >>>
+    {{{ RET y; P y }}}
+1 goal
+  
+  Σ : gFunctors
+  heapGS0 : heapGS Σ
+  P : val → iProp Σ
+  ============================
+  ⊢ <<< ∀∀ x : val, P x >>> code @ ∅ <<< P x >>> {{{ RET x; P x }}}
+1 goal
+  
+  Σ : gFunctors
+  heapGS0 : heapGS Σ
+  P : val → iProp Σ
+  ============================
+  ⊢ <<< P #() >>> code @ ∅ <<< ∃∃ y : val, P y >>> {{{ RET y; P y }}}
+1 goal
+  
+  Σ : gFunctors
+  heapGS0 : heapGS Σ
+  P : iProp Σ
+  ============================
+  ⊢ <<< P >>> code @ ∅ <<< P >>> {{{ RET #42; P }}}
 "Prettification"
      : string
 1 goal
diff --git a/tests/atomic.v b/tests/atomic.v
index 26688dbf2..7b2cdffd9 100644
--- a/tests/atomic.v
+++ b/tests/atomic.v
@@ -42,13 +42,14 @@ Section tests.
   Qed.
 End tests.
 
-(* Test if AWP and the AU obtained from AWP print. *)
+(* Test if AWP and the AU obtained from AWP print (and also tests that all the AWP variants parse and type-check). *)
 Check "printing".
 Section printing.
   Context `{!heapGS Σ}.
 
   Definition code : expr := #().
 
+  (* Without private postcondition or RET binders *)
   Lemma print_both_quant (P : val → iProp Σ) :
     ⊢ <<< ∀∀ x, P x >>> code @ ∅ <<< ∃∃ y, P y, RET #() >>>.
   Proof.
@@ -127,6 +128,29 @@ Section printing.
     Show. iIntros (Φ) "AU". Show.
   Abort.
 
+  (* With private postcondition.
+  (Makes no big difference for the AU so we only print the initial triple here.) *)
+  Lemma print_all (P : val → iProp Σ) :
+    ⊢ <<< ∀∀ x, P x >>> code @ ∅ <<< ∃∃ y, P y >>> {{{ z, RET z; P z }}}.
+  Proof. Show. Abort.
+
+  Lemma print_no_ret (P : val → iProp Σ) :
+    ⊢ <<< ∀∀ x, P x >>> code @ ∅ <<< ∃∃ y, P y >>> {{{ RET y; P y }}}.
+  Proof. Show. Abort.
+
+  Lemma print_no_ex_ret (P : val → iProp Σ) :
+    ⊢ <<< ∀∀ x, P x >>> code @ ∅ <<< P x >>> {{{ RET x; P x }}}.
+  Proof. Show. Abort.
+
+  Lemma print_no_all_ret (P : val → iProp Σ) :
+    ⊢ <<< P #() >>> code @ ∅ <<< ∃∃ y, P y >>> {{{ RET y; P y }}}.
+  Proof. Show. Abort.
+
+  Lemma print_no_all_ex_ret (P : iProp Σ) :
+    ⊢ <<< P >>> code @ ∅ <<< P >>> {{{ RET #42; P }}}.
+  Proof. Show. Abort.
+
+  (* misc *)
   Check "Prettification".
 
   Lemma iMod_prettify (P : val → iProp Σ) :
@@ -135,4 +159,5 @@ Section printing.
     iIntros (Φ) "AU". iMod "AU". Show.
   Abort.
 
+
 End printing.
-- 
GitLab