src/Sstable.bend checks

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

Data

Represent Bloom data used by the SSTable indexes, filters, and lookup.

Blm

@bits:0x4fcd94fa965aa1443134557fd075a483/src/BitTree.BitTree -> @size:Nat -> Bloom

type Table source · line 16 · raw

Data

Represent Table data used by the SSTable indexes, filters, and lookup.

Tbl

@entries:List<&2, 0x4fcd94fa965aa1443134557fd075a483/src/MemTable.Entry> -> @filter:Bloom -> @nbits:Nat -> @smallest:Maybe<&2, String> -> @largest:Maybe<&2, String> -> @count:Nat -> @chunks:List<&2, List<&2, 0x4fcd94fa965aa1443134557fd075a483/src/MemTable.Entry>> -> @blocks:List<&2, String> -> Table

type Metadata source · line 87 · raw

Data

Represent Metadata data used by the SSTable indexes, filters, and lookup.

Meta

@smallest:Maybe<&2, String> -> @largest:Maybe<&2, String> -> @count:Nat -> Metadata

Definitions

def block_entries source · line 29 · raw

Nat

Handle the block entries for the SSTable indexes, filters, and lookup.

def chunk_go source · line 33 · raw

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

Handle the chunk go for the SSTable indexes, filters, and lookup.

def chunk source · line 55 · raw

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

Handle chunk in the SSTable indexes, filters, and lookup.

def chunk_head_key source · line 63 · raw

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

Handle the chunk head key for the SSTable indexes, filters, and lookup.

def block_cons_acc source · line 71 · raw

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

Handle the block cons acc for the SSTable indexes, filters, and lookup.

def block_keys source · line 79 · raw

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

Handle the block keys for the SSTable indexes, filters, and lookup.

def bloom_bits source · line 92 · 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 104 · raw

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

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

def u32_byte source · line 120 · 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 124 · raw

@+word:U32 -> Nat

Encode or decode a 32-bit word for to nat exact for the SSTable indexes, filters, and lookup.

def bhash_n_pos source · line 132 · raw

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

Handle bhash n pos in the SSTable indexes, filters, and lookup.

def bhash_n source · line 140 · raw

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

Handle bhash n in the SSTable indexes, filters, and lookup.

def bit_words source · line 149 · 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 157 · raw

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

Handle bit data for new for the SSTable indexes, filters, and lookup.

def bit_set source · line 161 · raw

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

Handle bit set in the SSTable indexes, filters, and lookup.

def bit_get source · line 165 · raw

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

Handle bit get in the SSTable indexes, filters, and lookup.

def bloom_new source · line 169 · raw

@+num:Nat -> Bloom

Handle Bloom filter data for new for the SSTable indexes, filters, and lookup.

def bloom_well_formed source · line 173 · raw

@bloom:Bloom -> Bool

Handle Bloom filter data for well formed for the SSTable indexes, filters, and lookup.

def bloom_add source · line 183 · raw

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

Handle Bloom filter data for add for the SSTable indexes, filters, and lookup.

def both source · line 189 · raw

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

Handle both in the SSTable indexes, filters, and lookup.

def bloom_test source · line 197 · raw

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

Handle Bloom filter data for test for the SSTable indexes, filters, and lookup.

def table_bits source · line 203 · raw

@tab:Table -> Nat

Return the table bits for the SSTable indexes, filters, and lookup.

def maybe_present source · line 209 · raw

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

Handle the optional value for present for the SSTable indexes, filters, and lookup.

def probe_hit_if source · line 216 · 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 224 · raw

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

Count matching probes sequentially.

def probe_count_seq source · line 228 · raw

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

Sequential probe count over a probe list.

def probe_count_par source · line 236 · raw

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

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

def probe_count_bang_gate source · line 242 · raw

@+num:Nat -> Bool

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

def probe_count_pick source · line 246 · 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 254 · raw

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

Size-gated entry point for parallel probe counting.

def bloom_of source · line 258 · raw

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

--- Canonicalization and construction ---

def bloom_union_trees source · line 268 · raw

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

Handle Bloom filter data for union trees for the SSTable indexes, filters, and lookup.

def bloom_union source · line 276 · raw

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

Handle Bloom filter data for union for the SSTable indexes, filters, and lookup.

def bloom_of_chunk source · line 284 · raw

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

Handle Bloom filter data for of chunk for the SSTable indexes, filters, and lookup.

def bloom_of_par source · line 288 · raw

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

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

def chunk_third source · line 295 · raw

@+entries:List<&2, 0x4fcd94fa965aa1443134557fd075a483/src/MemTable.Entry> -> @+skip:Nat -> @+take:Nat -> List<&2, 0x4fcd94fa965aa1443134557fd075a483/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 299 · raw

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

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

def bloom_bang_gate source · line 307 · raw

@+num:Nat -> Bool

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

def bloom_of_pick source · line 311 · raw

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

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

def bloom_of_bang source · line 320 · raw

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

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

Sequential index collection over entries.

def hash_idxs_par_go source · line 342 · raw

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

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

def hash_idxs_par source · line 358 · raw

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

Parallel entry point; fuel covers the fork depth.

def bloom_set_all source · line 363 · raw

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

Sequential assembly of one filter from a flat index list.

def bloom_of_hybrid source · line 373 · raw

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

Hybrid build: parallel hashing, single-tree assembly.

def bloom_pick source · line 385 · raw

@small:Bool -> @+entries:List<&2, 0x4fcd94fa965aa1443134557fd075a483/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 393 · raw

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

Handle Bloom filter data for of auto for the SSTable indexes, filters, and lookup.

def metadata_tail source · line 397 · raw

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

Build table metadata for tail for the SSTable indexes, filters, and lookup.

def metadata source · line 405 · raw

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

Handle metadata in the SSTable indexes, filters, and lookup.

def from_sorted_unique_est_meta source · line 413 · raw

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

Handle from sorted unique est meta in the SSTable indexes, filters, and lookup.

def from_sorted_unique_meta source · line 420 · raw

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

Handle from sorted unique meta in the SSTable indexes, filters, and lookup.

def from_sorted_unique source · line 427 · raw

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

Handle from sorted unique in the SSTable indexes, filters, and lookup.

def build_sorted source · line 431 · raw

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

Build sorted for the SSTable indexes, filters, and lookup.

def build source · line 435 · raw

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

Handle build in the SSTable indexes, filters, and lookup.

def table_smallest source · line 440 · raw

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

Metadata accessors keep clients independent of the Tbl field layout.

def table_largest source · line 446 · raw

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

Return the table largest for the SSTable indexes, filters, and lookup.

def table_count source · line 452 · raw

@tab:Table -> Nat

Return the table count for the SSTable indexes, filters, and lookup.

def opt_name source · line 458 · raw

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

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

def table_id source · line 466 · raw

@tab:Table -> String

Return the table id for the SSTable indexes, filters, and lookup.

def table_bits_from_meta source · line 473 · raw

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

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

Return the table bits build for the SSTable indexes, filters, and lookup.

def ranges_disjoint source · line 494 · raw

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

Check key ranges for disjoint for the SSTable indexes, filters, and lookup.

def size_of source · line 498 · raw

@bloom:Bloom -> Nat

Return the size of of in the SSTable indexes, filters, and lookup.

def bloom_size_stable source · line 504 · raw

@entries:List<&2, 0x4fcd94fa965aa1443134557fd075a483/src/MemTable.Entry> -> @bits:0x4fcd94fa965aa1443134557fd075a483/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 520 · raw

@bt:List<&2, String> -> @ct:List<&2, List<&2, 0x4fcd94fa965aa1443134557fd075a483/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 534 · raw

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

Handle the chunk at go for the SSTable indexes, filters, and lookup.

def chunk_at source · line 548 · raw

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

Handle the chunk at for the SSTable indexes, filters, and lookup.

def block_scan source · line 552 · raw

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

Handle the block scan for the SSTable indexes, filters, and lookup.

def block_pick source · line 556 · raw

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

Handle the block pick for the SSTable indexes, filters, and lookup.

def block_finish source · line 570 · raw

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

Handle the block finish for the SSTable indexes, filters, and lookup.

def hit_finish source · line 582 · raw

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

Resolve the hit for finish for the SSTable indexes, filters, and lookup.

def block_get_hit source · line 594 · raw

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

Handle the block get hit for the SSTable indexes, filters, and lookup.

def block_get source · line 600 · raw

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

Handle the block get for the SSTable indexes, filters, and lookup.

def lookup source · line 606 · raw

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

Handle lookup in the SSTable indexes, filters, and lookup.