1	import Base
2	import ./MemTable.bend as MemTable
3	import ./Manifest.bend as Manifest
4	import ./Sstable.bend as Sstable
5	
6	# --- Flush-counter restore (pure) ---
7	
8	# Handle mid and in the pure recovery decisions.
9	def mid_and(lhs: Bool, rhs: Bool) -> Bool:
10	  match lhs:
11	    case True{}:
12	      rhs
13	    case False{}:
14	      False{}
15	
16	# Handle shape mid in the pure recovery decisions.
17	def shape_mid(first: Bool, second: Bool, third: Bool) -> Bool:
18	  mid_and(first, mid_and(second, third))
19	
20	# Table generations are compact decimal only. Unparsable middles are invalid
21	# (no unary-dash legacy reads: no retrocompat).
22	def gen_valid_read(parsed: Maybe<&2, Nat>) -> Bool:
23	  match parsed:
24	    case Some{n}:
25	      True{}
26	    case None{}:
27	      False{}
28	
29	# Handle gen valid in the pure recovery decisions.
30	def gen_valid(+middle: String) -> Bool:
31	  gen_valid_read(Nat.read(middle))
32	
33	# Handle ov ok in the pure recovery decisions.
34	def ov_ok(+big: Bool, +name: String, +ln: Nat) -> Bool:
35	  match big:
36	    case True{}:
37	      shape_mid(String.starts_with(name, "l"), String.ends_with(name, ".tbl"), gen_valid(String.take(String.drop(name, 3n), Nat.sub(ln, 7n))))
38	    case False{}:
39	      False{}
40	
41	# Handle name shape in the pure recovery decisions.
42	def name_shape(+name: String) -> Bool:
43	  +ln = String.length(name)
44	  ov_ok(Nat.is_le(7n, ln), name, ln)
45	
46	# Return the level name ok for the pure recovery decisions.
47	def level_name_ok(+big: Bool, +name: String, +ln: Nat, +prefix: String, +prefix_len: Nat) -> Bool:
48	  match big:
49	    case False{}:
50	      False{}
51	    case True{}:
52	      shape_mid(String.starts_with(name, prefix), String.ends_with(name, ".tbl"), gen_valid(String.take(String.drop(name, prefix_len), Nat.sub(ln, Nat.add(prefix_len, 4n)))))
53	
54	# Handle name shape level in the pure recovery decisions.
55	def name_shape_level(+name: String, +level: Nat) -> Bool:
56	  +prefix = "l" ++ Nat.show(level) ++ "-"
57	  +prefix_len = String.length(prefix)
58	  +ln = String.length(name)
59	  level_name_ok(Nat.is_le(Nat.add(prefix_len, 4n), ln), name, ln, prefix, prefix_len)
60	
61	# Handle gen value read in the pure recovery decisions.
62	def gen_value_read(parsed: Maybe<&2, Nat>) -> Nat:
63	  match parsed:
64	    case Some{n}:
65	      n
66	    case None{}:
67	      0n
68	
69	# Handle gen value in the pure recovery decisions.
70	def gen_value(+middle: String) -> Nat:
71	  gen_value_read(Nat.read(middle))
72	
73	# Handle name gen in the pure recovery decisions.
74	def name_gen(+name: String) -> Nat:
75	  +ln = String.length(name)
76	  gen_value(String.take(String.drop(name, 3n), Nat.sub(ln, 7n)))
77	
78	# Handle names ok in the pure recovery decisions.
79	def names_ok(xs: List<&2, String>) -> Bool:
80	  match xs:
81	    case Nil{}:
82	      True{}
83	    case Con{h, t}:
84	      mid_and(name_shape(h), names_ok(t))
85	
86	# Return the level names ok for the pure recovery decisions.
87	def level_names_ok(+level: Nat, xs: List<&2, String>) -> Bool:
88	  match xs:
89	    case Nil{}:
90	      True{}
91	    case Con{h, t}:
92	      mid_and(name_shape_level(h, level), level_names_ok(level, t))
93	
94	# Handle manifest names ok in the pure recovery decisions.
95	def manifest_names_ok(levels: List<&2, List<&2, String>>, +level: Nat) -> Bool:
96	  match levels:
97	    case Nil{}:
98	      True{}
99	    case Con{names, rest}:
100	      mid_and(Nat.is_le(level, 3n),
101	        mid_and(level_names_ok(level, names), manifest_names_ok(rest, Nat.add(level, 1n))))
102	
103	# Handle names all in the pure recovery decisions.
104	def names_all(lvls: List<&2, List<&2, String>>) -> List<&2, String>:
105	  match lvls:
106	    case Nil{}:
107	      Nil{}
108	    case Con{h, t}:
109	      List.append(&2, String, h, names_all(t))
110	
111	# Handle cmax in the pure recovery decisions.
112	def cmax(names: List<&2, String>, +cur: Nat) -> Nat:
113	  match names:
114	    case Nil{}:
115	      cur
116	    case Con{h, t}:
117	      cmax(t, Nat.max(name_gen(h), cur))
118	
119	# Count gen in the pure recovery decisions.
120	def count_gen(+lvls: List<&2, List<&2, String>>) -> Nat:
121	  Nat.add(cmax(names_all(lvls), 0n), 1n)
122	
123	# Handle mfst lists in the pure recovery decisions.
124	def mfst_lists(+mfst: Manifest.Manifest) -> List<&2, List<&2, String>>:
125	  match mfst:
126	    case Manifest.M{lvs}:
127	      lvs
128	
129	# L0 may overlap by design. Every table within each level below L0 must have
130	# a range disjoint from every peer; metadata makes this check independent of
131	# SortedRun and avoids reparsing entries during recovery.
132	def disjoint_with_table(+tbl: Sstable.Table, rest: List<&2, Sstable.Table>) -> Bool:
133	  match rest:
134	    case Nil{}:
135	      True{}
136	    case Con{+h, t}:
137	      mid_and(Sstable.ranges_disjoint(tbl, h), disjoint_with_table(tbl, t))
138	
139	# Return the level pairwise disjoint for the pure recovery decisions.
140	def level_pairwise_disjoint(tables: List<&2, Sstable.Table>) -> Bool:
141	  match tables:
142	    case Nil{}:
143	      True{}
144	    case Con{+h, +t}:
145	      mid_and(disjoint_with_table(h, t), level_pairwise_disjoint(t))
146	
147	# Check lower-level levels disjoint for the pure recovery decisions.
148	def lower_levels_disjoint(levels: List<&2, List<&2, Sstable.Table>>) -> Bool:
149	  match levels:
150	    case Nil{}:
151	      True{}
152	    case Con{+level, rest}:
153	      mid_and(level_pairwise_disjoint(level), lower_levels_disjoint(rest))
154	
155	# Handle l1 plus disjoint in the pure recovery decisions.
156	def l1_plus_disjoint(levels: List<&2, List<&2, Sstable.Table>>) -> Bool:
157	  match levels:
158	    case Nil{}:
159	      True{}
160	    case Con{l0, lower}:
161	      lower_levels_disjoint(lower)
162	
163	# Handle needs flush cap in the pure recovery decisions.
164	def needs_flush_cap(+mem: MemTable.MemTable, +cap: Nat) -> Bool:
165	  Nat.is_lt(cap, MemTable.count(mem))