bytes.bend

bend-osdev-bytes@0.1.1.0 · 696 lines · 118 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.1.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)