src/pb.bend

bendonnect-rpc@0.1.0.0 · 806 lines · 184 definitions

1# Protobuf binary runtime for generated code (alias Pbr). Pure. Reference: docs/runtime.md.
2#
3# Built on bend-kit-protobuf (Pb): Word64, Value, Field, decode/encode, packed_decode/encode.
4# Readers answer Result<&2, &1, String, T> (wrong wire type or malformed input -> Fail).
5# Writers answer List<&1, Pb.Field> so a message is encoded by concatenating per-field lists.
6import Base
7import bend-kit-bytes@0.3.2.0/bytes.bend as Bytes
8import bend-kit-encoding@0.4.0.0/encoding.bend as Enc
9import bend-kit-protobuf@0.1.0.0/protobuf.bend as Pb
10
11# ------------------------------------------------------------------ limits
12
13def max_size() -> U32:
14  2147483647
15
16def max_depth() -> Nat:
17  100n
18
19# ------------------------------------------------------------------ small list helpers
20
21def rev(-A: Data, xs: List<&2, A>) -> List<&2, A>:
22  List.reverse(&2, A, xs)
23
24def cat(xs: List<&1, Pb.Field>, ys: List<&1, Pb.Field>) -> List<&1, Pb.Field>:
25  match xs:
26    case Nil{}:
27      ys
28    case Con{h, t}:
29      h <> cat(t, ys)
30
31def cat.all(parts: List<&1, List<&1, Pb.Field>>) -> List<&1, Pb.Field>:
32  match parts:
33    case Nil{}:
34      Nil{}
35    case Con{h, t}:
36      cat(h, cat.all(t))
37
38def pick.then(z: Bool, acc: String, next: Unit -> String) -> String:
39  match z:
40    case True{}:
41      acc
42    case False{}:
43      next(Unit{})
44
45# ------------------------------------------------------------------ Word64
46
47def word64.of_u32(+x: U32) -> Pb.Word64:
48  Pb.Word64{0, x}
49
50# Sign-extends a 32-bit two's complement value.
51def word64.of_i32(+x: U32) -> Pb.Word64:
52  Pb.Word64{(0 - (x >> 31n) : U32), x}
53
54def word64.hi(w: Pb.Word64) -> U32:
55  Pb.Word64{h, l} = w
56  h
57
58def word64.lo(w: Pb.Word64) -> U32:
59  Pb.Word64{h, l} = w
60  l
61
62def word64.is_zero(w: Pb.Word64) -> Bool:
63  Pb.Word64.is_zero(w)
64
65def word64.eq(a: Pb.Word64, b: Pb.Word64) -> Bool:
66  Pb.Word64{ah, al} = a
67  Pb.Word64{bh, bl} = b
68  U32.is_eq(ah, bh) && U32.is_eq(al, bl)
69
70# True when the sign bit (bit 63) is set.
71def word64.is_neg(w: Pb.Word64) -> Bool:
72  Pb.Word64{h, l} = w
73  U32.is_ne((h >> 31n : U32), 0)
74
75# Two's complement negation.
76def word64.neg(w: Pb.Word64) -> Pb.Word64:
77  Pb.Word64{+h, +l} = w
78  Pb.Word64{(0 - h - Bool.to_u32(Bool.not(U32.is_zero(l))) : U32), (0 - l : U32)}
79
80# Logical shifts, n in 0..63.
81def word64.shl(w: Pb.Word64, +n: U32) -> Pb.Word64:
82  Pb.Word64{+h, +l} = w
83  +a = (n .&. 31 : U32)
84  +big = U32.is_ge(n, 32)
85  Pb.Word64{
86    Bool.pick(U32, big, (l << U32.to_nat(a) : U32), ((h << U32.to_nat(a)) .|. (l >> U32.to_nat((32 - a : U32))) : U32)),
87    Bool.pick(U32, big, 0, (l << U32.to_nat(a) : U32))}
88
89def word64.shr(w: Pb.Word64, +n: U32) -> Pb.Word64:
90  Pb.Word64{+h, +l} = w
91  +a = (n .&. 31 : U32)
92  +big = U32.is_ge(n, 32)
93  Pb.Word64{
94    Bool.pick(U32, big, 0, (h >> U32.to_nat(a) : U32)),
95    Bool.pick(U32, big, (h >> U32.to_nat(a) : U32), ((l >> U32.to_nat(a)) .|. (h << U32.to_nat((32 - a : U32))) : U32))}
96
97# Decimal conversion works on 16-bit limbs so every intermediate fits in U32.
98type Dm is Data:
99  Dm{q: Pb.Word64, r: U32}
100
101type Qr is Data:
102  Qr{q: U32, r: U32}
103
104def dm.step(+rem: U32, +chunk: U32) -> Qr:
105  +cur = (rem * 65536 + chunk : U32)
106  Qr{(cur / 10 : U32), (cur % 10 : U32)}
107
108def dm.d(+q3: U32, +q2: U32, +q1: U32, s: Qr) -> Dm:
109  Qr{q0, r0} = s
110  Dm{Pb.Word64{((q3 << 16n) .|. q2 : U32), ((q1 << 16n) .|. q0 : U32)}, r0}
111
112def dm.c(+ll: U32, +q3: U32, +q2: U32, s: Qr) -> Dm:
113  Qr{q1, r1} = s
114  dm.d(q3, q2, q1, dm.step(r1, ll))
115
116def dm.b(+l: U32, +q3: U32, s: Qr) -> Dm:
117  Qr{q2, r2} = s
118  dm.c((l .&. 65535 : U32), q3, q2, dm.step(r2, (l >> 16n : U32)))
119
120def dm.a(+hl: U32, +l: U32, s: Qr) -> Dm:
121  Qr{q3, r3} = s
122  dm.b(l, q3, dm.step(r3, hl))
123
124def dm.q(d: Dm) -> Pb.Word64:
125  Dm{q, r} = d
126  q
127
128def dm.r(d: Dm) -> U32:
129  Dm{q, r} = d
130  r
131
132def word64.divmod10(w: Pb.Word64) -> Dm:
133  Pb.Word64{+h, +l} = w
134  dm.a((h .&. 65535 : U32), l, dm.step(0, (h >> 16n : U32)))
135
136def show_u.go(fuel: Nat, +w: Pb.Word64, +acc: String) -> String:
137  match fuel:
138    case 0n:
139      acc
140    case 1n+p:
141      +d = word64.divmod10(w)
142      pick.then(Pb.Word64.is_zero(w), acc, u => show_u.go(p, dm.q(d), SCon{Chr{(48 + dm.r(d) : U32)}, acc}))
143
144# Unsigned decimal text.
145def word64.show_u(+w: Pb.Word64) -> String:
146  Bool.pick(String, Pb.Word64.is_zero(w), "0", show_u.go(20n, w, ""))
147
148def show_s.go(neg: Bool, +w: Pb.Word64) -> String:
149  match neg:
150    case True{}:
151      String.append("-", word64.show_u(word64.neg(w)))
152    case False{}:
153      word64.show_u(w)
154
155# Signed (two's complement) decimal text.
156def word64.show_s(+w: Pb.Word64) -> String:
157  show_s.go(word64.is_neg(w), w)
158
159type Acc is Data:
160  Acc{w: Pb.Word64, ovf: Bool}
161
162type Kc is Data:
163  Kc{c: U32, k: U32}
164
165def ma.step(+chunk: U32, +carry: U32) -> Kc:
166  +x = (chunk * 10 + carry : U32)
167  Kc{(x .&. 65535 : U32), (x >> 16n : U32)}
168
169def ma.d(+c0: U32, +c1: U32, +c2: U32, s: Kc) -> Acc:
170  Kc{c3, k3} = s
171  Acc{Pb.Word64{((c3 << 16n) .|. c2 : U32), ((c1 << 16n) .|. c0 : U32)}, U32.is_ne(k3, 0)}
172
173def ma.c(+h: U32, +c0: U32, +c1: U32, s: Kc) -> Acc:
174  Kc{c2, k2} = s
175  ma.d(c0, c1, c2, ma.step((h >> 16n : U32), k2))
176
177def ma.b(+h: U32, +l: U32, +c0: U32, s: Kc) -> Acc:
178  Kc{c1, k1} = s
179  ma.c(h, c0, c1, ma.step((h .&. 65535 : U32), k1))
180
181def ma.a(+h: U32, +l: U32, s: Kc) -> Acc:
182  Kc{c0, k0} = s
183  ma.b(h, l, c0, ma.step((l >> 16n : U32), k0))
184
185# w * 10 + d (d < 10), with an overflow flag.
186def word64.muladd10(w: Pb.Word64, d: U32) -> Acc:
187  Pb.Word64{+h, +l} = w
188  ma.a(h, l, ma.step((l .&. 65535 : U32), d))
189
190def acc.w(a: Acc) -> Pb.Word64:
191  Acc{w, o} = a
192  w
193
194def acc.o(a: Acc) -> Bool:
195  Acc{w, o} = a
196  o
197
198def read_u.go(s: String, w: Pb.Word64, bad: Bool) -> Maybe<&2, Pb.Word64>:
199  match s:
200    case SNil{}:
201      Bool.pick(Maybe<&2, Pb.Word64>, bad, None{}, Some{w})
202    case SCon{Chr{+c}, t}:
203      +digit = U32.is_ge(c, 48) && U32.is_le(c, 57)
204      +a = word64.muladd10(w, Bool.pick(U32, digit, (c - 48 : U32), 0))
205      read_u.go(t, acc.w(a), bad || acc.o(a) || Bool.not(digit))
206
207# Decimal digits -> Word64; None on empty input, a non-digit, or overflow past 2^64-1.
208def word64.read_u(+s: String) -> Maybe<&2, Pb.Word64>:
209  Bool.pick(Maybe<&2, Pb.Word64>, String.is_empty(s), None{}, read_u.go(s, Pb.Word64{0, 0}, False{}))
210
211def read_s.neg(m: Maybe<&2, Pb.Word64>) -> Maybe<&2, Pb.Word64>:
212  match m:
213    case None{}:
214      None{}
215    case Some{w}:
216      Pb.Word64{+h, +l} = w
217      Bool.pick(Maybe<&2, Pb.Word64>,
218        U32.is_lt(h, 2147483648) || (U32.is_eq(h, 2147483648) && U32.is_zero(l)),
219        Some{word64.neg(Pb.Word64{h, l})}, None{})
220
221def read_s.pos(m: Maybe<&2, Pb.Word64>) -> Maybe<&2, Pb.Word64>:
222  match m:
223    case None{}:
224      None{}
225    case Some{w}:
226      Pb.Word64{+h, +l} = w
227      Bool.pick(Maybe<&2, Pb.Word64>, U32.is_lt(h, 2147483648), Some{Pb.Word64{h, l}}, None{})
228
229def read_s.go(neg: Bool, +c: U32, +t: String) -> Maybe<&2, Pb.Word64>:
230  match neg:
231    case True{}:
232      read_s.neg(word64.read_u(t))
233    case False{}:
234      read_s.pos(word64.read_u(SCon{Chr{c}, t}))
235
236# Optional '-' then decimal digits -> two's complement Word64; None when it does not fit in int64.
237def word64.read_s(+s: String) -> Maybe<&2, Pb.Word64>:
238  match s:
239    case SNil{}:
240      None{}
241    case SCon{Chr{+c}, +t}:
242      read_s.go(U32.is_eq(c, 45), c, t)
243
244# ------------------------------------------------------------------ bytes, strings, zigzag
245
246def codes.to_chars(xs: List<&2, U32>) -> String:
247  match xs:
248    case Nil{}:
249      SNil{}
250    case Con{h, t}:
251      SCon{Chr{h}, codes.to_chars(t)}
252
253def chars.to_codes(s: String) -> List<&2, U32>:
254  match s:
255    case SNil{}:
256      Nil{}
257    case SCon{Chr{c}, t}:
258      c <> chars.to_codes(t)
259
260# One byte per cell (only the low 8 bits of each cell are kept).
261def bytes.of_list(xs: List<&2, U32>) -> Bytes.Bytes:
262  Bytes.from_string(codes.to_chars(xs))
263
264def bytes.to_list(b: Bytes.Bytes) -> List<&2, U32>:
265  chars.to_codes(Bytes.to_string(b))
266
267# UTF-8 (lone surrogates and out-of-range code points are replaced by U+FFFD).
268def string.encode(+s: String) -> Bytes.Bytes:
269  Enc.utf8.encode(s)
270
271def lift2(-T: Data, what: String, r: Result<&2, &2, Pb.Error, T>) -> Result<&2, &1, String, T>:
272  match r:
273    case Fail{e}:
274      Fail{what}
275    case Done{x}:
276      Done{x}
277
278def lift1(-T: Type, what: String, r: Result<&2, &1, Pb.Error, T>) -> Result<&2, &1, String, T>:
279  match r:
280    case Fail{e}:
281      Fail{what}
282    case Done{x}:
283      Done{x}
284
285# Strict UTF-8 decoding.
286def string.decode(b: Bytes.Bytes) -> Result<&2, &1, String, String>:
287  lift2(String, "protobuf: invalid UTF-8 in string field", Pb.utf8.decode(b))
288
289def zigzag32(+v: U32) -> U32:
290  ((v << 1n) .^. (0 - (v >> 31n)) : U32)
291
292def unzigzag32(+bits: U32) -> U32:
293  Pb.unzigzag32(bits)
294
295def zigzag64(w: Pb.Word64) -> Pb.Word64:
296  Pb.Word64.zigzag(w)
297
298def unzigzag64(w: Pb.Word64) -> Pb.Word64:
299  Pb.Word64.unzigzag(w)
300
301# ------------------------------------------------------------------ float / double
302
303def f32.bits(+f: F32) -> U32:
304  F32.bits(f)
305
306def f32.of_bits(+u: U32) -> F32:
307  Pb.float_of_bits(u)
308
309# floor(log2 m) for m >= 1 (0 for m = 0).
310def msb.go(fuel: Nat, +m: U32, +acc: U32) -> U32:
311  match fuel:
312    case 0n:
313      acc
314    case 1n+p:
315      msb.go(p, (m >> 1n : U32), (acc + Bool.to_u32(U32.is_gt(m, 1)) : U32))
316
317def msb(+m: U32) -> U32:
318  msb.go(24n, m, 0)
319
320# IEEE binary32 bits -> binary64 bits (exact).
321def double.of_f32bits(+b: U32) -> Pb.Word64:
322  +s = ((b >> 31n) << 31n : U32)
323  +e = ((b >> 23n) .&. 255 : U32)
324  +m = (b .&. 8388607 : U32)
325  +p = msb(m)
326  +sub = word64.shl(Pb.Word64{0, (m - (1 << U32.to_nat(p)) : U32)}, (52 - p : U32))
327  +mh = (m >> 3n : U32)
328  +ml = ((m .&. 7) << 29n : U32)
329  +nh = (s .|. ((e + 896) << 20n) .|. mh : U32)
330  +sh = (s .|. 2146435072 .|. mh : U32)
331  +uh = (s .|. ((p + 874) << 20n) .|. word64.hi(sub) : U32)
332  Pb.Word64{
333    Bool.pick(U32, U32.is_eq(e, 255), sh, Bool.pick(U32, U32.is_zero(e), Bool.pick(U32, U32.is_zero(m), s, uh), nh)),
334    Bool.pick(U32, U32.is_zero(e), Bool.pick(U32, U32.is_zero(m), 0, word64.lo(sub)), ml)}
335
336# IEEE binary64 bits -> binary32 bits, round to nearest even (overflow -> infinity, tiny -> zero).
337def double.f32bits(w: Pb.Word64) -> U32:
338  Pb.Word64{+h, +l} = w
339  +s = ((h >> 31n) << 31n : U32)
340  +e = ((h >> 20n) .&. 2047 : U32)
341  +fh = (h .&. 1048575 : U32)
342  +m23 = ((fh << 3n) .|. (l >> 29n) : U32)
343  +rem = (l .&. 536870911 : U32)
344  +up = U32.is_gt(rem, 268435456) || (U32.is_eq(rem, 268435456) && U32.is_eq((m23 .&. 1 : U32), 1))
345  +normal = (((e - 896) << 23n) + m23 + Bool.to_u32(up) : U32)
346  +special = Bool.pick(U32, U32.is_zero(fh) && U32.is_zero(l), 2139095040, (2143289344 .|. m23 : U32))
347  +k = (926 - e : U32)
348  +sig = {Pb.Word64{(fh .|. 1048576 : U32), l} : Pb.Word64}
349  +mm = word64.lo(word64.shr(sig, k))
350  +t = word64.shl(sig, (64 - k : U32))
351  +th = word64.hi(t)
352  +tl = word64.lo(t)
353  +gt = U32.is_gt(th, 2147483648) || (U32.is_eq(th, 2147483648) && U32.is_ne(tl, 0))
354  +eq = U32.is_eq(th, 2147483648) && U32.is_zero(tl)
355  +up2 = gt || (eq && U32.is_eq((mm .&. 1 : U32), 1))
356  +subn = (mm + Bool.to_u32(up2) : U32)
357  (s .|. Bool.pick(U32, U32.is_eq(e, 2047), special,
358        Bool.pick(U32, U32.is_ge(e, 1151), 2139095040,
359        Bool.pick(U32, U32.is_ge(e, 897), normal,
360        Bool.pick(U32, U32.is_ge(e, 873), subn, 0))))
361    : U32)
362
363# F32 <-> 64-bit wire bits. Doubles are LOSSY in this library: they are held in F32.
364def double.bits(+f: F32) -> Pb.Word64:
365  double.of_f32bits(F32.bits(f))
366
367def double.of_bits(w: Pb.Word64) -> F32:
368  Pb.float_of_bits(double.f32bits(w))
369
370# ------------------------------------------------------------------ decode / encode
371
372def decode(b: Bytes.Bytes) -> Result<&2, &1, String, List<&1, Pb.Field>>:
373  lift1(List<&1, Pb.Field>, "protobuf: malformed message", Pb.decode(b, max_size(), max_depth()))
374
375def encode.fin(r: Result<&2, &1, Pb.Error, Bytes.Bytes>) -> Bytes.Bytes:
376  match r:
377    case Fail{e}:
378      Bytes.new(0)
379    case Done{b}:
380      b
381
382# Never fails for well-formed field numbers (1..536870911); a bad field number yields empty bytes.
383def encode(fs: List<&1, Pb.Field>) -> Bytes.Bytes:
384  encode.fin(Pb.encode(fs, max_size(), max_depth()))
385
386# ------------------------------------------------------------------ Value constructors
387
388def value.double(+f: F32) -> Pb.Value:
389  Pb.Fixed64{double.bits(f)}
390
391def value.float(+f: F32) -> Pb.Value:
392  Pb.from_float(f)
393
394def value.int32(+x: U32) -> Pb.Value:
395  Pb.from_int32(x)
396
397def value.int64(+w: Pb.Word64) -> Pb.Value:
398  Pb.from_int64(w)
399
400def value.uint32(+x: U32) -> Pb.Value:
401  Pb.from_uint32(x)
402
403def value.uint64(+w: Pb.Word64) -> Pb.Value:
404  Pb.from_uint64(w)
405
406def value.sint32(+x: U32) -> Pb.Value:
407  Pb.from_sint32(x)
408
409def value.sint64(+w: Pb.Word64) -> Pb.Value:
410  Pb.from_sint64(w)
411
412def value.fixed32(+x: U32) -> Pb.Value:
413  Pb.from_fixed32(x)
414
415def value.fixed64(+w: Pb.Word64) -> Pb.Value:
416  Pb.from_fixed64(w)
417
418def value.sfixed32(+x: U32) -> Pb.Value:
419  Pb.from_sfixed32(x)
420
421def value.sfixed64(+w: Pb.Word64) -> Pb.Value:
422  Pb.from_sfixed64(w)
423
424def value.bool(+b: Bool) -> Pb.Value:
425  Pb.from_bool(b)
426
427def value.string(+s: String) -> Pb.Value:
428  Pb.Blob{string.encode(s)}
429
430def value.bytes(+xs: List<&2, U32>) -> Pb.Value:
431  Pb.Blob{bytes.of_list(xs)}
432
433def value.enum(+x: U32) -> Pb.Value:
434  Pb.from_int32(x)
435
436# A nested message: its fields, encoded.
437def value.message(fs: List<&1, Pb.Field>) -> Pb.Value:
438  Pb.Blob{encode(fs)}
439
440# ------------------------------------------------------------------ readers
441
442def read.double.fin(r: Result<&2, &1, String, Pb.Word64>) -> Result<&2, &1, String, F32>:
443  match r:
444    case Fail{e}:
445      Fail{e}
446    case Done{w}:
447      Done{double.of_bits(w)}
448
449def read.fixed64(v: Pb.Value) -> Result<&2, &1, String, Pb.Word64>:
450  lift2(Pb.Word64, "protobuf: wire type mismatch for fixed64", Pb.to_fixed64(v))
451
452def read.double(v: Pb.Value) -> Result<&2, &1, String, F32>:
453  read.double.fin(read.fixed64(v))
454
455def read.float(v: Pb.Value) -> Result<&2, &1, String, F32>:
456  lift2(F32, "protobuf: wire type mismatch for float", Pb.to_float(v))
457
458def read.int32(v: Pb.Value) -> Result<&2, &1, String, U32>:
459  lift2(U32, "protobuf: wire type mismatch for int32", Pb.to_int32(v))
460
461def read.int64(v: Pb.Value) -> Result<&2, &1, String, Pb.Word64>:
462  lift2(Pb.Word64, "protobuf: wire type mismatch for int64", Pb.to_int64(v))
463
464def read.uint32(v: Pb.Value) -> Result<&2, &1, String, U32>:
465  lift2(U32, "protobuf: wire type mismatch for uint32", Pb.to_uint32(v))
466
467def read.uint64(v: Pb.Value) -> Result<&2, &1, String, Pb.Word64>:
468  lift2(Pb.Word64, "protobuf: wire type mismatch for uint64", Pb.to_uint64(v))
469
470def read.sint32(v: Pb.Value) -> Result<&2, &1, String, U32>:
471  lift2(U32, "protobuf: wire type mismatch for sint32", Pb.to_sint32(v))
472
473def read.sint64(v: Pb.Value) -> Result<&2, &1, String, Pb.Word64>:
474  lift2(Pb.Word64, "protobuf: wire type mismatch for sint64", Pb.to_sint64(v))
475
476def read.fixed32(v: Pb.Value) -> Result<&2, &1, String, U32>:
477  lift2(U32, "protobuf: wire type mismatch for fixed32", Pb.to_fixed32(v))
478
479def read.sfixed32(v: Pb.Value) -> Result<&2, &1, String, U32>:
480  lift2(U32, "protobuf: wire type mismatch for sfixed32", Pb.to_sfixed32(v))
481
482def read.sfixed64(v: Pb.Value) -> Result<&2, &1, String, Pb.Word64>:
483  lift2(Pb.Word64, "protobuf: wire type mismatch for sfixed64", Pb.to_sfixed64(v))
484
485def read.bool(v: Pb.Value) -> Result<&2, &1, String, Bool>:
486  lift2(Bool, "protobuf: wire type mismatch for bool", Pb.to_bool(v))
487
488def read.enum(v: Pb.Value) -> Result<&2, &1, String, U32>:
489  lift2(U32, "protobuf: wire type mismatch for enum", Pb.to_int32(v))
490
491def read.string(v: Pb.Value) -> Result<&2, &1, String, String>:
492  lift2(String, "protobuf: invalid string field (wire type or UTF-8)", Pb.to_string(v))
493
494# The raw payload of a length-delimited field.
495def read.blob(v: Pb.Value) -> Result<&2, &1, String, Bytes.Bytes>:
496  lift1(Bytes.Bytes, "protobuf: wire type mismatch for length-delimited field", Pb.to_bytes(v))
497
498def read.bytes.fin(r: Result<&2, &1, String, Bytes.Bytes>) -> Result<&2, &1, String, List<&2, U32>>:
499  match r:
500    case Fail{e}:
501      Fail{e}
502    case Done{b}:
503      Done{bytes.to_list(b)}
504
505def read.bytes(v: Pb.Value) -> Result<&2, &1, String, List<&2, U32>>:
506  read.bytes.fin(read.blob(v))
507
508# A nested message's fields; decode them with the generated per-field fold.
509def read.message(v: Pb.Value) -> Result<&2, &1, String, List<&1, Pb.Field>>:
510  do Result<&2, &1, String, List<&1, Pb.Field>>:
511    b : Bytes.Bytes <- read.blob(v)
512    decode(b)
513
514# --- repeated: conses onto acc (so acc is in REVERSE order; finish with Pbr.rev)
515
516def rep.single(~T: Data, ~read: Pb.Value -> Result<&2, &1, String, T>, v: Pb.Value, acc: List<&2, T>) -> Result<&2, &1, String, List<&2, T>>:
517  do Result<&2, &1, String, List<&2, T>>:
518    x : T <- read(v)
519    return x <> acc
520
521def rep.vals(~T: Data, ~read: Pb.Value -> Result<&2, &1, String, T>, vs: List<&1, Pb.Value>, acc: List<&2, T>) -> Result<&2, &1, String, List<&2, T>>:
522  match vs:
523    case Nil{}:
524      Done{acc}
525    case Con{v, rest}:
526      do Result<&2, &1, String, List<&2, T>>:
527        x : T <- read(v)
528        rep.vals(~T, ~read, rest, x <> acc)
529
530def rep.packed(~T: Data, ~read: Pb.Value -> Result<&2, &1, String, T>, r: Result<&2, &1, Pb.Error, List<&1, Pb.Value>>, acc: List<&2, T>) -> Result<&2, &1, String, List<&2, T>>:
531  match r:
532    case Fail{e}:
533      Fail{"protobuf: malformed packed field"}
534    case Done{vs}:
535      rep.vals(~T, ~read, vs, acc)
536
537# wire: 0 varint, 1 fixed64, 5 fixed32 (the element encoding inside a packed blob).
538def rep.read(~T: Data, ~read: Pb.Value -> Result<&2, &1, String, T>, +wire: U32, v: Pb.Value, acc: List<&2, T>) -> Result<&2, &1, String, List<&2, T>>:
539  match v:
540    case Pb.Blob{b}:
541      rep.packed(~T, ~read, Pb.packed_decode(wire, b, max_size()), acc)
542    case Pb.Varint{w}:
543      rep.single(~T, ~read, Pb.Varint{w}, acc)
544    case Pb.Fixed32{x}:
545      rep.single(~T, ~read, Pb.Fixed32{x}, acc)
546    case Pb.Fixed64{w}:
547      rep.single(~T, ~read, Pb.Fixed64{w}, acc)
548    case Pb.Group{fs}:
549      Fail{"protobuf: unexpected group in repeated field"}
550
551def read.repeated.double(v: Pb.Value, acc: List<&2, F32>) -> Result<&2, &1, String, List<&2, F32>>:
552  rep.read(~F32, ~read.double, 1, v, acc)
553
554def read.repeated.float(v: Pb.Value, acc: List<&2, F32>) -> Result<&2, &1, String, List<&2, F32>>:
555  rep.read(~F32, ~read.float, 5, v, acc)
556
557def read.repeated.int32(v: Pb.Value, acc: List<&2, U32>) -> Result<&2, &1, String, List<&2, U32>>:
558  rep.read(~U32, ~read.int32, 0, v, acc)
559
560def read.repeated.int64(v: Pb.Value, acc: List<&2, Pb.Word64>) -> Result<&2, &1, String, List<&2, Pb.Word64>>:
561  rep.read(~Pb.Word64, ~read.int64, 0, v, acc)
562
563def read.repeated.uint32(v: Pb.Value, acc: List<&2, U32>) -> Result<&2, &1, String, List<&2, U32>>:
564  rep.read(~U32, ~read.uint32, 0, v, acc)
565
566def read.repeated.uint64(v: Pb.Value, acc: List<&2, Pb.Word64>) -> Result<&2, &1, String, List<&2, Pb.Word64>>:
567  rep.read(~Pb.Word64, ~read.uint64, 0, v, acc)
568
569def read.repeated.sint32(v: Pb.Value, acc: List<&2, U32>) -> Result<&2, &1, String, List<&2, U32>>:
570  rep.read(~U32, ~read.sint32, 0, v, acc)
571
572def read.repeated.sint64(v: Pb.Value, acc: List<&2, Pb.Word64>) -> Result<&2, &1, String, List<&2, Pb.Word64>>:
573  rep.read(~Pb.Word64, ~read.sint64, 0, v, acc)
574
575def read.repeated.fixed32(v: Pb.Value, acc: List<&2, U32>) -> Result<&2, &1, String, List<&2, U32>>:
576  rep.read(~U32, ~read.fixed32, 5, v, acc)
577
578def read.repeated.fixed64(v: Pb.Value, acc: List<&2, Pb.Word64>) -> Result<&2, &1, String, List<&2, Pb.Word64>>:
579  rep.read(~Pb.Word64, ~read.fixed64, 1, v, acc)
580
581def read.repeated.sfixed32(v: Pb.Value, acc: List<&2, U32>) -> Result<&2, &1, String, List<&2, U32>>:
582  rep.read(~U32, ~read.sfixed32, 5, v, acc)
583
584def read.repeated.sfixed64(v: Pb.Value, acc: List<&2, Pb.Word64>) -> Result<&2, &1, String, List<&2, Pb.Word64>>:
585  rep.read(~Pb.Word64, ~read.sfixed64, 1, v, acc)
586
587def read.repeated.bool(v: Pb.Value, acc: List<&2, Bool>) -> Result<&2, &1, String, List<&2, Bool>>:
588  rep.read(~Bool, ~read.bool, 0, v, acc)
589
590def read.repeated.enum(v: Pb.Value, acc: List<&2, U32>) -> Result<&2, &1, String, List<&2, U32>>:
591  rep.read(~U32, ~read.enum, 0, v, acc)
592
593# strings and bytes are never packed: one element per field
594def read.repeated.string(v: Pb.Value, acc: List<&2, String>) -> Result<&2, &1, String, List<&2, String>>:
595  rep.single(~String, ~read.string, v, acc)
596
597def read.repeated.bytes(v: Pb.Value, acc: List<&2, List<&2, U32>>) -> Result<&2, &1, String, List<&2, List<&2, U32>>>:
598  rep.single(~List<&2, U32>, ~read.bytes, v, acc)
599
600# ------------------------------------------------------------------ writers
601
602def one(+n: U32, v: Pb.Value) -> List<&1, Pb.Field>:
603  Con{Pb.Field{n, v}, Nil{}}
604
605def skip.if(skip: Bool, +n: U32, v: Pb.Value) -> List<&1, Pb.Field>:
606  match skip:
607    case True{}:
608      Nil{}
609    case False{}:
610      one(n, v)
611
612# `field.K.always`: exactly one field (use for oneof members and proto3 `optional`).
613def field.double.always(+n: U32, +f: F32) -> List<&1, Pb.Field>:
614  one(n, value.double(f))
615
616def field.float.always(+n: U32, +f: F32) -> List<&1, Pb.Field>:
617  one(n, value.float(f))
618
619def field.int32.always(+n: U32, +x: U32) -> List<&1, Pb.Field>:
620  one(n, value.int32(x))
621
622def field.int64.always(+n: U32, w: Pb.Word64) -> List<&1, Pb.Field>:
623  one(n, value.int64(w))
624
625def field.uint32.always(+n: U32, +x: U32) -> List<&1, Pb.Field>:
626  one(n, value.uint32(x))
627
628def field.uint64.always(+n: U32, w: Pb.Word64) -> List<&1, Pb.Field>:
629  one(n, value.uint64(w))
630
631def field.sint32.always(+n: U32, +x: U32) -> List<&1, Pb.Field>:
632  one(n, value.sint32(x))
633
634def field.sint64.always(+n: U32, w: Pb.Word64) -> List<&1, Pb.Field>:
635  one(n, value.sint64(w))
636
637def field.fixed32.always(+n: U32, +x: U32) -> List<&1, Pb.Field>:
638  one(n, value.fixed32(x))
639
640def field.fixed64.always(+n: U32, w: Pb.Word64) -> List<&1, Pb.Field>:
641  one(n, value.fixed64(w))
642
643def field.sfixed32.always(+n: U32, +x: U32) -> List<&1, Pb.Field>:
644  one(n, value.sfixed32(x))
645
646def field.sfixed64.always(+n: U32, w: Pb.Word64) -> List<&1, Pb.Field>:
647  one(n, value.sfixed64(w))
648
649def field.bool.always(+n: U32, +b: Bool) -> List<&1, Pb.Field>:
650  one(n, value.bool(b))
651
652def field.string.always(+n: U32, +s: String) -> List<&1, Pb.Field>:
653  one(n, value.string(s))
654
655def field.bytes.always(+n: U32, xs: List<&2, U32>) -> List<&1, Pb.Field>:
656  one(n, value.bytes(xs))
657
658def field.enum.always(+n: U32, +x: U32) -> List<&1, Pb.Field>:
659  one(n, value.enum(x))
660
661def field.message.always(+n: U32, fs: List<&1, Pb.Field>) -> List<&1, Pb.Field>:
662  one(n, value.message(fs))
663
664# A present singular message (an empty message is still emitted).
665def field.message(+n: U32, fs: List<&1, Pb.Field>) -> List<&1, Pb.Field>:
666  field.message.always(n, fs)
667
668# `field.K`: omitted when x is the proto3 default (0, 0.0 with zero bits, false, "", empty bytes).
669def field.double(+n: U32, +f: F32) -> List<&1, Pb.Field>:
670  skip.if(U32.is_zero(F32.bits(f)), n, value.double(f))
671
672def field.float(+n: U32, +f: F32) -> List<&1, Pb.Field>:
673  skip.if(U32.is_zero(F32.bits(f)), n, value.float(f))
674
675def field.int32(+n: U32, +x: U32) -> List<&1, Pb.Field>:
676  skip.if(U32.is_zero(x), n, value.int32(x))
677
678def field.int64(+n: U32, +w: Pb.Word64) -> List<&1, Pb.Field>:
679  skip.if(Pb.Word64.is_zero(w), n, value.int64(w))
680
681def field.uint32(+n: U32, +x: U32) -> List<&1, Pb.Field>:
682  skip.if(U32.is_zero(x), n, value.uint32(x))
683
684def field.uint64(+n: U32, +w: Pb.Word64) -> List<&1, Pb.Field>:
685  skip.if(Pb.Word64.is_zero(w), n, value.uint64(w))
686
687def field.sint32(+n: U32, +x: U32) -> List<&1, Pb.Field>:
688  skip.if(U32.is_zero(x), n, value.sint32(x))
689
690def field.sint64(+n: U32, +w: Pb.Word64) -> List<&1, Pb.Field>:
691  skip.if(Pb.Word64.is_zero(w), n, value.sint64(w))
692
693def field.fixed32(+n: U32, +x: U32) -> List<&1, Pb.Field>:
694  skip.if(U32.is_zero(x), n, value.fixed32(x))
695
696def field.fixed64(+n: U32, +w: Pb.Word64) -> List<&1, Pb.Field>:
697  skip.if(Pb.Word64.is_zero(w), n, value.fixed64(w))
698
699def field.sfixed32(+n: U32, +x: U32) -> List<&1, Pb.Field>:
700  skip.if(U32.is_zero(x), n, value.sfixed32(x))
701
702def field.sfixed64(+n: U32, +w: Pb.Word64) -> List<&1, Pb.Field>:
703  skip.if(Pb.Word64.is_zero(w), n, value.sfixed64(w))
704
705def field.bool(+n: U32, +b: Bool) -> List<&1, Pb.Field>:
706  skip.if(Bool.not(b), n, value.bool(b))
707
708def field.string(+n: U32, +s: String) -> List<&1, Pb.Field>:
709  skip.if(String.is_empty(s), n, value.string(s))
710
711def field.bytes(+n: U32, +xs: List<&2, U32>) -> List<&1, Pb.Field>:
712  skip.if(List.is_empty(&2, U32, xs), n, value.bytes(xs))
713
714def field.enum(+n: U32, +x: U32) -> List<&1, Pb.Field>:
715  skip.if(U32.is_zero(x), n, value.enum(x))
716
717# --- repeated
718
719def rep.pack.fin(+n: U32, r: Result<&2, &1, Pb.Error, Bytes.Bytes>) -> List<&1, Pb.Field>:
720  match r:
721    case Fail{e}:
722      Nil{}
723    case Done{b}:
724      one(n, Pb.Blob{b})
725
726def rep.map(~T: Data, ~val: @+x: T -> Pb.Value, xs: List<&2, T>) -> List<&1, Pb.Value>:
727  match xs:
728    case Nil{}:
729      Nil{}
730    case Con{h, t}:
731      val(h) <> rep.map(~T, ~val, t)
732
733def rep.pack.go(~T: Data, ~val: @+x: T -> Pb.Value, +n: U32, xs: List<&2, T>) -> List<&1, Pb.Field>:
734  rep.pack.fin(n, Pb.packed_encode(rep.map(~T, ~val, xs), max_size()))
735
736def rep.pack(~T: Data, ~val: @+x: T -> Pb.Value, +n: U32, xs: List<&2, T>) -> List<&1, Pb.Field>:
737  match xs:
738    case Nil{}:
739      Nil{}
740    case Con{h, t}:
741      rep.pack.go(~T, ~val, n, Con{h, t})
742
743def rep.each(~T: Data, ~val: @+x: T -> Pb.Value, +n: U32, xs: List<&2, T>) -> List<&1, Pb.Field>:
744  match xs:
745    case Nil{}:
746      Nil{}
747    case Con{h, t}:
748      Pb.Field{n, val(h)} <> rep.each(~T, ~val, n, t)
749
750# Packed for numeric, bool and enum kinds; [] for an empty list.
751def field.repeated.double(+n: U32, xs: List<&2, F32>) -> List<&1, Pb.Field>:
752  rep.pack(~F32, ~value.double, n, xs)
753
754def field.repeated.float(+n: U32, xs: List<&2, F32>) -> List<&1, Pb.Field>:
755  rep.pack(~F32, ~value.float, n, xs)
756
757def field.repeated.int32(+n: U32, xs: List<&2, U32>) -> List<&1, Pb.Field>:
758  rep.pack(~U32, ~value.int32, n, xs)
759
760def field.repeated.int64(+n: U32, xs: List<&2, Pb.Word64>) -> List<&1, Pb.Field>:
761  rep.pack(~Pb.Word64, ~value.int64, n, xs)
762
763def field.repeated.uint32(+n: U32, xs: List<&2, U32>) -> List<&1, Pb.Field>:
764  rep.pack(~U32, ~value.uint32, n, xs)
765
766def field.repeated.uint64(+n: U32, xs: List<&2, Pb.Word64>) -> List<&1, Pb.Field>:
767  rep.pack(~Pb.Word64, ~value.uint64, n, xs)
768
769def field.repeated.sint32(+n: U32, xs: List<&2, U32>) -> List<&1, Pb.Field>:
770  rep.pack(~U32, ~value.sint32, n, xs)
771
772def field.repeated.sint64(+n: U32, xs: List<&2, Pb.Word64>) -> List<&1, Pb.Field>:
773  rep.pack(~Pb.Word64, ~value.sint64, n, xs)
774
775def field.repeated.fixed32(+n: U32, xs: List<&2, U32>) -> List<&1, Pb.Field>:
776  rep.pack(~U32, ~value.fixed32, n, xs)
777
778def field.repeated.fixed64(+n: U32, xs: List<&2, Pb.Word64>) -> List<&1, Pb.Field>:
779  rep.pack(~Pb.Word64, ~value.fixed64, n, xs)
780
781def field.repeated.sfixed32(+n: U32, xs: List<&2, U32>) -> List<&1, Pb.Field>:
782  rep.pack(~U32, ~value.sfixed32, n, xs)
783
784def field.repeated.sfixed64(+n: U32, xs: List<&2, Pb.Word64>) -> List<&1, Pb.Field>:
785  rep.pack(~Pb.Word64, ~value.sfixed64, n, xs)
786
787def field.repeated.bool(+n: U32, xs: List<&2, Bool>) -> List<&1, Pb.Field>:
788  rep.pack(~Bool, ~value.bool, n, xs)
789
790def field.repeated.enum(+n: U32, xs: List<&2, U32>) -> List<&1, Pb.Field>:
791  rep.pack(~U32, ~value.enum, n, xs)
792
793# One field per element.
794def field.repeated.string(+n: U32, xs: List<&2, String>) -> List<&1, Pb.Field>:
795  rep.each(~String, ~value.string, n, xs)
796
797def field.repeated.bytes(+n: U32, xs: List<&2, List<&2, U32>>) -> List<&1, Pb.Field>:
798  rep.each(~List<&2, U32>, ~value.bytes, n, xs)
799
800# items: each element's fields (e.g. from List.map over the generated to-fields function).
801def field.repeated.message(+n: U32, items: List<&1, List<&1, Pb.Field>>) -> List<&1, Pb.Field>:
802  match items:
803    case Nil{}:
804      Nil{}
805    case Con{h, t}:
806      cat(field.message(n, h), field.repeated.message(n, t))