src/Wal.bend
mylsm-lsm-store@0.3.0.0 · 372 lines · 0 definitions
1import Base
2import mylsm-lsm-store@0.3.0.0/src/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
13type Mut is Data:
14 Put{key: String, val: String}
15 Del{key: String}
16
17type Batch is Data:
18 Batch{muts: List<&2, Mut>}
19
20# --- Encode (structural, no fuel) ---
21
22def dashes(num: Nat) -> String:
23 match num:
24 case 0n:
25 ""
26 case 1n+m:
27 SCon{'-', dashes(m)}
28
29def 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
36def hash3(tag: Char, key: String, val: String) -> U32:
37 hash_str(val, hash_str(key, hash_str(SCon{tag, SNil{}}, 7)))
38
39def 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
42def 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
49def 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
56def encode(batch: Batch) -> String:
57 match batch:
58 case Batch{muts}:
59 enc_muts(muts)
60
61def 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
66type Phase is Data:
67 PTag{} RLen{next: Phase} PKey{} PVal{} PChk{} PSemi{} DKey{} DChk{} DSemi{}
68
69type DecState is Data:
70 DS{phase: Phase, muts: List<&2, Mut>, tag: Char, num: Nat, kacc: String, vacc: String, cacc: String, ok: Bool}
71
72def 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
83def 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
94def 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
101def 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
112def 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
161def 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
170def 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
181def 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
186def 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.
197def 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
206def 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
215def 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
220def 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
228def 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 {==}
235def 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
243def 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
251def 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
263def 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).
272def jump(num: Nat, num0: Nat) -> Nat:
273 match num:
274 case 0n:
275 num0
276 case 1n+m:
277 1n+jump(m, num0)
278
279def 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
287def 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.
297def 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).
315def 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.
333def 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.
351def 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.
371def is_decided(+_m: Maybe<&2, Batch>) -> Bool:
372 True{}