diff --git a/source/vstd/tokens/map.rs b/source/vstd/tokens/map.rs index 2bfab0501e..826847938b 100644 --- a/source/vstd/tokens/map.rs +++ b/source/vstd/tokens/map.rs @@ -2,14 +2,18 @@ //! //! - [`GhostMapAuth`] represents authoritative ownership of the entire map; //! - [`GhostSubmap`] represents client ownership of a submap; +//! - [`GhostPersistentSubmap`] represents duplicable client knowledge of a submap which will never change; //! - [`GhostPointsTo`] represents client ownership of a single key-value pair. +//! - [`GhostPersistentPointsTo`] represents duplicable client knowledge of a single key-value pair which will never change. //! -//! Updating the authoritative `GhostMapAuth` requires a `GhostSubmap` containing the keys being updated. +//! Updating the authoritative `GhostMapAuth` requires a `GhostSubmap` containing the keys being updated. //! //! `GhostSubmap`s can be combined or split. //! Whenever a `GhostSubmap` can be used, we can instead use a `GhostPointsTo` (but not vice-versa). //! +//! `GhostPersistentSubmap`s can be combined or split. +//! Whenever a `GhostPersistentSubmap` can be used, we can instead use a `GhostPersistentPointsTo` (but not vice-versa). +//! //! ### Example //! //! ``` @@ -55,6 +59,12 @@ //! assert(auth[5u8] == 55u64); //! assert(auth[6u8] == 66u64); //! +//! // Persist and duplicate the submap +//! let mut psub1 = sub.persist(); +//! assert(psub1[2u8] == 22u64); +//! let psub2 = psub1.duplicate(); +//! assert(psub2[2u8] == 22u64); +//! //! // Not shown in this simple example is the main use case of this resource: //! // maintaining an invariant between GhostMapAuth and some exec-mode //! // shared state with a map view (e.g., HashMap), which states that @@ -74,61 +84,155 @@ verus! { broadcast use super::super::group_vstd_default; +#[verifier::reject_recursive_types(K)] +#[verifier::ext_equal] +enum AuthCarrier { + Auth(Map), + Frac, + Invalid, +} + +#[verifier::reject_recursive_types(K)] +#[verifier::ext_equal] +enum FracCarrier { + Frac { owning: Map, dup: Map }, + Invalid, +} + +impl AuthCarrier { + spec fn valid(self) -> bool { + !(self is Invalid) + } + + spec fn map(self) -> Map + recommends + self.valid(), + { + match self { + AuthCarrier::Auth(m) => m, + AuthCarrier::Frac => Map::empty(), + AuthCarrier::Invalid => Map::empty(), + } + } +} + +impl FracCarrier { + spec fn valid(self) -> bool { + match self { + FracCarrier::Invalid => false, + FracCarrier::Frac { owning, dup } => owning.dom().disjoint(dup.dom()), + } + } + + spec fn owning_map(self) -> Map { + match self { + FracCarrier::Frac { owning, .. } => owning, + FracCarrier::Invalid => Map::empty(), + } + } + + spec fn dup_map(self) -> Map { + match self { + FracCarrier::Frac { dup, .. } => dup, + FracCarrier::Invalid => Map::empty(), + } + } +} + #[verifier::reject_recursive_types(K)] #[verifier::ext_equal] // This struct represents the underlying resource algebra for GhostMaps struct MapCarrier { - auth: Option>>, - frac: Option>, + auth: AuthCarrier, + frac: FracCarrier, } impl PCM for MapCarrier { closed spec fn valid(self) -> bool { - match self.frac { - None => false, - Some(f) => match self.auth { - None => true, - Some(None) => false, - Some(Some(a)) => f.submap_of(a), + match (self.auth, self.frac) { + (AuthCarrier::Invalid, _) => false, + (_, FracCarrier::Invalid) => false, + (AuthCarrier::Auth(auth), FracCarrier::Frac { owning, dup }) => { + &&& owning <= auth + &&& dup <= auth + &&& owning.dom().disjoint(dup.dom()) }, + (AuthCarrier::Frac, FracCarrier::Frac { owning, dup }) => owning.dom().disjoint( + dup.dom(), + ), } } closed spec fn op(self, other: Self) -> Self { - MapCarrier { - auth: if self.auth is Some { - if other.auth is Some { - Some(None) + let auth = match (self.auth, other.auth) { + // Invalid carriers absorb + (AuthCarrier::Invalid, _) => AuthCarrier::Invalid, + (_, AuthCarrier::Invalid) => AuthCarrier::Invalid, + // There can't be two auths + (AuthCarrier::Auth(_), AuthCarrier::Auth(_)) => AuthCarrier::Invalid, + // Fracs remain the same + (AuthCarrier::Frac, AuthCarrier::Frac) => AuthCarrier::Frac, + // Whoever is the auth has precedence + (AuthCarrier::Auth(_), _) => self.auth, + (_, AuthCarrier::Auth(_)) => other.auth, + }; + + let frac = match (self.frac, other.frac) { + // Invalid fracs remain invalid + (FracCarrier::Invalid, _) => FracCarrier::Invalid, + (_, FracCarrier::Invalid) => FracCarrier::Invalid, + // We can mix two owning fracs iff they are disjoint -- we get the union + // There is a tricky element here: + // - one of the fracs may be invalid due to their maps overlapping + // - there is no real way to express this in the typesystem + // - we need to allow that through (because it does not equal Invalid) + ( + FracCarrier::Frac { owning: self_owning, dup: self_dup }, + FracCarrier::Frac { owning: other_owning, dup: other_dup }, + ) => { + let non_overlapping = { + &&& self_owning.dom().disjoint(other_dup.dom()) + &&& other_owning.dom().disjoint(self_dup.dom()) + &&& self_owning.dom().disjoint(other_owning.dom()) + }; + let aggreement = self_dup.agrees(other_dup); + if non_overlapping && aggreement { + FracCarrier::Frac { + owning: self_owning.union_prefer_right(other_owning), + dup: self_dup.union_prefer_right(other_dup), + } } else { - self.auth + FracCarrier::Invalid } - } else { - other.auth }, - frac: match self.frac { - None => None, - Some(sfr) => match other.frac { - None => None, - Some(ofr) => { - if sfr.dom().disjoint(ofr.dom()) { - Some(sfr.union_prefer_right(ofr)) - } else { - None - } - }, - }, - }, - } + }; + + MapCarrier { auth, frac } } closed spec fn unit() -> Self { - MapCarrier { auth: None, frac: Some(Map::empty()) } + MapCarrier { + auth: AuthCarrier::Frac, + frac: FracCarrier::Frac { owning: Map::empty(), dup: Map::empty() }, + } } proof fn closed_under_incl(a: Self, b: Self) { broadcast use lemma_submap_of_trans; - broadcast use lemma_op_frac_submap_of; + let ab = MapCarrier::op(a, b); + lemma_submap_of_op_frac(a, b); + // derive contradiction that the items are disjoint + if !a.frac.owning_map().dom().disjoint(a.frac.dup_map().dom()) { + // The intersection is not empty + lemma_disjoint_iff_empty_intersection( + a.frac.owning_map().dom(), + a.frac.dup_map().dom(), + ); + let a_k = choose|k: K| + a.frac.owning_map().dom().intersect(a.frac.dup_map().dom()).contains(k); + assert(ab.frac.owning_map().dom().intersect(ab.frac.dup_map().dom()).contains(a_k)); // CONTRADICTION + }; } proof fn commutative(a: Self, b: Self) { @@ -154,13 +258,40 @@ impl PCM for MapCarrier { } } -broadcast proof fn lemma_op_frac_submap_of(a: MapCarrier, b: MapCarrier) +proof fn lemma_submap_of_op_frac(a: MapCarrier, b: MapCarrier) + requires + MapCarrier::op(a, b).valid(), + ensures + a.frac.owning_map() <= MapCarrier::op(a, b).frac.owning_map(), + a.frac.dup_map() <= MapCarrier::op(a, b).frac.dup_map(), + b.frac.owning_map() <= MapCarrier::op(a, b).frac.owning_map(), + b.frac.dup_map() <= MapCarrier::op(a, b).frac.dup_map(), +{ + let ab = MapCarrier::op(a, b); + assert(ab.frac.owning_map() == a.frac.owning_map().union_prefer_right(b.frac.owning_map())); + assert(ab.frac.dup_map() == a.frac.dup_map().union_prefer_right(b.frac.dup_map())); + assert(a.frac.owning_map().dom().disjoint(b.frac.owning_map().dom())); +} + +broadcast proof fn lemma_submap_of_op(a: MapCarrier, b: MapCarrier) requires #[trigger] MapCarrier::op(a, b).valid(), ensures - a.frac.unwrap() <= MapCarrier::op(a, b).frac.unwrap(), - b.frac.unwrap() <= MapCarrier::op(a, b).frac.unwrap(), + a.frac.owning_map() <= MapCarrier::op(a, b).frac.owning_map(), + a.frac.dup_map() <= MapCarrier::op(a, b).frac.dup_map(), + a.auth.map() <= MapCarrier::op(a, b).auth.map(), + b.frac.owning_map() <= MapCarrier::op(a, b).frac.owning_map(), + b.frac.dup_map() <= MapCarrier::op(a, b).frac.dup_map(), + b.auth.map() <= MapCarrier::op(a, b).auth.map(), + a.valid(), + b.valid(), { + lemma_submap_of_op_frac(a, b); + MapCarrier::closed_under_incl(a, b); + MapCarrier::commutative(a, b); + MapCarrier::closed_under_incl(b, a); + let ab = MapCarrier::op(a, b); + assert(ab.auth.map() == a.auth.map().union_prefer_right(b.auth.map())); } /// A resource that has the authoritative ownership on the entire map @@ -169,26 +300,56 @@ pub struct GhostMapAuth { r: Resource>, } -/// A resource that has client ownership of a submap +/// A resource that asserts client ownership of a submap. +/// +/// The existence of a [`GhostSubmap`] implies that: +/// - Those keys will remain in the map (unless the onwer of the [`GhostSubmap`] deletes it using [`GhostMapAuth::delete`]); +/// - Those keys will remain pointing to the same values (unless the onwer of the [`GhostSubmap`] updates them using [`GhostSubmap::update`]) +/// - All other [`GhostSubmap`]/[`GhostPointsTo`]/[`GhostPersistentSubmap`]/[`GhostPersistentPointsTo`] are disjoint subsets of the domain #[verifier::reject_recursive_types(K)] pub struct GhostSubmap { r: Resource>, } -/// A resource that has client ownership of a single key-value pair +/// A resource representing duplicable client knowledge of a persistent submap. +/// +/// The existence of a [`GhostPersistentSubmap`] implies that: +/// - Those keys will remain in the map, pointing to the same values, forever; +/// - All other [`GhostSubmap`]/[`GhostPointsTo`]/[`GhostPersistentSubmap`]/[`GhostPersistentPointsTo`] are disjoint subsets of the domain +#[verifier::reject_recursive_types(K)] +pub struct GhostPersistentSubmap { + r: Resource>, +} + +/// A resource that asserts client ownership over a single key in the map. +/// +/// The existence of a [`GhostPointsTo`] implies that: +/// - Those key will remain in the map (unless the onwer of the [`GhostPointsTo`] deletes it using [`GhostMapAuth::delete_points_to`]); +/// - Those key will remain pointing to the same value (unless the onwer of the [`GhostPointsTo`] updates them using [`GhostPointsTo::update`]) +/// - All other [`GhostSubmap`]/[`GhostPointsTo`]/[`GhostPersistentSubmap`]/[`GhostPersistentPointsTo`] are disjoint subsets of the domain #[verifier::reject_recursive_types(K)] pub struct GhostPointsTo { submap: GhostSubmap, } -/// An implementation of a resource for owning a subset of keys in a map. +/// A resource representing duplicable client knowledge of a single key in the map. /// +/// The existence of a [`GhostPersistentPointsTo`] implies that: +/// - The key-value pair will remain in the map, forever; +/// - All other [`GhostSubmap`]/[`GhostPointsTo`]/[`GhostPersistentSubmap`]/[`GhostPersistentPointsTo`] are disjoint subsets of the domain +#[verifier::reject_recursive_types(K)] +pub struct GhostPersistentPointsTo { + submap: GhostPersistentSubmap, +} + impl GhostMapAuth { #[verifier::type_invariant] spec fn inv(self) -> bool { - &&& self.r.value().auth is Some - &&& self.r.value().auth.unwrap() is Some - &&& self.r.value().frac == Some(Map::::empty()) + &&& self.r.value().auth is Auth + &&& self.r.value().frac == FracCarrier::Frac { + owning: Map::::empty(), + dup: Map::::empty(), + } } /// Resource location @@ -198,10 +359,10 @@ impl GhostMapAuth { /// Logically underlying [`Map`] pub closed spec fn view(self) -> Map { - self.r.value().auth.unwrap().unwrap() + self.r.value().auth.map() } - /// Domain of the `GhostMapAuth` + /// Domain of the [`GhostMapAuth`] pub open spec fn dom(self) -> Set { self@.dom() } @@ -214,13 +375,13 @@ impl GhostMapAuth { self@[key] } - /// Instantiate a dummy `GhostMapAuth` + /// Instantiate a dummy [`GhostMapAuth`] pub proof fn dummy() -> (tracked result: GhostMapAuth) { let tracked (auth, submap) = GhostMapAuth::::new(Map::empty()); auth } - /// Extract the `GhostMapAuth` from a mutable reference + /// Extract the [`GhostMapAuth`] from a mutable reference pub proof fn take(tracked &mut self) -> (tracked result: GhostMapAuth) ensures result == *old(self), @@ -231,7 +392,7 @@ impl GhostMapAuth { r } - /// Create an empty `GhostSubmap` + /// Create an empty [`GhostSubmap`] pub proof fn empty(tracked &self) -> (tracked result: GhostSubmap) ensures result.id() == self.id(), @@ -241,7 +402,7 @@ impl GhostMapAuth { GhostSubmap::::empty(self.id()) } - /// Insert a `Map` of values, receiving the `GhostSubmap` that asserts ownership over the key + /// Insert a [`Map`] of values, receiving the [`GhostSubmap`] that asserts ownership over the key /// domain inserted. /// /// ``` @@ -265,33 +426,36 @@ impl GhostMapAuth { result@ == m, { broadcast use lemma_submap_of_trans; - broadcast use lemma_op_frac_submap_of; + broadcast use lemma_submap_of_op; let tracked mut mself = Self::dummy(); tracked_swap(self, &mut mself); use_type_invariant(&mself); assert(mself.inv()); - let tracked mut r = mself.r; + let tracked mut self_r = mself.r; - let rr = MapCarrier { - auth: Some(Some(r.value().auth.unwrap().unwrap().union_prefer_right(m))), - frac: Some(m), + let full_carrier = MapCarrier { + auth: AuthCarrier::Auth(self_r.value().auth.map().union_prefer_right(m)), + frac: FracCarrier::Frac { owning: m, dup: Map::empty() }, }; - let tracked r_upd = r.update(rr); + assert(full_carrier.valid()); + let tracked updated_r = self_r.update(full_carrier); - let arr = MapCarrier { auth: r_upd.value().auth, frac: Some(Map::empty()) }; - - let frr = MapCarrier { auth: None, frac: r_upd.value().frac }; + let auth_carrier = MapCarrier { + auth: updated_r.value().auth, + frac: FracCarrier::Frac { owning: Map::empty(), dup: Map::empty() }, + }; + let frac_carrier = MapCarrier { auth: AuthCarrier::Frac, frac: updated_r.value().frac }; - assert(r_upd.value() == MapCarrier::op(arr, frr)); - let tracked (ar, fr) = r_upd.split(arr, frr); - self.r = ar; - GhostSubmap { r: fr } + assert(updated_r.value() == MapCarrier::op(auth_carrier, frac_carrier)); + let tracked (auth_r, frac_r) = updated_r.split(auth_carrier, frac_carrier); + self.r = auth_r; + GhostSubmap { r: frac_r } } - /// Insert a key-value pair, receiving the `GhostPointsTo` that asserts ownerships over the key. + /// Insert a key-value pair, receiving the [`GhostPointsTo`] that asserts ownerships over the key. /// /// ``` /// proof fn insert_example(tracked mut m: GhostMapAuth) -> (tracked r: GhostPointsTo) @@ -330,31 +494,37 @@ impl GhostMapAuth { /// auth.delete(submap) /// } /// ``` - pub proof fn delete(tracked &mut self, tracked f: GhostSubmap) + pub proof fn delete(tracked &mut self, tracked submap: GhostSubmap) requires - f.id() == old(self).id(), + submap.id() == old(self).id(), ensures self.id() == old(self).id(), - self@ == old(self)@.remove_keys(f@.dom()), + self@ == old(self)@.remove_keys(submap@.dom()), { broadcast use lemma_submap_of_trans; - broadcast use lemma_op_frac_submap_of; + broadcast use lemma_submap_of_op; use_type_invariant(&*self); - use_type_invariant(&f); + use_type_invariant(&submap); let tracked mut mself = Self::dummy(); tracked_swap(self, &mut mself); - let tracked mut r = mself.r; + let tracked mut self_r = mself.r; - r = r.join(f.r); + // join the resource with the original carrier + self_r = self_r.join(submap.r); - let ra = r.value().auth.unwrap().unwrap(); - let ra_new = ra.remove_keys(f@.dom()); + // remove keys from the map + let auth_map = self_r.value().auth.map(); + let new_auth_map = auth_map.remove_keys(submap@.dom()); - let rnew = MapCarrier { auth: Some(Some(ra_new)), frac: Some(Map::empty()) }; + let new_r = MapCarrier { + auth: AuthCarrier::Auth(new_auth_map), + frac: FracCarrier::Frac { owning: Map::empty(), dup: Map::empty() }, + }; - self.r = r.update(rnew); + // update the resource + self.r = self_r.update(new_r); } /// Delete a single key from the map @@ -382,8 +552,8 @@ impl GhostMapAuth { self.delete(p.submap); } - /// Create a new `GhostMapAuth` from a `Map`. - /// Gives the other half of ownership in the form of a `GhostSubmap`. + /// Create a new [`GhostMapAuth`] from a [`Map`]. + /// Gives the other half of ownership in the form of a [`GhostSubmap`]. /// /// ``` /// fn example() { @@ -399,32 +569,39 @@ impl GhostMapAuth { result.0@ == m, result.1@ == m, { - let tracked rr = Resource::alloc(MapCarrier { auth: Some(Some(m)), frac: Some(m) }); + let tracked full_r = Resource::alloc( + MapCarrier { + auth: AuthCarrier::Auth(m), + frac: FracCarrier::Frac { owning: m, dup: Map::empty() }, + }, + ); - let arr = MapCarrier { auth: Some(Some(m)), frac: Some(Map::empty()) }; + let auth_carrier = MapCarrier { + auth: AuthCarrier::Auth(m), + frac: FracCarrier::Frac { owning: Map::empty(), dup: Map::empty() }, + }; - let frr = MapCarrier { auth: None, frac: Some(m) }; + let frac_carrier = MapCarrier { + auth: AuthCarrier::Frac, + frac: FracCarrier::Frac { owning: m, dup: Map::empty() }, + }; - assert(rr.value() == MapCarrier::op(arr, frr)); - let tracked (ar, fr) = rr.split(arr, frr); - (GhostMapAuth { r: ar }, GhostSubmap { r: fr }) + assert(full_r.value() == MapCarrier::op(auth_carrier, frac_carrier)); + let tracked (auth_r, frac_r) = full_r.split(auth_carrier, frac_carrier); + (GhostMapAuth { r: auth_r }, GhostSubmap { r: frac_r }) } } -/// A resource representing ownership of a subset of the domain of the map -/// The existence of a `GhostSubmap` implies that: -/// - Those keys will remain in the map; -/// - Those keys will remain pointing to the same values (unless explicitely `update`d) -/// - All other `GhostSubmap`/`GhostPointsTo` are disjoint subsets of the domain impl GhostSubmap { #[verifier::type_invariant] spec fn inv(self) -> bool { - &&& self.r.value().auth is None - &&& self.r.value().frac is Some + &&& self.r.value().auth is Frac + &&& self.r.value().frac is Frac + &&& self.r.value().frac.dup_map().is_empty() } - /// Checks whether the `GhostSubmap` refers to a single key (and thus can be converted to a - /// `GhostPointsTo`). + /// Checks whether the [`GhostSubmap`] refers to a single key (and thus can be converted to a + /// [`GhostPointsTo`]). pub open spec fn is_points_to(self) -> bool { &&& self@.len() == 1 &&& self.dom().finite() @@ -438,10 +615,10 @@ impl GhostSubmap { /// Logically underlying [`Map`] pub closed spec fn view(self) -> Map { - self.r.value().frac.unwrap() + self.r.value().frac.owning_map() } - /// Domain of the `GhostSubmap` + /// Domain of the [`GhostSubmap`] pub open spec fn dom(self) -> Set { self@.dom() } @@ -454,13 +631,13 @@ impl GhostSubmap { self@[key] } - /// Instantiate a dummy `GhostSubmap` + /// Instantiate a dummy [`GhostSubmap`] pub proof fn dummy() -> (tracked result: GhostSubmap) { let tracked (auth, submap) = GhostMapAuth::::new(Map::empty()); submap } - /// Instantiate an empty `GhostSubmap` of a particular id + /// Instantiate an empty [`GhostSubmap`] of a particular id pub proof fn empty(id: int) -> (tracked result: GhostSubmap) ensures result.id() == id, @@ -470,7 +647,7 @@ impl GhostSubmap { GhostSubmap { r } } - /// Extract the `GhostSubmap` from a mutable reference, leaving behind an empty map. + /// Extract the [`GhostSubmap`] from a mutable reference, leaving behind an empty map. pub proof fn take(tracked &mut self) -> (tracked result: GhostSubmap) ensures old(self).id() == self.id(), @@ -485,11 +662,11 @@ impl GhostSubmap { r } - /// Agreement between a `GhostSubmap` and a corresponding `GhostMapAuth` + /// Agreement between a [`GhostSubmap`] and a corresponding [`GhostMapAuth`] /// - /// Verus might not have full context of the `GhostMapAuth` and a corresponding `GhostSubmap`. + /// Verus might not have full context of the [`GhostMapAuth`] and a corresponding [`GhostSubmap`]. /// However, whenever we know that they refer to the same resource (i.e., have matching ids) we - /// can assert that the `GhostSubmap` is a submap of the `GhostMapAuth`. + /// can assert that the [`GhostSubmap`] is a submap of the [`GhostMapAuth`]. /// ``` /// proof fn test(tracked &auth: GhostMapAuth, tracked &sub: GhostSubmap) /// requires @@ -517,11 +694,11 @@ impl GhostSubmap { let tracked joined = self.r.join_shared(&auth.r); joined.validate(); - assert(self.r.value().frac.unwrap() <= joined.value().frac.unwrap()); + assert(self.r.value().frac.owning_map() <= joined.value().frac.owning_map()); } - /// Combining two `GhostSubmap`s is possible. - /// We consume the input `GhostSubmap` and merge it into the first. + /// Combining two [`GhostSubmap`]s is possible. + /// We consume the input [`GhostSubmap`] and merge it into the first. /// We also learn that they were disjoint. pub proof fn combine(tracked &mut self, tracked other: GhostSubmap) requires @@ -540,8 +717,8 @@ impl GhostSubmap { self.r = r.join(other.r); } - /// Combining a `GhostPointsTo` into `GhostSubmap` is possible, in a similar way to the way to combine - /// `GhostSubmap`s. + /// Combining a [`GhostPointsTo`] into [`GhostSubmap`] is possible, in a similar way to the way to combine + /// [`GhostSubmap`]s. pub proof fn combine_points_to(tracked &mut self, tracked other: GhostPointsTo) requires old(self).id() == other.id(), @@ -557,8 +734,7 @@ impl GhostSubmap { self.combine(other.submap); } - /// When we have two `GhostSubmap`s we can prove that they have disjoint domains. - /// This can be used to prove contradictions. + /// When we have two [`GhostSubmap`]s we can prove that they have disjoint domains. pub proof fn disjoint(tracked &mut self, tracked other: &GhostSubmap) requires old(self).id() == other.id(), @@ -572,8 +748,23 @@ impl GhostSubmap { self.r.validate_2(&other.r); } - /// When we have a `GhostSubmap` and a `GhostPointsTo`, we can prove that they are in disjoint - /// domains. This can be used to prove contradictions. + /// When we have a [`GhostSubmap`] and a [`GhostPersistentSubmap`] we can prove that they are in disjoint + /// domains. + pub proof fn disjoint_persistent(tracked &mut self, tracked other: &GhostPersistentSubmap) + requires + old(self).id() == other.id(), + ensures + self.id() == old(self).id(), + self@ == old(self)@, + self@.dom().disjoint(other@.dom()), + { + use_type_invariant(&*self); + use_type_invariant(other); + self.r.validate_2(&other.r); + } + + /// When we have a [`GhostSubmap`] and a [`GhostPointsTo`] we can prove that they are in disjoint + /// domains. pub proof fn disjoint_points_to(tracked &mut self, tracked other: &GhostPointsTo) requires old(self).id() == other.id(), @@ -587,7 +778,25 @@ impl GhostSubmap { self.disjoint(&other.submap); } - /// We can split a `GhostSubmap` based on a set of keys in its domain. + /// When we have a [`GhostSubmap`] and a [`GhostPersistentPointsTo`] we can prove that they are in disjoint + /// domains. + pub proof fn disjoint_persistent_points_to( + tracked &mut self, + tracked other: &GhostPersistentPointsTo, + ) + requires + old(self).id() == other.id(), + ensures + self.id() == old(self).id(), + self@ == old(self)@, + !self@.contains_key(other.key()), + { + use_type_invariant(&*self); + use_type_invariant(other); + self.disjoint_persistent(&other.submap); + } + + /// We can split a [`GhostSubmap`] based on a set of keys in its domain. pub proof fn split(tracked &mut self, s: Set) -> (tracked result: GhostSubmap) requires s <= old(self)@.dom(), @@ -603,17 +812,29 @@ impl GhostSubmap { let tracked mut r = Resource::alloc(MapCarrier::::unit()); tracked_swap(&mut self.r, &mut r); - let rr1 = MapCarrier { auth: None, frac: Some(r.value().frac.unwrap().remove_keys(s)) }; + let self_carrier = MapCarrier { + auth: AuthCarrier::Frac, + frac: FracCarrier::Frac { + owning: r.value().frac.owning_map().remove_keys(s), + dup: r.value().frac.dup_map(), + }, + }; - let rr2 = MapCarrier { auth: None, frac: Some(r.value().frac.unwrap().restrict(s)) }; + let res_carrier = MapCarrier { + auth: AuthCarrier::Frac, + frac: FracCarrier::Frac { + owning: r.value().frac.owning_map().restrict(s), + dup: r.value().frac.dup_map(), + }, + }; - assert(r.value().frac == MapCarrier::op(rr1, rr2).frac); - let tracked (r1, r2) = r.split(rr1, rr2); - self.r = r1; - GhostSubmap { r: r2 } + assert(r.value().frac == MapCarrier::op(self_carrier, res_carrier).frac); + let tracked (self_r, res_r) = r.split(self_carrier, res_carrier); + self.r = self_r; + GhostSubmap { r: res_r } } - /// We can separate a single key out of a `GhostSubmap` + /// We can separate a single key out of a [`GhostSubmap`] pub proof fn split_points_to(tracked &mut self, k: K) -> (tracked result: GhostPointsTo) requires old(self)@.contains_key(k), @@ -630,7 +851,7 @@ impl GhostSubmap { GhostPointsTo { submap } } - /// When we have both the `GhostMapAuth` and a `GhostSubmap` we can update the values for a + /// When we have both the [`GhostMapAuth`] and a [`GhostSubmap`] we can update the values for a /// subset of keys in our submap. /// ``` /// proof fn test(tracked auth: &mut GhostMapAuth, tracked sub: &mut GhostSubmap) @@ -659,42 +880,48 @@ impl GhostSubmap { auth@ == old(auth)@.union_prefer_right(m), { broadcast use lemma_submap_of_trans; - broadcast use lemma_op_frac_submap_of; + broadcast use lemma_submap_of_op; use_type_invariant(&*self); use_type_invariant(&*auth); let tracked mut mself = Self::dummy(); tracked_swap(self, &mut mself); - let tracked mut fr = mself.r; + let tracked mut frac_r = mself.r; let tracked mut mauth = GhostMapAuth::::dummy(); tracked_swap(auth, &mut mauth); - let tracked mut ar = mauth.r; + let tracked mut auth_r = mauth.r; - fr.validate_2(&ar); - let tracked mut r = fr.join(ar); + frac_r.validate_2(&auth_r); + let tracked mut full_r = frac_r.join(auth_r); - assert(r.value().frac == fr.value().frac); + assert(full_r.value().frac.owning_map() == frac_r.value().frac.owning_map()); - let rr = MapCarrier { - auth: Some(Some(r.value().auth.unwrap().unwrap().union_prefer_right(m))), - frac: Some(r.value().frac.unwrap().union_prefer_right(m)), + let auth_carrier = AuthCarrier::Auth(full_r.value().auth.map().union_prefer_right(m)); + let frac_carrier = FracCarrier::Frac { + owning: full_r.value().frac.owning_map().union_prefer_right(m), + dup: Map::empty(), }; + let new_full_carrier = MapCarrier { auth: auth_carrier, frac: frac_carrier }; - let tracked r_upd = r.update(rr); + assert(new_full_carrier.valid()); + let tracked r_upd = full_r.update(new_full_carrier); - let arr = MapCarrier { auth: r_upd.value().auth, frac: Some(Map::empty()) }; - - let frr = MapCarrier { auth: None, frac: r_upd.value().frac }; + let new_auth_carrier = MapCarrier { + auth: r_upd.value().auth, + frac: FracCarrier::Frac { owning: Map::empty(), dup: Map::empty() }, + }; + let new_frac_carrier = MapCarrier { auth: AuthCarrier::Frac, frac: r_upd.value().frac }; + assert(r_upd.value().frac == MapCarrier::op(new_auth_carrier, new_frac_carrier).frac); + assert(r_upd.value() == MapCarrier::op(new_auth_carrier, new_frac_carrier)); - assert(r_upd.value().frac == MapCarrier::op(arr, frr).frac); - let tracked (ar, fr) = r_upd.split(arr, frr); - auth.r = ar; - self.r = fr; + let tracked (new_auth_r, new_frac_r) = r_upd.split(new_auth_carrier, new_frac_carrier); + auth.r = new_auth_r; + self.r = new_frac_r; } - /// Converting a `GhostSubmap` into a `GhostPointsTo` + /// Converting a [`GhostSubmap`] into a [`GhostPointsTo`] pub proof fn points_to(tracked self) -> (tracked r: GhostPointsTo) requires self.is_points_to(), @@ -706,13 +933,326 @@ impl GhostSubmap { r.lemma_map_view(); r } + + /// Convert a [`GhostSubmap`] into a [`GhostPersistentSubmap`] + pub proof fn persist(tracked self) -> (tracked r: GhostPersistentSubmap) + ensures + self@ == r@, + self.id() == r.id(), + { + broadcast use lemma_submap_of_trans; + broadcast use lemma_submap_of_op; + + use_type_invariant(&self); + + let tracked mut r = self.r; + + let self_carrier = MapCarrier { + auth: AuthCarrier::Frac, + frac: FracCarrier::Frac { + owning: self.r.value().frac.owning_map(), + dup: self.r.value().frac.dup_map(), + }, + }; + + let res_carrier = MapCarrier { + auth: AuthCarrier::Frac, + frac: FracCarrier::Frac { + owning: self.r.value().frac.dup_map(), + dup: self.r.value().frac.owning_map(), + }, + }; + + let tracked r = r.update(res_carrier); + GhostPersistentSubmap { r } + } +} + +impl GhostPersistentSubmap { + #[verifier::type_invariant] + spec fn inv(self) -> bool { + &&& self.r.value().auth is Frac + &&& self.r.value().frac is Frac + &&& self.r.value().frac.owning_map().is_empty() + } + + /// Checks whether the [`GhostPersistentSubmap`] refers to a single key (and thus can be converted to a + /// [`GhostPersistentPointsTo`]). + pub open spec fn is_points_to(self) -> bool { + &&& self@.len() == 1 + &&& self.dom().finite() + &&& !self@.is_empty() + } + + /// Resource location + pub closed spec fn id(self) -> Loc { + self.r.loc() + } + + /// Logically underlying [`Map`] + pub closed spec fn view(self) -> Map { + self.r.value().frac.dup_map() + } + + /// Domain of the [`GhostPersistentSubmap`] + pub open spec fn dom(self) -> Set { + self@.dom() + } + + /// Indexing operation `submap[key]` + pub open spec fn spec_index(self, key: K) -> V + recommends + self.dom().contains(key), + { + self@[key] + } + + /// Instantiate a dummy [`GhostPersistentSubmap`] + pub proof fn dummy() -> (tracked result: GhostPersistentSubmap) { + let tracked owned = GhostSubmap::::dummy(); + owned.persist() + } + + /// Instantiate an empty [`GhostPersistentSubmap`] of a particular id + pub proof fn empty(id: int) -> (tracked result: GhostPersistentSubmap) + ensures + result.id() == id, + result@ == Map::::empty(), + { + let tracked r = Resource::create_unit(id); + GhostPersistentSubmap { r } + } + + /// Duplicate the [`GhostPersistentSubmap`] + pub proof fn duplicate(tracked &mut self) -> (tracked result: GhostPersistentSubmap) + ensures + self.id() == result.id(), + old(self).id() == self.id(), + old(self)@ == self@, + result@ == self@, + { + use_type_invariant(&*self); + + let tracked mut owned = Self::empty(self.id()); + let carrier = self.r.value(); + assert(carrier == MapCarrier::op(carrier, carrier)); + + tracked_swap(self, &mut owned); + let tracked (mut orig, new) = owned.r.split(carrier, carrier); + tracked_swap(&mut self.r, &mut orig); + GhostPersistentSubmap { r: new } + } + + /// Agreement between a [`GhostPersistentSubmap`] and a corresponding [`GhostMapAuth`] + /// + /// Verus might not have full context of the [`GhostMapAuth`] and a corresponding [`GhostPersistentSubmap`]. + /// However, whenever we know that they refer to the same resource (i.e., have matching ids) we + /// can assert that the [`GhostPersistentSubmap`] is a submap of the [`GhostMapAuth`]. + /// ``` + /// proof fn test(tracked &auth: GhostMapAuth, tracked &sub: GhostPersistentSubmap) + /// requires + /// auth.id() == sub.id(), + /// sub.dom().contains(1int), + /// sub[1int] == 1int, + /// ensures + /// auth[1int] == 1int + /// { + /// sub.agree(auth); + /// assert(sub@ <= auth@); + /// assert(auth[1int] == 1int); + /// } + /// ``` + pub proof fn agree( + tracked self: &GhostPersistentSubmap, + tracked auth: &GhostMapAuth, + ) + requires + self.id() == auth.id(), + ensures + self@ <= auth@, + { + broadcast use lemma_submap_of_trans; + + use_type_invariant(self); + use_type_invariant(auth); + + let tracked joined = self.r.join_shared(&auth.r); + joined.validate(); + assert(self.r.value().frac.dup_map() <= joined.value().frac.dup_map()); + } + + /// Combining two [`GhostPersistentSubmap`]s is possible. + /// We consume the input [`GhostPersistentSubmap`] and merge it into the first. + /// We also learn that they agreed + pub proof fn combine(tracked &mut self, tracked other: GhostPersistentSubmap) + requires + old(self).id() == other.id(), + ensures + self.id() == old(self).id(), + self@ == old(self)@.union_prefer_right(other@), + old(self)@.agrees(other@), + { + use_type_invariant(&*self); + use_type_invariant(&other); + + let tracked mut r = Resource::alloc(MapCarrier::unit()); + tracked_swap(&mut self.r, &mut r); + r.validate_2(&other.r); + self.r = r.join(other.r); + } + + /// Combining a [`GhostPersistentPointsTo`] into [`GhostPersistentSubmap`] is possible, in a similar way to the way to combine + /// [`GhostPersistentSubmap`]s. + pub proof fn combine_points_to(tracked &mut self, tracked other: GhostPersistentPointsTo) + requires + old(self).id() == other.id(), + ensures + self.id() == old(self).id(), + self@ == old(self)@.insert(other.key(), other.value()), + old(self)@.contains_key(other.key()) ==> old(self)@[other.key()] == other.value(), + { + use_type_invariant(&*self); + use_type_invariant(&other); + + other.lemma_map_view(); + self.combine(other.submap); + } + + /// When we have a [`GhostPersistentSubmap`] and a [`GhostSubmap`] we can prove that they have disjoint domains. + pub proof fn disjoint(tracked &mut self, tracked other: &GhostSubmap) + requires + old(self).id() == other.id(), + ensures + self.id() == old(self).id(), + self@ == old(self)@, + self@.dom().disjoint(other@.dom()), + { + use_type_invariant(&*self); + use_type_invariant(other); + self.r.validate_2(&other.r); + } + + /// When we have two [`GhostPersistentSubmap`]s we can prove that they agree on their intersection. + pub proof fn intersection_agrees(tracked &mut self, tracked other: &GhostPersistentSubmap) + requires + old(self).id() == other.id(), + ensures + self.id() == old(self).id(), + self@ == old(self)@, + self@.agrees(other@), + { + use_type_invariant(&*self); + use_type_invariant(other); + self.r.validate_2(&other.r); + } + + /// When we have a [`GhostPersistentSubmap`] and a [`GhostPointsTo`] we can prove that they are in disjoint + /// domains. + pub proof fn disjoint_points_to(tracked &mut self, tracked other: &GhostPointsTo) + requires + old(self).id() == other.id(), + ensures + self.id() == old(self).id(), + self@ == old(self)@, + !self@.contains_key(other.key()), + { + use_type_invariant(&*self); + use_type_invariant(other); + self.disjoint(&other.submap); + } + + /// When we have a [`GhostPersistentSubmap`] and a [`GhostPersistentPointsTo`], + /// we can prove that either they are disjoint domains or the key-value pair is in the + /// persistent submap. + pub proof fn intersection_agrees_points_to( + tracked &mut self, + tracked other: &GhostPersistentPointsTo, + ) + requires + old(self).id() == other.id(), + ensures + self.id() == old(self).id(), + self@ == old(self)@, + self@.contains_key(other.key()) ==> self@[other.key()] == other.value(), + { + use_type_invariant(&*self); + use_type_invariant(other); + self.intersection_agrees(&other.submap); + } + + /// We can split a [`GhostPersistentSubmap`] based on a set of keys in its domain. + pub proof fn split(tracked &mut self, s: Set) -> (tracked result: GhostPersistentSubmap< + K, + V, + >) + requires + s <= old(self)@.dom(), + ensures + self.id() == old(self).id(), + result.id() == self.id(), + old(self)@ == self@.union_prefer_right(result@), + result@.dom() =~= s, + self@.dom() =~= old(self)@.dom() - s, + { + use_type_invariant(&*self); + + let tracked mut r = Resource::alloc(MapCarrier::::unit()); + tracked_swap(&mut self.r, &mut r); + + let self_carrier = MapCarrier { + auth: AuthCarrier::Frac, + frac: FracCarrier::Frac { + owning: r.value().frac.owning_map(), + dup: r.value().frac.dup_map().remove_keys(s), + }, + }; + + let res_carrier = MapCarrier { + auth: AuthCarrier::Frac, + frac: FracCarrier::Frac { + owning: r.value().frac.owning_map(), + dup: r.value().frac.dup_map().restrict(s), + }, + }; + + assert(r.value().frac == MapCarrier::op(self_carrier, res_carrier).frac); + let tracked (self_r, res_r) = r.split(self_carrier, res_carrier); + self.r = self_r; + GhostPersistentSubmap { r: res_r } + } + + /// We can separate a single key out of a [`GhostPersistentSubmap`] + pub proof fn split_points_to(tracked &mut self, k: K) -> (tracked result: + GhostPersistentPointsTo) + requires + old(self)@.contains_key(k), + ensures + self.id() == old(self).id(), + result.id() == self.id(), + old(self)@ == self@.insert(result.key(), result.value()), + result.key() == k, + self@.dom() =~= old(self)@.dom().remove(k), + { + use_type_invariant(&*self); + + let tracked submap = self.split(set![k]); + GhostPersistentPointsTo { submap } + } + + /// Convert a [`GhostPersistentSubmap`] into a [`GhostPersistentPointsTo`] + pub proof fn points_to(tracked self) -> (tracked r: GhostPersistentPointsTo) + requires + self.is_points_to(), + ensures + self@ == map![r.key() => r.value()], + self.id() == r.id(), + { + let tracked r = GhostPersistentPointsTo { submap: self }; + r.lemma_map_view(); + r + } } -/// A resource representing ownership over a single key in the domain of the map -/// The existence of a `GhostPointsTo` implies that: -/// - The key will remain in the map; -/// - The key will remain pointing to the same value (unless explicitely `update`d) -/// - All other `GhostSubmap`/`GhostPointsTo` are disjoint subsets of the domain impl GhostPointsTo { #[verifier::type_invariant] spec fn inv(self) -> bool { @@ -739,11 +1279,11 @@ impl GhostPointsTo { self.submap[self.key()] } - /// Agreement between a `GhostPointsTo` and a corresponding `GhostMapAuth` + /// Agreement between a [`GhostPointsTo`] and a corresponding [`GhostMapAuth`] /// - /// Verus might not have full context of the `GhostMapAuth` and a corresponding `GhostPointsTo`. + /// Verus might not have full context of the [`GhostMapAuth`] and a corresponding [`GhostPointsTo`]. /// However, whenever we know that they refer to the same resource (i.e., have matching ids) we - /// can assert that the `GhostPointsTo` is a submap of the `GhostMapAuth`. + /// can assert that the [`GhostPointsTo`] is a key-value pair in the [`GhostMapAuth`]. /// ``` /// proof fn test(tracked &auth: GhostMapAuth, tracked &pt: GhostPointsTo) /// requires @@ -765,12 +1305,14 @@ impl GhostPointsTo { use_type_invariant(self); use_type_invariant(auth); + self.lemma_map_view(); self.submap.agree(auth); assert(self.submap@ <= auth@); assert(self.submap@.contains_key(self.key())); + assert(self.submap@.contains_pair(self.key(), self.value())); } - /// We can combine two `GhostPointsTo`s into a `GhostSubmap` + /// We can combine two [`GhostPointsTo`]s into a [`GhostSubmap`] /// We also learn that they were disjoint. pub proof fn combine(tracked self, tracked other: GhostPointsTo) -> (tracked r: GhostSubmap) @@ -790,7 +1332,7 @@ impl GhostPointsTo { submap } - /// Shows that if a two `GhostPointsTo`s are not owning the same key + /// Shows that if a two [`GhostPointsTo`]s are not owning the same key pub proof fn disjoint(tracked &mut self, tracked other: &GhostPointsTo) requires old(self).id() == other.id(), @@ -804,7 +1346,7 @@ impl GhostPointsTo { self.submap.disjoint(&other.submap); } - /// Shows that if a `GhostPointsTo` and a `GhostSubmap` are not owning the same key + /// Shows that if a [`GhostPointsTo`] and a [`GhostSubmap`] are not owning the same key pub proof fn disjoint_submap(tracked &mut self, tracked other: &GhostSubmap) requires old(self).id() == other.id(), @@ -818,6 +1360,40 @@ impl GhostPointsTo { self.submap.disjoint(other); } + /// Shows that if a [`GhostPointsTo`] and a [`GhostPersistentSubmap`] are not owning the same key + pub proof fn disjoint_persistent_submap( + tracked &mut self, + tracked other: &GhostPersistentSubmap, + ) + requires + old(self).id() == other.id(), + ensures + self.id() == old(self).id(), + self@ == old(self)@, + !other.dom().contains(self.key()), + { + use_type_invariant(&*self); + use_type_invariant(other); + self.submap.disjoint_persistent(other); + } + + /// Shows that if a [`GhostPointsTo`] and a [`GhostPersistentPointsTo`] are not owning the same key + pub proof fn disjoint_persistent( + tracked &mut self, + tracked other: &GhostPersistentPointsTo, + ) + requires + old(self).id() == other.id(), + ensures + self.id() == old(self).id(), + self@ == old(self)@, + self.key() != other.key(), + { + use_type_invariant(&*self); + use_type_invariant(other); + self.submap.disjoint_persistent_points_to(other); + } + /// Update pointed to value pub proof fn update(tracked &mut self, tracked auth: &mut GhostMapAuth, v: V) requires @@ -830,7 +1406,7 @@ impl GhostPointsTo { auth@ == old(auth)@.union_prefer_right(map![self.key() => v]), { broadcast use lemma_submap_of_trans; - broadcast use lemma_op_frac_submap_of; + broadcast use lemma_submap_of_op; use_type_invariant(&*self); use_type_invariant(&*auth); @@ -840,10 +1416,9 @@ impl GhostPointsTo { let m = map![self.key() => v]; assert(self.submap@.union_prefer_right(m) == m); self.submap.update(auth, m); - // assert(self.submap@ == m); } - /// Convert the `GhostPointsTo` a `GhostSubset` + /// Convert the [`GhostPointsTo`] a [`GhostSubmap`] pub proof fn submap(tracked self) -> (tracked r: GhostSubmap) ensures r.id() == self.id(), @@ -877,7 +1452,220 @@ impl GhostPointsTo { assert(self.submap@ == map![self.key() => self.value()]); } - /// Can be used to learn what the key-value pair of `GhostPointsTo` is + /// Can be used to learn what the key-value pair of [`GhostPointsTo`] is + pub proof fn lemma_view(self) + ensures + self@ == (self.key(), self.value()), + { + } + + /// Convert a [`GhostPointsTo`] into a [`GhostPersistentPointsTo`] + pub proof fn persist(tracked self) -> (tracked r: GhostPersistentPointsTo) + ensures + self@ == r@, + self.id() == r.id(), + { + use_type_invariant(&self); + self.submap.persist().points_to() + } +} + +impl GhostPersistentPointsTo { + #[verifier::type_invariant] + spec fn inv(self) -> bool { + self.submap.is_points_to() + } + + /// Location of the underlying resource + pub closed spec fn id(self) -> Loc { + self.submap.id() + } + + /// Key-Value pair underlying the points to relationship + pub open spec fn view(self) -> (K, V) { + (self.key(), self.value()) + } + + /// Key of the points to + pub closed spec fn key(self) -> K { + self.submap.dom().choose() + } + + /// Pointed-to value + pub closed spec fn value(self) -> V { + self.submap[self.key()] + } + + /// Duplicate the [`GhostPersistentPointsTo`] + pub proof fn duplicate(tracked &mut self) -> (tracked result: GhostPersistentPointsTo) + ensures + self.id() == result.id(), + old(self).id() == self.id(), + old(self)@ == self@, + result@ == self@, + { + use_type_invariant(&*self); + let tracked submap = self.submap.duplicate(); + GhostPersistentPointsTo { submap } + } + + /// Agreement between a [`GhostPersistentPointsTo`] and a corresponding [`GhostMapAuth`] + /// + /// Verus might not have full context of the [`GhostMapAuth`] and a corresponding [`GhostPersistentPointsTo`]. + /// However, whenever we know that they refer to the same resource (i.e., have matching ids) we + /// can assert that the [`GhostPersistentPointsTo`] is a key-value pair in the [`GhostMapAuth`]. + /// ``` + /// proof fn test(tracked &auth: GhostMapAuth, tracked &pt: GhostPersistentPointsTo) + /// requires + /// auth.id() == sub.id(), + /// pt@ == (1int, 1int) + /// ensures + /// auth[1int] == 1int + /// { + /// pt.agree(auth); + /// assert(auth[1int] == 1int); + /// } + /// ``` + pub proof fn agree( + tracked self: &GhostPersistentPointsTo, + tracked auth: &GhostMapAuth, + ) + requires + self.id() == auth.id(), + ensures + auth@.contains_pair(self.key(), self.value()), + { + use_type_invariant(self); + use_type_invariant(auth); + + self.lemma_map_view(); + self.submap.agree(auth); + assert(self.submap@ <= auth@); + assert(self.submap@.contains_key(self.key())); + } + + /// We can combine two [`GhostPersistentPointsTo`]s into a [`GhostPersistentSubmap`] + pub proof fn combine( + tracked self, + tracked other: GhostPersistentPointsTo, + ) -> (tracked submap: GhostPersistentSubmap) + requires + self.id() == other.id(), + ensures + submap.id() == self.id(), + submap@ == map![self.key() => self.value(), other.key() => other.value()], + self.key() != other.key() ==> submap@.len() == 2, + self.key() == other.key() ==> submap@.len() == 1, + { + use_type_invariant(&self); + use_type_invariant(&other); + + let tracked mut submap = self.submap(); + submap.combine_points_to(other); + + submap + } + + /// When we have a [`GhostPersistentPointsTo`] and a [`GhostPointsTo`], we can prove that they are in disjoint + /// domains. + pub proof fn disjoint(tracked &mut self, tracked other: &GhostPointsTo) + requires + old(self).id() == other.id(), + ensures + self.id() == old(self).id(), + self@ == old(self)@, + self.key() != other.key(), + { + use_type_invariant(&*self); + use_type_invariant(other); + self.disjoint_submap(&other.submap); + } + + /// When we have a [`GhostPersistentPointsTo`] and a [`GhostSubmap`], we can prove that they are in disjoint + /// domains. + pub proof fn disjoint_submap(tracked &mut self, tracked other: &GhostSubmap) + requires + old(self).id() == other.id(), + ensures + self.id() == old(self).id(), + self@ == old(self)@, + !other@.contains_key(self.key()), + { + use_type_invariant(&*self); + use_type_invariant(other); + self.submap.disjoint(&other); + } + + /// Shows that if a client has two [`GhostPersistentPointsTo`]s they are either disjoint or + /// agreeing in values in the intersection + pub proof fn intersection_agrees( + tracked &mut self, + tracked other: &GhostPersistentPointsTo, + ) + requires + old(self).id() == other.id(), + ensures + self.id() == old(self).id(), + self@ == old(self)@, + self.key() == other.key() ==> self.value() == other.value(), + { + use_type_invariant(&*self); + use_type_invariant(other); + self.submap.intersection_agrees_points_to(&other); + } + + /// Shows that if a [`GhostPersistentPointsTo`] and a [`GhostSubmap`] are not owning the same key + pub proof fn intersection_agrees_submap( + tracked &mut self, + tracked other: &GhostPersistentSubmap, + ) + requires + old(self).id() == other.id(), + ensures + self.id() == old(self).id(), + self@ == old(self)@, + other@.contains_key(self.key()) ==> other@[self.key()] == self.value(), + { + use_type_invariant(&*self); + use_type_invariant(other); + self.submap.intersection_agrees(other); + } + + /// Convert the [`GhostPersistentPointsTo`] a [`GhostPersistentSubmap`] + pub proof fn submap(tracked self) -> (tracked r: GhostPersistentSubmap) + ensures + r.id() == self.id(), + r@ == map![self.key() => self.value()], + { + self.lemma_map_view(); + self.submap + } + + proof fn lemma_map_view(tracked &self) + ensures + self.submap@ == map![self.key() => self.value()], + { + use_type_invariant(self); + let key = self.key(); + let target_dom = set![key]; + + assert(self.submap@.dom().len() == 1); + assert(target_dom.len() == 1); + + assert(self.submap@.dom().finite()); + assert(target_dom.finite()); + + assert(self.submap@.dom().contains(key)); + assert(target_dom.contains(key)); + + assert(self.submap@.dom().remove(key).len() == 0); + assert(target_dom.remove(key).len() == 0); + + assert(self.submap@.dom() =~= target_dom); + assert(self.submap@ == map![self.key() => self.value()]); + } + + /// Can be used to learn what the key-value pair of [`GhostPersistentPointsTo`] is pub proof fn lemma_view(self) ensures self@ == (self.key(), self.value()), diff --git a/source/vstd/tokens/set.rs b/source/vstd/tokens/set.rs index 6aeceefdcc..448717b61d 100644 --- a/source/vstd/tokens/set.rs +++ b/source/vstd/tokens/set.rs @@ -2,7 +2,9 @@ //! //! - [`GhostSetAuth`] represents authoritative ownership of the entire set; //! - [`GhostSubset`] represents client ownership of some subset; +//! - [`GhostPersistentSubset`] represents duplicable client knowledge of some persistent subset; //! - [`GhostSingleton`] represents client ownership of a singleton. +//! - [`GhostPersistentSingleton`] represents duplicable client knowledge of a persistent singleton; //! //! Updating the authoritative `GhostSetAuth` requires a `GhostSubset` containing //! the values being updated. @@ -10,6 +12,9 @@ //! `GhostSubset`s can be combined or split. //! Whenever a `GhostSubset` can be used, we can instead use a `GhostSingleton` (but not vice-versa). //! +//! `GhostPersistentSubset`s can be combined or split. +//! Whenever a `GhostPersistentSubset` can be used, we can instead use a `GhostPersistentSingleton` (but not vice-versa). +//! //! ### Example //! //! ``` @@ -44,6 +49,12 @@ //! assert(sub4@ <= auth@); //! assert(sub@ <= auth@); //! +//! // Persist and duplicate the submap +//! let mut psub1 = sub.persist(); +//! assert(psub1.contains(2u8)); +//! let psub2 = psub1.duplicate(); +//! assert(psub2.contains(2u8)); +//! //! // Not shown in this simple example is the main use case of this resource: //! // maintaining an invariant between GhostSetAuth and some exec-mode //! // shared state with a map view (e.g., HashSet), which states that @@ -60,6 +71,8 @@ use super::super::prelude::*; use super::super::set::*; use super::super::set_lib::*; use super::map::GhostMapAuth; +use super::map::GhostPersistentPointsTo; +use super::map::GhostPersistentSubmap; use super::map::GhostPointsTo; use super::map::GhostSubmap; @@ -87,6 +100,14 @@ pub struct GhostSubset { map: GhostSubmap, } +/// A resource that asserts duplicable client knowledge of a persistent subset +/// +/// For the authoritative resource of the whole set, see [`GhostSetAuth`] +#[verifier::reject_recursive_types(T)] +pub struct GhostPersistentSubset { + map: GhostPersistentSubmap, +} + /// A resource that has client ownership of a singleton /// /// The existence of a [`GhostSingleton`] implies that: @@ -97,6 +118,14 @@ pub struct GhostSingleton { map: GhostPointsTo, } +/// A resource that asserts duplicable client knowledge of a persistent singleton +/// +/// For the authoritative resource of the whole set, see [`GhostSetAuth`] +#[verifier::reject_recursive_types(T)] +pub struct GhostPersistentSingleton { + map: GhostPersistentPointsTo, +} + impl GhostSetAuth { /// Resource location pub closed spec fn id(self) -> Loc { @@ -368,7 +397,20 @@ impl GhostSubset { self.map.disjoint(&other.map); } - /// When we have a [`GhostSubset`] and a [`GhostSingleton`], we can prove that they are in disjoint + /// When we have a [`GhostSubset`] and a [`GhostPersistentSubset`] we can prove that they are in disjoint + /// domains. + pub proof fn disjoint_persistent(tracked &mut self, tracked other: &GhostPersistentSubset) + requires + old(self).id() == other.id(), + ensures + self.id() == old(self).id(), + self@ == old(self)@, + self@.disjoint(other@), + { + self.map.disjoint_persistent(&other.map); + } + + /// When we have a [`GhostSubset`] and a [`GhostSingleton`] we can prove that they are in disjoint /// domains. pub proof fn disjoint_singleton(tracked &mut self, tracked other: &GhostSingleton) requires @@ -381,6 +423,22 @@ impl GhostSubset { self.map.disjoint_points_to(&other.map); } + /// When we have a [`GhostSubset`] and a [`GhostPersistentSingleton`] we can prove that they are in disjoint + /// domains. + pub proof fn disjoint_persistent_singleton( + tracked &mut self, + tracked other: &GhostPersistentSingleton, + ) + requires + old(self).id() == other.id(), + ensures + self.id() == old(self).id(), + self@ == old(self)@, + !self@.contains(other@), + { + self.map.disjoint_persistent_points_to(&other.map); + } + /// We can split a [`GhostSubset`] based on a set of values pub proof fn split(tracked &mut self, s: Set) -> (tracked result: GhostSubset) requires @@ -422,6 +480,185 @@ impl GhostSubset { let tracked map = self.map.points_to(); GhostSingleton { map } } + + /// Converting a [`GhostSubset`] into a [`GhostPersistentSubset`] + pub proof fn persist(tracked self) -> (tracked r: GhostPersistentSubset) + ensures + self@ == r@, + self.id() == r.id(), + { + let tracked map = self.map.persist(); + GhostPersistentSubset { map } + } +} + +impl GhostPersistentSubset { + /// Checks whether the [`GhostPersistentSubset`] refers to a single key (and thus can be converted to a + /// [`GhostPersistentPointsTo`]). + pub open spec fn is_singleton(self) -> bool { + &&& self@.len() == 1 + &&& self@.finite() + &&& !self@.is_empty() + } + + /// Resource location + pub closed spec fn id(self) -> Loc { + self.map.id() + } + + /// Logically underlying [`Set`] + pub closed spec fn view(self) -> Set { + self.map@.dom() + } + + /// Instantiate a dummy [`GhostPersistentSubset`] + pub proof fn dummy() -> (tracked result: GhostPersistentSubset) { + let tracked map = GhostPersistentSubmap::dummy(); + GhostPersistentSubset { map } + } + + /// Instantiate an empty [`GhostPersistentSubset`] of a particular id + pub proof fn empty(id: int) -> (tracked result: GhostPersistentSubset) + ensures + result.id() == id, + result@ == Set::::empty(), + { + let tracked map = GhostPersistentSubmap::empty(id); + GhostPersistentSubset { map } + } + + /// Duplicate the [`GhostPersistentSubset`] + pub proof fn duplicate(tracked &mut self) -> (tracked result: GhostPersistentSubset) + ensures + self.id() == result.id(), + old(self).id() == self.id(), + old(self)@ == self@, + result@ == self@, + { + let tracked map = self.map.duplicate(); + GhostPersistentSubset { map } + } + + /// Agreement between a [`GhostPersistentSubset`] and a corresponding [`GhostMapAuth`] + /// + /// Verus might not have full context of the [`GhostMapAuth`] and a corresponding [`GhostPersistentSubset`]. + /// However, whenever we know that they refer to the same resource (i.e., have matching ids) we + /// can assert that the [`GhostPersistentSubset`] is a subset of the [`GhostMapAuth`]. + /// ``` + /// proof fn test(tracked &auth: GhostMapAuth, tracked &sub: GhostPersistentSubset) + /// requires + /// auth.id() == sub.id(), + /// sub.dom().contains(1int), + /// sub[1int] == 1int, + /// ensures + /// auth[1int] == 1int + /// { + /// sub.agree(auth); + /// assert(sub@ <= auth@); + /// assert(auth[1int] == 1int); + /// } + /// ``` + pub proof fn agree(tracked self: &GhostPersistentSubset, tracked auth: &GhostSetAuth) + requires + self.id() == auth.id(), + ensures + self@ <= auth@, + { + self.map.agree(&auth.map); + } + + /// Combining two [`GhostPersistentSubset`]s is possible. + /// We consume the input [`GhostPersistentSubset`] and merge it into the first. + /// We also learn that they agreed + pub proof fn combine(tracked &mut self, tracked other: GhostPersistentSubset) + requires + old(self).id() == other.id(), + ensures + self.id() == old(self).id(), + self@ == old(self)@.union(other@), + { + self.map.combine(other.map); + } + + /// Combining a [`GhostPersistentSingleton`] into [`GhostPersistentSubset`] is possible, in a similar way to the way to combine + /// [`GhostPersistentSubset`]s. + pub proof fn combine_points_to(tracked &mut self, tracked other: GhostPersistentSingleton) + requires + old(self).id() == other.id(), + ensures + self.id() == old(self).id(), + self@ == old(self)@.insert(other@), + { + self.map.combine_points_to(other.map); + } + + /// When we have a [`GhostPersistentSubset`] and a [`GhostSubset`] we can prove that they have disjoint domains. + pub proof fn disjoint(tracked &mut self, tracked other: &GhostSubset) + requires + old(self).id() == other.id(), + ensures + self.id() == old(self).id(), + self@ == old(self)@, + self@.disjoint(other@), + { + self.map.disjoint(&other.map); + } + + /// When we have a [`GhostPersistentSubset`] and a [`GhostSingleton`], we can prove that they are in disjoint + /// domains. + pub proof fn disjoint_singleton(tracked &mut self, tracked other: &GhostSingleton) + requires + old(self).id() == other.id(), + ensures + self.id() == old(self).id(), + self@ == old(self)@, + !self@.contains(other@), + { + self.map.disjoint_points_to(&other.map); + } + + /// We can split a [`GhostPersistentSubset`] based on a set of keys in its domain. + pub proof fn split(tracked &mut self, s: Set) -> (tracked result: GhostPersistentSubset) + requires + s <= old(self)@, + ensures + self.id() == old(self).id(), + result.id() == self.id(), + old(self)@ == self@.union(result@), + result@ =~= s, + self@ =~= old(self)@ - s, + { + let tracked map = self.map.split(s); + GhostPersistentSubset { map } + } + + /// We can separate a single value out of a [`GhostPersistentSubset`] + pub proof fn split_singleton(tracked &mut self, v: T) -> (tracked result: + GhostPersistentSingleton) + requires + old(self)@.contains(v), + ensures + self.id() == old(self).id(), + result.id() == self.id(), + old(self)@ == self@.insert(result@), + result@ == v, + self@ =~= old(self)@.remove(v), + { + let tracked map = self.map.split_points_to(v); + GhostPersistentSingleton { map } + } + + /// Convert a [`GhostPersistentSubset`] into a [`GhostPersistentSingleton`] + pub proof fn singleton(tracked self) -> (tracked r: GhostPersistentSingleton) + requires + self.is_singleton(), + ensures + self@ == set![r@], + self.id() == r.id(), + { + let tracked map = self.map.points_to(); + GhostPersistentSingleton { map } + } } impl GhostSingleton { @@ -489,6 +726,18 @@ impl GhostSingleton { self.map.disjoint(&other.map) } + /// Shows that if a [`GhostSingleton`] and a [`GhostPersistentSingleton`] are not owning the same value + pub proof fn disjoint_persistent(tracked &mut self, tracked other: &GhostPersistentSingleton) + requires + old(self).id() == other.id(), + ensures + self.id() == old(self).id(), + self@ == old(self)@, + self@ != other@, + { + self.map.disjoint_persistent(&other.map) + } + /// Shows that if a [`GhostSingleton`] and a [`GhostSubset`] are not owning the same value pub proof fn disjoint_subset(tracked &mut self, tracked other: &GhostSubset) requires @@ -501,6 +750,21 @@ impl GhostSingleton { self.map.disjoint_submap(&other.map); } + /// Shows that if a [`GhostSingleton`] and a [`GhostPersistentSubset`] are not owning the same value + pub proof fn disjoint_persistent_subset( + tracked &mut self, + tracked other: &GhostPersistentSubset, + ) + requires + old(self).id() == other.id(), + ensures + self.id() == old(self).id(), + self@ == old(self)@, + !other@.contains(self@), + { + self.map.disjoint_persistent_submap(&other.map); + } + /// Convert the [`GhostSingleton`] a [`GhostSubset`] pub proof fn subset(tracked self) -> (tracked r: GhostSubset) ensures @@ -510,6 +774,115 @@ impl GhostSingleton { let tracked map = self.map.submap(); GhostSubset { map } } + + /// Converting a [`GhostSingleton`] into a [`GhostPersistentSingleton`] + pub proof fn persist(tracked self) -> (tracked r: GhostPersistentSingleton) + ensures + self@ == r@, + self.id() == r.id(), + { + let tracked map = self.map.persist(); + GhostPersistentSingleton { map } + } +} + +impl GhostPersistentSingleton { + /// Location of the underlying resource + pub closed spec fn id(self) -> Loc { + self.map.id() + } + + /// Value known by the singleton + pub closed spec fn view(self) -> T { + self.map@.0 + } + + /// Duplicate the [`GhostPersistentSingleton`] + pub proof fn duplicate(tracked &mut self) -> (tracked result: GhostPersistentSingleton) + ensures + self.id() == result.id(), + old(self).id() == self.id(), + old(self)@ == self@, + result@ == self@, + { + let tracked map = self.map.duplicate(); + GhostPersistentSingleton { map } + } + + /// Agreement between a [`GhostPersistentSingleton`] and a corresponding [`GhostSetAuth`] + /// + /// Verus might not have full context of the [`GhostSetAuth`] and a corresponding [`GhostPersistentSingleton`]. + /// However, whenever we know that they refer to the same resource (i.e., have matching ids) we + /// can assert that the [`GhostPersistentSingleton`] is a subset of the [`GhostSetAuth`]. + /// ``` + /// proof fn test(tracked &auth: GhostSetAuth, tracked &pt: GhostPersistentSingleton) + /// requires + /// auth.id() == sub.id(), + /// pt@ == 1int + /// ensures + /// auth@.contains(1int) + /// { + /// pt.agree(auth); + /// assert(auth@.contains(1int)); + /// } + /// ``` + pub proof fn agree(tracked self: &GhostPersistentSingleton, tracked auth: &GhostSetAuth) + requires + self.id() == auth.id(), + ensures + auth@.contains(self@), + { + self.map.agree(&auth.map); + } + + /// We can combine two [`GhostPersistentSingleton`]s into a [`GhostPersistentSubset`] + pub proof fn combine(tracked self, tracked other: GhostPersistentSingleton) -> (tracked r: + GhostPersistentSubset) + requires + self.id() == other.id(), + ensures + r.id() == self.id(), + r@ == set![self@, other@], + self@ != other@ ==> r@.len() == 2, + self@ == other@ ==> r@.len() == 1, + { + let tracked map = self.map.combine(other.map); + GhostPersistentSubset { map } + } + + /// Shows that a [`GhostPersistentSingleton`] and a [`GhostSingleton`] are not owning the same value + pub proof fn disjoint(tracked &mut self, tracked other: &GhostSingleton) + requires + old(self).id() == other.id(), + ensures + self.id() == old(self).id(), + self@ == old(self)@, + self@ != other@, + { + self.map.disjoint(&other.map) + } + + /// Shows that if a [`GhostPersistentSingleton`] and a [`GhostSubset`] are not owning the same value + pub proof fn disjoint_subset(tracked &mut self, tracked other: &GhostSubset) + requires + old(self).id() == other.id(), + ensures + self.id() == old(self).id(), + self@ == old(self)@, + !other@.contains(self@), + { + self.map.disjoint_submap(&other.map); + } + + /// Convert the [`GhostPersistentSingleton`] a [`GhostPersistentSubset`] + pub proof fn subset(tracked self) -> (tracked r: GhostPersistentSubset) + ensures + r.id() == self.id(), + r@ == set![self@], + { + let tracked map = self.map.submap(); + GhostPersistentSubset { map } + } } } // verus!