Commit 80ffd297 authored by Robbert Krebbers's avatar Robbert Krebbers

Bump Iris.

parent 37145a3b
Pipeline #14873 passed with stage
in 12 minutes and 34 seconds
...@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"] ...@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
install: [make "install"] install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris_examples"] remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris_examples"]
depends: [ depends: [
"coq-iris" { (= "dev.2019-02-18.1.a1cf5cb9") | (= "dev") } "coq-iris" { (= "dev.2019-02-20.0.8a8c1405") | (= "dev") }
"coq-autosubst" { = "dev.coq86" } "coq-autosubst" { = "dev.coq86" }
] ]
...@@ -122,7 +122,7 @@ Proof. ...@@ -122,7 +122,7 @@ Proof.
as ([p I]) "(% & [Hl Hr] & Hclose)"; eauto. as ([p I]) "(% & [Hl Hr] & Hclose)"; eauto.
destruct p; [|done]. wp_store. destruct p; [|done]. wp_store.
iSpecialize ("HΦ" with "[#]") => //. iFrame "HΦ". iSpecialize ("HΦ" with "[#]") => //. iFrame "HΦ".
iMod ("Hclose" $! (State High I) ( : set token) with "[-]"); last done. iMod ("Hclose" $! (State High I) ( : propset token) with "[-]"); last done.
iSplit; [iPureIntro; by eauto using signal_step|]. iSplit; [iPureIntro; by eauto using signal_step|].
rewrite /barrier_inv /ress /=. iNext. iFrame "Hl". rewrite /barrier_inv /ress /=. iNext. iFrame "Hl".
iDestruct "Hr" as (Ψ) "[Hr Hsp]"; iExists Ψ; iFrame "Hsp". iDestruct "Hr" as (Ψ) "[Hr Hsp]"; iExists Ψ; iFrame "Hsp".
......
...@@ -19,7 +19,7 @@ Inductive prim_step : relation state := ...@@ -19,7 +19,7 @@ Inductive prim_step : relation state :=
| ChangeI p I2 I1 : prim_step (State p I1) (State p I2) | ChangeI p I2 I1 : prim_step (State p I1) (State p I2)
| ChangePhase I : prim_step (State Low I) (State High I). | ChangePhase I : prim_step (State Low I) (State High I).
Definition tok (s : state) : set token := Definition tok (s : state) : propset token :=
{[ t | i, t = Change i i state_I s ]} {[ t | i, t = Change i i state_I s ]}
(if state_phase s is High then {[ Send ]} else ). (if state_phase s is High then {[ Send ]} else ).
Global Arguments tok !_ /. Global Arguments tok !_ /.
...@@ -27,10 +27,10 @@ Global Arguments tok !_ /. ...@@ -27,10 +27,10 @@ Global Arguments tok !_ /.
Canonical Structure sts := sts.Sts prim_step tok. Canonical Structure sts := sts.Sts prim_step tok.
(* The set of states containing some particular i *) (* The set of states containing some particular i *)
Definition i_states (i : gname) : set state := {[ s | i state_I s ]}. Definition i_states (i : gname) : propset state := {[ s | i state_I s ]}.
(* The set of low states *) (* The set of low states *)
Definition low_states : set state := {[ s | state_phase s = Low ]}. Definition low_states : propset state := {[ s | state_phase s = Low ]}.
Lemma i_states_closed i : sts.closed (i_states i) {[ Change i ]}. Lemma i_states_closed i : sts.closed (i_states i) {[ Change i ]}.
Proof. Proof.
...@@ -77,7 +77,7 @@ Proof. ...@@ -77,7 +77,7 @@ Proof.
- destruct p; set_solver. - destruct p; set_solver.
- apply elem_of_equiv=> /= -[j|]; last set_solver. - apply elem_of_equiv=> /= -[j|]; last set_solver.
set_unfold; rewrite !(inj_iff Change). set_unfold; rewrite !(inj_iff Change).
assert (Change j match p with Low => : set token | High => {[Send]} end False) assert (Change j match p with Low => : propset token | High => {[Send]} end False)
as -> by (destruct p; set_solver). as -> by (destruct p; set_solver).
destruct (decide (i1 = j)) as [->|]; first naive_solver. destruct (decide (i1 = j)) as [->|]; first naive_solver.
destruct (decide (i2 = j)) as [->|]; first naive_solver. destruct (decide (i2 = j)) as [->|]; first naive_solver.
......
...@@ -62,7 +62,7 @@ Section proof. ...@@ -62,7 +62,7 @@ Section proof.
end. end.
Definition bag_inv (γb : gname) (b : loc) : iProp Σ := Definition bag_inv (γb : gname) (b : loc) : iProp Σ :=
( ls : list val, b (val_of_list ls) own γb ((1/2)%Qp, to_agree (of_list ls)))%I. ( ls : list val, b (val_of_list ls) own γb ((1/2)%Qp, to_agree (list_to_set ls)))%I.
Definition is_bag (γb : gname) (x : val) := Definition is_bag (γb : gname) (x : val) :=
( (lk : val) (b : loc) (γ : gname), ( (lk : val) (b : loc) (γ : gname),
......
...@@ -91,7 +91,7 @@ Section proof. ...@@ -91,7 +91,7 @@ Section proof.
Definition bag_inv (γb : gname) (b : loc) : iProp Σ := Definition bag_inv (γb : gname) (b : loc) : iProp Σ :=
( (hd : val) (ls : list val), ( (hd : val) (ls : list val),
b hd is_list hd ls own γb ((1/2)%Qp, to_agree (of_list ls)))%I. b hd is_list hd ls own γb ((1/2)%Qp, to_agree (list_to_set ls)))%I.
Definition is_bag (γb : gname) (x : val) := Definition is_bag (γb : gname) (x : val) :=
( (b : loc), x = #b inv N (bag_inv γb b))%I. ( (b : loc), x = #b inv N (bag_inv γb b))%I.
Definition bag_contents (γb : gname) (X : gmultiset val) : iProp Σ := Definition bag_contents (γb : gname) (X : gmultiset val) : iProp Σ :=
......
...@@ -57,7 +57,7 @@ Section Graphs. ...@@ -57,7 +57,7 @@ Section Graphs.
z t connected g z front g t t t = dom (gset _) g. z t connected g z front g t t t = dom (gset _) g.
Proof. Proof.
intros Hz Hc [Hsb Hdt]. intros Hz Hc [Hsb Hdt].
apply collection_equiv_spec_L; split; trivial. apply set_equiv_spec_L; split; trivial.
apply elem_of_subseteq => x Hx. destruct (Hc x Hx) as [p pv]. apply elem_of_subseteq => x Hx. destruct (Hc x Hx) as [p pv].
clear Hc Hx; revert z Hz pv. clear Hc Hx; revert z Hz pv.
induction p => z Hz pv. induction p => z Hz pv.
......
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