Commit 6b37b21d authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Merge branch 'robbert/fork_postcondition' into 'master'

Fine-grained post-conditions for forked-off threads

See merge request FP/iris-coq!182
parents b0e4b6fa 678b75da
......@@ -34,10 +34,14 @@ Changes in and extensions of the theory:
* [#] heap_lang values are now injected in heap_lang expressions via a specific
constructor of the expr inductive type. This simplifies much the tactical
infrastructure around the language. In particular, this allow us to get rid
the reflexion mechanism that was needed for proving closedness, atomicity and
the reflection mechanism that was needed for proving closedness, atomicity and
"valueness" of a term. The price to pay is the addition of new
"administrative" reductions in the operational semantics of the language.
* [#] Extend the state interpretation with a natural number that keeps track of
the number of forked-off threads, and have a global fixed proposition that
describes the postcondition of each forked-off thread (instead of it being
`True`). Additionally, there is a stronger variant of the adequacy theorem
that allows to make use of the postconditions of the forked-off threads.
Changes in Coq:
......
......@@ -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 *)
......@@ -161,17 +162,17 @@ Implicit Types σ : state.
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|].
iModIntro; iNext; iIntros "!> /= {$He}". by iApply wp_value.
iIntros "He HΦ". iApply wp_lift_atomic_head_step; [done|].
iIntros (σ1 κ κs n) "Hσ !>"; iSplit; first by eauto.
iNext; iIntros (v2 σ2 efs Hstep); inv_head_step. by iFrame.
Qed.
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|].
iIntros "!> /= {$He}". by iApply twp_value.
iIntros "He HΦ". iApply twp_lift_atomic_head_step; [done|].
iIntros (σ1 κs n) "Hσ !>"; iSplit; first by eauto.
iIntros (κ v2 σ2 efs Hstep); inv_head_step. by iFrame.
Qed.
(** Heap *)
......@@ -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) " 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,
state_interp σ2 κs' (length vs2) -
([ list] v vs2, fork_post v) ={,}= ⌜φ 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 ([ 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". }
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 : 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 *)
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 : val Λ iProp Σ),
let _ : irisG Λ Σ := IrisG _ _ Hinv stateI fork_post in
stateI σ1 κs 0 WP e @ s; {{ v,
stateI σ2 [] (length vs) -
([ list] v vs, fork_post v) ={,}= φ 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 : 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)
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 : val Λ iProp Σ),