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(level_names_ok(level, names), manifest_names_ok(rest, Nat.add(level, 1n)))
101	
102	# Handle names all in the pure recovery decisions.
103	def names_all(lvls: List<&2, List<&2, String>>) -> List<&2, String>:
104	  match lvls:
105	    case Nil{}:
106	      Nil{}
107	    case Con{h, t}:
108	      List.append(&2, String, h, names_all(t))
109	
110	# Handle cmax in the pure recovery decisions.
111	def cmax(names: List<&2, String>, +cur: Nat) -> Nat:
112	  match names:
113	    case Nil{}:
114	      cur
115	    case Con{h, t}:
116	      cmax(t, Nat.max(name_gen(h), cur))
117	
118	# Count gen in the pure recovery decisions.
119	def count_gen(+lvls: List<&2, List<&2, String>>) -> Nat:
120	  Nat.add(cmax(names_all(lvls), 0n), 1n)
121	
122	# Handle mfst lists in the pure recovery decisions.
123	def mfst_lists(+mfst: Manifest.Manifest) -> List<&2, List<&2, String>>:
124	  match mfst:
125	    case Manifest.M{lvs}:
126	      lvs
127	
128	# L0 may overlap by design. Every table within each level below L0 must have
129	# a range disjoint from every peer; metadata makes this check independent of
130	# SortedRun and avoids reparsing entries during recovery.
131	def disjoint_with_table(+tbl: Sstable.Table, rest: List<&2, Sstable.Table>) -> Bool:
132	  match rest:
133	    case Nil{}:
134	      True{}
135	    case Con{+h, t}:
136	      mid_and(Sstable.ranges_disjoint(tbl, h), disjoint_with_table(tbl, t))
137	
138	# Return the level pairwise disjoint for the pure recovery decisions.
139	def level_pairwise_disjoint(tables: List<&2, Sstable.Table>) -> Bool:
140	  match tables:
141	    case Nil{}:
142	      True{}
143	    case Con{+h, +t}:
144	      mid_and(disjoint_with_table(h, t), level_pairwise_disjoint(t))
145	
146	# Check lower-level levels disjoint for the pure recovery decisions.
147	def lower_levels_disjoint(levels: List<&2, List<&2, Sstable.Table>>) -> Bool:
148	  match levels:
149	    case Nil{}:
150	      True{}
151	    case Con{+level, rest}:
152	      mid_and(level_pairwise_disjoint(level), lower_levels_disjoint(rest))
153	
154	# Handle l1 plus disjoint in the pure recovery decisions.
155	def l1_plus_disjoint(levels: List<&2, List<&2, Sstable.Table>>) -> Bool:
156	  match levels:
157	    case Nil{}:
158	      True{}
159	    case Con{l0, lower}:
160	      lower_levels_disjoint(lower)
161	
162	# Handle needs flush cap in the pure recovery decisions.
163	def needs_flush_cap(+mem: MemTable.MemTable, +cap: Nat) -> Bool:
164	  Nat.is_lt(cap, MemTable.count(mem))