diff --git a/iris/algebra/lib/gmap_view.v b/iris/algebra/lib/gmap_view.v
index 74f2de7778a73a0c3fa37e6b0832f1dc79aa715c..96639d8f4e2e37a0ef1cdc761e640050e116910e 100644
--- a/iris/algebra/lib/gmap_view.v
+++ b/iris/algebra/lib/gmap_view.v
@@ -20,17 +20,28 @@ NOTE: The API surface for [gmap_view] is experimental and subject to change. We
plan to add notations for authoritative elements and fragments, and hope to
support arbitrary maps as fragments. *)
-Local Definition gmap_view_fragUR (K : Type) `{Countable K} (V : ofe) : ucmra :=
- gmapUR K (prodR dfracR (agreeR V)).
+Local Definition gmap_view_fragUR (K : Type) `{Countable K} (V : cmra) : ucmra :=
+ gmapUR K (prodR dfracR V).
(** View relation. *)
Section rel.
- Context (K : Type) `{Countable K} (V : ofe).
+ Context (K : Type) `{Countable K} (V : cmra).
Implicit Types (m : gmap K V) (k : K) (v : V) (n : nat).
- Implicit Types (f : gmap K (dfrac * agree V)).
-
+ Implicit Types (f : gmap K (dfrac * V)).
+
+ (* This is very similar to [auth] except that we do not require a unit,
+ and the authoritative fraction is "erased": instead of [dv ≼ (DfracOwn 1, v)],
+ we just say that [dv ≼ (_, v)] for *some* valid value in place of the
+ underscore, and we move to the reflexive closure via [Some dv ≼ Some (_, v)].
+ This ensures that if [dv.1] is the full fraction, we get the right behavior:
+ there is no frame, and hence [dv.2 ≡ v]. At the same time it allows
+ [dv.1 = DfracDiscarded], which would be ruled out by hard-coding [DfracOwn 1].
+
+ It is possible that [∀ k, ∃ dq, let auth := (pair dq) <$> m !! k in ✓{n} auth
+ ∧ f !! k ≼{n} auth] would also work, but now the proofs are all done already. ;)
+ The two are probably equivalent, with a proof similar to [lookup_includedN]? *)
Local Definition gmap_view_rel_raw n m f : Prop :=
- map_Forall (λ k dv, ∃ v, dv.2 ≡{n}≡ to_agree v ∧ ✓ dv.1 ∧ m !! k = Some v) f.
+ map_Forall (λ k dv, ∃ v dq, m !! k = Some v ∧ ✓{n} (dq, v) ∧ (Some dv ≼{n} Some (dq, v))) f.
Local Lemma gmap_view_rel_raw_mono n1 n2 m1 m2 f1 f2 :
gmap_view_rel_raw n1 m1 f1 →
@@ -39,40 +50,26 @@ Section rel.
n2 ≤ n1 →
gmap_view_rel_raw n2 m2 f2.
Proof.
- intros Hrel Hm Hf Hn k [q va] Hk.
+ intros Hrel Hm Hf Hn k [dqa va] Hk.
(* For some reason applying the lemma in [Hf] does not work... *)
destruct (lookup_includedN n2 f2 f1) as [Hf' _]. specialize (Hf' Hf). clear Hf.
specialize (Hf' k). rewrite Hk in Hf'.
- apply option_includedN in Hf'.
- destruct Hf' as [[=]|(? & [q' va'] & [= <-] & Hf1 & Hincl)].
- specialize (Hrel _ _ Hf1) as (v & Hagree & Hdval & Hm1). simpl in *.
+ destruct (Some_includedN_is_Some _ _ _ Hf') as [[q' va'] Heq]. rewrite Heq in Hf'.
+ specialize (Hrel _ _ Heq) as (v & dq & Hm1 & [Hvval Hdqval] & Hvincl). simpl in *.
specialize (Hm k).
edestruct (dist_Some_inv_l _ _ _ _ Hm Hm1) as (v' & Hm2 & Hv).
- exists v'. rewrite assoc. split; last done.
- rewrite -Hv.
- destruct Hincl as [[Heqq Heqva]|[Hinclq Hinclva]%pair_includedN].
- - simpl in *. split.
- + rewrite Heqva. eapply dist_le; last eassumption. done.
- + rewrite <-discrete_iff in Heqq; last by apply _.
- fold_leibniz. subst q'. done.
- - split.
- + etrans; last first.
- { eapply dist_le; last eassumption. done. }
- eapply agree_valid_includedN; last done.
- eapply cmra_validN_le; last eassumption.
- rewrite Hagree. done.
- + rewrite <-cmra_discrete_included_iff in Hinclq.
- eapply cmra_valid_included; done.
+ eexists. exists dq. split; first done. split.
+ { split; first done. simpl. rewrite -Hv. eapply cmra_validN_le; done. }
+ rewrite -Hv. etrans; first exact Hf'.
+ apply: cmra_includedN_le; eassumption.
Qed.
Local Lemma gmap_view_rel_raw_valid n m f :
gmap_view_rel_raw n m f → ✓{n} f.
Proof.
- intros Hrel k. destruct (f !! k) as [[q va]|] eqn:Hf; rewrite Hf; last done.
- specialize (Hrel _ _ Hf) as (v & Hagree & Hdval & Hm1). simpl in *.
- split; simpl.
- - apply cmra_discrete_valid_iff. done.
- - rewrite Hagree. done.
+ intros Hrel k. destruct (f !! k) as [[dqa va]|] eqn:Hf; rewrite Hf; last done.
+ specialize (Hrel _ _ Hf) as (v & dq & Hmval & Hvval & Hvincl). simpl in *.
+ eapply cmra_validN_includedN. 2:done. done.
Qed.
Local Lemma gmap_view_rel_raw_unit n :
@@ -83,7 +80,7 @@ Section rel.
ViewRel gmap_view_rel_raw gmap_view_rel_raw_mono
gmap_view_rel_raw_valid gmap_view_rel_raw_unit.
- Local Lemma gmap_view_rel_exists n (f : gmap K (dfrac * agreeR V)) :
+ Local Lemma gmap_view_rel_exists n f :
(∃ m, gmap_view_rel n m f) ↔ ✓{n} f.
Proof.
split.
@@ -91,16 +88,16 @@ Section rel.
intros Hf.
cut (∃ m, gmap_view_rel n m f ∧ ∀ k, f !! k = None → m !! k = None).
{ naive_solver. }
- induction f as [|k [dq ag] f Hk' IH] using map_ind.
+ induction f as [|k [dq v] f Hk' IH] using map_ind.
{ exists ∅. split; [|done]. apply: map_Forall_empty. }
move: (Hf k). rewrite lookup_insert=> -[/= ??].
- destruct (to_agree_uninjN n ag) as [v ?]; [done|].
destruct IH as (m & Hm & Hdom).
{ intros k'. destruct (decide (k = k')) as [->|?]; [by rewrite Hk'|].
move: (Hf k'). by rewrite lookup_insert_ne. }
exists (<[k:=v]> m).
rewrite /gmap_view_rel /= /gmap_view_rel_raw map_Forall_insert //=. split_and!.
- - exists v. by rewrite lookup_insert.
+ - exists v, dq. split; first by rewrite lookup_insert.
+ split; first by split. done.
- eapply map_Forall_impl; [apply Hm|]; simpl.
intros k' [dq' ag'] (v'&?&?&?). exists v'.
rewrite lookup_insert_ne; naive_solver.
@@ -111,14 +108,13 @@ Section rel.
Proof. apply: map_Forall_empty. Qed.
Local Lemma gmap_view_rel_discrete :
- OfeDiscrete V → ViewRelDiscrete gmap_view_rel.
+ CmraDiscrete V → ViewRelDiscrete gmap_view_rel.
Proof.
intros ? n m f Hrel k [df va] Hk.
- destruct (Hrel _ _ Hk) as (v & Hagree & Hdval & Hm).
- exists v. split; last by auto.
- eapply discrete_iff; first by apply _.
- eapply discrete_iff; first by apply _.
- done.
+ destruct (Hrel _ _ Hk) as (v & dq & Hm & Hvval & Hvincl).
+ exists v, dq. split; first done.
+ split; first by apply cmra_discrete_valid_iff_0.
+ rewrite -cmra_discrete_included_iff_0. done.
Qed.
End rel.
@@ -127,24 +123,24 @@ Local Existing Instance gmap_view_rel_discrete.
(** [gmap_view] is a notation to give canonical structure search the chance
to infer the right instances (see [auth]). *)
Notation gmap_view K V := (view (@gmap_view_rel_raw K _ _ V)).
-Definition gmap_viewO (K : Type) `{Countable K} (V : ofe) : ofe :=
+Definition gmap_viewO (K : Type) `{Countable K} (V : cmra) : ofe :=
viewO (gmap_view_rel K V).
-Definition gmap_viewR (K : Type) `{Countable K} (V : ofe) : cmra :=
+Definition gmap_viewR (K : Type) `{Countable K} (V : cmra) : cmra :=
viewR (gmap_view_rel K V).
-Definition gmap_viewUR (K : Type) `{Countable K} (V : ofe) : ucmra :=
+Definition gmap_viewUR (K : Type) `{Countable K} (V : cmra) : ucmra :=
viewUR (gmap_view_rel K V).
Section definitions.
- Context {K : Type} `{Countable K} {V : ofe}.
+ Context {K : Type} `{Countable K} {V : cmra}.
Definition gmap_view_auth (dq : dfrac) (m : gmap K V) : gmap_viewR K V :=
â—V{dq} m.
Definition gmap_view_frag (k : K) (dq : dfrac) (v : V) : gmap_viewR K V :=
- â—¯V {[k := (dq, to_agree v)]}.
+ â—¯V {[k := (dq, v)]}.
End definitions.
Section lemmas.
- Context {K : Type} `{Countable K} {V : ofe}.
+ Context {K : Type} `{Countable K} {V : cmra}.
Implicit Types (m : gmap K V) (k : K) (q : Qp) (dq : dfrac) (v : V).
Global Instance : Params (@gmap_view_auth) 5 := {}.
@@ -161,18 +157,18 @@ Section lemmas.
(* Helper lemmas *)
Local Lemma gmap_view_rel_lookup n m k dq v :
- gmap_view_rel K V n m {[k := (dq, to_agree v)]} ↔ ✓ dq ∧ m !! k ≡{n}≡ Some v.
+ gmap_view_rel K V n m {[k := (dq, v)]} ↔
+ ∃ v' dq', m !! k = Some v' ∧ ✓{n} (dq', v') ∧ Some (dq, v) ≼{n} Some (dq', v').
Proof.
split.
- intros Hrel.
- edestruct (Hrel k) as (v' & Hagree & Hval & ->).
+ edestruct (Hrel k) as (v' & dq' & Hlookup & Hval & Hinc).
{ rewrite lookup_singleton. done. }
- simpl in *. apply (inj _) in Hagree. rewrite Hagree.
- done.
- - intros [Hval (v' & Hm & Hv')%dist_Some_inv_r'] j [df va].
+ simpl in *. eexists _, _. split_and!; done.
+ - intros (v' & dq' & Hlookup & Hval & ?) j [df va].
destruct (decide (k = j)) as [<-|Hne]; last by rewrite lookup_singleton_ne.
rewrite lookup_singleton. intros [= <- <-]. simpl.
- exists v'. split_and!; by rewrite ?Hv'.
+ exists v', dq'. split_and!; by rewrite ?Hv'.
Qed.
(** Composition and validity *)
@@ -190,9 +186,6 @@ Section lemmas.
Lemma gmap_view_auth_dfrac_op_inv dp m1 dq m2 :
✓ (gmap_view_auth dp m1 ⋅ gmap_view_auth dq m2) → m1 ≡ m2.
Proof. apply view_auth_dfrac_op_inv. Qed.
- Lemma gmap_view_auth_dfrac_op_inv_L `{!LeibnizEquiv V} dq m1 dp m2 :
- ✓ (gmap_view_auth dp m1 ⋅ gmap_view_auth dq m2) → m1 = m2.
- Proof. apply view_auth_dfrac_op_inv_L, _. Qed.
Lemma gmap_view_auth_dfrac_validN m n dq : ✓{n} gmap_view_auth dq m ↔ ✓ dq.
Proof.
@@ -215,9 +208,6 @@ Section lemmas.
Proof.
rewrite view_auth_dfrac_op_valid. intuition eauto using gmap_view_rel_unit.
Qed.
- Lemma gmap_view_auth_dfrac_op_valid_L `{!LeibnizEquiv V} dq1 dq2 m1 m2 :
- ✓ (gmap_view_auth dq1 m1 ⋅ gmap_view_auth dq2 m2) ↔ ✓ (dq1 ⋅ dq2) ∧ m1 = m2.
- Proof. unfold_leibniz. apply gmap_view_auth_dfrac_op_valid. Qed.
Lemma gmap_view_auth_op_validN n m1 m2 :
✓{n} (gmap_view_auth (DfracOwn 1) m1 ⋅ gmap_view_auth (DfracOwn 1) m2) ↔ False.
@@ -226,121 +216,141 @@ Section lemmas.
✓ (gmap_view_auth (DfracOwn 1) m1 ⋅ gmap_view_auth (DfracOwn 1) m2) ↔ False.
Proof. apply view_auth_op_valid. Qed.
- Lemma gmap_view_frag_validN n k dq v : ✓{n} gmap_view_frag k dq v ↔ ✓ dq.
+ Lemma gmap_view_frag_validN n k dq v : ✓{n} gmap_view_frag k dq v ↔ ✓ dq ∧ ✓{n} v.
Proof.
rewrite view_frag_validN gmap_view_rel_exists singleton_validN pair_validN.
naive_solver.
Qed.
- Lemma gmap_view_frag_valid k dq v : ✓ gmap_view_frag k dq v ↔ ✓ dq.
+ Lemma gmap_view_frag_valid k dq v : ✓ gmap_view_frag k dq v ↔ ✓ dq ∧ ✓ v.
Proof.
rewrite cmra_valid_validN. setoid_rewrite gmap_view_frag_validN.
- naive_solver eauto using O.
+ rewrite cmra_valid_validN. naive_solver eauto using O.
Qed.
- Lemma gmap_view_frag_op k dq1 dq2 v :
- gmap_view_frag k (dq1 ⋅ dq2) v ≡ gmap_view_frag k dq1 v ⋅ gmap_view_frag k dq2 v.
- Proof. rewrite -view_frag_op singleton_op -pair_op agree_idemp //. Qed.
- Lemma gmap_view_frag_add k q1 q2 v :
- gmap_view_frag k (DfracOwn (q1 + q2)) v ≡
- gmap_view_frag k (DfracOwn q1) v â‹… gmap_view_frag k (DfracOwn q2) v.
+ Lemma gmap_view_frag_op k dq1 dq2 v1 v2 :
+ gmap_view_frag k (dq1 ⋅ dq2) (v1 ⋅ v2) ≡ gmap_view_frag k dq1 v1 ⋅ gmap_view_frag k dq2 v2.
+ Proof. rewrite -view_frag_op singleton_op -pair_op //. Qed.
+ Lemma gmap_view_frag_add k q1 q2 v1 v2 :
+ gmap_view_frag k (DfracOwn (q1 + q2)) (v1 ⋅ v2) ≡
+ gmap_view_frag k (DfracOwn q1) v1 â‹… gmap_view_frag k (DfracOwn q2) v2.
Proof. rewrite -gmap_view_frag_op. done. Qed.
Lemma gmap_view_frag_op_validN n k dq1 dq2 v1 v2 :
✓{n} (gmap_view_frag k dq1 v1 ⋅ gmap_view_frag k dq2 v2) ↔
- ✓ (dq1 ⋅ dq2) ∧ v1 ≡{n}≡ v2.
+ ✓ (dq1 ⋅ dq2) ∧ ✓{n} (v1 ⋅ v2).
Proof.
rewrite view_frag_validN gmap_view_rel_exists singleton_op singleton_validN.
- by rewrite -pair_op pair_validN to_agree_op_validN.
+ by rewrite -pair_op pair_validN.
Qed.
Lemma gmap_view_frag_op_valid k dq1 dq2 v1 v2 :
- ✓ (gmap_view_frag k dq1 v1 ⋅ gmap_view_frag k dq2 v2) ↔ ✓ (dq1 ⋅ dq2) ∧ v1 ≡ v2.
+ ✓ (gmap_view_frag k dq1 v1 ⋅ gmap_view_frag k dq2 v2) ↔ ✓ (dq1 ⋅ dq2) ∧ ✓ (v1 ⋅ v2).
Proof.
rewrite view_frag_valid. setoid_rewrite gmap_view_rel_exists.
rewrite -cmra_valid_validN singleton_op singleton_valid.
- by rewrite -pair_op pair_valid to_agree_op_valid.
+ by rewrite -pair_op pair_valid.
Qed.
- (* FIXME: Having a [valid_L] lemma is not consistent with [auth] and [view]; they
- have [inv_L] lemmas instead that just have an equality on the RHS. *)
- Lemma gmap_view_frag_op_valid_L `{!LeibnizEquiv V} k dq1 dq2 v1 v2 :
- ✓ (gmap_view_frag k dq1 v1 ⋅ gmap_view_frag k dq2 v2) ↔ ✓ (dq1 ⋅ dq2) ∧ v1 = v2.
- Proof. unfold_leibniz. apply gmap_view_frag_op_valid. Qed.
Lemma gmap_view_both_dfrac_validN n dp m k dq v :
✓{n} (gmap_view_auth dp m ⋅ gmap_view_frag k dq v) ↔
- ✓ dp ∧ ✓ dq ∧ m !! k ≡{n}≡ Some v.
+ ✓ dp ∧ ∃ v' dq', m !! k = Some v' ∧ ✓{n} (dq', v') ∧ Some (dq, v) ≼{n} Some (dq', v').
Proof.
rewrite /gmap_view_auth /gmap_view_frag.
- rewrite view_both_dfrac_validN gmap_view_rel_lookup.
- naive_solver.
+ rewrite view_both_dfrac_validN gmap_view_rel_lookup. done.
Qed.
- Lemma gmap_view_both_validN n m k dq v :
- ✓{n} (gmap_view_auth (DfracOwn 1) m ⋅ gmap_view_frag k dq v) ↔
- ✓ dq ∧ m !! k ≡{n}≡ Some v.
- Proof. rewrite gmap_view_both_dfrac_validN. naive_solver done. Qed.
- Lemma gmap_view_both_dfrac_valid dp m k dq v :
- ✓ (gmap_view_auth dp m ⋅ gmap_view_frag k dq v) ↔
- ✓ dp ∧ ✓ dq ∧ m !! k ≡ Some v.
+ Lemma gmap_view_both_validN n dp m k v :
+ ✓{n} (gmap_view_auth dp m ⋅ gmap_view_frag k (DfracOwn 1) v) ↔
+ ✓ dp ∧ ✓{n} v ∧ m !! k ≡{n}≡ Some v.
Proof.
- rewrite /gmap_view_auth /gmap_view_frag.
- rewrite view_both_dfrac_valid. setoid_rewrite gmap_view_rel_lookup.
- split=>[[Hq Hm]|[Hq Hm]].
- - split; first done. split.
- + apply (Hm 0%nat).
- + apply equiv_dist=>n. apply Hm.
- - split; first done. intros n. split.
- + apply Hm.
- + revert n. apply equiv_dist. apply Hm.
+ rewrite gmap_view_both_dfrac_validN. split.
+ - intros [Hdp (v' & dq' & Hlookup & Hvalid & Hincl)].
+ split; first done. rewrite Hlookup.
+ destruct (Some_includedN_exclusive _ _ _ Hincl Hvalid) as [_ Heq].
+ simpl in Heq. split.
+ + rewrite pair_validN in Hvalid. rewrite Heq. naive_solver.
+ + by rewrite Heq.
+ - intros (Hdp & Hval & Hlookup). split; first done.
+ apply dist_Some_inv_r' in Hlookup as [v' [Hlookup Heq]].
+ exists v', (DfracOwn 1). split; first done.
+ split.
+ + rewrite pair_validN. split; first done. rewrite -Heq. done.
+ + apply: Some_includedN_refl. split; done.
Qed.
- Lemma gmap_view_both_dfrac_valid_L `{!LeibnizEquiv V} dp m k dq v :
+ (** Without [CmraDiscrete], we cannot do much better than [∀ n, <same as above>].
+ This is because both the [dq'] and the witness for the [≼{n}] can be different for
+ each step-index. It is totally possible that at low step-indices, [v] has a frame
+ (and [dq' > dq]) while at higher step-indices, [v] has no frame (and [dq' = dq]). *)
+ Lemma gmap_view_both_dfrac_valid_discrete `{!CmraDiscrete V} dp m k dq v :
✓ (gmap_view_auth dp m ⋅ gmap_view_frag k dq v) ↔
- ✓ dp ∧ ✓ dq ∧ m !! k = Some v.
- Proof. unfold_leibniz. apply gmap_view_both_dfrac_valid. Qed.
- Lemma gmap_view_both_valid m k dq v :
- ✓ (gmap_view_auth (DfracOwn 1) m ⋅ gmap_view_frag k dq v) ↔
- ✓ dq ∧ m !! k ≡ Some v.
- Proof. rewrite gmap_view_both_dfrac_valid. naive_solver done. Qed.
- (* FIXME: Having a [valid_L] lemma is not consistent with [auth] and [view]; they
- have [inv_L] lemmas instead that just have an equality on the RHS. *)
- Lemma gmap_view_both_valid_L `{!LeibnizEquiv V} m k dq v :
- ✓ (gmap_view_auth (DfracOwn 1) m ⋅ gmap_view_frag k dq v) ↔
- ✓ dq ∧ m !! k = Some v.
- Proof. unfold_leibniz. apply gmap_view_both_valid. Qed.
+ ✓ dp ∧ ∃ v' dq', m !! k = Some v' ∧ ✓ (dq', v') ∧ Some (dq, v) ≼ Some (dq', v').
+ Proof.
+ rewrite cmra_valid_validN. setoid_rewrite gmap_view_both_dfrac_validN. split.
+ - intros Hvalid. specialize (Hvalid 0).
+ destruct Hvalid as [Hdp (v' & dq' & Hlookup & Hvalid & Hincl)].
+ split; first done. exists v', dq'. split; first done.
+ split; first by apply cmra_discrete_valid.
+ by apply: cmra_discrete_included_r.
+ - intros [Hdp (v' & dq' & Hlookup & Hvalid & Hincl)] n.
+ split; first done. exists v', dq'. split; first done.
+ split; first by apply cmra_valid_validN.
+ by apply: cmra_included_includedN.
+ Qed.
+ (** On the other hand, this one holds for all CMRAs, not just discrete ones. *)
+ Lemma gmap_view_both_valid m dp k v :
+ ✓ (gmap_view_auth dp m ⋅ gmap_view_frag k (DfracOwn 1) v) ↔
+ ✓ dp ∧ ✓ v ∧ m !! k ≡ Some v.
+ Proof.
+ rewrite cmra_valid_validN. setoid_rewrite gmap_view_both_validN. split.
+ - intros Hvalid. split; last split.
+ + eapply (Hvalid 0).
+ + apply cmra_valid_validN. intros n. eapply Hvalid.
+ + apply equiv_dist. intros n. eapply Hvalid.
+ - intros (Hdp & Hval & Hlookup). intros n.
+ split; first done. split.
+ + apply cmra_valid_validN. done.
+ + rewrite Hlookup. done.
+ Qed.
(** Frame-preserving updates *)
Lemma gmap_view_alloc m k dq v :
m !! k = None →
✓ dq →
+ ✓ v →
gmap_view_auth (DfracOwn 1) m ~~> gmap_view_auth (DfracOwn 1) (<[k := v]> m) â‹… gmap_view_frag k dq v.
Proof.
- intros Hfresh Hdq. apply view_update_alloc=>n bf Hrel j [df va] /=.
+ intros Hfresh Hdq Hval. apply view_update_alloc=>n bf Hrel j [df va] /=.
rewrite lookup_op. destruct (decide (j = k)) as [->|Hne].
- assert (bf !! k = None) as Hbf.
{ destruct (bf !! k) as [[df' va']|] eqn:Hbf; last done.
- specialize (Hrel _ _ Hbf). destruct Hrel as (v' & _ & _ & Hm).
+ specialize (Hrel _ _ Hbf). destruct Hrel as (v' & dq' & Hm & _).
exfalso. rewrite Hm in Hfresh. done. }
rewrite lookup_singleton Hbf right_id.
- intros [= <- <-]. eexists. do 2 (split; first done).
- rewrite lookup_insert. done.
+ intros [= <- <-]. eexists _, _.
+ rewrite lookup_insert. split; first done.
+ split; last by apply: Some_includedN_refl.
+ split; first done. by eapply cmra_valid_validN.
- rewrite lookup_singleton_ne; last done.
rewrite left_id=>Hbf.
- specialize (Hrel _ _ Hbf). destruct Hrel as (v' & ? & ? & Hm).
- eexists. do 2 (split; first done).
+ specialize (Hrel _ _ Hbf). destruct Hrel as (v' & ? & Hm & ?).
+ eexists _, _. split; last done.
rewrite lookup_insert_ne //.
Qed.
Lemma gmap_view_alloc_big m m' dq :
m' ##ₘ m →
✓ dq →
+ map_Forall (λ k v, ✓ v) m' →
gmap_view_auth (DfracOwn 1) m ~~>
gmap_view_auth (DfracOwn 1) (m' ∪ m) ⋅ ([^op map] k↦v ∈ m', gmap_view_frag k dq v).
Proof.
- intros. induction m' as [|k v m' ? IH] using map_ind; decompose_map_disjoint.
+ intros ?? Hm'. induction m' as [|k v m' ? IH] using map_ind; decompose_map_disjoint.
{ rewrite big_opM_empty left_id_L right_id. done. }
rewrite IH //.
+ 2:{ by eapply map_Forall_insert_1_2. }
rewrite big_opM_insert // assoc.
apply cmra_update_op; last done.
- rewrite -insert_union_l. apply (gmap_view_alloc _ k dq); last done.
- by apply lookup_union_None.
+ rewrite -insert_union_l. apply (gmap_view_alloc _ k dq); [|done|].
+ - by apply lookup_union_None.
+ - eapply Hm'. erewrite lookup_insert. done.
Qed.
Lemma gmap_view_delete m k v :
@@ -349,12 +359,15 @@ Section lemmas.
Proof.
apply view_update_dealloc=>n bf Hrel j [df va] Hbf /=.
destruct (decide (j = k)) as [->|Hne].
- - edestruct (Hrel k) as (v' & _ & Hdf & _).
+ - edestruct (Hrel k) as (v' & dq' & ? & Hval & Hincl).
{ rewrite lookup_op Hbf lookup_singleton -Some_op. done. }
- exfalso. apply: dfrac_full_exclusive. apply Hdf.
- - edestruct (Hrel j) as (v' & ? & ? & Hm).
+ eapply (cmra_validN_Some_includedN _ _ _ Hval) in Hincl as Hval'.
+ exfalso. clear Hval Hincl.
+ rewrite pair_validN /= in Hval'.
+ apply: dfrac_full_exclusive. apply Hval'.
+ - edestruct (Hrel j) as (v' & ? & ? & ?).
{ rewrite lookup_op lookup_singleton_ne // Hbf. done. }
- exists v'. do 2 (split; first done).
+ eexists v', _. split; last done.
rewrite lookup_delete_ne //.
Qed.
@@ -369,22 +382,89 @@ Section lemmas.
rewrite -delete_difference. done.
Qed.
- Lemma gmap_view_update m k v v' :
+ (** This cannot use [local_update] since we also want to expose the role of
+ the fractions. *)
+ Lemma gmap_view_update m k dq v mv' v' dq' :
+ (∀ n mv f,
+ m !! k = Some mv → ✓{n} ((dq, v) ⋅? f) → mv ≡{n}≡ v ⋅? (snd <$> f) →
+ ✓{n} ((dq', v') ⋅? f) ∧ mv' ≡{n}≡ v' ⋅? (snd <$> f)) →
+ gmap_view_auth (DfracOwn 1) m â‹… gmap_view_frag k dq v ~~>
+ gmap_view_auth (DfracOwn 1) (<[k := mv']> m) â‹… gmap_view_frag k dq' v'.
+ Proof.
+ intros Hup. apply view_update=> n bf Hrel j [df va].
+ rewrite lookup_op.
+ destruct (decide (j = k)) as [->|Hne]; last first.
+ { (* prove that other keys are unaffected *)
+ simplify_map_eq. rewrite lookup_singleton_ne //. (* FIXME simplify_map_eq should have done this *)
+ rewrite left_id. intros Hbf.
+ edestruct (Hrel j) as (mva & mdf & Hlookup & Hval & Hincl).
+ { rewrite lookup_op lookup_singleton_ne // left_id //. }
+ naive_solver. }
+ simplify_map_eq. rewrite lookup_singleton. (* FIXME simplify_map_eq should have done this *)
+ intros Hbf.
+ edestruct (Hrel k) as (mv & mdf & Hlookup & Hval & Hincl).
+ { rewrite lookup_op lookup_singleton // Some_op_opM //. }
+ rewrite Some_includedN_opM in Hincl.
+ destruct Hincl as [f' Hincl]. rewrite cmra_opM_opM_assoc in Hincl.
+ set f := bf !! k â‹… f'. (* the complete frame *)
+ change (bf !! k â‹… f') with f in Hincl.
+ specialize (Hup n mv f). destruct Hup as (Hval' & Hincl').
+ { done. }
+ { rewrite -Hincl. done. }
+ { destruct Hincl as [_ Hincl]. simpl in Hincl. rewrite Hincl.
+ by destruct f. }
+ eexists mv', (dq' â‹…? (fst <$> f)). split; first done.
+ rewrite -Hbf. clear Hbf. split.
+ - rewrite Hincl'. destruct Hval'. by destruct f.
+ - rewrite Some_op_opM. rewrite Some_includedN_opM.
+ exists f'. rewrite Hincl'.
+ rewrite cmra_opM_opM_assoc. change (bf !! k â‹… f') with f.
+ by destruct f.
+ Qed.
+
+ (** This derived version cannot exploit [dq = DfracOwn 1]. *)
+ Lemma gmap_view_update_local m k dq mv v mv' v' :
+ m !! k = Some mv →
+ (mv, v) ~l~> (mv', v') →
+ gmap_view_auth (DfracOwn 1) m â‹… gmap_view_frag k dq v ~~>
+ gmap_view_auth (DfracOwn 1) (<[k := mv']> m) â‹… gmap_view_frag k dq v'.
+ Proof.
+ intros Hlookup Hup. apply gmap_view_update.
+ intros n mv0 f Hmv0 Hval Hincl.
+ rewrite Hlookup in Hmv0. injection Hmv0 as [= <-].
+ specialize (Hup n (snd <$> f)). destruct Hup as (Hval' & Hincl').
+ { rewrite Hincl. destruct Hval. by destruct f. }
+ { simpl. done. }
+ split; last done. split.
+ - destruct Hval. by destruct f.
+ - simpl in *. replace (((dq, v') â‹…? f).2) with (v' â‹…? (snd <$> f)).
+ 2:{ by destruct f. }
+ rewrite -Hincl'. done.
+ Qed.
+
+ Lemma gmap_view_replace m k v v' :
+ ✓ v' →
gmap_view_auth (DfracOwn 1) m â‹… gmap_view_frag k (DfracOwn 1) v ~~>
gmap_view_auth (DfracOwn 1) (<[k := v']> m) â‹… gmap_view_frag k (DfracOwn 1) v'.
Proof.
- rewrite gmap_view_delete.
- rewrite (gmap_view_alloc _ k (DfracOwn 1) v') //; last by rewrite lookup_delete.
- rewrite insert_delete_insert //.
+ (* There would be a simple proof via delete-then-insert... but we use this as a
+ sanity check to make sure the update lemma is strong enough. *)
+ intros Hval'. apply gmap_view_update.
+ intros n mv f Hlookup Hval Hincl.
+ destruct f; simpl.
+ { apply exclusiveN_l in Hval; first done. apply _. }
+ split; last done.
+ split; first done. simpl. apply cmra_valid_validN. done.
Qed.
- Lemma gmap_view_update_big m m0 m1 :
+ Lemma gmap_view_replace_big m m0 m1 :
dom m0 = dom m1 →
+ map_Forall (λ k v, ✓ v) m1 →
gmap_view_auth (DfracOwn 1) m ⋅ ([^op map] k↦v ∈ m0, gmap_view_frag k (DfracOwn 1) v) ~~>
gmap_view_auth (DfracOwn 1) (m1 ∪ m) ⋅ ([^op map] k↦v ∈ m1, gmap_view_frag k (DfracOwn 1) v).
Proof.
intros Hdom%eq_sym. revert m1 Hdom.
- induction m0 as [|k v m0 Hnotdom IH] using map_ind; intros m1 Hdom.
+ induction m0 as [|k v m0 Hnotdom IH] using map_ind; intros m1 Hdom Hval.
{ rewrite dom_empty_L in Hdom.
apply dom_empty_iff_L in Hdom as ->.
rewrite left_id_L big_opM_empty. done. }
@@ -394,10 +474,12 @@ Section lemmas.
rewrite big_opM_insert //.
rewrite [gmap_view_frag _ _ _ â‹… _]comm assoc.
rewrite (IH (delete k m1)); last first.
+ { by apply map_Forall_delete. }
{ rewrite dom_delete_L Hdom.
apply not_elem_of_dom in Hnotdom. set_solver -Hdom. }
rewrite -assoc [_ â‹… gmap_view_frag _ _ _]comm assoc.
- rewrite (gmap_view_update _ _ _ v').
+ rewrite (gmap_view_replace _ _ _ v').
+ 2:{ eapply Hval. done. }
rewrite (big_opM_delete _ m1 k v') // -assoc.
rewrite insert_union_r; last by rewrite lookup_delete.
rewrite union_delete_insert //.
@@ -420,17 +502,26 @@ Section lemmas.
[apply view_updateP_frag with (P := λ b', ∃ dq', ◯V b' = gmap_view_frag k dq' v ∧ P dq')
|naive_solver].
intros m n bf Hrel.
- destruct (Hrel k ((dq, to_agree v) â‹…? bf !! k)) as (v' & Hdqv & Hv1 & Hv2).
+ destruct (Hrel k ((dq, v) â‹…? bf !! k)) as (v' & dq' & Hlookup & Hval & Hincl).
{ by rewrite lookup_op lookup_singleton Some_op_opM. }
- destruct (Hdq n (option_map fst (bf !! k))) as (dq' & HPdq' & Hvdq').
- { by destruct (bf !! k). }
- eexists. split; first by exists dq'.
+ rewrite Some_includedN_opM in Hincl.
+ destruct Hincl as [f' Hincl]. rewrite cmra_opM_opM_assoc in Hincl.
+ set f := bf !! k â‹… f'. (* the complete frame *)
+ change (bf !! k â‹… f') with f in Hincl.
+ destruct (Hdq n (option_map fst f)) as (dq'' & HPdq'' & Hvdq'').
+ { destruct Hincl as [Heq _]. simpl in Heq. rewrite Heq in Hval.
+ destruct Hval as [Hval _]. by destruct f. }
+ eexists. split; first by exists dq''.
intros j [df va] Heq.
destruct (decide (k = j)) as [->|Hne].
- - rewrite lookup_op lookup_singleton in Heq. exists v'.
- destruct (bf !! j) as [[dfbf vabf]|] eqn:Hbf.
- + rewrite Hbf -Some_op -pair_op in Heq. by simplify_eq.
- + rewrite Hbf right_id in Heq. by simplify_eq.
+ - rewrite lookup_op lookup_singleton in Heq.
+ eexists v', (dq'' â‹…? (fst <$> f)).
+ split; first done. split.
+ + split; last by apply Hval. simpl. done.
+ + rewrite -Heq. exists f'.
+ rewrite -assoc. change (bf !! j â‹… f') with f.
+ destruct Hincl as [_ Hincl]. simpl in Hincl. rewrite Hincl.
+ by destruct f.
- rewrite lookup_op lookup_singleton_ne // left_id in Heq.
eapply Hrel. rewrite lookup_op lookup_singleton_ne // left_id Heq //.
Qed.
@@ -452,46 +543,46 @@ Section lemmas.
Qed.
(** Typeclass instances *)
- Global Instance gmap_view_frag_core_id k dq v : CoreId dq → CoreId (gmap_view_frag k dq v).
+ Global Instance gmap_view_frag_core_id k dq v :
+ CoreId dq → CoreId v → CoreId (gmap_view_frag k dq v).
Proof. apply _. Qed.
- Global Instance gmap_view_cmra_discrete : OfeDiscrete V → CmraDiscrete (gmap_viewR K V).
+ Global Instance gmap_view_cmra_discrete : CmraDiscrete V → CmraDiscrete (gmap_viewR K V).
Proof. apply _. Qed.
- Global Instance gmap_view_frag_mut_is_op dq dq1 dq2 k v :
+ Global Instance gmap_view_frag_mut_is_op dq dq1 dq2 k v v1 v2 :
IsOp dq dq1 dq2 →
- IsOp' (gmap_view_frag k dq v) (gmap_view_frag k dq1 v) (gmap_view_frag k dq2 v).
- Proof. rewrite /IsOp' /IsOp => ->. apply gmap_view_frag_op. Qed.
+ IsOp v v1 v2 →
+ IsOp' (gmap_view_frag k dq v) (gmap_view_frag k dq1 v1) (gmap_view_frag k dq2 v2).
+ Proof. rewrite /IsOp' /IsOp => -> ->. apply gmap_view_frag_op. Qed.
End lemmas.
(** Functor *)
-Program Definition gmap_viewURF (K : Type) `{Countable K} (F : oFunctor) : urFunctor := {|
- urFunctor_car A _ B _ := gmap_viewUR K (oFunctor_car F A B);
+Program Definition gmap_viewURF (K : Type) `{Countable K} (F : rFunctor) : urFunctor := {|
+ urFunctor_car A _ B _ := gmap_viewUR K (rFunctor_car F A B);
urFunctor_map A1 _ A2 _ B1 _ B2 _ fg :=
- viewO_map (rel:=gmap_view_rel K (oFunctor_car F A1 B1))
- (rel':=gmap_view_rel K (oFunctor_car F A2 B2))
- (gmapO_map (K:=K) (oFunctor_map F fg))
- (gmapO_map (K:=K) (prodO_map cid (agreeO_map (oFunctor_map F fg))))
+ viewO_map (rel:=gmap_view_rel K (rFunctor_car F A1 B1))
+ (rel':=gmap_view_rel K (rFunctor_car F A2 B2))
+ (gmapO_map (K:=K) (rFunctor_map F fg))
+ (gmapO_map (K:=K) (prodO_map cid (rFunctor_map F fg)))
|}.
Next Obligation.
intros K ?? F A1 ? A2 ? B1 ? B2 ? n f g Hfg.
apply viewO_map_ne.
- - apply gmapO_map_ne, oFunctor_map_ne. done.
+ - apply gmapO_map_ne, rFunctor_map_ne. done.
- apply gmapO_map_ne. apply prodO_map_ne; first done.
- apply agreeO_map_ne, oFunctor_map_ne. done.
+ apply rFunctor_map_ne. done.
Qed.
Next Obligation.
intros K ?? F A ? B ? x; simpl in *. rewrite -{2}(view_map_id x).
apply (view_map_ext _ _ _ _)=> y.
- rewrite /= -{2}(map_fmap_id y).
apply map_fmap_equiv_ext=>k ??.
- apply oFunctor_map_id.
+ apply rFunctor_map_id.
- rewrite /= -{2}(map_fmap_id y).
apply map_fmap_equiv_ext=>k [df va] ?.
split; first done. simpl.
- rewrite -{2}(agree_map_id va).
- eapply agree_map_ext; first by apply _.
- apply oFunctor_map_id.
+ apply rFunctor_map_id.
Qed.
Next Obligation.
intros K ?? F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x; simpl in *.
@@ -499,13 +590,11 @@ Next Obligation.
apply (view_map_ext _ _ _ _)=> y.
- rewrite /= -map_fmap_compose.
apply map_fmap_equiv_ext=>k ??.
- apply oFunctor_map_compose.
+ apply rFunctor_map_compose.
- rewrite /= -map_fmap_compose.
apply map_fmap_equiv_ext=>k [df va] ?.
split; first done. simpl.
- rewrite -agree_map_compose.
- eapply agree_map_ext; first by apply _.
- apply oFunctor_map_compose.
+ apply rFunctor_map_compose.
Qed.
Next Obligation.
intros K ?? F A1 ? A2 ? B1 ? B2 ? fg; simpl.
@@ -515,34 +604,43 @@ Next Obligation.
rewrite !lookup_fmap.
destruct (f !! k) as [[df' va']|] eqn:Hfk; rewrite Hfk; last done.
simpl=>[= <- <-].
- specialize (Hrel _ _ Hfk). simpl in Hrel. destruct Hrel as (v & Hagree & Hdval & Hm).
- exists (oFunctor_map F fg v).
- rewrite Hm. split; last by auto.
- rewrite Hagree. rewrite agree_map_to_agree. done.
+ specialize (Hrel _ _ Hfk). simpl in Hrel. destruct Hrel as (v & dq & Hlookup & Hval & Hincl).
+ eexists (rFunctor_map F fg v), dq.
+ rewrite Hlookup. split; first done. split.
+ - split; first by apply Hval. simpl. apply: cmra_morphism_validN. apply Hval.
+ - destruct Hincl as [[[fdq fv]|] Hincl].
+ + apply: Some_includedN_mono. rewrite -Some_op in Hincl.
+ apply (inj _) in Hincl. rewrite -pair_op in Hincl.
+ exists (fdq, rFunctor_map F fg fv). rewrite -pair_op.
+ split; first apply Hincl. rewrite -cmra_morphism_op.
+ simpl. f_equiv. apply Hincl.
+ + exists None. rewrite right_id in Hincl. apply (inj _) in Hincl.
+ rewrite right_id. f_equiv. split; first apply Hincl.
+ simpl. f_equiv. apply Hincl.
Qed.
Global Instance gmap_viewURF_contractive (K : Type) `{Countable K} F :
- oFunctorContractive F → urFunctorContractive (gmap_viewURF K F).
+ rFunctorContractive F → urFunctorContractive (gmap_viewURF K F).
Proof.
intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg.
apply viewO_map_ne.
- - apply gmapO_map_ne. apply oFunctor_map_contractive. done.
+ - apply gmapO_map_ne. apply rFunctor_map_contractive. done.
- apply gmapO_map_ne. apply prodO_map_ne; first done.
- apply agreeO_map_ne, oFunctor_map_contractive. done.
+ apply rFunctor_map_contractive. done.
Qed.
-Program Definition gmap_viewRF (K : Type) `{Countable K} (F : oFunctor) : rFunctor := {|
- rFunctor_car A _ B _ := gmap_viewR K (oFunctor_car F A B);
+Program Definition gmap_viewRF (K : Type) `{Countable K} (F : rFunctor) : rFunctor := {|
+ rFunctor_car A _ B _ := gmap_viewR K (rFunctor_car F A B);
rFunctor_map A1 _ A2 _ B1 _ B2 _ fg :=
- viewO_map (rel:=gmap_view_rel K (oFunctor_car F A1 B1))
- (rel':=gmap_view_rel K (oFunctor_car F A2 B2))
- (gmapO_map (K:=K) (oFunctor_map F fg))
- (gmapO_map (K:=K) (prodO_map cid (agreeO_map (oFunctor_map F fg))))
+ viewO_map (rel:=gmap_view_rel K (rFunctor_car F A1 B1))
+ (rel':=gmap_view_rel K (rFunctor_car F A2 B2))
+ (gmapO_map (K:=K) (rFunctor_map F fg))
+ (gmapO_map (K:=K) (prodO_map cid (rFunctor_map F fg)))
|}.
Solve Obligations with apply gmap_viewURF.
Global Instance gmap_viewRF_contractive (K : Type) `{Countable K} F :
- oFunctorContractive F → rFunctorContractive (gmap_viewRF K F).
+ rFunctorContractive F → rFunctorContractive (gmap_viewRF K F).
Proof. apply gmap_viewURF_contractive. Qed.
Global Typeclasses Opaque gmap_view_auth gmap_view_frag.
diff --git a/iris/algebra/view.v b/iris/algebra/view.v
index bdd151537b121c697f5a04d5c688016a4c8bbaf4..93026bb89accc7fc1fd91cbab3a3cdc02f87c8dc 100644
--- a/iris/algebra/view.v
+++ b/iris/algebra/view.v
@@ -484,6 +484,12 @@ Section cmra.
(** 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'.
diff --git a/iris/base_logic/algebra.v b/iris/base_logic/algebra.v
index 4478c58049cb479b242681c960c3f2620c0b231b..88b5b47c60cc4ed608bc2ea088114cbdc0354428 100644
--- a/iris/base_logic/algebra.v
+++ b/iris/base_logic/algebra.v
@@ -1,5 +1,6 @@
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.
@@ -298,24 +299,24 @@ Section upred.
End dfrac_agree.
Section gmap_view.
- Context {K : Type} `{Countable K} {V : ofe}.
+ Context {K : Type} `{Countable K} {V : cmra}.
Implicit Types (m : gmap K V) (k : K) (dq : dfrac) (v : V).
- Lemma gmap_view_both_validI m k dq v :
- ✓ (gmap_view_auth (DfracOwn 1) m ⋅ gmap_view_frag k dq v) ⊢
- ✓ dq ∧ m !! k ≡ Some v.
+ Lemma gmap_view_both_validI dp m k dq v :
+ ✓ (gmap_view_auth dp m ⋅ gmap_view_frag k dq v) ⊣⊢
+ ⌜✓ dp⌠∧ ∃ v' dq', ⌜m !! k = Some v'⌠∧ ✓ (dq', v') ∧ Some (dq, v) ≼ Some (dq', v').
Proof.
- rewrite /gmap_view_auth /gmap_view_frag. apply view_both_validI_1.
- intros n a. uPred.unseal. apply gmap_view.gmap_view_rel_lookup.
+ rewrite /gmap_view_auth /gmap_view_frag. apply: view_both_dfrac_validI.
+ intros n a. rewrite /internal_included. uPred.unseal. apply gmap_view.gmap_view_rel_lookup.
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.
+ ⌜✓ (dq1 ⋅ dq2)⌠∧ ✓ (v1 ⋅ v2).
Proof.
rewrite /gmap_view_frag -view_frag_op. apply view_frag_validI=> n x.
rewrite gmap_view.gmap_view_rel_exists singleton_op singleton_validN.
- rewrite -pair_op pair_validN to_agree_op_validN. by uPred.unseal.
+ rewrite -pair_op pair_validN. by uPred.unseal.
Qed.
End gmap_view.