1	import Base
2	import ./Keys.bend as Keys
3	import ./MemTable.bend as MemTable
4	import ./Sstable.bend as Sstable
5	import ./Wal.bend as Wal
6	import ./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.
27	type 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.
31	def default_batch_cap() -> Nat:
32	  1n
33	
34	# Handle bcache bound in the database state and operations.
35	def 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.
40	type 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).
47	type 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.
51	def wal_path(+dir: String) -> String:
52	  dir ++ "/wal.log"
53	
54	# Open db for the database state and operations.
55	def 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.
61	def 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.
69	def 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.
79	def 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.
85	def 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.
93	def 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.
101	def 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.
109	def 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.
117	def 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.
121	def 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.
129	def 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.
137	def 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.
147	def 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.
155	def 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.
167	def 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.
175	def 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.
188	def 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.
192	def 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.
196	def 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.
208	def 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.
220	def 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.
228	def 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.
239	def 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.
251	def 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.
262	def 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.
274	def 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.
292	def 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.
313	def 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.
334	def 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.
340	def 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.
344	def 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.
352	def 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.
362	def 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.
366	def 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.
376	def 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.
390	def 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.
402	def 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.
408	def 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.
414	def 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) ---