Commit e09691b5 authored by Robbert Krebbers's avatar Robbert Krebbers

Bump Iris.

parent ee701141
Pipeline #17445 passed with stage
in 15 minutes and 28 seconds
......@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iron" ]
depends: [
"coq-iris" { (= "dev.2019-06-11.8.a51fa3cf") | (= "dev") }
"coq-iris" { (= "dev.2019-06-12.3.1a0c5860") | (= "dev") }
]
......@@ -41,14 +41,17 @@ Theorem iron_wp_adequacy Σ Λ `{ironInvPreG Σ} s e σ φ π π' :
}} π')%I)
adequate s e σ φ.
Proof.
intros Hwp. apply (wp_strong_adequacy Σ _)=> ? κs.
intros Hwp. apply adequate_alt; intros t2 σ2 [n [κs ?]]%erased_steps_nsteps.
eapply (wp_strong_adequacy Σ _); [|done]=> ?.
iMod Hwp as (perm stateI fork_post ?? P) "(Hσ&Hp&Hwp)". clear Hwp.
iExists stateI, fork_post. iIntros "!> {$Hσ}".
rewrite iron_wp_eq /=. iSpecialize ("Hwp" with "Hp"). iApply (wp_wand with "Hwp").
iIntros (v). iDestruct 1 as (π1 π2' ->) "[Hp H]". rewrite fracPred_at_sep.
iExists stateI, _, fork_post. iIntros "!> {$Hσ}".
rewrite iron_wp_eq /=. iSplitL. iApply ("Hwp" with "Hp").
iIntros (e2 t2' -> Hsafe) "Hσ Hpost _". rewrite bi.pure_and; iFrame (Hsafe).
iIntros (v t2'' [= -> <-]). rewrite to_of_val /=.
iDestruct "Hpost" as (π1 π2' ->) "[Hp H]". rewrite fracPred_at_sep.
iDestruct "H" as (π2 π2b ->) "[HP H]". rewrite fracPred_at_affinely.
iDestruct "H" as (->) "H". rewrite fracPred_at_embed bi.affinely_elim.
iIntros (σ' ?) "Hσ". iApply ("H" with "[] Hσ Hp HP"). by rewrite right_id_L.
iApply ("H" with "[] Hσ Hp HP"). by rewrite right_id_L.
Qed.
(* A generic version of adeqacy for correct usage of resources: this applies
......@@ -75,13 +78,16 @@ Theorem iron_wp_all_adequacy Σ Λ `{ironInvPreG Σ} s e σ1 σ2 v vs φ π π'
rtc erased_step ([e], σ1) (of_val <$> v :: vs, σ2)
φ v.
Proof.
intros Hwp [n [κs Hsteps]]%erased_steps_nsteps. revert Hsteps.
apply (wp_strong_all_adequacy Σ _ s)=>?.
iMod Hwp as (perm stateI fork_post ?? P) "(Hσ&Hp&Hwp)". clear Hwp v.
iExists stateI, fork_post. iIntros "!> {$Hσ}".
rewrite iron_wp_eq /=. iSpecialize ("Hwp" with "Hp"). iApply (wp_wand with "Hwp").
iIntros (v). iDestruct 1 as (π1 π2' ->) "[Hp H]". rewrite fracPred_at_sep.
assert ( vs : list (val Λ), omap to_val (of_val <$> vs) = vs) as Hmap_val.
{ intros vs'. induction vs'; csimpl; rewrite ?to_of_val; auto with f_equal. }
intros Hwp [n [κs Hsteps]]%erased_steps_nsteps.
eapply (wp_strong_adequacy Σ _); [|done]=> ?.
iMod Hwp as (perm stateI fork_post ?? P) "(Hσ&Hp&Hwp)".
iExists stateI, _, fork_post. iIntros "!> {$Hσ}"; csimpl.
rewrite iron_wp_eq /=. iSplitL. iApply ("Hwp" with "Hp").
iIntros (?? [= <- <-] _) "Hσ". rewrite fmap_length to_of_val Hmap_val.
iDestruct 1 as (π1 π2' ->) "[Hp H]". rewrite fracPred_at_sep.
iDestruct "H" as (π2 π2b ->) "[HP H]". rewrite fracPred_at_affinely.
iDestruct "H" as (->) "H". rewrite fracPred_at_embed bi.affinely_elim.
iIntros "Hσ HQs". iApply ("H" with "[//] Hσ HQs Hp"). by rewrite right_id_L.
iIntros "HQs". iApply ("H" with "[//] Hσ HQs Hp"). by rewrite right_id_L.
Qed.
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