Commit 8e90f022 authored by Robbert Krebbers's avatar Robbert Krebbers

Bump Iris.

parent 32a6cf2d
Pipeline #26176 passed with stage
in 19 minutes and 9 seconds
......@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/actris" ]
depends: [
"coq-iris" { (= "dev.2020-04-02.4.739cc004") | (= "dev") }
"coq-iris" { (= "dev.2020-04-04.2.c2367a65") | (= "dev") }
]
......@@ -61,8 +61,6 @@ Definition recv : val :=
end.
(** * Setup of Iris's cameras *)
Definition chanN := nroot .@ "chan".
Class chanG Σ := {
chanG_lockG :> lockG Σ;
chanG_protoG :> protoG Σ val;
......@@ -92,7 +90,7 @@ Definition iProto_mapsto_def `{!heapG Σ, !chanG Σ}
(c : val) (p : iProto Σ) : iProp Σ :=
γ s (l r : loc) (lk : val),
c = ((#(side_elim s l r), #(side_elim s r l)), lk)%V
is_lock chanN (chan_lock_name γ) lk ( vsl vsr,
is_lock (chan_lock_name γ) lk ( vsl vsr,
llist sbi_internal_eq l vsl
llist sbi_internal_eq r vsr
iProto_ctx (chan_proto_name γ) vsl vsr)
......@@ -199,7 +197,7 @@ Section channel.
wp_apply (lnil_spec sbi_internal_eq with "[//]"); iIntros (l) "Hl".
wp_apply (lnil_spec sbi_internal_eq with "[//]"); iIntros (r) "Hr".
iMod (iProto_init p) as (γp) "(Hctx & Hcl & Hcr)".
wp_apply (newlock_spec chanN ( vsl vsr,
wp_apply (newlock_spec ( vsl vsr,
llist sbi_internal_eq l vsl llist sbi_internal_eq r vsr
iProto_ctx γp vsl vsr) with "[Hl Hr Hctx]").
{ iExists [], []. iFrame. }
......
......@@ -281,7 +281,7 @@ Proof.
- iMod contribution_init as (γ) "Hs".
iMod (alloc_client with "Hs") as "[Hs Hcl1]".
iMod (alloc_client with "Hs") as "[Hs Hcl2]".
wp_apply (newlock_spec nroot ( n, server γ n ε
wp_apply (newlock_spec ( n, server γ n ε
c iProto_dual (prot_lock n))%I
with "[Hc Hs]"); first by eauto with iFrame.
iIntros (lk γlk) "#Hlk".
......
......@@ -90,7 +90,7 @@ Section map.
Lemma par_map_worker_spec γl γ vmap lk c :
map_spec vmap -
{{{ is_lock nroot γl lk (map_worker_lock_inv γ c) client γ ( : gmultiset A) }}}
{{{ is_lock γl lk (map_worker_lock_inv γ c) client γ ( : gmultiset A) }}}
par_map_worker vmap lk c
{{{ RET #(); True }}}.
Proof.
......@@ -130,7 +130,7 @@ Section map.
Lemma par_map_workers_spec γl γ n vmap lk c :
map_spec vmap -
{{{ is_lock nroot γl lk (map_worker_lock_inv γ c)
{{{ is_lock γl lk (map_worker_lock_inv γ c)
[] replicate n (client γ (:gmultiset A)) }}}
par_map_workers #n vmap lk c
{{{ RET #(); True }}}.
......@@ -153,7 +153,7 @@ Section map.
Proof.
iIntros "#Hf !>"; iIntros (Φ) "Hc HΦ". wp_lam; wp_pures.
iMod (contribution_init_pow (A:=gmultisetUR A) n) as (γ) "[Hs Hγs]".
wp_apply (newlock_spec nroot (map_worker_lock_inv γ c) with "[Hc Hs]").
wp_apply (newlock_spec (map_worker_lock_inv γ c) with "[Hc Hs]").
{ iExists n, . iFrame. }
iIntros (lk γl) "#Hlk".
wp_apply (par_map_workers_spec with "Hf [$Hlk $Hγs]"); auto.
......
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