Commit 407c8b0a authored by Ralf Jung's avatar Ralf Jung

bump Iris

parent a054f077
Pipeline #24437 passed with stage
in 25 minutes and 40 seconds
*.vo
*.vio
*.v.d
*.vok
*.vos
.Makefile.coq.d
.coqdeps.d
*.glob
*.cache
......
......@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iris-c" ]
depends: [
"coq-iris" { (= "dev.2020-02-01.2.dba20c7f") | (= "dev") }
"coq-iris" { (= "dev.2020-02-14.2.a3cea59c") | (= "dev") }
]
......@@ -211,7 +211,7 @@ Section cwp_rules.
iIntros (γ env l I) "#Hlock1 Hres #Heq1". wp_pures.
wp_apply (acquire_flock_spec with "[$]").
iIntros "Hfl".
iMod (flocked_inv_open with "Hfl") as "[HI Hcl]"; first done.
iMod (flocked_inv_acc with "Hfl") as "[HI Hcl]"; first done.
iRewrite "Heq1" in "HI".
iDestruct "HI" as "[Henv HR]".
wp_pures; simpl.
......@@ -245,7 +245,7 @@ Section cwp_rules.
iIntros (γ env l I) "#Hlock Hres #Heq". wp_pures.
wp_apply (acquire_flock_spec with "[$]").
iIntros "Hfl".
iMod (flocked_inv_open with "Hfl") as "[HI Hcl]"; first done.
iMod (flocked_inv_acc with "Hfl") as "[HI Hcl]"; first done.
iRewrite "Heq" in "HI".
iDestruct "HI" as "[Henv HR]".
wp_pures; simpl.
......
......@@ -399,7 +399,7 @@ Section flock.
Qed.
(** `flocked` supports invariant access just like regular invariants *)
Lemma flocked_inv_open_single E γ ρ πR I :
Lemma flocked_inv_acc_single E γ ρ πR I :
resN E
I !! ρ = Some πR
flocked γ I ={E}=
......@@ -410,13 +410,13 @@ Section flock.
iIntros "(Hst & Hfa & Htokens)".
rewrite (big_sepM_lookup_acc _ I ρ (π,R)) //.
iDestruct "Htokens" as "[(T2 & #Hinv & Hρ) Htokens]".
iMod (cinv_open with "Hinv Hρ") as "(HC & Hρ & Hcl)"; first solve_ndisj.
iMod (cinv_acc with "Hinv Hρ") as "(HC & Hρ & Hcl)"; first solve_ndisj.
rewrite /C /=. iDestruct "HC" as "[[HR >T1] | >T2']"; last first.
{ iDestruct (own_valid_2 with "T2 T2'") as %?. done. }
iMod ("Hcl" with "[T2]") as "_".
{ iNext. iRight. done. }
iModIntro. iFrame "HR". iIntros "HR".
iMod (cinv_open with "Hinv Hρ") as "(HC & Hρ & Hcl)"; first solve_ndisj.
iMod (cinv_acc with "Hinv Hρ") as "(HC & Hρ & Hcl)"; first solve_ndisj.
iDestruct "HC" as "[[? >T1'] | >T2]".
{ iDestruct (own_valid_2 with "T1 T1'") as %?. done. }
iMod ("Hcl" with "[T1 HR]") as "_".
......@@ -425,7 +425,7 @@ Section flock.
iFrame "Hst Hfa". iApply "Htokens". by iFrame.
Qed.
Lemma flocked_inv_open E γ I :
Lemma flocked_inv_acc E γ I :
resN E
flocked γ I ={E}=
([ map] ρ πR I, πR.2)
......@@ -447,7 +447,7 @@ Section flock.
iClear "IH".
(* The main induction step *)
iMod (cinv_open with "Hinv Hρ") as "(HC & Hρ & Hcl)"; first solve_ndisj.
iMod (cinv_acc with "Hinv Hρ") as "(HC & Hρ & Hcl)"; first solve_ndisj.
rewrite /C /=. iDestruct "HC" as "[[HR >T1] | >T2']"; last first.
{ iDestruct (own_valid_2 with "T2 T2'") as %?. done. }
iMod ("Hcl" with "[T2]") as "_".
......@@ -455,7 +455,7 @@ Section flock.
iModIntro. iFrame "HR". iIntros "[HR HRs]".
iMod ("IH'" with "HRs") as "$".
iMod (cinv_open with "Hinv Hρ") as "(HC & Hρ & Hcl)"; first solve_ndisj.
iMod (cinv_acc with "Hinv Hρ") as "(HC & Hρ & Hcl)"; first solve_ndisj.
iDestruct "HC" as "[[? >T1'] | >$]".
{ iDestruct (own_valid_2 with "T1 T1'") as %?. done. }
iMod ("Hcl" with "[T1 HR]") as "_".
......
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