Skip to content

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 ith 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): &Element;

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 ith 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 ith and jth 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 ith 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 ith 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 ith 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;