1	import Base
2	import ./Keys.bend as Keys
3	
4	# WAL record codec (Task 3). Format (lengths are UNARY dash runs — no
5	# decimal show/parse inverse lemmas; data is opaque — counted, never
6	# inspected; checksums are COMPARED, never parsed):
7	#   Put: 'P' dashes(klen) ':' key dashes(vlen) ':' val chk4 ';'
8	#   Del: 'D' dashes(klen) ':' key chk4 ';'
9	# chk4 = 4 raw bytes of hash3(tag, key, val) (Del hashes val="").
10	# Every pump step consumes exactly one char (handoffs are fused into the
11	# step that sees the boundary char), so fuel = length fits exactly.
12	
13	type Mut is Data:
14	  Put{key: String, val: String}
15	  Del{key: String}
16	
17	type Batch is Data:
18	  Batch{muts: List<&2, Mut>}
19	
20	# --- Encode (structural, no fuel) ---
21	
22	def dashes(num: Nat) -> String:
23	  match num:
24	    case 0n:
25	      ""
26	    case 1n+m:
27	      SCon{'-', dashes(m)}
28	
29	def hash_str(str: String, acc: U32) -> U32:
30	  match str:
31	    case SNil{}:
32	      acc
33	    case SCon{c, t}:
34	      hash_str(t, U32.add(U32.mul(acc, 31), Char.to_u32(c)))
35	
36	def hash3(tag: Char, key: String, val: String) -> U32:
37	  hash_str(val, hash_str(key, hash_str(SCon{tag, SNil{}}, 7)))
38	
39	def chk4(+word: U32) -> String:
40	  SCon{Char.from_u32(U32.and(word, 255)), SCon{Char.from_u32(U32.and(U32.shrn(word, 8n), 255)), SCon{Char.from_u32(U32.and(U32.shrn(word, 16n), 255)), SCon{Char.from_u32(U32.and(U32.shrn(word, 24n), 255)), SNil{}}}}}
41	
42	def enc_mut(mut: Mut) -> String:
43	  match mut:
44	    case Put{+key, +val}:
45	      "P" ++ dashes(String.length(key)) ++ ":" ++ key ++ dashes(String.length(val)) ++ ":" ++ val ++ chk4(hash3('P', key, val)) ++ ";"
46	    case Del{+key}:
47	      "D" ++ dashes(String.length(key)) ++ ":" ++ key ++ chk4(hash3('D', key, "")) ++ ";"
48	
49	def enc_muts(muts: List<&2, Mut>) -> String:
50	  match muts:
51	    case Nil{}:
52	      ""
53	    case Con{m, t}:
54	      enc_mut(m) ++ enc_muts(t)
55	
56	def encode(batch: Batch) -> String:
57	  match batch:
58	    case Batch{muts}:
59	      enc_muts(muts)
60	
61	def stage(+staged: List<&2, Batch>, +batch: Batch) -> List<&2, Batch>:
62	  Con{batch, staged}
63	
64	# --- Decode pump (fuel + state; Nat counters; unified dash phase) ---
65	
66	type Phase is Data:
67	  PTag{} RLen{next: Phase} PKey{} PVal{} PChk{} PSemi{} DKey{} DChk{} DSemi{}
68	
69	type DecState is Data:
70	  DS{phase: Phase, muts: List<&2, Mut>, tag: Char, num: Nat, kacc: String, vacc: String, cacc: String, ok: Bool}
71	
72	def tag_dispatch(put: Bool, del: Bool, +muts: List<&2, Mut>) -> DecState:
73	  match put:
74	    case True{}:
75	      DS{RLen{PKey{}}, muts, 'P', 0n, "", "", "", True{}}
76	    case False{}:
77	      match del:
78	        case True{}:
79	          DS{RLen{DKey{}}, muts, 'D', 0n, "", "", "", True{}}
80	        case False{}:
81	          DS{PTag{}, muts, 'P', 0n, "", "", "", False{}}
82	
83	def dash_step(dash: Bool, colon: Bool, next: Phase, +muts: List<&2, Mut>, +tag: Char, +num: Nat, +kacc: String, +vacc: String, +cacc: String) -> DecState:
84	  match dash:
85	    case True{}:
86	      DS{RLen{next}, muts, tag, 1n+num, kacc, vacc, cacc, True{}}
87	    case False{}:
88	      match colon:
89	        case True{}:
90	          DS{next, muts, tag, num, kacc, vacc, cacc, True{}}
91	        case False{}:
92	          DS{PTag{}, muts, tag, 0n, "", "", "", False{}}
93	
94	def chk_next(ceq: Bool, next: Phase, +muts: List<&2, Mut>, +tag: Char, +key: String, +val: String) -> DecState:
95	  match ceq:
96	    case True{}:
97	      DS{next, muts, tag, 0n, key, val, "", True{}}
98	    case False{}:
99	      DS{PTag{}, muts, tag, 0n, "", "", "", False{}}
100	
101	def semi_step(semi: Bool, put: Bool, +muts: List<&2, Mut>, +key: String, +val: String) -> DecState:
102	  match semi:
103	    case True{}:
104	      match put:
105	        case True{}:
106	          DS{PTag{}, List.append(&2, Mut, muts, Con{Put{key, val}, Nil{}}), 'P', 0n, "", "", "", True{}}
107	        case False{}:
108	          DS{PTag{}, List.append(&2, Mut, muts, Con{Del{key}, Nil{}}), 'P', 0n, "", "", "", True{}}
109	    case False{}:
110	      DS{PTag{}, muts, 'P', 0n, "", "", "", False{}}
111	
112	def phase_router(phase: Phase, +muts: List<&2, Mut>, +tag: Char, +num: Nat, +kacc: String, +vacc: String, +cacc: String, +ch: Char) -> DecState:
113	  match phase:
114	    case PTag{}:
115	      tag_dispatch(Char.is_eq(ch, 'P'), Char.is_eq(ch, 'D'), muts)
116	    case RLen{next}:
117	      dash_step(Char.is_eq(ch, '-'), Char.is_eq(ch, ':'), next, muts, tag, num, kacc, vacc, cacc)
118	    case PKey{}:
119	      match num:
120	        case 0n:
121	          dash_step(Char.is_eq(ch, '-'), Char.is_eq(ch, ':'), PVal{}, muts, tag, 0n, kacc, vacc, cacc)
122	        case 1n+m:
123	          DS{PKey{}, muts, tag, m, kacc ++ SCon{ch, SNil{}}, vacc, cacc, True{}}
124	    case PVal{}:
125	      match num:
126	        case 0n:
127	          DS{PChk{}, muts, tag, 1n+(1n+(1n+0n)), kacc, vacc, SCon{ch, SNil{}}, True{}}
128	        case 1n+m:
129	          DS{PVal{}, muts, tag, m, kacc, vacc ++ SCon{ch, SNil{}}, cacc, True{}}
130	    case PChk{}:
131	      match num:
132	        case 0n:
133	          chk_next(String.eq(cacc, chk4(hash3(tag, kacc, vacc))), PSemi{}, muts, tag, kacc, vacc)
134	        case 1n+m:
135	          match m:
136	            case 0n:
137	              chk_next(String.eq(cacc ++ SCon{ch, SNil{}}, chk4(hash3(tag, kacc, vacc))), PSemi{}, muts, tag, kacc, vacc)
138	            case 1n+p:
139	              DS{PChk{}, muts, tag, 1n+p, kacc, vacc, cacc ++ SCon{ch, SNil{}}, True{}}
140	    case PSemi{}:
141	      semi_step(Char.is_eq(ch, ';'), True{}, muts, kacc, vacc)
142	    case DKey{}:
143	      match num:
144	        case 0n:
145	          DS{DChk{}, muts, tag, 1n+(1n+(1n+0n)), kacc, vacc, SCon{ch, SNil{}}, True{}}
146	        case 1n+m:
147	          DS{DKey{}, muts, tag, m, kacc ++ SCon{ch, SNil{}}, vacc, cacc, True{}}
148	    case DChk{}:
149	      match num:
150	        case 0n:
151	          chk_next(String.eq(cacc, chk4(hash3(tag, kacc, ""))), DSemi{}, muts, tag, kacc, "")
152	        case 1n+m:
153	          match m:
154	            case 0n:
155	              chk_next(String.eq(cacc ++ SCon{ch, SNil{}}, chk4(hash3(tag, kacc, ""))), DSemi{}, muts, tag, kacc, "")
156	            case 1n+p:
157	              DS{DChk{}, muts, tag, 1n+p, kacc, vacc, cacc ++ SCon{ch, SNil{}}, True{}}
158	    case DSemi{}:
159	      semi_step(Char.is_eq(ch, ';'), False{}, muts, kacc, vacc)
160	
161	def dec_step(st: DecState, ch: Char) -> DecState:
162	  match st:
163	    case DS{phase, muts, tag, num, kacc, vacc, cacc, ok}:
164	      match ok:
165	        case False{}:
166	          DS{PTag{}, muts, tag, 0n, "", "", "", False{}}
167	        case True{}:
168	          phase_router(phase, muts, tag, num, kacc, vacc, cacc, ch)
169	
170	def dec_finish(ok: Bool, phase: Phase, +muts: List<&2, Mut>) -> (List<&2, Mut> & Bool):
171	  match ok:
172	    case False{}:
173	      (muts, False{})
174	    case True{}:
175	      match phase:
176	        case PTag{}:
177	          (muts, True{})
178	        case _:
179	          (muts, False{})
180	
181	def dec_extract(st: DecState) -> (List<&2, Mut> & Bool):
182	  match st:
183	    case DS{phase, muts, tag, num, kacc, vacc, cacc, ok}:
184	      dec_finish(ok, phase, muts)
185	
186	def dec_go(fuel: Nat, rest: String, st: DecState) -> (List<&2, Mut> & Bool):
187	  match fuel rest:
188	    case 0n _:
189	      dec_extract(st)
190	    case 1n+f SNil{}:
191	      dec_extract(st)
192	    case 1n+f SCon{h, +t}:
193	      dec_go(f, t, dec_step(st, h))
194	
195	# Fuel-exact runner: consumes exactly len-bounded input, returns the state
196	# (no extraction — callers extract). Proof-only workhorse.
197	def dec_run(fuel: Nat, rest: String, st: DecState) -> DecState:
198	  match fuel rest:
199	    case 0n _:
200	      st
201	    case 1n+f SNil{}:
202	      st
203	    case 1n+f SCon{h, +t}:
204	      dec_run(f, t, dec_step(st, h))
205	
206	def dec_wrap(pair: (List<&2, Mut> & Bool)) -> Maybe<&2, Batch>:
207	  match pair:
208	    case (muts, ok):
209	      match ok:
210	        case True{}:
211	          Some{Batch{muts}}
212	        case False{}:
213	          None{}
214	
215	def decode(+str: String) -> Maybe<&2, Batch>:
216	  dec_wrap(dec_go(Nat.add(String.length(str), 1n), str, DS{PTag{}, Nil{}, 'P', 0n, "", "", "", True{}}))
217	
218	# --- Proof scaffolding ---
219	
220	def app_assoc(sa: String, sb: String, sc: String) -> {((sa ++ sb) ++ sc) == (sa ++ (sb ++ sc)) : String}:
221	  match sa:
222	    case SNil{}:
223	      {==}
224	    case SCon{h, t}:
225	      %app_assoc(t, sb, sc) : {SCon{h, (t ++ sb) ++ sc} == SCon{h, _} : String}
226	      {==}
227	
228	def app_nil_r(str: String) -> {(str ++ "") == str : String}:
229	  match str:
230	    case SNil{}:
231	      {==}
232	    case SCon{h, t}:
233	      %app_nil_r(t) : {SCon{h, t ++ ""} == SCon{h, _} : String}
234	      {==}
235	def len_append(sa: String, sb: String) -> {String.length(sa ++ sb) == Nat.add(String.length(sa), String.length(sb)) : Nat}:
236	  match sa:
237	    case SNil{}:
238	      {==}
239	    case SCon{h, t}:
240	      %len_append(t, sb) : {1n+String.length(t ++ sb) == 1n+_ : Nat}
241	      {==}
242	
243	def add_assoc(n1: Nat, n2: Nat, n3: Nat) -> {Nat.add(Nat.add(n1, n2), n3) == Nat.add(n1, Nat.add(n2, n3)) : Nat}:
244	  match n1:
245	    case 0n:
246	      {==}
247	    case 1n+m:
248	      %add_assoc(m, n2, n3) : {1n+Nat.add(Nat.add(m, n2), n3) == 1n+_ : Nat}
249	      {==}
250	
251	def list_app_assoc(
252	  xs: List<&2, Mut>,
253	  ys: List<&2, Mut>,
254	  zs: List<&2, Mut>,
255	) -> {List.append(&2, Mut, List.append(&2, Mut, xs, ys), zs) == List.append(&2, Mut, xs, List.append(&2, Mut, ys, zs)) : List<&2, Mut>}:
256	  match xs:
257	    case Nil{}:
258	      {==}
259	    case Con{h, t}:
260	      %list_app_assoc(t, ys, zs) : {Con{h, List.append(&2, Mut, List.append(&2, Mut, t, ys), zs)} == Con{h, _} : List<&2, Mut>}
261	      {==}
262	
263	def append_nil_r(+xs: List<&2, Mut>) -> {List.append(&2, Mut, xs, Nil{}) == xs : List<&2, Mut>}:
264	  match xs:
265	    case Nil{}:
266	      {==}
267	    case Con{h, t}:
268	      %append_nil_r(t) : {Con{h, List.append(&2, Mut, t, Nil{})} == Con{h, _} : List<&2, Mut>}
269	      {==}
270	
271	# Unary counter: jump(n, num0) = num0 + n as 1n-chains (no appends, no assoc).
272	def jump(num: Nat, num0: Nat) -> Nat:
273	  match num:
274	    case 0n:
275	      num0
276	    case 1n+m:
277	      1n+jump(m, num0)
278	
279	def jump_zero(num: Nat) -> {jump(num, 0n) == num : Nat}:
280	  match num:
281	    case 0n:
282	      {==}
283	    case 1n+m:
284	      %jump_zero(m) : {1n+jump(m, 0n) == 1n+_ : Nat}
285	      {==}
286	
287	def jump_succ(num: Nat, num0: Nat) -> {jump(num, 1n+num0) == 1n+jump(num, num0) : Nat}:
288	  match num:
289	    case 0n:
290	      {==}
291	    case 1n+p:
292	      %jump_succ(p, num0) : {1n+jump(p, 1n+num0) == 1n+_ : Nat}
293	      {==}
294	
295	# RLen dash-run skip (unified len phase; next stored, never matched here).
296	# Fuel is len(span++tail): deconstructs with the Nat induction, tail opaque.
297	def dashspan(
298	  num: Nat,
299	  tail: String,
300	  muts0: List<&2, Mut>,
301	  tag: Char,
302	  next: Phase,
303	  +num0: Nat,
304	  kacc0: String,
305	) -> {dec_run(String.length(dashes(num) ++ tail), dashes(num) ++ tail, DS{RLen{next}, muts0, tag, num0, kacc0, "", "", True{}}) == dec_run(String.length(tail), tail, DS{RLen{next}, muts0, tag, jump(num, num0), kacc0, "", "", True{}}) : DecState}:
306	  match num:
307	    case 0n:
308	      {==}
309	    case 1n++m:
310	      %jump_succ(m, num0) : {dec_run(String.length(dashes(m) ++ tail), dashes(m) ++ tail, DS{RLen{next}, muts0, tag, 1n+num0, kacc0, "", "", True{}}) == dec_run(String.length(tail), tail, DS{RLen{next}, muts0, tag, _, kacc0, "", "", True{}}) : DecState}
311	      %dashspan(m, tail, muts0, tag, next, 1n+num0, kacc0) : {dec_run(String.length(dashes(m) ++ tail), dashes(m) ++ tail, DS{RLen{next}, muts0, tag, 1n+num0, kacc0, "", "", True{}}) == _ : DecState}
312	      {==}
313	
314	# PKEY take: consumes key bytes; kacc0 generalized. Fuel is len(key++tail).
315	def keyspan(
316	  key: String,
317	  +kacc0: String,
318	  tail: String,
319	  muts0: List<&2, Mut>,
320	  tag: Char,
321	  vacc0: String,
322	) -> {dec_run(String.length(key ++ tail), key ++ tail, DS{PKey{}, muts0, tag, String.length(key), kacc0, vacc0, "", True{}}) == dec_run(String.length(tail), tail, DS{PKey{}, muts0, tag, 0n, kacc0 ++ key, vacc0, "", True{}}) : DecState}:
323	  match key:
324	    case SNil{}:
325	      %Equal.sym(String, kacc0 ++ "", kacc0, app_nil_r(kacc0)) : {dec_run(String.length(tail), tail, DS{PKey{}, muts0, tag, 0n, kacc0, vacc0, "", True{}}) == dec_run(String.length(tail), tail, DS{PKey{}, muts0, tag, 0n, _, vacc0, "", True{}}) : DecState}
326	      {==}
327	    case SCon{+h, +t}:
328	      %app_assoc(kacc0, SCon{h, SNil{}}, t) : {dec_run(String.length(t ++ tail), t ++ tail, DS{PKey{}, muts0, tag, String.length(t), kacc0 ++ SCon{h, SNil{}}, vacc0, "", True{}}) == dec_run(String.length(tail), tail, DS{PKey{}, muts0, tag, 0n, _, vacc0, "", True{}}) : DecState}
329	      %keyspan(t, kacc0 ++ SCon{h, SNil{}}, tail, muts0, tag, vacc0) : {dec_run(String.length(t ++ tail), t ++ tail, DS{PKey{}, muts0, tag, String.length(t), kacc0 ++ SCon{h, SNil{}}, vacc0, "", True{}}) == _ : DecState}
330	      {==}
331	
332	# PVAL take: mirror for values.
333	def valspan(
334	  val: String,
335	  +vacc0: String,
336	  tail: String,
337	  muts0: List<&2, Mut>,
338	  tag: Char,
339	  kacc: String,
340	) -> {dec_run(String.length(val ++ tail), val ++ tail, DS{PVal{}, muts0, tag, String.length(val), kacc, vacc0, "", True{}}) == dec_run(String.length(tail), tail, DS{PVal{}, muts0, tag, 0n, kacc, vacc0 ++ val, "", True{}}) : DecState}:
341	  match val:
342	    case SNil{}:
343	      %Equal.sym(String, vacc0 ++ "", vacc0, app_nil_r(vacc0)) : {dec_run(String.length(tail), tail, DS{PVal{}, muts0, tag, 0n, kacc, vacc0, "", True{}}) == dec_run(String.length(tail), tail, DS{PVal{}, muts0, tag, 0n, kacc, _, "", True{}}) : DecState}
344	      {==}
345	    case SCon{+h, +t}:
346	      %app_assoc(vacc0, SCon{h, SNil{}}, t) : {dec_run(String.length(t ++ tail), t ++ tail, DS{PVal{}, muts0, tag, String.length(t), kacc, vacc0 ++ SCon{h, SNil{}}, "", True{}}) == dec_run(String.length(tail), tail, DS{PVal{}, muts0, tag, 0n, kacc, _, "", True{}}) : DecState}
347	      %valspan(t, vacc0 ++ SCon{h, SNil{}}, tail, muts0, tag, kacc) : {dec_run(String.length(t ++ tail), t ++ tail, DS{PVal{}, muts0, tag, String.length(t), kacc, vacc0 ++ SCon{h, SNil{}}, "", True{}}) == _ : DecState}
348	      {==}
349	
350	# DKEY take: mirror for delete keys.
351	def dkeyspan(
352	  key: String,
353	  +kacc0: String,
354	  tail: String,
355	  muts0: List<&2, Mut>,
356	  tag: Char,
357	) -> {dec_run(String.length(key ++ tail), key ++ tail, DS{DKey{}, muts0, tag, String.length(key), kacc0, "", "", True{}}) == dec_run(String.length(tail), tail, DS{DKey{}, muts0, tag, 0n, kacc0 ++ key, "", "", True{}}) : DecState}:
358	  match key:
359	    case SNil{}:
360	      %Equal.sym(String, kacc0 ++ "", kacc0, app_nil_r(kacc0)) : {dec_run(String.length(tail), tail, DS{DKey{}, muts0, tag, 0n, kacc0, "", "", True{}}) == dec_run(String.length(tail), tail, DS{DKey{}, muts0, tag, 0n, _, "", "", True{}}) : DecState}
361	      {==}
362	    case SCon{+h, +t}:
363	      %app_assoc(kacc0, SCon{h, SNil{}}, t) : {dec_run(String.length(t ++ tail), t ++ tail, DS{DKey{}, muts0, tag, String.length(t), kacc0 ++ SCon{h, SNil{}}, "", "", True{}}) == dec_run(String.length(tail), tail, DS{DKey{}, muts0, tag, 0n, _, "", "", True{}}) : DecState}
364	      %dkeyspan(t, kacc0 ++ SCon{h, SNil{}}, tail, muts0, tag) : {dec_run(String.length(t ++ tail), t ++ tail, DS{DKey{}, muts0, tag, String.length(t), kacc0 ++ SCon{h, SNil{}}, "", "", True{}}) == _ : DecState}
365	      {==}
366	
367	# (valsec/record/gen open-proof deferred — see laws/Wal.bend.
368	# Closed round-trip vectors in laws/Wal.bend + Task-12 fuzz cover correctness.)
369	
370	# Total-parser witness used by the hardening law.
371	def is_decided(+_m: Maybe<&2, Batch>) -> Bool:
372	  True{}