Struct FMap 

pub struct FMap<K, V>(/* 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> FMap<K, V>

Logical definitions

pub fn empty() -> Self

Returns the empty map.

(opaque)

ensures

result.len() == 0

ensures

result@ == Mapping::cst(None)

pub fn len(self) -> Int

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

(opaque)

ensures

result >= 0

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

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

(opaque)

ensures

result@ == self@.set(k, Some(v))

ensures

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

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

Returns the map where containing the only key-value pair (k, v).

(open)

Self::empty().insert(k, v)

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

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

(opaque)

ensures

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

ensures

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

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

Get the value associated with key k in the map.

If no value is present, returns None.

(open, inline)

self.view().get(k)

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

Get the value associated with key k in the map.

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

(open, inline)

self.get(k).unwrap_logic()

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

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

(open, inline)

self.get(k) != None

pub fn is_empty(self) -> bool

Returns true if the map contains no elements.

(open)

self.ext_eq(FMap::empty())

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

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

(open)

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.

(open)

pearlite! {
    forall<k: K> self.contains(k) ==> other.get(k) == self.get(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.

(opaque)

requires

self.disjoint(other)

ensures

forall<k: K> #[trigger(result.get(k))] !self.contains(k) ==> result.get(k) == other.get(k)

ensures

forall<k: K> #[trigger(result.get(k))] !other.contains(k) ==> result.get(k) == self.get(k)

ensures

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

pub fn subtract(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.

(opaque)

ensures

result.disjoint(other)

ensures

other.subset(self) ==> other.union(result) == self

ensures

forall<k: K> #[trigger(result.get(k))] result.get(k) ==
        if other.contains(k) {
            None
        } else {
            self.get(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.

(open)

pearlite! {
    let _ = Self::view_inj;
    forall<k: K> self.get(k) == other.get(k)
}

ensures

result == (self == other)

pub fn merge(self, m: FMap<K, V>, f: Mapping<(V, V), V>) -> FMap<K, V>

Merge the two maps together

If both map contain the same key, the entry for the result is determined by f.

(opaque)

ensures

forall<k: K> #[trigger(result.get(k))]
            match (self.get(k), m.get(k)) {
                (None, y) => result.get(k) == y,
                (x, None) => result.get(k) == x,
                (Some(x), Some(y)) => result.get(k) == Some(f[(x, y)]),
            }

pub fn map<V2>(self, f: Mapping<(K, V), V2>) -> FMap<K, V2>

Map every value in self according to f. Keys are unchanged.

ensures

forall<k: K> #[trigger(result.get(k))] result.get(k) == match self.get(k) {
        None => None,
        Some(v) => Some(f[(k, v)]),
    }

ensures

result.len() == self.len()

pub fn filter(self, p: Mapping<(K, V), bool>) -> Self

Filter key-values in self according to p.

A key-value pair will be in the result map if and only if it is in self and p returns true on this pair.

ensures

forall<k: K> #[trigger(result.get(k))] result.get(k) == match self.get(k) {
        None => None,
        Some(v) => if p[(k, v)] { Some(v) } else { None },
    }

pub fn filter_map<V2>(self, f: Mapping<(K, V), Option<V2>>) -> FMap<K, V2>

Map every value in self according to f. Keys are unchanged. If f returns false, remove the key-value from the map.

(opaque)

ensures

forall<k: K> #[trigger(result.get(k))] result.get(k) == match self.get(k) {
        None => None,
        Some(v) => f[(k, v)],
    }

pub fn keys(self) -> FSet<K>

Returns the set of keys in the map.

(opaque)

ensures

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

ensures

result.len() == self.len()

impl<K, V> FMap<K, V>

Ghost definitions

pub fn new() -> Ghost<Self>

Create a new, empty map on the ghost heap.

terminates

ghost

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, prelude::*};

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

terminates

ghost

ensures

result == self.len()

pub fn is_empty_ghost(&self) -> bool

terminates

ghost

ensures

result == (self.len() == 0 && forall<k> !self.contains(k))

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, prelude::*};

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

terminates

ghost

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, prelude::*};

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

terminates

ghost

ensures

result == self.get(*key).map_logic(|v|&v)

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, prelude::*};

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[1i32] == 42i32);
};

terminates

ghost

ensures

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

ensures

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

ensures

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

pub fn split_mut_ghost(&mut self, key: &K) -> (&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, prelude::*};

let mut map = FMap::new();
ghost! {
    map.insert_ghost(1, 21);
    map.insert_ghost(2, 42);
    let (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[1i32] == 22i32);
    proof_assert!(map[2i32] == 42i32);
    proof_assert!(map[3i32] == 30i32);
};

terminates

ghost

requires

self.contains(*key)

ensures

*result.1 == (*self).remove(*key)

ensures

self[*key] == *result.0 && ^self == (^result.1).insert(*key, ^result.0)

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

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, prelude::*};

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[37i32] == 42i32);
};

terminates

ghost

ensures

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

ensures

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

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

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, prelude::*};

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

terminates

ghost

ensures

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

ensures

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

pub fn clear_ghost(&mut self)

Clears the map, removing all values.

Example

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

let mut s = FMap::new();
ghost! {
    s.insert_ghost(1, 2);
    s.insert_ghost(2, 3);
    s.insert_ghost(3, 42);
    s.clear_ghost();
    proof_assert!(s == FMap::empty());
};

terminates

ghost

ensures

^self == Self::empty()

pub fn remove_one_ghost(&mut self) -> Option<(K, V)>

terminates

ghost

ensures

match result {
        None => *self == ^self && self.is_empty(),
        Some((k, v)) => *self == (^self).insert(k, v) && !(^self).contains(k),
    }

pub fn to_seq(self) -> Seq<(K, V)>

terminates

ghost

ensures

result.len() == self.len()

ensures

forall<k, v> (self.get(k) == Some(v)) == (exists<i> result.get(i) == Some((k, v)))

pub fn as_ref_ghost(&self) -> FMap<&K, &V>

terminates

ghost

ensures

result.len() == self.len()

ensures

forall<k, v> (self.get(k) == Some(v)) == (result.get(&k) == Some(&v))

pub fn as_mut_ghost(&mut self) -> FMap<&K, &mut V>

terminates

ghost

ensures

result.len() == self.len()

ensures

forall<k> match result.get(&k) {
        None => !(*self).contains(k) && !(^self).contains(k),
        Some(v) => (*self).get(k) == Some(*v) && (^self).get(k) == Some(^v),
    }

impl<K, V: RA> FMap<K, V>

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

requires

forall<k: K> self.get(k).op(other.get(k)) != None

ensures

forall<k: K> Some(result.get(k)) == self.get(k).op(other.get(k))

Trait Implementations

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

fn clone(&self) -> Self

terminates

ghost

ensures

result == *self

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

Performs copy-assignment from source.

impl<'a, K, V> Index<&'a K> for FMap<K, V>

fn index(&self, key: &'a K) -> &Self::Output

terminates

ghost

requires

self.contains(*key)

ensures

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

type Output = V

The returned type after indexing.

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

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

(open, inline)

self.lookup(key)

type Item = V

impl<'a, K, V> IntoIterator for &'a FMap<K, V>

fn into_iter(self) -> FMapIterRef<'a, K, V>

terminates

ghost

ensures

result@ == *self

type Item = (&'a K, &'a V)

The type of the elements being iterated over.

type IntoIter = FMapIterRef<'a, K, V>

Which kind of iterator are we turning this into?

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

fn into_iter(self) -> Self::IntoIter

terminates

ghost

ensures

result@ == self

type Item = (K, V)

The type of the elements being iterated over.

type IntoIter = FMapIter<K, V>

Which kind of iterator are we turning this into?

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

fn invariant(self) -> bool

(open, prophetic, inline)

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

impl<K, V: RA> LocalUpdate<FMap<K, V>> for FMapInsertLocalUpdate<K, V>

fn premise(self, from_auth: FMap<K, V>, _: FMap<K, V>) -> bool

(open)

from_auth.get(*self.0) == None

fn update( self, from_auth: FMap<K, V>, from_frag: FMap<K, V>, ) -> (FMap<K, V>, FMap<K, V>)

(open)

(from_auth.insert(*self.0, *self.1), from_frag.insert(*self.0, *self.1))

fn frame_preserving( self, from_auth: FMap<K, V>, from_frag: FMap<K, V>, frame: Option<FMap<K, V>>, )

requires

self.premise(from_auth, from_frag)

requires

Some(from_frag).op(frame) == Some(Some(from_auth))

ensures

let (to_auth, to_frag) = self.update(from_auth, from_frag);
Some(to_frag).op(frame) == Some(Some(to_auth))

impl<K, V: RA> RA for FMap<K, V>

fn op(self, other: Self) -> Option<Self>

(open)

pearlite! {
    if (forall<k: K> self.get(k).op(other.get(k)) != None) {
        Some(self.total_op(other))
    } else {
        None
    }
}

fn factor(self, factor: Self) -> Option<Self>

(open)

pearlite! {
    if (forall<k: K> factor.get(k).incl(self.get(k))) {
        let res = self.filter_map(|(k, vo): (K, V)|
            match Some(vo).factor(factor.get(k)) {
                Some(r) => r,
                None => None,
        });
        proof_assert!(
            match factor.op(res) {
                None => false,
                Some(o) => o.ext_eq(self)
            }
        );
        Some(res)
    } else {
        None
    }
}

ensures

match result {
        Some(c) => factor.op(c) == Some(self),
        None => forall<c: Self> factor.op(c) != Some(self),
    }

fn commutative(a: Self, b: Self)

(law)

ensures

a.op(b) == b.op(a)

fn associative(a: Self, b: Self, c: Self)

(law)

ensures

a.op(b).and_then_logic(|ab: Self| ab.op(c)) == b.op(c).and_then_logic(|bc| a.op(bc))

fn core(self) -> Option<Self>

(open)

Some(self.core_total())

ensures

match result {
        Some(c) => c.op(c) == Some(c) && c.op(self) == Some(self),
        None => true
    }

fn core_is_maximal_idemp(self, i: Self)

requires

i.op(i) == Some(i)

requires

i.op(self) == Some(self)

ensures

match self.core() {
        Some(c) => i.incl(c),
        None => false,
    }

fn incl(self, other: Self) -> bool

Inclusion of RA.

fn incl_op(self, other: Self, comb: Self)

(law, sealed)

fn incl_eq(self, other: Self) -> bool

(open, sealed)

fn incl_eq_op(a: Self, b: Self, x: Self) -> bool

(open, sealed)

fn update(self, x: Self) -> bool

Ensures that we can go from self to x without making composition with the frame invalid.

fn update_nondet(self, s: Set<Self>) -> bool

This is used in Resource::update_nondet.

fn incl_transitive(a: Self, b: Self, c: Self)

RA::incl is transitive.

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

fn resolve(self) -> bool

(open, prophetic)

pearlite! { forall<k: K, v: V> self.get(k) == Some(v) ==> resolve(k) && resolve(v) }

fn resolve_coherence(self)

(open(pub(self)), prophetic)

requires

structural_resolve(self)

ensures

self.resolve()

impl<K, V: RA> UnitRA for FMap<K, V>

fn unit() -> Self

(open)

proof_assert!(forall<x: Self> x.op(Self::empty()).unwrap_logic().ext_eq(x));
Self::empty()

ensures

forall<x: Self> #[trigger(x.op(result))] x.op(result) == Some(x)

fn core_total(self) -> Self

(open)

let r = self.filter_map(|(_, v): (K, V)| v.core());
proof_assert!(r.op(r).unwrap_logic().ext_eq(r));
proof_assert!(r.op(self).unwrap_logic().ext_eq(self));
r

ensures

result.op(result) == Some(result)

ensures

result.op(self) == Some(self)

fn core_is_total(self)

ensures

self.core() == Some(self.core_total())

fn incl_refl()

(law, sealed)

fn unit_core()

(law, sealed)

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

fn view(self) -> Self::ViewTy

View of the map

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

(opaque)

type ViewTy = Mapping<K, Option<V>>

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