Module 0x1::bit_vector

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

Struct BitVector

struct BitVector has copy, drop, store

Constants

The provided index is out of bounds

const EINDEX: u64 = 131072;

An invalid length of bitvector was given

const ELENGTH: u64 = 131073;

The maximum allowed bitvector size

const MAX_SIZE: u64 = 1024;

const WORD_SIZE: u64 = 1;

Function new

public fun new(length: u64): bit_vector::BitVector

public fun new(length: u64): BitVector {
    assert!(length > 0, ELENGTH);
    assert!(length < MAX_SIZE, ELENGTH);
    let counter = 0;
    let bit_field = vector::empty();
    while ({spec {
        invariant counter <= length;
        invariant len(bit_field) == counter;
    };
        (counter < length)}) {
        bit_field.push_back(false);
        counter += 1;
    };
    spec {
        assert counter == length;
        assert len(bit_field) == length;
    };

    BitVector {
        length,
        bit_field,
    }
}

Function set

Set the bit at bit_index in the self regardless of its previous state.

public fun set(self: &mut bit_vector::BitVector, bit_index: u64)

public fun set(self: &mut BitVector, bit_index: u64) {
    assert!(bit_index < self.bit_field.length(), EINDEX);
    self.bit_field[bit_index] = true;
}

Function unset

Unset the bit at bit_index in the self regardless of its previous state.

public fun unset(self: &mut bit_vector::BitVector, bit_index: u64)

public fun unset(self: &mut BitVector, bit_index: u64) {
    assert!(bit_index < self.bit_field.length(), EINDEX);
    self.bit_field[bit_index] = false;
}

Function shift_left

Shift the self left by amount. If amount is greater than the bitvector’s length the bitvector will be zeroed out.

public fun shift_left(self: &mut bit_vector::BitVector, amount: u64)

public fun shift_left(self: &mut BitVector, amount: u64) {
    if (amount >= self.length) {
        self.bit_field.for_each_mut(|elem| {
            *elem = false;
        });
    } else {
        let i = amount;

        while (i < self.length) {
            if (self.is_index_set(i)) self.set(i - amount)
            else self.unset(i - amount);
            i += 1;
        };

        i = self.length - amount;

        while (i < self.length) {
            self.unset(i);
            i += 1;
        };
    }
}

Function is_index_set

Return the value of the bit at bit_index in the self. true represents “1” and false represents a 0

public fun is_index_set(self: &bit_vector::BitVector, bit_index: u64): bool

public fun is_index_set(self: &BitVector, bit_index: u64): bool {
    assert!(bit_index < self.bit_field.length(), EINDEX);
    self.bit_field[bit_index]
}

Function length

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

public fun length(self: &bit_vector::BitVector): u64

public fun length(self: &BitVector): u64 {
    self.bit_field.length()
}

Function longest_set_sequence_starting_at

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

public fun longest_set_sequence_starting_at(self: &bit_vector::BitVector, start_index: u64): u64

public fun longest_set_sequence_starting_at(self: &BitVector, start_index: u64): u64 {
    assert!(start_index < self.length, EINDEX);
    let index = start_index;

    // Find the greatest index in the vector such that all indices less than it are set.
    while ({
        spec {
            invariant index >= start_index;
            invariant index == start_index || self.is_index_set(index - 1);
            invariant index == start_index || index - 1 < len(self.bit_field);
            invariant forall j in start_index..index: self.is_index_set(j);
            invariant forall j in start_index..index: j < len(self.bit_field);
        };
        index < self.length
    }) {
        if (!self.is_index_set(index)) break;
        index += 1;
    };

    index - start_index
}

Specification

Struct BitVector

struct BitVector has copy, drop, store

length: u64

bit_field: vector<bool>

invariant length == len(bit_field);

Function new

public fun new(length: u64): bit_vector::BitVector

include NewAbortsIf;
ensures result.length == length;
ensures len(result.bit_field) == length;

schema NewAbortsIf {
    length: u64;
    aborts_if length <= 0 with ELENGTH;
    aborts_if length >= MAX_SIZE with ELENGTH;
}

Function set

public fun set(self: &mut bit_vector::BitVector, bit_index: u64)

include SetAbortsIf;
ensures self.bit_field[bit_index];

schema SetAbortsIf {
    self: BitVector;
    bit_index: u64;
    aborts_if bit_index >= self.length() with EINDEX;
}

Function unset

public fun unset(self: &mut bit_vector::BitVector, bit_index: u64)

include UnsetAbortsIf;
ensures !self.bit_field[bit_index];

schema UnsetAbortsIf {
    self: BitVector;
    bit_index: u64;
    aborts_if bit_index >= self.length() with EINDEX;
}

Function shift_left

public fun shift_left(self: &mut bit_vector::BitVector, amount: u64)

pragma verify = false;

Function is_index_set

public fun is_index_set(self: &bit_vector::BitVector, bit_index: u64): bool

include IsIndexSetAbortsIf;
ensures result == self.bit_field[bit_index];

schema IsIndexSetAbortsIf {
    self: BitVector;
    bit_index: u64;
    aborts_if bit_index >= self.length() with EINDEX;
}

fun spec_is_index_set(self: BitVector, bit_index: u64): bool {
   if (bit_index >= self.length()) {
       false
   } else {
       self.bit_field[bit_index]
   }
}

Function longest_set_sequence_starting_at

public fun longest_set_sequence_starting_at(self: &bit_vector::BitVector, start_index: u64): u64

aborts_if start_index >= self.length;
ensures forall i in start_index..result: self.is_index_set(i);