Struct FSet 

pub struct FSet<T>(/* private fields */);

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

If you need an infinite set, see Set.

Ghost

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

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

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

Implementations

impl<T> FSet<T>

pub fn empty() -> Self

Returns the empty set.

pub fn contains(self, e: T) -> bool

Returns true if e is in the set.

(open, inline)

Self::mem(e, self)

pub fn insert(self, e: T) -> Self

Returns a new set, where e has been added if it was not present.

(open, inline)

Self::add(e, self)

pub fn is_empty(self) -> bool

Returns true if the set contains no elements.

pub fn remove(self, e: T) -> Self

Returns a new set, where e is no longer present.

(open, inline)

Self::rem(e, self)

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

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

An element is in the result if it is in self or if it is in other.

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

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

An element is in the result if it is in self or if it is in other.

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

Returns a new set, which is the difference of self with other.

An element is in the result if and only if it is in self but not in other.

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

Returns true if every element of self is in other.

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

Returns true if every element of other is in self.

(open, inline)

Self::is_subset(other, self)

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

Returns true if self and other are disjoint.

pub fn len(self) -> Int

Returns the number of elements in the set, also called its length.

pub fn peek(self) -> T

Get an arbitrary element of the set.

Returns

• If the set is nonempty, the result is guaranteed to be in the set
• If the set is empty, the result is unspecified

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

Extensional equality

Returns true if self and other contain exactly the same elements.

This is in fact equivalent with normal equality.

(open)

pearlite! {
    forall <e: T> self.contains(e) == other.contains(e)
}

ensures

result == (self == other)

pub fn singleton(x: T) -> Self

Returns the set containing only x.

(open)

FSet::empty().insert(x)

ensures

forall<y: T> result.contains(y) == (x == y)

pub fn unions<U>(self, f: Mapping<T, FSet<U>>) -> FSet<U>

Returns the union of sets f(t) over all t: T.

(open)

if self.len() == 0 {
    FSet::empty()
} else {
    let x = self.peek();
    f.get(x).union(self.remove(x).unions(f))
}

ensures

forall<y: U> result.contains(y) == exists<x: T> self.contains(x) && f.get(x).contains(y)

pub fn fmap<U>(_: Mapping<T, U>, _: Self) -> FSet<U>

Flipped map.

pub fn map<U>(self, f: Mapping<T, U>) -> FSet<U>

Returns the image of a set by a function.

(open)

FSet::fmap(f, self)

pub fn filter(self, f: Mapping<T, bool>) -> Self

Returns the subset of elements of self which satisfy the predicate f.

pub fn cons(s: FSet<T>, ss: FSet<Seq<T>>) -> FSet<Seq<T>>

Returns the set of sequences whose head is in s and whose tail is in ss.

(open)

proof_assert!(forall<x:T, xs: Seq<T>> xs.push_front(x).tail() == xs);
proof_assert!(forall<xs: Seq<T>> 0 < xs.len() ==> xs.tail().push_front(xs[0]) == xs);
s.unions(|x| ss.map(|xs: Seq<_>| xs.push_front(x)))

ensures

forall<xs: Seq<T>> result.contains(xs) == (0 < xs.len() && s.contains(xs[0]) && ss.contains(xs.tail()))

pub fn concat(s: FSet<Seq<T>>, t: FSet<Seq<T>>) -> FSet<Seq<T>>

Returns the set of concatenations of a sequence in s and a sequence in t.

(open)

s.unions(|ys: Seq<_>| t.map(|zs| ys.concat(zs)))

ensures

forall<xs: Seq<T>> result.contains(xs) == (exists<ys: Seq<T>, zs: Seq<T>> s.contains(ys) && t.contains(zs) && xs == ys.concat(zs))

pub fn replicate(self, n: Int) -> FSet<Seq<T>>

Returns the set of sequences of length n whose elements are in self.

(open)

pearlite! {
    if n == 0 {
        proof_assert! { forall<xs: Seq<T>> xs.len() == 0 ==> xs == Seq::empty() };
        FSet::singleton(Seq::empty())
    } else {
        proof_assert! { forall<xs: Seq<T>, i> 0 < i && i < xs.len() ==> xs[i] == xs.tail()[i-1] };
        FSet::cons(self, self.replicate(n - 1))
    }
}

requires

n >= 0

ensures

forall<xs: Seq<T>> result.contains(xs) == (xs.len() == n && forall<x: T> xs.contains(x) ==> self.contains(x))

pub fn replicate_up_to(self, n: Int) -> FSet<Seq<T>>

Returns the set of sequences of length at most n whose elements are in self.

(open)

pearlite! {
    if n == 0 {
        proof_assert! { forall<xs: Seq<T>> xs.len() == 0 ==> xs == Seq::empty() };
        FSet::singleton(Seq::empty())
    } else {
        self.replicate_up_to(n - 1).union(self.replicate(n))
    }
}

requires

n >= 0

ensures

forall<xs: Seq<T>> result.contains(xs) == (xs.len() <= n && forall<x: T> xs.contains(x) ==> self.contains(x))

impl FSet<Int>

pub fn interval(i: Int, j: Int) -> FSet<Int>

Return the interval of integers in [i, j).

(open)

let _ = (i, j);
dead

impl<T> FSet<T>

Ghost definitions

pub fn new() -> Ghost<Self>

Create a new, empty set on the ghost heap.

terminates

ghost

ensures

result.is_empty()

pub fn len_ghost(&self) -> Int

Returns the number of elements in the set.

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

Example

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

let mut set = FSet::new();
ghost! {
    let len1 = set.len_ghost();
    set.insert_ghost(1);
    set.insert_ghost(2);
    set.insert_ghost(1);
    let len2 = set.len_ghost();
    proof_assert!(len1 == 0);
    proof_assert!(len2 == 2);
};

terminates

ghost

ensures

result == self.len()

pub fn contains_ghost(&self, value: &T) -> bool

Returns true if the set contains the specified value.

Example

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

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

terminates

ghost

ensures

result == self.contains(*value)

pub fn insert_ghost(&mut self, value: T) -> bool

Adds a value to the set.

Returns whether the value was newly inserted. That is:

• If the set did not previously contain this value, true is returned.
• If the set already contained this value, false is returned, and the set is not modified: original value is not replaced, and the value passed as argument is dropped.

Example

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

let mut set = FSet::new();
ghost! {
    let res1 = set.insert_ghost(42);
    proof_assert!(res1);
    proof_assert!(set.contains(42i32));

    let res2 = set.insert_ghost(41);
    let res3 = set.insert_ghost(42);
    proof_assert!(res2);
    proof_assert!(!res3);
    proof_assert!(set.len() == 2);
};

terminates

ghost

ensures

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

ensures

result == !(*self).contains(value)

pub fn insert_ghost_unsized(&mut self, value: Box<T>) -> bool

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

terminates

ghost

ensures

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

ensures

result == !(*self).contains(*value)

pub fn remove_ghost(&mut self, value: &T) -> bool

Removes a value from the set. Returns whether the value was present in the set.

Example

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

let mut set = FSet::new();
let res = ghost! {
    set.insert_ghost(1);
    let res1 = set.remove_ghost(&1);
    let res2 = set.remove_ghost(&1);
    proof_assert!(res1 && !res2);
};

terminates

ghost

ensures

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

ensures

result == (*self).contains(*value)

pub fn clear_ghost(&mut self)

Clears the set, removing all values.

Example

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

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

terminates

ghost

ensures

^self == Self::empty()

Trait Implementations

impl<T: Clone + Copy> Clone for FSet<T>

fn clone(&self) -> Self

terminates

ghost

ensures

result == *self

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

Performs copy-assignment from source.

impl<T> Invariant for FSet<T>

fn invariant(self) -> bool

(open, prophetic, inline)

pearlite! { forall<x: T> self.contains(x) ==> inv(x) }

impl<T> Resolve for FSet<T>

fn resolve(self) -> bool

(open, prophetic)

pearlite! { forall<x: T> self.contains(x) ==> resolve(x) }

fn resolve_coherence(self)

(open(pub(self)), prophetic)

requires

structural_resolve(self)

ensures

self.resolve()

impl<T: Clone + Copy> Copy for FSet<T>