Commit ad30138f authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Makes it possible to use several logical steps for one logical steps, in a way...

Makes it possible to use several logical steps for one logical steps, in a way which can be controlled by ghost state.
parent f38829da
......@@ -26,6 +26,28 @@ s/\bbij_both_frac_valid\b/bij_both_dfrac_valid/g
EOF
```
**Changes in `base_logic`:**
* The soundness lemma of the base logic `step_fupdN_soundness`, has been
generalized. It now states the soundness of the logic even if invariants stay
open accross an arbitrary number of laters.
**Changes in `program_logic`:**
* The definition of weakest precondition has been changed in order to use
a variable number of laters (i.e., logical steps) for each physical step of
the operational semantics, depending on the number of physical steps executed
since the begining of the execution of the program. See merge request !595.
This implies several API-breaking changes, which can be easily fixed in client
formalizations in a backward compatible manner as follows:
- Ignore the new parameter `ns` in the state interpretation, which
corresponds to a step counter.
- Use the constant function "0" for the new field `num_laters_per_step` of
`irisG`.
- Use `fupd_intro _ _` for the new field `state_interp_mono` of `irisG`.
- Some proofs using lifting lemmas and adequacy theorems need to be adapted
to ignore the new step counter.
## Iris 3.4.0
The highlights and most notable changes of this release are as follows:
......
......@@ -71,28 +71,26 @@ Proof.
Qed.
Lemma step_fupdN_soundness `{!invPreG Σ} φ n :
( `{Hinv: !invG Σ}, @{iPropI Σ} |={}[]=>^n |={,}=> φ )
( `{Hinv: !invG Σ}, @{iPropI Σ} |={,}=> |={}=>^n φ )
φ.
Proof.
intros Hiter.
apply (soundness (M:=iResUR Σ) _ (S n)); simpl.
apply (fupd_plain_soundness _)=> Hinv.
iPoseProof (Hiter Hinv) as "H". clear Hiter.
destruct n as [|n].
- iApply fupd_plainly_mask_empty. iMod "H" as %?; auto.
- iDestruct (step_fupdN_wand _ _ _ _ (|={}=> ⌜φ⌝)%I with "H []") as "H'".
{ by iApply fupd_plain_mask_empty. }
rewrite -step_fupdN_S_fupd.
iMod (step_fupdN_plain with "H'") as "Hφ". iModIntro. iNext.
rewrite -later_laterN laterN_later.
iNext. by iMod "Hφ".
iApply fupd_plainly_mask_empty. iMod "H".
iMod (step_fupdN_plain with "H") as "H". iModIntro.
rewrite -later_plainly -laterN_plainly -later_laterN laterN_later.
iNext. iMod "H" as %Hφ. auto.
Qed.
Lemma step_fupdN_soundness' `{!invPreG Σ} φ n :
( `{Hinv: !invG Σ}, @{iPropI Σ} |={}[]=>^n φ )
φ.
Proof.
iIntros (Hiter). eapply (step_fupdN_soundness _ n).
iIntros (Hinv). iPoseProof (Hiter Hinv) as "Hiter".
iApply (step_fupdN_wand with "Hiter"). by iApply fupd_mask_intro_discard.
iIntros (Hiter). eapply (step_fupdN_soundness _ n)=>Hinv. destruct n as [|n].
{ by iApply fupd_mask_intro_discard; [|iApply (Hiter Hinv)]. }
simpl in Hiter |- *. iMod Hiter as "H". iIntros "!>!>!>".
iMod "H". clear. iInduction n as [|n] "IH"; [by iApply fupd_mask_intro_discard|].
simpl. iMod "H". iIntros "!>!>!>". iMod "H". by iApply "IH".
Qed.
......@@ -370,6 +370,16 @@ Section fupd_derived.
rewrite {4}(union_difference_L _ _ HE). done.
Qed.
Lemma fupd_mask_subseteq_emptyset_difference E1 E2 :
E2 E1
@{PROP} |={E1, E2}=> |={, E1E2}=> emp.
Proof.
intros ?. rewrite [in fupd E1](union_difference_L E2 E1); [|done].
rewrite (comm_L ())
-[X in fupd _ X](left_id_L () E2) -fupd_mask_frame_r; [|set_solver+].
apply fupd_mask_intro_subseteq; set_solver.
Qed.
Lemma fupd_sep E P Q : (|={E}=> P) (|={E}=> Q) ={E}= P Q.
Proof. by rewrite fupd_frame_r fupd_frame_l fupd_trans. Qed.
......@@ -460,6 +470,12 @@ Section fupd_derived.
by apply sep_mono; first apply later_intro.
Qed.
Lemma step_fupdN_intro Ei Eo n P : Ei Eo ^n P - |={Eo}[Ei]=>^n P.
Proof.
induction n as [|n IH]=> ?; [done|].
rewrite /= -step_fupd_intro; [|done]. by rewrite IH.
Qed.
Lemma step_fupdN_S_fupd n E P :
(|={E}[]=>^(S n) P) (|={E}[]=>^(S n) |={E}=> P).
Proof.
......
......@@ -7,6 +7,7 @@ Import uPred.
(** This file contains the adequacy statements of the Iris program logic. First
we prove a number of auxilary results. *)
Section adequacy.
Context `{!irisG Λ Σ}.
Implicit Types e : expr Λ.
......@@ -16,84 +17,96 @@ Implicit Types Φs : list (val Λ → iProp Σ).
Notation wptp s t Φs := ([ list] e;Φ t;Φs, WP e @ s; {{ Φ }})%I.
Lemma wp_step s e1 σ1 κ κs e2 σ2 efs nt Φ :
Lemma wp_step s e1 σ1 ns κ κs e2 σ2 efs nt Φ :
prim_step e1 σ1 κ e2 σ2 efs
state_interp σ1 (κ ++ κs) nt - WP e1 @ s; {{ Φ }} ={}[]=
state_interp σ2 κs (nt + length efs) WP e2 @ s; {{ Φ }}
state_interp σ1 ns (κ ++ κs) nt - WP e1 @ s; {{ Φ }}
={,}= |={}=>^(S $ num_laters_per_step ns) |={,}=>
state_interp σ2 (S ns) κs (nt + length efs) WP e2 @ s; {{ Φ }}
wptp s efs (replicate (length efs) fork_post).
Proof.
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".
iMod ("H" $! σ1 ns with "Hσ") as "(_ & H)". iModIntro.
iApply (step_fupdN_wand with "[H]"); first by iApply "H". iIntros ">H".
by rewrite Nat.add_comm big_sepL2_replicate_r.
Qed.
Lemma wptp_step s es1 es2 κ κs σ1 σ2 Φs nt :
Lemma wptp_step s es1 es2 κ κs σ1 ns σ2 Φs nt :
step (es1,σ1) κ (es2, σ2)
state_interp σ1 (κ ++ κs) nt - wptp s es1 Φs -
nt', |={}[]=> state_interp σ2 κs (nt + nt')
state_interp σ1 ns (κ ++ κs) nt - wptp s es1 Φs -
nt', |={,}=> |={}=>^(S $ num_laters_per_step$ ns) |={,}=>
state_interp σ2 (S ns) κs (nt + nt')
wptp s es2 (Φs ++ replicate nt' fork_post).
Proof.
iIntros (Hstep) "Hσ Ht".
destruct Hstep as [e1' σ1' e2' σ2' efs t2' t3 Hstep]; simplify_eq/=.
iDestruct (big_sepL2_app_inv_l with "Ht") as (Φs1 Φs2 ->) "[? Ht]".
iDestruct (big_sepL2_cons_inv_l with "Ht") as (Φ Φs3 ->) "[Ht ?]".
iExists _. iMod (wp_step with "Hσ Ht") as "H"; first done.
iIntros "!> !>". iMod "H" as "($ & He2 & Hefs)". iIntros "!>".
iExists _. iMod (wp_step with "Hσ Ht") as "H"; first done. iModIntro.
iApply (step_fupdN_wand with "H"). iIntros ">($ & He2 & Hefs) !>".
rewrite -(assoc_L app) -app_comm_cons. iFrame.
Qed.
Lemma wptp_steps s n es1 es2 κs κs' σ1 σ2 Φs nt :
(* The total number of laters used between the physical steps number
[start] (included) to [start+ns] (excluded). *)
Local Fixpoint steps_sum (num_laters_per_step : nat nat) (start ns : nat) : nat :=
match ns with
| O => 0
| S ns =>
S $ num_laters_per_step start + steps_sum num_laters_per_step (S start) ns
end.
Lemma wptp_steps s n es1 es2 κs κs' σ1 ns σ2 Φs nt :
nsteps n (es1, σ1) κs (es2, σ2)
state_interp σ1 (κs ++ κs') nt - wptp s es1 Φs
={}[]=^n nt',
state_interp σ2 κs' (nt + nt') wptp s es2 (Φs ++ replicate nt' fork_post).
state_interp σ1 ns (κs ++ κs') nt - wptp s es1 Φs
={,}= |={}=>^(steps_sum num_laters_per_step ns n) |={,}=> nt',
state_interp σ2 (n + ns) κs' (nt + nt')
wptp s es2 (Φs ++ replicate nt' fork_post).
Proof.
revert nt es1 es2 κs κs' σ1 σ2 Φs.
induction n as [|n IH]=> nt es1 es2 κs κs' σ1 σ2 Φs /=.
revert nt es1 es2 κs κs' σ1 ns σ2 Φs.
induction n as [|n IH]=> nt es1 es2 κs κs' σ1 ns σ2 Φs /=.
{ inversion_clear 1; iIntros "? ?"; iExists 0=> /=.
rewrite Nat.add_0_r right_id_L. by iFrame. }
rewrite Nat.add_0_r right_id_L. iFrame. by iApply fupd_mask_subseteq. }
iIntros (Hsteps) "Hσ He". inversion_clear Hsteps as [|?? [t1' σ1']].
rewrite -(assoc_L (++)).
rewrite -(assoc_L (++)) Nat_iter_add plus_n_Sm.
iDestruct (wptp_step with "Hσ He") as (nt') ">H"; first eauto; simplify_eq.
iIntros "!> !>". iMod "H" as "(Hσ & He)". iModIntro.
iApply (step_fupdN_wand with "[Hσ He]"); first by iApply (IH with "Hσ He").
iDestruct 1 as (nt'') "[??]". rewrite -Nat.add_assoc -(assoc_L app) -replicate_plus.
by eauto with iFrame.
iModIntro. iApply step_fupdN_S_fupd. iApply (step_fupdN_wand with "H").
iIntros ">(Hσ & He)". iMod (IH with "Hσ He") as "IH"; first done. iModIntro.
iApply (step_fupdN_wand with "IH"). iIntros ">IH".
iDestruct "IH" as (nt'') "[??]".
rewrite -Nat.add_assoc -(assoc_L app) -replicate_plus. by eauto with iFrame.
Qed.
Lemma wp_not_stuck κs nt e σ Φ :
state_interp σ κs nt - WP e {{ Φ }} ={}= not_stuck e σ⌝.
Lemma wp_not_stuck κs nt e σ ns Φ :
state_interp σ ns κs nt - WP e {{ Φ }} ={}= not_stuck e σ⌝.
Proof.
rewrite wp_unfold /wp_pre /not_stuck. iIntros "Hσ H".
destruct (to_val e) as [v|] eqn:?; first by eauto.
iSpecialize ("H" $! σ [] κs with "Hσ"). rewrite sep_elim_l.
iSpecialize ("H" $! σ ns [] κs with "Hσ"). rewrite sep_elim_l.
iMod (fupd_plain_mask with "H") as %?; eauto.
Qed.
Lemma wptp_strong_adequacy Φs κs' s n es1 es2 κs σ1 σ2 nt:
Lemma wptp_strong_adequacy Φs κs' s n es1 es2 κs σ1 ns σ2 nt:
nsteps n (es1, σ1) κs (es2, σ2)
state_interp σ1 (κs ++ κs') nt -
wptp s es1 Φs ={}[]=^(S n) nt',
state_interp σ1 ns (κs ++ κs') nt - wptp s es1 Φs
={,}= |={}=>^(steps_sum num_laters_per_step ns n) |={,}=> nt',
e2, s = NotStuck e2 es2 not_stuck e2 σ2
state_interp σ2 κs' (nt + nt')
state_interp σ2 (n + ns) κs' (nt + nt')
[ list] e;Φ es2;Φs ++ replicate nt' fork_post, from_option Φ True (to_val e).
Proof.
iIntros (Hstep) "Hσ He". rewrite Nat_iter_S_r.
iDestruct (wptp_steps with "Hσ He") as "Hwp"; first done.
iApply (step_fupdN_wand with "Hwp").
iDestruct 1 as (nt') "(Hσ & Ht)"; simplify_eq/=.
iIntros (Hstep) "Hσ He". iMod (wptp_steps with "Hσ He") as "Hwp"; first done.
iModIntro. iApply (step_fupdN_wand with "Hwp").
iMod 1 as (nt') "(Hσ & Ht)"; simplify_eq/=.
iMod (fupd_plain_keep_l
e2, s = NotStuck e2 es2 not_stuck e2 σ2 %I
(state_interp σ2 κs' (nt + nt') wptp s es2 (Φs ++ replicate nt' fork_post))%I
(state_interp σ2 (n + ns) κs' (nt + nt')
wptp s es2 (Φs ++ replicate nt' fork_post))%I
with "[$Hσ $Ht]") as "(%&Hσ&Hwp)".
{ iIntros "(Hσ & Ht)" (e' -> He').
move: He' => /(elem_of_list_split _ _)[?[?->]].
iDestruct (big_sepL2_app_inv_l with "Ht") as (Φs1 Φs2 ?) "[? Hwp]".
iDestruct (big_sepL2_cons_inv_l with "Hwp") as (Φ Φs3 ->) "[Hwp ?]".
iMod (wp_not_stuck with "Hσ Hwp") as "$"; auto. }
iApply step_fupd_fupd. iApply step_fupd_intro; first done. iNext.
iExists _. iSplitR; first done. iFrame "Hσ".
iApply big_sepL2_fupd.
iApply (big_sepL2_impl with "Hwp").
......@@ -104,15 +117,19 @@ Qed.
End adequacy.
(** Iris's generic adequacy result *)
Theorem wp_strong_adequacy Σ Λ `{!invPreG Σ} es σ1 n κs t2 σ2 φ :
Theorem wp_strong_adequacy Σ Λ `{!invPreG Σ} es σ1 n κs t2 σ2 φ
(num_laters_per_step : nat nat) :
( `{Hinv : !invG Σ},
|={}=>
(s: stuckness)
(stateI : state Λ list (observation Λ) nat iProp Σ)
(stateI : state Λ nat list (observation Λ) nat iProp Σ)
(Φs : list (val Λ iProp Σ))
(fork_post : val Λ iProp Σ),
let _ : irisG Λ Σ := IrisG _ _ Hinv stateI fork_post in
stateI σ1 κs 0
(fork_post : val Λ iProp Σ)
state_interp_mono,
let _ : irisG Λ Σ := IrisG _ _ Hinv stateI fork_post num_laters_per_step
state_interp_mono
in
stateI σ1 0 κs 0
([ list] e;Φ es;Φs, WP e @ s; {{ Φ }})
( es' t2',
(* es' is the final state of the initial threads, t2' the rest *)
......@@ -123,7 +140,7 @@ Theorem wp_strong_adequacy Σ Λ `{!invPreG Σ} es σ1 n κs t2 σ2 φ :
threads in [t2] are not stuck *)
e2, s = NotStuck e2 t2 not_stuck e2 σ2 -
(* The state interpretation holds for [σ2] *)
stateI σ2 [] (length t2') -
stateI σ2 n [] (length t2') -
(* If the initial threads are done, their post-condition [Φ] holds *)
([ list] e;Φ es';Φs, from_option Φ True (to_val e)) -
(* For all forked-off threads that are done, their postcondition
......@@ -138,19 +155,22 @@ Theorem wp_strong_adequacy Σ Λ `{!invPreG Σ} es σ1 n κs t2 σ2 φ :
φ.
Proof.
intros Hwp ?.
eapply (step_fupdN_soundness' _ (S (S n)))=> Hinv. rewrite Nat_iter_S.
iMod Hwp as (s stateI Φ fork_post) "(Hσ & Hwp & Hφ)".
apply (step_fupdN_soundness _ (steps_sum num_laters_per_step 0 n))=> Hinv.
iMod Hwp as (s stateI Φ fork_post state_interp_mono) "(Hσ & Hwp & Hφ)".
iDestruct (big_sepL2_length with "Hwp") as %Hlen1.
iApply step_fupd_intro; [done|]; iModIntro.
iApply step_fupdN_S_fupd. iApply (step_fupdN_wand with "[-Hφ]").
{ iApply (@wptp_strong_adequacy _ _ (IrisG _ _ Hinv stateI fork_post) _ []
with "[Hσ] Hwp"); eauto; by rewrite right_id_L. }
iDestruct 1 as (nt' ?) "(Hσ & Hval) /=".
iMod (@wptp_strong_adequacy _ _
(IrisG _ _ Hinv stateI fork_post num_laters_per_step state_interp_mono) _ []
with "[Hσ] Hwp") as "H"; [done|by rewrite right_id_L|].
iAssert (|={}=>^(steps_sum num_laters_per_step 0 n) |={}=> ⌜φ⌝)%I
with "[-]" as "H"; last first.
{ destruct steps_sum; [done|]. by iApply step_fupdN_S_fupd. }
iApply (step_fupdN_wand with "H").
iMod 1 as (nt' ?) "(Hσ & Hval) /=".
iDestruct (big_sepL2_app_inv_r with "Hval") as (es' t2' ->) "[Hes' Ht2']".
iDestruct (big_sepL2_length with "Ht2'") as %Hlen2.
rewrite replicate_length in Hlen2; subst.
iDestruct (big_sepL2_length with "Hes'") as %Hlen3.
iApply fupd_plain_mask_empty.
rewrite -plus_n_O.
iApply ("Hφ" with "[//] [%] [//] Hσ Hes'"); [congruence|].
by rewrite big_sepL2_replicate_r // big_sepL_omap.
Qed.
......@@ -199,14 +219,17 @@ Corollary wp_adequacy Σ Λ `{!invPreG Σ} s e σ φ :
|={}=>
(stateI : state Λ list (observation Λ) iProp Σ)
(fork_post : val Λ iProp Σ),
let _ : irisG Λ Σ := IrisG _ _ Hinv (λ σ κs _, stateI σ κs) fork_post in
let _ : irisG Λ Σ :=
IrisG _ _ Hinv (λ σ _ κs _, stateI σ κs) fork_post (λ _, 0)
(λ _ _ _ _, fupd_intro _ _)
in
stateI σ κs WP e @ s; {{ v, ⌜φ v }})
adequate s e σ (λ v _, φ v).
Proof.
intros Hwp. apply adequate_alt; intros t2 σ2 [n [κs ?]]%erased_steps_nsteps.
eapply (wp_strong_adequacy Σ _); [|done]=> ?.
iMod Hwp as (stateI fork_post) "[Hσ Hwp]".
iExists s, (λ σ κs _, stateI σ κs), [(λ v, ⌜φ v%I)], fork_post => /=.
iExists s, (λ σ _ κs _, stateI σ κs), [(λ v, ⌜φ v%I)], fork_post, _ => /=.
iIntros "{$Hσ $Hwp} !>" (e2 t2' -> ? ?) "_ H _".
iApply fupd_mask_intro_discard; [done|]. iSplit; [|done].
iDestruct (big_sepL2_cons_inv_r with "H") as (e' ? ->) "[Hwp H]".
......@@ -219,7 +242,8 @@ Corollary wp_invariance Σ Λ `{!invPreG Σ} s e1 σ1 t2 σ2 φ :
|={}=>
(stateI : state Λ list (observation Λ) nat iProp Σ)
(fork_post : val Λ iProp Σ),
let _ : irisG Λ Σ := IrisG _ _ Hinv stateI fork_post in
let _ : irisG Λ Σ := IrisG _ _ Hinv (λ σ _, stateI σ) fork_post
(λ _, 0) (λ _ _ _ _, fupd_intro _ _) in
stateI σ1 κs 0 WP e1 @ s; {{ _, True }}
(stateI σ2 [] (pred (length t2)) - E, |={,E}=> ⌜φ⌝))
rtc erased_step ([e1], σ1) (t2, σ2)
......@@ -228,7 +252,7 @@ Proof.
intros Hwp [n [κs ?]]%erased_steps_nsteps.
eapply (wp_strong_adequacy Σ _); [|done]=> ?.
iMod (Hwp _ κs) as (stateI fork_post) "(Hσ & Hwp & Hφ)".
iExists s, stateI, [(λ _, True)%I], fork_post => /=.
iExists s, (λ σ _, stateI σ), [(λ _, True)%I], fork_post, _ => /=.
iIntros "{$Hσ $Hwp} !>" (e2 t2' -> _ _) "Hσ H _ /=".
iDestruct (big_sepL2_cons_inv_r with "H") as (? ? ->) "[_ H]".
iDestruct (big_sepL2_nil_inv_r with "H") as %->.
......
......@@ -17,15 +17,15 @@ Local Hint Resolve head_stuck_stuck : core.
Lemma wp_lift_head_step_fupd {s E Φ} e1 :
to_val e1 = None
( σ1 κ κs n, state_interp σ1 (κ ++ κs) n ={E,}=
( σ1 ns κ κs nt, state_interp σ1 ns (κ ++ κs) nt ={E,}=
head_reducible e1 σ1
e2 σ2 efs, head_step e1 σ1 κ e2 σ2 efs ={}= |={,E}=>
state_interp σ2 κs (length efs + n)
state_interp σ2 (S ns) κs (length efs + nt)
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 Qs) "Hσ".
iIntros (?) "H". iApply wp_lift_step_fupd=>//. iIntros (σ1 ns κ κs nt) "Hσ".
iMod ("H" with "Hσ") as "[% H]"; iModIntro.
iSplit; first by destruct s; eauto. iIntros (e2 σ2 efs ?).
iApply "H"; eauto.
......@@ -33,26 +33,26 @@ Qed.
Lemma wp_lift_head_step {s E Φ} e1 :
to_val e1 = None
( σ1 κ κs n, state_interp σ1 (κ ++ κs) n ={E,}=
( σ1 ns κ κs nt, state_interp σ1 ns (κ ++ κs) nt ={E,}=
head_reducible e1 σ1
e2 σ2 efs, head_step e1 σ1 κ e2 σ2 efs ={,E}=
state_interp σ2 κs (length efs + n)
state_interp σ2 (S ns) κs (length efs + nt)
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 n, state_interp σ κs n ={E,}= head_stuck e σ⌝)
( σ ns κs nt, state_interp σ ns κs nt ={E,}= head_stuck e σ⌝)
WP e @ E ?{{ Φ }}.
Proof.
iIntros (??) "H". iApply wp_lift_stuck; first done.
iIntros (σ κs n) "Hσ". iMod ("H" with "Hσ") as "%". by auto.
iIntros (σ ns κs nt) "Hσ". iMod ("H" with "Hσ") as "%". by auto.
Qed.
Lemma wp_lift_pure_head_stuck E Φ e :
......@@ -62,51 +62,51 @@ Lemma wp_lift_pure_head_stuck E Φ e :
WP e @ E ?{{ Φ }}.
Proof using Hinh.
iIntros (?? Hstuck). iApply wp_lift_head_stuck; [done|done|].
iIntros (σ κs n) "_". iApply fupd_mask_intro; by auto with set_solver.
iIntros (σ ns κs nt) "_". iApply fupd_mask_intro; by auto with set_solver.
Qed.
Lemma wp_lift_atomic_head_step_fupd {s E1 E2 Φ} e1 :
to_val e1 = None
( σ1 κ κs n, state_interp σ1 (κ ++ κs) n ={E1}=
( σ1 ns κ κs nt, state_interp σ1 ns (κ ++ κs) nt ={E1}=
head_reducible e1 σ1
e2 σ2 efs, head_step e1 σ1 κ e2 σ2 efs ={E1}[E2]=
state_interp σ2 κs (length efs + n)
state_interp σ2 (S ns) κs (length efs + nt)
from_option Φ False (to_val e2)
[ list] ef efs, WP ef @ s; {{ fork_post }})
WP e1 @ s; E1 {{ Φ }}.
Proof.
iIntros (?) "H". iApply wp_lift_atomic_step_fupd; [done|].
iIntros (σ1 κ κs Qs) "Hσ1". iMod ("H" with "Hσ1") as "[% H]"; iModIntro.
iIntros (σ1 ns κ κs nt) "Hσ1". iMod ("H" with "Hσ1") as "[% H]"; iModIntro.
iSplit; first by destruct s; auto. iIntros (e2 σ2 efs Hstep).
iApply "H"; eauto.
Qed.
Lemma wp_lift_atomic_head_step {s E Φ} e1 :
to_val e1 = None
( σ1 κ κs n, state_interp σ1 (κ ++ κs) n ={E}=
( σ1 ns κ κs nt, state_interp σ1 ns (κ ++ κs) nt ={E}=
head_reducible e1 σ1
e2 σ2 efs, head_step e1 σ1 κ e2 σ2 efs ={E}=
state_interp σ2 κs (length efs + n)
state_interp σ2 (S ns) κs (length efs + nt)
from_option Φ False (to_val e2)
[ list] ef efs, WP ef @ s; {{ fork_post }})
WP e1 @ s; E {{ Φ }}.
Proof.
iIntros (?) "H". iApply wp_lift_atomic_step; eauto.
iIntros (σ1 κ κs Qs) "Hσ1". iMod ("H" with "Hσ1") as "[% H]"; iModIntro.
iIntros (σ1 ns κ κs nt) "Hσ1". iMod ("H" with "Hσ1") as "[% H]"; iModIntro.
iSplit; first by destruct s; auto. iNext. iIntros (e2 σ2 efs Hstep).
iApply "H"; eauto.
Qed.
Lemma wp_lift_atomic_head_step_no_fork_fupd {s E1 E2 Φ} e1 :
to_val e1 = None
( σ1 κ κs n, state_interp σ1 (κ ++ κs) n ={E1}=
( σ1 ns κ κs nt, state_interp σ1 ns (κ ++ κs) nt ={E1}=
head_reducible e1 σ1
e2 σ2 efs, head_step e1 σ1 κ e2 σ2 efs ={E1}[E2]=
efs = [] state_interp σ2 κs n from_option Φ False (to_val e2))
efs = [] state_interp σ2 (S ns) κs nt from_option Φ False (to_val e2))
WP e1 @ s; E1 {{ Φ }}.
Proof.
iIntros (?) "H". iApply wp_lift_atomic_head_step_fupd; [done|].
iIntros (σ1 κ κs Qs) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[$ H]"; iModIntro.
iIntros (σ1 ns κ κs nt) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[$ H]"; iModIntro.
iIntros (v2 σ2 efs Hstep).
iMod ("H" $! v2 σ2 efs with "[# //]") as "H".
iIntros "!> !>". iMod "H" as "(-> & ? & ?) /=". by iFrame.
......@@ -114,14 +114,14 @@ Qed.
Lemma wp_lift_atomic_head_step_no_fork {s E Φ} e1 :
to_val e1 = None
( σ1 κ κs n, state_interp σ1 (κ ++ κs) n ={E}=
( σ1 ns κ κs nt, state_interp σ1 ns (κ ++ κs) nt ={E}=
head_reducible e1 σ1
e2 σ2 efs, head_step e1 σ1 κ e2 σ2 efs ={E}=
efs = [] state_interp σ2 κs n from_option Φ False (to_val e2))
efs = [] state_interp σ2 (S ns) κs nt from_option Φ False (to_val e2))
WP e1 @ s; E {{ Φ }}.
Proof.
iIntros (?) "H". iApply wp_lift_atomic_head_step; eauto.
iIntros (σ1 κ κs Qs) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[$ H]"; iModIntro.
iIntros (σ1 ns κ κs nt) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[$ H]"; iModIntro.
iNext; iIntros (v2 σ2 efs Hstep).
iMod ("H" $! v2 σ2 efs with "[//]") as "(-> & ? & ?) /=". by iFrame.
Qed.
......
......@@ -16,23 +16,38 @@ Implicit Types Φ : val Λ → iProp Σ.
Local Hint Resolve reducible_no_obs_reducible : core.
Lemma wp_lift_step_fupdN s E Φ e1 :
to_val e1 = None
( σ1 ns κ κs nt, state_interp σ1 ns (κ ++ κs) nt ={E,}=
if s is NotStuck then reducible e1 σ1 else True
e2 σ2 efs, prim_step e1 σ1 κ e2 σ2 efs
={}=^(S $ num_laters_per_step ns) |={,E}=>
state_interp σ2 (S ns) κs (length efs + nt)
WP e2 @ s; E {{ Φ }}
[ list] ef efs, WP ef @ s; {{ fork_post }})
WP e1 @ s; E {{ Φ }}.
Proof. by rewrite wp_unfold /wp_pre=>->. Qed.
Lemma wp_lift_step_fupd s E Φ e1 :
to_val e1 = None
( σ1 κ κs n, state_interp σ1 (κ ++ κs) n ={E,}=
( σ1 ns κ κs nt, state_interp σ1 ns (κ ++ κs) nt ={E,}=
if s is NotStuck then reducible e1 σ1 else True
e2 σ2 efs, prim_step e1 σ1 κ e2 σ2 efs ={}= |={,E}=>
state_interp σ2 κs (length efs + n)
state_interp σ2 (S ns) κs (length efs + nt)
WP e2 @ s; E {{ Φ }}
[ list] ef efs, WP ef @ s; {{ fork_post }})
WP e1 @ s; E {{ Φ }}.
Proof. by rewrite wp_unfold /wp_pre=>->. Qed.
Proof.
intros ?. rewrite -wp_lift_step_fupdN; [|done]. simpl. do 22 f_equiv.
rewrite -step_fupdN_intro; [|done]. rewrite -bi.laterN_intro. auto.
Qed.
Lemma wp_lift_stuck E Φ e :
to_val e = None