Struct IMap

pub struct IMap<K, V> { /* private fields */ }

Expand description

IMap<K, V> is an abstract map type for specifications.

An object map: IMap<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, use Map.

IMaps can be constructed in a few different ways:

IMap::empty() constructs an empty map.
IMap::new and IMap::total construct a map given functions that specify its domain and the mapping from keys to values (a map comprehension).
The imap! macro, to construct small maps of a fixed size.
By manipulating an existing map with IMap::insert or IMap::remove.

To prove that two maps are equal, it is usually easiest to use the extensionality operator =~=.

Implementations§

§

impl<K, V> IMap<K, V>

pub fn empty() -> IMap<K, V>

An empty map.

pub fn total(fv: FnSpec<(K,), V>) -> IMap<K, V>

Gives a IMap<K, V> whose domain contains every key, and maps each key to the value given by fv.

pub fn new(fk: FnSpec<(K,), bool>, fv: FnSpec<(K,), V>) -> IMap<K, V>

Gives a IMap<K, V> whose domain is given by the boolean predicate on keys fk, and maps each key to the value given by fv.

pub fn dom(self) -> ISet<K>

The domain of the map as a set.

pub fn index(self, key: K) -> V

Gets the value that the given key key maps to. For keys not in the domain, the result is meaningless and arbitrary.

pub fn spec_index(self, key: K) -> V

[] operator, synonymous with index

pub fn insert(self, key: K, value: V) -> IMap<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.

pub fn remove(self, key: K) -> IMap<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.

pub fn len(self) -> nat

Returns the number of key-value pairs in the map

pub fn tracked_empty() -> IMap<K, V>

Create an empty tracked map.

This allows us to create a map, which we know is empty, that is tracked.

pub fn tracked_insert(&mut self, key: K, value: V)

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 fn tracked_remove(&mut self, key: K) -> V

Removes the given key and its associated tracked value from the map.

The key must exist in the map

pub fn tracked_borrow(&self, key: K) -> &V

Index into a tracked map, getting a tracked borrow of the value

pub fn tracked_borrow_mut(&mut self, key: K) -> &mut V

Index into a tracked map, getting a tracked mutable borrow of the value

pub fn tracked_borrow_mut_split( &mut self, keys: ISet<K>, ) -> (&mut IMap<K, V>, &mut IMap<K, V>)

Split a mutable borrow of a map into two.

pub fn tracked_map_keys<J>( old_map: IMap<K, V>, key_map: IMap<J, K>, ) -> IMap<J, V>

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 fn tracked_remove_keys(&mut self, keys: ISet<K>) -> IMap<K, V>

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 fn tracked_union_prefer_right(&mut self, right: IMap<K, V>)

Consume a tracked map and merge its entries into this tracked map.

The new (key, value) pairs take precedence.

§

impl<K, V> IMap<K, V>

pub fn tracked_map_keys_in_place(&mut self, key_map: IMap<K, K>)

§

impl<K, V> IMap<K, V>

pub fn is_full(self) -> bool

Is true if called by a “full” map, i.e., a map containing every element of type A.

pub fn is_empty(self) -> bool

Is true if called by an “empty” map, i.e., a map containing no elements and has length 0

pub fn contains_key(self, k: K) -> bool

Returns true if the key k is in the domain of self.

pub fn contains_value(self, v: V) -> bool

Returns true if the value v is in the range of self.

pub fn index_opt(self, k: K) -> Option<V>

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.

pub fn values(self) -> ISet<V>

Returns the set of values in the map.

§Example

let m: IMap<int, int> = imap![1 => 10, 2 => 11];
assert(m.values() == iset![10int, 11int]) by {
    assert(m.contains_key(1));
    assert(m.contains_key(2));
    assert(m.values() =~= iset![10int, 11int]);
}

pub fn kv_pairs(self) -> ISet<(K, V)>

Returns the set of key-value pairs representing the map

§Example

let m: IMap<int, int> = imap![1 => 10, 2 => 11];
assert(m.kv_pairs() == iset![(1int, 10int), (2int, 11int)] by {
    assert(m.contains_pair(1int, 10int));
    assert(m.contains_pair(2int, 11int));
    assert(m.kv_pairs() =~= iset![(1int, 10int), (2int, 11int)]);
}

pub fn contains_pair(self, k: K, v: V) -> bool

Returns true if the key k is in the domain of self, and it maps to the value v.

pub fn submap_of(self, m2: IMap<K, V>) -> bool

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(
   imap![1 => 10, 2 => 11].le(imap![1 => 10, 2 => 11, 3 => 12])
);

pub fn spec_le(self, m2: IMap<K, V>) -> bool

pub fn union_prefer_right(self, m2: IMap<K, V>) -> IMap<K, V>

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]);

pub fn remove_keys(self, keys: ISet<K>) -> IMap<K, V>

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(
   imap![1 => 10, 2 => 11, 3 => 12].remove_keys(iset!{2, 3, 4})
   =~= imap![1 => 10]);

pub fn restrict(self, keys: ISet<K>) -> IMap<K, V>

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]);

pub fn is_equal_on_key(self, m2: IMap<K, V>, key: K) -> bool

Returns true if and only if the given key maps to the same value or does not exist in self and m2.

pub fn agrees(self, m2: IMap<K, V>) -> bool

Returns true if the two given maps agree on all keys that their domains share

pub fn map_entries<W>(self, f: FnSpec<(K, V), W>) -> IMap<K, W>

Map a function f over all (k, v) pairs in self.

pub fn map_values<W>(self, f: FnSpec<(V,), W>) -> IMap<K, W>

Map a function f over the values in self.

pub fn is_injective(self) -> bool

Returns true if and only if a map is injective

pub fn invert(self) -> IMap<V, K>

Swaps map keys and values. Values are not required to be unique; no promises on which key is chosen on the intersection.

pub fn lemma_remove_key_len(self, key: K)

Removing a key from a map that previously contained that key decreases the map’s length by one

pub fn lemma_remove_equivalency(self, key: K)

The domain of a map after removing a key is equivalent to removing the key from the domain of the original map.

pub fn lemma_remove_keys_len(self, keys: ISet<K>)

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.

pub fn lemma_invert_is_injective(self)

The function invert results in an injective map

pub fn filter_keys(self, p: FnSpec<(K,), bool>) -> IMap<K, V>

Keeps only those key-value pairs whose key satisfies p.

§Example

proof fn example() {
    let m = imap![1 => 10, 2 => 20];
    let even = |k: int| k % 2 == 0;
    assert(m.filter_keys(even) =~= imap![2 => 20]);
}

pub fn get(self, k: K) -> Option<V>

Returns the value associated with key k in the map if it exists, otherwise returns None.

§Example

proof fn get_test() {
    let m: IMap<int, bool> = imap![
        1 => true,
        2 => false
    ];

    assert(m.get(1) == Some(true));
    assert(m.get(3) == None);
}

pub fn get_dom_value_any(self, p: FnSpec<(V,), bool>)

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 = imap![1 => 10, 2 => 20, 3 => 30];
    let p = |v: int| v > 25;
    assert(m[3] == 30);
    assert(m.dom().any(|k| p(m[k])));
}

pub fn lemma_submap_eq_iff(self, m: IMap<K, V>)

Two maps are equal if and only if they are submaps of each other.

§Example

proof fn submap_eq_test() {
    let m1 = imap![1 => 10, 2 => 20];
    let m2 = imap![1 => 10, 2 => 20];
    let m3 = imap![1 => 10, 2 => 30];

    assert(m1.submap_of(m2) && m2.submap_of(m1));
    assert(m1 == m2);
}

pub fn lemma_imap_remove_keys_insert(self, r: ISet<K>, k: K, v: 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 = imap![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));
}

pub fn lemma_filter_keys_insert(self, p: FnSpec<(K,), bool>, k: K, v: V)

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 = imap![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));
}

pub fn lemma_insert_contains_value(self, k: K, v: V)

Inserting a value in a map means it contains the value that was inserted.

§Example

proof fn example() {
    let a = imap![1int => 2int];
    assert(a.contains_value(2));
}

pub fn lemma_insert_invariant_contains(self, old_v: V, k: K, v: V)

Inserting a value in a map where that key is already present ensures The contains value sees (only) the updated value;

§Example

proof fn example() {
    let a = imap![1int => 2int].insert(1int, 3int);
    assert(!a.contains_value(2));
    assert(a.contains_value(3));
}

pub fn lemma_injective_values_len(self)

pub fn lemma_values_len(self)

§

impl<K, V> IMap<Seq<K>, V>

pub fn prefixed_entries(self, prefix: Seq<K>) -> IMap<Seq<K>, V>

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 = imap![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
}

pub fn lemma_prefixed_entries_get(self, prefix: Seq<K>, k: Seq<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 = imap![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
}

pub fn lemma_prefixed_entries_contains(self, prefix: Seq<K>, k: Seq<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 = imap![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]));
}

pub fn lemma_prefixed_entries_insert(self, prefix: Seq<K>, k: Seq<K>, v: 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 = imap![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);
}

pub fn lemma_prefixed_entries_union(self, m: IMap<Seq<K>, V>, prefix: Seq<K>)

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 = imap![seq![1, 2] => 10, seq![2, 3] => 20];
    let b = imap![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))
    );
}