Skip to content

Latest commit

 

History

History
660 lines (337 loc) · 16 KB

Vector.md

File metadata and controls

660 lines (337 loc) · 16 KB
Raw

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.

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 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 == spec_singleton(e);


define spec_singleton<Element>(e: Element): vector<Element> {
    singleton_vector(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>) {
    let len = length(v);
    if (len == 0) return ();

    let front_index = 0;
    let back_index = len -1;
    while (front_index < back_index) {
        swap(v, front_index, back_index);
        front_index = front_index + 1;
        back_index = back_index - 1;
    }
}
Specification 
pragma intrinsic = true;

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>) {
    reverse(&mut other);
    while (!is_empty(&other)) push_back(lhs, pop_back(&mut other));
    destroy_empty(other);
}
Specification 
pragma intrinsic = true;

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;

    len = len - 1;
    while (i < len) swap(v, i, { i = i + 1; i });
    pop_back(v)
}
Specification 
pragma intrinsic = true;

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;

Module Specification

Helper Functions

Check whether a vector contains an element.

define 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

define 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

define 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

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