Commit 26b60a28 authored by Ralf Jung's avatar Ralf Jung

bump Iris

parent 4b943421
...@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"] ...@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"] install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris_atomic"] remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris_atomic"]
depends: [ depends: [
"coq-iris" { (= "dev.2018-07-13.2.af5611c8") | (= "dev") } "coq-iris" { (= "dev.2018-10-31.4.4a1eb8a3") | (= "dev") }
] ]
...@@ -107,7 +107,7 @@ Section proof. ...@@ -107,7 +107,7 @@ Section proof.
{{{ p ts, RET #p; installed_recp ts x Q inv N (p_inv R γm γr ts p) }}}. {{{ p ts, RET #p; installed_recp ts x Q inv N (p_inv R γm γr ts p) }}}.
Proof. Proof.
iIntros (Φ) "(#? & HP & Hf) HΦ". iIntros (Φ) "(#? & HP & Hf) HΦ".
wp_seq. wp_let. wp_let. wp_alloc p as "Hl". wp_lam. wp_pures. wp_alloc p as "Hl".
iApply fupd_wp. iApply fupd_wp.
iMod (own_alloc (Excl ())) as (γ1) "Ho1"; first done. iMod (own_alloc (Excl ())) as (γ1) "Ho1"; first done.
iMod (own_alloc (Excl ())) as (γ3) "Ho3"; first done. iMod (own_alloc (Excl ())) as (γ3) "Ho3"; first done.
...@@ -151,10 +151,10 @@ Section proof. ...@@ -151,10 +151,10 @@ Section proof.
by apply pair_l_frac_op'. } by apply pair_l_frac_op'. }
wp_load. iMod ("Hclose" with "[-Hf' Ho1 Hx2 HoQ HR HΦ Hpx]"). wp_load. iMod ("Hclose" with "[-Hf' Ho1 Hx2 HoQ HR HΦ Hpx]").
{ iNext. iFrame. iFrame "#". iRight. iRight. iLeft. iExists f, x. iFrame. } { iNext. iFrame. iFrame "#". iRight. iRight. iLeft. iExists f, x. iFrame. }
iModIntro. wp_match. wp_proj. wp_proj. iModIntro. wp_match. wp_pures.
wp_bind (f _). iApply wp_wand_r. iSplitL "Hpx Hf' HR". wp_bind (f _). iApply wp_wand_r. iSplitL "Hpx Hf' HR".
{ iApply "Hf'". iFrame. } { iApply "Hf'". iFrame. }
iIntros (v) "[HR HQ]". iIntros (v) "[HR HQ]". wp_pures.
iInv N as "Hx" "Hclose". iInv N as "Hx" "Hclose".
iDestruct "Hx" as "[Hp | [Hp | [Hp | Hp]]]"; subst. iDestruct "Hx" as "[Hp | [Hp | [Hp | Hp]]]"; subst.
* iDestruct "Hp" as (?) "(_ & >Ho1' & _)". * iDestruct "Hp" as (?) "(_ & >Ho1' & _)".
...@@ -215,7 +215,7 @@ Section proof. ...@@ -215,7 +215,7 @@ Section proof.
is_lock N γlk lk (own γr (Excl ()) R) Φ #() is_lock N γlk lk (own γr (Excl ()) R) Φ #()
WP try_srv lk #s {{ Φ }}. WP try_srv lk #s {{ Φ }}.
Proof. Proof.
iIntros "(#? & #? & HΦ)". wp_seq. wp_let. iIntros "(#? & #? & HΦ)". wp_lam. wp_pures.
wp_bind (try_acquire _). iApply (try_acquire_spec with "[]"); first done. wp_bind (try_acquire _). iApply (try_acquire_spec with "[]"); first done.
iNext. iIntros ([]); last by (iIntros; wp_if). iNext. iIntros ([]); last by (iIntros; wp_if).
iIntros "[Hlocked [Ho2 HR]]". iIntros "[Hlocked [Ho2 HR]]".
...@@ -271,16 +271,16 @@ Section proof. ...@@ -271,16 +271,16 @@ Section proof.
Proof. Proof.
iIntros (R Φ) "HR HΦ". iIntros (R Φ) "HR HΦ".
iMod (own_alloc (Excl ())) as (γr) "Ho2"; first done. iMod (own_alloc (Excl ())) as (γr) "Ho2"; first done.
wp_seq. wp_bind (newlock _). wp_lam. wp_bind (newlock _).
iApply (newlock_spec _ (own γr (Excl ()) R)%I with "[$Ho2 $HR]")=>//. iApply (newlock_spec _ (own γr (Excl ()) R)%I with "[$Ho2 $HR]")=>//.
iNext. iIntros (lk γlk) "#Hlk". iNext. iIntros (lk γlk) "#Hlk".
wp_let. wp_bind (new_stack _). wp_let. wp_bind (new_stack _).
iApply (new_bag_spec N (p_inv' R γm γr))=>//. iApply (new_bag_spec N (p_inv' R γm γr))=>//.
iNext. iIntros (s) "#Hss". iNext. iIntros (s) "#Hss".
wp_let. iApply "HΦ". rewrite /synced. wp_pures. iApply "HΦ". rewrite /synced.
iAlways. iIntros (f). wp_let. iAlways. iAlways. iIntros (f). wp_pures. iAlways.
iIntros (P Q x) "#Hf". iIntros (P Q x) "#Hf".
iIntros "!# Hp". wp_let. wp_bind (install _ _ _). iIntros "!# Hp". wp_pures. wp_bind (install _ _ _).
iApply (install_spec R P Q f x γm γr s with "[-]")=>//. iApply (install_spec R P Q f x γm γr s with "[-]")=>//.
{ iFrame. iFrame "#". } { iFrame. iFrame "#". }
iNext. iIntros (p [[[[γx γ1] γ3] γ4] γq]) "[(Ho3 & Hx & HoQ) #?]". iNext. iIntros (p [[[[γx γ1] γ3] γ4] γq]) "[(Ho3 & Hx & HoQ) #?]".
......
...@@ -47,7 +47,7 @@ Section proofs. ...@@ -47,7 +47,7 @@ Section proofs.
{{{ True }}} new_stack #() {{{ s, RET #s; bag_inv s }}}. {{{ True }}} new_stack #() {{{ s, RET #s; bag_inv s }}}.
Proof. Proof.
iIntros (Φ) "_ HΦ". iApply wp_fupd. iIntros (Φ) "_ HΦ". iApply wp_fupd.
wp_seq. wp_bind (ref NONE)%E. wp_alloc l as "Hl". wp_lam. wp_bind (ref NONE)%E. wp_alloc l as "Hl".
wp_alloc s as "Hs". wp_alloc s as "Hs".
iAssert (( xs, is_bag_R N R xs s))%I with "[-HΦ]" as "Hxs". iAssert (( xs, is_bag_R N R xs s))%I with "[-HΦ]" as "Hxs".
{ iFrame. iExists [], l. { iFrame. iExists [], l.
......
...@@ -22,12 +22,12 @@ Section syncer. ...@@ -22,12 +22,12 @@ Section syncer.
Lemma mk_sync_spec: mk_syncer_spec mk_sync. Lemma mk_sync_spec: mk_syncer_spec mk_sync.
Proof. Proof.
iIntros (R Φ) "HR HΦ". iIntros (R Φ) "HR HΦ".
wp_seq. wp_bind (newlock _). wp_lam. wp_bind (newlock _).
iApply (newlock_spec N R with "[HR]"); first done. iNext. iApply (newlock_spec N R with "[HR]"); first done. iNext.
iIntros (lk γ) "#Hl". wp_let. iApply "HΦ". iIntros "!#". iIntros (lk γ) "#Hl". wp_pures. iApply "HΦ". iIntros "!#".
iIntros (f). wp_let. iAlways. iIntros (f). wp_pures. iAlways.
iIntros (P Q x) "#Hf !# HP". iIntros (P Q x) "#Hf !# HP".
wp_let. wp_bind (acquire _). wp_pures. wp_bind (acquire _).
iApply (acquire_spec with "Hl"). iNext. iApply (acquire_spec with "Hl"). iNext.
iIntros "[Hlocked R]". wp_seq. wp_bind (f _). iIntros "[Hlocked R]". wp_seq. wp_bind (f _).
iSpecialize ("Hf" with "[R HP]"); first by iFrame. iSpecialize ("Hf" with "[R HP]"); first by iFrame.
......
...@@ -91,7 +91,7 @@ Section proof. ...@@ -91,7 +91,7 @@ Section proof.
(Φ: val iProp Σ), (Φ: val iProp Σ),
( s, is_stack s [] - Φ #s) WP new_stack #() {{ Φ }}. ( s, is_stack s [] - Φ #s) WP new_stack #() {{ Φ }}.
Proof. Proof.
iIntros (Φ) "HΦ". wp_seq. iIntros (Φ) "HΦ". wp_lam.
wp_bind (ref NONE)%E. wp_alloc l as "Hl". wp_bind (ref NONE)%E. wp_alloc l as "Hl".
wp_alloc l' as "Hl'". wp_alloc l' as "Hl'".
iApply "HΦ". rewrite /is_stack. iExists l. iApply "HΦ". rewrite /is_stack. iExists l.
...@@ -144,7 +144,7 @@ Section proof. ...@@ -144,7 +144,7 @@ Section proof.
iDestruct "Hhd" as (q) "[Hhd Hhd']". iDestruct "Hhd" as (q) "[Hhd Hhd']".
iMod ("Hvs'" with "[-Hhd]") as "HQ". iMod ("Hvs'" with "[-Hhd]") as "HQ".
{ iFrame. eauto. } { iFrame. eauto. }
iModIntro. wp_let. wp_load. wp_match. iModIntro. wp_let. wp_load. wp_pures.
eauto. eauto.
- simpl. iDestruct "Hhd" as (hd' q) "([[Hhd1 Hhd2] Hhd'] & Hxs')". - simpl. iDestruct "Hhd" as (hd' q) "([[Hhd1 Hhd2] Hhd'] & Hxs')".
iDestruct (dup_is_list with "[Hxs']") as "[Hxs1 Hxs2]"; first by iFrame. iDestruct (dup_is_list with "[Hxs']") as "[Hxs1 Hxs2]"; first by iFrame.
...@@ -166,7 +166,7 @@ Section proof. ...@@ -166,7 +166,7 @@ Section proof.
iDestruct (uniq_is_list with "[Hxs1 Hxs'']") as "%"; first by iFrame. subst. iDestruct (uniq_is_list with "[Hxs1 Hxs'']") as "%"; first by iFrame. subst.
repeat (iSplitR "Hxs1 Hs"; first done). repeat (iSplitR "Hxs1 Hs"; first done).
iFrame. } iFrame. }
iModIntro. wp_if. wp_proj. eauto. iModIntro. wp_if. wp_pures. eauto.
+ wp_cas_fail. iDestruct "Hvs'" as "[Hvs' _]". + wp_cas_fail. iDestruct "Hvs'" as "[Hvs' _]".
iMod ("Hvs'" with "[-]") as "HP"; first by iFrame. iMod ("Hvs'" with "[-]") as "HP"; first by iFrame.
iModIntro. wp_if. by iApply "IH". iModIntro. wp_if. by iApply "IH".
......
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