~/bend-docscommunity

src/Sstable.bend fails

raw source on the hub · import mylsm-lsm-store@0.3.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 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, 0x8bf6d41adbe0e67e438f6cdc25a6cb6e/src/MemTable.Entry> -> @+cur:List<&2, 0x8bf6d41adbe0e67e438f6cdc25a6cb6e/src/MemTable.Entry> -> @room:Nat -> @acc:List<&2, List<&2, 0x8bf6d41adbe0e67e438f6cdc25a6cb6e/src/MemTable.Entry>> -> List<&2, List<&2, 0x8bf6d41adbe0e67e438f6cdc25a6cb6e/src/MemTable.Entry>>

def chunk source · line 44 · raw

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

def chunk_head_key source · line 51 · raw

@+xs:List<&2, 0x8bf6d41adbe0e67e438f6cdc25a6cb6e/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, 0x8bf6d41adbe0e67e438f6cdc25a6cb6e/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 -> 0x8bf6d41adbe0e67e438f6cdc25a6cb6e/src/BitTree.BitTree

def bit_set source · line 141 · raw

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

def bit_get source · line 144 · raw

@idx:Nat -> @bits:0x8bf6d41adbe0e67e438f6cdc25a6cb6e/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 bloom_of source · line 187 · raw

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

--- Canonicalization and construction ---

def metadata_tail source · line 196 · raw

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

def metadata source · line 203 · raw

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

def from_sorted_unique_est_meta source · line 210 · raw

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

def from_sorted_unique_meta source · line 216 · raw

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

def from_sorted_unique source · line 222 · raw

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

def build_sorted source · line 225 · raw

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

def build source · line 228 · raw

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

def table_smallest source · line 233 · raw

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

Metadata accessors keep clients independent of the Tbl field layout.

def table_largest source · line 238 · raw

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

def table_count source · line 243 · raw

@tab:Table -> Nat

def opt_name source · line 249 · raw

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

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

def table_id source · line 256 · raw

@tab:Table -> String

def table_bits_from_meta source · line 263 · raw

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

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

def ranges_disjoint source · line 282 · raw

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

def size_of source · line 285 · raw

@bloom:Bloom -> Nat

def bloom_size_stable source · line 291 · raw

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

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

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

def chunk_at source · line 329 · raw

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

def block_scan source · line 332 · raw

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

def block_pick source · line 335 · raw

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

def block_finish source · line 344 · raw

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

def hit_finish source · line 351 · raw

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

def block_get_hit source · line 358 · raw

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

def block_get source · line 363 · raw

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

def lookup source · line 368 · raw

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