Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Module 0x1::vector

A variable-sized container that can hold any type. Indexing is 0-based, and vectors are growable. This module has many native functions. Verification of modules that use this one uses model functions that are implemented directly in Boogie. The specification language has built-in functions operations such as singleton_vector. There are some helper functions defined here for specifications in other modules as well.

Note: We did not verify most of the Move functions here because many have loops, requiring loop invariants to prove, and the return on investment didn’t seem worth it for these simple functions.

use 0x1::mem;

Constants

The index into the vector is out of bounds

const EINDEX_OUT_OF_BOUNDS: u64 = 131072;

The index into the vector is out of bounds

const EINVALID_RANGE: u64 = 131073;

The range in slice is invalid.

const EINVALID_SLICE_RANGE: u64 = 131076;

The step provided in range is invalid, must be greater than zero.

const EINVALID_STEP: u64 = 131075;

The length of the vectors are not equal.

const EVECTORS_LENGTH_MISMATCH: u64 = 131074;

Whether to utilize native vector::move_range Vector module cannot call features module, due to cyclic dependency, so this is a constant.

const USE_MOVE_RANGE: bool = true;

Function empty

Create an empty vector.

#[bytecode_instruction]
public fun empty<Element>(): vector<Element>
Implementation 
native public fun empty<Element>(): vector<Element>;

Function length

Return the length of the vector.

#[bytecode_instruction]
public fun length<Element>(self: &vector<Element>): u64
Implementation 
native public fun length<Element>(self: &vector<Element>): u64;

Function borrow

Acquire an immutable reference to the ith element of the vector self. Aborts if i is out of bounds.

#[bytecode_instruction]
public fun borrow<Element>(self: &vector<Element>, i: u64): &Element
Implementation 
native public fun borrow<Element>(self: &vector<Element>, i: u64): ∈

Function push_back

Add element e to the end of the vector self.

#[bytecode_instruction]
public fun push_back<Element>(self: &mut vector<Element>, e: Element)
Implementation 
native public fun push_back<Element>(self: &mut vector<Element>, e: Element);

Function borrow_mut

Return a mutable reference to the ith element in the vector self. Aborts if i is out of bounds.

#[bytecode_instruction]
public fun borrow_mut<Element>(self: &mut vector<Element>, i: u64): &mut Element
Implementation 
native public fun borrow_mut<Element>(self: &mut vector<Element>, i: u64): &mut Element;

Function pop_back

Pop an element from the end of vector self. Aborts if self is empty.

#[bytecode_instruction]
public fun pop_back<Element>(self: &mut vector<Element>): Element
Implementation 
native public fun pop_back<Element>(self: &mut vector<Element>): Element;

Function destroy_empty

Destroy the vector self. Aborts if self is not empty.

#[bytecode_instruction]
public fun destroy_empty<Element>(self: vector<Element>)
Implementation 
native public fun destroy_empty<Element>(self: vector<Element>);

Function swap

Swaps the elements at the ith and jth indices in the vector self. Aborts if i or j is out of bounds.

#[bytecode_instruction]
public fun swap<Element>(self: &mut vector<Element>, i: u64, j: u64)
Implementation 
native public fun swap<Element>(self: &mut vector<Element>, i: u64, j: u64);

Function move_range

Moves range of elements [removal_position, removal_position + length) from vector from, to vector to, inserting them starting at the insert_position. In the from vector, elements after the selected range are moved left to fill the hole (i.e. range is removed, while the order of the rest of the elements is kept) In the to vector, elements after the insert_position are moved to the right to make space for new elements (i.e. range is inserted, while the order of the rest of the elements is kept). Move prevents from having two mutable references to the same value, so from and to vectors are always distinct.

public fun move_range<T>(from: &mut vector<T>, removal_position: u64, length: u64, to: &mut vector<T>, insert_position: u64)
Implementation 
native public fun move_range<T>(
    from: &mut vector<T>,
    removal_position: u64,
    length: u64,
    to: &mut vector<T>,
    insert_position: u64
);

Function singleton

Return an vector of size one containing element e.

public fun singleton<Element>(e: Element): vector<Element>
Implementation 
public fun singleton<Element>(e: Element): vector<Element> {
    let v = empty();
    v.push_back(e);
    v
}

Function last

Returns a reference to last element in the vector, or aborts if the vector is empty.

public fun last<Element>(self: &vector<Element>): &Element
Implementation 
public fun last<Element>(self: &vector<Element>): &Element {
    assert!(self.length() > 0, EINDEX_OUT_OF_BOUNDS);

    &self[self.length() - 1]
}

Function last_mut

Returns a mutable reference to the last element in the vector, or aborts if the vector is empty.

public fun last_mut<Element>(self: &mut vector<Element>): &mut Element
Implementation 
public fun last_mut<Element>(self: &mut vector<Element>): &mut Element {
    assert!(self.length() > 0, EINDEX_OUT_OF_BOUNDS);
    let len = self.length();
    &mut self[len - 1]
}

Function reverse

Reverses the order of the elements in the vector self in place.

public fun reverse<Element>(self: &mut vector<Element>)
Implementation 
public fun reverse<Element>(self: &mut vector<Element>) {
    let len = self.length();
    self.reverse_slice(0, len);
}

Function reverse_slice

Reverses the order of the elements [left, right) in the vector self in place.

public fun reverse_slice<Element>(self: &mut vector<Element>, left: u64, right: u64)
Implementation 
public fun reverse_slice<Element>(self: &mut vector<Element>, left: u64, right: u64) {
    assert!(left <= right, EINVALID_RANGE);
    if (left == right) return;
    right -= 1;
    while (left < right) {
        self.swap(left, right);
        left += 1;
        right -= 1;
    }
}

Function append

Pushes all of the elements of the other vector into the self vector.

public fun append<Element>(self: &mut vector<Element>, other: vector<Element>)
Implementation 
public fun append<Element>(self: &mut vector<Element>, other: vector<Element>) {
    if (USE_MOVE_RANGE) {
        let self_length = self.length();
        let other_length = other.length();
        move_range(&mut other, 0, other_length, self, self_length);
        other.destroy_empty();
    } else {
        other.reverse();
        self.reverse_append(other);
    }
}

Function reverse_append

Pushes all of the elements of the other vector into the self vector.

public fun reverse_append<Element>(self: &mut vector<Element>, other: vector<Element>)
Implementation 
public fun reverse_append<Element>(self: &mut vector<Element>, other: vector<Element>) {
    let len = other.length();
    while (len > 0) {
        self.push_back(other.pop_back());
        len -= 1;
    };
    other.destroy_empty();
}

Function trim

Splits (trims) the collection into two at the given index. Returns a newly allocated vector containing the elements in the range [new_len, len). After the call, the original vector will be left containing the elements [0, new_len) with its previous capacity unchanged. In many languages this is also called split_off.

public fun trim<Element>(self: &mut vector<Element>, new_len: u64): vector<Element>
Implementation 
public fun trim<Element>(self: &mut vector<Element>, new_len: u64): vector<Element> {
    let len = self.length();
    assert!(new_len <= len, EINDEX_OUT_OF_BOUNDS);

    let other = empty();
    if (USE_MOVE_RANGE) {
        move_range(self, new_len, len - new_len, &mut other, 0);
    } else {
        while (len > new_len) {
            other.push_back(self.pop_back());
            len -= 1;
        };
        other.reverse();
    };

    other
}

Function trim_reverse

Trim a vector to a smaller size, returning the evicted elements in reverse order

public fun trim_reverse<Element>(self: &mut vector<Element>, new_len: u64): vector<Element>
Implementation 
public fun trim_reverse<Element>(self: &mut vector<Element>, new_len: u64): vector<Element> {
    let len = self.length();
    assert!(new_len <= len, EINDEX_OUT_OF_BOUNDS);
    let result = empty();
    while (new_len < len) {
        result.push_back(self.pop_back());
        len -= 1;
    };
    result
}

Function is_empty

Return true if the vector self has no elements and false otherwise.

public fun is_empty<Element>(self: &vector<Element>): bool
Implementation 
public fun is_empty<Element>(self: &vector<Element>): bool {
    self.length() == 0
}

Function contains

Return true if e is in the vector self.

public fun contains<Element>(self: &vector<Element>, e: &Element): bool
Implementation 
public fun contains<Element>(self: &vector<Element>, e: &Element): bool {
    let i = 0;
    let len = self.length();
    while (i < len) {
        if (self.borrow(i) == e) return true;
        i += 1;
    };
    false
}

Function index_of

Return (true, i) if e is in the vector self at index i. Otherwise, returns (false, 0).

public fun index_of<Element>(self: &vector<Element>, e: &Element): (bool, u64)
Implementation 
public fun index_of<Element>(self: &vector<Element>, e: &Element): (bool, u64) {
    let i = 0;
    let len = self.length();
    while (i < len) {
        if (self.borrow(i) == e) return (true, i);
        i += 1;
    };
    (false, 0)
}

Function find

Return (true, i) if there’s an element that matches the predicate. If there are multiple elements that match the predicate, only the index of the first one is returned. Otherwise, returns (false, 0).

public fun find<Element>(self: &vector<Element>, f: |&Element|bool): (bool, u64)
Implementation 
public inline fun find<Element>(self: &vector<Element>, f: |&Element|bool): (bool, u64) {
    let find = false;
    let found_index = 0;
    let i = 0;
    let len = self.length();
    while ({
        spec {
            invariant i <= len;
            invariant forall j: num where j >= 0 && j < i: !f(self[j]);
            invariant find ==> i < len && f(self[i]);
        };
        i < len
        }) {
        // Cannot call return in an inline function so we need to resort to break here.
        if (f(self.borrow(i))) {
            find = true;
            found_index = i;
            break
        };
        i += 1;
    };
    spec {
        assert !find <==> (forall j: num where j >= 0 && j < len: !f(self[j]));
    };
    (find, found_index)
}

Function insert

Insert a new element at position 0 <= i <= length, using O(length - i) time. Aborts if out of bounds.

public fun insert<Element>(self: &mut vector<Element>, i: u64, e: Element)
Implementation 
public fun insert<Element>(self: &mut vector<Element>, i: u64, e: Element) {
    let len = self.length();
    assert!(i <= len, EINDEX_OUT_OF_BOUNDS);

    if (USE_MOVE_RANGE) {
        if (i + 2 >= len) {
            // When we are close to the end, it is cheaper to not create
            // a temporary vector, and swap directly
            self.push_back(e);
            while (i < len) {
                self.swap(i, len);
                i += 1;
            };
        } else {
            let other = singleton(e);
            move_range(&mut other, 0, 1, self, i);
            other.destroy_empty();
        }
    } else {
        self.push_back(e);
        while (i < len) {
            self.swap(i, len);
            i += 1;
        };
    };
}

Function remove

Remove the ith element of the vector self, shifting all subsequent elements. This is O(n) and preserves ordering of elements in the vector. Aborts if i is out of bounds.

public fun remove<Element>(self: &mut vector<Element>, i: u64): Element
Implementation 
public fun remove<Element>(self: &mut vector<Element>, i: u64): Element {
    let len = self.length();
    // i out of bounds; abort
    if (i >= len) abort EINDEX_OUT_OF_BOUNDS;

    if (USE_MOVE_RANGE) {
        // When we are close to the end, it is cheaper to not create
        // a temporary vector, and swap directly
        if (i + 3 >= len) {
            len -= 1;
            while (i < len) self.swap(i, { i += 1; i });
            self.pop_back()
        } else {
            let other = empty();
            move_range(self, i, 1, &mut other, 0);
            let result = other.pop_back();
            other.destroy_empty();
            result
        }
    } else {
        len -= 1;
        while (i < len) self.swap(i, { i += 1; i });
        self.pop_back()
    }
}

Function remove_value

Remove the first occurrence of a given value in the vector self and return it in a vector, shifting all subsequent elements. This is O(n) and preserves ordering of elements in the vector. This returns an empty vector if the value isn’t present in the vector. Note that this cannot return an option as option uses vector and there’d be a circular dependency between option and vector.

public fun remove_value<Element>(self: &mut vector<Element>, val: &Element): vector<Element>
Implementation 
public fun remove_value<Element>(self: &mut vector<Element>, val: &Element): vector<Element> {
    // This doesn't cost a O(2N) run time as index_of scans from left to right and stops when the element is found,
    // while remove would continue from the identified index to the end of the vector.
    let (found, index) = self.index_of(val);
    if (found) {
        vector[self.remove(index)]
    } else {
       vector[]
    }
}

Function swap_remove

Swap the ith element of the vector self with the last element and then pop the vector. This is O(1), but does not preserve ordering of elements in the vector. Aborts if i is out of bounds.

public fun swap_remove<Element>(self: &mut vector<Element>, i: u64): Element
Implementation 
public fun swap_remove<Element>(self: &mut vector<Element>, i: u64): Element {
    assert!(!self.is_empty(), EINDEX_OUT_OF_BOUNDS);
    let last_idx = self.length() - 1;
    self.swap(i, last_idx);
    self.pop_back()
}

Function replace

Replace the ith element of the vector self with the given value, and return to the caller the value that was there before. Aborts if i is out of bounds.

public fun replace<Element>(self: &mut vector<Element>, i: u64, val: Element): Element
Implementation 
public fun replace<Element>(self: &mut vector<Element>, i: u64, val: Element): Element {
    let last_idx = self.length();
    assert!(i < last_idx, EINDEX_OUT_OF_BOUNDS);
    if (USE_MOVE_RANGE) {
        mem::replace(self.borrow_mut(i), val)
    } else {
        self.push_back(val);
        self.swap(i, last_idx);
        self.pop_back()
    }
}

Function for_each

Apply the function to each element in the vector, consuming it.

public fun for_each<Element>(self: vector<Element>, f: |Element|)
Implementation 
public inline fun for_each<Element>(self: vector<Element>, f: |Element|) {
    self.reverse(); // We need to reverse the vector to consume it efficiently
    self.for_each_reverse(|e| f(e));
}

Function for_each_reverse

Apply the function to each element in the vector, consuming it.

public fun for_each_reverse<Element>(self: vector<Element>, f: |Element|)
Implementation 
public inline fun for_each_reverse<Element>(self: vector<Element>, f: |Element|) {
    let len = self.length();
    while (len > 0) {
        f(self.pop_back());
        len -= 1;
    };
    self.destroy_empty()
}

Function for_each_ref

Apply the function to a reference of each element in the vector.

public fun for_each_ref<Element>(self: &vector<Element>, f: |&Element|)
Implementation 
public inline fun for_each_ref<Element>(self: &vector<Element>, f: |&Element|) {
    let i = 0;
    let len = self.length();
    while (i < len) {
        f(self.borrow(i));
        i += 1
    }
}

Function zip

Apply the function to each pair of elements in the two given vectors, consuming them.

public fun zip<Element1, Element2>(self: vector<Element1>, v2: vector<Element2>, f: |Element1, Element2|)
Implementation 
public inline fun zip<Element1, Element2>(self: vector<Element1>, v2: vector<Element2>, f: |Element1, Element2|) {
    // We need to reverse the vectors to consume it efficiently
    self.reverse();
    v2.reverse();
    self.zip_reverse(v2, |e1, e2| f(e1, e2));
}

Function zip_reverse

Apply the function to each pair of elements in the two given vectors in the reverse order, consuming them. This errors out if the vectors are not of the same length.

public fun zip_reverse<Element1, Element2>(self: vector<Element1>, v2: vector<Element2>, f: |Element1, Element2|)
Implementation 
public inline fun zip_reverse<Element1, Element2>(
    self: vector<Element1>,
    v2: vector<Element2>,
    f: |Element1, Element2|,
) {
    let len = self.length();
    // We can't use the constant EVECTORS_LENGTH_MISMATCH here as all calling code would then need to define it
    // due to how inline functions work.
    assert!(len == v2.length(), 0x20002);
    while (len > 0) {
        f(self.pop_back(), v2.pop_back());
        len -= 1;
    };
    self.destroy_empty();
    v2.destroy_empty();
}

Function zip_ref

Apply the function to the references of each pair of elements in the two given vectors. This errors out if the vectors are not of the same length.

public fun zip_ref<Element1, Element2>(self: &vector<Element1>, v2: &vector<Element2>, f: |&Element1, &Element2|)
Implementation 
public inline fun zip_ref<Element1, Element2>(
    self: &vector<Element1>,
    v2: &vector<Element2>,
    f: |&Element1, &Element2|,
) {
    let len = self.length();
    // We can't use the constant EVECTORS_LENGTH_MISMATCH here as all calling code would then need to define it
    // due to how inline functions work.
    assert!(len == v2.length(), 0x20002);
    let i = 0;
    while (i < len) {
        f(self.borrow(i), v2.borrow(i));
        i += 1
    }
}

Function enumerate_ref

Apply the function to a reference of each element in the vector with its index.

public fun enumerate_ref<Element>(self: &vector<Element>, f: |u64, &Element|)
Implementation 
public inline fun enumerate_ref<Element>(self: &vector<Element>, f: |u64, &Element|) {
    let i = 0;
    let len = self.length();
    while (i < len) {
        f(i, self.borrow(i));
        i += 1;
    };
}

Function for_each_mut

Apply the function to a mutable reference to each element in the vector.

public fun for_each_mut<Element>(self: &mut vector<Element>, f: |&mut Element|)
Implementation 
public inline fun for_each_mut<Element>(self: &mut vector<Element>, f: |&mut Element|) {
    let i = 0;
    let len = self.length();
    while (i < len) {
        f(self.borrow_mut(i));
        i += 1
    }
}

Function zip_mut

Apply the function to mutable references to each pair of elements in the two given vectors. This errors out if the vectors are not of the same length.

public fun zip_mut<Element1, Element2>(self: &mut vector<Element1>, v2: &mut vector<Element2>, f: |&mut Element1, &mut Element2|)
Implementation 
public inline fun zip_mut<Element1, Element2>(
    self: &mut vector<Element1>,
    v2: &mut vector<Element2>,
    f: |&mut Element1, &mut Element2|,
) {
    let i = 0;
    let len = self.length();
    // We can't use the constant EVECTORS_LENGTH_MISMATCH here as all calling code would then need to define it
    // due to how inline functions work.
    assert!(len == v2.length(), 0x20002);
    while (i < len) {
        f(self.borrow_mut(i), v2.borrow_mut(i));
        i += 1
    }
}

Function enumerate_mut

Apply the function to a mutable reference of each element in the vector with its index.

public fun enumerate_mut<Element>(self: &mut vector<Element>, f: |u64, &mut Element|)
Implementation 
public inline fun enumerate_mut<Element>(self: &mut vector<Element>, f: |u64, &mut Element|) {
    let i = 0;
    let len = self.length();
    while (i < len) {
        f(i, self.borrow_mut(i));
        i += 1;
    };
}

Function fold

Fold the function over the elements. For example, fold(vector[1,2,3], 0, f) will execute f(f(f(0, 1), 2), 3)

public fun fold<Accumulator, Element>(self: vector<Element>, init: Accumulator, f: |Accumulator, Element|Accumulator): Accumulator
Implementation 
public inline fun fold<Accumulator, Element>(
    self: vector<Element>,
    init: Accumulator,
    f: |Accumulator,Element|Accumulator
): Accumulator {
    let accu = init;
    self.for_each(|elem| accu = f(accu, elem));
    accu
}

Function foldr

Fold right like fold above but working right to left. For example, fold(vector[1,2,3], 0, f) will execute f(1, f(2, f(3, 0)))

public fun foldr<Accumulator, Element>(self: vector<Element>, init: Accumulator, f: |Element, Accumulator|Accumulator): Accumulator
Implementation 
public inline fun foldr<Accumulator, Element>(
    self: vector<Element>,
    init: Accumulator,
    f: |Element, Accumulator|Accumulator
): Accumulator {
    let accu = init;
    self.for_each_reverse(|elem| accu = f(elem, accu));
    accu
}

Function map_ref

Map the function over the references of the elements of the vector, producing a new vector without modifying the original vector.

public fun map_ref<Element, NewElement>(self: &vector<Element>, f: |&Element|NewElement): vector<NewElement>
Implementation 
public inline fun map_ref<Element, NewElement>(
    self: &vector<Element>,
    f: |&Element|NewElement
): vector<NewElement> {
    let result = vector<NewElement>[];
    self.for_each_ref(|elem| result.push_back(f(elem)));
    result
}

Function zip_map_ref

Map the function over the references of the element pairs of two vectors, producing a new vector from the return values without modifying the original vectors.

public fun zip_map_ref<Element1, Element2, NewElement>(self: &vector<Element1>, v2: &vector<Element2>, f: |&Element1, &Element2|NewElement): vector<NewElement>
Implementation 
public inline fun zip_map_ref<Element1, Element2, NewElement>(
    self: &vector<Element1>,
    v2: &vector<Element2>,
    f: |&Element1, &Element2|NewElement
): vector<NewElement> {
    // We can't use the constant EVECTORS_LENGTH_MISMATCH here as all calling code would then need to define it
    // due to how inline functions work.
    assert!(self.length() == v2.length(), 0x20002);

    let result = vector<NewElement>[];
    self.zip_ref(v2, |e1, e2| result.push_back(f(e1, e2)));
    result
}

Function map

Map the function over the elements of the vector, producing a new vector.

public fun map<Element, NewElement>(self: vector<Element>, f: |Element|NewElement): vector<NewElement>
Implementation 
public inline fun map<Element, NewElement>(
    self: vector<Element>,
    f: |Element|NewElement
): vector<NewElement> {
    let result = vector<NewElement>[];
    self.for_each(|elem| result.push_back(f(elem)));
    result
}

Function zip_map

Map the function over the element pairs of the two vectors, producing a new vector.

public fun zip_map<Element1, Element2, NewElement>(self: vector<Element1>, v2: vector<Element2>, f: |Element1, Element2|NewElement): vector<NewElement>
Implementation 
public inline fun zip_map<Element1, Element2, NewElement>(
    self: vector<Element1>,
    v2: vector<Element2>,
    f: |Element1, Element2|NewElement
): vector<NewElement> {
    // We can't use the constant EVECTORS_LENGTH_MISMATCH here as all calling code would then need to define it
    // due to how inline functions work.
    assert!(self.length() == v2.length(), 0x20002);

    let result = vector<NewElement>[];
    self.zip(v2, |e1, e2| result.push_back(f(e1, e2)));
    result
}

Function filter

Filter the vector using the boolean function, removing all elements for which p(e) is not true.

public fun filter<Element: drop>(self: vector<Element>, p: |&Element|bool): vector<Element>
Implementation 
public inline fun filter<Element:drop>(
    self: vector<Element>,
    p: |&Element|bool
): vector<Element> {
    let result = vector<Element>[];
    self.for_each(|elem| {
        if (p(&elem)) result.push_back(elem);
    });
    result
}

Function partition

Partition, sorts all elements for which pred is true to the front. Preserves the relative order of the elements for which pred is true, BUT NOT for the elements for which pred is false.

public fun partition<Element>(self: &mut vector<Element>, pred: |&Element|bool): u64
Implementation 
public inline fun partition<Element>(
    self: &mut vector<Element>,
    pred: |&Element|bool
): u64 {
    let i = 0;
    let len = self.length();
    while (i < len) {
        if (!pred(self.borrow(i))) break;
        i += 1;
    };
    let p = i;
    i += 1;
    while (i < len) {
        if (pred(self.borrow(i))) {
            self.swap(p, i);
            p += 1;
        };
        i += 1;
    };
    p
}

Function rotate

rotate(&mut [1, 2, 3, 4, 5], 2) -> [3, 4, 5, 1, 2] in place, returns the split point ie. 3 in the example above

public fun rotate<Element>(self: &mut vector<Element>, rot: u64): u64
Implementation 
public fun rotate<Element>(
    self: &mut vector<Element>,
    rot: u64
): u64 {
    let len = self.length();
    self.rotate_slice(0, rot, len)
}

Function rotate_slice

Same as above but on a sub-slice of an array [left, right) with left <= rot <= right returns the

public fun rotate_slice<Element>(self: &mut vector<Element>, left: u64, rot: u64, right: u64): u64
Implementation 
public fun rotate_slice<Element>(
    self: &mut vector<Element>,
    left: u64,
    rot: u64,
    right: u64
): u64 {
    self.reverse_slice(left, rot);
    self.reverse_slice(rot, right);
    self.reverse_slice(left, right);
    left + (right - rot)
}

Function stable_partition

Partition the array based on a predicate p, this routine is stable and thus preserves the relative order of the elements in the two partitions.

public fun stable_partition<Element>(self: &mut vector<Element>, p: |&Element|bool): u64
Implementation 
public inline fun stable_partition<Element>(
    self: &mut vector<Element>,
    p: |&Element|bool
): u64 {
    let len = self.length();
    let t = empty();
    let f = empty();
    while (len > 0) {
        let e = self.pop_back();
        if (p(&e)) {
            t.push_back(e);
        } else {
            f.push_back(e);
        };
        len -= 1;
    };
    let pos = t.length();
    self.reverse_append(t);
    self.reverse_append(f);
    pos
}

Function any

Return true if any element in the vector satisfies the predicate.

public fun any<Element>(self: &vector<Element>, p: |&Element|bool): bool
Implementation 
public inline fun any<Element>(
    self: &vector<Element>,
    p: |&Element|bool
): bool {
    let result = false;
    let i = 0;
    while (i < self.length()) {
        result = p(self.borrow(i));
        if (result) {
            break
        };
        i += 1
    };
    result
}

Function all

Return true if all elements in the vector satisfy the predicate.

public fun all<Element>(self: &vector<Element>, p: |&Element|bool): bool
Implementation 
public inline fun all<Element>(
    self: &vector<Element>,
    p: |&Element|bool
): bool {
    let result = true;
    let i = 0;
    while (i < self.length()) {
        result = p(self.borrow(i));
        if (!result) {
            break
        };
        i += 1
    };
    result
}

Function destroy

Destroy a vector, just a wrapper around for_each_reverse with a descriptive name when used in the context of destroying a vector.

public fun destroy<Element>(self: vector<Element>, d: |Element|)
Implementation 
public inline fun destroy<Element>(
    self: vector<Element>,
    d: |Element|
) {
    self.for_each_reverse(|e| d(e))
}

Function range 

public fun range(start: u64, end: u64): vector<u64>
Implementation 
public fun range(start: u64, end: u64): vector<u64> {
    range_with_step(start, end, 1)
}

Function range_with_step 

public fun range_with_step(start: u64, end: u64, step: u64): vector<u64>
Implementation 
public fun range_with_step(start: u64, end: u64, step: u64): vector<u64> {
    assert!(step > 0, EINVALID_STEP);

    let vec = vector[];
    while (start < end) {
        vec.push_back(start);
        start += step;
    };
    vec
}

Function slice 

public fun slice<Element: copy>(self: &vector<Element>, start: u64, end: u64): vector<Element>
Implementation 
public fun slice<Element: copy>(
    self: &vector<Element>,
    start: u64,
    end: u64
): vector<Element> {
    assert!(start <= end && end <= self.length(), EINVALID_SLICE_RANGE);

    let vec = vector[];
    while (start < end) {
        vec.push_back(self[start]);
        start += 1;
    };
    vec
}

Specification

Helper Functions

Check if self is equal to the result of adding e at the end of v2

fun eq_push_back<Element>(self: vector<Element>, v2: vector<Element>, e: Element): bool {
    len(self) == len(v2) + 1 &&
    self[len(self)-1] == e &&
    self[0..len(self)-1] == v2[0..len(v2)]
}

Check if self is equal to the result of concatenating v1 and v2

fun eq_append<Element>(self: vector<Element>, v1: vector<Element>, v2: vector<Element>): bool {
    len(self) == len(v1) + len(v2) &&
    self[0..len(v1)] == v1 &&
    self[len(v1)..len(self)] == v2
}

Check self is equal to the result of removing the first element of v2

fun eq_pop_front<Element>(self: vector<Element>, v2: vector<Element>): bool {
    len(self) + 1 == len(v2) &&
    self == v2[1..len(v2)]
}

Check that v1 is equal to the result of removing the element at index i from v2.

fun eq_remove_elem_at_index<Element>(i: u64, v1: vector<Element>, v2: vector<Element>): bool {
    len(v1) + 1 == len(v2) &&
    v1[0..i] == v2[0..i] &&
    v1[i..len(v1)] == v2[i + 1..len(v2)]
}

Check if self contains e.

fun spec_contains<Element>(self: vector<Element>, e: Element): bool {
    exists x in self: x == e
}

Function singleton 

public fun singleton<Element>(e: Element): vector<Element>

aborts_if false;
ensures result == vec(e);

Function reverse 

public fun reverse<Element>(self: &mut vector<Element>)

pragma intrinsic = true;

Function reverse_slice 

public fun reverse_slice<Element>(self: &mut vector<Element>, left: u64, right: u64)

pragma intrinsic = true;

Function append 

public fun append<Element>(self: &mut vector<Element>, other: vector<Element>)

pragma intrinsic = true;

Function reverse_append 

public fun reverse_append<Element>(self: &mut vector<Element>, other: vector<Element>)

pragma intrinsic = true;

Function trim 

public fun trim<Element>(self: &mut vector<Element>, new_len: u64): vector<Element>

pragma intrinsic = true;

Function trim_reverse 

public fun trim_reverse<Element>(self: &mut vector<Element>, new_len: u64): vector<Element>

pragma intrinsic = true;

Function is_empty 

public fun is_empty<Element>(self: &vector<Element>): bool

pragma intrinsic = true;

Function contains 

public fun contains<Element>(self: &vector<Element>, e: &Element): bool

pragma intrinsic = true;

Function index_of 

public fun index_of<Element>(self: &vector<Element>, e: &Element): (bool, u64)

pragma intrinsic = true;

Function insert 

public fun insert<Element>(self: &mut vector<Element>, i: u64, e: Element)

pragma intrinsic = true;

Function remove 

public fun remove<Element>(self: &mut vector<Element>, i: u64): Element

pragma intrinsic = true;

Function remove_value 

public fun remove_value<Element>(self: &mut vector<Element>, val: &Element): vector<Element>

pragma intrinsic = true;

Function swap_remove 

public fun swap_remove<Element>(self: &mut vector<Element>, i: u64): Element

pragma intrinsic = true;

Function rotate 

public fun rotate<Element>(self: &mut vector<Element>, rot: u64): u64

pragma intrinsic = true;

Function rotate_slice 

public fun rotate_slice<Element>(self: &mut vector<Element>, left: u64, rot: u64, right: u64): u64

pragma intrinsic = true;