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.

logic

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

Returns true if e is in the set.

logic(open, inline)

Self::mem(e, self)

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

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

logic(open, inline)

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

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

Self::is_subset(other, self)

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

Returns true if self and other are disjoint.

logic

pub fn len_logic(self) -> Int

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

logic

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

logic

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.

logic(open)

forall <e: &T> self.contains(e) == other.contains(e)

ensures

#[trigger(self == other)] result == (self == other)

pub fn singleton(x: T) -> Self

Returns the set containing only x.

logic(open)

FSet::empty().add(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(opaque)

ensures

forall<y: U> #[trigger(result.contains(&y))]
    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(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.

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

proof_assert!(forall<x:T, xs: Seq<T>> xs.cons(x).tail() == xs);
proof_assert!(forall<xs: Seq<T>> 0 < xs.len() ==> xs.tail().cons(xs[0]) == xs);
s.unions(|x| ss.map(|xs: Seq<_>| xs.cons(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.

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

logic(open)

/* Macro-generated */

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

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

pub fn unions_union<U>( self, other: Self, f: Mapping<T, FSet<U>>, g: Mapping<T, FSet<U>>, )

Distributivity of unions over union.

logic

ensures

self.union(other).unions(f) == self.unions(f).union(other.unions(f))

ensures

self.unions(|x| f.get(x).union(g.get(x))) == self.unions(f).union(self.unions(g))

pub fn map_union<U>(self, other: Self, f: Mapping<T, U>)

Distributivity of map over union.

logic

ensures

self.union(other).map(f) == self.map(f).union(other.map(f))

pub fn concat_union(s1: FSet<Seq<T>>, s2: FSet<Seq<T>>, t: FSet<Seq<T>>)

Distributivity of concat over union.

logic

ensures

FSet::concat(s1.union(s2), t) == FSet::concat(s1, t).union(FSet::concat(s2, t))

ensures

FSet::concat(t, s1.union(s2)) == FSet::concat(t, s1).union(FSet::concat(t, s2))

pub fn cons_concat(self, t: FSet<Seq<T>>, u: FSet<Seq<T>>)

Distributivity of cons over union.

logic

ensures

FSet::concat(FSet::cons(self, t), u) == FSet::cons(self, FSet::concat(t, u))

pub fn concat_replicate(self, n: Int, m: Int)

Distributivity of replicate over union.

logic

requires

0 <= n && 0 <= m

ensures

self.replicate(n + m) == FSet::concat(self.replicate(n), self.replicate(m))

pub fn concat_empty(s: FSet<Seq<T>>)

The neutral element of FSet::concat is FSet::singleton(Seq::empty()).

logic

ensures

FSet::concat(FSet::singleton(Seq::empty()), s) == s

ensures

FSet::concat(s, FSet::singleton(Seq::empty())) == s

pub fn concat_replicate_up_to(self, n: Int, m: Int)

An equation relating s.replicate_up_to(m) and s.replicate_up_to(n).

logic

requires

0 <= n && n < m

ensures

self.replicate_up_to(m) == self.replicate_up_to(n).union(
    FSet::concat(self.replicate(n + 1), self.replicate_up_to(m - n - 1)))

impl FSet<Int>

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

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

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

ghost

ensures

result.is_empty()

pub fn len(&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_std::{logic::FSet, prelude::*};

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

ghost

ensures

#[logic_alias(self.len_logic())]

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

Returns true if the set contains the specified value.

Example

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

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

ghost

ensures

#[logic_alias(self.contains_logic(*value))]

pub fn insert(&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_std::{logic::FSet, prelude::*};

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

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

ghost

ensures

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

ensures

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

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

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

Example

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

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

ghost

ensures

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

ensures

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

pub fn clear(&mut self)

Clears the set, removing all values.

Example

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

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

ghost

ensures

^self == Self::empty()

Trait Implementations

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

fn clone(&self) -> Self

ghost

ensures

result == *self

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

Performs copy-assignment from source.

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

impl<T> Invariant for FSet<T>

fn invariant(self) -> bool

logic(open, prophetic, inline)

forall<x: T> self.contains(&x) ==> inv(x)

impl<T> Resolve for FSet<T>

fn resolve(self) -> bool

logic(open, prophetic)

forall<x: T> self.contains(&x) ==> resolve(x)

fn resolve_coherence(self)

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

requires

structural_resolve(self)

ensures

self.resolve()