src/SortedRun.bend

mylsm-lsm-store@0.3.2.0 · 397 lines · 50 definitions

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