Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551552553554555556557558559560561562563564565566567568569570571572573574575576577578579580581582583584585586587588589590591592593594595596597598599600601602603604605606607608609610611612613614615616617618619620621622623624625626627628629630631632633634635636637638639640641642643644645646647648649650651652653654655656657658659660661662663664665666667668669670671672673674675676677678679680681682683684685686687688689690691692693694695696697698699700701702703704705706707708709710711712713714715716717718719720721722723724725726727728729730731732733734735736737738739740741742743744745746747748749750751752753754755756757758759760761762763764765766767768769770771772773774775776777778779780781782783784785786787788789790791792793794795796797798799800801802803804805806807808809810811812813814815816817818819820821822823824825826827828829830831832833834835836837838839840841842843844845846847848849850851852853854855856857858859860861862863864865866867868869870871872873874875876877878879880881882883//! Implementation of a resource for ownership of subsets of values in a set//!//! - [`GhostSetAuth<T>`] represents authoritative ownership of the entire set;//! - [`GhostSubset<T>`] represents client ownership of some subset;//! - [`GhostPersistentSubset<T>`] represents duplicable client knowledge of some persistent subset;//! - [`GhostSingleton<T>`] represents client ownership of a singleton.//! - [`GhostPersistentSingleton<T>`] represents duplicable client knowledge of a persistent singleton;//!//! Updating the authoritative `GhostSetAuth<T>` requires a `GhostSubset<T>` containing//! the values being updated.//!//! `GhostSubset<T>`s can be combined or split.//! Whenever a `GhostSubset<T>` can be used, we can instead use a `GhostSingleton<T>` (but not vice-versa).//!//! `GhostPersistentSubset<T>`s can be combined or split.//! Whenever a `GhostPersistentSubset<T>` can be used, we can instead use a `GhostPersistentSingleton<T>` (but not vice-versa).//!//! ### Example//!//! ```//! fn example_use() {//! let tracked (mut auth, mut sub) = GhostSetAuth::new(set![1u8, 2u8, 3u8]);//!//! // Allocate some more values in the auth set, receiving a new subset.//! let tracked sub2 = auth.insert_set(set![4u8, 5u8]);//! proof { sub.combine(sub2); }//!//! // Allocate a single value in the auth set, receiving a points to//! let tracked pt1 = auth.insert(6u8);//! proof { sub.combine_points_to(pt1); }//!//! // Delete some values in the auth set, by returning corresponding subset.//! let tracked sub3 = sub.split(set![3u8, 4u8]);//! proof { auth.delete(sub3); }//!//! // Split the subset into a singleton and a subset//! let tracked pt1 = sub.split_singleton(1u8);//! let tracked sub4 = sub.split(set![5u8, 6u8]);//!//! // In general, we might need to call agree() to establish the fact that//! // a singleton/subset has the same values as the auth set. Here, Verus//! // doesn't need agree because it can track where both the auth, singleton//! // and subset came from.//! proof { sub.agree(&auth); }//! proof { pt1.agree(&auth); }//! proof { sub4.agree(&auth); }//!//! assert(auth@.contains(pt1@));//! 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<T> and some exec-mode//! // shared state with a map view (e.g., HashSet<T>), which states that//! // the Set<T> view of GhostSetAuth<T> is the same as the view of the//! // HashSet<T>, and then handing out a GhostSubset<T> to different//! // clients that might need to operate on different values in the set//! }//! ```use super::super::super::map::*;use super::super::super::map_lib::*;use super::super::super::modes::*;use super::super::super::prelude::*;use super::super::super::set::*;use super::super::super::set_lib::*;use super::super::Loc;use super::map::GhostMapAuth;use super::map::GhostPersistentPointsTo;use super::map::GhostPersistentSubmap;use super::map::GhostPointsTo;use super::map::GhostSubmap;
verus! {
broadcast use super::super::super::group_vstd_default;
/// A resource that has the authoritative ownership on the entire set////// For ownership of only a subset of values, see [`GhostSubset`]./// For ownership of a single value, see [`GhostSingleton`].#[verifier::reject_recursive_types(T)]pub struct GhostSetAuth<T> { map: GhostMapAuth<T, ()>,}
/// A resource that has client ownership of a subset////// The existence of a [`GhostSubset`] implies that:/// - Those values will remain in the set unless ;/// - Those values will remain in the set (unless the onwer of the [`GhostSubset`] deletes it using [`GhostSetAuth::delete`]);/// - All other [`GhostSubset`]/[`GhostSingleton`] are disjoint from it#[verifier::reject_recursive_types(T)]pub struct GhostSubset<T> { map: GhostSubmap<T, ()>,}
/// 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<T> { map: GhostPersistentSubmap<T, ()>,}
/// A resource that has client ownership of a singleton////// The existence of a [`GhostSingleton`] implies that:/// - The value will remain in the set;/// - All other [`GhostSubset`]/[`GhostSingleton`] are disjoint subsets of the domain#[verifier::reject_recursive_types(T)]pub struct GhostSingleton<T> { map: GhostPointsTo<T, ()>,}
/// 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<T> { map: GhostPersistentPointsTo<T, ()>,}
impl<T> GhostSetAuth<T> { /// Resource location pub closed spec fn id(self) -> Loc { self.map.id() }
/// Logically underlying [`Set`] pub closed spec fn view(self) -> Set<T> { self.map@.dom() }
/// Create a new [`GhostSetAuth`] from a [`Set`]. /// Gives the other half of ownership in the form of a [`GhostSubset`] /// /// ``` /// fn example() { /// let s = set![1int, 2int]; /// let tracked (auth, sub) = GhostSetAuth::new(s); /// assert(auth@ == s); /// assert(sub@ == auth@); /// } /// ``` pub proof fn new(s: Set<T>) -> (tracked result: (GhostSetAuth<T>, GhostSubset<T>)) ensures result.0.id() == result.1.id(), result.0@ == s, result.1@ == s, { let m = Map::new(s, |k: T| ()); let tracked (map, submap) = GhostMapAuth::new(m); (GhostSetAuth { map }, GhostSubset { map: submap }) }
/// Instantiate a dummy [`GhostSetAuth`] pub proof fn dummy() -> (tracked result: GhostSetAuth<T>) { let tracked map = GhostMapAuth::dummy(); GhostSetAuth { map } }
/// Extract the [`GhostSetAuth`] from a mutable reference pub proof fn take(tracked &mut self) -> (tracked result: GhostSetAuth<T>) ensures result == *old(self), { let tracked map = self.map.take(); GhostSetAuth { map } }
/// Create an empty [`GhostSubset`] pub proof fn empty(tracked &self) -> (tracked result: GhostSubset<T>) ensures result.id() == self.id(), result@ == Set::<T>::empty(), { let tracked map = self.map.empty(); GhostSubset { map } }
/// Insert a [`Set`] of values, receiving the [`GhostSubset`] that asserts ownership over the set inserted. /// /// ``` /// proof fn insert_set_example(tracked mut m: GhostSetAuth<int>) -> (tracked r: GhostSubset<int>) /// requires /// m@.contains(1int), /// m@.contains(2int), /// { /// let tracked subset = m.insert_set(set![1int, 2int]); /// // do something with the subset /// subset /// } /// ``` pub proof fn insert_set(tracked &mut self, s: Set<T>) -> (tracked result: GhostSubset<T>) requires old(self)@.disjoint(s), ensures final(self).id() == old(self).id(), final(self)@ == old(self)@.union(s), result.id() == final(self).id(), result@ == s, { let m = Map::new(s, |k: T| ()); let tracked submap = self.map.insert_map(m); GhostSubset { map: submap } }
/// Insert a value, receiving the [`GhostSingleton`] that asserts ownerships over the value. /// /// ``` /// proof fn insert_example(tracked mut s: GhostSetAuth<int>) -> (tracked r: GhostSingleton<int>) /// requires /// !m@.contains(1int), /// { /// let tracked singleton = m.insert(1); /// // do something with the singleton /// singleton /// } /// ``` pub proof fn insert(tracked &mut self, v: T) -> (tracked result: GhostSingleton<T>) requires !old(self)@.contains(v), ensures final(self).id() == old(self).id(), final(self)@ == old(self)@.insert(v), result.id() == final(self).id(), result@ == v, { let tracked map = self.map.insert(v, ()); GhostSingleton { map } }
/// Delete a set of values /// ``` /// proof fn delete(tracked mut auth: GhostSetAuth<int>) /// requires /// auth@.contains(1int), /// auth@.contains(2int), /// ensures /// old(auth)@ == auth@ /// { /// let tracked submap = auth.insert_set(set![1int, 2int]); /// // do something with the submap /// auth.delete(submap) /// } /// ``` pub proof fn delete(tracked &mut self, tracked f: GhostSubset<T>) requires f.id() == old(self).id(), ensures final(self).id() == old(self).id(), final(self)@ == old(self)@.difference(f@), { self.map.delete(f.map); }
/// Delete a single key from the map /// ``` /// proof fn delete_key(tracked mut auth: GhostSetAuth<int>) /// requires /// auth.dom().contains(1int), /// ensures /// old(auth)@ == auth@ /// { /// let tracked points_to = auth.insert(1, 1); /// // do something with the submap /// auth.delete_points_to(points_to) /// } /// ``` pub proof fn delete_singleton(tracked &mut self, tracked p: GhostSingleton<T>) requires p.id() == old(self).id(), ensures final(self).id() == old(self).id(), final(self)@ == old(self)@.remove(p@), { self.map.delete_points_to(p.map); }}
impl<T> GhostSubset<T> { /// Checks whether the [`GhostSubset`] refers to a single value (and thus can be converted to a /// [`GhostSingleton`]). pub open spec fn is_singleton(self) -> bool { &&& self@.len() == 1 &&& !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<T> { self.map@.dom() }
/// Instantiate a dummy [`GhostSubset`] pub proof fn dummy() -> (tracked result: GhostSubset<T>) { let tracked map = GhostSubmap::dummy(); GhostSubset { map } }
/// Create an empty [`GhostSubset`] pub proof fn empty(tracked &self) -> (tracked result: GhostSubset<T>) ensures result.id() == self.id(), result@ == Set::<T>::empty(), { let tracked map = self.map.empty(); GhostSubset { map } }
/// Extract the [`GhostSubset`] from a mutable reference, leaving behind an empty map. pub proof fn take(tracked &mut self) -> (tracked result: GhostSubset<T>) ensures old(self).id() == final(self).id(), final(self)@.is_empty(), result == *old(self), result.id() == final(self).id(), { let tracked map = self.map.take(); GhostSubset { map } }
/// Agreement between a [`GhostSubset`] and a corresponding [`GhostSetAuth`] /// /// Verus might not have full context of the [`GhostSetAuth`] and a corresponding [`GhostSubset`]. /// However, whenever we know that they refer to the same resource (i.e., have matching ids) we /// can assert that the [`GhostSubset`] is a submap of the [`GhostSetAuth`]. /// ``` /// proof fn test(tracked &auth: GhostSetAuth<int>, tracked &sub: GhostSubset<int>) /// requires /// auth.id() == sub.id(), /// sub@.contains(1int), /// ensures /// auth@.contains(1int), /// { /// sub.agree(auth); /// assert(sub@ <= auth@); /// assert(auth.contains(1int)); /// } /// ``` pub proof fn agree(tracked self: &GhostSubset<T>, tracked auth: &GhostSetAuth<T>) requires self.id() == auth.id(), ensures self@ <= auth@, { self.map.agree(&auth.map); }
/// Combining two [`GhostSubset`]s is possible. /// We consume the input [`GhostSubset`] and merge it into the first. /// We also learn that they were disjoint. pub proof fn combine(tracked &mut self, tracked other: GhostSubset<T>) requires old(self).id() == other.id(), ensures final(self).id() == old(self).id(), final(self)@ == old(self)@.union(other@), old(self)@.disjoint(other@), { self.map.combine(other.map); }
/// Combining a [`GhostSingleton`] into [`GhostSubset`] is possible, in a similar way to the way to combine /// [`GhostSubset`]s. pub proof fn combine_singleton(tracked &mut self, tracked other: GhostSingleton<T>) requires old(self).id() == other.id(), ensures final(self).id() == old(self).id(), final(self)@ == old(self)@.insert(other@), !old(self)@.contains(other@), { self.map.combine_points_to(other.map); }
/// When we have two [`GhostSubset`]s we can prove that they have disjoint domains. pub proof fn disjoint(tracked &mut self, tracked other: &GhostSubset<T>) requires old(self).id() == other.id(), ensures final(self).id() == old(self).id(), final(self)@ == old(self)@, final(self)@.disjoint(other@), { self.map.disjoint(&other.map); }
/// 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<T>) requires old(self).id() == other.id(), ensures final(self).id() == old(self).id(), final(self)@ == old(self)@, final(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<T>) requires old(self).id() == other.id(), ensures final(self).id() == old(self).id(), final(self)@ == old(self)@, !final(self)@.contains(other@), { 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<T>, ) requires old(self).id() == other.id(), ensures final(self).id() == old(self).id(), final(self)@ == old(self)@, !final(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<T>) -> (tracked result: GhostSubset<T>) requires s <= old(self)@, ensures final(self).id() == old(self).id(), result.id() == final(self).id(), old(self)@ == final(self)@.union(result@), result@ =~= s, final(self)@ =~= old(self)@ - s, { let tracked map = self.map.split(s); GhostSubset { map } }
/// We can separate a single value out of a [`GhostSubset`] pub proof fn split_singleton(tracked &mut self, v: T) -> (tracked result: GhostSingleton<T>) requires old(self)@.contains(v), ensures final(self).id() == old(self).id(), result.id() == final(self).id(), old(self)@ == final(self)@.insert(result@), result@ == v, final(self)@ =~= old(self)@.remove(v), { let tracked map = self.map.split_points_to(v); GhostSingleton { map } }
/// Converting a [`GhostSubset`] into a [`GhostSingleton`] pub proof fn singleton(tracked self) -> (tracked r: GhostSingleton<T>) requires self.is_singleton(), ensures self@ == set![r@], self.id() == r.id(), { let tracked map = self.map.points_to(); GhostSingleton { map } }
/// Converting a [`GhostSubset`] into a [`GhostPersistentSubset`] pub proof fn persist(tracked self) -> (tracked r: GhostPersistentSubset<T>) ensures self@ == r@, self.id() == r.id(), { let tracked map = self.map.persist(); GhostPersistentSubset { map } }}
impl<T> GhostPersistentSubset<T> { /// 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@.is_empty() }
/// Resource location pub closed spec fn id(self) -> Loc { self.map.id() }
/// Logically underlying [`Set`] pub closed spec fn view(self) -> Set<T> { self.map@.dom() }
/// Instantiate a dummy [`GhostPersistentSubset`] pub proof fn dummy() -> (tracked result: GhostPersistentSubset<T>) { let tracked map = GhostPersistentSubmap::dummy(); GhostPersistentSubset { map } }
/// Create an empty [`GhostPersistentSubset`] pub proof fn empty(tracked &self) -> (tracked result: GhostPersistentSubset<T>) ensures result.id() == self.id(), result@ == Set::<T>::empty(), { let tracked map = self.map.empty(); GhostPersistentSubset { map } }
/// Duplicate the [`GhostPersistentSubset`] pub proof fn duplicate(tracked &self) -> (tracked result: GhostPersistentSubset<T>) ensures result@ == self@, result.id() == self.id(), { 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<int, int>, tracked &sub: GhostPersistentSubset<int, int>) /// 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<T>, tracked auth: &GhostSetAuth<T>) 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<T>) requires old(self).id() == other.id(), ensures final(self).id() == old(self).id(), final(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<T>) requires old(self).id() == other.id(), ensures final(self).id() == old(self).id(), final(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<T>) requires old(self).id() == other.id(), ensures final(self).id() == old(self).id(), final(self)@ == old(self)@, final(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<T>) requires old(self).id() == other.id(), ensures final(self).id() == old(self).id(), final(self)@ == old(self)@, !final(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<T>) -> (tracked result: GhostPersistentSubset<T>) requires s <= old(self)@, ensures final(self).id() == old(self).id(), result.id() == final(self).id(), old(self)@ == final(self)@.union(result@), result@ =~= s, final(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<T>) requires old(self)@.contains(v), ensures final(self).id() == old(self).id(), result.id() == final(self).id(), old(self)@ == final(self)@.insert(result@), result@ == v, final(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<T>) requires self.is_singleton(), ensures self@ == set![r@], self.id() == r.id(), { let tracked map = self.map.points_to(); GhostPersistentSingleton { map } }}
impl<T> GhostSingleton<T> { /// Location of the underlying resource pub closed spec fn id(self) -> Loc { self.map.id() }
/// Value owned by the singleton pub closed spec fn view(self) -> T { self.map@.0 }
/// Agreement between a [`GhostSingleton`] and a corresponding [`GhostSetAuth`] /// /// Verus might not have full context of the [`GhostSetAuth`] and a corresponding [`GhostSingleton`]. /// However, whenever we know that they refer to the same resource (i.e., have matching ids) we /// can assert that the [`GhostSingleton`] is a subset of the [`GhostSetAuth`]. /// ``` /// proof fn test(tracked &auth: GhostSetAuth<int>, tracked &pt: GhostSingleton<int>) /// requires /// auth.id() == sub.id(), /// pt@ == 1int /// ensures /// auth@.contains(1int) /// { /// pt.agree(auth); /// assert(auth@.contains(1int)); /// } /// ``` pub proof fn agree(tracked self: &GhostSingleton<T>, tracked auth: &GhostSetAuth<T>) requires self.id() == auth.id(), ensures auth@.contains(self@), { self.map.agree(&auth.map); }
/// We can combine two [`GhostSingleton`]s into a [`GhostSubset`] /// We also learn that they were disjoint. pub proof fn combine(tracked self, tracked other: GhostSingleton<T>) -> (tracked r: GhostSubset< T, >) requires self.id() == other.id(), ensures r.id() == self.id(), r@ == set![self@, other@], self@ != other@, { let tracked map = self.map.combine(other.map); GhostSubset { map } }
/// Shows that if a two [`GhostSingleton`]s are not owning the same value pub proof fn disjoint(tracked &mut self, tracked other: &GhostSingleton<T>) requires old(self).id() == other.id(), ensures final(self).id() == old(self).id(), final(self)@ == old(self)@, final(self)@ != other@, { 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<T>) requires old(self).id() == other.id(), ensures final(self).id() == old(self).id(), final(self)@ == old(self)@, final(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<T>) requires old(self).id() == other.id(), ensures final(self).id() == old(self).id(), final(self)@ == old(self)@, !other@.contains(final(self)@), { 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<T>, ) requires old(self).id() == other.id(), ensures final(self).id() == old(self).id(), final(self)@ == old(self)@, !other@.contains(final(self)@), { self.map.disjoint_persistent_submap(&other.map); }
/// Convert the [`GhostSingleton`] a [`GhostSubset`] pub proof fn subset(tracked self) -> (tracked r: GhostSubset<T>) ensures r.id() == self.id(), r@ == set![self@], { let tracked map = self.map.submap(); GhostSubset { map } }
/// Converting a [`GhostSingleton`] into a [`GhostPersistentSingleton`] pub proof fn persist(tracked self) -> (tracked r: GhostPersistentSingleton<T>) ensures self@ == r@, self.id() == r.id(), { let tracked map = self.map.persist(); GhostPersistentSingleton { map } }}
impl<T> GhostPersistentSingleton<T> { /// 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 &self) -> (tracked result: GhostPersistentSingleton<T>) ensures result@ == self@, result.id() == self.id(), { 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<int>, tracked &pt: GhostPersistentSingleton<int>) /// 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<T>, tracked auth: &GhostSetAuth<T>) 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<T>) -> (tracked r: GhostPersistentSubset<T>) 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<T>) requires old(self).id() == other.id(), ensures final(self).id() == old(self).id(), final(self)@ == old(self)@, final(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<T>) requires old(self).id() == other.id(), ensures final(self).id() == old(self).id(), final(self)@ == old(self)@, !other@.contains(final(self)@), { self.map.disjoint_submap(&other.map); }
/// Convert the [`GhostPersistentSingleton`] a [`GhostPersistentSubset`] pub proof fn subset(tracked self) -> (tracked r: GhostPersistentSubset<T>) ensures r.id() == self.id(), r@ == set![self@], { let tracked map = self.map.submap(); GhostPersistentSubset { map } }}
} // verus!