cbor.bend
bend-kit-cbor@0.1.0.1 · 785 lines · 0 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.0.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)