1	# MPEG-1 Layer III (ISO/IEC 11172-3). Mono and stereo. Layer I and II are rejected.
2	import Base
3	import ./mp3_enc.bend as Enc
4	import ./mp3_dec.bend as Dec
5	
6	# one pulled bit, or a field, beside the reader
7	type Bit is Data:
8	  Bit{xs: List<&2, U32>, buf: U32, n: U32, v: U32}
9	
10	# bitstream: leftover bytes, the current byte, how many low bits remain
11	type Br is Data:
12	  Br{xs: List<&2, U32>, buf: U32, n: U32}
13	
14	# a field just read
15	type Acc is Data:
16	  Acc{br: Br, v: U32}
17	
18	# 'MPEG-1 Layer III' is layer code 1 in the header
19	def hdr.layer(xs: List<&2, U32>) -> U32:
20	  match xs:
21	    case _b0 <> +b1 <> _b2 <> _b3 <> _rest:
22	      ((b1 >> 1n : U32) .&. 3 : U32)
23	    case _:
24	      0
25	
26	# 1 when the ID bit selects MPEG-1
27	def hdr.mpeg1(xs: List<&2, U32>) -> U32:
28	  match xs:
29	    case _b0 <> +b1 <> _b2 <> _b3 <> _rest:
30	      ((b1 >> 3n : U32) .&. 1 : U32)
31	    case _:
32	      0
33	
34	# bitrate index, 0 and 15 are not a frame
35	def hdr.index(xs: List<&2, U32>) -> U32:
36	  match xs:
37	    case _b0 <> _b1 <> +b2 <> _b3 <> _rest:
38	      (b2 >> 4n : U32)
39	    case _:
40	      0
41	
42	# sampling-frequency index. 3 is reserved.
43	def hdr.sr(xs: List<&2, U32>) -> U32:
44	  match xs:
45	    case _b0 <> _b1 <> +b2 <> _b3 <> _rest:
46	      ((b2 >> 2n : U32) .&. 3 : U32)
47	    case _:
48	      3
49	
50	# channel mode. 3 is mono.
51	def hdr.mode(xs: List<&2, U32>) -> U32:
52	  match xs:
53	    case _b0 <> _b1 <> _b2 <> +b3 <> _rest:
54	      (b3 >> 6n : U32)
55	    case _:
56	      0
57	
58	# padding bit
59	def hdr.pad(xs: List<&2, U32>) -> U32:
60	  match xs:
61	    case _b0 <> _b1 <> +b2 <> _b3 <> _rest:
62	      ((b2 >> 1n : U32) .&. 1 : U32)
63	    case _:
64	      0
65	
66	# protection bit 0 means a 16-bit CRC follows the header
67	def hdr.crc(xs: List<&2, U32>) -> U32:
68	  match xs:
69	    case _b0 <> +b1 <> _b2 <> _b3 <> _rest:
70	      U32.xor((b1 .&. 1 : U32), 1)
71	    case _:
72	      0
73	
74	# 1 when the first two bytes carry the 11-bit sync 0xFFE
75	def hdr.sync(xs: List<&2, U32>) -> Bool:
76	  match xs:
77	    case 255 <> +b1 <> _b2 <> _b3 <> _rest:
78	      U32.is_eq((b1 .&. 224 : U32), 224)
79	    case _:
80	      False{}
81	
82	def kbps.of(+ix: U32) -> U32:
83	  match ix:
84	    case 1:
85	      32
86	    case 2:
87	      40
88	    case 3:
89	      48
90	    case 4:
91	      56
92	    case 5:
93	      64
94	    case 6:
95	      80
96	    case 7:
97	      96
98	    case 8:
99	      112
100	    case 9:
101	      128
102	    case 10:
103	      160
104	    case 11:
105	      192
106	    case 12:
107	      224
108	    case 13:
109	      256
110	    case 14:
111	      320
112	    case _:
113	      0
114	
115	# ISO/IEC 11172-3 MPEG-1 Layer III bitrate, kilobits per second
116	def hdr.kbps(xs: List<&2, U32>) -> U32:
117	  kbps.of(hdr.index(xs))
118	
119	def hz.of(+ix: U32) -> U32:
120	  match ix:
121	    case 0:
122	      44100
123	    case 1:
124	      48000
125	    case 2:
126	      32000
127	    case _:
128	      0
129	
130	# ISO/IEC 11172-3 sampling frequency, hertz
131	def hdr.hz(xs: List<&2, U32>) -> U32:
132	  hz.of(hdr.sr(xs))
133	
134	# 1 or 2 channels. mode 3 is single channel.
135	def ch.of(+mode: U32) -> U32:
136	  match mode:
137	    case 3:
138	      1
139	    case _:
140	      2
141	
142	def hdr.ch(xs: List<&2, U32>) -> U32:
143	  ch.of(hdr.mode(xs))
144	
145	def l3.and(a: Bool, b: Bool) -> Bool:
146	  match a:
147	    case False{}:
148	      False{}
149	    case True{}:
150	      b
151	
152	def l3.ok(+xs: List<&2, U32>) -> Bool:
153	  l3.and(
154	    hdr.sync(xs) && U32.is_eq(hdr.mpeg1(xs), 1) && U32.is_eq(hdr.layer(xs), 1),
155	    U32.is_ne(hdr.kbps(xs), 0) && U32.is_ne(hdr.hz(xs), 0))
156	
157	# frame length in bytes: 1152 * kbps * 125 / hz, plus the pad bit
158	def frame.n(+kb: U32, +hz: U32, +pad: U32) -> U32:
159	  (U32.div(((1152 * kb : U32) * 125 : U32), hz) + pad : U32)
160	
161	def frame.of(+xs: List<&2, U32>) -> U32:
162	  frame.n(hdr.kbps(xs), hdr.hz(xs), hdr.pad(xs))
163	
164	def br.zero(xs: List<&2, U32>) -> Br:
165	  Br{xs, 0, 0}
166	
167	def br.fill(xs: List<&2, U32>) -> Br:
168	  match xs:
169	    case Nil{}:
170	      Br{[], 0, 0}
171	    case +hd <> tl:
172	      Br{tl, hd, 8}
173	
174	def br.norm(br: Br) -> Br:
175	  match br:
176	    case Br{xs, _buf, 0}:
177	      br.fill(xs)
178	    case Br{xs, buf, n}:
179	      Br{xs, buf, n}
180	
181	def bit.at(z: Bool, xs: List<&2, U32>, +buf: U32, +n: U32) -> Bit:
182	  match z:
183	    case True{}:
184	      Bit{xs, buf, n, 0}
185	    case False{}:
186	      Bit{xs, buf, (n - 1 : U32), ((buf >> U32.to_nat((n - 1 : U32)) : U32) .&. 1 : U32)}
187	
188	def br.one.at(br: Br) -> Bit:
189	  match br:
190	    case Br{xs, +buf, +n}:
191	      bit.at(U32.is_eq(n, 0), xs, buf, n)
192	
193	def br.one(br: Br) -> Bit:
194	  br.one.at(br.norm(br))
195	
196	def br.shift(b: Bit, +acc: U32) -> Acc:
197	  match b:
198	    case Bit{xs, buf, n, v}:
199	      Acc{Br{xs, buf, n}, ((acc << 1n : U32) .|. v : U32)}
200	
201	def br.next(ac: Acc) -> Acc:
202	  match ac:
203	    case Acc{br, +v}:
204	      br.shift(br.one(br), v)
205	
206	def br.get(hop: Nat, ac: Acc) -> Acc:
207	  match hop:
208	    case 0n:
209	      ac
210	    case 1n+p:
211	      br.get(p, br.next(ac))
212	
213	def br.take(br: Br, +k: U32) -> Acc:
214	  br.get(U32.to_nat(k), Acc{br, 0})
215	
216	def acc.br(ac: Acc) -> Br:
217	  match ac:
218	    case Acc{br, _v}:
219	      br
220	
221	def acc.v(ac: Acc) -> U32:
222	  match ac:
223	    case Acc{_br, v}:
224	      v
225	
226	# side-info length in bytes. MPEG-1 mono is 17, stereo is 32.
227	def side.n(+ch: U32) -> U32:
228	  match ch:
229	    case 1:
230	      17
231	    case _:
232	      32
233	
234	def sr.row(+hz: U32) -> U32:
235	  match hz:
236	    case 48000:
237	      6
238	    case 32000:
239	      7
240	    case _:
241	      5
242	
243	# encoder header at 320 kbit/s, original bit set, no CRC, no pad
244	def enc.b2(+hz: U32) -> U32:
245	  (224 .|. (sr.row(hz) .&. 0 : U32) : U32)
246	
247	def enc.srbits(+hz: U32) -> U32:
248	  match hz:
249	    case 48000:
250	      4
251	    case 32000:
252	      8
253	    case _:
254	      0
255	
256	def enc.b3(+ch: U32) -> U32:
257	  match ch:
258	    case 1:
259	      196
260	    case _:
261	      4
262	
263	def enc.hdr(+hz: U32, +ch: U32) -> List<&2, U32>:
264	  [255, 251, (224 .|. enc.srbits(hz) : U32), enc.b3(ch)]
265	
266	def enc.rate(+hz: U32) -> Bool:
267	  match hz:
268	    case 44100:
269	      True{}
270	    case 48000:
271	      True{}
272	    case 32000:
273	      True{}
274	    case _:
275	      False{}
276	
277	def enc.ch(+ch: U32) -> Bool:
278	  match ch:
279	    case 1:
280	      True{}
281	    case 2:
282	      True{}
283	    case _:
284	      False{}
285	
286	def kind.ok(+k: U32) -> Bool:
287	  match k:
288	    case 1:
289	      True{}
290	    case 3:
291	      True{}
292	    case _:
293	      False{}
294	
295	def zeros.rest(xs: List<&2, U32>) -> Bool:
296	  match xs:
297	    case Nil{}:
298	      True{}
299	    case 0 <> t:
300	      zeros.rest(t)
301	    case _ <> _t:
302	      False{}
303	
304	# an empty sample list is not silence. Silence is one or more zero samples.
305	def frames.zero(xs: List<&2, U32>) -> Bool:
306	  match xs:
307	    case Nil{}:
308	      False{}
309	    case 0 <> t:
310	      zeros.rest(t)
311	    case _ <> _t:
312	      False{}
313	
314	def frames.empty(xs: List<&2, U32>) -> Bool:
315	  match xs:
316	    case Nil{}:
317	      True{}
318	    case _ <> _t:
319	      False{}
320	
321	def ls.cat(xs: List<&2, U32>, ys: List<&2, U32>) -> List<&2, U32>:
322	  List.append(&2, U32, xs, ys)
323	
324	# one silent 320 kbit/s frame. big_values and part2_3_length are zero.
325	def silence.of(+hz: U32, +ch: U32) -> List<&2, U32>:
326	  ls.cat(enc.hdr(hz, ch), List.replicate(U32, U32.to_nat((frame.n(320, hz, 0) - 4 : U32)), 0))
327	
328	def silence.ok(ok: Bool, +hz: U32, +ch: U32) -> Maybe<&2, List<&2, U32>>:
329	  match ok:
330	    case False{}:
331	      None{}
332	    case True{}:
333	      Some{silence.of(hz, ch)}
334	
335	# non-zero PCM goes through the analysis filterbank, MDCT, and Huffman encoder.
336	def mp3.live(
337	  +hz: U32, +ch: U32, +kind: U32, frames: List<&2, U32>
338	) -> Maybe<&2, List<&2, U32>>:
339	  Enc.enc.run(hz, ch, kind, frames)
340	
341	def one.tail(xs: List<&2, U32>) -> Bool:
342	  match xs:
343	    case Nil{}:
344	      True{}
345	    case _hd <> _tl:
346	      False{}
347	
348	def one.only(xs: List<&2, U32>) -> Bool:
349	  match xs:
350	    case _hd <> tl:
351	      one.tail(tl)
352	    case Nil{}:
353	      False{}
354	
355	def samp.hd(xs: List<&2, U32>) -> U32:
356	  match xs:
357	    case +hd <> _tl:
358	      hd
359	    case Nil{}:
360	      0
361	
362	def pulse.ch(one: Bool, mono: Bool, pcm: Bool) -> Bool:
363	  match one:
364	    case False{}:
365	      False{}
366	    case True{}:
367	      match mono:
368	        case False{}:
369	          False{}
370	        case True{}:
371	          pcm
372	
373	# one signed sample is a single Huffman pair, not the filterbank
374	def pulse.yes(one: Bool, +ch: U32, +kind: U32) -> Bool:
375	  pulse.ch(one, U32.is_eq(ch, 1), U32.is_eq(kind, 1))
376	
377	# a magnitude above 15 stays on the filterbank. 0 is not a pair.
378	def pulse.fit(yes: Bool, +w: U32) -> Bool:
379	  match yes:
380	    case False{}:
381	      False{}
382	    case True{}:
383	      U32.is_ne(w, 0) && U32.is_lt(w, 16)
384	
385	def pulse.small(one: Bool, +ch: U32, +kind: U32, +w: U32) -> Bool:
386	  pulse.fit(pulse.yes(one, ch, kind), w)
387	
388	def mp3.arm(
389	  pulse: Bool, +hz: U32, +ch: U32, +kind: U32, frames: List<&2, U32>
390	) -> Maybe<&2, List<&2, U32>>:
391	  match pulse:
392	    case True{}:
393	      Some{Enc.pulse.frame(hz, Enc.pulse.mag(samp.hd(frames)))}
394	    case False{}:
395	      mp3.live(hz, ch, kind, frames)
396	
397	def mp3.nz(
398	  z: Bool, +hz: U32, +ch: U32, +kind: U32, +frames: List<&2, U32>
399	) -> Maybe<&2, List<&2, U32>>:
400	  match z:
401	    case True{}:
402	      silence.ok(True{}, hz, ch)
403	    case False{}:
404	      mp3.arm(pulse.small(one.only(frames), ch, kind, samp.hd(frames)), hz, ch, kind, frames)
405	
406	def mp3.body(
407	  empty: Bool, +hz: U32, +ch: U32, +kind: U32, +frames: List<&2, U32>
408	) -> Maybe<&2, List<&2, U32>>:
409	  match empty:
410	    case True{}:
411	      None{}
412	    case False{}:
413	      mp3.nz(frames.zero(frames), hz, ch, kind, frames)
414	
415	def mp3.pick(
416	  ok: Bool, +hz: U32, +ch: U32, +kind: U32, +frames: List<&2, U32>
417	) -> Maybe<&2, List<&2, U32>>:
418	  match ok:
419	    case False{}:
420	      None{}
421	    case True{}:
422	      mp3.body(frames.empty(frames), hz, ch, kind, frames)
423	
424	# samples are interleaved U32 bits. kind 1 is s16, kind 3 is binary32.
425	def mp3.encode(
426	  +hz: U32, +ch: U32, +kind: U32, frames: List<&2, U32>
427	) -> Maybe<&2, List<&2, U32>>:
428	  mp3.pick(enc.rate(hz) && enc.ch(ch) && kind.ok(kind), hz, ch, kind, frames)
429	
430	# a decoded frame: hertz, channels, interleaved binary32 words
431	type Pcm is Data:
432	  Pcm{hz: U32, ch: U32, pcm: List<&2, U32>}
433	
434	# decoder state. phase 0 seeks a header, 1 collects a frame, 2 has failed.
435	type Wk is Data:
436	  Wk{
437	    hz: U32, ch: U32, pcm: List<&2, U32>, ov: List<&2, F32>, qmf: List<&2, F32>, fresh: U32,
438	    lib: Dec.Lib, on: U32, phase: U32, left: U32, buf: List<&2, U32>
439	  }
440	
441	def le.pick(eq: Bool, +aa: U32, +bb: U32) -> Bool:
442	  match eq:
443	    case True{}:
444	      True{}
445	    case False{}:
446	      U32.is_lt(aa, bb)
447	
448	def le.u(+aa: U32, +bb: U32) -> Bool:
449	  le.pick(U32.is_eq(aa, bb), aa, bb)
450	
451	def frm.fit(+xs: List<&2, U32>, +nn: U32) -> Bool:
452	  le.u(nn, U32.from_nat(List.length(&2, U32, xs)))
453	
454	def frm.take(+xs: List<&2, U32>, +nn: U32) -> List<&2, U32>:
455	  Dec.bd.take(U32.to_nat(nn), xs, [])
456	
457	def frm.rest(+xs: List<&2, U32>, +nn: U32) -> List<&2, U32>:
458	  Dec.bd.drop(U32.to_nat(nn), xs)
459	
460	def frm.and(aa: Bool, bb: Bool) -> Bool:
461	  match aa:
462	    case False{}:
463	      False{}
464	    case True{}:
465	      bb
466	
467	# MPEG-1 Layer III, no CRC, not joint stereo
468	def frm.yes(+xs: List<&2, U32>) -> Bool:
469	  frm.and(l3.ok(xs), frm.and(U32.is_ne(hdr.mode(xs), 1), U32.is_eq(hdr.crc(xs), 0)))
470	
471	def wk.make(+hz: U32, +ch: U32, lib: Dec.Lib) -> Wk:
472	  Wk{hz, ch, [], Dec.dec.ov(ch), Dec.dec.qmf(), 1, lib, 0, 0, 0, []}
473	
474	
475	def buf.add(xs: List<&2, U32>, +hd: U32) -> List<&2, U32>:
476	  List.append(&2, U32, xs, [hd])
477	
478	def win.tail(xs: List<&2, U32>) -> List<&2, U32>:
479	  match xs:
480	    case _hd <> tl:
481	      tl
482	    case Nil{}:
483	      []
484	
485	def wk.bad(st: Wk) -> Wk:
486	  match st:
487	    case Wk{hz, ch, pcm, ov, qmf, fresh, lib, on, _phase, _left, _buf}:
488	      Wk{hz, ch, pcm, ov, qmf, fresh, lib, on, 2, 0, []}
489	
490	def wk.seek(st: Wk, buf: List<&2, U32>) -> Wk:
491	  match st:
492	    case Wk{hz, ch, pcm, ov, qmf, fresh, lib, on, _phase, _left, _buf}:
493	      Wk{hz, ch, pcm, ov, qmf, fresh, lib, on, 0, 0, buf}
494	
495	def wk.read(st: Wk, +left: U32, buf: List<&2, U32>) -> Wk:
496	  match st:
497	    case Wk{hz, ch, pcm, ov, qmf, fresh, lib, on, _phase, _left, _buf}:
498	      Wk{hz, ch, pcm, ov, qmf, fresh, lib, on, 1, left, buf}
499	
500	def wk.fail(+hz: U32, +ch: U32, pcm: List<&2, U32>) -> Wk:
501	  Wk{hz, ch, pcm, [], [], 0, Dec.lib.of(), 0, 2, 0, []}
502	
503	def walk.keep(oo: Dec.Out, +hz: U32, +ch: U32, +pcm0: List<&2, U32>) -> Wk:
504	  match oo:
505	    case Dec.Out{pcm, ov, qmf, fresh, lib}:
506	      Wk{hz, ch, List.append(&2, U32, pcm0, pcm), ov, qmf, fresh, lib, 1, 0, 0, []}
507	
508	def walk.apply(got: Maybe<&2, Dec.Out>, +hz: U32, +ch: U32, pcm0: List<&2, U32>) -> Wk:
509	  match got:
510	    case None{}:
511	      wk.fail(hz, ch, pcm0)
512	    case Some{oo}:
513	      walk.keep(oo, hz, ch, pcm0)
514	
515	def wk.eq(eqh: Bool, eqc: Bool) -> Bool:
516	  match eqh:
517	    case False{}:
518	      False{}
519	    case True{}:
520	      eqc
521	
522	def walk.fr2(
523	  ok: Bool, +buf: List<&2, U32>, +hz: U32, +ch: U32, pcm0: List<&2, U32>, ov: List<&2, F32>,
524	  qmf: List<&2, F32>, +fresh: U32, lib: Dec.Lib
525	) -> Wk:
526	  match ok:
527	    case False{}:
528	      wk.fail(hz, ch, pcm0)
529	    case True{}:
530	      walk.apply(Dec.dec.step(buf, ch, ov, qmf, fresh, lib), hz, ch, pcm0)
531	
532	def walk.fr1(+buf: List<&2, U32>, +hz: U32, +ch: U32, lib: Dec.Lib) -> Wk:
533	  walk.apply(Dec.dec.step(buf, ch, Dec.dec.ov(ch), Dec.dec.qmf(), 1, lib), hz, ch, [])
534	
535	def walk.fr0(
536	  cold: Bool, +buf: List<&2, U32>, +hz0: U32, +ch0: U32, pcm0: List<&2, U32>, ov: List<&2, F32>,
537	  qmf: List<&2, F32>, +fresh: U32, lib: Dec.Lib
538	) -> Wk:
539	  match cold:
540	    case True{}:
541	      walk.fr1(buf, hdr.hz(buf), hdr.ch(buf), Dec.lib.use(lib, hdr.hz(buf)))
542	    case False{}:
543	      walk.fr2(wk.eq(U32.is_eq(hdr.hz(buf), hz0), U32.is_eq(hdr.ch(buf), ch0)), buf, hz0, ch0, pcm0, ov,
544	        qmf, fresh, lib)
545	
546	def walk.frame(
547	  +buf: List<&2, U32>, +hz: U32, +ch: U32, pcm: List<&2, U32>, ov: List<&2, F32>, qmf: List<&2, F32>,
548	  +fresh: U32, lib: Dec.Lib, +on: U32
549	) -> Wk:
550	  walk.fr0(U32.is_eq(on, 0), buf, hz, ch, pcm, ov, qmf, fresh, lib)
551	
552	def walk.rd2(
553	  done: Bool, +hz: U32, +ch: U32, pcm: List<&2, U32>, ov: List<&2, F32>, qmf: List<&2, F32>,
554	  +fresh: U32, lib: Dec.Lib, +on: U32, +left: U32, buf: List<&2, U32>
555	) -> Wk:
556	  match done:
557	    case False{}:
558	      Wk{hz, ch, pcm, ov, qmf, fresh, lib, on, 1, (left - 1 : U32), buf}
559	    case True{}:
560	      walk.frame(buf, hz, ch, pcm, ov, qmf, fresh, lib, on)
561	
562	def walk.arm(big: Bool, st: Wk, +buf: List<&2, U32>) -> Wk:
563	  match big:
564	    case False{}:
565	      wk.bad(st)
566	    case True{}:
567	      wk.read(st, (frame.of(buf) - 4 : U32), buf)
568	
569	def walk.good(ok: Bool, st: Wk, +buf: List<&2, U32>) -> Wk:
570	  match ok:
571	    case False{}:
572	      wk.bad(st)
573	    case True{}:
574	      walk.arm(le.u(5, frame.of(buf)), st, buf)
575	
576	def walk.hdr(sync: Bool, st: Wk, +buf: List<&2, U32>) -> Wk:
577	  match sync:
578	    case False{}:
579	      wk.seek(st, win.tail(buf))
580	    case True{}:
581	      walk.good(frm.yes(buf), st, buf)
582	
583	def walk.seen2(full: Bool, +buf: List<&2, U32>, st: Wk) -> Wk:
584	  match full:
585	    case False{}:
586	      st
587	    case True{}:
588	      walk.hdr(hdr.sync(buf), st, buf)
589	
590	def walk.seen(full: Bool, st: Wk) -> Wk:
591	  match st:
592	    case Wk{hz, ch, pcm, ov, qmf, fresh, lib, on, phase, left, +buf}:
593	      walk.seen2(full, buf, Wk{hz, ch, pcm, ov, qmf, fresh, lib, on, phase, left, buf})
594	
595	def walk.ph(
596	  +phase: U32, +hz: U32, +ch: U32, pcm: List<&2, U32>, ov: List<&2, F32>, qmf: List<&2, F32>,
597	  +fresh: U32, lib: Dec.Lib, +on: U32, +left: U32, +buf: List<&2, U32>, +hd: U32
598	) -> Wk:
599	  match phase:
600	    case 2:
601	      Wk{hz, ch, pcm, ov, qmf, fresh, lib, on, 2, 0, []}
602	    case 1:
603	      walk.rd2(U32.is_eq(left, 1), hz, ch, pcm, ov, qmf, fresh, lib, on, left, buf.add(buf, hd))
604	    case _:
605	      walk.seen(U32.is_eq(U32.from_nat(List.length(&2, U32, buf.add(buf, hd))), 4),
606	        Wk{hz, ch, pcm, ov, qmf, fresh, lib, on, 0, 0, buf.add(buf, hd)})
607	
608	def walk.byte(st: Wk, +hd: U32) -> Wk:
609	  match st:
610	    case Wk{hz, ch, pcm, ov, qmf, fresh, lib, on, phase, left, buf}:
611	      walk.ph(phase, hz, ch, pcm, ov, qmf, fresh, lib, on, left, buf, hd)
612	
613	def walk.done(ok: Bool, +hz: U32, +ch: U32, pcm: List<&2, U32>) -> Maybe<&2, Pcm>:
614	  match ok:
615	    case False{}:
616	      None{}
617	    case True{}:
618	      Some{Pcm{hz, ch, pcm}}
619	
620	def walk.fin(seek: Bool, have: Bool, +hz: U32, +ch: U32, pcm: List<&2, U32>) -> Maybe<&2, Pcm>:
621	  match seek:
622	    case False{}:
623	      None{}
624	    case True{}:
625	      walk.done(have, hz, ch, pcm)
626	
627	def walk.finish(st: Wk) -> Maybe<&2, Pcm>:
628	  match st:
629	    case Wk{+hz, +ch, pcm, _ov, _qmf, _fresh, _lib, on, phase, _left, _buf}:
630	      walk.fin(U32.is_eq(phase, 0), U32.is_eq(on, 1), hz, ch, pcm)
631	
632	def walk.go(xs: List<&2, U32>, st: Wk) -> Maybe<&2, Pcm>:
633	  match xs:
634	    case Nil{}:
635	      walk.finish(st)
636	    case +hd <> tl:
637	      walk.go(tl, walk.byte(st, hd))
638	
639	def wk.zero() -> Wk:
640	  Wk{0, 0, [], [], [], 1, Dec.lib.of(), 0, 0, 0, []}
641	
642	# bytes in, PCM out. Layer I, Layer II, joint stereo, a CRC, and a bit reservoir are none.
643	def mp3.decode(xs: List<&2, U32>) -> Maybe<&2, Pcm>:
644	  walk.go(xs, wk.zero())