bytes.bend
bend-kit-bytes@0.3.0.0 · 700 lines · 0 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
4# Bytes{len, buf}: byte i is bits 8*(i%4) of buf[i/4]. buf has the fewest 2^d words
5# that hold len bytes. Every byte at or past len is 0, so equal buffers have equal words.
6# Out-of-range reads answer None and out-of-range writes do nothing; Array alone would wrap.
7# import ./bytes/bytes.bend as Bytes
8
9type Bytes is Type:
10 Bytes{len: U32, buf: Array<U32>}
11
12def b8(+x: U32) -> U32:
13 (x .&. 255 : U32)
14
15def shift(+i: U32) -> Nat:
16 U32.to_nat(((i .&. 3 : U32) * 8 : U32))
17
18def words(+n: U32) -> U32:
19 ((n + 3 : U32) >> 2n : U32)
20
21# The fewest d with 2^d >= w.
22def depth.go(f: Nat, more: Bool, +w: U32, +d: Nat, +cap: U32) -> Nat:
23 match f:
24 case 0n:
25 d
26 case 1n+p:
27 match more:
28 case False{}:
29 d
30 case True{}:
31 depth.go(p, U32.is_lt((cap * 2 : U32), w), w, 1n+d, (cap * 2 : U32))
32
33def depth(+w: U32) -> Nat:
34 depth.go(32n, U32.is_lt(1, w), w, 0n, 1)
35
36def alloc(+n: U32) -> Array<U32>:
37 Array.new(U32, depth(words(n)), 0)
38
39# Unchecked byte read and write. Callers keep i below len.
40def peek.of(+sh: Nat, r: Array<U32> & U32) -> Array<U32> & U32:
41 (a, w) = r
42 (a, b8(U32.shrn(w, sh)))
43
44def peek(a: Array<U32>, +i: U32) -> Array<U32> & U32:
45 peek.of(shift(i), Array.get(U32, a, (i >> 2n : U32)))
46
47def poke.of(+i: U32, +v: U32, r: Array<U32> & U32) -> Array<U32>:
48 (a, w) = r
49 +sh = shift(i)
50 Array.set(U32, a, (i >> 2n : U32), ((w .&. ((255 << sh) .^. 4294967295)) .|. (b8(v) << sh) : U32))
51
52def poke(a: Array<U32>, +i: U32, +v: U32) -> Array<U32>:
53 poke.of(i, v, Array.get(U32, a, (i >> 2n : U32)))
54
55# n bytes from src[s..] to dst[d..], one byte at a time.
56def copy.go(n: Nat, r: Array<U32> & U32, dst: Array<U32>, +s: U32, +d: U32) -> Array<U32> & Array<U32>:
57 match n:
58 case 0n:
59 (a, v) = r
60 (a, dst)
61 case 1n+p:
62 (a, v) = r
63 copy.go(p, peek(a, (s + 1 : U32)), poke(dst, d, v), (s + 1 : U32), (d + 1 : U32))
64
65def copy.bytes(+m: U32, src: Array<U32>, dst: Array<U32>, +s: U32, +d: U32) -> Array<U32> & Array<U32>:
66 copy.go(U32.to_nat(m), peek(src, s), dst, s, d)
67
68# n words from src[s..] to dst[d..] (word indexes).
69def copy.words(n: Nat, r: Array<U32> & U32, dst: Array<U32>, +s: U32, +d: U32) -> Array<U32> & Array<U32>:
70 match n:
71 case 0n:
72 (a, w) = r
73 (a, dst)
74 case 1n+p:
75 (a, +w) = r
76 copy.words(p, Array.get(U32, a, (s + 1 : U32)), Array.set(U32, dst, d, w), (s + 1 : U32), (d + 1 : U32))
77
78# m bytes to a word-aligned d from an unaligned s: each out word joins two source words.
79# lo = 8*(s%4) and hi = 32 - lo; r holds source word k, prev the word before it.
80def 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>:
81 match n:
82 case 0n:
83 (a, w) = r
84 (a, dst)
85 case 1n+p:
86 (a, +w) = r
87 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))
88
89def copy.shift.at(+w: U32, +lo: U32, +k: U32, +d: U32, r: Array<U32> & U32, dst: Array<U32>) -> Array<U32> & Array<U32>:
90 (a, prev) = r
91 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)
92
93def copy.tail(+m: U32, +s: U32, +d: U32, r: Array<U32> & Array<U32>) -> Array<U32> & Array<U32>:
94 (a, b) = r
95 copy.bytes(m, a, b, s, d)
96
97def copy.pick(aligned: Bool, +m: U32, src: Array<U32>, dst: Array<U32>, +s: U32, +d: U32) -> Array<U32> & Array<U32>:
98 match aligned:
99 case True{}:
100 +w = (m >> 2n : U32)
101 +k = (w * 4 : U32)
102 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)))
103 case False{}:
104 +w = (m >> 2n : U32)
105 +k = (w * 4 : U32)
106 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))
107
108def copy.dst(daligned: Bool, +m: U32, src: Array<U32>, dst: Array<U32>, +s: U32, +d: U32) -> Array<U32> & Array<U32>:
109 match daligned:
110 case False{}:
111 copy.bytes(m, src, dst, s, d)
112 case True{}:
113 copy.pick(U32.is_eq((s .&. 3 : U32), 0), m, src, dst, s, d)
114
115# m bytes from src[s..] to dst[d..]. Whole words when d is word-aligned, shifted when s is not.
116# ponytail: an unaligned d (append after an odd length) copies bytes; merge into d's first word if that gets hot.
117def copy(+m: U32, src: Array<U32>, dst: Array<U32>, +s: U32, +d: U32) -> Array<U32> & Array<U32>:
118 copy.dst(U32.is_eq((d .&. 3 : U32), 0), m, src, dst, s, d)
119
120# n zero bytes.
121def new(+n: U32) -> Bytes:
122 Bytes{n, alloc(n)}
123
124def length(b: Bytes) -> Bytes & U32:
125 Bytes{+len, buf} = b
126 (Bytes{len, buf}, len)
127
128def get.some(+len: U32, r: Array<U32> & U32) -> Bytes & Maybe<&2, U32>:
129 (a, v) = r
130 (Bytes{len, a}, Some{v})
131
132def get.if(ok: Bool, +len: U32, buf: Array<U32>, +i: U32) -> Bytes & Maybe<&2, U32>:
133 match ok:
134 case True{}:
135 get.some(len, peek(buf, i))
136 case False{}:
137 (Bytes{len, buf}, None{})
138
139# Byte i, or None when i >= len.
140def get(b: Bytes, +i: U32) -> Bytes & Maybe<&2, U32>:
141 Bytes{+len, buf} = b
142 get.if(U32.is_lt(i, len), len, buf, i)
143
144def set.if(ok: Bool, +len: U32, buf: Array<U32>, +i: U32, +v: U32) -> Bytes:
145 match ok:
146 case True{}:
147 Bytes{len, poke(buf, i, v)}
148 case False{}:
149 Bytes{len, buf}
150
151# Byte i becomes v & 255. Nothing changes when i >= len.
152def set(b: Bytes, +i: U32, +v: U32) -> Bytes:
153 Bytes{+len, buf} = b
154 set.if(U32.is_lt(i, len), len, buf, i, v)
155
156# The next index: one forward when up, one back when not.
157def step(+up: Bool, +i: U32) -> U32:
158 Bool.pick(U32, up, (i + 1 : U32), (i - 1 : U32))
159
160# Do n bytes from i fit in len?
161def fits(+len: U32, +i: U32, +n: U32) -> Bool:
162 Bool.and(U32.is_le(n, len), U32.is_le(i, (len - n : U32)))
163
164# n bytes from j, each shifted in below the ones before: the first byte read is the most significant.
165def uint.go(n: Nat, r: Array<U32> & U32, +j: U32, +up: Bool, +acc: U32) -> Array<U32> & U32:
166 match n:
167 case 0n:
168 (a, v) = r
169 (a, acc)
170 case 1n+p:
171 (a, +v) = r
172 uint.go(p, peek(a, step(up, j)), step(up, j), up, ((acc << 8n) .|. v : U32))
173
174# Big-endian reads forward from i; little-endian reads back from the last byte.
175def uint.if(ok: Bool, +len: U32, buf: Array<U32>, +i: U32, +n: U32, +be: Bool) -> Bytes & Maybe<&2, U32>:
176 match ok:
177 case True{}:
178 +j = Bool.pick(U32, be, i, (i + n - 1 : U32))
179 get.some(len, uint.go(U32.to_nat(n), peek(buf, j), j, be, 0))
180 case False{}:
181 (Bytes{len, buf}, None{})
182
183def uint(b: Bytes, +i: U32, +n: U32, +be: Bool) -> Bytes & Maybe<&2, U32>:
184 Bytes{+len, buf} = b
185 uint.if(fits(len, i, n), len, buf, i, n, be)
186
187# Unsigned integers at byte i, or None when they run past len.
188# be: most significant byte first (network order); le: least significant first.
189def get.u16be(b: Bytes, +i: U32) -> Bytes & Maybe<&2, U32>:
190 uint(b, i, 2, True{})
191
192def get.u16le(b: Bytes, +i: U32) -> Bytes & Maybe<&2, U32>:
193 uint(b, i, 2, False{})
194
195def get.u32be(b: Bytes, +i: U32) -> Bytes & Maybe<&2, U32>:
196 uint(b, i, 4, True{})
197
198def get.u32le(b: Bytes, +i: U32) -> Bytes & Maybe<&2, U32>:
199 uint(b, i, 4, False{})
200
201# n bytes of v from j, least significant first.
202def put.go(n: Nat, a: Array<U32>, +j: U32, +up: Bool, +v: U32) -> Array<U32>:
203 match n:
204 case 0n:
205 a
206 case 1n+p:
207 put.go(p, poke(a, j, v), step(up, j), up, U32.shrn(v, 8n))
208
209# Little-endian writes forward from i; big-endian writes back from the last byte.
210def put.if(ok: Bool, +len: U32, buf: Array<U32>, +i: U32, +n: U32, +be: Bool, +v: U32) -> Bytes:
211 match ok:
212 case True{}:
213 Bytes{len, put.go(U32.to_nat(n), buf, Bool.pick(U32, be, (i + n - 1 : U32), i), Bool.not(be), v)}
214 case False{}:
215 Bytes{len, buf}
216
217def put(b: Bytes, +i: U32, +n: U32, +be: Bool, +v: U32) -> Bytes:
218 Bytes{+len, buf} = b
219 put.if(fits(len, i, n), len, buf, i, n, be, v)
220
221# v's low 16 or 32 bits at byte i. Nothing changes when they would run past len.
222def set.u16be(b: Bytes, +i: U32, +v: U32) -> Bytes:
223 put(b, i, 2, True{}, v)
224
225def set.u16le(b: Bytes, +i: U32, +v: U32) -> Bytes:
226 put(b, i, 2, False{}, v)
227
228def set.u32be(b: Bytes, +i: U32, +v: U32) -> Bytes:
229 put(b, i, 4, True{}, v)
230
231def set.u32le(b: Bytes, +i: U32, +v: U32) -> Bytes:
232 put(b, i, 4, False{}, v)
233
234# String.length counts in Nat, which costs more than the walk itself.
235def count(s: String, +n: U32) -> U32:
236 match s:
237 case SNil{}:
238 n
239 case SCon{c, t}:
240 count(t, (n + 1 : U32))
241
242# Bytes enter at the top of w and shift down, so a full word has byte 0 lowest.
243def flush(full: Bool, a: Array<U32>, +k: U32, +w: U32) -> Array<U32>:
244 match full:
245 case True{}:
246 Array.set(U32, a, k, w)
247 case False{}:
248 a
249
250def from.go(s: String, a: Array<U32>, +i: U32, +w: U32) -> Array<U32>:
251 match s:
252 case SNil{}:
253 +r = (i .&. 3 : U32)
254 flush(U32.is_ne(r, 0), a, (i >> 2n : U32), U32.shrn(w, U32.to_nat((((4 - r) .&. 3) * 8 : U32))))
255 case SCon{Chr{+c}, t}:
256 +w2 = ((w >> 8n) .|. (b8(c) << 24n) : U32)
257 +full = U32.is_eq((i .&. 3 : U32), 3)
258 from.go(t, flush(full, a, (i >> 2n : U32), w2), (i + 1 : U32), Bool.pick(U32, full, 0, w2))
259
260# A byte string (one Char per octet, as Wire and Http use) to Bytes. Each Char keeps its low 8 bits.
261def from_string(+s: String) -> Bytes:
262 +n = count(s, 0)
263 Bytes{n, from.go(s, alloc(n), 0, 0)}
264
265def to.go(n: Nat, r: Array<U32> & U32, +i: U32, acc: String) -> String:
266 match n:
267 case 0n:
268 acc
269 case 1n+p:
270 (a, v) = r
271 to.go(p, peek(a, (i - 1 : U32)), (i - 1 : U32), SCon{Chr{v}, acc})
272
273# Bytes to a byte string, one Char per octet.
274def to_string(b: Bytes) -> String:
275 Bytes{+len, buf} = b
276 to.go(U32.to_nat(len), peek(buf, (len - 1 : U32)), (len - 1 : U32), SNil{})
277
278def slice.fin(+len: U32, +m: U32, r: Array<U32> & Array<U32>) -> Bytes & Bytes:
279 (a, c) = r
280 (Bytes{len, a}, Bytes{m, c})
281
282def slice.at(+len: U32, buf: Array<U32>, +s: U32, +m: U32) -> Bytes & Bytes:
283 slice.fin(len, m, copy(m, buf, alloc(m), s, 0))
284
285# The buffer back, and a copy of up to n bytes from start. Both ends are clamped to len.
286def slice(b: Bytes, +start: U32, +n: U32) -> Bytes & Bytes:
287 Bytes{+len, buf} = b
288 +s = U32.min(start, len)
289 slice.at(len, buf, s, U32.min(n, (len - s : U32)))
290
291def dst(r: Array<U32> & Array<U32>) -> Array<U32>:
292 (src, out) = r
293 out
294
295# Does a buffer holding len bytes have room for n? Its 2^d words fit the fewest that hold len.
296def room(+len: U32, +n: U32) -> Bool:
297 U32.is_le(words(n), U32.shln(1, depth(words(len))))
298
299def grow.if(fits: Bool, +len: U32, buf: Array<U32>, +n: U32) -> Array<U32>:
300 match fits:
301 case True{}:
302 buf
303 case False{}:
304 dst(copy(len, buf, alloc(n), 0, 0))
305
306# buf, or a copy of its first len bytes in the fewest 2^d words that hold n.
307def grow(+len: U32, buf: Array<U32>, +n: U32) -> Array<U32>:
308 grow.if(room(len, n), len, buf, n)
309
310# a then b. b is written into a's buffer while it has room, and the buffer at least
311# doubles when it runs out, so building a buffer one piece at a time is O(total).
312def append(a: Bytes, b: Bytes) -> Bytes:
313 Bytes{+la, ba} = a
314 Bytes{+lb, bb} = b
315 +n = (la + lb : U32)
316 Bytes{n, dst(copy(lb, bb, grow(la, ba, n), 0, la))}
317
318def concat.total.con(x: Bytes, r: List<&1, Bytes> & U32) -> List<&1, Bytes> & U32:
319 (t, n) = r
320 (Con{x, t}, n)
321
322def concat.total(xs: List<&1, Bytes>, +n: U32) -> List<&1, Bytes> & U32:
323 match xs:
324 case Nil{}:
325 (Nil{}, n)
326 case Con{x, t}:
327 Bytes{+l, buf} = x
328 concat.total.con(Bytes{l, buf}, concat.total(t, (n + l : U32)))
329
330def concat.go(xs: List<&1, Bytes>, out: Array<U32>, +at: U32) -> Array<U32>:
331 match xs:
332 case Nil{}:
333 out
334 case Con{x, t}:
335 Bytes{+l, buf} = x
336 concat.go(t, dst(copy(l, buf, out, 0, at)), (at + l : U32))
337
338def concat.of(r: List<&1, Bytes> & U32) -> Bytes:
339 (xs, +n) = r
340 Bytes{n, concat.go(xs, alloc(n), 0)}
341
342# The pieces in order, in one new buffer: one copy per byte, however many pieces.
343def concat(xs: List<&1, Bytes>) -> Bytes:
344 concat.of(concat.total(xs, 0))
345
346# Does needle match at j? ok is the previous byte's result; the first mismatch stops the walk.
347def at.go(needle: String, ok: Bool, r: Array<U32> & U32, +j: U32) -> Array<U32> & Bool:
348 match needle:
349 case SNil{}:
350 (a, v) = r
351 (a, ok)
352 case SCon{Chr{+c}, t}:
353 match ok:
354 case False{}:
355 (a, v) = r
356 (a, False{})
357 case True{}:
358 (a, +v) = r
359 at.go(t, U32.is_eq(v, c), peek(a, (j + 1 : U32)), (j + 1 : U32))
360
361def at(a: Array<U32>, +needle: String, +j: U32) -> Array<U32> & Bool:
362 at.go(needle, True{}, peek(a, j), j)
363
364# 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.
365# f counts the positions left after i.
366def find.go(f: Nat, r: Array<U32> & Bool, +needle: String, +i: U32, +up: Bool) -> Array<U32> & Maybe<&2, U32>:
367 match f:
368 case 0n:
369 (a, hit) = r
370 (a, Bool.pick(Maybe<&2, U32>, hit, Some{i}, None{}))
371 case 1n+p:
372 (a, hit) = r
373 match hit:
374 case True{}:
375 (a, Some{i})
376 case False{}:
377 find.go(p, at(a, needle, step(up, i)), needle, step(up, i), up)
378
379def find.fin(+len: U32, r: Array<U32> & Maybe<&2, U32>) -> Bytes & Maybe<&2, U32>:
380 (a, x) = r
381 (Bytes{len, a}, x)
382
383def find.at(none: Bool, +len: U32, buf: Array<U32>, +needle: String, +i: U32, +f: U32, +up: Bool) -> Bytes & Maybe<&2, U32>:
384 match none:
385 case True{}:
386 (Bytes{len, buf}, None{})
387 case False{}:
388 find.fin(len, find.go(U32.to_nat(f), at(buf, needle, i), needle, i, up))
389
390# Index of the first match of needle (a byte string) at or after start, or None.
391# An empty needle matches at start when start <= len.
392def find.from(b: Bytes, +needle: String, +start: U32) -> Bytes & Maybe<&2, U32>:
393 Bytes{+len, buf} = b
394 +m = count(needle, 0)
395 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{})
396
397# Index of the first match of needle (a byte string), or None. An empty needle matches at 0.
398def find(b: Bytes, +needle: String) -> Bytes & Maybe<&2, U32>:
399 find.from(b, needle, 0)
400
401# Index of the last match of needle, or None. An empty needle matches at len.
402def rfind(b: Bytes, +needle: String) -> Bytes & Maybe<&2, U32>:
403 Bytes{+len, buf} = b
404 +m = count(needle, 0)
405 find.at(U32.is_lt(len, m), len, buf, needle, (len - m : U32), (len - m : U32), False{})
406
407def at.fin(+len: U32, r: Array<U32> & Bool) -> Bytes & Bool:
408 (a, ok) = r
409 (Bytes{len, a}, ok)
410
411def at.if(fits: Bool, +len: U32, buf: Array<U32>, +needle: String, +j: U32) -> Bytes & Bool:
412 match fits:
413 case True{}:
414 at.fin(len, at(buf, needle, j))
415 case False{}:
416 (Bytes{len, buf}, False{})
417
418# Does b begin with prefix (a byte string)?
419def starts_with(b: Bytes, +prefix: String) -> Bytes & Bool:
420 Bytes{+len, buf} = b
421 +m = count(prefix, 0)
422 at.if(U32.is_le(m, len), len, buf, prefix, 0)
423
424# Does b end with suffix (a byte string)?
425def ends_with(b: Bytes, +suffix: String) -> Bytes & Bool:
426 Bytes{+len, buf} = b
427 +m = count(suffix, 0)
428 at.if(U32.is_le(m, len), len, buf, suffix, (len - m : U32))
429
430# Match positions of sep, latest first, that do not overlap an earlier match.
431# f counts the positions left; skip counts the bytes still inside the last match.
432def 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>:
433 match f:
434 case 0n:
435 (a, hit) = r
436 (a, cuts)
437 case 1n+p:
438 (a, +hit) = r
439 +take = Bool.and(hit, U32.is_eq(skip, 0))
440 +next = Bool.pick(U32, take, (m - 1 : U32), Bool.pick(U32, U32.is_eq(skip, 0), 0, (skip - 1 : U32)))
441 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))
442
443def snd(r: Bytes & Bytes) -> Bytes:
444 (a, b) = r
445 b
446
447# r holds the buffer and the piece that ends at end; each earlier cut j starts one at j + m.
448def split.cut(cuts: List<&2, U32>, r: Bytes & Bytes, +end: U32, +m: U32, acc: List<&1, Bytes>) -> List<&1, Bytes>:
449 match cuts:
450 case Nil{}:
451 (b, piece) = r
452 Con{snd(slice(b, 0, end)), Con{piece, acc}}
453 case Con{+j, t}:
454 (b, piece) = r
455 split.cut(t, slice(b, (j + m : U32), (end - j - m : U32)), j, m, Con{piece, acc})
456
457def split.of(cuts: List<&2, U32>, b: Bytes, +len: U32, +m: U32) -> List<&1, Bytes>:
458 match cuts:
459 case Nil{}:
460 Con{b, Nil{}}
461 case Con{+j, t}:
462 split.cut(t, slice(b, (j + m : U32), (len - j - m : U32)), j, m, Nil{})
463
464def split.run(+len: U32, +m: U32, r: Array<U32> & List<&2, U32>) -> List<&1, Bytes>:
465 (a, cuts) = r
466 split.of(cuts, Bytes{len, a}, len, m)
467
468def split.if(whole: Bool, +len: U32, buf: Array<U32>, +sep: String, +m: U32) -> List<&1, Bytes>:
469 match whole:
470 case True{}:
471 Con{Bytes{len, buf}, Nil{}}
472 case False{}:
473 split.run(len, m, split.scan(U32.to_nat((len - m + 1 : U32)), at(buf, sep, 0), sep, m, 0, 0, Nil{}))
474
475# The pieces between matches of sep (a byte string), left to right. n matches give n + 1
476# pieces, so a match at either end gives an empty piece. An empty sep gives b whole.
477def split(b: Bytes, +sep: String) -> List<&1, Bytes>:
478 Bytes{+len, buf} = b
479 +m = count(sep, 0)
480 split.if(Bool.or(U32.is_eq(m, 0), U32.is_lt(len, m)), len, buf, sep, m)
481
482# Compares whole words; same tells whether the previous pair matched.
483def eq.go(n: Nat, same: Bool, r: Array<U32> & U32, s: Array<U32> & U32, +i: U32) -> Array<U32> & Array<U32> & Bool:
484 match n:
485 case 0n:
486 (x, v) = r
487 (y, w) = s
488 (x, y, same)
489 case 1n+p:
490 match same:
491 case False{}:
492 (x, v) = r
493 (y, w) = s
494 (x, y, False{})
495 case True{}:
496 (x, +v) = r
497 (y, +w) = s
498 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))
499
500def eq.fin(+la: U32, +lb: U32, r: Array<U32> & Array<U32> & Bool) -> Bytes & Bytes & Bool:
501 (x, y, ok) = r
502 (Bytes{la, x}, Bytes{lb, y}, ok)
503
504def eq.len(same: Bool, +la: U32, xa: Array<U32>, +lb: U32, ya: Array<U32>) -> Bytes & Bytes & Bool:
505 match same:
506 case False{}:
507 (Bytes{la, xa}, Bytes{lb, ya}, False{})
508 case True{}:
509 eq.fin(la, lb, eq.go(U32.to_nat(words(la)), True{}, Array.get(U32, xa, 0), Array.get(U32, ya, 0), 0))
510
511# Both buffers back, and whether they hold the same bytes.
512def eq(a: Bytes, b: Bytes) -> Bytes & Bytes & Bool:
513 Bytes{+la, xa} = a
514 Bytes{+lb, ya} = b
515 eq.len(U32.is_eq(la, lb), la, xa, lb, ya)
516
517# Byte 0 of w becomes the most significant, so words compare in byte order.
518def bswap(+w: U32) -> U32:
519 ((b8(w) << 24n) .|. (b8(U32.shrn(w, 8n)) << 16n) .|. (b8(U32.shrn(w, 16n)) << 8n) .|. U32.shrn(w, 24n) : U32)
520
521# Compares whole words; c is the previous pair's order.
522def cmp.go(n: Nat, c: Cmp, r: Array<U32> & U32, s: Array<U32> & U32, +i: U32) -> Array<U32> & Array<U32> & Cmp:
523 match n:
524 case 0n:
525 (x, v) = r
526 (y, w) = s
527 (x, y, c)
528 case 1n+p:
529 match c:
530 case LT{}:
531 (x, v) = r
532 (y, w) = s
533 (x, y, LT{})
534 case GT{}:
535 (x, v) = r
536 (y, w) = s
537 (x, y, GT{})
538 case EQ{}:
539 (x, +v) = r
540 (y, +w) = s
541 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))
542
543def cmp.len(c: Cmp, +la: U32, +lb: U32) -> Cmp:
544 match c:
545 case EQ{}:
546 U32.cmp(la, lb)
547 case LT{}:
548 LT{}
549 case GT{}:
550 GT{}
551
552def cmp.fin(+la: U32, +lb: U32, r: Array<U32> & Array<U32> & Cmp) -> Bytes & Bytes & Cmp:
553 (x, y, c) = r
554 (Bytes{la, x}, Bytes{lb, y}, cmp.len(c, la, lb))
555
556# Both buffers back, and their order byte by byte; a prefix sorts first.
557# The shorter buffer's bytes past its len are 0, so its last word compares low when only the longer one goes on.
558def cmp(a: Bytes, b: Bytes) -> Bytes & Bytes & Cmp:
559 Bytes{+la, xa} = a
560 Bytes{+lb, ya} = b
561 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))
562
563def nibble(+n: U32) -> Char:
564 Chr{Bool.pick(U32, U32.is_lt(n, 10), (48 + n : U32), (87 + n : U32))}
565
566def hex.go(n: Nat, r: Array<U32> & U32, +i: U32, acc: String) -> String:
567 match n:
568 case 0n:
569 acc
570 case 1n+p:
571 (a, +v) = r
572 hex.go(p, peek(a, (i - 1 : U32)), (i - 1 : U32), SCon{nibble(U32.shrn(v, 4n)), SCon{nibble((v .&. 15 : U32)), acc}})
573
574# Two lowercase hex digits per byte.
575def to_hex(b: Bytes) -> String:
576 Bytes{+len, buf} = b
577 hex.go(U32.to_nat(len), peek(buf, (len - 1 : U32)), (len - 1 : U32), SNil{})
578
579def in(+lo: U32, +c: U32, +hi: U32) -> Bool:
580 Bool.and(U32.is_le(lo, c), U32.is_le(c, hi))
581
582# A hex digit's value, or 16.
583def unnibble(+c: U32) -> U32:
584 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)))
585
586def poke.when(write: Bool, a: Array<U32>, +i: U32, +v: U32) -> Array<U32>:
587 match write:
588 case True{}:
589 poke(a, i, v)
590 case False{}:
591 a
592
593# hi is the previous digit; an odd i completes a byte.
594def unhex.go(s: String, a: Array<U32>, +i: U32, +hi: U32, +ok: Bool) -> Array<U32> & Bool:
595 match s:
596 case SNil{}:
597 (a, ok)
598 case SCon{Chr{+c}, t}:
599 +d = unnibble(c)
600 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)))
601
602def decoded(+n: U32, r: Array<U32> & Bool) -> Maybe<&1, Bytes>:
603 (a, ok) = r
604 match ok:
605 case True{}:
606 Some{Bytes{n, a}}
607 case False{}:
608 None{}
609
610def unhex.if(even: Bool, +s: String, +n: U32) -> Maybe<&1, Bytes>:
611 match even:
612 case True{}:
613 decoded((n >> 1n : U32), unhex.go(s, alloc((n >> 1n : U32)), 0, 0, True{}))
614 case False{}:
615 None{}
616
617# Hex digits, either case, to bytes. None for an odd count or a non-hex char.
618def from_hex(+s: String) -> Maybe<&1, Bytes>:
619 +n = count(s, 0)
620 unhex.if(U32.is_eq((n .&. 1 : U32), 0), s, n)
621
622# RFC 4648 §4: the standard alphabet, padded with '='.
623def b64.char(+i: U32) -> U32:
624 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))))
625
626# The six bits of v at k as a base64 char.
627def b64.at(+v: U32, +k: Nat) -> Char:
628 Chr{b64.char((U32.shrn(v, k) .&. 63 : U32))}
629
630# Groups of three bytes, last first; r holds the 24 bits of the group at i.
631def b64.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 +j = (i - 3 : U32)
638 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}}}})
639
640# The rem < 3 bytes after the last whole group, then the groups before them.
641def b64.tail(+rem: U32, +t: U32, +q: U32, r: Array<U32> & U32) -> String:
642 (a, +v0) = r
643 +v = U32.shln(v0, U32.to_nat(((3 - rem) * 8 : U32)))
644 +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), "="}}}))
645 +j = (t - 3 : U32)
646 b64.go(U32.to_nat(q), uint.go(3n, peek(a, j), j, True{}, 0), j, end)
647
648# Base64 (RFC 4648 §4) with '=' padding.
649def to_base64(b: Bytes) -> String:
650 Bytes{+len, buf} = b
651 +q = (len / 3 : U32)
652 +t = (q * 3 : U32)
653 b64.tail((len - t : U32), t, q, uint.go(U32.to_nat((len - t : U32)), peek(buf, t), t, True{}, 0))
654
655# A base64 char's value, 64 for '=', or 65.
656def b64.val(+c: U32) -> U32:
657 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))))))
658
659# The count of '=' at the end of s.
660def b64.pads(s: String, +run: U32) -> U32:
661 match s:
662 case SNil{}:
663 run
664 case SCon{Chr{+c}, t}:
665 b64.pads(t, Bool.pick(U32, U32.is_eq(c, 61), (run + 1 : U32), 0))
666
667# A whole group of four chars writes its bytes at o, as many as fit before len.
668def b64.put(full: Bool, a: Array<U32>, +o: U32, +w: U32, +v: U32) -> Array<U32>:
669 match full:
670 case True{}:
671 put.go(U32.to_nat(w), a, (o + w - 1 : U32), False{}, U32.shrn(v, U32.to_nat(((3 - w) * 8 : U32))))
672 case False{}:
673 a
674
675# v collects six bits per char. '=' is allowed only at body and after.
676def unb64.go(s: String, a: Array<U32>, +i: U32, +v: U32, +ok: Bool, +len: U32, +body: U32) -> Array<U32> & Bool:
677 match s:
678 case SNil{}:
679 (a, ok)
680 case SCon{Chr{+c}, t}:
681 +d = b64.val(c)
682 +v2 = ((v << 6n) .|. (d .&. 63) : U32)
683 +o = ((i >> 2n) * 3 : U32)
684 +good = Bool.pick(Bool, U32.is_lt(i, body), U32.is_lt(d, 64), U32.is_eq(d, 64))
685 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)
686
687def unb64.if(ok: Bool, +s: String, +n: U32, +pads: U32) -> Maybe<&1, Bytes>:
688 match ok:
689 case True{}:
690 +len = ((n >> 2n) * 3 - pads : U32)
691 decoded(len, unb64.go(s, alloc(len), 0, 0, True{}, len, (n - pads : U32)))
692 case False{}:
693 None{}
694
695# Padded base64 (RFC 4648 §4) to bytes. None for a length that is not a multiple of 4,
696# more than two '=', '=' before the end, or a char outside the alphabet.
697def from_base64(+s: String) -> Maybe<&1, Bytes>:
698 +n = count(s, 0)
699 +pads = b64.pads(s, 0)
700 unb64.if(Bool.and(U32.is_eq((n .&. 3 : U32), 0), U32.is_le(pads, 2)), s, n, pads)