diff --git a/src/Iris/Algebra.lean b/src/Iris/Algebra.lean index 2fc931d7..af74986d 100644 --- a/src/Iris/Algebra.lean +++ b/src/Iris/Algebra.lean @@ -3,3 +3,6 @@ import Iris.Algebra.CMRA import Iris.Algebra.COFESolver import Iris.Algebra.OFE import Iris.Algebra.Frac +import Iris.Algebra.Heap +import Iris.Algebra.View +import Iris.Algebra.HeapView diff --git a/src/Iris/Algebra/Agree.lean b/src/Iris/Algebra/Agree.lean index 21c3f51b..dc53683a 100644 --- a/src/Iris/Algebra/Agree.lean +++ b/src/Iris/Algebra/Agree.lean @@ -233,6 +233,41 @@ theorem Agree.includedN {x y : Agree α} : x ≼{n} y ↔ y ≡{n}≡ y • x := theorem Agree.included {x y : Agree α} : x ≼ y ↔ y ≡ y • x := ⟨fun ⟨z, h⟩ n => includedN.mp ⟨z, h n⟩, fun h => ⟨y, h.trans op_comm⟩⟩ +theorem Agree.toAgree.is_discrete {a : α} (Ha : OFE.DiscreteE a) : OFE.DiscreteE (toAgree a) := by + refine ⟨fun ⟨Hal, Har⟩ _ => ?_⟩ + constructor <;> simp_all [toAgree] + · rcases Hal with ⟨b, Hb1, Hb2⟩ + exact ⟨b, ⟨Hb1, Ha.discrete (Har b Hb1) |>.dist⟩⟩ + · intro H Hb + exact Ha.discrete (Har H Hb) |>.dist + +open OFE OFE.Discrete in +instance [OFE α] [Discrete α] : Discrete (Agree α) where + discrete_0 {x y} H := by + refine fun n => ⟨fun a Ha => ?_, fun b Hb => ?_⟩ + · rcases H.1 a Ha with ⟨c, Hc⟩ + refine ⟨c, ⟨Hc.1, ?_⟩⟩ + apply equiv_dist.mp <| discrete_0 (Hc.2.le <| Nat.zero_le 0) + · rcases H.2 b Hb with ⟨c, Hc⟩ + refine ⟨c, ⟨Hc.1, ?_⟩⟩ + apply equiv_dist.mp <| discrete_0 (Hc.2.le <| Nat.zero_le 0) + +instance toAgree.ne [OFE α] : OFE.NonExpansive (toAgree : α → Agree α) where + ne n x y H := by + refine ⟨?_, ?_⟩ + · intro a Ha; exists y; revert Ha + simp [toAgree]; exact (·▸H) + · intro b Hb; exists x; revert Hb + simp [toAgree]; exact (·▸H) + +theorem toAgree.inj {a1 a2 : α} {n} (H : toAgree a1 ≡{n}≡ toAgree a2) : a1 ≡{n}≡ a2 := by + have Hinc : a1 ∈ (toAgree a1).car := by simp [toAgree] + rcases H.1 a1 Hinc with ⟨_, ⟨_, _⟩⟩ + simp_all [toAgree] + +instance : CMRA.IsTotal (Agree α) where + total := by simp [CMRA.pcore] + theorem Agree.valid_includedN {x y : Agree α} : ✓{n} y → x ≼{n} y → x ≡{n}≡ y := by intro hval ⟨z, heq⟩ have : ✓{n} (x • z) := heq.validN.mp hval @@ -354,4 +389,9 @@ theorem Agree.agree_map_ext {g : α → β} [OFE.NonExpansive g] (heq : ∀ a, f · exact ⟨g a, ⟨a, ha, rfl⟩, (heq a).dist⟩ · exact ⟨f a, ⟨a, ha, rfl⟩, (heq a).dist⟩ +theorem toAgree.incN {a b : α} {n} : toAgree a ≼{n} toAgree b ↔ a ≡{n}≡ b := by + refine ⟨?_, fun H => (CMRA.incN_iff_right <| toAgree.ne.ne H).mp <| CMRA.incN_refl _⟩ + intro H + apply toAgree.inj + exact Agree.valid_includedN trivial H end agree_map diff --git a/src/Iris/Algebra/CMRA.lean b/src/Iris/Algebra/CMRA.lean index dd726f91..3a5e6908 100644 --- a/src/Iris/Algebra/CMRA.lean +++ b/src/Iris/Algebra/CMRA.lean @@ -183,6 +183,7 @@ theorem op_opM_assoc (x y : α) (mz : Option α) : (x • y) •? mz ≡ x • ( theorem op_opM_assoc_dist (x y : α) (mz : Option α) : (x • y) •? mz ≡{n}≡ x • (y •? mz) := by unfold op?; cases mz <;> simp [assoc.dist, Dist.symm] + /-! ## Validity -/ theorem Valid.validN : ✓ (x : α) → ✓{n} x := (valid_iff_validN.1 · _) @@ -1098,6 +1099,10 @@ theorem CMRA.op_some_opM_assoc (x y : α) (mz : Option α) : (x • y) •? mz | none => .rfl | some _ => assoc.symm +theorem CMRA.opM_opM_assoc {x : α} {y z : Option α} : (x •? y) •? z ≡ x •? (y • z) := by + cases y <;> cases z <;> simp [CMRA.op?, CMRA.op, optionOp] + exact assoc.symm + theorem CMRA.op_some_opM_assoc_dist (x y : α) (mz : Option α) : (x • y) •? mz ≡{n}≡ x •? (some y • mz) := match mz with @@ -1116,7 +1121,7 @@ theorem CMRA.inc_of_some_inc_some [CMRA.IsTotal α] {x y : α} (h : some y ≼ s | none => ⟨core y, (CMRA.equiv_of_some_equiv_some hmz).trans (op_core y).symm⟩ | some z => ⟨z, hmz⟩ -theorem CMRA.incN_of_some_incN_some [CMRA.IsTotal α] {x y : α} : some y ≼{n} some x → y ≼{n} x +theorem CMRA.incN_of_Option.some_incN_some_iff_some [CMRA.IsTotal α] {x y : α} : some y ≼{n} some x → y ≼{n} x | ⟨none, hmz⟩ => ⟨core y, (CMRA.dist_of_some_dist_some hmz).trans (op_core_dist y).symm⟩ | ⟨some z, hmz⟩ => ⟨z, hmz⟩ @@ -1134,6 +1139,163 @@ theorem not_valid_some_exclN_op_left {n} {x : α} [CMRA.Exclusive x] {y : α} : theorem validN_op_unit {n} {x : Option α} (vx : ✓{n} x) : ✓{n} x • CMRA.unit := by cases x <;> trivial +theorem Option.inc_iff {ma mb : Option α} : + ma ≼ mb ↔ ma = none ∨ ∃ a b, ma = some a ∧ mb = some b ∧ (a ≡ b ∨ a ≼ b) := by + constructor + · rintro ⟨mc, Hmc⟩ + cases ma <;> cases mb <;> cases mc <;> simp_all [CMRA.op, optionOp] + · exact .inl Hmc.symm + · right; rename_i v3; exists v3 + · rintro (H|⟨a, b, Ha, Hb, (H|⟨z, Hz⟩)⟩) + · subst H; exists mb; simp [CMRA.op, optionOp] + · subst Ha; subst Hb; exists none; simp [CMRA.op, optionOp]; exact H.symm + · subst Ha; subst Hb; exists some z + +theorem Option.incN_iff {ma mb : Option α} : + ma ≼{n} mb ↔ ma = none ∨ ∃ a b, ma = some a ∧ mb = some b ∧ (a ≡{n}≡ b ∨ a ≼{n} b) := by + constructor + · rintro ⟨mc, Hmc⟩ + cases ma <;> cases mb <;> cases mc <;> simp_all [CMRA.op, optionOp] + · exact .inl Hmc.symm + · right; rename_i v3; exists v3 + · rintro (H|⟨a, b, Ha, Hb, (H|⟨z, Hz⟩)⟩) + · subst H; exists mb; simp [CMRA.op, optionOp] + · subst Ha; subst Hb; exists none; simp [CMRA.op, optionOp]; exact H.symm + · subst Ha; subst Hb; exists some z + +theorem Option.inc_iff_isTotal [CMRA.IsTotal α] {ma mb : Option α} : + ma ≼ mb ↔ ma = none ∨ ∃ a b, ma = some a ∧ mb = some b ∧ a ≼ b := by + apply Option.inc_iff.trans _ + constructor + · rintro (H|⟨a, b, Ha, Hb, (H|H)⟩) + · exact .inl H + · right + refine ⟨a, b, Ha, Hb, ?_⟩ + exists (CMRA.core a) + exact H.symm.trans (CMRA.op_core a).symm + · exact .inr ⟨a, b, Ha, Hb, H⟩ + · rintro (H|⟨a, b, Ha, Hb, H⟩) + · exact .inl H + · exact .inr ⟨a, b, Ha, Hb, .inr H⟩ + +theorem Option.incN_iff_isTotal [CMRA.IsTotal α] {ma mb : Option α} : + ma ≼{n} mb ↔ ma = none ∨ ∃ a b, ma = some a ∧ mb = some b ∧ a ≼{n} b := by + apply Option.incN_iff.trans _ + constructor + · rintro (H|⟨a, b, Ha, Hb, (H|H)⟩) + · exact .inl H + · right + refine ⟨a, b, Ha, Hb, ?_⟩ + exists (CMRA.core a) + apply H.symm.trans (CMRA.op_core_dist a).symm + · exact .inr ⟨a, b, Ha, Hb, H⟩ + · rintro (H|⟨a, b, Ha, Hb, H⟩) + · exact .inl H + · exact .inr ⟨a, b, Ha, Hb, .inr H⟩ + +theorem Option.some_incN_some_iff {a b : α} : some a ≼{n} some b ↔ a ≡{n}≡ b ∨ a ≼{n} b := by + apply Option.incN_iff.trans; simp + +-- Here +theorem Option.some_inc_some_iff {a b : α} : some a ≼ some b ↔ a ≡ b ∨ a ≼ b := by + apply Option.inc_iff.trans; simp + +theorem Option.eqv_of_inc_exclusive [CMRA.Exclusive (a : α)] {b : α} (H : some a ≼ some b) (Hv : ✓ b) : + a ≡ b := by + rcases Option.inc_iff.mp H with (H|⟨a', b', Ha, Hb, H⟩); simp at H + simp only [Option.some.injEq] at Ha Hb; subst Ha; subst Hb + rcases H with (H|H); trivial + exact (CMRA.not_valid_of_excl_inc H Hv).elim + +theorem Option.dst_of_inc_exclusive [CMRA.Exclusive (a : α)] {b : α} (H : some a ≼{n} some b) (Hv : ✓{n} b) : + a ≡{n}≡ b := by + rcases Option.incN_iff.mp H with (H|⟨a', b', Ha, Hb, H⟩); simp at H + simp only [Option.some.injEq] at Ha Hb; subst Ha; subst Hb + rcases H with (H|H); trivial + exact (CMRA.not_valid_of_exclN_inc H Hv).elim + +theorem Option.some_inc_some_iff_isTotal [CMRA.IsTotal α] {a b : α} : some a ≼ some b ↔ a ≼ b := by + apply Option.some_inc_some_iff.trans + refine ⟨?_, .inr⟩ + rintro (H|H) + · exists (CMRA.core a) + exact H.symm.trans (CMRA.op_core a).symm + · exact H + +theorem Option.some_incN_some_iff_isTotal [CMRA.IsTotal α] {a b : α} : some a ≼{n} some b ↔ a ≼{n} b := by + apply Option.some_incN_some_iff.trans + refine ⟨?_, .inr⟩ + rintro (H|H) + · exists (CMRA.core a) + exact H.symm.trans (CMRA.op_core_dist a).symm + · exact H + +instance {a : α} [Hid : CMRA.IdFree a] [Hc : CMRA.Cancelable a] : CMRA.Cancelable (some a) := by + constructor + rintro n (_|b) (_|c) _ HE + · trivial + · rename_i h + simp [CMRA.op, optionOp] at HE + exact Hid.id_free0_r c (CMRA.valid0_of_validN h) (HE.symm.le (n.zero_le)) + · rename_i h + simp [CMRA.op, optionOp] at HE + apply Hid.id_free0_r b + · simp [CMRA.op, optionOp, CMRA.ValidN, optionValidN] at h + apply CMRA.valid0_of_validN + exact (Dist.validN HE).mp h + · apply Dist.le HE (n.zero_le) + · simp [OFE.Dist, Option.Forall₂] + apply Hc.cancelableN + · rename_i h; exact h + · apply HE + +instance (ma : Option α) [Hid : ∀ a : α, CMRA.IdFree a] [Hc : ∀ a : α, CMRA.Cancelable a] : + CMRA.Cancelable ma := by + cases ma + constructor + · simp [CMRA.op, optionOp] + · infer_instance + +-- Weird that replacing this proof with the #print-ed term doesn't work for some reason +theorem Option.validN_of_incN_validN {a b : α} (Hv : ✓{n} a) (Hinc : some b ≼{n} some a) : ✓{n} b := by + apply CMRA.validN_of_incN Hinc + apply Hv + +-- Same, can't replace with #print-ed term +theorem Option.valid_of_inc_valid {a b : α} (Hv : ✓ a) (Hinc : some b ≼ some a) : ✓ b := by + apply CMRA.valid_of_inc Hinc + apply Hv + +theorem Option.some_inc_some_iff_op? {a b : α} : some a ≼ some b ↔ ∃ mc, b ≡ a •? mc := by + simp [Option.inc_iff] + constructor + · rintro (H|H) + · exists none; simpa [CMRA.op?] using H.symm + · rcases H with ⟨mc', H⟩ + exists (some mc') + · rintro ⟨(_|z), H⟩ + · exact .inl H.symm + · right; exists z + +theorem Option.some_incN_some_iff_op? {a b : α} : some a ≼{n} some b ↔ ∃ mc, b ≡{n}≡ a •? mc := by + simp [Option.incN_iff] + constructor + · rintro (H|H) + · exists none; simpa [CMRA.op?] using H.symm + · rcases H with ⟨mc', H⟩ + exists (some mc') + · rintro ⟨(_|z), H⟩ + · exact .inl H.symm + · right; exists z + +instance [CMRA.Discrete α] : CMRA.Discrete (Option α) where + discrete_valid {x} := by + cases x <;> simp [CMRA.Valid, optionValid] + exact (CMRA.discrete_valid ·) + +theorem Option.some_op_op? {a : α} {ma : Option α} : some a • ma = some (a •? ma) := by + cases ma <;> simp [CMRA.op?, CMRA.op, optionOp] + end option section unit @@ -1232,6 +1394,12 @@ theorem valid_snd {x : α × β} (h : ✓ x) : ✓ x.snd := h.right theorem validN_fst {n} {x : α × β} (h : ✓{n} x) : ✓{n} x.fst := h.left theorem validN_snd {n} {x : α × β} (h : ✓{n} x) : ✓{n} x.snd := h.right +instance [CMRA.Discrete α] [CMRA.Discrete β]: CMRA.Discrete (α × β) where + discrete_valid := by + rintro ⟨_, _⟩ + simp [CMRA.ValidN] + exact (⟨CMRA.discrete_valid ·, CMRA.discrete_valid ·⟩) + end Prod section optionOF diff --git a/src/Iris/Algebra/DFrac.lean b/src/Iris/Algebra/DFrac.lean index e578e167..6cadc8fa 100644 --- a/src/Iris/Algebra/DFrac.lean +++ b/src/Iris/Algebra/DFrac.lean @@ -7,6 +7,8 @@ Authors: Markus de Medeiros, Mario Carneiro import Iris.Algebra.CMRA import Iris.Algebra.OFE import Iris.Algebra.Frac +import Iris.Algebra.Updates +import Iris.Algebra.LocalUpdates namespace Iris @@ -138,4 +140,66 @@ theorem valid_discard : ✓ (discard : DFrac F) := by simp [CMRA.Valid, valid] theorem valid_own_op_discard {q : F} : ✓ own q • discard ↔ Fractional q := by simp [CMRA.op, op, CMRA.Valid, valid] +instance : CMRA.Discrete (DFrac F) where + discrete_valid {x} := by simp [CMRA.Valid, CMRA.ValidN] + +theorem DFrac.is_discrete {q : DFrac F} : OFE.DiscreteE q := ⟨congrArg id⟩ + +instance : CMRA.Discrete (DFrac F) where + discrete_valid {x} := by simp [CMRA.Valid, CMRA.ValidN] + +instance : CMRA.Discrete (DFrac F) where + discrete_valid {x} := by simp [CMRA.Valid, CMRA.ValidN] + +-- dfrac_discard_update +theorem DFrac.update_discard {dq : DFrac F} : dq ~~> .discard := by + rintro n (_|⟨q|_|q⟩) H <;> + have H' := (CMRA.valid_iff_validN' n).mpr H <;> + apply (CMRA.valid_iff_validN' n).mp <;> + simp [CMRA.op?] at H' ⊢ + · simp [CMRA.Valid, valid] + · cases dq + · exact valid_op_own H + · exact H + · exact valid_op_own H + · simp [CMRA.Valid, valid, CMRA.op, op] + · cases dq + · exact CMRA.valid_op_right _ _ H + · exact H + · exact CMRA.valid_op_right _ _ H + +-- dfrac_undiscard_update +theorem DFrac.update_acquire [IsSplitFraction F] : + (.discard : DFrac F) ~~>: fun k => ∃ q, k = .own q := by + apply UpdateP.discrete.mpr + rintro (_|⟨q|_|q⟩) + · rintro _ + exists (.own One.one) + refine ⟨⟨One.one, rfl⟩, ?_⟩ + simp [CMRA.op?, CMRA.op, op, CMRA.Valid, valid, add_comm] + apply UFraction.one_whole.1 + · rintro ⟨q', HP⟩ + exists (.own q') + refine ⟨⟨q', rfl⟩, ?_⟩ + simp [CMRA.op?, CMRA.op, op, CMRA.Valid, valid, add_comm] + exact HP + · intro _ + let q' : F := (IsSplitFraction.split One.one).1 + exists (.own q') + refine ⟨⟨q', rfl⟩, ?_⟩ + simp [CMRA.op?, CMRA.op, op, CMRA.Valid, valid] + exists (IsSplitFraction.split One.one).2 + rw [IsSplitFraction.split_add] + apply UFraction.one_whole.1 + · rintro ⟨q', HP⟩ + let q'' : F := (IsSplitFraction.split q').1 + exists (.own q'') + refine ⟨⟨q'', rfl⟩, ?_⟩ + simp [CMRA.op?, CMRA.op, op, CMRA.Valid, valid] + rw [add_comm] + exists (IsSplitFraction.split q').2 + rw [← add_assoc] + rw [IsSplitFraction.split_add] + exact HP + end dfrac diff --git a/src/Iris/Algebra/Frac.lean b/src/Iris/Algebra/Frac.lean index 59be0f53..3f94d905 100644 --- a/src/Iris/Algebra/Frac.lean +++ b/src/Iris/Algebra/Frac.lean @@ -27,6 +27,10 @@ class Fraction (α : Type _) extends Add α where add_ne : ∀ {a b : α}, a ≠ b + a proper_add_mono_left : ∀ {a b : α}, Proper (a + b) → Proper a +class IsSplitFraction (α : Type _) [Fraction α] where + split : α → α × α + split_add {a : α} : (split a).1 + (split a).2 = a + namespace Fraction /-- A fraction does not represent the entire resource. diff --git a/src/Iris/Algebra/Heap.lean b/src/Iris/Algebra/Heap.lean new file mode 100644 index 00000000..1db3bfa6 --- /dev/null +++ b/src/Iris/Algebra/Heap.lean @@ -0,0 +1,596 @@ +/- +Copyright (c) 2025 Markus de Medeiros. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Markus de Medeiros +-/ + +import Iris.Algebra.CMRA +import Iris.Algebra.OFE + +open Iris + +/-! ## Generic heaps + +Note: There are three definitions of equivalence in this file + +[1] OFE.Equiv (pointwise equvalence) +[2] StoreO.Equiv (pointwise equality of .get) +[3] Eq (equality of representations) + +[3] -> [2] -> [1] always +[1] -> [2] when the value type is Leibniz +[2] -> [3] when the store is an IsoFunStore +-/ + +-- TODO: Move this to a generic set theory library +def set_disjoint {X : Type _} (S1 S2 : X → Prop) : Prop := ∀ x : X, ¬(S1 x ∧ S2 x) +def set_union {X : Type _} (S1 S2 : X → Prop) : X → Prop := fun x => S1 x ∨ S2 x +def set_included {X : Type _} (S1 S2 : X → Prop) : Prop := ∀ x, S1 x → S2 x + +/-- The type `T` can store and retrieve keys of type `K` and obtain values of type `V`. -/ +class Store (T : Type _) (K V : outParam (Type _)) where + get : T → K → V + set : T → K → V → T + get_set_eq {t k k' v} : k = k' → get (set t k v) k' = v + get_set_ne {t k k' v} : k ≠ k' → get (set t k v) k' = get t k' +export Store (get set get_set_eq get_set_ne) + +open Classical in +theorem Store.get_set [Store T K V] {t : T} {k k' : K} {v : V} : + get (set t k v) k' = if k = k' then v else get t k' := by + split <;> rename_i h + · exact get_set_eq h + · exact get_set_ne h + +/-- An index-dependent predicate holds at every member of the store. -/ +def Store.all [Store T K V] (P : K → V → Prop) : T → Prop := + fun t => ∀ k, P k (get t k) + +/-- Two Stores are pointwise equivalent. -/ +@[simp] def Store.Equiv [Store T K V] (t1 t2 : T) : Prop := get t1 = get t2 + +instance Store.Equiv_trans [Store T K V] : Trans Equiv (Equiv (T := T)) Equiv := ⟨by simp_all⟩ + +/-- RepFunStore: The type T can represent all functions that satisfy Rep. +For instance, this holds with `rep _ = True` when `T = K → V`. On the other hand, when +`T = list (K × Option V)` representing a partial function with an association list, this holds +when `rep f` is the predicate that says `f` has finite domain. -/ +class RepFunStore (T : Type _) (K V : outParam (Type _)) [Store T K V] where + rep : (K → V) → Prop + rep_get (t : T) : rep (get t) + ofFun : { f : K → V // rep f } → T + get_ofFun: get (ofFun f) = f +export RepFunStore (rep rep_get ofFun get_ofFun) + +/-- IsoFunStore: The type T is isomorphic the type of functions `{f : Rep f}`, or in other words, +equality of T is the same as equality of `{f : Rep f}`. -/ +class IsoFunStore (T : Type _) (K V : outParam (Type _)) [Store T K V] extends RepFunStore T K V where + ofFun_get {t : T} : ofFun ⟨get t, rep_get t⟩ = t +export IsoFunStore (ofFun_get) + +theorem IsStoreIso.ext [Store T K V] [IsoFunStore T K V] {t1 t2 : T} + (H : ∀ k, get t1 k = get t2 k) : t1 = t2 := by + rw [← ofFun_get (t := t1), ← ofFun_get (t := t2)] + congr 2; exact funext H + +/-- [2] → [3] -/ +theorem IsoFunStore.store_eq_of_Equiv [Store T K V] [IsoFunStore T K V] {t1 t2 : T} : + Store.Equiv t1 t2 → t1 = t2 := (IsStoreIso.ext <| fun k => congrFun · k) + +/-- Stores of type T1 can be coerced to stores of type T2. -/ +class HasStoreMap (T1 T2 : Type _) (K V1 V2 : outParam (Type _)) [Store T1 K V1] [Store T2 K V2] where + /-- Map a function that depends on the elemet across the entire structure -/ + dmap (f : K → V1 → V2) : T1 → T2 + get_dmap : get (dmap f t) k = f k (get t k) +export HasStoreMap (dmap get_dmap) + +/-- Map between heaps that preserves non-allocations. -/ +class HasHHMap (T1 T2 : Type _) (K V1 V2 : outParam (Type _)) + [Store T1 K (Option V1)] [Store T2 K (Option V2)] where + hhmap (f : K → V1 → Option V2) : T1 → T2 + hhmap_get (f : K → V1 → Option V2) : get (hhmap f t) k = (get t k).bind (f k) +export HasHHMap (hhmap hhmap_get) + +def HasStoreMap.map (f : V1 → V2) [Store T1 K V1] [Store T2 K V2] [HasStoreMap T1 T2 K V1 V2] : T1 → T2 := + HasStoreMap.dmap (fun (_ : K) => f) + +class Heap (T : Type _) (K V : outParam (Type _)) extends Store T K (Option V) where + empty : T + hmap (f : K → V → Option V) : T → T + merge (op : V → V → V) : T → T → T + get_empty : get empty k = none + get_hmap : get (hmap f t) k = (get t k).bind (f k) + get_merge : get (merge op t1 t2) k = Option.merge op (get t1 k) (get t2 k) +export Heap (empty hmap merge get_empty get_hmap get_merge) + +theorem hmap_alloc [Heap T K V] {t : T} (H : get t k = some v) : get (hmap f t) k = f k v := by + simp [get_hmap, bind, H] + +theorem hmap_unalloc [Heap T K V] {t : T} (H : get t k = none) : get (hmap f t) k = none := by + simp [get_hmap, bind, H] + +/-- The heap of a single point -/ +def Heap.point [Heap T K V] (k : K) (v : Option V) : T := set empty k v + +/-- Delete an element from a heap by setting its value to .none -/ +def Heap.delete [Heap T K V] (t : T) (k : K) : T := set t k none + +/-- The domain of a heap is the set of keys that map to .some values. -/ +def Heap.dom [Heap T K V] (t : T) : K → Prop := fun k => (get t k).isSome + +@[simp] def Heap.union [Heap T K V] : T → T → T := merge (fun v _ => v) + +theorem Heap.point_get_eq [Heap T K V] (H : k = k') : get (point k v : T) k' = v := by + rw [point, get_set_eq H] + +theorem Heap.point_get_ne [Heap T K V] (H : k ≠ k') : get (point k v : T) k' = none := by + rw [point, get_set_ne H, get_empty] + +open Classical in +theorem Heap.get_point [Heap T K V] {k k' : K} {v : Option V} : + get (point k v : T) k' = if k = k' then v else .none := by + split <;> rename_i h + · exact point_get_eq h + · exact point_get_ne h + +/-- An AllocHeap is a heap which can allocate elements under some condition. -/ +class AllocHeap (T : Type _) (K V : outParam (Type _)) extends Heap T K V where + notFull : T → Prop + fresh {t : T} : notFull t → K + get_fresh {H : notFull t} : get t (fresh H) = none +export AllocHeap (notFull fresh get_fresh) + +/-- An UnboundeHeap is a heap which can allocate an unbounded number of elements starting at empty. -/ +class UnboundedHeap (T : Type _) (K V : outParam (Type _)) extends AllocHeap T K V where + notFull_empty : notFull (empty : T) + notFull_set_fresh {H : notFull t} : notFull (set t (fresh H) v) +export UnboundedHeap (notFull_empty notFull_set_fresh) + +section ofe +open OFE + +instance Store.instOFE [Store T K V] [OFE V] : OFE T where + Equiv s0 s1 := get s0 ≡ get s1 + Dist n s0 s1 := get s0 ≡{n}≡ get s1 + dist_eqv := ⟨fun _ => .of_eq rfl, (·.symm), (·.trans ·)⟩ + equiv_dist := equiv_dist + dist_lt := dist_lt + +@[simp] def Store.toMap [Store T K V] [OFE V] : T -n> (K → V) where + f x := get x + ne.1 {_ _ _} H k := H k + +@[simp] def Store.ofMap [Store T K V] [R : RepFunStore T K V] [OFE V] : {f : K → V // R.rep f} -n> T where + f x := ofFun x + ne.1 {_ _ _} H k := by rw [get_ofFun, get_ofFun]; exact H k + +instance get_ne [Store T K V] [OFE V] (k : K) : NonExpansive (get · k : T → V) where + ne {_ _ _} Ht := Ht k + +instance [Store T K V] [OFE V] (k : K) : NonExpansive₂ (set · k · : T → V → T) where + ne {_ _ _} Hv {_ _} Ht k' := by + if h : k = k' + then rw [get_set_eq h, get_set_eq h]; exact Ht + else rw [get_set_ne h, get_set_ne h]; exact Hv k' + +theorem Store.eqv_of_Equiv [OFE V] [Store T K V] {t1 t2 : T} (H : Equiv t1 t2) : t1 ≡ t2 := + (.of_eq <| congrFun H ·) + +instance [Heap T K V] [OFE V] (op : V → V → V) [NonExpansive₂ op] : + NonExpansive₂ (merge (T := T) op) where + ne _ {_ _} Ht {_ _} Hs k := by + simp only [get_merge] + exact NonExpansive₂.ne (Ht k) (Hs k) + +instance [Store T1 K V1] [Store T2 K V2] [OFE V1] [OFE V2] (f : K → V1 → V2) + [∀ k, NonExpansive (f k)] [HasStoreMap T1 T2 K V1 V2] : NonExpansive (dmap f : T1 → T2) where + ne _ {_ _} H k := by simp only [get_dmap]; exact NonExpansive.ne (H k) + +/-- Project a chain of stores through it's kth coordinate to a chain of values. -/ +def Store.chain [Store T K V] [OFE V] (k : K) (c : Chain T) : Chain V where + chain i := get (c i) k + cauchy Hni := c.cauchy Hni k + +theorem Store.chain_get [Store T K V] [OFE V] (k : K) (c : Chain T) : + (chain k c) i = get (c i) k := by + simp [chain] + +open Store in +instance Heap.instCOFE [Heap T K V] [COFE V] : COFE T where + compl c := hmap (fun _ => COFE.compl <| c.map ⟨_, get_ne ·⟩) (c 0) + conv_compl {_ c} k := by + rw [get_hmap] + rcases H : get (c.chain 0) k + · rw [← chain_get, chain_none_const (c := chain k c) (n := 0) (H▸rfl)]; rfl + · exact IsCOFE.conv_compl + +end ofe + +section cmra +open CMRA + +/- ## A CMRA on Heaps -/ + +variable [Heap T K V] [CMRA V] + +@[simp] def Store.op (s1 s2 : T) : T := merge (K := K) CMRA.op s1 s2 +@[simp] def Store.unit : T := empty +@[simp] def Store.pcore (s : T) : Option T := some <| hmap (fun _ => CMRA.pcore) s +@[simp] def Store.valid (s : T) : Prop := ∀ k, ✓ (get s k : Option V) +@[simp] def Store.validN (n : Nat) (s : T) : Prop := ∀ k, ✓{n} (get s k : Option V) + +theorem lookup_incN {n} {m1 m2 : T} : + (∃ (z : T), m2 ≡{n}≡ Store.op m1 z) ↔ + ∀ i, (∃ z, (get m2 i) ≡{n}≡ (get m1 i) • z) := by + refine ⟨fun ⟨z, Hz⟩ i => ?_, fun H => ?_⟩ + · refine ⟨get z i, ?_⟩ + refine .trans (get_ne i |>.ne Hz) ?_ + simp only [Store.op, op, optionOp, get_merge] + cases get m1 i <;> cases get z i <;> simp + · obtain ⟨f, Hf⟩ := Classical.axiomOfChoice H + exists hmap (fun k _ => f k) m2 + refine fun i => (Hf i).trans ?_ + specialize Hf i; revert Hf + simp [CMRA.op, optionOp, get_merge, get_hmap] + cases get m2 i <;> cases get m1 i <;> cases f i <;> simp + +theorem lookup_inc {m1 m2 : T} : + (∃ (z : T), m2 ≡ Store.op m1 z) ↔ + ∀ i, (∃ z, (Store.get m2 i) ≡ (Store.get m1 i) • z) := by + refine ⟨fun ⟨z, Hz⟩ i => ?_, fun H => ?_⟩ + · refine ⟨get z i, ?_⟩ + refine .trans (get_ne i |>.eqv Hz) ?_ + simp only [Store.op, op, optionOp, get_merge] + cases get m1 i <;> cases get z i <;> simp + · obtain ⟨f, Hf⟩ := Classical.axiomOfChoice H + exists hmap (fun k _ => f k) m2 + refine fun i => (Hf i).trans ?_ + specialize Hf i; revert Hf + simp [CMRA.op, optionOp, get_merge, get_hmap] + cases get m2 i <;> cases get m1 i <;> cases f i <;> simp + +open OFE in +instance instStoreCMRA : CMRA T where + pcore := Store.pcore + op := Store.op + ValidN := Store.validN + Valid := Store.valid + op_ne.ne _ x1 x2 H i := by + specialize H i; revert H; rename_i x _ + simp [op, get_merge] + cases get x1 i <;> cases get x2 i <;> cases get x i <;> simp + apply op_right_dist + pcore_ne {n x y _} H := by + simp only [Store.pcore, Option.some.injEq, exists_eq_left'] + refine (· ▸ fun k => ?_); specialize H k; revert H + rw [get_hmap, get_hmap] + cases Store.get x k <;> cases Store.get y k <;> simp + exact (NonExpansive.ne ·) + validN_ne Hx H k := + validN_ne (NonExpansive.ne (f := (Store.get · k : T → Option V)) Hx) (H k) + valid_iff_validN := + ⟨fun H n k => valid_iff_validN.mp (H k) n, + fun H k => valid_iff_validN.mpr (H · k)⟩ + validN_succ H k := validN_succ (H k) + validN_op_left {n x1 x2} H k := by + refine validN_op_left (y := Store.get x2 k) ?_ + specialize H k; revert H + simp only [Store.op, get_merge, Option.merge] + cases get x1 k <;> cases get x2 k <;> simp [optionOp, op] + assoc {x y z} k := by + simp only [Store.op, get_merge] + cases Store.get x k <;> cases Store.get y k <;> cases Store.get z k <;> simp + exact assoc + comm {x y} k := by + simp [Store.op, Heap.get_merge] + cases Store.get x k <;> cases Store.get y k <;> simp + exact comm + pcore_op_left {x cx} H k := by + simp only [← Option.getD_some (a := cx) (b := cx), Store.op, get_merge] + cases Hcx : Store.get cx k <;> cases hx : Store.get x k <;> simp <;> + simp only [Store.pcore, Option.some.injEq] at H + · rw [← H, hmap_unalloc hx] at Hcx + cases Hcx + · apply pcore_op_left + rw [← Hcx, ← H, hmap_alloc hx] + pcore_idem {x cx} H := by + simp only [Store.pcore, Option.some.injEq] at H + change (Store.pcore cx |>.getD cx) ≡ cx + intro k + simp [← H, get_hmap] + rcases Store.get x k with (_|v) <;> simp + cases HY : pcore v; simp + exact pcore_idem HY + pcore_op_mono := by + apply pcore_op_mono_of_core_op_mono + rintro x cx y ⟨z, Hz⟩ + suffices ∃ z, (Store.pcore y |>.getD y) ≡ Store.op (Store.pcore x |>.getD x) z by + rintro Hx + simp only [Store.pcore, Option.some.injEq, Store.op, exists_eq_left'] + rcases this with ⟨z', Hz'⟩ + exists z' + refine .trans Hz' (fun i => ?_) + cases get z' i <;> cases get x i <;> simp_all + refine lookup_inc.mpr (fun i => ?_) + obtain ⟨v', Hv'⟩ : (core (Store.get x i)) ≼ (core (Store.get y i)) := by + apply core_mono + exists get z i + have Hz := Hz i; revert Hz + simp [CMRA.op, optionOp, get_merge] + cases get x i <;> cases get z i <;> simp_all + exists v' + simp_all [core, pcore, optionCore, get_hmap] + extend {n x y1 y2} Hm Heq := by + have Hslice i : Store.get x i ≡{n}≡ Store.get y1 i • Store.get y2 i := by + refine (get_ne i |>.ne Heq).trans ?_ + simp [CMRA.op, get_merge, optionOp] + cases get y1 i <;> cases get y2 i <;> simp + let extendF (i : K) := CMRA.extend (Hm i) (Hslice i) + exists hmap (fun k (_ : V) => extendF k |>.fst) y1 + exists hmap (fun k (_ : V) => extendF k |>.snd.fst) y2 + simp [Store.op, get_merge] + refine ⟨fun i => ?_, fun i => ?_, fun i => ?_⟩ + all_goals rcases hF : extendF i with ⟨z1, z2, Hm, Hz1, Hz2⟩ + · refine Hm.trans ?_ + simp [Store.op, get_merge, hF, CMRA.op, optionOp] + cases z1 <;> cases z2 <;> cases h1 : get y1 i <;> cases h2 : get y2 i <;> simp [h1, h2] at Hz1 Hz2 + · rw [hmap_unalloc h1, hmap_unalloc h2]; simp + · rw [hmap_unalloc h1, hmap_alloc h2, hF]; simp + · rw [hmap_alloc h1, hmap_unalloc h2, hF]; simp + · rw [hmap_alloc h1, hmap_alloc h2, hF]; simp + · cases h : Store.get y1 i + · rw [hmap_unalloc h] + · rw [hmap_alloc h, ← h, hF]; exact Hz1 + · cases h : Store.get y2 i + · rw [hmap_unalloc h] + · rw [hmap_alloc h, ← h, hF]; exact Hz2 + +instance instStoreUCMRA : UCMRA T where + unit := Store.unit + unit_valid := by + simp [CMRA.Valid, Store.valid, optionValid, Store.unit, get_empty] + unit_left_id _ := by + simp [CMRA.op, Heap.get_merge, Store.unit, get_empty] + pcore_unit _ := by + simp [Store.unit, hmap_unalloc get_empty, get_empty] + +end cmra + +namespace Heap + +variable {K V : Type _} [Heap T K V] [CMRA V] +open CMRA Store + +theorem validN_get_validN {m : T} (Hv : ✓{n} m) (He : get m i ≡{n}≡ some x) : ✓{n} x := by + specialize Hv i; revert Hv + rcases h : get m i <;> simp [h] at He + exact OFE.Dist.validN He |>.mp + +theorem valid_get_valid {m : T} (Hv : ✓ m) (He : get m i ≡ some x) : ✓ x := + valid_iff_validN.mpr (fun _ => validN_get_validN Hv.validN He.dist) + +theorem insert_validN {m : T} (Hx : ✓{n} x) (Hm : ✓{n} m) : ✓{n} (set m i x) := by + intro k + rw [get_set]; split; rename_i He + · exact Hx + · apply Hm + +theorem insert_valid {m : T} (Hx : ✓ x) (Hm : ✓ m) : ✓ (set m i x) := + valid_iff_validN.mpr (fun _ => insert_validN Hx.validN Hm.validN) + +theorem point_valid_iff : ✓ (point i x : T) ↔ ✓ x := by + refine ⟨fun H => ?_, fun H k => ?_⟩ + · specialize H i; rw [point_get_eq rfl] at H; trivial + · rw [get_point]; split <;> trivial + +theorem point_validN_iff : ✓{n} (point i x : T) ↔ ✓{n} x := by + refine ⟨fun H => ?_, fun H k => ?_⟩ + · specialize H i; rw [point_get_eq rfl] at H; trivial + · rw [get_point]; split <;> trivial + +theorem delete_validN {m : T} (Hv : ✓{n} m) : ✓{n} (delete m i) := by + intro k + rw [delete, get_set]; split + · trivial + · exact Hv k + +theorem delete_valid {m : T} (Hv : ✓ m) : ✓ (delete m i) := + valid_iff_validN.mpr (fun _ => delete_validN Hv.validN) + +theorem set_equiv_point_op_point {m : T} (Hemp : get m i = none) : Equiv (set m i x) (point i x • m) := by + refine funext (fun k => ?_) + simp [CMRA.op, Store.op, Equiv, get_merge, Option.merge, get_point, Hemp, get_set] + split <;> rename_i He + · rw [← He, Hemp]; cases x <;> rfl + · cases (Store.get m k) <;> rfl + +theorem set_eq_point_op_point [IsoFunStore T K (Option V)] {m : T} (Hemp : get m i = none) : + set m i x = point i x • m := + IsoFunStore.store_eq_of_Equiv (set_equiv_point_op_point Hemp) + +theorem core_point_equiv {i : K} {x : V} {cx} (Hpcore : pcore x = some cx) : + Equiv (T := T) (core <| point i (some x)) (point i (some cx)) := by + refine funext fun k => ?_ + simp [← Hpcore, core, CMRA.pcore, get_point, get_hmap] + split <;> rfl + +theorem point_core_eq [IsoFunStore T K (Option V)] {i : K} {x : V} {cx} (Hpcore : pcore x = some cx) : + core (point (T := T) i (some x)) = point i (some cx) := + IsoFunStore.store_eq_of_Equiv (core_point_equiv Hpcore) + +theorem point_core_eqv {i : K} {x : V} {cx} (Hpcore : pcore x ≡ some cx) : + core (point (T := T) i (some x)) ≡ point i (some cx) := by + intro k + simp [core, CMRA.pcore, get_point, get_hmap] + split <;> trivial + +theorem point_core_total [IsTotal V] {i : K} {x : V} : + Equiv (core <| point (T := T) i (some x)) ((point i (some (core x)))) := by + obtain ⟨_, Hxc⟩ := total x + apply (core_point_equiv Hxc).trans + simp [core, Hxc] + +theorem point_core_total_eq [IsTotal V] [IsoFunStore T K (Option V)] {i : K} {x : V} : + core (point (T := T) i (some x)) = point i (some (core x)) := + IsoFunStore.store_eq_of_Equiv point_core_total + +theorem point_op_point {i : K} {x y : V} : + Equiv ((point (T := T) i (some x)) • (point i (some y))) ((point i (some (x • y)))) := by + refine funext fun k => ?_ + simp only [CMRA.op, Store.op, get_merge, get_point] + split <;> simp [Option.merge] + +theorem point_op_point_eq [IsoFunStore T K (Option V)] {i : K} {x y : V} : + (point (T := T) i (some x)) • (point i (some y)) = (point i (some (x • y))) := + IsoFunStore.store_eq_of_Equiv point_op_point + +instance {m : T} [∀ x : V, CoreId x] : CoreId m where + core_id i := by + rw [get_hmap] + cases Store.get m i <;> simp + exact core_id + +instance [CoreId (x : V)] : CoreId (point (T := T) i (some x)) where + core_id k := by + simp [get_hmap, get_point] + split <;> simp + exact core_id + +theorem point_incN_iff {m : T} : + (point (T := T) i (some x)) ≼{n} m ↔ ∃ y, (get m i ≡{n}≡ some y) ∧ some x ≼{n} some y := by + refine ⟨fun ⟨z, Hz⟩ => ?_, fun ⟨y, Hy, z, Hz⟩ => ?_⟩ + · specialize Hz i; revert Hz + simp only [CMRA.op, Store.op, get_merge, point_get_eq rfl] + rcases get z i with (_|v) + · intro _ + exists x + · refine (⟨x • v, ·, ?_⟩) + exists v + · exists set m i z + intro j + simp [CMRA.op, get_merge, get_point, get_set] + split <;> rename_i He + · refine (He ▸ Hy).trans (Hz.trans ?_) + cases z <;> simp [CMRA.op, optionOp] + · simp + +theorem point_inc_iff {m : T} : + (point i (T := T) (some x)) ≼ m ↔ ∃ y, (get m i ≡ some y) ∧ some x ≼ some y := by + refine ⟨fun ⟨z, Hz⟩ => ?_, fun ⟨y, Hy, z, Hz⟩ => ?_⟩ + · specialize Hz i; revert Hz + simp only [CMRA.op, Store.op, get_merge, point_get_eq rfl] + rcases get z i with (_|v) + · intro _ + exists x + · refine (⟨x • v, ·, ?_⟩) + exists v + · exists set m i z + intro j + simp [CMRA.op, get_merge, get_point, get_set] + split <;> rename_i He + · refine (He ▸ Hy).trans (Hz.trans ?_) + cases z <;> simp [CMRA.op, optionOp] + · simp + +theorem exclusive_point_inc_iff {m : T} (He : Exclusive x) (Hv : ✓ m) : + (point i (T := T) (some x)) ≼ m ↔ (get m i ≡ some x) := by + refine point_inc_iff.trans ⟨fun ⟨y, Hy, Hxy⟩ => ?_, fun _ => ?_⟩ + · suffices x ≡ y by exact Hy.trans <| this.symm + exact Option.eqv_of_inc_exclusive Hxy <| valid_get_valid Hv Hy + · exists x + +theorem point_inc_point_iff : (point i (T := T) (some x)) ≼ (point i (some y)) ↔ some x ≼ some y := by + refine point_inc_iff.trans ⟨fun ⟨z, Hz, Hxz⟩ => ?_, fun H => ?_⟩ + · refine inc_of_inc_of_eqv Hxz ?_ + refine .trans Hz.symm ?_ + exact .of_eq <| point_get_eq rfl + · refine ⟨y, ?_, H⟩ + exact .of_eq <| point_get_eq rfl + +theorem total_point_inc_point_iff [IsTotal V] : (point i (T := T) (some x)) ≼ (point i (some y)) ↔ x ≼ y := + point_inc_point_iff.trans <| Option.some_inc_some_iff_isTotal + +theorem point_inc_point_mono (Hinc : x ≼ y) : (point (T := T) i (some x)) ≼ (point i (some y)) := + point_inc_point_iff.mpr <| Option.some_inc_some_iff.mpr <| .inr Hinc + +instance [H : Cancelable (some x)] : Cancelable (point (T := T) i (some x)) where + cancelableN {n m1 m2} Hv He j := by + specialize Hv j; revert Hv + specialize He j; revert He + simp only [CMRA.op, Store.op, get_merge, Option.merge, get_point] + if He : i = j + then + simp_all only [↓reduceIte] + intro Hv He + cases _ : get m1 j <;> cases _ : get m2 j + all_goals apply H.cancelableN + all_goals simp_all [CMRA.op, Store.op, optionOp] + else + cases get m1 j <;> cases get m2 j + all_goals simp_all [CMRA.op, optionOp] + +instance {m : T} [Hid : ∀ x : V, IdFree x] [Hc : ∀ x : V, Cancelable x] : Cancelable m where + cancelableN {n m1 m2} Hv He i := by + apply cancelableN (x := get m i) + · specialize Hv i; revert Hv + simp [CMRA.op, Store.op, Heap.get_merge, optionOp] + cases _ : get m i <;> cases _ : get m1 i <;> simp_all + · specialize He i; revert He + simp [Heap.get_merge, CMRA.op, Store.op, optionOp] + cases get m i <;> cases get m1 i <;> cases get m2 i <;> simp_all [Heap.get_merge] + +theorem insert_op_equiv {m1 m2 : T} : + Equiv ((set (V := Option V) (m1 • m2) i (x • y))) (set m1 i x • set m2 i y) := by + refine funext fun j => ?_ + if He : i = j + then + simp [CMRA.op, get_set_eq He, get_merge, optionOp] + cases x <;> cases y <;> simp_all + else + simp [CMRA.op, get_set_ne (T := T) He, get_merge] + +theorem insert_op_eq [IsoFunStore T K (Option V)] {m1 m2 : T} : + (set (V := Option V) (m1 • m2) i (x • y)) = (set m1 i x • set m2 i y) := + IsoFunStore.store_eq_of_Equiv insert_op_equiv + +theorem disjoint_op_equiv_union {m1 m2 : T} (Hd : set_disjoint (dom m1) (dom m2)) : + Equiv (m1 • m2) (union m1 m2) := by + refine funext fun j => ?_ + simp [CMRA.op, Store.op, Heap.get_merge] + rcases _ : get m1 j <;> cases _ : get m2 j <;> simp_all + refine (Hd j ?_).elim + simp_all [dom] + +theorem disjoint_op_eq_union [IsoFunStore T K (Option V)] {m1 m2 : T} (H : set_disjoint (dom m1) (dom m2)) : + m1 • m2 = Heap.union m1 m2 := + IsoFunStore.store_eq_of_Equiv (disjoint_op_equiv_union H) + +theorem valid0_disjoint_dom {m1 m2 : T} (Hv : ✓{0} (m1 • m2)) (H : ∀ {k x}, get m1 k = some x → Exclusive x) : + set_disjoint (dom m1) (dom m2) := by + rintro k + simp only [dom, Option.isSome] + rcases HX : get m1 k with (_|x) <;> simp + rcases HY : get m2 k with (_|y) <;> simp + apply (H HX).1 y + simp [CMRA.op, CMRA.ValidN] at Hv; specialize Hv k; revert Hv + simp [Heap.get_merge, optionValidN, HX, HY] + +theorem valid_disjoint_dom {m1 m2 : T} (Hv : ✓ (m1 • m2)) (H : ∀ {k x}, get m1 k = some x → Exclusive x) : + set_disjoint (dom m1) (dom m2) := + valid0_disjoint_dom (Valid.validN Hv) H + +theorem dom_op_union (m1 m2 : T) : dom (m1 • m2) = set_union (dom m1) (dom m2) := by + refine funext fun k => ?_ + cases get m1 k <;> cases get m2 k <;> simp_all [CMRA.op, dom, set_union, get_merge] + +theorem inc_dom_inc {m1 m2 : T} (Hinc : m1 ≼ m2) : set_included (dom m1) (dom m2) := by + intro i; unfold Heap.dom + rcases lookup_inc.mp Hinc i with ⟨z, Hz⟩; revert Hz + cases get m1 i <;> cases get m2 i <;> cases z <;> + simp [CMRA.op, optionOp] + +nonrec instance [HD : CMRA.Discrete V] [Heap T K V] : Discrete T where + discrete_0 {_ _} H := (OFE.Discrete.discrete_0 <| H ·) + discrete_valid {_} := (CMRA.Discrete.discrete_valid <| · ·) + +end Heap diff --git a/src/Iris/Algebra/HeapView.lean b/src/Iris/Algebra/HeapView.lean new file mode 100644 index 00000000..b5e1050d --- /dev/null +++ b/src/Iris/Algebra/HeapView.lean @@ -0,0 +1,764 @@ +/- +Copyright (c) 2025 Markus de Medeiros. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Markus de Medeiros +-/ + +import Iris.Algebra.Heap +import Iris.Algebra.View +import Iris.Algebra.DFrac +import Iris.Algebra.Frac + +open Iris + +section heap_view +open Heap + +variable (F K V : Type _) (H : Type _ → Type _) [UFraction F] [∀ V, Heap (H V) K V] [CMRA V] +variable [IHHmap : ∀ V, HasHHMap (H (DFrac F × V)) (H V) K (DFrac F × V) V] + +@[simp] def HeapR (n : Nat) (m : H V) (f : H ((DFrac F) × V)) : Prop := + ∀ k fv, Store.get f k = some fv → + ∃ (v : V) (dq : DFrac F), Store.get m k = .some v ∧ ✓{n} (dq, v) ∧ (some fv ≼{n} some (dq, v)) + +instance : ViewRel (HeapR F K V H) where + mono {n1 m1 f1 n2 m2 f2 Hrel Hm Hf Hn k} := by + intro vk Hk + obtain ⟨Hf'', _⟩ := lookup_incN (n := n2) (m1 := f2) (m2 := f1) + have Hf''' := Hf'' Hf k; clear Hf Hf'' + obtain Hf' : ∃ z, Store.get f1 k ≡{n2}≡ (some vk) • z := by + obtain ⟨z, Hz⟩ := Hf'''; exists z + apply Hz.trans + exact OFE.Dist.of_eq (congrFun (congrArg CMRA.op Hk) z) + clear Hf''' + cases h : Store.get f1 k + · exfalso + rw [h] at Hf' + obtain ⟨z, HK⟩ := Hf' + cases z <;> simp [CMRA.op, optionOp] at HK + rename_i val + rcases Heq : val with ⟨q', va'⟩ + rw [h, Heq] at Hf' + simp only [HeapR, Store.all] at Hrel + obtain ⟨v, dq, Hm1, ⟨Hvval, Hdqval⟩, Hvincl⟩ := Hrel k val h + have X : ∃ y : V, get m2 k = some y ∧ v ≡{n2}≡ y := by + simp_all + have Hmm := Hm1 ▸ Hm k + rcases h : Store.get m2 k with (_|y) <;> simp [h] at Hmm + exists y + obtain ⟨v', Hm2, Hv⟩ := X + exists v' + exists dq + refine ⟨Hm2, ⟨Hvval, ?_⟩, ?_⟩ + · exact CMRA.validN_ne Hv (CMRA.validN_of_le Hn Hdqval) + · suffices some vk ≼{n2} some (dq, v) by + apply CMRA.incN_of_incN_of_dist this + refine ⟨rfl, Hv⟩ + apply CMRA.incN_trans + · apply Hf' + apply CMRA.incN_trans _ (CMRA.incN_of_incN_le Hn Hvincl) + rw [Heq] + rel_validN := by + intro n m f Hrel k + rcases Hf : Store.get f k with (_|⟨dqa, va⟩) + · simp [CMRA.ValidN, optionValidN] + · simp only [HeapR, Store.all] at Hrel + obtain ⟨v, dq, Hmval, Hvval, Hvincl⟩ := Hf ▸ Hrel k _ Hf + rw [Hf] at Hvincl + refine CMRA.validN_of_incN Hvincl ?_ + exact Hvval + rel_unit n := by + exists Heap.empty + intro k + simp [HeapR, Store.all, UCMRA.unit, Store.unit, Heap.get_empty] + +omit IHHmap in +theorem view_rel_unit : HeapR F K V H n m UCMRA.unit := by + simp [HeapR, Store.all, UCMRA.unit, Heap.get_empty] + +theorem HeapR.exists_iff_validN n f : (∃ m, HeapR F K V H n m f) ↔ ✓{n} f := by + constructor + · rintro ⟨m, Hrel⟩ + exact ViewRel.rel_validN _ _ _ Hrel + intro Hv + let FF : (K → (DFrac F × V) → Option V) := fun k _ => (Store.get f k).bind (fun x => some x.2) + exists ((IHHmap V).hhmap FF f) + simp [HeapR, Store.all] + intro k + cases h : Store.get f k <;> simp [] + rename_i val + rintro a b rfl + exists b + simp [hhmap_get, h, FF] + exists a + refine ⟨?_, CMRA.incN_refl _⟩ + have Hv' := h ▸ Hv k + exact Hv' + +omit IHHmap in +theorem HeapR.point_get_iff n m k dq v : + HeapR F K V H n m (Heap.point k <| .some (dq, v)) ↔ + ∃ (v' : V) (dq' : DFrac F), Store.get m k = some v' ∧ ✓{n} (dq', v') ∧ some (dq, v) ≼{n} some (dq', v') := by + constructor + · intro Hrel + have Hrel' := Hrel k (dq, v) + simp only [HeapR, Store.all, Heap.point, Store.get_set_eq] at Hrel' + obtain ⟨v', dq', Hlookup, Hval, Hinc⟩ := Hrel' trivial + exists v'; exists dq' + · rintro ⟨v', dq', Hlookup, Hval, _⟩ j + simp only [HeapR, Store.all, Heap.point] + if h : k = j + then + simp [Store.get_set_eq h] + exists v' + refine ⟨h ▸ Hlookup, ?_⟩ + exists dq' + else simp [Store.get_set_ne h, Heap.get_empty] + +instance [CMRA.Discrete V] : ViewRelDiscrete (HeapR F K V H) where + discrete n h H := by + simp [HeapR, Store.all] + intro H k a b He + have H' := H k a b He + obtain ⟨v, Hv1, ⟨x, Hx1, Hx2⟩⟩ := H' + refine ⟨v, Hv1, ⟨x, ?_, ?_⟩⟩ + · simp [CMRA.ValidN, Prod.ValidN] at Hx1 ⊢ + refine ⟨Hx1.1, ?_⟩ + apply CMRA.valid_iff_validN.mp + apply CMRA.Discrete.discrete_valid + exact Hx1.2 + · exact (CMRA.inc_0_iff_incN n).mp Hx2 + +abbrev HeapView := View F (HeapR F K V H) + +end heap_view + +section heap_view_laws + +variable {F K V : Type _} {H : Type _ → Type _} [UFraction F] [∀ V, Heap (H V) K V] [CMRA V] +variable [IHHmap : ∀ V, HasHHMap (H (DFrac F × V)) (H V) K (DFrac F × V) V] + +/-- Authoratative (fractional) ownership over an entire heap. -/ +def HeapView.Auth (dq : DFrac F) (m : H V) : HeapView F K V H := ●V{dq} m + +/-- Fragmental (fractional) ownership over an allocated element in the heap. -/ +def HeapView.Frag (k : K) (dq : DFrac F) (v : V) : HeapView F K V H := + ◯V Heap.point k <| some (dq, v) + +/-- Fragmental (fractional) ownership over an element in the heap. -/ +def HeapView.Elem (k : K) (v : Option (DFrac F × V)) : HeapView F K V H := + ◯V Heap.point k v + +open OFE + +instance : NonExpansive (HeapView.Auth dq : _ → HeapView F K V H) := by apply View.auth_ne + +instance : NonExpansive (HeapView.Frag k dq : _ → HeapView F K V H) where + ne := by + intro i x1 x2 Hx + apply View.frag_ne.ne + intro k' + simp [Heap.point] + if h : k = k' + then simp [get_set_eq h]; exact dist_prod_ext rfl Hx + else simp [get_set_ne h] + +omit IHHmap in +theorem HeapView.auth_dfrac_op_eqv (dp dq : DFrac F) (m : H V) : + (HeapView.Auth (dp • dq) m) ≡ (HeapView.Auth dp m) • HeapView.Auth dq m := by + exact View.auth_op_eqv + +omit IHHmap in +theorem HeapView.dst_of_validN_auth_op n dp m1 dq m2 : + (✓{n} ((HeapView.Auth dp m1) : HeapView F K V H) • HeapView.Auth dq m2) → m1 ≡{n}≡ m2 := by + exact fun a => View.dst_of_validN_auth a + +omit IHHmap in +theorem HeapView.eqv_of_valid_auth_op dp m1 dq m2 : ✓ ((HeapView.Auth dp m1 : HeapView F K V H) • HeapView.Auth dq m2) → m1 ≡ m2 := by + exact fun a => View.eqv_of_valid_auth a + +omit IHHmap in +theorem HeapView.auth_validN_iff m n dq : ✓{n} (HeapView.Auth dq m : HeapView F K V H) ↔ ✓ (dq : DFrac F) := by + apply View.auth_validN_iff.trans + suffices ✓{n} dq ↔ ✓ dq by + apply and_iff_left_of_imp (fun _ => ?_) + apply view_rel_unit + exact Eq.to_iff rfl + +omit IHHmap in +theorem HeapView.auth_valid_iff m dq : ✓ (HeapView.Auth dq m : HeapView F K V H) ↔ ✓ dq := by + apply View.auth_valid_iff.trans + refine and_iff_left_of_imp (fun _ n => ?_) + exact view_rel_unit F K V H + +omit IHHmap in +theorem HeapView.auth_one_valid m : ✓ (HeapView.Auth (.own One.one) m : HeapView F K V H) := by + apply (HeapView.auth_valid_iff _ _).mpr valid_own_one + +omit IHHmap in +theorem HeapView.validN_auth_op_iff n dq1 dq2 m1 m2 : + ✓{n} ((HeapView.Auth dq1 m1 : HeapView F K V H) • HeapView.Auth dq2 m2) ↔ ✓ (dq1 • dq2) ∧ m1 ≡{n}≡ m2 := by + apply View.auth_op_auth_validN_iff.trans + refine and_congr_right (fun _ => ?_) + refine and_iff_left_of_imp (fun _ => ?_) + exact view_rel_unit F K V H + +omit IHHmap in +theorem HeapView.valid_auth_op_iff dq1 dq2 m1 m2 : + ✓ ((HeapView.Auth dq1 m1 : HeapView F K V H) • HeapView.Auth dq2 m2) ↔ ✓ (dq1 • dq2) ∧ m1 ≡ m2 := by + apply View.auth_op_auth_valid_iff.trans + refine and_congr_right (fun _ => ?_) + refine and_iff_left_of_imp (fun _ n => ?_) + exact view_rel_unit F K V H + +omit IHHmap in +theorem HeapView.auth_one_op_validN_iff n m1 m2 : ✓{n} ((HeapView.Auth (.own One.one) m1 : HeapView F K V H) • (HeapView.Auth (.own One.one) m2)) ↔ False := by + apply View.auth_one_op_validN_iff + +omit IHHmap in +theorem HeapView.auth_one_op_valid_iff m1 m2 : ✓ ((HeapView.Auth (.own One.one) m1 : HeapView F K V H) • HeapView.Auth (.own One.one) m2) ↔ False := by + apply View.auth_one_op_auth_one_valid_iff + +theorem HeapView.frag_validN_iff n k dq v : ✓{n} (HeapView.Frag k dq v : HeapView F K V H) ↔ ✓ dq ∧ ✓{n} v := by + apply View.frag_validN_iff.trans + apply (HeapR.exists_iff_validN F K V H _ _).trans + apply Heap.point_validN_iff + +theorem HeapView.frag_valid_iff k dq v : ✓ (HeapView.Frag k dq v : HeapView F K V H) ↔ ✓ dq ∧ ✓ v := by + suffices (∀ n, ✓{n} (HeapView.Frag k dq v : HeapView F K V H)) ↔ ✓ dq ∧ ✓ v by exact this + suffices (∀ n, ✓ dq ∧ ✓{n} v) ↔ ✓ dq ∧ ✓ v by + apply Iff.trans (forall_congr' (HeapView.frag_validN_iff · k dq v)) this + constructor + · refine fun H => ⟨?_, ?_⟩ + · apply CMRA.valid_iff_validN.mpr (H · |>.1) + · apply CMRA.valid_iff_validN.mpr (H · |>.2) + · rintro ⟨H1, H2⟩ n + refine ⟨?_, ?_⟩ + · apply CMRA.valid_iff_validN.mp H1 n + · apply CMRA.valid_iff_validN.mp H2 n + +omit IHHmap in +theorem HeapView.frag_op_eqv k dq1 dq2 v1 v2 : + (HeapView.Frag k (dq1 • dq2) (v1 • v2) : HeapView F K V H) ≡ + HeapView.Frag k dq1 v1 • HeapView.Frag k dq2 v2 := by + simp [HeapView.Frag] + rw [← View.frag_op_eq] + apply View.frag_ne.eqv + apply Store.eqv_of_Equiv + apply Store.Equiv_trans.trans _ Heap.point_op_point.symm + rfl + +omit IHHmap in +theorem HeapView.frag_add_op_eqv k q1 q2 v1 v2 : + (HeapView.Frag k (.own (q1 + q2)) (v1 • v2) : HeapView F K V H) ≡ + HeapView.Frag k (.own q1) v1 • HeapView.Frag k (.own q2) v2 := by + apply HeapView.frag_op_eqv + +theorem HeapView.frag_op_validN_iff n k dq1 dq2 v1 v2 : + ✓{n} ((HeapView.Frag k dq1 v1 : HeapView F K V H) • HeapView.Frag k dq2 v2) ↔ + ✓ (dq1 • dq2) ∧ ✓{n} (v1 • v2) := by + apply View.frag_validN_iff.trans + apply (HeapR.exists_iff_validN F K V H _ _ ).trans + apply Iff.trans + · apply CMRA.validN_iff + apply OFE.equiv_dist.mp + apply Store.eqv_of_Equiv + apply Heap.point_op_point + apply Heap.point_validN_iff.trans + apply Eq.to_iff rfl + +theorem HeapView.frag_op_valid_iff k dq1 dq2 v1 v2 : + ✓ ((HeapView.Frag k dq1 v1 : HeapView F K V H) • HeapView.Frag k dq2 v2) ↔ + ✓ (dq1 • dq2) ∧ ✓ (v1 • v2) := by + apply View.frag_valid_iff.trans + suffices (∀ (n : Nat), ✓{n} dq1 • dq2 ∧ ✓{n} v1 • v2) ↔ ✓ dq1 • dq2 ∧ ✓ v1 • v2 by + apply Iff.trans _ this + apply forall_congr' + intro n + apply (HeapR.exists_iff_validN F K V H _ _ ).trans + simp [HeapView.Frag] + apply Iff.trans + · apply CMRA.validN_iff + apply OFE.equiv_dist.mp + apply Store.eqv_of_Equiv + apply Heap.point_op_point + apply Heap.point_validN_iff.trans + apply Eq.to_iff rfl + constructor + · intro H + refine ⟨?_, ?_⟩ + · apply CMRA.valid_iff_validN.mpr <| fun n => (H n).1 + · apply CMRA.valid_iff_validN.mpr <| fun n => (H n).2 + · rintro ⟨H1, H2⟩ n + refine ⟨?_, ?_⟩ + · apply CMRA.valid_iff_validN.mp H1 + · apply CMRA.valid_iff_validN.mp H2 + + +omit IHHmap in +theorem HeapView.auth_op_frag_validN_iff n dp m k dq v : + ✓{n} ((HeapView.Auth dp m : HeapView F K V H) • HeapView.Frag k dq v) ↔ + ∃ v' dq', ✓ dp ∧ Store.get m k = some v' ∧ ✓{n} (dq', v') ∧ + some (dq, v) ≼{n} some (dq', v') := by + simp [HeapView.Auth, HeapView.Frag] + apply View.auth_op_frag_validN_iff.trans + refine and_congr_right (fun H1 => ?_) + refine (HeapR.point_get_iff _ _ _ _ _ _ _ _ _).trans ?_ + refine exists_congr (fun x => ?_) + exact exists_and_left + +omit IHHmap in +theorem HeapView.auth_op_frag_one_validN_iff n dp m k v : + ✓{n} ((HeapView.Auth dp m : HeapView F K V H) • HeapView.Frag k (.own One.one) v) ↔ + ✓ dp ∧ ✓{n} v ∧ Store.get m k ≡{n}≡ some v := by + apply (HeapView.auth_op_frag_validN_iff _ _ _ _ _ _).trans + constructor + · rintro ⟨Hdp, v', dq', Hlookup, Hvalid, Hincl⟩ + have Heq : v ≡{n}≡ Hdp := by + have Z := @Option.dst_of_inc_exclusive _ _ (DFrac.own One.one, v) n ?G _ Hincl Hvalid + case G => + -- TODO: This should be a DFrac lemma + constructor + rintro ⟨y1, y2⟩ + simp [CMRA.ValidN, CMRA.op] + intro H + exfalso + cases y1 <;> simp [valid, op] at H + · apply (UFraction.one_whole (α := F)).2 + rename_i f; exists f + · apply (UFraction.one_whole (α := F)).2 H + · apply (UFraction.one_whole (α := F)).2 + exact Fraction.Fractional.of_add_left H + exact Z.2 + refine ⟨dq', ?_, ?_⟩ + · simp [CMRA.ValidN, Prod.ValidN] at Hvalid + apply CMRA.validN_ne Heq.symm Hvalid.2 + · rw [Hlookup] + exact Heq.symm + · rintro ⟨Hdp, Hval, Hlookup⟩ + rcases h : Store.get m k with (_|v'); simp [h] at Hlookup + exists v'; exists (DFrac.own One.one) + refine ⟨Hdp, rfl, ?_, ?_⟩ + · simp [CMRA.ValidN, Prod.ValidN] + refine ⟨?_, ?_⟩ + · simp [valid] + apply (UFraction.one_whole (α := F)).1 + rw [h] at Hlookup + exact (Dist.validN (id (Dist.symm Hlookup))).mp Hval + · apply Option.some_incN_some_iff.mpr ?_ + left + apply dist_prod_ext rfl ?_ + exact id (Dist.symm (h.symm ▸ Hlookup : some _ ≡{n}≡ some _)) + +omit IHHmap in +theorem HeapView.auth_op_frag_validN_total_iff [CMRA.IsTotal V] n dp m k dq v : + ✓{n} ((HeapView.Auth dp m : HeapView F K V H) • HeapView.Frag k dq v) → + ∃ v', ✓ dp ∧ ✓ dq ∧ Store.get m k = some v' ∧ ✓{n} v' ∧ v ≼{n} v' := by + intro H; have H' := (HeapView.auth_op_frag_validN_iff _ _ _ _ _ _).mp H; clear H + obtain ⟨v', dq', Hdp, Hlookup, Hvalid, Hincl⟩ := H' + exists v' + refine ⟨Hdp, ?_, Hlookup, Hvalid.2, ?_⟩ + · suffices some dq ≼ some dq' by + refine Option.valid_of_inc_valid ?_ this + apply (CMRA.valid_iff_validN' n).mpr Hvalid.1 + apply (CMRA.inc_iff_incN n).mpr + rcases Hincl with ⟨x, Hx⟩ + rcases x with (_|x) <;> simp [CMRA.op, optionOp, Prod.op] at Hx + · apply CMRA.incN_of_incN_of_dist (CMRA.incN_refl _) + apply Hx.1.symm + · exists x.1 + simp [CMRA.op, optionOp] + apply Hx.1 + · suffices some v ≼{n} some v' by + apply CMRA.incN_of_Option.some_incN_some_iff_some this + refine Option.some_incN_some_iff_isTotal.mpr ?_ + rcases Hincl with ⟨x, Hx⟩ + rcases x with (_|x) <;> simp [CMRA.op, optionOp, Prod.op] at Hx + · apply CMRA.incN_of_incN_of_dist (CMRA.incN_refl _) + apply Hx.2.symm + · exists x.2 + apply Hx.2 + +omit IHHmap in +theorem HeapView.auth_op_frag_discrete_valid_iff [CMRA.Discrete V] dp m k dq v : + ✓ ((HeapView.Auth dp m : HeapView F K V H) • HeapView.Frag k dq v) ↔ + ∃ v' dq', ✓ dp ∧ Store.get m k = some v' ∧ ✓ (dq', v') ∧ some (dq, v) ≼ some (dq', v') := by + apply CMRA.valid_iff_validN.trans + apply Iff.trans + · apply forall_congr' + intro _ + apply HeapView.auth_op_frag_validN_iff + constructor + · intro Hvalid' + obtain ⟨v', dq', Hdp, Hlookup, Hvalid, Hincl⟩ := Hvalid' 0 + exists v'; exists dq' + refine ⟨Hdp, Hlookup, ?_, ?_⟩ + · refine ⟨?_, ?_⟩ + · apply CMRA.Discrete.discrete_valid + apply Hvalid.1 + · apply CMRA.Discrete.discrete_valid + apply Hvalid.2 + · exact (CMRA.inc_iff_incN 0).mpr Hincl + · rintro ⟨v', dq', Hdp, Hlookup, Hvalid, Hincl⟩ n + exists v'; exists dq' + refine ⟨Hdp, Hlookup, Hvalid.validN, (CMRA.inc_iff_incN n).mp Hincl⟩ + +omit IHHmap in +theorem HeapView.auth_op_frag_valid_total_discrete_iff [CMRA.IsTotal V] [CMRA.Discrete V] dp m k dq v : + ✓ ((HeapView.Auth dp m : HeapView F K V H) • HeapView.Frag k dq v) → + ∃ v', ✓ dp ∧ ✓ dq ∧ Store.get m k = some v' ∧ ✓ v' ∧ v ≼ v' := by + intro H + obtain ⟨v', dq', Hdp, Hlookup, Hvalid, Hincl⟩ := (HeapView.auth_op_frag_discrete_valid_iff _ _ _ _ _).mp H + exists v' + refine ⟨Hdp, ?_, Hlookup , ?_, ?_⟩ + · rcases Hincl with ⟨(_|x), Hx⟩ <;> simp [CMRA.op, optionOp, Prod.op] at Hx + · apply CMRA.valid_of_eqv Hx.1 + simp [CMRA.Valid, Prod.Valid] at Hvalid + apply Hvalid.1 + · suffices some dq ≼ some dq' by exact Option.valid_of_inc_valid Hvalid.1 this + exists x.fst + simp [CMRA.op, optionOp] + have Hx' := Hx.1 + exact Hx' + · exact Hvalid.2 + · rcases Hincl with ⟨(_|x), Hx⟩ <;> simp [CMRA.op, optionOp, Prod.op] at Hx + · simp [OFE.Equiv] at Hx + apply CMRA.inc_of_inc_of_eqv (CMRA.inc_refl _) + exact Hx.2.symm + · suffices some v ≼ some v' by + rcases this with ⟨z, Hz⟩ + rcases z with (_|z) <;> simp [CMRA.op, optionOp] at Hz + · apply CMRA.inc_of_inc_of_eqv + · apply CMRA.inc_refl + · apply Hz.symm + · exists z + exists x.snd + simp [CMRA.op, optionOp] + have Hx' := Hx.2 + exact Hx' + +omit IHHmap in +theorem HeapView.auth_op_frag_one_valid_iff m dp k v : + ✓ ((HeapView.Auth dp m : HeapView F K V H) • HeapView.Frag k (.own One.one) v) ↔ + ✓ dp ∧ ✓ v ∧ Store.get m k ≡ some v := by + apply CMRA.valid_iff_validN.trans + apply Iff.trans + · apply forall_congr' + intro _ + apply HeapView.auth_op_frag_one_validN_iff + constructor + · intro Hvalid + refine ⟨?_, ?_, ?_⟩ + · obtain ⟨Hdp, Hv, Hl⟩ := Hvalid 0 + exact Hdp + · apply CMRA.valid_iff_validN.mpr (fun n => ?_) + obtain ⟨Hdp, Hv, Hl⟩ := Hvalid n + exact Hv + · apply OFE.equiv_dist.mpr (fun n => ?_) + obtain ⟨Hdp, Hv, Hl⟩ := Hvalid n + exact Hl + · rintro ⟨Hdp, Hv, Hl⟩ n + refine ⟨Hdp, Hv.validN, Hl.dist⟩ + +instance [CMRA.CoreId dq] [CMRA.CoreId v] : + CMRA.CoreId (HeapView.Frag k dq v : HeapView F K V H) := by + rename_i H1 H2 + obtain ⟨H1⟩ := H1 + obtain ⟨H2⟩ := H2 + constructor + simp only [HeapView.Frag, CMRA.pcore] + simp only [View.Pcore, some_eqv_some] + refine NonExpansive₂.eqv trivial ?_ + refine Heap.point_core_eqv ?_ + simp [CMRA.pcore, Prod.pcore] + simp [CMRA.pcore] at H1 + simp [H1] + cases h : (CMRA.pcore v) <;> simp_all + refine ⟨rfl, ?_⟩ + exact H2 + +instance [CMRA.Discrete V] : CMRA.Discrete (HeapView F K V H) := by + infer_instance + +end heap_view_laws + +section heap_updates + +variable {F K V : Type _} {H : Type _ → Type _} [UFraction F] [∀ V, Heap (H V) K V] [CMRA V] + +theorem HeapView.update_one_alloc m k dq (v : V) : (Store.get m k = none) → ✓ dq → ✓ v → + HeapView.Auth (.own 1) m ~~> + ((HeapView.Auth (.own 1) (Store.set m k (.some v)) : HeapView F K V H) • HeapView.Frag k dq v) := by + intro Hfresh Hdq Hval + refine View.auth_one_alloc (fun n bf Hrel j => ?_ ) + simp [CMRA.op, get_merge, Option.merge] + if h : k = j + then + rw [Heap.point_get_eq h] + have Hbf : Store.get bf j = none := by + cases hc : Store.get bf j; rfl + simp [HeapR, Store.all] at Hrel + exfalso + rename_i val + have Hrel' := Hrel _ _ _ hc + rcases Hrel' with ⟨_, HK, _, _, _⟩ + subst h + simp [HK] at Hfresh + simp only [Hbf] + intro a b Hab + obtain ⟨rfl⟩ := Hab + exists v + rw [get_set_eq h] + refine ⟨rfl, ?_⟩ + exists dq + exact ⟨⟨Hdq, Hval.validN⟩, CMRA.incN_refl _⟩ + else + rw [Heap.point_get_ne h] + cases hc : Store.get bf j <;> simp only [] + · rintro _ _ ⟨⟩ + intro a b Hab + obtain ⟨rfl⟩ := Hab + simp [HeapR, Store.all] at Hrel + rcases Hrel j a b hc with ⟨v, He, q, Hv, Hframe, Hinc⟩ + rw [get_set_ne h] + exists v + refine ⟨He, ?_⟩ + exists q + refine ⟨Hv, ?_⟩ + exists Hframe + +theorem HeapView.update_one_delete m k (v : V) : + (HeapView.Auth (.own 1) m : HeapView F K V H) • (HeapView.Frag k (.own 1) v : HeapView F K V H) ~~> + HeapView.Auth (.own 1) (Heap.delete m k) := by + refine View.auth_one_op_frag_dealloc (fun n bf Hrel j => ?_) + cases He : Store.get bf j + · intro _ HK; simp at HK + if h : k = j + then + simp [HeapR, Store.all, CMRA.op, get_merge, Option.merge] at Hrel + have Hrel' := Hrel k; clear Hrel + simp [h, He, Heap.point_get_eq rfl] at Hrel' + obtain ⟨v, HK, q, Hqv, Hqinc⟩ := Hrel' + rename_i vv + have Hval := Option.validN_of_incN_validN (Hv := Hqv) (Hinc := Hqinc) + exfalso + obtain ⟨z, _⟩ := Hqinc + simp [CMRA.ValidN, Prod.op, Prod.ValidN] at Hval + have HK := Hval.1 + obtain ⟨(f|_|f), _⟩ := vv <;> simp [valid, CMRA.op, op] at HK + · apply (UFraction.one_whole (α := F)).2; exists f + · apply (UFraction.one_whole (α := F)).2; exact HK + · apply (UFraction.one_whole (α := F)).2 + exists f + exact Fraction.Fractional.proper HK + else + simp [HeapR, Store.all, CMRA.op, get_merge, Option.merge] at Hrel + have Hrel' := Hrel j; clear Hrel + simp [He, Heap.point_get_ne h] at Hrel' + rintro ⟨a, b⟩ Hab + obtain ⟨rfl⟩ := Hab + obtain ⟨v, H1, q, H2⟩ := Hrel' a b rfl + exists v + exists q + refine ⟨?_, H2⟩ + · unfold Heap.delete + rw [Store.get_set_ne h] + trivial + +theorem HeapView.update_auth_op_frag (m : H _) k (dq : DFrac F) (v mv' v': V) (dq' : DFrac F) : + (∀ (n : Nat) (mv : V) (f : Option (DFrac F × V)), + (Store.get m k = some mv) → + ✓{n} ((dq, v) •? f) → + (mv ≡{n}≡ ((v : V) •? (Prod.snd <$> f))) → + ✓{n} ((dq', v') •? f) ∧ (mv' ≡{n}≡ v' •? (Prod.snd <$> f))) → + ((HeapView.Auth (.own 1) m : HeapView F K V H) • (HeapView.Frag k dq v : HeapView F K V H)) ~~> + ((HeapView.Auth (.own 1) (Store.set m k (some mv')) : HeapView F K V H) • (HeapView.Frag k dq' v' : HeapView F K V H)) := by + intro Hup + apply View.auth_one_op_frag_update + rintro n bf Hrel j ⟨df, va⟩ + simp [CMRA.op, Heap.get_merge, Prod.op] + if h : k = j + then + simp [Heap.point, Store.get_set_eq h, Heap.get_empty] + intro Hbf + have Hrel' := Hrel k ((dq, v) •? (Store.get bf k)) + have Hrel'' := Hrel' ?G; clear Hrel' + case G=> + clear Hrel' + simp [CMRA.op, Heap.get_merge, Heap.point, Store.get_set_eq h, CMRA.op?] + cases h : Store.get bf k <;> simp [Option.merge, h, Store.get_set_eq rfl] + obtain ⟨mv, mdf, Hlookup, Hval, Hincl'⟩ := Hrel'' + obtain ⟨f', Hincl⟩ := Option.some_incN_some_iff_op?.mp Hincl'; clear Hincl' + let f := (Store.get bf k) • f' + have Hincl' : (mdf, mv) ≡{n}≡ (dq, v) •? f := by + refine .trans Hincl ?_ + apply OFE.Equiv.dist + apply CMRA.opM_opM_assoc + clear Hincl + have Hup' := Hup n mv f Hlookup (Hincl'.validN.mp Hval) ?G + case G=> + apply Hincl'.2.trans + match f with + | none => simp [CMRA.op?] + | some ⟨_, _⟩ => simp [CMRA.op?, CMRA.op] + obtain ⟨Hval', Hincl'⟩ := Hup' + exists ((dq' •? (Option.map Prod.fst f))) + refine ⟨?_, ?_⟩ + · apply CMRA.validN_ne (x := (dq' •? Option.map Prod.fst f, v' •? Prod.snd <$> f)) + · refine ⟨.rfl, Hincl'.symm⟩ + cases h : f <;> simp [CMRA.op?] + · exact CMRA.validN_opM Hval' + · simp [h, CMRA.op?, CMRA.op, Prod.op] at Hval' + exact Hval' + · rw [← Hbf] + suffices HF : some ((dq', v') •? (Store.get bf j)) ≼{n} some (dq' •? (Option.map Prod.fst f), mv') by + apply CMRA.incN_trans ?_ HF + simp [Option.merge, Prod.op, CMRA.op?] + cases h : Store.get bf j <;> simp + · exact CMRA.incN_refl _ + · exact CMRA.incN_refl _ + apply Option.some_incN_some_iff_op?.mpr + exists f' + refine OFE.Dist.trans (y := (dq' •? Option.map Prod.fst f, v' •? Prod.snd <$> f)) ?_ ?_ + · exact OFE.dist_prod_ext rfl Hincl' + apply OFE.Dist.trans ?_ + · apply OFE.equiv_dist.mp + exact CMRA.opM_opM_assoc.symm + obtain H : Store.get bf j • f' = f := by rw [← h] + rw [H] + simp [Option.map] + cases h : f + · simp [CMRA.op, optionOp, CMRA.op?] + · simp [CMRA.op, optionOp, CMRA.op?, Prod.op] + else + simp [Heap.point, Store.get_set_ne h, Heap.get_empty] + intro Hbf + have Hrel' := Hrel j (df, va) -- (dq • df, v • va) + simp [CMRA.op, Heap.get_merge, Prod.op] at Hrel' + simp [Option.merge, Heap.point, Store.get_set_ne h, Heap.get_empty] at Hrel' + simp only [Hbf] at Hrel' + exact Hrel' trivial + +theorem HeapView.update_of_localUpdate m k dq v mv' v' : + (Store.get m k = some mv) → + (mv, v) ~l~> (mv', v') → + ((HeapView.Auth (.own 1) m : HeapView F K V H) • HeapView.Frag k dq v) ~~> + ((HeapView.Auth (.own 1) (Store.set m k (.some mv')) : HeapView F K V H) • HeapView.Frag k dq v') := by + intro Hlookup Hup + apply HeapView.update_auth_op_frag + intro n mv0 f Hmv0 Hval Hincl + simp [Hlookup] at Hmv0; subst Hmv0 + have Hup' := Hup n (Prod.snd <$> f) ?G1 Hincl + case G1 => + refine CMRA.validN_ne Hincl.symm ?_ + cases Hval; cases f <;> simp_all [CMRA.op?, CMRA.op] + obtain ⟨Hval', Hincl'⟩ := Hup' + refine ⟨?_, Hincl'⟩ + simp_all + simp [CMRA.op?] at ⊢ Hincl Hincl' + cases f <;> simp_all [CMRA.op?, CMRA.op, Prod.op] <;> + refine ⟨Hval.1, CMRA.validN_ne Hincl' Hval'⟩ + +theorem HeapView.update_replace m k v v' : + ✓ v' → + ((HeapView.Auth (.own 1) m : HeapView F K V H) • (HeapView.Frag k (.own 1) v : HeapView F K V H)) ~~> + ((HeapView.Auth (F := F) (.own 1) (Store.set m k (.some v'))) • (HeapView.Frag (F := F) k (.own 1) v')) := by + intro Hval' + apply HeapView.update_auth_op_frag + intro n mv f Hlookup Hval Hincl + cases f <;> simp + · simp_all [CMRA.op?] + refine ⟨Hval.1, ?_⟩ + simp + exact CMRA.Valid.validN Hval' + · simp_all [CMRA.op?, CMRA.op, Prod.op] + exfalso + apply (own_whole_exclusive (UFraction.one_whole (α := F))).exclusive0_l + apply CMRA.valid0_of_validN + exact Hval.1 + +theorem HeapView.auth_frac_discard dq m : (HeapView.Auth dq m : HeapView F K V H) ~~> HeapView.Auth .discard m := + View.auth_discard + +theorem HeapView.auth_frac_acquire [IsSplitFraction F] m : + (HeapView.Auth .discard m : HeapView F K V H) ~~>: fun a => ∃ q, a = HeapView.Auth (F := F) (.own q) m := + View.auth_acquire + +theorem HeapView.update_of_dfrac_update k dq P v : dq ~~>: P → + (HeapView.Frag k dq v : HeapView F K V H) ~~>: fun a => ∃ dq', a = HeapView.Frag k dq' v ∧ P dq' := by + intro Hdq + apply UpdateP.weaken + · apply View.frag_updateP (P := fun b' => ∃ dq', ((◯V b') = HeapView.Frag k dq' v) ∧ P dq') + intros m n bf Hrel + simp only [HeapR, Store.all] at Hrel + have Hrel' := Hrel k ((dq, v) •? Store.get bf k) ?G + case G=> + simp [CMRA.op, Heap.get_merge, Heap.point_get_eq rfl, Option.merge, CMRA.op?] + cases Store.get bf k <;> simp + obtain ⟨v', dq', Hlookup, Hval, Hincl⟩ := Hrel' + obtain ⟨f', Hincl⟩ := Option.some_incN_some_iff_op?.mp Hincl + have Hincl' : (dq', v') ≡{n}≡ (dq, v) •? ((Store.get bf k) • f') := by + refine Hincl.trans ?_ + apply OFE.equiv_dist.mp + exact CMRA.opM_opM_assoc + clear Hincl + -- f := bf !! k ⋅ f' + -- (Store.get bf k) • f' + have X := Hdq n (Option.map Prod.fst ((Store.get bf k) • f')) ?G + case G => + cases h : (Store.get bf k) • f' <;> simp [Option.map, CMRA.op?] + · simp [h, CMRA.op?] at Hincl' + exact CMRA.validN_ne Hincl'.1 Hval.1 + · simp [h, CMRA.op?] at Hincl' + exact CMRA.validN_ne Hincl'.1 Hval.1 + obtain ⟨dq'', HPdq'', Hvdq''⟩ := X + exists Heap.point k (dq'', v) + refine ⟨?_, ?_⟩ + · exists dq'' + rintro j ⟨df, va⟩ Heq + if h : k = j + then + simp [CMRA.op, Heap.get_merge, Heap.point_get_eq h] at Heq + exists v' + exists ((dq'' •? (Option.map Prod.fst $ (Store.get bf k) • f'))) + refine ⟨h ▸ Hlookup, ⟨Hvdq'' , Hval.2⟩, ?_⟩ + exists f' + cases h : f' <;> cases h' : Store.get bf k <;> simp [OFE.Dist, Option.Forall₂, CMRA.op, optionOp, CMRA.op?] <;> + simp_all [h', h, CMRA.op, optionOp, CMRA.op?, Prod.op] + · exact Hincl'.2 + · exact Hincl'.2 + · exact Hincl'.2 + · have HR := Hincl'.2 + refine ⟨?_, ?_⟩ + · rw [← Heq.1] + exact CMRA.op_assocN + · simp at HR + rw [← Heq.2] + refine HR.trans ?_ + exact CMRA.op_assocN + else + apply Hrel + simp [CMRA.op, Heap.get_merge, Heap.point_get_ne h] at Heq ⊢ + exact Heq + · intro y + rintro ⟨b, rfl, q, _, _⟩ + exists q + +theorem HeapView.update_frag_discard k dq v : + (HeapView.Frag k dq v : HeapView F K V H) ~~> HeapView.Frag k .discard v := by + apply Update.lift_updateP (fun (dq : DFrac F) => HeapView.Frag (H := H) (F := F) k dq v) + · exact fun P Hupd => HeapView.update_of_dfrac_update k dq P v Hupd + · exact DFrac.update_discard + +theorem HeapView.update_frag_acquire [IsSplitFraction F] k v : + (HeapView.Frag k .discard v : HeapView F K V H) ~~>: + fun a => ∃ q, a = HeapView.Frag k (.own q) v := by + apply UpdateP.weaken + · apply HeapView.update_of_dfrac_update + apply DFrac.update_acquire + rintro y ⟨q, rfl, ⟨q1, rfl⟩⟩ + exists q1 + +section heap_updates + +-- TODO: Port functors diff --git a/src/Iris/Algebra/LocalUpdates.lean b/src/Iris/Algebra/LocalUpdates.lean index bb09b7de..8f7c019a 100644 --- a/src/Iris/Algebra/LocalUpdates.lean +++ b/src/Iris/Algebra/LocalUpdates.lean @@ -116,7 +116,7 @@ theorem LocalUpdate.valid [CMRA.Discrete α] {x y x' y' : α} theorem LocalUpdate.total_valid0 [CMRA.IsTotal α] {x y x' y' : α} (h : ✓{0} x → ✓{0} y → y ≼{0} x → (x, y) ~l~> (x', y')) : (x, y) ~l~> (x', y') := - .valid0 fun vx0 vy0 mz => h vx0 vy0 (CMRA.incN_of_some_incN_some mz) + .valid0 fun vx0 vy0 mz => h vx0 vy0 (Option.some_incN_some_iff_isTotal.mp mz) theorem LocalUpdate.total_valid [CMRA.IsTotal α] [CMRA.Discrete α] {x y x' y' : α} (h : ✓ x → ✓ y → y ≼ x → (x, y) ~l~> (x', y')) : (x, y) ~l~> (x', y') := diff --git a/src/Iris/Algebra/OFE.lean b/src/Iris/Algebra/OFE.lean index 1d6404f2..adc19eb6 100644 --- a/src/Iris/Algebra/OFE.lean +++ b/src/Iris/Algebra/OFE.lean @@ -284,6 +284,30 @@ instance [OFE α] [Leibniz α] : Leibniz (Option α) where | none, none, _ => rfl | some _, some _, h => congrArg some (Leibniz.eq_of_eqv h) +instance [OFE α] [Discrete α] : Discrete (Option α) where + discrete_0 {x y} H := + match x, y with + | none, none => H + | some _, some _ => some_eqv_some.mpr (discrete_0 H) + +instance OFE.Option.some.ne [OFE α] : OFE.NonExpansive (some : α → Option α) := ⟨fun _ _ _ => id⟩ + +theorem Option.some_is_discrete [OFE α] {a : α} (Ha : DiscreteE a) : DiscreteE (some a) := by + constructor + intro y H; cases y + · exact H + · exact Ha.discrete H + +theorem Option.none_is_discrete [OFE α] : DiscreteE (none : Option α) := by + constructor + intro y; cases y <;> simp + +instance Option.merge_ne [OFE α] {op : α → α → α} [NonExpansive₂ op] : + NonExpansive₂ (Option.merge op) where + ne n x1 x2 Hx y1 y2 Hy := by + cases x1 <;> cases x2 <;> cases y1 <;> cases y2 <;> simp_all + exact NonExpansive₂.ne Hx Hy + abbrev OFEFun {α : Type _} (β : α → Type _) := ∀ a, OFE (β a) instance [OFEFun (β : α → _)] : OFE ((x : α) → β x) where @@ -349,6 +373,19 @@ theorem dist_snd {n} [OFE α] [OFE β] {x y : α × β} (h : x ≡{n}≡ y) : x. theorem dist_prod_ext {n} [OFE α] [OFE β] {x₁ x₂ : α} {y₁ y₂ : β} (ex : x₁ ≡{n}≡ x₂) (ey : y₁ ≡{n}≡ y₂) : (x₁, y₁) ≡{n}≡ (x₂, y₂) := ⟨ex, ey⟩ +theorem prod.is_discrete [OFE α] [OFE β] {a : α} {b : β} (Ha : DiscreteE a) (Hb : DiscreteE b) : + DiscreteE (a, b) := by + constructor + intro y H; refine ⟨Ha.discrete H.1, Hb.discrete H.2⟩ + +instance [OFE α] [OFE β] [Discrete α] [Discrete β] : Discrete (α × β) where + discrete_0 H := by + constructor + · apply Discrete.discrete_0 + apply H.1 + · apply Discrete.discrete_0 + apply H.2 + /-- An isomorphism between two OFEs is a pair of morphisms whose composition is equivalent to the identity morphism. -/ @[ext] structure Iso (α β : Type _) [OFE α] [OFE β] where @@ -458,6 +495,40 @@ theorem map_comp [OFE α] [OFE β] [OFE γ] {f : α -n> β} {g : β -n> γ} {c : end Chain +/-- If a chain of Option is ever none, is the constant none chain. -/ +theorem chain_none_const [OFE V] {c : Chain (Option V)} (H : c n = none) : + c = Chain.const none := by + rcases c with ⟨c, Hc⟩ + congr 1; refine funext (fun k => ?_) + rcases Nat.le_or_ge n k with (Hnk|Hnk) + · suffices c k ≡{n}≡ c n by cases _ : c k <;> simp_all + exact Hc Hnk + · suffices c k ≡{k}≡ c n by cases _ : c k <;> simp_all + exact (Hc Hnk).symm + +/-- If a chain of Option is ever some, it is the lift a chain by some. -/ +def chain_option_some [OFE V] {c : Chain (Option V)} (H : c n = some v) : + ∃ c' : Chain V, c = Chain.map ⟨some, OFE.Option.some.ne⟩ c' := by + have HVc (k) : ∃ v', c k = some v' := by + rcases h : c.chain k with (_|v') + · simp [chain_none_const h] at H + · exists v' + let c' : Chain V := + ⟨fun n => Classical.choose <| HVc n, + by + intro n i Hni + have HR := c.cauchy Hni + rw [Classical.choose_spec (HVc n), Classical.choose_spec (HVc i)] at HR + exact HR ⟩ + exists c' + rcases hcc : c with ⟨cc, Hcc⟩ + simp only [Chain.map, Chain.mk.injEq] + refine funext (fun i => ?_) + simp only [c'] + have Hchoose := Classical.choose_spec (HVc i) + rw [← Hchoose] + simp [hcc] + /-- Complete ordered family of equivalences -/ class IsCOFE (α : Type _) [OFE α] where compl : Chain α → α @@ -788,3 +859,18 @@ instance [OFunctorContractive F] : OFunctorContractive (LaterOF F) where simp_all only [Dist, DistLater, Function.uncurry, OFunctor.map, laterMap] end LaterOF + +section subtype + +instance [OFE α] {P : α → Prop} : OFE { x : α // P x } where + Equiv := (·.val ≡ ·.val) + Dist n := (·.val ≡{n}≡ ·.val) + dist_eqv := { + refl x := dist_eqv.refl x.val + symm H := H.symm + trans H1 H2 := H1.trans H2 + } + equiv_dist := equiv_dist + dist_lt := dist_lt + +end subtype diff --git a/src/Iris/Algebra/Updates.lean b/src/Iris/Algebra/Updates.lean index fda07960..b506f62e 100644 --- a/src/Iris/Algebra/Updates.lean +++ b/src/Iris/Algebra/Updates.lean @@ -110,7 +110,7 @@ theorem UpdateP.op {P Q R : α → Prop} {x y} exact ⟨z • w, pqr z w pz pw, CMRA.validN_ne (CMRA.op_opM_assoc_dist z w mz).symm vz⟩ theorem UpdateP.op' {P Q : α → Prop} {x y : α} (uxp : x ~~>: P) (uyq : y ~~>: Q) : - x • y ~~>: λ t ↦ ∃ z w, t = (z • w : α) ∧ P z ∧ Q w := + (x • y : α) ~~>: λ t ↦ ∃ z w, t = (z • w : α) ∧ P z ∧ Q w := .op uxp uyq fun z w pz qw => ⟨z, w, rfl, pz, qw⟩ theorem Update.op {x₁ x₂ y₁ y₂ : α} (xy₁ : x₁ ~~> y₁) (xy₂ : x₂ ~~> y₂) : x₁ • x₂ ~~> y₁ • y₂ := diff --git a/src/Iris/Algebra/View.lean b/src/Iris/Algebra/View.lean new file mode 100644 index 00000000..98f844c0 --- /dev/null +++ b/src/Iris/Algebra/View.lean @@ -0,0 +1,756 @@ +/- +Copyright (c) 2025 Markus de Medeiros. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Markus de Medeiros +-/ + +import Iris.Algebra.CMRA +import Iris.Algebra.OFE +import Iris.Algebra.Frac +import Iris.Algebra.DFrac +import Iris.Algebra.Agree +import Iris.Algebra.Updates +import Iris.Algebra.LocalUpdates + +open Iris + +abbrev view_rel (A B : Type _) := Nat → A → B → Prop + +class ViewRel [OFE A] [UCMRA B] (R : view_rel A B) where + mono : R n1 a1 b1 → a1 ≡{n2}≡ a2 → b2 ≼{n2} b1 → n2 ≤ n1 → R n2 a2 b2 + rel_validN n a b : R n a b → ✓{n} b + rel_unit n : ∃ a, R n a UCMRA.unit + +class ViewRelDiscrete [OFE A] [UCMRA B] (R : view_rel A B) extends ViewRel R where + discrete n a b : R 0 a b → R n a b + +namespace viewrel +open ViewRel DFrac + +variable [OFE A] [UCMRA B] {R : view_rel A B} [ViewRel R] + +theorem ne (Ha : a1 ≡{n}≡ a2) (Hb : b1 ≡{n}≡ b2) : R n a1 b1 ↔ R n a2 b2 := + ⟨(mono · Ha Hb.symm.to_incN n.le_refl), (mono · Ha.symm Hb.to_incN n.le_refl)⟩ + +theorem eqv_ne (Ha : a1 ≡ a2) (Hb : b1 ≡ b2) : R n a1 b1 ↔ R n a2 b2 := + ne Ha.dist Hb.dist + +end viewrel + +structure View (F : Type _) {A B : Type _} (R : view_rel A B) where + π_auth : Option ((DFrac F) × Agree A) + π_frag : B + +abbrev View.Auth [UCMRA B] {R : view_rel A B} (dq : DFrac F) (a : A) : View F R := + ⟨some (dq, toAgree a), UCMRA.unit⟩ + +abbrev View.Frag {R : view_rel A B} (b : B) : View F R := ⟨none, b⟩ + +notation "●V{" dq "} " a => View.Auth dq a +notation "●V " a => View.Auth (DFrac.own One.one) a +notation "◯V " b => View.Frag b + +namespace View +section ofe + +variable [OFE A] [OFE B] {R : view_rel A B} + +abbrev equiv (x y : View F R) : Prop := x.π_auth ≡ y.π_auth ∧ x.π_frag ≡ y.π_frag +abbrev dist (n : Nat) (x y : View F R) : Prop := x.π_auth ≡{n}≡ y.π_auth ∧ x.π_frag ≡{n}≡ y.π_frag + +instance : OFE (View F R) where + Equiv := equiv + Dist := dist + dist_eqv := { + refl _ := ⟨OFE.Dist.of_eq rfl, OFE.Dist.of_eq rfl⟩ + symm H := ⟨H.1.symm, H.2.symm⟩ + trans H1 H2 := ⟨H1.1.trans H2.1, H1.2.trans H2.2⟩ + } + equiv_dist := + ⟨fun H _ => ⟨H.1.dist, H.2.dist⟩, + fun H => ⟨OFE.equiv_dist.mpr (H · |>.1), OFE.equiv_dist.mpr (H · |>.2)⟩⟩ + dist_lt H Hn := ⟨OFE.dist_lt H.1 Hn, OFE.dist_lt H.2 Hn⟩ + +instance View.mk.ne : OFE.NonExpansive₂ (View.mk : _ → _ → View F R) := ⟨fun _ _ _ Ha _ _ Hb => ⟨Ha, Hb⟩⟩ +instance View.π_auth.ne : OFE.NonExpansive (View.π_auth : View F R → _) := ⟨fun _ _ _ H => H.1⟩ +instance View.π_frag.ne : OFE.NonExpansive (View.π_frag : View F R → _) := ⟨fun _ _ _ H => H.2⟩ + +theorem View.is_discrete {ag : Option ((DFrac F) × Agree A)} (Ha : OFE.DiscreteE ag) (Hb : OFE.DiscreteE b) : + OFE.DiscreteE (α := View F R) (View.mk ag b) := ⟨fun H => ⟨Ha.discrete H.1, Hb.discrete H.2⟩⟩ + +open OFE in +instance [Discrete A] [Discrete B] : Discrete (View F R) where + discrete_0 H := ⟨discrete_0 H.1, discrete_0 H.2⟩ + +theorem View.auth_inj_frac [UCMRA B] {q1 q2 : DFrac F} {a1 a2 : A} {n} (H : (●V{q1} a1 : View F R) ≡{n}≡ ●V{q2} a2) : + q1 = q2 := H.1.1 + +theorem View.auth_inj_ag [UCMRA B] {q1 q2 : DFrac F} {a1 a2 : A} {n} (H : (●V{q1} a1 : View F R) ≡{n}≡ ●V{q2} a2) : + a1 ≡{n}≡ a2 := toAgree.inj H.1.2 + +theorem View.frag_inj [UCMRA B] {b1 b2 : B} {n} (H : (◯V b1 : View F R) ≡{n}≡ ◯V b2) : + b1 ≡{n}≡ b2 := H.2 + +theorem View.auth_is_discrete [UFraction F] [UCMRA B] {dq a} (Ha : OFE.DiscreteE a) (He : OFE.DiscreteE (UCMRA.unit : B)) : + OFE.DiscreteE (●V{dq} a : View F R) := by + refine View.is_discrete ?_ He + apply OFE.Option.some_is_discrete + apply OFE.prod.is_discrete DFrac.is_discrete + apply Agree.toAgree.is_discrete + exact Ha + +theorem View.frag_is_discrete [UCMRA B] {b : B} (Hb : OFE.DiscreteE b) : (OFE.DiscreteE (◯V b : View F R)) := + View.is_discrete OFE.Option.none_is_discrete Hb + +end ofe + +section cmra +open ViewRel toAgree OFE + +variable [UFraction F] [OFE A] [IB : UCMRA B] {R : view_rel A B} [ViewRel R] + +theorem ViewRel.of_agree_dst_iff (Hb : b' ≡{n}≡ b) : + (∃ a', toAgree a ≡{n}≡ toAgree a' ∧ R n a' b') ↔ R n a b := by + refine ⟨fun H => ?_, fun H => ?_⟩ + · rcases H with ⟨_, HA, HR⟩ + exact mono HR (inj HA.symm) Hb.symm.to_incN n.le_refl + · exact ⟨a, .rfl, mono H .rfl Hb.to_incN n.le_refl⟩ + +instance auth_ne {dq : DFrac F} : NonExpansive (Auth dq : A → View F R) where + ne _ _ _ H := by + refine View.mk.ne.ne ?_ .rfl + refine some_dist_some.mpr ⟨.rfl, ?_⟩ + simp only + exact OFE.NonExpansive.ne H + +instance auth_ne₂ : NonExpansive₂ (Auth : DFrac F → A → View F R) where + ne _ _ _ Hq _ _ Hf := by + unfold View.Auth + refine (NonExpansive₂.ne ?_ .rfl) + refine NonExpansive.ne ?_ + exact dist_prod_ext Hq (NonExpansive.ne Hf) + +instance frag_ne : NonExpansive (Frag : B → View F R) where + ne _ _ _ H := View.mk.ne.ne .rfl H + +@[simp] def Valid (v : View F R) : Prop := + match v.π_auth with + | some (dq, ag) => ✓ dq ∧ (∀ n, ∃ a, ag ≡{n}≡ toAgree a ∧ R n a (π_frag v)) + | none => ∀ n, ∃ a, R n a (π_frag v) + +@[simp] def ValidN (n : Nat) (v : View F R) : Prop := + match v.π_auth with + | some (dq, ag) => ✓{n} dq ∧ (∃ a, ag ≡{n}≡ toAgree a ∧ R n a (π_frag v)) + | none => ∃ a, R n a (π_frag v) + +@[simp] def Pcore (v : View F R) : Option (View F R) := + some <| View.mk (CMRA.core v.1) (CMRA.core v.2) + +@[simp] def Op (v1 v2 : View F R) : View F R := + View.mk (v1.1 • v2.1) (v1.2 • v2.2) + +instance : CMRA (View F R) where + pcore := Pcore + op := Op + ValidN := ValidN + Valid := Valid + op_ne.ne n x1 x2 H := by + refine View.mk.ne.ne ?_ ?_ + · exact cmraOption.op_ne.ne <| NonExpansive.ne H + · exact IB.op_ne.ne <| NonExpansive.ne H + pcore_ne {n x y} cx H := by + simp only [Pcore, Option.some.injEq] + rintro ⟨rfl⟩ + exists ⟨CMRA.core y.π_auth, CMRA.core y.π_frag⟩ + exact ⟨rfl, OFE.Dist.core H.1, OFE.Dist.core H.2⟩ + validN_ne {n x1 x2} := by + rintro ⟨Hl, Hr⟩ + rcases x1 with ⟨_|⟨q1, ag1⟩, b1⟩ <;> + rcases x2 with ⟨_|⟨q2, ag2⟩, b2⟩ <;> + simp_all + · exact fun x H => ⟨x, ViewRel.mono H .rfl Hr.symm.to_incN n.le_refl⟩ + intro Hq a Hag HR + refine ⟨CMRA.discrete_valid <| DFrac_CMRA.validN_ne Hl.1 Hq, ?_⟩ + refine ⟨a, ?_⟩ + refine ⟨Hl.2.symm.trans Hag, ?_⟩ + refine ViewRel.mono HR .rfl ?_ n.le_refl + exact Dist.to_incN Hr.symm + valid_iff_validN {x} := by + simp only [Valid, ValidN]; split + · exact ⟨fun H n => ⟨H.1, H.2 n⟩, fun H => ⟨(H 0).1, fun n => (H n).2⟩⟩ + · exact Eq.to_iff rfl + validN_succ {x n} := by + simp only [ValidN] + split + · refine fun H => ⟨H.1, ?_⟩ + rcases H.2 with ⟨ag, Ha⟩; exists ag + refine ⟨Dist.le Ha.1 n.le_succ, ?_⟩ + exact mono Ha.2 .rfl (CMRA.incN_refl x.π_frag) n.le_succ + · rintro ⟨z, HR⟩ + exact ⟨z, mono HR .rfl (CMRA.incN_refl _) n.le_succ⟩ + validN_op_left {n x y} := by + rcases x with ⟨_|⟨q1, ag1⟩, b1⟩ <;> + rcases y with ⟨_|⟨q2, ag2⟩, b2⟩ <;> + simp [CMRA.op, optionOp] + · exact fun a Hr => ⟨a, mono Hr .rfl (CMRA.incN_op_left n b1 b2) n.le_refl⟩ + · exact fun _ a _ Hr => ⟨a, mono Hr .rfl (CMRA.incN_op_left n b1 b2) n.le_refl⟩ + · exact fun Hq a H Hr => ⟨Hq, ⟨a, ⟨H, mono Hr .rfl (CMRA.incN_op_left n b1 b2) n.le_refl⟩⟩⟩ + · refine fun Hq a H Hr => ⟨CMRA.validN_op_left Hq, ⟨a, ?_, ?_⟩⟩ + · refine .trans ?_ H + refine .trans Agree.idemp.symm.dist ?_ + exact CMRA.op_ne.ne <| Agree.op_invN (Agree.validN_ne H.symm trivial) + · exact ViewRel.mono Hr .rfl (CMRA.incN_op_left n b1 b2) n.le_refl + assoc := OFE.NonExpansive₂.eqv CMRA.assoc CMRA.assoc + comm := OFE.NonExpansive₂.eqv CMRA.comm CMRA.comm + pcore_op_left {x _} := by + simp only [Pcore, Option.some.injEq] + exact fun H => H ▸ OFE.NonExpansive₂.eqv (CMRA.core_op x.π_auth) (CMRA.core_op x.π_frag) + pcore_idem {_ cx} := by + simp only [Pcore, Option.some.injEq, OFE.some_eqv_some] + rcases cx + simp only [mk.injEq, and_imp] + intro H1 H2 + constructor + · simp only; exact H1 ▸ CMRA.core_idem _ + · exact H2 ▸ CMRA.core_idem _ + + -- Here + + pcore_op_mono := by + apply pcore_op_mono_of_core_op_mono + let f : (Option ((DFrac F) × Agree A) × B) → View F R := fun x => ⟨x.1, x.2⟩ + let g : View F R → (Option ((DFrac F) × Agree A) × B) := fun x => (x.1, x.2) + let opM' (x : View F R) (y : Option (View F R)) : View F R := + match y with | some y => Op x y | none => x + + have g_pcore_0 {y : View F R} : CMRA.pcore (g y) ≡ g <$> Pcore y := by + rcases y with ⟨x, b⟩ + simp only [pcore, Option.map_eq_map, Option.map, g] + simp [CMRA.pcore, Prod.pcore, optionCore] + simp [CMRA.pcore_eq_core] + rfl + + have g_pcore {y cy : View F R} : Pcore y ≡ some cy ↔ CMRA.pcore (g y) ≡ some (g cy) := by + suffices y.Pcore ≡ some cy ↔ g <$> y.Pcore ≡ some (g cy) by + exact ⟨g_pcore_0.trans ∘ this.mp, this.mpr ∘ g_pcore_0.symm.trans⟩ + refine Iff.trans OFE.equiv_dist (Iff.trans ?_ OFE.equiv_dist.symm) + exact ⟨fun H n => H n, fun H n => H n⟩ + + have g_opM_f {x y} : g (opM' y (f x)) ≡ CMRA.op (g y) x := by + simp [opM', g, f, CMRA.op, Prod.op] + + rintro y1 cy y2 ⟨z, Hy2⟩ Hy1 + let Lcore := (@CMRA.pcore_mono' _ _ (g y1) (g y2) (g cy) ?G1 ?G2) + case G1 => exists (g z) + case G2 => exact g_pcore.mp <| OFE.Equiv.of_eq Hy1 + rcases Lcore with ⟨cx, Hcgy2, ⟨x, Hcx⟩⟩ + have Hcx' : cx ≡ g (opM' cy (f x)) := Hcx + have Hcgy2' : CMRA.pcore (g y2) ≡ some (g (opM' cy (f x))) := by rw [Hcgy2]; exact Hcx + have Hcgy2'' : Pcore y2 ≡ some (opM' cy (f x)) := g_pcore.mpr Hcgy2' + generalize HC : y2.Pcore = C + rw [HC] at Hcgy2'' + cases C; exact Hcgy2''.elim + rename_i cy' + refine ⟨cy', ⟨rfl, ?_⟩⟩ + exists (f x) + extend {n x y1 y2} Hv He := by + let g : View F R → (Option ((DFrac F) × Agree A) × B) := fun x => (x.1, x.2) + have H2 := @CMRA.extend _ _ n (g x) (g y1) (g y2) ?G1 He + case G1 => + simp_all [ValidN, CMRA.ValidN, Prod.ValidN, g, optionValidN] + rcases x with ⟨_|⟨q1, ag1⟩, b1⟩ <;> simp_all only + · refine ⟨trivial, ?_⟩ + rcases Hv with ⟨_, Ha⟩ + apply ViewRel.rel_validN _ _ _ Ha + · rcases Hv with ⟨Hq, ⟨a, ⟨Ha1, Ha2⟩⟩⟩ + refine ⟨⟨trivial, ?_⟩, ?_⟩ + · exact Agree.validN_ne Ha1.symm trivial + · exact ViewRel.rel_validN _ _ _ Ha2 + rcases H2 with ⟨z1, z2, Hze, Hz1, Hz2⟩ + exists ⟨z1.1, z1.2⟩ + exists ⟨z2.1, z2.2⟩ + +instance [OFE.Discrete A] [CMRA.Discrete B] [ViewRelDiscrete R] : CMRA.Discrete (View F R) where + discrete_valid := by + simp [CMRA.ValidN, ValidN, CMRA.Valid, Valid] + intro x + split + · rintro ⟨H1, ⟨a, H2, H3⟩⟩ + refine ⟨H1, fun n => ⟨a, ⟨?_, ?_⟩⟩⟩ + · exact OFE.equiv_dist.mp (OFE.Discrete.discrete_0 H2) _ + · exact ViewRelDiscrete.discrete _ _ _ H3 + · rintro ⟨a, H⟩ _ + exact ⟨a, ViewRelDiscrete.discrete _ _ _ H⟩ + +instance : UCMRA (View F R) where + unit := ⟨UCMRA.unit, UCMRA.unit⟩ + unit_valid := ViewRel.rel_unit + unit_left_id := ⟨UCMRA.unit_left_id, UCMRA.unit_left_id⟩ + pcore_unit := ⟨by rfl, CMRA.core_eqv_self UCMRA.unit⟩ + +theorem auth_op_eqv : (●V{dq1 • dq2} a : View F R) ≡ (●V{dq1} a) • ●V{dq2} a := + ⟨⟨rfl, Agree.idemp.symm⟩, UCMRA.unit_left_id.symm⟩ + +theorem frag_op_eq : (◯V (b1 • b2) : View F R) = ((◯V b1) • ◯V b2 : View F R):= rfl + +theorem frag_inc_of_inc (H : b1 ≼ b2) : (◯V b1 : View F R) ≼ ◯V b2 := by + rcases H with ⟨c, H⟩ + refine CMRA.inc_of_inc_of_eqv ?_ (NonExpansive.eqv H.symm) + rw [View.frag_op_eq] + exact CMRA.inc_op_left _ _ + +theorem core_frag : CMRA.core (◯V b : View F R) = ◯V (CMRA.core b) := rfl + +theorem core_discard_op_frag_eqv : CMRA.core ((●V{.discard} a) • ◯V b : View F R) ≡ (●V{.discard} a) • ◯V (CMRA.core b) := + ⟨.rfl, (CMRA.core_ne.eqv UCMRA.unit_left_id).trans UCMRA.unit_left_id.symm⟩ + +theorem core_own_op_frag_eqv : CMRA.core ((●V{.own q} a) • ◯V b : View F R) ≡ ◯V (CMRA.core b) := + ⟨trivial, CMRA.core_ne.eqv UCMRA.unit_left_id⟩ + +instance : CMRA.CoreId (●V{.discard} a : View F R) where + core_id := ⟨.rfl, CMRA.core_eqv_self UCMRA.unit⟩ + +instance [CMRA.CoreId b] : CMRA.CoreId (◯V b : View F R) where + core_id := ⟨.rfl, CMRA.coreId_iff_core_eqv_self.mp (by trivial)⟩ + +instance [CMRA.CoreId b] : CMRA.CoreId ((●V{.discard} a : View F R) • ◯V b) where + core_id := by + refine ⟨.rfl, ?_⟩ + refine (CMRA.core_ne.eqv UCMRA.unit_left_id).trans ?_ + refine (CMRA.coreId_iff_core_eqv_self.mp (by trivial)).trans ?_ + refine UCMRA.unit_left_id.symm + +theorem dst_of_validN_auth (H : ✓{n} ((●V{dq1} a1 : View F R) • ●V{dq2} a2)) : a1 ≡{n}≡ a2 := by + rcases H with ⟨_, _, H, _⟩ + refine toAgree.inj (Agree.op_invN ?_) + exact Agree.validN_ne H.symm trivial + +theorem eqv_of_valid_auth (H : ✓ ((●V{dq1} a1 : View F R) • ●V{dq2} a2)) : a1 ≡ a2 := + OFE.equiv_dist.mpr fun _ => dst_of_validN_auth H.validN + +theorem auth_validN_iff : ✓{n} (●V{dq} a : View F R) ↔ ✓{n}dq ∧ R n a UCMRA.unit := + and_congr_right fun _ => ViewRel.of_agree_dst_iff .rfl + +theorem auth_one_validN_iff n a : ✓{n} (●V a : View F R) ↔ R n a UCMRA.unit := + ⟨(auth_validN_iff.mp · |>.2), (auth_validN_iff.mpr ⟨UFraction.one_whole.1, ·⟩)⟩ + +theorem auth_op_auth_validN_iff : + ✓{n} ((●V{dq1} a1 : View F R) • ●V{dq2} a2) ↔ ✓(dq1 • dq2) ∧ a1 ≡{n}≡ a2 ∧ R n a1 UCMRA.unit := by + refine ⟨fun H => ?_, fun H => ?_⟩ + · let Ha' : a1 ≡{n}≡ a2 := dst_of_validN_auth H + rcases H with ⟨Hq, _, Ha, HR⟩ + refine ⟨Hq, Ha', ViewRel.mono HR ?_ CMRA.incN_unit n.le_refl⟩ + refine .trans ?_ Ha'.symm + refine toAgree.inj ?_ + apply Ha.symm.trans + apply CMRA.op_commN.trans + apply (CMRA.op_ne.ne (toAgree.ne.ne Ha')).trans + apply Agree.idemp + · simp [CMRA.op, CMRA.ValidN, ValidN, optionOp, Prod.op] + refine ⟨H.1, a1, ?_, ?_⟩ + · exact (CMRA.op_ne.ne <| toAgree.ne.ne H.2.1.symm).trans Agree.idemp.dist + · refine ViewRel.mono H.2.2 .rfl ?_ n.le_refl + exact OFE.Dist.to_incN <| CMRA.unit_left_id_dist UCMRA.unit + +theorem auth_one_op_validN_iff : ✓{n} ((●V a1 : View F R) • ●V a2) ↔ False := by + refine auth_op_auth_validN_iff.trans ?_ + simp only [iff_false, not_and] + intro _ + refine (UFraction.one_whole (α := F)).2 ?_ |>.elim + exists 1 + +theorem frag_validN_iff : ✓{n} (◯V b : View F R) ↔ ∃ a, R n a b := by rfl + +theorem auth_op_frag_validN_iff : ✓{n} ((●V{dq} a : View F R) • ◯V b) ↔ ✓dq ∧ R n a b := + and_congr_right (fun _ => ViewRel.of_agree_dst_iff <| CMRA.unit_left_id_dist b) + +theorem auth_one_op_frag_validN_iff : ✓{n} ((●V a : View F R) • ◯V b) ↔ R n a b := + auth_op_frag_validN_iff.trans <| and_iff_right_iff_imp.mpr (fun _ => valid_own_one) + +theorem auth_valid_iff : ✓ (●V{dq} a : View F R) ↔ ✓dq ∧ ∀ n, R n a UCMRA.unit := + and_congr_right (fun _=> forall_congr' fun _ => ViewRel.of_agree_dst_iff .rfl) + +theorem auth_one_valid_iff : ✓ (●V a : View F R) ↔ ∀ n, R n a UCMRA.unit := + auth_valid_iff.trans <| and_iff_right_iff_imp.mpr (fun _ => valid_own_one) + +theorem auth_op_auth_valid_iff : ✓ ((●V{dq1} a1 : View F R) • ●V{dq2} a2) ↔ ✓(dq1 • dq2) ∧ a1 ≡ a2 ∧ ∀ n, R n a1 UCMRA.unit := by + refine CMRA.valid_iff_validN.trans ?_ + refine ⟨fun H => ?_, fun H n => ?_⟩ + · simp [CMRA.Valid, valid, Auth, CMRA.op, op, optionOp, CMRA.ValidN, ValidN] at H + let Hn (n) := dst_of_validN_auth (H n) + refine ⟨(H 0).1, OFE.equiv_dist.mpr Hn, fun n => ?_⟩ + · rcases (H n) with ⟨_, _, Hl, H⟩ + apply ViewRel.mono H ?_ CMRA.incN_unit n.le_refl + apply toAgree.inj + apply Hl.symm.trans + exact (CMRA.op_ne.ne <| toAgree.ne.ne (Hn _).symm).trans Agree.idemp.dist + · exact auth_op_auth_validN_iff.mpr ⟨H.1, H.2.1.dist, H.2.2 n⟩ + +theorem auth_one_op_auth_one_valid_iff : ✓ ((●V a1 : View F R) • ●V a2) ↔ False := by + refine auth_op_auth_valid_iff.trans ?_ + simp [CMRA.op, op, CMRA.Valid, op, valid] + intro _ + refine (UFraction.one_whole (α := F)).2 ?_ |>.elim + exists 1 + +theorem frag_valid_iff : ✓ (◯V b : View F R) ↔ ∀ n, ∃ a, R n a b := by rfl + +theorem auth_op_frag_valid_iff : ✓ ((●V{dq} a : View F R) • ◯V b) ↔ ✓dq ∧ ∀ n, R n a b := + and_congr_right (fun _ => forall_congr' fun _ => ViewRel.of_agree_dst_iff <| CMRA.unit_left_id_dist b) + +theorem auth_one_op_frag_valid_iff : ✓ ((●V a : View F R) • ◯V b) ↔ ∀ n, R n a b := + auth_op_frag_valid_iff.trans <| and_iff_right_iff_imp.mpr (fun _ => valid_own_one) + +theorem auth_incN_auth_op_frag_iff : (●V{dq1} a1 : View F R) ≼{n} ((●V{dq2} a2) • ◯V b) ↔ (dq1 ≼ dq2 ∨ dq1 = dq2) ∧ a1 ≡{n}≡ a2 := by + refine ⟨?_, ?_⟩ + · simp only [Auth, Frag, CMRA.IncludedN, CMRA.op, op, optionOp, Prod.op] + rintro ⟨(_|⟨dqf, af⟩),⟨⟨x1, x2⟩, y⟩⟩ + · exact ⟨Or.inr x1.symm, toAgree.inj x2.symm⟩ + · simp_all only [] + apply And.intro + · left; exists dqf + · apply toAgree.incN.mp; exists af + · intro H + -- simp only [auth, frag, CMRA.IncludedN, CMRA.op, op, optionOp, Prod.op] + rcases H with ⟨(⟨z, HRz⟩| HRa2), HRb⟩ + · -- have _ := @View.auth_op_eqv + apply (CMRA.incN_iff_right <| ?G).mp + case G => + apply OFE.equiv_dist.mp + apply CMRA.comm + apply (CMRA.incN_iff_right <| ?G).mp + case G => + apply CMRA.op_ne.ne + apply OFE.NonExpansive₂.ne HRz.symm HRb + apply (CMRA.incN_iff_right <| ?G).mp + case G => + apply CMRA.op_ne.ne + apply OFE.equiv_dist.mp + apply View.auth_op_eqv.symm + apply (CMRA.incN_iff_right <| ?G).mp + case G => + apply CMRA.op_ne.ne + apply OFE.equiv_dist.mp + apply CMRA.comm + apply (CMRA.incN_iff_right <| ?G).mp + case G => + apply OFE.equiv_dist.mp + apply CMRA.assoc.symm + apply (CMRA.incN_iff_right <| ?G).mp + case G => + apply OFE.equiv_dist.mp + apply CMRA.comm + exists ((◯V b) • ●V{z} a1) + · exists (◯V b) + refine .trans (OFE.equiv_dist.mp CMRA.comm _) (.trans ?_ (OFE.equiv_dist.mp CMRA.comm _)) + apply CMRA.op_ne.ne + rw [HRa2] + exact OFE.NonExpansive₂.ne rfl HRb.symm + +theorem auth_inc_auth_op_frag_iff : ((●V{dq1} a1 : View F R) ≼ (●V{dq2} a2 : View F R) • ◯V b) ↔ (dq1 ≼ dq2 ∨ dq1 = dq2) ∧ a1 ≡ a2 := by + refine ⟨fun H => ⟨?_, ?_⟩, fun H => ?_⟩ + · exact auth_incN_auth_op_frag_iff (n := 0) |>.mp (CMRA.incN_of_inc _ H) |>.1 + · refine OFE.equiv_dist.mpr (fun n => ?_) + exact auth_incN_auth_op_frag_iff |>.mp (CMRA.incN_of_inc _ H) |>.2 + · rcases H with ⟨(⟨q, Hq⟩|Hq), Ha⟩ + · apply (CMRA.inc_iff_right <| ?G).mp + case G => + apply OFE.Equiv.symm + apply CMRA.comm.trans + apply CMRA.op_ne.eqv + exact NonExpansive₂.eqv Hq Ha.symm + apply (CMRA.inc_iff_right <| ?G1).mp + case G1 => + apply CMRA.op_ne.eqv + apply View.auth_op_eqv.symm + apply (CMRA.inc_iff_right <| CMRA.comm).mp + apply (CMRA.inc_iff_right <| CMRA.assoc).mp + exists ((●V{q} a1) • ◯V b) + · exists (◯V b) + refine .trans CMRA.comm (.trans ?_ CMRA.comm ) + apply CMRA.op_ne.eqv + rw [Hq] + exact OFE.NonExpansive₂.eqv rfl Ha.symm + +theorem auth_one_incN_auth_one_op_frag_iff : (●V a1 : View F R) ≼{n} ((●V a2) • ◯V b) ↔ a1 ≡{n}≡ a2 := + auth_incN_auth_op_frag_iff.trans <| and_iff_right_iff_imp.mpr <| fun _ => .inr rfl + +theorem auth_one_inc_auth_one_op_frag_iff : (●V a1 : View F R) ≼ ((●V a2) • ◯V b) ↔ a1 ≡ a2 := + auth_inc_auth_op_frag_iff.trans <| and_iff_right_iff_imp.mpr <| fun _ => .inr rfl + +theorem frag_incN_auth_frag_iff : (◯V b1 : View F R) ≼{n} ((●V{p} a) • ◯V b2) ↔ b1 ≼{n} b2 := by + constructor + · rintro ⟨xf, ⟨_, Hb⟩⟩ + simp [Auth, Frag, CMRA.op, op] at Hb + have Hb' : b2 ≡{n}≡ b1 • xf.π_frag := by + apply OFE.Dist.trans + apply OFE.Dist.symm + apply OFE.equiv_dist.mp + apply UCMRA.unit_left_id + apply Hb + apply (CMRA.incN_iff_right <| Hb'.symm).mp + exists xf.π_frag + · rintro ⟨bf, Hbf⟩ + apply (CMRA.incN_iff_right <| ?G).mp + case G => + apply CMRA.op_ne.ne + apply NonExpansive.ne Hbf.symm + rw [View.frag_op_eq] + apply (CMRA.incN_iff_right <| ?G).mp + case G => + apply OFE.equiv_dist.mp + apply CMRA.comm + apply (CMRA.incN_iff_right <| ?G).mp + case G => + apply OFE.equiv_dist.mp + apply CMRA.assoc + exists ((◯V bf) • ●V{p} a) + +theorem frag_inc_auth_op_frag : (◯V b1 : View F R) ≼ ((●V{p} a) • ◯V b2) ↔ b1 ≼ b2 := by + constructor + · rintro ⟨xf, ⟨_, Hb⟩⟩ + simp [Auth, Frag, CMRA.op, op] at Hb + have Hb' : b2 ≡ b1 • xf.π_frag := by + apply OFE.Equiv.trans + apply OFE.Equiv.symm + apply UCMRA.unit_left_id + apply Hb + apply (CMRA.inc_iff_right <| Hb'.symm).mp + exists xf.π_frag + · rintro ⟨bf, Hbf⟩ + apply (CMRA.inc_iff_right <| ?G).mp + case G => + apply CMRA.op_ne.eqv + apply NonExpansive.eqv Hbf.symm + rw [View.frag_op_eq] + apply (CMRA.inc_iff_right <| ?G).mp + case G => apply CMRA.comm + apply (CMRA.inc_iff_right <| ?G).mp + case G => + apply CMRA.assoc + exists ((◯V bf) • ●V{p} a) + +theorem auth_op_frag_incN_auth_op_frag_iff : + ((●V{dq1} a1 : View F R) • ◯V b1) ≼{n} ((●V{dq2} a2) • ◯V b2) ↔ + (dq1 ≼ dq2 ∨ dq1 = dq2) ∧ a1 ≡{n}≡ a2 ∧ b1 ≼{n} b2 := by + constructor + · intro H + rw [← and_assoc] + constructor + · apply (auth_incN_auth_op_frag_iff (R := R)).mp + apply CMRA.incN_trans ?_ H + exact CMRA.incN_op_left n (●V{dq1} a1) (◯V b1) + · apply (frag_incN_auth_frag_iff (R := R) (F := F)).mp + apply CMRA.incN_trans (CMRA.incN_op_right _ _ _) + apply H + · rintro ⟨H0, H1, ⟨bf, H2⟩⟩ + apply (CMRA.incN_iff_right <| ?G).mp + case G => + apply CMRA.op_ne.ne + apply NonExpansive.ne + apply OFE.Dist.symm + apply H2.trans + apply OFE.equiv_dist.mp + apply CMRA.comm + rewrite [View.frag_op_eq] + apply (CMRA.incN_iff_right <| ?G).mp + case G => + apply OFE.equiv_dist.mp + apply CMRA.assoc.symm + refine CMRA.op_monoN_left (◯V b1) ?_ + apply auth_incN_auth_op_frag_iff.mpr + exact ⟨H0, H1⟩ + +theorem auth_op_frag_inc_auth_op_frag_iff : ((●V{dq1} a1 : View F R) • ◯V b1) ≼ ((●V{dq2} a2) • ◯V b2) ↔ + (dq1 ≼ dq2 ∨ dq1 = dq2) ∧ a1 ≡ a2 ∧ b1 ≼ b2 := by + constructor + · intro H + rw [← and_assoc] + constructor + · apply (auth_inc_auth_op_frag_iff (R := R)).mp + apply CMRA.inc_trans ?_ H + exact CMRA.inc_op_left (●V{dq1} a1) (◯V b1) + · apply (frag_inc_auth_op_frag (R := R) (F := F)).mp + apply CMRA.inc_trans (CMRA.inc_op_right _ _) + apply H + · rintro ⟨H0, H1, ⟨bf, H2⟩⟩ + apply (CMRA.inc_iff_right <| ?G).mp + case G => + apply CMRA.op_ne.eqv + apply NonExpansive.eqv + apply OFE.Equiv.symm + apply H2.trans + apply CMRA.comm + rewrite [View.frag_op_eq] + apply (CMRA.inc_iff_right <| ?G).mp + case G => + apply CMRA.assoc.symm + refine CMRA.op_mono_left (◯V b1) ?_ + apply auth_inc_auth_op_frag_iff.mpr + exact ⟨H0, H1⟩ + +theorem auth_one_op_frag_incN_auth_one_op_frag_iff : ((●V a1 : View F R) • ◯V b1) ≼{n} ((●V a2) • ◯V b2) ↔ (a1 ≡{n}≡ a2 ∧ b1 ≼{n} b2) := + auth_op_frag_incN_auth_op_frag_iff.trans <| and_iff_right_iff_imp.mpr <| fun _ => .inr rfl + +theorem auth_op_one_frag_inc_auth_one_op_frag_iff : ((●V a1 : View F R) • ◯V b1) ≼ ((●V a2) • ◯V b2) ↔ a1 ≡ a2 ∧ b1 ≼ b2 := + auth_op_frag_inc_auth_op_frag_iff.trans <| and_iff_right_iff_imp.mpr <| fun _ => .inr rfl + +end cmra + +section updates + +variable [UFraction F] [OFE A] [IB : UCMRA B] {R : view_rel A B} [ViewRel R] + +theorem auth_op_frag_update {Pab : A → B → Prop} + (Hup : ∀ n bf, R n a (b • bf) → ∃ a' b', Pab a' b' ∧ R n a' (b' • bf)) : + ((●V a) • ◯V b : View F R) ~~>: fun k => ∃ a' b', k = ((●V a') • ◯V b' : View F R) ∧ Pab a' b' := by + refine UpdateP.total.mpr (fun n ⟨ag, bf⟩ => ?_) + rcases ag with (_|⟨dq, ag⟩) + · intro H + simp [CMRA.op, op, CMRA.ValidN, optionOp, ValidN] at H + obtain ⟨_, a0, He', Hrel'⟩ := H + have He := toAgree.inj He'; clear He' + have Hrel : R n a (b • bf) := by + apply ViewRel.mono Hrel' He.symm _ n.le_refl + apply Iris.OFE.Dist.to_incN + refine CMRA.comm.dist.trans (.trans ?_ CMRA.comm.dist) + refine CMRA.op_ne.ne ?_ + exact (CMRA.unit_left_id_dist b).symm + obtain ⟨a', b', Hab', Hrel''⟩ := Hup _ _ Hrel + refine ⟨((●V a') • ◯V b'), ?_, ⟨by trivial, ?_⟩⟩ + · exists a'; exists b' + · refine ⟨a', .rfl, ?_⟩ + apply ViewRel.mono Hrel'' .rfl _ n.le_refl + simp [CMRA.op, op] + apply Iris.OFE.Dist.to_incN + refine CMRA.comm.dist.trans (.trans ?_ CMRA.comm.dist) + refine CMRA.op_ne.ne ?_ + exact (CMRA.unit_left_id_dist b') + · -- FIXME: Why doesn't this synthesize? + have _ : CMRA.Exclusive (DFrac.own One.one : DFrac F) := by + apply own_whole_exclusive <| UFraction.one_whole + exact (CMRA.not_valid_exclN_op_left ·.1 |>.elim) + +theorem auth_one_op_frag_update (Hup : ∀ n bf, R n a (b • bf) → R n a' (b' • bf)) : + ((●V a) • ◯V b : View F R) ~~> (●V a') • ◯V b' := by + apply Update.of_updateP + apply UpdateP.weaken + · apply auth_op_frag_update (Pab := fun a b => a = a' ∧ b = b') + intro _ _ H + exact ⟨a', b', ⟨rfl, rfl⟩, Hup _ _ H⟩ + · rintro y ⟨a', b', H, rfl, rfl⟩; exact H.symm + +theorem auth_one_alloc (Hup : ∀ n bf, R n a bf → R n a' (b' • bf)) : + ((●V a) ~~> ((●V a' : View F R) • ◯V b')) := by + refine Update.equiv_left CMRA.unit_right_id ?_ + refine auth_one_op_frag_update (fun n bf H => Hup n bf <| ViewRel.mono H .rfl ?_ n.le_refl) + exact CMRA.incN_op_right n UCMRA.unit bf + +theorem auth_one_op_frag_dealloc (Hup : (∀ n bf, R n a (b • bf) → R n a' bf)) : + ((●V a : View F R) • ◯V b) ~~> ●V a' := by + refine Update.equiv_right CMRA.unit_right_id ?_ + refine auth_one_op_frag_update (fun n bf H => ?_) + refine ViewRel.mono (Hup n bf H) .rfl ?_ n.le_refl + exact Iris.OFE.Dist.to_incN (CMRA.unit_left_id_dist bf) + +theorem auth_one_update (Hup : ∀ n bf, R n a bf → R n a' bf) : + (●V a : View F R) ~~> ●V a' := by + refine Update.equiv_right CMRA.unit_right_id ?_ + refine Update.equiv_left CMRA.unit_right_id ?_ + refine auth_one_op_frag_update (fun n bf H => ?_) + exact ViewRel.mono (Hup n _ H) .rfl .rfl n.le_refl + +theorem auth_update (Hupd : dq ~~>: P) : + (●V{dq} a : View F R ) ~~>: (fun k => ∃ dq', (k = ●V{dq'} a) ∧ P dq') := by + refine UpdateP.total.mpr (fun n ⟨ag, bf⟩ => ?_) + rcases ag with (_|⟨dq', ag⟩) <;> rintro ⟨Hv, a', _, _⟩ + · obtain ⟨dr, Hdr, Heq⟩ := Hupd n none Hv + refine ⟨●V{dr} a, (by exists dr), ⟨Heq, (by exists a')⟩⟩ + · obtain ⟨dr, Hdr, Heq⟩ := Hupd n (some dq') Hv + refine ⟨●V{dr} a, (by exists dr), ⟨Heq, (by exists a')⟩⟩ + +theorem auth_discard : (●V{dq} a : View F R) ~~> ●V{.discard} a := by + apply Update.lift_updateP (g := fun dq => ●V{dq} a) + · intro P + apply auth_update + · exact DFrac.update_discard + +theorem auth_acquire [IsSplitFraction F] : + (●V{.discard} a : View F R) ~~>: fun k => ∃ q, k = ●V{.own q} a := by + apply UpdateP.weaken + · apply auth_update + exact DFrac.update_acquire + · rintro y ⟨dq, rfl, q', rfl⟩ + exists q' + +theorem auth_op_frag_acquire [IsSplitFraction F] : + ((●V{.discard} a : View F R) • ◯V b) ~~>: fun k => ∃ q, k = ((●V{.own q} a : View F R) • ◯V b ):= by + apply UpdateP.op + apply auth_acquire + apply UpdateP.id rfl + rintro z1 z2 ⟨q, rfl⟩ rfl; exists q + +theorem frag_updateP {P : B → Prop} (Hupd : ∀ a n bf, R n a (b • bf) → ∃ b', P b' ∧ R n a (b' • bf)) : + (◯V b : View F R) ~~>: (fun k => ∃ b', (k = (◯V b' : View F R)) ∧ P b') := by + refine UpdateP.total.mpr (fun n ⟨ag, bf⟩ => ?_) + rcases ag with (_|⟨dq,af⟩) + simp only [CMRA.ValidN, ValidN] + · rintro ⟨a, Ha⟩ + obtain ⟨b', HP, Hb'⟩ := Hupd a n bf Ha + exists (◯V b') + simp only [mk.injEq, true_and, exists_eq_left'] + refine ⟨HP, ⟨a, Hb'⟩⟩ + · rintro ⟨Hq, a, Hae, Hr⟩ + obtain ⟨b', Hb', Hp⟩ := Hupd a n bf Hr + exists (◯V b') + simp only [mk.injEq, true_and, exists_eq_left'] + refine ⟨Hb', ?_⟩ + simp [CMRA.ValidN, ValidN, CMRA.op, op, optionOp] + refine ⟨Hq, ⟨a, Hae, Hp⟩⟩ + +theorem frag_update (Hupd : ∀ a n bf, R n a (b • bf) → R n a (b' • bf)) : + (◯V b : View F R) ~~> (◯V b' : View F R) := by + refine Update.total.mpr (fun n ⟨ag, bf⟩ => ?_) + rcases ag with (_|⟨dq,af⟩) + simp only [CMRA.ValidN, ValidN] + · simp_all [CMRA.op, optionOp] + intro a HR + exists a + apply Hupd _ _ _ HR + · simp_all [CMRA.op, op, optionOp, CMRA.ValidN, ValidN] + intro Hq a He Hr + exists a + exact ⟨He, Hupd _ _ _ Hr⟩ + +theorem auth_alloc (Hup : ∀ n bf, R n a bf → R n a (b • bf)) : + (●V{dq} a : View F R) ~~> ((●V{dq} a) • ◯V b) := by + refine Update.total.mpr (fun n ⟨ag', bf⟩ => ?_) + obtain (_|⟨p, ag⟩) := ag' + · simp [CMRA.op, op, optionOp, CMRA.ValidN, ValidN] + intro Hq a' Hag HR + refine ⟨Hq, a', Hag, ?_⟩ + have He := toAgree.inj Hag + have HR' := ViewRel.mono HR He.symm (CMRA.incN_op_right n UCMRA.unit bf) n.le_refl + apply ViewRel.mono (Hup n bf HR') He ?_ n.le_refl + apply Iris.OFE.Dist.to_incN + refine CMRA.comm.dist.trans (.trans ?_ CMRA.comm.dist) + refine CMRA.op_ne.ne ?_ + exact (CMRA.unit_left_id_dist _) + · rintro ⟨Hv, a0, Hag, Hrel⟩ + refine ⟨Hv, ?_⟩ + simp + exists a0 + refine ⟨Hag, ?_⟩ + simp_all [CMRA.op, op] + have Heq := toAgree.incN.mp ⟨ag, Hag.symm⟩ + have HR' := ViewRel.mono Hrel Heq.symm (CMRA.incN_op_right n UCMRA.unit bf) n.le_refl + apply ViewRel.mono (Hup _ _ HR') Heq ?_ n.le_refl + apply Iris.OFE.Dist.to_incN + refine CMRA.comm.dist.trans (.trans ?_ CMRA.comm.dist) + refine CMRA.op_ne.ne ?_ + exact (CMRA.unit_left_id_dist _) + +-- TODO: Local update lemma + +end updates +end View