Skip to content
Snippets Groups Projects

Compare revisions

Changes are shown as if the source revision was being merged into the target revision. Learn more about comparing revisions.

Source

Select target project
No results found

Target

Select target project
  • iris/iris
  • jeehoon.kang/iris-coq
  • amintimany/iris-coq
  • dfrumin/iris-coq
  • Villetaneuse/iris
  • gares/iris
  • shiatsumat/iris
  • Blaisorblade/iris
  • jihgfee/iris-coq
  • mrhaandi/iris
  • tlsomers/iris
  • Quarkbeast/iris-coq
  • janno/iris
  • amaurremi/iris-coq
  • proux/iris
  • tchajed/iris
  • herbelin/iris-coq
  • msammler/iris-coq
  • maximedenes/iris-coq
  • bpeters/iris
  • haidang/iris
  • lepigre/iris
  • lczch/iris
  • simonspies/iris
  • gpirlea/iris
  • dkhalanskiyjb/iris
  • gmalecha/iris
  • germanD/iris
  • aa755/iris
  • jules/iris
  • abeln/iris
  • simonfv/iris
  • atrieu/iris
  • arthuraa/iris
  • simonh/iris
  • jung/iris
  • mattam82/iris
  • Armael/iris
  • adamAndMath/iris
  • gmevel/iris
  • snyke7/iris
  • johannes/iris
  • NiklasM/iris
  • simonspies/iris-parametric-index
  • svancollem/iris
  • proux1/iris
  • wmansky/iris
  • LukeXuan/iris
  • ivanbakel/iris
  • SkySkimmer/iris
  • tjhance/iris
  • yiyunliu/iris
  • Lee-Janggun/iris
  • thomas-lamiaux/iris
  • dongjae/iris
  • dnezam/iris
  • Tragicus/iris
  • clef-men/iris
  • ffengyu/iris
59 results
Show changes
Showing
with 4455 additions and 145 deletions
From stdpp Require Export vector. From stdpp Require Export vector.
From iris.algebra Require Export ofe. From iris.algebra Require Export ofe.
From iris.algebra Require Import list. From iris.algebra Require Import list.
Set Default Proof Using "Type". From iris.prelude Require Import options.
Section ofe. Section ofe.
Context {A : ofeT}. Context {SI : sidx} {A : ofe}.
Instance vec_equiv m : Equiv (vec A m) := equiv (A:=list A). Local Instance vec_equiv m : Equiv (vec A m) := equiv (A:=list A).
Instance vec_dist m : Dist (vec A m) := dist (A:=list A). Local Instance vec_dist m : Dist (vec A m) := dist (A:=list A).
Definition vec_ofe_mixin m : OfeMixin (vec A m). Definition vec_ofe_mixin m : OfeMixin (vec A m).
Proof. by apply (iso_ofe_mixin vec_to_list). Qed. Proof. by apply (iso_ofe_mixin vec_to_list). Qed.
Canonical Structure vecC m : ofeT := OfeT (vec A m) (vec_ofe_mixin m). Canonical Structure vecO m : ofe := Ofe (vec A m) (vec_ofe_mixin m).
Global Instance list_cofe `{Cofe A} m : Cofe (vecC m). Global Instance list_cofe `{!Cofe A} m : Cofe (vecO m).
Proof. Proof.
apply: (iso_cofe_subtype (λ l : list A, length l = m) apply: (iso_cofe_subtype (λ l : list A, length l = m)
(λ l, eq_rect _ (vec A) (list_to_vec l) m) vec_to_list)=> //. (λ l, eq_rect _ (vec A) (list_to_vec l) m) vec_to_list)=> //.
- intros v []. by rewrite /= vec_to_list_of_list. - intros v []. by rewrite /= vec_to_list_to_vec.
- intros c. by rewrite (conv_compl 0 (chain_map _ c)) /= vec_to_list_length. - intros c. by rewrite (conv_compl 0 (chain_map _ c)) /= length_vec_to_list.
- intros n Hn c.
rewrite (conv_lbcompl Hn (bchain_map _ c) (SIdx.limit_lt_0 _ Hn)) /=.
by rewrite length_vec_to_list.
Qed. Qed.
Global Instance vnil_timeless : Timeless (@vnil A). Global Instance vnil_discrete : Discrete (@vnil A).
Proof. intros v _. by inv_vec v. Qed. Proof. intros v _. by inv_vec v. Qed.
Global Instance vcons_timeless n x (v : vec A n) : Global Instance vcons_discrete n x (v : vec A n) :
Timeless x Timeless v Timeless (x ::: v). Discrete x Discrete v Discrete (x ::: v).
Proof. Proof.
intros ?? v' ?. inv_vec v'=>x' v'. inversion_clear 1. intros ?? v' ?. inv_vec v'=>x' v'. inversion_clear 1.
constructor. by apply timeless. change (v v'). by apply timeless. constructor.
- by eapply discrete.
- change (v v'). by eapply discrete.
Qed. Qed.
Global Instance vec_discrete_cofe m : Discrete A Discrete (vecC m). Global Instance vec_ofe_discrete m : OfeDiscrete A OfeDiscrete (vecO m).
Proof. intros ? v. induction v; apply _. Qed. Proof. intros ? v. induction v; apply _. Qed.
End ofe. End ofe.
Arguments vecC : clear implicits. Global Arguments vecO {_} _.
Typeclasses Opaque vec_dist. Global Typeclasses Opaque vec_dist.
Section proper. Section proper.
Context {A : ofeT}. Context {SI : sidx} {A : ofe}.
Global Instance vcons_ne n : Global Instance vcons_ne n :
Proper (dist n ==> forall_relation (λ x, dist n ==> dist n)) (@vcons A). Proper (dist n ==> forall_relation (λ x, dist n ==> dist n)) (@vcons A).
...@@ -66,48 +71,49 @@ Section proper. ...@@ -66,48 +71,49 @@ Section proper.
End proper. End proper.
(** Functor *) (** Functor *)
Definition vec_map {A B : ofeT} m (f : A B) : vecC A m vecC B m := Definition vec_map {SI : sidx} {A B : ofe} m (f : A B) : vecO A m vecO B m :=
@vmap A B f m. @vmap A B f m.
Lemma vec_map_ext_ne {A B : ofeT} m (f g : A B) (v : vec A m) n : Lemma vec_map_ext_ne {SI : sidx} {A B : ofe} m (f g : A B) (v : vec A m) n :
( x, f x {n} g x) vec_map m f v {n} vec_map m g v. ( x, f x {n} g x) vec_map m f v {n} vec_map m g v.
Proof. Proof.
intros Hf. eapply (list_fmap_ext_ne f g v) in Hf. intros Hf. eapply (list_fmap_ext_ne f g v) in Hf.
by rewrite -!vec_to_list_map in Hf. by rewrite -!vec_to_list_map in Hf.
Qed. Qed.
Instance vec_map_ne {A B : ofeT} m f n : Global Instance vec_map_ne {SI : sidx} {A B : ofe} m f n :
Proper (dist n ==> dist n) f Proper (dist n ==> dist n) f
Proper (dist n ==> dist n) (@vec_map A B m f). Proper (dist n ==> dist n) (@vec_map SI A B m f).
Proof. Proof.
intros ? v v' H. eapply list_fmap_ne in H; last done. intros ? v v' H. eapply list_fmap_ne in H; last done.
by rewrite -!vec_to_list_map in H. by rewrite -!vec_to_list_map in H.
Qed. Qed.
Definition vecC_map {A B : ofeT} m (f : A -n> B) : vecC A m -n> vecC B m := Definition vecO_map {SI : sidx} {A B : ofe} m (f : A -n> B) : vecO A m -n> vecO B m :=
CofeMor (vec_map m f). OfeMor (vec_map m f).
Instance vecC_map_ne {A A'} m : Global Instance vecO_map_ne {SI : sidx} {A A'} m :
NonExpansive (@vecC_map A A' m). NonExpansive (@vecO_map SI A A' m).
Proof. intros n f g ? v. by apply vec_map_ext_ne. Qed. Proof. intros n f g ? v. by apply vec_map_ext_ne. Qed.
Program Definition vecCF (F : cFunctor) m : cFunctor := {| Program Definition vecOF {SI : sidx} (F : oFunctor) m : oFunctor := {|
cFunctor_car A B := vecC (cFunctor_car F A B) m; oFunctor_car A _ B _ := vecO (oFunctor_car F A B) m;
cFunctor_map A1 A2 B1 B2 fg := vecC_map m (cFunctor_map F fg) oFunctor_map A1 _ A2 _ B1 _ B2 _ fg := vecO_map m (oFunctor_map F fg)
|}. |}.
Next Obligation. Next Obligation.
intros F A1 A2 B1 B2 n m f g Hfg. by apply vecC_map_ne, cFunctor_ne. intros ? F A1 ? A2 ? B1 ? B2 ? n m f g Hfg. by apply vecO_map_ne, oFunctor_map_ne.
Qed. Qed.
Next Obligation. Next Obligation.
intros F m A B l. intros ? F m A ? B ? l.
change (vec_to_list (vec_map m (cFunctor_map F (cid, cid)) l) l). change (vec_to_list (vec_map m (oFunctor_map F (cid, cid)) l) l).
rewrite vec_to_list_map. apply listCF. rewrite vec_to_list_map. apply listOF.
Qed. Qed.
Next Obligation. Next Obligation.
intros F m A1 A2 A3 B1 B2 B3 f g f' g' l. intros ? F m A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' l.
change (vec_to_list (vec_map m (cFunctor_map F (f g, g' f')) l) change (vec_to_list (vec_map m (oFunctor_map F (f g, g' f')) l)
vec_map m (cFunctor_map F (g, g')) (vec_map m (cFunctor_map F (f, f')) l)). vec_map m (oFunctor_map F (g, g')) (vec_map m (oFunctor_map F (f, f')) l)).
rewrite !vec_to_list_map. by apply (cFunctor_compose (listCF F) f g f' g'). rewrite !vec_to_list_map. by apply: (oFunctor_map_compose (listOF F) f g f' g').
Qed. Qed.
Instance vecCF_contractive F m : Global Instance vecOF_contractive {SI : sidx} F m :
cFunctorContractive F cFunctorContractive (vecCF F m). oFunctorContractive F oFunctorContractive (vecOF F m).
Proof. Proof.
by intros ?? A1 A2 B1 B2 n ???; apply vecC_map_ne; first apply cFunctor_contractive. by intros ?? A1 ? A2 ? B1 ? B2 ? n ???; apply vecO_map_ne;
apply oFunctor_map_contractive.
Qed. Qed.
From iris.algebra Require Export updates local_updates frac dfrac agree.
From iris.algebra Require Import proofmode_classes big_op.
From iris.prelude Require Import options.
(** The view camera with fractional authoritative elements *)
(** The view camera, which is reminiscent of the views framework, is used to
provide a logical/"small-footprint" "view" of some "large-footprint" piece of
data, which can be shared in the separation logic sense, i.e., different parts
of the data can be separately owned by different functions or threads. This is
achieved using the two elements of the view camera:
- The authoritative element [●V a], which describes the data under consideration.
- The fragment [◯V b], which provides a logical view of the data [a].
To enable sharing of the fragments, the type of fragments is equipped with a
camera structure so ownership of fragments can be split. Concretely, fragments
enjoy the rule [◯V (b1 ⋅ b2) = ◯V b1 ⋅ ◯V b2].
To enable sharing of the authoritative element [●V{dq} a], it is equipped with a
discardable fraction [dq]. Updates are only possible with the full authoritative
element [●V a] (syntax for [●V{#1} a]]), while fractional authoritative elements
have agreement, i.e., [✓ (●V{dq1} a1 ⋅ ●V{dq2} a2) → a1 ≡ a2]. *)
(** * The view relation *)
(** To relate the authoritative element [a] to its possible fragments [b], the
view camera is parametrized by a (step-indexed) relation [view_rel n a b]. This
relation should be a.) closed under smaller step-indexes [n], b.) non-expansive
w.r.t. the argument [a], c.) closed under smaller [b] (which implies
non-expansiveness w.r.t. [b]), and d.) ensure validity of the argument [b].
Note 1: Instead of requiring both a step-indexed and a non-step-indexed version
of the relation (like cameras do for validity), we use [∀ n, view_rel n] as the
non-step-indexed version. This is anyway necessary when using [≼{n}] as the
relation (like the authoritative camera does) as its non-step-indexed version
is not equivalent to [∀ n, x ≼{n} y].
Note 2: The view relation is defined as a canonical structure so that given a
relation [nat → A → B → Prop], the instance with the laws can be inferred. We do
not use type classes for this purpose because cameras themselves are represented
using canonical structures. It has proven fragile for a canonical structure
instance to take a type class as a parameter (in this case, [viewR] would need
to take a class with the view relation laws). *)
Structure view_rel {SI : sidx} (A : ofe) (B : ucmra) := ViewRel {
view_rel_holds :> SI A B Prop;
view_rel_mono n1 n2 a1 a2 b1 b2 :
view_rel_holds n1 a1 b1
a1 {n2} a2
b2 {n2} b1
(n2 n1)%sidx
view_rel_holds n2 a2 b2;
view_rel_validN n a b :
view_rel_holds n a b {n} b;
view_rel_unit n :
a, view_rel_holds n a ε
}.
Global Arguments ViewRel {_ _ _} _ _.
Global Arguments view_rel_holds {_ _ _} _ _ _ _.
Global Instance: Params (@view_rel_holds) 5 := {}.
Global Instance view_rel_ne {SI : sidx} {A B} (rel : view_rel A B) n :
Proper (dist n ==> dist n ==> iff) (rel n).
Proof.
intros a1 a2 Ha b1 b2 Hb.
split=> ?; (eapply view_rel_mono; [done|done|by rewrite Hb|done]).
Qed.
Global Instance view_rel_proper {SI : sidx} {A B} (rel : view_rel A B) n :
Proper (() ==> () ==> iff) (rel n).
Proof. intros a1 a2 Ha b1 b2 Hb. apply view_rel_ne; by apply equiv_dist. Qed.
Class ViewRelDiscrete {SI : sidx} {A B} (rel : view_rel A B) :=
view_rel_discrete n a b : rel 0 a b rel n a b.
(** * Definition of the view camera *)
(** To make use of the lemmas provided in this file, elements of [view] should
always be constructed using [●V] and [◯V], and never using the constructor
[View]. *)
Record view {SI : sidx} {A B} (rel : SI A B Prop) :=
View { view_auth_proj : option (dfrac * agree A) ; view_frag_proj : B }.
Add Printing Constructor view.
Global Arguments View {_ _ _ _} _ _.
Global Arguments view_auth_proj {_ _ _ _} _.
Global Arguments view_frag_proj {_ _ _ _} _.
Global Instance: Params (@View) 4 := {}.
Global Instance: Params (@view_auth_proj) 4 := {}.
Global Instance: Params (@view_frag_proj) 4 := {}.
Definition view_auth {SI : sidx} {A B} {rel : view_rel A B}
(dq : dfrac) (a : A) : view rel :=
View (Some (dq, to_agree a)) ε.
Definition view_frag {SI : sidx} {A B} {rel : view_rel A B} (b : B) : view rel :=
View None b.
Global Typeclasses Opaque view_auth view_frag.
Global Instance: Params (@view_auth) 4 := {}.
Global Instance: Params (@view_frag) 4 := {}.
Notation "●V dq a" := (view_auth dq a)
(at level 20, dq custom dfrac at level 1, format "●V dq a").
Notation "◯V a" := (view_frag a) (at level 20).
(** * The OFE structure *)
(** We omit the usual [equivI] lemma because it is hard to state a suitably
general version in terms of [●V] and [◯V], and because such a lemma has never
been needed in practice. *)
Section ofe.
Context {SI : sidx} {A B : ofe} (rel : SI A B Prop).
Implicit Types a : A.
Implicit Types ag : option (dfrac * agree A).
Implicit Types b : B.
Implicit Types x y : view rel.
Local Instance view_equiv : Equiv (view rel) := λ x y,
view_auth_proj x view_auth_proj y view_frag_proj x view_frag_proj y.
Local Instance view_dist : Dist (view rel) := λ n x y,
view_auth_proj x {n} view_auth_proj y
view_frag_proj x {n} view_frag_proj y.
Global Instance View_ne : NonExpansive2 (@View SI A B rel).
Proof. by split. Qed.
Global Instance View_proper : Proper (() ==> () ==> ()) (@View SI A B rel).
Proof. by split. Qed.
Global Instance view_auth_proj_ne : NonExpansive (@view_auth_proj SI A B rel).
Proof. by destruct 1. Qed.
Global Instance view_auth_proj_proper :
Proper (() ==> ()) (@view_auth_proj SI A B rel).
Proof. by destruct 1. Qed.
Global Instance view_frag_proj_ne : NonExpansive (@view_frag_proj SI A B rel).
Proof. by destruct 1. Qed.
Global Instance view_frag_proj_proper :
Proper (() ==> ()) (@view_frag_proj SI A B rel).
Proof. by destruct 1. Qed.
Definition view_ofe_mixin : OfeMixin (view rel).
Proof. by apply (iso_ofe_mixin (λ x, (view_auth_proj x, view_frag_proj x))). Qed.
Canonical Structure viewO := Ofe (view rel) view_ofe_mixin.
Global Instance View_discrete ag b :
Discrete ag Discrete b Discrete (View ag b).
Proof. by intros ?? [??] [??]; split; apply: discrete. Qed.
Global Instance view_ofe_discrete :
OfeDiscrete A OfeDiscrete B OfeDiscrete viewO.
Proof. intros ?? [??]; apply _. Qed.
End ofe.
(** * The camera structure *)
Section cmra.
Context {SI : sidx} {A B} (rel : view_rel A B).
Implicit Types a : A.
Implicit Types ag : option (dfrac * agree A).
Implicit Types b : B.
Implicit Types x y : view rel.
Implicit Types q : frac.
Implicit Types dq : dfrac.
Global Instance view_auth_ne dq : NonExpansive (@view_auth SI A B rel dq).
Proof. solve_proper. Qed.
Global Instance view_auth_proper dq :
Proper (() ==> ()) (@view_auth SI A B rel dq).
Proof. solve_proper. Qed.
Global Instance view_frag_ne : NonExpansive (@view_frag SI A B rel).
Proof. done. Qed.
Global Instance view_frag_proper : Proper (() ==> ()) (@view_frag SI A B rel).
Proof. done. Qed.
Global Instance view_auth_dist_inj n :
Inj2 (=) (dist n) (dist n) (@view_auth SI A B rel).
Proof.
intros dq1 a1 dq2 a2 [Hag ?]; inversion Hag as [?? [??]|]; simplify_eq/=.
split; [done|]. by apply (inj to_agree).
Qed.
Global Instance view_auth_inj : Inj2 (=) () () (@view_auth SI A B rel).
Proof.
intros dq1 a1 dq2 a2 [Hag ?]; inversion Hag as [?? [??]|]; simplify_eq/=.
split; [done|]. by apply (inj to_agree).
Qed.
Global Instance view_frag_dist_inj n :
Inj (dist n) (dist n) (@view_frag SI A B rel).
Proof. by intros ?? [??]. Qed.
Global Instance view_frag_inj : Inj () () (@view_frag SI A B rel).
Proof. by intros ?? [??]. Qed.
Local Instance view_valid_instance : Valid (view rel) := λ x,
match view_auth_proj x with
| Some (dq, ag) =>
dq ( n, a, ag {n} to_agree a rel n a (view_frag_proj x))
| None => n, a, rel n a (view_frag_proj x)
end.
Local Instance view_validN_instance : ValidN (view rel) := λ n x,
match view_auth_proj x with
| Some (dq, ag) =>
{n} dq a, ag {n} to_agree a rel n a (view_frag_proj x)
| None => a, rel n a (view_frag_proj x)
end.
Local Instance view_pcore_instance : PCore (view rel) := λ x,
Some (View (core (view_auth_proj x)) (core (view_frag_proj x))).
Local Instance view_op_instance : Op (view rel) := λ x y,
View (view_auth_proj x view_auth_proj y) (view_frag_proj x view_frag_proj y).
Local Definition view_valid_eq :
valid = λ x,
match view_auth_proj x with
| Some (dq, ag) =>
dq ( n, a, ag {n} to_agree a rel n a (view_frag_proj x))
| None => n, a, rel n a (view_frag_proj x)
end := eq_refl _.
Local Definition view_validN_eq :
validN = λ n x,
match view_auth_proj x with
| Some (dq, ag) => {n} dq a, ag {n} to_agree a rel n a (view_frag_proj x)
| None => a, rel n a (view_frag_proj x)
end := eq_refl _.
Local Definition view_pcore_eq :
pcore = λ x, Some (View (core (view_auth_proj x)) (core (view_frag_proj x))) :=
eq_refl _.
Local Definition view_core_eq :
core = λ x, View (core (view_auth_proj x)) (core (view_frag_proj x)) :=
eq_refl _.
Local Definition view_op_eq :
op = λ x y, View (view_auth_proj x view_auth_proj y)
(view_frag_proj x view_frag_proj y) :=
eq_refl _.
Lemma view_cmra_mixin : CmraMixin (view rel).
Proof.
apply (iso_cmra_mixin_restrict_validity
(λ x : option (dfrac * agree A) * B, View x.1 x.2)
(λ x, (view_auth_proj x, view_frag_proj x))); try done.
- intros [x b]. by rewrite /= pair_pcore !cmra_pcore_core.
- intros n [[[dq ag]|] b]; rewrite /= view_validN_eq /=.
+ intros (?&a&->&?). repeat split; simpl; [done|]. by eapply view_rel_validN.
+ intros [a ?]. repeat split; simpl. by eapply view_rel_validN.
- rewrite view_validN_eq.
intros n [x1 b1] [x2 b2] [Hx ?]; simpl in *;
destruct Hx as [[q1 ag1] [q2 ag2] [??]|]; intros ?; by ofe_subst.
- rewrite view_valid_eq view_validN_eq.
intros [[[dq aa]|] b]; rewrite /= ?cmra_valid_validN; naive_solver.
- rewrite view_validN_eq=> n m [[[dq ag]|] b] /=.
+ intros [? (a&?&?)]; split; [done|].
exists a; split; [by eauto using dist_le|].
apply view_rel_mono with n a b; auto.
+ intros [a ?]. exists a. apply view_rel_mono with n a b; auto.
- rewrite view_validN_eq=> n [[[q1 ag1]|] b1] [[[q2 ag2]|] b2] /=.
+ intros [?%cmra_validN_op_l (a & Haga & ?)]. split; [done|].
assert (ag1 {n} ag2) as Ha12 by (apply agree_op_invN; by rewrite Haga).
exists a. split; [by rewrite -Haga -Ha12 agree_idemp|].
apply view_rel_mono with n a (b1 b2); eauto using cmra_includedN_l.
+ intros [? (a & Haga & ?)]. split; [done|]. exists a; split; [done|].
apply view_rel_mono with n a (b1 b2); eauto using cmra_includedN_l.
+ intros [? (a & Haga & ?)]. exists a.
apply view_rel_mono with n a (b1 b2); eauto using cmra_includedN_l.
+ intros [a ?]. exists a.
apply view_rel_mono with n a (b1 b2); eauto using cmra_includedN_l.
Qed.
Canonical Structure viewR := Cmra (view rel) view_cmra_mixin.
Global Instance view_auth_discrete dq a :
Discrete a Discrete (ε : B) Discrete (V{dq} a : view rel).
Proof. intros. apply View_discrete; apply _. Qed.
Global Instance view_frag_discrete b :
Discrete b Discrete (V b : view rel).
Proof. intros. apply View_discrete; apply _. Qed.
Global Instance view_cmra_discrete :
OfeDiscrete A CmraDiscrete B ViewRelDiscrete rel
CmraDiscrete viewR.
Proof.
split; [apply _|]=> -[[[dq ag]|] b]; rewrite view_valid_eq view_validN_eq /=.
- rewrite -cmra_discrete_valid_iff.
setoid_rewrite <-(discrete_iff _ ag). naive_solver.
- naive_solver.
Qed.
Local Instance view_empty_instance : Unit (view rel) := View ε ε.
Lemma view_ucmra_mixin : UcmraMixin (view rel).
Proof.
split; simpl.
- rewrite view_valid_eq /=. apply view_rel_unit.
- by intros x; constructor; rewrite /= left_id.
- do 2 constructor; [done| apply (core_id_core _)].
Qed.
Canonical Structure viewUR := Ucmra (view rel) view_ucmra_mixin.
(** Operation *)
Lemma view_auth_dfrac_op dq1 dq2 a : V{dq1 dq2} a V{dq1} a V{dq2} a.
Proof.
intros; split; simpl; last by rewrite left_id.
by rewrite -Some_op -pair_op agree_idemp.
Qed.
Global Instance view_auth_dfrac_is_op dq dq1 dq2 a :
IsOp dq dq1 dq2 IsOp' (V{dq} a) (V{dq1} a) (V{dq2} a).
Proof. rewrite /IsOp' /IsOp => ->. by rewrite -view_auth_dfrac_op. Qed.
Lemma view_frag_op b1 b2 : V (b1 b2) = V b1 V b2.
Proof. done. Qed.
Lemma view_frag_mono b1 b2 : b1 b2 V b1 V b2.
Proof. intros [c ->]. by rewrite view_frag_op. Qed.
Lemma view_frag_core b : core (V b) = V (core b).
Proof. done. Qed.
Lemma view_both_core_discarded a b :
core (V a V b) V a V (core b).
Proof. rewrite view_core_eq view_op_eq /= !left_id //. Qed.
Lemma view_both_core_frac q a b :
core (V{#q} a V b) V (core b).
Proof. rewrite view_core_eq view_op_eq /= !left_id //. Qed.
Global Instance view_auth_core_id a : CoreId (V a).
Proof. do 2 constructor; simpl; auto. apply: core_id_core. Qed.
Global Instance view_frag_core_id b : CoreId b CoreId (V b).
Proof. do 2 constructor; simpl; auto. apply: core_id_core. Qed.
Global Instance view_both_core_id a b : CoreId b CoreId (V a V b).
Proof. do 2 constructor; simpl; auto. rewrite !left_id. apply: core_id_core. Qed.
Global Instance view_frag_is_op b b1 b2 :
IsOp b b1 b2 IsOp' (V b) (V b1) (V b2).
Proof. done. Qed.
Global Instance view_frag_sep_homomorphism :
MonoidHomomorphism op op () (@view_frag SI A B rel).
Proof. by split; [split; try apply _|]. Qed.
Lemma big_opL_view_frag {C} (g : nat C B) (l : list C) :
(V [^op list] kx l, g k x) [^op list] kx l, V (g k x).
Proof. apply (big_opL_commute _). Qed.
Lemma big_opM_view_frag `{Countable K} {C} (g : K C B) (m : gmap K C) :
(V [^op map] kx m, g k x) [^op map] kx m, V (g k x).
Proof. apply (big_opM_commute _). Qed.
Lemma big_opS_view_frag `{Countable C} (g : C B) (X : gset C) :
(V [^op set] x X, g x) [^op set] x X, V (g x).
Proof. apply (big_opS_commute _). Qed.
Lemma big_opMS_view_frag `{Countable C} (g : C B) (X : gmultiset C) :
(V [^op mset] x X, g x) [^op mset] x X, V (g x).
Proof. apply (big_opMS_commute _). Qed.
(** Validity *)
Lemma view_auth_dfrac_op_invN n dq1 a1 dq2 a2 :
{n} (V{dq1} a1 V{dq2} a2) a1 {n} a2.
Proof.
rewrite /op /view_op_instance /= left_id -Some_op -pair_op view_validN_eq /=.
intros (?&?& Eq &?). apply (inj to_agree), agree_op_invN. by rewrite Eq.
Qed.
Lemma view_auth_dfrac_op_inv dq1 a1 dq2 a2 : (V{dq1} a1 V{dq2} a2) a1 a2.
Proof.
intros ?. apply equiv_dist. intros n.
by eapply view_auth_dfrac_op_invN, cmra_valid_validN.
Qed.
Lemma view_auth_dfrac_op_inv_L `{!LeibnizEquiv A} dq1 a1 dq2 a2 :
(V{dq1} a1 V{dq2} a2) a1 = a2.
Proof. by intros ?%view_auth_dfrac_op_inv%leibniz_equiv. Qed.
Lemma view_auth_dfrac_validN n dq a : {n} (V{dq} a) {n}dq rel n a ε.
Proof.
rewrite view_validN_eq /=. apply and_iff_compat_l. split; [|by eauto].
by intros [? [->%(inj to_agree) ?]].
Qed.
Lemma view_auth_validN n a : {n} (V a) rel n a ε.
Proof. rewrite view_auth_dfrac_validN. split; [naive_solver|done]. Qed.
Lemma view_auth_dfrac_op_validN n dq1 dq2 a1 a2 :
{n} (V{dq1} a1 V{dq2} a2) (dq1 dq2) a1 {n} a2 rel n a1 ε.
Proof.
split.
- intros Hval. assert (a1 {n} a2) as Ha by eauto using view_auth_dfrac_op_invN.
revert Hval. rewrite Ha -view_auth_dfrac_op view_auth_dfrac_validN. naive_solver.
- intros (?&->&?). by rewrite -view_auth_dfrac_op view_auth_dfrac_validN.
Qed.
Lemma view_auth_op_validN n a1 a2 : {n} (V a1 V a2) False.
Proof. rewrite view_auth_dfrac_op_validN. naive_solver. Qed.
Lemma view_frag_validN n b : {n} (V b) a, rel n a b.
Proof. done. Qed.
Lemma view_both_dfrac_validN n dq a b :
{n} (V{dq} a V b) dq rel n a b.
Proof.
rewrite view_validN_eq /=. apply and_iff_compat_l.
setoid_rewrite (left_id _ _ b). split; [|by eauto].
by intros [?[->%(inj to_agree)]].
Qed.
Lemma view_both_validN n a b : {n} (V a V b) rel n a b.
Proof. rewrite view_both_dfrac_validN. split; [naive_solver|done]. Qed.
Lemma view_auth_dfrac_valid dq a : (V{dq} a) dq n, rel n a ε.
Proof.
rewrite view_valid_eq /=. apply and_iff_compat_l. split; [|by eauto].
intros H n. by destruct (H n) as [? [->%(inj to_agree) ?]].
Qed.
Lemma view_auth_valid a : (V a) n, rel n a ε.
Proof. rewrite view_auth_dfrac_valid. split; [naive_solver|done]. Qed.
Lemma view_auth_dfrac_op_valid dq1 dq2 a1 a2 :
(V{dq1} a1 V{dq2} a2) (dq1 dq2) a1 a2 n, rel n a1 ε.
Proof.
rewrite 1!cmra_valid_validN equiv_dist. setoid_rewrite view_auth_dfrac_op_validN.
split; last naive_solver. intros Hv.
split; last naive_solver. apply (Hv 0).
Qed.
Lemma view_auth_op_valid a1 a2 : (V a1 V a2) False.
Proof. rewrite view_auth_dfrac_op_valid. naive_solver. Qed.
Lemma view_frag_valid b : (V b) n, a, rel n a b.
Proof. done. Qed.
Lemma view_both_dfrac_valid dq a b : (V{dq} a V b) dq n, rel n a b.
Proof.
rewrite view_valid_eq /=. apply and_iff_compat_l.
setoid_rewrite (left_id _ _ b). split; [|by eauto].
intros H n. by destruct (H n) as [?[->%(inj to_agree)]].
Qed.
Lemma view_both_valid a b : (V a V b) n, rel n a b.
Proof. rewrite view_both_dfrac_valid. split; [naive_solver|done]. Qed.
(** Inclusion *)
Lemma view_auth_dfrac_includedN n dq1 dq2 a1 a2 b :
V{dq1} a1 {n} V{dq2} a2 V b (dq1 dq2 dq1 = dq2) a1 {n} a2.
Proof.
split.
- intros [[[[dqf agf]|] bf]
[[?%(discrete_iff _ _) ?]%(inj Some) _]]; simplify_eq/=.
+ split; [eauto|]. apply to_agree_includedN. by exists agf.
+ split; [right; done|]. by apply (inj to_agree).
- intros [[[? ->]| ->] ->].
+ rewrite view_auth_dfrac_op -assoc. apply cmra_includedN_l.
+ apply cmra_includedN_l.
Qed.
Lemma view_auth_dfrac_included dq1 dq2 a1 a2 b :
V{dq1} a1 V{dq2} a2 V b (dq1 dq2 dq1 = dq2) a1 a2.
Proof.
intros. split.
- split.
+ by eapply (view_auth_dfrac_includedN 0), cmra_included_includedN.
+ apply equiv_dist=> n.
by eapply view_auth_dfrac_includedN, cmra_included_includedN.
- intros [[[dq ->]| ->] ->].
+ by rewrite view_auth_dfrac_op -assoc.
+ done.
Qed.
Lemma view_auth_includedN n a1 a2 b :
V a1 {n} V a2 V b a1 {n} a2.
Proof. rewrite view_auth_dfrac_includedN. naive_solver. Qed.
Lemma view_auth_included a1 a2 b :
V a1 V a2 V b a1 a2.
Proof. rewrite view_auth_dfrac_included. naive_solver. Qed.
Lemma view_frag_includedN n p a b1 b2 :
V b1 {n} V{p} a V b2 b1 {n} b2.
Proof.
split.
- intros [xf [_ Hb]]; simpl in *.
revert Hb; rewrite left_id. by exists (view_frag_proj xf).
- intros [bf ->]. rewrite comm view_frag_op -assoc. apply cmra_includedN_l.
Qed.
Lemma view_frag_included p a b1 b2 :
V b1 V{p} a V b2 b1 b2.
Proof.
split.
- intros [xf [_ Hb]]; simpl in *.
revert Hb; rewrite left_id. by exists (view_frag_proj xf).
- intros [bf ->]. by rewrite comm view_frag_op -assoc.
Qed.
(** The weaker [view_both_included] lemmas below are a consequence of the
[view_auth_included] and [view_frag_included] lemmas above. *)
Lemma view_both_dfrac_includedN n dq1 dq2 a1 a2 b1 b2 :
V{dq1} a1 V b1 {n} V{dq2} a2 V b2
(dq1 dq2 dq1 = dq2) a1 {n} a2 b1 {n} b2.
Proof.
split.
- intros. rewrite assoc. split.
+ rewrite -view_auth_dfrac_includedN. by etrans; [apply cmra_includedN_l|].
+ rewrite -view_frag_includedN. by etrans; [apply cmra_includedN_r|].
- intros (?&->&?bf&->). rewrite (comm _ b1) view_frag_op assoc.
by apply cmra_monoN_r, view_auth_dfrac_includedN.
Qed.
Lemma view_both_dfrac_included dq1 dq2 a1 a2 b1 b2 :
V{dq1} a1 V b1 V{dq2} a2 V b2
(dq1 dq2 dq1 = dq2) a1 a2 b1 b2.
Proof.
split.
- intros. rewrite assoc. split.
+ rewrite -view_auth_dfrac_included. by etrans; [apply cmra_included_l|].
+ rewrite -view_frag_included. by etrans; [apply cmra_included_r|].
- intros (?&->&?bf&->). rewrite (comm _ b1) view_frag_op assoc.
by apply cmra_mono_r, view_auth_dfrac_included.
Qed.
Lemma view_both_includedN n a1 a2 b1 b2 :
V a1 V b1 {n} V a2 V b2 a1 {n} a2 b1 {n} b2.
Proof. rewrite view_both_dfrac_includedN. naive_solver. Qed.
Lemma view_both_included a1 a2 b1 b2 :
V a1 V b1 V a2 V b2 a1 a2 b1 b2.
Proof. rewrite view_both_dfrac_included. naive_solver. Qed.
(** Updates *)
(** Note that we quantify over a frame [bf], and since conceptually [rel n a b]
means "[b] is a valid fragment to be part of [a]", there is another implicit
frame quantification inside [rel] (usually because [rel] is defined via [≼]
which contains an existential quantifier). The difference between the two
frames is that the frame quantified inside [rel] may change but [bf] has
to be preserved. It is not clear if it is possible to avoid this. *)
Lemma view_updateP a b Pab :
( n bf, rel n a (b bf) a' b', Pab a' b' rel n a' (b' bf))
V a V b ~~>: λ k, a' b', k = V a' V b' Pab a' b'.
Proof.
intros Hup; apply cmra_total_updateP=> n [[[dq ag]|] bf] [/=].
{ by intros []%(exclusiveN_l _ _). }
intros _ (a0 & <-%(inj to_agree) & Hrel).
rewrite !left_id in Hrel. apply Hup in Hrel as (a' & b' & Hab' & Hrel).
eexists; split.
- naive_solver.
- split; simpl; [done|].
exists a'; split; [done|]. by rewrite left_id.
Qed.
Lemma view_update a b a' b' :
( n bf, rel n a (b bf) rel n a' (b' bf))
V a V b ~~> V a' V b'.
Proof.
intros Hup.
eapply cmra_update_updateP, cmra_updateP_weaken.
{ eapply view_updateP with (Pab := λ a b, a = a' b = b').
naive_solver. }
{ naive_solver. }
Qed.
Lemma view_update_alloc a a' b' :
( n bf, rel n a bf rel n a' (b' bf))
V a ~~> V a' V b'.
Proof.
intros Hup. rewrite -(right_id _ _ (V a)).
apply view_update=> n bf. rewrite left_id. apply Hup.
Qed.
Lemma view_update_dealloc a b a' :
( n bf, rel n a (b bf) rel n a' bf)
V a V b ~~> V a'.
Proof.
intros Hup. rewrite -(right_id _ _ (V a')).
apply view_update=> n bf. rewrite left_id. apply Hup.
Qed.
Lemma view_update_auth a a' b' :
( n bf, rel n a bf rel n a' bf)
V a ~~> V a'.
Proof.
intros Hup. rewrite -(right_id _ _ (V a)) -(right_id _ _ (V a')).
apply view_update=> n bf. rewrite !left_id. apply Hup.
Qed.
Local Lemma view_updateP_auth_dfrac dq P a :
dq ~~>: P
V{dq} a ~~>: λ k, dq', k = V{dq'} a P dq'.
Proof.
intros Hupd. apply cmra_total_updateP.
move=> n [[[dq' ag]|] bf] [Hv ?].
- destruct (Hupd n (Some dq') Hv) as (dr&Hdr&Heq).
eexists. split; first by eexists. done.
- destruct (Hupd n None Hv) as (dr&Hdr&Heq).
eexists. split; first by eexists. done.
Qed.
Lemma view_update_auth_persist dq a : V{dq} a ~~> V a.
Proof.
eapply (cmra_update_lift_updateP (λ dq, view_auth dq a)).
{ intros; by apply view_updateP_auth_dfrac. }
{ apply dfrac_discard_update. }
Qed.
Lemma view_updateP_auth_unpersist a : V a ~~>: λ k, q, k = V{#q} a.
Proof.
eapply cmra_updateP_weaken.
{ eapply view_updateP_auth_dfrac, dfrac_undiscard_update. }
naive_solver.
Qed.
Lemma view_updateP_both_unpersist a b : V a V b ~~>: λ k, q, k = V{#q} a V b.
Proof.
eapply cmra_updateP_weaken.
{ eapply cmra_updateP_op'.
{ eapply view_updateP_auth_unpersist. }
by eapply cmra_update_updateP. }
naive_solver.
Qed.
Lemma view_updateP_frag b P :
( a n bf, rel n a (b bf) b', P b' rel n a (b' bf))
V b ~~>: λ k, b', k = V b' P b'.
Proof.
rewrite !cmra_total_updateP view_validN_eq=> ? n [[[dq ag]|] bf]; naive_solver.
Qed.
Lemma view_update_frag b b' :
( a n bf, rel n a (b bf) rel n a (b' bf))
V b ~~> V b'.
Proof.
rewrite !cmra_total_update view_validN_eq=> ? n [[[dq ag]|] bf]; naive_solver.
Qed.
Lemma view_update_dfrac_alloc dq a b :
( n bf, rel n a bf rel n a (b bf))
V{dq} a ~~> V{dq} a V b.
Proof.
intros Hup. apply cmra_total_update=> n [[[p ag]|] bf] [/=].
- intros ? (a0 & Hag & Hrel). split; simpl; [done|].
exists a0; split; [done|]. revert Hrel.
assert (to_agree a {n} to_agree a0) as <-%to_agree_includedN.
{ by exists ag. }
rewrite !left_id. apply Hup.
- intros ? (a0 & <-%(inj to_agree) & Hrel). split; simpl; [done|].
exists a; split; [done|]. revert Hrel. rewrite !left_id. apply Hup.
Qed.
Lemma view_local_update a b0 b1 a' b0' b1' :
(b0, b1) ~l~> (b0', b1')
( n, view_rel_holds rel n a b0 view_rel_holds rel n a' b0')
(V a V b0, V a V b1) ~l~> (V a' V b0', V a' V b1').
Proof.
rewrite !local_update_unital.
move=> Hup Hrel n [[[qd ag]|] bf] /view_both_validN Hrel' [/=].
- rewrite right_id -Some_op -pair_op => /Some_dist_inj [/= H1q _].
by destruct (id_free_r (DfracOwn 1) qd).
- rewrite !left_id=> _ Hb0.
destruct (Hup n bf) as [? Hb0']; [by eauto using view_rel_validN..|].
split; [apply view_both_validN; by auto|]. by rewrite -assoc Hb0'.
Qed.
End cmra.
(** * Utilities to construct functors *)
(** Due to the dependent type [rel] in [view] we cannot actually define
instances of the functor structures [rFunctor] and [urFunctor]. Functors can
only be defined for instances of [view], like [auth]. To make it more convenient
to define functors for instances of [view], we define the map operation
[view_map] and a bunch of lemmas about it. *)
Definition view_map {SI : sidx} {A A' B B'}
{rel : SI A B Prop} {rel' : SI A' B' Prop}
(f : A A') (g : B B') (x : view rel) : view rel' :=
View (prod_map id (agree_map f) <$> view_auth_proj x) (g (view_frag_proj x)).
Lemma view_map_id {SI : sidx} {A B} {rel : SI A B Prop} (x : view rel) :
view_map id id x = x.
Proof. destruct x as [[[]|] ]; by rewrite // /view_map /= agree_map_id. Qed.
Lemma view_map_compose {SI : sidx} {A A' A'' B B' B''}
{rel : SI A B Prop} {rel' : SI A' B' Prop}
{rel'' : SI A'' B'' Prop}
(f1 : A A') (f2 : A' A'') (g1 : B B') (g2 : B' B'') (x : view rel) :
view_map (f2 f1) (g2 g1) x
=@{view rel''} view_map f2 g2 (view_map (rel':=rel') f1 g1 x).
Proof. destruct x as [[[]|] ]; by rewrite // /view_map /= agree_map_compose. Qed.
Lemma view_map_ext {SI : sidx} {A A' B B' : ofe}
{rel : SI A B Prop} {rel' : SI A' B' Prop}
(f1 f2 : A A') (g1 g2 : B B')
`{!NonExpansive f1, !NonExpansive g1} (x : view rel) :
( a, f1 a f2 a) ( b, g1 b g2 b)
view_map f1 g1 x ≡@{view rel'} view_map f2 g2 x.
Proof.
intros. constructor; simpl; [|by auto].
apply option_fmap_equiv_ext=> a; by rewrite /prod_map /= agree_map_ext.
Qed.
Global Instance view_map_ne {SI : sidx} {A A' B B' : ofe}
{rel : SI A B Prop} {rel' : SI A' B' Prop}
(f : A A') (g : B B') `{Hf : !NonExpansive f, Hg : !NonExpansive g} :
NonExpansive (view_map (rel':=rel') (rel:=rel) f g).
Proof.
intros n [o1 bf1] [o2 bf2] [??]; split; simpl in *; [|by apply Hg].
apply option_fmap_ne; [|done]=> pag1 pag2 ?.
apply prod_map_ne; [done| |done]. by apply agree_map_ne.
Qed.
Definition viewO_map {SI : sidx} {A A' B B' : ofe}
{rel : SI A B Prop} {rel' : SI A' B' Prop}
(f : A -n> A') (g : B -n> B') : viewO rel -n> viewO rel' :=
OfeMor (view_map f g).
Lemma viewO_map_ne {SI : sidx} {A A' B B' : ofe}
{rel : SI A B Prop} {rel' : SI A' B' Prop} :
NonExpansive2 (viewO_map (rel:=rel) (rel':=rel')).
Proof.
intros n f f' Hf g g' Hg [[[p ag]|] bf]; split=> //=.
do 2 f_equiv. by apply agreeO_map_ne.
Qed.
Lemma view_map_cmra_morphism {SI : sidx} {A A' B B'}
{rel : view_rel A B} {rel' : view_rel A' B'}
(f : A A') (g : B B') `{!NonExpansive f, !CmraMorphism g} :
( n a b, rel n a b rel' n (f a) (g b))
CmraMorphism (view_map (rel:=rel) (rel':=rel') f g).
Proof.
intros Hrel. split.
- apply _.
- rewrite !view_validN_eq=> n [[[p ag]|] bf] /=;
[|naive_solver eauto using cmra_morphism_validN].
intros [? [a' [Hag ?]]]. split; [done|]. exists (f a'). split; [|by auto].
by rewrite -agree_map_to_agree -Hag.
- intros [o bf]. apply Some_proper; rewrite /view_map /=.
f_equiv; by rewrite cmra_morphism_core.
- intros [[[dq1 ag1]|] bf1] [[[dq2 ag2]|] bf2];
try apply View_proper=> //=; by rewrite cmra_morphism_op.
Qed.
From iris.algebra Require Import cmra view auth agree csum list excl gmap.
From iris.algebra.lib Require Import excl_auth gmap_view dfrac_agree.
From iris.bi Require Import lib.cmra.
From iris.base_logic Require Import bi derived.
From iris.prelude Require Import options.
(** Internalized properties of our CMRA constructions. *)
Local Coercion uPred_holds : uPred >-> Funclass.
Section upred.
Context {M : ucmra}.
(* Force implicit argument M *)
Notation "P ⊢ Q" := (bi_entails (PROP:=uPredI M) P Q).
Notation "P ⊣⊢ Q" := (equiv (A:=uPredI M) P%I Q%I).
Notation "⊢ Q" := (bi_emp_valid (PROP:=uPredI M) Q).
Lemma prod_validI {A B : cmra} (x : A * B) : x ⊣⊢ x.1 x.2.
Proof. by uPred.unseal. Qed.
Lemma option_validI {A : cmra} (mx : option A) :
mx ⊣⊢ match mx with Some x => x | None => True : uPred M end.
Proof. uPred.unseal. by destruct mx. Qed.
Lemma discrete_fun_validI {A} {B : A ucmra} (g : discrete_fun B) :
g ⊣⊢ i, g i.
Proof. by uPred.unseal. Qed.
(* Analogues of [id_freeN_l] and [id_freeN_r] in the logic, stated in a way
that allows us to do [iDestruct (id_freeI_r with "H✓ H≡") as %[]]*)
Lemma id_freeI_r {A : cmra} (x y : A) :
IdFree x x -∗ (x y) x -∗ False.
Proof.
intros ?. apply bi.wand_intro_l. rewrite bi.sep_and right_id.
apply bi.wand_intro_r. rewrite bi.sep_and.
uPred.unseal. split => n m Hm. case. by apply id_freeN_r.
Qed.
Lemma id_freeI_l {A : cmra} (x y : A) :
IdFree x x -∗ (y x) x -∗ False.
Proof.
intros ?. apply bi.wand_intro_l. rewrite bi.sep_and right_id.
apply bi.wand_intro_r. rewrite bi.sep_and.
uPred.unseal. split => n m Hm. case. by apply id_freeN_l.
Qed.
Section gmap_ofe.
Context `{Countable K} {A : ofe}.
Implicit Types m : gmap K A.
Implicit Types i : K.
Lemma gmap_equivI m1 m2 : m1 m2 ⊣⊢ i, m1 !! i m2 !! i.
Proof. by uPred.unseal. Qed.
Lemma gmap_union_equiv_eqI m m1 m2 :
m m1 m2 ⊣⊢ m1' m2', m = m1' m2' m1' m1 m2' m2.
Proof. uPred.unseal; split=> n x _. apply gmap_union_dist_eq. Qed.
End gmap_ofe.
Section gmap_cmra.
Context `{Countable K} {A : cmra}.
Implicit Types m : gmap K A.
Lemma gmap_validI m : m ⊣⊢ i, (m !! i).
Proof. by uPred.unseal. Qed.
Lemma singleton_validI i x : ({[ i := x ]} : gmap K A) ⊣⊢ x.
Proof.
rewrite gmap_validI. apply: anti_symm.
- rewrite (bi.forall_elim i) lookup_singleton option_validI. done.
- apply bi.forall_intro=>j. destruct (decide (i = j)) as [<-|Hne].
+ rewrite lookup_singleton option_validI. done.
+ rewrite lookup_singleton_ne // option_validI.
apply bi.True_intro.
Qed.
End gmap_cmra.
Section list_ofe.
Context {A : ofe}.
Implicit Types l : list A.
Lemma list_equivI l1 l2 : l1 l2 ⊣⊢ i, l1 !! i l2 !! i.
Proof. uPred.unseal; constructor=> n x ?. apply list_dist_lookup. Qed.
End list_ofe.
Section excl.
Context {A : ofe}.
Implicit Types x : excl A.
Lemma excl_validI x :
x ⊣⊢ if x is ExclInvalid then False else True.
Proof. uPred.unseal. by destruct x. Qed.
End excl.
Section agree.
Context {A : ofe}.
Implicit Types a b : A.
Implicit Types x y : agree A.
Lemma agree_equivI a b : to_agree a to_agree b ⊣⊢ (a b).
Proof.
uPred.unseal. do 2 split.
- intros Hx. exact: (inj to_agree).
- intros Hx. exact: to_agree_ne.
Qed.
Lemma agree_validI x y : (x y) x y.
Proof. uPred.unseal; split=> r n _ ?; by apply: agree_op_invN. Qed.
Lemma to_agree_validI a : to_agree a.
Proof. uPred.unseal; done. Qed.
Lemma to_agree_op_validI a b : (to_agree a to_agree b) ⊣⊢ a b.
Proof.
apply bi.entails_anti_sym.
- rewrite agree_validI. by rewrite agree_equivI.
- pose (Ψ := (λ x : A, (to_agree a to_agree x) : uPred M)%I).
assert (NonExpansive Ψ) as ? by solve_proper.
rewrite (internal_eq_rewrite a b Ψ).
eapply bi.impl_elim; first reflexivity.
etrans; first apply bi.True_intro.
subst Ψ; simpl.
rewrite agree_idemp. apply to_agree_validI.
Qed.
Lemma to_agree_uninjI x : x a, to_agree a x.
Proof. uPred.unseal. split=> n y _. exact: to_agree_uninjN. Qed.
(** Derived lemma: If two [x y : agree O] compose to some [to_agree a],
they are internally equal, and also equal to the [to_agree a].
Empirically, [x ⋅ y ≡ to_agree a] appears often when agreement comes up
in CMRA validity terms, especially when [view]s are involved. The desired
simplification [x ≡ y ∧ y ≡ to_agree a] is also not straightforward to
derive, so we have a special lemma to handle this common case. *)
Lemma agree_op_equiv_to_agreeI x y a :
x y to_agree a x y y to_agree a.
Proof.
assert (x y to_agree a x y) as Hxy_equiv.
{ rewrite -(agree_validI x y) internal_eq_sym.
apply: (internal_eq_rewrite' _ _ (λ o, o)%I); first done.
rewrite -to_agree_validI. apply bi.True_intro. }
apply bi.and_intro; first done.
rewrite -{1}(idemp bi_and (_ _)%I) {1}Hxy_equiv. apply bi.impl_elim_l'.
apply: (internal_eq_rewrite' _ _
(λ y', x y' to_agree a y' to_agree a)%I); [solve_proper|done|].
rewrite agree_idemp. apply bi.impl_refl.
Qed.
Lemma to_agree_includedI a b :
to_agree a to_agree b ⊣⊢ a b.
Proof.
apply (anti_symm _).
- apply bi.exist_elim=>c. rewrite internal_eq_sym.
rewrite agree_op_equiv_to_agreeI -agree_equivI.
apply internal_eq_trans.
- apply: (internal_eq_rewrite' _ _ (λ b, to_agree a to_agree b)%I);
[solve_proper|done|].
rewrite -internal_included_refl. apply bi.True_intro.
Qed.
End agree.
Section csum_cmra.
Context {A B : cmra}.
Implicit Types a : A.
Implicit Types b : B.
Lemma csum_validI (x : csum A B) :
x ⊣⊢ match x with
| Cinl a => a
| Cinr b => b
| CsumInvalid => False
end.
Proof. uPred.unseal. by destruct x. Qed.
End csum_cmra.
Section view.
Context {A B} (rel : view_rel A B).
Implicit Types a : A.
Implicit Types ag : option (frac * agree A).
Implicit Types b : B.
Implicit Types x y : view rel.
Lemma view_both_dfrac_validI_1 (relI : uPred M) dq a b :
( n (x : M), rel n a b relI n x)
(V{dq} a V b : view rel) ⌜✓dq relI.
Proof.
intros Hrel. uPred.unseal. split=> n x _ /=.
rewrite /uPred_holds /= view_both_dfrac_validN. by move=> [? /Hrel].
Qed.
Lemma view_both_dfrac_validI_2 (relI : uPred M) dq a b :
( n (x : M), relI n x rel n a b)
⌜✓dq relI (V{dq} a V b : view rel).
Proof.
intros Hrel. uPred.unseal. split=> n x _ /=.
rewrite /uPred_holds /= view_both_dfrac_validN. by move=> [? /Hrel].
Qed.
Lemma view_both_dfrac_validI (relI : uPred M) dq a b :
( n (x : M), rel n a b relI n x)
(V{dq} a V b : view rel) ⊣⊢ ⌜✓dq relI.
Proof.
intros. apply (anti_symm _);
[apply view_both_dfrac_validI_1|apply view_both_dfrac_validI_2]; naive_solver.
Qed.
Lemma view_both_validI_1 (relI : uPred M) a b :
( n (x : M), rel n a b relI n x)
(V a V b : view rel) relI.
Proof. intros. by rewrite view_both_dfrac_validI_1 // bi.and_elim_r. Qed.
Lemma view_both_validI_2 (relI : uPred M) a b :
( n (x : M), relI n x rel n a b)
relI (V a V b : view rel).
Proof.
intros. rewrite -view_both_dfrac_validI_2 //.
apply bi.and_intro; [|done]. by apply bi.pure_intro.
Qed.
Lemma view_both_validI (relI : uPred M) a b :
( n (x : M), rel n a b relI n x)
(V a V b : view rel) ⊣⊢ relI.
Proof.
intros. apply (anti_symm _);
[apply view_both_validI_1|apply view_both_validI_2]; naive_solver.
Qed.
Lemma view_auth_dfrac_validI (relI : uPred M) dq a :
( n (x : M), relI n x rel n a ε)
(V{dq} a : view rel) ⊣⊢ ⌜✓dq relI.
Proof.
intros. rewrite -(right_id ε op (V{dq} a)). by apply view_both_dfrac_validI.
Qed.
Lemma view_auth_validI (relI : uPred M) a :
( n (x : M), relI n x rel n a ε)
(V a : view rel) ⊣⊢ relI.
Proof. intros. rewrite -(right_id ε op (V a)). by apply view_both_validI. Qed.
Lemma view_frag_validI (relI : uPred M) b :
( n (x : M), relI n x a, rel n a b)
(V b : view rel) ⊣⊢ relI.
Proof. uPred.unseal=> Hrel. split=> n x _. by rewrite Hrel. Qed.
End view.
Section auth.
Context {A : ucmra}.
Implicit Types a b : A.
Implicit Types x y : auth A.
Lemma auth_auth_dfrac_validI dq a : ({dq} a) ⊣⊢ ⌜✓dq a.
Proof.
apply view_auth_dfrac_validI=> n. uPred.unseal; split; [|by intros [??]].
split; [|done]. apply ucmra_unit_leastN.
Qed.
Lemma auth_auth_validI a : ( a) ⊣⊢ a.
Proof.
by rewrite auth_auth_dfrac_validI bi.pure_True // left_id.
Qed.
Lemma auth_auth_dfrac_op_validI dq1 dq2 a1 a2 :
({dq1} a1 {dq2} a2) ⊣⊢ (dq1 dq2) (a1 a2) a1.
Proof. uPred.unseal; split => n x _. apply auth_auth_dfrac_op_validN. Qed.
Lemma auth_frag_validI a : ( a) ⊣⊢ a.
Proof.
apply view_frag_validI=> n x.
rewrite auth_view_rel_exists. by uPred.unseal.
Qed.
Lemma auth_both_dfrac_validI dq a b :
({dq} a b) ⊣⊢ ⌜✓dq ( c, a b c) a.
Proof. apply view_both_dfrac_validI=> n. by uPred.unseal. Qed.
Lemma auth_both_validI a b :
( a b) ⊣⊢ ( c, a b c) a.
Proof.
by rewrite auth_both_dfrac_validI bi.pure_True // left_id.
Qed.
End auth.
Section excl_auth.
Context {A : ofe}.
Implicit Types a b : A.
Lemma excl_auth_agreeI a b : (E a E b) (a b).
Proof.
rewrite auth_both_validI bi.and_elim_l.
apply bi.exist_elim=> -[[c|]|];
by rewrite option_equivI /= excl_equivI //= bi.False_elim.
Qed.
End excl_auth.
Section dfrac_agree.
Context {A : ofe}.
Implicit Types a b : A.
Lemma dfrac_agree_validI dq a : (to_dfrac_agree dq a) ⊣⊢ ⌜✓ dq⌝.
Proof.
rewrite prod_validI /= uPred.discrete_valid. apply bi.entails_anti_sym.
- by rewrite bi.and_elim_l.
- apply bi.and_intro; first done. etrans; last apply to_agree_validI.
apply bi.True_intro.
Qed.
Lemma dfrac_agree_validI_2 dq1 dq2 a b :
(to_dfrac_agree dq1 a to_dfrac_agree dq2 b) ⊣⊢ ⌜✓ (dq1 dq2) (a b).
Proof.
rewrite prod_validI /= uPred.discrete_valid to_agree_op_validI //.
Qed.
Lemma frac_agree_validI q a : (to_frac_agree q a) ⊣⊢ (q 1)%Qp⌝.
Proof.
rewrite dfrac_agree_validI dfrac_valid_own //.
Qed.
Lemma frac_agree_validI_2 q1 q2 a b :
(to_frac_agree q1 a to_frac_agree q2 b) ⊣⊢ (q1 + q2 1)%Qp (a b).
Proof.
rewrite dfrac_agree_validI_2 dfrac_valid_own //.
Qed.
End dfrac_agree.
Section gmap_view.
Context {K : Type} `{Countable K} {V : cmra}.
Implicit Types (m : gmap K V) (k : K) (dq : dfrac) (v : V).
Lemma gmap_view_both_dfrac_validI dp m k dq v :
(gmap_view_auth dp m gmap_view_frag k dq v) ⊣⊢
v' dq', ⌜✓ dp m !! k = Some v' (dq', v')
Some (dq, v) Some (dq', v').
Proof.
unfold internal_included.
uPred.unseal. split=> n x _. apply: gmap_view_both_dfrac_validN.
Qed.
Lemma gmap_view_both_validI m dp k v :
(gmap_view_auth dp m gmap_view_frag k (DfracOwn 1) v) ⊣⊢
dp v m !! k Some v.
Proof. uPred.unseal. split=> n x _. apply: gmap_view_both_validN. Qed.
Lemma gmap_view_both_validI_total `{!CmraTotal V} dp m k dq v :
(gmap_view_auth dp m gmap_view_frag k dq v)
v', ⌜✓ dp dq m !! k = Some v' v' v v'.
Proof.
unfold internal_included.
uPred.unseal. split=> n x _. apply: gmap_view_both_dfrac_validN_total.
Qed.
Lemma gmap_view_frag_op_validI k dq1 dq2 v1 v2 :
(gmap_view_frag k dq1 v1 gmap_view_frag k dq2 v2) ⊣⊢
⌜✓ (dq1 dq2) (v1 v2).
Proof. uPred.unseal. split=> n x _. apply: gmap_view_frag_op_validN. Qed.
End gmap_view.
End upred.
From iris.bi Require Export bi.
From iris.base_logic Require Export derived proofmode algebra.
From iris.prelude Require Import options.
(* The trick of having multiple [uPred] modules, which are all exported in
another [uPred] module is by Jason Gross and described in:
https://sympa.inria.fr/sympa/arc/coq-club/2016-12/msg00069.html *)
Module Import uPred.
Export base_logic.bi.uPred.
Export derived.uPred.
Export bi.bi.
End uPred.
From iris.bi Require Export derived_connectives extensions
updates internal_eq plainly lib.cmra.
From iris.base_logic Require Export upred.
From iris.prelude Require Import options.
Import uPred_primitive.
(** BI instances for [uPred], and re-stating the remaining primitive laws in
terms of the BI interface. This file does *not* unseal. *)
Definition uPred_emp {M} : uPred M := uPred_pure True.
Local Existing Instance entails_po.
Lemma uPred_bi_mixin (M : ucmra) :
BiMixin
uPred_entails uPred_emp uPred_pure uPred_and uPred_or uPred_impl
(@uPred_forall M) (@uPred_exist M) uPred_sep uPred_wand.
Proof.
split.
- exact: entails_po.
- exact: equiv_entails.
- exact: pure_ne.
- exact: and_ne.
- exact: or_ne.
- exact: impl_ne.
- exact: forall_ne.
- exact: exist_ne.
- exact: sep_ne.
- exact: wand_ne.
- exact: pure_intro.
- exact: pure_elim'.
- exact: and_elim_l.
- exact: and_elim_r.
- exact: and_intro.
- exact: or_intro_l.
- exact: or_intro_r.
- exact: or_elim.
- exact: impl_intro_r.
- exact: impl_elim_l'.
- exact: @forall_intro.
- exact: @forall_elim.
- exact: @exist_intro.
- exact: @exist_elim.
- exact: sep_mono.
- exact: True_sep_1.
- exact: True_sep_2.
- exact: sep_comm'.
- exact: sep_assoc'.
- exact: wand_intro_r.
- exact: wand_elim_l'.
Qed.
Lemma uPred_bi_persistently_mixin (M : ucmra) :
BiPersistentlyMixin
uPred_entails uPred_emp uPred_and
(@uPred_exist M) uPred_sep uPred_persistently.
Proof.
split.
- exact: persistently_ne.
- exact: persistently_mono.
- exact: persistently_idemp_2.
- (* emp ⊢ <pers> emp (ADMISSIBLE) *)
trans (uPred_forall (M:=M) (λ _ : False, uPred_persistently uPred_emp)).
+ apply forall_intro=>-[].
+ etrans; first exact: persistently_forall_2.
apply persistently_mono. exact: pure_intro.
- (* ((<pers> P) ∧ (<pers> Q)) ⊢ <pers> (P ∧ Q) (ADMISSIBLE) *)
intros P Q.
trans (uPred_forall (M:=M) (λ b : bool, uPred_persistently (if b then P else Q))).
+ apply forall_intro=>[[]].
* apply and_elim_l.
* apply and_elim_r.
+ etrans; first exact: persistently_forall_2.
apply persistently_mono. apply and_intro.
* etrans; first apply (forall_elim true). done.
* etrans; first apply (forall_elim false). done.
- exact: @persistently_exist_1.
- (* <pers> P ∗ Q ⊢ <pers> P (ADMISSIBLE) *)
intros. etrans; first exact: sep_comm'.
etrans; last exact: True_sep_2.
apply sep_mono; last done.
exact: pure_intro.
- exact: persistently_and_sep_l_1.
Qed.
Lemma uPred_bi_later_mixin (M : ucmra) :
BiLaterMixin
uPred_entails uPred_pure uPred_or uPred_impl
(@uPred_forall M) (@uPred_exist M) uPred_sep uPred_persistently uPred_later.
Proof.
split.
- apply contractive_ne, later_contractive.
- exact: later_mono.
- exact: later_intro.
- exact: @later_forall_2.
- exact: @later_exist_false.
- exact: later_sep_1.
- exact: later_sep_2.
- exact: later_persistently_1.
- exact: later_persistently_2.
- exact: later_false_em.
Qed.
Canonical Structure uPredI (M : ucmra) : bi :=
{| bi_ofe_mixin := ofe_mixin_of (uPred M);
bi_bi_mixin := uPred_bi_mixin M;
bi_bi_later_mixin := uPred_bi_later_mixin M;
bi_bi_persistently_mixin := uPred_bi_persistently_mixin M |}.
Lemma uPred_internal_eq_mixin M : BiInternalEqMixin (uPredI M) (@uPred_internal_eq M).
Proof.
split.
- exact: internal_eq_ne.
- exact: @internal_eq_refl.
- exact: @internal_eq_rewrite.
- exact: @fun_ext.
- exact: @sig_eq.
- exact: @discrete_eq_1.
- exact: @later_eq_1.
- exact: @later_eq_2.
Qed.
Global Instance uPred_internal_eq M : BiInternalEq (uPredI M) :=
{| bi_internal_eq_mixin := uPred_internal_eq_mixin M |}.
Lemma uPred_plainly_mixin M : BiPlainlyMixin (uPredI M) uPred_plainly.
Proof.
split.
- exact: plainly_ne.
- exact: plainly_mono.
- exact: plainly_elim_persistently.
- exact: plainly_idemp_2.
- exact: @plainly_forall_2.
- exact: plainly_impl_plainly.
- (* P ⊢ ■ emp (ADMISSIBLE) *)
intros P.
trans (uPred_forall (M:=M) (λ _ : False , uPred_plainly uPred_emp)).
+ apply forall_intro=>[[]].
+ etrans; first exact: plainly_forall_2.
apply plainly_mono. exact: pure_intro.
- (* ■ P ∗ Q ⊢ ■ P (ADMISSIBLE) *)
intros P Q. etrans; last exact: True_sep_2.
etrans; first exact: sep_comm'.
apply sep_mono; last done.
exact: pure_intro.
- exact: later_plainly_1.
- exact: later_plainly_2.
Qed.
Global Instance uPred_plainly M : BiPlainly (uPredI M) :=
{| bi_plainly_mixin := uPred_plainly_mixin M |}.
Lemma uPred_bupd_mixin M : BiBUpdMixin (uPredI M) uPred_bupd.
Proof.
split.
- exact: bupd_ne.
- exact: bupd_intro.
- exact: bupd_mono.
- exact: bupd_trans.
- exact: bupd_frame_r.
Qed.
Global Instance uPred_bi_bupd M : BiBUpd (uPredI M) := {| bi_bupd_mixin := uPred_bupd_mixin M |}.
(** extra BI instances *)
Global Instance uPred_affine M : BiAffine (uPredI M) | 0.
Proof. intros P. exact: pure_intro. Qed.
(* Also add this to the global hint database, otherwise [eauto] won't work for
many lemmas that have [BiAffine] as a premise. *)
Global Hint Immediate uPred_affine : core.
Global Instance uPred_persistently_forall M : BiPersistentlyForall (uPredI M).
Proof. exact: @persistently_forall_2. Qed.
Global Instance uPred_pure_forall M : BiPureForall (uPredI M).
Proof. exact: @pure_forall_2. Qed.
Global Instance uPred_later_contractive {M} : BiLaterContractive (uPredI M).
Proof. exact: @later_contractive. Qed.
Global Instance uPred_persistently_impl_plainly M : BiPersistentlyImplPlainly (uPredI M).
Proof. exact: persistently_impl_plainly. Qed.
Global Instance uPred_plainly_exist_1 M : BiPlainlyExist (uPredI M).
Proof. exact: @plainly_exist_1. Qed.
Global Instance uPred_prop_ext M : BiPropExt (uPredI M).
Proof. exact: prop_ext_2. Qed.
Global Instance uPred_bi_bupd_plainly M : BiBUpdPlainly (uPredI M).
Proof. exact: bupd_plainly. Qed.
(** Re-state/export lemmas about Iris-specific primitive connectives (own, valid) *)
Module uPred.
Section restate.
Context {M : ucmra}.
Implicit Types φ : Prop.
Implicit Types P Q : uPred M.
Implicit Types A : Type.
(* Force implicit argument M *)
Notation "P ⊢ Q" := (bi_entails (PROP:=uPredI M) P%I Q%I).
Notation "P ⊣⊢ Q" := (equiv (A:=uPredI M) P%I Q%I).
Global Instance ownM_ne : NonExpansive (@uPred_ownM M) := uPred_primitive.ownM_ne.
Global Instance cmra_valid_ne {A : cmra} : NonExpansive (@uPred_cmra_valid M A) :=
uPred_primitive.cmra_valid_ne.
(** Re-exporting primitive lemmas that are not in any interface *)
Lemma ownM_op (a1 a2 : M) :
uPred_ownM (a1 a2) ⊣⊢ uPred_ownM a1 uPred_ownM a2.
Proof. exact: uPred_primitive.ownM_op. Qed.
Lemma persistently_ownM_core (a : M) : uPred_ownM a <pers> uPred_ownM (core a).
Proof. exact: uPred_primitive.persistently_ownM_core. Qed.
Lemma ownM_unit P : P (uPred_ownM ε).
Proof. exact: uPred_primitive.ownM_unit. Qed.
Lemma later_ownM a : uPred_ownM a b, uPred_ownM b (a b).
Proof. exact: uPred_primitive.later_ownM. Qed.
Lemma bupd_ownM_updateP x (Φ : M Prop) :
x ~~>: Φ uPred_ownM x |==> y, Φ y uPred_ownM y.
Proof. exact: uPred_primitive.bupd_ownM_updateP. Qed.
Lemma ownM_forall {A} (f : A M) :
( a, uPred_ownM (f a)) z, uPred_ownM z ( a, f a z).
Proof. exact: uPred_primitive.ownM_forall. Qed.
(** This is really just a special case of an entailment
between two [siProp], but we do not have the infrastructure
to express the more general case. This temporary proof rule will
be replaced by the proper one eventually. *)
Lemma internal_eq_entails {A B : ofe} (a1 a2 : A) (b1 b2 : B) :
(a1 a2 b1 b2) ( n, a1 {n} a2 b1 {n} b2).
Proof. exact: uPred_primitive.internal_eq_entails. Qed.
Lemma ownM_valid (a : M) : uPred_ownM a a.
Proof. exact: uPred_primitive.ownM_valid. Qed.
Lemma cmra_valid_intro {A : cmra} P (a : A) : a P ( a).
Proof. exact: uPred_primitive.cmra_valid_intro. Qed.
Lemma cmra_valid_elim {A : cmra} (a : A) : a {0} a ⌝.
Proof. exact: uPred_primitive.cmra_valid_elim. Qed.
Lemma plainly_cmra_valid_1 {A : cmra} (a : A) : a a.
Proof. exact: uPred_primitive.plainly_cmra_valid_1. Qed.
Lemma cmra_valid_weaken {A : cmra} (a b : A) : (a b) a.
Proof. exact: uPred_primitive.cmra_valid_weaken. Qed.
(** This is really just a special case of an entailment
between two [siProp], but we do not have the infrastructure
to express the more general case. This temporary proof rule will
be replaced by the proper one eventually. *)
Lemma valid_entails {A B : cmra} (a : A) (b : B) :
( n, {n} a {n} b) a b.
Proof. exact: uPred_primitive.valid_entails. Qed.
(** Consistency/soundness statement *)
Lemma pure_soundness φ : (⊢@{uPredI M} φ ) φ.
Proof. apply pure_soundness. Qed.
Lemma internal_eq_soundness {A : ofe} (x y : A) : (⊢@{uPredI M} x y) x y.
Proof. apply internal_eq_soundness. Qed.
Lemma later_soundness P : ( P) P.
Proof. apply later_soundness. Qed.
(** We restate the unsealing lemmas for the BI layer. The sealing lemmas
are partially applied so that they also rewrite under binders. *)
Local Lemma uPred_emp_unseal : bi_emp = @upred.uPred_pure_def M True.
Proof. by rewrite -upred.uPred_pure_unseal. Qed.
Local Lemma uPred_pure_unseal : bi_pure = @upred.uPred_pure_def M.
Proof. by rewrite -upred.uPred_pure_unseal. Qed.
Local Lemma uPred_and_unseal : bi_and = @upred.uPred_and_def M.
Proof. by rewrite -upred.uPred_and_unseal. Qed.
Local Lemma uPred_or_unseal : bi_or = @upred.uPred_or_def M.
Proof. by rewrite -upred.uPred_or_unseal. Qed.
Local Lemma uPred_impl_unseal : bi_impl = @upred.uPred_impl_def M.
Proof. by rewrite -upred.uPred_impl_unseal. Qed.
Local Lemma uPred_forall_unseal : @bi_forall _ = @upred.uPred_forall_def M.
Proof. by rewrite -upred.uPred_forall_unseal. Qed.
Local Lemma uPred_exist_unseal : @bi_exist _ = @upred.uPred_exist_def M.
Proof. by rewrite -upred.uPred_exist_unseal. Qed.
Local Lemma uPred_internal_eq_unseal :
@internal_eq _ _ = @upred.uPred_internal_eq_def M.
Proof. by rewrite -upred.uPred_internal_eq_unseal. Qed.
Local Lemma uPred_sep_unseal : bi_sep = @upred.uPred_sep_def M.
Proof. by rewrite -upred.uPred_sep_unseal. Qed.
Local Lemma uPred_wand_unseal : bi_wand = @upred.uPred_wand_def M.
Proof. by rewrite -upred.uPred_wand_unseal. Qed.
Local Lemma uPred_plainly_unseal : plainly = @upred.uPred_plainly_def M.
Proof. by rewrite -upred.uPred_plainly_unseal. Qed.
Local Lemma uPred_persistently_unseal :
bi_persistently = @upred.uPred_persistently_def M.
Proof. by rewrite -upred.uPred_persistently_unseal. Qed.
Local Lemma uPred_later_unseal : bi_later = @upred.uPred_later_def M.
Proof. by rewrite -upred.uPred_later_unseal. Qed.
Local Lemma uPred_bupd_unseal : bupd = @upred.uPred_bupd_def M.
Proof. by rewrite -upred.uPred_bupd_unseal. Qed.
Local Definition uPred_unseal :=
(uPred_emp_unseal, uPred_pure_unseal, uPred_and_unseal, uPred_or_unseal,
uPred_impl_unseal, uPred_forall_unseal, uPred_exist_unseal,
uPred_internal_eq_unseal, uPred_sep_unseal, uPred_wand_unseal,
uPred_plainly_unseal, uPred_persistently_unseal, uPred_later_unseal,
upred.uPred_ownM_unseal, upred.uPred_cmra_valid_unseal, @uPred_bupd_unseal).
End restate.
(** A tactic for rewriting with the above lemmas. Unfolds [uPred] goals that use
the BI layer. This is used by [base_logic.algebra] and [base_logic.bupd_alt]. *)
Ltac unseal := rewrite !uPred_unseal /=.
End uPred.
From iris.proofmode Require Import proofmode.
From iris.base_logic Require Export base_logic.
From iris.prelude Require Import options.
(* The sections add extra BI assumptions, which is only picked up with [Type*]. *)
Set Default Proof Using "Type*".
(** This file contains an alternative version of basic updates, that is
expression in terms of just the plain modality [■]. *)
Definition bupd_alt {PROP : bi} `{!BiPlainly PROP} (P : PROP) : PROP :=
R, (P -∗ R) -∗ R.
(** This definition is stated for any BI with a plain modality. The above
definition is akin to the continuation monad, where one should think of [■ R]
being the final result that one wants to get out of the basic update in the end
of the day (via [bupd_alt (■ P) ⊢ ■ P]).
We show that:
1. [bupd_alt] enjoys the usual rules of the basic update modality.
2. Any other modality that enjoys the laws of a basic update modality
entails [bupd_alt] (see [bupd_bupd_alt]).
3. [bupd_alt] entails the ordinary basic update modality [|==>] on [uPred]
(see [bupd_alt_bupd]). This result is proven in the model of [uPred].
The first two points are shown for any BI with a plain modality. *)
Local Coercion uPred_holds : uPred >-> Funclass.
Section bupd_alt.
Context {PROP : bi} `{!BiPlainly PROP}.
Implicit Types P Q R : PROP.
Notation bupd_alt := (@bupd_alt PROP _).
Global Instance bupd_alt_ne : NonExpansive bupd_alt.
Proof. solve_proper. Qed.
Global Instance bupd_alt_proper : Proper (() ==> ()) bupd_alt.
Proof. solve_proper. Qed.
Global Instance bupd_alt_mono' : Proper (() ==> ()) bupd_alt.
Proof. solve_proper. Qed.
Global Instance bupd_alt_flip_mono' : Proper (flip () ==> flip ()) bupd_alt.
Proof. solve_proper. Qed.
(** The laws of the basic update modality hold *)
Lemma bupd_alt_intro P : P bupd_alt P.
Proof. iIntros "HP" (R) "H". by iApply "H". Qed.
Lemma bupd_alt_mono P Q : (P Q) bupd_alt P bupd_alt Q.
Proof. by intros ->. Qed.
Lemma bupd_alt_trans P : bupd_alt (bupd_alt P) bupd_alt P.
Proof. iIntros "HP" (R) "H". iApply "HP". iIntros "HP". by iApply "HP". Qed.
Lemma bupd_alt_frame_r P Q : bupd_alt P Q bupd_alt (P Q).
Proof.
iIntros "[HP HQ]" (R) "H". iApply "HP". iIntros "HP". iApply ("H" with "[$]").
Qed.
Lemma bupd_alt_plainly P : bupd_alt ( P) P.
Proof. iIntros "H". iApply ("H" $! P with "[]"); auto. Qed.
(** Any modality conforming with [BiBUpdPlainly] entails the alternative
definition *)
Lemma bupd_bupd_alt `{!BiBUpd PROP, !BiBUpdPlainly PROP} P : (|==> P) bupd_alt P.
Proof. iIntros "HP" (R) "H". by iMod ("H" with "HP") as "?". Qed.
(** We get the usual rule for frame preserving updates if we have an [own]
connective satisfying the following rule w.r.t. interaction with plainly. *)
Context {M : ucmra} (own : M PROP).
Context (own_updateP_plainly : x Φ R,
x ~~>: Φ
own x ( y, Φ y -∗ own y -∗ R) R).
Lemma own_updateP x (Φ : M Prop) :
x ~~>: Φ own x bupd_alt ( y, Φ y own y).
Proof.
iIntros (Hup) "Hx"; iIntros (R) "H".
iApply (own_updateP_plainly with "[$Hx H]"); first done.
iIntros (y ?) "Hy". iApply "H"; auto.
Qed.
End bupd_alt.
(** The alternative definition entails the ordinary basic update *)
Lemma bupd_alt_bupd {M} (P : uPred M) : bupd_alt P |==> P.
Proof.
rewrite /bupd_alt. uPred.unseal; split=> n x Hx H k y ? Hxy.
unshelve refine (H {| uPred_holds k _ :=
x' : M, {k} (x' y) P k x' |} k y _ _ _).
- intros n1 n2 x1 x2 (z&?&?) _ ?.
eauto using cmra_validN_le, uPred_mono.
- done.
- done.
- intros k' z ?? HP. exists z. by rewrite (comm op).
Qed.
Lemma bupd_alt_bupd_iff {M} (P : uPred M) : bupd_alt P ⊣⊢ |==> P.
Proof.
apply (anti_symm _).
- apply bupd_alt_bupd.
- apply bupd_bupd_alt.
Qed.
(** The law about the interaction between [uPred_ownM] and plainly holds. *)
Lemma ownM_updateP {M : ucmra} x (Φ : M Prop) (R : uPred M) :
x ~~>: Φ
uPred_ownM x ( y, Φ y -∗ uPred_ownM y -∗ R) R.
Proof.
uPred.unseal=> Hup; split; intros n z Hv (?&z2&?&[z1 ?]&HR); ofe_subst.
destruct (Hup n (Some (z1 z2))) as (y&?&?); simpl in *.
{ by rewrite assoc. }
refine (HR y n z1 _ _ _ n y _ _ _); auto.
- rewrite comm. by eapply cmra_validN_op_r.
- by rewrite (comm _ _ y) (comm _ z2).
- apply (reflexivity (R:=includedN _)).
Qed.
From iris.algebra Require Import frac.
From iris.bi Require Export bi.
From iris.base_logic Require Export bi.
From iris.prelude Require Import options.
Import bi.bi base_logic.bi.uPred.
(** Derived laws for Iris-specific primitive connectives (own, valid).
This file does NOT unseal! *)
Module uPred.
Section derived.
Context {M : ucmra}.
Implicit Types φ : Prop.
Implicit Types P Q : uPred M.
Implicit Types A : Type.
(* Force implicit argument M *)
Notation "P ⊢ Q" := (bi_entails (PROP:=uPredI M) P Q).
Notation "P ⊣⊢ Q" := (equiv (A:=uPredI M) P%I Q%I).
(** Propers *)
Global Instance ownM_proper: Proper (() ==> (⊣⊢)) (@uPred_ownM M) := ne_proper _.
Global Instance cmra_valid_proper {A : cmra} :
Proper (() ==> (⊣⊢)) (@uPred_cmra_valid M A) := ne_proper _.
(** Own and valid derived *)
Lemma persistently_cmra_valid_1 {A : cmra} (a : A) : a ⊢@{uPredI M} <pers> ( a).
Proof. by rewrite {1}plainly_cmra_valid_1 plainly_elim_persistently. Qed.
Lemma intuitionistically_ownM (a : M) : CoreId a uPred_ownM a ⊣⊢ uPred_ownM a.
Proof.
rewrite /bi_intuitionistically affine_affinely=>?; apply (anti_symm _);
[by rewrite persistently_elim|].
by rewrite {1}persistently_ownM_core core_id_core.
Qed.
Lemma ownM_invalid (a : M) : ¬ {0} a uPred_ownM a False.
Proof. intros. rewrite ownM_valid cmra_valid_elim. by apply pure_elim'. Qed.
Global Instance ownM_mono : Proper (flip () ==> ()) (@uPred_ownM M).
Proof. intros a b [b' ->]. by rewrite ownM_op sep_elim_l. Qed.
Lemma ownM_unit' : uPred_ownM ε ⊣⊢ True.
Proof. apply (anti_symm _); first by apply pure_intro. apply ownM_unit. Qed.
Lemma plainly_cmra_valid {A : cmra} (a : A) : a ⊣⊢ a.
Proof. apply (anti_symm _), plainly_cmra_valid_1. apply plainly_elim, _. Qed.
Lemma intuitionistically_cmra_valid {A : cmra} (a : A) : a ⊣⊢ a.
Proof.
rewrite /bi_intuitionistically affine_affinely. intros; apply (anti_symm _);
first by rewrite persistently_elim.
apply:persistently_cmra_valid_1.
Qed.
Lemma discrete_valid {A : cmra} `{!CmraDiscrete A} (a : A) : a ⊣⊢ ⌜✓ a⌝.
Proof.
apply (anti_symm _).
- rewrite cmra_valid_elim. by apply pure_mono, cmra_discrete_valid.
- apply pure_elim'=> ?. by apply cmra_valid_intro.
Qed.
Lemma bupd_ownM_update x y : x ~~> y uPred_ownM x |==> uPred_ownM y.
Proof.
intros; rewrite (bupd_ownM_updateP _ (y =.)); last by apply cmra_update_updateP.
by apply bupd_mono, exist_elim=> y'; apply pure_elim_l=> ->.
Qed.
(** Timeless instances *)
Global Instance valid_timeless {A : cmra} `{!CmraDiscrete A} (a : A) :
Timeless ( a : uPred M)%I.
Proof. rewrite /Timeless !discrete_valid. apply (timeless _). Qed.
Global Instance ownM_timeless (a : M) : Discrete a Timeless (uPred_ownM a).
Proof.
intros ?. rewrite /Timeless later_ownM. apply exist_elim=> b.
rewrite (timeless (ab)) (except_0_intro (uPred_ownM b)) -except_0_and.
apply except_0_mono. rewrite internal_eq_sym.
apply (internal_eq_rewrite' b a (uPred_ownM) _);
auto using and_elim_l, and_elim_r.
Qed.
(** Plainness *)
Global Instance cmra_valid_plain {A : cmra} (a : A) :
Plain ( a : uPred M)%I.
Proof. rewrite /Persistent. apply plainly_cmra_valid_1. Qed.
(** Persistence *)
Global Instance cmra_valid_persistent {A : cmra} (a : A) :
Persistent ( a : uPred M)%I.
Proof. rewrite /Persistent. apply persistently_cmra_valid_1. Qed.
Global Instance ownM_persistent a : CoreId a Persistent (@uPred_ownM M a).
Proof.
intros. rewrite /Persistent -{2}(core_id_core a). apply persistently_ownM_core.
Qed.
(** For big ops *)
Global Instance uPred_ownM_sep_homomorphism :
MonoidHomomorphism op uPred_sep () (@uPred_ownM M).
Proof. split; [split|]; try apply _; [apply ownM_op | apply ownM_unit']. Qed.
(** Derive [NonExpansive]/[Contractive] from an internal statement *)
Lemma ne_internal_eq {A B : ofe} (f : A B) :
NonExpansive f x1 x2, x1 x2 f x1 f x2.
Proof.
split; [apply f_equivI|].
intros Hf n x1 x2. by eapply internal_eq_entails.
Qed.
Lemma ne_2_internal_eq {A B C : ofe} (f : A B C) :
NonExpansive2 f x1 x2 y1 y2, x1 x2 y1 y2 f x1 y1 f x2 y2.
Proof.
split.
- intros Hf x1 x2 y1 y2.
change ((x1,y1).1 (x2,y2).1 (x1,y1).2 (x2,y2).2
uncurry f (x1,y1) uncurry f (x2,y2)).
rewrite -prod_equivI. apply ne_internal_eq. solve_proper.
- intros Hf n x1 x2 Hx y1 y2 Hy.
change (uncurry f (x1,y1) {n} uncurry f (x2,y2)).
apply ne_internal_eq; [|done].
intros [??] [??]. rewrite prod_equivI. apply Hf.
Qed.
Lemma contractive_internal_eq {A B : ofe} (f : A B) :
Contractive f x1 x2, (x1 x2) f x1 f x2.
Proof.
split; [apply f_equivI_contractive|].
intros Hf n x1 x2 Hx. specialize (Hf x1 x2).
rewrite -later_equivI internal_eq_entails in Hf. apply Hf. by f_contractive.
Qed.
(** Soundness statement for our modalities: facts derived under modalities in
the empty context also without the modalities.
For basic updates, soundness only holds for plain propositions. *)
Lemma bupd_soundness P `{!Plain P} : ( |==> P) P.
Proof. rewrite bupd_elim. done. Qed.
Lemma laterN_soundness P n : ( ▷^n P) P.
Proof. induction n; eauto using later_soundness. Qed.
(** As pure demonstration, we also show that this holds for an arbitrary nesting
of modalities. We have to do a bit of work to be able to state this theorem
though. *)
Inductive modality := MBUpd | MLater | MPersistently | MPlainly.
Definition denote_modality (m : modality) : uPred M uPred M :=
match m with
| MBUpd => bupd
| MLater => bi_later
| MPersistently => bi_persistently
| MPlainly => plainly
end.
Definition denote_modalities (ms : list modality) : uPred M uPred M :=
λ P, foldr denote_modality P ms.
(** Now we can state and prove 'soundness under arbitrary modalities' for plain
propositions. This is probably not a lemma you want to actually use. *)
Corollary modal_soundness P `{!Plain P} (ms : list modality) :
( denote_modalities ms P) P.
Proof.
intros H. apply (laterN_soundness _ (length ms)).
move: H. apply bi_emp_valid_mono.
induction ms as [|m ms IH]; first done; simpl.
destruct m; simpl; rewrite IH.
- rewrite -later_intro. apply bupd_elim. apply _.
- done.
- rewrite -later_intro persistently_elim. done.
- rewrite -later_intro plainly_elim. done.
Qed.
(** Consistency: one cannot deive [False] in the logic, not even under
modalities. Again this is just for demonstration and probably not practically
useful. *)
Corollary consistency : ¬ ⊢@{uPredI M} False.
Proof. intros H. by eapply pure_soundness. Qed.
End derived.
End uPred.
From iris.algebra Require Import lib.excl_auth gmap agree.
From iris.proofmode Require Import proofmode.
From iris.base_logic.lib Require Export invariants. From iris.base_logic.lib Require Export invariants.
From iris.algebra Require Import auth gmap agree. From iris.prelude Require Import options.
From iris.base_logic Require Import big_op.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Import uPred. Import uPred.
(** The CMRAs we need. *) (** The CMRAs we need. *)
Class boxG Σ := Class boxG Σ :=
boxG_inG :> inG Σ (prodR #[local] boxG_inG :: inG Σ (prodR
(authR (optionUR (exclR boolC))) (excl_authR boolO)
(optionR (agreeR (laterC (iPreProp Σ))))). (optionR (agreeR (laterO (iPropO Σ))))).
Definition boxΣ : gFunctors := #[ GFunctor (authR (optionUR (exclR boolC)) * Definition boxΣ : gFunctors := #[ GFunctor (excl_authR boolO *
optionRF (agreeRF ( )) ) ]. optionRF (agreeRF ( )) ) ].
Instance subG_stsΣ Σ : subG boxΣ Σ boxG Σ. Global Instance subG_boxΣ Σ : subG boxΣ Σ boxG Σ.
Proof. solve_inG. Qed. Proof. solve_inG. Qed.
Section box_defs. Section box_defs.
Context `{invG Σ, boxG Σ} (N : namespace). Context `{!invGS_gen hlc Σ, !boxG Σ} (N : namespace).
Definition slice_name := gname. Definition slice_name := gname.
Definition box_own_auth (γ : slice_name) (a : auth (option (excl bool))) : iProp Σ := Definition box_own_auth (γ : slice_name) (a : excl_authR boolO) : iProp Σ :=
own γ (a, (∅:option (agree (later (iPreProp Σ))))). own γ (a, None).
Definition box_own_prop (γ : slice_name) (P : iProp Σ) : iProp Σ := Definition box_own_prop (γ : slice_name) (P : iProp Σ) : iProp Σ :=
own γ (∅:auth (option (excl bool)), Some (to_agree (Next (iProp_unfold P)))). own γ (ε, Some (to_agree (Next P))).
Definition slice_inv (γ : slice_name) (P : iProp Σ) : iProp Σ := Definition slice_inv (γ : slice_name) (P : iProp Σ) : iProp Σ :=
( b, box_own_auth γ ( Excl' b) if b then P else True)%I. b, box_own_auth γ (E b) if b then P else True.
Definition slice (γ : slice_name) (P : iProp Σ) : iProp Σ := Definition slice (γ : slice_name) (P : iProp Σ) : iProp Σ :=
(box_own_prop γ P inv N (slice_inv γ P))%I. box_own_prop γ P inv N (slice_inv γ P).
Definition box (f : gmap slice_name bool) (P : iProp Σ) : iProp Σ := Definition box (f : gmap slice_name bool) (P : iProp Σ) : iProp Σ :=
( Φ : slice_name iProp Σ, tc_opaque ( Φ : slice_name iProp Σ,
(P [ map] γ _ f, Φ γ) (P [ map] γ _ f, Φ γ)
[ map] γ b f, box_own_auth γ ( Excl' b) box_own_prop γ (Φ γ) [ map] γ b f, box_own_auth γ (E b) box_own_prop γ (Φ γ)
inv N (slice_inv γ (Φ γ)))%I. inv N (slice_inv γ (Φ γ)))%I.
End box_defs. End box_defs.
Instance: Params (@box_own_prop) 3. Global Instance: Params (@box_own_prop) 3 := {}.
Instance: Params (@slice_inv) 3. Global Instance: Params (@slice_inv) 3 := {}.
Instance: Params (@slice) 5. Global Instance: Params (@slice) 5 := {}.
Instance: Params (@box) 5. Global Instance: Params (@box) 5 := {}.
Section box. Section box.
Context `{invG Σ, boxG Σ} (N : namespace). Context `{!invGS_gen hlc Σ, !boxG Σ} (N : namespace).
Implicit Types P Q : iProp Σ. Implicit Types P Q : iProp Σ.
Global Instance box_own_prop_ne γ : NonExpansive (box_own_prop γ). Global Instance box_own_prop_ne γ : NonExpansive (box_own_prop γ).
...@@ -65,7 +64,7 @@ Proof. solve_contractive. Qed. ...@@ -65,7 +64,7 @@ Proof. solve_contractive. Qed.
Global Instance slice_proper γ : Proper (() ==> ()) (slice N γ). Global Instance slice_proper γ : Proper (() ==> ()) (slice N γ).
Proof. apply ne_proper, _. Qed. Proof. apply ne_proper, _. Qed.
Global Instance slice_persistent γ P : PersistentP (slice N γ P). Global Instance slice_persistent γ P : Persistent (slice N γ P).
Proof. apply _. Qed. Proof. apply _. Qed.
Global Instance box_contractive f : Contractive (box N f). Global Instance box_contractive f : Contractive (box N f).
...@@ -76,33 +75,30 @@ Global Instance box_proper f : Proper ((≡) ==> (≡)) (box N f). ...@@ -76,33 +75,30 @@ Global Instance box_proper f : Proper ((≡) ==> (≡)) (box N f).
Proof. apply ne_proper, _. Qed. Proof. apply ne_proper, _. Qed.
Lemma box_own_auth_agree γ b1 b2 : Lemma box_own_auth_agree γ b1 b2 :
box_own_auth γ ( Excl' b1) box_own_auth γ ( Excl' b2) b1 = b2⌝. box_own_auth γ (E b1) box_own_auth γ (E b2) b1 = b2⌝.
Proof. Proof.
rewrite /box_own_prop -own_op own_valid prod_validI /= and_elim_l. 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 %?%excl_auth_agree_L.
Qed. Qed.
Lemma box_own_auth_update γ b1 b2 b3 : Lemma box_own_auth_update γ b1 b2 b3 :
box_own_auth γ ( Excl' b1) box_own_auth γ ( Excl' b2) box_own_auth γ (E b1) box_own_auth γ (E b2)
==∗ box_own_auth γ ( Excl' b3) box_own_auth γ ( Excl' b3). ==∗ box_own_auth γ (E b3) box_own_auth γ (E b3).
Proof. Proof.
rewrite /box_own_auth -!own_op. apply own_update, prod_update; last done. rewrite /box_own_auth -!own_op. iApply own_update. apply prod_update; last done.
by apply auth_update, option_local_update, exclusive_local_update. apply excl_auth_update.
Qed. Qed.
Lemma box_own_agree γ Q1 Q2 : Lemma box_own_agree γ Q1 Q2 :
box_own_prop γ Q1 box_own_prop γ Q2 (Q1 Q2). box_own_prop γ Q1 box_own_prop γ Q2 (Q1 Q2).
Proof. Proof.
rewrite /box_own_prop -own_op own_valid prod_validI /= and_elim_r. rewrite /box_own_prop -own_op own_valid prod_validI /= and_elim_r.
rewrite option_validI /= agree_validI agree_equivI later_equivI /=. by rewrite option_validI /= agree_validI agree_equivI later_equivI /=.
iIntros "#HQ". iNext. rewrite -{2}(iProp_fold_unfold Q1).
iRewrite "HQ". by rewrite iProp_fold_unfold.
Qed. Qed.
Lemma box_alloc : box N True%I. Lemma box_alloc : box N True.
Proof. Proof.
iIntros; iExists (λ _, True)%I; iSplit; last done. iIntros. iExists (λ _, True)%I. by rewrite !big_opM_empty.
iNext. by rewrite big_opM_empty.
Qed. Qed.
Lemma slice_insert_empty E q f Q P : Lemma slice_insert_empty E q f Q P :
...@@ -110,9 +106,9 @@ Lemma slice_insert_empty E q f Q P : ...@@ -110,9 +106,9 @@ Lemma slice_insert_empty E q f Q P :
slice N γ Q ?q box N (<[γ:=false]> f) (Q P). slice N γ Q ?q box N (<[γ:=false]> f) (Q P).
Proof. Proof.
iDestruct 1 as (Φ) "[#HeqP Hf]". iDestruct 1 as (Φ) "[#HeqP Hf]".
iMod (own_alloc_strong ( Excl' false Excl' false, iMod (own_alloc_cofinite (E false E false,
Some (to_agree (Next (iProp_unfold Q)))) (dom _ f)) Some (to_agree (Next Q))) (dom f))
as (γ) "[Hdom Hγ]"; first done. as (γ) "[Hdom Hγ]"; first by (split; [apply auth_both_valid_discrete|]).
rewrite pair_split. iDestruct "Hγ" as "[[Hγ Hγ'] #HγQ]". rewrite pair_split. iDestruct "Hγ" as "[[Hγ Hγ'] #HγQ]".
iDestruct "Hdom" as % ?%not_elem_of_dom. iDestruct "Hdom" as % ?%not_elem_of_dom.
iMod (inv_alloc N _ (slice_inv γ Q) with "[Hγ]") as "#Hinv". iMod (inv_alloc N _ (slice_inv γ Q) with "[Hγ]") as "#Hinv".
...@@ -128,15 +124,15 @@ Lemma slice_delete_empty E q f P Q γ : ...@@ -128,15 +124,15 @@ Lemma slice_delete_empty E q f P Q γ :
N E N E
f !! γ = Some false f !! γ = Some false
slice N γ Q -∗ ?q box N f P ={E}=∗ P', slice N γ Q -∗ ?q box N f P ={E}=∗ P',
?q (P (Q P')) ?q box N (delete γ f) P'. ?q ( (P (Q P')) box N (delete γ f) P').
Proof. Proof.
iIntros (??) "[#HγQ Hinv] H". iDestruct "H" as (Φ) "[#HeqP Hf]". iIntros (??) "[#HγQ Hinv] H". iDestruct "H" as (Φ) "[#HeqP Hf]".
iExists ([ map] γ'↦_ delete γ f, Φ γ')%I. iExists ([ map] γ'↦_ delete γ f, Φ γ')%I.
iInv N as (b) "[>Hγ _]" "Hclose". iInv N as (b) "[>Hγ _]".
iDestruct (big_opM_delete _ f _ false with "Hf") iDestruct (big_sepM_delete _ f _ false with "Hf")
as "[[>Hγ' #[HγΦ ?]] ?]"; first done. as "[[>Hγ' #[HγΦ ?]] ?]"; first done.
iDestruct (box_own_auth_agree γ b false with "[-]") as %->; first by iFrame. iDestruct (box_own_auth_agree γ b false with "[-]") as %->; first by iFrame.
iMod ("Hclose" with "[]"); first iExists false; eauto. iModIntro. iSplitL "Hγ"; first iExists false; eauto.
iModIntro. iNext. iSplit. iModIntro. iNext. iSplit.
- iDestruct (box_own_agree γ Q (Φ γ) with "[#]") as "HeqQ"; first by eauto. - iDestruct (box_own_agree γ Q (Φ γ) with "[#]") as "HeqQ"; first by eauto.
iNext. iRewrite "HeqP". iRewrite "HeqQ". by rewrite -big_opM_delete. iNext. iRewrite "HeqP". iRewrite "HeqQ". by rewrite -big_opM_delete.
...@@ -149,14 +145,14 @@ Lemma slice_fill E q f γ P Q : ...@@ -149,14 +145,14 @@ Lemma slice_fill E q f γ P Q :
slice N γ Q -∗ Q -∗ ?q box N f P ={E}=∗ ?q box N (<[γ:=true]> f) P. slice N γ Q -∗ Q -∗ ?q box N f P ={E}=∗ ?q box N (<[γ:=true]> f) P.
Proof. Proof.
iIntros (??) "#[HγQ Hinv] HQ H"; iDestruct "H" as (Φ) "[#HeqP Hf]". iIntros (??) "#[HγQ Hinv] HQ H"; iDestruct "H" as (Φ) "[#HeqP Hf]".
iInv N as (b') "[>Hγ _]" "Hclose". iInv N as (b') "[>Hγ _]".
iDestruct (big_opM_delete _ f _ false with "Hf") iDestruct (big_sepM_delete _ f _ false with "Hf")
as "[[>Hγ' #[HγΦ Hinv']] ?]"; first done. as "[[>Hγ' #[HγΦ Hinv']] ?]"; first done.
iMod (box_own_auth_update γ b' false true with "[$Hγ $Hγ']") as "[Hγ Hγ']". iMod (box_own_auth_update γ b' false true with "[$Hγ $Hγ']") as "[Hγ Hγ']".
iMod ("Hclose" with "[Hγ HQ]"); first (iNext; iExists true; by iFrame). iModIntro. iSplitL "Hγ HQ"; first (iNext; iExists true; by iFrame).
iModIntro; iNext; iExists Φ; iSplit. iModIntro; iNext; iExists Φ; iSplit.
- by rewrite big_opM_insert_override. - by rewrite big_opM_insert_override.
- rewrite -insert_delete big_opM_insert ?lookup_delete //. - rewrite -insert_delete_insert big_opM_insert ?lookup_delete //.
iFrame; eauto. iFrame; eauto.
Qed. Qed.
...@@ -166,16 +162,16 @@ Lemma slice_empty E q f P Q γ : ...@@ -166,16 +162,16 @@ Lemma slice_empty E q f P Q γ :
slice N γ Q -∗ ?q box N f P ={E}=∗ Q ?q box N (<[γ:=false]> f) P. slice N γ Q -∗ ?q box N f P ={E}=∗ Q ?q box N (<[γ:=false]> f) P.
Proof. Proof.
iIntros (??) "#[HγQ Hinv] H"; iDestruct "H" as (Φ) "[#HeqP Hf]". iIntros (??) "#[HγQ Hinv] H"; iDestruct "H" as (Φ) "[#HeqP Hf]".
iInv N as (b) "[>Hγ HQ]" "Hclose". iInv N as (b) "[>Hγ HQ]".
iDestruct (big_opM_delete _ f with "Hf") iDestruct (big_sepM_delete _ f with "Hf")
as "[[>Hγ' #[HγΦ Hinv']] ?]"; first done. as "[[>Hγ' #[HγΦ Hinv']] ?]"; first done.
iDestruct (box_own_auth_agree γ b true with "[-]") as %->; first by iFrame. iDestruct (box_own_auth_agree γ b true with "[-]") as %->; first by iFrame.
iFrame "HQ". iFrame "HQ".
iMod (box_own_auth_update γ with "[$Hγ $Hγ']") as "[Hγ Hγ']". iMod (box_own_auth_update γ with "[$Hγ $Hγ']") as "[Hγ Hγ']".
iMod ("Hclose" with "[]"); first (iNext; iExists false; by repeat iSplit). iModIntro. iSplitL "Hγ"; first (iNext; iExists false; by repeat iSplit).
iModIntro; iNext; iExists Φ; iSplit. iModIntro; iNext; iExists Φ; iSplit.
- by rewrite big_opM_insert_override. - by rewrite big_opM_insert_override.
- rewrite -insert_delete big_opM_insert ?lookup_delete //. - rewrite -insert_delete_insert big_opM_insert ?lookup_delete //.
iFrame; eauto. iFrame; eauto.
Qed. Qed.
...@@ -185,9 +181,10 @@ Lemma slice_insert_full E q f P Q : ...@@ -185,9 +181,10 @@ Lemma slice_insert_full E q f P Q :
slice N γ Q ?q box N (<[γ:=true]> f) (Q P). slice N γ Q ?q box N (<[γ:=true]> f) (Q P).
Proof. Proof.
iIntros (?) "HQ Hbox". iIntros (?) "HQ Hbox".
iMod (slice_insert_empty with "Hbox") as (γ) "(% & #Hslice & Hbox)". iMod (slice_insert_empty with "Hbox") as (γ ?) "[#Hslice Hbox]".
iExists γ. iFrame "%#". iMod (slice_fill with "Hslice HQ Hbox"); first done. iExists γ. iFrame "%#". iMod (slice_fill with "Hslice HQ Hbox"); first done.
by apply lookup_insert. by rewrite insert_insert. - by apply lookup_insert.
- by rewrite insert_insert.
Qed. Qed.
Lemma slice_delete_full E q f P Q γ : Lemma slice_delete_full E q f P Q γ :
...@@ -200,7 +197,7 @@ Proof. ...@@ -200,7 +197,7 @@ Proof.
iMod (slice_empty with "Hslice Hbox") as "[$ Hbox]"; try done. iMod (slice_empty with "Hslice Hbox") as "[$ Hbox]"; try done.
iMod (slice_delete_empty with "Hslice Hbox") as (P') "[Heq Hbox]"; first done. iMod (slice_delete_empty with "Hslice Hbox") as (P') "[Heq Hbox]"; first done.
{ by apply lookup_insert. } { by apply lookup_insert. }
iExists P'. iFrame. rewrite -insert_delete delete_insert ?lookup_delete //. iExists P'. iFrame. rewrite -insert_delete_insert delete_insert ?lookup_delete //.
Qed. Qed.
Lemma box_fill E f P : Lemma box_fill E f P :
...@@ -209,36 +206,36 @@ Lemma box_fill E f P : ...@@ -209,36 +206,36 @@ Lemma box_fill E f P :
Proof. Proof.
iIntros (?) "H HP"; iDestruct "H" as (Φ) "[#HeqP Hf]". iIntros (?) "H HP"; iDestruct "H" as (Φ) "[#HeqP Hf]".
iExists Φ; iSplitR; first by rewrite big_opM_fmap. iExists Φ; iSplitR; first by rewrite big_opM_fmap.
rewrite internal_eq_iff later_iff big_opM_commute. iEval (rewrite internal_eq_iff later_iff big_sepM_later) in "HeqP".
iDestruct ("HeqP" with "HP") as "HP". iDestruct ("HeqP" with "HP") as "HP".
iCombine "Hf" "HP" as "Hf". iCombine "Hf" "HP" as "Hf".
rewrite -big_opM_opM big_opM_fmap; iApply (fupd_big_sepM _ _ f). rewrite -big_sepM_sep big_opM_fmap; iApply (big_sepM_fupd _ _ f).
iApply (@big_sepM_impl with "[$Hf]"). iApply (@big_sepM_impl with "Hf").
iIntros "!#" (γ b' ?) "[(Hγ' & #$ & #$) HΦ]". iIntros "!>" (γ b' ?) "[(Hγ' & #$ & #$) HΦ]".
iInv N as (b) "[>Hγ _]" "Hclose". iInv N as (b) "[>Hγ _]".
iMod (box_own_auth_update γ with "[Hγ Hγ']") as "[Hγ $]"; first by iFrame. iMod (box_own_auth_update γ with "[Hγ Hγ']") as "[Hγ $]"; first by iFrame.
iApply "Hclose". iNext; iExists true. by iFrame. iModIntro. iSplitL; last done. iNext; iExists true. iFrame.
Qed. Qed.
Lemma box_empty E f P : Lemma box_empty E f P :
N E N E
map_Forall (λ _, (true =)) f map_Forall (λ _, (true =.)) f
box N f P ={E}=∗ P box N (const false <$> f) P. box N f P ={E}=∗ P box N (const false <$> f) P.
Proof. Proof.
iDestruct 1 as (Φ) "[#HeqP Hf]". iDestruct 1 as (Φ) "[#HeqP Hf]".
iAssert (([ map] γb f, Φ γ) iAssert (([ map] γb f, Φ γ)
[ map] γb f, box_own_auth γ ( Excl' false) box_own_prop γ (Φ γ) [ map] γb f, box_own_auth γ (E false) box_own_prop γ (Φ γ)
inv N (slice_inv γ (Φ γ)))%I with "[> Hf]" as "[HΦ ?]". inv N (slice_inv γ (Φ γ)))%I with "[> Hf]" as "[HΦ ?]".
{ rewrite -big_opM_opM -fupd_big_sepM. iApply (@big_sepM_impl with "[$Hf]"). { rewrite -big_sepM_sep -big_sepM_fupd. iApply (@big_sepM_impl with "[$Hf]").
iIntros "!#" (γ b ?) "(Hγ' & #HγΦ & #Hinv)". iIntros "!>" (γ b ?) "(Hγ' & #HγΦ & #Hinv)".
assert (true = b) as <- by eauto. assert (true = b) as <- by eauto.
iInv N as (b) "[>Hγ HΦ]" "Hclose". iInv N as (b) "[>Hγ HΦ]".
iDestruct (box_own_auth_agree γ b true with "[-]") as %->; first by iFrame. iDestruct (box_own_auth_agree γ b true with "[-]") as %->; first by iFrame.
iMod (box_own_auth_update γ true true false with "[$Hγ $Hγ']") as "[Hγ $]". iMod (box_own_auth_update γ true true false with "[$Hγ $Hγ']") as "[Hγ $]".
iMod ("Hclose" with "[]"); first (iNext; iExists false; iFrame; eauto). iModIntro. iSplitL "Hγ"; first (iNext; iExists false; iFrame; eauto).
iFrame "HγΦ Hinv". by iApply "HΦ". } iFrame "HγΦ Hinv". by iApply "HΦ". }
iModIntro; iSplitL "HΦ". iModIntro; iSplitL "HΦ".
- rewrite internal_eq_iff later_iff big_opM_commute. by iApply "HeqP". - rewrite internal_eq_iff later_iff big_sepM_later. by iApply "HeqP".
- iExists Φ; iSplit; by rewrite big_opM_fmap. - iExists Φ; iSplit; by rewrite big_opM_fmap.
Qed. Qed.
...@@ -251,13 +248,13 @@ Proof. ...@@ -251,13 +248,13 @@ Proof.
iIntros (??) "#HQQ' #Hs Hb". destruct b. iIntros (??) "#HQQ' #Hs Hb". destruct b.
- iMod (slice_delete_full with "Hs Hb") as (P') "(HQ & Heq & Hb)"; try done. - iMod (slice_delete_full with "Hs Hb") as (P') "(HQ & Heq & Hb)"; try done.
iDestruct ("HQQ'" with "HQ") as "HQ'". iDestruct ("HQQ'" with "HQ") as "HQ'".
iMod (slice_insert_full with "HQ' Hb") as (γ') "(% & #Hs' & Hb)"; try done. iMod (slice_insert_full with "HQ' Hb") as (γ' ?) "[#Hs' Hb]"; try done.
iExists γ', _. iIntros "{$∗ $# $%} !>". do 2 iNext. iRewrite "Heq". iExists γ', _. iIntros "{$∗ $# $%} !>". do 2 iNext. iRewrite "Heq".
iAlways. by iSplit; iIntros "[? $]"; iApply "HQQ'". iIntros "!>". by iSplit; iIntros "[? $]"; iApply "HQQ'".
- iMod (slice_delete_empty with "Hs Hb") as (P') "(Heq & Hb)"; try done. - iMod (slice_delete_empty with "Hs Hb") as (P') "(Heq & Hb)"; try done.
iMod (slice_insert_empty with "Hb") as (γ') "(% & #Hs' & Hb)"; try done. iMod (slice_insert_empty with "Hb") as (γ' ?) "[#Hs' Hb]"; try done.
iExists γ', _. iIntros "{$∗ $# $%} !>". do 2 iNext. iRewrite "Heq". iExists γ', (Q' P')%I. iIntros "{$∗ $# $%} !>". do 2 iNext. iRewrite "Heq".
iAlways. by iSplit; iIntros "[? $]"; iApply "HQQ'". iIntros "!>". by iSplit; iIntros "[? $]"; iApply "HQQ'".
Qed. Qed.
Lemma slice_split E q f P Q1 Q2 γ b : Lemma slice_split E q f P Q1 Q2 γ b :
...@@ -268,20 +265,20 @@ Lemma slice_split E q f P Q1 Q2 γ b : ...@@ -268,20 +265,20 @@ Lemma slice_split E q f P Q1 Q2 γ b :
Proof. Proof.
iIntros (??) "#Hslice Hbox". destruct b. iIntros (??) "#Hslice Hbox". destruct b.
- iMod (slice_delete_full with "Hslice Hbox") as (P') "([HQ1 HQ2] & Heq & Hbox)"; try done. - iMod (slice_delete_full with "Hslice Hbox") as (P') "([HQ1 HQ2] & Heq & Hbox)"; try done.
iMod (slice_insert_full with "HQ1 Hbox") as (γ1) "(% & #Hslice1 & Hbox)"; first done. iMod (slice_insert_full with "HQ1 Hbox") as (γ1 ?) "[#Hslice1 Hbox]"; first done.
iMod (slice_insert_full with "HQ2 Hbox") as (γ2) "(% & #Hslice2 & Hbox)"; first done. iMod (slice_insert_full with "HQ2 Hbox") as (γ2 ?) "[#Hslice2 Hbox]"; first done.
iExists γ1, γ2. iIntros "{$% $#} !>". iSplit; last iSplit; try iPureIntro. iExists γ1, γ2. iIntros "{$% $#} !>". iSplit; last iSplit; try iPureIntro.
{ by eapply lookup_insert_None. } { by eapply lookup_insert_None. }
{ by apply (lookup_insert_None (delete γ f) γ1 γ2 true). } { by apply (lookup_insert_None (delete γ f) γ1 γ2 true). }
iNext. eapply internal_eq_rewrite_contractive; [by apply _| |by eauto]. iNext. iApply (internal_eq_rewrite_contractive _ _ (box _ _) with "[Heq] Hbox").
iNext. iRewrite "Heq". iPureIntro. by rewrite assoc (comm _ Q2). iNext. iRewrite "Heq". iPureIntro. by rewrite assoc (comm _ Q2).
- iMod (slice_delete_empty with "Hslice Hbox") as (P') "[Heq Hbox]"; try done. - iMod (slice_delete_empty with "Hslice Hbox") as (P') "[Heq Hbox]"; try done.
iMod (slice_insert_empty with "Hbox") as (γ1) "(% & #Hslice1 & Hbox)". iMod (slice_insert_empty with "Hbox") as (γ1 ?) "[#Hslice1 Hbox]".
iMod (slice_insert_empty with "Hbox") as (γ2) "(% & #Hslice2 & Hbox)". iMod (slice_insert_empty with "Hbox") as (γ2 ?) "[#Hslice2 Hbox]".
iExists γ1, γ2. iIntros "{$% $#} !>". iSplit; last iSplit; try iPureIntro. iExists γ1, γ2. iIntros "{$% $#} !>". iSplit; last iSplit; try iPureIntro.
{ by eapply lookup_insert_None. } { by eapply lookup_insert_None. }
{ by apply (lookup_insert_None (delete γ f) γ1 γ2 false). } { by apply (lookup_insert_None (delete γ f) γ1 γ2 false). }
iNext. eapply internal_eq_rewrite_contractive; [by apply _| |by eauto]. iNext. iApply (internal_eq_rewrite_contractive _ _ (box _ _) with "[Heq] Hbox").
iNext. iRewrite "Heq". iPureIntro. by rewrite assoc (comm _ Q2). iNext. iRewrite "Heq". iPureIntro. by rewrite assoc (comm _ Q2).
Qed. Qed.
...@@ -295,19 +292,19 @@ Proof. ...@@ -295,19 +292,19 @@ Proof.
- iMod (slice_delete_full with "Hslice1 Hbox") as (P1) "(HQ1 & Heq1 & Hbox)"; try done. - iMod (slice_delete_full with "Hslice1 Hbox") as (P1) "(HQ1 & Heq1 & Hbox)"; try done.
iMod (slice_delete_full with "Hslice2 Hbox") as (P2) "(HQ2 & Heq2 & Hbox)"; first done. iMod (slice_delete_full with "Hslice2 Hbox") as (P2) "(HQ2 & Heq2 & Hbox)"; first done.
{ by simplify_map_eq. } { by simplify_map_eq. }
iMod (slice_insert_full _ _ _ _ (Q1 Q2)%I with "[$HQ1 $HQ2] Hbox") iMod (slice_insert_full _ _ _ _ (Q1 Q2) with "[$HQ1 $HQ2] Hbox")
as (γ) "(% & #Hslice & Hbox)"; first done. as (γ ?) "[#Hslice Hbox]"; first done.
iExists γ. iIntros "{$% $#} !>". iNext. iExists γ. iIntros "{$% $#} !>". iNext.
eapply internal_eq_rewrite_contractive; [by apply _| |by eauto]. iApply (internal_eq_rewrite_contractive _ _ (box _ _) with "[Heq1 Heq2] Hbox").
iNext. iRewrite "Heq1". iRewrite "Heq2". by rewrite assoc. iNext. iRewrite "Heq1". iRewrite "Heq2". by rewrite assoc.
- iMod (slice_delete_empty with "Hslice1 Hbox") as (P1) "(Heq1 & Hbox)"; try done. - iMod (slice_delete_empty with "Hslice1 Hbox") as (P1) "(Heq1 & Hbox)"; try done.
iMod (slice_delete_empty with "Hslice2 Hbox") as (P2) "(Heq2 & Hbox)"; first done. iMod (slice_delete_empty with "Hslice2 Hbox") as (P2) "(Heq2 & Hbox)"; first done.
{ by simplify_map_eq. } { by simplify_map_eq. }
iMod (slice_insert_empty with "Hbox") as (γ) "(% & #Hslice & Hbox)". iMod (slice_insert_empty with "Hbox") as (γ ?) "[#Hslice Hbox]".
iExists γ. iIntros "{$% $#} !>". iNext. iExists γ. iIntros "{$% $#} !>". iNext.
eapply internal_eq_rewrite_contractive; [by apply _| |by eauto]. iApply (internal_eq_rewrite_contractive _ _ (box _ _) with "[Heq1 Heq2] Hbox").
iNext. iRewrite "Heq1". iRewrite "Heq2". by rewrite assoc. iNext. iRewrite "Heq1". iRewrite "Heq2". by rewrite assoc.
Qed. Qed.
End box. End box.
Typeclasses Opaque slice box. Global Typeclasses Opaque slice box.
From iris.algebra Require Export frac.
From iris.bi.lib Require Import fractional.
From iris.proofmode Require Import proofmode.
From iris.base_logic.lib Require Export invariants.
From iris.prelude Require Import options.
Class cinvG Σ := { #[local] cinv_inG :: inG Σ fracR }.
Definition cinvΣ : gFunctors := #[GFunctor fracR].
Global Instance subG_cinvΣ {Σ} : subG cinvΣ Σ cinvG Σ.
Proof. solve_inG. Qed.
Section defs.
Context `{!invGS_gen hlc Σ, !cinvG Σ}.
Definition cinv_own (γ : gname) (p : frac) : iProp Σ := own γ p.
Definition cinv (N : namespace) (γ : gname) (P : iProp Σ) : iProp Σ :=
inv N (P cinv_own γ 1).
End defs.
Global Instance: Params (@cinv) 5 := {}.
Section proofs.
Context `{!invGS_gen hlc Σ, !cinvG Σ}.
Global Instance cinv_own_timeless γ p : Timeless (cinv_own γ p).
Proof. rewrite /cinv_own; apply _. Qed.
Global Instance cinv_contractive N γ : Contractive (cinv N γ).
Proof. solve_contractive. Qed.
Global Instance cinv_ne N γ : NonExpansive (cinv N γ).
Proof. exact: contractive_ne. Qed.
Global Instance cinv_proper N γ : Proper (() ==> ()) (cinv N γ).
Proof. exact: ne_proper. Qed.
Global Instance cinv_persistent N γ P : Persistent (cinv N γ P).
Proof. rewrite /cinv; apply _. Qed.
Global Instance cinv_own_fractional γ : Fractional (cinv_own γ).
Proof. intros ??. by rewrite /cinv_own -own_op. Qed.
Global Instance cinv_own_as_fractional γ q :
AsFractional (cinv_own γ q) (cinv_own γ) q.
Proof. split; [done|]. apply _. Qed.
Lemma cinv_own_valid γ q1 q2 : cinv_own γ q1 -∗ cinv_own γ q2 -∗ q1 + q2 1⌝%Qp.
Proof. rewrite -frac_valid -uPred.discrete_valid. apply (own_valid_2 γ q1 q2). Qed.
Lemma cinv_own_1_l γ q : cinv_own γ 1 -∗ cinv_own γ q -∗ False.
Proof.
iIntros "H1 H2".
iDestruct (cinv_own_valid with "H1 H2") as %[]%(exclusive_l 1%Qp).
Qed.
Lemma cinv_iff N γ P Q : cinv N γ P -∗ (P Q) -∗ cinv N γ Q.
Proof.
iIntros "HI #HPQ". iApply (inv_iff with "HI"). iIntros "!> !>".
iSplit; iIntros "[?|$]"; iLeft; by iApply "HPQ".
Qed.
(*** Allocation rules. *)
(** The "strong" variants permit any infinite [I], and choosing [P] is delayed
until after [γ] was chosen.*)
Lemma cinv_alloc_strong (I : gname Prop) E N :
pred_infinite I
|={E}=> γ, I γ cinv_own γ 1 P, P ={E}=∗ cinv N γ P.
Proof.
iIntros (?). iMod (own_alloc_strong 1%Qp I) as (γ) "[Hfresh Hγ]"; [done|done|].
iExists γ. iIntros "!> {$Hγ $Hfresh}" (P) "HP".
iMod (inv_alloc N _ (P cinv_own γ 1) with "[HP]"); eauto.
Qed.
(** The "open" variants create the invariant in the open state, and delay
having to prove [P].
These do not imply the other variants because of the extra assumption [↑N ⊆ E]. *)
Lemma cinv_alloc_strong_open (I : gname Prop) E N :
pred_infinite I
N E
|={E}=> γ, I γ cinv_own γ 1 P,
|={E,E∖↑N}=> cinv N γ P ( P ={E∖↑N,E}=∗ True).
Proof.
iIntros (??). iMod (own_alloc_strong 1%Qp I) as (γ) "[Hfresh Hγ]"; [done|done|].
iExists γ. iIntros "!> {$Hγ $Hfresh}" (P).
iMod (inv_alloc_open N _ (P cinv_own γ 1)) as "[Hinv Hclose]"; first by eauto.
iIntros "!>". iFrame. iIntros "HP". iApply "Hclose". iLeft. done.
Qed.
Lemma cinv_alloc_cofinite (G : gset gname) E N :
|={E}=> γ, γ G cinv_own γ 1 P, P ={E}=∗ cinv N γ P.
Proof.
apply cinv_alloc_strong. apply (pred_infinite_set (C:=gset gname))=> E'.
exists (fresh (G E')). apply not_elem_of_union, is_fresh.
Qed.
Lemma cinv_alloc E N P : P ={E}=∗ γ, cinv N γ P cinv_own γ 1.
Proof.
iIntros "HP". iMod (cinv_alloc_cofinite E N) as (γ _) "[Hγ Halloc]".
iExists γ. iFrame "Hγ". by iApply "Halloc".
Qed.
Lemma cinv_alloc_open E N P :
N E |={E,E∖↑N}=> γ, cinv N γ P cinv_own γ 1 ( P ={E∖↑N,E}=∗ True).
Proof.
iIntros (?). iMod (cinv_alloc_strong_open (λ _, True)) as (γ) "(_ & Htok & Hmake)"; [|done|].
{ apply pred_infinite_True. }
iMod ("Hmake" $! P) as "[Hinv Hclose]". iIntros "!>". iExists γ. iFrame.
Qed.
(*** Accessors *)
Lemma cinv_acc_strong E N γ p P :
N E
cinv N γ P -∗ (cinv_own γ p ={E,E∖↑N}=∗
P cinv_own γ p ( E' : coPset, P cinv_own γ 1 ={E',N E'}=∗ True)).
Proof.
iIntros (?) "Hinv Hown".
iMod (inv_acc_strong with "Hinv") as "[[$ | >Hown'] H]"; first done.
- iIntros "{$Hown} !>" (E') "HP". iApply "H". by iNext.
- iDestruct (cinv_own_1_l with "Hown' Hown") as %[].
Qed.
Lemma cinv_acc E N γ p P :
N E
cinv N γ P -∗ cinv_own γ p ={E,E∖↑N}=∗ P cinv_own γ p ( P ={E∖↑N,E}=∗ True).
Proof.
iIntros (?) "#Hinv Hγ".
iMod (cinv_acc_strong with "Hinv Hγ") as "($ & $ & H)"; first done.
iIntros "!> HP".
iMod ("H" with "[$HP]") as "_".
rewrite -union_difference_L //.
Qed.
(*** Other *)
Lemma cinv_cancel E N γ P : N E cinv N γ P -∗ cinv_own γ 1 ={E}=∗ P.
Proof.
iIntros (?) "#Hinv Hγ".
iMod (cinv_acc_strong with "Hinv Hγ") as "($ & Hγ & H)"; first done.
iMod ("H" with "[$Hγ]") as "_".
rewrite -union_difference_L //.
Qed.
Global Instance into_inv_cinv N γ P : IntoInv (cinv N γ P) N := {}.
Global Instance into_acc_cinv E N γ P p :
IntoAcc (X:=unit) (cinv N γ P)
(N E) (cinv_own γ p) (fupd E (E∖↑N)) (fupd (E∖↑N) E)
(λ _, P cinv_own γ p)%I (λ _, P)%I (λ _, None)%I.
Proof.
rewrite /IntoAcc /accessor bi.exist_unit -assoc.
iIntros (?) "#Hinv Hown". by iApply cinv_acc.
Qed.
End proofs.
Global Typeclasses Opaque cinv_own cinv.
From stdpp Require Export coPset.
From iris.algebra Require Import gmap auth agree gset coPset.
From iris.proofmode Require Import proofmode.
From iris.base_logic.lib Require Export own.
From iris.base_logic.lib Require Import wsat.
From iris.base_logic Require Export later_credits.
From iris.prelude Require Import options.
Export wsatGS.
Import uPred.
Import le_upd_if.
(** The definition of fancy updates (and in turn the logic built on top of it) is parameterized
by whether it supports elimination of laters via later credits or not.
This choice is necessary as the fancy update *with* later credits does *not* support
the interaction laws with the plainly modality in [BiFUpdPlainly]. While these laws are
seldomly used, support for them is required for backwards compatibility.
Thus, the [invGS_gen] typeclass ("gen" for "generalized") is parameterized by
a parameter of type [has_lc] that determines whether later credits are
available or not. [invGS] is provided as a convenient notation for the default [HasLc].
We don't use that notation in this file to avoid confusion.
*)
Inductive has_lc := HasLc | HasNoLc.
Class invGpreS (Σ : gFunctors) : Set := InvGpreS {
#[local] invGpreS_wsat :: wsatGpreS Σ;
#[local] invGpreS_lc :: lcGpreS Σ;
}.
(* [invGS_lc] needs to be global in order to enable the use of lemmas like
[lc_split] that require [lcGS], and not [invGS]. [invGS_wsat] also needs to be
global as the lemmas in [invariants.v] require it. *)
Class invGS_gen (hlc : has_lc) (Σ : gFunctors) : Set := InvG {
#[global] invGS_wsat :: wsatGS Σ;
#[global] invGS_lc :: lcGS Σ;
}.
Global Hint Mode invGS_gen - - : typeclass_instances.
Global Hint Mode invGpreS - : typeclass_instances.
Notation invGS := (invGS_gen HasLc).
Definition invΣ : gFunctors :=
#[wsatΣ; lcΣ].
Global Instance subG_invΣ {Σ} : subG invΣ Σ invGpreS Σ.
Proof. solve_inG. Qed.
Local Definition uPred_fupd_def `{!invGS_gen hlc Σ} (E1 E2 : coPset) (P : iProp Σ) : iProp Σ :=
wsat ownE E1 -∗ le_upd_if (if hlc is HasLc then true else false) ( (wsat ownE E2 P)).
Local Definition uPred_fupd_aux : seal (@uPred_fupd_def). Proof. by eexists. Qed.
Definition uPred_fupd := uPred_fupd_aux.(unseal).
Global Arguments uPred_fupd {hlc Σ _}.
Local Lemma uPred_fupd_unseal `{!invGS_gen hlc Σ} : @fupd _ uPred_fupd = uPred_fupd_def.
Proof. rewrite -uPred_fupd_aux.(seal_eq) //. Qed.
Lemma uPred_fupd_mixin `{!invGS_gen hlc Σ} : BiFUpdMixin (uPredI (iResUR Σ)) uPred_fupd.
Proof.
split.
- rewrite uPred_fupd_unseal. solve_proper.
- intros E1 E2 (E1''&->&?)%subseteq_disjoint_union_L.
rewrite uPred_fupd_unseal /uPred_fupd_def ownE_op //.
by iIntros "($ & $ & HE) !> !> [$ $] !> !>".
- rewrite uPred_fupd_unseal.
iIntros (E1 E2 P) ">H [Hw HE]". iApply "H"; by iFrame.
- rewrite uPred_fupd_unseal.
iIntros (E1 E2 P Q HPQ) "HP HwE". rewrite -HPQ. by iApply "HP".
- rewrite uPred_fupd_unseal. iIntros (E1 E2 E3 P) "HP HwE".
iMod ("HP" with "HwE") as ">(Hw & HE & HP)". iApply "HP"; by iFrame.
- intros E1 E2 Ef P HE1Ef. rewrite uPred_fupd_unseal /uPred_fupd_def ownE_op //.
iIntros "Hvs (Hw & HE1 &HEf)".
iMod ("Hvs" with "[Hw HE1]") as ">($ & HE2 & HP)"; first by iFrame.
iDestruct (ownE_op' with "[HE2 HEf]") as "[? $]"; first by iFrame.
iIntros "!> !>". by iApply "HP".
- rewrite uPred_fupd_unseal /uPred_fupd_def. by iIntros (????) "[HwP $]".
Qed.
Global Instance uPred_bi_fupd `{!invGS_gen hlc Σ} : BiFUpd (uPredI (iResUR Σ)) :=
{| bi_fupd_mixin := uPred_fupd_mixin |}.
Global Instance uPred_bi_bupd_fupd `{!invGS_gen hlc Σ} : BiBUpdFUpd (uPredI (iResUR Σ)).
Proof. rewrite /BiBUpdFUpd uPred_fupd_unseal. by iIntros (E P) ">? [$ $] !> !>". Qed.
(** The interaction laws with the plainly modality are only supported when
we opt out of the support for later credits. *)
Global Instance uPred_bi_fupd_plainly_no_lc `{!invGS_gen HasNoLc Σ} :
BiFUpdPlainly (uPredI (iResUR Σ)).
Proof.
split; rewrite uPred_fupd_unseal /uPred_fupd_def.
- iIntros (E E' P Q) "[H HQ] [Hw HE]".
iAssert ( P)%I as "#>HP".
{ by iMod ("H" with "HQ [$]") as "(_ & _ & HP)". }
by iFrame.
- iIntros (E P) "H [Hw HE]".
iAssert ( P)%I as "#HP".
{ iNext. by iMod ("H" with "[$]") as "(_ & _ & HP)". }
iFrame. iIntros "!> !> !>". by iMod "HP".
- iIntros (E A Φ) "HΦ [Hw HE]".
iAssert ( x : A, Φ x)%I as "#>HP".
{ iIntros (x). by iMod ("HΦ" with "[$Hw $HE]") as "(_&_&?)". }
by iFrame.
Qed.
(** Later credits: the laws are only available when we opt into later credit support.*)
(** [lc_fupd_elim_later] allows to eliminate a later from a hypothesis at an update.
This is typically used as [iMod (lc_fupd_elim_later with "Hcredit HP") as "HP".],
where ["Hcredit"] is a credit available in the context and ["HP"] is the
assumption from which a later should be stripped. *)
Lemma lc_fupd_elim_later `{!invGS_gen HasLc Σ} E P :
£ 1 -∗ ( P) -∗ |={E}=> P.
Proof.
iIntros "Hf Hupd".
rewrite uPred_fupd_unseal /uPred_fupd_def.
iIntros "[$ $]". iApply (le_upd_later with "Hf").
iNext. by iModIntro.
Qed.
(** If the goal is a fancy update, this lemma can be used to make a later appear
in front of it in exchange for a later credit.
This is typically used as [iApply (lc_fupd_add_later with "Hcredit")],
where ["Hcredit"] is a credit available in the context. *)
Lemma lc_fupd_add_later `{!invGS_gen HasLc Σ} E1 E2 P :
£ 1 -∗ ( |={E1, E2}=> P) -∗ |={E1, E2}=> P.
Proof.
iIntros "Hf Hupd". iApply (fupd_trans E1 E1).
iApply (lc_fupd_elim_later with "Hf Hupd").
Qed.
(** Similar to above, but here we are adding [n] laters. *)
Lemma lc_fupd_add_laterN `{!invGS_gen HasLc Σ} E1 E2 P n :
£ n -∗ (▷^n |={E1, E2}=> P) -∗ |={E1, E2}=> P.
Proof.
iIntros "Hf Hupd". iInduction n as [|n] "IH"; first done.
iDestruct "Hf" as "[H1 Hf]".
iApply (lc_fupd_add_later with "H1"); iNext.
iApply ("IH" with "[$] [$]").
Qed.
(** * [fupd] soundness lemmas *)
(** "Unfolding" soundness stamement for no-LC fupd:
This exposes that when initializing the [invGS_gen], we can provide
a general lemma that lets one unfold a [|={E1, E2}=> P] into a basic update
while also carrying around some frame [ω E] that tracks the current mask.
We also provide a bunch of later credits for consistency,
but there is no way to use them since this is a [HasNoLc] lemma. *)
Lemma fupd_soundness_no_lc_unfold `{!invGpreS Σ} m E :
|==> `(Hws: invGS_gen HasNoLc Σ) (ω : coPset iProp Σ),
£ m ω E ( E1 E2 P, (|={E1, E2}=> P) -∗ ω E1 ==∗ (ω E2 P)).
Proof.
iMod wsat_alloc as (Hw) "[Hw HE]".
(* We don't actually want any credits, but we need the [lcGS]. *)
iMod (later_credits.le_upd.lc_alloc m) as (Hc) "[_ Hlc]".
set (Hi := InvG HasNoLc _ Hw Hc).
iExists Hi, (λ E, wsat ownE E)%I.
rewrite (union_difference_L E ); [|set_solver].
rewrite ownE_op; [|set_solver].
iDestruct "HE" as "[HE _]". iFrame.
iIntros "!>!>" (E1 E2 P) "HP HwE".
rewrite fancy_updates.uPred_fupd_unseal
/fancy_updates.uPred_fupd_def -assoc /=.
by iApply ("HP" with "HwE").
Qed.
(** Note: the [_no_lc] soundness lemmas also allow generating later credits, but
these cannot be used for anything. They are merely provided to enable making
the adequacy proof generic in whether later credits are used. *)
Lemma fupd_soundness_no_lc `{!invGpreS Σ} E1 E2 (P : iProp Σ) `{!Plain P} m :
( `{Hinv: !invGS_gen HasNoLc Σ}, £ m ={E1,E2}=∗ P) P.
Proof.
intros Hfupd. apply later_soundness, bupd_soundness; [by apply later_plain|].
iMod fupd_soundness_no_lc_unfold as (hws ω) "(Hlc & Hω & #H)".
iMod ("H" with "[Hlc] Hω") as "H'".
{ iMod (Hfupd with "Hlc") as "H'". iModIntro. iApply "H'". }
iDestruct "H'" as "[>H1 >H2]". by iFrame.
Qed.
Lemma fupd_soundness_lc `{!invGpreS Σ} n E1 E2 (P : iProp Σ) `{!Plain P} :
( `{Hinv: !invGS_gen HasLc Σ}, £ n ={E1,E2}=∗ P) P.
Proof.
intros Hfupd. eapply (lc_soundness (S n)); first done.
intros Hc. rewrite lc_succ.
iIntros "[Hone Hn]". rewrite -le_upd_trans. iApply bupd_le_upd.
iMod wsat_alloc as (Hw) "[Hw HE]".
set (Hi := InvG HasLc _ Hw Hc).
iAssert (|={,E2}=> P)%I with "[Hn]" as "H".
{ iMod (fupd_mask_subseteq E1) as "_"; first done. by iApply (Hfupd Hi). }
rewrite uPred_fupd_unseal /uPred_fupd_def.
iModIntro. iMod ("H" with "[$Hw $HE]") as "H".
iPoseProof (except_0_into_later with "H") as "H".
iApply (le_upd_later with "Hone"). iNext.
iDestruct "H" as "(_ & _ & $)".
Qed.
(** Generic soundness lemma for the fancy update, parameterized by [use_credits]
on whether to use credits or not. *)
Lemma fupd_soundness_gen `{!invGpreS Σ} (P : iProp Σ) `{!Plain P}
(hlc : has_lc) n E1 E2 :
( `{Hinv : invGS_gen hlc Σ},
£ n ={E1,E2}=∗ P)
P.
Proof.
destruct hlc.
- apply fupd_soundness_lc. done.
- apply fupd_soundness_no_lc. done.
Qed.
(** [step_fupdN] soundness lemmas *)
Lemma step_fupdN_soundness_no_lc `{!invGpreS Σ} (P : iProp Σ) `{!Plain P} n m :
( `{Hinv: !invGS_gen HasNoLc Σ}, £ m ={,}=∗ |={}▷=>^n P)
P.
Proof.
intros Hiter.
apply (laterN_soundness _ (S n)); simpl.
apply (fupd_soundness_no_lc _ m)=> Hinv. iIntros "Hc".
iPoseProof (Hiter Hinv) as "H". clear Hiter.
iApply fupd_plainly_mask. iSpecialize ("H" with "Hc").
iMod (step_fupdN_plain with "H") as "H". iMod "H". iModIntro.
rewrite -later_plainly -laterN_plainly -later_laterN laterN_later.
iNext. iMod "H" as "#H". auto.
Qed.
Lemma step_fupdN_soundness_no_lc' `{!invGpreS Σ} (P : iProp Σ) `{!Plain P} n m :
( `{Hinv: !invGS_gen HasNoLc Σ}, £ m ={}[]▷=∗^n P)
P.
Proof.
intros Hiter. eapply (step_fupdN_soundness_no_lc _ n m)=>Hinv.
iIntros "Hcred". destruct n as [|n].
{ by iApply fupd_mask_intro_discard; [|iApply (Hiter Hinv)]. }
simpl in Hiter |- *. iMod (Hiter with "Hcred") as "H". iIntros "!>!>!>".
iMod "H". clear. iInduction n as [|n] "IH"; [by iApply fupd_mask_intro_discard|].
simpl. iMod "H". iIntros "!>!>!>". iMod "H". by iApply "IH".
Qed.
Lemma step_fupdN_soundness_lc `{!invGpreS Σ} (P : iProp Σ) `{!Plain P} n m :
( `{Hinv: !invGS_gen HasLc Σ}, £ m ={,}=∗ |={}▷=>^n P)
P.
Proof.
intros Hiter.
eapply (fupd_soundness_lc (m + n)); [apply _..|].
iIntros (Hinv) "Hlc". rewrite lc_split.
iDestruct "Hlc" as "[Hm Hn]". iMod (Hiter with "Hm") as "Hupd".
clear Hiter.
iInduction n as [|n] "IH"; simpl.
- by iModIntro.
- rewrite lc_succ. iDestruct "Hn" as "[Hone Hn]".
iMod "Hupd". iMod (lc_fupd_elim_later with "Hone Hupd") as "> Hupd".
by iApply ("IH" with "Hn Hupd").
Qed.
Lemma step_fupdN_soundness_lc' `{!invGpreS Σ} (P : iProp Σ) `{!Plain P} n m :
( `{Hinv: !invGS_gen hlc Σ}, £ m ={}[]▷=∗^n P)
P.
Proof.
intros Hiter.
eapply (fupd_soundness_lc (m + n) ); [apply _..|].
iIntros (Hinv) "Hlc". rewrite lc_split.
iDestruct "Hlc" as "[Hm Hn]". iPoseProof (Hiter with "Hm") as "Hupd".
clear Hiter.
(* FIXME can we reuse [step_fupdN_soundness_lc] instead of redoing the induction? *)
iInduction n as [|n] "IH"; simpl.
- by iModIntro.
- rewrite lc_succ. iDestruct "Hn" as "[Hone Hn]".
iMod "Hupd". iMod (lc_fupd_elim_later with "Hone Hupd") as "> Hupd".
by iApply ("IH" with "Hn Hupd").
Qed.
(** Generic soundness lemma for the fancy update, parameterized by [use_credits]
on whether to use credits or not. *)
Lemma step_fupdN_soundness_gen `{!invGpreS Σ} (P : iProp Σ) `{!Plain P}
(hlc : has_lc) (n m : nat) :
( `{Hinv : invGS_gen hlc Σ},
£ m ={,}=∗ |={}▷=>^n P)
P.
Proof.
destruct hlc.
- apply step_fupdN_soundness_lc. done.
- apply step_fupdN_soundness_no_lc. done.
Qed.
(* This file shows that the fancy update can be encoded in terms of the (* This file shows that the fancy update can be encoded in terms of the
view shift, and that the laws of the fancy update can be derived from the view shift, and that the laws of the fancy update can be derived from the
laws of the view shift. *) laws of the view shift. *)
From iris.proofmode Require Import tactics.
From stdpp Require Export coPset. From stdpp Require Export coPset.
From iris.proofmode Require Import proofmode.
From iris.base_logic Require Export base_logic.
From iris.prelude Require Import options.
(* The sections add extra BI assumptions, which is only picked up with [Type*]. *)
Set Default Proof Using "Type*". Set Default Proof Using "Type*".
Section fupd. Section fupd.
...@@ -10,29 +14,27 @@ Context {M} (vs : coPset → coPset → uPred M → uPred M → uPred M). ...@@ -10,29 +14,27 @@ Context {M} (vs : coPset → coPset → uPred M → uPred M → uPred M).
Notation "P ={ E1 , E2 }=> Q" := (vs E1 E2 P Q) Notation "P ={ E1 , E2 }=> Q" := (vs E1 E2 P Q)
(at level 99, E1,E2 at level 50, Q at level 200, (at level 99, E1,E2 at level 50, Q at level 200,
format "P ={ E1 , E2 }=> Q") : uPred_scope. format "P ={ E1 , E2 }=> Q") : bi_scope.
Context (vs_ne : E1 E2, NonExpansive2 (vs E1 E2)). Context (vs_ne : E1 E2, NonExpansive2 (vs E1 E2)).
Context (vs_persistent : E1 E2 P Q, PersistentP (P ={E1,E2}=> Q)). Context (vs_persistent : E1 E2 P Q, Persistent (P ={E1,E2}=> Q)).
Context (vs_impl : E P Q, (P Q) P ={E,E}=> Q). Context (vs_impl : E P Q, (P Q) P ={E,E}=> Q).
Context (vs_transitive : E1 E2 E3 P Q R, Context (vs_transitive : E1 E2 E3 P Q R,
(P ={E1,E2}=> Q) (Q ={E2,E3}=> R) P ={E1,E3}=> R). (P ={E1,E2}=> Q) (Q ={E2,E3}=> R) P ={E1,E3}=> R).
Context (vs_mask_frame_r : E1 E2 Ef P Q, Context (vs_mask_frame_r : E1 E2 Ef P Q,
E1 Ef (P ={E1,E2}=> Q) P ={E1 Ef,E2 Ef}=> Q). E1 ## Ef (P ={E1,E2}=> Q) P ={E1 Ef,E2 Ef}=> Q).
Context (vs_frame_r : E1 E2 P Q R, (P ={E1,E2}=> Q) P R ={E1,E2}=> Q R). Context (vs_frame_r : E1 E2 P Q R, (P ={E1,E2}=> Q) P R ={E1,E2}=> Q R).
Context (vs_exists : {A} E1 E2 (Φ : A uPred M) Q, Context (vs_exists : {A} E1 E2 (Φ : A uPred M) Q,
( x, Φ x ={E1,E2}=> Q) ( x, Φ x) ={E1,E2}=> Q). ( x, Φ x ={E1,E2}=> Q) ( x, Φ x) ={E1,E2}=> Q).
Context (vs_persistent_intro_r : E1 E2 P Q R, Context (vs_persistent_intro_r : E1 E2 P Q R,
PersistentP R Persistent R
(R -∗ (P ={E1,E2}=> Q)) P R ={E1,E2}=> Q). (R -∗ (P ={E1,E2}=> Q)) P R ={E1,E2}=> Q).
Definition fupd (E1 E2 : coPset) (P : uPred M) : uPred M := Definition fupd (E1 E2 : coPset) (P : uPred M) : uPred M :=
( R, R vs E1 E2 R P)%I. R, R vs E1 E2 R P.
Notation "|={ E1 , E2 }=> Q" := (fupd E1 E2 Q) Notation "|={ E1 , E2 }=> Q" := (fupd E1 E2 Q) : bi_scope.
(at level 99, E1, E2 at level 50, Q at level 200,
format "|={ E1 , E2 }=> Q") : uPred_scope.
Global Instance fupd_ne E1 E2 : NonExpansive (@fupd E1 E2). Global Instance fupd_ne E1 E2 : NonExpansive (@fupd E1 E2).
Proof. solve_proper. Qed. Proof. solve_proper. Qed.
...@@ -44,7 +46,7 @@ Lemma fupd_mono E1 E2 P Q : (P ⊢ Q) → (|={E1,E2}=> P) ⊢ |={E1,E2}=> Q. ...@@ -44,7 +46,7 @@ Lemma fupd_mono E1 E2 P Q : (P ⊢ Q) → (|={E1,E2}=> P) ⊢ |={E1,E2}=> Q.
Proof. Proof.
iIntros (HPQ); iDestruct 1 as (R) "[HR Hvs]". iIntros (HPQ); iDestruct 1 as (R) "[HR Hvs]".
iExists R; iFrame "HR". iApply (vs_transitive with "[$Hvs]"). iExists R; iFrame "HR". iApply (vs_transitive with "[$Hvs]").
iApply vs_impl. iIntros "!# HP". by iApply HPQ. iApply vs_impl. iIntros "!> HP". by iApply HPQ.
Qed. Qed.
Lemma fupd_trans E1 E2 E3 P : (|={E1,E2}=> |={E2,E3}=> P) |={E1,E3}=> P. Lemma fupd_trans E1 E2 E3 P : (|={E1,E2}=> |={E2,E3}=> P) |={E1,E3}=> P.
...@@ -56,7 +58,7 @@ Proof. ...@@ -56,7 +58,7 @@ Proof.
Qed. Qed.
Lemma fupd_mask_frame_r E1 E2 Ef P : Lemma fupd_mask_frame_r E1 E2 Ef P :
E1 Ef (|={E1,E2}=> P) |={E1 Ef,E2 Ef}=> P. E1 ## Ef (|={E1,E2}=> P) |={E1 Ef,E2 Ef}=> P.
Proof. Proof.
iIntros (HE); iDestruct 1 as (R) "[HR Hvs]". iExists R; iFrame "HR". iIntros (HE); iDestruct 1 as (R) "[HR Hvs]". iExists R; iFrame "HR".
by iApply vs_mask_frame_r. by iApply vs_mask_frame_r.
...@@ -67,4 +69,4 @@ Proof. ...@@ -67,4 +69,4 @@ Proof.
iIntros "[Hvs HQ]". iDestruct "Hvs" as (R) "[HR Hvs]". iIntros "[Hvs HQ]". iDestruct "Hvs" as (R) "[HR Hvs]".
iExists (R Q)%I. iFrame "HR HQ". by iApply vs_frame_r. iExists (R Q)%I. iFrame "HR HQ". by iApply vs_frame_r.
Qed. Qed.
End fupd. End fupd.
\ No newline at end of file
From stdpp Require Export namespaces.
From iris.algebra Require Import reservation_map agree frac.
From iris.algebra Require Export dfrac.
From iris.bi.lib Require Import fractional.
From iris.proofmode Require Import proofmode.
From iris.base_logic.lib Require Export own.
From iris.base_logic.lib Require Import ghost_map.
From iris.prelude Require Import options.
Import uPred.
(** This file provides a generic mechanism for a language-level point-to
connective [l ↦{dq} v] reflecting the physical heap. This library is designed to
be used as a singleton (i.e., with only a single instance existing in any
proof), with the [gen_heapGS] typeclass providing the ghost names of that unique
instance. That way, [pointsto] does not need an explicit [gname] parameter.
This mechanism can be plugged into a language and related to the physical heap
by using [gen_heap_interp σ] in the state interpretation of the weakest
precondition. See heap-lang for an example.
If you are looking for a library providing "ghost heaps" independent of the
physical state, you will likely want explicit ghost names to disambiguate
multiple heaps and are thus better off using [ghost_map], or (if you need more
flexibility), directly using the underlying [algebra.lib.gmap_view].
This library is generic in the types [L] for locations and [V] for values and
supports fractional permissions. Next to the point-to connective [l ↦{dq} v],
which keeps track of the value [v] of a location [l], this library also provides
a way to attach "meta" or "ghost" data to locations. This is done as follows:
- When one allocates a location, in addition to the point-to connective [l ↦ v],
one also obtains the token [meta_token l ⊤]. This token is an exclusive
resource that denotes that no meta data has been associated with the
namespaces in the mask [⊤] for the location [l].
- Meta data tokens can be split w.r.t. namespace masks, i.e.
[meta_token l (E1 ∪ E2) ⊣⊢ meta_token l E1 ∗ meta_token l E2] if [E1 ## E2].
- Meta data can be set using the update [meta_token l E ==∗ meta l N x] provided
[↑N ⊆ E], and [x : A] for any countable [A]. The [meta l N x] connective is
persistent and denotes the knowledge that the meta data [x] has been
associated with namespace [N] to the location [l].
To make the mechanism as flexible as possible, the [x : A] in [meta l N x] can
be of any countable type [A]. This means that you can associate e.g. single
ghost names, but also tuples of ghost names, etc.
To further increase flexibility, the [meta l N x] and [meta_token l E]
connectives are annotated with a namespace [N] and mask [E]. That way, one can
assign a map of meta information to a location. This is particularly useful when
building abstractions, then one can gradually assign more ghost information to a
location instead of having to do all of this at once. We use namespaces so that
these can be matched up with the invariant namespaces. *)
(** To implement this mechanism, we use three pieces of ghost state:
- A [ghost_map L V], which keeps track of the values of locations.
- A [ghost_map L gname], which keeps track of the meta information of
locations. More specifically, this RA introduces an indirection: it keeps
track of a ghost name for each location.
- The ghost names in the aforementioned authoritative RA refer to namespace maps
[reservation_map (agree positive)], which store the actual meta information.
This indirection is needed because we cannot perform frame preserving updates
in an authoritative fragment without owning the full authoritative element
(in other words, without the indirection [meta_set] would need [gen_heap_interp]
as a premise).
*)
(** The CMRAs we need, and the global ghost names we are using. *)
Class gen_heapGpreS (L V : Type) (Σ : gFunctors) `{Countable L} := {
#[local] gen_heapGpreS_heap :: ghost_mapG Σ L V;
#[local] gen_heapGpreS_meta :: ghost_mapG Σ L gname;
#[local] gen_heapGpreS_meta_data :: inG Σ (reservation_mapR (agreeR positiveO));
}.
Class gen_heapGS (L V : Type) (Σ : gFunctors) `{Countable L} := GenHeapGS {
#[local] gen_heap_inG :: gen_heapGpreS L V Σ;
gen_heap_name : gname;
gen_meta_name : gname
}.
Global Arguments GenHeapGS L V Σ {_ _ _} _ _.
Global Arguments gen_heap_name {L V Σ _ _} _ : assert.
Global Arguments gen_meta_name {L V Σ _ _} _ : assert.
Definition gen_heapΣ (L V : Type) `{Countable L} : gFunctors := #[
ghost_mapΣ L V;
ghost_mapΣ L gname;
GFunctor (reservation_mapR (agreeR positiveO))
].
Global Instance subG_gen_heapGpreS {Σ L V} `{Countable L} :
subG (gen_heapΣ L V) Σ gen_heapGpreS L V Σ.
Proof. solve_inG. Qed.
Section definitions.
Context `{Countable L, hG : !gen_heapGS L V Σ}.
Definition gen_heap_interp (σ : gmap L V) : iProp Σ := m : gmap L gname,
(* The [⊆] is used to avoid assigning ghost information to the locations in
the initial heap (see [gen_heap_init]). *)
dom m dom σ
ghost_map_auth (gen_heap_name hG) 1 σ
ghost_map_auth (gen_meta_name hG) 1 m.
Local Definition pointsto_def (l : L) (dq : dfrac) (v: V) : iProp Σ :=
l [gen_heap_name hG]{dq} v.
Local Definition pointsto_aux : seal (@pointsto_def). Proof. by eexists. Qed.
Definition pointsto := pointsto_aux.(unseal).
Local Definition pointsto_unseal : @pointsto = @pointsto_def :=
pointsto_aux.(seal_eq).
Local Definition meta_token_def (l : L) (E : coPset) : iProp Σ :=
γm, l [gen_meta_name hG] γm own γm (reservation_map_token E).
Local Definition meta_token_aux : seal (@meta_token_def). Proof. by eexists. Qed.
Definition meta_token := meta_token_aux.(unseal).
Local Definition meta_token_unseal :
@meta_token = @meta_token_def := meta_token_aux.(seal_eq).
(** TODO: The use of [positives_flatten] violates the namespace abstraction
(see the proof of [meta_set]. *)
Local Definition meta_def `{Countable A} (l : L) (N : namespace) (x : A) : iProp Σ :=
γm, l [gen_meta_name hG] γm
own γm (reservation_map_data (positives_flatten N) (to_agree (encode x))).
Local Definition meta_aux : seal (@meta_def). Proof. by eexists. Qed.
Definition meta := meta_aux.(unseal).
Local Definition meta_unseal : @meta = @meta_def := meta_aux.(seal_eq).
End definitions.
Global Arguments meta {L _ _ V Σ _ A _ _} l N x.
Local Notation "l ↦ dq v" := (pointsto l dq v)
(at level 20, dq custom dfrac at level 1, format "l ↦ dq v") : bi_scope.
Section gen_heap.
Context {L V} `{Countable L, !gen_heapGS L V Σ}.
Implicit Types P Q : iProp Σ.
Implicit Types Φ : V iProp Σ.
Implicit Types σ : gmap L V.
Implicit Types m : gmap L gname.
Implicit Types l : L.
Implicit Types v : V.
(** General properties of pointsto *)
Global Instance pointsto_timeless l dq v : Timeless (l {dq} v).
Proof. rewrite pointsto_unseal. apply _. Qed.
Global Instance pointsto_fractional l v : Fractional (λ q, l {#q} v)%I.
Proof. rewrite pointsto_unseal. apply _. Qed.
Global Instance pointsto_as_fractional l q v :
AsFractional (l {#q} v) (λ q, l {#q} v)%I q.
Proof. rewrite pointsto_unseal. apply _. Qed.
Global Instance pointsto_persistent l v : Persistent (l ↦□ v).
Proof. rewrite pointsto_unseal. apply _. Qed.
Lemma pointsto_valid l dq v : l {dq} v -∗ ⌜✓ dq⌝%Qp.
Proof. rewrite pointsto_unseal. apply ghost_map_elem_valid. Qed.
Lemma pointsto_valid_2 l dq1 dq2 v1 v2 :
l {dq1} v1 -∗ l {dq2} v2 -∗ ⌜✓ (dq1 dq2) v1 = v2⌝.
Proof. rewrite pointsto_unseal. apply ghost_map_elem_valid_2. Qed.
(** Almost all the time, this is all you really need. *)
Lemma pointsto_agree l dq1 dq2 v1 v2 : l {dq1} v1 -∗ l {dq2} v2 -∗ v1 = v2⌝.
Proof. rewrite pointsto_unseal. apply ghost_map_elem_agree. Qed.
Global Instance pointsto_combine_sep_gives l dq1 dq2 v1 v2 :
CombineSepGives (l {dq1} v1) (l {dq2} v2) ⌜✓ (dq1 dq2) v1 = v2 | 30.
Proof.
rewrite /CombineSepGives. iIntros "[H1 H2]".
iDestruct (pointsto_valid_2 with "H1 H2") as %?. eauto.
Qed.
Lemma pointsto_combine l dq1 dq2 v1 v2 :
l {dq1} v1 -∗ l {dq2} v2 -∗ l {dq1 dq2} v1 v1 = v2⌝.
Proof. rewrite pointsto_unseal. apply ghost_map_elem_combine. Qed.
Global Instance pointsto_combine_as l dq1 dq2 v1 v2 :
CombineSepAs (l {dq1} v1) (l {dq2} v2) (l {dq1 dq2} v1) | 60.
(* higher cost than the Fractional instance, which kicks in for #qs *)
Proof.
rewrite /CombineSepAs. iIntros "[H1 H2]".
iDestruct (pointsto_combine with "H1 H2") as "[$ _]".
Qed.
Lemma pointsto_frac_ne l1 l2 dq1 dq2 v1 v2 :
¬ (dq1 dq2) l1 {dq1} v1 -∗ l2 {dq2} v2 -∗ l1 l2⌝.
Proof. rewrite pointsto_unseal. apply ghost_map_elem_frac_ne. Qed.
Lemma pointsto_ne l1 l2 dq2 v1 v2 : l1 v1 -∗ l2 {dq2} v2 -∗ l1 l2⌝.
Proof. rewrite pointsto_unseal. apply ghost_map_elem_ne. Qed.
(** Permanently turn any points-to predicate into a persistent
points-to predicate. *)
Lemma pointsto_persist l dq v : l {dq} v ==∗ l ↦□ v.
Proof. rewrite pointsto_unseal. apply ghost_map_elem_persist. Qed.
(** Recover fractional ownership for read-only element. *)
Lemma pointsto_unpersist l v :
l ↦□ v ==∗ q, l {# q} v.
Proof. rewrite pointsto_unseal. apply ghost_map_elem_unpersist. Qed.
(** Framing support *)
Global Instance frame_pointsto p l v q1 q2 q :
FrameFractionalQp q1 q2 q
Frame p (l {#q1} v) (l {#q2} v) (l {#q} v) | 5.
Proof. apply: frame_fractional. Qed.
(** General properties of [meta] and [meta_token] *)
Global Instance meta_token_timeless l N : Timeless (meta_token l N).
Proof. rewrite meta_token_unseal. apply _. Qed.
Global Instance meta_timeless `{Countable A} l N (x : A) : Timeless (meta l N x).
Proof. rewrite meta_unseal. apply _. Qed.
Global Instance meta_persistent `{Countable A} l N (x : A) : Persistent (meta l N x).
Proof. rewrite meta_unseal. apply _. Qed.
Lemma meta_token_union_1 l E1 E2 :
E1 ## E2 meta_token l (E1 E2) -∗ meta_token l E1 meta_token l E2.
Proof.
rewrite meta_token_unseal /meta_token_def. intros ?. iDestruct 1 as (γm1) "[#Hγm Hm]".
rewrite reservation_map_token_union //. iDestruct "Hm" as "[Hm1 Hm2]".
iSplitL "Hm1"; eauto.
Qed.
Lemma meta_token_union_2 l E1 E2 :
meta_token l E1 -∗ meta_token l E2 -∗ meta_token l (E1 E2).
Proof.
rewrite meta_token_unseal /meta_token_def.
iIntros "(%γm1 & #Hγm1 & Hm1) (%γm2 & #Hγm2 & Hm2)".
iCombine "Hγm1 Hγm2" gives %[_ ->].
iCombine "Hm1 Hm2" gives %?%reservation_map_token_valid_op.
iExists γm2. iFrame "Hγm2". rewrite reservation_map_token_union //. by iSplitL "Hm1".
Qed.
Lemma meta_token_union l E1 E2 :
E1 ## E2 meta_token l (E1 E2) ⊣⊢ meta_token l E1 meta_token l E2.
Proof.
intros; iSplit; first by iApply meta_token_union_1.
iIntros "[Hm1 Hm2]". by iApply (meta_token_union_2 with "Hm1 Hm2").
Qed.
Lemma meta_token_difference l E1 E2 :
E1 E2 meta_token l E2 ⊣⊢ meta_token l E1 meta_token l (E2 E1).
Proof.
intros. rewrite {1}(union_difference_L E1 E2) //.
by rewrite meta_token_union; last set_solver.
Qed.
Lemma meta_agree `{Countable A} l i (x1 x2 : A) :
meta l i x1 -∗ meta l i x2 -∗ x1 = x2⌝.
Proof.
rewrite meta_unseal /meta_def.
iIntros "(%γm1 & Hγm1 & Hm1) (%γm2 & Hγm2 & Hm2)".
iCombine "Hγm1 Hγm2" gives %[_ ->].
iCombine "Hm1 Hm2" gives %; iPureIntro.
move: . rewrite -reservation_map_data_op reservation_map_data_valid.
move=> /to_agree_op_inv_L. naive_solver.
Qed.
Lemma meta_set `{Countable A} E l (x : A) N :
N E meta_token l E ==∗ meta l N x.
Proof.
rewrite meta_token_unseal meta_unseal /meta_token_def /meta_def.
iDestruct 1 as (γm) "[Hγm Hm]". iExists γm. iFrame "Hγm".
iApply (own_update with "Hm").
apply reservation_map_alloc; last done.
cut (positives_flatten N ∈@{coPset} N); first by set_solver.
(* TODO: Avoid unsealing here. *)
rewrite namespaces.nclose_unseal. apply elem_coPset_suffixes.
exists 1%positive. by rewrite left_id_L.
Qed.
(** Update lemmas *)
Lemma gen_heap_alloc σ l v :
σ !! l = None
gen_heap_interp σ ==∗ gen_heap_interp (<[l:=v]>σ) l v meta_token l .
Proof.
iIntros (Hσl). rewrite /gen_heap_interp pointsto_unseal /pointsto_def
meta_token_unseal /meta_token_def /=.
iDestruct 1 as (m Hσm) "[Hσ Hm]".
iMod (ghost_map_insert l with "Hσ") as "[Hσ Hl]"; first done.
iMod (own_alloc (reservation_map_token )) as (γm) "Hγm".
{ apply reservation_map_token_valid. }
iMod (ghost_map_insert_persist l with "Hm") as "[Hm Hlm]".
{ move: Hσl. rewrite -!not_elem_of_dom. set_solver. }
iModIntro. iFrame "Hl". iSplitL "Hσ Hm"; last by eauto with iFrame.
iExists (<[l:=γm]> m). iFrame. iPureIntro.
rewrite !dom_insert_L. set_solver.
Qed.
Lemma gen_heap_alloc_big σ σ' :
σ' ## σ
gen_heap_interp σ ==∗
gen_heap_interp (σ' σ) ([ map] l v σ', l v) ([ map] l _ σ', meta_token l ).
Proof.
revert σ; induction σ' as [| l v σ' Hl IH] using map_ind; iIntros (σ Hdisj) "Hσ".
{ rewrite left_id_L. auto. }
iMod (IH with "Hσ") as "[Hσ'σ Hσ']"; first by eapply map_disjoint_insert_l.
decompose_map_disjoint.
rewrite !big_opM_insert // -insert_union_l //.
by iMod (gen_heap_alloc with "Hσ'σ") as "($ & $ & $)";
first by apply lookup_union_None.
Qed.
Lemma gen_heap_valid σ l dq v : gen_heap_interp σ -∗ l {dq} v -∗ σ !! l = Some v⌝.
Proof.
iDestruct 1 as (m Hσm) "[Hσ _]". iIntros "Hl".
rewrite /gen_heap_interp pointsto_unseal.
by iCombine "Hσ Hl" gives %?.
Qed.
Lemma gen_heap_update σ l v1 v2 :
gen_heap_interp σ -∗ l v1 ==∗ gen_heap_interp (<[l:=v2]>σ) l v2.
Proof.
iDestruct 1 as (m Hσm) "[Hσ Hm]".
iIntros "Hl". rewrite /gen_heap_interp pointsto_unseal /pointsto_def.
iCombine "Hσ Hl" gives %Hl.
iMod (ghost_map_update with "Hσ Hl") as "[Hσ Hl]".
iModIntro. iFrame "Hl". iExists m. iFrame.
iPureIntro. apply elem_of_dom_2 in Hl.
rewrite dom_insert_L. set_solver.
Qed.
End gen_heap.
(** This variant of [gen_heap_init] should only be used when absolutely needed.
The key difference to [gen_heap_init] is that the [inG] instances in the new
[gen_heapGS] instance are related to the original [gen_heapGpreS] instance,
whereas [gen_heap_init] forgets about that relation. *)
Lemma gen_heap_init_names `{Countable L, !gen_heapGpreS L V Σ} σ :
|==> γh γm : gname,
let hG := GenHeapGS L V Σ γh γm in
gen_heap_interp σ ([ map] l v σ, l v) ([ map] l _ σ, meta_token l ).
Proof.
iMod (ghost_map_alloc_empty (K:=L) (V:=V)) as (γh) "Hh".
iMod (ghost_map_alloc_empty (K:=L) (V:=gname)) as (γm) "Hm".
iExists γh, γm.
iAssert (gen_heap_interp (hG:=GenHeapGS _ _ _ γh γm) ) with "[Hh Hm]" as "Hinterp".
{ iExists ; simpl. iFrame "Hh Hm". by rewrite dom_empty_L. }
iMod (gen_heap_alloc_big with "Hinterp") as "(Hinterp & $ & $)".
{ apply map_disjoint_empty_r. }
rewrite right_id_L. done.
Qed.
Lemma gen_heap_init `{Countable L, !gen_heapGpreS L V Σ} σ :
|==> _ : gen_heapGS L V Σ,
gen_heap_interp σ ([ map] l v σ, l v) ([ map] l _ σ, meta_token l ).
Proof.
iMod (gen_heap_init_names σ) as (γh γm) "Hinit".
iExists (GenHeapGS _ _ _ γh γm).
done.
Qed.
From iris.algebra Require Import auth excl gmap.
From iris.base_logic.lib Require Import own invariants gen_heap.
From iris.proofmode Require Import proofmode.
From iris.prelude Require Import options.
(** An "invariant" location is a location that has some invariant about its
value attached to it, and that can never be deallocated explicitly by the
program. It provides a persistent witness that will always allow reading the
location, guaranteeing that the value read will satisfy the invariant.
This is useful for data structures like RDCSS that need to read locations long
after their ownership has been passed back to the client, but do not care *what*
it is that they are reading in that case. In that extreme case, the invariant
may just be [True].
Since invariant locations cannot be deallocated, they only make sense when
modeling languages with garbage collection. HeapLang can be used to model
either language by choosing whether or not to use the [Free] operation. By
using a separate assertion [inv_pointsto_own] for "invariant" locations, we can
keep all the other proofs that do not need it conservative. *)
Definition inv_heapN: namespace := nroot .@ "inv_heap".
Local Notation "l ↦ v" := (pointsto l (DfracOwn 1) v) (at level 20) : bi_scope.
Definition inv_heap_mapUR (L V : Type) `{Countable L} : ucmra := gmapUR L $ prodR
(optionR $ exclR $ leibnizO V)
(agreeR (V -d> PropO)).
Definition to_inv_heap {L V : Type} `{Countable L}
(h: gmap L (V * (V -d> PropO))) : inv_heap_mapUR L V :=
prod_map (λ x, Excl' x) to_agree <$> h.
Class inv_heapGpreS (L V : Type) (Σ : gFunctors) `{Countable L} := {
#[local] inv_heapGpreS_inG :: inG Σ (authR (inv_heap_mapUR L V))
}.
Class inv_heapGS (L V : Type) (Σ : gFunctors) `{Countable L} := Inv_HeapG {
#[local] inv_heap_inG :: inv_heapGpreS L V Σ;
inv_heap_name : gname
}.
Global Arguments Inv_HeapG _ _ {_ _ _ _}.
Global Arguments inv_heap_name {_ _ _ _ _} _ : assert.
Definition inv_heapΣ (L V : Type) `{Countable L} : gFunctors :=
#[ GFunctor (authR (inv_heap_mapUR L V)) ].
Global Instance subG_inv_heapGpreS (L V : Type) `{Countable L} {Σ} :
subG (inv_heapΣ L V) Σ inv_heapGpreS L V Σ.
Proof. solve_inG. Qed.
Section definitions.
Context {L V : Type} `{Countable L}.
Context `{!invGS_gen hlc Σ, !gen_heapGS L V Σ, gG: !inv_heapGS L V Σ}.
Definition inv_heap_inv_P : iProp Σ :=
h : gmap L (V * (V -d> PropO)),
own (inv_heap_name gG) ( to_inv_heap h)
[ map] l p h, p.2 p.1 l p.1.
Definition inv_heap_inv : iProp Σ := inv inv_heapN inv_heap_inv_P.
Definition inv_pointsto_own (l : L) (v : V) (I : V Prop) : iProp Σ :=
own (inv_heap_name gG) ( {[l := (Excl' v, to_agree I) ]}).
Definition inv_pointsto (l : L) (I : V Prop) : iProp Σ :=
own (inv_heap_name gG) ( {[l := (None, to_agree I)]}).
End definitions.
Local Notation "l '↦_' I v" := (inv_pointsto_own l v I%stdpp%type)
(at level 20, I at level 9, format "l '↦_' I v") : bi_scope.
Local Notation "l '↦_' I □" := (inv_pointsto l I%stdpp%type)
(at level 20, I at level 9, format "l '↦_' I '□'") : bi_scope.
(* [inv_heap_inv] has no parameters to infer the types from, so we need to
make them explicit. *)
Global Arguments inv_heap_inv _ _ {_ _ _ _ _ _ _}.
Global Instance: Params (@inv_pointsto_own) 8 := {}.
Global Instance: Params (@inv_pointsto) 7 := {}.
Section to_inv_heap.
Context {L V : Type} `{Countable L}.
Implicit Types (h : gmap L (V * (V -d> PropO))).
Lemma to_inv_heap_valid h : to_inv_heap h.
Proof. intros l. rewrite lookup_fmap. by case: (h !! l). Qed.
Lemma to_inv_heap_singleton l v I :
to_inv_heap {[l := (v, I)]} =@{inv_heap_mapUR L V} {[l := (Excl' v, to_agree I)]}.
Proof. by rewrite /to_inv_heap fmap_insert fmap_empty. Qed.
Lemma to_inv_heap_insert l v I h :
to_inv_heap (<[l := (v, I)]> h) = <[l := (Excl' v, to_agree I)]> (to_inv_heap h).
Proof. by rewrite /to_inv_heap fmap_insert. Qed.
Lemma lookup_to_inv_heap_None h l :
h !! l = None to_inv_heap h !! l = None.
Proof. by rewrite /to_inv_heap lookup_fmap=> ->. Qed.
Lemma lookup_to_inv_heap_Some h l v I :
h !! l = Some (v, I) to_inv_heap h !! l = Some (Excl' v, to_agree I).
Proof. by rewrite /to_inv_heap lookup_fmap=> ->. Qed.
Lemma lookup_to_inv_heap_Some_2 h l v' I' :
to_inv_heap h !! l Some (v', I')
v I, v' = Excl' v I' to_agree I h !! l = Some (v, I).
Proof.
rewrite /to_inv_heap /prod_map lookup_fmap. rewrite fmap_Some_equiv.
intros ([] & Hsome & [Heqv HeqI]); simplify_eq/=; eauto.
Qed.
End to_inv_heap.
Lemma inv_heap_init (L V : Type) `{Countable L, !invGS_gen hlc Σ, !gen_heapGS L V Σ, !inv_heapGpreS L V Σ} E :
|==> _ : inv_heapGS L V Σ, |={E}=> inv_heap_inv L V.
Proof.
iMod (own_alloc ( (to_inv_heap ))) as (γ) "H●".
{ rewrite auth_auth_valid. exact: to_inv_heap_valid. }
iModIntro.
iExists (Inv_HeapG L V γ).
iAssert (inv_heap_inv_P (gG := Inv_HeapG L V γ)) with "[H●]" as "P".
{ iExists _. iFrame. done. }
iApply (inv_alloc inv_heapN E inv_heap_inv_P with "P").
Qed.
Section inv_heap.
Context {L V : Type} `{Countable L}.
Context `{!invGS_gen hlc Σ, !gen_heapGS L V Σ, gG: !inv_heapGS L V Σ}.
Implicit Types (l : L) (v : V) (I : V Prop).
Implicit Types (h : gmap L (V * (V -d> PropO))).
(** * Helpers *)
Lemma inv_pointsto_lookup_Some l h I :
l ↦_I -∗ own (inv_heap_name gG) ( to_inv_heap h) -∗
⌜∃ v I', h !! l = Some (v, I') w, I w I' w ⌝.
Proof.
iIntros "Hl_inv H◯".
iCombine "H◯ Hl_inv" gives %[Hincl Hvalid]%auth_both_valid_discrete.
iPureIntro.
move: Hincl; rewrite singleton_included_l; intros ([v' I'] & Hsome & Hincl).
apply lookup_to_inv_heap_Some_2 in Hsome as (v'' & I'' & _ & HI & Hh).
move: Hincl; rewrite HI Some_included_total pair_included
to_agree_included; intros [??]; eauto.
Qed.
Lemma inv_pointsto_own_lookup_Some l v h I :
l ↦_I v -∗ own (inv_heap_name gG) ( to_inv_heap h) -∗
I', h !! l = Some (v, I') w, I w I' w ⌝.
Proof.
iIntros "Hl_inv H●".
iCombine "H● Hl_inv" gives %[Hincl Hvalid]%auth_both_valid_discrete.
iPureIntro.
move: Hincl; rewrite singleton_included_l; intros ([v' I'] & Hsome & Hincl).
apply lookup_to_inv_heap_Some_2 in Hsome as (v'' & I'' & -> & HI & Hh).
move: Hincl; rewrite HI Some_included_total pair_included
Excl_included to_agree_included; intros [-> ?]; eauto.
Qed.
(** * Typeclass instances *)
(* FIXME(Coq #6294): needs new unification
The uses of [apply:] and [move: ..; rewrite ..] (by lack of [apply: .. in ..])
in this file are needed because Coq's default unification algorithm fails. *)
Global Instance inv_pointsto_own_proper l v :
Proper (pointwise_relation _ iff ==> ()) (inv_pointsto_own l v).
Proof.
intros I1 I2 ?. rewrite /inv_pointsto_own. do 2 f_equiv.
apply: singletonM_proper. f_equiv. by apply: to_agree_proper.
Qed.
Global Instance inv_pointsto_proper l :
Proper (pointwise_relation _ iff ==> ()) (inv_pointsto l).
Proof.
intros I1 I2 ?. rewrite /inv_pointsto. do 2 f_equiv.
apply: singletonM_proper. f_equiv. by apply: to_agree_proper.
Qed.
Global Instance inv_heap_inv_persistent : Persistent (inv_heap_inv L V).
Proof. apply _. Qed.
Global Instance inv_pointsto_persistent l I : Persistent (l ↦_I ).
Proof. apply _. Qed.
Global Instance inv_pointsto_timeless l I : Timeless (l ↦_I ).
Proof. apply _. Qed.
Global Instance inv_pointsto_own_timeless l v I : Timeless (l ↦_I v).
Proof. apply _. Qed.
(** * Public lemmas *)
Lemma make_inv_pointsto l v I E :
inv_heapN E
I v
inv_heap_inv L V -∗ l v ={E}=∗ l ↦_I v.
Proof.
iIntros (HN HI) "#Hinv Hl".
iMod (inv_acc_timeless _ inv_heapN with "Hinv") as "[HP Hclose]"; first done.
iDestruct "HP" as (h) "[H● HsepM]".
destruct (h !! l) as [v'| ] eqn: Hlookup.
- (* auth map contains l --> contradiction *)
iDestruct (big_sepM_lookup with "HsepM") as "[_ Hl']"; first done.
by iCombine "Hl Hl'" gives %[??].
- iMod (own_update with "H●") as "[H● H◯]".
{ apply lookup_to_inv_heap_None in Hlookup.
apply (auth_update_alloc _
(to_inv_heap (<[l:=(v,I)]> h)) (to_inv_heap ({[l:=(v,I)]}))).
rewrite to_inv_heap_insert to_inv_heap_singleton.
by apply: alloc_singleton_local_update. }
iMod ("Hclose" with "[H● HsepM Hl]").
+ iExists _.
iDestruct (big_sepM_insert _ _ _ (_,_) with "[$HsepM $Hl]")
as "HsepM"; auto with iFrame.
+ iModIntro. by rewrite /inv_pointsto_own to_inv_heap_singleton.
Qed.
Lemma inv_pointsto_own_inv l v I : l ↦_I v -∗ l ↦_I □.
Proof.
iApply own_mono. apply auth_frag_mono.
rewrite singleton_included_total pair_included.
split; [apply: ucmra_unit_least|done].
Qed.
(** An accessor to make use of [inv_pointsto_own].
This opens the invariant *before* consuming [inv_pointsto_own] so that you can use
this before opening an atomic update that provides [inv_pointsto_own]!. *)
Lemma inv_pointsto_own_acc_strong E :
inv_heapN E
inv_heap_inv L V ={E, E inv_heapN}=∗ l v I, l ↦_I v -∗
(I v l v ( w, I w -∗ l w ==∗
inv_pointsto_own l w I |={E inv_heapN, E}=> True)).
Proof.
iIntros (HN) "#Hinv".
iMod (inv_acc_timeless _ inv_heapN _ with "Hinv") as "[HP Hclose]"; first done.
iIntros "!>" (l v I) "Hl_inv".
iDestruct "HP" as (h) "[H● HsepM]".
iDestruct (inv_pointsto_own_lookup_Some with "Hl_inv H●") as %(I'&?&HI').
setoid_rewrite HI'.
iDestruct (big_sepM_delete with "HsepM") as "[[HI Hl] HsepM]"; first done.
iIntros "{$HI $Hl}" (w ?) "Hl".
iMod (own_update_2 with "H● Hl_inv") as "[H● H◯]".
{ apply (auth_update _ _ (<[l := (Excl' w, to_agree I')]> (to_inv_heap h))
{[l := (Excl' w, to_agree I)]}).
apply: singleton_local_update.
{ by apply lookup_to_inv_heap_Some. }
apply: prod_local_update_1. apply: option_local_update.
apply: exclusive_local_update. done. }
iDestruct (big_sepM_insert _ _ _ (w, I') with "[$HsepM $Hl //]") as "HsepM".
{ apply lookup_delete. }
rewrite insert_delete_insert -to_inv_heap_insert. iIntros "!> {$H◯}".
iApply ("Hclose" with "[H● HsepM]"). iExists _; by iFrame.
Qed.
(** Derive a more standard accessor. *)
Lemma inv_pointsto_own_acc E l v I:
inv_heapN E
inv_heap_inv L V -∗ l ↦_I v ={E, E inv_heapN}=∗
(I v l v ( w, I w -∗ l w ={E inv_heapN, E}=∗ l ↦_I w)).
Proof.
iIntros (?) "#Hinv Hl".
iMod (inv_pointsto_own_acc_strong with "Hinv") as "Hacc"; first done.
iDestruct ("Hacc" with "Hl") as "(HI & Hl & Hclose)".
iIntros "!> {$HI $Hl}" (w) "HI Hl".
iMod ("Hclose" with "HI Hl") as "[$ $]".
Qed.
Lemma inv_pointsto_acc l I E :
inv_heapN E
inv_heap_inv L V -∗ l ↦_I ={E, E inv_heapN}=∗
v, I v l v (l v ={E inv_heapN, E}=∗ True).
Proof.
iIntros (HN) "#Hinv Hl_inv".
iMod (inv_acc_timeless _ inv_heapN _ with "Hinv") as "[HP Hclose]"; first done.
iModIntro.
iDestruct "HP" as (h) "[H● HsepM]".
iDestruct (inv_pointsto_lookup_Some with "Hl_inv H●") as %(v&I'&?&HI').
iDestruct (big_sepM_lookup_acc with "HsepM") as "[[#HI Hl] HsepM]"; first done.
setoid_rewrite HI'.
iExists _. iIntros "{$HI $Hl} Hl".
iMod ("Hclose" with "[H● HsepM Hl]"); last done.
iExists _. iFrame "H●". iApply ("HsepM" with "[$Hl //]").
Qed.
End inv_heap.
Global Typeclasses Opaque inv_heap_inv inv_pointsto inv_pointsto_own.
(** A "ghost map" (or "ghost heap") with a proposition controlling authoritative
ownership of the entire heap, and a "points-to-like" proposition for (mutable,
fractional, or persistent read-only) ownership of individual elements. *)
From iris.bi.lib Require Import fractional.
From iris.proofmode Require Import proofmode.
From iris.algebra Require Import gmap_view.
From iris.algebra Require Export dfrac.
From iris.base_logic.lib Require Export own.
From iris.prelude Require Import options.
(** The CMRA we need.
FIXME: This is intentionally discrete-only, but
should we support setoids via [Equiv]? *)
Class ghost_mapG Σ (K V : Type) `{Countable K} := GhostMapG {
#[local] ghost_map_inG :: inG Σ (gmap_viewR K (agreeR (leibnizO V)));
}.
Definition ghost_mapΣ (K V : Type) `{Countable K} : gFunctors :=
#[ GFunctor (gmap_viewR K (agreeR (leibnizO V))) ].
Global Instance subG_ghost_mapΣ Σ (K V : Type) `{Countable K} :
subG (ghost_mapΣ K V) Σ ghost_mapG Σ K V.
Proof. solve_inG. Qed.
Section definitions.
Context `{ghost_mapG Σ K V}.
Local Definition ghost_map_auth_def
(γ : gname) (q : Qp) (m : gmap K V) : iProp Σ :=
own γ (gmap_view_auth (V:=agreeR $ leibnizO V) (DfracOwn q) (to_agree <$> m)).
Local Definition ghost_map_auth_aux : seal (@ghost_map_auth_def).
Proof. by eexists. Qed.
Definition ghost_map_auth := ghost_map_auth_aux.(unseal).
Local Definition ghost_map_auth_unseal :
@ghost_map_auth = @ghost_map_auth_def := ghost_map_auth_aux.(seal_eq).
Local Definition ghost_map_elem_def
(γ : gname) (k : K) (dq : dfrac) (v : V) : iProp Σ :=
own γ (gmap_view_frag (V:=agreeR $ leibnizO V) k dq (to_agree v)).
Local Definition ghost_map_elem_aux : seal (@ghost_map_elem_def).
Proof. by eexists. Qed.
Definition ghost_map_elem := ghost_map_elem_aux.(unseal).
Local Definition ghost_map_elem_unseal :
@ghost_map_elem = @ghost_map_elem_def := ghost_map_elem_aux.(seal_eq).
End definitions.
Notation "k ↪[ γ ] dq v" := (ghost_map_elem γ k dq v)
(at level 20, γ at level 50, dq custom dfrac at level 1,
format "k ↪[ γ ] dq v") : bi_scope.
Local Ltac unseal := rewrite
?ghost_map_auth_unseal /ghost_map_auth_def
?ghost_map_elem_unseal /ghost_map_elem_def.
Section lemmas.
Context `{ghost_mapG Σ K V}.
Implicit Types (k : K) (v : V) (dq : dfrac) (q : Qp) (m : gmap K V).
(** * Lemmas about the map elements *)
Global Instance ghost_map_elem_timeless k γ dq v : Timeless (k [γ]{dq} v).
Proof. unseal. apply _. Qed.
Global Instance ghost_map_elem_persistent k γ v : Persistent (k [γ] v).
Proof. unseal. apply _. Qed.
Global Instance ghost_map_elem_fractional k γ v :
Fractional (λ q, k [γ]{#q} v)%I.
Proof. unseal=> p q. rewrite -own_op -gmap_view_frag_add agree_idemp //. Qed.
Global Instance ghost_map_elem_as_fractional k γ q v :
AsFractional (k [γ]{#q} v) (λ q, k [γ]{#q} v)%I q.
Proof. split; first done. apply _. Qed.
Local Lemma ghost_map_elems_unseal γ m dq :
([ map] k v m, k [γ]{dq} v) ==∗
own γ ([^op map] kv m,
gmap_view_frag (V:=agreeR (leibnizO V)) k dq (to_agree v)).
Proof.
unseal. destruct (decide (m = )) as [->|Hne].
- rewrite !big_opM_empty. iIntros "_". iApply own_unit.
- rewrite big_opM_own //. iIntros "?". done.
Qed.
Lemma ghost_map_elem_valid k γ dq v : k [γ]{dq} v -∗ ⌜✓ dq⌝.
Proof.
unseal. iIntros "Helem".
iDestruct (own_valid with "Helem") as %?%gmap_view_frag_valid.
naive_solver.
Qed.
Lemma ghost_map_elem_valid_2 k γ dq1 dq2 v1 v2 :
k [γ]{dq1} v1 -∗ k [γ]{dq2} v2 -∗ ⌜✓ (dq1 dq2) v1 = v2⌝.
Proof.
unseal. iIntros "H1 H2".
iCombine "H1 H2" gives %[? Hag]%gmap_view_frag_op_valid.
rewrite to_agree_op_valid_L in Hag. done.
Qed.
Lemma ghost_map_elem_agree k γ dq1 dq2 v1 v2 :
k [γ]{dq1} v1 -∗ k [γ]{dq2} v2 -∗ v1 = v2⌝.
Proof.
iIntros "Helem1 Helem2".
iDestruct (ghost_map_elem_valid_2 with "Helem1 Helem2") as %[_ ?].
done.
Qed.
Global Instance ghost_map_elem_combine_gives γ k v1 dq1 v2 dq2 :
CombineSepGives (k [γ]{dq1} v1) (k [γ]{dq2} v2) ⌜✓ (dq1 dq2) v1 = v2⌝.
Proof.
rewrite /CombineSepGives. iIntros "[H1 H2]".
iDestruct (ghost_map_elem_valid_2 with "H1 H2") as %[H1 H2].
eauto.
Qed.
Lemma ghost_map_elem_combine k γ dq1 dq2 v1 v2 :
k [γ]{dq1} v1 -∗ k [γ]{dq2} v2 -∗ k [γ]{dq1 dq2} v1 v1 = v2⌝.
Proof.
iIntros "Hl1 Hl2". iDestruct (ghost_map_elem_agree with "Hl1 Hl2") as %->.
unseal. iCombine "Hl1 Hl2" as "Hl". rewrite agree_idemp. eauto with iFrame.
Qed.
Global Instance ghost_map_elem_combine_as k γ dq1 dq2 v1 v2 :
CombineSepAs (k [γ]{dq1} v1) (k [γ]{dq2} v2) (k [γ]{dq1 dq2} v1) | 60.
(* higher cost than the Fractional instance [combine_sep_fractional_bwd],
which kicks in for #qs *)
Proof.
rewrite /CombineSepAs. iIntros "[H1 H2]".
iDestruct (ghost_map_elem_combine with "H1 H2") as "[$ _]".
Qed.
Lemma ghost_map_elem_frac_ne γ k1 k2 dq1 dq2 v1 v2 :
¬ (dq1 dq2) k1 [γ]{dq1} v1 -∗ k2 [γ]{dq2} v2 -∗ k1 k2⌝.
Proof.
iIntros (?) "H1 H2"; iIntros (->).
by iCombine "H1 H2" gives %[??].
Qed.
Lemma ghost_map_elem_ne γ k1 k2 dq2 v1 v2 :
k1 [γ] v1 -∗ k2 [γ]{dq2} v2 -∗ k1 k2⌝.
Proof. apply ghost_map_elem_frac_ne. apply: exclusive_l. Qed.
(** Make an element read-only. *)
Lemma ghost_map_elem_persist k γ dq v :
k [γ]{dq} v ==∗ k [γ] v.
Proof. unseal. iApply own_update. apply gmap_view_frag_persist. Qed.
(** Recover fractional ownership for read-only element. *)
Lemma ghost_map_elem_unpersist k γ v :
k [γ] v ==∗ q, k [γ]{# q} v.
Proof.
unseal. iIntros "H".
iMod (own_updateP with "H") as "H";
first by apply gmap_view_frag_unpersist.
iDestruct "H" as (? (q&->)) "H".
iIntros "!>". iExists q. done.
Qed.
(** * Lemmas about [ghost_map_auth] *)
Lemma ghost_map_alloc_strong P m :
pred_infinite P
|==> γ, P γ ghost_map_auth γ 1 m [ map] k v m, k [γ] v.
Proof.
unseal. intros.
iMod (own_alloc_strong
(gmap_view_auth (V:=agreeR (leibnizO V)) (DfracOwn 1) ) P)
as (γ) "[% Hauth]"; first done.
{ apply gmap_view_auth_valid. }
iExists γ. iSplitR; first done.
rewrite -big_opM_own_1 -own_op. iApply (own_update with "Hauth").
etrans; first apply (gmap_view_alloc_big _ (to_agree <$> m) (DfracOwn 1)).
- apply map_disjoint_empty_r.
- done.
- by apply map_Forall_fmap.
- rewrite right_id big_opM_fmap. done.
Qed.
Lemma ghost_map_alloc_strong_empty P :
pred_infinite P
|==> γ, P γ ghost_map_auth γ 1 ( : gmap K V).
Proof.
intros. iMod (ghost_map_alloc_strong P ) as (γ) "(% & Hauth & _)"; eauto.
Qed.
Lemma ghost_map_alloc m :
|==> γ, ghost_map_auth γ 1 m [ map] k v m, k [γ] v.
Proof.
iMod (ghost_map_alloc_strong (λ _, True) m) as (γ) "[_ Hmap]".
- by apply pred_infinite_True.
- eauto.
Qed.
Lemma ghost_map_alloc_empty :
|==> γ, ghost_map_auth γ 1 ( : gmap K V).
Proof.
intros. iMod (ghost_map_alloc ) as (γ) "(Hauth & _)"; eauto.
Qed.
Global Instance ghost_map_auth_timeless γ q m : Timeless (ghost_map_auth γ q m).
Proof. unseal. apply _. Qed.
Global Instance ghost_map_auth_fractional γ m : Fractional (λ q, ghost_map_auth γ q m)%I.
Proof. intros p q. unseal. rewrite -own_op -gmap_view_auth_dfrac_op //. Qed.
Global Instance ghost_map_auth_as_fractional γ q m :
AsFractional (ghost_map_auth γ q m) (λ q, ghost_map_auth γ q m)%I q.
Proof. split; first done. apply _. Qed.
Lemma ghost_map_auth_valid γ q m : ghost_map_auth γ q m -∗ q 1⌝%Qp.
Proof.
unseal. iIntros "Hauth".
iDestruct (own_valid with "Hauth") as %?%gmap_view_auth_dfrac_valid.
done.
Qed.
Lemma ghost_map_auth_valid_2 γ q1 q2 m1 m2 :
ghost_map_auth γ q1 m1 -∗ ghost_map_auth γ q2 m2 -∗ (q1 + q2 1)%Qp m1 = m2⌝.
Proof.
unseal. iIntros "H1 H2".
(* We need to explicitly specify the Inj instances instead of
using inj _ since we need to specify [leibnizO] for [to_agree_inj]. *)
iCombine "H1 H2" gives %[? ?%(map_fmap_equiv_inj _
(to_agree_inj (A:=(leibnizO _))))]%gmap_view_auth_dfrac_op_valid.
iPureIntro. split; first done. by fold_leibniz.
Qed.
Lemma ghost_map_auth_agree γ q1 q2 m1 m2 :
ghost_map_auth γ q1 m1 -∗ ghost_map_auth γ q2 m2 -∗ m1 = m2⌝.
Proof.
iIntros "H1 H2".
iDestruct (ghost_map_auth_valid_2 with "H1 H2") as %[_ ?].
done.
Qed.
(** * Lemmas about the interaction of [ghost_map_auth] with the elements *)
Lemma ghost_map_lookup {γ q m k dq v} :
ghost_map_auth γ q m -∗ k [γ]{dq} v -∗ m !! k = Some v⌝.
Proof.
unseal. iIntros "Hauth Hel".
iCombine "Hauth Hel" gives
%(av' & _ & _ & Hav' & _ & Hincl)%gmap_view_both_dfrac_valid_discrete_total.
iPureIntro.
apply lookup_fmap_Some in Hav' as [v' [<- Hv']].
(* FIXME: Why do we need [(SI:=natSI) (A:=leibnizO V)]
https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/555 seems to resolve
the problem? *)
apply (to_agree_included_L (SI:=natSI) (A:=leibnizO V)) in Hincl.
by rewrite Hincl.
Qed.
Global Instance ghost_map_lookup_combine_gives_1 {γ q m k dq v} :
CombineSepGives (ghost_map_auth γ q m) (k [γ]{dq} v) m !! k = Some v⌝.
Proof.
rewrite /CombineSepGives. iIntros "[H1 H2]".
iDestruct (ghost_map_lookup with "H1 H2") as %->. eauto.
Qed.
Global Instance ghost_map_lookup_combine_gives_2 {γ q m k dq v} :
CombineSepGives (k [γ]{dq} v) (ghost_map_auth γ q m) m !! k = Some v⌝.
Proof.
rewrite /CombineSepGives comm. apply ghost_map_lookup_combine_gives_1.
Qed.
Lemma ghost_map_insert {γ m} k v :
m !! k = None
ghost_map_auth γ 1 m ==∗ ghost_map_auth γ 1 (<[k := v]> m) k [γ] v.
Proof.
unseal. intros Hm. rewrite -own_op.
iApply own_update. rewrite fmap_insert. apply: gmap_view_alloc; [|done..].
rewrite lookup_fmap Hm //.
Qed.
Lemma ghost_map_insert_persist {γ m} k v :
m !! k = None
ghost_map_auth γ 1 m ==∗ ghost_map_auth γ 1 (<[k := v]> m) k [γ] v.
Proof.
iIntros (?) "Hauth".
iMod (ghost_map_insert k with "Hauth") as "[$ Helem]"; first done.
iApply ghost_map_elem_persist. done.
Qed.
Lemma ghost_map_delete {γ m k v} :
ghost_map_auth γ 1 m -∗ k [γ] v ==∗ ghost_map_auth γ 1 (delete k m).
Proof.
unseal. iApply bi.wand_intro_r. rewrite -own_op.
iApply own_update. rewrite fmap_delete. apply: gmap_view_delete.
Qed.
Lemma ghost_map_update {γ m k v} w :
ghost_map_auth γ 1 m -∗ k [γ] v ==∗ ghost_map_auth γ 1 (<[k := w]> m) k [γ] w.
Proof.
unseal. iApply bi.wand_intro_r. rewrite -!own_op.
iApply own_update. rewrite fmap_insert. apply: gmap_view_replace; done.
Qed.
(** Big-op versions of above lemmas *)
Lemma ghost_map_lookup_big {γ q m} m0 :
ghost_map_auth γ q m -∗
([ map] kv m0, k [γ] v) -∗
m0 m⌝.
Proof.
iIntros "Hauth Hfrag". rewrite map_subseteq_spec. iIntros (k v Hm0).
iDestruct (ghost_map_lookup with "Hauth [Hfrag]") as %->.
{ rewrite big_sepM_lookup; done. }
done.
Qed.
Lemma ghost_map_insert_big {γ m} m' :
m' ## m
ghost_map_auth γ 1 m ==∗
ghost_map_auth γ 1 (m' m) ([ map] k v m', k [γ] v).
Proof.
unseal. intros ?. rewrite -big_opM_own_1 -own_op. iApply own_update.
etrans; first apply: (gmap_view_alloc_big _ (to_agree <$> m') (DfracOwn 1)).
- apply map_disjoint_fmap. done.
- done.
- by apply map_Forall_fmap.
- rewrite map_fmap_union big_opM_fmap. done.
Qed.
Lemma ghost_map_insert_persist_big {γ m} m' :
m' ## m
ghost_map_auth γ 1 m ==∗
ghost_map_auth γ 1 (m' m) ([ map] k v m', k [γ] v).
Proof.
iIntros (Hdisj) "Hauth".
iMod (ghost_map_insert_big m' with "Hauth") as "[$ Helem]"; first done.
iApply big_sepM_bupd. iApply (big_sepM_impl with "Helem").
iIntros "!#" (k v) "_". iApply ghost_map_elem_persist.
Qed.
Lemma ghost_map_delete_big {γ m} m0 :
ghost_map_auth γ 1 m -∗
([ map] kv m0, k [γ] v) ==∗
ghost_map_auth γ 1 (m m0).
Proof.
iIntros "Hauth Hfrag". iMod (ghost_map_elems_unseal with "Hfrag") as "Hfrag".
unseal. iApply (own_update_2 with "Hauth Hfrag").
rewrite map_fmap_difference.
etrans; last apply: gmap_view_delete_big.
rewrite big_opM_fmap. done.
Qed.
Theorem ghost_map_update_big {γ m} m0 m1 :
dom m0 = dom m1
ghost_map_auth γ 1 m -∗
([ map] kv m0, k [γ] v) ==∗
ghost_map_auth γ 1 (m1 m)
[ map] kv m1, k [γ] v.
Proof.
iIntros (?) "Hauth Hfrag".
iMod (ghost_map_elems_unseal with "Hfrag") as "Hfrag".
unseal. rewrite -big_opM_own_1 -own_op.
iApply (own_update_2 with "Hauth Hfrag").
rewrite map_fmap_union.
rewrite -!(big_opM_fmap to_agree (λ k, gmap_view_frag k (DfracOwn 1))).
apply: gmap_view_replace_big.
- rewrite !dom_fmap_L. done.
- by apply map_Forall_fmap.
Qed.
End lemmas.
(** A simple "ghost variable" of arbitrary type with fractional ownership.
Can be mutated when fully owned. *)
From iris.algebra Require Import dfrac_agree proofmode_classes frac.
From iris.bi.lib Require Import fractional.
From iris.proofmode Require Import proofmode.
From iris.base_logic.lib Require Export own.
From iris.prelude Require Import options.
(** The CMRA we need. *)
Class ghost_varG Σ (A : Type) := GhostVarG {
#[local] ghost_var_inG :: inG Σ (dfrac_agreeR $ leibnizO A);
}.
Global Hint Mode ghost_varG - ! : typeclass_instances.
Definition ghost_varΣ (A : Type) : gFunctors :=
#[ GFunctor (dfrac_agreeR $ leibnizO A) ].
Global Instance subG_ghost_varΣ Σ A : subG (ghost_varΣ A) Σ ghost_varG Σ A.
Proof. solve_inG. Qed.
Local Definition ghost_var_def `{!ghost_varG Σ A}
(γ : gname) (q : Qp) (a : A) : iProp Σ :=
own γ (to_frac_agree (A:=leibnizO A) q a).
Local Definition ghost_var_aux : seal (@ghost_var_def). Proof. by eexists. Qed.
Definition ghost_var := ghost_var_aux.(unseal).
Local Definition ghost_var_unseal :
@ghost_var = @ghost_var_def := ghost_var_aux.(seal_eq).
Global Arguments ghost_var {Σ A _} γ q a.
Local Ltac unseal := rewrite ?ghost_var_unseal /ghost_var_def.
Section lemmas.
Context `{!ghost_varG Σ A}.
Implicit Types (a b : A) (q : Qp).
Global Instance ghost_var_timeless γ q a : Timeless (ghost_var γ q a).
Proof. unseal. apply _. Qed.
Global Instance ghost_var_fractional γ a : Fractional (λ q, ghost_var γ q a).
Proof. intros q1 q2. unseal. rewrite -own_op -frac_agree_op //. Qed.
Global Instance ghost_var_as_fractional γ a q :
AsFractional (ghost_var γ q a) (λ q, ghost_var γ q a) q.
Proof. split; [done|]. apply _. Qed.
Lemma ghost_var_alloc_strong a (P : gname Prop) :
pred_infinite P
|==> γ, P γ ghost_var γ 1 a.
Proof. unseal. intros. iApply own_alloc_strong; done. Qed.
Lemma ghost_var_alloc a :
|==> γ, ghost_var γ 1 a.
Proof. unseal. iApply own_alloc. done. Qed.
Lemma ghost_var_valid_2 γ a1 q1 a2 q2 :
ghost_var γ q1 a1 -∗ ghost_var γ q2 a2 -∗ (q1 + q2 1)%Qp a1 = a2⌝.
Proof.
unseal. iIntros "Hvar1 Hvar2".
iCombine "Hvar1 Hvar2" gives %[Hq Ha]%frac_agree_op_valid.
done.
Qed.
(** Almost all the time, this is all you really need. *)
Lemma ghost_var_agree γ a1 q1 a2 q2 :
ghost_var γ q1 a1 -∗ ghost_var γ q2 a2 -∗ a1 = a2⌝.
Proof.
iIntros "Hvar1 Hvar2".
iDestruct (ghost_var_valid_2 with "Hvar1 Hvar2") as %[_ ?]. done.
Qed.
Global Instance ghost_var_combine_gives γ a1 q1 a2 q2 :
CombineSepGives (ghost_var γ q1 a1) (ghost_var γ q2 a2)
(q1 + q2 1)%Qp a1 = a2⌝.
Proof.
rewrite /CombineSepGives. iIntros "[H1 H2]".
iDestruct (ghost_var_valid_2 with "H1 H2") as %[H1 H2].
eauto.
Qed.
Global Instance ghost_var_combine_as γ a1 q1 a2 q2 q :
IsOp q q1 q2
CombineSepAs (ghost_var γ q1 a1) (ghost_var γ q2 a2)
(ghost_var γ q a1) | 60.
(* higher cost than the Fractional instance, which is used for a1 = a2 *)
Proof.
rewrite /CombineSepAs /IsOp => ->. iIntros "[H1 H2]".
(* This can't be a single [iCombine] since the instance providing that is
exactly what we are proving here. *)
iCombine "H1 H2" gives %[_ ->].
by iCombine "H1 H2" as "H".
Qed.
(** This is just an instance of fractionality above, but that can be hard to find. *)
Lemma ghost_var_split γ a q1 q2 :
ghost_var γ (q1 + q2) a -∗ ghost_var γ q1 a ghost_var γ q2 a.
Proof. iIntros "[$$]". Qed.
(** Update the ghost variable to new value [b]. *)
Lemma ghost_var_update b γ a :
ghost_var γ 1 a ==∗ ghost_var γ 1 b.
Proof.
unseal. iApply own_update. apply cmra_update_exclusive. done.
Qed.
Lemma ghost_var_update_2 b γ a1 q1 a2 q2 :
(q1 + q2 = 1)%Qp
ghost_var γ q1 a1 -∗ ghost_var γ q2 a2 ==∗ ghost_var γ q1 b ghost_var γ q2 b.
Proof.
intros Hq. unseal. rewrite -own_op. iApply own_update_2.
apply frac_agree_update_2. done.
Qed.
Lemma ghost_var_update_halves b γ a1 a2 :
ghost_var γ (1/2) a1 -∗
ghost_var γ (1/2) a2 ==∗
ghost_var γ (1/2) b ghost_var γ (1/2) b.
Proof. iApply ghost_var_update_2. apply Qp.half_half. Qed.
(** Framing support *)
Global Instance frame_ghost_var p γ a q1 q2 q :
FrameFractionalQp q1 q2 q
Frame p (ghost_var γ q1 a) (ghost_var γ q2 a) (ghost_var γ q a) | 5.
Proof. apply: frame_fractional. Qed.
End lemmas.
(** Propositions for reasoning about monotone partial bijections.
This library provides two propositions [gset_bij_own_auth γ L] and
[gset_bij_own_elem γ a b], where [L] is a bijection between types [A] and [B]
represented by a set of associations [gset (A * B)]. The idea is that
[gset_bij_own_auth γ L] is an authoritative bijection [L], while
[gset_bij_own_elem γ a b] is a persistent resource saying [L] associates [a]
and [b].
The main use case is in a logical relation-based proof where [L] maintains the
association between locations [A] in one execution and [B] in another (perhaps
of different types, if the logical relation relates two different semantics).
The association [L] is always bijective, so that if [a] is mapped to [b], there
should be no other mappings for either [a] or [b]; the [gset_bij_own_extend]
update theorem enforces that new mappings respect this property, and
[gset_bij_own_elem_agree] allows the user to exploit bijectivity. The bijection
grows monotonically, so that the set of associations only grows; this is
captured by the persistence of [gset_bij_own_elem].
This library is a logical, ownership-based wrapper around [gset_bij]. *)
From iris.algebra.lib Require Import gset_bij.
From iris.bi.lib Require Import fractional.
From iris.base_logic.lib Require Import own.
From iris.proofmode Require Import proofmode.
From iris.prelude Require Import options.
(* The uCMRA we need. *)
Class gset_bijG Σ A B `{Countable A, Countable B} :=
GsetBijG { #[local] gset_bijG_inG :: inG Σ (gset_bijR A B); }.
Global Hint Mode gset_bijG - ! ! - - - - : typeclass_instances.
Definition gset_bijΣ A B `{Countable A, Countable B}: gFunctors :=
#[ GFunctor (gset_bijR A B) ].
Global Instance subG_gset_bijΣ `{Countable A, Countable B} Σ :
subG (gset_bijΣ A B) Σ gset_bijG Σ A B.
Proof. solve_inG. Qed.
Definition gset_bij_own_auth_def `{gset_bijG Σ A B} (γ : gname)
(dq : dfrac) (L : gset (A * B)) : iProp Σ :=
own γ (gset_bij_auth dq L).
Definition gset_bij_own_auth_aux : seal (@gset_bij_own_auth_def). Proof. by eexists. Qed.
Definition gset_bij_own_auth := unseal gset_bij_own_auth_aux.
Definition gset_bij_own_auth_eq :
@gset_bij_own_auth = @gset_bij_own_auth_def := seal_eq gset_bij_own_auth_aux.
Global Arguments gset_bij_own_auth {_ _ _ _ _ _ _ _}.
Definition gset_bij_own_elem_def `{gset_bijG Σ A B} (γ : gname)
(a : A) (b : B) : iProp Σ := own γ (gset_bij_elem a b).
Definition gset_bij_own_elem_aux : seal (@gset_bij_own_elem_def). Proof. by eexists. Qed.
Definition gset_bij_own_elem := unseal gset_bij_own_elem_aux.
Definition gset_bij_own_elem_eq :
@gset_bij_own_elem = @gset_bij_own_elem_def := seal_eq gset_bij_own_elem_aux.
Global Arguments gset_bij_own_elem {_ _ _ _ _ _ _ _}.
Section gset_bij.
Context `{gset_bijG Σ A B}.
Implicit Types (L : gset (A * B)) (a : A) (b : B).
Global Instance gset_bij_own_auth_timeless γ q L :
Timeless (gset_bij_own_auth γ q L).
Proof. rewrite gset_bij_own_auth_eq. apply _. Qed.
Global Instance gset_bij_own_elem_timeless γ a b :
Timeless (gset_bij_own_elem γ a b).
Proof. rewrite gset_bij_own_elem_eq. apply _. Qed.
Global Instance gset_bij_own_elem_persistent γ a b :
Persistent (gset_bij_own_elem γ a b).
Proof. rewrite gset_bij_own_elem_eq. apply _. Qed.
Global Instance gset_bij_own_auth_fractional γ L :
Fractional (λ q, gset_bij_own_auth γ (DfracOwn q) L).
Proof.
intros p q. rewrite gset_bij_own_auth_eq -own_op gset_bij_auth_dfrac_op //.
Qed.
Global Instance gset_bij_own_auth_as_fractional γ q L :
AsFractional (gset_bij_own_auth γ (DfracOwn q) L) (λ q, gset_bij_own_auth γ (DfracOwn q) L) q.
Proof. split; [auto|apply _]. Qed.
Lemma gset_bij_own_auth_agree γ dq1 dq2 L1 L2 :
gset_bij_own_auth γ dq1 L1 -∗ gset_bij_own_auth γ dq2 L2 -∗
⌜✓ (dq1 dq2) L1 = L2 gset_bijective L1⌝.
Proof.
rewrite gset_bij_own_auth_eq. iIntros "H1 H2".
by iCombine "H1 H2" gives %?%gset_bij_auth_dfrac_op_valid.
Qed.
Lemma gset_bij_own_auth_exclusive γ L1 L2 :
gset_bij_own_auth γ (DfracOwn 1) L1 -∗ gset_bij_own_auth γ (DfracOwn 1) L2 -∗ False.
Proof.
iIntros "H1 H2".
by iDestruct (gset_bij_own_auth_agree with "H1 H2") as %[[] _].
Qed.
Lemma gset_bij_own_valid γ q L :
gset_bij_own_auth γ q L -∗ ⌜✓ q gset_bijective L⌝.
Proof.
rewrite gset_bij_own_auth_eq. iIntros "Hauth".
by iDestruct (own_valid with "Hauth") as %?%gset_bij_auth_dfrac_valid.
Qed.
Lemma gset_bij_own_elem_agree γ a a' b b' :
gset_bij_own_elem γ a b -∗ gset_bij_own_elem γ a' b' -∗
a = a' b = b'⌝.
Proof.
rewrite gset_bij_own_elem_eq. iIntros "Hel1 Hel2".
by iCombine "Hel1 Hel2" gives %?%gset_bij_elem_agree.
Qed.
Lemma gset_bij_own_elem_get {γ q L} a b :
(a, b) L
gset_bij_own_auth γ q L -∗ gset_bij_own_elem γ a b.
Proof.
intros. rewrite gset_bij_own_auth_eq gset_bij_own_elem_eq.
iApply own_mono. by apply bij_view_included.
Qed.
Lemma gset_bij_elem_of {γ q L} a b :
gset_bij_own_auth γ q L -∗ gset_bij_own_elem γ a b -∗ (a, b) L⌝.
Proof.
iIntros "Hauth Helem". rewrite gset_bij_own_auth_eq gset_bij_own_elem_eq.
iCombine "Hauth Helem" gives "%Ha".
iPureIntro. revert Ha. rewrite bij_both_dfrac_valid. intros (_ & _ & ?); done.
Qed.
Lemma gset_bij_own_elem_get_big γ q L :
gset_bij_own_auth γ q L -∗ [ set] ab L, gset_bij_own_elem γ ab.1 ab.2.
Proof.
iIntros "Hauth". iApply big_sepS_forall. iIntros ([a b] ?) "/=".
by iApply gset_bij_own_elem_get.
Qed.
Lemma gset_bij_own_alloc L :
gset_bijective L
|==> γ, gset_bij_own_auth γ (DfracOwn 1) L [ set] ab L, gset_bij_own_elem γ ab.1 ab.2.
Proof.
intro. iAssert ( γ, gset_bij_own_auth γ (DfracOwn 1) L)%I with "[>]" as (γ) "Hauth".
{ rewrite gset_bij_own_auth_eq. iApply own_alloc. by apply gset_bij_auth_valid. }
iExists γ. iModIntro. iSplit; [done|].
by iApply gset_bij_own_elem_get_big.
Qed.
Lemma gset_bij_own_alloc_empty :
|==> γ, gset_bij_own_auth γ (DfracOwn 1) ( : gset (A * B)).
Proof. iMod (gset_bij_own_alloc ) as (γ) "[Hauth _]"; by auto. Qed.
Lemma gset_bij_own_extend {γ L} a b :
( b', (a, b') L) ( a', (a', b) L)
gset_bij_own_auth γ (DfracOwn 1) L ==∗
gset_bij_own_auth γ (DfracOwn 1) ({[(a, b)]} L) gset_bij_own_elem γ a b.
Proof.
iIntros (??) "Hauth".
iAssert (gset_bij_own_auth γ (DfracOwn 1) ({[(a, b)]} L)) with "[> Hauth]" as "Hauth".
{ rewrite gset_bij_own_auth_eq. iApply (own_update with "Hauth").
by apply gset_bij_auth_extend. }
iModIntro. iSplit; [done|].
iApply (gset_bij_own_elem_get with "Hauth"). set_solver.
Qed.
Lemma gset_bij_own_extend_internal {γ L} a b :
( b', gset_bij_own_elem γ a b' -∗ False) -∗
( a', gset_bij_own_elem γ a' b -∗ False) -∗
gset_bij_own_auth γ (DfracOwn 1) L ==∗
gset_bij_own_auth γ (DfracOwn 1) ({[(a, b)]} L) gset_bij_own_elem γ a b.
Proof.
iIntros "Ha Hb HL".
iAssert ⌜∀ b', (a, b') L⌝%I as %?.
{ iIntros (b' ?). iApply ("Ha" $! b'). by iApply gset_bij_own_elem_get. }
iAssert ⌜∀ a', (a', b) L⌝%I as %?.
{ iIntros (a' ?). iApply ("Hb" $! a'). by iApply gset_bij_own_elem_get. }
by iApply (gset_bij_own_extend with "HL").
Qed.
End gset_bij.
From stdpp Require Export namespaces.
From iris.algebra Require Import gmap.
From iris.proofmode Require Import proofmode.
From iris.base_logic.lib Require Export fancy_updates.
From iris.base_logic.lib Require Import wsat.
From iris.prelude Require Import options.
Import le_upd_if.
(** Semantic Invariants *)
Local Definition inv_def `{!invGS_gen hlc Σ} (N : namespace) (P : iProp Σ) : iProp Σ :=
E, ⌜↑N E |={E,E N}=> P ( P ={E N,E}=∗ True).
Local Definition inv_aux : seal (@inv_def). Proof. by eexists. Qed.
Definition inv := inv_aux.(unseal).
Global Arguments inv {hlc Σ _} N P.
Local Definition inv_unseal : @inv = @inv_def := inv_aux.(seal_eq).
Global Instance: Params (@inv) 3 := {}.
(** * Invariants *)
Section inv.
Context `{!invGS_gen hlc Σ}.
Implicit Types i : positive.
Implicit Types N : namespace.
Implicit Types E : coPset.
Implicit Types P Q R : iProp Σ.
(** ** Internal model of invariants *)
Definition own_inv (N : namespace) (P : iProp Σ) : iProp Σ :=
i, i (N:coPset) ownI i P.
Lemma own_inv_acc E N P :
N E own_inv N P ={E,E∖↑N}=∗ P ( P ={E∖↑N,E}=∗ True).
Proof.
rewrite fancy_updates.uPred_fupd_unseal /fancy_updates.uPred_fupd_def.
iDestruct 1 as (i) "[Hi #HiP]".
iDestruct "Hi" as % ?%elem_of_subseteq_singleton.
rewrite {1 4}(union_difference_L ( N) E) // ownE_op; last set_solver.
rewrite {1 5}(union_difference_L {[ i ]} ( N)) // ownE_op; last set_solver.
iIntros "(Hw & [HE $] & $) !> !>".
iDestruct (ownI_open i with "[$Hw $HE $HiP]") as "($ & $ & HD)".
iIntros "HP [Hw $] !> !>". iApply (ownI_close _ P). by iFrame.
Qed.
Lemma fresh_inv_name (E : gset positive) N : i, i E i (N:coPset).
Proof.
exists (coPpick ( N gset_to_coPset E)).
rewrite -elem_of_gset_to_coPset (comm and) -elem_of_difference.
apply coPpick_elem_of=> Hfin.
eapply nclose_infinite, (difference_finite_inv _ _), Hfin.
apply gset_to_coPset_finite.
Qed.
Lemma own_inv_alloc N E P : P ={E}=∗ own_inv N P.
Proof.
rewrite fancy_updates.uPred_fupd_unseal /fancy_updates.uPred_fupd_def.
iIntros "HP [Hw $]".
iMod (ownI_alloc (. (N : coPset)) P with "[$HP $Hw]")
as (i ?) "[$ ?]"; auto using fresh_inv_name.
do 2 iModIntro. iExists i. auto.
Qed.
(* This does not imply [own_inv_alloc] due to the extra assumption [↑N ⊆ E]. *)
Lemma own_inv_alloc_open N E P :
N E |={E, E∖↑N}=> own_inv N P (P ={E∖↑N, E}=∗ True).
Proof.
rewrite fancy_updates.uPred_fupd_unseal /fancy_updates.uPred_fupd_def.
iIntros (Sub) "[Hw HE]".
iMod (ownI_alloc_open (. (N : coPset)) P with "Hw")
as (i ?) "(Hw & #Hi & HD)"; auto using fresh_inv_name.
iAssert (ownE {[i]} ownE ( N {[i]}) ownE (E N))%I
with "[HE]" as "(HEi & HEN\i & HE\N)".
{ rewrite -?ownE_op; [|set_solver..].
rewrite assoc_L -!union_difference_L //. set_solver. }
do 2 iModIntro. iFrame "HE\N". iSplitL "Hw HEi"; first by iApply "Hw".
iSplitL "Hi".
{ iExists i. auto. }
iIntros "HP [Hw HE\N]".
iDestruct (ownI_close with "[$Hw $Hi $HP $HD]") as "[$ HEi]".
do 2 iModIntro. iSplitL; [|done].
iCombine "HEi HEN\i HE\N" as "HEN".
rewrite -?ownE_op; [|set_solver..].
rewrite assoc_L -!union_difference_L //; set_solver.
Qed.
Lemma own_inv_to_inv M P: own_inv M P -∗ inv M P.
Proof.
iIntros "#I". rewrite inv_unseal. iIntros (E H).
iPoseProof (own_inv_acc with "I") as "H"; eauto.
Qed.
(** ** Public API of invariants *)
Global Instance inv_contractive N : Contractive (inv N).
Proof. rewrite inv_unseal. solve_contractive. Qed.
Global Instance inv_ne N : NonExpansive (inv N).
Proof. apply contractive_ne, _. Qed.
Global Instance inv_proper N : Proper (equiv ==> equiv) (inv N).
Proof. apply ne_proper, _. Qed.
Global Instance inv_persistent N P : Persistent (inv N P).
Proof. rewrite inv_unseal. apply _. Qed.
Lemma inv_alter N P Q : inv N P -∗ (P -∗ Q (Q -∗ P)) -∗ inv N Q.
Proof.
rewrite inv_unseal. iIntros "#HI #HPQ !>" (E H).
iMod ("HI" $! E H) as "[HP Hclose]".
iDestruct ("HPQ" with "HP") as "[$ HQP]".
iIntros "!> HQ". iApply "Hclose". iApply "HQP". done.
Qed.
Lemma inv_iff N P Q : inv N P -∗ (P Q) -∗ inv N Q.
Proof.
iIntros "#HI #HPQ". iApply (inv_alter with "HI").
iIntros "!> !> HP". iSplitL "HP".
- by iApply "HPQ".
- iIntros "HQ". by iApply "HPQ".
Qed.
Lemma inv_alloc N E P : P ={E}=∗ inv N P.
Proof.
iIntros "HP". iApply own_inv_to_inv.
iApply (own_inv_alloc N E with "HP").
Qed.
Lemma inv_alloc_open N E P :
N E |={E, E∖↑N}=> inv N P (P ={E∖↑N, E}=∗ True).
Proof.
iIntros (?). iMod own_inv_alloc_open as "[HI $]"; first done.
iApply own_inv_to_inv. done.
Qed.
Lemma inv_acc E N P :
N E inv N P ={E,E∖↑N}=∗ P ( P ={E∖↑N,E}=∗ True).
Proof.
rewrite inv_unseal /inv_def; iIntros (?) "#HI". by iApply "HI".
Qed.
Lemma inv_combine N1 N2 N P Q :
N1 ## N2
N1 N2 ⊆@{coPset} N
inv N1 P -∗ inv N2 Q -∗ inv N (P Q).
Proof.
rewrite inv_unseal. iIntros (??) "#HinvP #HinvQ !>"; iIntros (E ?).
iMod ("HinvP" with "[%]") as "[$ HcloseP]"; first set_solver.
iMod ("HinvQ" with "[%]") as "[$ HcloseQ]"; first set_solver.
iApply fupd_mask_intro; first set_solver.
iIntros "Hclose [HP HQ]".
iMod "Hclose" as % _. iMod ("HcloseQ" with "HQ") as % _. by iApply "HcloseP".
Qed.
Lemma inv_combine_dup_l N P Q :
(P -∗ P P) -∗
inv N P -∗ inv N Q -∗ inv N (P Q).
Proof.
rewrite inv_unseal. iIntros "#HPdup #HinvP #HinvQ !>" (E ?).
iMod ("HinvP" with "[//]") as "[HP HcloseP]".
iDestruct ("HPdup" with "HP") as "[$ HP]".
iMod ("HcloseP" with "HP") as % _.
iMod ("HinvQ" with "[//]") as "[$ HcloseQ]".
iIntros "!> [HP HQ]". by iApply "HcloseQ".
Qed.
Lemma except_0_inv N P : inv N P inv N P.
Proof.
rewrite inv_unseal /inv_def. iIntros "#H !>" (E ?).
iMod "H". by iApply "H".
Qed.
(** ** Proof mode integration *)
Global Instance is_except_0_inv N P : IsExcept0 (inv N P).
Proof. apply except_0_inv. Qed.
Global Instance into_inv_inv N P : IntoInv (inv N P) N := {}.
Global Instance into_acc_inv N P E:
IntoAcc (X := unit) (inv N P)
(N E) True (fupd E (E N)) (fupd (E N) E)
(λ _ : (), ( P)%I) (λ _ : (), ( P)%I) (λ _ : (), None).
Proof.
rewrite /IntoAcc /accessor bi.exist_unit.
iIntros (?) "#Hinv _". by iApply inv_acc.
Qed.
(** ** Derived properties *)
Lemma inv_acc_strong E N P :
N E inv N P ={E,E∖↑N}=∗ P E', P ={E',N E'}=∗ True.
Proof.
iIntros (?) "Hinv".
iPoseProof (inv_acc ( N) N with "Hinv") as "H"; first done.
rewrite difference_diag_L.
iPoseProof (fupd_mask_frame_r _ _ (E N) with "H") as "H"; first set_solver.
rewrite left_id_L -union_difference_L //. iMod "H" as "[$ H]"; iModIntro.
iIntros (E') "HP".
iPoseProof (fupd_mask_frame_r _ _ E' with "(H HP)") as "H"; first set_solver.
by rewrite left_id_L.
Qed.
Lemma inv_acc_timeless E N P `{!Timeless P} :
N E inv N P ={E,E∖↑N}=∗ P (P ={E∖↑N,E}=∗ True).
Proof.
iIntros (?) "Hinv". iMod (inv_acc with "Hinv") as "[>HP Hclose]"; auto.
iIntros "!> {$HP} HP". iApply "Hclose"; auto.
Qed.
Lemma inv_split_l N P Q : inv N (P Q) -∗ inv N P.
Proof.
iIntros "#HI". iApply inv_alter; eauto.
iIntros "!> !> [$ $] $".
Qed.
Lemma inv_split_r N P Q : inv N (P Q) -∗ inv N Q.
Proof.
rewrite (comm _ P Q). eapply inv_split_l.
Qed.
Lemma inv_split N P Q : inv N (P Q) -∗ inv N P inv N Q.
Proof.
iIntros "#H".
iPoseProof (inv_split_l with "H") as "$".
iPoseProof (inv_split_r with "H") as "$".
Qed.
End inv.
From iris.base_logic Require Export base_logic. From iris.algebra Require Import gmap.
From iris.algebra Require Import iprod gmap.
From iris.algebra Require cofe_solver. From iris.algebra Require cofe_solver.
Set Default Proof Using "Type". From iris.base_logic Require Export base_logic.
From iris.prelude Require Import options.
(** In this file we construct the type [iProp] of propositions of the Iris (** In this file we construct the type [iProp] of propositions of the Iris
logic. This is done by solving the following recursive domain equation: logic. This is done by solving the following recursive domain equation:
...@@ -26,41 +26,48 @@ the agreement CMRA. *) ...@@ -26,41 +26,48 @@ the agreement CMRA. *)
category of CMRAs with a proof that it is locally contractive. *) category of CMRAs with a proof that it is locally contractive. *)
Structure gFunctor := GFunctor { Structure gFunctor := GFunctor {
gFunctor_F :> rFunctor; gFunctor_F :> rFunctor;
gFunctor_contractive : rFunctorContractive gFunctor_F; gFunctor_map_contractive : rFunctorContractive gFunctor_F;
}. }.
Arguments GFunctor _ {_}. Global Arguments GFunctor _ {_}.
Existing Instance gFunctor_contractive. Global Existing Instance gFunctor_map_contractive.
Add Printing Constructor gFunctor.
(** The type [gFunctors] describes the parameters [Σ] of the Iris logic: lists (** The type [gFunctors] describes the parameters [Σ] of the Iris logic: lists
of [gFunctor]s. of [gFunctor]s.
Note that [gFunctors] is isomorphic to [list gFunctor], but defined in an Note that [gFunctors] is isomorphic to [list gFunctor], but defined in an
alternative way to avoid universe inconsistencies with respect to the universe alternative way to avoid universe inconsistencies with respect to the universe
monomorphic [list] type. *) monomorphic [list] type.
Definition gFunctors := { n : nat & fin n gFunctor }.
Defining [gFunctors] as a dependent record instead of a [sigT] avoids other
universe inconsistencies. *)
Record gFunctors := GFunctors {
gFunctors_len : nat;
gFunctors_lookup : fin gFunctors_len gFunctor
}.
Definition gid (Σ : gFunctors) := fin (projT1 Σ). Definition gid (Σ : gFunctors) := fin (gFunctors_len Σ).
Definition gFunctors_lookup (Σ : gFunctors) : gid Σ gFunctor := projT2 Σ.
Coercion gFunctors_lookup : gFunctors >-> Funclass.
Definition gname := positive. Definition gname := positive.
Canonical Structure gnameO := leibnizO gname.
(** The resources functor [iResF Σ A := ∀ i : gid, gname -fin-> (Σ i) A]. *) (** The resources functor [iResF Σ A := ∀ i : gid, gname -fin-> (Σ i) A]. *)
Definition iResF (Σ : gFunctors) : urFunctor := Definition iResF (Σ : gFunctors) : urFunctor :=
iprodURF (λ i, gmapURF gname (Σ i)). discrete_funURF (λ i, gmapURF gname (gFunctors_lookup Σ i)).
(** We define functions for the empty list of functors, the singleton list of (** We define functions for the empty list of functors, the singleton list of
functors, and the append operator on lists of functors. These are used to functors, and the append operator on lists of functors. These are used to
compose [gFunctors] out of smaller pieces. *) compose [gFunctors] out of smaller pieces. *)
Module gFunctors. Module gFunctors.
Definition nil : gFunctors := existT 0 (fin_0_inv _). Definition nil : gFunctors := GFunctors 0 (fin_0_inv _).
Definition singleton (F : gFunctor) : gFunctors := Definition singleton (F : gFunctor) : gFunctors :=
existT 1 (fin_S_inv (λ _, gFunctor) F (fin_0_inv _)). GFunctors 1 (fin_S_inv (λ _, gFunctor) F (fin_0_inv _)).
Definition app (Σ1 Σ2 : gFunctors) : gFunctors := Definition app (Σ1 Σ2 : gFunctors) : gFunctors :=
existT (projT1 Σ1 + projT1 Σ2) (fin_plus_inv _ (projT2 Σ1) (projT2 Σ2)). GFunctors (gFunctors_len Σ1 + gFunctors_len Σ2)
(fin_add_inv _ (gFunctors_lookup Σ1) (gFunctors_lookup Σ2)).
End gFunctors. End gFunctors.
Coercion gFunctors.singleton : gFunctor >-> gFunctors. Coercion gFunctors.singleton : gFunctor >-> gFunctors.
...@@ -79,33 +86,34 @@ lock invariant. ...@@ -79,33 +86,34 @@ lock invariant.
The contraints to can be expressed using the type class [subG Σ1 Σ2], which The contraints to can be expressed using the type class [subG Σ1 Σ2], which
expresses that the functors [Σ1] are contained in [Σ2]. *) expresses that the functors [Σ1] are contained in [Σ2]. *)
Class subG (Σ1 Σ2 : gFunctors) := in_subG i : { j | Σ1 i = Σ2 j }. Class subG (Σ1 Σ2 : gFunctors) := in_subG i :
{ j | gFunctors_lookup Σ1 i = gFunctors_lookup Σ2 j }.
(** Avoid trigger happy type class search: this line ensures that type class (** Avoid trigger happy type class search: this line ensures that type class
search is only triggered if the arguments of [subG] do not contain evars. Since search is only triggered if the arguments of [subG] do not contain evars. Since
instance search for [subG] is restrained, instances should always have [subG] as instance search for [subG] is restrained, instances should persistently have [subG] as
their first parameter to avoid loops. For example, the instances [subG_authΣ] their first parameter to avoid loops. For example, the instances [subG_authΣ]
and [auth_discrete] otherwise create a cycle that pops up arbitrarily. *) and [auth_discrete] otherwise create a cycle that pops up arbitrarily. *)
Hint Mode subG + + : typeclass_instances. Global Hint Mode subG ! + : typeclass_instances.
Lemma subG_inv Σ1 Σ2 Σ : subG (gFunctors.app Σ1 Σ2) Σ subG Σ1 Σ * subG Σ2 Σ. Lemma subG_inv Σ1 Σ2 Σ : subG (gFunctors.app Σ1 Σ2) Σ subG Σ1 Σ * subG Σ2 Σ.
Proof. Proof.
move=> H; split. move=> H; split.
- move=> i; move: H=> /(_ (Fin.L _ i)) [j] /=. rewrite fin_plus_inv_L; eauto. - move=> i; move: H=> /(_ (Fin.L _ i)) [j] /=. rewrite fin_add_inv_l; eauto.
- move=> i; move: H=> /(_ (Fin.R _ i)) [j] /=. rewrite fin_plus_inv_R; eauto. - move=> i; move: H=> /(_ (Fin.R _ i)) [j] /=. rewrite fin_add_inv_r; eauto.
Qed. Qed.
Instance subG_refl Σ : subG Σ Σ. Global Instance subG_refl Σ : subG Σ Σ.
Proof. move=> i; by exists i. Qed. Proof. move=> i; by exists i. Qed.
Instance subG_app_l Σ Σ1 Σ2 : subG Σ Σ1 subG Σ (gFunctors.app Σ1 Σ2). Global Instance subG_app_l Σ Σ1 Σ2 : subG Σ Σ1 subG Σ (gFunctors.app Σ1 Σ2).
Proof. Proof.
move=> H i; move: H=> /(_ i) [j ?]. move=> H i; move: H=> /(_ i) [j ?].
exists (Fin.L _ j). by rewrite /= fin_plus_inv_L. exists (Fin.L _ j). by rewrite /= fin_add_inv_l.
Qed. Qed.
Instance subG_app_r Σ Σ1 Σ2 : subG Σ Σ2 subG Σ (gFunctors.app Σ1 Σ2). Global Instance subG_app_r Σ Σ1 Σ2 : subG Σ Σ2 subG Σ (gFunctors.app Σ1 Σ2).
Proof. Proof.
move=> H i; move: H=> /(_ i) [j ?]. move=> H i; move: H=> /(_ i) [j ?].
exists (Fin.R _ j). by rewrite /= fin_plus_inv_R. exists (Fin.R _ j). by rewrite /= fin_add_inv_r.
Qed. Qed.
...@@ -114,44 +122,51 @@ Qed. ...@@ -114,44 +122,51 @@ Qed.
the construction, this way we are sure we do not use any properties of the the construction, this way we are sure we do not use any properties of the
construction, and also avoid Coq from blindly unfolding it. *) construction, and also avoid Coq from blindly unfolding it. *)
Module Type iProp_solution_sig. Module Type iProp_solution_sig.
Parameter iPreProp : gFunctors ofeT. Parameter iPrePropO : gFunctors ofe.
Definition iResUR (Σ : gFunctors) : ucmraT := Global Declare Instance iPreProp_cofe {Σ} : Cofe (iPrePropO Σ).
iprodUR (λ i, gmapUR gname (Σ i (iPreProp Σ))).
Notation iProp Σ := (uPredC (iResUR Σ)). Definition iResUR (Σ : gFunctors) : ucmra :=
discrete_funUR (λ i,
Parameter iProp_unfold: {Σ}, iProp Σ -n> iPreProp Σ. gmapUR gname (rFunctor_apply (gFunctors_lookup Σ i) (iPrePropO Σ))).
Parameter iProp_fold: {Σ}, iPreProp Σ -n> iProp Σ. Notation iProp Σ := (uPred (iResUR Σ)).
Notation iPropO Σ := (uPredO (iResUR Σ)).
Notation iPropI Σ := (uPredI (iResUR Σ)).
Parameter iProp_unfold: {Σ}, iPropO Σ -n> iPrePropO Σ.
Parameter iProp_fold: {Σ}, iPrePropO Σ -n> iPropO Σ.
Parameter iProp_fold_unfold: {Σ} (P : iProp Σ), Parameter iProp_fold_unfold: {Σ} (P : iProp Σ),
iProp_fold (iProp_unfold P) P. iProp_fold (iProp_unfold P) P.
Parameter iProp_unfold_fold: {Σ} (P : iPreProp Σ), Parameter iProp_unfold_fold: {Σ} (P : iPrePropO Σ),
iProp_unfold (iProp_fold P) P. iProp_unfold (iProp_fold P) P.
End iProp_solution_sig. End iProp_solution_sig.
Module Export iProp_solution : iProp_solution_sig. Module Export iProp_solution : iProp_solution_sig.
Import cofe_solver. Import cofe_solver.
Definition iProp_result (Σ : gFunctors) : Definition iProp_result (Σ : gFunctors) :
solution (uPredCF (iResF Σ)) := solver.result _. solution (uPredOF (iResF Σ)) := solver.result _.
Definition iPrePropO (Σ : gFunctors) : ofe := iProp_result Σ.
Definition iPreProp (Σ : gFunctors) : ofeT := iProp_result Σ. Global Instance iPreProp_cofe {Σ} : Cofe (iPrePropO Σ) := _.
Definition iResUR (Σ : gFunctors) : ucmraT :=
iprodUR (λ i, gmapUR gname (Σ i (iPreProp Σ))). Definition iResUR (Σ : gFunctors) : ucmra :=
Notation iProp Σ := (uPredC (iResUR Σ)). discrete_funUR (λ i,
gmapUR gname (rFunctor_apply (gFunctors_lookup Σ i) (iPrePropO Σ))).
Definition iProp_unfold {Σ} : iProp Σ -n> iPreProp Σ := Notation iProp Σ := (uPred (iResUR Σ)).
solution_fold (iProp_result Σ). Notation iPropO Σ := (uPredO (iResUR Σ)).
Definition iProp_fold {Σ} : iPreProp Σ -n> iProp Σ := solution_unfold _.
Definition iProp_unfold {Σ} : iPropO Σ -n> iPrePropO Σ :=
ofe_iso_1 (iProp_result Σ).
Definition iProp_fold {Σ} : iPrePropO Σ -n> iPropO Σ :=
ofe_iso_2 (iProp_result Σ).
Lemma iProp_fold_unfold {Σ} (P : iProp Σ) : iProp_fold (iProp_unfold P) P. Lemma iProp_fold_unfold {Σ} (P : iProp Σ) : iProp_fold (iProp_unfold P) P.
Proof. apply solution_unfold_fold. Qed. Proof. apply ofe_iso_21. Qed.
Lemma iProp_unfold_fold {Σ} (P : iPreProp Σ) : iProp_unfold (iProp_fold P) P. Lemma iProp_unfold_fold {Σ} (P : iPrePropO Σ) : iProp_unfold (iProp_fold P) P.
Proof. apply solution_fold_unfold. Qed. Proof. apply ofe_iso_12. Qed.
End iProp_solution. End iProp_solution.
(** * Properties of the solution to the recursive domain equation *) (** * Properties of the solution to the recursive domain equation *)
Lemma iProp_unfold_equivI {Σ} (P Q : iProp Σ) : Lemma iProp_unfold_equivI {Σ} (P Q : iProp Σ) :
iProp_unfold P iProp_unfold Q (P Q : iProp Σ). iProp_unfold P iProp_unfold Q @{iPropI Σ} P Q.
Proof. Proof.
rewrite -{2}(iProp_fold_unfold P) -{2}(iProp_fold_unfold Q). rewrite -{2}(iProp_fold_unfold P) -{2}(iProp_fold_unfold Q). apply: f_equivI.
eapply (uPred.internal_eq_rewrite _ _ (λ z,
iProp_fold (iProp_unfold P) iProp_fold z))%I; auto with I; solve_proper.
Qed. Qed.
(** This file implements later credits, in particular the later-elimination update.
That update is used internally to define the Iris [fupd]; it should not
usually be directly used unless you are defining your own [fupd]. *)
From iris.prelude Require Import options.
From iris.proofmode Require Import tactics.
From iris.algebra Require Export auth numbers.
From iris.base_logic.lib Require Import iprop own.
Import uPred.
(** The ghost state for later credits *)
Class lcGpreS (Σ : gFunctors) := LcGpreS {
#[local] lcGpreS_inG :: inG Σ (authR natUR)
}.
Class lcGS (Σ : gFunctors) := LcGS {
#[local] lcGS_inG :: inG Σ (authR natUR);
lcGS_name : gname;
}.
Global Hint Mode lcGS - : typeclass_instances.
Definition lcΣ := #[GFunctor (authR (natUR))].
Global Instance subG_lcΣ {Σ} : subG lcΣ Σ lcGpreS Σ.
Proof. solve_inG. Qed.
(** The user-facing credit resource, denoting ownership of [n] credits. *)
Local Definition lc_def `{!lcGS Σ} (n : nat) : iProp Σ := own lcGS_name ( n).
Local Definition lc_aux : seal (@lc_def). Proof. by eexists. Qed.
Definition lc := lc_aux.(unseal).
Local Definition lc_unseal :
@lc = @lc_def := lc_aux.(seal_eq).
Global Arguments lc {Σ _} n.
Notation "'£' n" := (lc n) (at level 1).
(** The internal authoritative part of the credit ghost state,
tracking how many credits are available in total.
Users should not directly interface with this. *)
Local Definition lc_supply_def `{!lcGS Σ} (n : nat) : iProp Σ := own lcGS_name ( n).
Local Definition lc_supply_aux : seal (@lc_supply_def). Proof. by eexists. Qed.
Local Definition lc_supply := lc_supply_aux.(unseal).
Local Definition lc_supply_unseal :
@lc_supply = @lc_supply_def := lc_supply_aux.(seal_eq).
Global Arguments lc_supply {Σ _} n.
Section later_credit_theory.
Context `{!lcGS Σ}.
Implicit Types (P Q : iProp Σ).
(** Later credit rules *)
Lemma lc_split n m :
£ (n + m) ⊣⊢ £ n £ m.
Proof.
rewrite lc_unseal /lc_def.
rewrite -own_op auth_frag_op //=.
Qed.
Lemma lc_zero : |==> £ 0.
Proof.
rewrite lc_unseal /lc_def. iApply own_unit.
Qed.
Lemma lc_supply_bound n m :
lc_supply m -∗ £ n -∗ n m⌝.
Proof.
rewrite lc_unseal /lc_def.
rewrite lc_supply_unseal /lc_supply_def.
iIntros "H1 H2".
iCombine "H1 H2" gives %Hop.
iPureIntro. eapply auth_both_valid_discrete in Hop as [Hlt _].
by eapply nat_included.
Qed.
Lemma lc_decrease_supply n m :
lc_supply (n + m) -∗ £ n -∗ |==> lc_supply m.
Proof.
rewrite lc_unseal /lc_def.
rewrite lc_supply_unseal /lc_supply_def.
iIntros "H1 H2".
iMod (own_update_2 with "H1 H2") as "Hown".
{ eapply auth_update. eapply (nat_local_update _ _ m 0). lia. }
by iDestruct "Hown" as "[Hm _]".
Qed.
Lemma lc_succ n :
£ (S n) ⊣⊢ £ 1 £ n.
Proof. rewrite -lc_split //=. Qed.
Lemma lc_weaken {n} m :
m n £ n -∗ £ m.
Proof.
intros [k ->]%Nat.le_sum. rewrite lc_split. iIntros "[$ _]".
Qed.
Global Instance lc_timeless n : Timeless (£ n).
Proof.
rewrite lc_unseal /lc_def. apply _.
Qed.
Global Instance lc_0_persistent : Persistent (£ 0).
Proof.
rewrite lc_unseal /lc_def. apply _.
Qed.
(** Make sure that the rule for [+] is used before [S], otherwise Coq's
unification applies the [S] hint too eagerly. See Iris issue #470. *)
Global Instance from_sep_lc_add n m :
FromSep (£ (n + m)) (£ n) (£ m) | 0.
Proof.
by rewrite /FromSep lc_split.
Qed.
Global Instance from_sep_lc_S n :
FromSep (£ (S n)) (£ 1) (£ n) | 1.
Proof.
by rewrite /FromSep (lc_succ n).
Qed.
(** When combining later credits with [iCombine], the priorities are
reversed when compared to [FromSep] and [IntoSep]. This causes
[£ n] and [£ 1] to be combined as [£ (S n)], not as [£ (n + 1)]. *)
Global Instance combine_sep_lc_add n m :
CombineSepAs (£ n) (£ m) (£ (n + m)) | 1.
Proof.
by rewrite /CombineSepAs lc_split.
Qed.
Global Instance combine_sep_lc_S_l n :
CombineSepAs (£ n) (£ 1) (£ (S n)) | 0.
Proof.
by rewrite /CombineSepAs comm (lc_succ n).
Qed.
Global Instance into_sep_lc_add n m :
IntoSep (£ (n + m)) (£ n) (£ m) | 0.
Proof.
by rewrite /IntoSep lc_split.
Qed.
Global Instance into_sep_lc_S n :
IntoSep (£ (S n)) (£ 1) (£ n) | 1.
Proof.
by rewrite /IntoSep (lc_succ n).
Qed.
End later_credit_theory.
(** Let users import the above without also getting the below laws.
This should only be imported by the internal development of fancy updates. *)
Module le_upd.
(** Definition of the later-elimination update *)
Definition le_upd_pre `{!lcGS Σ}
(le_upd : iProp Σ -d> iPropO Σ) : iProp Σ -d> iPropO Σ := λ P,
( n, lc_supply n ==∗
(lc_supply n P) ( m, m < n lc_supply m le_upd P))%I.
Local Instance le_upd_pre_contractive `{!lcGS Σ} : Contractive le_upd_pre.
Proof. solve_contractive. Qed.
Local Definition le_upd_def `{!lcGS Σ} :
iProp Σ -d> iPropO Σ := fixpoint le_upd_pre.
Local Definition le_upd_aux : seal (@le_upd_def). Proof. by eexists. Qed.
Definition le_upd := le_upd_aux.(unseal).
Local Definition le_upd_unseal : @le_upd = @le_upd_def := le_upd_aux.(seal_eq).
Global Arguments le_upd {_ _} _.
Notation "'|==£>' P" := (le_upd P%I) (at level 99, P at level 200, format "|==£> P") : bi_scope.
Local Lemma le_upd_unfold `{!lcGS Σ} P:
(|==£> P) ⊣⊢
n, lc_supply n ==∗
(lc_supply n P) ( m, m < n lc_supply m le_upd P).
Proof.
by rewrite le_upd_unseal
/le_upd_def {1}(fixpoint_unfold le_upd_pre P) {1}/le_upd_pre.
Qed.
Section le_upd.
Context `{!lcGS Σ}.
Implicit Types (P Q : iProp Σ).
(** Rules for the later elimination update *)
Global Instance le_upd_ne : NonExpansive le_upd.
Proof.
intros n; induction (lt_wf n) as [n _ IH].
intros P1 P2 HP. rewrite (le_upd_unfold P1) (le_upd_unfold P2).
do 9 (done || f_equiv). f_contractive. by eapply IH, dist_lt.
Qed.
Lemma bupd_le_upd P : (|==> P) (|==£> P).
Proof.
rewrite le_upd_unfold; iIntros "Hupd" (x) "Hpr".
iMod "Hupd" as "P". iModIntro. iLeft. by iFrame.
Qed.
Lemma le_upd_intro P : P |==£> P.
Proof.
iIntros "H"; by iApply bupd_le_upd.
Qed.
Lemma le_upd_bind P Q :
(P -∗ |==£> Q) -∗ (|==£> P) -∗ (|==£> Q).
Proof.
iLöb as "IH". iIntros "PQ".
iEval (rewrite (le_upd_unfold P) (le_upd_unfold Q)).
iIntros "Hupd" (x) "Hpr". iMod ("Hupd" with "Hpr") as "[Hupd|Hupd]".
- iDestruct "Hupd" as "[Hpr Hupd]".
iSpecialize ("PQ" with "Hupd").
iEval (rewrite le_upd_unfold) in "PQ".
iMod ("PQ" with "Hpr") as "[Hupd|Hupd]".
+ iModIntro. by iLeft.
+ iModIntro. iRight. iDestruct "Hupd" as (x'' Hstep'') "[Hpr Hupd]".
iExists _; iFrame. by iPureIntro.
- iModIntro. iRight. iDestruct "Hupd" as (x') "(Hstep & Hpr & Hupd)".
iExists _; iFrame. iNext. by iApply ("IH" with "PQ Hupd").
Qed.
Lemma le_upd_later_elim P :
£ 1 -∗ ( |==£> P) -∗ |==£> P.
Proof.
iIntros "Hc Hl".
iEval (rewrite le_upd_unfold). iIntros (n) "Hs".
iDestruct (lc_supply_bound with "Hs Hc") as "%".
destruct n as [ | n]; first by lia.
replace (S n) with (1 + n) by lia.
iMod (lc_decrease_supply with "Hs Hc") as "Hs". eauto 10 with iFrame lia.
Qed.
(** Derived lemmas *)
Lemma le_upd_mono P Q : (P Q) (|==£> P) (|==£> Q).
Proof.
intros Hent. iApply le_upd_bind.
iIntros "P"; iApply le_upd_intro; by iApply Hent.
Qed.
Global Instance le_upd_mono' : Proper (() ==> ()) le_upd.
Proof. intros P Q PQ; by apply le_upd_mono. Qed.
Global Instance le_upd_flip_mono' : Proper (flip () ==> flip ()) le_upd.
Proof. intros P Q PQ; by apply le_upd_mono. Qed.
Global Instance le_upd_equiv_proper : Proper (() ==> ()) le_upd.
Proof. apply ne_proper. apply _. Qed.
Lemma le_upd_trans P : (|==£> |==£> P) |==£> P.
Proof.
iIntros "HP". iApply le_upd_bind; eauto.
Qed.
Lemma le_upd_frame_r P R : (|==£> P) R |==£> P R.
Proof.
iIntros "[Hupd R]". iApply (le_upd_bind with "[R]"); last done.
iIntros "P". iApply le_upd_intro. by iFrame.
Qed.
Lemma le_upd_frame_l P R : R (|==£> P) |==£> R P.
Proof. rewrite comm le_upd_frame_r comm //. Qed.
Lemma le_upd_later P :
£ 1 -∗ P -∗ |==£> P.
Proof.
iIntros "H1 H2". iApply (le_upd_later_elim with "H1").
iNext. by iApply le_upd_intro.
Qed.
Lemma except_0_le_upd P : (le_upd P) le_upd ( P).
Proof.
rewrite /bi_except_0. apply or_elim; eauto using le_upd_mono, or_intro_r.
by rewrite -le_upd_intro -or_intro_l.
Qed.
(** A safety check that later-elimination updates can replace basic updates *)
(** We do not use this to build an instance, because it would conflict
with the basic updates. *)
Local Lemma bi_bupd_mixin_le_upd : BiBUpdMixin (iPropI Σ) le_upd.
Proof.
split; rewrite /bupd.
- apply _.
- apply le_upd_intro.
- apply le_upd_mono.
- apply le_upd_trans.
- apply le_upd_frame_r.
Qed.
(** unfolding the later elimination update *)
Lemma le_upd_elim n P :
lc_supply n -∗
(|==£> P) -∗
Nat.iter n (λ P, |==> P) (|==> ( m, m n lc_supply m P)).
Proof.
induction (Nat.lt_wf_0 n) as [n _ IH].
iIntros "Ha". rewrite (le_upd_unfold P) //=.
iIntros "Hupd". iSpecialize ("Hupd" with "Ha").
destruct n as [|n]; simpl.
- iMod "Hupd" as "[[H● ?]| Hf]".
{ do 2 iModIntro. iExists 0. iFrame. done. }
iDestruct "Hf" as (x' Hlt) "_". lia.
- iMod "Hupd" as "[[Hc P]|Hupd]".
+ iModIntro. iNext. iApply iter_modal_intro; last first.
{ do 2 iModIntro. iExists (S n); iFrame; done. }
iIntros (Q) "Q"; iModIntro; by iNext.
+ iModIntro. iDestruct "Hupd" as (m Hstep) "[Hown Hupd]". iNext.
iPoseProof (IH with "Hown Hupd") as "Hit"; first done.
clear IH.
assert (m n) as [k ->]%Nat.le_sum by lia.
rewrite Nat.add_comm Nat.iter_add.
iApply iter_modal_intro.
{ by iIntros (Q) "$". }
iApply (iter_modal_mono with "[] Hit").
{ iIntros (R S) "Hent H". by iApply "Hent". }
iIntros "H". iMod "H". iModIntro. iMod "H" as (m' Hle) "H".
iModIntro. iExists m'. iFrame. iPureIntro. lia.
Qed.
Lemma le_upd_elim_complete n P :
lc_supply n -∗
(|==£> P) -∗
Nat.iter (S n) (λ Q, |==> Q) P.
Proof.
iIntros "Hlc Hupd". iPoseProof (le_upd_elim with "Hlc Hupd") as "Hit".
rewrite Nat.iter_succ_r. iApply (iter_modal_mono with "[] Hit").
{ clear. iIntros (P Q) "Hent HP". by iApply "Hent". }
iIntros "Hupd". iMod "Hupd". iModIntro. iMod "Hupd".
iNext. iDestruct "Hupd" as "[%m (_ & _ & $)]".
Qed.
(** Proof mode class instances internally needed for people defining their
[fupd] with [le_upd]. *)
Global Instance elim_bupd_le_upd p P Q :
ElimModal True p false (bupd P) P (le_upd Q) (le_upd Q)%I.
Proof.
rewrite /ElimModal bi.intuitionistically_if_elim //=.
rewrite bupd_le_upd. iIntros "_ [HP HPQ]".
iApply (le_upd_bind with "HPQ HP").
Qed.
Global Instance from_assumption_le_upd p P Q :
FromAssumption p P Q KnownRFromAssumption p P (le_upd Q).
Proof.
rewrite /KnownRFromAssumption /FromAssumption=>->. apply le_upd_intro.
Qed.
Global Instance from_pure_le_upd a P φ :
FromPure a P φ FromPure a (le_upd P) φ.
Proof. rewrite /FromPure=> <-. apply le_upd_intro. Qed.
Global Instance is_except_0_le_upd P : IsExcept0 P IsExcept0 (le_upd P).
Proof.
rewrite /IsExcept0=> HP.
by rewrite -{2}HP -(except_0_idemp P) -except_0_le_upd -(except_0_intro P).
Qed.
Global Instance from_modal_le_upd P :
FromModal True modality_id (le_upd P) (le_upd P) P.
Proof. by rewrite /FromModal /= -le_upd_intro. Qed.
Global Instance elim_modal_le_upd p P Q :
ElimModal True p false (le_upd P) P (le_upd Q) (le_upd Q).
Proof.
by rewrite /ElimModal
intuitionistically_if_elim le_upd_frame_r wand_elim_r le_upd_trans.
Qed.
Global Instance frame_le_upd p R P Q :
Frame p R P Q Frame p R (le_upd P) (le_upd Q).
Proof. rewrite /Frame=><-. by rewrite le_upd_frame_l. Qed.
End le_upd.
(** You probably do NOT want to use this lemma; use [lc_soundness] if you want
to actually use [le_upd]! *)
Local Lemma lc_alloc `{!lcGpreS Σ} n :
|==> _ : lcGS Σ, lc_supply n £ n.
Proof.
rewrite lc_unseal /lc_def lc_supply_unseal /lc_supply_def.
iMod (own_alloc ( n n)) as (γLC) "[H● H◯]";
first (apply auth_both_valid; split; done).
pose (C := LcGS _ _ γLC).
iModIntro. iExists C. iFrame.
Qed.
Lemma lc_soundness `{!lcGpreS Σ} m (P : iProp Σ) `{!Plain P} :
( {Hc: lcGS Σ}, £ m -∗ |==£> P) P.
Proof.
intros H. apply (laterN_soundness _ (S m)).
eapply bupd_soundness; first apply _.
iStartProof.
iMod (lc_alloc m) as (C) "[H● H◯]".
iPoseProof (H C) as "Hc". iSpecialize ("Hc" with "H◯").
iPoseProof (le_upd_elim_complete m with "H● Hc") as "H".
simpl. iMod "H". iModIntro. iNext.
clear H. iInduction m as [|m IH]; simpl; [done|].
iMod "H". iNext. by iApply "IH".
Qed.
End le_upd.
(** This should only be imported by the internal development of fancy updates. *)
Module le_upd_if.
Export le_upd.
Section le_upd_if.
Context `{!lcGS Σ}.
Definition le_upd_if (b : bool) : iProp Σ iProp Σ :=
if b then le_upd else bupd.
Global Instance le_upd_if_mono' b : Proper (() ==> ()) (le_upd_if b).
Proof. destruct b; apply _. Qed.
Global Instance le_upd_if_flip_mono' b :
Proper (flip () ==> flip ()) (le_upd_if b).
Proof. destruct b; apply _. Qed.
Global Instance le_upd_if_proper b : Proper (() ==> ()) (le_upd_if b).
Proof. destruct b; apply _. Qed.
Global Instance le_upd_if_ne b : NonExpansive (le_upd_if b).
Proof. destruct b; apply _. Qed.
Lemma le_upd_if_intro b P : P le_upd_if b P.
Proof.
destruct b; [apply le_upd_intro | apply bupd_intro].
Qed.
Lemma le_upd_if_bind b P Q :
(P -∗ le_upd_if b Q) -∗ (le_upd_if b P) -∗ (le_upd_if b Q).
Proof.
destruct b; first apply le_upd_bind. simpl.
iIntros "HPQ >HP". by iApply "HPQ".
Qed.
Lemma le_upd_if_mono b P Q : (P Q) (le_upd_if b P) (le_upd_if b Q).
Proof.
destruct b; [apply le_upd_mono | apply bupd_mono].
Qed.
Lemma le_upd_if_trans b P : (le_upd_if b (le_upd_if b P)) le_upd_if b P.
Proof.
destruct b; [apply le_upd_trans | apply bupd_trans].
Qed.
Lemma le_upd_if_frame_r b P R : (le_upd_if b P) R le_upd_if b (P R).
Proof.
destruct b; [apply le_upd_frame_r | apply bupd_frame_r].
Qed.
Lemma bupd_le_upd_if b P : (|==> P) (le_upd_if b P).
Proof.
destruct b; [apply bupd_le_upd | done].
Qed.
Lemma le_upd_if_frame_l b R Q : (R le_upd_if b Q) le_upd_if b (R Q).
Proof.
rewrite comm le_upd_if_frame_r comm //.
Qed.
Lemma except_0_le_upd_if b P : (le_upd_if b P) le_upd_if b ( P).
Proof.
rewrite /bi_except_0. apply or_elim; eauto using le_upd_if_mono, or_intro_r.
by rewrite -le_upd_if_intro -or_intro_l.
Qed.
(** Proof mode class instances that we need for the internal development,
i.e. for the definition of fancy updates. *)
Global Instance elim_bupd_le_upd_if b p P Q :
ElimModal True p false (bupd P) P (le_upd_if b Q) (le_upd_if b Q)%I.
Proof.
rewrite /ElimModal bi.intuitionistically_if_elim //=.
rewrite bupd_le_upd_if. iIntros "_ [HP HPQ]".
iApply (le_upd_if_bind with "HPQ HP").
Qed.
Global Instance from_assumption_le_upd_if b p P Q :
FromAssumption p P Q KnownRFromAssumption p P (le_upd_if b Q).
Proof.
rewrite /KnownRFromAssumption /FromAssumption=>->. apply le_upd_if_intro.
Qed.
Global Instance from_pure_le_upd_if b a P φ :
FromPure a P φ FromPure a (le_upd_if b P) φ.
Proof. rewrite /FromPure=> <-. apply le_upd_if_intro. Qed.
Global Instance is_except_0_le_upd_if b P : IsExcept0 P IsExcept0 (le_upd_if b P).
Proof.
rewrite /IsExcept0=> HP.
by rewrite -{2}HP -(except_0_idemp P) -except_0_le_upd_if -(except_0_intro P).
Qed.
Global Instance from_modal_le_upd_if b P :
FromModal True modality_id (le_upd_if b P) (le_upd_if b P) P.
Proof. by rewrite /FromModal /= -le_upd_if_intro. Qed.
Global Instance elim_modal_le_upd_if b p P Q :
ElimModal True p false (le_upd_if b P) P (le_upd_if b Q) (le_upd_if b Q).
Proof.
by rewrite /ElimModal
intuitionistically_if_elim le_upd_if_frame_r wand_elim_r le_upd_if_trans.
Qed.
Global Instance frame_le_upd_if b p R P Q :
Frame p R P Q Frame p R (le_upd_if b P) (le_upd_if b Q).
Proof. rewrite /Frame=><-. by rewrite le_upd_if_frame_l. Qed.
End le_upd_if.
End le_upd_if.
(** Ghost state for a monotonically increasing non-negative integer.
This is basically a [Z]-typed wrapper over [mono_nat], which can be useful when
one wants to use [Z] consistently for everything.
Provides an authoritative proposition [mono_Z_auth_own γ q n] for the
underlying number [n] and a persistent proposition [mono_nat_lb_own γ m]
witnessing that the authoritative nat is at least [m].
The key rules are [mono_Z_lb_own_valid], which asserts that an auth at [n] and
a lower-bound at [m] imply that [m ≤ n], and [mono_Z_update], which allows to
increase the auth element. At any time the auth nat can be "snapshotted" with
[mono_Z_get_lb] to produce a persistent lower-bound proposition.
Note: This construction requires the integers to be non-negative, i.e., to have
the lower bound 0, which gives [mono_Z_lb_own_0 : |==> mono_Z_lb_own γ 0]. This
rule would be false if we were to generalize to negative integers. See
https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/889 for a discussion about
the generalization to negative integers. *)
From iris.proofmode Require Import proofmode.
From iris.algebra.lib Require Import mono_nat.
From iris.bi.lib Require Import fractional.
From iris.base_logic.lib Require Export own.
From iris.base_logic.lib Require Import mono_nat.
From iris.prelude Require Import options.
Local Open Scope Z_scope.
Class mono_ZG Σ :=
MonoZG { #[local] mono_ZG_natG :: mono_natG Σ; }.
Definition mono_ZΣ := mono_natΣ.
Local Definition mono_Z_auth_own_def `{!mono_ZG Σ}
(γ : gname) (q : Qp) (n : Z) : iProp Σ :=
0 n mono_nat_auth_own γ q (Z.to_nat n).
Local Definition mono_Z_auth_own_aux : seal (@mono_Z_auth_own_def).
Proof. by eexists. Qed.
Definition mono_Z_auth_own := mono_Z_auth_own_aux.(unseal).
Local Definition mono_Z_auth_own_unseal :
@mono_Z_auth_own = @mono_Z_auth_own_def := mono_Z_auth_own_aux.(seal_eq).
Global Arguments mono_Z_auth_own {Σ _} γ q n.
Local Definition mono_Z_lb_own_def `{!mono_ZG Σ} (γ : gname) (n : Z) : iProp Σ :=
0 n mono_nat_lb_own γ (Z.to_nat n).
Local Definition mono_Z_lb_own_aux : seal (@mono_Z_lb_own_def). Proof. by eexists. Qed.
Definition mono_Z_lb_own := mono_Z_lb_own_aux.(unseal).
Local Definition mono_Z_lb_own_unseal :
@mono_Z_lb_own = @mono_Z_lb_own_def := mono_Z_lb_own_aux.(seal_eq).
Global Arguments mono_Z_lb_own {Σ _} γ n.
Local Ltac unseal := rewrite
?mono_Z_auth_own_unseal /mono_Z_auth_own_def
?mono_Z_lb_own_unseal /mono_Z_lb_own_def.
Section mono_Z.
Context `{!mono_ZG Σ}.
Implicit Types (n m : Z).
Global Instance mono_Z_auth_own_timeless γ q n : Timeless (mono_Z_auth_own γ q n).
Proof. unseal. apply _. Qed.
Global Instance mono_Z_lb_own_timeless γ n : Timeless (mono_Z_lb_own γ n).
Proof. unseal. apply _. Qed.
Global Instance mono_Z_lb_own_persistent γ n : Persistent (mono_Z_lb_own γ n).
Proof. unseal. apply _. Qed.
Global Instance mono_Z_auth_own_fractional γ n :
Fractional (λ q, mono_Z_auth_own γ q n).
Proof.
unseal. intros p q. iSplit.
- iIntros "[% [$ $]]". eauto.
- iIntros "[[% H1] [% H2]]". iCombine "H1 H2" as "$". eauto.
Qed.
Global Instance mono_Z_auth_own_as_fractional γ q n :
AsFractional (mono_Z_auth_own γ q n) (λ q, mono_Z_auth_own γ q n) q.
Proof. split; [auto|apply _]. Qed.
Lemma mono_Z_auth_own_agree γ q1 q2 n1 n2 :
mono_Z_auth_own γ q1 n1 -∗
mono_Z_auth_own γ q2 n2 -∗
(q1 + q2 1)%Qp n1 = n2⌝.
Proof.
unseal. iIntros "[% H1] [% H2]".
iDestruct (mono_nat_auth_own_agree with "H1 H2") as %?.
iPureIntro. naive_solver lia.
Qed.
Lemma mono_Z_auth_own_exclusive γ n1 n2 :
mono_Z_auth_own γ 1 n1 -∗ mono_Z_auth_own γ 1 n2 -∗ False.
Proof.
iIntros "H1 H2".
by iDestruct (mono_Z_auth_own_agree with "H1 H2") as %[[] _].
Qed.
Lemma mono_Z_lb_own_valid γ q n m :
mono_Z_auth_own γ q n -∗ mono_Z_lb_own γ m -∗ (q 1)%Qp m n⌝.
Proof.
unseal. iIntros "[% Hauth] [% Hlb]".
iDestruct (mono_nat_lb_own_valid with "Hauth Hlb") as %Hvalid.
iPureIntro. naive_solver lia.
Qed.
(** The conclusion of this lemma is persistent; the proofmode will preserve
the [mono_Z_auth_own] in the premise as long as the conclusion is introduced
to the persistent context, for example with [iDestruct (mono_Z_lb_own_get
with "Hauth") as "#Hfrag"]. *)
Lemma mono_Z_lb_own_get γ q n :
mono_Z_auth_own γ q n -∗ mono_Z_lb_own γ n.
Proof. unseal. iIntros "[% ?]". iSplit; first done. by iApply mono_nat_lb_own_get. Qed.
Lemma mono_Z_lb_own_le {γ n} n' :
n' n
0 n'
mono_Z_lb_own γ n -∗ mono_Z_lb_own γ n'.
Proof.
unseal. iIntros "% % [% ?]". iSplit; first done.
iApply mono_nat_lb_own_le; last done. lia.
Qed.
Lemma mono_Z_lb_own_0 γ :
|==> mono_Z_lb_own γ 0.
Proof. unseal. iMod mono_nat_lb_own_0 as "$". eauto. Qed.
Lemma mono_Z_own_alloc n :
0 n
|==> γ, mono_Z_auth_own γ 1 n mono_Z_lb_own γ n.
Proof.
unseal. intros. iMod mono_nat_own_alloc as (γ) "[??]".
iModIntro. iExists _. iFrame. eauto.
Qed.
Lemma mono_Z_own_update {γ n} n' :
n n'
mono_Z_auth_own γ 1 n ==∗ mono_Z_auth_own γ 1 n' mono_Z_lb_own γ n'.
Proof.
iIntros (?) "Hauth".
iAssert (mono_Z_auth_own γ 1 n') with "[> Hauth]" as "Hauth".
{ unseal. iDestruct "Hauth" as "[% Hauth]".
iMod (mono_nat_own_update with "Hauth") as "[$ _]"; auto with lia. }
iModIntro. iSplit; [done|]. by iApply mono_Z_lb_own_get.
Qed.
End mono_Z.