Module `0x1::BitVector`

Struct BitVector
Constants
Function new
Function set
Function unset
Function shift_left
Function is_index_set
Function length
Function longest_set_sequence_starting_at

<pre><code>use <a href="Errors.md#0x1_Errors">0x1::Errors</a>; use <a href="Vector.md#0x1_Vector">0x1::Vector</a>; </code></pre>

Struct `BitVector`

<pre><code>struct <a href="BitVector.md#0x1_BitVector">BitVector</a> has copy, drop, store </code></pre> <details> <summary>Fields</summary> <dl> <dt> <code>length: u64</code> </dt> <dd> </dd> <dt> <code>bit_field: vector<bool></code> </dt> <dd> </dd> </dl> </details>

Constants

The provided index is out of bounds

<pre><code>const <a href="BitVector.md#0x1_BitVector_EINDEX">EINDEX</a>: u64 = 0; </code></pre>

An invalid length of bitvector was given

<pre><code>const <a href="BitVector.md#0x1_BitVector_ELENGTH">ELENGTH</a>: u64 = 1; </code></pre>

The maximum allowed bitvector size

<pre><code>const <a href="BitVector.md#0x1_BitVector_MAX_SIZE">MAX_SIZE</a>: u64 = 1024; </code></pre>

<pre><code>const <a href="BitVector.md#0x1_BitVector_WORD_SIZE">WORD_SIZE</a>: u64 = 1; </code></pre>

Function `new`

<pre><code>public fun <a href="BitVector.md#0x1_BitVector_new">new</a>(length: u64): <a href="BitVector.md#0x1_BitVector_BitVector">BitVector::BitVector</a> </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="BitVector.md#0x1_BitVector_new">new</a>(length: u64): <a href="BitVector.md#0x1_BitVector">BitVector</a> { assert(length > 0, <a href="Errors.md#0x1_Errors_invalid_argument">Errors::invalid_argument</a>(<a href="BitVector.md#0x1_BitVector_ELENGTH">ELENGTH</a>)); assert(<a href="BitVector.md#0x1_BitVector_length">length</a> < <a href="BitVector.md#0x1_BitVector_MAX_SIZE">MAX_SIZE</a>, <a href="Errors.md#0x1_Errors_invalid_argument">Errors::invalid_argument</a>(<a href="BitVector.md#0x1_BitVector_ELENGTH">ELENGTH</a>)); let counter = 0; let bit_field = <a href="Vector.md#0x1_Vector_empty">Vector::empty</a>(); while ({spec { invariant counter <= length; invariant len(bit_field) == counter; }; (counter < length)}) { <a href="Vector.md#0x1_Vector_push_back">Vector::push_back</a>(&mut bit_field, false); counter = counter + 1; }; spec { assert counter == length; assert len(bit_field) == length; }; <a href="BitVector.md#0x1_BitVector">BitVector</a> { length, bit_field, } } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>include <a href="BitVector.md#0x1_BitVector_NewAbortsIf">NewAbortsIf</a>; ensures result.length == length; ensures len(result.bit_field) == length; </code></pre>

<pre><code>schema <a href="BitVector.md#0x1_BitVector_NewAbortsIf">NewAbortsIf</a> { length: u64; aborts_if <a href="BitVector.md#0x1_BitVector_length">length</a> <= 0 with <a href="Errors.md#0x1_Errors_INVALID_ARGUMENT">Errors::INVALID_ARGUMENT</a>; aborts_if length >= <a href="BitVector.md#0x1_BitVector_MAX_SIZE">MAX_SIZE</a> with <a href="Errors.md#0x1_Errors_INVALID_ARGUMENT">Errors::INVALID_ARGUMENT</a>; } </code></pre> </details>

Function `set`

Set the bit at <code>bit_index</code> in the <code>bitvector</code> regardless of its previous state.

<pre><code>public fun <a href="BitVector.md#0x1_BitVector_set">set</a>(bitvector: &mut <a href="BitVector.md#0x1_BitVector_BitVector">BitVector::BitVector</a>, bit_index: u64) </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="BitVector.md#0x1_BitVector_set">set</a>(bitvector: &mut <a href="BitVector.md#0x1_BitVector">BitVector</a>, bit_index: u64) { assert(bit_index < <a href="Vector.md#0x1_Vector_length">Vector::length</a>(&bitvector.bit_field), <a href="Errors.md#0x1_Errors_invalid_argument">Errors::invalid_argument</a>(<a href="BitVector.md#0x1_BitVector_EINDEX">EINDEX</a>)); let x = <a href="Vector.md#0x1_Vector_borrow_mut">Vector::borrow_mut</a>(&mut bitvector.bit_field, bit_index); *x = true; } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>include <a href="BitVector.md#0x1_BitVector_SetAbortsIf">SetAbortsIf</a>; ensures bitvector.bit_field[bit_index]; </code></pre>

<pre><code>schema <a href="BitVector.md#0x1_BitVector_SetAbortsIf">SetAbortsIf</a> { bitvector: <a href="BitVector.md#0x1_BitVector">BitVector</a>; bit_index: u64; aborts_if bit_index >= <a href="BitVector.md#0x1_BitVector_length">length</a>(bitvector) with <a href="Errors.md#0x1_Errors_INVALID_ARGUMENT">Errors::INVALID_ARGUMENT</a>; } </code></pre> <pre><code>include <a href="BitVector.md#0x1_BitVector_UnsetAbortsIf">UnsetAbortsIf</a>; ensures bitvector.bit_field[bit_index]; </code></pre>

<pre><code>schema <a href="BitVector.md#0x1_BitVector_UnsetAbortsIf">UnsetAbortsIf</a> { bitvector: <a href="BitVector.md#0x1_BitVector">BitVector</a>; bit_index: u64; aborts_if bit_index >= <a href="BitVector.md#0x1_BitVector_length">length</a>(bitvector) with <a href="Errors.md#0x1_Errors_INVALID_ARGUMENT">Errors::INVALID_ARGUMENT</a>; } </code></pre> </details>

Function `unset`

Unset the bit at <code>bit_index</code> in the <code>bitvector</code> regardless of its previous state.

<pre><code>public fun <a href="BitVector.md#0x1_BitVector_unset">unset</a>(bitvector: &mut <a href="BitVector.md#0x1_BitVector_BitVector">BitVector::BitVector</a>, bit_index: u64) </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="BitVector.md#0x1_BitVector_unset">unset</a>(bitvector: &mut <a href="BitVector.md#0x1_BitVector">BitVector</a>, bit_index: u64) { assert(bit_index < <a href="Vector.md#0x1_Vector_length">Vector::length</a>(&bitvector.bit_field), <a href="Errors.md#0x1_Errors_invalid_argument">Errors::invalid_argument</a>(<a href="BitVector.md#0x1_BitVector_EINDEX">EINDEX</a>)); let x = <a href="Vector.md#0x1_Vector_borrow_mut">Vector::borrow_mut</a>(&mut bitvector.bit_field, bit_index); *x = false; } </code></pre> </details>

Function `shift_left`

Shift the <code>bitvector</code> left by <code>amount</code>. If <code>amount</code> is greater than the bitvector's length the bitvector will be zeroed out.

<pre><code>public fun <a href="BitVector.md#0x1_BitVector_shift_left">shift_left</a>(bitvector: &mut <a href="BitVector.md#0x1_BitVector_BitVector">BitVector::BitVector</a>, amount: u64) </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="BitVector.md#0x1_BitVector_shift_left">shift_left</a>(bitvector: &mut <a href="BitVector.md#0x1_BitVector">BitVector</a>, amount: u64) { if (amount >= bitvector.length) { let len = <a href="Vector.md#0x1_Vector_length">Vector::length</a>(&bitvector.bit_field); let i = 0; while (i < len) { let elem = <a href="Vector.md#0x1_Vector_borrow_mut">Vector::borrow_mut</a>(&mut bitvector.bit_field, i); *elem = false; i = i + 1; }; } else { let i = amount; while (i < bitvector.length) { if (<a href="BitVector.md#0x1_BitVector_is_index_set">is_index_set</a>(bitvector, i)) <a href="BitVector.md#0x1_BitVector_set">set</a>(bitvector, i - amount) else <a href="BitVector.md#0x1_BitVector_unset">unset</a>(bitvector, i - amount); i = i + 1; }; i = bitvector.length - amount; while (i < bitvector.length) { <a href="BitVector.md#0x1_BitVector_unset">unset</a>(bitvector, i); i = i + 1; }; } } </code></pre> </details>

Function `is_index_set`

Return the value of the bit at <code>bit_index</code> in the <code>bitvector</code>. <code>true</code> represents "1" and <code>false</code> represents a 0

<pre><code>public fun <a href="BitVector.md#0x1_BitVector_is_index_set">is_index_set</a>(bitvector: &<a href="BitVector.md#0x1_BitVector_BitVector">BitVector::BitVector</a>, bit_index: u64): bool </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="BitVector.md#0x1_BitVector_is_index_set">is_index_set</a>(bitvector: &<a href="BitVector.md#0x1_BitVector">BitVector</a>, bit_index: u64): bool { assert(bit_index < <a href="Vector.md#0x1_Vector_length">Vector::length</a>(&bitvector.bit_field), <a href="Errors.md#0x1_Errors_invalid_argument">Errors::invalid_argument</a>(<a href="BitVector.md#0x1_BitVector_EINDEX">EINDEX</a>)); *<a href="Vector.md#0x1_Vector_borrow">Vector::borrow</a>(&bitvector.bit_field, bit_index) } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>include <a href="BitVector.md#0x1_BitVector_IsIndexSetAbortsIf">IsIndexSetAbortsIf</a>; ensures result == bitvector.bit_field[bit_index]; </code></pre>

<pre><code>schema <a href="BitVector.md#0x1_BitVector_IsIndexSetAbortsIf">IsIndexSetAbortsIf</a> { bitvector: <a href="BitVector.md#0x1_BitVector">BitVector</a>; bit_index: u64; aborts_if bit_index >= <a href="BitVector.md#0x1_BitVector_length">length</a>(bitvector) with <a href="Errors.md#0x1_Errors_INVALID_ARGUMENT">Errors::INVALID_ARGUMENT</a>; } </code></pre>

<pre><code>fun <a href="BitVector.md#0x1_BitVector_spec_is_index_set">spec_is_index_set</a>(bitvector: <a href="BitVector.md#0x1_BitVector">BitVector</a>, bit_index: u64): bool { if (bit_index >= <a href="BitVector.md#0x1_BitVector_length">length</a>(bitvector)) { false } else { bitvector.bit_field[bit_index] } } </code></pre> </details>

Function `length`

Return the length (number of usable bits) of this bitvector

<pre><code>public fun <a href="BitVector.md#0x1_BitVector_length">length</a>(bitvector: &<a href="BitVector.md#0x1_BitVector_BitVector">BitVector::BitVector</a>): u64 </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="BitVector.md#0x1_BitVector_length">length</a>(bitvector: &<a href="BitVector.md#0x1_BitVector">BitVector</a>): u64 { <a href="Vector.md#0x1_Vector_length">Vector::length</a>(&bitvector.bit_field) } </code></pre> </details>

Function `longest_set_sequence_starting_at`

Returns the length of the longest sequence of set bits starting at (and including) <code>start_index</code> in the <code>bitvector</code>. If there is no such sequence, then <code>0</code> is returned.

<pre><code>public fun <a href="BitVector.md#0x1_BitVector_longest_set_sequence_starting_at">longest_set_sequence_starting_at</a>(bitvector: &<a href="BitVector.md#0x1_BitVector_BitVector">BitVector::BitVector</a>, start_index: u64): u64 </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="BitVector.md#0x1_BitVector_longest_set_sequence_starting_at">longest_set_sequence_starting_at</a>(bitvector: &<a href="BitVector.md#0x1_BitVector">BitVector</a>, start_index: u64): u64 { assert(start_index < bitvector.length, <a href="Errors.md#0x1_Errors_invalid_argument">Errors::invalid_argument</a>(<a href="BitVector.md#0x1_BitVector_EINDEX">EINDEX</a>)); let index = start_index; // Find the greatest index in the vector such that all indices less than it are set. while (index < bitvector.length) { if (!<a href="BitVector.md#0x1_BitVector_is_index_set">is_index_set</a>(bitvector, index)) break; index = index + 1; }; index - start_index } </code></pre> </details>

Module `0x1::BitVector`

Module 0x1::BitVector

Struct BitVector

Constants

Function new

Function set

Function unset

Function shift_left

Function is_index_set

Function length

Function longest_set_sequence_starting_at

Module `0x1::BitVector`

Struct `BitVector`

Function `new`

Function `set`

Function `unset`

Function `shift_left`

Function `is_index_set`

Function `length`

Function `longest_set_sequence_starting_at`