Commit 1ddda46e authored by Ralf Jung's avatar Ralf Jung

bump Iris

parent eac03c6a
......@@ -9,7 +9,7 @@ dev-repo: "git+https://gitlab.mpi-sws.org/FP/iris-examples.git"
synopsis: "A collection of case studies for Iris"
depends: [
"coq-iris" { (= "dev.2020-02-01.2.dba20c7f") | (= "dev") }
"coq-iris" { (= "dev.2020-02-14.2.a3cea59c") | (= "dev") }
"coq-autosubst" { = "dev.coq86" }
]
......
......@@ -145,7 +145,7 @@ Section gc.
Lemma make_gc l v E: gcN E gc_inv - l v ={E}= gc_mapsto l v.
Proof.
iIntros (HN) "#Hinv Hl".
iMod (inv_open_timeless _ gcN _ with "Hinv") as "[P Hclose]"=>//.
iMod (inv_acc_timeless _ gcN _ with "Hinv") as "[P Hclose]"=>//.
iDestruct "P" as (gcm) "[H● HsepM]".
destruct (gcm !! l) as [v' | ] eqn: Hlookup.
- (* auth map contains l --> contradiction *)
......@@ -205,7 +205,7 @@ Section gc.
(l v ( w, l w == gc_mapsto l w |={E gcN, E}=> True)).
Proof.
iIntros (HN) "#Hinv".
iMod (inv_open_timeless _ gcN _ with "Hinv") as "[P Hclose]"=>//.
iMod (inv_acc_timeless _ gcN _ with "Hinv") as "[P Hclose]"=>//.
iIntros "!>" (l v) "Hgc_l".
iDestruct "P" as (gcm) "[H● HsepM]".
iDestruct (gc_mapsto_lookup_Some with "Hgc_l H●") as %Hsome.
......@@ -227,7 +227,7 @@ Section gc.
Lemma is_gc_access l E: gcN E gc_inv - is_gc_loc l ={E, E gcN}= v, l v (l v ={E gcN, E}= True).
Proof.
iIntros (HN) "#Hinv Hgc_l".
iMod (inv_open_timeless _ gcN _ with "Hinv") as "[P Hclose]"=>//.
iMod (inv_acc_timeless _ gcN _ with "Hinv") as "[P Hclose]"=>//.
iModIntro.
iDestruct "P" as (gcm) "[H● HsepM]".
iDestruct (is_gc_lookup_Some with "Hgc_l H●") as %Hsome.
......
......@@ -47,7 +47,7 @@ Section Helpers.
Proof.
iIntros (Hgx) "(#Hgr & Hx & key)".
wp_lam; wp_bind (! _)%E. unfold graph_ctx.
iMod (cinv_open with "Hgr key") as "(>Hinv & key & Hcl)"; first done.
iMod (cinv_acc with "Hgr key") as "(>Hinv & key & Hcl)"; first done.
unfold graph_inv at 2.
iDestruct "Hinv" as (G) "(Hi1 & Hi2 & Hi3 & Hi4)".
iDestruct (graph_open with "[Hi1 Hi3]") as
......@@ -63,7 +63,7 @@ Section Helpers.
iModIntro. wp_proj. wp_let.
destruct u as [u1 u2]; simpl.
wp_bind (CmpXchg _ _ _).
iMod (cinv_open _ graphN with "Hgr key")
iMod (cinv_acc _ graphN with "Hgr key")
as "(>Hinv & key & Hclose)"; first done.
unfold graph_inv at 2.
iDestruct "Hinv" as (G') "(Hi1 & Hi2 & Hi3 & Hi4)".
......@@ -128,7 +128,7 @@ Section Helpers.
assert (Hgx' : x dom (gset _) g).
{ rewrite elem_of_dom Hgx; eauto. }
unfold graph_ctx.
iMod (cinv_open _ graphN with "Hgr key")
iMod (cinv_acc _ graphN with "Hgr key")
as "(>Hinv & key & Hclose)"; first done.
unfold graph_inv at 2.
iDestruct "Hinv" as (G) "(Hi1 & Hi2 & Hi3 & Hi4)".
......@@ -165,7 +165,7 @@ Section Helpers.
assert (Hgx' : x dom (gset _) g).
{ rewrite elem_of_dom Hgx; eauto. }
unfold graph_ctx. wp_pures.
iMod (cinv_open _ graphN with "Hgr key")
iMod (cinv_acc _ graphN with "Hgr key")
as "(>Hinv & key & Hclose)"; first done.
unfold graph_inv at 2.
iDestruct "Hinv" as (G) "(Hi1 & Hi2 & Hi3 & Hi4)".
......
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