pub struct Map<K, V> { /* private fields */ }
Expand description
Map<K, V>
is an abstract map type for specifications.
To use a “map” in compiled code, use an exec
type like HashMap (TODO)
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()
,
and a mapping for keys in the domain to values, given by map[key]
.
Alternatively, a map can be thought of as a set of (K, V)
pairs where each key
appears in at most entry.
In general, a map might be infinite.
To work specifically with finite maps, see the self.finite()
predicate.
Maps can be constructed in a few different ways:
Map::empty()
constructs an empty map.Map::new
andMap::total
construct a map given functions that specify 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
orMap::remove
.
To prove that two maps are equal, it is usually easiest to use the extensionality operator =~=
.
Implementations§
Source§impl<K, V> Map<K, V>
impl<K, V> Map<K, V>
Sourcepub open spec fn total(fv: FnSpec<(K,), V>) -> Map<K, V>
pub open spec fn total(fv: FnSpec<(K,), V>) -> Map<K, V>
{ Set::full().mk_map(fv) }
Gives a Map<K, V>
whose domain contains every key, and maps each key
to the value given by fv
.
Sourcepub open spec fn new(fk: FnSpec<(K,), bool>, fv: FnSpec<(K,), V>) -> Map<K, V>
pub open spec fn new(fk: FnSpec<(K,), bool>, fv: FnSpec<(K,), V>) -> Map<K, V>
{ Set::new(fk).mk_map(fv) }
Gives a Map<K, V>
whose domain is given by the boolean predicate on keys fk
,
and maps each key to the value given by fv
.
Sourcepub closed spec fn index(self, key: K) -> V
pub closed spec fn index(self, key: K) -> V
self.dom().contains(key),
Gets the value that the given key key
maps to.
For keys not in the domain, the result is meaningless and arbitrary.
Sourcepub open spec fn spec_index(self, key: K) -> V
pub open spec fn spec_index(self, key: K) -> V
self.dom().contains(key),
{ self.index(key) }
[]
operator, synonymous with index
Sourcepub closed spec fn insert(self, key: K, value: V) -> Map<K, V>
pub closed spec fn insert(self, key: K, value: V) -> Map<K, V>
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.
Sourcepub closed spec fn remove(self, key: K) -> Map<K, V>
pub closed spec fn remove(self, key: K) -> Map<K, V>
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.
Sourcepub open spec fn len(self) -> nat
pub open spec fn len(self) -> nat
{ self.dom().len() }
Returns the number of key-value pairs in the map
Sourcepub proof fn tracked_empty() -> tracked out_v : Self
pub proof fn tracked_empty() -> tracked out_v : Self
out_v == Map::<K, V>::empty(),
Sourcepub proof fn tracked_insert(tracked &mut self, key: K, tracked value: V)
pub proof fn tracked_insert(tracked &mut self, key: K, tracked value: V)
*self == Map::insert(*old(self), key, value),
Sourcepub proof fn tracked_remove(tracked &mut self, key: K) -> tracked v : V
pub proof fn tracked_remove(tracked &mut self, key: K) -> tracked v : V
old(self).dom().contains(key),
ensures*self == Map::remove(*old(self), key),
v == old(self)[key],
todo fill in documentation
Sourcepub proof fn tracked_borrow(tracked &self, key: K) -> tracked v : &V
pub proof fn tracked_borrow(tracked &self, key: K) -> tracked v : &V
self.dom().contains(key),
ensures*v === self.index(key),
Sourcepub proof fn tracked_map_keys<J>(tracked old_map: Map<K, V>, key_map: Map<J, K>) -> tracked new_map : Map<J, V>
pub proof fn tracked_map_keys<J>(tracked old_map: Map<K, V>, key_map: Map<J, K>) -> tracked new_map : Map<J, V>
forall |j| key_map.dom().contains(j) ==> old_map.dom().contains(key_map.index(j)),
forall |j1, j2| {
!equal(j1, j2) && key_map.dom().contains(j1) && key_map.dom().contains(j2)
==> !equal(key_map.index(j1), key_map.index(j2))
},
ensuresforall |j| #[trigger] new_map.dom().contains(j) <==> key_map.dom().contains(j),
forall |j| {
key_map.dom().contains(j)
==> new_map.dom().contains(j)
&& #[trigger] new_map.index(j) == old_map.index(key_map.index(j))
},
Sourcepub proof fn tracked_remove_keys(tracked &mut self, keys: Set<K>) -> tracked out_map : Map<K, V>
pub proof fn tracked_remove_keys(tracked &mut self, keys: Set<K>) -> tracked out_map : Map<K, V>
keys.subset_of(old(self).dom()),
ensuresself == old(self).remove_keys(keys),
out_map == old(self).restrict(keys),
Sourcepub proof fn tracked_union_prefer_right(tracked &mut self, right: Self)
pub proof fn tracked_union_prefer_right(tracked &mut self, right: Self)
*self == old(self).union_prefer_right(right),
Source§impl<K, V> Map<K, V>
impl<K, V> Map<K, V>
Sourcepub proof fn tracked_map_keys_in_place(&mut self, key_map: Map<K, K>)
pub proof fn tracked_map_keys_in_place(&mut self, key_map: Map<K, K>)
forall |j| key_map.dom().contains(j) ==> old(self).dom().contains(key_map.index(j)),
forall |j1, j2| {
j1 != j2 && key_map.dom().contains(j1) && key_map.dom().contains(j2)
==> key_map.index(j1) != key_map.index(j2)
},
ensuresforall |j| #[trigger] self.dom().contains(j) == key_map.dom().contains(j),
forall |j| {
key_map.dom().contains(j)
==> self.dom().contains(j)
&& #[trigger] self.index(j) == old(self).index(key_map.index(j))
},
Source§impl<K, V> Map<K, V>
impl<K, V> Map<K, V>
Sourcepub open spec fn is_full(self) -> bool
pub open spec fn is_full(self) -> bool
{ self.dom().is_full() }
Is true
if called by a “full” map, i.e., a map containing every element of type A
.
Sourcepub open spec fn is_empty(self) -> b : bool
pub open spec fn is_empty(self) -> b : bool
{ self.dom().is_empty() }
Is true
if called by an “empty” map, i.e., a map containing no elements and has length 0
Sourcepub open spec fn contains_key(self, k: K) -> bool
pub open spec fn contains_key(self, k: K) -> bool
{ self.dom().contains(k) }
Returns true if the key k
is in the domain of self
.
Sourcepub open spec fn contains_value(self, v: V) -> bool
pub open spec fn contains_value(self, v: V) -> bool
{ exists |i: K| #[trigger] self.dom().contains(i) && self[i] == v }
Returns true if the value v
is in the range of self
.
Sourcepub open spec fn index_opt(self, k: K) -> Option<V>
pub open spec fn index_opt(self, k: K) -> Option<V>
{ if self.contains_key(k) { Some(self[k]) } else { None } }
Returns Some(v)
if the key k
is in the domain of self
and maps to v
,
and None
if the key k
is not in the domain of self
.
Sourcepub open spec fn values(self) -> Set<V>
pub open spec fn values(self) -> Set<V>
{ Set::<V>::new(|v: V| self.contains_value(v)) }
Returns the set of values in the map.
§Example
let m: Map<int, int> = map![1 => 10, 2 => 11];
assert(m.values() == set![10int, 11int]) by {
assert(m.contains_key(1));
assert(m.contains_key(2));
assert(m.values() =~= set![10int, 11int]);
}
Sourcepub open spec fn kv_pairs(self) -> Set<(K, V)>
pub open spec fn kv_pairs(self) -> Set<(K, V)>
{ Set::<(K, V)>::new(|kv: (K, V)| self.dom().contains(kv.0) && self[kv.0] == kv.1) }
Returns the set of key-value pairs representing the map
§Example
let m: Map<int, int> = map![1 => 10, 2 => 11];
assert(m.kv_pairs() == set![(1int, 10int), (2int, 11int)] by {
assert(m.contains_pair(1int, 10int));
assert(m.contains_pair(2int, 11int));
assert(m.kv_pairs() =~= set![(1int, 10int), (2int, 11int)]);
}
Sourcepub open spec fn contains_pair(self, k: K, v: V) -> bool
pub open spec fn contains_pair(self, k: K, v: V) -> bool
{ self.dom().contains(k) && self[k] == v }
Returns true if the key k
is in the domain of self
, and it maps to the value v
.
Sourcepub open spec fn submap_of(self, m2: Self) -> bool
pub open spec fn submap_of(self, m2: Self) -> bool
{
forall |k: K| {
#[trigger] self.dom().contains(k)
==> #[trigger] m2.dom().contains(k) && self[k] == m2[k]
}
}
Returns true if m1
is contained in m2
, i.e., the domain of m1
is a subset
of the domain of m2
, and they agree on all values in m1
.
§Example
assert(
map![1 => 10, 2 => 11].le(map![1 => 10, 2 => 11, 3 => 12])
);
Sourcepub open spec fn union_prefer_right(self, m2: Self) -> Self
pub open spec fn union_prefer_right(self, m2: Self) -> Self
{
Self::new(
|k: K| self.dom().contains(k) || m2.dom().contains(k),
|k: K| if m2.dom().contains(k) { m2[k] } else { self[k] },
)
}
Gives the union of two maps, defined as:
- The domain is the union of the two input maps.
- For a given key in both input maps, it maps to the same value that it maps to in the right map (
m2
). - For any other key in either input map (but not both), it maps to the same value as it does in that map.
§Example
assert(
map![1 => 10, 2 => 11].union_prefer_right(map![1 => 20, 3 => 13])
=~= map![1 => 20, 2 => 11, 3 => 13]);
Sourcepub open spec fn remove_keys(self, keys: Set<K>) -> Self
pub open spec fn remove_keys(self, keys: Set<K>) -> Self
{ Self::new(|k: K| self.dom().contains(k) && !keys.contains(k), |k: K| self[k]) }
Removes the given keys and their associated values from the map.
Ignores any key in keys
which is not in the domain of self
.
§Example
assert(
map![1 => 10, 2 => 11, 3 => 12].remove_keys(set!{2, 3, 4})
=~= map![1 => 10]);
Sourcepub open spec fn restrict(self, keys: Set<K>) -> Self
pub open spec fn restrict(self, keys: Set<K>) -> Self
{ Self::new(|k: K| self.dom().contains(k) && keys.contains(k), |k: K| self[k]) }
Complement to remove_keys
. Restricts the map to (key, value) pairs
for keys that are in the given set; that is, it removes any keys
not in the set.
§Example
assert(
map![1 => 10, 2 => 11, 3 => 12].remove_keys(set!{2, 3, 4})
=~= map![2 => 11, 3 => 12]);
Sourcepub open spec fn is_equal_on_key(self, m2: Self, key: K) -> bool
pub open spec fn is_equal_on_key(self, m2: Self, key: K) -> bool
{
||| (!self.dom().contains(key) && !m2.dom().contains(key))
||| (self.dom().contains(key) && m2.dom().contains(key) && self[key] == m2[key])
}
Returns true
if and only if the given key maps to the same value or does not exist in self and m2.
Sourcepub open spec fn agrees(self, m2: Self) -> bool
pub open spec fn agrees(self, m2: Self) -> bool
{ forall |k| self.dom().contains(k) && m2.dom().contains(k) ==> self[k] == m2[k] }
Returns true
if the two given maps agree on all keys that their domains share
Sourcepub open spec fn map_entries<W>(self, f: FnSpec<(K, V), W>) -> Map<K, W>
pub open spec fn map_entries<W>(self, f: FnSpec<(K, V), W>) -> Map<K, W>
{ Map::new(|k: K| self.contains_key(k), |k: K| f(k, self[k])) }
Map a function f
over all (k, v) pairs in self
.
Sourcepub open spec fn map_values<W>(self, f: FnSpec<(V,), W>) -> Map<K, W>
pub open spec fn map_values<W>(self, f: FnSpec<(V,), W>) -> Map<K, W>
{ Map::new(|k: K| self.contains_key(k), |k: K| f(self[k])) }
Map a function f
over the values in self
.
Sourcepub open spec fn is_injective(self) -> bool
pub open spec fn is_injective(self) -> bool
{
forall |x: K, y: K| {
x != y && self.dom().contains(x) && self.dom().contains(y)
==> #[trigger] self[x] != #[trigger] self[y]
}
}
Returns true
if and only if a map is injective
Sourcepub open spec fn invert(self) -> Map<V, K>
pub open spec fn invert(self) -> Map<V, K>
{
Map::<
V,
K,
>::new(|v: V| self.contains_value(v), |v: V| choose |k: K| self.contains_pair(k, v))
}
Swaps map keys and values. Values are not required to be unique; no promises on which key is chosen on the intersection.
Sourcepub proof fn lemma_remove_key_len(self, key: K)
pub proof fn lemma_remove_key_len(self, key: K)
self.dom().contains(key),
self.dom().finite(),
ensuresself.dom().len() == 1 + self.remove(key).dom().len(),
Removing a key from a map that previously contained that key decreases the map’s length by one
Sourcepub proof fn lemma_remove_equivalency(self, key: K)
pub proof fn lemma_remove_equivalency(self, key: K)
self.remove(key).dom() == self.dom().remove(key),
The domain of a map after removing a key is equivalent to removing the key from the domain of the original map.
Sourcepub proof fn lemma_remove_keys_len(self, keys: Set<K>)
pub proof fn lemma_remove_keys_len(self, keys: Set<K>)
forall |k: K| #[trigger] keys.contains(k) ==> self.contains_key(k),
keys.finite(),
self.dom().finite(),
ensuresself.remove_keys(keys).dom().len() == self.dom().len() - keys.len(),
Removing a set of n keys from a map that previously contained all n keys results in a domain of size n less than the original domain.
Sourcepub proof fn lemma_invert_is_injective(self)
pub proof fn lemma_invert_is_injective(self)
self.invert().is_injective(),
The function invert
results in an injective map
Sourcepub open spec fn filter_keys(self, p: FnSpec<(K,), bool>) -> Self
pub open spec fn filter_keys(self, p: FnSpec<(K,), bool>) -> Self
{ self.restrict(self.dom().filter(p)) }
Keeps only those key-value pairs whose key satisfies p
.
§Example
proof fn example() {
let m = map![1 => 10, 2 => 20];
let even = |k: int| k % 2 == 0;
assert(m.filter_keys(even) =~= map![2 => 20]);
}
Sourcepub open spec fn get(self, k: K) -> Option<V>
pub open spec fn get(self, k: K) -> Option<V>
{ if self.dom().contains(k) { Some(self[k]) } else { None } }
Returns the value associated with key k
in the map if it exists,
otherwise returns None.
§Example
proof fn get_test() {
let m: Map<int, bool> = map![
1 => true,
2 => false
];
assert(m.get(1) == Some(true));
assert(m.get(3) == None);
}
Sourcepub proof fn get_dom_value_any(self, p: FnSpec<(V,), bool>)
pub proof fn get_dom_value_any(self, p: FnSpec<(V,), bool>)
self.dom().any(|k: K| p(self[k])) <==> self.values().any(p),
A map contains a value satisfying predicate p
iff some key maps to a value satisfying p
.
§Example
proof fn get_dom_value_any_test() {
let m = map![1 => 10, 2 => 20, 3 => 30];
let p = |v: int| v > 25;
assert(m[3] == 30);
assert(m.dom().any(|k| p(m[k])));
}
Sourcepub proof fn lemma_submap_eq_iff(self, m: Self)
pub proof fn lemma_submap_eq_iff(self, m: Self)
(self == m) <==> (self.submap_of(m) && m.submap_of(self)),
Two maps are equal if and only if they are submaps of each other.
§Example
proof fn submap_eq_test() {
let m1 = map![1 => 10, 2 => 20];
let m2 = map![1 => 10, 2 => 20];
let m3 = map![1 => 10, 2 => 30];
assert(m1.submap_of(m2) && m2.submap_of(m1));
assert(m1 == m2);
}
Sourcepub broadcast proof fn lemma_map_remove_keys_insert(self, r: Set<K>, k: K, v: V)
pub broadcast proof fn lemma_map_remove_keys_insert(self, r: Set<K>, k: K, v: V)
#[trigger] self.insert(k, v).remove_keys(r)
== if r.contains(k) { self.remove_keys(r) } else { self.remove_keys(r).insert(k, v) },
When removing a set of keys from a map after inserting (k,v), the result depends on whether k is in the set: if k is in the set, the insertion is discarded; if not, the insertion happens after removal.
§Example
proof fn map_remove_keys_insert_test() {
let m = map![1 => 10, 2 => 20, 3 => 30];
let to_remove = set![2, 4];
// 5 not in m: insert happens after remove
assert(m.insert(5, 15).remove_keys(to_remove) == m.remove_keys(to_remove).insert(5, 15));
// 2 in m: insert is eliminated by remove
assert(m.insert(2, 25).remove_keys(to_remove) == m.remove_keys(to_remove));
}
Sourcepub broadcast proof fn lemma_filter_keys_insert(self, p: FnSpec<(K,), bool>, k: K, v: V)
pub broadcast proof fn lemma_filter_keys_insert(self, p: FnSpec<(K,), bool>, k: K, v: V)
#[trigger] self.insert(k, v).filter_keys(p)
== (if p(k) { self.filter_keys(p).insert(k, v) } else { self.filter_keys(p) }),
Filtering keys after inserting (k, v)
leaves the result unchanged when p(k)
is false,
and otherwise adds (k, v)
to the already-filtered map.
§Example
proof fn example() {
let m = map![1 => 10];
let even = |k: int| k % 2 == 0;
assert(m.insert(3, 30).filter_keys(even) =~= m.filter_keys(even));
assert(m.insert(2, 20).filter_keys(even)
=~= m.filter_keys(even).insert(2, 20));
}
Source§impl<K, V> Map<Seq<K>, V>
impl<K, V> Map<Seq<K>, V>
Sourcepub open spec fn prefixed_entries(self, prefix: Seq<K>) -> Self
pub open spec fn prefixed_entries(self, prefix: Seq<K>) -> Self
{ Map::new(|k: Seq<K>| self.contains_key(prefix + k), |k: Seq<K>| self[prefix + k]) }
Returns a sub-map of all entries whose key begins with prefix
,
re-indexed so that the stored keys have that prefix removed.
§Example
proof fn example() {
let m = map![seq![1, 2] => 10, seq![1, 2, 3] => 20, seq![2] => 30];
let sub = m.prefixed_entries(seq![1, 2]);
assert(sub.contains_key(seq![])); // original key [1,2]
assert(sub[seq![]] == 10);
assert(sub.contains_key(seq![3])); // original key [1,2,3]
assert(sub[seq![3]] == 20);
assert(!sub.contains_key(seq![2])); // original key [2] was not prefixed
}
Sourcepub broadcast proof fn lemma_prefixed_entries_get(self, prefix: Seq<K>, k: Seq<K>)
pub broadcast proof fn lemma_prefixed_entries_get(self, prefix: Seq<K>, k: Seq<K>)
self.prefixed_entries(prefix).contains_key(k),
ensuresself.prefixed_entries(prefix)[k] == #[trigger] self[prefix + k],
For every key k
kept by prefixed_entries(prefix)
,
the associated value is the one stored at prefix + k
in the original map.
§Example
proof fn example() {
let m = map![seq![1, 2] => 10, seq![1, 2, 3] => 20];
let p = seq![1, 2];
// key inside the sub-map
assert(m.prefixed_entries(p)[seq![]] == m[p + seq![]]); // 10
assert(m.prefixed_entries(p)[seq![3]] == m[p + seq![3]]); // 20
}
Sourcepub broadcast proof fn lemma_prefixed_entries_contains(self, prefix: Seq<K>, k: Seq<K>)
pub broadcast proof fn lemma_prefixed_entries_contains(self, prefix: Seq<K>, k: Seq<K>)
#[trigger] self.prefixed_entries(prefix).contains_key(k)
<==> self.contains_key(prefix + k),
A key k
is in prefixed_entries(prefix)
exactly when the original map
contains the key prefix + k
.
§Example
proof fn example() {
let m = map![seq![1, 2] => 10, seq![1, 2, 3] => 20];
let p = seq![1, 2];
assert(m.prefixed_entries(p).contains_key(seq![])
<==> m.contains_key(p + seq![]));
assert(m.prefixed_entries(p).contains_key(seq![3])
<==> m.contains_key(p + seq![3]));
assert(!m.prefixed_entries(p).contains_key(seq![2]));
}
Sourcepub broadcast proof fn lemma_prefixed_entries_insert(self, prefix: Seq<K>, k: Seq<K>, v: V)
pub broadcast proof fn lemma_prefixed_entries_insert(self, prefix: Seq<K>, k: Seq<K>, v: V)
#[trigger] self.insert(prefix + k, v).prefixed_entries(prefix)
== self.prefixed_entries(prefix).insert(k, v),
Inserting (prefix + k, v)
before taking prefixed_entries(prefix)
has the same effect as inserting (k, v)
into the prefixed map.
§Example
proof fn example() {
let m = map![seq![1, 2] => 10];
let p = seq![1, 2];
let left = m.insert(p + seq![3], 20).prefixed_entries(p);
let right = m.prefixed_entries(p).insert(seq![3], 20);
assert(left == right);
}
Sourcepub broadcast proof fn lemma_prefixed_entries_union(self, m: Self, prefix: Seq<K>)
pub broadcast proof fn lemma_prefixed_entries_union(self, m: Self, prefix: Seq<K>)
#[trigger] self.union_prefer_right(m).prefixed_entries(prefix)
== self.prefixed_entries(prefix).union_prefer_right(m.prefixed_entries(prefix)),
Taking the entries that share prefix
commutes with union_prefer_right
:
union the two maps first and then strip the prefix, or strip the prefix from
each map and then union them—the resulting maps are identical.
§Example
proof fn example() {
let a = map![seq![1, 2] => 10, seq![2, 3] => 20];
let b = map![seq![1, 2] => 99, seq![2, 4] => 40];
let p = seq![2];
assert(
a.union_prefer_right(b).prefixed_entries(p)
== a.prefixed_entries(p).union_prefer_right(b.prefixed_entries(p))
);
}
Source§impl Map<int, int>
impl Map<int, int>
Sourcepub open spec fn is_monotonic(self) -> bool
pub open spec fn is_monotonic(self) -> bool
{
forall |x: int, y: int| {
self.dom().contains(x) && self.dom().contains(y) && x <= y
==> #[trigger] self[x] <= #[trigger] self[y]
}
}
Returns true
if a map is monotonic – that is, if the mapping between ordered sets
preserves the regular <=
ordering on integers.
Sourcepub open spec fn is_monotonic_from(self, start: int) -> bool
pub open spec fn is_monotonic_from(self, start: int) -> bool
{
forall |x: int, y: int| {
self.dom().contains(x) && self.dom().contains(y) && start <= x <= y
==> #[trigger] self[x] <= #[trigger] self[y]
}
}
Returns true
if and only if a map is monotonic, only considering keys greater than
or equal to start