src/Db.bend
mylsm-lsm-store@0.5.0.0 · 421 lines · 0 definitions
1import Base
2import mylsm-lsm-store@0.5.0.0/src/Keys.bend as Keys
3import mylsm-lsm-store@0.5.0.0/src/MemTable.bend as MemTable
4import mylsm-lsm-store@0.5.0.0/src/Sstable.bend as Sstable
5import mylsm-lsm-store@0.5.0.0/src/Wal.bend as Wal
6import mylsm-lsm-store@0.5.0.0/src/Manifest.bend as Manifest
7
8# Db API (Task 7): durable write path + reads.
9#
10# Write path (durability ordering, the load-bearing property): encode the
11# batch -> append the WAL -> fsync -> THEN update mem. A crash before fsync
12# loses at most unacked writes (recovery replays the WAL prefix, Task 10).
13# This ordering is a code-review property (no law over IO exists); Task 12
14# fault-injection crashes between each step to verify it empirically.
15# CrashPoint calls are test-only host effects. Unset or unequal checkpoints are
16# successful no-ops; signal delivery and filesystem ordering are not Bend proofs.
17#
18# Read path: mem (newest-first) ++ L0 newest-first ++ L1 ... — first match
19# wins INCLUDING tombstones (MemTable.scan_go freezes), so deletes can never
20# resurrect older versions. Cross-level newest-first order is CORRECT iff
21# Task 9 maintains the L0-drain invariant: compaction always drains ALL of
22# L0 (inputs deleted), so every L0 table is strictly newer than every L1+
23# table; within a level, tables are stored newest-first. Flush (Task 8)
24# Cons'es new tables at the head; compaction (Task 9) preserves the order.
25
26# Represent BEntry data used by the database state and operations.
27type BEntry is Data:
28 BEntry{tab: String, key: String, val: Maybe<&2, String>}
29
30# Return the default batch cap in the database state and operations.
31def default_batch_cap() -> Nat:
32 1n
33
34# Handle bcache bound in the database state and operations.
35def bcache_bound() -> Nat:
36 256n
37
38# manifest_token is the exact serialized Manifest observed by this handle. Flush
39# and compaction compare it before publication to reject stale-handle drift.
40type Db is Data:
41 Db{dir: String, mem: MemTable.MemTable, frozen: MemTable.MemTable, batch_cap: Nat, bcache: List<&2, BEntry>, levels: List<&2, List<&2, Sstable.Table>>, flushed: Nat,
42 manifest_token: String, mem_count: Nat, frozen_count: Nat}
43
44# Rotation result: both tables plus their exact counts, so no pass ever
45# walks a memtable to learn its size. Counts stay exact by construction
46# (open_db starts 0/0; every transition does arithmetic, never List.length).
47type RotRes is Data:
48 Rot{mem: MemTable.MemTable, frozen: MemTable.MemTable, mem_count: Nat, frozen_count: Nat}
49
50# Handle wal path in the database state and operations.
51def wal_path(+dir: String) -> String:
52 dir ++ "/wal.log"
53
54# Open db for the database state and operations.
55def open_db(+dir: String) -> Db:
56 Db{dir, MemTable.empty(), MemTable.empty(), default_batch_cap(), Nil{}, Nil{}, 0n, Manifest.token(Manifest.M{Nil{}}), 0n, 0n}
57
58# --- Pure write core (laws below pin batch == sequential) ---
59
60# Apply mut for the database state and operations.
61def apply_mut(+mem: MemTable.MemTable, +mut: Wal.Mut) -> MemTable.MemTable:
62 match mut:
63 case Wal.Put{key, val}:
64 MemTable.put(mem, key, val)
65 case Wal.Del{key}:
66 MemTable.del(mem, key)
67
68# Apply batch for the database state and operations.
69def apply_batch(+muts: List<&2, Wal.Mut>, +mem: MemTable.MemTable) -> MemTable.MemTable:
70 match muts:
71 case Nil{}:
72 mem
73 case Con{+h, t}:
74 apply_batch(t, apply_mut(mem, h))
75
76# --- Pure read core (concat newest-first, first match wins) ---
77
78# Return the table entries for the database state and operations.
79def table_entries(+tab: Sstable.Table) -> List<&2, MemTable.Entry>:
80 match tab:
81 case Sstable.Tbl{entries, filter, nbits, smallest, largest, count, chunks, blocks}:
82 entries
83
84# Return the level entries for the database state and operations.
85def level_entries(+tabs: List<&2, Sstable.Table>) -> List<&2, MemTable.Entry>:
86 match tabs:
87 case Nil{}:
88 Nil{}
89 case Con{+h, t}:
90 List.append(&2, MemTable.Entry, table_entries(h), level_entries(t))
91
92# Check all level entries for the database state and operations.
93def all_level_entries(+lvls: List<&2, List<&2, Sstable.Table>>) -> List<&2, MemTable.Entry>:
94 match lvls:
95 case Nil{}:
96 Nil{}
97 case Con{+h, t}:
98 List.append(&2, MemTable.Entry, level_entries(h), all_level_entries(t))
99
100# Check all entries for the database state and operations.
101def all_entries(+db: Db) -> List<&2, MemTable.Entry>:
102 match db:
103 case Db{dir, mem, frozen, batch_cap, bcache, levels, flushed, manifest_token, mem_count, frozen_count}:
104 match mem:
105 case MemTable.MT{entries}:
106 List.append(&2, MemTable.Entry, entries, all_level_entries(levels))
107
108# Return the table hit if for the database state and operations.
109def table_hit_if(present: Bool, tab: Sstable.Table, +key: String) -> Maybe<&2, Maybe<&2, String>>:
110 match present:
111 case False{}:
112 None{}
113 case True{}:
114 Sstable.block_get_hit(tab, key)
115
116# Return the table hit for the database state and operations.
117def table_hit(+tab: Sstable.Table, +key: String) -> Maybe<&2, Maybe<&2, String>>:
118 table_hit_if(Sstable.maybe_present(tab, key), tab, key)
119
120# Return the table s hits for the database state and operations.
121def tables_hits(+tabs: List<&2, Sstable.Table>, +key: String) -> List<&2, Maybe<&2, Maybe<&2, String>>>:
122 match tabs:
123 case Nil{}:
124 Nil{}
125 case Con{+h, t}:
126 Con{table_hit(h, key), tables_hits(t, key)}
127
128# Return the level s hits for the database state and operations.
129def levels_hits(+lvls: List<&2, List<&2, Sstable.Table>>, +key: String) -> List<&2, Maybe<&2, Maybe<&2, String>>>:
130 match lvls:
131 case Nil{}:
132 Nil{}
133 case Con{h, t}:
134 List.append(&2, Maybe<&2, Maybe<&2, String>>, tables_hits(h, key), levels_hits(t, key))
135
136# Resolve the hit for s first for the database state and operations.
137def hits_first(+hits: List<&2, Maybe<&2, Maybe<&2, String>>>) -> Maybe<&2, Maybe<&2, String>>:
138 match hits:
139 case Nil{}:
140 None{}
141 case Con{None{}, t}:
142 hits_first(t)
143 case Con{Some{found}, t}:
144 Some{found}
145
146# Flatten opt for the database state and operations.
147def flatten_opt(+opt: Maybe<&2, Maybe<&2, String>>) -> Maybe<&2, String>:
148 match opt:
149 case None{}:
150 None{}
151 case Some{inner}:
152 inner
153
154# Handle db get in the database state and operations.
155def db_get(+db: Db, +key: String) -> Maybe<&2, String>:
156 match db:
157 case Db{dir, mem, frozen, batch_cap, bcache, levels, flushed, manifest_token, mem_count, frozen_count}:
158 flatten_opt(hits_first(Con{MemTable.get_hit(mem, key), Con{MemTable.get_hit(frozen, key), levels_hits(levels, key)}}))
159
160# --- Phase A3: table-identity read cache (assoc-list, bounded FIFO) ---
161# LRU verdict (spike-by-inspection, 2026-09-25): hub lru has no simple public
162# put, reads hand the cache back, and every op needs a W.U64 clock — adopting
163# it threads time through the pure read path and changes db_get's shape for a
164# marginal gain over this list. Custom assoc-list wins; see the Task 3 commit.
165
166# Select hit for the database state and operations.
167def pick_hit(hit: Bool, ans: Maybe<&2, String>, best: Maybe<&2, Maybe<&2, String>>) -> Maybe<&2, Maybe<&2, String>>:
168 match hit:
169 case True{}:
170 Some{ans}
171 case False{}:
172 best
173
174# Handle bcache go in the database state and operations.
175def bcache_go(
176 +cache: List<&2, BEntry>,
177 +tab: String,
178 +key: String,
179 +best: Maybe<&2, Maybe<&2, String>>
180) -> Maybe<&2, Maybe<&2, String>>:
181 match cache:
182 case Nil{}:
183 best
184 case Con{BEntry{t, ky, val}, rest}:
185 bcache_go(rest, tab, key, pick_hit(Bool.and(String.eq(t, tab), String.eq(ky, key)), val, best))
186
187# Handle bcache lookup in the database state and operations.
188def bcache_lookup(+cache: List<&2, BEntry>, +tab: String, +key: String) -> Maybe<&2, Maybe<&2, String>>:
189 bcache_go(cache, tab, key, None{})
190
191# Handle bcache push all in the database state and operations.
192def bcache_push_all(+fresh: List<&2, BEntry>, +old: List<&2, BEntry>) -> List<&2, BEntry>:
193 List.take(&2, BEntry, List.append(&2, BEntry, fresh, old), bcache_bound())
194
195# Probe fill for the database state and operations.
196def probe_fill(
197 hit: Maybe<&2, Maybe<&2, String>>,
198 +tab: String,
199 +key: String
200) -> (Maybe<&2, Maybe<&2, String>> & List<&2, BEntry>):
201 match hit:
202 case None{}:
203 (None{}, Nil{})
204 case Some{+inner}:
205 (Some{inner}, Con{BEntry{tab, key, inner}, Nil{}})
206
207# Probe cached for the database state and operations.
208def probe_cached(
209 cached: Maybe<&2, Maybe<&2, String>>,
210 +tab: Sstable.Table,
211 +key: String
212) -> (Maybe<&2, Maybe<&2, String>> & List<&2, BEntry>):
213 match cached:
214 case None{}:
215 probe_fill(table_hit(tab, key), Sstable.table_id(tab), key)
216 case Some{ans}:
217 (Some{ans}, Nil{})
218
219# Return the table probe for the database state and operations.
220def table_probe(
221 +tab: Sstable.Table,
222 +key: String,
223 +cache: List<&2, BEntry>
224) -> (Maybe<&2, Maybe<&2, String>> & List<&2, BEntry>):
225 probe_cached(bcache_lookup(cache, Sstable.table_id(tab), key), tab, key)
226
227# Return the table s cons for the database state and operations.
228def tables_cons(
229 cur: Maybe<&2, Maybe<&2, String>> & List<&2, BEntry>,
230 rest: List<&2, Maybe<&2, Maybe<&2, String>>> & List<&2, BEntry>
231) -> List<&2, Maybe<&2, Maybe<&2, String>>> & List<&2, BEntry>:
232 match cur:
233 case (hit, delta):
234 match rest:
235 case (rhits, rdelta):
236 (Con{hit, rhits}, List.append(&2, BEntry, delta, rdelta))
237
238# Return the table s walk for the database state and operations.
239def tables_walk(
240 +tabs: List<&2, Sstable.Table>,
241 +key: String,
242 +cache: List<&2, BEntry>
243) -> List<&2, Maybe<&2, Maybe<&2, String>>> & List<&2, BEntry>:
244 match tabs:
245 case Nil{}:
246 (Nil{}, Nil{})
247 case Con{+h, t}:
248 tables_cons(table_probe(h, key, cache), tables_walk(t, key, cache))
249
250# Return the level s cons for the database state and operations.
251def levels_cons(
252 cur: List<&2, Maybe<&2, Maybe<&2, String>>> & List<&2, BEntry>,
253 rest: List<&2, Maybe<&2, Maybe<&2, String>>> & List<&2, BEntry>
254) -> List<&2, Maybe<&2, Maybe<&2, String>>> & List<&2, BEntry>:
255 match cur:
256 case (chits, cdelta):
257 match rest:
258 case (rhits, rdelta):
259 (List.append(&2, Maybe<&2, Maybe<&2, String>>, chits, rhits), List.append(&2, BEntry, cdelta, rdelta))
260
261# Return the level s cached for the database state and operations.
262def levels_cached(
263 +lvls: List<&2, List<&2, Sstable.Table>>,
264 +key: String,
265 +cache: List<&2, BEntry>
266) -> List<&2, Maybe<&2, Maybe<&2, String>>> & List<&2, BEntry>:
267 match lvls:
268 case Nil{}:
269 (Nil{}, Nil{})
270 case Con{+h, t}:
271 levels_cons(tables_walk(h, key, cache), levels_cached(t, key, cache))
272
273# Read the cached levels for the database state and operations.
274def cached_levels(
275 lr: List<&2, Maybe<&2, Maybe<&2, String>>> & List<&2, BEntry>,
276 +dir: String,
277 +mem: MemTable.MemTable,
278 +frozen: MemTable.MemTable,
279 +batch_cap: Nat,
280 +bcache: List<&2, BEntry>,
281 +levels: List<&2, List<&2, Sstable.Table>>,
282 +flushed: Nat,
283 +manifest_token: String,
284 +mem_count: Nat,
285 +frozen_count: Nat
286) -> Db & Maybe<&2, String>:
287 match lr:
288 case (hits, delta):
289 (Db{dir, mem, frozen, batch_cap, bcache_push_all(delta, bcache), levels, flushed, manifest_token, mem_count, frozen_count}, flatten_opt(hits_first(hits)))
290
291# Read the cached frozen for the database state and operations.
292def cached_frozen(
293 fhit: Maybe<&2, Maybe<&2, String>>,
294 +dir: String,
295 +mem: MemTable.MemTable,
296 +frozen: MemTable.MemTable,
297 +batch_cap: Nat,
298 +bcache: List<&2, BEntry>,
299 +levels: List<&2, List<&2, Sstable.Table>>,
300 +flushed: Nat,
301 +manifest_token: String,
302 +key: String,
303 +mem_count: Nat,
304 +frozen_count: Nat
305) -> Db & Maybe<&2, String>:
306 match fhit:
307 case Some{found}:
308 (Db{dir, mem, frozen, batch_cap, bcache, levels, flushed, manifest_token, mem_count, frozen_count}, flatten_opt(Some{found}))
309 case None{}:
310 cached_levels(levels_cached(levels, key, bcache), dir, mem, frozen, batch_cap, bcache, levels, flushed, manifest_token, mem_count, frozen_count)
311
312# Read the cached mem for the database state and operations.
313def cached_mem(
314 mhit: Maybe<&2, Maybe<&2, String>>,
315 +dir: String,
316 +mem: MemTable.MemTable,
317 +frozen: MemTable.MemTable,
318 +batch_cap: Nat,
319 +bcache: List<&2, BEntry>,
320 +levels: List<&2, List<&2, Sstable.Table>>,
321 +flushed: Nat,
322 +manifest_token: String,
323 +key: String,
324 +mem_count: Nat,
325 +frozen_count: Nat
326) -> Db & Maybe<&2, String>:
327 match mhit:
328 case Some{found}:
329 (Db{dir, mem, frozen, batch_cap, bcache, levels, flushed, manifest_token, mem_count, frozen_count}, flatten_opt(Some{found}))
330 case None{}:
331 cached_frozen(MemTable.get_hit(frozen, key), dir, mem, frozen, batch_cap, bcache, levels, flushed, manifest_token, key, mem_count, frozen_count)
332
333# Handle db get cached in the database state and operations.
334def db_get_cached(+db: Db, +key: String) -> Db & Maybe<&2, String>:
335 match db:
336 case Db{dir, +mem, +frozen, +batch_cap, +bcache, +levels, +flushed, +manifest_token, +mem_count, +frozen_count}:
337 cached_mem(MemTable.get_hit(mem, key), dir, mem, frozen, batch_cap, bcache, levels, flushed, manifest_token, key, mem_count, frozen_count)
338
339# Handle batch len in the database state and operations.
340def batch_len(+muts: List<&2, Wal.Mut>) -> Nat:
341 List.length(&2, Wal.Mut, muts)
342
343# Rotate cnt for the database state and operations.
344def rotate_cnt(full: Bool, +grown: MemTable.MemTable, +frozen: MemTable.MemTable, +count: Nat, +fcount: Nat) -> RotRes:
345 match full:
346 case True{}:
347 Rot{MemTable.empty(), grown, 0n, count}
348 case False{}:
349 Rot{grown, frozen, count, fcount}
350
351# Handle frozen empty in the database state and operations.
352def frozen_empty(+frozen: MemTable.MemTable) -> Bool:
353 match frozen:
354 case MemTable.MT{entries}:
355 match entries:
356 case Nil{}:
357 True{}
358 case Con{_, _}:
359 False{}
360
361# Rotate after for the database state and operations.
362def rotate_after(+grown: MemTable.MemTable, +frozen: MemTable.MemTable, +count: Nat, +fcount: Nat) -> RotRes:
363 rotate_cnt(Bool.and(Nat.is_le(4096n, count), frozen_empty(frozen)), grown, frozen, count, fcount)
364
365# Apply and rotate for the database state and operations.
366def apply_and_rotate(
367 +muts: List<&2, Wal.Mut>,
368 +mem: MemTable.MemTable,
369 +frozen: MemTable.MemTable,
370 +mem_count: Nat,
371 +frozen_count: Nat
372) -> RotRes:
373 rotate_after(apply_batch(muts, mem), frozen, Nat.add(mem_count, batch_len(muts)), frozen_count)
374
375# Apply done for the database state and operations.
376def apply_done(
377 res: RotRes,
378 +dir: String,
379 +batch_cap: Nat,
380 +bcache: List<&2, BEntry>,
381 +levels: List<&2, List<&2, Sstable.Table>>,
382 +flushed: Nat,
383 +manifest_token: String
384) -> Db:
385 match res:
386 case Rot{mem2, frozen2, mc, fc}:
387 Db{dir, mem2, frozen2, batch_cap, bcache, levels, flushed, manifest_token, mc, fc}
388
389# Handle rot done in the database state and operations.
390def rot_done(
391 res: RotRes,
392 +dir: String,
393 +batch_cap: Nat,
394 +bcache: List<&2, BEntry>,
395 +levels: List<&2, List<&2, Sstable.Table>>,
396 +flushed: Nat,
397 +manifest_token: String
398) -> Result<&1, &1, U32 & String, Db>:
399 Done{apply_done(res, dir, batch_cap, bcache, levels, flushed, manifest_token)}
400
401# Handle batch cap of in the database state and operations.
402def batch_cap_of(+db: Db) -> Nat:
403 match db:
404 case Db{dir, mem, frozen, batch_cap, bcache, levels, flushed, manifest_token, mem_count, frozen_count}:
405 batch_cap
406
407# Handle with batch cap in the database state and operations.
408def with_batch_cap(+db: Db, +cap: Nat) -> Db:
409 match db:
410 case Db{dir, mem, frozen, batch_cap, bcache, levels, flushed, manifest_token, mem_count, frozen_count}:
411 Db{dir, mem, frozen, cap, bcache, levels, flushed, manifest_token, mem_count, frozen_count}
412
413# Stage d muts for the database state and operations.
414def staged_muts(+staged: List<&2, Wal.Batch>) -> List<&2, Wal.Mut>:
415 match staged:
416 case Nil{}:
417 Nil{}
418 case Con{Wal.Batch{muts}, t}:
419 List.append(&2, Wal.Mut, muts, staged_muts(t))
420
421# --- Closed-vector laws live in laws/Db.bend (spec laws 1, 2, 3, 7) ---