src/BitTree.bend checks

raw source on the hub · import 0x05fa0e42448e8e221df592b204de523d/src/BitTree.bend as BitTree

1 import

import Base

Types

type WordTree source · line 15 · raw

Data

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

Fork

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

type BitTree source · line 20 · raw

Data

BT

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

type Plan source · line 23 · raw

Data

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

Definitions

def plan_go source · line 28 · 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 40 · raw

@+need:Nat -> Plan

def zero_tree source · line 48 · raw

@+height:Nat -> WordTree

Independent subtrees are built in parallel.

def new_from_plan source · line 56 · raw

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

def new source · line 61 · raw

@+words:Nat -> BitTree

def word_count source · line 70 · raw

@t:BitTree -> Nat

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

def capacity_words source · line 75 · raw

@t:BitTree -> Nat

def tree_height source · line 80 · raw

@t:BitTree -> Nat

def bit_count source · line 85 · raw

@t:BitTree -> Nat

def valid_bit source · line 88 · raw

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

def same_metadata source · line 91 · raw

@+a:BitTree -> @+b:BitTree -> Bool

def path_bit source · line 99 · raw

@rem:Nat -> Bool

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

def index_path source · line 106 · raw

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

def tree_word source · line 113 · raw

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

def tree_set_word source · line 130 · raw

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

def word_at_if source · line 147 · raw

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

def word_at source · line 157 · raw

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

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

def replace_word_if source · line 160 · raw

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

def replace_word source · line 171 · raw

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

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

def bit_mask source · line 174 · raw

@bit:Nat -> U32

def set_if source · line 177 · raw

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

def set source · line 187 · raw

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

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

def test_if source · line 190 · raw

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

def test source · line 199 · raw

@+t: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 204 · 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 220 · raw

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

def nonempty_metadata_ok source · line 223 · raw

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

def well_formed source · line 234 · raw

@t: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.