~/bend-docscommunity

src/Sstable.bend fails

raw source on the hub · import mylsm-lsm-store@0.3.1.0/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 72 · raw

Data

Definitions

def block_entries source · line 26 · raw

Nat

def chunk_go source · line 29 · raw

@fuel:Nat -> @+entries:List<&2, 0x0ae7ac793853e753f5f74c16e06ee078/src/MemTable.Entry> -> @+cur:List<&2, 0x0ae7ac793853e753f5f74c16e06ee078/src/MemTable.Entry> -> @room:Nat -> @acc:List<&2, List<&2, 0x0ae7ac793853e753f5f74c16e06ee078/src/MemTable.Entry>> -> List<&2, List<&2, 0x0ae7ac793853e753f5f74c16e06ee078/src/MemTable.Entry>>

def chunk source · line 44 · raw

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

def chunk_head_key source · line 51 · raw

@+xs:List<&2, 0x0ae7ac793853e753f5f74c16e06ee078/src/MemTable.Entry> -> Maybe<&2, String>

def block_cons_acc source · line 58 · raw

@head:Maybe<&2, String> -> @acc:List<&2, String> -> List<&2, String>

def block_keys source · line 65 · raw

@+chunks:List<&2, List<&2, 0x0ae7ac793853e753f5f74c16e06ee078/src/MemTable.Entry>> -> @acc:List<&2, String> -> List<&2, String>

def bloom_bits source · line 77 · 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 89 · raw

@str:String -> @acc:U32 -> U32

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

def u32_byte source · line 105 · raw

@+word: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 108 · raw

@+word:U32 -> Nat

def bhash_n_pos source · line 115 · raw

@+str:String -> @+seed:U32 -> @+mod:Nat -> Nat

def bhash_n source · line 122 · raw

@str:String -> @seed:U32 -> @mod:Nat -> Nat

def bit_words source · line 131 · raw

@num: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 138 · raw

@+num:Nat -> 0x0ae7ac793853e753f5f74c16e06ee078/src/BitTree.BitTree

def bit_set source · line 141 · raw

@idx:Nat -> @bits:0x0ae7ac793853e753f5f74c16e06ee078/src/BitTree.BitTree -> 0x0ae7ac793853e753f5f74c16e06ee078/src/BitTree.BitTree

def bit_get source · line 144 · raw

@idx:Nat -> @bits:0x0ae7ac793853e753f5f74c16e06ee078/src/BitTree.BitTree -> Bool

def bloom_new source · line 147 · raw

@+num:Nat -> Bloom

def bloom_well_formed source · line 150 · raw

@bloom:Bloom -> Bool

def bloom_add source · line 159 · raw

@bloom:Bloom -> @+key:String -> Bloom

def both source · line 164 · raw

@lhs:Bool -> @rhs:Bool -> Bool

def bloom_test source · line 171 · raw

@bloom:Bloom -> @+key:String -> Bool

def table_bits source · line 176 · raw

@tab:Table -> Nat

def maybe_present source · line 181 · raw

@tab:Table -> @+key:String -> Bool

def probe_hit_if source · line 188 · raw

@present:Bool -> Nat

--- Parallel probe counters (Task 1): sequential leaf, two-way fork, ! gate --- Single probe as 0/1 for counting.

def probe_hit source · line 196 · raw

@+tab:Table -> @+key:String -> Nat

Count matching probes sequentially.

def probe_count_seq source · line 200 · raw

@+probes:List<&2, String> -> @+tab:Table -> Nat

Sequential probe count over a probe list.

def probe_count_par source · line 208 · raw

@+probes:List<&2, String> -> @+tab:Table -> Nat

Two-way parallel probe count; halves share no state.

def probe_count_bang_gate source · line 214 · raw

@+num:Nat -> Bool

Bang gate: GPU pays only with enough probes to fill lanes.

def probe_count_pick source · line 218 · raw

@gate:Bool -> @+probes:List<&2, String> -> @+tab:Table -> Nat

Pick CPU-pool or GPU execution for the same fork tree.

def probe_count_auto source · line 226 · raw

@+probes:List<&2, String> -> @+tab:Table -> Nat

Size-gated entry point for parallel probe counting.

def bloom_of source · line 230 · raw

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

--- Canonicalization and construction ---

def bloom_union_trees source · line 239 · raw

@+abits:0x0ae7ac793853e753f5f74c16e06ee078/src/BitTree.BitTree -> @+bbits:0x0ae7ac793853e753f5f74c16e06ee078/src/BitTree.BitTree -> @size:Nat -> Bloom

def bloom_union source · line 246 · raw

@ba:Bloom -> @bb:Bloom -> Bloom

def bloom_of_chunk source · line 253 · raw

@+chunk:List<&2, 0x0ae7ac793853e753f5f74c16e06ee078/src/MemTable.Entry> -> @+nb:Nat -> Bloom

def bloom_of_par source · line 257 · raw

@+entries:List<&2, 0x0ae7ac793853e753f5f74c16e06ee078/src/MemTable.Entry> -> @+nb:Nat -> Bloom

Two-half parallel build (spike 1): one spawn, one union. Sequential below.

def chunk_third source · line 264 · raw

@+entries:List<&2, 0x0ae7ac793853e753f5f74c16e06ee078/src/MemTable.Entry> -> @+skip:Nat -> @+take:Nat -> List<&2, 0x0ae7ac793853e753f5f74c16e06ee078/src/MemTable.Entry>

--- Four-chunk parallel build (Task 2): two-level fork, three unions --- Third chunk slice as take-after-drop.

def bloom_of_chunks source · line 268 · raw

@+entries:List<&2, 0x0ae7ac793853e753f5f74c16e06ee078/src/MemTable.Entry> -> @+nb:Nat -> Bloom

Four-way chunk build with a two-level fork tree.

def bloom_bang_gate source · line 276 · raw

@+num:Nat -> Bool

Bang gate: GPU pays only with enough entries to feed lanes.

def bloom_of_pick source · line 280 · raw

@gate:Bool -> @+entries:List<&2, 0x0ae7ac793853e753f5f74c16e06ee078/src/MemTable.Entry> -> @+nb:Nat -> Bloom

Pick CPU-pool or GPU execution for the same chunk tree.

def bloom_of_bang source · line 289 · raw

@+entries:List<&2, 0x0ae7ac793853e753f5f74c16e06ee078/src/MemTable.Entry> -> @+nb:Nat -> Bloom

Size-gated ! entry point: the bang fires only at >= 8192 entries, where every flush in the durable write path lands (frozen merge of 4096 + 4096).

def key_idxs source · line 299 · raw

@+key:String -> @+size:Nat -> List<&2, Nat>

--- Hybrid bloom (spike): parallel index collection, sequential assembly --- Phase 1 emits a flat index list (two per key); joins concatenate, so no chunk tree or union is ever built. Phase 2 folds the indexes into ONE tree on the CPU. This removes the tree-allocation amplification that costs ~10% at 1M scale in the chunk+union design, while keeping a fork tree that a future ! can ship once the GPU recovery crash is fixed upstream. Both bit positions of one key as a flat two-element list.

def hash_idxs_seq source · line 303 · raw

@+entries:List<&2, 0x0ae7ac793853e753f5f74c16e06ee078/src/MemTable.Entry> -> @+size:Nat -> List<&2, Nat>

Sequential index collection over entries.

def hash_idxs_par_go source · line 311 · raw

@+fuel:Nat -> @+entries:List<&2, 0x0ae7ac793853e753f5f74c16e06ee078/src/MemTable.Entry> -> @+size:Nat -> List<&2, Nat>

Balanced parallel index collection; reusable fuel bounds the fork depth.

def hash_idxs_par source · line 327 · raw

@+entries:List<&2, 0x0ae7ac793853e753f5f74c16e06ee078/src/MemTable.Entry> -> @+size:Nat -> List<&2, Nat>

Parallel entry point; fuel covers the fork depth.

def bloom_set_all source · line 332 · raw

@+idxs:List<&2, Nat> -> @+blm:Bloom -> Bloom

Sequential assembly of one filter from a flat index list.

def bloom_of_hybrid source · line 342 · raw

@+entries:List<&2, 0x0ae7ac793853e753f5f74c16e06ee078/src/MemTable.Entry> -> @+nb:Nat -> Bloom

Hybrid build: parallel hashing, single-tree assembly.

def bloom_pick source · line 354 · raw

@small:Bool -> @+entries:List<&2, 0x0ae7ac793853e753f5f74c16e06ee078/src/MemTable.Entry> -> @+nb:Nat -> Bloom

Size-gated entry point: sequential on both sides of the gate. MEASURED VERDICT (2026-09-26, 1M interleaved A/B, Darwin arm64, Bend 2.0.28): sequential median 225105 ms (4442 ops/s) vs 4-chunk 249150 ms (4014 ops/s) vs hybrid 261746 ms — the parallel builds cost ~10% (fork/join plus allocation overhead dominates; invisible at 100k, compounds over 244 flushes). Confirmed under two machine states (all arms shifted +15k ms on the slow day; relative order unchanged). The parallel builds stay as law-covered spikes; the ! variants stay opt-in behind the GPU recovery crash documented below.

def bloom_of_auto source · line 361 · raw

@+entries:List<&2, 0x0ae7ac793853e753f5f74c16e06ee078/src/MemTable.Entry> -> @+nb:Nat -> Bloom

def metadata_tail source · line 364 · raw

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

def metadata source · line 371 · raw

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

def from_sorted_unique_est_meta source · line 378 · raw

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

def from_sorted_unique_meta source · line 384 · raw

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

def from_sorted_unique source · line 390 · raw

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

def build_sorted source · line 393 · raw

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

def build source · line 396 · raw

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

def table_smallest source · line 401 · raw

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

Metadata accessors keep clients independent of the Tbl field layout.

def table_largest source · line 406 · raw

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

def table_count source · line 411 · raw

@tab:Table -> Nat

def opt_name source · line 417 · raw

@+opt:Maybe<&2, String> -> String

Total table identity for the read cache: smallest|largest|count.

def table_id source · line 424 · raw

@tab:Table -> String

def table_bits_from_meta source · line 431 · raw

@+entries:List<&2, 0x0ae7ac793853e753f5f74c16e06ee078/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 441 · raw

@+entries:List<&2, 0x0ae7ac793853e753f5f74c16e06ee078/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, 0x0ae7ac793853e753f5f74c16e06ee078/src/MemTable.Entry, entries))) : Nat}

def ranges_disjoint source · line 450 · raw

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

def size_of source · line 453 · raw

@bloom:Bloom -> Nat

def bloom_size_stable source · line 459 · raw

@entries:List<&2, 0x0ae7ac793853e753f5f74c16e06ee078/src/MemTable.Entry> -> @bits:0x0ae7ac793853e753f5f74c16e06ee078/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 pick_ix source · line 471 · raw

@bt:List<&2, String> -> @ct:List<&2, List<&2, 0x0ae7ac793853e753f5f74c16e06ee078/src/MemTable.Entry>> -> @ix:Nat -> @+key:String -> @order:Cmp -> Nat

Block-scoped lookup. Checker constraints (proven by scratch experiments): multi-scrutinee matches follow declaration order, and only Nat answers flow through match arms — so selection returns an index, picked up by chunk_at_go.

def chunk_at_go source · line 484 · raw

@fuel:Nat -> @+chunks:List<&2, List<&2, 0x0ae7ac793853e753f5f74c16e06ee078/src/MemTable.Entry>> -> @ix:Nat -> List<&2, 0x0ae7ac793853e753f5f74c16e06ee078/src/MemTable.Entry>

def chunk_at source · line 497 · raw

@+chunks:List<&2, List<&2, 0x0ae7ac793853e753f5f74c16e06ee078/src/MemTable.Entry>> -> @ix:Nat -> List<&2, 0x0ae7ac793853e753f5f74c16e06ee078/src/MemTable.Entry>

def block_scan source · line 500 · raw

@+chunk:List<&2, 0x0ae7ac793853e753f5f74c16e06ee078/src/MemTable.Entry> -> @+key:String -> Maybe<&2, String>

def block_pick source · line 503 · raw

@+chunks:List<&2, List<&2, 0x0ae7ac793853e753f5f74c16e06ee078/src/MemTable.Entry>> -> @+blocks:List<&2, String> -> @+key:String -> List<&2, 0x0ae7ac793853e753f5f74c16e06ee078/src/MemTable.Entry>

def block_finish source · line 512 · raw

@picked:List<&2, 0x0ae7ac793853e753f5f74c16e06ee078/src/MemTable.Entry> -> @+entries:List<&2, 0x0ae7ac793853e753f5f74c16e06ee078/src/MemTable.Entry> -> @+key:String -> Maybe<&2, String>

def hit_finish source · line 519 · raw

@picked:List<&2, 0x0ae7ac793853e753f5f74c16e06ee078/src/MemTable.Entry> -> @+entries:List<&2, 0x0ae7ac793853e753f5f74c16e06ee078/src/MemTable.Entry> -> @+key:String -> Maybe<&2, Maybe<&2, String>>

def block_get_hit source · line 526 · raw

@tab:Table -> @+key:String -> Maybe<&2, Maybe<&2, String>>

def block_get source · line 531 · raw

@tab:Table -> @+key:String -> Maybe<&2, String>

def lookup source · line 536 · raw

@tab:Table -> @+key:String -> Maybe<&2, String>