Vector.md

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 vec. 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.

• Constants
• Function empty
• Function length
• Function borrow
• Function push_back
• Function borrow_mut
• Function pop_back
• Function destroy_empty
• Function spawn_from
• Function spawn_from_vec
• Function swap
• Function singleton
• Function reverse
• Function native_reverse
• Function append
• Function native_append
• Function is_empty
• Function contains
• Function index_of
• Function remove
• Function native_remove
• Function swap_remove
• Function split
• Module Specification
  • Helper Functions

Constants

The index into the vector is out of bounds

const EINDEX_OUT_OF_BOUNDS: u64 = 0;

Function empty

Create an empty vector.

public fun empty<Element>(): vector<Element>

Implementation

native public fun empty<Element>(): vector<Element>;

Function length

Return the length of the vector.

public fun length<Element>(v: &vector<Element>): u64

Implementation

native public fun length<Element>(v: &vector<Element>): u64;

Function borrow

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

public fun borrow<Element>(v: &vector<Element>, i: u64): &Element

Implementation

native public fun borrow<Element>(v: &vector<Element>, i: u64): ∈

Function push_back

Add element e to the end of the vector v.

public fun push_back<Element>(v: &mut vector<Element>, e: Element)

Implementation

native public fun push_back<Element>(v: &mut vector<Element>, e: Element);

Function borrow_mut

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

public fun borrow_mut<Element>(v: &mut vector<Element>, i: u64): &mut Element

Implementation

native public fun borrow_mut<Element>(v: &mut vector<Element>, i: u64): &mut Element;

Function pop_back

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

public fun pop_back<Element>(v: &mut vector<Element>): Element

Implementation

native public fun pop_back<Element>(v: &mut vector<Element>): Element;

Function destroy_empty

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

public fun destroy_empty<Element>(v: vector<Element>)

Implementation

native public fun destroy_empty<Element>(v: vector<Element>);

Function spawn_from

Spawn a sub vector from a vector

fun spawn_from<Element>(v: &vector<Element>, offset: u64, size: u64): vector<Element>

Implementation

native fun spawn_from<Element>(v: &vector<Element>, offset: u64, size: u64): vector<Element>;

Specification

pragma opaque;
ensures [abstract] result == v[offset..offset+size];

Function spawn_from_vec

public fun spawn_from_vec<Element: copy>(v: &vector<Element>, offset: u64, size: u64): vector<Element>

Implementation

public fun spawn_from_vec<Element: copy>(v: &vector<Element>, offset: u64, size: u64): vector<Element> {
    let len = length(v);
    let end_idx = (offset + size);
    assert!(end_idx <= len, EINDEX_OUT_OF_BOUNDS);
    assert!(size > 0, EINDEX_OUT_OF_BOUNDS);
    if (offset == 0 && end_idx == len) {
        return *v
    };
    spawn_from(v, offset, size)
}

Function swap

Swaps the elements at the ith and jth indices in the vector v. Aborts if ior j is out of bounds.

public fun swap<Element>(v: &mut vector<Element>, i: u64, j: u64)

Implementation

native public fun swap<Element>(v: &mut vector<Element>, i: u64, j: 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();
    push_back(&mut v, e);
    v
}

Specification

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

fun spec_singleton<Element>(e: Element): vector<Element> {
   vec(e)
}

Function reverse

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

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

Implementation

public fun reverse<Element>(v: &mut vector<Element>) {
    native_reverse(v)
}

Specification

pragma intrinsic = true;

Function native_reverse

fun native_reverse<Element>(this: &mut vector<Element>)

Implementation

native fun native_reverse<Element>(this: &mut vector<Element>);

Function append

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

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

Implementation

public fun append<Element>(lhs: &mut vector<Element>, other: vector<Element>) {
    native_append(lhs, other);
}

Specification

pragma intrinsic = true;

Function native_append

fun native_append<Element>(lhs: &mut vector<Element>, other: vector<Element>)

Implementation

native fun native_append<Element>(lhs: &mut vector<Element>, other: vector<Element>);

Function is_empty

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

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

Implementation

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

Specification

pragma intrinsic = true;

Function contains

Return true if e is in the vector v.

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

Implementation

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

Specification

pragma intrinsic = true;

Function index_of

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

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

Implementation

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

Specification

pragma intrinsic = true;

Function remove

Remove the ith element of the vector v, 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>(v: &mut vector<Element>, i: u64): Element

Implementation

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

    native_remove(v, i)
}

Specification

pragma intrinsic = true;

Function native_remove

fun native_remove<Element>(this: &mut vector<Element>, i: u64): Element

Implementation

native fun native_remove<Element>(this: &mut vector<Element>, i: u64): Element;

Function swap_remove

Swap the ith element of the vector v 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>(v: &mut vector<Element>, i: u64): Element

Implementation

public fun swap_remove<Element>(v: &mut vector<Element>, i: u64): Element {
    let last_idx = length(v) - 1;
    swap(v, i, last_idx);
    pop_back(v)
}

Specification

pragma intrinsic = true;

Function split

Split a vector into sub-vectors of size sub_len,

public fun split<Element: copy, drop, store>(v: &vector<Element>, sub_len: u64): vector<vector<Element>>

Implementation

public fun split<Element: copy + drop + store>(v: &vector<Element>, sub_len: u64): vector<vector<Element>> {
    let result = empty<vector<Element>>();
    let len = length(v) / sub_len;

    let rem = 0;
    if (len * sub_len < length(v)) {
        rem = length(v) - len * sub_len;
    };

    let i = 0;
    while (i < len) {
        let sub = empty<Element>();
        let j = 0;
        while (j < sub_len) {
            let index = sub_len * i + j;
            push_back(&mut sub, *borrow(v, index));
            j = j + 1;
        };
        push_back<vector<Element>>(&mut result, sub);
        i = i + 1;
    };

    if (rem > 0) {
        let sub = empty<Element>();
        let index = length(v) - rem;
        while (index < length(v)) {
            push_back(&mut sub, *borrow(v, index));
            index = index + 1;
        };
        push_back<vector<Element>>(&mut result, sub);
    };
    result
}

Specification

pragma verify = false;
aborts_if sub_len == 0;

Module Specification

Helper Functions

Check whether a vector contains an element.

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

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

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

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

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

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

fun eq_pop_front<Element>(v1: vector<Element>, v2: vector<Element>): bool {
   len(v1) + 1 == len(v2) &&
   v1 == 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)]
}