vector - [mainnet]
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;
Functions
empty
Create an empty vector.
#[bytecode_instruction]public fun empty<Element>(): vector<Element>
Implementation
native public fun empty<Element>(): vector<Element>;
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;
borrow
Acquire an immutable reference to the i
th 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): ∈
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);
borrow_mut
Return a mutable reference to the i
th 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;
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;
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>);
swap
Swaps the elements at the i
th and j
th 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);
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);
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}
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);}
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; }}
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); }}
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();}
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}
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}
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}
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}
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)}
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 (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; }; (find, found_index)}
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; }; };}
remove
Remove the i
th 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() }}
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[] }}
swap_remove
Swap the i
th 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()}
replace
Replace the i
th 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() }}
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));}
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()}
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 }}
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));}
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();}
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 }}
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; };}
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 }}
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 }}
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; };}
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}
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}
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}
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}
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}
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}
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}
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}
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)}
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)}
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}
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}
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}
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))}
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)}
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}
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}
singleton
public fun singleton<Element>(e: Element): vector<Element>
aborts_if false;ensures result == vec(e);
reverse
public fun reverse<Element>(self: &mut vector<Element>)
pragma intrinsic = true;
reverse_slice
public fun reverse_slice<Element>(self: &mut vector<Element>, left: u64, right: u64)
pragma intrinsic = true;
append
public fun append<Element>(self: &mut vector<Element>, other: vector<Element>)
pragma intrinsic = true;
reverse_append
public fun reverse_append<Element>(self: &mut vector<Element>, other: vector<Element>)
pragma intrinsic = true;
trim
public fun trim<Element>(self: &mut vector<Element>, new_len: u64): vector<Element>
pragma intrinsic = true;
trim_reverse
public fun trim_reverse<Element>(self: &mut vector<Element>, new_len: u64): vector<Element>
pragma intrinsic = true;
is_empty
public fun is_empty<Element>(self: &vector<Element>): bool
pragma intrinsic = true;
contains
public fun contains<Element>(self: &vector<Element>, e: &Element): bool
pragma intrinsic = true;
index_of
public fun index_of<Element>(self: &vector<Element>, e: &Element): (bool, u64)
pragma intrinsic = true;
insert
public fun insert<Element>(self: &mut vector<Element>, i: u64, e: Element)
pragma intrinsic = true;
remove
public fun remove<Element>(self: &mut vector<Element>, i: u64): Element
pragma intrinsic = true;
remove_value
public fun remove_value<Element>(self: &mut vector<Element>, val: &Element): vector<Element>
pragma intrinsic = true;
swap_remove
public fun swap_remove<Element>(self: &mut vector<Element>, i: u64): Element
pragma intrinsic = true;
rotate
public fun rotate<Element>(self: &mut vector<Element>, rot: u64): u64
pragma intrinsic = true;
rotate_slice
public fun rotate_slice<Element>(self: &mut vector<Element>, left: u64, rot: u64, right: u64): u64
pragma intrinsic = true;