src/SortedRun.bend
mylsm-lsm-store@0.5.0.0 · 455 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
4
5# Pure reference semantics and stable sorted-run merging. This module stays
6# independent of Sstable so table construction can depend on it later.
7
8# Evaluate not for the sorted-run operations.
9def bool_not(rhs: Bool) -> Bool:
10 match rhs:
11 case False{}:
12 True{}
13 case True{}:
14 False{}
15
16# Evaluate and for the sorted-run operations.
17def bool_and(lhs: Bool, rhs: Bool) -> Bool:
18 match lhs:
19 case False{}:
20 False{}
21 case True{}:
22 rhs
23
24# Evaluate or for the sorted-run operations.
25def bool_or(lhs: Bool, rhs: Bool) -> Bool:
26 match lhs:
27 case False{}:
28 rhs
29 case True{}:
30 True{}
31
32# Handle the entry cmp for the sorted-run operations.
33def entry_cmp(e1: MemTable.Entry, e2: MemTable.Entry) -> Cmp:
34 match e1:
35 case MemTable.Entry{k1, v1}:
36 match e2:
37 case MemTable.Entry{k2, v2}:
38 Keys.cmp(k1, k2)
39
40# Handle the entry key eq for the sorted-run operations.
41def entry_key_eq(entry: MemTable.Entry, +key: String) -> Bool:
42 match entry:
43 case MemTable.Entry{k, v}:
44 Keys.eq(k, key)
45
46# --- Reference predicates and observable model ---
47
48# Check membership for whether key holds for the sorted-run operations.
49def contains_key(+entry: MemTable.Entry, entries: List<&2, MemTable.Entry>) -> Bool:
50 match entry:
51 case MemTable.Entry{+key, val}:
52 match entries:
53 case Nil{}:
54 False{}
55 case Con{h, t}:
56 bool_or(entry_key_eq(h, key), contains_key(MemTable.Entry{key, val}, t))
57
58# Check whether unique holds for the sorted-run operations.
59def is_unique(entries: List<&2, MemTable.Entry>) -> Bool:
60 match entries:
61 case Nil{}:
62 True{}
63 case Con{+h, +t}:
64 bool_and(bool_not(contains_key(h, t)), is_unique(t))
65
66# Check whether strict holds for the sorted-run operations.
67def is_strict(entries: List<&2, MemTable.Entry>) -> Bool:
68 match entries:
69 case Nil{}:
70 True{}
71 case Con{h, Nil{}}:
72 True{}
73 case Con{+h, Con{+next, +rest}}:
74 bool_and(Keys.cmp_is_lt(entry_cmp(h, next)), is_strict(Con{next, rest}))
75
76# Resolve step for the sorted-run operations.
77def resolve_step(
78 done: Bool,
79 hit: Bool,
80 val: Maybe<&2, String>,
81 ans: Maybe<&2, Maybe<&2, String>>
82) -> Bool & Maybe<&2, Maybe<&2, String>>:
83 match done:
84 case True{}:
85 (True{}, ans)
86 case False{}:
87 match hit:
88 case True{}:
89 (True{}, Some{val})
90 case False{}:
91 (False{}, ans)
92
93# Resolve state for the sorted-run operations.
94def resolve_state(
95 entries: List<&2, MemTable.Entry>,
96 +key: String,
97 state: Bool & Maybe<&2, Maybe<&2, String>>
98) -> Bool & Maybe<&2, Maybe<&2, String>>:
99 match entries:
100 case Nil{}:
101 state
102 case Con{MemTable.Entry{k, val}, t}:
103 (done, ans) = state
104 resolve_state(t, key, resolve_step(done, Keys.eq(k, key), val, ans))
105
106# Resolve answer for the sorted-run operations.
107def resolve_answer(state: Bool & Maybe<&2, Maybe<&2, String>>) -> Maybe<&2, Maybe<&2, String>>:
108 match state:
109 case (done, ans):
110 ans
111
112# Handle resolve in the sorted-run operations.
113def resolve(entries: List<&2, MemTable.Entry>, key: String) -> Maybe<&2, Maybe<&2, String>>:
114 resolve_answer(resolve_state(entries, key, (False{}, None{})))
115
116# Resolve newest go for the sorted-run operations.
117def resolve_newest_go(
118 runs: List<&2, List<&2, MemTable.Entry>>,
119 +key: String,
120 state: Bool & Maybe<&2, Maybe<&2, String>>
121) -> Bool & Maybe<&2, Maybe<&2, String>>:
122 match runs:
123 case Nil{}:
124 state
125 case Con{run, rest}:
126 resolve_newest_go(rest, key, resolve_state(run, key, state))
127
128# Resolve newest for the sorted-run operations.
129def resolve_newest(runs: List<&2, List<&2, MemTable.Entry>>, key: String) -> Maybe<&2, Maybe<&2, String>>:
130 resolve_answer(resolve_newest_go(runs, key, (False{}, None{})))
131
132
133# Run s well formed for the sorted-run operations.
134def runs_well_formed(runs: List<&2, List<&2, MemTable.Entry>>) -> Bool:
135 match runs:
136 case Nil{}:
137 True{}
138 case Con{+run, rest}:
139 bool_and(bool_and(is_strict(run), is_unique(run)), runs_well_formed(rest))
140
141# L1 helpers operate on entry runs to avoid a SortedRun <-> Sstable cycle.
142def first_key(entries: List<&2, MemTable.Entry>) -> Maybe<&2, String>:
143 match entries:
144 case Nil{}:
145 None{}
146 case Con{MemTable.Entry{key, val}, t}:
147 Some{key}
148
149# Return the last key go in the sorted-run operations.
150def last_key_go(entries: List<&2, MemTable.Entry>, last: String) -> Maybe<&2, String>:
151 match entries:
152 case Nil{}:
153 Some{last}
154 case Con{MemTable.Entry{key, val}, t}:
155 last_key_go(t, key)
156
157# Return the last key in the sorted-run operations.
158def last_key(entries: List<&2, MemTable.Entry>) -> Maybe<&2, String>:
159 match entries:
160 case Nil{}:
161 None{}
162 case Con{MemTable.Entry{key, val}, t}:
163 last_key_go(t, key)
164
165# Handle range disjoint bounds in the sorted-run operations.
166def range_disjoint_bounds(
167 af: Maybe<&2, String>,
168 al: Maybe<&2, String>,
169 bf: Maybe<&2, String>,
170 bl: Maybe<&2, String>
171) -> Bool:
172 match af al bf bl:
173 case None{} _ _ _:
174 True{}
175 case _ None{} _ _:
176 True{}
177 case _ _ None{} _:
178 True{}
179 case _ _ _ None{}:
180 True{}
181 case Some{a_first} Some{a_last} Some{b_first} Some{b_last}:
182 bool_or(Keys.lt(a_last, b_first), Keys.lt(b_last, a_first))
183
184# Handle range disjoint in the sorted-run operations.
185def range_disjoint(+xs: List<&2, MemTable.Entry>, +ys: List<&2, MemTable.Entry>) -> Bool:
186 range_disjoint_bounds(first_key(xs), last_key(xs), first_key(ys), last_key(ys))
187
188# Check disjointness of whether with holds for the sorted-run operations.
189def disjoint_with(+run: List<&2, MemTable.Entry>, runs: List<&2, List<&2, MemTable.Entry>>) -> Bool:
190 match runs:
191 case Nil{}:
192 True{}
193 case Con{+h, t}:
194 bool_and(range_disjoint(run, h), disjoint_with(run, t))
195
196# Handle pairwise disjoint in the sorted-run operations.
197def pairwise_disjoint(runs: List<&2, List<&2, MemTable.Entry>>) -> Bool:
198 match runs:
199 case Nil{}:
200 True{}
201 case Con{+h, +t}:
202 bool_and(disjoint_with(h, t), pairwise_disjoint(t))
203
204# Return the level disjoint for the sorted-run operations.
205def level_disjoint(+runs: List<&2, List<&2, MemTable.Entry>>) -> Bool:
206 bool_and(runs_well_formed(runs), pairwise_disjoint(runs))
207
208# Return the level s well formed for the sorted-run operations.
209def levels_well_formed(levels: List<&2, List<&2, List<&2, MemTable.Entry>>>) -> Bool:
210 match levels:
211 case Nil{}:
212 True{}
213 case Con{+level, rest}:
214 bool_and(level_disjoint(level), levels_well_formed(rest))
215
216# Expressible prerequisite for lower-shadow reasoning: every supplied level
217# strictly below target is itself well formed and pairwise range-disjoint.
218def lower_levels_well_formed(levels: List<&2, List<&2, List<&2, MemTable.Entry>>>, target: Nat) -> Bool:
219 match levels target:
220 case Nil{} _:
221 True{}
222 case Con{level, below} 0n:
223 levels_well_formed(below)
224 case Con{level, rest} 1n+n:
225 lower_levels_well_formed(rest, n)
226
227# --- Fuel-bounded stable two-run linear merge ---
228
229# Merge step for the sorted-run operations.
230def merge_step(
231 order: Cmp,
232 +newer_head: MemTable.Entry,
233 newer_tail: List<&2, MemTable.Entry>,
234 +older_head: MemTable.Entry,
235 older_tail: List<&2, MemTable.Entry>,
236 acc: List<&2, MemTable.Entry>
237) -> List<&2, MemTable.Entry> & List<&2, MemTable.Entry> & List<&2, MemTable.Entry>:
238 match order:
239 case LT{}:
240 (Con{newer_head, acc}, newer_tail, Con{older_head, older_tail})
241 case EQ{}:
242 (Con{newer_head, acc}, newer_tail, older_tail)
243 case GT{}:
244 (Con{older_head, acc}, Con{newer_head, newer_tail}, older_tail)
245
246# Merge go for the sorted-run operations.
247def merge_go(
248 fuel: Nat,
249 state: List<&2, MemTable.Entry> & List<&2, MemTable.Entry> & List<&2, MemTable.Entry>
250) -> List<&2, MemTable.Entry>:
251 match fuel:
252 case 0n:
253 (acc, newer, older) = state
254 List.reverse.go(&2, MemTable.Entry, acc, List.append(&2, MemTable.Entry, newer, older))
255 case 1n+f:
256 (acc, newer, older) = state
257 match newer older:
258 case Nil{} Nil{}:
259 List.reverse(&2, MemTable.Entry, acc)
260 case Nil{} rest:
261 List.reverse.go(&2, MemTable.Entry, acc, rest)
262 case rest Nil{}:
263 List.reverse.go(&2, MemTable.Entry, acc, rest)
264 case Con{+nh, nt} Con{+oh, ot}:
265 merge_go(f, merge_step(entry_cmp(nh, oh), nh, nt, oh, ot, acc))
266
267# Merge newer for the sorted-run operations.
268def merge_newer(+newer: List<&2, MemTable.Entry>, +older: List<&2, MemTable.Entry>) -> List<&2, MemTable.Entry>:
269 fuel = Nat.add(Nat.add(List.length(&2, MemTable.Entry, newer), List.length(&2, MemTable.Entry, older)), 1n)
270 merge_go(fuel, (Nil{}, newer, older))
271
272# --- Precedence-preserving balanced multi-run merge ---
273
274# Represent RunGroup data used by the sorted-run operations.
275type RunGroup is Data:
276 RunGroup{
277 newest_rank: Nat,
278 oldest_rank: Nat,
279 entries: List<&2, MemTable.Entry>
280 }
281
282# Rank runs for the sorted-run operations.
283def rank_runs(runs: List<&2, List<&2, MemTable.Entry>>, +rank: Nat) -> List<&2, RunGroup>:
284 match runs:
285 case Nil{}:
286 Nil{}
287 case Con{entries, rest}:
288 Con{RunGroup{rank, rank, entries}, rank_runs(rest, 1n+rank)}
289
290# Merge groups for the sorted-run operations.
291def merge_groups(newer: RunGroup, older: RunGroup) -> RunGroup:
292 match newer:
293 case RunGroup{newest_rank, oldest_rank, newer_entries}:
294 match older:
295 case RunGroup{older_newest, older_oldest, older_entries}:
296 RunGroup{newest_rank, older_oldest, merge_newer(newer_entries, older_entries)}
297
298# Merge round for the sorted-run operations.
299def merge_round(groups: List<&2, RunGroup>) -> List<&2, RunGroup>:
300 match groups:
301 case Nil{}:
302 Nil{}
303 case Con{group, Nil{}}:
304 Con{group, Nil{}}
305 case Con{newer, Con{older, rest}}:
306 merged tail = merge_groups(newer, older) merge_round(rest)
307 Con{merged, tail}
308
309# Group entries for the sorted-run operations.
310def group_entries(groups: List<&2, RunGroup>) -> List<&2, MemTable.Entry>:
311 match groups:
312 case Nil{}:
313 Nil{}
314 case Con{RunGroup{newest_rank, oldest_rank, entries}, rest}:
315 entries
316
317# Merge many go for the sorted-run operations.
318def merge_many_go(fuel: Nat, groups: List<&2, RunGroup>) -> List<&2, MemTable.Entry>:
319 match fuel:
320 case 0n:
321 group_entries(groups)
322 case 1n+f:
323 merge_many_go(f, merge_round(groups))
324
325# Merge many newest for the sorted-run operations.
326def merge_many_newest(+runs: List<&2, List<&2, MemTable.Entry>>) -> List<&2, MemTable.Entry>:
327 fuel = Nat.add(List.length(&2, List<&2, MemTable.Entry>, runs), 1n)
328 merge_many_go(fuel, rank_runs(runs, 0n))
329
330# Canonicalize raw newest-first entries in O(N log N): each entry starts as one
331# already-sorted run, and stable EQ selection preserves the earlier/newer entry.
332def singleton_runs(entries: List<&2, MemTable.Entry>) -> List<&2, List<&2, MemTable.Entry>>:
333 match entries:
334 case Nil{}:
335 Nil{}
336 case Con{entry, rest}:
337 Con{Con{entry, Nil{}}, singleton_runs(rest)}
338
339# Sort newest for the sorted-run operations.
340def sort_newest(entries: List<&2, MemTable.Entry>) -> List<&2, MemTable.Entry>:
341 merge_many_newest(singleton_runs(entries))
342
343# Merge disjoint dec for the sorted-run operations.
344def merge_disjoint_dec(ok: Bool, runs: List<&2, List<&2, MemTable.Entry>>) -> Maybe<&2, List<&2, MemTable.Entry>>:
345 match ok:
346 case False{}:
347 None{}
348 case True{}:
349 Some{merge_many_newest(runs)}
350
351# L1 has no age tie-breaker. Reject malformed overlapping/duplicate ranges;
352# for accepted disjoint runs, balanced merge order is observationally irrelevant.
353def merge_many_disjoint(+runs: List<&2, List<&2, MemTable.Entry>>) -> Maybe<&2, List<&2, MemTable.Entry>>:
354 merge_disjoint_dec(level_disjoint(runs), runs)
355
356# --- Pure bounded output partitioning ---
357
358# A zero target cannot bound a non-empty partition, so the public partitioning
359# API and its bound predicate consistently interpret it as the smallest safe
360# target: one entry per chunk.
361def partition_target(target: Nat) -> Nat:
362 match target:
363 case 0n:
364 1n
365 case 1n+n:
366 1n+n
367
368# Partition finish for the sorted-run operations.
369def partition_finish(
370 current_rev: List<&2, MemTable.Entry>,
371 chunks_rev: List<&2, List<&2, MemTable.Entry>>
372) -> List<&2, List<&2, MemTable.Entry>>:
373 match current_rev:
374 case Nil{}:
375 List.reverse(&2, List<&2, MemTable.Entry>, chunks_rev)
376 case Con{entry, rest}:
377 chunk = List.reverse(&2, MemTable.Entry, Con{entry, rest})
378 List.reverse(&2, List<&2, MemTable.Entry>, Con{chunk, chunks_rev})
379
380# Represent PartitionState data used by the sorted-run operations.
381type PartitionState is Data:
382 PartitionState{
383 room: Nat,
384 entries: List<&2, MemTable.Entry>,
385 current_rev: List<&2, MemTable.Entry>,
386 chunks_rev: List<&2, List<&2, MemTable.Entry>>
387 }
388
389# Partition step for the sorted-run operations.
390def partition_step(
391 full: Bool,
392 target: Nat,
393 room_after: Nat,
394 entry: MemTable.Entry,
395 rest: List<&2, MemTable.Entry>,
396 current_rev: List<&2, MemTable.Entry>,
397 chunks_rev: List<&2, List<&2, MemTable.Entry>>
398) -> PartitionState:
399 match full:
400 case False{}:
401 PartitionState{room_after, rest, Con{entry, current_rev}, chunks_rev}
402 case True{}:
403 chunk = List.reverse(&2, MemTable.Entry, Con{entry, current_rev})
404 PartitionState{target, rest, Nil{}, Con{chunk, chunks_rev}}
405
406# Partition go for the sorted-run operations.
407def partition_go(
408 fuel: Nat,
409 +target: Nat,
410 state: PartitionState
411) -> List<&2, List<&2, MemTable.Entry>>:
412 match fuel state:
413 case 0n PartitionState{room, entries, current_rev, chunks_rev}:
414 partition_finish(current_rev, chunks_rev)
415 case 1n+f PartitionState{0n, entries, current_rev, chunks_rev}:
416 partition_finish(current_rev, chunks_rev)
417 case 1n+f PartitionState{1n+r, Nil{}, current_rev, chunks_rev}:
418 partition_finish(current_rev, chunks_rev)
419 case 1n+f PartitionState{1n++r, Con{entry, rest}, current_rev, chunks_rev}:
420 partition_go(f, target, partition_step(Nat.is_eq(r, 0n), target, r, entry, rest, current_rev, chunks_rev))
421
422# Handle partition in the sorted-run operations.
423def partition(+target: Nat, +entries: List<&2, MemTable.Entry>) -> List<&2, List<&2, MemTable.Entry>>:
424 +size = partition_target(target)
425 partition_go(List.length(&2, MemTable.Entry, entries), size, PartitionState{size, entries, Nil{}, Nil{}})
426
427# Concatenate chunks for the sorted-run operations.
428def concat_chunks(chunks: List<&2, List<&2, MemTable.Entry>>) -> List<&2, MemTable.Entry>:
429 match chunks:
430 case Nil{}:
431 Nil{}
432 case Con{chunk, rest}:
433 List.append(&2, MemTable.Entry, chunk, concat_chunks(rest))
434
435# Handle the chunk s bounded go for the sorted-run operations.
436def chunks_bounded_go(+target: Nat, chunks: List<&2, List<&2, MemTable.Entry>>) -> Bool:
437 match chunks:
438 case Nil{}:
439 True{}
440 case Con{chunk, rest}:
441 bool_and(
442 Nat.is_le(List.length(&2, MemTable.Entry, chunk), target),
443 chunks_bounded_go(target, rest))
444
445# Handle the chunk s bounded for the sorted-run operations.
446def chunks_bounded(target: Nat, chunks: List<&2, List<&2, MemTable.Entry>>) -> Bool:
447 chunks_bounded_go(partition_target(target), chunks)
448
449# Handle the chunk s strict unique for the sorted-run operations.
450def chunks_strict_unique(chunks: List<&2, List<&2, MemTable.Entry>>) -> Bool:
451 runs_well_formed(chunks)
452
453# Handle the chunk s pairwise disjoint for the sorted-run operations.
454def chunks_pairwise_disjoint(chunks: List<&2, List<&2, MemTable.Entry>>) -> Bool:
455 pairwise_disjoint(chunks)