Struct Seq 

pub struct Seq<T>(/* 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> Seq<T>

Logical definitions

pub fn empty() -> Self

Returns the empty sequence.

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> 0 <= i && i < 5 ==> s[i] == i + 1);

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

Returns the value at index ix.

If ix is out of bounds, return None.

(open)

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

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

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

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![5, 10, 15]);
proof_assert!(s.tail() == seq![10, 15]);
proof_assert!(s.tail().tail() == Seq::singleton(15));
proof_assert!(s.tail().tail().tail() == Seq::empty());

(open)

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

pub fn pop_front(self) -> Self

Alias for Self::tail.

(open)

self.tail()

pub fn pop_back(self) -> Self

Returns the sequence without its last element.

If the sequence is empty, the result is meaningless.

Example

let s = snapshot!(seq![5, 10, 15]);
proof_assert!(s.pop_back() == seq![5, 10]);
proof_assert!(s.pop_back().pop_back() == Seq::singleton(5));
proof_assert!(s.pop_back().pop_back().pop_back() == Seq::empty());

(open)

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

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>) { /* ... */ }

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

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.

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

(open, inline)

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

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

pub fn map<U>(self, m: Mapping<T, U>) -> Seq<U>

ensures

result.len() == self.len()

ensures

forall<i> 0 <= i && i < self.len() ==> result[i] == m[self[i]]

pub fn flat_map<U>(self, other: Mapping<T, Seq<U>>) -> Seq<U>

(open)

if self.len() == 0 {
    Seq::empty()
} else {
    other.get(*self.index_logic_unsized(0)).concat(self.tail().flat_map(other))
}

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

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

Returns true if other is a permutation of self.

(open)

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

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

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

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

(open)

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

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

where T: OrdLogic,

Returns true if self is sorted between start and end.

(open)

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

pub fn sorted(self) -> bool

where T: OrdLogic,

Returns true if self is sorted.

(open)

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

pub fn concat_contains()

(open)

{}

ensures

forall<a: Seq<T>, b: Seq<T>, x>
        a.concat(b).contains(x) == a.contains(x) || b.contains(x)

impl<T> Seq<Seq<T>>

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

(open)

if self.len() == 0 {
    Seq::empty()
} else {
    self.index_logic_unsized(0).concat(self.tail().flatten())
}

impl<T> 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.

impl<T> Seq<T>

Ghost definitions

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_contracts::prelude::*;
let ghost_seq = Seq::<i32>::new();
proof_assert!(seq == Seq::create());

terminates

ghost

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

terminates

ghost

ensures

result == self.len()

pub fn is_empty_ghost(&self) -> bool

Returns true if the sequence is empty.

Example

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

terminates

ghost

ensures

result == (self.len() == 0)

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

Appends an element to the front of a collection.

Example

use creusot_contracts::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);
};

terminates

ghost

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

terminates

ghost

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

terminates

ghost

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

terminates

ghost

ensures

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

ensures

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

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

terminates

ghost

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

terminates

ghost

ensures

match result {
        None => *self == Seq::empty() && *self == ^self,
        Some(r) => (*self).len() > 0 && r == (*self)[0] && ^self == (*self).tail()
    }

pub fn clear_ghost(&mut self)

Clears the sequence, removing all values.

Example

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

terminates

ghost

ensures

^self == Self::empty()

pub fn split_off_ghost(&mut self, mid: Int) -> Self

Split a sequence in two at the given index.

terminates

ghost

requires

0 <= mid && mid <= self.len()

ensures

(^self).len() == mid

ensures

(^self).concat(result) == *self

impl Seq<char>

pub fn to_bytes(self) -> Seq<u8>

(open)

pearlite! { self.flat_map(|c: char| c.to_utf8()) }

Trait Implementations

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

fn clone(&self) -> Self

terminates

ghost

ensures

result == *self

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

Performs copy-assignment from source.

impl<T> Index<(Int, Int)> for Seq<T>

fn index(&self, index: (Int, Int)) -> &Self::Output

terminates

ghost

requires

0 <= index.0 && index.0 < self.len() && 0 <= index.1 && index.1 < self.len()

ensures

result.0 == self[index.0] && result.1 == self[index.1]

type Output = (T, T)

The returned type after indexing.

impl<T> Index<Int> for Seq<T>

fn index(&self, index: Int) -> &Self::Output

terminates

ghost

requires

0 <= index && index < self.len()

ensures

*result == self[index]

type Output = T

The returned type after indexing.

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

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

type Item = T

impl<T> IndexMut<(Int, Int)> for Seq<T>

fn index_mut(&mut self, index: (Int, Int)) -> &mut Self::Output

terminates

ghost

requires

0 <= index.0 && index.0 < self.len() && 0 <= index.1 && index.1 < self.len()

requires

index.0 != index.1

ensures

(*result).0 == (*self)[index.0] && (*result).1 == (*self)[index.1]
           && (^result).0 == (^self)[index.0] && (^result).1 == (^self)[index.1]

ensures

forall<i> i != index.0 && i != index.1 ==> (*self).get(i) == (^self).get(i)

ensures

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

impl<T> IndexMut<Int> for Seq<T>

fn index_mut(&mut self, index: Int) -> &mut Self::Output

terminates

ghost

requires

0 <= index && index < self.len()

ensures

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

ensures

*result == (*self)[index] && ^result == (^self)[index]

ensures

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

impl<'a, T> IntoIterator for &'a Seq<T>

fn into_iter(self) -> Self::IntoIter

terminates

ghost

ensures

result@ == *self

type Item = &'a T

The type of the elements being iterated over.

type IntoIter = SeqIterRef<'a, T>

Which kind of iterator are we turning this into?

impl<T> IntoIterator for Seq<T>

fn into_iter(self) -> SeqIter<T>

terminates

ghost

ensures

result@ == self

type Item = T

The type of the elements being iterated over.

type IntoIter = SeqIter<T>

Which kind of iterator are we turning this into?

impl<T> Invariant for Seq<T>

fn invariant(self) -> bool

(open, prophetic, inline)

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

impl<T> Resolve for Seq<T>

fn resolve(self) -> bool

(open, prophetic)

pearlite! { forall<i : Int> resolve(self.get(i)) }

fn resolve_coherence(self)

(open(pub(self)), prophetic)

requires

structural_resolve(self)

ensures

self.resolve()

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

impl<T: Plain> Plain for Seq<T>