src/BitTree.bend checks

raw source on the hub · import mylsm-lsm-store@0.3.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 17 · raw

Data

Empty
```
WordTree
```
Leaf
```
@word:U32 -> WordTree
```

Fork

@left:WordTree -> @right:WordTree -> WordTree

type BitTree source · line 22 · raw

Data

BT

@root:WordTree -> @words:Nat -> @capacity:Nat -> @height:Nat -> BitTree

type Plan source · line 25 · raw

Data

Plan
```
@capacity:Nat -> @height:Nat -> Plan
```

Definitions

def plan_go source · line 30 · 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 42 · raw

@+need:Nat -> Plan

def zero_tree source · line 50 · raw

@+height:Nat -> WordTree

Independent subtrees are built in parallel.

def new_from_plan source · line 58 · raw

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

def new source · line 63 · raw

@+words:Nat -> BitTree

def word_count source · line 72 · raw

@tree:BitTree -> Nat

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

def capacity_words source · line 77 · raw

@tree:BitTree -> Nat

def tree_height source · line 82 · raw

@tree:BitTree -> Nat

def bit_count source · line 87 · raw

@tree:BitTree -> Nat

def valid_bit source · line 90 · raw

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

def same_metadata source · line 93 · raw

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

def path_bit source · line 101 · raw

@rem:Nat -> Bool

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

def index_path source · line 108 · raw

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

def tree_word source · line 115 · raw

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

def tree_set_word source · line 132 · raw

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

def word_at_if source · line 149 · raw

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

def word_at source · line 159 · raw

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

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

def replace_word_if source · line 162 · raw

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

def replace_word source · line 173 · 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 176 · raw

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

def set source · line 186 · raw

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

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

def test_if source · line 189 · raw

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

def test source · line 198 · 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 shape_ok source · line 203 · raw

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

Structural checker for the exact perfect-tree shape described by metadata. The two equal-sized subtrees are checked in parallel.

def empty_metadata_ok source · line 219 · raw

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

def nonempty_metadata_ok source · line 222 · raw

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

def well_formed source · line 233 · 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.