Commit 1046aa23 authored by Joseph Tassarotti's avatar Joseph Tassarotti
Browse files

Fix wp_pre', allow credits in adequacy

parent 3ba09d5b
......@@ -137,7 +137,7 @@ 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 k σ1 n κs t2 σ2 φ
(num_laters_per_step : nat nat) :
( `{Hinv : !invG Σ},
|={}=>
......@@ -149,7 +149,7 @@ Theorem wp_strong_adequacy Σ Λ `{!invPreG Σ} es σ1 n κs t2 σ2 φ
let _ : irisG Λ Σ := IrisG _ _ Hinv stateI fork_post num_laters_per_step
state_interp_mono
in
stateI σ1 0 κs 0
stateI σ1 k κs 0
([ list] e;Φ es;Φs, WP e @ s; {{ Φ }})
( es' t2',
(* es' is the final state of the initial threads, t2' the rest *)
......@@ -160,7 +160,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 n [] (length t2') -
stateI σ2 (n + k) [] (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
......@@ -175,7 +175,7 @@ Theorem wp_strong_adequacy Σ Λ `{!invPreG Σ} es σ1 n κs t2 σ2 φ
φ.
Proof.
intros Hwp ?.
apply (step_fupdN_soundness _ (steps_sum num_laters_per_step 0 n + (S (S (num_laters_per_step n)))))=> Hinv.
apply (step_fupdN_soundness _ (steps_sum num_laters_per_step k n + (S (S (num_laters_per_step (n + k))))))=> Hinv.
iMod Hwp as (s stateI Φ fork_post state_interp_mono) "(Hσ & Hwp & Hφ)".
iDestruct (big_sepL2_length with "Hwp") as %Hlen1.
iMod (@wptp_strong_adequacy _ _
......@@ -190,7 +190,7 @@ Proof.
iApply step_fupdN_S_fupd.
iApply step_fupdN_intro; first auto.
iApply step_fupd_intro; first auto.
iNext. iNext. rewrite -plus_n_O. iNext. iMod "Hclose".
iNext. iNext. iNext. iMod "Hclose".
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.
......@@ -239,7 +239,7 @@ Proof.
right; exists (t2' ++ e3 :: t2'' ++ efs), σ3, κ; econstructor; eauto.
Qed.
Corollary wp_adequacy' Σ Λ `{!invPreG Σ} s e σ φ (num_laters_per_step : nat nat) :
Corollary wp_adequacy' Σ Λ `{!invPreG Σ} s e σ φ (num_laters_per_step : nat nat) k :
( `{Hinv : !invG Σ} κs,
|={}=>
(stateI : state Λ nat list (observation Λ) nat iProp Σ)
......@@ -249,7 +249,7 @@ Corollary wp_adequacy' Σ Λ `{!invPreG Σ} s e σ φ (num_laters_per_step : nat
IrisG _ _ Hinv stateI fork_post num_laters_per_step
state_interp_mono
in
stateI σ 0 κs 0 WP e @ s; {{ v, ⌜φ v }})
stateI σ k κs 0 WP e @ s; {{ v, ⌜φ v }})
adequate s e σ (λ v _, φ v).
Proof.
intros Hwp. apply adequate_alt; intros t2 σ2 [n [κs ?]]%erased_steps_nsteps.
......@@ -276,7 +276,7 @@ Corollary wp_adequacy Σ Λ `{!invPreG Σ} s e σ φ :
adequate s e σ (λ v _, φ v).
Proof.
intros Hwp. apply adequate_alt; intros t2 σ2 [n [κs ?]]%erased_steps_nsteps.
eapply (wp_strong_adequacy Σ _); [|done]=> ?.
eapply (wp_strong_adequacy Σ _ _ 0); [|done]=> ?.
iMod Hwp as (stateI fork_post) "[Hσ Hwp]".
iExists s, (λ σ _ κs _, stateI σ κs), [(λ v, ⌜φ v%I)], fork_post, _ => /=.
iIntros "{$Hσ $Hwp} !>" (e2 t2' -> ? ?) "_ H _".
......@@ -299,7 +299,7 @@ Corollary wp_invariance Σ Λ `{!invPreG Σ} s e1 σ1 t2 σ2 φ :
φ.
Proof.
intros Hwp [n [κs ?]]%erased_steps_nsteps.
eapply (wp_strong_adequacy Σ _); [|done]=> ?.
eapply (wp_strong_adequacy Σ _ _ 0); [|done]=> ?.
iMod (Hwp _ κs) as (stateI fork_post) "(Hσ & Hwp & Hφ)".
iExists s, (λ σ _, stateI σ), [(λ _, True)%I], fork_post, _ => /=.
iIntros "{$Hσ $Hwp} !>" (e2 t2' -> _ _) "Hσ H _ /=".
......
......@@ -81,6 +81,20 @@ Existing Instance wp'.
Lemma wp_eq `{!irisG Λ Σ} : wp = @wp_def Λ Σ _.
Proof. rewrite -wp_aux.(seal_eq) //. Qed.
Definition wp_pre' `{!irisG Λ Σ} (s : stuckness)
(next : coPset -d> expr Λ -d> (val Λ -d> iPropO Σ) -d> iPropO Σ) :
coPset -d> expr Λ -d> (val Λ -d> iPropO Σ) -d> iPropO Σ := λ E e1 Φ,
match to_val e1 with
| Some v => |={E}=> Φ v
| None => σ1 ns κ κs nt,
state_interp σ1 ns (κ ++ κs) nt ={E,}= |={}=>^(S $ num_laters_per_step ns)
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 ns) κs (length efs + nt)
next E e2 Φ
[ list] i ef efs, wp s ef fork_post
end%I.
Section wp.
Context `{!irisG Λ Σ}.
Implicit Types s : stuckness.
......@@ -129,11 +143,11 @@ Qed.
Lemma wp_value_fupd' s E Φ v : WP of_val v @ s; E {{ Φ }} ⊣⊢ |={E}=> Φ v.
Proof. rewrite wp_unfold /wp_pre to_of_val. auto. Qed.
Lemma wp_pre_wand s E e Φ Ψ next :
Lemma wp_pre'_wand s E e Φ Ψ next :
( e, next E e Φ - ( v, Φ v ={E}= Ψ v) - next E e Ψ) -
wp_pre s next E e Φ - ( v, Φ v ={E}= Ψ v) - wp_pre s next E e Ψ.
wp_pre' s next E e Φ - ( v, Φ v ={E}= Ψ v) - wp_pre' s next E e Ψ.
Proof.
iIntros "#Hwand H HΦ". rewrite /wp_pre /=.
iIntros "#Hwand H HΦ". rewrite /wp_pre' /=.
destruct (to_val e) as [v|] eqn:?.
{ iApply ("HΦ" with "[> -]"). eauto. }
iIntros (σ1 ns κ κs nt) "Hσ".
......@@ -147,11 +161,10 @@ Proof.
- eauto.
Qed.
(*
Lemma wp_pre_wand2 s E e Φ next1 next2 :
wp_pre s next1 E e Φ - ( E e' Φ, next1 E e' Φ - next2 E e' Φ) - wp_pre s next2 E e Φ.
Lemma wp_pre'_wand2 s E e Φ next1 next2 :
wp_pre' s next1 E e Φ - ( E e' Φ, next1 E e' Φ - next2 E e' Φ) - wp_pre' s next2 E e Φ.
Proof.
iIntros "H HΦ". rewrite /wp_pre /=.
iIntros "H HΦ". rewrite /wp_pre' /=.
destruct (to_val e) as [v|] eqn:?.
{ eauto. }
iIntros (σ1 ns κ κs nt) "Hσ".
......@@ -162,10 +175,8 @@ Proof.
iMod ("H" with "[//]") as "H".
iDestruct "H" as "($ & H & Hefs)". iModIntro. iSplitR "Hefs".
- iApply ("HΦ" with "[$]").
- iApply (big_sepL_impl with "Hefs"); iIntros "!>" (k ef _).
- eauto.
Qed.
*)
Lemma wp_strong_mono s1 s2 E1 E2 e Φ Ψ :
s1 s2 E1 E2
......@@ -181,25 +192,25 @@ Proof.
iApply (step_fupdN_wand with "H"). iNext.
iIntros "[% H]".
iSplit; [by destruct s1, s2|]. iIntros (e2 σ2 efs Hstep).
iMod ("H" with "[//]") as "H".
iMod ("H" with "[//]") as "H".
iDestruct "H" as "($ & H & Hefs)". iMod "Hclose" as "_". iModIntro. iSplitR "Hefs".
- iApply ("IH" with "[//] H HΦ").
- iApply (big_sepL_impl with "Hefs"); iIntros "!>" (k ef _).
iIntros "H". iApply ("IH" with "[] H"); auto.
Qed.
Lemma fupd_wp_pre s E next e Φ : (|={E}=> wp_pre s next E e Φ) wp_pre s next E e Φ.
Lemma fupd_wp_pre' s E next e Φ : (|={E}=> wp_pre' s next E e Φ) wp_pre' s next E e Φ.
Proof.
rewrite /wp_pre. iIntros "H". destruct (to_val e) as [v|] eqn:?.
rewrite /wp_pre'. iIntros "H". destruct (to_val e) as [v|] eqn:?.
{ by iMod "H". }
iIntros (σ1 ns κ κs nt) "Hσ1". iMod "H". by iApply "H".
Qed.
Lemma wp_pre_fupd s E next e Φ :
Lemma wp_pre'_fupd s E next e Φ :
( e Φ, next E e (λ v, |={E}=> Φ v) - next E e Φ) -
(wp_pre s next E e (λ v, |={E}=> Φ v)) - wp_pre s next E e Φ.
(wp_pre' s next E e (λ v, |={E}=> Φ v)) - wp_pre' s next E e Φ.
Proof.
rewrite /wp_pre. iIntros "#Hnext H". destruct (to_val e) as [v|] eqn:?.
rewrite /wp_pre'. iIntros "#Hnext H". destruct (to_val e) as [v|] eqn:?.
{ by iMod "H". }
iIntros (σ1 ns κ κs nt) "Hσ1". iMod ("H" with "[$]") as "H". iModIntro.
iApply (step_fupdN_wand with "H"). iIntros "($&H)".
......@@ -213,6 +224,7 @@ Proof.
{ by iMod "H". }
iIntros (σ1 ns κ κs nt) "Hσ1". iMod "H". by iApply "H".
Qed.
Lemma wp_fupd s E e Φ : WP e @ s; E {{ v, |={E}=> Φ v }} WP e @ s; E {{ Φ }}.
Proof. iIntros "H". iApply (wp_strong_mono s s E with "H"); auto. Qed.
......@@ -250,13 +262,12 @@ Qed.
Lemma wp_fupd_weaken_unroll s E1 E2 e Φ :
to_val e = None
( σ1 κ e2 σ2 efs, prim_step e σ1 κ e2 σ2 efs efs = [])
E1 E2
((|={E1,E2}=> True) - wp_pre s (λ _ e Φ, |={E1, E2}=> wp (PROP:=iProp Σ) s E2 e Φ) E1 e Φ) -
((|={E1,E2}=> True) - wp_pre' s (λ _ e Φ, |={E1, E2}=> wp (PROP:=iProp Σ) s E2 e Φ) E1 e Φ) -
WP e @ s; E2 {{ Φ }}.
Proof.
iIntros (Hnval Hnofork HE) "Hwp".
rewrite wp_unfold /wp_pre.
iIntros (Hnval HE) "Hwp".
rewrite wp_unfold /wp_pre' /wp_pre.
rewrite Hnval.
iIntros (σ1 ns κ κs nt) "Hσ".
iApply (fupd_mask_weaken E1); auto. iIntros "Hclo".
......@@ -266,8 +277,7 @@ Proof.
iIntros "[$ H]".
iIntros (e2 σ2 efs Hstep).
iMod ("H" with "[//]") as "(Hinterp&Hwp&Hefs)".
iMod "Hwp". iFrame. eauto. iApply (fupd_mask_weaken E1); auto. iIntros "Hclo".
rewrite (Hnofork _ _ _ _ _ Hstep) //=.
iMod "Hwp". iFrame. eauto.
Qed.
(*
......@@ -294,12 +304,11 @@ Proof.
Qed.
*)
Lemma wp_pre_atomic next E1 E2 e s Φ :
Lemma wp_pre'_atomic next E1 E2 e s Φ :
to_val e = None
( σ1 κ e2 σ2 efs, prim_step e σ1 κ e2 σ2 efs efs = [])
(|={E1,E2}=> wp_pre s (λ E e Φ, |={E2, E1}=> next E1 e Φ) E2 e Φ) wp_pre s next E1 e Φ.
(|={E1,E2}=> wp_pre' s (λ E e Φ, |={E2, E1}=> next E1 e Φ) E2 e Φ) wp_pre' s next E1 e Φ.
Proof.
iIntros (Hnval Hnofork) "H". rewrite /wp_pre.
iIntros (Hnval) "H". rewrite /wp_pre'.
rewrite Hnval.
iIntros (σ1 ns κ κs nt) "Hσ". iMod "H".
iMod ("H" $! σ1 with "Hσ") as "H". iModIntro.
......@@ -307,19 +316,7 @@ Proof.
iIntros "[% H]". iSplit; first done.
iIntros (e2 σ2 efs Hstep).
iMod ("H" with "[//]") as "(Hσ & H & Hefs)".
(*
destruct s.
- rewrite !wp_unfold /wp_pre. destruct (to_val e2) as [v2|] eqn:He2.
+ iDestruct "H" as ">> $". by iFrame.
+ iFrame. iMod (fupd_mask_subseteq E1) as "Hclose"; first done.
iModIntro. iIntros (?????) "Hσ".
iMod "Hclose".
iMod ("H" $! _ _ [] with "[$]") as "H". iModIntro.
iApply (step_fupdN_wand with "H").
iIntros "[H _]". iDestruct "H" as %(? & ? & ? & ? & ?).
edestruct (atomic _ _ _ _ _ Hstep); eauto.
*)
iMod "H". rewrite (Hnofork _ _ _ _ _ Hstep) //=. iFrame. eauto.
iMod "H". iFrame. eauto.
Qed.
Lemma wp_atomic E1 E2 e Φ `{!Atomic StronglyAtomic e} :
......@@ -339,7 +336,7 @@ Proof.
- rewrite !wp_unfold /wp_pre. destruct (to_val e2) as [v2|] eqn:He2.
+ iDestruct "H" as ">> $". by iFrame.
+ iFrame. iMod (fupd_mask_subseteq E1) as "Hclose"; first done.
iModIntro. iIntros (?????) "Hσ".
iModIntro. iIntros (?????) "Hσ".
iMod "Hclose".
iMod ("H" $! _ _ [] with "[$]") as "H". iModIntro.
iApply (step_fupdN_wand with "H").
......
......@@ -18,6 +18,30 @@ Definition heapΣ : gFunctors :=
Global Instance subG_heapPreG {Σ} : subG heapΣ Σ heapPreG Σ.
Proof. solve_inG. Qed.
Definition heap_adequacy' Σ `{!heapPreG Σ} s e σ φ k :
( `{!heapG Σ}, cred_frag' k inv_heap_inv - WP e @ s; {{ v, ⌜φ v }})
adequate s e σ (λ v _, φ v).
Proof.
intros Hwp; eapply (wp_adequacy' _ _); iIntros (? κs) "".
iMod (gen_heap_init σ.(heap)) as (?) "[Hh _]".
iMod (inv_heap_init loc (option val)) as (?) ">Hi".
iMod (proph_map_init κs σ.(used_proph_id)) as (?) "Hp".
iMod (own_alloc (F 0 F 0)) as (γ) "[Hγ Hγ']";
first by apply auth_both_valid_discrete.
set (hG := (HeapG _ _ _ _ _ _ γ)).
iAssert (cred_interp 0) with "[Hγ Hγ']" as "Hcσ".
{ rewrite /cred_interp. iFrame. iExists _; iFrame. }
iMod (cred_interp_incr_k _ k with "Hcσ") as "(Hcσ&Hfrag)".
iExists
(λ σ ns κs nt, (cred_interp ns gen_heap_interp σ.(heap) proph_map_interp κs σ.(used_proph_id))%I),
(λ _, True%I), _.
iFrame.
iModIntro.
iApply (Hwp (HeapG _ _ _ _ _ _ γ) with "[Hfrag] [$]").
{ destruct k; eauto. }
Qed.
Definition heap_adequacy Σ `{!heapPreG Σ} s e σ φ :
( `{!heapG Σ}, inv_heap_inv - WP e @ s; {{ v, ⌜φ v }})
adequate s e σ (λ v _, φ v).
......
......@@ -40,6 +40,17 @@ Proof.
iFrame. iExists _. eauto.
Qed.
Lemma cred_auth_frag_incr_k (ns n k: nat) :
cred_auth ns cred_frag n ==
cred_auth (ns + k) cred_frag (n + k).
Proof.
iIntros "(Hγ&Hγf)".
iDestruct "Hγf" as (q) "Hγf".
iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]".
{ apply frac_auth_update, (nat_local_update _ _ (ns + k) (n + k)); lia. }
iFrame. iExists _. eauto.
Qed.
Lemma cred_auth_frag_decr (ns n: nat) :
cred_auth ns cred_frag (S n) ==
ns', ns = S ns' cred_auth ns' cred_frag n.
......@@ -97,6 +108,15 @@ Proof.
eauto.
Qed.
Lemma cred_interp_incr_k ns k :
cred_interp ns == cred_interp (ns + k) cred_frag k.
Proof.
iIntros "H".
iMod (cred_auth_frag_incr_k _ _ k with "H") as "(?&H)".
iDestruct (cred_frag_split with "H") as "($&$)".
eauto.
Qed.
Lemma cred_interp_decr ns n :
cred_interp ns cred_frag (S n) ==
ns', ns = S ns' cred_interp ns' cred_frag n.
......@@ -201,13 +221,13 @@ Proof.
iExists _. iModIntro. iFrame. eauto.
Qed.
Lemma wp_pre_pure_later_cred s E e1 e2 next φ Φ :
Lemma wp_pre'_pure_later_cred s E e1 e2 next φ Φ :
PureExec φ 1 e1 e2 φ (cred_frag 1 - next E e2 Φ) -
wp_pre s next E e1 Φ.
wp_pre' s next E e1 Φ.
Proof.
iIntros (HPure Hφ) "Hwp".
rewrite /PureExec in HPure. apply HPure in Hφ.
rewrite /wp_pre.
rewrite /wp_pre'.
assert (language.to_val e1 = None) as ->.
{
eapply (reducible_not_val _ inhabitant), reducible_no_obs_reducible.
......@@ -235,16 +255,16 @@ Lemma wp_pure_later_cred s E e1 e2 φ Φ :
PureExec φ 1 e1 e2 φ (cred_frag 1 - WP e2 @ s; E {{ v, Φ v }}) - WP e1 @ s; E {{ v, Φ v }}.
Proof.
iIntros (HPure Hφ) "Hwp".
iEval (rewrite wp_unfold). iApply (wp_pre_pure_later_cred with "[$]"); auto.
iEval (rewrite wp_unfold). iApply (wp_pre'_pure_later_cred with "[$]"); auto.
Qed.
Lemma wp_pre_pure_later_cred_n s E e1 e2 next φ Φ n :
Lemma wp_pre'_pure_later_cred_n s E e1 e2 next φ Φ n :
PureExec φ 1 e1 e2 φ cred_frag n - ^(S n) (cred_frag (S n) - next E e2 Φ) -
wp_pre s next E e1 Φ.
wp_pre' s next E e1 Φ.
Proof.
iIntros (HPure Hφ) "Hfrag Hwp".
rewrite /PureExec in HPure. apply HPure in Hφ.
rewrite /wp_pre.
rewrite /wp_pre'.
assert (language.to_val e1 = None) as ->.
{
eapply (reducible_not_val _ inhabitant), reducible_no_obs_reducible.
......@@ -274,7 +294,7 @@ Lemma wp_pure_later_cred_n s E e1 e2 φ Φ n :
^(S n) (cred_frag (S n) - WP e2 @ s; E {{ v, Φ v }}) - WP e1 @ s; E {{ v, Φ v }}.
Proof.
iIntros (HPure Hφ) "Hfrag Hwp".
iEval (rewrite wp_unfold). iApply (wp_pre_pure_later_cred_n with "[$]"); auto.
iEval (rewrite wp_unfold). iApply (wp_pre'_pure_later_cred_n with "[$]"); auto.
Qed.
Definition cred_frag' n :=
......@@ -283,14 +303,14 @@ Definition cred_frag' n :=
| _ => cred_frag n
end.
Lemma wp_pre_pure_later_cred_n' s E e1 e2 next φ Φ n :
Lemma wp_pre'_pure_later_cred_n' s E e1 e2 next φ Φ n :
PureExec φ 1 e1 e2 φ cred_frag' n - ^(S n) (cred_frag' (S n) - next E e2 Φ) -
wp_pre s next E e1 Φ.
wp_pre' s next E e1 Φ.
Proof.
iIntros (HPure Hφ) "Hfrag Hwp".
destruct n.
- simpl. iApply wp_pre_pure_later_cred; auto.
- simpl. iApply (wp_pre_pure_later_cred_n with "[$]"); auto.
- simpl. iApply wp_pre'_pure_later_cred; auto.
- simpl. iApply (wp_pre'_pure_later_cred_n with "[$]"); auto.
Qed.
Lemma wp_pure_later_cred_n' s E e1 e2 φ Φ n :
......@@ -303,15 +323,14 @@ Proof.
- simpl. iApply (wp_pure_later_cred_n with "[$]"); auto.
Qed.
Lemma wp_pre_later_cred_use next s E e Φ :
Lemma wp_pre'_later_cred_use next s E e Φ :
language.to_val e = None
( σ1 κ e2 σ2 efs, prim_step e σ1 κ e2 σ2 efs efs = [])
cred_frag 1 -
(wp_pre s (λ E e Φ, cred_frag 1 - next E e Φ) E e Φ) -
wp_pre s next E e Φ.
(wp_pre' s (λ E e Φ, cred_frag 1 - next E e Φ) E e Φ) -
wp_pre' s next E e Φ.
Proof.
iIntros (Hnval Hnofork) "Hcred Hwp".
rewrite /wp_pre.
iIntros (Hnval) "Hcred Hwp".
rewrite /wp_pre'.
rewrite Hnval.
iIntros (σ1 ns κ κs nt) "Hσ".
iMod (state_interp_step_decr with "[$]") as (ns' ->) "(Hσ&Hcred)".
......@@ -324,8 +343,7 @@ Proof.
iIntros (??? Hstep). iMod ("H" with "[//]") as "(Hσ&Hwp&Hefs)".
iMod (state_interp_step_incr' _ _ _ 0 with "[$]") as "(Hσ&Hcred')".
iFrame. iModIntro.
rewrite (Hnofork _ _ _ _ _ Hstep) //=.
iFrame "Hefs". iApply "Hwp". eauto.
iApply "Hwp". eauto.
Qed.
Lemma wp_later_cred_use s E e Φ :
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment