cbor.bend

bend-kit-cbor@0.3.0.0 · 785 lines · 96 definitions

1# CBOR (RFC 8949) values encoded and decoded over Bytes. Source: https://github.com/paymog/bend-kit/tree/main/cbor
2import Base
3import bend-kit-bytes@0.3.3.0/bytes.bend as Bytes
4
5# Raw words preserve CBOR integer and floating-point bit patterns.
6type W64 is Data:
7  W64{hi: U32, lo: U32}
8
9type Float is Data:
10  Half{bits: U32}
11  Single{bits: U32}
12  Double{bits: W64}
13
14type Simple is Data:
15  SFalse{}
16  STrue{}
17  SNull{}
18  SUndefined{}
19  Other{value: U32}
20
21type Val is Type:
22  UInt{value: W64}
23  NInt{value: W64}
24  BStr{value: Bytes.Bytes}
25  TStr{value: Bytes.Bytes}
26  Arr{items: List<&1, Val>}
27  Obj{items: List<&1, Val & Val>}
28  Tag{number: W64, value: Val}
29  Sim{value: Simple}
30  Flt{value: Float}
31
32type W is Type:
33  W{buf: Array<U32>, cap: U32, n: U32, word: U32}
34def grow.if(grow: Bool, buf: Array<U32>, +k: U32) -> Array<U32>:
35  match grow:
36    case True{}:
37      Bytes.grow((k * 4 : U32), buf, (k * 8 : U32))
38    case False{}:
39      buf
40
41
42def put(full: Bool, buf: Array<U32>, +cap: U32, +n: U32, +word: U32) -> W:
43  match full:
44    case True{}:
45      +k = (n >> 2n : U32)
46      +grow = U32.is_eq(k, cap)
47      +cap2 = Bool.pick(U32, grow, (cap * 2 : U32), cap)
48      W{Array.set(U32, grow.if(grow, buf, k), k, word), cap2, (n + 1 : U32), 0}
49    case False{}:
50      W{buf, cap, (n + 1 : U32), word}
51def finish.buf(full: Bool, cap: U32, buf: Array<U32>, +k: U32, +r: U32, +word: U32) -> Array<U32>:
52  match full:
53    case True{}:
54      +grow = U32.is_eq(k, cap)
55      Bytes.flush(True{}, grow.if(grow, buf, k), k, U32.shrn(word, U32.to_nat(((4 - r) * 8 : U32))))
56    case False{}:
57      buf
58
59
60def byte(o: W, +b: U32) -> W:
61  W{buf, +cap, +n, +word} = o
62  +w = ((word >> 8n) .|. (b << 24n) : U32)
63  put(U32.is_eq((n .&. 3 : U32), 3), buf, cap, n, w)
64
65def finish(o: W) -> Bytes.Bytes:
66  W{buf, cap, +n, +word} = o
67  +r = (n .&. 3 : U32)
68  +k = (n >> 2n : U32)
69  +full = U32.is_ne(r, 0)
70  Bytes.Bytes{n, finish.buf(full, cap, buf, k, r, word)}
71def empty() -> W:
72  W{Bytes.alloc(0), 1, 0, 0}
73
74def head.small(+major: U32, +v: U32, o: W) -> W:
75  byte(o, ((major << 5n) .|. v : U32))
76
77def head.u32.sixteen(fits: Bool, +major: U32, +v: U32, o: W) -> W:
78  match fits:
79    case True{}:
80      byte(byte(byte(o, ((major << 5n) .|. 25 : U32)), (v >> 8n : U32)), v)
81    case False{}:
82      byte(byte(byte(byte(byte(o, ((major << 5n) .|. 26 : U32)), (v >> 24n : U32)), (v >> 16n : U32)), (v >> 8n : U32)), v)
83
84def head.u32.eight(fits: Bool, +major: U32, +v: U32, o: W) -> W:
85  match fits:
86    case True{}:
87      byte(byte(o, ((major << 5n) .|. 24 : U32)), v)
88    case False{}:
89      head.u32.sixteen(U32.is_le(v, 65535), major, v, o)
90
91def head.u32.small(small: Bool, +major: U32, +v: U32, o: W) -> W:
92  match small:
93    case True{}:
94      head.small(major, v, o)
95    case False{}:
96      head.u32.eight(U32.is_le(v, 255), major, v, o)
97def head.u32(+major: U32, +v: U32, o: W) -> W:
98  head.u32.small(U32.is_lt(v, 24), major, v, o)
99
100def raw.u32(o: W, +v: U32) -> W:
101  byte(byte(byte(byte(o, (v >> 24n : U32)), (v >> 16n : U32)), (v >> 8n : U32)), v)
102
103def uint.bytes.small(small: Bool, +major: U32, +hi: U32, +lo: U32, o: W) -> W:
104  match small:
105    case True{}:
106      head.u32(major, lo, o)
107    case False{}:
108      raw.u32(raw.u32(byte(o, ((major << 5n) .|. 27 : U32)), hi), lo)
109
110def uint.bytes(+major: U32, v: W64, o: W) -> W:
111  W64{+hi, +lo} = v
112  uint.bytes.small(U32.is_eq(hi, 0), major, hi, lo, o)
113
114def raw.bytes.go(n: Nat, r: Array<U32> & U32, +i: U32, o: W) -> W:
115  match n:
116    case 0n:
117      o
118    case 1n+p:
119      (a, +b) = r
120      raw.bytes.go(p, Bytes.peek(a, (i + 1 : U32)), (i + 1 : U32), byte(o, b))
121
122def raw.bytes(b: Bytes.Bytes, o: W) -> W:
123  Bytes.Bytes{+len, buf} = b
124  raw.bytes.go(U32.to_nat(len), Bytes.peek(buf, 0), 0, o)
125
126# RFC 3629 §4 validity, as in json: overlong forms, surrogates, and code points past U+10FFFF have width 0.
127type Cp is Data:
128  Cp{c: U32, w: U32}
129
130def pk.if(ok: Bool, a: Array<U32>, +i: U32) -> Array<U32> & U32:
131  match ok:
132    case True{}:
133      Bytes.peek(a, i)
134    case False{}:
135      (a, 256)
136
137# Byte i, or 256 at end, which no rule accepts.
138def pk(a: Array<U32>, +end: U32, +i: U32) -> Array<U32> & U32:
139  pk.if(U32.is_lt(i, end), a, i)
140
141def cont(+b: U32) -> Bool:
142  U32.is_eq((b .&. 192 : U32), 128)
143
144def utf8.n(+b0: U32, +b1: U32, +b2: U32, +b3: U32) -> Cp:
145  +x1 = (b1 .&. 63 : U32)
146  +x2 = (b2 .&. 63 : U32)
147  +x3 = (b3 .&. 63 : U32)
148  +c2 = (((b0 .&. 31) << 6n) .|. x1 : U32)
149  +c3 = ((((b0 .&. 15) << 12n) .|. (x1 << 6n)) .|. x2 : U32)
150  +c4 = (((((b0 .&. 7) << 18n) .|. (x1 << 12n)) .|. (x2 << 6n)) .|. x3 : U32)
151  +ok2 = U32.is_le(192, b0) && U32.is_lt(b0, 224) && cont(b1) && U32.is_le(128, c2)
152  +ok3 = U32.is_le(224, b0) && U32.is_lt(b0, 240) && cont(b1) && cont(b2) && U32.is_le(2048, c3) && (U32.is_lt(c3, 55296) || U32.is_lt(57343, c3))
153  +ok4 = U32.is_le(240, b0) && U32.is_lt(b0, 248) && cont(b1) && cont(b2) && cont(b3) && U32.is_le(65536, c4) && U32.is_le(c4, 1114111)
154  Bool.pick(Cp, ok2, Cp{c2, 2}, Bool.pick(Cp, ok3, Cp{c3, 3}, Bool.pick(Cp, ok4, Cp{c4, 4}, Cp{0, 0})))
155
156def utf8.b3(+b0: U32, +b1: U32, +b2: U32, r: Array<U32> & U32) -> Array<U32> & Cp:
157  (a, +b3) = r
158  (a, utf8.n(b0, b1, b2, b3))
159
160def utf8.b2(+end: U32, +i: U32, +b0: U32, +b1: U32, r: Array<U32> & U32) -> Array<U32> & Cp:
161  (a, +b2) = r
162  utf8.b3(b0, b1, b2, pk(a, end, (i + 3 : U32)))
163
164def utf8.b1(+end: U32, +i: U32, +b0: U32, r: Array<U32> & U32) -> Array<U32> & Cp:
165  (a, +b1) = r
166  utf8.b2(end, i, b0, b1, pk(a, end, (i + 2 : U32)))
167
168def utf8.cp(+i: U32, r: Array<U32> & Cp) -> Array<U32> & U32 & Bool:
169  (a, cp) = r
170  Cp{c, +w} = cp
171  (a, (i + w : U32), U32.is_ne(w, 0))
172
173def utf8.byte(ascii: Bool, a: Array<U32>, +end: U32, +i: U32, +b: U32) -> Array<U32> & U32 & Bool:
174  match ascii:
175    case True{}:
176      (a, (i + 1 : U32), True{})
177    case False{}:
178      utf8.cp(i, utf8.b1(end, i, b, pk(a, end, (i + 1 : U32))))
179
180def utf8.lead(+end: U32, +i: U32, r: Array<U32> & U32) -> Array<U32> & U32 & Bool:
181  (a, +b) = r
182  utf8.byte(U32.is_lt(b, 128), a, end, i, b)
183
184def utf8.more(go: Bool, a: Array<U32>, +end: U32, +i: U32) -> Array<U32> & U32 & Bool:
185  match go:
186    case True{}:
187      utf8.lead(end, i, Bytes.peek(a, i))
188    case False{}:
189      (a, i, True{})
190
191def utf8.step(ok: Bool, a: Array<U32>, +end: U32, +i: U32) -> Array<U32> & U32 & Bool:
192  match ok:
193    case True{}:
194      utf8.more(U32.is_lt(i, end), a, end, i)
195    case False{}:
196      (a, i, False{})
197
198# Each step eats a whole code point, so end - i steps reach end.
199def utf8.go(n: Nat, r: Array<U32> & U32 & Bool, +end: U32) -> Array<U32> & Bool:
200  match n:
201    case 0n:
202      (a, i, ok) = r
203      (a, ok)
204    case 1n+p:
205      (a, +i, ok) = r
206      utf8.go(p, utf8.step(ok, a, end, i), end)
207
208# Are bytes i until end well-formed UTF-8?
209def utf8.check(a: Array<U32>, +i: U32, +end: U32) -> Array<U32> & Bool:
210  utf8.go(U32.to_nat((end - i : U32)), (a, i, True{}), end)
211
212def text.fin(+len: U32, r: Array<U32> & Bool) -> Bytes.Bytes & Bool:
213  (a, ok) = r
214  (Bytes.Bytes{len, a}, ok)
215
216def text.check(b: Bytes.Bytes) -> Bytes.Bytes & Bool:
217  Bytes.Bytes{+len, buf} = b
218  text.fin(len, utf8.check(buf, 0, len))
219
220# Simple values 20..23 have their own constructors, 24..31 are reserved (RFC 8949 §3.3).
221def simple.ok(+v: U32) -> Bool:
222  U32.is_lt(v, 20) || (U32.is_le(32, v) && U32.is_le(v, 255))
223
224# IGuard aborts the encoding when a value has no CBOR form; IText carries a text string and its UTF-8 check.
225type Item is Type:
226  IVal{value: Val}
227  IArr{items: List<&1, Val>}
228  IMap{items: List<&1, Val & Val>}
229  IArrLen{value: List<&1, Val> & Nat}
230  IMapLen{value: List<&1, Val & Val> & Nat}
231  IGuard{ok: Bool}
232  IText{value: Bytes.Bytes & Bool}
233def vals.length.put(h: Val, r: List<&1, Val> & Nat) -> List<&1, Val> & Nat:
234  (rest, n) = r
235  (Con{h, rest}, (1n + n : Nat))
236
237def pairs.length.put(h: Val & Val, r: List<&1, Val & Val> & Nat) -> List<&1, Val & Val> & Nat:
238  (rest, n) = r
239  (Con{h, rest}, (1n + n : Nat))
240
241def vals.length(xs: List<&1, Val>) -> List<&1, Val> & Nat:
242  match xs:
243    case Nil{}:
244      (Nil{}, 0n)
245    case Con{h, t}:
246      vals.length.put(h, vals.length(t))
247
248def pairs.length(xs: List<&1, Val & Val>) -> List<&1, Val & Val> & Nat:
249  match xs:
250    case Nil{}:
251      (Nil{}, 0n)
252    case Con{h, t}:
253      pairs.length.put(h, pairs.length(t))
254
255def size.arr(h: Val, r: Val & Nat) -> Val & Nat:
256  (t, n) = r
257  match t:
258    case Arr{items}:
259      (Arr{Con{h, items}}, n)
260    case _:
261      (Arr{Nil{}}, n)
262
263def size.obj(k: Val, v: Val, r: Val & Nat) -> Val & Nat:
264  (t, n) = r
265  match t:
266    case Obj{items}:
267      (Obj{Con{(k, v), items}}, n)
268    case _:
269      (Obj{Nil{}}, n)
270
271def size.cons(hr: Val & Nat, r: Val & Nat) -> Val & Nat:
272  (h, a) = hr
273  (t, b) = r
274  size.arr(h, (t, (1n + a + b : Nat)))
275
276def size.pair(kr: Val & Nat, vr: Val & Nat, r: Val & Nat) -> Val & Nat:
277  (k, a) = kr
278  (v, b) = vr
279  (t, c) = r
280  size.obj(k, v, (t, (2n + a + b + c : Nat)))
281
282def size.tag(+number: W64, r: Val & Nat) -> Val & Nat:
283  (v, n) = r
284  (Tag{number, v}, (4n + n : Nat))
285
286# v, and at least the number of encode.go steps it takes.
287def size(v: Val) -> Val & Nat:
288  match v:
289    case Arr{items}:
290      match items:
291        case Nil{}:
292          (Arr{Nil{}}, 3n)
293        case Con{h, t}:
294          size.cons(size(h), size(Arr{t}))
295    case Obj{items}:
296      match items:
297        case Nil{}:
298          (Obj{Nil{}}, 3n)
299        case Con{(k, x), t}:
300          size.pair(size(k), size(x), size(Obj{t}))
301    case Tag{number, value}:
302      size.tag(number, size(value))
303    case UInt{value}:
304      (UInt{value}, 3n)
305    case NInt{value}:
306      (NInt{value}, 3n)
307    case BStr{value}:
308      (BStr{value}, 3n)
309    case TStr{value}:
310      (TStr{value}, 3n)
311    case Sim{value}:
312      (Sim{value}, 3n)
313    case Flt{value}:
314      (Flt{value}, 3n)
315
316# fuel bounds the steps; size(v) gives enough, so the 0n arm is never reached.
317def encode.go(fuel: Nat, items: List<&1, Item>, o: W) -> Maybe<&1, W>:
318  match fuel:
319    case 0n:
320      None{}
321    case 1n+fuel:
322      match items:
323        case Nil{}:
324          Some{o}
325        case Con{IGuard{ok}, rest}:
326          match ok:
327            case True{}:
328              encode.go(fuel, rest, o)
329            case False{}:
330              None{}
331        case Con{IText{value}, rest}:
332          (b, ok) = value
333          Bytes.Bytes{+len, buf} = b
334          encode.go(fuel, Con{IGuard{ok}, rest}, raw.bytes(Bytes.Bytes{len, buf}, head.u32(3, len, o)))
335        case Con{IArrLen{value}, rest}:
336          (xs, n) = value
337          encode.go(fuel, Con{IArr{xs}, rest}, head.u32(4, U32.from_nat(n), o))
338        case Con{IMapLen{value}, rest}:
339          (kvs, n) = value
340          encode.go(fuel, Con{IMap{kvs}, rest}, head.u32(5, U32.from_nat(n), o))
341        case Con{IArr{xs}, rest}:
342          match xs:
343            case Nil{}:
344              encode.go(fuel, rest, o)
345            case Con{h, t}:
346              encode.go(fuel, Con{IVal{h}, Con{IArr{t}, rest}}, o)
347        case Con{IMap{kvs}, rest}:
348          match kvs:
349            case Nil{}:
350              encode.go(fuel, rest, o)
351            case Con{(k, v), t}:
352              encode.go(fuel, Con{IVal{k}, Con{IVal{v}, Con{IMap{t}, rest}}}, o)
353        case Con{IVal{value}, rest}:
354          match value:
355            case UInt{value}:
356              encode.go(fuel, rest, uint.bytes(0, value, o))
357            case NInt{value}:
358              encode.go(fuel, rest, uint.bytes(1, value, o))
359            case BStr{value}:
360              Bytes.Bytes{+len, buf} = value
361              encode.go(fuel, rest, raw.bytes.go(U32.to_nat(len), Bytes.peek(buf, 0), 0, head.u32(2, len, o)))
362            case TStr{value}:
363              encode.go(fuel, Con{IText{text.check(value)}, rest}, o)
364            case Arr{items}:
365              encode.go(fuel, Con{IArrLen{vals.length(items)}, rest}, o)
366            case Obj{items}:
367              encode.go(fuel, Con{IMapLen{pairs.length(items)}, rest}, o)
368            case Tag{number, value}:
369              encode.go(fuel, Con{IVal{value}, rest}, uint.bytes(6, number, o))
370            case Sim{value}:
371              match value:
372                case SFalse{}:
373                  encode.go(fuel, rest, byte(o, 244))
374                case STrue{}:
375                  encode.go(fuel, rest, byte(o, 245))
376                case SNull{}:
377                  encode.go(fuel, rest, byte(o, 246))
378                case SUndefined{}:
379                  encode.go(fuel, rest, byte(o, 247))
380                case Other{+value}:
381                  encode.go(fuel, Con{IGuard{simple.ok(value)}, rest}, head.u32(7, value, o))
382            case Flt{value}:
383              match value:
384                case Half{+bits}:
385                  encode.go(fuel, Con{IGuard{U32.is_lt(bits, 65536)}, rest}, byte(byte(byte(o, 249), (bits >> 8n : U32)), bits))
386                case Single{+bits}:
387                  encode.go(fuel, rest, raw.u32(byte(o, 250), bits))
388                case Double{+bits}:
389                  W64{+hi, +lo} = bits
390                  encode.go(fuel, rest, raw.u32(raw.u32(byte(o, 251), hi), lo))
391
392def encode.done(r: Maybe<&1, W>) -> Maybe<&1, Bytes.Bytes>:
393  match r:
394    case Some{o}:
395      Some{finish(o)}
396    case None{}:
397      None{}
398
399def encode.sized(r: Val & Nat) -> Maybe<&1, Bytes.Bytes>:
400  (v, n) = r
401  encode.done(encode.go((1n + n : Nat), Con{IVal{v}, Nil{}}, empty()))
402
403# Definite lengths and the shortest head for every length, integer, and tag; floats keep their width.
404# None when a TStr is not UTF-8, a Half has more than 16 bits, or Other is not a simple value 0..19 or 32..255.
405def encode(v: Val) -> Maybe<&1, Bytes.Bytes>:
406  encode.sized(size(v))
407
408def decode.other(ok: Bool, +value: U32) -> Maybe<&1, Val>:
409  match ok:
410    case True{}:
411      Some{Sim{Other{value}}}
412    case False{}:
413      None{}
414
415def decode.simple(+ai: U32) -> Maybe<&1, Val>:
416  match ai:
417    case 20:
418      Some{Sim{SFalse{}}}
419    case 21:
420      Some{Sim{STrue{}}}
421    case 22:
422      Some{Sim{SNull{}}}
423    case 23:
424      Some{Sim{SUndefined{}}}
425    case _:
426      decode.other(U32.is_lt(ai, 20), ai)
427
428def decode.major7.arg(+ai: U32, +arg: W64) -> Maybe<&1, Val>:
429  match ai:
430    case 24:
431      W64{+hi, +lo} = arg
432      decode.other(U32.is_le(32, lo) && U32.is_le(lo, 255), lo)
433    case 25:
434      W64{hi, lo} = arg
435      Some{Flt{Half{lo}}}
436    case 26:
437      W64{hi, lo} = arg
438      Some{Flt{Single{lo}}}
439    case 27:
440      Some{Flt{Double{arg}}}
441    case _:
442      None{}
443
444def decode.major7(small: Bool, +ai: U32, +arg: W64) -> Maybe<&1, Val>:
445  match small:
446    case True{}:
447      decode.simple(ai)
448    case False{}:
449      decode.major7.arg(ai, arg)
450
451# A head: major type, additional info, argument, and the index after it.
452type Hd is Data:
453  Hd{major: U32, ai: U32, arg: W64, next: U32}
454
455# n argument bytes from j, most significant first.
456def hd.words(n: Nat, r: Array<U32> & U32, +j: U32, +hi: U32, +lo: U32, +major: U32, +ai: U32) -> Array<U32> & Maybe<&2, Hd>:
457  match n:
458    case 0n:
459      (a, b) = r
460      (a, Some{Hd{major, ai, W64{hi, lo}, j}})
461    case 1n+p:
462      (a, +b) = r
463      hd.words(p, Bytes.peek(a, (j + 1 : U32)), (j + 1 : U32), ((hi << 8n) .|. (lo >> 24n) : U32), ((lo << 8n) .|. b : U32), major, ai)
464
465def hd.wide(ok: Bool, n: Nat, a: Array<U32>, +i: U32, +major: U32, +ai: U32) -> Array<U32> & Maybe<&2, Hd>:
466  match ok:
467    case True{}:
468      hd.words(n, Bytes.peek(a, (i + 1 : U32)), (i + 1 : U32), 0, 0, major, ai)
469    case False{}:
470      (a, None{})
471
472# ai 24..27 take 1, 2, 4 or 8 more bytes; 28..30 are reserved; 31 is indefinite or break.
473def hd.arg(+ai: U32, a: Array<U32>, +len: U32, +i: U32, +major: U32) -> Array<U32> & Maybe<&2, Hd>:
474  match ai:
475    case 24:
476      hd.wide(Bytes.fits(len, (i + 1 : U32), 1), 1n, a, i, major, 24)
477    case 25:
478      hd.wide(Bytes.fits(len, (i + 1 : U32), 2), 2n, a, i, major, 25)
479    case 26:
480      hd.wide(Bytes.fits(len, (i + 1 : U32), 4), 4n, a, i, major, 26)
481    case 27:
482      hd.wide(Bytes.fits(len, (i + 1 : U32), 8), 8n, a, i, major, 27)
483    case 28:
484      (a, None{})
485    case 29:
486      (a, None{})
487    case 30:
488      (a, None{})
489    case _:
490      (a, Some{Hd{major, ai, W64{0, ai}, (i + 1 : U32)}})
491
492def hd.of(+len: U32, +i: U32, r: Array<U32> & U32) -> Array<U32> & Maybe<&2, Hd>:
493  (a, +b) = r
494  hd.arg((b .&. 31 : U32), a, len, i, (b >> 5n : U32))
495
496def hd.read(ok: Bool, a: Array<U32>, +len: U32, +i: U32) -> Array<U32> & Maybe<&2, Hd>:
497  match ok:
498    case True{}:
499      hd.of(len, i, Bytes.peek(a, i))
500    case False{}:
501      (a, None{})
502
503def bstr.some(+n: U32, r: Array<U32> & Array<U32>) -> Array<U32> & Maybe<&1, Bytes.Bytes>:
504  (a, out) = r
505  (a, Some{Bytes.Bytes{n, out}})
506
507def bstr.copy(+n: U32, +i: U32, r: Array<U32> & Bool) -> Array<U32> & Maybe<&1, Bytes.Bytes>:
508  (a, ok) = r
509  match ok:
510    case True{}:
511      bstr.some(n, Bytes.copy(n, a, Bytes.alloc(n), i, 0))
512    case False{}:
513      (a, None{})
514
515def bstr.valid(text: Bool, a: Array<U32>, +i: U32, +end: U32) -> Array<U32> & Bool:
516  match text:
517    case True{}:
518      utf8.check(a, i, end)
519    case False{}:
520      (a, True{})
521
522def bstr.fit(ok: Bool, +text: Bool, a: Array<U32>, +n: U32, +i: U32) -> Array<U32> & Maybe<&1, Bytes.Bytes>:
523  match ok:
524    case True{}:
525      bstr.copy(n, i, bstr.valid(text, a, i, (i + n : U32)))
526    case False{}:
527      (a, None{})
528
529# A definite string of arg bytes from i. None when it runs past len, or when text is not UTF-8.
530def bstr.read(+text: Bool, +arg: W64, a: Array<U32>, +len: U32, +i: U32) -> Array<U32> & Maybe<&1, Bytes.Bytes>:
531  W64{+hi, +lo} = arg
532  bstr.fit(U32.is_eq(hi, 0) && Bytes.fits(len, i, lo), text, a, lo, i)
533
534def wrap(text: Bool, b: Bytes.Bytes) -> Val:
535  match text:
536    case True{}:
537      TStr{b}
538    case False{}:
539      BStr{b}
540
541# An open container. Items are reversed; left counts the definite items (or pairs) still due, this one included.
542type Frame is Type:
543  FArr{left: U32, xs: List<&1, Val>}
544  FArrI{xs: List<&1, Val>}
545  FMap{left: U32, kvs: List<&1, Val & Val>}
546  FKey{left: U32, kvs: List<&1, Val & Val>, key: Val}
547  FMapI{kvs: List<&1, Val & Val>}
548  FKeyI{kvs: List<&1, Val & Val>, key: Val}
549  FTag{number: W64}
550
551# SHead reads an item at i; SChunk reads the next chunk of an indefinite string; SDone hands v to the open frame.
552type St is Type:
553  SHead{i: U32, stack: List<&1, Frame>}
554  SChunk{i: U32, text: Bool, chunks: List<&1, Bytes.Bytes>, stack: List<&1, Frame>}
555  SDone{v: Val, i: U32, stack: List<&1, Frame>}
556  SOk{v: Val}
557  SFail{}
558
559def item.str(+text: Bool, +i: U32, stack: List<&1, Frame>, r: Array<U32> & Maybe<&1, Bytes.Bytes>) -> Array<U32> & St:
560  (a, m) = r
561  match m:
562    case Some{b}:
563      Bytes.Bytes{+n, buf} = b
564      (a, SDone{wrap(text, Bytes.Bytes{n, buf}), (i + n : U32), stack})
565    case None{}:
566      (a, SFail{})
567
568def item.empty(map: Bool, +i: U32, stack: List<&1, Frame>) -> St:
569  match map:
570    case True{}:
571      SDone{Obj{Nil{}}, i, stack}
572    case False{}:
573      SDone{Arr{Nil{}}, i, stack}
574
575def item.push(map: Bool, +n: U32, +i: U32, stack: List<&1, Frame>) -> St:
576  match map:
577    case True{}:
578      SHead{i, Con{FMap{n, Nil{}}, stack}}
579    case False{}:
580      SHead{i, Con{FArr{n, Nil{}}, stack}}
581
582def item.open(empty: Bool, +map: Bool, +n: U32, +i: U32, stack: List<&1, Frame>) -> St:
583  match empty:
584    case True{}:
585      item.empty(map, i, stack)
586    case False{}:
587      item.push(map, n, i, stack)
588
589def item.count(ok: Bool, +map: Bool, +n: U32, +i: U32, stack: List<&1, Frame>) -> St:
590  match ok:
591    case True{}:
592      item.open(U32.is_eq(n, 0), map, n, i, stack)
593    case False{}:
594      SFail{}
595
596# Every item takes a byte, so a count past the bytes left is malformed; this also keeps it in a U32.
597def item.len(+map: Bool, +arg: W64, +len: U32, +i: U32, stack: List<&1, Frame>) -> St:
598  W64{+hi, +lo} = arg
599  item.count(U32.is_eq(hi, 0) && U32.is_le(lo, (len - i : U32)), map, lo, i, stack)
600
601def item.simple(m: Maybe<&1, Val>, +i: U32, stack: List<&1, Frame>) -> St:
602  match m:
603    case Some{v}:
604      SDone{v, i, stack}
605    case None{}:
606      SFail{}
607
608def item.def(+major: U32, +ai: U32, +arg: W64, +i: U32, a: Array<U32>, +len: U32, stack: List<&1, Frame>) -> Array<U32> & St:
609  match major:
610    case 0:
611      (a, SDone{UInt{arg}, i, stack})
612    case 1:
613      (a, SDone{NInt{arg}, i, stack})
614    case 2:
615      item.str(False{}, i, stack, bstr.read(False{}, arg, a, len, i))
616    case 3:
617      item.str(True{}, i, stack, bstr.read(True{}, arg, a, len, i))
618    case 4:
619      (a, item.len(False{}, arg, len, i, stack))
620    case 5:
621      (a, item.len(True{}, arg, len, i, stack))
622    case 6:
623      (a, SHead{i, Con{FTag{arg}, stack}})
624    case _:
625      (a, item.simple(decode.major7(U32.is_lt(ai, 24), ai, arg), i, stack))
626
627# A break closes the innermost indefinite array, or map with no key pending; anywhere else it is malformed.
628def brk.fr(fr: Frame, +i: U32, rest: List<&1, Frame>) -> St:
629  match fr:
630    case FArrI{xs}:
631      SDone{Arr{List.reverse(&1, Val, xs)}, i, rest}
632    case FMapI{kvs}:
633      SDone{Obj{List.reverse(&1, Val & Val, kvs)}, i, rest}
634    case FArr{left, xs}:
635      SFail{}
636    case FMap{left, kvs}:
637      SFail{}
638    case FKey{left, kvs, k}:
639      SFail{}
640    case FKeyI{kvs, k}:
641      SFail{}
642    case FTag{number}:
643      SFail{}
644
645def brk(stack: List<&1, Frame>, +i: U32) -> St:
646  match stack:
647    case Nil{}:
648      SFail{}
649    case Con{fr, rest}:
650      brk.fr(fr, i, rest)
651
652# ai 31: indefinite string, array, or map, or (major 7) a break. Majors 0, 1 and 6 have no indefinite form.
653def item.indef(+major: U32, +i: U32, stack: List<&1, Frame>) -> St:
654  match major:
655    case 2:
656      SChunk{i, False{}, Nil{}, stack}
657    case 3:
658      SChunk{i, True{}, Nil{}, stack}
659    case 4:
660      SHead{i, Con{FArrI{Nil{}}, stack}}
661    case 5:
662      SHead{i, Con{FMapI{Nil{}}, stack}}
663    case 7:
664      brk(stack, i)
665    case _:
666      SFail{}
667
668def item.hd(indef: Bool, +major: U32, +ai: U32, +arg: W64, +i: U32, a: Array<U32>, +len: U32, stack: List<&1, Frame>) -> Array<U32> & St:
669  match indef:
670    case True{}:
671      (a, item.indef(major, i, stack))
672    case False{}:
673      item.def(major, ai, arg, i, a, len, stack)
674
675def step.head(stack: List<&1, Frame>, +len: U32, r: Array<U32> & Maybe<&2, Hd>) -> Array<U32> & St:
676  (a, h) = r
677  match h:
678    case Some{Hd{+major, +ai, +arg, +i}}:
679      item.hd(U32.is_eq(ai, 31), major, ai, arg, i, a, len, stack)
680    case None{}:
681      (a, SFail{})
682
683def chunk.str(+text: Bool, chunks: List<&1, Bytes.Bytes>, +i: U32, stack: List<&1, Frame>, r: Array<U32> & Maybe<&1, Bytes.Bytes>) -> Array<U32> & St:
684  (a, m) = r
685  match m:
686    case Some{b}:
687      Bytes.Bytes{+n, buf} = b
688      (a, SChunk{(i + n : U32), text, Con{Bytes.Bytes{n, buf}, chunks}, stack})
689    case None{}:
690      (a, SFail{})
691
692def chunk.more(ok: Bool, +text: Bool, chunks: List<&1, Bytes.Bytes>, +arg: W64, +i: U32, a: Array<U32>, +len: U32, stack: List<&1, Frame>) -> Array<U32> & St:
693  match ok:
694    case True{}:
695      chunk.str(text, chunks, i, stack, bstr.read(text, arg, a, len, i))
696    case False{}:
697      (a, SFail{})
698
699# Each chunk is a definite string of the same major type, UTF-8 by itself for text (RFC 8949 §3.2.3).
700def chunk.end(stop: Bool, ok: Bool, +text: Bool, chunks: List<&1, Bytes.Bytes>, +arg: W64, +i: U32, a: Array<U32>, +len: U32, stack: List<&1, Frame>) -> Array<U32> & St:
701  match stop:
702    case True{}:
703      (a, SDone{wrap(text, Bytes.concat(List.reverse(&1, Bytes.Bytes, chunks))), i, stack})
704    case False{}:
705      chunk.more(ok, text, chunks, arg, i, a, len, stack)
706
707def step.chunk(+text: Bool, chunks: List<&1, Bytes.Bytes>, stack: List<&1, Frame>, +len: U32, r: Array<U32> & Maybe<&2, Hd>) -> Array<U32> & St:
708  (a, h) = r
709  match h:
710    case Some{Hd{+major, +ai, +arg, +i}}:
711      chunk.end(U32.is_eq(major, 7) && U32.is_eq(ai, 31), U32.is_eq(major, Bool.pick(U32, text, 3, 2)) && U32.is_ne(ai, 31), text, chunks, arg, i, a, len, stack)
712    case None{}:
713      (a, SFail{})
714
715def done.arr(last: Bool, +left: U32, xs: List<&1, Val>, +i: U32, rest: List<&1, Frame>) -> St:
716  match last:
717    case True{}:
718      SDone{Arr{List.reverse(&1, Val, xs)}, i, rest}
719    case False{}:
720      SHead{i, Con{FArr{(left - 1 : U32), xs}, rest}}
721
722def done.map(last: Bool, +left: U32, kvs: List<&1, Val & Val>, +i: U32, rest: List<&1, Frame>) -> St:
723  match last:
724    case True{}:
725      SDone{Obj{List.reverse(&1, Val & Val, kvs)}, i, rest}
726    case False{}:
727      SHead{i, Con{FMap{(left - 1 : U32), kvs}, rest}}
728
729def done.fr(fr: Frame, v: Val, +i: U32, rest: List<&1, Frame>) -> St:
730  match fr:
731    case FArr{+left, xs}:
732      done.arr(U32.is_eq(left, 1), left, Con{v, xs}, i, rest)
733    case FArrI{xs}:
734      SHead{i, Con{FArrI{Con{v, xs}}, rest}}
735    case FMap{+left, kvs}:
736      SHead{i, Con{FKey{left, kvs, v}, rest}}
737    case FKey{+left, kvs, k}:
738      done.map(U32.is_eq(left, 1), left, Con{(k, v), kvs}, i, rest)
739    case FMapI{kvs}:
740      SHead{i, Con{FKeyI{kvs, v}, rest}}
741    case FKeyI{kvs, k}:
742      SHead{i, Con{FMapI{Con{(k, v), kvs}}, rest}}
743    case FTag{number}:
744      SDone{Tag{number, v}, i, rest}
745
746def done.top(end: Bool, v: Val) -> St:
747  match end:
748    case True{}:
749      SOk{v}
750    case False{}:
751      SFail{}
752
753# A finished top-level item must end the input.
754def done(stack: List<&1, Frame>, v: Val, +i: U32, +len: U32) -> St:
755  match stack:
756    case Nil{}:
757      done.top(U32.is_eq(i, len), v)
758    case Con{fr, rest}:
759      done.fr(fr, v, i, rest)
760
761def run(fuel: Nat, r: Array<U32> & St, +len: U32) -> Maybe<&1, Val>:
762  match fuel:
763    case 0n:
764      None{}
765    case 1n+f:
766      (a, st) = r
767      match st:
768        case SOk{v}:
769          Some{v}
770        case SFail{}:
771          None{}
772        case SHead{+i, stack}:
773          run(f, step.head(stack, len, hd.read(U32.is_lt(i, len), a, len, i)), len)
774        case SChunk{+i, +text, chunks, stack}:
775          run(f, step.chunk(text, chunks, stack, len, hd.read(U32.is_lt(i, len), a, len, i)), len)
776        case SDone{v, +i, stack}:
777          run(f, (a, done(stack, v, i, len)), len)
778
779# One well-formed data item (RFC 8949 §3, Appendix C) filling b. Indefinite strings, arrays and maps come back
780# definite, with chunks joined. None for truncation, reserved ai 28..30, a misplaced break or indefinite form,
781# a simple value 0..31 in two bytes, text that is not UTF-8, or trailing bytes.
782# fuel: a head or chunk eats a byte, and each SDone step follows one, so 2 * len + 2 steps are enough.
783def decode(b: Bytes.Bytes) -> Maybe<&1, Val>:
784  Bytes.Bytes{+len, buf} = b
785  run(Nat.add(Nat.mul(U32.to_nat(len), 2n), 2n), (buf, SHead{0, Nil{}}), len)