~/bend-docscommunity

src/BitTree.bend checks

raw source on the hub · import mylsm-lsm-store@0.5.0.0/src/BitTree.bend as BitTree

3 imports
import Base
import 0x9ee2e9a299991dcc089fe22c7f3ceb5f/src/containers/bitset.bend as BitWords
import 0x9ee2e9a299991dcc089fe22c7f3ceb5f/src/math/pow2.bend as Pow2

Types

type WordTree source · line 18 · raw

Data

Represent WordTree data used by the packed bit-tree operations.

type BitTree source · line 24 · raw

Data

Represent BitTree data used by the packed bit-tree operations.

type Plan source · line 28 · raw

Data

Represent Plan data used by the packed bit-tree operations.

Definitions

def plan_go source · line 33 · raw

@fuel:Nat -> @+need:Nat -> @+capacity:Nat -> @+height:Nat -> @done:Bool -> Plan

Find the least power of two >= need. fuel = need is a conservative termination bound; each non-final step doubles capacity.

def plan source · line 46 · raw

@+need:Nat -> Plan

Handle plan in the packed bit-tree operations.

def zero_tree source · line 54 · raw

@+height:Nat -> WordTree

Independent subtrees are built in parallel.

def new_from_plan source · line 63 · raw

@words:Nat -> @plan:Plan -> BitTree

Create from plan for the packed bit-tree operations.

def new source · line 69 · raw

@+words:Nat -> BitTree

Handle new in the packed bit-tree operations.

def word_count source · line 78 · raw

@tree:BitTree -> Nat

Metadata helpers intended to keep representation laws independent of field layout.

def capacity_words source · line 84 · raw

@tree:BitTree -> Nat

Handle capacity words in the packed bit-tree operations.

def tree_height source · line 90 · raw

@tree:BitTree -> Nat

Handle tree height in the packed bit-tree operations.

def bit_count source · line 96 · raw

@tree:BitTree -> Nat

Handle bit count in the packed bit-tree operations.

def valid_bit source · line 100 · raw

@tree:BitTree -> @bit:Nat -> Bool

Check whether bit holds for the packed bit-tree operations.

def same_metadata source · line 104 · raw

@+ta:BitTree -> @+tb:BitTree -> Bool

Handle same metadata in the packed bit-tree operations.

def path_bit source · line 112 · raw

@rem:Nat -> Bool

Build the root-to-leaf path by consuming low bits while prepending them.

def index_path source · line 120 · raw

@height:Nat -> @+index:Nat -> @acc:List<&2, Bool> -> List<&2, Bool>

Handle index path in the packed bit-tree operations.

def tree_word source · line 128 · raw

@path:List<&2, Bool> -> @tree:WordTree -> U32

Handle tree word in the packed bit-tree operations.

def tree_set_word source · line 146 · raw

@path:List<&2, Bool> -> @value:U32 -> @tree:WordTree -> WordTree

Handle tree set word in the packed bit-tree operations.

def word_at_if source · line 164 · raw

@inside:Bool -> @tree:BitTree -> @index:Nat -> U32

Handle word at if in the packed bit-tree operations.

def word_at source · line 174 · raw

@+tree:BitTree -> @+index:Nat -> U32

Safe logical-word lookup; padding leaves are not externally addressable.

def replace_word_if source · line 178 · raw

@inside:Bool -> @tree:BitTree -> @index:Nat -> @value:U32 -> BitTree

Replace word if for the packed bit-tree operations.

def replace_word source · line 189 · raw

@+tree:BitTree -> @+index:Nat -> @value:U32 -> BitTree

Safe logical-word update. This helper makes metadata preservation and unaffected-word laws direct to state.

def set_if source · line 193 · raw

@inside:Bool -> @+tree:BitTree -> @+bit:Nat -> BitTree

Update if for the packed bit-tree operations.

def set source · line 203 · raw

@+tree:BitTree -> @+bit:Nat -> BitTree

Set one logical bit. Out-of-range indexes leave the tree unchanged.

def test_if source · line 207 · raw

@inside:Bool -> @+tree:BitTree -> @+bit:Nat -> Bool

Handle test if in the packed bit-tree operations.

def test source · line 216 · raw

@+tree:BitTree -> @+bit:Nat -> Bool

Test one logical bit. Out-of-range indexes, including every index in the zero-word tree, return False{}.

def union_bits source · line 222 · raw

@ta:WordTree -> @tb:WordTree -> WordTree

Word-wise union for chunked Bloom builds. Both sides always share the exact shape (same height from the same bit count); mismatched arms are unreachable by construction and keep the Fork side.

def shape_ok source · line 244 · raw

@+height:Nat -> @tree:WordTree -> Bool

Structural checker for the exact perfect-tree shape described by metadata.

def empty_metadata_ok source · line 261 · raw

@words:Nat -> @capacity:Nat -> @height:Nat -> Bool

Check whether whether metadata ok holds for the packed bit-tree operations.

def nonempty_metadata_ok source · line 265 · raw

@root:WordTree -> @+words:Nat -> @+capacity:Nat -> @+height:Nat -> Bool

Handle nonempty metadata ok in the packed bit-tree operations.

def well_formed source · line 276 · raw

@tree:BitTree -> Bool

Checks zero canonicality, logical bounds, power-of-two capacity, height, and exact tree shape. It does not require padding words to remain zero.