Struct Seq

Source

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

Expand description

A type of sequence usable in pearlite and ghost! blocks.

§Logic

This type is (in particular) the logical representation of a Vec. This can be accessed via its view (The @ operator).

#[logic]
fn get_model<T>(v: Vec<T>) -> Seq<T> {
    pearlite!(v@)
}

§Ghost

Since Vec have finite capacity, this could cause some issues in ghost code:

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

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

Implementations§

Source §

impl<T> Seq<T>

This impl block contains no items.

Logical definitions

Source §

impl<T> Seq<T>

Ghost definitions

Source

pub fn new() -> Ghost<Self>

Constructs a new, empty Seq<T>.

This can only be manipulated in the ghost world, and as such is wrapped in Ghost.

§Example

use creusot_std::prelude::*;
let ghost_seq = Seq::<i32>::new();
proof_assert!(seq == Seq::create());

Source

pub fn len_ghost(&self) -> Int

Returns the number of elements in the sequence, also referred to as its ‘length’.

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

§Example

use creusot_std::prelude::*;

let mut s = Seq::new();
ghost! {
    s.push_back_ghost(1);
    s.push_back_ghost(2);
    s.push_back_ghost(3);
    let len = s.len_ghost();
    proof_assert!(len == 3);
};

Source

pub fn is_empty_ghost(&self) -> bool

Returns true if the sequence is empty.

§Example

use creusot_std::prelude::*;
#[check(ghost)]
#[requires(s.len() == 0)]
pub fn foo(mut s: Seq<i32>) {
    assert!(s.is_empty_ghost());
    s.push_back_ghost(1i32);
    assert!(!s.is_empty_ghost());
}
ghost! {
    foo(Seq::new().into_inner())
};

Source

pub fn push_front_ghost(&mut self, x: T)

Appends an element to the front of a collection.

§Example

use creusot_std::prelude::*;

let mut s = Seq::new();
ghost! {
    s.push_front_ghost(1);
    s.push_front_ghost(2);
    s.push_front_ghost(3);
    proof_assert!(s[0] == 3i32 && s[1] == 2i32 && s[2] == 1i32);
};

Source

pub fn push_back_ghost(&mut self, x: T)

Appends an element to the back of a collection.

§Example

use creusot_std::prelude::*;

let mut s = Seq::new();
ghost! {
    s.push_back_ghost(1);
    s.push_back_ghost(2);
    s.push_back_ghost(3);
    proof_assert!(s[0] == 1i32 && s[1] == 2i32 && s[2] == 3i32);
};

Source

pub fn get_ghost(&self, index: Int) -> Option<&T>

Returns a reference to an element at index or None if index is out of bounds.

§Example

use creusot_std::prelude::*;

let mut s = Seq::new();
ghost! {
    s.push_back_ghost(10);
    s.push_back_ghost(40);
    s.push_back_ghost(30);
    let get1 = s.get_ghost(1int);
    let get2 = s.get_ghost(3int);
    proof_assert!(get1 == Some(&40i32));
    proof_assert!(get2 == None);
};

Source

pub fn get_mut_ghost(&mut self, index: Int) -> Option<&mut T>

Returns a mutable reference to an element at index or None if index is out of bounds.

§Example

use creusot_std::prelude::*;

let mut s = Seq::new();

ghost! {
    s.push_back_ghost(0);
    s.push_back_ghost(1);
    s.push_back_ghost(2);
    if let Some(elem) = s.get_mut_ghost(1int) {
        *elem = 42;
    }
    proof_assert!(s[0] == 0i32 && s[1] == 42i32 && s[2] == 2i32);
};

Source

pub fn pop_back_ghost(&mut self) -> Option<T>

Removes the last element from a vector and returns it, or None if it is empty.

§Example

use creusot_std::prelude::*;

let mut s = Seq::new();
ghost! {
    s.push_back_ghost(1);
    s.push_back_ghost(2);
    s.push_back_ghost(3);
    let popped = s.pop_back_ghost();
    proof_assert!(popped == Some(3i32));
    proof_assert!(s[0] == 1i32 && s[1] == 2i32);
};

Source

pub fn pop_front_ghost(&mut self) -> Option<T>

Removes the first element from a vector and returns it, or None if it is empty.

§Example

use creusot_std::prelude::*;

let mut s = Seq::new();
ghost! {
    s.push_back_ghost(1);
    s.push_back_ghost(2);
    s.push_back_ghost(3);
    let popped = s.pop_front_ghost();
    proof_assert!(popped == Some(1i32));
    proof_assert!(s[0] == 2i32 && s[1] == 3i32);
};

Source

pub fn clear_ghost(&mut self)

Clears the sequence, removing all values.

§Example

use creusot_std::prelude::*;

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

Source