Turn global fork postcondition into a predicate over return values.

theories/heap_lang/lifting.v

@@ -18,7 +18,7 @@ Instance heapG_irisG `{heapG Σ} : irisG heap_lang Σ := {
   iris_invG := heapG_invG;
   state_interp σ κs _ :=
     (gen_heap_ctx σ.(heap) ∗ proph_map_ctx κs σ.(used_proph_id))%I;
-  fork_post := True%I;
+  fork_post _ := True%I;
 }.
 
 (** Override the notations so that scopes and coercions work out *)

theories/heap_lang/total_adequacy.v

@@ -14,6 +14,6 @@ Proof.
   iModIntro.
   iExists
     (λ σ κs _, (gen_heap_ctx σ.(heap) ∗ proph_map_ctx κs σ.(used_proph_id))%I),
-    True%I; iFrame.
+    (λ _, True%I); iFrame.
   iApply (Hwp (HeapG _ _ _ _)).
 Qed.

theories/program_logic/adequacy.v

@@ -39,7 +39,7 @@ Implicit Types P Q : iProp Σ.
 Implicit Types Φ : val Λ → iProp Σ.
 Implicit Types Φs : list (val Λ → iProp Σ).
 
-Notation wptp s t := ([∗ list] ef ∈ t, WP ef @ s; ⊤ {{ _, fork_post }})%I.
+Notation wptp s t := ([∗ list] ef ∈ t, WP ef @ s; ⊤ {{ fork_post }})%I.
 
 Lemma wp_step s e1 σ1 κ κs e2 σ2 efs m Φ :
   prim_step e1 σ1 κ e2 σ2 efs →
@@ -112,8 +112,8 @@ Lemma wptp_all_result φ κs' s n e1 t1 κs v2 vs2 σ1 σ2 :
   nsteps n (e1 :: t1, σ1) κs (of_val <$> v2 :: vs2, σ2) →
   state_interp σ1 (κs ++ κs') (length t1) -∗
   WP e1 @ s; ⊤ {{ v,
-    let m' := length vs2 in
-    state_interp σ2 κs' m' -∗ [∗] replicate m' fork_post ={⊤,∅}=∗ ⌜φ v ⌝ }} -∗
+    state_interp σ2 κs' (length vs2) -∗
+    ([∗ list] v ∈ vs2, fork_post v) ={⊤,∅}=∗ ⌜φ v ⌝ }} -∗
   wptp s t1
   ={⊤,∅}▷=∗^(S n) ⌜φ v2 ⌝.
 Proof.
@@ -122,7 +122,7 @@ Proof.
   iApply (step_fupdN_wand with "H").
   iDestruct 1 as (e2 t2' ?) "(Hσ & H & Hvs)"; simplify_eq/=.
   rewrite fmap_length. iMod (wp_value_inv' with "H") as "H".
-  iAssert ([∗] replicate (length vs2) fork_post)%I with "[> Hvs]" as "Hm".
+  iAssert ([∗ list] v ∈ vs2, fork_post v)%I with "[> Hvs]" as "Hm".
   { clear Hstep. iInduction vs2 as [|v vs] "IH"; csimpl; first by iFrame.
     iDestruct "Hvs" as "[Hv Hvs]".
     iMod (wp_value_inv' with "Hv") as "$". by iApply "IH". }
@@ -178,7 +178,7 @@ Theorem wp_strong_adequacy Σ Λ `{invPreG Σ} s e σ φ :
   (∀ `{Hinv : invG Σ} κs,
      (|={⊤}=> ∃
          (stateI : state Λ → list (observation Λ) → nat → iProp Σ)
-         (fork_post : iProp Σ),
+         (fork_post : val Λ → iProp Σ),
        let _ : irisG Λ Σ := IrisG _ _ Hinv stateI fork_post in
        (* This could be strengthened so that φ also talks about the number 
        of forked-off threads *)
@@ -202,12 +202,12 @@ Qed.
 Theorem wp_adequacy Σ Λ `{invPreG Σ} s e σ φ :
   (∀ `{Hinv : invG Σ} κs,
      (|={⊤}=> ∃ stateI : state Λ → list (observation Λ) → iProp Σ,
-       let _ : irisG Λ Σ := IrisG _ _ Hinv (λ σ κs _, stateI σ κs) True%I in
+       let _ : irisG Λ Σ := IrisG _ _ Hinv (λ σ κs _, stateI σ κs) (λ _, True%I) in
        stateI σ κs ∗ WP e @ s; ⊤ {{ v, ⌜φ v⌝ }})%I) →
   adequate s e σ (λ v _, φ v).
 Proof.
   intros Hwp. apply (wp_strong_adequacy Σ _)=> Hinv κs.
-  iMod Hwp as (stateI) "[Hσ H]". iExists (λ σ κs _, stateI σ κs), True%I.
+  iMod Hwp as (stateI) "[Hσ H]". iExists (λ σ κs _, stateI σ κs), (λ _, True%I).
   iIntros "{$Hσ} !>".
   iApply (wp_wand with "H"). iIntros (v ? σ') "_".
   iIntros "_". by iApply fupd_mask_weaken.
@@ -217,11 +217,11 @@ Theorem wp_strong_all_adequacy Σ Λ `{invPreG Σ} s e σ1 v vs σ2 φ :
   (∀ `{Hinv : invG Σ} κs,
      (|={⊤}=> ∃
          (stateI : state Λ → list (observation Λ) → nat → iProp Σ)
-         (fork_post : iProp Σ),
+         (fork_post : val Λ → iProp Σ),
        let _ : irisG Λ Σ := IrisG _ _ Hinv stateI fork_post in
        stateI σ1 κs 0 ∗ WP e @ s; ⊤ {{ v,
-         let m := length vs in
-         stateI σ2 [] m -∗ [∗] replicate m fork_post ={⊤,∅}=∗ ⌜ φ v ⌝ }})%I) →
+         stateI σ2 [] (length vs) -∗
+         ([∗ list] v ∈ vs, fork_post v) ={⊤,∅}=∗ ⌜ φ v ⌝ }})%I) →
   rtc erased_step ([e], σ1) (of_val <$> v :: vs, σ2) →
   φ v.
 Proof.
@@ -237,7 +237,7 @@ Theorem wp_invariance Σ Λ `{invPreG Σ} s e σ1 t2 σ2 φ :
   (∀ `{Hinv : invG Σ} κs κs',
      (|={⊤}=> ∃
          (stateI : state Λ → list (observation Λ) → nat → iProp Σ)
-         (fork_post : iProp Σ),
+         (fork_post : val Λ → iProp Σ),
        let _ : irisG Λ Σ := IrisG _ _ Hinv stateI fork_post in
        stateI σ1 (κs ++ κs') 0 ∗ WP e @ s; ⊤ {{ _, True }} ∗
        (stateI σ2 κs' (pred (length t2)) ={⊤,∅}=∗ ⌜φ⌝))%I) →
@@ -258,7 +258,7 @@ Corollary wp_invariance' Σ Λ `{invPreG Σ} s e σ1 t2 σ2 φ :
   (∀ `{Hinv : invG Σ} κs κs',
      (|={⊤}=> ∃
          (stateI : state Λ → list (observation Λ) → nat → iProp Σ)
-         (fork_post : iProp Σ),
+         (fork_post : val Λ → iProp Σ),
        let _ : irisG Λ Σ := IrisG _ _ Hinv stateI fork_post in
        stateI σ1 κs 0 ∗ WP e @ s; ⊤ {{ _, True }} ∗
        (stateI σ2 κs' (pred (length t2)) -∗ ∃ E, |={⊤,E}=> ⌜φ⌝))%I) →

theories/program_logic/ectx_lifting.v

@@ -21,7 +21,7 @@ Lemma wp_lift_head_step_fupd {s E Φ} e1 :
     ∀ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={∅,∅,E}▷=∗
       state_interp σ2 κs (length efs + n) ∗
       WP e2 @ s; E {{ Φ }} ∗
-      [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, fork_post }})
+      [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ fork_post }})
   ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
   iIntros (?) "H". iApply wp_lift_step_fupd=>//. iIntros (σ1 κ κs Qs) "Hσ".
@@ -37,7 +37,7 @@ Lemma wp_lift_head_step {s E Φ} e1 :
     ▷ ∀ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={∅,E}=∗
       state_interp σ2 κs (length efs + n) ∗
       WP e2 @ s; E {{ Φ }} ∗
-      [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, fork_post }})
+      [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ fork_post }})
   ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
   iIntros (?) "H". iApply wp_lift_head_step_fupd; [done|]. iIntros (????) "?".
@@ -72,7 +72,7 @@ Lemma wp_lift_atomic_head_step_fupd {s E1 E2 Φ} e1 :
     ∀ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={E1,E2}▷=∗
       state_interp σ2 κs (length efs + n) ∗
       from_option Φ False (to_val e2) ∗
-      [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, fork_post }})
+      [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ fork_post }})
   ⊢ WP e1 @ s; E1 {{ Φ }}.
 Proof.
   iIntros (?) "H". iApply wp_lift_atomic_step_fupd; [done|].
@@ -88,7 +88,7 @@ Lemma wp_lift_atomic_head_step {s E Φ} e1 :
     ▷ ∀ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={E}=∗
       state_interp σ2 κs (length efs + n) ∗
       from_option Φ False (to_val e2) ∗
-      [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, fork_post }})
+      [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ fork_post }})
   ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
   iIntros (?) "H". iApply wp_lift_atomic_step; eauto.

theories/program_logic/lifting.v

@@ -20,7 +20,7 @@ Lemma wp_lift_step_fupd s E Φ e1 :
     ∀ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={∅,∅,E}▷=∗
       state_interp σ2 κs (length efs + n) ∗
       WP e2 @ s; E {{ Φ }} ∗
-      [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, fork_post }})
+      [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ fork_post }})
   ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
   rewrite wp_unfold /wp_pre=>->. iIntros "H" (σ1 κ κs n) "Hσ".
@@ -46,7 +46,7 @@ Lemma wp_lift_step s E Φ e1 :
     ▷ ∀ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={∅,E}=∗
       state_interp σ2 κs (length efs + n) ∗
       WP e2 @ s; E {{ Φ }} ∗
-      [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, fork_post }})
+      [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ fork_post }})
   ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
   iIntros (?) "H". iApply wp_lift_step_fupd; [done|]. iIntros (????) "Hσ".
@@ -89,7 +89,7 @@ Lemma wp_lift_atomic_step_fupd {s E1 E2 Φ} e1 :
     ∀ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={E1,E2}▷=∗
       state_interp σ2 κs (length efs + n) ∗
       from_option Φ False (to_val e2) ∗
-      [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, fork_post }})
+      [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ fork_post }})
   ⊢ WP e1 @ s; E1 {{ Φ }}.
 Proof.
   iIntros (?) "H".
@@ -111,7 +111,7 @@ Lemma wp_lift_atomic_step {s E Φ} e1 :
     ▷ ∀ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={E}=∗
       state_interp σ2 κs (length efs + n) ∗
       from_option Φ False (to_val e2) ∗
-      [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, fork_post }})
+      [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ fork_post }})
   ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
   iIntros (?) "H". iApply wp_lift_atomic_step_fupd; [done|].

theories/program_logic/ownp.v

@@ -14,7 +14,7 @@ Class ownPG (Λ : language) (Σ : gFunctors) := OwnPG {
 Instance ownPG_irisG `{ownPG Λ Σ} : irisG Λ Σ := {
   iris_invG := ownP_invG;
   state_interp σ κs _ := own ownP_name (● (Excl' σ))%I;
-  fork_post := True%I;
+  fork_post _ := True%I;
 }.
 Global Opaque iris_invG.
 
@@ -60,7 +60,7 @@ Proof.
   intros Hwp Hsteps. eapply (wp_invariance Σ Λ s e σ1 t2 σ2 _)=> //.
   iIntros (? κs κs').
   iMod (own_alloc (● (Excl' σ1) ⋅ ◯ (Excl' σ1))) as (γσ) "[Hσ Hσf]"; first done.
-  iExists (λ σ κs' _, own γσ (● (Excl' σ)))%I, True%I.
+  iExists (λ σ κs' _, own γσ (● (Excl' σ)))%I, (λ _, True%I).
   iFrame "Hσ".
   iMod (Hwp (OwnPG _ _ _ _ γσ) with "[Hσf]") as "[$ H]";
     first by rewrite /ownP; iFrame.

theories/program_logic/total_adequacy.v

@@ -118,7 +118,7 @@ Theorem twp_total Σ Λ `{invPreG Σ} s e σ Φ :
   (∀ `{Hinv : invG Σ},
      (|={⊤}=> ∃
          (stateI : state Λ → list (observation Λ) → nat → iProp Σ)
-         (fork_post : iProp Σ),
+         (fork_post : val Λ → iProp Σ),
        let _ : irisG Λ Σ := IrisG _ _ Hinv stateI fork_post in
        stateI σ [] 0 ∗ WP e @ s; ⊤ [{ Φ }])%I) →
   sn erased_step ([e], σ). (* i.e. ([e], σ) is strongly normalizing *)

theories/program_logic/total_ectx_lifting.v

@@ -21,7 +21,7 @@ Lemma twp_lift_head_step {s E Φ} e1 :
       ⌜κ = []⌝ ∗
       state_interp σ2 κs (length efs + n) ∗
       WP e2 @ s; E [{ Φ }] ∗
-      [∗ list] i ↦ ef ∈ efs, WP ef @ s; ⊤ [{ _, fork_post }])
+      [∗ list] i ↦ ef ∈ efs, WP ef @ s; ⊤ [{ fork_post }])
   ⊢ WP e1 @ s; E [{ Φ }].
 Proof.
   iIntros (?) "H".
@@ -49,7 +49,7 @@ Lemma twp_lift_atomic_head_step {s E Φ} e1 :
       ⌜κ = []⌝ ∗
       state_interp σ2 κs (length efs + n) ∗
       from_option Φ False (to_val e2) ∗
-      [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ _, fork_post }])
+      [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ fork_post }])
   ⊢ WP e1 @ s; E [{ Φ }].
 Proof.
   iIntros (?) "H". iApply twp_lift_atomic_step; eauto.

theories/program_logic/total_lifting.v

@@ -21,7 +21,7 @@ Lemma twp_lift_step s E Φ e1 :
       ⌜κ = []⌝ ∗
       state_interp σ2 κs (length efs + n) ∗
       WP e2 @ s; E [{ Φ }] ∗
-      [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ _, fork_post }])
+      [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ fork_post }])
   ⊢ WP e1 @ s; E [{ Φ }].
 Proof. by rewrite twp_unfold /twp_pre=> ->. Qed.
 
@@ -52,7 +52,7 @@ Lemma twp_lift_atomic_step {s E Φ} e1 :
       ⌜κ = []⌝ ∗
       state_interp σ2 κs (length efs + n) ∗
       from_option Φ False (to_val e2) ∗
-      [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ _, fork_post }])
+      [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ fork_post }])
   ⊢ WP e1 @ s; E [{ Φ }].
 Proof.
   iIntros (?) "H".

theories/program_logic/total_weakestpre.v

@@ -16,7 +16,7 @@ Definition twp_pre `{irisG Λ Σ} (s : stuckness)
          ⌜κ = []⌝ ∗
          state_interp σ2 κs (length efs + n) ∗
          wp E e2 Φ ∗
-         [∗ list] ef ∈ efs, wp ⊤ ef (λ _, fork_post)
+         [∗ list] ef ∈ efs, wp ⊤ ef fork_post
   end%I.
 
 Lemma twp_pre_mono `{irisG Λ Σ} s

theories/program_logic/weakestpre.v

@@ -18,7 +18,7 @@ Class irisG (Λ : language) (Σ : gFunctors) := IrisG {
   (** A fixed postcondition for any forked-off thread. For most languages, e.g.
   heap_lang, this will simply be [True]. However, it is useful if one wants to
   keep track of resources precisely, as in e.g. Iron. *)
-  fork_post : iProp Σ;
+  fork_post : val Λ → iProp Σ;
 }.
 Global Opaque iris_invG.
 
@@ -33,7 +33,7 @@ Definition wp_pre `{irisG Λ Σ} (s : stuckness)
        ∀ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={∅,∅,E}▷=∗
          state_interp σ2 κs (length efs + n) ∗
          wp E e2 Φ ∗
-         [∗ list] i ↦ ef ∈ efs, wp ⊤ ef (λ _, fork_post)
+         [∗ list] i ↦ ef ∈ efs, wp ⊤ ef fork_post
   end%I.
 
 Local Instance wp_pre_contractive `{irisG Λ Σ} s : Contractive (wp_pre s).