bytes.bend

bend-kit-bytes@0.3.3.0 · 940 lines · 161 definitions

1# Byte buffers packed four bytes to a U32, with bounds-checked access. Source: https://github.com/paymog/bend-kit/tree/main/bytes
2import Base
3# bend-kit-int@0.2.0.0
4import bend-kit-int@0.2.0.0/int.bend as Int
5
6# Bytes{len, buf}: byte i is bits 8*(i%4) of buf[i/4]. buf has the fewest 2^d words
7# that hold len bytes. Every byte at or past len is 0, so equal buffers have equal words.
8# Out-of-range reads answer None and out-of-range writes do nothing; Array alone would wrap.
9#   import ./bytes/bytes.bend as Bytes
10
11type Bytes is Type:
12  Bytes{len: U32, buf: Array<U32>}
13
14def b8(+x: U32) -> U32:
15  (x .&. 255 : U32)
16
17def shift(+i: U32) -> Nat:
18  U32.to_nat(((i .&. 3 : U32) * 8 : U32))
19
20def words(+n: U32) -> U32:
21  ((n + 3 : U32) >> 2n : U32)
22
23# The fewest d with 2^d >= w.
24def depth.go(f: Nat, more: Bool, +w: U32, +d: Nat, +cap: U32) -> Nat:
25  match f:
26    case 0n:
27      d
28    case 1n+p:
29      match more:
30        case False{}:
31          d
32        case True{}:
33          depth.go(p, U32.is_lt((cap * 2 : U32), w), w, 1n+d, (cap * 2 : U32))
34
35def depth(+w: U32) -> Nat:
36  depth.go(32n, U32.is_lt(1, w), w, 0n, 1)
37
38def alloc(+n: U32) -> Array<U32>:
39  Array.new(U32, depth(words(n)), 0)
40
41# Unchecked byte read and write. Callers keep i below len.
42def peek.of(+sh: Nat, r: Array<U32> & U32) -> Array<U32> & U32:
43  (a, w) = r
44  (a, b8(U32.shrn(w, sh)))
45
46def peek(a: Array<U32>, +i: U32) -> Array<U32> & U32:
47  peek.of(shift(i), Array.get(U32, a, (i >> 2n : U32)))
48
49def poke.of(+i: U32, +v: U32, r: Array<U32> & U32) -> Array<U32>:
50  (a, w) = r
51  +sh = shift(i)
52  Array.set(U32, a, (i >> 2n : U32), ((w .&. ((255 << sh) .^. 4294967295)) .|. (b8(v) << sh) : U32))
53
54def poke(a: Array<U32>, +i: U32, +v: U32) -> Array<U32>:
55  poke.of(i, v, Array.get(U32, a, (i >> 2n : U32)))
56
57# n bytes from src[s..] to dst[d..], one byte at a time.
58def copy.go(n: Nat, r: Array<U32> & U32, dst: Array<U32>, +s: U32, +d: U32) -> Array<U32> & Array<U32>:
59  match n:
60    case 0n:
61      (a, v) = r
62      (a, dst)
63    case 1n+p:
64      (a, v) = r
65      copy.go(p, peek(a, (s + 1 : U32)), poke(dst, d, v), (s + 1 : U32), (d + 1 : U32))
66
67def copy.bytes(+m: U32, src: Array<U32>, dst: Array<U32>, +s: U32, +d: U32) -> Array<U32> & Array<U32>:
68  copy.go(U32.to_nat(m), peek(src, s), dst, s, d)
69
70# n words from src[s..] to dst[d..] (word indexes).
71def copy.words(n: Nat, r: Array<U32> & U32, dst: Array<U32>, +s: U32, +d: U32) -> Array<U32> & Array<U32>:
72  match n:
73    case 0n:
74      (a, w) = r
75      (a, dst)
76    case 1n+p:
77      (a, +w) = r
78      copy.words(p, Array.get(U32, a, (s + 1 : U32)), Array.set(U32, dst, d, w), (s + 1 : U32), (d + 1 : U32))
79
80# m bytes to a word-aligned d from an unaligned s: each out word joins two source words.
81# lo = 8*(s%4) and hi = 32 - lo; r holds source word k, prev the word before it.
82def copy.shift(n: Nat, +lo: Nat, +hi: Nat, +prev: U32, r: Array<U32> & U32, dst: Array<U32>, +k: U32, +d: U32) -> Array<U32> & Array<U32>:
83  match n:
84    case 0n:
85      (a, w) = r
86      (a, dst)
87    case 1n+p:
88      (a, +w) = r
89      copy.shift(p, lo, hi, w, Array.get(U32, a, (k + 1 : U32)), Array.set(U32, dst, d, (U32.shrn(prev, lo) .|. U32.shln(w, hi) : U32)), (k + 1 : U32), (d + 1 : U32))
90
91def copy.shift.at(+w: U32, +lo: U32, +k: U32, +d: U32, r: Array<U32> & U32, dst: Array<U32>) -> Array<U32> & Array<U32>:
92  (a, prev) = r
93  copy.shift(U32.to_nat(w), U32.to_nat(lo), U32.to_nat((32 - lo : U32)), prev, Array.get(U32, a, (k + 1 : U32)), dst, (k + 1 : U32), d)
94
95def copy.tail(+m: U32, +s: U32, +d: U32, r: Array<U32> & Array<U32>) -> Array<U32> & Array<U32>:
96  (a, b) = r
97  copy.bytes(m, a, b, s, d)
98
99def copy.pick(aligned: Bool, +m: U32, src: Array<U32>, dst: Array<U32>, +s: U32, +d: U32) -> Array<U32> & Array<U32>:
100  match aligned:
101    case True{}:
102      +w = (m >> 2n : U32)
103      +k = (w * 4 : U32)
104      copy.tail((m - k : U32), (s + k : U32), (d + k : U32), copy.words(U32.to_nat(w), Array.get(U32, src, (s >> 2n : U32)), dst, (s >> 2n : U32), (d >> 2n : U32)))
105    case False{}:
106      +w = (m >> 2n : U32)
107      +k = (w * 4 : U32)
108      copy.tail((m - k : U32), (s + k : U32), (d + k : U32), copy.shift.at(w, ((s .&. 3 : U32) * 8 : U32), (s >> 2n : U32), (d >> 2n : U32), Array.get(U32, src, (s >> 2n : U32)), dst))
109
110def copy.dst(daligned: Bool, +m: U32, src: Array<U32>, dst: Array<U32>, +s: U32, +d: U32) -> Array<U32> & Array<U32>:
111  match daligned:
112    case False{}:
113      copy.bytes(m, src, dst, s, d)
114    case True{}:
115      copy.pick(U32.is_eq((s .&. 3 : U32), 0), m, src, dst, s, d)
116
117# m bytes from src[s..] to dst[d..]. Whole words when d is word-aligned, shifted when s is not.
118# ponytail: an unaligned d (append after an odd length) copies bytes; merge into d's first word if that gets hot.
119def copy(+m: U32, src: Array<U32>, dst: Array<U32>, +s: U32, +d: U32) -> Array<U32> & Array<U32>:
120  copy.dst(U32.is_eq((d .&. 3 : U32), 0), m, src, dst, s, d)
121
122# n zero bytes.
123def new(+n: U32) -> Bytes:
124  Bytes{n, alloc(n)}
125
126def length(b: Bytes) -> Bytes & U32:
127  Bytes{+len, buf} = b
128  (Bytes{len, buf}, len)
129
130def get.some(+len: U32, r: Array<U32> & U32) -> Bytes & Maybe<&2, U32>:
131  (a, v) = r
132  (Bytes{len, a}, Some{v})
133
134def get.if(ok: Bool, +len: U32, buf: Array<U32>, +i: U32) -> Bytes & Maybe<&2, U32>:
135  match ok:
136    case True{}:
137      get.some(len, peek(buf, i))
138    case False{}:
139      (Bytes{len, buf}, None{})
140
141# Byte i, or None when i >= len.
142def get(b: Bytes, +i: U32) -> Bytes & Maybe<&2, U32>:
143  Bytes{+len, buf} = b
144  get.if(U32.is_lt(i, len), len, buf, i)
145
146def set.if(ok: Bool, +len: U32, buf: Array<U32>, +i: U32, +v: U32) -> Bytes:
147  match ok:
148    case True{}:
149      Bytes{len, poke(buf, i, v)}
150    case False{}:
151      Bytes{len, buf}
152
153# Byte i becomes v & 255. Nothing changes when i >= len.
154def set(b: Bytes, +i: U32, +v: U32) -> Bytes:
155  Bytes{+len, buf} = b
156  set.if(U32.is_lt(i, len), len, buf, i, v)
157
158# The next index: one forward when up, one back when not.
159def step(+up: Bool, +i: U32) -> U32:
160  Bool.pick(U32, up, (i + 1 : U32), (i - 1 : U32))
161
162# Do n bytes from i fit in len?
163def fits(+len: U32, +i: U32, +n: U32) -> Bool:
164  Bool.and(U32.is_le(n, len), U32.is_le(i, (len - n : U32)))
165
166# n bytes from j, each shifted in below the ones before: the first byte read is the most significant.
167def uint.go(n: Nat, r: Array<U32> & U32, +j: U32, +up: Bool, +acc: U32) -> Array<U32> & U32:
168  match n:
169    case 0n:
170      (a, v) = r
171      (a, acc)
172    case 1n+p:
173      (a, +v) = r
174      uint.go(p, peek(a, step(up, j)), step(up, j), up, ((acc << 8n) .|. v : U32))
175
176# Big-endian reads forward from i; little-endian reads back from the last byte.
177def uint.if(ok: Bool, +len: U32, buf: Array<U32>, +i: U32, +n: U32, +be: Bool) -> Bytes & Maybe<&2, U32>:
178  match ok:
179    case True{}:
180      +j = Bool.pick(U32, be, i, (i + n - 1 : U32))
181      get.some(len, uint.go(U32.to_nat(n), peek(buf, j), j, be, 0))
182    case False{}:
183      (Bytes{len, buf}, None{})
184
185def uint(b: Bytes, +i: U32, +n: U32, +be: Bool) -> Bytes & Maybe<&2, U32>:
186  Bytes{+len, buf} = b
187  uint.if(fits(len, i, n), len, buf, i, n, be)
188
189# Unsigned integers at byte i, or None when they run past len.
190# be: most significant byte first (network order); le: least significant first.
191def get.u16be(b: Bytes, +i: U32) -> Bytes & Maybe<&2, U32>:
192  uint(b, i, 2, True{})
193
194def get.u16le(b: Bytes, +i: U32) -> Bytes & Maybe<&2, U32>:
195  uint(b, i, 2, False{})
196
197def get.u32be(b: Bytes, +i: U32) -> Bytes & Maybe<&2, U32>:
198  uint(b, i, 4, True{})
199
200def get.u32le(b: Bytes, +i: U32) -> Bytes & Maybe<&2, U32>:
201  uint(b, i, 4, False{})
202
203# n bytes of v from j, least significant first.
204def put.go(n: Nat, a: Array<U32>, +j: U32, +up: Bool, +v: U32) -> Array<U32>:
205  match n:
206    case 0n:
207      a
208    case 1n+p:
209      put.go(p, poke(a, j, v), step(up, j), up, U32.shrn(v, 8n))
210
211# Little-endian writes forward from i; big-endian writes back from the last byte.
212def put.if(ok: Bool, +len: U32, buf: Array<U32>, +i: U32, +n: U32, +be: Bool, +v: U32) -> Bytes:
213  match ok:
214    case True{}:
215      Bytes{len, put.go(U32.to_nat(n), buf, Bool.pick(U32, be, (i + n - 1 : U32), i), Bool.not(be), v)}
216    case False{}:
217      Bytes{len, buf}
218
219def put(b: Bytes, +i: U32, +n: U32, +be: Bool, +v: U32) -> Bytes:
220  Bytes{+len, buf} = b
221  put.if(fits(len, i, n), len, buf, i, n, be, v)
222
223# v's low 16 or 32 bits at byte i. Nothing changes when they would run past len.
224def set.u16be(b: Bytes, +i: U32, +v: U32) -> Bytes:
225  put(b, i, 2, True{}, v)
226
227def set.u16le(b: Bytes, +i: U32, +v: U32) -> Bytes:
228  put(b, i, 2, False{}, v)
229
230def set.u32be(b: Bytes, +i: U32, +v: U32) -> Bytes:
231  put(b, i, 4, True{}, v)
232
233def set.u32le(b: Bytes, +i: U32, +v: U32) -> Bytes:
234  put(b, i, 4, False{}, v)
235
236# The U64 whose words, in byte order, are x then y.
237def u64.of(be: Bool, +x: U32, +y: U32) -> Int.U64:
238  match be:
239    case True{}:
240      Int.U64.or(Int.U64.shl(Int.U64.from_u32(x), 32n), Int.U64.from_u32(y))
241    case False{}:
242      Int.U64.or(Int.U64.shl(Int.U64.from_u32(y), 32n), Int.U64.from_u32(x))
243
244def u64.join(+be: Bool, x: Maybe<&2, U32>, y: Maybe<&2, U32>) -> Maybe<&2, Int.U64>:
245  match x y:
246    case Some{a} Some{c}:
247      Some{u64.of(be, a, c)}
248    case _ _:
249      None{}
250
251def u64.lo(+be: Bool, x: Maybe<&2, U32>, r: Bytes & Maybe<&2, U32>) -> Bytes & Maybe<&2, Int.U64>:
252  (b, y) = r
253  (b, u64.join(be, x, y))
254
255def u64.hi(+i: U32, +be: Bool, r: Bytes & Maybe<&2, U32>) -> Bytes & Maybe<&2, Int.U64>:
256  (b, x) = r
257  u64.lo(be, x, uint(b, (i + 4 : U32), 4, be))
258
259def u64(b: Bytes, +i: U32, +be: Bool) -> Bytes & Maybe<&2, Int.U64>:
260  u64.hi(i, be, uint(b, i, 4, be))
261
262# A U64 at byte i, or None when its 8 bytes run past len.
263def get.u64be(b: Bytes, +i: U32) -> Bytes & Maybe<&2, Int.U64>:
264  u64(b, i, True{})
265
266def get.u64le(b: Bytes, +i: U32) -> Bytes & Maybe<&2, Int.U64>:
267  u64(b, i, False{})
268
269# Writes words x then y at byte i, both in the same byte order.
270def put64.if(ok: Bool, +len: U32, buf: Array<U32>, +i: U32, +be: Bool, +x: U32, +y: U32) -> Bytes:
271  match ok:
272    case True{}:
273      put(put(Bytes{len, buf}, i, 4, be, x), (i + 4 : U32), 4, be, y)
274    case False{}:
275      Bytes{len, buf}
276
277def put64(b: Bytes, +i: U32, +be: Bool, +v: Int.U64) -> Bytes:
278  Bytes{+len, buf} = b
279  +hi = Int.U64.to_u32(Int.U64.shr(v, 32n))
280  +lo = Int.U64.to_u32(v)
281  put64.if(fits(len, i, 8), len, buf, i, be, Bool.pick(U32, be, hi, lo), Bool.pick(U32, be, lo, hi))
282
283# v at byte i. Nothing changes when its 8 bytes would run past len.
284def set.u64be(b: Bytes, +i: U32, +v: Int.U64) -> Bytes:
285  put64(b, i, True{}, v)
286
287def set.u64le(b: Bytes, +i: U32, +v: Int.U64) -> Bytes:
288  put64(b, i, False{}, v)
289
290# String.length counts in Nat, which costs more than the walk itself.
291def count(s: String, +n: U32) -> U32:
292  match s:
293    case SNil{}:
294      n
295    case SCon{c, t}:
296      count(t, (n + 1 : U32))
297
298# Bytes enter at the top of w and shift down, so a full word has byte 0 lowest.
299def flush(full: Bool, a: Array<U32>, +k: U32, +w: U32) -> Array<U32>:
300  match full:
301    case True{}:
302      Array.set(U32, a, k, w)
303    case False{}:
304      a
305
306def from.go(s: String, a: Array<U32>, +i: U32, +w: U32) -> Array<U32>:
307  match s:
308    case SNil{}:
309      +r = (i .&. 3 : U32)
310      flush(U32.is_ne(r, 0), a, (i >> 2n : U32), U32.shrn(w, U32.to_nat((((4 - r) .&. 3) * 8 : U32))))
311    case SCon{Chr{+c}, t}:
312      +w2 = ((w >> 8n) .|. (b8(c) << 24n) : U32)
313      +full = U32.is_eq((i .&. 3 : U32), 3)
314      from.go(t, flush(full, a, (i >> 2n : U32), w2), (i + 1 : U32), Bool.pick(U32, full, 0, w2))
315
316# A byte string (one Char per octet, as Wire and Http use) to Bytes. Each Char keeps its low 8 bits.
317def from_string(+s: String) -> Bytes:
318  +n = count(s, 0)
319  Bytes{n, from.go(s, alloc(n), 0, 0)}
320
321def to.go(n: Nat, r: Array<U32> & U32, +i: U32, acc: String) -> String:
322  match n:
323    case 0n:
324      acc
325    case 1n+p:
326      (a, v) = r
327      to.go(p, peek(a, (i - 1 : U32)), (i - 1 : U32), SCon{Chr{v}, acc})
328
329# Bytes to a byte string, one Char per octet.
330def to_string(b: Bytes) -> String:
331  Bytes{+len, buf} = b
332  to.go(U32.to_nat(len), peek(buf, (len - 1 : U32)), (len - 1 : U32), SNil{})
333
334def slice.fin(+len: U32, +m: U32, r: Array<U32> & Array<U32>) -> Bytes & Bytes:
335  (a, c) = r
336  (Bytes{len, a}, Bytes{m, c})
337
338def slice.at(+len: U32, buf: Array<U32>, +s: U32, +m: U32) -> Bytes & Bytes:
339  slice.fin(len, m, copy(m, buf, alloc(m), s, 0))
340
341# The buffer back, and a copy of up to n bytes from start. Both ends are clamped to len.
342def slice(b: Bytes, +start: U32, +n: U32) -> Bytes & Bytes:
343  Bytes{+len, buf} = b
344  +s = U32.min(start, len)
345  slice.at(len, buf, s, U32.min(n, (len - s : U32)))
346
347def clone.of(+len: U32, r: Array<U32> & Array<U32>) -> Bytes & Bytes:
348  (a, c) = r
349  (Bytes{len, a}, Bytes{len, c})
350
351# Two buffers that hold the same bytes.
352def clone(b: Bytes) -> Bytes & Bytes:
353  Bytes{+len, buf} = b
354  clone.of(len, Array.clone(U32, buf))
355
356def dst(r: Array<U32> & Array<U32>) -> Array<U32>:
357  (src, out) = r
358  out
359
360# Does a buffer holding len bytes have room for n? Its 2^d words fit the fewest that hold len.
361def room(+len: U32, +n: U32) -> Bool:
362  U32.is_le(words(n), U32.shln(1, depth(words(len))))
363
364def grow.if(fits: Bool, +len: U32, buf: Array<U32>, +n: U32) -> Array<U32>:
365  match fits:
366    case True{}:
367      buf
368    case False{}:
369      dst(copy(len, buf, alloc(n), 0, 0))
370
371# buf, or a copy of its first len bytes in the fewest 2^d words that hold n.
372def grow(+len: U32, buf: Array<U32>, +n: U32) -> Array<U32>:
373  grow.if(room(len, n), len, buf, n)
374
375# a then b. b is written into a's buffer while it has room, and the buffer at least
376# doubles when it runs out, so building a buffer one piece at a time is O(total).
377def append(a: Bytes, b: Bytes) -> Bytes:
378  Bytes{+la, ba} = a
379  Bytes{+lb, bb} = b
380  +n = (la + lb : U32)
381  Bytes{n, dst(copy(lb, bb, grow(la, ba, n), 0, la))}
382
383def concat.total.con(x: Bytes, r: List<&1, Bytes> & U32) -> List<&1, Bytes> & U32:
384  (t, n) = r
385  (Con{x, t}, n)
386
387def concat.total(xs: List<&1, Bytes>, +n: U32) -> List<&1, Bytes> & U32:
388  match xs:
389    case Nil{}:
390      (Nil{}, n)
391    case Con{x, t}:
392      Bytes{+l, buf} = x
393      concat.total.con(Bytes{l, buf}, concat.total(t, (n + l : U32)))
394
395def concat.go(xs: List<&1, Bytes>, out: Array<U32>, +at: U32) -> Array<U32>:
396  match xs:
397    case Nil{}:
398      out
399    case Con{x, t}:
400      Bytes{+l, buf} = x
401      concat.go(t, dst(copy(l, buf, out, 0, at)), (at + l : U32))
402
403def concat.of(r: List<&1, Bytes> & U32) -> Bytes:
404  (xs, +n) = r
405  Bytes{n, concat.go(xs, alloc(n), 0)}
406
407# The pieces in order, in one new buffer: one copy per byte, however many pieces.
408def concat(xs: List<&1, Bytes>) -> Bytes:
409  concat.of(concat.total(xs, 0))
410
411# Does needle match at j? ok is the previous byte's result; the first mismatch stops the walk.
412def at.go(needle: String, ok: Bool, r: Array<U32> & U32, +j: U32) -> Array<U32> & Bool:
413  match needle:
414    case SNil{}:
415      (a, v) = r
416      (a, ok)
417    case SCon{Chr{+c}, t}:
418      match ok:
419        case False{}:
420          (a, v) = r
421          (a, False{})
422        case True{}:
423          (a, +v) = r
424          at.go(t, U32.is_eq(v, c), peek(a, (j + 1 : U32)), (j + 1 : U32))
425
426def at(a: Array<U32>, +needle: String, +j: U32) -> Array<U32> & Bool:
427  at.go(needle, True{}, peek(a, j), j)
428
429# ponytail: naive search; a mismatch costs one byte read per position, but a repetitive needle is O(len * needle). Add a SWAR scan or two-way search if find gets hot.
430# f counts the positions left after i.
431def find.go(f: Nat, r: Array<U32> & Bool, +needle: String, +i: U32, +up: Bool) -> Array<U32> & Maybe<&2, U32>:
432  match f:
433    case 0n:
434      (a, hit) = r
435      (a, Bool.pick(Maybe<&2, U32>, hit, Some{i}, None{}))
436    case 1n+p:
437      (a, hit) = r
438      match hit:
439        case True{}:
440          (a, Some{i})
441        case False{}:
442          find.go(p, at(a, needle, step(up, i)), needle, step(up, i), up)
443
444def find.fin(+len: U32, r: Array<U32> & Maybe<&2, U32>) -> Bytes & Maybe<&2, U32>:
445  (a, x) = r
446  (Bytes{len, a}, x)
447
448def find.at(none: Bool, +len: U32, buf: Array<U32>, +needle: String, +i: U32, +f: U32, +up: Bool) -> Bytes & Maybe<&2, U32>:
449  match none:
450    case True{}:
451      (Bytes{len, buf}, None{})
452    case False{}:
453      find.fin(len, find.go(U32.to_nat(f), at(buf, needle, i), needle, i, up))
454
455# Index of the first match of needle (a byte string) at or after start, or None.
456# An empty needle matches at start when start <= len.
457def find.from(b: Bytes, +needle: String, +start: U32) -> Bytes & Maybe<&2, U32>:
458  Bytes{+len, buf} = b
459  +m = count(needle, 0)
460  find.at(Bool.or(U32.is_lt(len, m), U32.is_lt((len - m : U32), start)), len, buf, needle, start, (len - m - start : U32), True{})
461
462# Index of the first match of needle (a byte string), or None. An empty needle matches at 0.
463def find(b: Bytes, +needle: String) -> Bytes & Maybe<&2, U32>:
464  find.from(b, needle, 0)
465
466# Index of the last match of needle, or None. An empty needle matches at len.
467def rfind(b: Bytes, +needle: String) -> Bytes & Maybe<&2, U32>:
468  Bytes{+len, buf} = b
469  +m = count(needle, 0)
470  find.at(U32.is_lt(len, m), len, buf, needle, (len - m : U32), (len - m : U32), False{})
471
472def at.fin(+len: U32, r: Array<U32> & Bool) -> Bytes & Bool:
473  (a, ok) = r
474  (Bytes{len, a}, ok)
475
476def at.if(fits: Bool, +len: U32, buf: Array<U32>, +needle: String, +j: U32) -> Bytes & Bool:
477  match fits:
478    case True{}:
479      at.fin(len, at(buf, needle, j))
480    case False{}:
481      (Bytes{len, buf}, False{})
482
483# Does b begin with prefix (a byte string)?
484def starts_with(b: Bytes, +prefix: String) -> Bytes & Bool:
485  Bytes{+len, buf} = b
486  +m = count(prefix, 0)
487  at.if(U32.is_le(m, len), len, buf, prefix, 0)
488
489# Does b end with suffix (a byte string)?
490def ends_with(b: Bytes, +suffix: String) -> Bytes & Bool:
491  Bytes{+len, buf} = b
492  +m = count(suffix, 0)
493  at.if(U32.is_le(m, len), len, buf, suffix, (len - m : U32))
494
495# Match positions of sep, latest first, that do not overlap an earlier match.
496# f counts the positions left; skip counts the bytes still inside the last match.
497def split.scan(f: Nat, r: Array<U32> & Bool, +sep: String, +m: U32, +i: U32, +skip: U32, +cuts: List<&2, U32>) -> Array<U32> & List<&2, U32>:
498  match f:
499    case 0n:
500      (a, hit) = r
501      (a, cuts)
502    case 1n+p:
503      (a, +hit) = r
504      +take = Bool.and(hit, U32.is_eq(skip, 0))
505      +next = Bool.pick(U32, take, (m - 1 : U32), Bool.pick(U32, U32.is_eq(skip, 0), 0, (skip - 1 : U32)))
506      split.scan(p, at(a, sep, (i + 1 : U32)), sep, m, (i + 1 : U32), next, Bool.pick(List<&2, U32>, take, Con{i, cuts}, cuts))
507
508def snd(r: Bytes & Bytes) -> Bytes:
509  (a, b) = r
510  b
511
512# r holds the buffer and the piece that ends at end; each earlier cut j starts one at j + m.
513def split.cut(cuts: List<&2, U32>, r: Bytes & Bytes, +end: U32, +m: U32, acc: List<&1, Bytes>) -> List<&1, Bytes>:
514  match cuts:
515    case Nil{}:
516      (b, piece) = r
517      Con{snd(slice(b, 0, end)), Con{piece, acc}}
518    case Con{+j, t}:
519      (b, piece) = r
520      split.cut(t, slice(b, (j + m : U32), (end - j - m : U32)), j, m, Con{piece, acc})
521
522def split.of(cuts: List<&2, U32>, b: Bytes, +len: U32, +m: U32) -> List<&1, Bytes>:
523  match cuts:
524    case Nil{}:
525      Con{b, Nil{}}
526    case Con{+j, t}:
527      split.cut(t, slice(b, (j + m : U32), (len - j - m : U32)), j, m, Nil{})
528
529def split.run(+len: U32, +m: U32, r: Array<U32> & List<&2, U32>) -> List<&1, Bytes>:
530  (a, cuts) = r
531  split.of(cuts, Bytes{len, a}, len, m)
532
533def split.if(whole: Bool, +len: U32, buf: Array<U32>, +sep: String, +m: U32) -> List<&1, Bytes>:
534  match whole:
535    case True{}:
536      Con{Bytes{len, buf}, Nil{}}
537    case False{}:
538      split.run(len, m, split.scan(U32.to_nat((len - m + 1 : U32)), at(buf, sep, 0), sep, m, 0, 0, Nil{}))
539
540# The pieces between matches of sep (a byte string), left to right. n matches give n + 1
541# pieces, so a match at either end gives an empty piece. An empty sep gives b whole.
542def split(b: Bytes, +sep: String) -> List<&1, Bytes>:
543  Bytes{+len, buf} = b
544  +m = count(sep, 0)
545  split.if(Bool.or(U32.is_eq(m, 0), U32.is_lt(len, m)), len, buf, sep, m)
546
547# Compares whole words; same tells whether the previous pair matched.
548def eq.go(n: Nat, same: Bool, r: Array<U32> & U32, s: Array<U32> & U32, +i: U32) -> Array<U32> & Array<U32> & Bool:
549  match n:
550    case 0n:
551      (x, v) = r
552      (y, w) = s
553      (x, y, same)
554    case 1n+p:
555      match same:
556        case False{}:
557          (x, v) = r
558          (y, w) = s
559          (x, y, False{})
560        case True{}:
561          (x, +v) = r
562          (y, +w) = s
563          eq.go(p, U32.is_eq(v, w), Array.get(U32, x, (i + 1 : U32)), Array.get(U32, y, (i + 1 : U32)), (i + 1 : U32))
564
565def eq.fin(+la: U32, +lb: U32, r: Array<U32> & Array<U32> & Bool) -> Bytes & Bytes & Bool:
566  (x, y, ok) = r
567  (Bytes{la, x}, Bytes{lb, y}, ok)
568
569def eq.len(same: Bool, +la: U32, xa: Array<U32>, +lb: U32, ya: Array<U32>) -> Bytes & Bytes & Bool:
570  match same:
571    case False{}:
572      (Bytes{la, xa}, Bytes{lb, ya}, False{})
573    case True{}:
574      eq.fin(la, lb, eq.go(U32.to_nat(words(la)), True{}, Array.get(U32, xa, 0), Array.get(U32, ya, 0), 0))
575
576# Both buffers back, and whether they hold the same bytes.
577def eq(a: Bytes, b: Bytes) -> Bytes & Bytes & Bool:
578  Bytes{+la, xa} = a
579  Bytes{+lb, ya} = b
580  eq.len(U32.is_eq(la, lb), la, xa, lb, ya)
581
582# Byte 0 of w becomes the most significant, so words compare in byte order.
583def bswap(+w: U32) -> U32:
584  ((b8(w) << 24n) .|. (b8(U32.shrn(w, 8n)) << 16n) .|. (b8(U32.shrn(w, 16n)) << 8n) .|. U32.shrn(w, 24n) : U32)
585
586# Compares whole words; c is the previous pair's order.
587def cmp.go(n: Nat, c: Cmp, r: Array<U32> & U32, s: Array<U32> & U32, +i: U32) -> Array<U32> & Array<U32> & Cmp:
588  match n:
589    case 0n:
590      (x, v) = r
591      (y, w) = s
592      (x, y, c)
593    case 1n+p:
594      match c:
595        case LT{}:
596          (x, v) = r
597          (y, w) = s
598          (x, y, LT{})
599        case GT{}:
600          (x, v) = r
601          (y, w) = s
602          (x, y, GT{})
603        case EQ{}:
604          (x, +v) = r
605          (y, +w) = s
606          cmp.go(p, U32.cmp(bswap(v), bswap(w)), Array.get(U32, x, (i + 1 : U32)), Array.get(U32, y, (i + 1 : U32)), (i + 1 : U32))
607
608def cmp.len(c: Cmp, +la: U32, +lb: U32) -> Cmp:
609  match c:
610    case EQ{}:
611      U32.cmp(la, lb)
612    case LT{}:
613      LT{}
614    case GT{}:
615      GT{}
616
617def cmp.fin(+la: U32, +lb: U32, r: Array<U32> & Array<U32> & Cmp) -> Bytes & Bytes & Cmp:
618  (x, y, c) = r
619  (Bytes{la, x}, Bytes{lb, y}, cmp.len(c, la, lb))
620
621# Both buffers back, and their order byte by byte; a prefix sorts first.
622# The shorter buffer's bytes past its len are 0, so its last word compares low when only the longer one goes on.
623def cmp(a: Bytes, b: Bytes) -> Bytes & Bytes & Cmp:
624  Bytes{+la, xa} = a
625  Bytes{+lb, ya} = b
626  cmp.fin(la, lb, cmp.go(U32.to_nat(words(U32.min(la, lb))), EQ{}, Array.get(U32, xa, 0), Array.get(U32, ya, 0), 0))
627
628def nibble(+n: U32) -> Char:
629  Chr{Bool.pick(U32, U32.is_lt(n, 10), (48 + n : U32), (87 + n : U32))}
630
631def hex.go(n: Nat, r: Array<U32> & U32, +i: U32, acc: String) -> String:
632  match n:
633    case 0n:
634      acc
635    case 1n+p:
636      (a, +v) = r
637      hex.go(p, peek(a, (i - 1 : U32)), (i - 1 : U32), SCon{nibble(U32.shrn(v, 4n)), SCon{nibble((v .&. 15 : U32)), acc}})
638
639# Two lowercase hex digits per byte.
640def to_hex(b: Bytes) -> String:
641  Bytes{+len, buf} = b
642  hex.go(U32.to_nat(len), peek(buf, (len - 1 : U32)), (len - 1 : U32), SNil{})
643
644def in(+lo: U32, +c: U32, +hi: U32) -> Bool:
645  Bool.and(U32.is_le(lo, c), U32.is_le(c, hi))
646
647# A hex digit's value, or 16.
648def unnibble(+c: U32) -> U32:
649  Bool.pick(U32, in(48, c, 57), (c - 48 : U32), Bool.pick(U32, in(97, c, 102), (c - 87 : U32), Bool.pick(U32, in(65, c, 70), (c - 55 : U32), 16)))
650
651def poke.when(write: Bool, a: Array<U32>, +i: U32, +v: U32) -> Array<U32>:
652  match write:
653    case True{}:
654      poke(a, i, v)
655    case False{}:
656      a
657
658# hi is the previous digit; an odd i completes a byte.
659def unhex.go(s: String, a: Array<U32>, +i: U32, +hi: U32, +ok: Bool) -> Array<U32> & Bool:
660  match s:
661    case SNil{}:
662      (a, ok)
663    case SCon{Chr{+c}, t}:
664      +d = unnibble(c)
665      unhex.go(t, poke.when(U32.is_eq((i .&. 1 : U32), 1), a, (i >> 1n : U32), ((hi << 4n) .|. d : U32)), (i + 1 : U32), d, Bool.and(ok, U32.is_lt(d, 16)))
666
667def decoded(+n: U32, r: Array<U32> & Bool) -> Maybe<&1, Bytes>:
668  (a, ok) = r
669  match ok:
670    case True{}:
671      Some{Bytes{n, a}}
672    case False{}:
673      None{}
674
675def unhex.if(even: Bool, +s: String, +n: U32) -> Maybe<&1, Bytes>:
676  match even:
677    case True{}:
678      decoded((n >> 1n : U32), unhex.go(s, alloc((n >> 1n : U32)), 0, 0, True{}))
679    case False{}:
680      None{}
681
682# Hex digits, either case, to bytes. None for an odd count or a non-hex char.
683def from_hex(+s: String) -> Maybe<&1, Bytes>:
684  +n = count(s, 0)
685  unhex.if(U32.is_eq((n .&. 1 : U32), 0), s, n)
686
687# RFC 4648 §4: the standard alphabet, padded with '='.
688def b64.char(+i: U32) -> U32:
689  Bool.pick(U32, U32.is_lt(i, 26), (65 + i : U32), Bool.pick(U32, U32.is_lt(i, 52), (71 + i : U32), Bool.pick(U32, U32.is_lt(i, 62), (i - 4 : U32), Bool.pick(U32, U32.is_eq(i, 62), 43, 47))))
690
691# The six bits of v at k as a base64 char.
692def b64.at(+v: U32, +k: Nat) -> Char:
693  Chr{b64.char((U32.shrn(v, k) .&. 63 : U32))}
694
695# Groups of three bytes, last first; r holds the 24 bits of the group at i.
696def b64.go(n: Nat, r: Array<U32> & U32, +i: U32, acc: String) -> String:
697  match n:
698    case 0n:
699      acc
700    case 1n+p:
701      (a, +v) = r
702      +j = (i - 3 : U32)
703      b64.go(p, uint.go(3n, peek(a, j), j, True{}, 0), j, SCon{b64.at(v, 18n), SCon{b64.at(v, 12n), SCon{b64.at(v, 6n), SCon{b64.at(v, 0n), acc}}}})
704
705# The rem < 3 bytes after the last whole group, then the groups before them.
706def b64.tail(+rem: U32, +t: U32, +q: U32, r: Array<U32> & U32) -> String:
707  (a, +v0) = r
708  +v = U32.shln(v0, U32.to_nat(((3 - rem) * 8 : U32)))
709  +end = Bool.pick(String, U32.is_eq(rem, 0), "", Bool.pick(String, U32.is_eq(rem, 1), SCon{b64.at(v, 18n), SCon{b64.at(v, 12n), "=="}}, SCon{b64.at(v, 18n), SCon{b64.at(v, 12n), SCon{b64.at(v, 6n), "="}}}))
710  +j = (t - 3 : U32)
711  b64.go(U32.to_nat(q), uint.go(3n, peek(a, j), j, True{}, 0), j, end)
712
713# Base64 (RFC 4648 §4) with '=' padding.
714def to_base64(b: Bytes) -> String:
715  Bytes{+len, buf} = b
716  +q = (len / 3 : U32)
717  +t = (q * 3 : U32)
718  b64.tail((len - t : U32), t, q, uint.go(U32.to_nat((len - t : U32)), peek(buf, t), t, True{}, 0))
719
720# A base64 char's value, 64 for '=', or 65.
721def b64.val(+c: U32) -> U32:
722  Bool.pick(U32, in(65, c, 90), (c - 65 : U32), Bool.pick(U32, in(97, c, 122), (c - 71 : U32), Bool.pick(U32, in(48, c, 57), (c + 4 : U32), Bool.pick(U32, U32.is_eq(c, 43), 62, Bool.pick(U32, U32.is_eq(c, 47), 63, Bool.pick(U32, U32.is_eq(c, 61), 64, 65))))))
723
724# The count of '=' at the end of s.
725def b64.pads(s: String, +run: U32) -> U32:
726  match s:
727    case SNil{}:
728      run
729    case SCon{Chr{+c}, t}:
730      b64.pads(t, Bool.pick(U32, U32.is_eq(c, 61), (run + 1 : U32), 0))
731
732# A whole group of four chars writes its bytes at o, as many as fit before len.
733def b64.put(full: Bool, a: Array<U32>, +o: U32, +w: U32, +v: U32) -> Array<U32>:
734  match full:
735    case True{}:
736      put.go(U32.to_nat(w), a, (o + w - 1 : U32), False{}, U32.shrn(v, U32.to_nat(((3 - w) * 8 : U32))))
737    case False{}:
738      a
739
740# v collects six bits per char. '=' is allowed only at body and after.
741def unb64.go(s: String, a: Array<U32>, +i: U32, +v: U32, +ok: Bool, +len: U32, +body: U32) -> Array<U32> & Bool:
742  match s:
743    case SNil{}:
744      (a, ok)
745    case SCon{Chr{+c}, t}:
746      +d = b64.val(c)
747      +v2 = ((v << 6n) .|. (d .&. 63) : U32)
748      +o = ((i >> 2n) * 3 : U32)
749      +good = Bool.pick(Bool, U32.is_lt(i, body), U32.is_lt(d, 64), U32.is_eq(d, 64))
750      unb64.go(t, b64.put(U32.is_eq((i .&. 3 : U32), 3), a, o, U32.min(3, (len - o : U32)), v2), (i + 1 : U32), v2, Bool.and(ok, good), len, body)
751
752def unb64.if(ok: Bool, +s: String, +n: U32, +pads: U32) -> Maybe<&1, Bytes>:
753  match ok:
754    case True{}:
755      +len = ((n >> 2n) * 3 - pads : U32)
756      decoded(len, unb64.go(s, alloc(len), 0, 0, True{}, len, (n - pads : U32)))
757    case False{}:
758      None{}
759
760# Padded base64 (RFC 4648 §4) to bytes. None for a length that is not a multiple of 4,
761# more than two '=', '=' before the end, or a char outside the alphabet.
762def from_base64(+s: String) -> Maybe<&1, Bytes>:
763  +n = count(s, 0)
764  +pads = b64.pads(s, 0)
765  unb64.if(Bool.and(U32.is_eq((n .&. 3 : U32), 0), U32.is_le(pads, 2)), s, n, pads)
766
767# For a digit d, n * 10 + d overflows exactly when (n * 10 + d) / 10 != n in wrapping U32.
768def u32.read.go(n: Nat, r: Array<U32> & U32, +i: U32, +acc: U32, +ok: Bool) -> Maybe<&2, U32>:
769  match n:
770    case 0n:
771      (a, v) = r
772      Bool.pick(Maybe<&2, U32>, ok, Some{acc}, None{})
773    case 1n+p:
774      (a, +v) = r
775      +m = (acc * 10 + (v - 48) : U32)
776      u32.read.go(p, peek(a, (i + 1 : U32)), (i + 1 : U32), m, Bool.and(ok, Bool.and(in(48, v, 57), U32.is_eq((m / 10 : U32), acc))))
777
778# ASCII decimal digits to a U32. None when b is empty, holds a non-digit, or exceeds 4294967295.
779def u32.read(b: Bytes) -> Maybe<&2, U32>:
780  Bytes{+len, buf} = b
781  u32.read.go(U32.to_nat(len), peek(buf, 0), 0, 0, U32.is_ne(len, 0))
782
783# The digit count of n, at most 10.
784def u32.width(f: Nat, small: Bool, +n: U32, +k: U32) -> U32:
785  match f:
786    case 0n:
787      k
788    case 1n+p:
789      match small:
790        case True{}:
791          k
792        case False{}:
793          u32.width(p, U32.is_lt((n / 10 : U32), 10), (n / 10 : U32), (k + 1 : U32))
794
795def u32.digits(f: Nat, a: Array<U32>, +i: U32, +n: U32) -> Array<U32>:
796  match f:
797    case 0n:
798      a
799    case 1n+p:
800      u32.digits(p, poke(a, i, (48 + n % 10 : U32)), (i - 1 : U32), (n / 10 : U32))
801
802# n in ASCII decimal, with no leading zeros.
803def u32.show(+n: U32) -> Bytes:
804  +k = u32.width(10n, U32.is_lt(n, 10), n, 1)
805  Bytes{k, u32.digits(U32.to_nat(k), alloc(k), (k - 1 : U32), n)}
806
807# A cursor owns the same packed buffer; start and end bound a region without slicing it.
808type Cursor is Type:
809  Cursor{bytes: Bytes, pos: U32, start: U32, end: U32}
810
811type CursorLimit is Type:
812  CursorLimit{resume: U32, start: U32, end: U32}
813
814def Cursor.new(b: Bytes) -> Cursor:
815  Bytes{+len, buf} = b
816  Cursor{Bytes{len, buf}, 0, 0, len}
817
818def Cursor.finish(c: Cursor) -> Bytes & U32:
819  Cursor{b, pos, start, end} = c
820  (b, pos)
821
822def Cursor.position(c: Cursor) -> Cursor & U32:
823  Cursor{b, +pos, start, end} = c
824  (Cursor{b, pos, start, end}, pos)
825
826def Cursor.remaining(c: Cursor) -> Cursor & U32:
827  Cursor{b, +pos, start, +end} = c
828  (Cursor{b, pos, start, end}, (end - U32.min(pos, end) : U32))
829
830def Cursor.fits(+len: U32, +pos: U32, +start: U32, +end: U32, +n: U32) -> Bool:
831  U32.is_le(start, pos) && U32.is_le(end, len) && fits(end, pos, n)
832
833def Cursor.seek.if(ok: Bool, c: Cursor, +pos: U32) -> Cursor & Bool:
834  match ok:
835    case False{}:
836      (c, False{})
837    case True{}:
838      Cursor{b, old, start, end} = c
839      (Cursor{b, pos, start, end}, True{})
840
841def Cursor.seek(c: Cursor, +pos: U32) -> Cursor & Bool:
842  Cursor{Bytes{+len, buf}, old, +start, +end} = c
843  Cursor.seek.if(Cursor.fits(len, pos, start, end, 0), Cursor{Bytes{len, buf}, old, start, end}, pos)
844
845def Cursor.skip(c: Cursor, +n: U32) -> Cursor & Bool:
846  Cursor{Bytes{+len, buf}, +pos, +start, +end} = c
847  Cursor.seek.if(Cursor.fits(len, pos, start, end, n), Cursor{Bytes{len, buf}, pos, start, end}, (pos + n : U32))
848
849# On success, read inside the region, then leave with the returned affine limit.
850def Cursor.region.if(ok: Bool, c: Cursor, +n: U32) -> Cursor & Maybe<&1, CursorLimit>:
851  match ok:
852    case False{}:
853      (c, None{})
854    case True{}:
855      Cursor{b, +pos, start, end} = c
856      +resume = (pos + n : U32)
857      (Cursor{b, pos, pos, resume}, Some{CursorLimit{resume, start, end}})
858
859def Cursor.region(c: Cursor, +n: U32) -> Cursor & Maybe<&1, CursorLimit>:
860  Cursor{Bytes{+len, buf}, +pos, +start, +end} = c
861  Cursor.region.if(Cursor.fits(len, pos, start, end, n), Cursor{Bytes{len, buf}, pos, start, end}, n)
862
863def Cursor.leave(c: Cursor, limit: CursorLimit) -> Cursor:
864  Cursor{b, pos, start, end} = c
865  CursorLimit{resume, outer_start, outer_end} = limit
866  Cursor{b, resume, outer_start, outer_end}
867
868def Cursor.read.done(~T: Data, +pos: U32, start: U32, end: U32, +n: U32, r: Bytes & Maybe<&2, T>) -> Cursor & Maybe<&2, T>:
869  (b, m) = r
870  match m:
871    case None{}:
872      (Cursor{b, pos, start, end}, None{})
873    case Some{v}:
874      (Cursor{b, (pos + n : U32), start, end}, Some{v})
875
876def Cursor.read.if(~T: Data, ~read: Bytes -> @+i:U32 -> Bytes & Maybe<&2, T>, ok: Bool, c: Cursor, +n: U32) -> Cursor & Maybe<&2, T>:
877  match ok:
878    case False{}:
879      (c, None{})
880    case True{}:
881      Cursor{b, +pos, start, end} = c
882      Cursor.read.done(~T, pos, start, end, n, read(b, pos))
883
884def Cursor.read(~T: Data, ~read: Bytes -> @+i:U32 -> Bytes & Maybe<&2, T>, c: Cursor, +n: U32) -> Cursor & Maybe<&2, T>:
885  Cursor{Bytes{+len, buf}, +pos, +start, +end} = c
886  Cursor.read.if(~T, ~read, Cursor.fits(len, pos, start, end, n), Cursor{Bytes{len, buf}, pos, start, end}, n)
887
888def Cursor.u8(c: Cursor) -> Cursor & Maybe<&2, U32>:
889  Cursor.read(~U32, ~get, c, 1)
890
891def Cursor.u16be(c: Cursor) -> Cursor & Maybe<&2, U32>:
892  Cursor.read(~U32, ~get.u16be, c, 2)
893
894def Cursor.u16le(c: Cursor) -> Cursor & Maybe<&2, U32>:
895  Cursor.read(~U32, ~get.u16le, c, 2)
896
897def Cursor.u32be(c: Cursor) -> Cursor & Maybe<&2, U32>:
898  Cursor.read(~U32, ~get.u32be, c, 4)
899
900def Cursor.u32le(c: Cursor) -> Cursor & Maybe<&2, U32>:
901  Cursor.read(~U32, ~get.u32le, c, 4)
902
903def Cursor.u64be(c: Cursor) -> Cursor & Maybe<&2, Int.U64>:
904  Cursor.read(~Int.U64, ~get.u64be, c, 8)
905
906def Cursor.u64le(c: Cursor) -> Cursor & Maybe<&2, Int.U64>:
907  Cursor.read(~Int.U64, ~get.u64le, c, 8)
908
909def Cursor.write.if(~T: Data, ~write: Bytes -> @+i:U32 -> @+v:T -> Bytes, ok: Bool, c: Cursor, +n: U32, v: T) -> Cursor & Bool:
910  match ok:
911    case False{}:
912      (c, False{})
913    case True{}:
914      Cursor{b, +pos, start, end} = c
915      (Cursor{write(b, pos, v), (pos + n : U32), start, end}, True{})
916
917def Cursor.write(~T: Data, ~write: Bytes -> @+i:U32 -> @+v:T -> Bytes, c: Cursor, +n: U32, v: T) -> Cursor & Bool:
918  Cursor{Bytes{+len, buf}, +pos, +start, +end} = c
919  Cursor.write.if(~T, ~write, Cursor.fits(len, pos, start, end, n), Cursor{Bytes{len, buf}, pos, start, end}, n, v)
920
921def Cursor.put.u8(c: Cursor, v: U32) -> Cursor & Bool:
922  Cursor.write(~U32, ~set, c, 1, v)
923
924def Cursor.put.u16be(c: Cursor, v: U32) -> Cursor & Bool:
925  Cursor.write(~U32, ~set.u16be, c, 2, v)
926
927def Cursor.put.u16le(c: Cursor, v: U32) -> Cursor & Bool:
928  Cursor.write(~U32, ~set.u16le, c, 2, v)
929
930def Cursor.put.u32be(c: Cursor, v: U32) -> Cursor & Bool:
931  Cursor.write(~U32, ~set.u32be, c, 4, v)
932
933def Cursor.put.u32le(c: Cursor, v: U32) -> Cursor & Bool:
934  Cursor.write(~U32, ~set.u32le, c, 4, v)
935
936def Cursor.put.u64be(c: Cursor, v: Int.U64) -> Cursor & Bool:
937  Cursor.write(~Int.U64, ~set.u64be, c, 8, v)
938
939def Cursor.put.u64le(c: Cursor, v: Int.U64) -> Cursor & Bool:
940  Cursor.write(~Int.U64, ~set.u64le, c, 8, v)