1	import Base
2	
3	# Manifest (Task 5): which SSTables live at which level.
4	# Format is positional (line i = level i, no level numbers to parse):
5	#   <name>,<name>
6	#   <name>
7	#   #<checksum-decimal>
8	# Names are engine-generated (sst-<level>-<counter>.tbl) AND strictly
9	# validated on parse ([A-Za-z0-9._-], not "." / ".."): T1 hostile bytes
10	# must fail closed, never traverse directories (spec §8).
11	# Checksum covers all content lines (fail-closed on corruption, like WAL).
12	# Parsing leans on Base (split/join/starts_with/drop/read): precompiled,
13	# trusted, zero proof burden — laws pin OUR format, not Base.
14	
15	type Manifest is Data:
16	  M{levels: List<&2, List<&2, String>>}
17	
18	def mhash(str: String, seed: U32) -> U32:
19	  match str:
20	    case SNil{}:
21	      seed
22	    case SCon{c, t}:
23	      mhash(t, U32.add(U32.mul(seed, 31), Char.to_u32(c)))
24	
25	def encode_line(names: List<&2, String>) -> String:
26	  String.join(names, ",")
27	
28	def encode_lines(xss: List<&2, List<&2, String>>) -> List<&2, String>:
29	  match xss:
30	    case Nil{}:
31	      Nil{}
32	    case Con{h, t}:
33	      Con{encode_line(h), encode_lines(t)}
34	
35	def serialize(mfst: Manifest) -> String:
36	  match mfst:
37	    case M{levels}:
38	      +ls = encode_lines(levels)
39	      +content = String.join(ls, SCon{Char.from_u32(10), SNil{}})
40	      String.join(List.append(&2, String, ls, Con{"#" ++ U32.show(mhash(content, 7)), Nil{}}), SCon{Char.from_u32(10), SNil{}})
41	
42	# --- Strict name validation (structural recursion + leaves; no fuel:
43	# recursion is unconditional, decisions combine via leaves) ---
44	def name_ok_step(ok: Bool, good: Bool) -> Bool:
45	  match ok:
46	    case True{}:
47	      good
48	    case False{}:
49	      False{}
50	
51	def nc_alpha(ok: Bool, ch: Char) -> Bool:
52	  match ok:
53	    case True{}:
54	      True{}
55	    case False{}:
56	      Char.is_digit(ch)
57	
58	def nc_us(ok: Bool, +ch: Char) -> Bool:
59	  match ok:
60	    case True{}:
61	      True{}
62	    case False{}:
63	      nc_alpha(Char.is_alpha(ch), ch)
64	
65	def nc_dot(ok: Bool, +ch: Char) -> Bool:
66	  match ok:
67	    case True{}:
68	      True{}
69	    case False{}:
70	      nc_us(Char.is_eq(ch, Char.from_u32(95)), ch)
71	
72	def nc_dash(ok: Bool, +ch: Char) -> Bool:
73	  match ok:
74	    case True{}:
75	      True{}
76	    case False{}:
77	      nc_dot(Char.is_eq(ch, Char.from_u32(46)), ch)
78	
79	def name_char_ok(+ch: Char) -> Bool:
80	  nc_dash(Char.is_eq(ch, Char.from_u32(45)), ch)
81	
82	def name_go(str: String, ok: Bool) -> Bool:
83	  match str:
84	    case SNil{}:
85	      ok
86	    case SCon{h, t}:
87	      name_go(t, name_ok_step(ok, name_char_ok(h)))
88	
89	def name_dots2(d2: Bool, str: String) -> Bool:
90	  match d2:
91	    case True{}:
92	      False{}
93	    case False{}:
94	      name_go(str, True{})
95	
96	def name_dots(d1: Bool, d2: Bool, str: String) -> Bool:
97	  match d1:
98	    case True{}:
99	      False{}
100	    case False{}:
101	      name_dots2(d2, str)
102	
103	def name_ok(str: String) -> Bool:
104	  match str:
105	    case SNil{}:
106	      False{}
107	    case SCon{+h, +t}:
108	      name_dots(String.eq(SCon{h, t}, "."), String.eq(SCon{h, t}, ".."), SCon{h, t})
109	
110	def names_and(lhs: Bool, rhs: Bool) -> Bool:
111	  match lhs:
112	    case True{}:
113	      rhs
114	    case False{}:
115	      False{}
116	
117	def names_ok(xs: List<&2, String>) -> Bool:
118	  match xs:
119	    case Nil{}:
120	      True{}
121	    case Con{h, t}:
122	      names_and(name_ok(h), names_ok(t))
123	
124	# --- Parse: validate everything first (Bool), then parse unchecked
125	# (total, structural, no Maybe in loops). Top dispatch is a leaf. ---
126	def line_valid(line: String) -> Bool:
127	  match line:
128	    case SNil{}:
129	      True{}
130	    case SCon{h, t}:
131	      names_ok(String.split(SCon{h, t}, Char.from_u32(44)))
132	
133	def body_valid(ls: List<&2, String>) -> Bool:
134	  match ls:
135	    case Nil{}:
136	      True{}
137	    case Con{h, t}:
138	      names_and(line_valid(h), body_valid(t))
139	
140	def chk_rd(opt: Maybe<&2, U32>, content: String) -> Bool:
141	  match opt:
142	    case None{}:
143	      False{}
144	    case Some{v}:
145	      U32.is_eq(v, mhash(content, 7))
146	
147	def chk_sw(sw: Bool, chk: String, content: String) -> Bool:
148	  match sw:
149	    case True{}:
150	      chk_rd(U32.read(String.drop(chk, 1n)), content)
151	    case False{}:
152	      False{}
153	
154	def chk_valid(+chk: String, content: String) -> Bool:
155	  chk_sw(String.starts_with(chk, "#"), chk, content)
156	
157	def valid_split(pair: (List<&2, String> & String)) -> Bool:
158	  match pair:
159	    case (+body, chk):
160	      names_and(body_valid(body), chk_valid(chk, String.join(body, SCon{Char.from_u32(10), SNil{}})))
161	
162	def split_last(ls: List<&2, String>, acc: List<&2, String>) -> (List<&2, String> & String):
163	  match ls:
164	    case Nil{}:
165	      (List.reverse(&2, String, acc), "")
166	    case Con{h, Nil{}}:
167	      (List.reverse(&2, String, acc), h)
168	    case Con{h, Con{k, t}}:
169	      split_last(Con{k, t}, Con{h, acc})
170	
171	def valid_lines(lines: List<&2, String>) -> Bool:
172	  valid_split(split_last(lines, Nil{}))
173	
174	def valid_manifest(str: String) -> Bool:
175	  valid_lines(String.split(str, Char.from_u32(10)))
176	
177	def parse_line_u(line: String) -> List<&2, String>:
178	  match line:
179	    case SNil{}:
180	      Nil{}
181	    case SCon{h, t}:
182	      String.split(SCon{h, t}, Char.from_u32(44))
183	
184	def parse_levels_u(ls: List<&2, String>, acc: List<&2, List<&2, String>>) -> List<&2, List<&2, String>>:
185	  match ls:
186	    case Nil{}:
187	      List.reverse(&2, List<&2, String>, acc)
188	    case Con{h, t}:
189	      parse_levels_u(t, Con{parse_line_u(h), acc})
190	
191	def parse_unchecked(pair: (List<&2, String> & String)) -> Manifest:
192	  match pair:
193	    case (body, chk):
194	      M{parse_levels_u(body, Nil{})}
195	
196	def parse_dispatch(ok: Bool, str: String) -> Maybe<&2, Manifest>:
197	  match ok:
198	    case True{}:
199	      Some{parse_unchecked(split_last(String.split(str, Char.from_u32(10)), Nil{}))}
200	    case False{}:
201	      None{}
202	
203	def parse(+str: String) -> Maybe<&2, Manifest>:
204	  parse_dispatch(valid_manifest(str), str)
205	
206	# Total-parser witness used by the hardening law.
207	def is_decided(+_m: Maybe<&2, Manifest>) -> Bool:
208	  True{}