bytes.bend
bend-osdev-bytes@0.1.0.0 · 696 lines · 0 definitions
1# bend-osdev-bytes: byte strings, and the fixed-width fields that formats store
2# in them.
3#
4# A byte string is a List<&2, U32> whose elements are 0 to 255 (the shape Base's
5# own I/O uses). Readers take the low 8 bits of each element, so a malformed
6# element is masked, never trusted.
7#
8# The field readers and writers work on bits (slicing and joining words), not
9# with shifts and masks, so that their round trips can be proved for every
10# value. That costs speed: use them for header fields, not bulk data.
11import Base
12import bend-osdev-word64@0.1.0.0/word64.bend as W
13
14# Bytes and bits
15
16# the low 8 bits of a word, as bits
17def bits8(b: U32) -> Word(8n):
18 match b:
19 case U32{w}:
20 W.W64.bits.lo(8n, 24n, w)
21
22# the byte (0 to 255) with these 8 bits
23def of_bits8(s: Word(8n)) -> U32:
24 U32{W.W64.bits.cat(8n, 24n, s, Word.zero(24n))}
25
26# One byte of an Octets: eight bits as one record, the low bit first. Every
27# value of the type is a byte (there is nothing to mask), and it is built
28# from a word's bits and back without branching, so proofs about symbolic
29# bytes compute through it. One record per byte costs about a quarter of the
30# memory of an 8-bit Word, which is a chain of eight cells.
31type OctByte is Data:
32 OctByte{b0: Bool, b1: Bool, b2: Bool, b3: Bool, b4: Bool, b5: Bool, b6: Bool, b7: Bool}
33
34# the low 8 bits of a word (the high 24 are never looked at)
35def oct.of(x: U32) -> OctByte:
36 match x:
37 case U32{WCon{c0, WCon{c1, WCon{c2, WCon{c3, WCon{c4, WCon{c5, WCon{c6, WCon{c7, hi}}}}}}}}}:
38 OctByte{c0, c1, c2, c3, c4, c5, c6, c7}
39
40# the byte as a word (0 to 255)
41def oct.to(b: OctByte) -> U32:
42 match b:
43 case OctByte{b0, b1, b2, b3, b4, b5, b6, b7}:
44 U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, Word.zero(24n)}}}}}}}}}
45
46def oct.zero() -> OctByte:
47 OctByte{False{}, False{}, False{}, False{}, False{}, False{}, False{}, False{}}
48
49# the byte of a word: its low 8 bits (through OctByte, so that a byte read
50# back from an Octets and byte(b) are the same term even for an unknown b)
51def byte(b: U32) -> U32:
52 oct.to(oct.of(b))
53
54# List operations
55
56def len(xs: List<&2, U32>) -> Nat:
57 List.length(&2, U32, xs)
58
59# the first n bytes (all of them if there are fewer)
60def take(n: Nat, xs: List<&2, U32>) -> List<&2, U32>:
61 match n:
62 case 0n:
63 Nil{}
64 case 1n+p:
65 match xs:
66 case Nil{}:
67 Nil{}
68 case Con{h, t}:
69 Con{h, take(p, t)}
70
71# all but the first n bytes
72def drop(n: Nat, xs: List<&2, U32>) -> List<&2, U32>:
73 match n:
74 case 0n:
75 xs
76 case 1n+p:
77 match xs:
78 case Nil{}:
79 Nil{}
80 case Con{h, t}:
81 drop(p, t)
82
83def append(a: List<&2, U32>, b: List<&2, U32>) -> List<&2, U32>:
84 List.append(&2, U32, a, b)
85
86# n zero bytes
87def zeros(n: Nat) -> List<&2, U32>:
88 match n:
89 case 0n:
90 Nil{}
91 case 1n+p:
92 Con{0, zeros(p)}
93
94# the byte at offset i, if there is one
95def at.head(xs: List<&2, U32>) -> Maybe<&2, U32>:
96 match xs:
97 case Con{h, t}:
98 Some{byte(h)}
99 case Nil{}:
100 None{}
101
102def at(xs: List<&2, U32>, i: Nat) -> Maybe<&2, U32>:
103 at.head(drop(i, xs))
104
105# Fields: writing (each answers its bytes, in storage order)
106
107# the low 16 bits of a word
108def low16(v: U32) -> U32:
109 match v:
110 case U32{w}:
111 U32{W.W64.bits.cat(16n, 16n, W.W64.bits.lo(16n, 16n, w), Word.zero(16n))}
112
113def le16(v: U32) -> List<&2, U32>:
114 match v:
115 case U32{w}:
116 +lo = W.W64.bits.lo(16n, 16n, w)
117 [of_bits8(W.W64.bits.lo(8n, 8n, lo)), of_bits8(W.W64.bits.hi(8n, 8n, lo))]
118
119def be16(v: U32) -> List<&2, U32>:
120 match v:
121 case U32{w}:
122 +lo = W.W64.bits.lo(16n, 16n, w)
123 [of_bits8(W.W64.bits.hi(8n, 8n, lo)), of_bits8(W.W64.bits.lo(8n, 8n, lo))]
124
125# the four bytes of a word, least significant first
126def le32(+v: U32) -> List<&2, U32>:
127 match v:
128 case U32{w}:
129 +r1 = W.W64.bits.hi(8n, 24n, w)
130 +r2 = W.W64.bits.hi(8n, 16n, r1)
131 [of_bits8(W.W64.bits.lo(8n, 24n, w)), of_bits8(W.W64.bits.lo(8n, 16n, r1)), of_bits8(W.W64.bits.lo(8n, 8n, r2)), of_bits8(W.W64.bits.hi(8n, 8n, r2))]
132
133def be32.rev(xs: List<&2, U32>) -> List<&2, U32>:
134 match xs:
135 case Con{a, Con{b, Con{c, Con{d, Nil{}}}}}:
136 [d, c, b, a]
137 case _:
138 Nil{}
139
140def be32(v: U32) -> List<&2, U32>:
141 be32.rev(le32(v))
142
143def le64(+v: W.W64) -> List<&2, U32>:
144 append(le32(W.W64.lo(v)), le32(W.W64.hi(v)))
145
146def be64(+v: W.W64) -> List<&2, U32>:
147 append(be32(W.W64.hi(v)), be32(W.W64.lo(v)))
148
149# Fields: reading at the head of a byte string
150
151def le16.head(xs: List<&2, U32>) -> Maybe<&2, U32>:
152 match xs:
153 case Con{a, Con{b, t}}:
154 Some{U32{W.W64.bits.cat(16n, 16n, W.W64.bits.cat(8n, 8n, bits8(a), bits8(b)), Word.zero(16n))}}
155 case _:
156 None{}
157
158def be16.head(xs: List<&2, U32>) -> Maybe<&2, U32>:
159 match xs:
160 case Con{a, Con{b, t}}:
161 Some{U32{W.W64.bits.cat(16n, 16n, W.W64.bits.cat(8n, 8n, bits8(b), bits8(a)), Word.zero(16n))}}
162 case _:
163 None{}
164
165def le32.head(xs: List<&2, U32>) -> Maybe<&2, U32>:
166 match xs:
167 case Con{a, Con{b, Con{c, Con{d, t}}}}:
168 Some{U32{W.W64.bits.cat(8n, 24n, bits8(a), W.W64.bits.cat(8n, 16n, bits8(b), W.W64.bits.cat(8n, 8n, bits8(c), bits8(d))))}}
169 case _:
170 None{}
171
172def be32.head(xs: List<&2, U32>) -> Maybe<&2, U32>:
173 match xs:
174 case Con{a, Con{b, Con{c, Con{d, t}}}}:
175 Some{U32{W.W64.bits.cat(8n, 24n, bits8(d), W.W64.bits.cat(8n, 16n, bits8(c), W.W64.bits.cat(8n, 8n, bits8(b), bits8(a))))}}
176 case _:
177 None{}
178
179def le64.join(lo: Maybe<&2, U32>, hi: Maybe<&2, U32>) -> Maybe<&2, W.W64>:
180 match lo hi:
181 case Some{l} Some{h}:
182 Some{W.W64.from_parts(h, l)}
183 case _ _:
184 None{}
185
186# Fields: reading at an offset (None if the string is too short)
187
188def le16_at(xs: List<&2, U32>, i: Nat) -> Maybe<&2, U32>:
189 le16.head(drop(i, xs))
190
191def be16_at(xs: List<&2, U32>, i: Nat) -> Maybe<&2, U32>:
192 be16.head(drop(i, xs))
193
194def le32_at(xs: List<&2, U32>, i: Nat) -> Maybe<&2, U32>:
195 le32.head(drop(i, xs))
196
197def be32_at(xs: List<&2, U32>, i: Nat) -> Maybe<&2, U32>:
198 be32.head(drop(i, xs))
199
200def le64_at(+xs: List<&2, U32>, +i: Nat) -> Maybe<&2, W.W64>:
201 le64.join(le32_at(xs, i), le32_at(xs, Nat.add(i, 4n)))
202
203def be64_at(+xs: List<&2, U32>, +i: Nat) -> Maybe<&2, W.W64>:
204 le64.join(be32_at(xs, Nat.add(i, 4n)), be32_at(xs, i))
205
206# Text
207
208def of_string(s: String) -> List<&2, U32>:
209 match s:
210 case SNil{}:
211 Nil{}
212 case SCon{Chr{c}, t}:
213 Con{byte(c), of_string(t)}
214
215def to_string(xs: List<&2, U32>) -> String:
216 match xs:
217 case Nil{}:
218 SNil{}
219 case Con{h, t}:
220 SCon{Chr{byte(h)}, to_string(t)}
221
222def hex.digit.pick(lt: Bool, d: U32) -> Char:
223 match lt:
224 case True{}:
225 Chr{U32.add(48, d)}
226 case False{}:
227 Chr{U32.add(87, d)}
228
229def hex.digit(+d: U32) -> Char:
230 hex.digit.pick(U32.is_lt(d, 10), d)
231
232# two lower-case hex digits per byte
233def hex(xs: List<&2, U32>) -> String:
234 match xs:
235 case Nil{}:
236 SNil{}
237 case Con{h, t}:
238 +b = byte(h)
239 SCon{hex.digit(U32.shrn(b, 4n)), SCon{hex.digit(U32.and(b, 15)), hex(t)}}
240
241# The list layer, tail-recursive. Bend 2.0.37's runtime overflows its stack
242# at some tens of thousands of nested non-tail calls, so the structural forms
243# above cannot run on long lists; these build their answer in an accumulator
244# (reversed where order matters). Each is proved equal to its structural form
245# for every input (LAWS.bend: *_fast), so code can run these while proofs
246# reason about the structural forms.
247
248def rev_onto(xs: List<&2, U32>, acc: List<&2, U32>) -> List<&2, U32>:
249 match xs:
250 case Nil{}:
251 acc
252 case Con{h, t}:
253 rev_onto(t, Con{h, acc})
254
255def rev(xs: List<&2, U32>) -> List<&2, U32>:
256 rev_onto(xs, Nil{})
257
258def len.go(xs: List<&2, U32>, n: Nat) -> Nat:
259 match xs:
260 case Nil{}:
261 n
262 case Con{h, t}:
263 len.go(t, 1n+n)
264
265def len.fast(xs: List<&2, U32>) -> Nat:
266 len.go(xs, 0n)
267
268def take.go(n: Nat, xs: List<&2, U32>, acc: List<&2, U32>) -> List<&2, U32>:
269 match n:
270 case 0n:
271 acc
272 case 1n+p:
273 match xs:
274 case Nil{}:
275 acc
276 case Con{h, t}:
277 take.go(p, t, Con{h, acc})
278
279def take.fast(n: Nat, xs: List<&2, U32>) -> List<&2, U32>:
280 rev(take.go(n, xs, Nil{}))
281
282def append.fast(xs: List<&2, U32>, ys: List<&2, U32>) -> List<&2, U32>:
283 rev_onto(rev(xs), ys)
284
285def zeros.go(n: Nat, acc: List<&2, U32>) -> List<&2, U32>:
286 match n:
287 case 0n:
288 acc
289 case 1n+p:
290 zeros.go(p, Con{0, acc})
291
292def zeros.fast(n: Nat) -> List<&2, U32>:
293 zeros.go(n, Nil{})
294
295def of_string.go(s: String, acc: List<&2, U32>) -> List<&2, U32>:
296 match s:
297 case SNil{}:
298 acc
299 case SCon{Chr{c}, t}:
300 of_string.go(t, Con{byte(c), acc})
301
302def of_string.fast(s: String) -> List<&2, U32>:
303 rev(of_string.go(s, Nil{}))
304
305# the string of xs's bytes in front of acc (structural; the laws' form)
306def to_string.cat(xs: List<&2, U32>, acc: String) -> String:
307 match xs:
308 case Nil{}:
309 acc
310 case Con{h, t}:
311 SCon{Chr{byte(h)}, to_string.cat(t, acc)}
312
313def to_string.go(rs: List<&2, U32>, acc: String) -> String:
314 match rs:
315 case Nil{}:
316 acc
317 case Con{h, t}:
318 to_string.go(t, SCon{Chr{byte(h)}, acc})
319
320def to_string.fast(xs: List<&2, U32>) -> String:
321 to_string.go(rev(xs), SNil{})
322
323def hex.cat(xs: List<&2, U32>, acc: String) -> String:
324 match xs:
325 case Nil{}:
326 acc
327 case Con{h, t}:
328 +b = byte(h)
329 SCon{hex.digit(U32.shrn(b, 4n)), SCon{hex.digit(U32.and(b, 15)), hex.cat(t, acc)}}
330
331def hex.go(rs: List<&2, U32>, acc: String) -> String:
332 match rs:
333 case Nil{}:
334 acc
335 case Con{h, t}:
336 +b = byte(h)
337 hex.go(t, SCon{hex.digit(U32.shrn(b, 4n)), SCon{hex.digit(U32.and(b, 15)), acc}})
338
339def hex.fast(xs: List<&2, U32>) -> String:
340 hex.go(rev(xs), SNil{})
341
342# Octets: the byte-string interface
343#
344# Public interfaces take and answer Octets. Its representation is internal:
345# other packages use only the Octets.* defs below and, in proofs, this
346# package's laws, never the constructor. Today an Octets is a list of
347# OctByte records, so every value of the type is a valid byte string (no
348# element can be 256 or more), which is what makes laws like
349# of_list(to_list(o)) == o hold for every o.
350
351type Octets is Data:
352 Octets{words: List<&2, OctByte>}
353
354# masking every element of a list to 8 bits (the list layer's view)
355def mask(xs: List<&2, U32>) -> List<&2, U32>:
356 match xs:
357 case Nil{}:
358 Nil{}
359 case Con{h, t}:
360 Con{byte(h), mask(t)}
361
362def list_eq(xs: List<&2, U32>, ys: List<&2, U32>) -> Bool:
363 match xs ys:
364 case Nil{} Nil{}:
365 True{}
366 case Con{a, s} Con{b, t}:
367 Bool.and(U32.is_eq(a, b), list_eq(s, t))
368 case _ _:
369 False{}
370
371def mask.go(xs: List<&2, U32>, acc: List<&2, U32>) -> List<&2, U32>:
372 match xs:
373 case Nil{}:
374 acc
375 case Con{h, t}:
376 mask.go(t, Con{byte(h), acc})
377
378# mask, tail-recursive (LAWS.bend: mask_fast)
379def mask.fast(xs: List<&2, U32>) -> List<&2, U32>:
380 rev(mask.go(xs, Nil{}))
381
382def list_eq.go(xs: List<&2, U32>, ys: List<&2, U32>, ok: Bool) -> Bool:
383 match xs ys:
384 case Nil{} Nil{}:
385 ok
386 case Con{a, s} Con{b, t}:
387 list_eq.go(s, t, Bool.and(ok, U32.is_eq(a, b)))
388 case _ _:
389 False{}
390
391# list_eq, tail-recursive; every element is compared (LAWS.bend: list_eq_fast)
392def list_eq.fast(xs: List<&2, U32>, ys: List<&2, U32>) -> Bool:
393 list_eq.go(xs, ys, True{})
394
395# Word lists: the operations Octets is built from
396
397def w8s.of_list(xs: List<&2, U32>) -> List<&2, OctByte>:
398 match xs:
399 case Nil{}:
400 Nil{}
401 case Con{h, t}:
402 Con{oct.of(h), w8s.of_list(t)}
403
404def w8s.to_list(ws: List<&2, OctByte>) -> List<&2, U32>:
405 match ws:
406 case Nil{}:
407 Nil{}
408 case Con{h, t}:
409 Con{oct.to(h), w8s.to_list(t)}
410
411def w8s.take(n: Nat, ws: List<&2, OctByte>) -> List<&2, OctByte>:
412 match n:
413 case 0n:
414 Nil{}
415 case 1n+p:
416 match ws:
417 case Nil{}:
418 Nil{}
419 case Con{h, t}:
420 Con{h, w8s.take(p, t)}
421
422def w8s.drop(n: Nat, ws: List<&2, OctByte>) -> List<&2, OctByte>:
423 match n:
424 case 0n:
425 ws
426 case 1n+p:
427 match ws:
428 case Nil{}:
429 Nil{}
430 case Con{h, t}:
431 w8s.drop(p, t)
432
433def w8s.zeros(n: Nat) -> List<&2, OctByte>:
434 match n:
435 case 0n:
436 Nil{}
437 case 1n+p:
438 Con{oct.zero(), w8s.zeros(p)}
439
440def w8s.at(ws: List<&2, OctByte>) -> Maybe<&2, U32>:
441 match ws:
442 case Con{h, t}:
443 Some{oct.to(h)}
444 case Nil{}:
445 None{}
446
447# The same operations, tail-recursive: what Octets runs. Bend 2.0.37's
448# runtime overflows its stack at a depth of some tens of thousands of nested
449# non-tail calls, so the structural forms above, which the proofs reason
450# about, cannot run on long strings. Each form here builds its answer in an
451# accumulator (reversed where order matters) and is proved equal to its
452# structural form for every input (PROOF.bend: *_fast).
453
454def w8s.rev_onto(ws: List<&2, OctByte>, acc: List<&2, OctByte>) -> List<&2, OctByte>:
455 match ws:
456 case Nil{}:
457 acc
458 case Con{h, t}:
459 w8s.rev_onto(t, Con{h, acc})
460
461def w8s.of_list.go(xs: List<&2, U32>, acc: List<&2, OctByte>) -> List<&2, OctByte>:
462 match xs:
463 case Nil{}:
464 acc
465 case Con{h, t}:
466 w8s.of_list.go(t, Con{oct.of(h), acc})
467
468def w8s.of_list.fast(xs: List<&2, U32>) -> List<&2, OctByte>:
469 w8s.rev_onto(w8s.of_list.go(xs, Nil{}), Nil{})
470
471def w8s.to_list.go(ws: List<&2, OctByte>, acc: List<&2, U32>) -> List<&2, U32>:
472 match ws:
473 case Nil{}:
474 acc
475 case Con{h, t}:
476 w8s.to_list.go(t, Con{oct.to(h), acc})
477
478def w8s.to_list.fast(ws: List<&2, OctByte>) -> List<&2, U32>:
479 rev_onto(w8s.to_list.go(ws, Nil{}), Nil{})
480
481def w8s.take.go(n: Nat, ws: List<&2, OctByte>, acc: List<&2, OctByte>) -> List<&2, OctByte>:
482 match n:
483 case 0n:
484 acc
485 case 1n+p:
486 match ws:
487 case Nil{}:
488 acc
489 case Con{h, t}:
490 w8s.take.go(p, t, Con{h, acc})
491
492def w8s.take.fast(n: Nat, ws: List<&2, OctByte>) -> List<&2, OctByte>:
493 w8s.rev_onto(w8s.take.go(n, ws, Nil{}), Nil{})
494
495def w8s.append.fast(xs: List<&2, OctByte>, ys: List<&2, OctByte>) -> List<&2, OctByte>:
496 w8s.rev_onto(w8s.rev_onto(xs, Nil{}), ys)
497
498def w8s.len.go(ws: List<&2, OctByte>, n: Nat) -> Nat:
499 match ws:
500 case Nil{}:
501 n
502 case Con{h, t}:
503 w8s.len.go(t, 1n+n)
504
505def w8s.len.fast(ws: List<&2, OctByte>) -> Nat:
506 w8s.len.go(ws, 0n)
507
508def w8s.zeros.go(n: Nat, acc: List<&2, OctByte>) -> List<&2, OctByte>:
509 match n:
510 case 0n:
511 acc
512 case 1n+p:
513 w8s.zeros.go(p, Con{oct.zero(), acc})
514
515def w8s.zeros.fast(n: Nat) -> List<&2, OctByte>:
516 w8s.zeros.go(n, Nil{})
517
518# whether two word lists are equal; every word is compared (no early exit)
519def w8s.eq(xs: List<&2, OctByte>, ys: List<&2, OctByte>, ok: Bool) -> Bool:
520 match xs ys:
521 case Nil{} Nil{}:
522 ok
523 case Con{a, s} Con{b, t}:
524 w8s.eq(s, t, Bool.and(ok, U32.is_eq(oct.to(a), oct.to(b))))
525 case _ _:
526 False{}
527
528# text and hex, built from the last byte back (rs is the string reversed)
529def w8s.text.go(rs: List<&2, OctByte>, acc: String) -> String:
530 match rs:
531 case Nil{}:
532 acc
533 case Con{h, t}:
534 w8s.text.go(t, SCon{Chr{oct.to(h)}, acc})
535
536def w8s.hex.go(rs: List<&2, OctByte>, acc: String) -> String:
537 match rs:
538 case Nil{}:
539 acc
540 case Con{h, t}:
541 +b = oct.to(h)
542 w8s.hex.go(t, SCon{hex.digit(U32.shrn(b, 4n)), SCon{hex.digit(U32.and(b, 15)), acc}})
543
544# Conversions: of_list masks every element to 8 bits
545
546def Octets.of_list(xs: List<&2, U32>) -> Octets:
547 Octets{w8s.of_list.fast(xs)}
548
549def Octets.to_list(o: Octets) -> List<&2, U32>:
550 match o:
551 case Octets{ws}:
552 w8s.to_list.fast(ws)
553
554def Octets.of_string(s: String) -> Octets:
555 Octets.of_list(of_string(s))
556
557def Octets.to_string(o: Octets) -> String:
558 match o:
559 case Octets{ws}:
560 w8s.text.go(w8s.rev_onto(ws, Nil{}), SNil{})
561
562def Octets.hex(o: Octets) -> String:
563 match o:
564 case Octets{ws}:
565 w8s.hex.go(w8s.rev_onto(ws, Nil{}), SNil{})
566
567# Building and slicing
568
569def Octets.empty() -> Octets:
570 Octets{Nil{}}
571
572def Octets.zeros(n: Nat) -> Octets:
573 Octets{w8s.zeros.fast(n)}
574
575# a byte (the low 8 bits of b) in front of o
576def Octets.cons(b: U32, o: Octets) -> Octets:
577 match o:
578 case Octets{ws}:
579 Octets{Con{oct.of(b), ws}}
580
581def Octets.append(a: Octets, b: Octets) -> Octets:
582 match a b:
583 case Octets{xs} Octets{ys}:
584 Octets{w8s.append.fast(xs, ys)}
585
586# concat as the laws state it: each piece in front of the rest
587def Octets.concat.ref(os: List<&2, Octets>) -> Octets:
588 match os:
589 case Nil{}:
590 Octets.empty()
591 case Con{h, t}:
592 Octets.append(h, Octets.concat.ref(t))
593
594# every piece's words pushed, reversed, onto acc
595def w8s.concat.go(os: List<&2, Octets>, acc: List<&2, OctByte>) -> List<&2, OctByte>:
596 match os:
597 case Nil{}:
598 acc
599 case Con{Octets{ws}, t}:
600 w8s.concat.go(t, w8s.rev_onto(ws, acc))
601
602# the pieces joined in order, tail-recursive (LAWS.bend: octets_concat_*)
603def Octets.concat(os: List<&2, Octets>) -> Octets:
604 Octets{w8s.rev_onto(w8s.concat.go(os, Nil{}), Nil{})}
605
606# the words of an Octets (internal; for the proofs)
607def Octets.words(o: Octets) -> List<&2, OctByte>:
608 match o:
609 case Octets{ws}:
610 ws
611
612def Octets.len(o: Octets) -> Nat:
613 match o:
614 case Octets{ws}:
615 w8s.len.fast(ws)
616
617def Octets.take(n: Nat, o: Octets) -> Octets:
618 match o:
619 case Octets{ws}:
620 Octets{w8s.take.fast(n, ws)}
621
622def Octets.drop(n: Nat, o: Octets) -> Octets:
623 match o:
624 case Octets{ws}:
625 Octets{w8s.drop(n, ws)}
626
627# the n bytes at offset i (fewer if o ends first)
628def Octets.slice(+i: Nat, n: Nat, o: Octets) -> Octets:
629 Octets.take(n, Octets.drop(i, o))
630
631# a byte string cut in two
632type OctetsSplit is Data:
633 OctetsSplit{head: Octets, rest: Octets}
634
635def Octets.split_at.pick(fits: Bool, +n: Nat, +o: Octets) -> Maybe<&2, OctetsSplit>:
636 match fits:
637 case True{}:
638 Some{OctetsSplit{Octets.take(n, o), Octets.drop(n, o)}}
639 case False{}:
640 None{}
641
642# the first n bytes and the rest, or None if o has fewer than n bytes
643def Octets.split_at(+n: Nat, +o: Octets) -> Maybe<&2, OctetsSplit>:
644 Octets.split_at.pick(Nat.is_le(n, Octets.len(o)), n, o)
645
646def Octets.is_eq(a: Octets, b: Octets) -> Bool:
647 match a b:
648 case Octets{xs} Octets{ys}:
649 w8s.eq(xs, ys, True{})
650
651def Octets.at(o: Octets, i: Nat) -> Maybe<&2, U32>:
652 match o:
653 case Octets{ws}:
654 w8s.at(w8s.drop(i, ws))
655
656# Fields: written as bytes, read through the list layer over just the
657# bytes a field needs (a read walks to its offset, never past it)
658
659def Octets.le16(v: U32) -> Octets:
660 Octets.of_list(le16(v))
661
662def Octets.be16(v: U32) -> Octets:
663 Octets.of_list(be16(v))
664
665def Octets.le32(v: U32) -> Octets:
666 Octets.of_list(le32(v))
667
668def Octets.be32(v: U32) -> Octets:
669 Octets.of_list(be32(v))
670
671def Octets.le64(v: W.W64) -> Octets:
672 Octets.of_list(le64(v))
673
674def Octets.be64(v: W.W64) -> Octets:
675 Octets.of_list(be64(v))
676
677def Octets.field(+i: Nat, n: Nat, o: Octets) -> List<&2, U32>:
678 Octets.to_list(Octets.slice(i, n, o))
679
680def Octets.le16_at(o: Octets, +i: Nat) -> Maybe<&2, U32>:
681 le16.head(Octets.field(i, 2n, o))
682
683def Octets.be16_at(o: Octets, +i: Nat) -> Maybe<&2, U32>:
684 be16.head(Octets.field(i, 2n, o))
685
686def Octets.le32_at(o: Octets, +i: Nat) -> Maybe<&2, U32>:
687 le32.head(Octets.field(i, 4n, o))
688
689def Octets.be32_at(o: Octets, +i: Nat) -> Maybe<&2, U32>:
690 be32.head(Octets.field(i, 4n, o))
691
692def Octets.le64_at(o: Octets, +i: Nat) -> Maybe<&2, W.W64>:
693 le64_at(Octets.field(i, 8n, o), 0n)
694
695def Octets.be64_at(o: Octets, +i: Nat) -> Maybe<&2, W.W64>:
696 be64_at(Octets.field(i, 8n, o), 0n)