Skip to content

Latest commit

 

History

History
768 lines (373 loc) · 25.4 KB

vector.md

File metadata and controls

768 lines (373 loc) · 25.4 KB

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

Function empty

Create an empty vector.

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

Function length

Return the length of the vector.

#[bytecode_instruction]
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.

#[bytecode_instruction]
public fun borrow<Element>(v: &vector<Element>, i: u64): &Element

Function push_back

Add element e to the end of the vector v.

#[bytecode_instruction]
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.

#[bytecode_instruction]
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.

#[bytecode_instruction]
public fun pop_back<Element>(v: &mut vector<Element>): Element

Function destroy_empty

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

#[bytecode_instruction]
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 i or j is out of bounds.

#[bytecode_instruction]
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>

Function reverse

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

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

Function reverse_slice

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

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

Function append

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

Function reverse_append

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

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

Function trim

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

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

Function trim_reverse

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

public fun trim_reverse<Element>(v: &mut vector<Element>, new_len: u64): 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

Function contains

Return true if e is in the vector v.

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

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)

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>(v: &vector<Element>, f: |&Element|bool): (bool, u64)

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>(v: &mut vector<Element>, i: u64, e: Element)

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

Function remove_value

Remove the first occurrence of a given value in the vector v 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>(v: &mut vector<Element>, val: &Element): vector<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

Function for_each

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

public fun for_each<Element>(v: vector<Element>, f: |Element|())

Function for_each_reverse

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

public fun for_each_reverse<Element>(v: vector<Element>, f: |Element|())

Function for_each_ref

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

public fun for_each_ref<Element>(v: &vector<Element>, f: |&Element|())

Function zip

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

public fun zip<Element1, Element2>(v1: vector<Element1>, v2: vector<Element2>, f: |(Element1, Element2)|())

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>(v1: vector<Element1>, v2: vector<Element2>, f: |(Element1, Element2)|())

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>(v1: &vector<Element1>, v2: &vector<Element2>, f: |(&Element1, &Element2)|())

Function enumerate_ref

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

public fun enumerate_ref<Element>(v: &vector<Element>, f: |(u64, &Element)|())

Function for_each_mut

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

public fun for_each_mut<Element>(v: &mut vector<Element>, f: |&mut Element|())

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>(v1: &mut vector<Element1>, v2: &mut vector<Element2>, f: |(&mut Element1, &mut Element2)|())

Function enumerate_mut

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

public fun enumerate_mut<Element>(v: &mut vector<Element>, f: |(u64, &mut Element)|())

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>(v: vector<Element>, init: Accumulator, f: |(Accumulator, Element)|Accumulator): Accumulator

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>(v: vector<Element>, init: Accumulator, f: |(Element, Accumulator)|Accumulator): Accumulator

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>(v: &vector<Element>, f: |&Element|NewElement): vector<NewElement>

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>(v1: &vector<Element1>, v2: &vector<Element2>, f: |(&Element1, &Element2)|NewElement): vector<NewElement>

Function map

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

public fun map<Element, NewElement>(v: vector<Element>, f: |Element|NewElement): vector<NewElement>

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>(v1: vector<Element1>, v2: vector<Element2>, f: |(Element1, Element2)|NewElement): vector<NewElement>

Function filter

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

public fun filter<Element: drop>(v: vector<Element>, p: |&Element|bool): vector<Element>

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>(v: &mut vector<Element>, pred: |&Element|bool): u64

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>(v: &mut vector<Element>, rot: u64): u64

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>(v: &mut vector<Element>, left: u64, rot: u64, right: u64): u64

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>(v: &mut vector<Element>, p: |&Element|bool): u64

Function any

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

public fun any<Element>(v: &vector<Element>, p: |&Element|bool): bool

Function all

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

public fun all<Element>(v: &vector<Element>, p: |&Element|bool): bool

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>(v: vector<Element>, d: |Element|())

Function range

public fun range(start: u64, end: u64): vector<u64>

Function range_with_step

public fun range_with_step(start: u64, end: u64, step: u64): vector<u64>

Function slice

public fun slice<Element: copy>(self: &vector<Element>, start: u64, end: u64): vector<Element>

Module Specification