From 54937df19e965c0d7b098db067ca6b19a588ba15 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 30 Sep 2020 09:35:54 +0200
Subject: [PATCH] update dependencies; fix for auth changes
---
opam | 2 +-
theories/lang/arc.v | 12 ++++++------
theories/lang/arc_cmra.v | 16 ++++++++--------
theories/lifetime/model/accessors.v | 16 ++++++++--------
theories/lifetime/model/borrow_sep.v | 6 +++---
theories/lifetime/model/boxes.v | 4 ++--
theories/lifetime/model/creation.v | 4 ++--
theories/lifetime/model/faking.v | 4 ++--
theories/lifetime/model/primitive.v | 6 +++---
theories/lifetime/model/reborrow.v | 6 +++---
theories/typing/lib/rc/rc.v | 14 +++++++-------
theories/typing/lib/rc/weak.v | 10 +++++-----
theories/typing/lib/refcell/ref_code.v | 4 ++--
theories/typing/lib/refcell/refmut_code.v | 4 ++--
theories/typing/lib/rwlock/rwlock.v | 4 ++--
15 files changed, 56 insertions(+), 56 deletions(-)
diff --git a/opam b/opam
index 36332e3a..eb9277d0 100644
--- a/opam
+++ b/opam
@@ -16,7 +16,7 @@ This branch uses a proper weak memory model.
"""
depends: [
- "coq-gpfsl" { (= "dev.2020-09-15.0.f118e18e") | (= "dev") }
+ "coq-gpfsl" { (= "dev.2020-09-30.0.50bc07aa") | (= "dev") }
]
build: [make "-j%{jobs}%"]
diff --git a/theories/lang/arc.v b/theories/lang/arc.v
index f0c472fd..43454d35 100644
--- a/theories/lang/arc.v
+++ b/theories/lang/arc.v
@@ -606,10 +606,10 @@ Section arc.
rewrite -5!(@pair_op (prodUR (authUR strong_stUR) (authUR weak_stUR))
(prodUR (prodUR move_selfUR move_otherUR) move_otherUR)).
rewrite /= -2!pair_op /= !left_id /=. split.
- { by split; apply auth_both_valid. }
+ { by split; apply auth_both_valid_discrete. }
do 2 setoid_rewrite <-pair_op. rewrite /= !left_id !right_id.
- split; split; [..|by apply auth_both_valid|by apply auth_auth_valid];
- (split; [by apply auth_both_valid|rewrite /= right_id]);
+ split; split; [..|by apply auth_both_valid_discrete|by apply auth_auth_valid];
+ (split; [by apply auth_both_valid_discrete|rewrite /= right_id]);
[|rewrite left_id]; by apply auth_auth_valid. }
iDestruct "Own" as (γsw)
"(SA & St & WA & SMA & [SM1 SM2] & SDA & [SD1 SD2] & WUA & WU & [S1 S2])".
@@ -663,10 +663,10 @@ Section arc.
rewrite -4!(@pair_op (prodUR (authUR strong_stUR) (authUR weak_stUR))
(prodUR (prodUR move_selfUR move_otherUR) move_otherUR)).
rewrite /= -2!pair_op /= !left_id /=. split.
- { by split; apply auth_both_valid. }
+ { by split; apply auth_both_valid_discrete. }
do 2 setoid_rewrite <-pair_op. rewrite /= !left_id !right_id.
- split; split; [..|by apply auth_both_valid|by apply auth_auth_valid];
- (split; [by apply auth_both_valid|rewrite /= right_id]);
+ split; split; [..|by apply auth_both_valid_discrete|by apply auth_auth_valid];
+ (split; [by apply auth_both_valid_discrete|rewrite /= right_id]);
[|rewrite left_id]; by apply auth_auth_valid. }
iDestruct "Own" as (γsw) "(SA & WA & Wt & SMA & SM & SDA & SD & WUA & [WU1 WU2])".
iMod (view_inv_alloc_frac N _ (1/2 + 1/2/2) (1/2/2)) as (γi) "[[tok2 tok1] VI]";
diff --git a/theories/lang/arc_cmra.v b/theories/lang/arc_cmra.v
index ce111fe8..b0c3e88c 100644
--- a/theories/lang/arc_cmra.v
+++ b/theories/lang/arc_cmra.v
@@ -195,14 +195,14 @@ Section ArcGhost.
✓ (moveSAuth Mt1 ⋅ moveSMain q Mt2) → Mt2 = Mt1.
Proof.
rewrite -pair_op right_id.
- move => [/= /auth_both_valid [/Some_included
+ move => [/= /auth_both_valid_discrete [/Some_included
[[_ /= /to_agree_inj /to_latT_inj /leibniz_equiv_iff //]|
/prod_included[_ /to_agree_included /to_latT_inj /leibniz_equiv_iff //]]_]_].
Qed.
Lemma arc_ghost_move_self_cert_valid Mt1 Mt2:
✓ (moveSAuth Mt1 ⋅ certS Mt2) → Mt2 ⊆ Mt1.
- Proof. rewrite -pair_op => [[_ /auth_both_valid [/latT_included // _]]]. Qed.
+ Proof. rewrite -pair_op => [[_ /auth_both_valid_discrete [/latT_included // _]]]. Qed.
Lemma StrongMoveAuth_agree γ Mt q Mt':
StrongMoveAuth γ Mt ∗ StrMoves γ q Mt' -∗ ⌜Mt = Mt'⌝.
@@ -259,7 +259,7 @@ Section ArcGhost.
✓ (moveOAuth Mt1 ⋅ moveOMain 1%Qp Mt2) → Mt2 = Mt1.
Proof.
rewrite -pair_op.
- move => [/= /auth_both_valid [/Some_included
+ move => [/= /auth_both_valid_discrete [/Some_included
[[/= _ /to_latT_inj /leibniz_equiv_iff //]|
/prod_included [/= /frac_included /= // _]]]].
Qed.
@@ -268,7 +268,7 @@ Section ArcGhost.
✓ (moveOAuth Mt1 ⋅ certO Mt2) → Mt2 ⊆ Mt1.
Proof.
rewrite -pair_op right_id.
- move => [/= _ /auth_both_valid [/latT_included // ]].
+ move => [/= _ /auth_both_valid_discrete [/latT_included // ]].
Qed.
Lemma StrongDownAuth_agree γ Dt Dt':
@@ -397,7 +397,7 @@ Section ArcGhost.
Proof.
rewrite -embed_sep -own_op. iIntros "oA".
iDestruct (own_valid with "oA")
- as %[[[[|INCL]%option_included _]%auth_both_valid _] _]; [done|].
+ as %[[[[|INCL]%option_included _]%auth_both_valid_discrete _] _]; [done|].
iPureIntro. destruct INCL as [q1 [[q' n] [Eq1 [Eq2 Eq3]]]].
inversion Eq1. subst q1. exists q', n. split; [done|].
destruct Eq3 as [[Eq3 Eq4]|[[q'' Le1] Le2%pos_included]%prod_included].
@@ -413,7 +413,7 @@ Section ArcGhost.
Proof.
rewrite -embed_sep -own_op. iIntros "oA".
iDestruct (own_valid with "oA")
- as %[[_ [[_ INCL]%prod_included VALID]%auth_both_valid] _].
+ as %[[_ [[_ INCL]%prod_included VALID]%auth_both_valid_discrete] _].
iPureIntro. destruct st as [st' st]. simpl in *.
apply option_included in INCL as [|[q1 [qn [Eq1 [Eq2 Eq3]]]]]; [done|].
subst st. inversion Eq1. subst q1. destruct Eq3 as [Eq3|INCL].
@@ -539,7 +539,7 @@ Section ArcGhost.
WeakAuth γ (iS, st) ∗ agown γ (awk_n ((Some q, ε))) -∗ ∃ q', ⌜iS = Some q'⌝.
Proof.
rewrite -embed_sep -own_op. iIntros "own".
- iDestruct (own_valid with "own") as %[[_ [VAL _]%auth_both_valid] _].
+ iDestruct (own_valid with "own") as %[[_ [VAL _]%auth_both_valid_discrete] _].
iPureIntro. move : VAL => /prod_included /= [/option_included [//|[?[? [?[??]]]]] _].
subst iS. by eexists.
Qed.
@@ -608,7 +608,7 @@ Section ArcGhost.
Proof.
rewrite -embed_sep -own_op. iIntros "own".
iDestruct (@own_valid _ arcUR with "own")
- as %[[_ [[_ [?|INCL]%option_included]%prod_included [_ VAL]]%auth_both_valid] _];
+ as %[[_ [[_ [?|INCL]%option_included]%prod_included [_ VAL]]%auth_both_valid_discrete] _];
[done|]. iPureIntro.
destruct INCL as (x & y & Eq1 & Eq2 & INCL). simpl in *. inversion Eq1.
subst x st. destruct INCL as [Eq|INCL].
diff --git a/theories/lifetime/model/accessors.v b/theories/lifetime/model/accessors.v
index cf5ab66f..3073b4d2 100644
--- a/theories/lifetime/model/accessors.v
+++ b/theories/lifetime/model/accessors.v
@@ -18,7 +18,7 @@ Proof.
iIntros (?) "Hslice Halive Hbor Htok". rewrite /lft_bor_alive /idx_bor_own.
iDestruct "Halive" as (B) "[[Hbox >Hown] HB]". iDestruct "Hbor" as (V') "[% Hbor]".
iDestruct (own_bor_valid_2 with "Hown Hbor")
- as %[EQB%to_borUR_included _]%auth_both_valid.
+ as %[EQB%to_borUR_included _]%auth_both_valid_discrete.
iMod (slice_empty _ _ true with "Hslice Hbox") as "[HP Hbox]".
solve_ndisj. by rewrite lookup_fmap EQB.
rewrite -(fmap_insert bor_filled _ _ (Bor_open q Vtok V')).
@@ -39,7 +39,7 @@ Proof.
iIntros (? HVV') "Hslice Halive Hbor HP". unfold lft_bor_alive, idx_bor_own.
iDestruct "Halive" as (B) "[[Hbox >Hown] HB]".
iDestruct (own_bor_valid_2 with "Hown Hbor")
- as %[EQB%to_borUR_included _]%auth_both_valid.
+ as %[EQB%to_borUR_included _]%auth_both_valid_discrete.
iMod (slice_fill _ _ true with "Hslice HP Hbox") as "Hbox".
solve_ndisj. by rewrite lookup_fmap EQB.
rewrite -(fmap_insert bor_filled _ _ (Bor_in (Vtok' ⊔ V))).
@@ -78,7 +78,7 @@ Proof.
[by rewrite Hf2 Hf1|by apply Hhv2, Hhv1].
- clear. iIntros (Λ HΛ A) "Htok HA". iDestruct "Htok" as (V') "[% Htok]".
iDestruct (own_valid_2 with "HA Htok") as
- %[(s0 & Hv & Hincl)%singleton_included_l _]%auth_both_valid.
+ %[(s0 & Hv & Hincl)%singleton_included_l _]%auth_both_valid_discrete.
revert Hv Hincl. rewrite lookup_fmap. case HA: (A!!Λ)=>[[b V'']|]; [|by inversion 1].
move=> <- /Some_included Hincl. destruct b; last first.
{ case Hincl=>[|/csum_included]; [by inversion 1|]. naive_solver. }
@@ -101,7 +101,7 @@ Proof.
iAssert (⌜lft_has_view A' κ V⌝)%I as %HA'V.
{ iIntros (Λ HΛ). iDestruct (@big_sepMS_elem_of with "Htok") as "Htok"=>//.
iDestruct (own_valid_2 with "HA' Htok")
- as %[(s & HA' & [Hs|Hs]%Some_included)%singleton_included_l _]%auth_both_valid.
+ as %[(s & HA' & [Hs|Hs]%Some_included)%singleton_included_l _]%auth_both_valid_discrete.
- setoid_subst. rewrite lookup_fmap /to_lft_stateR in HA'.
destruct (A'!!Λ) as [[[] V']|]=>/=.
+ apply (inj Some), (inj Cinl), (inj2 pair), proj2, (inj to_latT) in HA'=>//.
@@ -171,7 +171,7 @@ Proof.
iDestruct "Hinv" as (Vκ) "[>% [[Hinv >%]|[Hinv >%]]]"; last first.
{ iDestruct "Hinv" as (??) "(_ & Hinv & _)". iDestruct "Hinv" as (B ?) "[>Hinv _]".
iDestruct (own_bor_valid_2 with "Hinv Hf")
- as %[(_ & <- & INCL%option_included)%singleton_included_l _]%auth_both_valid.
+ as %[(_ & <- & INCL%option_included)%singleton_included_l _]%auth_both_valid_discrete.
exfalso. destruct INCL as [[=]|(? & ? & [=<-] & Hi & Ho)].
rewrite lookup_fmap in Hi. destruct (B !! s); inversion Hi; subst; clear Hi.
by destruct Ho as [?%(inj Excl)|?%(exclusive_included _)]. }
@@ -273,7 +273,7 @@ Proof.
iDestruct "Hinv" as (Vκ) "[>% [[Hinv >%]|[Hinv >%]]]"; last first.
{ iDestruct "Hinv" as (??) "(_ & Hinv & _)". iDestruct "Hinv" as (B ?) "[>Hinv _]".
iDestruct (own_bor_valid_2 with "Hinv Hbor")
- as %[(_ & <- & INCL%option_included)%singleton_included_l _]%auth_both_valid.
+ as %[(_ & <- & INCL%option_included)%singleton_included_l _]%auth_both_valid_discrete.
exfalso. destruct INCL as [[=]|(? & ? & [=<-] & Hi & Ho)].
rewrite lookup_fmap /= in Hi. destruct (B !! s''); inversion Hi; subst; clear Hi.
by destruct Ho as [?%(inj Excl)|?%(exclusive_included _)]. }
@@ -281,7 +281,7 @@ Proof.
iDestruct "Hinv" as (Pb Pi) "(Halive & Hvs & Hinh)".
iDestruct "Halive" as (B) "[[Hbox >Hown] HB]".
iDestruct (own_bor_valid_2 with "Hown Hbor")
- as %[EQB%to_borUR_included _]%auth_both_valid.
+ as %[EQB%to_borUR_included _]%auth_both_valid_discrete.
iDestruct (slice_delete_empty _ true with "Hs Hbox") as (Pb') "[EQ Hbox]".
by rewrite lookup_fmap EQB.
iMod (slice_insert_empty _ _ true _ Q with "Hbox") as (j) "(% & #Hs' & Hbox)".
@@ -353,7 +353,7 @@ Proof.
iDestruct "Hinv" as (Pb Pi) "(Halive & Hvs & Hinh)".
iDestruct "Halive" as (B) "[[Hbox >Hown] HB]".
iDestruct (own_bor_valid_2 with "Hown Hbor")
- as %[EQB%to_borUR_included _]%auth_both_valid.
+ as %[EQB%to_borUR_included _]%auth_both_valid_discrete.
iMod (slice_delete_full _ _ true with "Hs Hbox") as (Pb') "(HP' & EQ & Hbox)".
solve_ndisj. by rewrite lookup_fmap EQB.
iApply fupd_frame_l. iSplitL "HP'".
diff --git a/theories/lifetime/model/borrow_sep.v b/theories/lifetime/model/borrow_sep.v
index fdfbddf5..f10112f5 100644
--- a/theories/lifetime/model/borrow_sep.v
+++ b/theories/lifetime/model/borrow_sep.v
@@ -55,7 +55,7 @@ Proof.
iDestruct "Hinv" as (Pb Pi) "(H & Hvs & Hinh)".
iDestruct "H" as (B) "[[Hbox >Hown] HB]".
iDestruct (own_bor_valid_2 with "Hown Hbor")
- as %[EQB%to_borUR_included _]%auth_both_valid.
+ as %[EQB%to_borUR_included _]%auth_both_valid_discrete.
iAssert (▷ ⌜V' ⊑ Vκ⌝)%I with "[#]" as ">%".
{ iNext. rewrite big_sepM_lookup //. simpl. by iDestruct "HB" as %?. }
iMod (slice_delete_full _ _ true with "Hslice Hbox")
@@ -149,9 +149,9 @@ Proof.
iDestruct "Hinv" as (Pb Pi) "(H & Hvs & Hinh)".
iDestruct "H" as (B) "[[Hbox >Hown] HB]".
iDestruct (own_bor_valid_2 with "Hown Hbor1")
- as %[EQB1%to_borUR_included _]%auth_both_valid.
+ as %[EQB1%to_borUR_included _]%auth_both_valid_discrete.
iDestruct (own_bor_valid_2 with "Hown Hbor2")
- as %[EQB2%to_borUR_included _]%auth_both_valid.
+ as %[EQB2%to_borUR_included _]%auth_both_valid_discrete.
iAssert ⌜j1 ≠ j2⌝%I with "[#]" as %Hj1j2.
{ iIntros (->).
iDestruct (own_bor_valid_2 with "Hbor1 Hbor2") as %Hj1j2%auth_valid_discrete.
diff --git a/theories/lifetime/model/boxes.v b/theories/lifetime/model/boxes.v
index 772c9b7c..4a3ac825 100644
--- a/theories/lifetime/model/boxes.v
+++ b/theories/lifetime/model/boxes.v
@@ -94,7 +94,7 @@ Lemma box_own_auth_agree γ o1 o2 :
box_own_auth γ (● Excl' o1) ∗ box_own_auth γ (◯ Excl' o2) ⊢ o1 ≡ o2.
Proof.
rewrite /box_own_prop -own_op own_valid prod_validI /= and_elim_l.
- iDestruct 1 as %[[[[]|] EQ%(inj Some)] _]%auth_both_valid; by inversion_clear EQ.
+ iDestruct 1 as %[[[[]|] EQ%(inj Some)] _]%auth_both_valid_discrete; by inversion_clear EQ.
Qed.
Lemma box_own_auth_update γ o1 o2 o3 :
@@ -126,7 +126,7 @@ Proof.
iDestruct 1 as (Φ) "[#HeqP Hf]".
iMod (own_alloc_cofinite (● Excl' None ⋅ ◯ Excl' None,
Some (to_agree (Next ((λ V, iProp_unfold (Q V)) : _ -d> _)))) (dom _ f))
- as (γ) "[Hdom Hγ]". { split; [by apply auth_both_valid|done]. }
+ as (γ) "[Hdom Hγ]". { split; [by apply auth_both_valid_discrete|done]. }
rewrite pair_split. iDestruct "Hγ" as "[[Hγ Hγ'] #HγQ]".
iDestruct "Hdom" as % ?%not_elem_of_dom.
iMod (inv_alloc N _ (slice_inv γ Q) with "[Hγ]") as "#Hinv".
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index c3525888..244e3ddb 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -33,7 +33,7 @@ Proof.
iDestruct (@big_sepS_elem_of with "Hdead") as "Hdead"; [by apply HK|].
rewrite /lft_inv_dead; iDestruct "Hdead" as (R Vinh) "(_ & _ & Hcnt' & _)".
iDestruct (own_cnt_valid_2 with "Hcnt' Hcnt")
- as %[?%nat_included _]%auth_both_valid; lia. }
+ as %[?%nat_included _]%auth_both_valid_discrete; lia. }
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 (Vκ n) "(% & Hcnt & Hvs)".
@@ -184,7 +184,7 @@ Proof.
iDestruct "H" as (A I) "(% & HA & HI & Hinv)".
rewrite /lft_tok /= big_sepMS_singleton. iDestruct "HΛ" as (V'0) "[#HV'0 HΛ]".
iDestruct (own_valid_2 with "HA HΛ")
- as %[[s [Hs Hincl%Some_included]]%singleton_included_l Hv]%auth_both_valid.
+ as %[[s [Hs Hincl%Some_included]]%singleton_included_l Hv]%auth_both_valid_discrete.
destruct Hincl; last first.
{ destruct (exclusive_included (Cinl (1%Qp, to_latT V'0)) s)=>//.
move: (Hv Λ). by rewrite Hs. }
diff --git a/theories/lifetime/model/faking.v b/theories/lifetime/model/faking.v
index 23f13c27..112cdaa8 100644
--- a/theories/lifetime/model/faking.v
+++ b/theories/lifetime/model/faking.v
@@ -15,9 +15,9 @@ Proof.
iIntros "HA HI Hinv".
destruct (decide (is_Some (I !! κ))) as [?|HIκ%eq_None_not_Some].
{ iModIntro. iExists A, I. iFrame. iPureIntro. by apply elem_of_dom. }
- iMod (own_alloc (● 0 ⋅ ◯ 0)) as (γcnt) "[Hcnt Hcnt']"; first by apply auth_both_valid.
+ iMod (own_alloc (● 0 ⋅ ◯ 0)) as (γcnt) "[Hcnt Hcnt']"; first by apply auth_both_valid_discrete.
iMod (own_alloc ((● ∅ ⋅ ◯ ∅) :auth (gmap slice_name (excl (bor_state Lat)))))
- as (γbor) "[Hbor Hbor']"; first by apply auth_both_valid.
+ as (γbor) "[Hbor Hbor']"; first by apply auth_both_valid_discrete.
iMod (own_alloc ((● ε) :auth (gset_disj slice_name)))
as (γinh) "Hinh"; first by apply auth_auth_valid.
set (γs := LftNames γbor γcnt γinh).
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index fb9343ca..999912e1 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -35,7 +35,7 @@ Lemma own_ilft_auth_agree (I : gmap lft lft_names) κ γs :
own ilft_name (◯ {[κ := to_agree γs]}) -∗ ⌜κ ∈ dom (gset _) I⌝.
Proof.
iIntros "HI Hκ". iDestruct (own_valid_2 with "HI Hκ")
- as %[[? [Hl ?]]%singleton_included_l _]%auth_both_valid.
+ as %[[? [Hl ?]]%singleton_included_l _]%auth_both_valid_discrete.
iPureIntro. apply elem_of_dom. unfold to_ilftUR in *. simplify_map_eq.
destruct (fmap_Some_equiv_1 _ _ _ Hl) as (?&?&?). eauto.
Qed.
@@ -45,7 +45,7 @@ Lemma own_alft_auth_agree (A : gmap atomic_lft (bool * Lat)) Λ bV :
own alft_name (◯ {[Λ := to_lft_stateR bV]}) -∗ ⌜A !! Λ ≡ Some bV⌝.
Proof.
iIntros "HA HΛ".
- iDestruct (own_valid_2 with "HA HΛ") as %[HA _]%auth_both_valid.
+ iDestruct (own_valid_2 with "HA HΛ") as %[HA _]%auth_both_valid_discrete.
iPureIntro. move: HA=> /singleton_included_l [qs []].
rewrite lookup_fmap fmap_Some_equiv=> -[bV' [-> ->]] /Some_included [EQ|/csum_included].
- destruct bV as [[]?], bV' as [[]?]; (try by inversion EQ); do 2 f_equiv.
@@ -456,7 +456,7 @@ Proof.
{ iIntros (I) "HI". iApply (own_inh_auth with "HI HE◯'"). }
iIntros (Q'). rewrite {1}/lft_inh. iDestruct 1 as (PE) "[>HE Hbox]".
iDestruct (own_inh_valid_2 with "HE HE◯")
- as %[Hle%gset_disj_included _]%auth_both_valid.
+ as %[Hle%gset_disj_included _]%auth_both_valid_discrete.
iMod (own_inh_update_2 with "HE HE◯") as "HE".
{ apply auth_update_dealloc, gset_disj_dealloc_local_update. }
iMod (slice_delete_full _ _ true with "Hslice Hbox")
diff --git a/theories/lifetime/model/reborrow.v b/theories/lifetime/model/reborrow.v
index 6f79fbc2..15ce9b6f 100644
--- a/theories/lifetime/model/reborrow.v
+++ b/theories/lifetime/model/reborrow.v
@@ -65,7 +65,7 @@ Proof.
iDestruct "Hκ" as (Pb' Pi') "(Hκalive & Hvs' & Hinh')".
rewrite {2}/lft_bor_alive; iDestruct "Hκalive" as (B) "[[Hbox >HB●] HB]".
iDestruct (own_bor_valid_2 with "HB● Hi")
- as %[HB%to_borUR_included _]%auth_both_valid.
+ as %[HB%to_borUR_included _]%auth_both_valid_discrete.
iMod (slice_empty _ _ true with "Hislice Hbox") as "[HP Hbox]"; first done.
{ by rewrite lookup_fmap HB. }
iMod (own_bor_update_2 with "HB● Hi") as "[HB● Hi]".
@@ -112,7 +112,7 @@ Proof.
iDestruct ("Hκalive" with "[//]") as (Pb' Pi') "(Hκalive & Hvs' & Hinh)".
rewrite /lft_bor_alive; iDestruct "Hκalive" as (B') "[[Hbox HB●] HB]".
iDestruct (own_bor_valid_2 with "HB● Hi")
- as %[HB%to_borUR_included _]%auth_both_valid.
+ as %[HB%to_borUR_included _]%auth_both_valid_discrete.
iAssert ⌜V0 ⊑ Vs κ⌝%I with "[#]" as "%".
{ rewrite (big_sepM_lookup _ _ _ _ HB) /=. iDestruct "HB" as "[$ _]". }
iAssert (∃ VP, ⌜VP ⊑ Vs κ⌝ ∗ ▷ Q (Vs κ') ∗ ▷ P VP ∗
@@ -173,7 +173,7 @@ Proof.
iDestruct "Halive" as (B) "[[Hbox >H●] HB]". rewrite [_ (κ', i')]/idx_bor_own.
iDestruct "Hbor" as (V') "[#HV' Hbor]".
iDestruct (own_bor_valid_2 with "H● Hbor")
- as %[EQB%to_borUR_included _]%auth_both_valid.
+ as %[EQB%to_borUR_included _]%auth_both_valid_discrete.
iMod (slice_empty _ _ true with "Hs' Hbox") as "[Hidx Hbox]".
solve_ndisj. by rewrite lookup_fmap EQB.
iAssert (▷ ⌜κ ∈ dom (gset lft) I⌝)%I with "[#]" as ">%".
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index a50131a6..5dc181dc 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -164,7 +164,7 @@ Section rc.
iMod (bor_create with "LFT Hown") as "[HP HPend]"; first solve_ndisj.
iMod (own_alloc (● (Some $ Cinl ((1/2)%Qp, 1%positive), 0%nat) ⋅
◯ (Some $ Cinl ((1/2)%Qp, 1%positive), 0%nat))) as (γ) "[Ha Hf]".
- { by apply auth_both_valid. }
+ { by apply auth_both_valid_discrete. }
iMod (na_inv_alloc tid _ _ (rc_inv tid ν γ l' ty)
with "[Ha Hν2 Hl'1 Hl'2 H† HPend]") as "#?".
{ rewrite /rc_inv. iExists (Some $ Cinl (_, _), _). iFrame "Ha". iExists _.
@@ -289,7 +289,7 @@ Section code.
iMod (na_inv_acc with "Hinv Hna") as "(Hproto & Hna & Hclose)"; [solve_ndisj..|].
iDestruct "Hproto" as ([st weak]) "[>Hst Hproto]".
iDestruct (own_valid_2 with "Hst Htok") as %[[[[=]|(?&st'&[=<-]&EQst'&Hincl)]
- %option_included _]%prod_included [Hval _]]%auth_both_valid.
+ %option_included _]%prod_included [Hval _]]%auth_both_valid_discrete.
simpl in EQst'. subst st. destruct Hincl as [Hincl|Hincl].
+ destruct st' as [[]| |]; try by inversion Hincl. apply (inj Cinl) in Hincl.
apply (inj2 pair) in Hincl. destruct Hincl as [<-%leibniz_equiv <-%leibniz_equiv].
@@ -348,7 +348,7 @@ Section code.
iMod (na_inv_acc with "Hinv Hna") as "(Hproto & Hna & Hclose)"; [solve_ndisj..|].
iDestruct "Hproto" as ([st weak]) "[>Hst Hproto]".
iDestruct (own_valid_2 with "Hst Htok") as %[[[[=]|(?&st'&[=<-]&EQst'&Hincl)]
- %option_included _]%prod_included [Hval _]]%auth_both_valid.
+ %option_included _]%prod_included [Hval _]]%auth_both_valid_discrete.
simpl in EQst'. subst st. destruct Hincl as [Hincl|Hincl]; first last.
{ apply csum_included in Hincl. destruct Hincl as
[->|[(?&?&[=]&?)|(?&?&[=<-]&->&?%exclusive_included)]]; try done. apply _. }
@@ -419,7 +419,7 @@ Section code.
iMod (na_bor_acc with "LFT Hrctokb Hα1 Hna") as "(>Hrctok & Hna & Hclose3)"; [solve_ndisj..|].
iDestruct "Hrcproto" as ([st weak]) "[>Hrc● Hrcst]".
iDestruct (own_valid_2 with "Hrc● Hrctok") as %[[[[=]|(?&[[q0 s0]| |]&[=<-]&?&Hincl)]
- %option_included _]%prod_included [Hval _]]%auth_both_valid;
+ %option_included _]%prod_included [Hval _]]%auth_both_valid_discrete;
setoid_subst; try done; last first.
{ exfalso. destruct Hincl as [Hincl|Hincl]. by inversion Hincl.
apply csum_included in Hincl. naive_solver. }
@@ -478,7 +478,7 @@ Section code.
iMod (na_bor_acc with "LFT Hrctokb Hα1 Hna") as "(>Hrctok & Hna & Hclose3)"; [solve_ndisj..|].
iDestruct "Hrcproto" as ([st weak]) "[>Hrc● Hrcst]".
iDestruct (own_valid_2 with "Hrc● Hrctok") as %[[[[=]|(?&[[q0 weak0]| |]&[=<-]&?&Hincl)]
- %option_included _]%prod_included [Hval _]]%auth_both_valid;
+ %option_included _]%prod_included [Hval _]]%auth_both_valid_discrete;
setoid_subst; try done; last first.
{ exfalso. destruct Hincl as [Hincl|Hincl]. by inversion Hincl.
apply csum_included in Hincl. naive_solver. }
@@ -583,7 +583,7 @@ Section code.
iMod (na_bor_acc with "LFT Hrctokb Hα1 Hna") as "(>Hrctok & Hna & Hclose3)"; [solve_ndisj..|].
iDestruct "Hrcproto" as ([st weak]) "[>Hrc● Hrcst]".
iDestruct (own_valid_2 with "Hrc● Hrctok") as %[[[[=]|(?&[[q0 s0]| |]&[=<-]&?&Hincl)]
- %option_included _]%prod_included [Hval _]]%auth_both_valid;
+ %option_included _]%prod_included [Hval _]]%auth_both_valid_discrete;
setoid_subst; try done; last first.
{ exfalso. destruct Hincl as [Hincl|Hincl]. by inversion Hincl.
apply csum_included in Hincl. naive_solver. }
@@ -1078,7 +1078,7 @@ Section code.
{ iDestruct "Hty" as "[(Hl1 & Hl2 & Hl† & Hl3)|Hty]"; last done.
iMod (own_alloc (● (Some $ Cinl ((1/2)%Qp, 1%positive), 0%nat) ⋅
rc_tok (1/2)%Qp)) as (γ) "[Ha Hf]";
- first by apply auth_both_valid.
+ first by apply auth_both_valid_discrete.
iMod (lft_create with "LFT") as (ν) "[[Hν1 Hν2] #Hν†]"=>//.
iApply (fupd_mask_mono (↑lftN))=>//. iExists γ, ν, (1/2)%Qp. iFrame.
iMod (bor_create _ ν with "LFT Hl3") as "[Hb Hh]"=>//. iExists _.
diff --git a/theories/typing/lib/rc/weak.v b/theories/typing/lib/rc/weak.v
index 798b16c7..eadb9ca5 100644
--- a/theories/typing/lib/rc/weak.v
+++ b/theories/typing/lib/rc/weak.v
@@ -164,7 +164,7 @@ Section code.
iMod (na_bor_acc with "LFT Hwtokb Hα1 Hna") as "(>Hwtok & Hna & Hclose3)"; [solve_ndisj..|].
iDestruct "Hrcproto" as ([st weakc]) "[>Hrc● Hrcst]".
iDestruct (own_valid_2 with "Hrc● Hwtok") as
- %[[_ Hweak%nat_included]%prod_included [Hval _]]%auth_both_valid.
+ %[[_ Hweak%nat_included]%prod_included [Hval _]]%auth_both_valid_discrete.
destruct st as [[[q'' strong]| |]|]; try done.
- (* Success case. *)
iDestruct "Hrcst" as (qb) "(Hl'1 & Hl'2 & Hl'† & >Hq''q0 & [Hν1 Hν2] & Hν†)".
@@ -267,7 +267,7 @@ Section code.
iMod (na_bor_acc with "LFT Hrctokb Hα1 Hna") as "(>Hrctok & Hna & Hclose3)"; [solve_ndisj..|].
iDestruct "Hrcproto" as ([st weakc]) "[>Hrc● Hrcst]".
iDestruct (own_valid_2 with "Hrc● Hrctok") as %[[[[=]|(?&[[q0 weak0]| |]&[=<-]&?&Hincl)]
- %option_included _]%prod_included [Hval _]]%auth_both_valid;
+ %option_included _]%prod_included [Hval _]]%auth_both_valid_discrete;
setoid_subst; try done; last first.
{ exfalso. destruct Hincl as [Hincl|Hincl]. by inversion Hincl.
apply csum_included in Hincl. naive_solver. }
@@ -333,7 +333,7 @@ Section code.
iMod (na_bor_acc with "LFT Hwtokb Hα1 Hna") as "(>Hwtok & Hna & Hclose3)"; [solve_ndisj..|].
iDestruct "Hrcproto" as ([st weakc]) "[>Hrc● Hrcst]".
iDestruct (own_valid_2 with "Hrc● Hwtok") as
- %[[_ Hweak%nat_included]%prod_included [Hval _]]%auth_both_valid.
+ %[[_ Hweak%nat_included]%prod_included [Hval _]]%auth_both_valid_discrete.
iMod (own_update with "Hrc●") as "[Hrc● $]".
{ by apply auth_update_alloc, prod_local_update_2,
(op_local_update_discrete _ _ 1%nat). }
@@ -406,7 +406,7 @@ Section code.
iMod (na_inv_acc with "Hinv Hna") as "(Hrcproto & Hna & Hclose)"; [solve_ndisj..|].
iDestruct "Hrcproto" as ([st weakc]) "[>Hrc● Hrcst]".
iDestruct (own_valid_2 with "Hrc● Hwtok") as
- %[[_ Hweak%nat_included]%prod_included [Hval _]]%auth_both_valid.
+ %[[_ Hweak%nat_included]%prod_included [Hval _]]%auth_both_valid_discrete.
destruct weakc; first by simpl in *; lia.
iMod (own_update_2 with "Hrc● Hwtok") as "Hrc●".
{ apply auth_update_dealloc, prod_local_update_2,
@@ -479,7 +479,7 @@ Section code.
{ rewrite tctx_interp_singleton tctx_hasty_val' //=. iFrame.
iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame.
iMod (own_alloc (● _ ⋅ ◯ _)) as (γ) "[??]"; last (iExists _, _; iFrame).
- { apply auth_both_valid. by split. }
+ { apply auth_both_valid_discrete. by split. }
iExists ty. iFrame "Hν†". iSplitR; first by iApply type_incl_refl.
iSplitL; last by iRight. iMod (na_inv_alloc with "[-]") as "$"; last done.
iExists _. iFrame. rewrite freeable_sz_full_S shift_loc_assoc. iFrame.
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index c76a2634..f8d64e9f 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -25,7 +25,7 @@ Section ref_functions.
{ destruct st as [[[[??]?]?]|];
iDestruct (own_valid_2 with "H● H◯")
as %[[[=]|(?&[[? q'] n]&[=<-]&[=]&[[[Eq_ag ?%leibniz_equiv]_]|Hle])]
- %option_included Hv]%auth_both_valid; simpl in *; subst.
+ %option_included Hv]%auth_both_valid_discrete; simpl in *; subst.
- apply (inj to_agree), (inj2 pair) in Eq_ag.
destruct Eq_ag. setoid_subst. eauto.
- revert Hle=> /prod_included [/= /prod_included
@@ -165,7 +165,7 @@ Section ref_functions.
with "[H↦lrc H●◯ Hν Hν' Hshr H†]" as "INV".
{ iDestruct (own_valid with "H●◯") as
%[[[[_ ?]?]|[[_ [q0 Hq0]]%prod_included [n' Hn']]%prod_included]
- %Some_included _]%auth_both_valid.
+ %Some_included _]%auth_both_valid_discrete.
- simpl in *. setoid_subst.
iExists None. iFrame. iMod (own_update with "H●◯") as "$".
{ apply auth_update_dealloc. rewrite -(right_id None op (Some _)).
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index d5488459..57f781da 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -130,7 +130,7 @@ Section refmut_functions.
with "[H↦lrc H● H◯ Hν INV]" as "INV".
{ iDestruct (own_valid_2 with "H● H◯") as
%[[[=]|(? & [[? q'] ?] & [= <-] & Hst & INCL)]%option_included _]
- %auth_both_valid.
+ %auth_both_valid_discrete.
destruct st as [[[[??]?]?]|]; [|done]. move: Hst=>-[= ???]. subst.
destruct INCL as [[[[ν' ?]%to_agree_inj ?] ?]|
[[[??]%to_agree_included [q'' Hq'']]%prod_included [n' Hn']]%prod_included].
@@ -298,7 +298,7 @@ Section refmut_functions.
iMod (na_bor_acc with "LFT Hinv Hβ Hna") as "(INV & Hna & Hclosena)"; [done..|].
wp_seq. wp_op. wp_read.
iDestruct "INV" as (st) "(Hlrc & H● & Hst)".
- iDestruct (own_valid_2 with "H● Hγ") as %[Hst _]%auth_both_valid.
+ iDestruct (own_valid_2 with "H● Hγ") as %[Hst _]%auth_both_valid_discrete.
destruct st as [[[[??]?]?]|]; last by destruct Hst as [[?|] Hst]; inversion Hst.
move:Hst=>/Some_pair_included [/Some_pair_included_total_1
[/to_agree_included /(leibniz_equiv _ _) [= <- <-] _] _].
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index 2dab818e..de3da62e 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -107,7 +107,7 @@ Section rwlock_inv.
∨ (∃ q0, q' = (q + q0)%Qp) ∧ n = (1 + Pos.pred n)%positive)⌝.
Proof.
iIntros "m r". iCombine "m" "r" as "mr".
- iDestruct (own_valid with "mr") as %[INCL VAL]%auth_both_valid.
+ iDestruct (own_valid with "mr") as %[INCL VAL]%auth_both_valid_discrete.
iPureIntro. destruct st as [[[]|[[]]]|].
- move : INCL =>
/Some_included [Eq|/csum_included [//|[[?[?[??//]]]|[?[?[?[??//]]]]]]].
@@ -155,7 +155,7 @@ Section rwlock_inv.
⌜st = (Some (inl tt))⌝.
Proof.
iIntros "m w". iCombine "m" "w" as "mw".
- iDestruct (own_valid with "mw") as %[INCL VAL]%auth_both_valid.
+ iDestruct (own_valid with "mw") as %[INCL VAL]%auth_both_valid_discrete.
iPureIntro. destruct st as [[[]|[[]]]|]; [done|..].
- move : INCL =>
/Some_included [Eq|/csum_included [//|[[?[?[?[Eq _]]]]|[?[?[?[??//]]]]]]];
--
GitLab