Struct FMap

pub struct FMap<K, V: ?Sized>(/* private fields */);

A finite map type usable in pearlite and ghost! blocks.

If you need an infinite map, see Mapping.

Ghost

Since std::collections::HashMap and std::collections::BTreeMap have finite capacity, this could cause some issues in ghost code:

ghost! {
    let mut map = HashMap::new();
    for _ in 0..=usize::MAX as u128 + 1 {
        map.insert(0, 0); // cannot fail, since we are in a ghost block
    }
    proof_assert!(map.len() <= usize::MAX@); // by definition
    proof_assert!(map.len() > usize::MAX@); // uh-oh
}

This type is designed for this use-case, with no restriction on the capacity.

Implementations

impl<K, V: ?Sized> FMap<K, V>

Logical definitions

pub fn empty() -> Self

Returns the empty map.

logic

ensures

result.len() == 0

ensures

result.view() == Mapping::cst(None)

pub fn len(self) -> Int

The number of elements in the map, also called its length.

logic

ensures

result >= 0

pub fn view(self) -> Mapping<K, Option<SizedW<V>>>

View of the map

This represents the actual content of the map: other methods are specified relative to this.

logic

ensures

forall<m1: Self, m2: Self> m1 != m2 ==> Self::view(m1) != Self::view(m2)

pub fn insert(self, k: K, v: V) -> Self

Returns a new map, where the key-value pair (k, v) have been inserted.

logic

ensures

result.view() == self.view().set(k, Some(v.make_sized()))

ensures

self.contains(k) ==> result.len() == self.len()

ensures

!self.contains(k) ==> result.len() == self.len() + 1

pub fn remove(self, k: K) -> Self

Returns a new map, where the key k is no longer present.

logic

ensures

result.view() == self.view().set(k, None)

ensures

result.len() == if self.contains(k) {self.len() - 1} else {self.len()}

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

where V: Sized,

Get the value associated with key k in the map.

If no value is present, returns None.

logic

match self.get_unsized(k) {
    None => None,
    Some(x) => Some(*x),
}

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

Same as Self::get, but can handle unsized values.

logic

self.view().get(k)

pub fn lookup(self, k: K) -> V

where V: Sized,

Get the value associated with key k in the map.

If no value is present, the returned value is meaningless.

logic

*self.lookup_unsized(k)

pub fn lookup_unsized(self, k: K) -> SizedW<V>

Same as Self::lookup, but can handle unsized values.

logic

unwrap(self.get_unsized(k))

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

Returns true if the map contains a value for the specified key.

logic

self.get_unsized(k) != None

pub fn is_empty(self) -> bool

Returns true if the map contains no elements.

logic

self.ext_eq(FMap::empty())

pub fn disjoint(self, other: Self) -> bool

Returns true if the two maps have no key in common.

logic

pearlite! {forall<k: K> !self.contains(k) || !other.contains(k)}

pub fn subset(self, other: Self) -> bool

Returns true if all key-value pairs in self are also in other.

logic

pearlite! {
    forall<k: K> self.contains(k) ==> other.get_unsized(k) == self.get_unsized(k)
}

pub fn union(self, other: Self) -> Self

Returns a new map, which is the union of self and other.

If self and other are not disjoint, the result is unspecified.

logic

requires

self.disjoint(other)

ensures

forall<k: K> result.get_unsized(k) == if self.contains(k) {
        self.get_unsized(k)
    } else if other.contains(k) {
        other.get_unsized(k)
    } else {
        None
    }

ensures

result.len() == self.len() + other.len()

pub fn subtract_keys(self, other: Self) -> Self

Returns a new map, that contains all the key-value pairs of self such that the key is not in other.

logic

ensures

forall<k: K> result.get_unsized(k) == if other.contains(k) {
        None
    } else {
        self.get_unsized(k)
    }

pub fn subtract(self, other: Self) -> Self

Same as Self::subtract_keys, but the result is meaningless if other is not a subset of self.

In return, this gives more guarantees than Self::subtract_keys.

logic

self.subtract_keys(other)

requires

other.subset(self)

ensures

result.disjoint(other)

ensures

other.union(result).ext_eq(self)

ensures

forall<k: K> result.get_unsized(k) == if other.contains(k) {
        None
    } else {
        self.get_unsized(k)
    }

pub fn ext_eq(self, other: Self) -> bool

Extensional equality.

Returns true if self and other contain exactly the same key-value pairs.

This is in fact equivalent with normal equality.

logic

self.view() == other.view()

ensures

result ==> self == other

ensures

(forall<k: K> self.get_unsized(k) == other.get_unsized(k)) ==> result

impl<K, V: ?Sized> FMap<K, V>

Ghost definitions

pub fn new() -> Ghost<Self>

Create a new, empty map on the ghost heap.

pure

ensures

result.is_empty()

pub fn len_ghost(&self) -> Int

Returns the number of elements in the map.

If you need to get the length in pearlite, consider using len.

Example

use creusot_contracts::{logic::FMap, *};

let mut map = FMap::new();
ghost! {
    let len1 = map.len_ghost();
    map.insert_ghost(1, 21);
    map.insert_ghost(1, 42);
    map.insert_ghost(2, 50);
    let len2 = map.len_ghost();
    proof_assert!(len1 == 0);
    proof_assert!(len2 == 2);
};

pure

ensures

result == self.len()

pub fn contains_ghost(&self, key: &K) -> bool

Returns true if the map contains a value for the specified key.

Example

use creusot_contracts::{logic::FMap, *};

let mut map = FMap::new();
ghost! {
    map.insert_ghost(1, 42);
    let (b1, b2) = (map.contains_ghost(&1), map.contains_ghost(&2));
    proof_assert!(b1);
    proof_assert!(!b2);
};

pure

ensures

result == self.contains(*key)

pub fn get_ghost(&self, key: &K) -> Option<&V>

Returns a reference to the value corresponding to the key.

Example

use creusot_contracts::{logic::FMap, *};

let mut map = FMap::new();
ghost! {
    map.insert_ghost(1, 2);
    let x1 = map.get_ghost(&1);
    let x2 = map.get_ghost(&2);
    proof_assert!(x1 == Some(&2));
    proof_assert!(x2 == None);
};

pure

ensures

if self.contains(*key) {
            match result {
                None => false,
                Some(r) => *self.lookup_unsized(*key) == *r,
            }
        } else {
            result == None
        }

pub fn get_mut_ghost(&mut self, key: &K) -> Option<&mut V>

Returns a mutable reference to the value corresponding to the key.

Example

use creusot_contracts::{logic::FMap, *};

let mut map = FMap::new();
ghost! {
    map.insert_ghost(1, 21);
    if let Some(x) = map.get_mut_ghost(&1) {
        *x = 42;
    }
    proof_assert!(map.lookup(1i32) == 42i32);
};

pure

ensures

if self.contains(*key) {
            match result {
                None => false,
                Some(r) => (^self).contains(*key) &&
                           *(*self).lookup_unsized(*key) == *r &&
                           *(^self).lookup_unsized(*key) == ^r,
            }
        } else {
            result == None && *self == ^self
        }

ensures

forall<k: K> k != *key ==> (*self).get_unsized(k) == (^self).get_unsized(k)

ensures

(*self).len() == (^self).len()

pub fn split_mut_ghost(&mut self, key: &K) -> (Option<&mut V>, &mut Self)

Returns a mutable reference to the value corresponding to a key, while still allowing modification on the other keys.

Example

use creusot_contracts::{logic::FMap, *};

let mut map = FMap::new();
ghost! {
    map.insert_ghost(1, 21);
    map.insert_ghost(2, 42);
    if let (Some(x), map2) = map.split_mut_ghost(&1) {
        *x = 22;
        map2.insert_ghost(3, 30);
        map2.insert_ghost(1, 56); // This modification will be ignored on `map`
    }
    proof_assert!(map.lookup(1i32) == 22i32);
    proof_assert!(map.lookup(2i32) == 42i32);
    proof_assert!(map.lookup(3i32) == 30i32);
};

pure

ensures

if self.contains(*key) {
        *result.1 == (*self).remove(*key) &&
        match result.0 {
            None => false,
            Some(r) => *(*self).lookup_unsized(*key) == *r && ^self == (^result.1).insert(*key, ^r),
        }
    } else {
        result.0 == None && result.1 == self
    }

pub fn insert_ghost(&mut self, key: K, value: V) -> Option<V>

where V: Sized,

Inserts a key-value pair into the map.

If the map did not have this key present, None is returned.

Example

use creusot_contracts::{logic::FMap, *};

let mut map = FMap::new();
ghost! {
    let res1 = map.insert_ghost(37, 41);
    proof_assert!(res1 == None);
    proof_assert!(map.is_empty() == false);

    let res2 = map.insert_ghost(37, 42);
    proof_assert!(res2 == Some(41));
    proof_assert!(map.lookup(37i32) == 42i32);
};

pure

ensures

^self == (*self).insert(key, value)

ensures

result == (*self).get(key)

pub fn insert_ghost_unsized(&mut self, key: K, value: Box<V>) -> Option<Box<V>>

Same as Self::insert_ghost, but for unsized values.

pure

ensures

^self == (*self).insert(key, *value)

ensures

result == (*self).get_unsized(key)

pub fn remove_ghost(&mut self, key: &K) -> Option<V>

where V: Sized,

Removes a key from the map, returning the value at the key if the key was previously in the map.

Example

use creusot_contracts::{logic::FMap, *};

let mut map = FMap::new();
let res = ghost! {
    map.insert_ghost(1, 42);
    let res1 = map.remove_ghost(&1);
    let res2 = map.remove_ghost(&1);
    proof_assert!(res1 == Some(42i32));
    proof_assert!(res2 == None);
};

pure

ensures

^self == (*self).remove(*key)

ensures

result == (*self).get(*key)

pub fn remove_ghost_unsized(&mut self, key: &K) -> Option<Box<V>>

Same as Self::remove_ghost, but for unsized values.

pure

ensures

^self == (*self).remove(*key)

ensures

result == (*self).get_unsized(*key)

Trait Implementations

impl<K: Clone + Copy, V: Clone + Copy> Clone for FMap<K, V>

fn clone(&self) -> Self

pure

ensures

result == *self

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl<K, V> IndexLogic<K> for FMap<K, V>

fn index_logic(self, key: K) -> Self::Item

logic

self.lookup(key)

type Item = V

impl<K, V: ?Sized> Invariant for FMap<K, V>

fn invariant(self) -> bool

logic(prophetic)

pearlite! { forall<k: K> self.contains(k) ==> inv(k) && inv(self.lookup_unsized(k)) }

impl<K: Clone + Copy, V: Clone + Copy> Copy for FMap<K, V>