1	import Base
2	import ./Keys.bend as Keys
3	import ./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.
9	def 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.
17	def 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.
25	def 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.
33	def 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.
41	def 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.
49	def 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.
59	def 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.
67	def 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.
77	def 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.
94	def 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.
107	def 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.
113	def 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.
117	def 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.
129	def 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.
134	def 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.
142	def 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.
150	def 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.
158	def 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.
166	def 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.
185	def 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.
189	def 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.
197	def 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.
205	def 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.
209	def 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.
218	def 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.
230	def 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.
247	def 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.
268	def 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.
275	type 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.
283	def 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.
291	def 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.
299	def 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.
310	def 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.
318	def 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.
326	def 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.
332	def 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.
340	def 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.
344	def 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.
353	def 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.
361	def 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.
369	def 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.
381	type 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.
390	def 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.
407	def 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.
423	def 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.
428	def 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.
436	def 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.
446	def 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.
450	def 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.
454	def chunks_pairwise_disjoint(chunks: List<&2, List<&2, MemTable.Entry>>) -> Bool:
455	  pairwise_disjoint(chunks)