Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551552553554555556557558559560561562563564565566567568569570571572573574575576577578579580581582583584585586587588589590591592593594595596597598599600601602603604605606607608609610611612613614615616617618619620621622623624625626627628629630631632633634635636637638639640641642643644645646647648649650651652653654655656657658659660661662663664665666667668669670671672673674675676677678679680681682683684685686687688689690691692693694695696697698699700701702703704705706707708709710711712713714715716717718719720721722723724725726727728729730731732733734735736737738739740741742743744745746747748749750751752753754755756757758759760761762763764765766767768769770771772773774775776777778779780781782783784785786787788789790791792793794795796797798799800801802803804805806807808809810811812813814815816817818819820821822823824825826827828829830831832833834835836837838839840841842843844845846847848849850851852853854855856857858859860861862863864865866867868869870871872873874875876877878879880881882883884885886887888889890891892893894895896897898899900901902903904905906907908909910911912913914915916917918919920921922923924925926927928929930931932933934935936937938939940941942943944945946947948949950951952953954955956957958959960961962963964965966967968969970971972973974975976977978979980981982983984985986987988989990991992993994995996997998999100010011002100310041005100610071008100910101011101210131014101510161017101810191020102110221023102410251026102710281029103010311032103310341035103610371038103910401041104210431044104510461047104810491050105110521053105410551056105710581059106010611062106310641065106610671068106910701071107210731074107510761077107810791080108110821083108410851086108710881089109010911092109310941095109610971098109911001101110211031104110511061107110811091110111111121113111411151116111711181119112011211122112311241125112611271128112911301131113211331134113511361137113811391140114111421143114411451146114711481149115011511152115311541155115611571158115911601161116211631164116511661167116811691170117111721173117411751176117711781179118011811182118311841185118611871188118911901191119211931194119511961197119811991200120112021203120412051206120712081209121012111212121312141215121612171218121912201221122212231224122512261227122812291230123112321233123412351236123712381239124012411242124312441245124612471248124912501251125212531254125512561257125812591260126112621263126412651266126712681269127012711272127312741275127612771278127912801281128212831284128512861287128812891290129112921293129412951296129712981299130013011302130313041305130613071308130913101311131213131314131513161317131813191320132113221323132413251326132713281329133013311332133313341335133613371338133913401341134213431344134513461347134813491350135113521353135413551356135713581359136013611362136313641365136613671368136913701371137213731374137513761377137813791380138113821383138413851386138713881389139013911392139313941395139613971398139914001401140214031404140514061407140814091410141114121413141414151416141714181419142014211422142314241425142614271428142914301431143214331434143514361437143814391440144114421443144414451446144714481449145014511452145314541455145614571458145914601461146214631464146514661467146814691470147114721473147414751476147714781479148014811482148314841485148614871488148914901491149214931494149514961497149814991500150115021503150415051506150715081509151015111512151315141515151615171518151915201521152215231524152515261527152815291530153115321533153415351536153715381539154015411542154315441545154615471548154915501551155215531554155515561557155815591560156115621563156415651566156715681569157015711572157315741575157615771578157915801581158215831584158515861587158815891590159115921593159415951596159715981599160016011602160316041605160616071608160916101611161216131614161516161617161816191620162116221623162416251626162716281629163016311632163316341635163616371638163916401641164216431644164516461647164816491650165116521653165416551656165716581659166016611662166316641665166616671668166916701671167216731674167516761677167816791680168116821683168416851686168716881689169016911692169316941695//! Maps that support ownership of keys//!//! - [`GhostMapAuth<K, V>`] represents authoritative ownership of the entire map;//! - [`GhostSubmap<K, V>`] represents client ownership of a submap;//! - [`GhostPersistentSubmap<K, V>`] represents duplicable client knowledge of a submap which will never change;//! - [`GhostPointsTo<K, V>`] represents client ownership of a single key-value pair.//! - [`GhostPersistentPointsTo<K, V>`] represents duplicable client knowledge of a single key-value pair which will never change.//!//! Updating the authoritative `GhostMapAuth<K, V>` requires a `GhostSubmap<K, V>` containing the keys being updated.//!//! `GhostSubmap<K, V>`s can be combined or split.//! Whenever a `GhostSubmap<K, V>` can be used, we can instead use a `GhostPointsTo<K, V>` (but not vice-versa).//!//! `GhostPersistentSubmap<K, V>`s can be combined or split.//! Whenever a `GhostPersistentSubmap<K, V>` can be used, we can instead use a `GhostPersistentPointsTo<K, V>` (but not vice-versa).//!//! ### Example//!//! ```//! fn example_use() {//! let tracked (mut auth, mut sub) = GhostMapAuth::new(map![1u8 => 1u64, 2u8 => 2u64, 3u8 => 3u64]);//!//! // Allocate some more keys in the auth map, receiving a new submap.//! let tracked sub2 = auth.insert_map(map![4u8 => 4u64, 5u8 => 5u64]);//! proof { sub.combine(sub2); }//!//! // Allocate a single key in the auth map, receiving a points to//! let tracked pt1 = auth.insert(6u8, 6u64);//! proof { sub.combine_points_to(pt1); }//!//! // Delete some keys in the auth map, by returning corresponding submap.//! let tracked sub3 = sub.split(set![3u8, 4u8]);//! proof { auth.delete(sub3); }//!//! // Split the submap into a points to and a submap//! let tracked pt2 = sub.split_points_to(1u8);//! let tracked sub4 = sub.split(set![5u8, 6u8]);//!//! // In general, we might need to call agree() to establish the fact that//! // a points-to/submap has the same values as the auth map. Here, Verus//! // doesn't need agree because it can track where both the auth, points-to//! // and submap came from.//! proof { sub.agree(&auth); }//! proof { pt2.agree(&auth); }//! proof { sub4.agree(&auth); }//!//! assert(pt2.key() == 1u8);//! assert(pt2.value() == auth[1u8]);//! assert(sub4[5u8] == auth[5u8]);//! assert(sub4[6u8] == auth[6u8]);//! assert(sub[2u8] == auth[2u8]);//!//! // Update keys using ownership of submaps.//! proof { sub.update(&mut auth, map![2u8 => 22u64]); }//! proof { pt2.update(&mut auth, 11u64); }//! proof { sub4.update(&mut auth, map![5u8 => 55u64, 6u8 => 66u8]); }//! assert(auth[1u8] == 11u64);//! assert(auth[2u8] == 22u64);//! 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<K, V> and some exec-mode//! // shared state with a map view (e.g., HashMap<K, V>), which states that//! // the Map<K, V> view of GhostMapAuth<K, V> is the same as the view of the//! // HashMap<K, V>, and then handing out a GhostSubmap<K, V> to different//! // clients that might need to operate on different keys in this map.//! }//! ```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_lib::*;use super::super::Loc;use super::super::algebra::ResourceAlgebra;#[cfg(verus_keep_ghost)]use super::super::incorporate;use super::super::pcm::PCM;use super::super::pcm::Resource;#[cfg(verus_keep_ghost)]use super::super::split_mut;
verus! {
broadcast use {super::super::super::group_vstd_default, super::super::super::map::group_map_lemmas};
#[verifier::reject_recursive_types(K)]#[verifier::ext_equal]enum AuthCarrier<K, V> { Auth(Map<K, V>), Frac, Invalid,}
#[verifier::reject_recursive_types(K)]#[verifier::ext_equal]enum FracCarrier<K, V> { Frac { owning: Map<K, V>, dup: Map<K, V> }, Invalid,}
impl<K, V> AuthCarrier<K, V> { spec fn valid(self) -> bool { !(self is Invalid) }
spec fn map(self) -> Map<K, V> recommends self.valid(), { match self { AuthCarrier::Auth(m) => m, AuthCarrier::Frac => Map::empty(), AuthCarrier::Invalid => Map::empty(), } }}
impl<K, V> FracCarrier<K, V> { 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<K, V> { match self { FracCarrier::Frac { owning, .. } => owning, FracCarrier::Invalid => Map::empty(), } }
spec fn dup_map(self) -> Map<K, V> { 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 GhostMapstracked struct MapCarrier<K, V> { auth: AuthCarrier<K, V>, frac: FracCarrier<K, V>,}
impl<K, V> ResourceAlgebra for MapCarrier<K, V> { closed spec fn valid(self) -> bool { 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(a: Self, b: Self) -> Self { let auth = match (a.auth, b.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(_), _) => a.auth, (_, AuthCarrier::Auth(_)) => b.auth, };
let frac = match (a.frac, b.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: a_owning, dup: a_dup }, FracCarrier::Frac { owning: b_owning, dup: b_dup }, ) => { let non_overlapping = { &&& a_owning.dom().disjoint(b_dup.dom()) &&& b_owning.dom().disjoint(a_dup.dom()) &&& a_owning.dom().disjoint(b_owning.dom()) }; let aggreement = a_dup.agrees(b_dup); if non_overlapping && aggreement { FracCarrier::Frac { owning: a_owning.union_prefer_right(b_owning), dup: a_dup.union_prefer_right(b_dup), } } else { FracCarrier::Invalid } }, };
MapCarrier { auth, frac } }
proof fn valid_op(a: Self, b: Self) { broadcast use lemma_submap_of_trans;
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_set_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) { let ab = Self::op(a, b); let ba = Self::op(b, a); assert(ab == ba); }
proof fn associative(a: Self, b: Self, c: Self) { let bc = Self::op(b, c); let ab = Self::op(a, b); let a_bc = Self::op(a, bc); let ab_c = Self::op(ab, c); assert(a_bc == ab_c); }}
impl<K, V> PCM for MapCarrier<K, V> { closed spec fn unit() -> Self { MapCarrier { auth: AuthCarrier::Frac, frac: FracCarrier::Frac { owning: Map::empty(), dup: Map::empty() }, } }
proof fn op_unit(self) { let x = Self::op(self, Self::unit()); assert(self == x); }
proof fn unit_valid() { }}
proof fn lemma_submap_of_op_frac<K, V>(a: MapCarrier<K, V>, b: MapCarrier<K, V>) 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<K, V>(a: MapCarrier<K, V>, b: MapCarrier<K, V>) requires #[trigger] 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(), 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::valid_op(a, b); MapCarrier::commutative(a, b); MapCarrier::valid_op(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#[verifier::reject_recursive_types(K)]pub tracked struct GhostMapAuth<K, V> { r: Resource<MapCarrier<K, V>>,}
/// 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 tracked struct GhostSubmap<K, V> { r: Resource<MapCarrier<K, V>>,}
/// 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`] are disjoint subsets of the domain#[verifier::reject_recursive_types(K)]pub tracked struct GhostPersistentSubmap<K, V> { r: Resource<MapCarrier<K, V>>,}
/// 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 tracked struct GhostPointsTo<K, V> { submap: GhostSubmap<K, V>,}
/// 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`] are disjoint subsets of the domain#[verifier::reject_recursive_types(K)]pub tracked struct GhostPersistentPointsTo<K, V> { submap: GhostPersistentSubmap<K, V>,}
impl<K, V> GhostMapAuth<K, V> { #[verifier::type_invariant] spec fn inv(self) -> bool { &&& self.r.value().auth is Auth &&& self.r.value().frac == FracCarrier::Frac { owning: Map::<K, V>::empty(), dup: Map::<K, V>::empty(), } }
/// Resource location pub closed spec fn id(self) -> Loc { self.r.loc() }
/// Logically underlying [`Map`] pub closed spec fn view(self) -> Map<K, V> { self.r.value().auth.map() }
/// Domain of the [`GhostMapAuth`] pub open spec fn dom(self) -> Set<K> { self@.dom() }
/// Indexing operation `auth[key]` pub open spec fn spec_index(self, key: K) -> V recommends self.dom().contains(key), { self@[key] }
/// Instantiate a dummy [`GhostMapAuth`] pub proof fn dummy() -> (tracked result: GhostMapAuth<K, V>) { let tracked (auth, submap) = GhostMapAuth::<K, V>::new(Map::empty()); auth }
/// Extract the [`GhostMapAuth`] from a mutable reference pub proof fn take(tracked &mut self) -> (tracked result: GhostMapAuth<K, V>) ensures result == *old(self), { use_type_invariant(&*self); let tracked mut r = Self::dummy(); tracked_swap(self, &mut r); r }
/// Create an empty [`GhostSubmap`] pub proof fn empty(tracked &self) -> (tracked result: GhostSubmap<K, V>) ensures result.id() == self.id(), result@ == Map::<K, V>::empty(), { use_type_invariant(self); let tracked r = Resource::<MapCarrier<_, _>>::create_unit(self.r.loc()); GhostSubmap { r } }
/// Insert an [`Map`] of values, receiving the [`GhostSubmap`] that asserts ownership over the key /// domain inserted. /// /// ``` /// proof fn insert_map_example(tracked mut m: GhostMapAuth<int, int>) -> (tracked r: GhostSubmap<int, int>) /// requires /// !m.dom().contains(1int), /// !m.dom().contains(2int), /// { /// let tracked submap = m.insert_map(map![1int => 1int, 2int => 4int]); /// // do something with the submap /// submap /// } /// ``` pub proof fn insert_map(tracked &mut self, m: Map<K, V>) -> (tracked result: GhostSubmap<K, V>) requires old(self)@.dom().disjoint(m.dom()), ensures final(self).id() == old(self).id(), final(self)@ == old(self)@.union_prefer_right(m), result.id() == final(self).id(), result@ == m, { broadcast use lemma_submap_of_trans; 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 self_r = mself.r;
let full_carrier = MapCarrier { auth: AuthCarrier::Auth(self_r.value().auth.map().union_prefer_right(m)), frac: FracCarrier::Frac { owning: m, dup: Map::empty() }, };
assert(full_carrier.valid()); assert forall|c: MapCarrier<K, V>| #[trigger] MapCarrier::op(self_r.value(), c).valid() implies MapCarrier::op( full_carrier, c, ).valid() by { assert(full_carrier.frac.owning_map().dom().disjoint(c.frac.dup_map().dom())); } let tracked updated_r = self_r.update(full_carrier);
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(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. /// /// ``` /// proof fn insert_example(tracked mut m: GhostMapAuth<int, int>) -> (tracked r: GhostPointsTo<int, int>) /// requires /// !m.dom().contains(1int), /// { /// let tracked points_to = m.insert(1, 1); /// // do something with the points_to /// points_to /// } /// ``` pub proof fn insert(tracked &mut self, k: K, v: V) -> (tracked result: GhostPointsTo<K, V>) requires !old(self)@.contains_key(k), ensures final(self).id() == old(self).id(), final(self)@ == old(self)@.insert(k, v), result.id() == final(self).id(), result@ == (k, v), { let tracked submap = self.insert_map(map![k => v]); GhostPointsTo { submap } }
/// Delete a set of keys /// ``` /// proof fn delete(tracked mut auth: GhostMapAuth<int, int>) /// requires /// auth.dom().contains(1int), /// auth.dom().contains(2int), /// ensures /// old(auth)@ == auth@ /// { /// let tracked submap = auth.insert_map(map![1int => 1int, 2int => 4int]); /// // do something with the submap /// auth.delete(submap) /// } /// ``` pub proof fn delete(tracked &mut self, tracked submap: GhostSubmap<K, V>) requires submap.id() == old(self).id(), ensures final(self).id() == old(self).id(), final(self)@ == old(self)@.remove_keys(submap@.dom()), { broadcast use lemma_submap_of_trans; broadcast use lemma_submap_of_op;
use_type_invariant(&*self); use_type_invariant(&submap);
let tracked mut mself = Self::dummy(); tracked_swap(self, &mut mself); let tracked mut self_r = mself.r;
// join the resource with the original carrier self_r = self_r.join(submap.r);
// remove keys from the map let auth_map = self_r.value().auth.map(); let new_auth_map = auth_map.remove_keys(submap@.dom());
let new_r = MapCarrier { auth: AuthCarrier::Auth(new_auth_map), frac: FracCarrier::Frac { owning: Map::empty(), dup: Map::empty() }, };
// update the resource self.r = self_r.update(new_r); }
/// Delete a single key from the map /// ``` /// proof fn delete_key(tracked mut auth: GhostMapAuth<int, 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_points_to(tracked &mut self, tracked p: GhostPointsTo<K, V>) requires p.id() == old(self).id(), ensures final(self).id() == old(self).id(), final(self)@ == old(self)@.remove(p.key()), { use_type_invariant(&p); p.lemma_map_view(); self.delete(p.submap); }
/// Create a new [`GhostMapAuth`] from an [`Map`]. /// Gives the other half of ownership in the form of a [`GhostSubmap`]. /// /// ``` /// fn example() { /// let m = map![1int => 1int, 2int => 4int, 3int => 9int]; /// let tracked (auth, sub) = GhostMapAuth::new(m); /// assert(auth@ == m); /// assert(sub.dom() == m.dom()); /// } /// ``` pub proof fn new(m: Map<K, V>) -> (tracked result: (GhostMapAuth<K, V>, GhostSubmap<K, V>)) ensures result.0.id() == result.1.id(), result.0@ == m, result.1@ == m, { let tracked full_r = Resource::alloc( MapCarrier { auth: AuthCarrier::Auth(m), frac: FracCarrier::Frac { owning: m, dup: Map::empty() }, }, );
let auth_carrier = MapCarrier { auth: AuthCarrier::Auth(m), frac: FracCarrier::Frac { owning: Map::empty(), dup: Map::empty() }, };
let frac_carrier = MapCarrier { auth: AuthCarrier::Frac, frac: FracCarrier::Frac { owning: m, dup: Map::empty() }, };
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 }) }}
impl<K, V> GhostSubmap<K, V> { #[verifier::type_invariant] spec fn inv(self) -> bool { &&& 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`]). pub open spec fn is_points_to(self) -> bool { &&& self@.len() == 1 &&& !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<K, V> { self.r.value().frac.owning_map() }
/// Domain of the [`GhostSubmap`] pub open spec fn dom(self) -> Set<K> { 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 [`GhostSubmap`] pub proof fn dummy() -> (tracked result: GhostSubmap<K, V>) { let tracked (auth, submap) = GhostMapAuth::<K, V>::new(Map::empty()); submap }
/// Create an empty [`GhostSubmap`] pub proof fn empty(tracked &self) -> (tracked result: GhostSubmap<K, V>) ensures result.id() == self.id(), result@ == Map::<K, V>::empty(), { use_type_invariant(self); let tracked r = Resource::<MapCarrier<_, _>>::create_unit(self.r.loc()); GhostSubmap { r } }
/// Extract the [`GhostSubmap`] from a mutable reference, leaving behind an empty map. pub proof fn take(tracked &mut self) -> (tracked result: GhostSubmap<K, V>) ensures old(self).id() == final(self).id(), final(self)@.is_empty(), result == *old(self), result.id() == final(self).id(), { use_type_invariant(&*self);
let tracked mut r = self.empty(); tracked_swap(self, &mut r); r }
/// Agreement between a [`GhostSubmap`] and a corresponding [`GhostMapAuth`] /// /// 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`]. /// ``` /// proof fn test(tracked &auth: GhostMapAuth<int, int>, tracked &sub: GhostSubmap<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: &GhostSubmap<K, V>, tracked auth: &GhostMapAuth<K, V>) 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.owning_map() <= joined.value().frac.owning_map()); }
/// 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<K, V>) requires old(self).id() == other.id(), ensures final(self).id() == old(self).id(), final(self)@ == old(self)@.union_prefer_right(other@), old(self)@.dom().disjoint(other@.dom()), { use_type_invariant(&*self); use_type_invariant(&other);
self.r.validate_2(&other.r); incorporate(&mut self.r, other.r); }
/// 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<K, V>) requires old(self).id() == other.id(), ensures final(self).id() == old(self).id(), final(self)@ == old(self)@.insert(other.key(), other.value()), !old(self)@.contains_key(other.key()), { use_type_invariant(&*self); use_type_invariant(&other);
other.lemma_map_view(); self.combine(other.submap); }
/// When we have two [`GhostSubmap`]s we can prove that they have disjoint domains. pub proof fn disjoint(tracked &mut self, tracked other: &GhostSubmap<K, V>) requires old(self).id() == other.id(), ensures final(self).id() == old(self).id(), final(self)@ == old(self)@, final(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 [`GhostPersistentSubmap`] we can prove that they are in disjoint /// domains. pub proof fn disjoint_persistent(tracked &mut self, tracked other: &GhostPersistentSubmap<K, V>) requires old(self).id() == other.id(), ensures final(self).id() == old(self).id(), final(self)@ == old(self)@, final(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<K, V>) requires old(self).id() == other.id(), ensures final(self).id() == old(self).id(), final(self)@ == old(self)@, !final(self)@.contains_key(other.key()), { use_type_invariant(&*self); use_type_invariant(other); self.disjoint(&other.submap); }
/// 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<K, V>, ) requires old(self).id() == other.id(), ensures final(self).id() == old(self).id(), final(self)@ == old(self)@, !final(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<K>) -> (tracked result: GhostSubmap<K, V>) requires s <= old(self)@.dom(), ensures final(self).id() == old(self).id(), result.id() == final(self).id(), old(self)@ == final(self)@.union_prefer_right(result@), result@.dom() =~= s, final(self)@.dom() =~= old(self)@.dom() - s, { use_type_invariant(&*self);
let self_carrier = MapCarrier { auth: AuthCarrier::Frac, frac: FracCarrier::Frac { owning: self.r.value().frac.owning_map().remove_keys(s), dup: self.r.value().frac.dup_map(), }, };
let res_carrier = MapCarrier { auth: AuthCarrier::Frac, frac: FracCarrier::Frac { owning: self.r.value().frac.owning_map().restrict(s), dup: self.r.value().frac.dup_map(), }, };
assert(self.r.value().frac == MapCarrier::op(self_carrier, res_carrier).frac); let tracked r = split_mut(&mut self.r, self_carrier, res_carrier); GhostSubmap { r } }
pub proof fn split_with_olddom(tracked &mut self, s: Set<K>, olddom: Set<K>) -> (tracked result: GhostSubmap<K, V>) requires olddom == old(self)@.dom(), s <= olddom, ensures final(self).id() == old(self).id(), result.id() == final(self).id(), old(self)@ == final(self)@.union_prefer_right(result@), result@.dom() == s, final(self)@.dom() == olddom - s, { let tracked out = self.split(s); assert(olddom == old(self)@.dom()); assert(self@.dom() == old(self)@.dom() - s); assert(self@.dom() == olddom - s); assert(out@.dom() == s); out }
/// We can separate a single key out of a [`GhostSubmap`] pub proof fn split_points_to(tracked &mut self, k: K) -> (tracked result: GhostPointsTo<K, V>) requires old(self)@.contains_key(k), ensures final(self).id() == old(self).id(), result.id() == final(self).id(), old(self)@ == final(self)@.insert(result.key(), result.value()), result.key() == k, final(self)@ == old(self)@.remove(k), { use_type_invariant(&*self);
let tracked submap = self.split(set![k]); GhostPointsTo { submap } }
/// 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<int, int>, tracked sub: &mut GhostSubmap<int, int>) /// requires /// auth.id() == sub.id(), /// sub.dom() == set![1int, 2int, 3int] /// ensures /// auth[1int] == 9int /// auth[2int] == 10int /// auth[3int] == 11int /// { /// // need to agree on the subset /// sub.agree(auth); /// assert(sub@ <= auth@); /// sub.update(map![1int => 9int, 2int => 10int, 3int => 11int]); /// } /// ``` pub proof fn update(tracked &mut self, tracked auth: &mut GhostMapAuth<K, V>, m: Map<K, V>) requires m.dom() <= old(self)@.dom(), old(self).id() == old(auth).id(), ensures final(self).id() == old(self).id(), final(auth).id() == old(auth).id(), final(self)@ == old(self)@.union_prefer_right(m), final(auth)@ == old(auth)@.union_prefer_right(m), { broadcast use lemma_submap_of_trans; 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 frac_r = mself.r;
let tracked mut mauth = GhostMapAuth::<K, V>::dummy(); tracked_swap(auth, &mut mauth); let tracked mut auth_r = mauth.r;
frac_r.validate_2(&auth_r); let tracked mut full_r = frac_r.join(auth_r);
assert(full_r.value().frac.owning_map() == frac_r.value().frac.owning_map());
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 };
assert(new_full_carrier.valid()); let tracked r_upd = full_r.update(new_full_carrier);
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));
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`] pub proof fn points_to(tracked self) -> (tracked r: GhostPointsTo<K, V>) requires self.is_points_to(), ensures self@ == map![r.key() => r.value()], self.id() == r.id(), { let tracked r = GhostPointsTo { submap: self }; r.lemma_map_view(); r }
/// Convert a [`GhostSubmap`] into a [`GhostPersistentSubmap`] pub proof fn persist(tracked self) -> (tracked r: GhostPersistentSubmap<K, V>) 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<K, V> GhostPersistentSubmap<K, V> { #[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@.is_empty() }
/// Resource location pub closed spec fn id(self) -> Loc { self.r.loc() }
/// Logically underlying [`Map`] pub closed spec fn view(self) -> Map<K, V> { self.r.value().frac.dup_map() }
/// Domain of the [`GhostPersistentSubmap`] pub open spec fn dom(self) -> Set<K> { 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<K, V>) { let tracked owned = GhostSubmap::<K, V>::dummy(); owned.persist() }
/// Create an empty [`GhostPersistentSubmap`] pub proof fn empty(tracked &self) -> (tracked result: GhostPersistentSubmap<K, V>) ensures result.id() == self.id(), result@ == Map::<K, V>::empty(), { use_type_invariant(self); let tracked r = Resource::<MapCarrier<_, _>>::create_unit(self.r.loc()); GhostSubmap { r }.persist() }
/// Duplicate the [`GhostPersistentSubmap`] pub proof fn duplicate(tracked &self) -> (tracked result: GhostPersistentSubmap<K, V>) ensures result.id() == self.id(), result@ == self@, { use_type_invariant(&*self);
assert(MapCarrier::op(self.r.value(), self.r.value()) == self.r.value()); let tracked r = super::super::lib::duplicate(&self.r);
GhostPersistentSubmap { r } }
/// 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<int, int>, tracked &sub: GhostPersistentSubmap<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: &GhostPersistentSubmap<K, V>, tracked auth: &GhostMapAuth<K, V>, ) 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<K, V>) requires old(self).id() == other.id(), ensures final(self).id() == old(self).id(), final(self)@ == old(self)@.union_prefer_right(other@), old(self)@.agrees(other@), { use_type_invariant(&*self); use_type_invariant(&other);
self.r.validate_2(&other.r); incorporate(&mut self.r, 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<K, V>) requires old(self).id() == other.id(), ensures final(self).id() == old(self).id(), final(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<K, V>) requires old(self).id() == other.id(), ensures final(self).id() == old(self).id(), final(self)@ == old(self)@, final(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<K, V>) requires old(self).id() == other.id(), ensures final(self).id() == old(self).id(), final(self)@ == old(self)@, final(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<K, V>) requires old(self).id() == other.id(), ensures final(self).id() == old(self).id(), final(self)@ == old(self)@, !final(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<K, V>, ) requires old(self).id() == other.id(), ensures final(self).id() == old(self).id(), final(self)@ == old(self)@, final(self)@.contains_key(other.key()) ==> final(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<K>) -> (tracked result: GhostPersistentSubmap< K, V, >) requires s <= old(self)@.dom(), ensures final(self).id() == old(self).id(), result.id() == final(self).id(), old(self)@ == final(self)@.union_prefer_right(result@), result@.dom() =~= s, final(self)@.dom() =~= old(self)@.dom() - s, { use_type_invariant(&*self);
let tracked mut r = Resource::alloc(MapCarrier::<K, V>::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<K, V>) requires old(self)@.contains_key(k), ensures final(self).id() == old(self).id(), result.id() == final(self).id(), old(self)@ == final(self)@.insert(result.key(), result.value()), result.key() == k, final(self)@ == old(self)@.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<K, V>) 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 }}
impl<K, V> GhostPointsTo<K, V> { #[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()] }
/// Agreement between a [`GhostPointsTo`] and a corresponding [`GhostMapAuth`] /// /// 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 key-value pair in the [`GhostMapAuth`]. /// ``` /// proof fn test(tracked &auth: GhostMapAuth<int, int>, tracked &pt: GhostPointsTo<int, int>) /// 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: &GhostPointsTo<K, V>, tracked auth: &GhostMapAuth<K, V>) 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@.dom().contains(self.key())); assert(auth@.dom().contains(self.key())); assert(self.submap@[self.key()] == self.value()); assert(auth@[self.key()] == self.value()); }
/// 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<K, V>) -> (tracked r: GhostSubmap<K, V>) requires self.id() == other.id(), ensures r.id() == self.id(), r@ == map![self.key() => self.value(), other.key() => other.value()], self.key() != other.key(), { use_type_invariant(&self); use_type_invariant(&other);
let tracked mut submap = self.submap(); submap.combine_points_to(other);
submap }
/// Shows that if a two [`GhostPointsTo`]s are not owning the same key pub proof fn disjoint(tracked &mut self, tracked other: &GhostPointsTo<K, V>) requires old(self).id() == other.id(), ensures final(self).id() == old(self).id(), final(self)@ == old(self)@, final(self).key() != other.key(), { use_type_invariant(&*self); use_type_invariant(other); self.submap.disjoint(&other.submap); }
/// 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<K, V>) requires old(self).id() == other.id(), ensures final(self).id() == old(self).id(), final(self)@ == old(self)@, !other.dom().contains(final(self).key()), { use_type_invariant(&*self); use_type_invariant(other); 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<K, V>, ) requires old(self).id() == other.id(), ensures final(self).id() == old(self).id(), final(self)@ == old(self)@, !other.dom().contains(final(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<K, V>, ) requires old(self).id() == other.id(), ensures final(self).id() == old(self).id(), final(self)@ == old(self)@, final(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<K, V>, v: V) requires old(self).id() == old(auth).id(), ensures final(self).id() == old(self).id(), final(auth).id() == old(auth).id(), final(self).key() == old(self).key(), final(self)@ == (final(self).key(), v), final(auth)@ == old(auth)@.union_prefer_right(map![final(self).key() => v]), { broadcast use lemma_submap_of_trans; broadcast use lemma_submap_of_op;
use_type_invariant(&*self); use_type_invariant(&*auth);
let ghost old_dom = self.submap.dom(); self.lemma_map_view(); let m = map![self.key() => v]; assert(self.submap@.union_prefer_right(m) == m); self.submap.update(auth, m); }
/// Convert the [`GhostPointsTo`] a [`GhostSubmap`] pub proof fn submap(tracked self) -> (tracked r: GhostSubmap<K, V>) 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().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 [`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<K, V>) ensures self@ == r@, self.id() == r.id(), { use_type_invariant(&self); self.submap.persist().points_to() }}
impl<K, V> GhostPersistentPointsTo<K, V> { #[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 &self) -> (tracked result: GhostPersistentPointsTo<K, V>) ensures result.id() == self.id(), 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<int, int>, tracked &pt: GhostPersistentPointsTo<int, int>) /// 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<K, V>, tracked auth: &GhostMapAuth<K, V>, ) 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<K, V>, ) -> (tracked submap: GhostPersistentSubmap<K, V>) 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<K, V>) requires old(self).id() == other.id(), ensures final(self).id() == old(self).id(), final(self)@ == old(self)@, final(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<K, V>) requires old(self).id() == other.id(), ensures final(self).id() == old(self).id(), final(self)@ == old(self)@, !other@.contains_key(final(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<K, V>, ) requires old(self).id() == other.id(), ensures final(self).id() == old(self).id(), final(self)@ == old(self)@, final(self).key() == other.key() ==> final(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<K, V>, ) requires old(self).id() == other.id(), ensures final(self).id() == old(self).id(), final(self)@ == old(self)@, other@.contains_key(final(self).key()) ==> other@[final(self).key()] == final(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<K, V>) 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().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()), { }}
} // verus!