Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499#![allow(unused_imports)]
use super::pervasive::*;use super::prelude::*;use super::set::*;
use verus as verus_skip_verusfmt; // skip verusfmt due to unhandled return-value-patternverus_skip_verusfmt! {
broadcast use { super::set::group_set_lemmas, super::set_lib::group_set_lib_default,};
/// `Map<K, V>` is an abstract map type for specifications./// To use a "map" in compiled code, use an `exec` type like HashMap/// that has a `Map<K, V>` as its specification type.////// An object `map: Map<K, V>` has a _domain_, a set of keys given by [`map.dom()`](Map::dom),/// and a mapping for keys in the domain to values, given by [`map[key]`](Map::index)./// Alternatively, a map can be thought of as a set of `(K, V)` pairs where each key/// appears in at most entry.////// A Map must will always be finite./// To work with infinite maps, see `IMap`.////// Maps can be constructed in a few different ways:/// * [`Map::empty()`] constructs an empty map./// * [`Map::new`] constructs a map given a `Set` that specifies its domain and the mapping/// from keys to values (a _map comprehension_)./// * The [`map!`] macro, to construct small maps of a fixed size./// * By manipulating an existing map with [`Map::insert`] or [`Map::remove`].////// To prove that two maps are equal, it is usually easiest to use the extensionality operator `=~=`.////// `Map` always has a finite domain, so it can be used in recursive types. For instance,/// a type `T` can contain a `Map<T, T>`.#[verifier::ext_equal]#[verifier::external_body]#[verifier::accept_recursive_types(K)]#[verifier::accept_recursive_types(V)]pub tracked struct Map<K, V> { // To prevent Verus's internal checks from rejecting recursive types // using `Map`, we use an artificial definition of `Map` that hides its // inclusion of a function from keys to values. // // To make sure that proofs in this file don't take advantage of // this artificial structure (e.g., to prove that any two `Map`s are // equal), we mark this definition as `external_body`. dummy_key: core::marker::PhantomData<K>, dummy_value: core::marker::PhantomData<V>,}
impl<K, V> Map<K, V> { /// The domain of the map as a set. pub uninterp spec fn dom(self) -> Set<K>;
/// Gets the value that the given key `key` maps to. /// For keys not in the domain, the result is meaningless and arbitrary. pub uninterp spec fn index(self, key: K) -> V recommends self.dom().contains(key), ;
/// Gives a `Map<K, V>` whose domain is given, mapping each key to /// the value given by `fv`. pub uninterp spec fn new(s: Set<K>, fv: spec_fn(K) -> V) -> Map<K, V>;
/// This axiom says that `Map<K, V>::new` produces a `Map` whose domain /// is given, mapping each key `k` to the value given by `fv(k)`. broadcast axiom fn axiom_new(s: Set<K>, fv: spec_fn(K) -> V) ensures #![trigger Self::new(s, fv)] Self::new(s, fv).dom() == s, forall|k| s.contains(k) ==> #[trigger] Self::new(s, fv)[k] == fv(k), ;
/// An empty map. pub closed spec fn empty() -> Map<K, V> { Self::new(Set::<K>::empty(), |k| arbitrary()) }
/// `[]` operator, synonymous with `index` #[verifier::inline] pub open spec fn spec_index(self, key: K) -> V recommends self.dom().contains(key), { self.index(key) }
/// Inserts the given (key, value) pair into the map. /// /// If the key is already present from the map, then its existing value is overwritten /// by the new value. pub closed spec fn insert(self, key: K, value: V) -> Map<K, V> { Map::new(self.dom().insert(key), |k| if k == key { value } else { self[k] }) }
/// Removes the given key and its associated value from the map. /// /// If the key is already absent from the map, then the map is left unchanged. pub closed spec fn remove(self, key: K) -> Map<K, V> { Map::new(self.dom().remove(key), |k| self[k]) }
/// Returns the number of key-value pairs in the map pub open spec fn len(self) -> nat { self.dom().len() }
/// Converts this `Map` into an equivalent `IMap` pub open spec fn to_imap(self) -> IMap<K, V> { IMap::new(|k| self.dom().contains(k), |k| self[k]) }
/// Indicates if this `Map` is equivalent to the given `IMap`. pub open spec fn congruent(self, m2: IMap<K, V>) -> bool { &&& self.dom().congruent(m2.dom()) &&& forall|k| #[trigger] self.dom().contains(k) ==> self[k] == m2[k] }
/// Create an empty tracked map. /// /// This allows us to create a map, which we know is empty, that is _tracked_. pub axiom fn tracked_empty() -> (tracked out_v: Self) ensures out_v == Map::<K, V>::empty(), ;
/// Inserts the given `(key, tracked value)` pair into the map. /// /// If the key is already present from the map, then its existing value is overwritten /// by the new value. pub axiom fn tracked_insert(tracked &mut self, key: K, tracked value: V) ensures *final(self) == Map::insert(*old(self), key, value), ;
/// Removes the given key and its associated _tracked_ value from the map. /// /// The key must exist in the map pub axiom fn tracked_remove(tracked &mut self, key: K) -> (tracked v: V) requires old(self).dom().contains(key), ensures *final(self) == Map::remove(*old(self), key), v == old(self)[key], ;
/// Index into a tracked map, getting a tracked borrow of the value pub axiom fn tracked_borrow(tracked &self, key: K) -> (tracked v: &V) requires self.dom().contains(key), ensures *v == self.index(key), ;
/// Index into a tracked map, getting a tracked mutable borrow of the value pub axiom fn tracked_borrow_mut(tracked &mut self, key: K) -> (tracked v: &mut V) requires self.dom().contains(key), ensures *v == old(self).index(key), *final(self) == old(self).insert(key, *final(v)) ;
/// Split a mutable borrow of a map into two. pub axiom fn tracked_borrow_mut_split(tracked &mut self, keys: Set<K>) -> (tracked (m1, m2): (&mut Self, &mut Self)) requires keys <= self.dom(), ensures *m1 == old(self).restrict(keys), *m2 == old(self).remove_keys(keys), *final(self) == final(m1).union_prefer_right(*final(m2)), ;
/// Change the keys of a map, by reverse lookup in a different map. /// /// For each `(old_key, new_key)` pair in `key_map`, the new map will have `(new_key, old_map[old_key])`. /// Note the new map may be smaller than the old map if the `key_map` omits mappings for some of the old keys. pub axiom fn tracked_map_keys<J>( tracked old_map: Map<K, V>, key_map: Map<J, K>, ) -> (tracked new_map: Map<J, V>) requires forall|j| #![auto] key_map.contains_key(j) ==> old_map.contains_key(key_map[j]), forall|j1, j2| #![auto] j1 != j2 && key_map.contains_key(j1) && key_map.contains_key(j2) ==> key_map[j1] != key_map[j2], ensures new_map.dom() == key_map.dom(), forall|j| key_map.contains_key(j) ==> new_map.contains_key(j) && #[trigger] new_map[j] == old_map[key_map[j]], ;
/// Extract a set of keys (and their corresponding values) out of the map. /// /// This allows us to split a map based on a subset of the domain. pub axiom fn tracked_remove_keys(tracked &mut self, keys: Set<K>) -> (tracked out_map: Map< K, V, >) requires keys.subset_of(old(self).dom()), ensures *final(self) == old(self).remove_keys(keys), out_map == old(self).restrict(keys), ;
/// Consume a tracked map and merge its entries into this tracked map. /// /// The new (key, value) pairs take precedence. pub axiom fn tracked_union_prefer_right(tracked &mut self, tracked right: Self) ensures *final(self) == old(self).union_prefer_right(right), ;}
// Trusted axiomspub broadcast axiom fn axiom_map_index_decreases<K, V>(m: Map<K, V>, key: K) requires m.dom().contains(key), ensures #[trigger](decreases_to!(m => m[key]));
pub broadcast axiom fn axiom_map_decreases_to_entry<K, V>(m: Map<K, V>, key: K) requires m.dom().contains(key), ensures #[trigger](decreases_to!(m => (key, m[key])));
/// Since `Map::new` is uninterpret, this broadcast lemma is needed to establish/// that it produces a map with the given set as its domain.pub broadcast proof fn lemma_map_new_domain<K, V>(s: Set<K>, fv: spec_fn(K) -> V) ensures #![trigger Map::new(s, fv)] Map::new(s, fv).dom() == s,{ broadcast use Map::axiom_new;}
/// Since `Map::new` is closed, this broadcast lemma is needed to establish/// that it produces a map that maps elements using the given function.pub broadcast proof fn lemma_map_new_index<K, V>(s: Set<K>, fv: spec_fn(K) -> V, k: K) requires s.contains(k), ensures #![trigger Map::new(s, fv)[k]] Map::new(s, fv)[k] == fv(k){ broadcast use Map::axiom_new;}
/// The domain of the empty map is the empty setpub broadcast proof fn lemma_map_empty<K, V>() ensures #[trigger] Map::<K, V>::empty().dom() == Set::<K>::empty(),{ broadcast use Map::axiom_new;}
/// The domain of a map after inserting a key-value pair is equivalent to inserting the key into/// the original map's domain set.pub broadcast proof fn lemma_map_insert_domain<K, V>(m: Map<K, V>, key: K, value: V) ensures #[trigger] m.insert(key, value).dom() == m.dom().insert(key),{ broadcast use Map::axiom_new;}
/// Inserting `value` at `key` in `m` results in a map that maps `key` to `value`pub broadcast proof fn lemma_map_insert_same<K, V>(m: Map<K, V>, key: K, value: V) ensures #[trigger] m.insert(key, value)[key] == value,{ broadcast use Map::axiom_new;}
/// Inserting `value` at `key2` does not change the value mapped to by any other keys in `m`./// This has to be an axiom because normally constructing a new map sets values outside/// the domain to arbitrary values.pub broadcast axiom fn axiom_map_insert_different<K, V>(m: Map<K, V>, key1: K, key2: K, value: V) requires key1 != key2, ensures #[trigger] m.insert(key2, value)[key1] == m[key1],;
/// The domain of a map after removing a key-value pair is equivalent to removing the key from/// the original map's domain set.pub broadcast proof fn lemma_map_remove_domain<K, V>(m: Map<K, V>, key: K) ensures #[trigger] m.remove(key).dom() == m.dom().remove(key),{ broadcast use Map::axiom_new;}
/// Removing a key-value pair from a map does not change the value mapped to by/// any other keys in the map./// This has to be an axiom because normally constructing a new map sets values outside/// the domain to arbitrary values.pub broadcast axiom fn axiom_map_remove_different<K, V>(m: Map<K, V>, key1: K, key2: K) requires key1 != key2, ensures #[trigger] m.remove(key2)[key1] == m[key1],;
/// Two maps are equivalent if their domains are equivalent and every key in their domains map to the same value.pub broadcast axiom fn axiom_map_ext_equal<K, V>(m1: Map<K, V>, m2: Map<K, V>) ensures #[trigger] (m1 =~= m2) <==> { &&& m1.dom() =~= m2.dom() &&& forall|k: K| #![auto] m1.dom().contains(k) ==> m1[k] == m2[k] },;
/// Two maps are deeply equivalent if their domains are equivalent and/// every key in their domains map to values that are deeply/// equivalent.pub broadcast proof fn axiom_map_ext_equal_deep<K, V>(m1: Map<K, V>, m2: Map<K, V>) ensures #[trigger] (m1 =~~= m2) <==> { &&& m1.dom() =~~= m2.dom() &&& forall|k: K| #![auto] m1.dom().contains(k) ==> m1[k] =~~= m2[k] },{ axiom_map_ext_equal(m1, m2);}
pub broadcast group group_map_lemmas { axiom_map_index_decreases, axiom_map_decreases_to_entry, lemma_map_new_domain, lemma_map_new_index, lemma_map_empty, lemma_map_insert_domain, lemma_map_insert_same, axiom_map_insert_different, lemma_map_remove_domain, axiom_map_remove_different, axiom_map_ext_equal, axiom_map_ext_equal_deep,}
// Macros#[doc(hidden)]#[macro_export]macro_rules! map_internal { [$($key:expr => $value:expr),* $(,)?] => { $crate::vstd::map::Map::empty() $(.insert($key, $value))* }}
/// Create a map using syntax like `map![key1 => val1, key2 => val, ...]`.////// This is equivalent to `Map::empty().insert(key1, val1).insert(key2, val2)...`.////// Note that this does _not_ require all keys to be distinct. In the case that two/// or more keys are equal, the resulting map uses the value of the rightmost entry.#[macro_export]macro_rules! map { [$($tail:tt)*] => { $crate::vstd::prelude::verus_proof_macro_exprs!($crate::vstd::map::map_internal!($($tail)*)) };}
#[doc(hidden)]#[verifier::inline]pub open spec fn check_argument_is_map<K, V>(m: Map<K, V>) -> Map<K, V> { m}
#[doc(hidden)]pub use map_internal;pub use map;
/// Prove two maps `map1` and `map2` are equal by proving that their values are equal at each key.////// More precisely, `assert_maps_equal!` requires that for each key `k`:/// * `map1` contains `k` in its domain if and only if `map2` does (`map1.dom().contains(k) <==> map2.dom().contains(k)`)/// * If they contain `k` in their domains, then their values are equal (`map1.dom().contains(k) && map2.dom().contains(k) ==> map1[k] == map2[k]`)////// The property that equality follows from these facts is often called _extensionality_.////// `assert_maps_equal!` can handle many trivial-looking/// identities without any additional help:////// ```rust/// proof fn insert_remove(m: Map<int, int>, k: int, v: int)/// requires !m.dom().contains(k)/// ensures m.insert(k, v).remove(k) == m/// {/// let m2 = m.insert(k, v).remove(k);/// assert_maps_equal!(m == m2);/// assert(m == m2);/// }/// ```////// For more complex cases, a proof may be required for each key:////// ```rust/// proof fn bitvector_maps() {/// let m1 = Map::<u64, u64>::new(/// |key: u64| key & 31 == key,/// |key: u64| key | 5);////// let m2 = Map::<u64, u64>::new(/// |key: u64| key < 32,/// |key: u64| 5 | key);////// assert_maps_equal!(m1 == m2, key => {/// // Show that the domains of m1 and m2 are the same by showing their predicates/// // are equivalent./// assert_bit_vector((key & 31 == key) <==> (key < 32));////// // Show that the values are the same by showing that these expressions/// // are equivalent./// assert_bit_vector(key | 5 == 5 | key);/// });/// }/// ```#[macro_export]macro_rules! assert_maps_equal { [$($tail:tt)*] => { $crate::vstd::prelude::verus_proof_macro_exprs!($crate::vstd::map::assert_maps_equal_internal!($($tail)*)) };}
#[macro_export]#[doc(hidden)]macro_rules! assert_maps_equal_internal { (::verus_builtin::spec_eq($m1:expr, $m2:expr)) => { assert_maps_equal_internal!($m1, $m2) }; (::verus_builtin::spec_eq($m1:expr, $m2:expr), $k:ident $( : $t:ty )? => $bblock:block) => { assert_maps_equal_internal!($m1, $m2, $k $( : $t )? => $bblock) }; ($m1:expr, $m2:expr $(,)?) => { assert_maps_equal_internal!($m1, $m2, key => { }) }; ($m1:expr, $m2:expr, $k:ident $( : $t:ty )? => $bblock:block) => { #[verifier::spec] let m1 = $crate::vstd::map::check_argument_is_map($m1); #[verifier::spec] let m2 = $crate::vstd::map::check_argument_is_map($m2); $crate::vstd::prelude::assert_by($crate::vstd::prelude::equal(m1, m2), { $crate::vstd::prelude::assert_forall_by(|$k $( : $t )?| { // TODO better error message here: show the individual conjunct that fails, // and maybe give an error message in english as well $crate::vstd::prelude::ensures([ $crate::vstd::prelude::imply(#[verifier::trigger] m1.dom().contains($k), m2.dom().contains($k)) && $crate::vstd::prelude::imply(m2.dom().contains($k), m1.dom().contains($k)) && $crate::vstd::prelude::imply(m1.dom().contains($k) && m2.dom().contains($k), $crate::vstd::prelude::equal(m1.index($k), m2.index($k))) ]); { $bblock } }); $crate::vstd::prelude::assert_($crate::vstd::prelude::ext_equal(m1, m2)); }); }}
#[doc(hidden)]pub use assert_maps_equal_internal;pub use assert_maps_equal;
} // verus!
verus_skip_verusfmt! { // skip verusfmt, issue with 'final'
impl<K, V> Map<K, V> { pub proof fn tracked_map_keys_in_place(tracked &mut self, key_map: Map<K, K>) requires forall|j| #![auto] key_map.dom().contains(j) ==> old(self).dom().contains(key_map.index(j)), forall|j1, j2| #![auto] j1 != j2 && key_map.dom().contains(j1) && key_map.dom().contains(j2) ==> key_map.index(j1) != key_map.index(j2), ensures forall|j| #[trigger] final(self).dom().contains(j) == key_map.dom().contains(j), forall|j| key_map.dom().contains(j) ==> final(self).dom().contains(j) && #[trigger] final(self).index(j) == old(self).index(key_map.index(j)), { let tracked mut tmp = Self::tracked_empty(); super::modes::tracked_swap(&mut tmp, self); let tracked mut tmp = Self::tracked_map_keys(tmp, key_map); super::modes::tracked_swap(&mut tmp, self); }}
} // verus!