Commit 0a1a5875 authored by Ralf Jung's avatar Ralf Jung

bump Iris

parent b6ee7aa6
Pipeline #24234 passed with stage
in 10 minutes and 31 seconds
...@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"] ...@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"] install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iron" ] remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iron" ]
depends: [ depends: [
"coq-iris" { (= "dev.2020-01-23.2.e2f65bbd") | (= "dev") } "coq-iris" { (= "dev.2020-02-14.2.a3cea59c") | (= "dev") }
] ]
...@@ -21,7 +21,7 @@ Section proof. ...@@ -21,7 +21,7 @@ Section proof.
iIntros "#Hinv !#" (Φ) "Hown Hcont". iIntros "#Hinv !#" (Φ) "Hown Hcont".
wp_let. wp_let.
wp_bind (FAA _ _). wp_bind (FAA _ _).
iMod (cinv_open_strong with "Hinv Hown") iMod (cinv_acc_strong with "Hinv Hown")
as "([Hℓ | [Hℓ Hown']] & Hown & Hclose)"; first set_solver. as "([Hℓ | [Hℓ Hown']] & Hown & Hclose)"; first set_solver.
- wp_apply (wp_faa with "Hℓ"). - wp_apply (wp_faa with "Hℓ").
rewrite -{4}(Qp_div_2 π) Some_op mapsto_uniform. rewrite -{4}(Qp_div_2 π) Some_op mapsto_uniform.
......
...@@ -17,7 +17,7 @@ Section special. ...@@ -17,7 +17,7 @@ Section special.
rewrite fcinv_eq fcinv_own_eq fcinv_cancel_own_eq. iStartProof (iProp _). rewrite fcinv_eq fcinv_own_eq fcinv_cancel_own_eq. iStartProof (iProp _).
iIntros (? π1) "#[-> ?]"; iIntros (?) "[-> Hγinv]". iIntros (πc) "Hcancel". iIntros (? π1) "#[-> ?]"; iIntros (?) "[-> Hγinv]". iIntros (πc) "Hcancel".
iIntros (π2) "Hp". iIntros (π2) "Hp".
iMod (cinv_open_strong _ N with "[$] [$]") as "(Hinv & Hγinv & Hclose)"; first done. iMod (cinv_acc_strong _ N with "[$] [$]") as "(Hinv & Hγinv & Hclose)"; first done.
iDestruct "Hinv" as (π21 π22) "(>Hγauth & >Hp' & Hspecial)". iDestruct "Hinv" as (π21 π22) "(>Hγauth & >Hp' & Hspecial)".
rewrite {2}/special. rewrite {2}/special.
rewrite /bi_or /= {1}fracPred_or_eq. rewrite /bi_or /= {1}fracPred_or_eq.
......
...@@ -147,7 +147,7 @@ Lemma fcinv_open_strong E N γ p P `{!Uniform P} : ...@@ -147,7 +147,7 @@ Lemma fcinv_open_strong E N γ p P `{!Uniform P} :
Proof. Proof.
rewrite fcinv_eq fcinv_own_eq fcinv_cancel_own_eq. iStartProof (iProp _). rewrite fcinv_eq fcinv_own_eq fcinv_cancel_own_eq. iStartProof (iProp _).
iIntros (? π1) "#[-> ?]"; iIntros (?) "[-> Hγinv]"; iIntros (π2) "Hp". iIntros (? π1) "#[-> ?]"; iIntros (?) "[-> Hγinv]"; iIntros (π2) "Hp".
iMod (cinv_open_strong _ N with "[$] [$]") as "(Hinv & Hγinv & Hclose)"; first done. iMod (cinv_acc_strong _ N with "[$] [$]") as "(Hinv & Hγinv & Hclose)"; first done.
iDestruct "Hinv" as (π21 π22) "(>Hγauth & >Hp' & HP)". iDestruct "Hinv" as (π21 π22) "(>Hγauth & >Hp' & HP)".
iAssert ( π3 π4, π2 = π3 ? π4 perm (π3 (π21 ? π22)) P π4)%I iAssert ( π3 π4, π2 = π3 ? π4 perm (π3 (π21 ? π22)) P π4)%I
with "[Hp Hp' HP]" as (π3 π4) "(>-> & >[Hp Hp'] & HP)". with "[Hp Hp' HP]" as (π3 π4) "(>-> & >[Hp Hp'] & 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