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	# --- Fuel-bounded stable two-run linear merge ---
205	
206	# Merge step for the sorted-run operations.
207	def merge_step(
208	  order: Cmp,
209	  +newer_head: MemTable.Entry,
210	  newer_tail: List<&2, MemTable.Entry>,
211	  +older_head: MemTable.Entry,
212	  older_tail: List<&2, MemTable.Entry>,
213	  acc: List<&2, MemTable.Entry>
214	) -> List<&2, MemTable.Entry> & List<&2, MemTable.Entry> & List<&2, MemTable.Entry>:
215	  match order:
216	    case LT{}:
217	      (Con{newer_head, acc}, newer_tail, Con{older_head, older_tail})
218	    case EQ{}:
219	      (Con{newer_head, acc}, newer_tail, older_tail)
220	    case GT{}:
221	      (Con{older_head, acc}, Con{newer_head, newer_tail}, older_tail)
222	
223	# Merge go for the sorted-run operations.
224	def merge_go(
225	  fuel: Nat,
226	  state: List<&2, MemTable.Entry> & List<&2, MemTable.Entry> & List<&2, MemTable.Entry>
227	) -> List<&2, MemTable.Entry>:
228	  match fuel:
229	    case 0n:
230	      (acc, newer, older) = state
231	      List.reverse.go(&2, MemTable.Entry, acc, List.append(&2, MemTable.Entry, newer, older))
232	    case 1n+f:
233	      (acc, newer, older) = state
234	      match newer older:
235	        case Nil{} Nil{}:
236	          List.reverse(&2, MemTable.Entry, acc)
237	        case Nil{} rest:
238	          List.reverse.go(&2, MemTable.Entry, acc, rest)
239	        case rest Nil{}:
240	          List.reverse.go(&2, MemTable.Entry, acc, rest)
241	        case Con{+nh, nt} Con{+oh, ot}:
242	          merge_go(f, merge_step(entry_cmp(nh, oh), nh, nt, oh, ot, acc))
243	
244	# Merge newer for the sorted-run operations.
245	def merge_newer(+newer: List<&2, MemTable.Entry>, +older: List<&2, MemTable.Entry>) -> List<&2, MemTable.Entry>:
246	  fuel = Nat.add(Nat.add(List.length(&2, MemTable.Entry, newer), List.length(&2, MemTable.Entry, older)), 1n)
247	  merge_go(fuel, (Nil{}, newer, older))
248	
249	# --- Precedence-preserving balanced multi-run merge ---
250	
251	# Represent RunGroup data used by the sorted-run operations.
252	type RunGroup is Data:
253	  RunGroup{
254	    newest_rank: Nat,
255	    oldest_rank: Nat,
256	    entries: List<&2, MemTable.Entry>
257	  }
258	
259	# Rank runs for the sorted-run operations.
260	def rank_runs(runs: List<&2, List<&2, MemTable.Entry>>, +rank: Nat) -> List<&2, RunGroup>:
261	  match runs:
262	    case Nil{}:
263	      Nil{}
264	    case Con{entries, rest}:
265	      Con{RunGroup{rank, rank, entries}, rank_runs(rest, 1n+rank)}
266	
267	# Merge groups for the sorted-run operations.
268	def merge_groups(newer: RunGroup, older: RunGroup) -> RunGroup:
269	  match newer:
270	    case RunGroup{newest_rank, oldest_rank, newer_entries}:
271	      match older:
272	        case RunGroup{older_newest, older_oldest, older_entries}:
273	          RunGroup{newest_rank, older_oldest, merge_newer(newer_entries, older_entries)}
274	
275	# Merge round for the sorted-run operations.
276	def merge_round(groups: List<&2, RunGroup>) -> List<&2, RunGroup>:
277	  match groups:
278	    case Nil{}:
279	      Nil{}
280	    case Con{group, Nil{}}:
281	      Con{group, Nil{}}
282	    case Con{newer, Con{older, rest}}:
283	      merged tail = merge_groups(newer, older) merge_round(rest)
284	      Con{merged, tail}
285	
286	# Group entries for the sorted-run operations.
287	def group_entries(groups: List<&2, RunGroup>) -> List<&2, MemTable.Entry>:
288	  match groups:
289	    case Nil{}:
290	      Nil{}
291	    case Con{RunGroup{newest_rank, oldest_rank, entries}, rest}:
292	      entries
293	
294	# Merge many go for the sorted-run operations.
295	def merge_many_go(fuel: Nat, groups: List<&2, RunGroup>) -> List<&2, MemTable.Entry>:
296	  match fuel:
297	    case 0n:
298	      group_entries(groups)
299	    case 1n+f:
300	      merge_many_go(f, merge_round(groups))
301	
302	# Merge many newest for the sorted-run operations.
303	def merge_many_newest(+runs: List<&2, List<&2, MemTable.Entry>>) -> List<&2, MemTable.Entry>:
304	  fuel = Nat.add(List.length(&2, List<&2, MemTable.Entry>, runs), 1n)
305	  merge_many_go(fuel, rank_runs(runs, 0n))
306	
307	# Canonicalize raw newest-first entries in O(N log N): each entry starts as one
308	# already-sorted run, and stable EQ selection preserves the earlier/newer entry.
309	def singleton_runs(entries: List<&2, MemTable.Entry>) -> List<&2, List<&2, MemTable.Entry>>:
310	  match entries:
311	    case Nil{}:
312	      Nil{}
313	    case Con{entry, rest}:
314	      Con{Con{entry, Nil{}}, singleton_runs(rest)}
315	
316	# Sort newest for the sorted-run operations.
317	def sort_newest(entries: List<&2, MemTable.Entry>) -> List<&2, MemTable.Entry>:
318	  merge_many_newest(singleton_runs(entries))
319	
320	# --- Pure bounded output partitioning ---
321	
322	# A zero target cannot bound a non-empty partition, so the public partitioning
323	# API and its bound predicate consistently interpret it as the smallest safe
324	# target: one entry per chunk.
325	def partition_target(target: Nat) -> Nat:
326	  match target:
327	    case 0n:
328	      1n
329	    case 1n+n:
330	      1n+n
331	
332	# Partition finish for the sorted-run operations.
333	def partition_finish(
334	  current_rev: List<&2, MemTable.Entry>,
335	  chunks_rev: List<&2, List<&2, MemTable.Entry>>
336	) -> List<&2, List<&2, MemTable.Entry>>:
337	  match current_rev:
338	    case Nil{}:
339	      List.reverse(&2, List<&2, MemTable.Entry>, chunks_rev)
340	    case Con{entry, rest}:
341	      chunk = List.reverse(&2, MemTable.Entry, Con{entry, rest})
342	      List.reverse(&2, List<&2, MemTable.Entry>, Con{chunk, chunks_rev})
343	
344	# Represent PartitionState data used by the sorted-run operations.
345	type PartitionState is Data:
346	  PartitionState{
347	    room: Nat,
348	    entries: List<&2, MemTable.Entry>,
349	    current_rev: List<&2, MemTable.Entry>,
350	    chunks_rev: List<&2, List<&2, MemTable.Entry>>
351	  }
352	
353	# Partition step for the sorted-run operations.
354	def partition_step(
355	  full: Bool,
356	  target: Nat,
357	  room_after: Nat,
358	  entry: MemTable.Entry,
359	  rest: List<&2, MemTable.Entry>,
360	  current_rev: List<&2, MemTable.Entry>,
361	  chunks_rev: List<&2, List<&2, MemTable.Entry>>
362	) -> PartitionState:
363	  match full:
364	    case False{}:
365	      PartitionState{room_after, rest, Con{entry, current_rev}, chunks_rev}
366	    case True{}:
367	      chunk = List.reverse(&2, MemTable.Entry, Con{entry, current_rev})
368	      PartitionState{target, rest, Nil{}, Con{chunk, chunks_rev}}
369	
370	# Partition go for the sorted-run operations.
371	def partition_go(
372	  fuel: Nat,
373	  +target: Nat,
374	  state: PartitionState
375	) -> List<&2, List<&2, MemTable.Entry>>:
376	  match fuel state:
377	    case 0n PartitionState{room, entries, current_rev, chunks_rev}:
378	      partition_finish(current_rev, chunks_rev)
379	    case 1n+f PartitionState{0n, entries, current_rev, chunks_rev}:
380	      partition_finish(current_rev, chunks_rev)
381	    case 1n+f PartitionState{1n+r, Nil{}, current_rev, chunks_rev}:
382	      partition_finish(current_rev, chunks_rev)
383	    case 1n+f PartitionState{1n++r, Con{entry, rest}, current_rev, chunks_rev}:
384	      partition_go(f, target, partition_step(Nat.is_eq(r, 0n), target, r, entry, rest, current_rev, chunks_rev))
385	
386	# Handle partition in the sorted-run operations.
387	def partition(+target: Nat, +entries: List<&2, MemTable.Entry>) -> List<&2, List<&2, MemTable.Entry>>:
388	  +size = partition_target(target)
389	  partition_go(List.length(&2, MemTable.Entry, entries), size, PartitionState{size, entries, Nil{}, Nil{}})
390	
391	# Concatenate chunks for the sorted-run operations.
392	def concat_chunks(chunks: List<&2, List<&2, MemTable.Entry>>) -> List<&2, MemTable.Entry>:
393	  match chunks:
394	    case Nil{}:
395	      Nil{}
396	    case Con{chunk, rest}:
397	      List.append(&2, MemTable.Entry, chunk, concat_chunks(rest))
398	
399	# Handle the chunk s bounded go for the sorted-run operations.
400	def chunks_bounded_go(+target: Nat, chunks: List<&2, List<&2, MemTable.Entry>>) -> Bool:
401	  match chunks:
402	    case Nil{}:
403	      True{}
404	    case Con{chunk, rest}:
405	      bool_and(
406	        Nat.is_le(List.length(&2, MemTable.Entry, chunk), target),
407	        chunks_bounded_go(target, rest))
408	
409	# Handle the chunk s bounded for the sorted-run operations.
410	def chunks_bounded(target: Nat, chunks: List<&2, List<&2, MemTable.Entry>>) -> Bool:
411	  chunks_bounded_go(partition_target(target), chunks)
412	
413	# Handle the chunk s strict unique for the sorted-run operations.
414	def chunks_strict_unique(chunks: List<&2, List<&2, MemTable.Entry>>) -> Bool:
415	  runs_well_formed(chunks)
416	
417	# Handle the chunk s pairwise disjoint for the sorted-run operations.
418	def chunks_pairwise_disjoint(chunks: List<&2, List<&2, MemTable.Entry>>) -> Bool:
419	  pairwise_disjoint(chunks)