Commit 26b62a4b authored by Robbert Krebbers's avatar Robbert Krebbers

Bump Iris.

parent 1a7c8ecf
Pipeline #20158 passed with stage
in 13 minutes and 30 seconds
......@@ -11,5 +11,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ]
depends: [
"coq-iris" { (= "dev.2019-09-19.0.ca3f9d11") | (= "dev") }
"coq-iris" { (= "dev.2019-09-19.3.aa7871c7") | (= "dev") }
]
......@@ -174,7 +174,7 @@ Section heap.
{ rewrite !heap_mapsto_vec_nil. iIntros "_"; auto. }
rewrite !heap_mapsto_vec_cons. iIntros "[[Hv1 Hvl1] [Hv2 Hvl2]]".
iDestruct (IH (l + 1) with "[$Hvl1 $Hvl2]") as "[% $]"; subst.
rewrite (inj_iff (:: vl2)).
rewrite (inj_iff (.:: vl2)).
iDestruct (heap_mapsto_agree with "[$Hv1 $Hv2]") as %<-.
iSplit; first done. iFrame.
- by iIntros "[% [$ Hl2]]"; subst.
......
......@@ -430,13 +430,13 @@ Qed.
Definition fresh_block (σ : state) : block :=
let loclst : list loc := elements (dom _ σ : gset loc) in
let blockset : gset block := foldr (λ l, ({[l.1]} )) loclst in
let blockset : gset block := foldr (λ l, ({[l.1]} .)) loclst in
fresh blockset.
Lemma is_fresh_block σ i : σ !! (fresh_block σ,i) = None.
Proof.
assert ( (l : loc) ls (X : gset block),
l ls l.1 foldr (λ l, ({[l.1]} )) X ls) as help.
l ls l.1 foldr (λ l, ({[l.1]} .)) X ls) as help.
{ induction 1; set_solver. }
rewrite /fresh_block /shift_loc /= -(not_elem_of_dom (D := gset loc)) -elem_of_elements.
move=> /(help _ _ ) /=. apply is_fresh.
......
......@@ -54,8 +54,8 @@ Module Type lifetime_sig.
Global Declare Instance lft_intersect_comm : Comm (A:=lft) eq ().
Global Declare Instance lft_intersect_assoc : Assoc (A:=lft) eq ().
Global Declare Instance lft_intersect_inj_1 (κ : lft) : Inj eq eq (κ ).
Global Declare Instance lft_intersect_inj_2 (κ : lft) : Inj eq eq ( κ).
Global Declare Instance lft_intersect_inj_1 (κ : lft) : Inj eq eq (κ .).
Global Declare Instance lft_intersect_inj_2 (κ : lft) : Inj eq eq (. κ).
Global Declare Instance lft_intersect_left_id : LeftId eq static meet.
Global Declare Instance lft_intersect_right_id : RightId eq static meet.
......
......@@ -36,14 +36,14 @@ Proof.
iMod (box_empty with "Hbox") as "[HP Hbox]"=>//; first set_solver.
{ intros i s. by rewrite lookup_fmap fmap_Some=> -[? [/HB -> ->]]. }
rewrite lft_vs_unfold; iDestruct "Hvs" as (n) "[Hcnt Hvs]".
iDestruct (big_sepS_filter_acc ( κ) _ _ (dom _ I) with "Halive")
iDestruct (big_sepS_filter_acc (. κ) _ _ (dom _ I) with "Halive")
as "[Halive Halive']".
{ intros κ'. rewrite elem_of_dom. eauto. }
iApply fupd_trans. iApply fupd_mask_mono; first by apply union_subseteq_l.
iMod ("Hvs" $! I with "[HI Halive Hbox Hbor] HP Hκ") as "(Hinv & HQ & Hcnt')".
{ rewrite lft_vs_inv_unfold. iFrame. rewrite /lft_bor_dead.
iExists (dom _ B), P. rewrite !gset_to_gmap_dom -map_fmap_compose.
rewrite (map_fmap_ext _ ((1%Qp,) to_agree) B); last naive_solver.
rewrite (map_fmap_ext _ ((1%Qp,.) to_agree) B); last naive_solver.
iFrame. }
rewrite lft_vs_inv_unfold; iDestruct "Hinv" as "(?&HI&Halive)".
iSpecialize ("Halive'" with "Halive").
......@@ -100,7 +100,7 @@ Proof.
Qed.
Definition kill_set (I : gmap lft lft_names) (Λ : atomic_lft) : gset lft :=
filter (Λ ) (dom (gset lft) I).
filter (Λ .) (dom (gset lft) I).
Lemma elem_of_kill_set I Λ κ : κ kill_set I Λ Λ κ is_Some (I !! κ).
Proof. by rewrite /kill_set elem_of_filter elem_of_dom. Qed.
......
......@@ -74,7 +74,7 @@ Definition to_lft_stateR (b : bool) : lft_stateR :=
if b then Cinl 1%Qp else Cinr ().
Definition to_alftUR : gmap atomic_lft bool alftUR := fmap to_lft_stateR.
Definition to_ilftUR : gmap lft lft_names ilftUR := fmap to_agree.
Definition to_borUR : gmap slice_name bor_state borUR := fmap ((1%Qp,) to_agree).
Definition to_borUR : gmap slice_name bor_state borUR := fmap ((1%Qp,.) to_agree).
Section defs.
Context `{!invG Σ, !lftG Σ}.
......
......@@ -258,8 +258,8 @@ Instance lft_inhabited : Inhabited lft := _.
Instance bor_idx_inhabited : Inhabited bor_idx := _.
Instance lft_intersect_comm : Comm (A:=lft) eq () := _.
Instance lft_intersect_assoc : Assoc (A:=lft) eq () := _.
Instance lft_intersect_inj_1 κ : Inj eq eq (κ ) := _.
Instance lft_intersect_inj_2 κ : Inj eq eq ( κ) := _.
Instance lft_intersect_inj_1 κ : Inj eq eq (κ .) := _.
Instance lft_intersect_inj_2 κ : Inj eq eq (. κ) := _.
Instance lft_intersect_left_id : LeftId eq static () := _.
Instance lft_intersect_right_id : RightId eq static () := _.
......
......@@ -51,7 +51,7 @@ Section lft_contexts.
- iDestruct "H" as "[Hq Hq']".
iDestruct "Hq" as (κ0) "(% & Hq & #?)".
iDestruct "Hq'" as (κ0') "(% & Hq' & #?)". simpl in *.
rewrite (inj ((lft_intersect_list κs) ) κ0' κ0); last congruence.
rewrite (inj ((lft_intersect_list κs) .) κ0' κ0); last congruence.
iExists κ0. by iFrame "∗%".
Qed.
......
......@@ -166,8 +166,8 @@ Section ofe.
Instance type_dist : Dist type := type_dist'.
Let T := prodO
(prodO natO (thread_id -d> list val -d> iProp Σ))
(lft -d> thread_id -d> loc -d> iProp Σ).
(prodO natO (thread_id -d> list val -d> iPropO Σ))
(lft -d> thread_id -d> loc -d> iPropO Σ).
Let P (x : T) : Prop :=
( κ tid l, Persistent (x.2 κ tid l))
( tid vl, x.1.2 tid vl - length vl = x.1.1)
......@@ -231,7 +231,7 @@ Section ofe.
st_dist' n ty1 ty2.
Instance st_dist : Dist simple_type := st_dist'.
Definition st_unpack (ty : simple_type) : thread_id -d> list val -d> iProp Σ :=
Definition st_unpack (ty : simple_type) : thread_id -d> list val -d> iPropO Σ :=
λ tid vl, ty.(ty_own) tid vl.
Definition st_ofe_mixin : OfeMixin simple_type.
......
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