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.
11	import Base
12	import 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
17	def 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
23	def 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.
31	type 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)
35	def 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)
41	def 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	
46	def 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)
51	def byte(b: U32) -> U32:
52	  oct.to(oct.of(b))
53	
54	# List operations
55	
56	def 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)
60	def 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
72	def 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	
83	def append(a: List<&2, U32>, b: List<&2, U32>) -> List<&2, U32>:
84	  List.append(&2, U32, a, b)
85	
86	# n zero bytes
87	def 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
95	def 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	
102	def 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
108	def 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	
113	def 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	
119	def 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
126	def 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	
133	def 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	
140	def be32(v: U32) -> List<&2, U32>:
141	  be32.rev(le32(v))
142	
143	def le64(+v: W.W64) -> List<&2, U32>:
144	  append(le32(W.W64.lo(v)), le32(W.W64.hi(v)))
145	
146	def 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	
151	def 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	
158	def 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	
165	def 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	
172	def 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	
179	def 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	
188	def le16_at(xs: List<&2, U32>, i: Nat) -> Maybe<&2, U32>:
189	  le16.head(drop(i, xs))
190	
191	def be16_at(xs: List<&2, U32>, i: Nat) -> Maybe<&2, U32>:
192	  be16.head(drop(i, xs))
193	
194	def le32_at(xs: List<&2, U32>, i: Nat) -> Maybe<&2, U32>:
195	  le32.head(drop(i, xs))
196	
197	def be32_at(xs: List<&2, U32>, i: Nat) -> Maybe<&2, U32>:
198	  be32.head(drop(i, xs))
199	
200	def 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	
203	def 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	
208	def 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	
215	def 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	
222	def 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	
229	def hex.digit(+d: U32) -> Char:
230	  hex.digit.pick(U32.is_lt(d, 10), d)
231	
232	# two lower-case hex digits per byte
233	def 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	
248	def 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	
255	def rev(xs: List<&2, U32>) -> List<&2, U32>:
256	  rev_onto(xs, Nil{})
257	
258	def 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	
265	def len.fast(xs: List<&2, U32>) -> Nat:
266	  len.go(xs, 0n)
267	
268	def 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	
279	def take.fast(n: Nat, xs: List<&2, U32>) -> List<&2, U32>:
280	  rev(take.go(n, xs, Nil{}))
281	
282	def append.fast(xs: List<&2, U32>, ys: List<&2, U32>) -> List<&2, U32>:
283	  rev_onto(rev(xs), ys)
284	
285	def 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	
292	def zeros.fast(n: Nat) -> List<&2, U32>:
293	  zeros.go(n, Nil{})
294	
295	def 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	
302	def 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)
306	def 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	
313	def 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	
320	def to_string.fast(xs: List<&2, U32>) -> String:
321	  to_string.go(rev(xs), SNil{})
322	
323	def 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	
331	def 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	
339	def 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	
351	type 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)
355	def 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	
362	def 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	
371	def 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)
379	def mask.fast(xs: List<&2, U32>) -> List<&2, U32>:
380	  rev(mask.go(xs, Nil{}))
381	
382	def 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)
392	def 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	
397	def 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	
404	def 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	
411	def 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	
422	def 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	
433	def 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	
440	def 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	
454	def 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	
461	def 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	
468	def w8s.of_list.fast(xs: List<&2, U32>) -> List<&2, OctByte>:
469	  w8s.rev_onto(w8s.of_list.go(xs, Nil{}), Nil{})
470	
471	def 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	
478	def w8s.to_list.fast(ws: List<&2, OctByte>) -> List<&2, U32>:
479	  rev_onto(w8s.to_list.go(ws, Nil{}), Nil{})
480	
481	def 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	
492	def w8s.take.fast(n: Nat, ws: List<&2, OctByte>) -> List<&2, OctByte>:
493	  w8s.rev_onto(w8s.take.go(n, ws, Nil{}), Nil{})
494	
495	def 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	
498	def 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	
505	def w8s.len.fast(ws: List<&2, OctByte>) -> Nat:
506	  w8s.len.go(ws, 0n)
507	
508	def 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	
515	def 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)
519	def 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)
529	def 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	
536	def 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	
546	def Octets.of_list(xs: List<&2, U32>) -> Octets:
547	  Octets{w8s.of_list.fast(xs)}
548	
549	def Octets.to_list(o: Octets) -> List<&2, U32>:
550	  match o:
551	    case Octets{ws}:
552	      w8s.to_list.fast(ws)
553	
554	def Octets.of_string(s: String) -> Octets:
555	  Octets.of_list(of_string(s))
556	
557	def Octets.to_string(o: Octets) -> String:
558	  match o:
559	    case Octets{ws}:
560	      w8s.text.go(w8s.rev_onto(ws, Nil{}), SNil{})
561	
562	def 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	
569	def Octets.empty() -> Octets:
570	  Octets{Nil{}}
571	
572	def 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
576	def Octets.cons(b: U32, o: Octets) -> Octets:
577	  match o:
578	    case Octets{ws}:
579	      Octets{Con{oct.of(b), ws}}
580	
581	def 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
587	def 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
595	def 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_*)
603	def 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)
607	def Octets.words(o: Octets) -> List<&2, OctByte>:
608	  match o:
609	    case Octets{ws}:
610	      ws
611	
612	def Octets.len(o: Octets) -> Nat:
613	  match o:
614	    case Octets{ws}:
615	      w8s.len.fast(ws)
616	
617	def Octets.take(n: Nat, o: Octets) -> Octets:
618	  match o:
619	    case Octets{ws}:
620	      Octets{w8s.take.fast(n, ws)}
621	
622	def 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)
628	def 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
632	type OctetsSplit is Data:
633	  OctetsSplit{head: Octets, rest: Octets}
634	
635	def 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
643	def 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	
646	def 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	
651	def 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	
659	def Octets.le16(v: U32) -> Octets:
660	  Octets.of_list(le16(v))
661	
662	def Octets.be16(v: U32) -> Octets:
663	  Octets.of_list(be16(v))
664	
665	def Octets.le32(v: U32) -> Octets:
666	  Octets.of_list(le32(v))
667	
668	def Octets.be32(v: U32) -> Octets:
669	  Octets.of_list(be32(v))
670	
671	def Octets.le64(v: W.W64) -> Octets:
672	  Octets.of_list(le64(v))
673	
674	def Octets.be64(v: W.W64) -> Octets:
675	  Octets.of_list(be64(v))
676	
677	def Octets.field(+i: Nat, n: Nat, o: Octets) -> List<&2, U32>:
678	  Octets.to_list(Octets.slice(i, n, o))
679	
680	def Octets.le16_at(o: Octets, +i: Nat) -> Maybe<&2, U32>:
681	  le16.head(Octets.field(i, 2n, o))
682	
683	def Octets.be16_at(o: Octets, +i: Nat) -> Maybe<&2, U32>:
684	  be16.head(Octets.field(i, 2n, o))
685	
686	def Octets.le32_at(o: Octets, +i: Nat) -> Maybe<&2, U32>:
687	  le32.head(Octets.field(i, 4n, o))
688	
689	def Octets.be32_at(o: Octets, +i: Nat) -> Maybe<&2, U32>:
690	  be32.head(Octets.field(i, 4n, o))
691	
692	def Octets.le64_at(o: Octets, +i: Nat) -> Maybe<&2, W.W64>:
693	  le64_at(Octets.field(i, 8n, o), 0n)
694	
695	def Octets.be64_at(o: Octets, +i: Nat) -> Maybe<&2, W.W64>:
696	  be64_at(Octets.field(i, 8n, o), 0n)