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.

logic

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

logic

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

Returns the value at index ix.

If ix is out of bounds, return None.

logic(open)

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

pub fn index_logic_unsized<'a>(self, ix: Int) -> &'a 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![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());

logic(open)

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

pub fn pop_front(self) -> Self

Alias for Self::tail.

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

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

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

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 map<U>(self, m: Mapping<T, U>) -> Seq<U>

logic

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>

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

logic

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

Returns true if other is a permutation of self.

logic(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 occurs as many times in self[start..end] as in other[start..end].

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

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

logic(open)

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.

logic(open)

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.

logic(open)

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

pub fn concat_contains()

logic(open)

/* Macro-generated */

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>

logic(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.

logic

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

terminates

ghost

ensures

result == self.len()

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

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

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

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

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

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

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

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

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>

logic(open)

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

logic

type Item = T

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

fn index_logic(self, range: Range<Int>) -> Self::Item

logic(open, inline)

self.subsequence(range.start, range.end)

type Item = Seq<T>

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

fn index_logic(self, range: RangeFrom<Int>) -> Self::Item

logic(open, inline)

self.subsequence(range.start, self.len())

type Item = Seq<T>

impl<T> IndexLogic<RangeFull> for Seq<T>

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

logic(open, inline)

self

type Item = Seq<T>

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

fn index_logic(self, range: RangeInclusive<Int>) -> Self::Item

logic(open, inline)

self.subsequence(range.start_log(), range.end_log() + 1)

type Item = Seq<T>

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

fn index_logic(self, range: RangeTo<Int>) -> Self::Item

logic(open, inline)

self.subsequence(0, range.end)

type Item = Seq<T>

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

fn index_logic(self, range: RangeToInclusive<Int>) -> Self::Item

logic(open, inline)

self.subsequence(0, range.end + 1)

type Item = Seq<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

logic(open, prophetic, inline)

forall<i> 0 <= i && i < self.len() ==> inv(self.index_logic_unsized(i))

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

fn into_ghost(snap: Snapshot<Self>) -> Ghost<Self>

ensures

*result == *snap

terminates

ghost

impl<T> Resolve for Seq<T>

fn resolve(self) -> bool

logic(open, prophetic)

forall<i : Int> resolve(self.get(i))

fn resolve_coherence(self)

logic(open(pub(self)), prophetic)

requires

structural_resolve(self)

ensures

self.resolve()

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