Struct FSet

Source

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

Expand description

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§

Source §

impl<T> FSet<T>

Ghost definitions

Source

pub fn new() -> Ghost<Self>

Create a new, empty set on the ghost heap.

Source

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_std::{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);
};

Source

pub fn contains_ghost(&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_ghost(1);
    let (b1, b2) = (set.contains_ghost(&1), set.contains_ghost(&2));
    proof_assert!(b1);
    proof_assert!(!b2);
};

Source

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_std::{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);
};

Source

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_std::{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);
};

Source

pub fn clear_ghost(&mut self)

Clears the set, removing all values.

§Example

use creusot_std::{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());
};