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 to_mapping(self) -> Mapping<K, Option<V>>

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

logic(opaque)

pub fn empty() -> Self

Returns the empty map.

logic(opaque)

ensures

result.len() == 0

ensures

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

pub fn len(self) -> Int

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

logic(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.

logic(opaque)

ensures

result.to_mapping() == self.to_mapping().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).

logic(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.

logic(opaque)

ensures

result.to_mapping() == self.to_mapping().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.

logic(open, inline)

self.to_mapping().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.

logic(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.

logic(open, inline)

self.get(k) != None

pub fn is_empty(self) -> bool

Returns true if the map contains no elements.

logic(open)

self.ext_eq(FMap::empty())

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

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

logic(open)

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(open)

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.

logic(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.

logic(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.

logic(open)

let _ = Self::to_mapping_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.

logic(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.

logic

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.

logic

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.

logic(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.

logic(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_std::{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_std::{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_std::{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_std::{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_std::{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_std::{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_std::{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_std::{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

logic

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

logic(open, inline)

self.lookup(key)

type Item = V

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

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

terminates

ghost

ensures

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

ensures

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

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

The type of the elements being iterated over.

type IntoIter = FMap<&'a K, &'a V>

Which kind of iterator are we turning this into?

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

fn invariant(self) -> bool

logic(open, prophetic, inline)

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

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

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

terminates

ghost

ensures

match result {
    None => self.completed(),
    Some((k, v)) => (*self).produces(Seq::singleton((k, v)), ^self) && (*self) == (^self).insert(k, v),
}

type Item = (K, V)

The type of the elements being iterated over.

fn next_chunk<const N: usize>( &mut self, ) -> Result<[Self::Item; N], IntoIter<Self::Item, N>>

where Self: Sized,

🔬This is a nightly-only experimental API. (iter_next_chunk)

Advances the iterator and returns an array containing the next N values.

fn size_hint(&self) -> (usize, Option<usize>)

Returns the bounds on the remaining length of the iterator.

fn count(self) -> usize

where Self: Sized,

Consumes the iterator, counting the number of iterations and returning it.

fn last(self) -> Option<Self::Item>

where Self: Sized,

Consumes the iterator, returning the last element.

fn advance_by(&mut self, n: usize) -> Result<(), NonZero<usize>>

🔬This is a nightly-only experimental API. (iter_advance_by)

Advances the iterator by n elements.

fn nth(&mut self, n: usize) -> Option<Self::Item>

Returns the nth element of the iterator.

fn step_by(self, step: usize) -> StepBy<Self>

where Self: Sized,

Creates an iterator starting at the same point, but stepping by the given amount at each iteration.

fn chain<U>(self, other: U) -> Chain<Self, <U as IntoIterator>::IntoIter>

where Self: Sized, U: IntoIterator<Item = Self::Item>,

Takes two iterators and creates a new iterator over both in sequence.

fn zip<U>(self, other: U) -> Zip<Self, <U as IntoIterator>::IntoIter>

where Self: Sized, U: IntoIterator,

‘Zips up’ two iterators into a single iterator of pairs.

fn intersperse(self, separator: Self::Item) -> Intersperse<Self>

where Self: Sized, Self::Item: Clone,

🔬This is a nightly-only experimental API. (iter_intersperse)

Creates a new iterator which places a copy of separator between adjacent items of the original iterator.

fn intersperse_with<G>(self, separator: G) -> IntersperseWith<Self, G>

where Self: Sized, G: FnMut() -> Self::Item,

🔬This is a nightly-only experimental API. (iter_intersperse)

Creates a new iterator which places an item generated by separator between adjacent items of the original iterator.

fn map<B, F>(self, f: F) -> Map<Self, F>

where Self: Sized, F: FnMut(Self::Item) -> B,

Takes a closure and creates an iterator which calls that closure on each element.

fn for_each<F>(self, f: F)

where Self: Sized, F: FnMut(Self::Item),

Calls a closure on each element of an iterator.

fn filter<P>(self, predicate: P) -> Filter<Self, P>

where Self: Sized, P: FnMut(&Self::Item) -> bool,

Creates an iterator which uses a closure to determine if an element should be yielded.

fn filter_map<B, F>(self, f: F) -> FilterMap<Self, F>

where Self: Sized, F: FnMut(Self::Item) -> Option<B>,

Creates an iterator that both filters and maps.

fn enumerate(self) -> Enumerate<Self>

where Self: Sized,

Creates an iterator which gives the current iteration count as well as the next value.

fn peekable(self) -> Peekable<Self>

where Self: Sized,

Creates an iterator which can use the peek and peek_mut methods to look at the next element of the iterator without consuming it. See their documentation for more information.

fn skip_while<P>(self, predicate: P) -> SkipWhile<Self, P>

where Self: Sized, P: FnMut(&Self::Item) -> bool,

Creates an iterator that skips elements based on a predicate.

fn take_while<P>(self, predicate: P) -> TakeWhile<Self, P>

where Self: Sized, P: FnMut(&Self::Item) -> bool,

Creates an iterator that yields elements based on a predicate.

fn map_while<B, P>(self, predicate: P) -> MapWhile<Self, P>

where Self: Sized, P: FnMut(Self::Item) -> Option<B>,

Creates an iterator that both yields elements based on a predicate and maps.

fn skip(self, n: usize) -> Skip<Self>

where Self: Sized,

Creates an iterator that skips the first n elements.

fn take(self, n: usize) -> Take<Self>

where Self: Sized,

Creates an iterator that yields the first n elements, or fewer if the underlying iterator ends sooner.

fn scan<St, B, F>(self, initial_state: St, f: F) -> Scan<Self, St, F>

where Self: Sized, F: FnMut(&mut St, Self::Item) -> Option<B>,

An iterator adapter which, like fold, holds internal state, but unlike fold, produces a new iterator.

fn flat_map<U, F>(self, f: F) -> FlatMap<Self, U, F>

where Self: Sized, U: IntoIterator, F: FnMut(Self::Item) -> U,

Creates an iterator that works like map, but flattens nested structure.

fn flatten(self) -> Flatten<Self>

where Self: Sized, Self::Item: IntoIterator,

Creates an iterator that flattens nested structure.

fn map_windows<F, R, const N: usize>(self, f: F) -> MapWindows<Self, F, N>

where Self: Sized, F: FnMut(&[Self::Item; N]) -> R,

🔬This is a nightly-only experimental API. (iter_map_windows)

Calls the given function f for each contiguous window of size N over self and returns an iterator over the outputs of f. Like slice::windows(), the windows during mapping overlap as well.

fn fuse(self) -> Fuse<Self>

where Self: Sized,

Creates an iterator which ends after the first None.

fn inspect<F>(self, f: F) -> Inspect<Self, F>

where Self: Sized, F: FnMut(&Self::Item),

Does something with each element of an iterator, passing the value on.

fn by_ref(&mut self) -> &mut Self

where Self: Sized,

Creates a “by reference” adapter for this instance of Iterator.

fn collect<B>(self) -> B

where B: FromIterator<Self::Item>, Self: Sized,

Transforms an iterator into a collection.

fn try_collect<B>( &mut self, ) -> <<Self::Item as Try>::Residual as Residual<B>>::TryType

where Self: Sized, Self::Item: Try, <Self::Item as Try>::Residual: Residual<B>, B: FromIterator<<Self::Item as Try>::Output>,

🔬This is a nightly-only experimental API. (iterator_try_collect)

Fallibly transforms an iterator into a collection, short circuiting if a failure is encountered.

fn collect_into<E>(self, collection: &mut E) -> &mut E

where E: Extend<Self::Item>, Self: Sized,

🔬This is a nightly-only experimental API. (iter_collect_into)

Collects all the items from an iterator into a collection.

fn partition<B, F>(self, f: F) -> (B, B)

where Self: Sized, B: Default + Extend<Self::Item>, F: FnMut(&Self::Item) -> bool,

Consumes an iterator, creating two collections from it.

fn is_partitioned<P>(self, predicate: P) -> bool

where Self: Sized, P: FnMut(Self::Item) -> bool,

🔬This is a nightly-only experimental API. (iter_is_partitioned)

Checks if the elements of this iterator are partitioned according to the given predicate, such that all those that return true precede all those that return false.

fn try_fold<B, F, R>(&mut self, init: B, f: F) -> R

where Self: Sized, F: FnMut(B, Self::Item) -> R, R: Try<Output = B>,

An iterator method that applies a function as long as it returns successfully, producing a single, final value.

fn try_for_each<F, R>(&mut self, f: F) -> R

where Self: Sized, F: FnMut(Self::Item) -> R, R: Try<Output = ()>,

An iterator method that applies a fallible function to each item in the iterator, stopping at the first error and returning that error.

fn fold<B, F>(self, init: B, f: F) -> B

where Self: Sized, F: FnMut(B, Self::Item) -> B,

Folds every element into an accumulator by applying an operation, returning the final result.

fn reduce<F>(self, f: F) -> Option<Self::Item>

where Self: Sized, F: FnMut(Self::Item, Self::Item) -> Self::Item,

Reduces the elements to a single one, by repeatedly applying a reducing operation.

fn try_reduce<R>( &mut self, f: impl FnMut(Self::Item, Self::Item) -> R, ) -> <<R as Try>::Residual as Residual<Option<<R as Try>::Output>>>::TryType

where Self: Sized, R: Try<Output = Self::Item>, <R as Try>::Residual: Residual<Option<Self::Item>>,

🔬This is a nightly-only experimental API. (iterator_try_reduce)

Reduces the elements to a single one by repeatedly applying a reducing operation. If the closure returns a failure, the failure is propagated back to the caller immediately.

fn all<F>(&mut self, f: F) -> bool

where Self: Sized, F: FnMut(Self::Item) -> bool,

Tests if every element of the iterator matches a predicate.

fn any<F>(&mut self, f: F) -> bool

where Self: Sized, F: FnMut(Self::Item) -> bool,

Tests if any element of the iterator matches a predicate.

fn find<P>(&mut self, predicate: P) -> Option<Self::Item>

where Self: Sized, P: FnMut(&Self::Item) -> bool,

Searches for an element of an iterator that satisfies a predicate.

fn find_map<B, F>(&mut self, f: F) -> Option<B>

where Self: Sized, F: FnMut(Self::Item) -> Option<B>,

Applies function to the elements of iterator and returns the first non-none result.

fn try_find<R>( &mut self, f: impl FnMut(&Self::Item) -> R, ) -> <<R as Try>::Residual as Residual<Option<Self::Item>>>::TryType

where Self: Sized, R: Try<Output = bool>, <R as Try>::Residual: Residual<Option<Self::Item>>,

🔬This is a nightly-only experimental API. (try_find)

Applies function to the elements of iterator and returns the first true result or the first error.

fn position<P>(&mut self, predicate: P) -> Option<usize>

where Self: Sized, P: FnMut(Self::Item) -> bool,

Searches for an element in an iterator, returning its index.

fn max(self) -> Option<Self::Item>

where Self: Sized, Self::Item: Ord,

Returns the maximum element of an iterator.

fn min(self) -> Option<Self::Item>

where Self: Sized, Self::Item: Ord,

Returns the minimum element of an iterator.

fn max_by_key<B, F>(self, f: F) -> Option<Self::Item>

where B: Ord, Self: Sized, F: FnMut(&Self::Item) -> B,

Returns the element that gives the maximum value from the specified function.

fn max_by<F>(self, compare: F) -> Option<Self::Item>

where Self: Sized, F: FnMut(&Self::Item, &Self::Item) -> Ordering,

Returns the element that gives the maximum value with respect to the specified comparison function.

fn min_by_key<B, F>(self, f: F) -> Option<Self::Item>

where B: Ord, Self: Sized, F: FnMut(&Self::Item) -> B,

Returns the element that gives the minimum value from the specified function.

fn min_by<F>(self, compare: F) -> Option<Self::Item>

where Self: Sized, F: FnMut(&Self::Item, &Self::Item) -> Ordering,

Returns the element that gives the minimum value with respect to the specified comparison function.

fn unzip<A, B, FromA, FromB>(self) -> (FromA, FromB)

where FromA: Default + Extend<A>, FromB: Default + Extend<B>, Self: Sized + Iterator<Item = (A, B)>,

Converts an iterator of pairs into a pair of containers.

fn copied<'a, T>(self) -> Copied<Self>

where T: Copy + 'a, Self: Sized + Iterator<Item = &'a T>,

Creates an iterator which copies all of its elements.

fn cloned<'a, T>(self) -> Cloned<Self>

where T: Clone + 'a, Self: Sized + Iterator<Item = &'a T>,

Creates an iterator which clones all of its elements.

fn cycle(self) -> Cycle<Self>

where Self: Sized + Clone,

Repeats an iterator endlessly.

fn array_chunks<const N: usize>(self) -> ArrayChunks<Self, N>

where Self: Sized,

🔬This is a nightly-only experimental API. (iter_array_chunks)

Returns an iterator over N elements of the iterator at a time.

fn sum<S>(self) -> S

where Self: Sized, S: Sum<Self::Item>,

Sums the elements of an iterator.

fn product<P>(self) -> P

where Self: Sized, P: Product<Self::Item>,

Iterates over the entire iterator, multiplying all the elements

fn cmp<I>(self, other: I) -> Ordering

where I: IntoIterator<Item = Self::Item>, Self::Item: Ord, Self: Sized,

Lexicographically compares the elements of this Iterator with those of another.

fn cmp_by<I, F>(self, other: I, cmp: F) -> Ordering

where Self: Sized, I: IntoIterator, F: FnMut(Self::Item, <I as IntoIterator>::Item) -> Ordering,

🔬This is a nightly-only experimental API. (iter_order_by)

Lexicographically compares the elements of this Iterator with those of another with respect to the specified comparison function.

fn partial_cmp<I>(self, other: I) -> Option<Ordering>

where I: IntoIterator, Self::Item: PartialOrd<<I as IntoIterator>::Item>, Self: Sized,

Lexicographically compares the PartialOrd elements of this Iterator with those of another. The comparison works like short-circuit evaluation, returning a result without comparing the remaining elements. As soon as an order can be determined, the evaluation stops and a result is returned.

fn partial_cmp_by<I, F>(self, other: I, partial_cmp: F) -> Option<Ordering>

where Self: Sized, I: IntoIterator, F: FnMut(Self::Item, <I as IntoIterator>::Item) -> Option<Ordering>,

🔬This is a nightly-only experimental API. (iter_order_by)

Lexicographically compares the elements of this Iterator with those of another with respect to the specified comparison function.

fn eq<I>(self, other: I) -> bool

where I: IntoIterator, Self::Item: PartialEq<<I as IntoIterator>::Item>, Self: Sized,

Determines if the elements of this Iterator are equal to those of another.

fn eq_by<I, F>(self, other: I, eq: F) -> bool

where Self: Sized, I: IntoIterator, F: FnMut(Self::Item, <I as IntoIterator>::Item) -> bool,

🔬This is a nightly-only experimental API. (iter_order_by)

Determines if the elements of this Iterator are equal to those of another with respect to the specified equality function.

fn ne<I>(self, other: I) -> bool

where I: IntoIterator, Self::Item: PartialEq<<I as IntoIterator>::Item>, Self: Sized,

Determines if the elements of this Iterator are not equal to those of another.

fn lt<I>(self, other: I) -> bool

where I: IntoIterator, Self::Item: PartialOrd<<I as IntoIterator>::Item>, Self: Sized,

Determines if the elements of this Iterator are lexicographically less than those of another.

fn le<I>(self, other: I) -> bool

where I: IntoIterator, Self::Item: PartialOrd<<I as IntoIterator>::Item>, Self: Sized,

Determines if the elements of this Iterator are lexicographically less or equal to those of another.

fn gt<I>(self, other: I) -> bool

where I: IntoIterator, Self::Item: PartialOrd<<I as IntoIterator>::Item>, Self: Sized,

Determines if the elements of this Iterator are lexicographically greater than those of another.

fn ge<I>(self, other: I) -> bool

where I: IntoIterator, Self::Item: PartialOrd<<I as IntoIterator>::Item>, Self: Sized,

Determines if the elements of this Iterator are lexicographically greater than or equal to those of another.

fn is_sorted(self) -> bool

where Self: Sized, Self::Item: PartialOrd,

Checks if the elements of this iterator are sorted.

fn is_sorted_by<F>(self, compare: F) -> bool

where Self: Sized, F: FnMut(&Self::Item, &Self::Item) -> bool,

Checks if the elements of this iterator are sorted using the given comparator function.

fn is_sorted_by_key<F, K>(self, f: F) -> bool

where Self: Sized, F: FnMut(Self::Item) -> K, K: PartialOrd,

Checks if the elements of this iterator are sorted using the given key extraction function.

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

fn produces(self, visited: Seq<(K, V)>, o: Self) -> bool

logic(open, prophetic)

/* Macro-generated */

fn completed(&mut self) -> bool

logic(open, prophetic)

self.is_empty()

fn produces_refl(self)

logic(law)

ensures

self.produces(Seq::empty(), self)

fn produces_trans( a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self, )

logic(law)

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

a.produces(ab.concat(bc), c)

fn map_inv<B, F>(self, func: F) -> MapInv<Self, F>

where Self: Sized, F: FnMut(Self::Item, Snapshot<Seq<Self::Item>>) -> B,

terminates

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

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

logic(open, inline)

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

logic(open, inline)

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>>, )

logic

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>

logic(open)

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>

logic(open)

/* Macro-generated */

ensures

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

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

logic(open, inline)

let _ = Self::ext_eq;
forall<k: K> self.get(k).eq(other.get(k))

ensures

result == (self == other)

fn commutative(a: Self, b: Self)

logic(law)

ensures

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

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

logic

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>

logic(open)

Some(self.filter_map(|(_, v): (K, V)| v.core()))

fn core_idemp(self)

logic

requires

self.core() != None

ensures

let c = self.core().unwrap_logic();
c.op(c) == Some(c)

ensures

self.core().unwrap_logic().op(self) == Some(self)

fn core_is_maximal_idemp(self, i: Self)

logic

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)

logic(law)

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

logic(open, sealed)

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

logic(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 associative_none(a: Self, b: Self, c: Self, bc: Self)

Specialized version of Self::associative, in the case where a.op(b) == None.

fn associative_some(a: Self, b: Self, c: Self, ab: Self, bc: Self)

Specialized version of Self::associative, in the case where a.op(b) and b.op(c) are both valid.

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

logic(open, prophetic)

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

fn resolve_coherence(self)

logic(open(pub(self)), prophetic)

requires

structural_resolve(self)

ensures

self.resolve()

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

fn unit() -> Self

logic(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

logic(open)

self.filter_map(|(_, v): (K, V)| v.core())

ensures

self.core() == Some(result)

fn core_total_idemp(self)

logic

ensures

self.core_total().op(self.core_total()) == Some(self.core_total())

ensures

self.core_total().op(self) == Some(self)

fn incl_refl()

In unitary RAs, the inclusion relation is reflexive

fn unit_core()

The unit is its own core

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