Struct creusot_contracts::logic::Seq

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

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

impl<T: ?Sized> Seq<T>

Logical definitions

pub const EMPTY: Self = _

The empty sequence.

pub fn empty() -> Self

Returns the empty sequence.

logic

Self::EMPTY

pub fn create(n: Int, mapping: Mapping<Int, T>) -> Self

Create a new sequence in pearlite.

The new sequence will be of length n, and will contain mapping[i] at index i.

Example

let s = snapshot!(Seq::create(5, |i| i + 1));
proof_assert!(s.len() == 5);
proof_assert!(forall<i: Int> 0 <= i && i < 5 ==> s[i] == i + 1);

logic

pub fn get(self, ix: Int) -> Option<T>

where T: Sized,

Returns the value at index ix.

If ix is out of bounds, return None.

logic

if 0 <= ix && ix < self.len() {
    Some(self.index_logic(ix))
} else {
    None
}

pub fn index_logic_unsized(self, ix: Int) -> Box<T>

Returns the value at index ix.

If ix is out of bounds, the returned value is meaningless.

You should prefer using the indexing operator s[ix].

Example

let s = snapshot!(Seq::singleton(2));
proof_assert!(s.index_logic_unsized(0) == 2);
proof_assert!(s[0] == 2); // prefer this

logic

pub fn subsequence(self, start: Int, end: Int) -> Self

Returns the subsequence between indices start and end.

If either start or end are out of bounds, the result is meaningless.

Example

let subs = snapshot! {
    let s: Seq<Int> = Seq::create(10, |i| i);
    s.subsequence(2, 5)
};
proof_assert!(subs.len() == 3);
proof_assert!(subs[0] == 2 && subs[1] == 3 && subs[2] == 4);

logic

pub fn singleton(value: T) -> Self

Create a sequence containing one element.

Example

let s = snapshot!(Seq::singleton(42));
proof_assert!(s.len() == 1);
proof_assert!(s[0] == 42);

logic

pub fn tail(self) -> Self

Returns the sequence without its first element.

If the sequence is empty, the result is meaningless.

Example

let s = snapshot!(Seq::singleton(5).push_back(10).push_back(15));
proof_assert!(s.tail() == Seq::singleton(10).push_back(15));
proof_assert!(s.tail().tail() == Seq::singleton(15));
proof_assert!(s.tail().tail().tail() == Seq::EMPTY);

logic

self.subsequence(1, self.len())

pub fn len(self) -> Int

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

Example

#[requires(v@.len() > 0)]
fn f<T>(v: Vec<T>) { /* ... */ }

logic

pub fn set(self, ix: Int, x: T) -> Self

Returns a new sequence, where the element at index ix has been replaced by x.

If ix is out of bounds, the result is meaningless.

Example

let s = snapshot!(Seq::create(2, |_| 0));
let s2 = snapshot!(s.set(1, 3));
proof_assert!(s2[0] == 0);
proof_assert!(s2[1] == 3);

logic

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

Extensional equality

Returns true if self and other have the same length, and contain the same elements at the same indices.

This is in fact equivalent with normal equality.

logic

pub fn push_front(self, x: T) -> Self

Returns a new sequence, where x has been prepended to self.

Example

let s = snapshot!(Seq::singleton(1));
let s2 = snapshot!(s.push_front(2));
proof_assert!(s2[0] == 2);
proof_assert!(s2[1] == 1);

logic

Self::cons(x, self)

pub fn push_back(self, x: T) -> Self

Returns a new sequence, where x has been appended to self.

Example

let s = snapshot!(Seq::singleton(1));
let s2 = snapshot!(s.push_back(2));
proof_assert!(s2[0] == 1);
proof_assert!(s2[1] == 2);

logic

pub fn concat(self, other: Self) -> Self

Returns a new sequence, made of the concatenation of self and other.

Example

let s1 = snapshot!(Seq::singleton(1));
let s2 = snapshot!(Seq::create(2, |i| i));
let s = snapshot!(s1.concat(s2));
proof_assert!(s[0] == 1);
proof_assert!(s[1] == 0);
proof_assert!(s[2] == 1);

logic

pub fn reverse(self) -> Self

Returns a new sequence, which is self in reverse order.

Example

let s = snapshot!(Seq::create(3, |i| i));
let s2 = snapshot!(s.reverse());
proof_assert!(s2[0] == 2);
proof_assert!(s2[1] == 1);
proof_assert!(s2[2] == 0);

logic

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

Returns true if other is a permutation of self.

logic

self.permut(other, 0, self.len())

pub fn permut(self, other: Self, start: Int, end: Int) -> bool

Returns true if:

• self and other have the same length
• start and end are in bounds (between 0 and self.len() included)
• Every element of self between start (included) and end (excluded) can also be found in other between start and end, and vice-versa

logic

pub fn exchange(self, other: Self, i: Int, j: Int) -> bool

Returns true if:

• self and other have the same length
• i and j are in bounds (between 0 and self.len() excluded)
• other is equal to self where the elements at i and j are swapped

logic

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

where T: Sized,

Returns true if there is an index i such that self[i] == x.

logic

pearlite! { exists<i : Int> 0 <= i &&  i < self.len() && self[i] == x }

pub fn sorted_range(self, start: Int, end: Int) -> bool

where T: OrdLogic + Sized,

Returns true if self is sorted between start and end.

logic

pearlite! {
    forall<i : Int, j : Int> start <= i && i <= j && j < end ==> self[i] <= self[j]
}

pub fn sorted(self) -> bool

where T: OrdLogic + Sized,

Returns true if self is sorted.

logic

self.sorted_range(0, self.len())

impl<T: ?Sized> Seq<&T>

pub fn to_owned_seq(self) -> Seq<T>

Convert Seq<&T> to Seq<T>.

This is simply a utility method, because &T is equivalent to T in pearlite.

logic

impl<T> Seq<T>

Ghost definitions

pub fn new() -> GhostBox<Self>

Constructs a new, empty Seq<T>.

This is allocated on the ghost heap, and as such is wrapped in GhostBox.

Example

use creusot_contracts::{proof_assert, Seq};
let ghost_seq = Seq::<i32>::new();
proof_assert!(seq == Seq::create());

pure

ensures

*result == Self::EMPTY

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_contracts::{ghost, proof_assert, Seq};

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

pure

ensures

result == self.len()

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

Appends an element to the front of a collection.

Example

use creusot_contracts::{ghost, proof_assert, Seq};

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

pure

ensures

^self == self.push_front(x)

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

Appends an element to the back of a collection.

Example

use creusot_contracts::{ghost, proof_assert, Seq};

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

pure

ensures

^self == self.push_back(x)

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_contracts::{ghost, Int, proof_assert, Seq};

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

pure

ensures

match self.get(index) {
        None => result == None,
        Some(v) => result == Some(&v),
    }

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_contracts::{ghost, Int, proof_assert, Seq};

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

pure

ensures

match result {
        None => self.get(index) == None && *self == ^self,
        Some(r) => self.get(index) == Some(*r) && ^r == (^self)[index],
    }

ensures

forall<i: Int> i != index ==> (*self).get(index) == (^self).get(index)

ensures

(*self).len() == (^self).len()

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_contracts::{ghost, proof_assert, Seq};

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

pure

ensures

match result {
        None => *self == Seq::EMPTY && *self == ^self,
        Some(r) => *self == (^self).push_back(r)
    }

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_contracts::{ghost, proof_assert, Seq};

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

pure

ensures

match result {
        None => *self == Seq::EMPTY && *self == ^self,
        Some(r) => *self == (^self).push_front(r)
    }

Trait Implementations

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

fn clone(&self) -> Self

pure

ensures

result == *self

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

Performs copy-assignment from source.

impl<T> IndexLogic<Int> for Seq<T>

fn index_logic(self, _: Int) -> Self::Item

logic

type Item = T

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

fn invariant(self) -> bool

logic(prophetic)

pearlite! { forall<i:Int> 0 <= i && i < self.len() ==> inv(self.index_logic_unsized(i)) }

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