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 <code>singleton_vector</code>. 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 swap
Function singleton
Function reverse
Function append
Function is_empty
Function contains
Function index_of
Function remove
Function swap_remove
Module Specification
- Helper Functions

Constants

The index into the vector is out of bounds

<pre><code>const <a href="Vector.md#0x1_Vector_EINDEX_OUT_OF_BOUNDS">EINDEX_OUT_OF_BOUNDS</a>: u64 = 0; </code></pre>

Function `empty`

Create an empty vector.

<pre><code>public fun <a href="Vector.md#0x1_Vector_empty">empty</a><Element>(): vector<Element> </code></pre> <details> <summary>Implementation</summary> <pre><code>native public fun <a href="Vector.md#0x1_Vector_empty">empty</a><Element>(): vector<Element>; </code></pre> </details>

Function `length`

Return the length of the vector.

<pre><code>public fun <a href="Vector.md#0x1_Vector_length">length</a><Element>(v: &vector<Element>): u64 </code></pre> <details> <summary>Implementation</summary> <pre><code>native public fun <a href="Vector.md#0x1_Vector_length">length</a><Element>(v: &vector<Element>): u64; </code></pre> </details>

Function `borrow`

Acquire an immutable reference to the <code>i</code>th element of the vector <code>v</code>. Aborts if <code>i</code> is out of bounds.

<pre><code>public fun <a href="Vector.md#0x1_Vector_borrow">borrow</a><Element>(v: &vector<Element>, i: u64): &Element </code></pre> <details> <summary>Implementation</summary> <pre><code>native public fun <a href="Vector.md#0x1_Vector_borrow">borrow</a><Element>(v: &vector<Element>, i: u64): &Element; </code></pre> </details>

Function `push_back`

Add element <code>e</code> to the end of the vector <code>v</code>.

<pre><code>public fun <a href="Vector.md#0x1_Vector_push_back">push_back</a><Element>(v: &mut vector<Element>, e: Element) </code></pre> <details> <summary>Implementation</summary> <pre><code>native public fun <a href="Vector.md#0x1_Vector_push_back">push_back</a><Element>(v: &mut vector<Element>, e: Element); </code></pre> </details>

Function `borrow_mut`

Return a mutable reference to the <code>i</code>th element in the vector <code>v</code>. Aborts if <code>i</code> is out of bounds.

<pre><code>public fun <a href="Vector.md#0x1_Vector_borrow_mut">borrow_mut</a><Element>(v: &mut vector<Element>, i: u64): &mut Element </code></pre> <details> <summary>Implementation</summary> <pre><code>native public fun <a href="Vector.md#0x1_Vector_borrow_mut">borrow_mut</a><Element>(v: &mut vector<Element>, i: u64): &mut Element; </code></pre> </details>

Function `pop_back`

Pop an element from the end of vector <code>v</code>. Aborts if <code>v</code> is empty.

<pre><code>public fun <a href="Vector.md#0x1_Vector_pop_back">pop_back</a><Element>(v: &mut vector<Element>): Element </code></pre> <details> <summary>Implementation</summary> <pre><code>native public fun <a href="Vector.md#0x1_Vector_pop_back">pop_back</a><Element>(v: &mut vector<Element>): Element; </code></pre> </details>

Function `destroy_empty`

Destroy the vector <code>v</code>. Aborts if <code>v</code> is not empty.

<pre><code>public fun <a href="Vector.md#0x1_Vector_destroy_empty">destroy_empty</a><Element>(v: vector<Element>) </code></pre> <details> <summary>Implementation</summary> <pre><code>native public fun <a href="Vector.md#0x1_Vector_destroy_empty">destroy_empty</a><Element>(v: vector<Element>); </code></pre> </details>

Function `swap`

Swaps the elements at the <code>i</code>th and <code>j</code>th indices in the vector <code>v</code>. Aborts if <code>i</code>or <code>j</code> is out of bounds.

<pre><code>public fun <a href="Vector.md#0x1_Vector_swap">swap</a><Element>(v: &mut vector<Element>, i: u64, j: u64) </code></pre> <details> <summary>Implementation</summary> <pre><code>native public fun <a href="Vector.md#0x1_Vector_swap">swap</a><Element>(v: &mut vector<Element>, i: u64, j: u64); </code></pre> </details>

Function `singleton`

Return an vector of size one containing element <code>e</code>.

<pre><code>public fun <a href="Vector.md#0x1_Vector_singleton">singleton</a><Element>(e: Element): vector<Element> </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="Vector.md#0x1_Vector_singleton">singleton</a><Element>(e: Element): vector<Element> { let v = <a href="Vector.md#0x1_Vector_empty">empty</a>(); <a href="Vector.md#0x1_Vector_push_back">push_back</a>(&mut v, e); v } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>aborts_if false; ensures result == vec(e); </code></pre> </details>

Function `reverse`

Reverses the order of the elements in the vector <code>v</code> in place.

<pre><code>public fun <a href="Vector.md#0x1_Vector_reverse">reverse</a><Element>(v: &mut vector<Element>) </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="Vector.md#0x1_Vector_reverse">reverse</a><Element>(v: &mut vector<Element>) { let len = <a href="Vector.md#0x1_Vector_length">length</a>(v); if (len == 0) return (); let front_index = 0; let back_index = len -1; while (front_index < back_index) { <a href="Vector.md#0x1_Vector_swap">swap</a>(v, front_index, back_index); front_index = front_index + 1; back_index = back_index - 1; } } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>pragma intrinsic = true; </code></pre> </details>

Function `append`

Pushes all of the elements of the <code>other</code> vector into the <code>lhs</code> vector.

<pre><code>public fun <a href="Vector.md#0x1_Vector_append">append</a><Element>(lhs: &mut vector<Element>, other: vector<Element>) </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="Vector.md#0x1_Vector_append">append</a><Element>(lhs: &mut vector<Element>, other: vector<Element>) { <a href="Vector.md#0x1_Vector_reverse">reverse</a>(&mut other); while (!<a href="Vector.md#0x1_Vector_is_empty">is_empty</a>(&other)) <a href="Vector.md#0x1_Vector_push_back">push_back</a>(lhs, <a href="Vector.md#0x1_Vector_pop_back">pop_back</a>(&mut other)); <a href="Vector.md#0x1_Vector_destroy_empty">destroy_empty</a>(other); } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>pragma intrinsic = true; </code></pre> </details>

Function `is_empty`

Return <code>true</code> if the vector <code>v</code> has no elements and <code>false</code> otherwise.

<pre><code>public fun <a href="Vector.md#0x1_Vector_is_empty">is_empty</a><Element>(v: &vector<Element>): bool </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="Vector.md#0x1_Vector_is_empty">is_empty</a><Element>(v: &vector<Element>): bool { <a href="Vector.md#0x1_Vector_length">length</a>(v) == 0 } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>pragma intrinsic = true; </code></pre> </details>

Function `contains`

Return true if <code>e</code> is in the vector <code>v</code>.

<pre><code>public fun <a href="Vector.md#0x1_Vector_contains">contains</a><Element>(v: &vector<Element>, e: &Element): bool </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="Vector.md#0x1_Vector_contains">contains</a><Element>(v: &vector<Element>, e: &Element): bool { let i = 0; let len = <a href="Vector.md#0x1_Vector_length">length</a>(v); while (i < len) { if (<a href="Vector.md#0x1_Vector_borrow">borrow</a>(v, i) == e) return true; i = i + 1; }; false } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>pragma intrinsic = true; </code></pre> </details>

Function `index_of`

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

<pre><code>public fun <a href="Vector.md#0x1_Vector_index_of">index_of</a><Element>(v: &vector<Element>, e: &Element): (bool, u64) </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="Vector.md#0x1_Vector_index_of">index_of</a><Element>(v: &vector<Element>, e: &Element): (bool, u64) { let i = 0; let len = <a href="Vector.md#0x1_Vector_length">length</a>(v); while (i < len) { if (<a href="Vector.md#0x1_Vector_borrow">borrow</a>(v, i) == e) return (true, i); i = i + 1; }; (false, 0) } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>pragma intrinsic = true; </code></pre> </details>

Function `remove`

Remove the <code>i</code>th element of the vector <code>v</code>, shifting all subsequent elements. This is O(n) and preserves ordering of elements in the vector. Aborts if <code>i</code> is out of bounds.

<pre><code>public fun <a href="Vector.md#0x1_Vector_remove">remove</a><Element>(v: &mut vector<Element>, i: u64): Element </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="Vector.md#0x1_Vector_remove">remove</a><Element>(v: &mut vector<Element>, i: u64): Element { let len = <a href="Vector.md#0x1_Vector_length">length</a>(v); // i out of bounds; abort if (i >= len) abort <a href="Vector.md#0x1_Vector_EINDEX_OUT_OF_BOUNDS">EINDEX_OUT_OF_BOUNDS</a>; len = len - 1; while (i < len) <a href="Vector.md#0x1_Vector_swap">swap</a>(v, i, { i = i + 1; i }); <a href="Vector.md#0x1_Vector_pop_back">pop_back</a>(v) } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>pragma intrinsic = true; </code></pre> </details>

Function `swap_remove`

Swap the <code>i</code>th element of the vector <code>v</code> 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 <code>i</code> is out of bounds.

<pre><code>public fun <a href="Vector.md#0x1_Vector_swap_remove">swap_remove</a><Element>(v: &mut vector<Element>, i: u64): Element </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="Vector.md#0x1_Vector_swap_remove">swap_remove</a><Element>(v: &mut vector<Element>, i: u64): Element { assert(!<a href="Vector.md#0x1_Vector_is_empty">is_empty</a>(v), <a href="Vector.md#0x1_Vector_EINDEX_OUT_OF_BOUNDS">EINDEX_OUT_OF_BOUNDS</a>); let last_idx = <a href="Vector.md#0x1_Vector_length">length</a>(v) - 1; <a href="Vector.md#0x1_Vector_swap">swap</a>(v, i, last_idx); <a href="Vector.md#0x1_Vector_pop_back">pop_back</a>(v) } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>pragma intrinsic = true; </code></pre> </details>

Module Specification

Helper Functions

Check if <code>v1</code> is equal to the result of adding <code>e</code> at the end of <code>v2</code>

<pre><code>fun <a href="Vector.md#0x1_Vector_eq_push_back">eq_push_back</a><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)] } </code></pre>

Check if <code>v</code> is equal to the result of concatenating <code>v1</code> and <code>v2</code>

<pre><code>fun <a href="Vector.md#0x1_Vector_eq_append">eq_append</a><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 } </code></pre>

Check <code>v1</code> is equal to the result of removing the first element of <code>v2</code>

<pre><code>fun <a href="Vector.md#0x1_Vector_eq_pop_front">eq_pop_front</a><Element>(v1: vector<Element>, v2: vector<Element>): bool { len(v1) + 1 == len(v2) && v1 == v2[1..len(v2)] } </code></pre>

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

<pre><code>fun <a href="Vector.md#0x1_Vector_eq_remove_elem_at_index">eq_remove_elem_at_index</a><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)] } </code></pre>

Module `0x1::Vector`

Module 0x1::Vector

Constants

Function empty

Function length

Function borrow

Function push_back

Function borrow_mut

Function pop_back

Function destroy_empty

Function swap

Function singleton

Function reverse

Function append

Function is_empty

Function contains

Function index_of

Function remove

Function swap_remove

Module Specification

Helper Functions

Module `0x1::Vector`

Function `empty`

Function `length`

Function `borrow`

Function `push_back`

Function `borrow_mut`

Function `pop_back`

Function `destroy_empty`

Function `swap`

Function `singleton`

Function `reverse`

Function `append`

Function `is_empty`

Function `contains`

Function `index_of`

Function `remove`

Function `swap_remove`