Struct creusot_contracts::logic::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 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 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

ensures

result ==> self == other

impl<T: ?Sized> FSet<T>

Ghost definitions

pub fn new() -> GhostBox<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>