From 3cfb7f842ae34d4bd62ca1d5d87d4e805b5b9bf3 Mon Sep 17 00:00:00 2001
From: Hoang-Hai Dang <haidang@mpi-sws.org>
Date: Fri, 24 May 2019 17:03:34 +0200
Subject: [PATCH] Bump Iris (changes in auth)
---
opam | 2 +-
theories/lang/adequacy.v | 3 +-
theories/lang/heap.v | 10 +++----
theories/lang/lib/arc.v | 17 ++++++-----
theories/lifetime/model/accessors.v | 14 ++++-----
theories/lifetime/model/borrow_sep.v | 6 ++--
theories/lifetime/model/creation.v | 4 +--
theories/lifetime/model/faking.v | 6 ++--
theories/lifetime/model/primitive.v | 30 +++++++++----------
theories/lifetime/model/reborrow.v | 6 ++--
theories/typing/lib/rc/rc.v | 17 ++++++-----
theories/typing/lib/rc/weak.v | 10 +++----
theories/typing/lib/refcell/ref_code.v | 4 +--
theories/typing/lib/refcell/refcell.v | 3 +-
theories/typing/lib/refcell/refmut_code.v | 4 +--
theories/typing/lib/rwlock/rwlock.v | 5 ++--
.../typing/lib/rwlock/rwlockreadguard_code.v | 2 +-
.../typing/lib/rwlock/rwlockwriteguard_code.v | 2 +-
18 files changed, 75 insertions(+), 70 deletions(-)
diff --git a/opam b/opam
index fc658175..ff8097f2 100644
--- a/opam
+++ b/opam
@@ -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-05-09.1.d0daa181") | (= "dev") }
+ "coq-iris" { (= "dev.2019-05-15.0.551c1ecc") | (= "dev") }
]
diff --git a/theories/lang/adequacy.v b/theories/lang/adequacy.v
index 05315b8c..7418153b 100644
--- a/theories/lang/adequacy.v
+++ b/theories/lang/adequacy.v
@@ -24,7 +24,8 @@ Proof.
intros Hwp; eapply (wp_adequacy _ _); iIntros (??).
iMod (own_alloc (◠to_heap σ)) as (vγ) "Hvγ".
{ apply (auth_auth_valid (to_heap _)), to_heap_valid. }
- iMod (own_alloc (◠(∅ : heap_freeableUR))) as (fγ) "Hfγ"; first done.
+ iMod (own_alloc (◠(∅ : heap_freeableUR))) as (fγ) "Hfγ";
+ first by apply auth_auth_valid.
set (Hheap := HeapG _ _ _ vγ fγ).
iModIntro. iExists (λ σ _, heap_ctx σ). iSplitL.
{ iExists ∅. by iFrame. }
diff --git a/theories/lang/heap.v b/theories/lang/heap.v
index 2c3acda7..93a6f98b 100644
--- a/theories/lang/heap.v
+++ b/theories/lang/heap.v
@@ -142,7 +142,7 @@ Section heap.
Lemma heap_mapsto_agree l q1 q2 v1 v2 : l ↦{q1} v1 ∗ l ↦{q2} v2 ⊢ ⌜v1 = v2âŒ.
Proof.
rewrite heap_mapsto_eq -own_op -auth_frag_op own_valid discrete_valid.
- eapply pure_elim; [done|]=> /auth_own_valid /=.
+ eapply pure_elim; [done|]=> /auth_frag_valid /=.
rewrite op_singleton pair_op singleton_valid=> -[? /agree_op_invL'->]; eauto.
Qed.
@@ -215,7 +215,7 @@ Section heap.
{[l +â‚— i := (q, Cinr 0%nat, to_agree v)]}).
Proof.
rewrite /heap_mapsto_vec heap_mapsto_eq /heap_mapsto_def /heap_mapsto_st=>?.
- by rewrite (big_opL_commute (Auth None)) big_opL_commute1 //.
+ by rewrite /auth_frag (big_opL_commute (Auth None)) big_opL_commute1 //.
Qed.
Global Instance heap_mapsto_pred_fractional l (P : list val → iProp Σ):
@@ -406,7 +406,7 @@ Section heap.
Proof.
iDestruct 1 as (hF) "(Hvalσ & HhF & REL)"; iDestruct "REL" as %REL.
iIntros "Hmt Hf". rewrite heap_freeable_eq /heap_freeable_def.
- iDestruct (own_valid_2 with "HhF Hf") as % [Hl Hv]%auth_valid_discrete_2.
+ iDestruct (own_valid_2 with "HhF Hf") as % [Hl Hv]%auth_both_valid.
move: Hl=> /singleton_included [[q qs] [/leibniz_equiv_iff Hl Hq]].
apply (Some_included_exclusive _ _) in Hq as [=<-<-]%leibniz_equiv; last first.
{ move: (Hv (l.1)). rewrite Hl. by intros [??]. }
@@ -429,7 +429,7 @@ Section heap.
σ !! l = Some (match ls with RSt n => RSt (n+n') | WSt => WSt end, v)âŒ.
Proof.
iIntros "Hâ— Hâ—¯".
- iDestruct (own_valid_2 with "Hâ— Hâ—¯") as %[Hl?]%auth_valid_discrete_2.
+ iDestruct (own_valid_2 with "Hâ— Hâ—¯") as %[Hl?]%auth_both_valid.
iPureIntro. move: Hl=> /singleton_included [[[q' ls'] dv]].
rewrite /to_heap lookup_fmap fmap_Some_equiv.
move=> [[[ls'' v'] [?[[/=??]->]]]]; simplify_eq.
@@ -446,7 +446,7 @@ Section heap.
⌜σ !! l = Some (ls, v)âŒ.
Proof.
iIntros "Hâ— Hâ—¯".
- iDestruct (own_valid_2 with "Hâ— Hâ—¯") as %[Hl?]%auth_valid_discrete_2.
+ iDestruct (own_valid_2 with "Hâ— Hâ—¯") as %[Hl?]%auth_both_valid.
iPureIntro. move: Hl=> /singleton_included [[[q' ls'] dv]].
rewrite /to_heap lookup_fmap fmap_Some_equiv.
move=> [[[ls'' v'] [?[[/=??]->]]] Hincl]; simplify_eq.
diff --git a/theories/lang/lib/arc.v b/theories/lang/lib/arc.v
index b63b63ce..a9c1c933 100644
--- a/theories/lang/lib/arc.v
+++ b/theories/lang/lib/arc.v
@@ -189,7 +189,7 @@ Section arc.
iIntros "Hl1 Hl2 [HP1 HP1']".
iMod (own_alloc ((â— (Some $ Cinl ((1/2)%Qp, xH, None), O) â‹…
â—¯ (Some $ Cinl ((1/2)%Qp, xH, None), O))))
- as (γ) "[H◠H◯]"; first done.
+ as (γ) "[H◠H◯]"; first by apply auth_both_valid.
iExists _, _. iFrame. iApply inv_alloc. iExists _. iFrame. iExists _. iFrame.
rewrite Qp_div_2. auto.
Qed.
@@ -198,7 +198,8 @@ Section arc.
l ↦ #0 -∗ (l +ₗ 1) ↦ #1 -∗ P2 ={E}=∗ ∃ γ, is_arc P1 P2 N γ l ∗ weak_tok γ.
Proof.
iIntros "Hl1 Hl2 HP2".
- iMod (own_alloc ((◠(None, 1%nat) ⋅ ◯ (None, 1%nat)))) as (γ) "[H◠H◯]"; first done.
+ iMod (own_alloc ((◠(None, 1%nat) ⋅ ◯ (None, 1%nat)))) as (γ) "[H◠H◯]";
+ first by apply auth_both_valid.
iExists _. iFrame. iApply inv_alloc. iExists _. iFrame.
Qed.
@@ -209,7 +210,7 @@ Section arc.
else ∃ q'', q' = (q + q'')%QpâŒ.
Proof.
iIntros "Hâ— Htok". iDestruct (own_valid_2 with "Hâ— Htok") as
- %[[Hincl%option_included _]%prod_included [Hval _]]%auth_valid_discrete_2.
+ %[[Hincl%option_included _]%prod_included [Hval _]]%auth_both_valid.
destruct st, Hincl as [[=]|(?&?&[= <-]&?&[Hincl|Hincl%csum_included])];
simpl in *; subst.
- setoid_subst. iExists _, _, _, _. by iSplit.
@@ -336,7 +337,7 @@ Section arc.
Proof.
iIntros "Hâ— Htok". iDestruct (own_valid_2 with "Hâ— Htok") as
%[[Hincl%option_included Hincl'%nat_included]%prod_included [Hval _]]
- %auth_valid_discrete_2.
+ %auth_both_valid.
destruct st as [?[]], Hincl as [_|(?&?&[=]&?)]; simpl in *; try lia. eauto.
Qed.
@@ -491,7 +492,7 @@ Section arc.
Proof.
iIntros "INV Hâ—¯ HP2". iInv N as ([st ?]) "[>Hâ— H]" "Hclose".
iDestruct (own_valid_2 with "Hâ— Hâ—¯")
- as %[[[[=]|Hincl]%option_included _]%prod_included [? _]]%auth_valid_discrete_2.
+ as %[[[[=]|Hincl]%option_included _]%prod_included [? _]]%auth_both_valid.
simpl in Hincl. destruct Hincl as (?&?&[=<-]&->&[?|[]%exclusive_included]);
try done; try apply _. setoid_subst.
iMod (own_update_2 with "Hâ— Hâ—¯") as "[Hâ— $]".
@@ -588,7 +589,7 @@ Section arc.
iMod ("Hclose" with "[-HΦ HP1 H◯]") as "_"; first by iExists _; eauto with iFrame.
iModIntro. wp_case. wp_bind (!ˢᶜ_)%E. iInv N as ([st ?]) "[>H◠H]" "Hclose".
iDestruct (own_valid_2 with "Hâ— Hâ—¯") as
- %[[[[=]|Hincl]%option_included _]%prod_included [? _]]%auth_valid_discrete_2.
+ %[[[[=]|Hincl]%option_included _]%prod_included [? _]]%auth_both_valid.
simpl in Hincl. destruct Hincl as (? & ? & [=<-] & -> & [|Hincl]); last first.
+ apply csum_included in Hincl. destruct Hincl as [->|[Hincl|(?&?&[=]&?)]]=>//.
destruct Hincl as (?&[[??]?]&[=<-]&->&[[_ Hlt]%prod_included _]%prod_included).
@@ -598,7 +599,7 @@ Section arc.
iModIntro. wp_let. wp_op; case_bool_decide; [lia|]. wp_let. wp_op. wp_bind (_ <-ˢᶜ _)%E.
iInv N as ([st w]) "[>Hâ— H]" "Hclose".
iDestruct (own_valid_2 with "Hâ— Hâ—¯") as
- %[[[[=]|Hincl]%option_included _]%prod_included [Hval _]]%auth_valid_discrete_2.
+ %[[[[=]|Hincl]%option_included _]%prod_included [Hval _]]%auth_both_valid.
simpl in Hincl. destruct Hincl as (? & ? & [=<-] & -> & Hincl); last first.
assert (∃ q p, x2 = Cinl (q, p, Excl' ())) as (? & ? & ->).
{ destruct Hincl as [|Hincl]; first by setoid_subst; eauto.
@@ -650,7 +651,7 @@ Section arc.
clear w. iModIntro. wp_case. wp_op. wp_bind (!ˢᶜ_)%E.
iInv N as ([st w']) "[>Hâ— H]" "Hclose".
iDestruct (own_valid_2 with "Hâ— Hâ—¯")
- as %[[[[=]|Hincl]%option_included _]%prod_included [? _]]%auth_valid_discrete_2.
+ as %[[[[=]|Hincl]%option_included _]%prod_included [? _]]%auth_both_valid.
simpl in Hincl. destruct Hincl as (?&?&[=<-]&->&[?|[]%exclusive_included]);
[|by apply _|done]. setoid_subst. iDestruct "H" as "[Hl Hl1]".
wp_read. destruct w'.
diff --git a/theories/lifetime/model/accessors.v b/theories/lifetime/model/accessors.v
index 573c4456..bd164ce8 100644
--- a/theories/lifetime/model/accessors.v
+++ b/theories/lifetime/model/accessors.v
@@ -19,7 +19,7 @@ Proof.
iIntros (?) "Hslice Halive Hbor Htok". 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_valid_discrete_2.
+ as %[EQB%to_borUR_included _]%auth_both_valid.
iMod (slice_empty _ _ true with "Hslice Hbox") as "[$ Hbox]".
solve_ndisj. by rewrite lookup_fmap EQB.
rewrite -(fmap_insert bor_filled _ _ (Bor_open q)).
@@ -41,7 +41,7 @@ Proof.
iIntros (?) "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_valid_discrete_2.
+ as %[EQB%to_borUR_included _]%auth_both_valid.
iMod (slice_fill _ _ true with "Hslice HP Hbox") as "Hbox".
solve_ndisj. by rewrite lookup_fmap EQB.
rewrite -(fmap_insert bor_filled _ _ Bor_in).
@@ -100,7 +100,7 @@ Proof.
iLeft. iFrame "%". iExists _, _. iFrame.
+ iDestruct "Hinv" as (?) "[Hinv _]". iDestruct "Hinv" as (B ?) "[>Hinv _]".
iDestruct (own_bor_valid_2 with "Hinv Hf")
- as %[(_ & <- & INCL%option_included)%singleton_included _]%auth_valid_discrete_2.
+ as %[(_ & <- & INCL%option_included)%singleton_included _]%auth_both_valid.
by destruct INCL as [[=]|(? & ? & [=<-] &
[[_<-]%lookup_gset_to_gmap_Some [[_ ?%(inj to_agree)]|[]%(exclusive_included _)]])].
- iMod (lft_dead_in_tok with "HA") as "[_ H†]". done.
@@ -124,7 +124,7 @@ Proof.
unfold lft_bor_alive.
iDestruct "Halive" as (B) "(Hbox & >Hown & HB)".
iDestruct (own_bor_valid_2 with "Hown Hbor")
- as %[EQB%to_borUR_included _]%auth_valid_discrete_2.
+ as %[EQB%to_borUR_included _]%auth_both_valid.
iMod (slice_empty _ _ true with "Hs Hbox") as "[HP' Hbox]".
solve_ndisj. by rewrite lookup_fmap EQB.
iDestruct ("HPP'" with "HP'") as "$".
@@ -176,7 +176,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_valid_discrete_2.
+ as %[EQB%to_borUR_included _]%auth_both_valid.
iMod (slice_delete_empty _ _ true with "Hs Hbox") as (Pb') "[EQ Hbox]".
solve_ndisj. by rewrite lookup_fmap EQB.
iDestruct (add_vs with "EQ Hvs [HvsQ]") as "Hvs".
@@ -204,7 +204,7 @@ Proof.
iExists Q. rewrite -bi.iff_refl. eauto.
+ iDestruct "Hinv" as (?) "[Hinv _]". iDestruct "Hinv" as (B ?) "[>Hinv _]".
iDestruct (own_bor_valid_2 with "Hinv Hbor")
- as %[(_ & <- & INCL%option_included)%singleton_included _]%auth_valid_discrete_2.
+ as %[(_ & <- & INCL%option_included)%singleton_included _]%auth_both_valid.
by destruct INCL as [[=]|(? & ? & [=<-] &
[[_<-]%lookup_gset_to_gmap_Some [[_?%(inj to_agree)]|[]%(exclusive_included _)]])].
- iMod (lft_dead_in_tok with "HA") as "[_ H†]". done.
@@ -231,7 +231,7 @@ Proof.
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_valid_discrete_2.
+ as %[EQB%to_borUR_included _]%auth_both_valid.
iMod (slice_delete_full _ _ true with "Hs Hbox") as (Pb') "(HP' & EQ & Hbox)".
solve_ndisj. by rewrite lookup_fmap EQB. iDestruct ("HPP'" with "HP'") as "$".
iMod fupd_intro_mask' as "Hclose"; last iIntros "!>* HvsQ HQ". solve_ndisj.
diff --git a/theories/lifetime/model/borrow_sep.v b/theories/lifetime/model/borrow_sep.v
index 70b98634..aa0c1763 100644
--- a/theories/lifetime/model/borrow_sep.v
+++ b/theories/lifetime/model/borrow_sep.v
@@ -25,7 +25,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_valid_discrete_2.
+ as %[EQB%to_borUR_included _]%auth_both_valid.
iMod (slice_iff _ _ true with "HPP' Hslice Hbox")
as (s' Pb') "(% & #HPbPb' & Hslice & Hbox)"; first solve_ndisj.
{ by rewrite lookup_fmap EQB. }
@@ -93,9 +93,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_valid_discrete_2.
+ as %[EQB1%to_borUR_included _]%auth_both_valid.
iDestruct (own_bor_valid_2 with "Hown Hbor2")
- as %[EQB2%to_borUR_included _]%auth_valid_discrete_2.
+ as %[EQB2%to_borUR_included _]%auth_both_valid.
iAssert ⌜j1 ≠j2âŒ%I with "[#]" as %Hj1j2.
{ iDestruct (own_bor_valid_2 with "Hbor1 Hbor2") as %Hj1j2%auth_valid_discrete.
iPureIntro. iIntros (->). (* FIXME this used to work without iPureIntro. *)
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index 672bf284..72ed9049 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -32,7 +32,7 @@ Proof.
iDestruct (@big_sepS_elem_of with "Hdead") as "Hdead"; first by eauto.
rewrite /lft_inv_dead; iDestruct "Hdead" as (R) "(_ & Hcnt' & _)".
iDestruct (own_cnt_valid_2 with "Hcnt' Hcnt")
- as %[?%nat_included _]%auth_valid_discrete_2; lia. }
+ as %[?%nat_included _]%auth_both_valid; 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 (n) "[Hcnt Hvs]".
@@ -129,7 +129,7 @@ Proof.
iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
rewrite /lft_tok big_sepMS_singleton.
iDestruct (own_valid_2 with "HA HΛ")
- as %[[s [?%leibniz_equiv ?]]%singleton_included _]%auth_valid_discrete_2.
+ as %[[s [?%leibniz_equiv ?]]%singleton_included _]%auth_both_valid.
iMod (own_update_2 with "HA HΛ") as "[HA HΛ]".
{ by eapply auth_update, singleton_local_update,
(exclusive_local_update _ (Cinr ())). }
diff --git a/theories/lifetime/model/faking.v b/theories/lifetime/model/faking.v
index decf7ad3..58c3ebe5 100644
--- a/theories/lifetime/model/faking.v
+++ b/theories/lifetime/model/faking.v
@@ -16,12 +16,12 @@ Proof.
iIntros "HA HI Hinv".
destruct (decide (is_Some (I !! κ))) as [?|HIκ%eq_None_not_Some].
{ iModIntro. iExists A, I. by iFrame. }
- iMod (own_alloc (◠0 ⋅ ◯ 0)) as (γcnt) "[Hcnt Hcnt']"; first done.
+ iMod (own_alloc (◠0 ⋅ ◯ 0)) as (γcnt) "[Hcnt Hcnt']"; first by apply auth_both_valid.
iMod (own_alloc ((◠∅ ⋅ ◯ ∅) :auth (gmap slice_name
(frac * agree bor_stateC)))) as (γbor) "[Hbor Hbor']";
- first by apply auth_valid_discrete_2.
+ first by apply auth_both_valid.
iMod (own_alloc ((◠ε) :auth (gset_disj slice_name)))
- as (γinh) "Hinh"; first by done.
+ as (γinh) "Hinh"; first by apply auth_auth_valid.
set (γs := LftNames γbor γcnt γinh).
iMod (own_update with "HI") as "[HI Hγs]".
{ apply auth_update_alloc,
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index 4086a824..6d16148d 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -22,8 +22,8 @@ Lemma lft_init `{!lftPreG Σ} E :
↑lftN ⊆ E → (|={E}=> ∃ _ : lftG Σ, lft_ctx)%I.
Proof.
iIntros (?). rewrite /lft_ctx.
- iMod (own_alloc (◠∅ : authR alftUR)) as (γa) "Ha"; first done.
- iMod (own_alloc (◠∅ : authR ilftUR)) as (γi) "Hi"; first done.
+ iMod (own_alloc (◠∅ : authR alftUR)) as (γa) "Ha"; first by apply auth_auth_valid.
+ iMod (own_alloc (◠∅ : authR ilftUR)) as (γi) "Hi"; first by apply auth_auth_valid.
set (HlftG := LftG _ _ _ γa _ γi _ _ _). iExists HlftG.
iMod (inv_alloc _ _ lfts_inv with "[Ha Hi]") as "$"; last done.
iModIntro. rewrite /lfts_inv /own_alft_auth /own_ilft_auth. iExists ∅, ∅.
@@ -37,7 +37,7 @@ Lemma own_ilft_auth_agree (I : gmap lft lft_names) κ γs :
own ilft_name (â—¯ {[κ := to_agree γs]}) -∗ ⌜is_Some (I !! κ)âŒ.
Proof.
iIntros "HI Hκ". iDestruct (own_valid_2 with "HI Hκ")
- as %[[? [Hl ?]]%singleton_included _]%auth_valid_discrete_2.
+ as %[[? [Hl ?]]%singleton_included _]%auth_both_valid.
unfold to_ilftUR in *. simplify_map_eq.
destruct (fmap_Some_equiv_1 _ _ _ Hl) as (?&?&?). eauto.
Qed.
@@ -47,7 +47,7 @@ Lemma own_alft_auth_agree (A : gmap atomic_lft bool) Λ b :
own alft_name (â—¯ {[Λ := to_lft_stateR b]}) -∗ ⌜A !! Λ = Some bâŒ.
Proof.
iIntros "HA HΛ".
- iDestruct (own_valid_2 with "HA HΛ") as %[HA _]%auth_valid_discrete_2.
+ iDestruct (own_valid_2 with "HA HΛ") as %[HA _]%auth_both_valid.
iPureIntro. move: HA=> /singleton_included [qs [/leibniz_equiv_iff]].
rewrite lookup_fmap fmap_Some=> -[b' [? ->]] /Some_included.
move=> [/leibniz_equiv_iff|/csum_included]; destruct b, b'; naive_solver.
@@ -65,8 +65,8 @@ Proof.
{ iDestruct 1 as (γs) "[#? [Hx Hy]]"; iSplitL "Hx"; iExists γs; eauto. }
iIntros "[Hx Hy]".
iDestruct "Hx" as (γs) "[Hγs Hx]"; iDestruct "Hy" as (γs') "[Hγs' Hy]".
- iDestruct (own_valid_2 with "Hγs Hγs'") as %Hγs%auth_own_valid.
- move: Hγs; rewrite /= op_singleton singleton_valid=> /agree_op_invL' <-.
+ iDestruct (own_valid_2 with "Hγs Hγs'") as %Hγs. move : Hγs.
+ rewrite -auth_frag_op auth_frag_valid op_singleton singleton_valid=> /agree_op_invL' <-.
iExists γs. iSplit. done. rewrite own_op; iFrame.
Qed.
Global Instance own_bor_into_op κ x x1 x2 :
@@ -99,14 +99,14 @@ Proof.
{ iDestruct 1 as (γs) "[#? [Hx Hy]]"; iSplitL "Hx"; iExists γs; eauto. }
iIntros "[Hx Hy]".
iDestruct "Hx" as (γs) "[Hγs Hx]"; iDestruct "Hy" as (γs') "[Hγs' Hy]".
- iDestruct (own_valid_2 with "Hγs Hγs'") as %Hγs%auth_own_valid.
- move: Hγs; rewrite /= op_singleton singleton_valid=> /agree_op_invL'=> <-.
+ iDestruct (own_valid_2 with "Hγs Hγs'") as %Hγs. move: Hγs.
+ rewrite -auth_frag_op auth_frag_valid op_singleton singleton_valid=> /agree_op_invL'=> <-.
iExists γs. iSplit; first done. rewrite own_op; iFrame.
Qed.
Global Instance own_cnt_into_op κ x x1 x2 :
IsOp x x1 x2 → IntoSep (own_cnt κ x) (own_cnt κ x1) (own_cnt κ x2).
Proof.
- rewrite /IsOp /IntoSep=> /leibniz_equiv_iff->. by rewrite -own_cnt_op.
+ rewrite /IsOp /IntoSep=> ->. by rewrite -own_cnt_op.
Qed.
Lemma own_cnt_valid κ x : own_cnt κ x -∗ ✓ x.
Proof. iDestruct 1 as (γs) "[#? Hx]". by iApply own_valid. Qed.
@@ -133,14 +133,14 @@ Proof.
{ iDestruct 1 as (γs) "[#? [Hx Hy]]"; iSplitL "Hx"; iExists γs; eauto. }
iIntros "[Hx Hy]".
iDestruct "Hx" as (γs) "[Hγs Hx]"; iDestruct "Hy" as (γs') "[Hγs' Hy]".
- iDestruct (own_valid_2 with "Hγs Hγs'") as %Hγs%auth_own_valid.
- move: Hγs; rewrite /= op_singleton singleton_valid=> /agree_op_invL' <-.
+ iDestruct (own_valid_2 with "Hγs Hγs'") as %Hγs. move: Hγs.
+ rewrite -auth_frag_op auth_frag_valid op_singleton singleton_valid=> /agree_op_invL'=> <-.
iExists γs. iSplit. done. rewrite own_op; iFrame.
Qed.
Global Instance own_inh_into_op κ x x1 x2 :
IsOp x x1 x2 → IntoSep (own_inh κ x) (own_inh κ x1) (own_inh κ x2).
Proof.
- rewrite /IsOp /IntoSep=> /leibniz_equiv_iff->. by rewrite -own_inh_op.
+ rewrite /IsOp /IntoSep=> ->. by rewrite -own_inh_op.
Qed.
Lemma own_inh_valid κ x : own_inh κ x -∗ ✓ x.
Proof. iDestruct 1 as (γs) "[#? Hx]". by iApply own_valid. Qed.
@@ -277,7 +277,7 @@ Proof.
rewrite /lft_tok /lft_dead. iIntros "H"; iDestruct 1 as (Λ') "[% H']".
iDestruct (@big_sepMS_elem_of _ _ _ _ _ _ Λ' with "H") as "H"=> //.
iDestruct (own_valid_2 with "H H'") as %Hvalid.
- move: Hvalid=> /auth_own_valid /=; by rewrite op_singleton singleton_valid.
+ move: Hvalid=> /auth_frag_valid /=; by rewrite op_singleton singleton_valid.
Qed.
Lemma lft_tok_static q : q.[static]%I.
@@ -452,12 +452,12 @@ Proof.
iModIntro. iSplitL "Hbox HE".
{ iNext. rewrite /lft_inh. iExists ({[γE]} ∪ PE).
rewrite gset_to_gmap_union_singleton. iFrame. }
- clear dependent PE. rewrite -(left_id_L ε op (◯ GSet {[γE]})).
+ clear dependent PE. rewrite -(left_id ε op (◯ GSet {[γE]})).
iDestruct "HEâ—¯" as "[HEâ—¯' HEâ—¯]". iSplitL "HEâ—¯'".
{ 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_valid_discrete_2.
+ as %[Hle%gset_disj_included _]%auth_both_valid.
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 d7e2e4b0..283317ab 100644
--- a/theories/lifetime/model/reborrow.v
+++ b/theories/lifetime/model/reborrow.v
@@ -34,7 +34,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_valid_discrete_2.
+ as %[HB%to_borUR_included _]%auth_both_valid.
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]".
@@ -75,7 +75,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_valid_discrete_2.
+ as %[HB%to_borUR_included _]%auth_both_valid.
iMod (own_bor_update_2 with "HBâ— Hi") as "[HBâ— Hi]".
{ eapply auth_update, singleton_local_update,
(exclusive_local_update _ (1%Qp, to_agree Bor_in)); last done.
@@ -118,7 +118,7 @@ Proof.
iDestruct "Hinvκ" as (Pb Pi) "(Halive & Hvs & Hinh)".
iDestruct "Halive" as (B) "(Hbox & >Hâ— & HB)".
iDestruct (own_bor_valid_2 with "Hâ— Hbor")
- as %[EQB%to_borUR_included _]%auth_valid_discrete_2.
+ as %[EQB%to_borUR_included _]%auth_both_valid.
iMod (slice_empty _ _ true with "Hs' Hbox") as "[Hidx Hbox]".
solve_ndisj. by rewrite lookup_fmap EQB.
iAssert (▷ idx_bor_own 1 (κ, i))%I with "[Hidx]" as ">Hidx"; [by iApply "HP'"|].
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index 742eea03..d74d620b 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -1,6 +1,6 @@
From Coq.QArith Require Import Qcanon.
From iris.proofmode Require Import tactics.
-From iris.algebra Require Import auth csum frac agree.
+From iris.algebra Require Import auth csum frac agree excl.
From lrust.lang.lib Require Import memcpy.
From lrust.lifetime Require Import na_borrow.
From lrust.typing Require Export type.
@@ -159,7 +159,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_valid_discrete_2. }
+ { by apply auth_both_valid. }
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. iExists _.
@@ -282,7 +282,7 @@ Section code.
iMod (na_inv_open 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_valid_discrete_2.
+ %option_included _]%prod_included [Hval _]]%auth_both_valid.
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].
@@ -337,7 +337,7 @@ Section code.
iMod (na_inv_open 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_valid_discrete_2.
+ %option_included _]%prod_included [Hval _]]%auth_both_valid.
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 _. }
@@ -408,7 +408,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_valid_discrete_2;
+ %option_included _]%prod_included [Hval _]]%auth_both_valid;
setoid_subst; try done; last first.
{ exfalso. destruct Hincl as [Hincl|Hincl]. by inversion Hincl.
apply csum_included in Hincl. naive_solver. }
@@ -467,7 +467,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_valid_discrete_2;
+ %option_included _]%prod_included [Hval _]]%auth_both_valid;
setoid_subst; try done; last first.
{ exfalso. destruct Hincl as [Hincl|Hincl]. by inversion Hincl.
apply csum_included in Hincl. naive_solver. }
@@ -572,7 +572,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_valid_discrete_2;
+ %option_included _]%prod_included [Hval _]]%auth_both_valid;
setoid_subst; try done; last first.
{ exfalso. destruct Hincl as [Hincl|Hincl]. by inversion Hincl.
apply csum_included in Hincl. naive_solver. }
@@ -1066,7 +1066,8 @@ Section code.
with "[>Hty]" as (γ ν q') "(Hty & Htok & Hν)".
{ 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]"=>//.
+ rc_tok (1/2)%Qp)) as (γ) "[Ha Hf]";
+ first by apply auth_both_valid.
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 12ab5f8b..230bbf11 100644
--- a/theories/typing/lib/rc/weak.v
+++ b/theories/typing/lib/rc/weak.v
@@ -158,7 +158,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_valid_discrete_2.
+ %[[_ Hweak%nat_included]%prod_included [Hval _]]%auth_both_valid.
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ν†)".
@@ -261,7 +261,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_valid_discrete_2;
+ %option_included _]%prod_included [Hval _]]%auth_both_valid;
setoid_subst; try done; last first.
{ exfalso. destruct Hincl as [Hincl|Hincl]. by inversion Hincl.
apply csum_included in Hincl. naive_solver. }
@@ -327,7 +327,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_valid_discrete_2.
+ %[[_ Hweak%nat_included]%prod_included [Hval _]]%auth_both_valid.
iMod (own_update with "Hrcâ—") as "[Hrcâ— $]".
{ by apply auth_update_alloc, prod_local_update_2,
(op_local_update_discrete _ _ 1%nat). }
@@ -400,7 +400,7 @@ Section code.
iMod (na_inv_open 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_valid_discrete_2.
+ %[[_ Hweak%nat_included]%prod_included [Hval _]]%auth_both_valid.
destruct weakc; first by simpl in *; lia.
iMod (own_update_2 with "Hrcâ— Hwtok") as "Hrcâ—".
{ apply auth_update_dealloc, prod_local_update_2,
@@ -473,7 +473,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_valid_discrete_2. by split. }
+ { apply auth_both_valid. 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 181d9dde..35d2901d 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -26,7 +26,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_valid_discrete_2; simpl in *; subst.
+ %option_included Hv]%auth_both_valid; simpl in *; subst.
- apply (inj to_agree), (inj2 pair) in Eq_ag.
destruct Eq_ag. setoid_subst. eauto.
- revert Hle=> /prod_included [/= /prod_included
@@ -166,7 +166,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_valid_discrete_2.
+ %Some_included _]%auth_both_valid.
- 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/refcell.v b/theories/typing/lib/refcell/refcell.v
index ebb22eba..b82faca9 100644
--- a/theories/typing/lib/refcell/refcell.v
+++ b/theories/typing/lib/refcell/refcell.v
@@ -137,7 +137,8 @@ Section refcell.
- iMod (bor_exists with "LFT Hb") as (γ) "Hb". done.
iExists κ, γ. iSplitR. by iApply lft_incl_refl. by iApply bor_na. }
clear dependent n. iDestruct "H" as ([|n|n]) "Hn"; try lia.
- - iFrame. iMod (own_alloc (◠None)) as (γ) "Hst". done. iExists γ, None. by iFrame.
+ - iFrame. iMod (own_alloc (◠None)) as (γ) "Hst"; first by apply auth_auth_valid.
+ iExists γ, None. by iFrame.
- iMod (lft_create with "LFT") as (ν) "[[Htok1 Htok2] #Hhν]". done.
iMod (own_alloc (◠(refcell_st_to_R $ Some (ν, false, (1/2)%Qp, n)))) as (γ) "Hst".
{ by apply auth_auth_valid. }
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index 719970bd..43e25130 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -131,7 +131,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_valid_discrete_2.
+ %auth_both_valid.
destruct st as [[[[??]?]?]|]; [|done]. move: Hst=>-[= ???]. subst.
destruct INCL as [[[[ν' ?]%to_agree_inj ?] ?]|
[[[??]%to_agree_included [q'' Hq'']]%prod_included [n' Hn']]%prod_included].
@@ -299,7 +299,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_valid_discrete_2.
+ iDestruct (own_valid_2 with "H◠Hγ") as %[Hst _]%auth_both_valid.
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 4d4e1a47..92cd7181 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -1,5 +1,5 @@
From iris.proofmode Require Import tactics.
-From iris.algebra Require Import auth csum frac agree.
+From iris.algebra Require Import auth csum frac agree excl.
From iris.bi Require Import fractional.
From lrust.lifetime Require Import at_borrow.
From lrust.typing Require Import typing.
@@ -128,7 +128,8 @@ Section rwlock.
iExists κ, γ. iSplitR. by iApply lft_incl_refl. iApply bor_share; try done.
solve_ndisj. }
clear dependent n. iDestruct "H" as ([|n|[]]) "[Hn >%]"; try lia.
- - iFrame. iMod (own_alloc (◠None)) as (γ) "Hst". done. iExists γ, None. by iFrame.
+ - iFrame. iMod (own_alloc (◠None)) as (γ) "Hst"; first by apply auth_auth_valid.
+ iExists γ, None. by iFrame.
- iMod (lft_create with "LFT") as (ν) "[[Htok1 Htok2] #Hhν]". done.
iMod (own_alloc (◠Some (Cinr (to_agree ν, (1/2)%Qp, n)))) as (γ) "Hst".
{ by apply auth_auth_valid. }
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index fccc7cea..0cca47c4 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -87,7 +87,7 @@ Section rwlockreadguard_functions.
(lx' ↦ #(Z_of_rwlock_st st'-1) ==∗ rwlock_inv tid lx' γ β ty))%I
with "[H◠H◯ Hx' Hν Hst H†]" as "INV".
{ iDestruct (own_valid_2 with "Hâ— Hâ—¯") as %[[[=]| (? & st0 & [=<-] & -> & [Heq|Hle])]
- %option_included Hv]%auth_valid_discrete_2.
+ %option_included Hv]%auth_both_valid.
- destruct st0 as [|[[agν q']n]|]; try by inversion Heq. revert Heq. simpl.
intros [[EQ <-%leibniz_equiv]%(inj2 pair) <-%leibniz_equiv]
%(inj Cinr)%(inj2 pair).
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard_code.v b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
index b9c9010a..0646d740 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
@@ -126,7 +126,7 @@ Section rwlockwriteguard_functions.
iDestruct "INV" as (st) "(H↦ & H◠& INV)". wp_write.
iMod ("Hcloseβ" with "[> H↦ H◠H◯ INV Hx']") as "Hβ".
{ iDestruct (own_valid_2 with "Hâ— Hâ—¯") as %[[[=]| (? & st0 & [=<-] & -> &
- [Heq|Hle])]%option_included Hv]%auth_valid_discrete_2;
+ [Heq|Hle])]%option_included Hv]%auth_both_valid;
last by destruct (exclusive_included _ _ Hle).
destruct st0 as [[[]|]| |]; try by inversion Heq.
iExists None. iFrame. iMod (own_update_2 with "Hâ— Hâ—¯") as "$"; last done.
--
GitLab