1 # Byte buffers packed four bytes to a U32, with bounds-checked access. Source: https://github.com/paymog/bend-kit/tree/main/bytes 2 import 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 9 type Bytes is Type: 10 Bytes{len: U32, buf: Array} 11 12 def b8(+x: U32) -> U32: 13 (x .&. 255 : U32) 14 15 def shift(+i: U32) -> Nat: 16 U32.to_nat(((i .&. 3 : U32) * 8 : U32)) 17 18 def words(+n: U32) -> U32: 19 ((n + 3 : U32) >> 2n : U32) 20 21 # The fewest d with 2^d >= w. 22 def 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 33 def depth(+w: U32) -> Nat: 34 depth.go(32n, U32.is_lt(1, w), w, 0n, 1) 35 36 def alloc(+n: U32) -> Array: 37 Array.new(U32, depth(words(n)), 0) 38 39 # Unchecked byte read and write. Callers keep i below len. 40 def peek.of(+sh: Nat, r: Array & U32) -> Array & U32: 41 (a, w) = r 42 (a, b8(U32.shrn(w, sh))) 43 44 def peek(a: Array, +i: U32) -> Array & U32: 45 peek.of(shift(i), Array.get(U32, a, (i >> 2n : U32))) 46 47 def poke.of(+i: U32, +v: U32, r: Array & U32) -> Array: 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 52 def poke(a: Array, +i: U32, +v: U32) -> Array: 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. 56 def copy.go(n: Nat, r: Array & U32, dst: Array, +s: U32, +d: U32) -> Array & Array: 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 65 def copy.bytes(+m: U32, src: Array, dst: Array, +s: U32, +d: U32) -> Array & Array: 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). 69 def copy.words(n: Nat, r: Array & U32, dst: Array, +s: U32, +d: U32) -> Array & Array: 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. 80 def copy.shift(n: Nat, +lo: Nat, +hi: Nat, +prev: U32, r: Array & U32, dst: Array, +k: U32, +d: U32) -> Array & Array: 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 89 def copy.shift.at(+w: U32, +lo: U32, +k: U32, +d: U32, r: Array & U32, dst: Array) -> Array & Array: 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 93 def copy.tail(+m: U32, +s: U32, +d: U32, r: Array & Array) -> Array & Array: 94 (a, b) = r 95 copy.bytes(m, a, b, s, d) 96 97 def copy.pick(aligned: Bool, +m: U32, src: Array, dst: Array, +s: U32, +d: U32) -> Array & Array: 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 108 def copy.dst(daligned: Bool, +m: U32, src: Array, dst: Array, +s: U32, +d: U32) -> Array & Array: 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. 117 def copy(+m: U32, src: Array, dst: Array, +s: U32, +d: U32) -> Array & Array: 118 copy.dst(U32.is_eq((d .&. 3 : U32), 0), m, src, dst, s, d) 119 120 # n zero bytes. 121 def new(+n: U32) -> Bytes: 122 Bytes{n, alloc(n)} 123 124 def length(b: Bytes) -> Bytes & U32: 125 Bytes{+len, buf} = b 126 (Bytes{len, buf}, len) 127 128 def get.some(+len: U32, r: Array & U32) -> Bytes & Maybe<&2, U32>: 129 (a, v) = r 130 (Bytes{len, a}, Some{v}) 131 132 def get.if(ok: Bool, +len: U32, buf: Array, +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. 140 def 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 144 def set.if(ok: Bool, +len: U32, buf: Array, +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. 152 def 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. 157 def 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? 161 def 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. 165 def uint.go(n: Nat, r: Array & U32, +j: U32, +up: Bool, +acc: U32) -> Array & 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. 175 def uint.if(ok: Bool, +len: U32, buf: Array, +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 183 def 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. 189 def get.u16be(b: Bytes, +i: U32) -> Bytes & Maybe<&2, U32>: 190 uint(b, i, 2, True{}) 191 192 def get.u16le(b: Bytes, +i: U32) -> Bytes & Maybe<&2, U32>: 193 uint(b, i, 2, False{}) 194 195 def get.u32be(b: Bytes, +i: U32) -> Bytes & Maybe<&2, U32>: 196 uint(b, i, 4, True{}) 197 198 def 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. 202 def put.go(n: Nat, a: Array, +j: U32, +up: Bool, +v: U32) -> Array: 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. 210 def put.if(ok: Bool, +len: U32, buf: Array, +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 217 def 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. 222 def set.u16be(b: Bytes, +i: U32, +v: U32) -> Bytes: 223 put(b, i, 2, True{}, v) 224 225 def set.u16le(b: Bytes, +i: U32, +v: U32) -> Bytes: 226 put(b, i, 2, False{}, v) 227 228 def set.u32be(b: Bytes, +i: U32, +v: U32) -> Bytes: 229 put(b, i, 4, True{}, v) 230 231 def 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. 235 def 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. 243 def flush(full: Bool, a: Array, +k: U32, +w: U32) -> Array: 244 match full: 245 case True{}: 246 Array.set(U32, a, k, w) 247 case False{}: 248 a 249 250 def from.go(s: String, a: Array, +i: U32, +w: U32) -> Array: 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. 261 def from_string(+s: String) -> Bytes: 262 +n = count(s, 0) 263 Bytes{n, from.go(s, alloc(n), 0, 0)} 264 265 def to.go(n: Nat, r: Array & 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. 274 def 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 278 def slice.fin(+len: U32, +m: U32, r: Array & Array) -> Bytes & Bytes: 279 (a, c) = r 280 (Bytes{len, a}, Bytes{m, c}) 281 282 def slice.at(+len: U32, buf: Array, +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. 286 def 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 291 def dst(r: Array & Array) -> Array: 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. 296 def room(+len: U32, +n: U32) -> Bool: 297 U32.is_le(words(n), U32.shln(1, depth(words(len)))) 298 299 def grow.if(fits: Bool, +len: U32, buf: Array, +n: U32) -> Array: 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. 307 def grow(+len: U32, buf: Array, +n: U32) -> Array: 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). 312 def 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 318 def concat.total.con(x: Bytes, r: List<&1, Bytes> & U32) -> List<&1, Bytes> & U32: 319 (t, n) = r 320 (Con{x, t}, n) 321 322 def 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 330 def concat.go(xs: List<&1, Bytes>, out: Array, +at: U32) -> Array: 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 338 def 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. 343 def 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. 347 def at.go(needle: String, ok: Bool, r: Array & U32, +j: U32) -> Array & 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 361 def at(a: Array, +needle: String, +j: U32) -> Array & 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. 366 def find.go(f: Nat, r: Array & Bool, +needle: String, +i: U32, +up: Bool) -> Array & 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 379 def find.fin(+len: U32, r: Array & Maybe<&2, U32>) -> Bytes & Maybe<&2, U32>: 380 (a, x) = r 381 (Bytes{len, a}, x) 382 383 def find.at(none: Bool, +len: U32, buf: Array, +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. 392 def 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. 398 def 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. 402 def 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 407 def at.fin(+len: U32, r: Array & Bool) -> Bytes & Bool: 408 (a, ok) = r 409 (Bytes{len, a}, ok) 410 411 def at.if(fits: Bool, +len: U32, buf: Array, +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)? 419 def 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)? 425 def 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. 432 def split.scan(f: Nat, r: Array & Bool, +sep: String, +m: U32, +i: U32, +skip: U32, +cuts: List<&2, U32>) -> Array & 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 443 def 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. 448 def 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 457 def 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 464 def split.run(+len: U32, +m: U32, r: Array & List<&2, U32>) -> List<&1, Bytes>: 465 (a, cuts) = r 466 split.of(cuts, Bytes{len, a}, len, m) 467 468 def split.if(whole: Bool, +len: U32, buf: Array, +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. 477 def 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. 483 def eq.go(n: Nat, same: Bool, r: Array & U32, s: Array & U32, +i: U32) -> Array & Array & 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 500 def eq.fin(+la: U32, +lb: U32, r: Array & Array & Bool) -> Bytes & Bytes & Bool: 501 (x, y, ok) = r 502 (Bytes{la, x}, Bytes{lb, y}, ok) 503 504 def eq.len(same: Bool, +la: U32, xa: Array, +lb: U32, ya: Array) -> 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. 512 def 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. 518 def 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. 522 def cmp.go(n: Nat, c: Cmp, r: Array & U32, s: Array & U32, +i: U32) -> Array & Array & 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 543 def 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 552 def cmp.fin(+la: U32, +lb: U32, r: Array & Array & 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. 558 def 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 563 def nibble(+n: U32) -> Char: 564 Chr{Bool.pick(U32, U32.is_lt(n, 10), (48 + n : U32), (87 + n : U32))} 565 566 def hex.go(n: Nat, r: Array & 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. 575 def 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 579 def 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. 583 def 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 586 def poke.when(write: Bool, a: Array, +i: U32, +v: U32) -> Array: 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. 594 def unhex.go(s: String, a: Array, +i: U32, +hi: U32, +ok: Bool) -> Array & 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 602 def decoded(+n: U32, r: Array & 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 610 def 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. 618 def 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 '='. 623 def 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. 627 def 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. 631 def b64.go(n: Nat, r: Array & 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. 641 def b64.tail(+rem: U32, +t: U32, +q: U32, r: Array & 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. 649 def 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. 656 def 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. 660 def 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. 668 def b64.put(full: Bool, a: Array, +o: U32, +w: U32, +v: U32) -> Array: 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. 676 def unb64.go(s: String, a: Array, +i: U32, +v: U32, +ok: Bool, +len: U32, +body: U32) -> Array & 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 687 def 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. 697 def 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)