Commit 662b530e authored by Robbert Krebbers's avatar Robbert Krebbers

Bump Iris (⊢ changes).

parent 1f8db35e
Pipeline #25802 passed with stage
in 17 minutes and 55 seconds
......@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iron" ]
depends: [
"coq-iris" { (= "dev.2020-03-10.6.79f576aa") | (= "dev") }
"coq-iris" { (= "dev.2020-03-16.0.62be0a86") | (= "dev") }
]
......@@ -72,7 +72,7 @@ Qed.
terminates, the postcondition hold. *)
Theorem heap_basic_adequacy Σ `{heapPreG Σ} s e σ φ :
( `{heapG Σ},
{{{ [ map] l v σ, l v }}} e @ s; {{{ v, RET v; ⌜φ v }}}%I)
{{{ [ map] l v σ, l v }}} e @ s; {{{ v, RET v; ⌜φ v }}})
adequate s e σ (λ v _, φ v).
Proof.
intros Hwp. apply (heap_adequacy Σ). iIntros (?) "Hall".
......@@ -87,7 +87,7 @@ fact of the given shape. *)
Theorem heap_all_adequacy Σ `{heapPreG Σ} s e σ1 σ2 σ2' v vs φ :
( `{heapG Σ},
([ map] l v σ1, l v)
WP e @ s; {{ v, ([ map] l v σ2, l v) ⌜φ v }}%I )
WP e @ s; {{ v, ([ map] l v σ2, l v) ⌜φ v }})
rtc erased_step ([e], σ1) (of_val <$> v :: vs, σ2')
σ2' = σ2.
Proof.
......
......@@ -73,8 +73,8 @@ Section proofs.
end.
Definition mkList_spec (n : nat) :
( ( (m : nat), Ψ (#m)) -
{{{ emp }}} mkList #n {{{ l, RET l; is_list Ψ l (mkList_ref n) }}})%I.
( (m : nat), Ψ (#m)) -
{{{ emp }}} mkList #n {{{ l, RET l; is_list Ψ l (mkList_ref n) }}}.
Proof.
iIntros "#HΨ".
iLöb as "IH" forall (n).
......
......@@ -72,7 +72,7 @@ Section sts.
by replace ((1 / 2 1 / 2 / 2)%Qp (1 / 2 / 2)%Qp) with 1%Qp
by (apply (bool_decide_unpack _); by compute).
Qed.
Lemma transfer_alloc : (|==> γ, t γ s γ t γ)%I.
Lemma transfer_alloc : |==> γ, t γ s γ t γ.
Proof.
iMod (own_alloc (Excl ())) as (transfer_name) "Htok"; first done.
iMod (own_alloc 1%Qp) as (transfer_name) "[Ht₁ [Hs₁ Ht₂]]"; first done.
......
......@@ -26,7 +26,7 @@ Proof. solve_inG. Qed.
has terminated. *)
Theorem iron_wp_adequacy Σ Λ `{ironInvPreG Σ} s e σ φ π π' :
( `{Hinv : invG Σ} κs,
(|={}=>
|={}=>
(perm : frac iProp Σ)
(stateI : state Λ list(observation Λ) nat iProp Σ)
(fork_post : val Λ iProp Σ)
......@@ -38,7 +38,7 @@ Theorem iron_wp_adequacy Σ Λ `{ironInvPreG Σ} s e σ φ π π' :
P
<affine> π1 π2 σ m, π ? π' = π1 ? π2 -
stateI σ [] m - perm π1 - P π2 ={,}= ⌜φ v σ⌝
}} π')%I)
}} π')
adequate s e σ φ.
Proof.
intros Hwp. apply adequate_alt; intros t2 σ2 [n [κs ?]]%erased_steps_nsteps.
......@@ -60,7 +60,7 @@ postconditions of all forked-off threads [ [∗] Qs ] to establish the meta-leve
post-condition [φ]. *)
Theorem iron_wp_all_adequacy Σ Λ `{ironInvPreG Σ} s e σ1 σ2 v vs φ π π' :
( `{Hinv : invG Σ} κs,
(|={}=>
|={}=>
(perm : frac iProp Σ)
(stateI : state Λ list(observation Λ) nat iProp Σ)
(fork_post : val Λ iProp Σ)
......@@ -74,7 +74,7 @@ Theorem iron_wp_all_adequacy Σ Λ `{ironInvPreG Σ} s e σ1 σ2 v vs φ π π'
stateI σ2 [] (length vs) -
([ list] v vs, fork_post v) -
perm π1 - P π2 ={,}= ⌜φ v
}} π')%I)
}} π')
rtc erased_step ([e], σ1) (of_val <$> v :: vs, σ2)
φ v.
Proof.
......
......@@ -115,8 +115,8 @@ Global Instance fcinv_persistent N γ P : Persistent (fcinv N γ P).
Proof. rewrite fcinv_eq. apply _. Qed.
Lemma fcinv_alloc_strong E N :
(|={E}=> γ, fcinv_own γ 1
P, P ={E}= fcinv N γ P fcinv_cancel_own γ 1)%I.
|={E}=> γ, fcinv_own γ 1
P, P ={E}= fcinv N γ P fcinv_cancel_own γ 1.
Proof.
rewrite fcinv_eq fcinv_own_eq fcinv_cancel_own_eq.
iStartProof (iProp _); iIntros (π1) "Hp".
......
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