Struct FSet

pub struct FSet<T: ?Sized>(/* 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: ?Sized> FSet<T>

pub const EMPTY: Self

The empty set.

pub fn empty() -> Self

Returns the empty set.

logic

Self::EMPTY

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

Returns true if e is in the set.

logic

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.

logic

Self::add(e, self)

pub fn is_empty(self) -> bool

Returns true if the set contains no elements.

logic

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

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

logic

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.

logic

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.

logic

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.

logic

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

Returns true if every element of self is in other.

logic

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

Returns true if every element of other is in self.

logic

Self::is_subset(other, self)

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

Returns true if self and other are disjoint.

logic

pub fn len(self) -> Int

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

logic

pub fn peek(self) -> T

where T: Sized,

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

logic

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

where T: Sized,

Extensional equality

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

This is in fact equivalent with normal equality.

logic

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

ensures

result ==> self == other

impl<T> FSet<T>

pub fn singleton(x: T) -> Self

Returns the set containing only x.

logic

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.

logic

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.

logic

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

Returns the image of a set by a function.

logic

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.

logic

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.

logic

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.

logic

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.

logic

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: Int> 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.

logic

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

logic

impl<T: ?Sized> FSet<T>

Ghost definitions

pub fn new() -> Ghost<Self>

Create a new, empty set on the ghost heap.

pure

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

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

pure

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

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

pure

ensures

result == self.contains(*value)

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

where T: Sized,

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

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

pure

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.

pure

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

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

pure

ensures

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

ensures

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

Trait Implementations

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

fn clone(&self) -> Self

pure

ensures

result == *self

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

Performs copy-assignment from source.

impl<T: ?Sized> Invariant for FSet<T>

fn invariant(self) -> bool

logic(prophetic)

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

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