~/bend-docscommunity

src/Sstable.bend fails

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

5 imports
import Base
import ./Keys.bend as Keys
import ./MemTable.bend as MemTable
import ./BitTree.bend as BitTree
import ./SortedRun.bend as SortedRun

Types

type Bloom source · line 11 · raw

Data

type Table source · line 14 · raw

Data

type Metadata source · line 24 · raw

Data

Definitions

def bloom_bits source · line 29 · raw

@level:Nat -> @est_keys:Nat -> Nat

--- Bloom allocator (Monkey-style: smaller/upper levels get more bits) --- Closed form pinned here; Dayan-exact coefficients are tuning follow-up.

def bhash source · line 41 · raw

@s:String -> @h:U32 -> U32

--- Local byte hash (kept stable for on-disk/rebuild compatibility) ---

def u32_byte source · line 57 · raw

@+w:U32 -> @shift:Nat -> Nat

--- U32->Nat bridges that stay checker-tractable --- The Bend checker does not share across sequentially-chained U32.mul terms: U32.to_nat applied to a hash accumulated over 4+ bytes diverges in {==} elaboration (runtime is unaffected). The bridges below therefore never materialize a chained U32 as a Nat: each to_nat covers at most two U32 ops (shift+mask on the ORIGINAL word — parallel, shared), and all accumulation happens in small-Nat land. Both are EXACT (no semantic change): bytes are the base-256 digits of the word (Horner), so u32_to_nat_exact(w) == U32.to_nat(w) and bhash_n computes the same mod.

def u32_to_nat_exact source · line 60 · raw

@+w:U32 -> Nat

def bhash_n_pos source · line 67 · raw

@+s:String -> @+seed:U32 -> @+m:Nat -> Nat

def bhash_n source · line 74 · raw

@s:String -> @seed:U32 -> @m:Nat -> Nat

def bit_words source · line 83 · raw

@n:Nat -> Nat

BitTree stores whole U32 words while Bloom.size preserves the exact logical bit count selected by bloom_bits.

def bits_new source · line 90 · raw

@+n:Nat -> 0x05fa0e42448e8e221df592b204de523d/src/BitTree.BitTree

def bit_set source · line 93 · raw

@i:Nat -> @bits:0x05fa0e42448e8e221df592b204de523d/src/BitTree.BitTree -> 0x05fa0e42448e8e221df592b204de523d/src/BitTree.BitTree

def bit_get source · line 96 · raw

@i:Nat -> @bits:0x05fa0e42448e8e221df592b204de523d/src/BitTree.BitTree -> Bool

def bloom_new source · line 99 · raw

@+n:Nat -> Bloom

def bloom_well_formed source · line 102 · raw

@b:Bloom -> Bool

def bloom_add source · line 111 · raw

@b:Bloom -> @+k:String -> Bloom

def both source · line 116 · raw

@a:Bool -> @b:Bool -> Bool

def bloom_test source · line 123 · raw

@b:Bloom -> @+k:String -> Bool

def table_bits source · line 128 · raw

@t:Table -> Nat

def maybe_present source · line 133 · raw

@t:Table -> @+k:String -> Bool

def bloom_of source · line 139 · raw

@entries:List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry> -> @+blm:Bloom -> Bloom

--- Canonicalization and construction ---

def metadata_tail source · line 148 · raw

@entries:List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry> -> @+first:String -> @last:String -> @+count:Nat -> Metadata

def metadata source · line 155 · raw

@entries:List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry> -> Metadata

def from_sorted_unique_est_meta source · line 162 · raw

@+entries:List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry> -> @level:Nat -> @est_keys:Nat -> @meta:Metadata -> Table

def from_sorted_unique_meta source · line 168 · raw

@+entries:List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry> -> @level:Nat -> @meta:Metadata -> Table

def from_sorted_unique source · line 174 · raw

@+entries:List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry> -> @level:Nat -> Table

def build_sorted source · line 177 · raw

@+entries:List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry> -> @level:Nat -> @est_keys:Nat -> Table

def build source · line 180 · raw

@+entries:List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry> -> @level:Nat -> @est_keys:Nat -> Table

def table_smallest source · line 185 · raw

@t:Table -> Maybe<&2, String>

Metadata accessors keep clients independent of the Tbl field layout.

def table_largest source · line 190 · raw

@t:Table -> Maybe<&2, String>

def table_count source · line 195 · raw

@t:Table -> Nat

def table_bits_from_meta source · line 202 · raw

@+entries:List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry> -> @level:Nat -> @est_keys:Nat -> @meta:Metadata -> {table_bits(from_sorted_unique_est_meta(entries, level, est_keys, meta)) == bloom_bits(level, est_keys) : Nat}

Open bridge: metadata is matched explicitly so the Bloom schedule projects through build without relying on reduction of an open entry list.

def table_bits_build source · line 207 · raw

@+entries:List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry> -> @level:Nat -> @est_keys:Nat -> {table_bits(build(entries, level, est_keys)) == bloom_bits(level, Nat.max(est_keys, List.length(&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry, entries))) : Nat}

def ranges_disjoint source · line 212 · raw

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

def size_of source · line 215 · raw

@b:Bloom -> Nat

def bloom_size_stable source · line 221 · raw

@entries:List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry> -> @bits:0x05fa0e42448e8e221df592b204de523d/src/BitTree.BitTree -> @+size:Nat -> {size_of(bloom_of(entries, Blm{bits, size})) == size : Nat}

Bloom insertions only set tree bits and preserve the exact logical size.

def lookup source · line 230 · raw

@t:Table -> @+k:String -> Maybe<&2, String>