Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Module 0x1::big_vector 

use 0x1::error;
use 0x1::table_with_length;
use 0x1::vector;

Struct BigVector

A scalable vector implementation based on tables where elements are grouped into buckets. Each bucket has a capacity of bucket_size elements.

struct BigVector<T> has store
Fields
buckets: table_with_length::TableWithLength<u64, vector<T>>
end_index: u64
bucket_size: u64

Resource Ghost$initial_end_index 

struct Ghost$initial_end_index has copy, drop, store, key
Fields
v: u64

Constants

Vector index is out of bounds

const EINDEX_OUT_OF_BOUNDS: u64 = 1;

Cannot pop back from an empty vector

const EVECTOR_EMPTY: u64 = 3;

Cannot destroy a non-empty vector

const EVECTOR_NOT_EMPTY: u64 = 2;

bucket_size cannot be 0

const EZERO_BUCKET_SIZE: u64 = 4;

Function empty

Regular Vector API Create an empty vector.

public(friend) fun empty<T: store>(bucket_size: u64): big_vector::BigVector<T>
Implementation 
friend fun empty<T: store>(bucket_size: u64): BigVector<T> {
    assert!(bucket_size > 0, error::invalid_argument(EZERO_BUCKET_SIZE));
    BigVector {
        buckets: table_with_length::new(),
        end_index: 0,
        bucket_size,
    }
}

Function singleton

Create a vector of length 1 containing the passed in element.

public(friend) fun singleton<T: store>(element: T, bucket_size: u64): big_vector::BigVector<T>
Implementation 
friend fun singleton<T: store>(element: T, bucket_size: u64): BigVector<T> {
    let v = empty(bucket_size);
    v.push_back(element);
    v
}

Function destroy_empty

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

public fun destroy_empty<T>(self: big_vector::BigVector<T>)
Implementation 
public fun destroy_empty<T>(self: BigVector<T>) {
    assert!(self.is_empty(), error::invalid_argument(EVECTOR_NOT_EMPTY));
    let BigVector { buckets, end_index: _, bucket_size: _ } = self;
    buckets.destroy_empty();
}

Function destroy

Destroy the vector self if T has drop

public fun destroy<T: drop>(self: big_vector::BigVector<T>)
Implementation 
public fun destroy<T: drop>(self: BigVector<T>) {
    let BigVector { buckets, end_index, bucket_size: _ } = self;
    let i = 0;
    while (end_index > 0) {
        let num_elements = buckets.remove(i).length();
        end_index -= num_elements;
        i += 1;
    };
    buckets.destroy_empty();
}

Function borrow

Acquire an immutable reference to the ith element of the vector self. Aborts if i is out of bounds.

public fun borrow<T>(self: &big_vector::BigVector<T>, i: u64): &T
Implementation 
public fun borrow<T>(self: &BigVector<T>, i: u64): &T {
    assert!(i < self.length(), error::invalid_argument(EINDEX_OUT_OF_BOUNDS));
    self.buckets.borrow(i / self.bucket_size).borrow(i % self.bucket_size)
}

Function borrow_mut

Return a mutable reference to the ith element in the vector self. Aborts if i is out of bounds.

public fun borrow_mut<T>(self: &mut big_vector::BigVector<T>, i: u64): &mut T
Implementation 
public fun borrow_mut<T>(self: &mut BigVector<T>, i: u64): &mut T {
    assert!(i < self.length(), error::invalid_argument(EINDEX_OUT_OF_BOUNDS));
    self.buckets.borrow_mut(i / self.bucket_size).borrow_mut(i % self.bucket_size)
}

Function append

Empty and destroy the other vector, and push each of the elements in the other vector onto the self vector in the same order as they occurred in other. Disclaimer: This function is costly. Use it at your own discretion.

public fun append<T: store>(self: &mut big_vector::BigVector<T>, other: big_vector::BigVector<T>)
Implementation 
public fun append<T: store>(self: &mut BigVector<T>, other: BigVector<T>) {
    let other_len = other.length();
    let half_other_len = other_len / 2;
    let i = 0;
    while (i < half_other_len) {
        self.push_back(other.swap_remove(i));
        i += 1;
    }
    spec {
        invariant i <= half_other_len;
        invariant other.length() == other_len - i;
        invariant self.length() == length(old(self)) + i;
    };
    while (i < other_len) {
        self.push_back(other.pop_back());
        i += 1;
    }
    spec {
        invariant half_other_len <= i && i <= other_len;
        invariant other.length() == other_len - i;
        invariant self.length() == length(old(self)) + i;
    };
    other.destroy_empty();
}

Function push_back

Add element val to the end of the vector self. It grows the buckets when the current buckets are full. This operation will cost more gas when it adds new bucket.

public fun push_back<T: store>(self: &mut big_vector::BigVector<T>, val: T)
Implementation 
public fun push_back<T: store>(self: &mut BigVector<T>, val: T) {
    let num_buckets = self.buckets.length();
    if (self.end_index == num_buckets * self.bucket_size) {
        self.buckets.add(num_buckets, vector::empty());
        self.buckets.borrow_mut(num_buckets).push_back(val);
    } else {
        self.buckets.borrow_mut(num_buckets - 1).push_back(val);
    };
    self.end_index += 1;
}

Function pop_back

Pop an element from the end of vector self. It doesn’t shrink the buckets even if they’re empty. Call shrink_to_fit explicity to deallocate empty buckets. Aborts if self is empty.

public fun pop_back<T>(self: &mut big_vector::BigVector<T>): T
Implementation 
public fun pop_back<T>(self: &mut BigVector<T>): T {
    assert!(!self.is_empty(), error::invalid_state(EVECTOR_EMPTY));
    let num_buckets = self.buckets.length();
    let last_bucket = self.buckets.borrow_mut(num_buckets - 1);
    let val = last_bucket.pop_back();
    // Shrink the table if the last vector is empty.
    if (last_bucket.is_empty()) {
        move last_bucket;
        self.buckets.remove(num_buckets - 1).destroy_empty();
    };
    self.end_index -= 1;
    val
}

Function remove

Remove the element at index i in the vector v and return the owned value that was previously stored at i in self. All elements occurring at indices greater than i will be shifted down by 1. Will abort if i is out of bounds. Disclaimer: This function is costly. Use it at your own discretion.

public fun remove<T>(self: &mut big_vector::BigVector<T>, i: u64): T
Implementation 
public fun remove<T>(self: &mut BigVector<T>, i: u64): T {
    let len = self.length();
    assert!(i < len, error::invalid_argument(EINDEX_OUT_OF_BOUNDS));
    let num_buckets = self.buckets.length();
    let cur_bucket_index = i / self.bucket_size + 1;
    let cur_bucket = self.buckets.borrow_mut(cur_bucket_index - 1);
    let res = cur_bucket.remove(i % self.bucket_size);
    self.end_index -= 1;
    move cur_bucket;
    spec {
        update initial_end_index = self.end_index;
    };
    while (cur_bucket_index < num_buckets) {
        // remove one element from the start of current vector
        let cur_bucket = self.buckets.borrow_mut(cur_bucket_index);
        let t = cur_bucket.remove(0);
        move cur_bucket;
        // and put it at the end of the last one
        let prev_bucket = self.buckets.borrow_mut(cur_bucket_index - 1);
        prev_bucket.push_back(t);
        cur_bucket_index += 1;
    }
    spec {
        invariant 1 <= cur_bucket_index && cur_bucket_index <= num_buckets;
        invariant self.end_index == old(self).end_index - 1;
        invariant self.bucket_size == old(self).bucket_size;
        invariant table_with_length::spec_len(self.buckets) == num_buckets;
        invariant forall j in 0..table_with_length::spec_len(self.buckets):
            table_with_length::spec_contains(self.buckets, j);
    };
    spec {
        assert cur_bucket_index == num_buckets;
    };

    // Shrink the table if the last vector is empty.
    let last_bucket = self.buckets.borrow_mut(num_buckets - 1);
    if (last_bucket.is_empty()) {
        move last_bucket;
        self.buckets.remove(num_buckets - 1).destroy_empty();
    };

    res
}

Function 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<T>(self: &mut big_vector::BigVector<T>, i: u64): T
Implementation 
public fun swap_remove<T>(self: &mut BigVector<T>, i: u64): T {
    assert!(i < self.length(), error::invalid_argument(EINDEX_OUT_OF_BOUNDS));
    let last_val = self.pop_back();
    // if the requested value is the last one, return it
    if (self.end_index == i) {
        return last_val
    };
    // because the lack of mem::swap, here we swap remove the requested value from the bucket
    // and append the last_val to the bucket then swap the last bucket val back
    let bucket = self.buckets.borrow_mut(i / self.bucket_size);
    let bucket_len = bucket.length();
    let val = bucket.swap_remove(i % self.bucket_size);
    bucket.push_back(last_val);
    bucket.swap(i % self.bucket_size, bucket_len - 1);
    val
}

Function swap

Swap the elements at the i’th and j’th indices in the vector self. Will abort if either of i or j are out of bounds for self.

public fun swap<T>(self: &mut big_vector::BigVector<T>, i: u64, j: u64)
Implementation 
public fun swap<T>(self: &mut BigVector<T>, i: u64, j: u64) {
    assert!(i < self.length() && j < self.length(), error::invalid_argument(EINDEX_OUT_OF_BOUNDS));
    let i_bucket_index = i / self.bucket_size;
    let j_bucket_index = j / self.bucket_size;
    let i_vector_index = i % self.bucket_size;
    let j_vector_index = j % self.bucket_size;
    if (i_bucket_index == j_bucket_index) {
        self.buckets.borrow_mut(i_bucket_index).swap(i_vector_index, j_vector_index);
        return
    };
    // If i and j are in different buckets, take the buckets out first for easy mutation.
    let bucket_i = self.buckets.remove(i_bucket_index);
    let bucket_j = self.buckets.remove(j_bucket_index);
    // Get the elements from buckets by calling `swap_remove`.
    let element_i = bucket_i.swap_remove(i_vector_index);
    let element_j = bucket_j.swap_remove(j_vector_index);
    // Swap the elements and push back to the other bucket.
    bucket_i.push_back(element_j);
    bucket_j.push_back(element_i);
    let last_index_in_bucket_i = bucket_i.length() - 1;
    let last_index_in_bucket_j = bucket_j.length() - 1;
    // Re-position the swapped elements to the right index.
    bucket_i.swap(i_vector_index, last_index_in_bucket_i);
    bucket_j.swap(j_vector_index, last_index_in_bucket_j);
    // Add back the buckets.
    self.buckets.add(i_bucket_index, bucket_i);
    self.buckets.add(j_bucket_index, bucket_j);
}

Function reverse

Reverse the order of the elements in the vector self in-place. Disclaimer: This function is costly. Use it at your own discretion.

public fun reverse<T>(self: &mut big_vector::BigVector<T>)
Implementation 
public fun reverse<T>(self: &mut BigVector<T>) {
    let new_buckets = vector[];
    let push_bucket = vector[];
    let num_buckets = self.buckets.length();
    let num_buckets_left = num_buckets;

    while (num_buckets_left > 0) {
        let pop_bucket = self.buckets.remove(num_buckets_left - 1);
        pop_bucket.for_each_reverse(|val| {
            push_bucket.push_back(val);
            if (push_bucket.length() == self.bucket_size) {
                new_buckets.push_back(push_bucket);
                push_bucket = vector[];
            };
        });
        num_buckets_left -= 1;
    };

    if (push_bucket.length() > 0) {
        new_buckets.push_back(push_bucket);
    } else {
        push_bucket.destroy_empty();
    };

    new_buckets.reverse();
    assert!(self.buckets.length() == 0, 0);
    for (i in 0..num_buckets) {
        self.buckets.add(i, new_buckets.pop_back());
    };
    new_buckets.destroy_empty();
}

Function index_of

Return the index of the first occurrence of an element in self that is equal to e. Returns (true, index) if such an element was found, and (false, 0) otherwise. Disclaimer: This function is costly. Use it at your own discretion.

public fun index_of<T>(self: &big_vector::BigVector<T>, val: &T): (bool, u64)
Implementation 
public fun index_of<T>(self: &BigVector<T>, val: &T): (bool, u64) {
    let num_buckets = self.buckets.length();
    let bucket_index = 0;
    while (bucket_index < num_buckets) {
        let cur = self.buckets.borrow(bucket_index);
        let (found, i) = cur.index_of(val);
        if (found) {
            return (true, bucket_index * self.bucket_size + i)
        };
        bucket_index += 1;
    }
    spec {
        invariant bucket_index <= num_buckets;
        // All buckets checked so far contain no element equal to val.
        invariant forall j in 0..bucket_index:
            (forall k in 0..len(table_with_length::spec_get(self.buckets, j)):
                table_with_length::spec_get(self.buckets, j)[k] != val);
    };
    (false, 0)
}

Function contains

Return if an element equal to e exists in the vector self. Disclaimer: This function is costly. Use it at your own discretion.

public fun contains<T>(self: &big_vector::BigVector<T>, val: &T): bool
Implementation 
public fun contains<T>(self: &BigVector<T>, val: &T): bool {
    if (self.is_empty()) return false;
    let (exist, _) = self.index_of(val);
    exist
}

Function to_vector

Convert a big vector to a native vector, which is supposed to be called mostly by view functions to get an atomic view of the whole vector. Disclaimer: This function may be costly as the big vector may be huge in size. Use it at your own discretion.

public fun to_vector<T: copy>(self: &big_vector::BigVector<T>): vector<T>
Implementation 
public fun to_vector<T: copy>(self: &BigVector<T>): vector<T> {
    let res = vector[];
    let num_buckets = self.buckets.length();
    for (i in 0..num_buckets) {
        res.append(*self.buckets.borrow(i));
    };
    res
}

Function length

Return the length of the vector.

public fun length<T>(self: &big_vector::BigVector<T>): u64
Implementation 
public fun length<T>(self: &BigVector<T>): u64 {
    self.end_index
}

Function is_empty

Return true if the vector v has no elements and false otherwise.

public fun is_empty<T>(self: &big_vector::BigVector<T>): bool
Implementation 
public fun is_empty<T>(self: &BigVector<T>): bool {
    self.length() == 0
}

Specification 

global initial_end_index: u64;

Struct BigVector 

struct BigVector<T> has store
buckets: table_with_length::TableWithLength<u64, vector<T>>
end_index: u64
bucket_size: u64 
invariant bucket_size != 0;
invariant spec_table_len(buckets) == 0 ==> end_index == 0;
invariant end_index == 0 ==> spec_table_len(buckets) == 0;
invariant end_index <= spec_table_len(buckets) * bucket_size;
invariant spec_table_len(buckets) == 0
    || (forall i in 0..spec_table_len(buckets)-1: len(table_with_length::spec_get(buckets, i)) == bucket_size);
invariant spec_table_len(buckets) == 0
    || len(table_with_length::spec_get(buckets, spec_table_len(buckets) -1 )) <= bucket_size;
invariant forall i in 0..spec_table_len(buckets): spec_table_contains(buckets, i);
invariant forall i: u64 {spec_table_contains(buckets, i)}: spec_table_contains(buckets, i) ==> i < spec_table_len(buckets);
invariant (spec_table_len(buckets) == 0 && end_index == 0)
    || (spec_table_len(buckets) != 0 && ((spec_table_len(buckets) - 1) * bucket_size) + (len(table_with_length::spec_get(buckets, spec_table_len(buckets) - 1))) == end_index);
invariant forall i: u64 {spec_table_contains(buckets, i)} where i >= spec_table_len(buckets):  {
    !spec_table_contains(buckets, i)
};
invariant spec_table_len(buckets) == 0
    || (len(table_with_length::spec_get(buckets, spec_table_len(buckets) - 1)) > 0);

Function empty 

public(friend) fun empty<T: store>(bucket_size: u64): big_vector::BigVector<T>

aborts_if bucket_size == 0;
ensures result.length() == 0;
ensures result.bucket_size == bucket_size;

Function singleton 

public(friend) fun singleton<T: store>(element: T, bucket_size: u64): big_vector::BigVector<T>

aborts_if bucket_size == 0;
ensures result.length() == 1;
ensures result.bucket_size == bucket_size;

Function destroy_empty 

public fun destroy_empty<T>(self: big_vector::BigVector<T>)

aborts_if !self.is_empty();

Function borrow 

public fun borrow<T>(self: &big_vector::BigVector<T>, i: u64): &T

aborts_if i >= self.length();
ensures result == spec_at(self, i);

Function borrow_mut 

public fun borrow_mut<T>(self: &mut big_vector::BigVector<T>, i: u64): &mut T

aborts_if i >= self.length();
ensures result == spec_at(self, i);

Function append 

public fun append<T: store>(self: &mut big_vector::BigVector<T>, other: big_vector::BigVector<T>)

ensures self.length() == old(self.length()) + other.length();

Function push_back 

public fun push_back<T: store>(self: &mut big_vector::BigVector<T>, val: T)

pragma opaque;
let num_buckets = spec_table_len(self.buckets);
include PushbackAbortsIf<T>;
ensures self.length() == old(self).length() + 1;
ensures self.end_index == old(self.end_index) + 1;
ensures spec_at(self, self.end_index-1) == val;
ensures forall i in 0..self.end_index-1: spec_at(self, i) == spec_at(old(self), i);
ensures self.bucket_size == old(self).bucket_size;


schema PushbackAbortsIf<T> {
    self: BigVector<T>;
    let num_buckets = spec_table_len(self.buckets);
    aborts_if num_buckets * self.bucket_size > MAX_U64;
    aborts_if self.end_index + 1 > MAX_U64;
}

Function pop_back 

public fun pop_back<T>(self: &mut big_vector::BigVector<T>): T

pragma opaque;
aborts_if self.is_empty();
ensures self.length() == old(self).length() - 1;
ensures result == old(spec_at(self, self.end_index-1));
ensures forall i in 0..self.end_index: spec_at(self, i) == spec_at(old(self), i);
ensures forall b in 0..spec_table_len(self.buckets):
    forall p in 0..len(table_with_length::spec_get(self.buckets, b)):
        table_with_length::spec_get(self.buckets, b)[p] ==
        table_with_length::spec_get(old(self).buckets, b)[p];
ensures self.bucket_size == old(self).bucket_size;

Function remove 

public fun remove<T>(self: &mut big_vector::BigVector<T>, i: u64): T

pragma opaque;
aborts_if i >= self.length();
ensures self.length() == old(self.length()) - 1;
ensures self.bucket_size == old(self.bucket_size);
ensures result == spec_at(old(self), i);

Function swap_remove 

public fun swap_remove<T>(self: &mut big_vector::BigVector<T>, i: u64): T

pragma opaque;
aborts_if i >= self.length();
ensures self.length() == old(self).length() - 1;
ensures result == spec_at(old(self), i);

Function swap 

public fun swap<T>(self: &mut big_vector::BigVector<T>, i: u64, j: u64)

pragma opaque;
aborts_if i >= self.length() || j >= self.length();
ensures self.length() == old(self).length();
ensures spec_at(self, i) == spec_at(old(self), j);
ensures spec_at(self, j) == spec_at(old(self), i);
ensures forall idx in 0..self.length()
    where idx != i && idx != j:
    spec_at(self, idx) == spec_at(old(self), idx);

Function index_of 

public fun index_of<T>(self: &big_vector::BigVector<T>, val: &T): (bool, u64)

pragma opaque;
aborts_if false;
ensures result_1 ==> result_2 < self.length();
ensures result_1 ==> spec_at(self, result_2) == val;
ensures !result_1 ==> (forall j in 0..spec_table_len(self.buckets):
    forall k in 0..len(table_with_length::spec_get(self.buckets, j)):
        table_with_length::spec_get(self.buckets, j)[k] != val);

Function contains 

public fun contains<T>(self: &big_vector::BigVector<T>, val: &T): bool

aborts_if false;


fun spec_table_len<K, V>(t: TableWithLength<K, V>): u64 {
   table_with_length::spec_len(t)
}


fun spec_table_contains<K, V>(t: TableWithLength<K, V>, k: K): bool {
   table_with_length::spec_contains(t, k)
}


fun spec_at<T>(v: BigVector<T>, i: u64): T {
   let bucket = i / v.bucket_size;
   let idx = i % v.bucket_size;
   let v = table_with_length::spec_get(v.buckets, bucket);
   v[idx]
}