protobuf.bend
bend-kit-protobuf@0.2.0.0 · 812 lines · 125 definitions
1
2import Base
3import bend-kit-bytes@0.3.3.0/bytes.bend as B
4import bend-kit-f64@0.1.0.0/f64.bend as F
5
6
7type Word64 is Data:
8 Word64{hi: U32, lo: U32}
9
10type Error is Data:
11 Incomplete{}
12 Malformed{}
13 Limit{}
14 InvalidUtf8{}
15
16type Value is Type:
17 Varint{value: Word64}
18 Fixed32{value: U32}
19 Fixed64{value: Word64}
20 Blob{value: B.Bytes}
21 Group{fields: List<&1, Field>}
22
23type Field is Type:
24 Field{number: U32, value: Value}
25
26def valid_number(+n: U32) -> Bool:
27 U32.is_ge(n, 1) && U32.is_le(n, 536870911)
28
29def Word64.zero() -> Word64:
30 Word64{0, 0}
31
32def Word64.is_zero(w: Word64) -> Bool:
33 Word64{h, l} = w
34 U32.is_zero(h) && U32.is_zero(l)
35
36def Word64.shr7(w: Word64) -> Word64:
37 Word64{+h, l} = w
38 Word64{(h >> 7n : U32), ((l >> 7n) .|. (h << 25n) : U32)}
39
40def Word64.zigzag(w: Word64) -> Word64:
41 Word64{+h, +l} = w
42 +mask = (0 - (h >> 31n) : U32)
43 Word64{(((h << 1n) .|. (l >> 31n)) .^. mask : U32), ((l << 1n) .^. mask : U32)}
44
45def Word64.unzigzag(w: Word64) -> Word64:
46 Word64{+h, +l} = w
47 +mask = (0 - (l .&. 1) : U32)
48 Word64{((h >> 1n) .^. mask : U32), (((l >> 1n) .|. (h << 31n)) .^. mask : U32)}
49
50def read32.result(r: B.Cursor & Maybe<&2, U32>) -> Result<&2, &1, Error, B.Cursor & U32>:
51 (c, v) = r
52 match v:
53 case None{}:
54 Fail{Incomplete{}}
55 case Some{x}:
56 Done{(c, x)}
57
58def read32(c: B.Cursor) -> Result<&2, &1, Error, B.Cursor & U32>:
59 read32.result(B.Cursor.u32le(c))
60
61def read64.hi(l: U32, r: B.Cursor & U32) -> Result<&2, &1, Error, B.Cursor & Word64>:
62 (c, h) = r
63 Done{(c, Word64{h, l})}
64
65def read64.lo(r: B.Cursor & U32) -> Result<&2, &1, Error, B.Cursor & Word64>:
66 (c, l) = r
67 do Result<&2, &1, Error, B.Cursor & Word64>:
68 high : B.Cursor & U32 <- read32(c)
69 read64.hi(l, high)
70
71def read64(c: B.Cursor) -> Result<&2, &1, Error, B.Cursor & Word64>:
72 do Result<&2, &1, Error, B.Cursor & Word64>:
73 low : B.Cursor & U32 <- read32(c)
74 read64.lo(low)
75
76def varint.add.low(fifth: Bool, +i: U32, +v: U32, h: U32, l: U32) -> Word64:
77 match fifth:
78 case False{}:
79 Word64{h, (l .|. (v << U32.to_nat((i * 7 : U32))) : U32)}
80 case True{}:
81 Word64{(h .|. (v >> 4n) : U32), (l .|. (v << 28n) : U32)}
82
83def varint.add.pick(low: Bool, +i: U32, +v: U32, w: Word64) -> Word64:
84 match low:
85 case True{}:
86 Word64{h, l} = w
87 varint.add.low(U32.is_eq(i, 4), i, v, h, l)
88 case False{}:
89 Word64{h, l} = w
90 Word64{(h .|. (v << U32.to_nat((i * 7 - 32 : U32))) : U32), l}
91
92def varint.add(+i: U32, +v: U32, w: Word64) -> Word64:
93 varint.add.pick(U32.is_lt(i, 5), i, v, w)
94
95type VarintByte is Data:
96 VarintByte{bad: Bool, done: Bool, value: U32}
97
98def varint.read.result(i: U32, last: U32, max_last: U32, r: B.Cursor & Maybe<&2, U32>) -> B.Cursor & Maybe<&2, VarintByte>:
99 (c, m) = r
100 match m:
101 case None{}:
102 (c, None{})
103 case Some{+b}:
104 (c, Some{VarintByte{U32.is_eq(i, last) && U32.is_gt(b, max_last), U32.is_lt(b, 128), b}})
105
106def varint.read(+i: U32, last: U32, max_last: U32, c: B.Cursor) -> B.Cursor & Maybe<&2, VarintByte>:
107 varint.read.result(i, last, max_last, B.Cursor.u8(c))
108
109
110def varint.go(fuel: Nat, r: B.Cursor & Maybe<&2, VarintByte>, +i: U32, +last: U32, +max_last: U32, w: Word64) -> Result<&2, &1, Error, B.Cursor & Word64>:
111 match fuel:
112 case 0n:
113 Fail{Malformed{}}
114 case 1n+p:
115 (c, v) = r
116 match v:
117 case None{}:
118 Fail{Incomplete{}}
119 case Some{VarintByte{bad, done, b}}:
120 match bad:
121 case True{}:
122 Fail{Malformed{}}
123 case False{}:
124 match done:
125 case True{}:
126 Done{(c, varint.add(i, (b .&. 127 : U32), w))}
127 case False{}:
128 varint.go(p, varint.read((i + 1 : U32), last, max_last, c), (i + 1 : U32), last, max_last, varint.add(i, (b .&. 127 : U32), w))
129
130def read_varint(c: B.Cursor) -> Result<&2, &1, Error, B.Cursor & Word64>:
131 varint.go(10n, varint.read(0, 9, 1, c), 0, 9, 1, Word64{0, 0})
132
133def read_varint32(c: B.Cursor) -> Result<&2, &1, Error, B.Cursor & Word64>:
134 varint.go(5n, varint.read(0, 4, 15, c), 0, 4, 15, Word64{0, 0})
135
136def read_blob.slice(pos: U32, start: U32, end: U32, r: B.Bytes & B.Bytes) -> Result<&2, &1, Error, B.Cursor & B.Bytes>:
137 (b, part) = r
138 Done{(B.Cursor{b, pos, start, end}, part)}
139
140def read_blob.fits(fits: Bool, c: B.Cursor, +n: U32) -> Result<&2, &1, Error, B.Cursor & B.Bytes>:
141 match fits:
142 case False{}:
143 Fail{Incomplete{}}
144 case True{}:
145 B.Cursor{b, +pos, start, end} = c
146 read_blob.slice((pos + n : U32), start, end, B.slice(b, pos, n))
147
148def read_blob.length(ok: Bool, c: B.Cursor, +n: U32) -> Result<&2, &1, Error, B.Cursor & B.Bytes>:
149 match ok:
150 case False{}:
151 Fail{Malformed{}}
152 case True{}:
153 B.Cursor{b, +pos, start, +end} = c
154 read_blob.fits(B.fits(end, pos, n), B.Cursor{b, pos, start, end}, n)
155
156def read_blob.word(r: B.Cursor & Word64) -> Result<&2, &1, Error, B.Cursor & B.Bytes>:
157 (c, Word64{h, +l}) = r
158 read_blob.length(U32.is_zero(h) && U32.is_le(l, 2147483647), c, l)
159
160def read_blob(c: B.Cursor) -> Result<&2, &1, Error, B.Cursor & B.Bytes>:
161 do Result<&2, &1, Error, B.Cursor & B.Bytes>:
162 r : B.Cursor & Word64 <- read_varint32(c)
163 read_blob.word(r)
164
165def read_value.varint(r: B.Cursor & Word64) -> Result<&2, &1, Error, B.Cursor & Value>:
166 (c, v) = r
167 Done{(c, Varint{v})}
168
169def read_value.fixed64(r: B.Cursor & Word64) -> Result<&2, &1, Error, B.Cursor & Value>:
170 (c, v) = r
171 Done{(c, Fixed64{v})}
172
173def read_value.blob(r: B.Cursor & B.Bytes) -> Result<&2, &1, Error, B.Cursor & Value>:
174 (c, v) = r
175 Done{(c, Blob{v})}
176
177def read_value.fixed32(r: B.Cursor & U32) -> Result<&2, &1, Error, B.Cursor & Value>:
178 (c, v) = r
179 Done{(c, Fixed32{v})}
180
181def read_value(kind: U32, c: B.Cursor) -> Result<&2, &1, Error, B.Cursor & Value>:
182 match kind:
183 case 0:
184 do Result<&2, &1, Error, B.Cursor & Value>:
185 r : B.Cursor & Word64 <- read_varint(c)
186 read_value.varint(r)
187 case 1:
188 do Result<&2, &1, Error, B.Cursor & Value>:
189 r : B.Cursor & Word64 <- read64(c)
190 read_value.fixed64(r)
191 case 2:
192 do Result<&2, &1, Error, B.Cursor & Value>:
193 r : B.Cursor & B.Bytes <- read_blob(c)
194 read_value.blob(r)
195 case 5:
196 do Result<&2, &1, Error, B.Cursor & Value>:
197 r : B.Cursor & U32 <- read32(c)
198 read_value.fixed32(r)
199 case _:
200 Fail{Malformed{}}
201
202type Frame is Type:
203 Frame{number: U32, outer: List<&1, Field>, depth: Nat}
204
205
206type DecodeState is Type:
207 DecodeState{empty: Bool, cursor: B.Cursor, depth: Nat, stack: List<&1, Frame>, acc: List<&1, Field>}
208
209def decode.state(cursor: B.Cursor, depth: Nat, stack: List<&1, Frame>, acc: List<&1, Field>) -> DecodeState:
210 B.Cursor{b, +pos, start, +end} = cursor
211 DecodeState{U32.is_ge(pos, end), B.Cursor{b, pos, start, end}, depth, stack, acc}
212
213def decode.step.value(depth: Nat, stack: List<&1, Frame>, acc: List<&1, Field>, number: U32, r: B.Cursor & Value) -> Result<&2, &1, Error, DecodeState>:
214 (c, v) = r
215 Done{decode.state(c, depth, stack, Con{Field{number, v}, acc})}
216
217def decode.step.close(ok: Bool, c: B.Cursor, number: U32, outer: List<&1, Field>, depth: Nat, stack: List<&1, Frame>, acc: List<&1, Field>) -> Result<&2, &1, Error, DecodeState>:
218 match ok:
219 case False{}:
220 Fail{Malformed{}}
221 case True{}:
222 Done{decode.state(c, depth, stack, Con{Field{number, Group{List.reverse(&1, Field, acc)}}, outer})}
223
224def decode.step.kind(kind: U32, c: B.Cursor, +depth: Nat, stack: List<&1, Frame>, acc: List<&1, Field>, +number: U32) -> Result<&2, &1, Error, DecodeState>:
225 match kind:
226 case 3:
227 match depth:
228 case 0n:
229 Fail{Limit{}}
230 case 1n+d:
231 Done{decode.state(c, d, Con{Frame{number, acc, 1n+d}, stack}, Nil{})}
232 case 4:
233 match stack:
234 case Nil{}:
235 Fail{Malformed{}}
236 case Con{Frame{expected, outer, parent_depth}, tail}:
237 decode.step.close(U32.is_eq(number, expected), c, number, outer, parent_depth, tail, acc)
238 case _:
239 do Result<&2, &1, Error, DecodeState>:
240 r : B.Cursor & Value <- read_value(kind, c)
241 decode.step.value(depth, stack, acc, number, r)
242
243def decode.step.valid(ok: Bool, kind: U32, c: B.Cursor, depth: Nat, stack: List<&1, Frame>, acc: List<&1, Field>, number: U32) -> Result<&2, &1, Error, DecodeState>:
244 match ok:
245 case False{}:
246 Fail{Malformed{}}
247 case True{}:
248 decode.step.kind(kind, c, depth, stack, acc, number)
249
250def decode.step.tag(depth: Nat, stack: List<&1, Frame>, acc: List<&1, Field>, tag: B.Cursor & Word64) -> Result<&2, &1, Error, DecodeState>:
251 (c, Word64{hi, +lo}) = tag
252 +number = (lo >> 3n : U32)
253 decode.step.valid(U32.is_zero(hi) && valid_number(number), (lo .&. 7 : U32), c, depth, stack, acc, number)
254
255def decode.step(c: B.Cursor, depth: Nat, stack: List<&1, Frame>, acc: List<&1, Field>) -> Result<&2, &1, Error, DecodeState>:
256 do Result<&2, &1, Error, DecodeState>:
257 tag : B.Cursor & Word64 <- read_varint32(c)
258 decode.step.tag(depth, stack, acc, tag)
259
260
261def decode.go(fuel: Nat, state: DecodeState) -> Result<&2, &1, Error, List<&1, Field>>:
262 match fuel:
263 case 0n:
264 Fail{Limit{}}
265 case 1n+p:
266 DecodeState{empty, c, depth, stack, acc} = state
267 match empty:
268 case True{}:
269 match stack:
270 case Nil{}:
271 Done{List.reverse(&1, Field, acc)}
272 case Con{h, t}:
273 Fail{Incomplete{}}
274 case False{}:
275 do Result<&2, &1, Error, List<&1, Field>>:
276 next : DecodeState <- decode.step(c, depth, stack, acc)
277 decode.go(p, next)
278
279def decode.limit(ok: Bool, b: B.Bytes, +n: U32, depth: Nat) -> Result<&2, &1, Error, List<&1, Field>>:
280 match ok:
281 case False{}:
282 Fail{Limit{}}
283 case True{}:
284 decode.go(1n+U32.to_nat(n), decode.state(B.Cursor.new(b), depth, Nil{}, Nil{}))
285
286def decode(b: B.Bytes, max_size: U32, depth: Nat) -> Result<&2, &1, Error, List<&1, Field>>:
287 B.Bytes{+n, buf} = b
288 decode.limit(U32.is_le(n, U32.min(max_size, 2147483647)), B.Bytes{n, buf}, n, depth)
289
290
291def append.limit(ok: Bool, out: B.Bytes, part: B.Bytes) -> Result<&2, &1, Error, B.Bytes>:
292 match ok:
293 case True{}:
294 Done{B.append(out, part)}
295 case False{}:
296 Fail{Limit{}}
297
298def append(out: B.Bytes, part: B.Bytes, +max_size: U32) -> Result<&2, &1, Error, B.Bytes>:
299 B.Bytes{+n, a_buf} = out
300 B.Bytes{+m, b_buf} = part
301 +limit = U32.min(max_size, 2147483647)
302 append.limit(U32.is_le(n, limit) && U32.is_le(m, (limit - n : U32)), B.Bytes{n, a_buf}, B.Bytes{m, b_buf})
303
304def byte.limit(ok: Bool, +n: U32, buf: Array<U32>, v: U32) -> Result<&2, &1, Error, B.Bytes>:
305 match ok:
306 case False{}:
307 Fail{Limit{}}
308 case True{}:
309 Done{B.Bytes{(n + 1 : U32), B.poke(B.grow(n, buf, (n + 1 : U32)), n, v)}}
310
311def byte(out: B.Bytes, v: U32, max_size: U32) -> Result<&2, &1, Error, B.Bytes>:
312 B.Bytes{+n, buf} = out
313 byte.limit(U32.is_lt(n, U32.min(max_size, 2147483647)), n, buf, v)
314
315def write_varint.done(w: Word64) -> Bool:
316 Word64{h, l} = w
317 U32.is_zero(h) && U32.is_lt(l, 128)
318
319def write_varint.go(fuel: Nat, done: Bool, w: Word64, out: B.Bytes, +max_size: U32) -> Result<&2, &1, Error, B.Bytes>:
320 match fuel:
321 case 0n:
322 Fail{Malformed{}}
323 case 1n+p:
324 match done:
325 case True{}:
326 Word64{h, l} = w
327 byte(out, l, max_size)
328 case False{}:
329 Word64{+h, +l} = w
330 +rest = Word64.shr7(Word64{h, l})
331 do Result<&2, &1, Error, B.Bytes>:
332 next : B.Bytes <- byte(out, ((l .&. 127) .|. 128 : U32), max_size)
333 write_varint.go(p, write_varint.done(rest), rest, next, max_size)
334
335def write_varint(+w: Word64, out: B.Bytes, max_size: U32) -> Result<&2, &1, Error, B.Bytes>:
336 write_varint.go(10n, write_varint.done(w), w, out, max_size)
337
338def write_tag.valid(valid: Bool, number: U32, kind: U32, out: B.Bytes, max_size: U32) -> Result<&2, &1, Error, B.Bytes>:
339 match valid:
340 case False{}:
341 Fail{Malformed{}}
342 case True{}:
343 write_varint(Word64{0, ((number << 3n) .|. kind : U32)}, out, max_size)
344
345def write_tag(+number: U32, kind: U32, out: B.Bytes, max_size: U32) -> Result<&2, &1, Error, B.Bytes>:
346 write_tag.valid(valid_number(number), number, kind, out, max_size)
347
348def write_fixed32.limit(ok: Bool, +n: U32, buf: Array<U32>, v: U32) -> Result<&2, &1, Error, B.Bytes>:
349 match ok:
350 case False{}:
351 Fail{Limit{}}
352 case True{}:
353 Done{B.set.u32le(B.Bytes{(n + 4 : U32), B.grow(n, buf, (n + 4 : U32))}, n, v)}
354
355def write_fixed32(v: U32, out: B.Bytes, max_size: U32) -> Result<&2, &1, Error, B.Bytes>:
356 B.Bytes{+n, buf} = out
357 +limit = U32.min(max_size, 2147483647)
358 write_fixed32.limit(U32.is_le(n, limit) && U32.is_le(4, (limit - n : U32)), n, buf, v)
359
360def write_fixed64.limit(ok: Bool, +n: U32, buf: Array<U32>, v: Word64) -> Result<&2, &1, Error, B.Bytes>:
361 match ok:
362 case False{}:
363 Fail{Limit{}}
364 case True{}:
365 Word64{h, l} = v
366 Done{B.set.u32le(B.set.u32le(B.Bytes{(n + 8 : U32), B.grow(n, buf, (n + 8 : U32))}, n, l), (n + 4 : U32), h)}
367
368def write_fixed64(v: Word64, out: B.Bytes, max_size: U32) -> Result<&2, &1, Error, B.Bytes>:
369 B.Bytes{+n, buf} = out
370 +limit = U32.min(max_size, 2147483647)
371 write_fixed64.limit(U32.is_le(n, limit) && U32.is_le(8, (limit - n : U32)), n, buf, v)
372
373def write_value(v: Value, out: B.Bytes, +max_size: U32) -> Result<&2, &1, Error, B.Bytes>:
374 match v:
375 case Varint{w}:
376 write_varint(w, out, max_size)
377 case Fixed32{w}:
378 write_fixed32(w, out, max_size)
379 case Fixed64{w}:
380 write_fixed64(w, out, max_size)
381 case Blob{b}:
382 B.Bytes{+n, buf} = b
383 do Result<&2, &1, Error, B.Bytes>:
384 next : B.Bytes <- write_varint(Word64{0, n}, out, max_size)
385 append(next, B.Bytes{n, buf}, max_size)
386 case Group{fields}:
387 Fail{Malformed{}}
388
389def write_field(number: U32, v: Value, out: B.Bytes, +max_size: U32) -> Result<&2, &1, Error, B.Bytes>:
390 match v:
391 case Varint{w}:
392 do Result<&2, &1, Error, B.Bytes>:
393 next : B.Bytes <- write_tag(number, 0, out, max_size)
394 write_value(Varint{w}, next, max_size)
395 case Fixed64{w}:
396 do Result<&2, &1, Error, B.Bytes>:
397 next : B.Bytes <- write_tag(number, 1, out, max_size)
398 write_value(Fixed64{w}, next, max_size)
399 case Blob{b}:
400 do Result<&2, &1, Error, B.Bytes>:
401 next : B.Bytes <- write_tag(number, 2, out, max_size)
402 write_value(Blob{b}, next, max_size)
403 case Fixed32{w}:
404 do Result<&2, &1, Error, B.Bytes>:
405 next : B.Bytes <- write_tag(number, 5, out, max_size)
406 write_value(Fixed32{w}, next, max_size)
407 case Group{fields}:
408 Fail{Malformed{}}
409
410
411def encode.go(+depth: Nat, fields: List<&1, Field>, out: B.Bytes, +max_size: U32) -> Result<&2, &1, Error, B.Bytes>:
412 match depth:
413 case 0n:
414 match fields:
415 case Nil{}:
416 Done{out}
417 case Con{Field{number, value}, tail}:
418 match value:
419 case Group{inner}:
420 Fail{Limit{}}
421 case Varint{w}:
422 do Result<&2, &1, Error, B.Bytes>:
423 next : B.Bytes <- write_field(number, Varint{w}, out, max_size)
424 encode.go(0n, tail, next, max_size)
425 case Fixed32{w}:
426 do Result<&2, &1, Error, B.Bytes>:
427 next : B.Bytes <- write_field(number, Fixed32{w}, out, max_size)
428 encode.go(0n, tail, next, max_size)
429 case Fixed64{w}:
430 do Result<&2, &1, Error, B.Bytes>:
431 next : B.Bytes <- write_field(number, Fixed64{w}, out, max_size)
432 encode.go(0n, tail, next, max_size)
433 case Blob{b}:
434 do Result<&2, &1, Error, B.Bytes>:
435 next : B.Bytes <- write_field(number, Blob{b}, out, max_size)
436 encode.go(0n, tail, next, max_size)
437 case 1n+p:
438 match fields:
439 case Nil{}:
440 Done{out}
441 case Con{Field{+number, value}, tail}:
442 match value:
443 case Group{inner}:
444 do Result<&2, &1, Error, B.Bytes>:
445 start : B.Bytes <- write_tag(number, 3, out, max_size)
446 body : B.Bytes <- encode.go(p, inner, start, max_size)
447 end : B.Bytes <- write_tag(number, 4, body, max_size)
448 encode.go(1n+p, tail, end, max_size)
449 case Varint{w}:
450 do Result<&2, &1, Error, B.Bytes>:
451 next : B.Bytes <- write_field(number, Varint{w}, out, max_size)
452 encode.go(1n+p, tail, next, max_size)
453 case Fixed32{w}:
454 do Result<&2, &1, Error, B.Bytes>:
455 next : B.Bytes <- write_field(number, Fixed32{w}, out, max_size)
456 encode.go(1n+p, tail, next, max_size)
457 case Fixed64{w}:
458 do Result<&2, &1, Error, B.Bytes>:
459 next : B.Bytes <- write_field(number, Fixed64{w}, out, max_size)
460 encode.go(1n+p, tail, next, max_size)
461 case Blob{b}:
462 do Result<&2, &1, Error, B.Bytes>:
463 next : B.Bytes <- write_field(number, Blob{b}, out, max_size)
464 encode.go(1n+p, tail, next, max_size)
465
466def encode(fields: List<&1, Field>, max_size: U32, depth: Nat) -> Result<&2, &1, Error, B.Bytes>:
467 encode.go(depth, fields, B.new(0), max_size)
468
469type PackedState is Type:
470 PackedState{empty: Bool, cursor: B.Cursor, acc: List<&1, Value>}
471
472def packed_decode.state(cursor: B.Cursor, acc: List<&1, Value>) -> PackedState:
473 B.Cursor{b, +pos, start, +end} = cursor
474 PackedState{U32.is_ge(pos, end), B.Cursor{b, pos, start, end}, acc}
475
476def packed_decode.step.value(acc: List<&1, Value>, r: B.Cursor & Value) -> Result<&2, &1, Error, PackedState>:
477 (c, v) = r
478 Done{packed_decode.state(c, Con{v, acc})}
479
480def packed_decode.step(kind: U32, c: B.Cursor, acc: List<&1, Value>) -> Result<&2, &1, Error, PackedState>:
481 do Result<&2, &1, Error, PackedState>:
482 r : B.Cursor & Value <- read_value(kind, c)
483 packed_decode.step.value(acc, r)
484
485def packed_decode.go(fuel: Nat, +kind: U32, state: PackedState) -> Result<&2, &1, Error, List<&1, Value>>:
486 match fuel:
487 case 0n:
488 Fail{Limit{}}
489 case 1n+p:
490 PackedState{empty, c, acc} = state
491 match empty:
492 case True{}:
493 Done{List.reverse(&1, Value, acc)}
494 case False{}:
495 do Result<&2, &1, Error, List<&1, Value>>:
496 next : PackedState <- packed_decode.step(kind, c, acc)
497 packed_decode.go(p, kind, next)
498
499def packed_decode.result(r: Result<&2, &1, Error, List<&1, Value>>) -> Result<&2, &1, Error, List<&1, Value>>:
500 match r:
501 case Done{values}:
502 Done{values}
503 case Fail{Incomplete{}}:
504 Fail{Malformed{}}
505 case Fail{e}:
506 Fail{e}
507
508def packed_decode.limit(fits: Bool, kind: U32, bytes: B.Bytes, n: U32) -> Result<&2, &1, Error, List<&1, Value>>:
509 match fits:
510 case False{}:
511 Fail{Limit{}}
512 case True{}:
513 packed_decode.result(packed_decode.go(1n+U32.to_nat(n), kind, packed_decode.state(B.Cursor.new(bytes), Nil{})))
514
515def packed_decode.valid(valid: Bool, kind: U32, b: B.Bytes, max_size: U32) -> Result<&2, &1, Error, List<&1, Value>>:
516 match valid:
517 case False{}:
518 Fail{Malformed{}}
519 case True{}:
520 B.Bytes{+n, buf} = b
521 packed_decode.limit(U32.is_le(n, U32.min(max_size, 2147483647)), kind, B.Bytes{n, buf}, n)
522
523def packed_decode(+kind: U32, b: B.Bytes, max_size: U32) -> Result<&2, &1, Error, List<&1, Value>>:
524 packed_decode.valid(U32.is_eq(kind, 0) || U32.is_eq(kind, 1) || U32.is_eq(kind, 5), kind, b, max_size)
525
526def packed_encode.go(values: List<&1, Value>, out: B.Bytes, +max_size: U32) -> Result<&2, &1, Error, B.Bytes>:
527 match values:
528 case Nil{}:
529 Done{out}
530 case Con{v, tail}:
531 match v:
532 case Varint{w}:
533 do Result<&2, &1, Error, B.Bytes>:
534 next : B.Bytes <- write_value(Varint{w}, out, max_size)
535 packed_encode.go(tail, next, max_size)
536 case Fixed32{w}:
537 do Result<&2, &1, Error, B.Bytes>:
538 next : B.Bytes <- write_value(Fixed32{w}, out, max_size)
539 packed_encode.go(tail, next, max_size)
540 case Fixed64{w}:
541 do Result<&2, &1, Error, B.Bytes>:
542 next : B.Bytes <- write_value(Fixed64{w}, out, max_size)
543 packed_encode.go(tail, next, max_size)
544 case Blob{b}:
545 Fail{Malformed{}}
546 case Group{fields}:
547 Fail{Malformed{}}
548
549def packed_encode(values: List<&1, Value>, max_size: U32) -> Result<&2, &1, Error, B.Bytes>:
550 packed_encode.go(values, B.new(0), max_size)
551
552def from_uint32(v: U32) -> Value:
553 Varint{Word64{0, v}}
554
555def to_uint32(v: Value) -> Result<&2, &2, Error, U32>:
556 match v:
557 case Varint{Word64{h, l}}:
558 Done{l}
559 case _:
560 Fail{Malformed{}}
561
562def from_int32(+v: U32) -> Value:
563 Varint{Word64{(0 - (v >> 31n) : U32), v}}
564
565def to_int32(v: Value) -> Result<&2, &2, Error, U32>:
566 to_uint32(v)
567
568def from_sint32(+v: U32) -> Value:
569 from_uint32(((v << 1n) .^. (0 - (v >> 31n)) : U32))
570
571def unzigzag32(+bits: U32) -> U32:
572 ((bits >> 1n) .^. (0 - (bits .&. 1)) : U32)
573
574def to_sint32(v: Value) -> Result<&2, &2, Error, U32>:
575 do Result<&2, &2, Error, U32>:
576 bits : U32 <- to_uint32(v)
577 return unzigzag32(bits)
578
579def from_fixed32(v: U32) -> Value:
580 Fixed32{v}
581
582def to_fixed32(v: Value) -> Result<&2, &2, Error, U32>:
583 match v:
584 case Fixed32{w}:
585 Done{w}
586 case _:
587 Fail{Malformed{}}
588
589def from_sfixed32(v: U32) -> Value:
590 from_fixed32(v)
591
592def to_sfixed32(v: Value) -> Result<&2, &2, Error, U32>:
593 to_fixed32(v)
594
595def from_uint64(v: Word64) -> Value:
596 Varint{v}
597
598def to_uint64(v: Value) -> Result<&2, &2, Error, Word64>:
599 match v:
600 case Varint{w}:
601 Done{w}
602 case _:
603 Fail{Malformed{}}
604
605def from_int64(v: Word64) -> Value:
606 from_uint64(v)
607
608def to_int64(v: Value) -> Result<&2, &2, Error, Word64>:
609 to_uint64(v)
610
611def from_sint64(v: Word64) -> Value:
612 from_uint64(Word64.zigzag(v))
613
614def to_sint64(v: Value) -> Result<&2, &2, Error, Word64>:
615 do Result<&2, &2, Error, Word64>:
616 bits : Word64 <- to_uint64(v)
617 return Word64.unzigzag(bits)
618
619def from_fixed64(v: Word64) -> Value:
620 Fixed64{v}
621
622def to_fixed64(v: Value) -> Result<&2, &2, Error, Word64>:
623 match v:
624 case Fixed64{w}:
625 Done{w}
626 case _:
627 Fail{Malformed{}}
628
629def from_sfixed64(v: Word64) -> Value:
630 from_fixed64(v)
631
632def to_sfixed64(v: Value) -> Result<&2, &2, Error, Word64>:
633 to_fixed64(v)
634
635def from_bool(v: Bool) -> Value:
636 from_uint32(Bool.to_u32(v))
637
638def to_bool(v: Value) -> Result<&2, &2, Error, Bool>:
639 do Result<&2, &2, Error, Bool>:
640 bits : Word64 <- to_uint64(v)
641 return Bool.not(Word64.is_zero(bits))
642
643
644def float_of_bits(v: U32) -> F32:
645 U32{bits} = v
646 F32{bits}
647
648def from_float(v: F32) -> Value:
649 from_fixed32(F32.bits(v))
650
651def to_float(v: Value) -> Result<&2, &2, Error, F32>:
652 do Result<&2, &2, Error, F32>:
653 bits : U32 <- to_fixed32(v)
654 return float_of_bits(bits)
655
656def from_double(v: F.F64) -> Value:
657 F.F64{h, l} = v
658 Fixed64{Word64{h, l}}
659
660def double_of_bits(bits: Word64) -> F.F64:
661 Word64{h, l} = bits
662 F.F64{h, l}
663
664def to_double(v: Value) -> Result<&2, &2, Error, F.F64>:
665 do Result<&2, &2, Error, F.F64>:
666 bits : Word64 <- to_fixed64(v)
667 return double_of_bits(bits)
668
669def from_bytes(v: B.Bytes) -> Value:
670 Blob{v}
671
672def to_bytes(v: Value) -> Result<&2, &1, Error, B.Bytes>:
673 match v:
674 case Blob{b}:
675 Done{b}
676 case _:
677 Fail{Malformed{}}
678
679type Utf8 is Data:
680 Utf8{need: U32, lo: U32, hi: U32, cp: U32, out: String}
681
682def utf8.lead.multi(+b: U32, out: String) -> Utf8:
683 +need = Bool.pick(U32, U32.is_lt(b, 224), 1, Bool.pick(U32, U32.is_lt(b, 240), 2, 3))
684 lo = Bool.pick(U32, U32.is_eq(b, 224), 160, Bool.pick(U32, U32.is_eq(b, 240), 144, 128))
685 hi = Bool.pick(U32, U32.is_eq(b, 237), 159, Bool.pick(U32, U32.is_eq(b, 244), 143, 191))
686 Utf8{need, lo, hi, (b .&. (63 >> U32.to_nat(need)) : U32), out}
687
688def utf8.lead.high(ok: Bool, b: U32, out: String) -> Result<&2, &2, Error, Utf8>:
689 match ok:
690 case False{}:
691 Fail{InvalidUtf8{}}
692 case True{}:
693 Done{utf8.lead.multi(b, out)}
694
695def utf8.lead(ascii: Bool, +b: U32, out: String) -> Result<&2, &2, Error, Utf8>:
696 match ascii:
697 case True{}:
698 Done{Utf8{0, 128, 191, 0, SCon{Chr{b}, out}}}
699 case False{}:
700 utf8.lead.high(U32.is_ge(b, 194) && U32.is_le(b, 244), b, out)
701
702def utf8.more(done: Bool, need: U32, cp: U32, out: String) -> Utf8:
703 match done:
704 case True{}:
705 Utf8{0, 128, 191, 0, SCon{Chr{cp}, out}}
706 case False{}:
707 Utf8{need, 128, 191, cp, out}
708
709def utf8.cont(ok: Bool, +need: U32, cp: U32, b: U32, out: String) -> Result<&2, &2, Error, Utf8>:
710 match ok:
711 case False{}:
712 Fail{InvalidUtf8{}}
713 case True{}:
714 Done{utf8.more(U32.is_eq(need, 1), (need - 1 : U32), ((cp << 6n) .|. (b .&. 63) : U32), out)}
715
716def utf8.step.idle(idle: Bool, +need: U32, lo: U32, hi: U32, cp: U32, +b: U32, out: String) -> Result<&2, &2, Error, Utf8>:
717 match idle:
718 case True{}:
719 utf8.lead(U32.is_lt(b, 128), b, out)
720 case False{}:
721 utf8.cont(U32.is_le(lo, b) && U32.is_le(b, hi), need, cp, b, out)
722
723def utf8.step(st: Utf8, b: U32) -> Result<&2, &2, Error, Utf8>:
724 Utf8{+need, lo, hi, cp, out} = st
725 utf8.step.idle(U32.is_zero(need), need, lo, hi, cp, b, out)
726
727def utf8.finish(ok: Bool, out: String) -> Result<&2, &2, Error, String>:
728 match ok:
729 case False{}:
730 Fail{InvalidUtf8{}}
731 case True{}:
732 Done{String.reverse(out)}
733
734def utf8.decode.go(n: Nat, r: B.Cursor & Maybe<&2, U32>, st: Utf8) -> Result<&2, &2, Error, String>:
735 match n:
736 case 0n:
737 Utf8{need, lo, hi, cp, out} = st
738 utf8.finish(U32.is_zero(need), out)
739 case 1n+p:
740 (next, v) = r
741 match v:
742 case None{}:
743 Fail{InvalidUtf8{}}
744 case Some{b}:
745 do Result<&2, &2, Error, String>:
746 state : Utf8 <- utf8.step(st, b)
747 utf8.decode.go(p, B.Cursor.u8(next), state)
748
749def utf8.decode(b: B.Bytes) -> Result<&2, &2, Error, String>:
750 B.Bytes{+n, buf} = b
751 utf8.decode.go(U32.to_nat(n), B.Cursor.u8(B.Cursor.new(B.Bytes{n, buf})), Utf8{0, 128, 191, 0, SNil{}})
752
753def utf8.width(+c: U32) -> U32:
754 Bool.pick(U32, U32.is_lt(c, 128), 1, Bool.pick(U32, U32.is_lt(c, 2048), 2, Bool.pick(U32, U32.is_lt(c, 65536), 3, 4)))
755
756def utf8.scalar(+c: U32) -> Bool:
757 U32.is_le(c, 1114111) && Bool.not(U32.is_ge(c, 55296) && U32.is_le(c, 57343))
758
759def require(ok: Bool, e: Error) -> Result<&2, &1, Error, Unit>:
760 match ok:
761 case False{}:
762 Fail{e}
763 case True{}:
764 Done{Unit{}}
765
766def utf8.cont_byte(c: U32, shift: Nat) -> U32:
767 (128 .|. ((c >> shift) .&. 63) : U32)
768
769def utf8.push(width: U32, +c: U32, out: B.Bytes) -> Result<&2, &1, Error, B.Bytes>:
770 match width:
771 case 1:
772 byte(out, c, 2147483647)
773 case 2:
774 do Result<&2, &1, Error, B.Bytes>:
775 a : B.Bytes <- byte(out, (192 .|. (c >> 6n) : U32), 2147483647)
776 byte(a, utf8.cont_byte(c, 0n), 2147483647)
777 case 3:
778 do Result<&2, &1, Error, B.Bytes>:
779 a : B.Bytes <- byte(out, (224 .|. (c >> 12n) : U32), 2147483647)
780 b : B.Bytes <- byte(a, utf8.cont_byte(c, 6n), 2147483647)
781 byte(b, utf8.cont_byte(c, 0n), 2147483647)
782 case _:
783 do Result<&2, &1, Error, B.Bytes>:
784 a : B.Bytes <- byte(out, (240 .|. (c >> 18n) : U32), 2147483647)
785 b : B.Bytes <- byte(a, utf8.cont_byte(c, 12n), 2147483647)
786 d : B.Bytes <- byte(b, utf8.cont_byte(c, 6n), 2147483647)
787 byte(d, utf8.cont_byte(c, 0n), 2147483647)
788
789def utf8.encode.go(s: String, out: B.Bytes) -> Result<&2, &1, Error, B.Bytes>:
790 match s:
791 case SNil{}:
792 Done{out}
793 case SCon{Chr{+c}, tail}:
794 do Result<&2, &1, Error, B.Bytes>:
795 ok : Unit <- require(utf8.scalar(c), InvalidUtf8{})
796 next : B.Bytes <- utf8.push(utf8.width(c), c, out)
797 utf8.encode.go(tail, next)
798
799def utf8.encode(s: String) -> Result<&2, &1, Error, B.Bytes>:
800 utf8.encode.go(s, B.new(0))
801
802def from_string(s: String) -> Result<&2, &1, Error, Value>:
803 do Result<&2, &1, Error, Value>:
804 bytes : B.Bytes <- utf8.encode(s)
805 return Blob{bytes}
806
807def to_string(v: Value) -> Result<&2, &2, Error, String>:
808 match v:
809 case Blob{bytes}:
810 utf8.decode(bytes)
811 case _:
812 Fail{Malformed{}}