diff --git a/CHANGELOG.md b/CHANGELOG.md
index 28c4f0b84caf8009a8f75a4d773d3d132060ab5b..d295f277e4b71a29db7456d15dd07e4aaa2cf379 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -112,6 +112,13 @@ Changes in Coq:
`(λ: x, e)` no longer add a `locked`. Instead, we made the `wp_` tactics
smarter to no longer unfold lambdas/recs that occur behind definitions.
* Export the fact that `iPreProp` is a COFE.
+* The CMRA `auth` now can have fractional authoritative parts. So now `auth` has
+ 3 types of elements: the fractional authoritative `â—{q} a`, the full
+ authoritative `â— a ≡ â—{1} a`, and the non-authoritative `â—¯ a`. Updates are
+ only possible with the full authoritative element `â— a`, while fractional
+ authoritative elements have agreement: `✓ (â—{p} a â‹… â—{q} b) ⇒ a ≡ b`. As a
+ consequence, `auth` is no longer a COFE and does not preserve Leibniz
+ equality.
## Iris 3.1.0 (released 2017-12-19)
diff --git a/theories/algebra/agree.v b/theories/algebra/agree.v
index cf7a5d31bb64aabbe9dd42d346931c95db2ebb19..360dc4778c5cab280d9bb560556d69067fb45add 100644
--- a/theories/algebra/agree.v
+++ b/theories/algebra/agree.v
@@ -28,7 +28,8 @@ Proof.
(** Note that the projection [agree_car] is not non-expansive, so it cannot be
used in the logic. If you need to get a witness out, you should use the
-lemma [to_agree_uninjN] instead. *)
+lemma [to_agree_uninjN] instead. In general, [agree_car] should ONLY be used
+internally in this file. *)
Record agree (A : Type) : Type := {
agree_car : list A;
agree_not_nil : bool_decide (agree_car = []) = false
diff --git a/theories/algebra/auth.v b/theories/algebra/auth.v
index d6f038dd57b91d7be8a1b34f9e0cc908b327ffc9..ec5d2b9bfa3bd7a72b961eb1cd9e9d73a663a518 100644
--- a/theories/algebra/auth.v
+++ b/theories/algebra/auth.v
@@ -1,61 +1,74 @@
-From iris.algebra Require Export excl local_updates.
+From iris.algebra Require Export frac agree local_updates.
From iris.algebra Require Import proofmode_classes.
From iris.base_logic Require Import base_logic.
+From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
-Record auth (A : Type) := Auth { authoritative : excl' A; auth_own : A }.
+(** Authoritative CMRA with fractional authoritative parts. [auth] has 3 types
+ of elements: the fractional authoritative `â—{q} a`, the full authoritative
+ `â— a ≡ â—{1} a`, and the non-authoritative `â—¯ a`. Updates are only possible
+ with the full authoritative element `â— a`, while fractional authoritative
+ elements have agreement: `✓ (â—{p} a â‹… â—{q} b) ⇒ a ≡ b`.
+*)
+
+Record auth (A : Type) :=
+ Auth { auth_auth_proj : option (frac * agree A) ; auth_frag_proj : A }.
Add Printing Constructor auth.
Arguments Auth {_} _ _.
-Arguments authoritative {_} _.
-Arguments auth_own {_} _.
+Arguments auth_auth_proj {_} _.
+Arguments auth_frag_proj {_} _.
Instance: Params (@Auth) 1 := {}.
-Instance: Params (@authoritative) 1 := {}.
-Instance: Params (@auth_own) 1 := {}.
-Notation "â—¯ a" := (Auth None a) (at level 20).
-Notation "◠a" := (Auth (Excl' a) ε) (at level 20).
+Instance: Params (@auth_auth_proj) 1 := {}.
+Instance: Params (@auth_frag_proj) 1 := {}.
+
+Definition auth_frag {A: ucmraT} (a: A) : auth A := (Auth None a).
+Definition auth_auth {A: ucmraT} (q: Qp) (a: A): auth A :=
+ (Auth (Some (q, to_agree a)) ε).
+
+Typeclasses Opaque auth_auth auth_frag.
+
+Instance: Params (@auth_frag) 1 := {}.
+Instance: Params (@auth_auth) 1 := {}.
+
+Notation "â—¯ a" := (auth_frag a) (at level 20).
+Notation "â—{ q } a" := (auth_auth q a) (at level 20, format "â—{ q } a").
+Notation "â— a" := (auth_auth 1 a) (at level 20).
(* COFE *)
Section cofe.
Context {A : ofeT}.
-Implicit Types a : excl' A.
+Implicit Types a : option (frac * agree A).
Implicit Types b : A.
Implicit Types x y : auth A.
Instance auth_equiv : Equiv (auth A) := λ x y,
- authoritative x ≡ authoritative y ∧ auth_own x ≡ auth_own y.
+ auth_auth_proj x ≡ auth_auth_proj y ∧ auth_frag_proj x ≡ auth_frag_proj y.
Instance auth_dist : Dist (auth A) := λ n x y,
- authoritative x ≡{n}≡ authoritative y ∧ auth_own x ≡{n}≡ auth_own y.
+ auth_auth_proj x ≡{n}≡ auth_auth_proj y ∧
+ auth_frag_proj x ≡{n}≡ auth_frag_proj y.
Global Instance Auth_ne : NonExpansive2 (@Auth A).
Proof. by split. Qed.
Global Instance Auth_proper : Proper ((≡) ==> (≡) ==> (≡)) (@Auth A).
Proof. by split. Qed.
-Global Instance authoritative_ne: NonExpansive (@authoritative A).
+Global Instance auth_auth_proj_ne: NonExpansive (@auth_auth_proj A).
Proof. by destruct 1. Qed.
-Global Instance authoritative_proper : Proper ((≡) ==> (≡)) (@authoritative A).
+Global Instance auth_auth_proj_proper : Proper ((≡) ==> (≡)) (@auth_auth_proj A).
Proof. by destruct 1. Qed.
-Global Instance own_ne : NonExpansive (@auth_own A).
+Global Instance auth_frag_proj_ne : NonExpansive (@auth_frag_proj A).
Proof. by destruct 1. Qed.
-Global Instance own_proper : Proper ((≡) ==> (≡)) (@auth_own A).
+Global Instance auth_frag_proj_proper : Proper ((≡) ==> (≡)) (@auth_frag_proj A).
Proof. by destruct 1. Qed.
Definition auth_ofe_mixin : OfeMixin (auth A).
-Proof. by apply (iso_ofe_mixin (λ x, (authoritative x, auth_own x))). Qed.
+Proof. by apply (iso_ofe_mixin (λ x, (auth_auth_proj x, auth_frag_proj x))). Qed.
Canonical Structure authC := OfeT (auth A) auth_ofe_mixin.
-Global Instance auth_cofe `{!Cofe A} : Cofe authC.
-Proof.
- apply (iso_cofe (λ y : _ * _, Auth (y.1) (y.2))
- (λ x, (authoritative x, auth_own x))); by repeat intro.
-Qed.
-
Global Instance Auth_discrete a b :
Discrete a → Discrete b → Discrete (Auth a b).
Proof. by intros ?? [??] [??]; split; apply: discrete. Qed.
Global Instance auth_ofe_discrete : OfeDiscrete A → OfeDiscrete authC.
Proof. intros ? [??]; apply _. Qed.
-Global Instance auth_leibniz : LeibnizEquiv A → LeibnizEquiv (auth A).
-Proof. by intros ? [??] [??] [??]; f_equal/=; apply leibniz_equiv. Qed.
End cofe.
Arguments authC : clear implicits.
@@ -66,75 +79,145 @@ Context {A : ucmraT}.
Implicit Types a b : A.
Implicit Types x y : auth A.
+Global Instance auth_frag_ne: NonExpansive (@auth_frag A).
+Proof. done. Qed.
+Global Instance auth_frag_proper : Proper ((≡) ==> (≡)) (@auth_frag A).
+Proof. done. Qed.
+Global Instance auth_auth_ne q : NonExpansive (@auth_auth A q).
+Proof. solve_proper. Qed.
+Global Instance auth_auth_proper : Proper ((≡) ==> (≡) ==> (≡)) (@auth_auth A).
+Proof. solve_proper. Qed.
+Global Instance auth_auth_discrete q a :
+ Discrete a → Discrete (ε : A) → Discrete (â—{q} a).
+Proof. intros. apply Auth_discrete; apply _. Qed.
+Global Instance auth_frag_discrete a : Discrete a → Discrete (◯ a).
+Proof. intros. apply Auth_discrete; apply _. Qed.
+
Instance auth_valid : Valid (auth A) := λ x,
- match authoritative x with
- | Excl' a => (∀ n, auth_own x ≼{n} a) ∧ ✓ a
- | None => ✓ auth_own x
- | ExclBot' => False
+ match auth_auth_proj x with
+ | Some (q, ag) =>
+ ✓ q ∧ (∀ n, ∃ a, ag ≡{n}≡ to_agree a ∧ auth_frag_proj x ≼{n} a ∧ ✓{n} a)
+ | None => ✓ auth_frag_proj x
end.
Global Arguments auth_valid !_ /.
Instance auth_validN : ValidN (auth A) := λ n x,
- match authoritative x with
- | Excl' a => auth_own x ≼{n} a ∧ ✓{n} a
- | None => ✓{n} auth_own x
- | ExclBot' => False
+ match auth_auth_proj x with
+ | Some (q, ag) =>
+ ✓{n} q ∧ ∃ a, ag ≡{n}≡ to_agree a ∧ auth_frag_proj x ≼{n} a ∧ ✓{n} a
+ | None => ✓{n} auth_frag_proj x
end.
Global Arguments auth_validN _ !_ /.
Instance auth_pcore : PCore (auth A) := λ x,
- Some (Auth (core (authoritative x)) (core (auth_own x))).
+ Some (Auth (core (auth_auth_proj x)) (core (auth_frag_proj x))).
Instance auth_op : Op (auth A) := λ x y,
- Auth (authoritative x â‹… authoritative y) (auth_own x â‹… auth_own y).
+ Auth (auth_auth_proj x â‹… auth_auth_proj y) (auth_frag_proj x â‹… auth_frag_proj y).
Definition auth_valid_eq :
- valid = λ x, match authoritative x with
- | Excl' a => (∀ n, auth_own x ≼{n} a) ∧ ✓ a
- | None => ✓ auth_own x
- | ExclBot' => False
+ valid = λ x, match auth_auth_proj x with
+ | Some (q, ag) => ✓ q ∧ (∀ n, ∃ a, ag ≡{n}≡ to_agree a ∧ auth_frag_proj x ≼{n} a ∧ ✓{n} a)
+ | None => ✓ auth_frag_proj x
end := eq_refl _.
Definition auth_validN_eq :
- validN = λ n x, match authoritative x with
- | Excl' a => auth_own x ≼{n} a ∧ ✓{n} a
- | None => ✓{n} auth_own x
- | ExclBot' => False
+ validN = λ n x, match auth_auth_proj x with
+ | Some (q, ag) => ✓{n} q ∧ ∃ a, ag ≡{n}≡ to_agree a ∧ auth_frag_proj x ≼{n} a ∧ ✓{n} a
+ | None => ✓{n} auth_frag_proj x
end := eq_refl _.
Lemma auth_included (x y : auth A) :
- x ≼ y ↔ authoritative x ≼ authoritative y ∧ auth_own x ≼ auth_own y.
+ x ≼ y ↔
+ auth_auth_proj x ≼ auth_auth_proj y ∧ auth_frag_proj x ≼ auth_frag_proj y.
Proof.
split; [intros [[z1 z2] Hz]; split; [exists z1|exists z2]; apply Hz|].
intros [[z1 Hz1] [z2 Hz2]]; exists (Auth z1 z2); split; auto.
Qed.
-Lemma authoritative_validN n x : ✓{n} x → ✓{n} authoritative x.
-Proof. by destruct x as [[[]|]]. Qed.
-Lemma auth_own_validN n x : ✓{n} x → ✓{n} auth_own x.
+Lemma auth_auth_proj_validN n x : ✓{n} x → ✓{n} auth_auth_proj x.
+Proof. destruct x as [[[]|]]; [by intros (? & ? & -> & ?)|done]. Qed.
+Lemma auth_frag_proj_validN n x : ✓{n} x → ✓{n} auth_frag_proj x.
Proof.
rewrite auth_validN_eq.
- destruct x as [[[]|]]; naive_solver eauto using cmra_validN_includedN.
+ destruct x as [[[]|]]; [|done]. naive_solver eauto using cmra_validN_includedN.
+Qed.
+Lemma auth_auth_proj_valid x : ✓ x → ✓ auth_auth_proj x.
+Proof.
+ destruct x as [[[]|]]; [intros [? H]|done]. split; [done|].
+ intros n. by destruct (H n) as [? [-> [? ?]]].
+Qed.
+Lemma auth_frag_proj_valid x : ✓ x → ✓ auth_frag_proj x.
+Proof.
+ destruct x as [[[]|]]; [intros [? H]|done]. apply cmra_valid_validN.
+ intros n. destruct (H n) as [? [? [? ?]]].
+ naive_solver eauto using cmra_validN_includedN.
+Qed.
+
+Lemma auth_frag_validN n a : ✓{n} a ↔ ✓{n} (◯ a).
+Proof. done. Qed.
+Lemma auth_auth_frac_validN n q a :
+ ✓{n} (â—{q} a) ↔ ✓{n} q ∧ ✓{n} a.
+Proof.
+ rewrite auth_validN_eq /=. apply and_iff_compat_l. split.
+ - by intros [?[->%to_agree_injN []]].
+ - naive_solver eauto using ucmra_unit_leastN.
+Qed.
+Lemma auth_auth_validN n a : ✓{n} a ↔ ✓{n} (◠a).
+Proof.
+ rewrite auth_auth_frac_validN -cmra_discrete_valid_iff frac_valid'. naive_solver.
+Qed.
+Lemma auth_both_frac_validN n q a b :
+ ✓{n} (â—{q} a â‹… â—¯ b) ↔ ✓{n} q ∧ b ≼{n} a ∧ ✓{n} a.
+Proof.
+ rewrite auth_validN_eq /=. apply and_iff_compat_l.
+ setoid_rewrite (left_id _ _ b). split.
+ - by intros [?[->%to_agree_injN]].
+ - naive_solver.
+Qed.
+Lemma auth_both_validN n a b : ✓{n} (◠a ⋅ ◯ b) ↔ b ≼{n} a ∧ ✓{n} a.
+Proof.
+ rewrite auth_both_frac_validN -cmra_discrete_valid_iff frac_valid'. naive_solver.
+Qed.
+
+Lemma auth_frag_valid a : ✓ a ↔ ✓ (◯ a).
+Proof. done. Qed.
+Lemma auth_auth_frac_valid q a : ✓ q ∧ ✓ a ↔ ✓ (â—{q} a).
+Proof.
+ rewrite auth_valid_eq /=. apply and_iff_compat_l. split.
+ - intros. exists a. split; [done|].
+ split; by [apply ucmra_unit_leastN|apply cmra_valid_validN].
+ - intros H'. apply cmra_valid_validN. intros n.
+ by destruct (H' n) as [? [->%to_agree_injN [??]]].
+Qed.
+Lemma auth_auth_valid a : ✓ a ↔ ✓ (◠a).
+Proof. rewrite -auth_auth_frac_valid frac_valid'. naive_solver. Qed.
+Lemma auth_both_frac_valid q a b : ✓ q → ✓ a → b ≼ a → ✓ (â—{q} a â‹… â—¯ b).
+Proof.
+ intros Val1 Val2 Incl. rewrite auth_valid_eq /=. split; [done|].
+ intros n. exists a. split; [done|]. rewrite left_id.
+ split; by [apply cmra_included_includedN|apply cmra_valid_validN].
Qed.
+Lemma auth_both_valid a b : ✓ a → b ≼ a → ✓ (◠a ⋅ ◯ b).
+Proof. intros ??. by apply auth_both_frac_valid. Qed.
Lemma auth_valid_discrete `{!CmraDiscrete A} x :
- ✓ x ↔ match authoritative x with
- | Excl' a => auth_own x ≼ a ∧ ✓ a
- | None => ✓ auth_own x
- | ExclBot' => False
+ ✓ x ↔ match auth_auth_proj x with
+ | Some (q, ag) => ✓ q ∧ ∃ a, ag ≡ to_agree a ∧ auth_frag_proj x ≼ a ∧ ✓ a
+ | None => ✓ auth_frag_proj x
end.
Proof.
- rewrite auth_valid_eq. destruct x as [[[?|]|] ?]; simpl; try done.
- setoid_rewrite <-cmra_discrete_included_iff; naive_solver eauto using 0.
+ rewrite auth_valid_eq. destruct x as [[[??]|] ?]; simpl; [|done].
+ setoid_rewrite <-cmra_discrete_included_iff.
+ setoid_rewrite <-(discrete_iff _ a).
+ setoid_rewrite <-cmra_discrete_valid_iff. naive_solver eauto using O.
Qed.
-Lemma auth_validN_2 n a b : ✓{n} (◠a ⋅ ◯ b) ↔ b ≼{n} a ∧ ✓{n} a.
-Proof. by rewrite auth_validN_eq /= left_id. Qed.
-Lemma auth_valid_discrete_2 `{!CmraDiscrete A} a b : ✓ (◠a ⋅ ◯ b) ↔ b ≼ a ∧ ✓ a.
-Proof. by rewrite auth_valid_discrete /= left_id. Qed.
-
-Lemma authoritative_valid x : ✓ x → ✓ authoritative x.
-Proof. by destruct x as [[[]|]]. Qed.
-Lemma auth_own_valid `{!CmraDiscrete A} x : ✓ x → ✓ auth_own x.
+Lemma auth_frac_valid_discrete_2 `{!CmraDiscrete A} q a b :
+ ✓ (â—{q} a â‹… â—¯ b) ↔ ✓ q ∧ b ≼ a ∧ ✓ a.
Proof.
- rewrite auth_valid_discrete.
- destruct x as [[[]|]]; naive_solver eauto using cmra_valid_included.
+ rewrite auth_valid_discrete /=. apply and_iff_compat_l.
+ setoid_rewrite (left_id _ _ b). split.
+ - by intros [?[->%to_agree_inj]].
+ - naive_solver.
Qed.
+Lemma auth_valid_discrete_2 `{!CmraDiscrete A} a b : ✓ (◠a ⋅ ◯ b) ↔ b ≼ a ∧ ✓ a.
+Proof. rewrite auth_frac_valid_discrete_2 frac_valid'. naive_solver. Qed.
Lemma auth_cmra_mixin : CmraMixin (auth A).
Proof.
@@ -143,12 +226,12 @@ Proof.
- by intros n x y1 y2 [Hy Hy']; split; simpl; rewrite ?Hy ?Hy'.
- by intros n y1 y2 [Hy Hy']; split; simpl; rewrite ?Hy ?Hy'.
- intros n [x a] [y b] [Hx Ha]; simpl in *. rewrite !auth_validN_eq.
- destruct Hx as [?? Hx|]; first destruct Hx; intros ?; ofe_subst; auto.
- - intros [[[?|]|] ?]; rewrite /= ?auth_valid_eq
- ?auth_validN_eq /= ?cmra_included_includedN ?cmra_valid_validN;
- naive_solver eauto using O.
- - intros n [[[]|] ?]; rewrite !auth_validN_eq /=;
- naive_solver eauto using cmra_includedN_S, cmra_validN_S.
+ destruct Hx as [x y Hx|]; first destruct Hx as [? Hx];
+ [destruct x,y|]; intros VI; ofe_subst; auto.
+ - intros [[[]|] ]; rewrite /= ?auth_valid_eq ?auth_validN_eq /=
+ ?cmra_valid_validN; naive_solver.
+ - intros n [[[]|] ]; rewrite !auth_validN_eq /=;
+ naive_solver eauto using dist_S, cmra_includedN_S, cmra_validN_S.
- by split; simpl; rewrite assoc.
- by split; simpl; rewrite comm.
- by split; simpl; rewrite ?cmra_core_l.
@@ -157,13 +240,17 @@ Proof.
by split; simpl; apply: cmra_core_mono. (* FIXME: apply cmra_core_mono. fails *)
- assert (∀ n (a b1 b2 : A), b1 ⋅ b2 ≼{n} a → b1 ≼{n} a).
{ intros n a b1 b2 <-; apply cmra_includedN_l. }
- intros n [[[a1|]|] b1] [[[a2|]|] b2]; rewrite auth_validN_eq;
- naive_solver eauto using cmra_validN_op_l, cmra_validN_includedN.
+ intros n [[[q1 a1]|] b1] [[[q2 a2]|] b2]; rewrite auth_validN_eq /=;
+ try naive_solver eauto using cmra_validN_op_l, cmra_validN_includedN.
+ intros [? [a [Eq [? Valid]]]].
+ assert (Eq': a1 ≡{n}≡ a2). { by apply agree_op_invN; rewrite Eq. }
+ split; [naive_solver eauto using cmra_validN_op_l|].
+ exists a. rewrite -Eq -Eq' agree_idemp. naive_solver.
- intros n x y1 y2 ? [??]; simpl in *.
- destruct (cmra_extend n (authoritative x) (authoritative y1)
- (authoritative y2)) as (ea1&ea2&?&?&?); auto using authoritative_validN.
- destruct (cmra_extend n (auth_own x) (auth_own y1) (auth_own y2))
- as (b1&b2&?&?&?); auto using auth_own_validN.
+ destruct (cmra_extend n (auth_auth_proj x) (auth_auth_proj y1)
+ (auth_auth_proj y2)) as (ea1&ea2&?&?&?); auto using auth_auth_proj_validN.
+ destruct (cmra_extend n (auth_frag_proj x) (auth_frag_proj y1) (auth_frag_proj y2))
+ as (b1&b2&?&?&?); auto using auth_frag_proj_validN.
by exists (Auth ea1 b1), (Auth ea2 b2).
Qed.
Canonical Structure authR := CmraT (auth A) auth_cmra_mixin.
@@ -171,9 +258,11 @@ Canonical Structure authR := CmraT (auth A) auth_cmra_mixin.
Global Instance auth_cmra_discrete : CmraDiscrete A → CmraDiscrete authR.
Proof.
split; first apply _.
- intros [[[?|]|] ?]; rewrite auth_valid_eq auth_validN_eq /=; auto.
+ intros [[[]|] ?]; rewrite auth_valid_eq auth_validN_eq /=; auto.
- setoid_rewrite <-cmra_discrete_included_iff.
- rewrite -cmra_discrete_valid_iff. tauto.
+ rewrite -cmra_discrete_valid_iff.
+ setoid_rewrite <-cmra_discrete_valid_iff.
+ setoid_rewrite <-(discrete_iff _ a). tauto.
- by rewrite -cmra_discrete_valid_iff.
Qed.
@@ -183,25 +272,13 @@ Proof.
split; simpl.
- rewrite auth_valid_eq /=. apply ucmra_unit_valid.
- by intros x; constructor; rewrite /= left_id.
- - do 2 constructor; simpl; apply (core_id_core _).
+ - do 2 constructor; [done| apply (core_id_core _)].
Qed.
Canonical Structure authUR := UcmraT (auth A) auth_ucmra_mixin.
Global Instance auth_frag_core_id a : CoreId a → CoreId (◯ a).
Proof. do 2 constructor; simpl; auto. by apply core_id_core. Qed.
-(** Internalized properties *)
-Lemma auth_equivI {M} x y :
- x ≡ y ⊣⊢@{uPredI M} authoritative x ≡ authoritative y ∧ auth_own x ≡ auth_own y.
-Proof. by uPred.unseal. Qed.
-Lemma auth_validI {M} x :
- ✓ x ⊣⊢@{uPredI M} match authoritative x with
- | Excl' a => (∃ b, a ≡ auth_own x ⋅ b) ∧ ✓ a
- | None => ✓ auth_own x
- | ExclBot' => False
- end.
-Proof. uPred.unseal. by destruct x as [[[]|]]. Qed.
-
Lemma auth_frag_op a b : â—¯ (a â‹… b) = â—¯ a â‹… â—¯ b.
Proof. done. Qed.
Lemma auth_frag_mono a b : a ≼ b → ◯ a ≼ ◯ b.
@@ -211,21 +288,77 @@ Global Instance auth_frag_sep_homomorphism :
MonoidHomomorphism op op (≡) (@Auth A None).
Proof. by split; [split; try apply _|]. Qed.
-Lemma auth_both_op a b : Auth (Excl' a) b ≡ ◠a ⋅ ◯ b.
+Lemma auth_both_frac_op q a b : Auth (Some (q,to_agree a)) b ≡ â—{q} a â‹… â—¯ b.
Proof. by rewrite /op /auth_op /= left_id. Qed.
-Lemma auth_auth_valid a : ✓ a → ✓ (◠a).
-Proof. intros; split; simpl; auto using ucmra_unit_leastN. Qed.
+Lemma auth_both_op a b : Auth (Some (1%Qp,to_agree a)) b ≡ ◠a ⋅ ◯ b.
+Proof. by rewrite auth_both_frac_op. Qed.
+
+Lemma auth_auth_frac_op p q a: â—{p} a â‹… â—{q} a ≡ â—{p + q} a.
+Proof.
+ intros; split; simpl; last by rewrite left_id.
+ by rewrite -Some_op pair_op agree_idemp.
+Qed.
+Lemma auth_auth_frac_op_invN n p a q b : ✓{n} (â—{p} a â‹… â—{q} b) → a ≡{n}≡ b.
+Proof.
+ rewrite /op /auth_op /= left_id -Some_op pair_op auth_validN_eq /=.
+ intros (?&?& Eq &?&?). apply to_agree_injN, agree_op_invN. by rewrite Eq.
+Qed.
+Lemma auth_auth_frac_op_inv p a q b : ✓ (â—{p} a â‹… â—{q} b) → a ≡ b.
+Proof.
+ intros ?. apply equiv_dist. intros n.
+ by eapply auth_auth_frac_op_invN, cmra_valid_validN.
+Qed.
+Lemma auth_auth_frac_op_invL `{!LeibnizEquiv A} q a p b :
+ ✓ (â—{p} a â‹… â—{q} b) → a = b.
+Proof. by intros ?%auth_auth_frac_op_inv%leibniz_equiv. Qed.
+
+(** Internalized properties *)
+Lemma auth_equivI {M} x y :
+ x ≡ y ⊣⊢@{uPredI M} auth_auth_proj x ≡ auth_auth_proj y ∧ auth_frag_proj x ≡ auth_frag_proj y.
+Proof. by uPred.unseal. Qed.
+Lemma auth_validI {M} x :
+ ✓ x ⊣⊢@{uPredI M} match auth_auth_proj x with
+ | Some (q, ag) => ✓ q ∧
+ ∃ a, ag ≡ to_agree a ∧ (∃ b, a ≡ auth_frag_proj x ⋅ b) ∧ ✓ a
+ | None => ✓ auth_frag_proj x
+ end.
+Proof. uPred.unseal. by destruct x as [[[]|]]. Qed.
+Lemma auth_frag_validI {M} (a : A):
+ ✓ (◯ a) ⊣⊢@{uPredI M} ✓ a.
+Proof. by rewrite auth_validI. Qed.
+
+Lemma auth_both_validI {M} q (a b: A) :
+ ✓ (â—{q} a â‹… â—¯ b) ⊣⊢@{uPredI M} ✓ q ∧ (∃ c, a ≡ b â‹… c) ∧ ✓ a.
+Proof.
+ rewrite -auth_both_frac_op auth_validI /=. apply bi.and_proper; [done|].
+ setoid_rewrite agree_equivI. iSplit.
+ - iDestruct 1 as (a') "[#Eq [H V]]". iDestruct "H" as (b') "H".
+ iRewrite -"Eq" in "H". iRewrite -"Eq" in "V". auto.
+ - iDestruct 1 as "[H V]". iExists a. auto.
+Qed.
+Lemma auth_auth_validI {M} q (a b: A) :
+ ✓ (â—{q} a) ⊣⊢@{uPredI M} ✓ q ∧ ✓ a.
+Proof.
+ rewrite auth_validI /=. apply bi.and_proper; [done|].
+ setoid_rewrite agree_equivI. iSplit.
+ - iDestruct 1 as (a') "[Eq [_ V]]". by iRewrite -"Eq" in "V".
+ - iIntros "V". iExists a. iSplit; [done|]. iSplit; [|done]. iExists a.
+ by rewrite left_id.
+Qed.
Lemma auth_update a b a' b' :
(a,b) ~l~> (a',b') → ◠a ⋅ ◯ b ~~> ◠a' ⋅ ◯ b'.
Proof.
intros Hup; apply cmra_total_update.
- move=> n [[[?|]|] bf1] // [[bf2 Ha] ?]; do 2 red; simpl in *.
- move: Ha; rewrite !left_id -assoc=> Ha.
- destruct (Hup n (Some (bf1 â‹… bf2))); auto.
- split; last done. exists bf2. by rewrite -assoc.
+ move=> n [[[??]|] bf1] [/= VL [a0 [Eq [[bf2 Ha] VL2]]]]; do 2 red; simpl in *.
+ + exfalso. move : VL => /frac_valid'.
+ rewrite frac_op'. by apply Qp_not_plus_q_ge_1.
+ + split; [done|]. apply to_agree_injN in Eq.
+ move: Ha; rewrite !left_id -assoc => Ha.
+ destruct (Hup n (Some (bf1 â‹… bf2))); [by rewrite Eq..|]. simpl in *.
+ exists a'. split; [done|]. split; [|done]. exists bf2.
+ by rewrite left_id -assoc.
Qed.
-
Lemma auth_update_alloc a a' b' : (a,ε) ~l~> (a',b') → ◠a ~~> ◠a' ⋅ ◯ b'.
Proof. intros. rewrite -(right_id _ _ (â— a)). by apply auth_update. Qed.
Lemma auth_update_dealloc a b a' : (a,b) ~l~> (a',ε) → ◠a ⋅ ◯ b ~~> ◠a'.
@@ -236,12 +369,15 @@ Lemma auth_local_update (a b0 b1 a' b0' b1': A) :
(â— a â‹… â—¯ b0, â— a â‹… â—¯ b1) ~l~> (â— a' â‹… â—¯ b0', â— a' â‹… â—¯ b1').
Proof.
rewrite !local_update_unital=> Hup ? ? n /=.
- move=> [[[ac|]|] bc] /auth_validN_2 [Le Val] [] /=;
- inversion_clear 1 as [?? Ha|]; inversion_clear Ha. (* need setoid_discriminate! *)
- rewrite !left_id=> ?.
- destruct (Hup n bc) as [Hval' Heq]; eauto using cmra_validN_includedN.
- rewrite -!auth_both_op auth_validN_eq /=.
- split_and!; [by apply cmra_included_includedN|by apply cmra_valid_validN|done].
+ move=> [[[qc ac]|] bc] /auth_both_validN [Le Val] [] /=.
+ - move => Ha. exfalso. move : Ha. rewrite right_id -Some_op pair_op.
+ move => /Some_dist_inj [/=]. rewrite frac_op' => Eq _.
+ apply (Qp_not_plus_q_ge_1 qc). by rewrite -Eq.
+ - move => _. rewrite !left_id=> ?.
+ destruct (Hup n bc) as [Hval' Heq]; eauto using cmra_validN_includedN.
+ rewrite -!auth_both_op auth_validN_eq /=.
+ split_and!; [done| |done]. exists a'.
+ split_and!; [done|by apply cmra_included_includedN|by apply cmra_valid_validN].
Qed.
End cmra.
@@ -252,41 +388,50 @@ Arguments authUR : clear implicits.
Instance is_op_auth_frag {A : ucmraT} (a b1 b2 : A) :
IsOp a b1 b2 → IsOp' (◯ a) (◯ b1) (◯ b2).
Proof. done. Qed.
+Instance is_op_auth_auth_frac {A : ucmraT} (q q1 q2 : frac) (a : A) :
+ IsOp q q1 q2 → IsOp' (â—{q} a) (â—{q1} a) (â—{q2} a).
+Proof. rewrite /IsOp' /IsOp => ->. by rewrite -auth_auth_frac_op. Qed.
(* Functor *)
Definition auth_map {A B} (f : A → B) (x : auth A) : auth B :=
- Auth (excl_map f <$> authoritative x) (f (auth_own x)).
+ Auth (prod_map id (agree_map f) <$> auth_auth_proj x) (f (auth_frag_proj x)).
Lemma auth_map_id {A} (x : auth A) : auth_map id x = x.
-Proof. by destruct x as [[[]|]]. Qed.
+Proof. destruct x as [[[]|] ]; by rewrite // /auth_map /= agree_map_id. Qed.
Lemma auth_map_compose {A B C} (f : A → B) (g : B → C) (x : auth A) :
auth_map (g ∘ f) x = auth_map g (auth_map f x).
-Proof. by destruct x as [[[]|]]. Qed.
-Lemma auth_map_ext {A B : ofeT} (f g : A → B) x :
+Proof. destruct x as [[[]|] ]; by rewrite // /auth_map /= agree_map_compose. Qed.
+Lemma auth_map_ext {A B : ofeT} (f g : A → B) `{_ : NonExpansive f} x :
(∀ x, f x ≡ g x) → auth_map f x ≡ auth_map g x.
Proof.
constructor; simpl; auto.
- apply option_fmap_equiv_ext=> a; by apply excl_map_ext.
+ apply option_fmap_equiv_ext=> a; by rewrite /prod_map /= agree_map_ext.
Qed.
-Instance auth_map_ne {A B : ofeT} n :
- Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@auth_map A B).
+Instance auth_map_ne {A B : ofeT} (f : A -> B) {Hf : NonExpansive f} :
+ NonExpansive (auth_map f).
Proof.
- intros f g Hf [??] [??] [??]; split; simpl in *; [|by apply Hf].
- apply option_fmap_ne; [|done]=> x y ?; by apply excl_map_ne.
+ intros n [??] [??] [??]; split; simpl in *; [|by apply Hf].
+ apply option_fmap_ne; [|done]=> x y ?. apply prod_map_ne; [done| |done].
+ by apply agree_map_ne.
Qed.
Instance auth_map_cmra_morphism {A B : ucmraT} (f : A → B) :
CmraMorphism f → CmraMorphism (auth_map f).
Proof.
split; try apply _.
- - intros n [[[a|]|] b]; rewrite !auth_validN_eq; try
- naive_solver eauto using cmra_morphism_monotoneN, cmra_morphism_validN.
+ - intros n [[[??]|] b]; rewrite !auth_validN_eq;
+ [|naive_solver eauto using cmra_morphism_monotoneN, cmra_morphism_validN].
+ intros [? [a' [Eq [? ?]]]]. split; [done|]. exists (f a').
+ rewrite -agree_map_to_agree -Eq.
+ naive_solver eauto using cmra_morphism_monotoneN, cmra_morphism_validN.
- intros [??]. apply Some_proper; rewrite /auth_map /=.
by f_equiv; rewrite /= cmra_morphism_core.
- - intros [[?|]?] [[?|]?]; try apply Auth_proper=>//=; by rewrite cmra_morphism_op.
+ - intros [[[??]|]?] [[[??]|]?]; try apply Auth_proper=>//=; try by rewrite cmra_morphism_op.
+ by rewrite -Some_op pair_op cmra_morphism_op.
Qed.
Definition authC_map {A B} (f : A -n> B) : authC A -n> authC B :=
CofeMor (auth_map f).
Lemma authC_map_ne A B : NonExpansive (@authC_map A B).
-Proof. intros n f f' Hf [[[a|]|] b]; repeat constructor; apply Hf. Qed.
+Proof. intros n f f' Hf [[[]|] ]; repeat constructor; try naive_solver;
+ apply agreeC_map_ne; auto. Qed.
Program Definition authRF (F : urFunctor) : rFunctor := {|
rFunctor_car A B := authR (urFunctor_car F A B);
@@ -297,11 +442,11 @@ Next Obligation.
Qed.
Next Obligation.
intros F A B x. rewrite /= -{2}(auth_map_id x).
- apply auth_map_ext=>y; apply urFunctor_id.
+ apply auth_map_ext=>y. apply _. apply urFunctor_id.
Qed.
Next Obligation.
intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -auth_map_compose.
- apply auth_map_ext=>y; apply urFunctor_compose.
+ apply auth_map_ext=>y. apply _. apply urFunctor_compose.
Qed.
Instance authRF_contractive F :
@@ -319,11 +464,11 @@ Next Obligation.
Qed.
Next Obligation.
intros F A B x. rewrite /= -{2}(auth_map_id x).
- apply auth_map_ext=>y; apply urFunctor_id.
+ apply auth_map_ext=>y. apply _. apply urFunctor_id.
Qed.
Next Obligation.
intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -auth_map_compose.
- apply auth_map_ext=>y; apply urFunctor_compose.
+ apply auth_map_ext=>y. apply _. apply urFunctor_compose.
Qed.
Instance authURF_contractive F :
diff --git a/theories/algebra/frac_auth.v b/theories/algebra/frac_auth.v
index 30cf54715ea4e496fb14f3dc014fd93ce8b6e58d..0706fe627a43af9fecdd99b5b0b5d0ff2b6a597d 100644
--- a/theories/algebra/frac_auth.v
+++ b/theories/algebra/frac_auth.v
@@ -2,6 +2,13 @@ From iris.algebra Require Export frac auth.
From iris.algebra Require Export updates local_updates.
From iris.algebra Require Import proofmode_classes.
+(** Authoritative CMRA where the NON-authoritative parts can be fractional.
+ This CMRA allows the original non-authoritative element `â—¯ a` to be split into
+ fractional parts `◯!{q} a`. Using `◯! a ≡ ◯!{1} a` is in effect the same as
+ using the original `â—¯ a`. Currently, however, this CMRA hides the ability to
+ split the authoritative part into fractions.
+*)
+
Definition frac_authR (A : cmraT) : cmraT :=
authR (optionUR (prodR fracR A)).
Definition frac_authUR (A : cmraT) : ucmraT :=
@@ -35,18 +42,18 @@ Section frac_auth.
Proof. solve_proper. Qed.
Global Instance frac_auth_auth_discrete a : Discrete a → Discrete (â—! a).
- Proof. intros; apply Auth_discrete; apply _. Qed.
+ Proof. intros; apply auth_auth_discrete; [apply Some_discrete|]; apply _. Qed.
Global Instance frac_auth_frag_discrete a : Discrete a → Discrete (◯! a).
- Proof. intros; apply Auth_discrete, Some_discrete; apply _. Qed.
+ Proof. intros; apply auth_frag_discrete, Some_discrete; apply _. Qed.
Lemma frac_auth_validN n a : ✓{n} a → ✓{n} (â—! a â‹… â—¯! a).
- Proof. done. Qed.
+ Proof. by rewrite auth_both_validN. Qed.
Lemma frac_auth_valid a : ✓ a → ✓ (â—! a â‹… â—¯! a).
- Proof. done. Qed.
+ Proof. intros. by apply auth_both_valid. Qed.
Lemma frac_auth_agreeN n a b : ✓{n} (â—! a â‹… â—¯! b) → a ≡{n}≡ b.
Proof.
- rewrite auth_validN_eq /= => -[Hincl Hvalid].
+ rewrite auth_both_validN /= => -[Hincl Hvalid].
by move: Hincl=> /Some_includedN_exclusive /(_ Hvalid ) [??].
Qed.
Lemma frac_auth_agree a b : ✓ (â—! a â‹… â—¯! b) → a ≡ b.
@@ -57,10 +64,10 @@ Section frac_auth.
Proof. intros. by apply leibniz_equiv, frac_auth_agree. Qed.
Lemma frac_auth_includedN n q a b : ✓{n} (â—! a â‹… â—¯!{q} b) → Some b ≼{n} Some a.
- Proof. by rewrite auth_validN_eq /= => -[/Some_pair_includedN [_ ?] _]. Qed.
+ Proof. by rewrite auth_both_validN /= => -[/Some_pair_includedN [_ ?] _]. Qed.
Lemma frac_auth_included `{CmraDiscrete A} q a b :
✓ (â—! a â‹… â—¯!{q} b) → Some b ≼ Some a.
- Proof. by rewrite auth_valid_discrete /= => -[/Some_pair_included [_ ?] _]. Qed.
+ Proof. by rewrite auth_valid_discrete_2 /= => -[/Some_pair_included [_ ?] _]. Qed.
Lemma frac_auth_includedN_total `{CmraTotal A} n q a b :
✓{n} (â—! a â‹… â—¯!{q} b) → b ≼{n} a.
Proof. intros. by eapply Some_includedN_total, frac_auth_includedN. Qed.
@@ -70,8 +77,8 @@ Section frac_auth.
Lemma frac_auth_auth_validN n a : ✓{n} (â—! a) ↔ ✓{n} a.
Proof.
- split; [by intros [_ [??]]|].
- by repeat split; simpl; auto using ucmra_unit_leastN.
+ rewrite auth_auth_frac_validN Some_validN. split.
+ by intros [?[]]. intros. by split.
Qed.
Lemma frac_auth_auth_valid a : ✓ (â—! a) ↔ ✓ a.
Proof. rewrite !cmra_valid_validN. by setoid_rewrite frac_auth_auth_validN. Qed.
diff --git a/theories/base_logic/lib/auth.v b/theories/base_logic/lib/auth.v
index 2664ddc3d4b728e6df3725f837100b1b2c2168d0..2a6974c29769c2dd8cb88b772108023dbd59d805 100644
--- a/theories/base_logic/lib/auth.v
+++ b/theories/base_logic/lib/auth.v
@@ -94,7 +94,7 @@ Section auth.
Lemma auth_own_mono γ a b : a ≼ b → auth_own γ b ⊢ auth_own γ a.
Proof. intros [? ->]. by rewrite auth_own_op sep_elim_l. Qed.
Lemma auth_own_valid γ a : auth_own γ a ⊢ ✓ a.
- Proof. by rewrite /auth_own own_valid auth_validI. Qed.
+ Proof. by rewrite /auth_own own_valid auth_frag_validI. Qed.
Global Instance auth_own_sep_homomorphism γ :
WeakMonoidHomomorphism op uPred_sep (≡) (auth_own γ).
Proof. split; try apply _. apply auth_own_op. Qed.
@@ -107,8 +107,8 @@ Section auth.
✓ (f t) → ▷ φ t ={E}=∗ ∃ γ, ⌜I γ⌠∧ auth_ctx γ N f φ ∧ auth_own γ (f t).
Proof.
iIntros (??) "Hφ". rewrite /auth_own /auth_ctx.
- iMod (own_alloc_strong (Auth (Excl' (f t)) (f t)) I) as (γ) "[% Hγ]"; [done|done|].
- iRevert "Hγ"; rewrite auth_both_op; iIntros "[Hγ Hγ']".
+ iMod (own_alloc_strong (◠f t ⋅ ◯ f t) I) as (γ) "[% [Hγ Hγ']]";
+ [done|by apply auth_valid_discrete_2|].
iMod (inv_alloc N _ (auth_inv γ f φ) with "[-Hγ']") as "#?".
{ iNext. rewrite /auth_inv. iExists t. by iFrame. }
eauto.
diff --git a/theories/base_logic/lib/boxes.v b/theories/base_logic/lib/boxes.v
index 84bbe329a2f2a120ad758e5ca50190e96ac3cc60..597c05835f1bd95bfd75fcb68c5360f9d89316ca 100644
--- a/theories/base_logic/lib/boxes.v
+++ b/theories/base_logic/lib/boxes.v
@@ -1,5 +1,5 @@
From iris.base_logic.lib Require Export invariants.
-From iris.algebra Require Import auth gmap agree.
+From iris.algebra Require Import excl auth gmap agree.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Import uPred.
@@ -78,7 +78,7 @@ Lemma box_own_auth_agree γ b1 b2 :
box_own_auth γ (â— Excl' b1) ∗ box_own_auth γ (â—¯ Excl' b2) ⊢ ⌜b1 = b2âŒ.
Proof.
rewrite /box_own_prop -own_op own_valid prod_validI /= and_elim_l.
- by iDestruct 1 as % [[[] [=]%leibniz_equiv] ?]%auth_valid_discrete.
+ by iDestruct 1 as % [[[] [=]%leibniz_equiv] ?]%auth_valid_discrete_2.
Qed.
Lemma box_own_auth_update γ b1 b2 b3 :
@@ -110,7 +110,7 @@ Proof.
iDestruct 1 as (Φ) "[#HeqP Hf]".
iMod (own_alloc_cofinite (â— Excl' false â‹… â—¯ Excl' false,
Some (to_agree (Next (iProp_unfold Q)))) (dom _ f))
- as (γ) "[Hdom Hγ]"; first done.
+ as (γ) "[Hdom Hγ]"; first by (split; [apply auth_valid_discrete_2|]).
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/base_logic/lib/gen_heap.v b/theories/base_logic/lib/gen_heap.v
index 8268ee417cd7168e1c54ccfc1669ef1f35b833c7..cb0b414a240dad85c02ebeeab93c04dfe90e29f8 100644
--- a/theories/base_logic/lib/gen_heap.v
+++ b/theories/base_logic/lib/gen_heap.v
@@ -76,7 +76,7 @@ Lemma gen_heap_init `{Countable L, !gen_heapPreG L V Σ} σ :
(|==> ∃ _ : gen_heapG L V Σ, gen_heap_ctx σ)%I.
Proof.
iMod (own_alloc (◠to_gen_heap σ)) as (γ) "Hh".
- { apply: auth_auth_valid. exact: to_gen_heap_valid. }
+ { rewrite -auth_auth_valid. exact: to_gen_heap_valid. }
iModIntro. by iExists (GenHeapG L V Σ _ _ _ γ).
Qed.
@@ -105,7 +105,7 @@ Section gen_heap.
Proof.
apply wand_intro_r.
rewrite mapsto_eq /mapsto_def -own_op -auth_frag_op own_valid discrete_valid.
- f_equiv=> /auth_own_valid /=. rewrite op_singleton singleton_valid pair_op.
+ f_equiv. rewrite -auth_frag_valid op_singleton singleton_valid pair_op.
by intros [_ ?%agree_op_invL'].
Qed.
@@ -122,8 +122,8 @@ Section gen_heap.
Lemma mapsto_valid l q v : l ↦{q} v -∗ ✓ q.
Proof.
- rewrite mapsto_eq /mapsto_def own_valid !discrete_valid.
- by apply pure_mono=> /auth_own_valid /singleton_valid [??].
+ rewrite mapsto_eq /mapsto_def own_valid !discrete_valid -auth_frag_valid.
+ by apply pure_mono=> /singleton_valid [??].
Qed.
Lemma mapsto_valid_2 l q1 q2 v1 v2 : l ↦{q1} v1 -∗ l ↦{q2} v2 -∗ ✓ (q1 + q2)%Qp.
Proof.
diff --git a/theories/base_logic/lib/proph_map.v b/theories/base_logic/lib/proph_map.v
index 22f3594928b9b422716a230f13b1ea6ae4f2c878..939ee30596e8547d80383b4cc1e98fa7cb82f7de 100644
--- a/theories/base_logic/lib/proph_map.v
+++ b/theories/base_logic/lib/proph_map.v
@@ -1,4 +1,4 @@
-From iris.algebra Require Import auth list gmap.
+From iris.algebra Require Import auth excl list gmap.
From iris.base_logic.lib Require Export own.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
@@ -111,7 +111,7 @@ Lemma proph_map_init `{Countable P, !proph_mapPreG P V PVS} pvs ps :
(|==> ∃ _ : proph_mapG P V PVS, proph_map_ctx pvs ps)%I.
Proof.
iMod (own_alloc (◠to_proph_map ∅)) as (γ) "Hh".
- { apply: auth_auth_valid. exact: to_proph_map_valid. }
+ { rewrite -auth_auth_valid. exact: to_proph_map_valid. }
iModIntro. iExists (ProphMapG P V PVS _ _ _ γ), ∅. iSplit; last by iFrame.
iPureIntro. split =>//.
Qed.
diff --git a/theories/base_logic/lib/wsat.v b/theories/base_logic/lib/wsat.v
index 78cb9f7645341533b0ad7ffe520e31e651fbdbdf..e09b59f9d14a72ce2d1070ebc19374860cf165c8 100644
--- a/theories/base_logic/lib/wsat.v
+++ b/theories/base_logic/lib/wsat.v
@@ -110,10 +110,10 @@ Lemma invariant_lookup (I : gmap positive (iProp Σ)) i P :
own invariant_name (◯ {[i := invariant_unfold P]}) ⊢
∃ Q, ⌜I !! i = Some Q⌠∗ ▷ (Q ≡ P).
Proof.
- rewrite -own_op own_valid auth_validI /=. iIntros "[#HI #HvI]".
+ rewrite -own_op own_valid auth_both_validI /=. iIntros "[_ [#HI #HvI]]".
iDestruct "HI" as (I') "HI". rewrite gmap_equivI gmap_validI.
iSpecialize ("HI" $! i). iSpecialize ("HvI" $! i).
- rewrite left_id_L lookup_fmap lookup_op lookup_singleton bi.option_equivI.
+ rewrite lookup_fmap lookup_op lookup_singleton bi.option_equivI.
case: (I !! i)=> [Q|] /=; [|case: (I' !! i)=> [Q'|] /=; by iExFalso].
iExists Q; iSplit; first done.
iAssert (invariant_unfold Q ≡ invariant_unfold P)%I as "?".
@@ -197,7 +197,8 @@ End wsat.
Lemma wsat_alloc `{!invPreG Σ} : (|==> ∃ _ : invG Σ, wsat ∗ ownE ⊤)%I.
Proof.
iIntros.
- iMod (own_alloc (◠(∅ : gmap _ _))) as (γI) "HI"; first done.
+ iMod (own_alloc (◠(∅ : gmap positive _))) as (γI) "HI";
+ first by rewrite -auth_auth_valid.
iMod (own_alloc (CoPset ⊤)) as (γE) "HE"; first done.
iMod (own_alloc (GSet ∅)) as (γD) "HD"; first done.
iModIntro; iExists (WsatG _ _ _ _ γI γE γD).
diff --git a/theories/heap_lang/lib/counter.v b/theories/heap_lang/lib/counter.v
index b49fff3ab6e11c44096c688db98edf4920529bb6..cb65f706b59cc6c8758b196c905d1640156d4d01 100644
--- a/theories/heap_lang/lib/counter.v
+++ b/theories/heap_lang/lib/counter.v
@@ -36,7 +36,8 @@ Section mono_proof.
{{{ True }}} newcounter #() {{{ l, RET #l; mcounter l 0 }}}.
Proof.
iIntros (Φ) "_ HΦ". rewrite -wp_fupd /newcounter /=. wp_lam. wp_alloc l as "Hl".
- iMod (own_alloc (◠(O:mnat) ⋅ ◯ (O:mnat))) as (γ) "[Hγ Hγ']"; first done.
+ iMod (own_alloc (◠(O:mnat) ⋅ ◯ (O:mnat))) as (γ) "[Hγ Hγ']";
+ first by apply auth_valid_discrete_2.
iMod (inv_alloc N _ (mcounter_inv γ l) with "[Hl Hγ]").
{ iNext. iExists 0%nat. by iFrame. }
iModIntro. iApply "HΦ". rewrite /mcounter; eauto 10.
@@ -113,7 +114,8 @@ Section contrib_spec.
{{{ γ l, RET #l; ccounter_ctx γ l ∗ ccounter γ 1 0 }}}.
Proof.
iIntros (Φ) "_ HΦ". rewrite -wp_fupd /newcounter /=. wp_lam. wp_alloc l as "Hl".
- iMod (own_alloc (â—! O%nat â‹… â—¯! 0%nat)) as (γ) "[Hγ Hγ']"; first done.
+ iMod (own_alloc (â—! O%nat â‹… â—¯! 0%nat)) as (γ) "[Hγ Hγ']";
+ first by apply auth_valid_discrete_2.
iMod (inv_alloc N _ (ccounter_inv γ l) with "[Hl Hγ]").
{ iNext. iExists 0%nat. by iFrame. }
iModIntro. iApply "HΦ". rewrite /ccounter_ctx /ccounter; eauto 10.
diff --git a/theories/heap_lang/lib/ticket_lock.v b/theories/heap_lang/lib/ticket_lock.v
index 017d256c7a6febf46c5bb15bf05abb5dc6abb64b..681b7a22b9e748690f1fe27fb166a4c70b280c20 100644
--- a/theories/heap_lang/lib/ticket_lock.v
+++ b/theories/heap_lang/lib/ticket_lock.v
@@ -2,7 +2,7 @@ From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation.
-From iris.algebra Require Import auth gset.
+From iris.algebra Require Import excl auth gset.
From iris.heap_lang.lib Require Export lock.
Set Default Proof Using "Type".
Import uPred.
@@ -76,7 +76,7 @@ Section proof.
iIntros (Φ) "HR HΦ". rewrite -wp_fupd. wp_lam.
wp_alloc ln as "Hln". wp_alloc lo as "Hlo".
iMod (own_alloc (◠(Excl' 0%nat, GSet ∅) ⋅ ◯ (Excl' 0%nat, GSet ∅))) as (γ) "[Hγ Hγ']".
- { by rewrite -auth_both_op. }
+ { by apply auth_valid_discrete_2. }
iMod (inv_alloc _ _ (lock_inv γ lo ln R) with "[-HΦ]").
{ iNext. rewrite /lock_inv.
iExists 0%nat, 0%nat. iFrame. iLeft. by iFrame. }
diff --git a/theories/program_logic/ownp.v b/theories/program_logic/ownp.v
index d48ef7a93774f68dca2d6fb5f41f21336ee290a5..0bbe407eeba6f29171c72072bfb371f9c432200c 100644
--- a/theories/program_logic/ownp.v
+++ b/theories/program_logic/ownp.v
@@ -1,7 +1,7 @@
From iris.program_logic Require Export weakestpre.
From iris.program_logic Require Import lifting adequacy.
From iris.program_logic Require ectx_language.
-From iris.algebra Require Import auth.
+From iris.algebra Require Import excl auth.
From iris.proofmode Require Import tactics classes.
Set Default Proof Using "Type".
@@ -53,7 +53,8 @@ Theorem ownP_adequacy Σ `{!ownPPreG Λ Σ} s e σ φ :
Proof.
intros Hwp. apply (wp_adequacy Σ _).
iIntros (? κs).
- iMod (own_alloc (◠(Excl' σ) ⋅ ◯ (Excl' σ))) as (γσ) "[Hσ Hσf]"; first done.
+ iMod (own_alloc (◠(Excl' σ) ⋅ ◯ (Excl' σ))) as (γσ) "[Hσ Hσf]";
+ first by apply auth_valid_discrete_2.
iModIntro. iExists (λ σ κs, own γσ (◠(Excl' σ)))%I.
iFrame "Hσ".
iApply (Hwp (OwnPG _ _ _ _ γσ)). rewrite /ownP. iFrame.
@@ -68,7 +69,8 @@ Theorem ownP_invariance Σ `{!ownPPreG Λ Σ} s e σ1 t2 σ2 φ :
Proof.
intros Hwp Hsteps. eapply (wp_invariance Σ Λ s e σ1 t2 σ2 _)=> //.
iIntros (? κs κs').
- iMod (own_alloc (◠(Excl' σ1) ⋅ ◯ (Excl' σ1))) as (γσ) "[Hσ Hσf]"; first done.
+ iMod (own_alloc (◠(Excl' σ1) ⋅ ◯ (Excl' σ1))) as (γσ) "[Hσ Hσf]";
+ first by apply auth_valid_discrete_2.
iExists (λ σ κs' _, own γσ (◠(Excl' σ)))%I, (λ _, True%I).
iFrame "Hσ".
iMod (Hwp (OwnPG _ _ _ _ γσ) with "[Hσf]") as "[$ H]";