Commit ebf06f91 authored by Robbert Krebbers's avatar Robbert Krebbers

Fine-grained post-conditions for forked-off threads.

This commit extends the state interpretation with an additional parameter to
talk about the number of forked-off threads, and a fixed postcondition for each
forked-off thread:

    state_interp : Λstate → list Λobservation → nat → iProp Σ;
    fork_post : iProp Σ;

This way, instead of having `True` as the post-condition of `Fork`, one can
have any post-condition, which is then recorded in the state interpretation.
The point of keeping track of the postconditions of forked-off threads, is that
we get an (additional) stronger adequacy theorem:

    Theorem wp_strong_all_adequacy Σ Λ `{invPreG Σ} s e σ1 v vs σ2 φ :
       (∀ `{Hinv : invG Σ} κs,
         (|={⊤}=> ∃
             (stateI : state Λ → list (observation Λ) → nat → iProp Σ)
             (fork_post : 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) →
      rtc erased_step ([e], σ1) (of_val <$> v :: vs, σ2) →
      φ v.

The difference with the ordinary adequacy theorem is that this one only applies
once all threads terminated. In this case, one gets back the post-conditions
`[∗] replicate m fork_post` of all forked-off threads.

In Iron we showed that we can use this mechanism to make sure that all
resources are disposed of properly in the presence of fork-based concurrency.
parent b0e4b6fa
......@@ -16,8 +16,9 @@ Class heapG Σ := HeapG {
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
state_interp σ κs _ :=
(gen_heap_ctx σ.(heap) proph_map_ctx κs σ.(used_proph_id))%I;
fork_post := True%I;
}.
(** Override the notations so that scopes and coercions work out *)
......@@ -162,7 +163,7 @@ Lemma wp_fork s E e Φ :
WP e @ s; {{ _, True }} - Φ (LitV LitUnit) - WP Fork e @ s; E {{ Φ }}.
Proof.
iIntros "He HΦ".
iApply wp_lift_pure_det_head_step; [by eauto|intros; inv_head_step; by eauto|].
iApply wp_lift_pure_det_head_step; [done|auto|intros; inv_head_step; eauto|].
iModIntro; iNext; iIntros "!> /= {$He}". by iApply wp_value.
Qed.
......@@ -170,7 +171,7 @@ Lemma twp_fork s E e Φ :
WP e @ s; [{ _, True }] - Φ (LitV LitUnit) - WP Fork e @ s; E [{ Φ }].
Proof.
iIntros "He HΦ".
iApply twp_lift_pure_det_head_step; [eauto|intros; inv_head_step; eauto|].
iApply twp_lift_pure_det_head_step; [done|auto|intros; inv_head_step; eauto|].
iIntros "!> /= {$He}". by iApply twp_value.
Qed.
......@@ -179,7 +180,7 @@ Lemma wp_alloc s E v :
{{{ True }}} Alloc (Val v) @ s; E {{{ l, RET LitV (LitLoc l); l v }}}.
Proof.
iIntros (Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 κ κs) "[Hσ Hκs] !>"; iSplit; first by auto.
iIntros (σ1 κ κs n) "[Hσ Hκs] !>"; iSplit; first by auto.
iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
iMod (@gen_heap_alloc with "Hσ") as "[Hσ Hl]"; first done.
iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
......@@ -188,7 +189,7 @@ Lemma twp_alloc s E v :
[[{ True }]] Alloc (Val v) @ s; E [[{ l, RET LitV (LitLoc l); l v }]].
Proof.
iIntros (Φ) "_ HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 κs) "[Hσ Hκs] !>"; iSplit; first by eauto.
iIntros (σ1 κs n) "[Hσ Hκs] !>"; iSplit; first by auto.
iIntros (κ v2 σ2 efs Hstep); inv_head_step.
iMod (@gen_heap_alloc with "Hσ") as "[Hσ Hl]"; first done.
iModIntro; iSplit=> //. iSplit; first done. iFrame. by iApply "HΦ".
......@@ -198,7 +199,7 @@ Lemma wp_load s E l q v :
{{{ l {q} v }}} Load (Val $ LitV $ LitLoc l) @ s; E {{{ RET v; l {q} v }}}.
Proof.
iIntros (Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 κ κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iIntros (σ1 κ κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto. iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
......@@ -206,7 +207,7 @@ Lemma twp_load s E l q v :
[[{ l {q} v }]] Load (Val $ LitV $ LitLoc l) @ s; E [[{ RET v; l {q} v }]].
Proof.
iIntros (Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto. iIntros (κ v2 σ2 efs Hstep); inv_head_step.
iModIntro; iSplit=> //. iSplit; first done. iFrame. by iApply "HΦ".
Qed.
......@@ -217,7 +218,7 @@ Lemma wp_store s E l v' v :
Proof.
iIntros (Φ) ">Hl HΦ".
iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 κ κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iIntros (σ1 κ κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto. iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
......@@ -228,7 +229,7 @@ Lemma twp_store s E l v' v :
Proof.
iIntros (Φ) "Hl HΦ".
iApply twp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto. iIntros (κ v2 σ2 efs Hstep); inv_head_step.
iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
iModIntro. iSplit=>//. iSplit; first done. iFrame. by iApply "HΦ".
......@@ -240,7 +241,7 @@ Lemma wp_cas_fail s E l q v' v1 v2 :
{{{ RET LitV (LitBool false); l {q} v' }}}.
Proof.
iIntros (?? Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 κ κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iIntros (σ1 κ κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
......@@ -250,7 +251,7 @@ Lemma twp_cas_fail s E l q v' v1 v2 :
[[{ RET LitV (LitBool false); l {q} v' }]].
Proof.
iIntros (?? Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto. iIntros (κ v2' σ2 efs Hstep); inv_head_step.
iModIntro; iSplit=> //. iSplit; first done. iFrame. by iApply "HΦ".
Qed.
......@@ -261,7 +262,7 @@ Lemma wp_cas_suc s E l v1 v2 :
{{{ RET LitV (LitBool true); l v2 }}}.
Proof.
iIntros (? Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 κ κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iIntros (σ1 κ κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
......@@ -272,7 +273,7 @@ Lemma twp_cas_suc s E l v1 v2 :
[[{ RET LitV (LitBool true); l v2 }]].
Proof.
iIntros (? Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto. iIntros (κ v2' σ2 efs Hstep); inv_head_step.
iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
iModIntro. iSplit=>//. iSplit; first done. iFrame. by iApply "HΦ".
......@@ -283,7 +284,7 @@ Lemma wp_faa s E l i1 i2 :
{{{ RET LitV (LitInt i1); l LitV (LitInt (i1 + i2)) }}}.
Proof.
iIntros (Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 κ κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iIntros (σ1 κ κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
......@@ -293,7 +294,7 @@ Lemma twp_faa s E l i1 i2 :
[[{ RET LitV (LitInt i1); l LitV (LitInt (i1 + i2)) }]].
Proof.
iIntros (Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto. iIntros (κ e2 σ2 efs Hstep); inv_head_step.
iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
iModIntro. iSplit=>//. iSplit; first done. iFrame. by iApply "HΦ".
......@@ -304,7 +305,7 @@ Lemma wp_new_proph :
{{{ True }}} NewProph {{{ v (p : proph_id), RET (LitV (LitProphecy p)); proph p v }}}.
Proof.
iIntros (Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 κ κs) "[Hσ HR] !>". iDestruct "HR" as (R [Hfr Hdom]) "HR".
iIntros (σ1 κ κs n) "[Hσ HR] !>". iDestruct "HR" as (R [Hfr Hdom]) "HR".
iSplit; first by eauto.
iNext; iIntros (v2 σ2 efs Hstep). inv_head_step.
iMod (@proph_map_alloc with "HR") as "[HR Hp]".
......@@ -323,7 +324,7 @@ Lemma wp_resolve_proph p v w:
{{{ RET (LitV LitUnit); v = Some w }}}.
Proof.
iIntros (Φ) "Hp HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 κ κs) "[Hσ HR] !>". iDestruct "HR" as (R [Hfr Hdom]) "HR".
iIntros (σ1 κ κs n) "[Hσ HR] !>". iDestruct "HR" as (R [Hfr Hdom]) "HR".
iDestruct (@proph_map_valid with "HR Hp") as %Hlookup.
iSplit; first by eauto.
iNext; iIntros (v2 σ2 efs Hstep); inv_head_step. iApply fupd_frame_l.
......@@ -331,8 +332,7 @@ Proof.
iMod (@proph_map_remove with "HR Hp") as "Hp". iModIntro.
iSplitR "HΦ".
- iExists _. iFrame. iPureIntro. split; first by eapply first_resolve_delete.
rewrite dom_delete. rewrite <- difference_empty_L. by eapply difference_mono.
rewrite dom_delete. set_solver.
- iApply "HΦ". iPureIntro. by eapply first_resolve_eq.
Qed.
End lifting.
......@@ -12,6 +12,8 @@ Proof.
iMod (gen_heap_init σ.(heap)) as (?) "Hh".
iMod (proph_map_init [] σ.(used_proph_id)) as (?) "Hp".
iModIntro.
iExists (λ σ κs, (gen_heap_ctx σ.(heap) proph_map_ctx κs σ.(used_proph_id))%I). iFrame.
iExists
(λ σ κs _, (gen_heap_ctx σ.(heap) proph_map_ctx κs σ.(used_proph_id))%I),
True%I; iFrame.
iApply (Hwp (HeapG _ _ _ _)).
Qed.
......@@ -39,14 +39,14 @@ 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; {{ _, True }})%I.
Notation wptp s t := ([ list] ef t, WP ef @ s; {{ _, fork_post }})%I.
Lemma wp_step s E e1 σ1 κ κs e2 σ2 efs Φ :
Lemma wp_step s e1 σ1 κ κs e2 σ2 efs m Φ :
prim_step e1 σ1 κ e2 σ2 efs
state_interp σ1 (κ ++ κs) WP e1 @ s; E {{ Φ }}
={E,}= (state_interp σ2 κs WP e2 @ s; E {{ Φ }} wptp s efs).
state_interp σ1 (κ ++ κs) m - WP e1 @ s; {{ Φ }} ={,}=
state_interp σ2 κs (length efs + m) WP e2 @ s; {{ Φ }} wptp s efs.
Proof.
rewrite {1}wp_unfold /wp_pre. iIntros (?) "[Hσ H]".
rewrite {1}wp_unfold /wp_pre. iIntros (?) "Hσ H".
rewrite (val_stuck e1 σ1 κ e2 σ2 efs) //.
iMod ("H" $! σ1 with "Hσ") as "(_ & H)".
iMod ("H" $! e2 σ2 efs with "[//]") as "H".
......@@ -55,43 +55,52 @@ Qed.
Lemma wptp_step s e1 t1 t2 κ κs σ1 σ2 Φ :
step (e1 :: t1,σ1) κ (t2, σ2)
state_interp σ1 (κ ++ κs) WP e1 @ s; {{ Φ }} wptp s t1
== e2 t2',
t2 = e2 :: t2' |={,}=> (state_interp σ2 κs WP e2 @ s; {{ Φ }} wptp s t2').
state_interp σ1 (κ ++ κs) (length t1) - WP e1 @ s; {{ Φ }} - wptp s t1 ==
e2 t2', t2 = e2 :: t2'
|={,}=> state_interp σ2 κs (pred (length t2)) WP e2 @ s; {{ Φ }} wptp s t2'.
Proof.
iIntros (Hstep) "(HW & He & Ht)".
iIntros (Hstep) "Hσ He Ht".
destruct Hstep as [e1' σ1' e2' σ2' efs [|? t1'] t2' ?? Hstep]; simplify_eq/=.
- iExists e2', (t2' ++ efs). iSplitR; first by eauto.
iFrame "Ht". iApply wp_step; eauto with iFrame.
- iExists e2', (t2' ++ efs). iModIntro. iSplitR; first by eauto.
iMod (wp_step with "Hσ He") as "H"; first done.
iIntros "!> !>". iMod "H" as "(Hσ & He2 & Hefs)".
iIntros "!>". rewrite Nat.add_comm app_length. iFrame.
- iExists e, (t1' ++ e2' :: t2' ++ efs); iSplitR; first eauto.
iDestruct "Ht" as "($ & He' & $)". iFrame "He".
iApply wp_step; eauto with iFrame.
iFrame "He". iDestruct "Ht" as "(Ht1 & He1 & Ht2)".
iModIntro. iMod (wp_step with "Hσ He1") as "H"; first done.
iIntros "!> !>". iMod "H" as "(Hσ & He2 & Hefs)". iIntros "!>".
rewrite !app_length /= !app_length.
replace (length t1' + S (length t2' + length efs))
with (length efs + (length t1' + S (length t2'))) by omega. iFrame.
Qed.
Lemma wptp_steps s n e1 t1 κs κs' t2 σ1 σ2 Φ :
nsteps n (e1 :: t1, σ1) κs (t2, σ2)
state_interp σ1 (κs ++ κs') WP e1 @ s; {{ Φ }} wptp s t1
|={,}=>^n ( e2 t2',
t2 = e2 :: t2' state_interp σ2 κs' WP e2 @ s; {{ Φ }} wptp s t2').
state_interp σ1 (κs ++ κs') (length t1) - WP e1 @ s; {{ Φ }} - wptp s t1
={,}=^n e2 t2',
t2 = e2 :: t2'
state_interp σ2 κs' (pred (length t2))
WP e2 @ s; {{ Φ }} wptp s t2'.
Proof.
revert e1 t1 κs κs' t2 σ1 σ2; simpl; induction n as [|n IH]=> e1 t1 κs κs' t2 σ1 σ2 /=.
{ inversion_clear 1; iIntros "(?&?&?)"; iExists e1, t1; iFrame; eauto 10. }
iIntros (Hsteps) "H". inversion_clear Hsteps as [|?? [t1' σ1']].
rewrite <- app_assoc.
iMod (wptp_step with "H") as (e1' t1'') "[% H]"; first eauto; simplify_eq.
iMod "H". iModIntro; iNext. iMod "H". iModIntro.
by iApply IH.
revert e1 t1 κs κs' t2 σ1 σ2; simpl.
induction n as [|n IH]=> e1 t1 κs κs' t2 σ1 σ2 /=.
{ inversion_clear 1; iIntros "???"; iExists e1, t1; iFrame; eauto 10. }
iIntros (Hsteps) "Hσ He Ht". inversion_clear Hsteps as [|?? [t1' σ1']].
rewrite -(assoc_L (++)).
iMod (wptp_step with "Hσ He Ht") as (e1' t1'' ?) ">H"; first eauto; simplify_eq.
iIntros "!> !>". iMod "H" as "(Hσ & He & Ht)". iModIntro.
by iApply (IH with "Hσ He Ht").
Qed.
Lemma wptp_result s n e1 t1 κs κs' v2 t2 σ1 σ2 φ :
Lemma wptp_result φ κs' s n e1 t1 κs v2 t2 σ1 σ2 :
nsteps n (e1 :: t1, σ1) κs (of_val v2 :: t2, σ2)
state_interp σ1 (κs ++ κs')
WP e1 @ s; {{ v, σ, state_interp σ κs' ={,}= ⌜φ v σ⌝ }}
wptp s t1
|={,}=>^(S n) ⌜φ v2 σ2.
state_interp σ1 (κs ++ κs') (length t1) -
WP e1 @ s; {{ v, σ, state_interp σ κs' (length t2) ={,}= ⌜φ v σ⌝ }} -
wptp s t1 ={,}=^(S n) ⌜φ v2 σ2.
Proof.
intros. rewrite Nat_iter_S_r wptp_steps //.
apply step_fupdN_mono.
iIntros (?) "Hσ He Ht". rewrite Nat_iter_S_r.
iDestruct (wptp_steps with "Hσ He Ht") as "H"; first done.
iApply (step_fupdN_wand with "H").
iDestruct 1 as (e2 t2' ?) "(Hσ & H & _)"; simplify_eq.
iMod (wp_value_inv' with "H") as "H".
iMod (fupd_plain_mask_empty _ ⌜φ v2 σ2%I with "[H Hσ]") as %?.
......@@ -99,109 +108,166 @@ Proof.
by iApply step_fupd_intro.
Qed.
Lemma wp_safe E e σ κs Φ :
state_interp σ κs - WP e @ E {{ Φ }} ={E, }= is_Some (to_val e) reducible e σ⌝.
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 }} -
wptp s t1
={,}=^(S n) ⌜φ v2 .
Proof.
iIntros (Hstep) "Hσ He Ht". rewrite Nat_iter_S_r.
iDestruct (wptp_steps with "Hσ He Ht") as "H"; first done.
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".
{ 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". }
iMod (fupd_plain_mask_empty _ ⌜φ v2%I with "[H Hm Hσ]") as %?.
{ iApply ("H" with "Hσ Hm"). }
by iApply step_fupd_intro.
Qed.
Lemma wp_safe κs m e σ Φ :
state_interp σ κs m -
WP e {{ Φ }} ={,}= is_Some (to_val e) reducible e σ⌝.
Proof.
rewrite wp_unfold /wp_pre. iIntros "Hσ H".
destruct (to_val e) as [v|] eqn:?.
{ iApply (step_fupd_mask_mono _ _ ); eauto. set_solver. }
{ iApply step_fupd_intro. set_solver. eauto. }
iMod (fupd_plain_mask_empty _ reducible e σ⌝%I with "[H Hσ]") as %?.
{ by iMod ("H" $! σ [] κs with "Hσ") as "($&H)". }
{ by iMod ("H" $! σ [] κs with "Hσ") as "[$ H]". }
iApply step_fupd_intro; first by set_solver+.
iIntros "!> !%". by right.
Qed.
Lemma wptp_safe n e1 κs κs' e2 t1 t2 σ1 σ2 Φ :
Lemma wptp_safe κs' n e1 κs e2 t1 t2 σ1 σ2 Φ :
nsteps n (e1 :: t1, σ1) κs (t2, σ2) e2 t2
state_interp σ1 (κs ++ κs') WP e1 {{ Φ }} wptp NotStuck t1
|={,}=>^(S n) is_Some (to_val e2) reducible e2 σ2.
state_interp σ1 (κs ++ κs') (length t1) - WP e1 {{ Φ }} - wptp NotStuck t1
={,}=^(S n) is_Some (to_val e2) reducible e2 σ2.
Proof.
intros ? He2. rewrite Nat_iter_S_r wptp_steps //.
apply step_fupdN_mono.
iDestruct 1 as (e2' t2' ?) "(Hw & H & Htp)"; simplify_eq.
apply elem_of_cons in He2 as [<-|?].
- iMod (wp_safe with "Hw H") as "$"; auto.
- iMod (wp_safe with "Hw [Htp]") as "$"; auto. by iApply (big_sepL_elem_of with "Htp").
iIntros (? He2) "Hσ He Ht". rewrite Nat_iter_S_r.
iDestruct (wptp_steps with "Hσ He Ht") as "H"; first done.
iApply (step_fupdN_wand with "H").
iDestruct 1 as (e2' t2' ?) "(Hσ & H & Ht)"; simplify_eq.
apply elem_of_cons in He2 as [<-|(t1''&t2''&->)%elem_of_list_split].
- iMod (wp_safe with "Hσ H") as "$"; auto.
- iDestruct "Ht" as "(_ & He2 & _)". by iMod (wp_safe with "Hσ He2").
Qed.
Lemma wptp_invariance s n e1 κs κs' e2 t1 t2 σ1 σ2 φ Φ :
Lemma wptp_invariance φ s n e1 κs κs' e2 t1 t2 σ1 σ2 Φ :
nsteps n (e1 :: t1, σ1) κs (t2, σ2)
(state_interp σ2 κs' ={,}= ⌜φ⌝)
state_interp σ1 (κs ++ κs') WP e1 @ s; {{ Φ }} wptp s t1
|={,}=>^(S n) |={,}=> ⌜φ⌝.
(state_interp σ2 κs' (pred (length t2)) ={,}= ⌜φ⌝) -
state_interp σ1 (κs ++ κs') (length t1) -
WP e1 @ s; {{ Φ }} - wptp s t1
={,}=^(S n) ⌜φ⌝.
Proof.
intros ?. rewrite Nat_iter_S_r wptp_steps // step_fupdN_frame_l.
apply step_fupdN_mono.
iIntros "[Hback H]"; iDestruct "H" as (e2' t2' ->) "[Hσ _]".
iSpecialize ("Hback" with "Hσ"). by iApply step_fupd_intro.
iIntros (?) "Hφ Hσ He Ht". rewrite Nat_iter_S_r.
iDestruct (wptp_steps _ n with "Hσ He Ht") as "H"; first done.
iApply (step_fupdN_wand with "H"). iDestruct 1 as (e2' t2' ->) "[Hσ _]".
iSpecialize ("Hφ" with "Hσ").
iMod (fupd_plain_mask_empty _ ⌜φ⌝%I with "Hφ") as %?.
by iApply step_fupd_intro.
Qed.
End adequacy.
Theorem wp_strong_adequacy Σ Λ `{invPreG Σ} s e σ φ :
( `{Hinv : invG Σ} κs,
(|={}=> stateI : state Λ list (observation Λ) iProp Σ,
let _ : irisG Λ Σ := IrisG _ _ _ Hinv stateI in
stateI σ κs WP e @ s; {{ v, σ, stateI σ [] ={,}= ⌜φ v σ⌝ }})%I)
(|={}=>
(stateI : state Λ list (observation Λ) nat iProp Σ)
(fork_post : iProp Σ),
let _ : irisG Λ Σ := IrisG _ _ _ Hinv stateI fork_post in
(* This could be strengthened so that φ also talks about the number
of forked-off threads *)
stateI σ κs 0 WP e @ s; {{ v, σ m, stateI σ [] m ={,}= ⌜φ v σ⌝ }})%I)
adequate s e σ φ.
Proof.
intros Hwp; split.
- intros t2 σ2 v2 [n [κs ?]]%erased_steps_nsteps.
eapply (step_fupdN_soundness' _ (S (S n)))=> Hinv.
rewrite Nat_iter_S.
iMod Hwp as (Istate) "[HI Hwp]".
iApply (step_fupd_mask_mono _ _ ); auto. iModIntro. iNext; iModIntro.
iApply (@wptp_result _ _ (IrisG _ _ _ Hinv Istate) _ _ _ _ _ []); eauto with iFrame.
eapply (step_fupdN_soundness' _ (S (S n)))=> Hinv. rewrite Nat_iter_S.
iMod (Hwp _ (κs ++ [])) as (stateI fork_post) "[Hσ Hwp]".
iApply step_fupd_intro; first done. iModIntro.
iApply (@wptp_result _ _ (IrisG _ _ _ Hinv stateI fork_post) with "[Hσ] [Hwp]"); eauto.
iApply (wp_wand with "Hwp"). iIntros (v) "H"; iIntros (σ'). iApply "H".
- destruct s; last done. intros t2 σ2 e2 _ [n [κs ?]]%erased_steps_nsteps ?.
eapply (step_fupdN_soundness' _ (S (S n)))=> Hinv.
rewrite Nat_iter_S.
iMod Hwp as (Istate) "[HI Hwp]".
iApply (step_fupd_mask_mono _ _ ); auto.
iApply (@wptp_safe _ _ (IrisG _ _ _ Hinv Istate) _ _ _ []); [by eauto..|].
rewrite app_nil_r. eauto with iFrame.
eapply (step_fupdN_soundness' _ (S (S n)))=> Hinv. rewrite Nat_iter_S.
iMod (Hwp _ (κs ++ [])) as (stateI fork_post) "[Hσ Hwp]".
iApply step_fupd_intro; first done. iModIntro.
iApply (@wptp_safe _ _ (IrisG _ _ _ Hinv stateI fork_post) with "[Hσ] Hwp"); eauto.
Qed.
Theorem wp_adequacy Σ Λ `{invPreG Σ} s e σ φ :
( `{Hinv : invG Σ} κs,
(|={}=> stateI : state Λ list (observation Λ) iProp Σ,
let _ : irisG Λ Σ := IrisG _ _ _ Hinv stateI 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 stateI. iIntros "{$Hσ} !>".
iMod Hwp as (stateI) "[Hσ H]". iExists (λ σ κs _, stateI σ κs), True%I.
iIntros "{$Hσ} !>".
iApply (wp_wand with "H"). iIntros (v ? σ') "_".
iMod (fupd_intro_mask' ) as "_"; auto.
iIntros "_". by iApply fupd_mask_weaken.
Qed.
Theorem wp_strong_all_adequacy Σ Λ `{invPreG Σ} s e σ1 v vs σ2 φ :
( `{Hinv : invG Σ} κs,
(|={}=>
(stateI : state Λ list (observation Λ) nat iProp Σ)
(fork_post : 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)
rtc erased_step ([e], σ1) (of_val <$> v :: vs, σ2)
φ v.
Proof.
intros Hwp [n [κs ?]]%erased_steps_nsteps.
eapply (step_fupdN_soundness' _ (S (S n)))=> Hinv. rewrite Nat_iter_S.
iMod Hwp as (stateI fork_post) "[Hσ Hwp]".
iApply step_fupd_intro; first done. iModIntro.
iApply (@wptp_all_result _ _ (IrisG _ _ _ Hinv stateI fork_post)
with "[Hσ] [Hwp]"); eauto. by rewrite right_id_L.
Qed.
Theorem wp_invariance Σ Λ `{invPreG Σ} s e σ1 t2 σ2 φ :
( `{Hinv : invG Σ} κs κs',
(|={}=> stateI : state Λ list (observation Λ) iProp Σ,
let _ : irisG Λ Σ := IrisG _ _ _ Hinv stateI in
stateI σ1 (κs ++ κs') WP e @ s; {{ _, True }} (stateI σ2 κs' ={,}= ⌜φ⌝))%I)
(|={}=>
(stateI : state Λ list (observation Λ) nat iProp Σ)
(fork_post : 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)
rtc erased_step ([e], σ1) (t2, σ2)
φ.
Proof.
intros Hwp [n [κs ?]]%erased_steps_nsteps.
eapply (step_fupdN_soundness _ (S (S n)))=> Hinv.
rewrite Nat_iter_S.
iMod (Hwp Hinv κs []) as (Istate) "(HIstate & Hwp & Hclose)".
apply (step_fupdN_soundness' _ (S (S n)))=> Hinv. rewrite Nat_iter_S.
iMod (Hwp Hinv κs []) as (Istate fork_post) "(Hσ & Hwp & Hclose)".
iApply step_fupd_intro; first done.
iApply (@wptp_invariance _ _ (IrisG _ _ _ Hinv Istate)); eauto with iFrame.
iApply (@wptp_invariance _ _ (IrisG _ _ _ Hinv Istate fork_post)
with "Hclose [Hσ] [Hwp]"); eauto.
Qed.
(* An equivalent version that does not require finding [fupd_intro_mask'], but
can be confusing to use. *)
Corollary wp_invariance' Σ Λ `{invPreG Σ} s e σ1 t2 σ2 φ :
( `{Hinv : invG Σ} κs κs',
(|={}=> stateI : state Λ list (observation Λ) iProp Σ,
let _ : irisG Λ Σ := IrisG _ _ _ Hinv stateI in
stateI σ1 κs WP e @ s; {{ _, True }} (stateI σ2 κs' - E, |={,E}=> ⌜φ⌝))%I)
(|={}=>
(stateI : state Λ list (observation Λ) nat iProp Σ)
(fork_post : 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)
rtc erased_step ([e], σ1) (t2, σ2)
φ.
Proof.
intros Hwp. eapply wp_invariance; first done.
intros Hinv κs κs'. iMod (Hwp Hinv) as (stateI) "(? & ? & Hφ)".
iModIntro. iExists stateI. iFrame. iIntros "Hσ".
intros Hinv κs κs'. iMod (Hwp Hinv) as (stateI fork_post) "(? & ? & Hφ)".
iModIntro. iExists stateI, fork_post. iFrame. iIntros "Hσ".
iDestruct ("Hφ" with "Hσ") as (E) ">Hφ".
iMod (fupd_intro_mask') as "_"; last by iModIntro. solve_ndisj.
by iApply fupd_mask_weaken; first set_solver.
Qed.
......@@ -16,48 +16,53 @@ Hint Resolve head_stuck_stuck.
Lemma wp_lift_head_step_fupd {s E Φ} e1 :
to_val e1 = None
( σ1 κ κs, state_interp σ1 (κ ++ κs) ={E,}=
( σ1 κ κs n, state_interp σ1 (κ ++ κs) n ={E,}=
head_reducible e1 σ1
e2 σ2 efs, head_step e1 σ1 κ e2 σ2 efs ={,,E}=
state_interp σ2 κs WP e2 @ s; E {{ Φ }} [ list] ef efs, WP ef @ s; {{ _, True }})
state_interp σ2 κs (length efs + n)
WP e2 @ s; E {{ Φ }}
[ list] ef efs, WP ef @ s; {{ _, fork_post }})
WP e1 @ s; E {{ Φ }}.
Proof.
iIntros (?) "H". iApply wp_lift_step_fupd=>//. iIntros (σ1 κ κs) "Hσ".
iIntros (?) "H". iApply wp_lift_step_fupd=>//. iIntros (σ1 κ κs Qs) "Hσ".
iMod ("H" with "Hσ") as "[% H]"; iModIntro.
iSplit; first by destruct s; eauto. iIntros (e2 σ2 efs Hstep).
iSplit; first by destruct s; eauto. iIntros (e2 σ2 efs ?).
iApply "H"; eauto.
Qed.
Lemma wp_lift_head_step {s E Φ} e1 :
to_val e1 = None
( σ1 κ κs, state_interp σ1 (κ ++ κs) ={E,}=
( σ1 κ κs n, state_interp σ1 (κ ++ κs) n ={E,}=
head_reducible e1 σ1
e2 σ2 efs, head_step e1 σ1 κ e2 σ2 efs ={,E}=
state_interp σ2 κs WP e2 @ s; E {{ Φ }} [ list] ef efs, WP ef @ s; {{ _, True }})
state_interp σ2 κs (length efs + n)
WP e2 @ s; E {{ Φ }}
[ list] ef efs, WP ef @ s; {{ _, fork_post }})
WP e1 @ s; E {{ Φ }}.
Proof.
iIntros (?) "H". iApply wp_lift_head_step_fupd; [done|]. iIntros (???) "?".
iIntros (?) "H". iApply wp_lift_head_step_fupd; [done|]. iIntros (????) "?".
iMod ("H" with "[$]") as "[$ H]". iIntros "!>" (e2 σ2 efs ?) "!> !>". by iApply "H".
Qed.
Lemma wp_lift_head_stuck E Φ e :
to_val e = None
sub_redexes_are_values e
( σ κs, state_interp σ κs ={E,}= head_stuck e σ⌝)
( σ κs n, state_interp σ κs n ={E,}= head_stuck e σ⌝)
WP e @ E ?{{ Φ }}.
Proof.
iIntros (??) "H". iApply wp_lift_stuck; first done.
iIntros (σ κs) "Hσ". iMod ("H" with "Hσ") as "%". by auto.
iIntros (σ κs n) "Hσ". iMod ("H" with "Hσ") as "%". by auto.
Qed.
Lemma wp_lift_pure_head_step {s E E' Φ} e1 :
state_interp_fork_indep
( σ1, head_reducible e1 σ1)
( σ1 κ e2 σ2 efs, head_step e1 σ1 κ e2 σ2 efs κ = [] σ1 = σ2)
(|={E,E'}=> κ e2 efs σ, head_step e1 σ κ e2 σ efs
WP e2 @ s; E {{ Φ }} [ list] ef efs, WP ef @ s; {{ _, True }})
WP e2 @ s; E {{ Φ }} [ list] ef efs, WP ef @ s; {{ _, fork_post }})
WP e1 @ s; E {{ Φ }}.
Proof using Hinh.
iIntros (??) "H". iApply wp_lift_pure_step; [|by eauto|].
iIntros (???) "H". iApply wp_lift_pure_step; [done| |by eauto|].
{ by destruct s; auto. }
iApply (step_fupd_wand with "H"); iIntros "H".
iIntros (?????). iApply "H"; eauto.
......@@ -70,74 +75,77 @@ Lemma wp_lift_pure_head_stuck E Φ e :
WP e @ E ?{{ Φ }}%I.
Proof using Hinh.
iIntros (?? Hstuck). iApply wp_lift_head_stuck; [done|done|].
iIntros (σ κs) "_". iMod (fupd_intro_mask' E ) as "_"; first set_solver.
iIntros (σ κs n) "_". iMod (fupd_intro_mask' E ) as "_"; first set_solver.
by auto.
Qed.
Lemma wp_lift_atomic_head_step_fupd {s E1 E2 Φ} e1 :