src/Sstable.bend
mylsm-lsm-store@0.3.0.0 · 369 lines · 0 definitions
1import Base
2import mylsm-lsm-store@0.3.0.0/src/Keys.bend as Keys
3import mylsm-lsm-store@0.3.0.0/src/MemTable.bend as MemTable
4import mylsm-lsm-store@0.3.0.0/src/BitTree.bend as BitTree
5import mylsm-lsm-store@0.3.0.0/src/SortedRun.bend as SortedRun
6
7# SSTables (Task 4): immutable strict sorted runs with BitTree Bloom filters.
8# `build` canonicalizes newest-first raw entries; `from_sorted_unique` trusts an
9# already strict, unique run and deliberately performs no sorting.
10
11type Bloom is Data:
12 Blm{bits: BitTree.BitTree, size: Nat}
13
14type Table is Data:
15 Tbl{
16 entries: List<&2, MemTable.Entry>,
17 filter: Bloom,
18 nbits: Nat,
19 smallest: Maybe<&2, String>,
20 largest: Maybe<&2, String>,
21 count: Nat,
22 chunks: List<&2, List<&2, MemTable.Entry>>,
23 blocks: List<&2, String>
24 }
25
26def block_entries() -> Nat:
27 64n
28
29def chunk_go(fuel: Nat, +entries: List<&2, MemTable.Entry>, +cur: List<&2, MemTable.Entry>, room: Nat, acc: List<&2, List<&2, MemTable.Entry>>) -> List<&2, List<&2, MemTable.Entry>>:
30 match fuel:
31 case 0n:
32 List.reverse(&2, List<&2, MemTable.Entry>, Con{List.reverse(&2, MemTable.Entry, cur), acc})
33 case 1n+f:
34 match entries:
35 case Nil{}:
36 List.reverse(&2, List<&2, MemTable.Entry>, Con{List.reverse(&2, MemTable.Entry, cur), acc})
37 case Con{e, t}:
38 match room:
39 case 0n:
40 chunk_go(f, t, Con{e, Nil{}}, Nat.sub(block_entries(), 1n), Con{List.reverse(&2, MemTable.Entry, cur), acc})
41 case 1n+r:
42 chunk_go(f, t, Con{e, cur}, r, acc)
43
44def chunk(+entries: List<&2, MemTable.Entry>) -> List<&2, List<&2, MemTable.Entry>>:
45 match entries:
46 case Nil{}:
47 Nil{}
48 case Con{e, t}:
49 chunk_go(List.length(&2, MemTable.Entry, entries), t, Con{e, Nil{}}, Nat.sub(block_entries(), 1n), Nil{})
50
51def chunk_head_key(+xs: List<&2, MemTable.Entry>) -> Maybe<&2, String>:
52 match xs:
53 case Nil{}:
54 None{}
55 case Con{MemTable.Entry{key, val}, t}:
56 Some{key}
57
58def block_cons_acc(head: Maybe<&2, String>, acc: List<&2, String>) -> List<&2, String>:
59 match head:
60 case None{}:
61 acc
62 case Some{k}:
63 Con{k, acc}
64
65def block_keys(+chunks: List<&2, List<&2, MemTable.Entry>>, acc: List<&2, String>) -> List<&2, String>:
66 match chunks:
67 case Nil{}:
68 List.reverse(&2, String, acc)
69 case Con{c, t}:
70 block_keys(t, block_cons_acc(chunk_head_key(c), acc))
71
72type Metadata is Data:
73 Meta{smallest: Maybe<&2, String>, largest: Maybe<&2, String>, count: Nat}
74
75# --- Bloom allocator (Monkey-style: smaller/upper levels get more bits) ---
76# Closed form pinned here; Dayan-exact coefficients are tuning follow-up.
77def bloom_bits(level: Nat, est_keys: Nat) -> Nat:
78 match level:
79 case 0n:
80 Nat.mul(est_keys, 20n)
81 case 1n+m:
82 match m:
83 case 0n:
84 Nat.mul(est_keys, 10n)
85 case 1n+p:
86 Nat.mul(est_keys, 5n)
87
88# --- Local byte hash (kept stable for on-disk/rebuild compatibility) ---
89def bhash(str: String, acc: U32) -> U32:
90 match str:
91 case SNil{}:
92 acc
93 case SCon{c, t}:
94 bhash(t, U32.add(U32.mul(acc, 31), Char.to_u32(c)))
95
96# --- U32->Nat bridges that stay checker-tractable ---
97# The Bend checker does not share across sequentially-chained U32.mul terms:
98# `U32.to_nat` applied to a hash accumulated over 4+ bytes diverges in
99# `{==}` elaboration (runtime is unaffected). The bridges below therefore
100# never materialize a chained U32 as a Nat: each `to_nat` covers at most two
101# U32 ops (shift+mask on the ORIGINAL word — parallel, shared), and all
102# accumulation happens in small-Nat land. Both are EXACT (no semantic
103# change): bytes are the base-256 digits of the word (Horner), so
104# u32_to_nat_exact(w) == U32.to_nat(w) and bhash_n computes the same mod.
105def u32_byte(+word: U32, shift: Nat) -> Nat:
106 U32.to_nat(U32.and(U32.shrn(word, shift), 255))
107
108def u32_to_nat_exact(+word: U32) -> Nat:
109 +b0 = u32_byte(word, 24n)
110 +b1 = u32_byte(word, 16n)
111 +b2 = u32_byte(word, 8n)
112 +b3 = u32_byte(word, 0n)
113 Nat.add(Nat.mul(b0, Nat.mul(Nat.mul(256n, 256n), 256n)), Nat.add(Nat.mul(b1, Nat.mul(256n, 256n)), Nat.add(Nat.mul(b2, 256n), b3)))
114
115def bhash_n_pos(+str: String, +seed: U32, +mod: Nat) -> Nat:
116 +w = bhash(str, seed)
117 +a0 = Nat.mod(u32_byte(w, 24n), mod)
118 +a1 = Nat.mod(Nat.add(Nat.mul(a0, 256n), u32_byte(w, 16n)), mod)
119 +a2 = Nat.mod(Nat.add(Nat.mul(a1, 256n), u32_byte(w, 8n)), mod)
120 Nat.mod(Nat.add(Nat.mul(a2, 256n), u32_byte(w, 0n)), mod)
121
122def bhash_n(str: String, seed: U32, mod: Nat) -> Nat:
123 match mod:
124 case 0n:
125 0n
126 case 1n+p:
127 bhash_n_pos(str, seed, mod)
128
129# BitTree stores whole U32 words while Bloom.size preserves the exact logical
130# bit count selected by bloom_bits.
131def bit_words(num: Nat) -> Nat:
132 match num:
133 case 0n:
134 0n
135 case 1n+m:
136 Nat.add(1n, Nat.div(m, 32n))
137
138def bits_new(+num: Nat) -> BitTree.BitTree:
139 BitTree.new(bit_words(num))
140
141def bit_set(idx: Nat, bits: BitTree.BitTree) -> BitTree.BitTree:
142 BitTree.set(bits, idx)
143
144def bit_get(idx: Nat, bits: BitTree.BitTree) -> Bool:
145 BitTree.test(bits, idx)
146
147def bloom_new(+num: Nat) -> Bloom:
148 Blm{bits_new(num), num}
149
150def bloom_well_formed(bloom: Bloom) -> Bool:
151 match bloom:
152 case Blm{+bits, +size}:
153 Bool.and(
154 BitTree.well_formed(bits),
155 Bool.and(
156 Nat.is_eq(BitTree.word_count(bits), bit_words(size)),
157 Nat.is_le(size, BitTree.bit_count(bits))))
158
159def bloom_add(bloom: Bloom, +key: String) -> Bloom:
160 match bloom:
161 case Blm{bits, +size}:
162 Blm{bit_set(bhash_n(key, 17, size), bit_set(bhash_n(key, 257, size), bits)), size}
163
164def both(lhs: Bool, rhs: Bool) -> Bool:
165 match lhs:
166 case True{}:
167 rhs
168 case False{}:
169 False{}
170
171def bloom_test(bloom: Bloom, +key: String) -> Bool:
172 match bloom:
173 case Blm{+bits, +size}:
174 both(bit_get(bhash_n(key, 17, size), bits), bit_get(bhash_n(key, 257, size), bits))
175
176def table_bits(tab: Table) -> Nat:
177 match tab:
178 case Tbl{entries, filter, nbits, smallest, largest, count, chunks, blocks}:
179 nbits
180
181def maybe_present(tab: Table, +key: String) -> Bool:
182 match tab:
183 case Tbl{entries, filter, nbits, smallest, largest, count, chunks, blocks}:
184 bloom_test(filter, key)
185
186# --- Canonicalization and construction ---
187def bloom_of(entries: List<&2, MemTable.Entry>, +blm: Bloom) -> Bloom:
188 match entries:
189 case Nil{}:
190 blm
191 case Con{e, t}:
192 match e:
193 case MemTable.Entry{key, val}:
194 bloom_of(t, bloom_add(blm, key))
195
196def metadata_tail(entries: List<&2, MemTable.Entry>, +first: String, last: String, +count: Nat) -> Metadata:
197 match entries:
198 case Nil{}:
199 Meta{Some{first}, Some{last}, count}
200 case Con{MemTable.Entry{key, val}, rest}:
201 metadata_tail(rest, first, key, Nat.add(count, 1n))
202
203def metadata(entries: List<&2, MemTable.Entry>) -> Metadata:
204 match entries:
205 case Nil{}:
206 Meta{None{}, None{}, 0n}
207 case Con{MemTable.Entry{+key, val}, rest}:
208 metadata_tail(rest, key, key, 1n)
209
210def from_sorted_unique_est_meta(+entries: List<&2, MemTable.Entry>, level: Nat, est_keys: Nat, meta: Metadata) -> Table:
211 match meta:
212 case Meta{smallest, largest, count}:
213 +nb = bloom_bits(level, est_keys)
214 Tbl{entries, bloom_of(entries, bloom_new(nb)), nb, smallest, largest, count, chunk(entries), block_keys(chunk(entries), Nil{})}
215
216def from_sorted_unique_meta(+entries: List<&2, MemTable.Entry>, level: Nat, meta: Metadata) -> Table:
217 match meta:
218 case Meta{smallest, largest, +count}:
219 +nb = bloom_bits(level, count)
220 Tbl{entries, bloom_of(entries, bloom_new(nb)), nb, smallest, largest, count, chunk(entries), block_keys(chunk(entries), Nil{})}
221
222def from_sorted_unique(+entries: List<&2, MemTable.Entry>, level: Nat) -> Table:
223 from_sorted_unique_meta(entries, level, metadata(entries))
224
225def build_sorted(+entries: List<&2, MemTable.Entry>, level: Nat, est_keys: Nat) -> Table:
226 from_sorted_unique_est_meta(entries, level, est_keys, metadata(entries))
227
228def build(+entries: List<&2, MemTable.Entry>, level: Nat, est_keys: Nat) -> Table:
229 +effective = Nat.max(est_keys, List.length(&2, MemTable.Entry, entries))
230 build_sorted(SortedRun.sort_newest(entries), level, effective)
231
232# Metadata accessors keep clients independent of the Tbl field layout.
233def table_smallest(tab: Table) -> Maybe<&2, String>:
234 match tab:
235 case Tbl{entries, filter, nbits, smallest, largest, count, chunks, blocks}:
236 smallest
237
238def table_largest(tab: Table) -> Maybe<&2, String>:
239 match tab:
240 case Tbl{entries, filter, nbits, smallest, largest, count, chunks, blocks}:
241 largest
242
243def table_count(tab: Table) -> Nat:
244 match tab:
245 case Tbl{entries, filter, nbits, smallest, largest, count, chunks, blocks}:
246 count
247
248# Total table identity for the read cache: smallest|largest|count.
249def opt_name(+opt: Maybe<&2, String>) -> String:
250 match opt:
251 case None{}:
252 "<none>"
253 case Some{s}:
254 s
255
256def table_id(tab: Table) -> String:
257 match tab:
258 case Tbl{entries, filter, nbits, smallest, largest, count, chunks, blocks}:
259 opt_name(smallest) ++ "|" ++ opt_name(largest) ++ "|" ++ Nat.show(count)
260
261# Open bridge: metadata is matched explicitly so the Bloom schedule projects
262# through `build` without relying on reduction of an open entry list.
263def table_bits_from_meta(
264 +entries: List<&2, MemTable.Entry>,
265 level: Nat,
266 est_keys: Nat,
267 meta: Metadata,
268) -> {table_bits(from_sorted_unique_est_meta(entries, level, est_keys, meta)) == bloom_bits(level, est_keys) : Nat}:
269 match meta:
270 case Meta{smallest, largest, count}:
271 {==}
272
273def table_bits_build(
274 +entries: List<&2, MemTable.Entry>,
275 level: Nat,
276 est_keys: Nat,
277) -> {table_bits(build(entries, level, est_keys)) == bloom_bits(level, Nat.max(est_keys, List.length(&2, MemTable.Entry, entries))) : Nat}:
278 +effective = Nat.max(est_keys, List.length(&2, MemTable.Entry, entries))
279 table_bits_from_meta(SortedRun.sort_newest(entries), level, effective, metadata(SortedRun.sort_newest(entries)))
280
281
282def ranges_disjoint(+ta: Table, +tb: Table) -> Bool:
283 SortedRun.range_disjoint_bounds(table_smallest(ta), table_largest(ta), table_smallest(tb), table_largest(tb))
284
285def size_of(bloom: Bloom) -> Nat:
286 match bloom:
287 case Blm{bits, size}:
288 size
289
290# Bloom insertions only set tree bits and preserve the exact logical size.
291def bloom_size_stable(entries: List<&2, MemTable.Entry>, bits: BitTree.BitTree, +size: Nat) -> {size_of(bloom_of(entries, Blm{bits, size})) == size : Nat}:
292 match entries:
293 case Nil{}:
294 {==}
295 case Con{e, t}:
296 match e:
297 case MemTable.Entry{+key, val}:
298 bloom_size_stable(t, bit_set(bhash_n(key, 17, size), bit_set(bhash_n(key, 257, size), bits)), size)
299
300# Block-scoped lookup. Checker constraints (proven by scratch experiments):
301# multi-scrutinee matches follow declaration order, and only Nat answers flow
302# through match arms — so selection returns an index, picked up by chunk_at_go.
303def pick_ix(bt: List<&2, String>, ct: List<&2, List<&2, MemTable.Entry>>, ix: Nat, +key: String, order: Cmp) -> Nat:
304 match bt ct order:
305 case _ _ GT{}:
306 Nat.sub(ix, 1n)
307 case Nil{} _ _:
308 ix
309 case _ Nil{} _:
310 ix
311 case Con{b2, bt2} Con{d2, ct2} LT{}:
312 pick_ix(bt2, ct2, Nat.add(ix, 1n), key, Keys.cmp(b2, key))
313 case Con{b2, bt2} Con{d2, ct2} EQ{}:
314 ix
315
316def chunk_at_go(fuel: Nat, +chunks: List<&2, List<&2, MemTable.Entry>>, ix: Nat) -> List<&2, MemTable.Entry>:
317 match fuel chunks:
318 case 0n _:
319 Nil{}
320 case 1n+f Nil{}:
321 Nil{}
322 case 1n+f Con{c, t}:
323 match ix:
324 case 0n:
325 c
326 case 1n+p:
327 chunk_at_go(f, t, p)
328
329def chunk_at(+chunks: List<&2, List<&2, MemTable.Entry>>, ix: Nat) -> List<&2, MemTable.Entry>:
330 chunk_at_go(List.length(&2, List<&2, MemTable.Entry>, chunks), chunks, ix)
331
332def block_scan(+chunk: List<&2, MemTable.Entry>, +key: String) -> Maybe<&2, String>:
333 MemTable.get(MemTable.MT{chunk}, key)
334
335def block_pick(+chunks: List<&2, List<&2, MemTable.Entry>>, +blocks: List<&2, String>, +key: String) -> List<&2, MemTable.Entry>:
336 match chunks blocks:
337 case Nil{} _:
338 Nil{}
339 case _ Nil{}:
340 Nil{}
341 case Con{c, ct} Con{b, bt}:
342 chunk_at(chunks, pick_ix(bt, ct, 0n, key, Keys.cmp(b, key)))
343
344def block_finish(picked: List<&2, MemTable.Entry>, +entries: List<&2, MemTable.Entry>, +key: String) -> Maybe<&2, String>:
345 match picked:
346 case Nil{}:
347 MemTable.get(MemTable.MT{entries}, key)
348 case Con{e, t}:
349 block_scan(Con{e, t}, key)
350
351def hit_finish(picked: List<&2, MemTable.Entry>, +entries: List<&2, MemTable.Entry>, +key: String) -> Maybe<&2, Maybe<&2, String>>:
352 match picked:
353 case Nil{}:
354 MemTable.get_hit(MemTable.MT{entries}, key)
355 case Con{e, t}:
356 MemTable.get_hit(MemTable.MT{Con{e, t}}, key)
357
358def block_get_hit(tab: Table, +key: String) -> Maybe<&2, Maybe<&2, String>>:
359 match tab:
360 case Tbl{entries, filter, nbits, smallest, largest, count, chunks, blocks}:
361 hit_finish(block_pick(chunks, blocks, key), entries, key)
362
363def block_get(tab: Table, +key: String) -> Maybe<&2, String>:
364 match tab:
365 case Tbl{entries, filter, nbits, smallest, largest, count, chunks, blocks}:
366 block_finish(block_pick(chunks, blocks, key), entries, key)
367
368def lookup(tab: Table, +key: String) -> Maybe<&2, String>:
369 block_get(tab, key)