1	# Every field writer and its reader agree, for every value; a byte is always
2	# below 256; and a byte string split anywhere joins back to itself. The
3	# vectors fix the byte orders, the hex text, and what a short input reads.
4	import Base
5	import bend-osdev-word64@0.1.1.1/word64.bend as W
6	import ./bytes.bend as B
7	
8	# Properties, for every input
9	
10	law le16_round_trip:
11	  for v: U32
12	  {B.le16_at(B.le16(v), 0n) == Some{B.low16(v)} : Maybe<&2, U32>}
13	
14	law be16_round_trip:
15	  for v: U32
16	  {B.be16_at(B.be16(v), 0n) == Some{B.low16(v)} : Maybe<&2, U32>}
17	
18	law le32_round_trip:
19	  for v: U32
20	  {B.le32_at(B.le32(v), 0n) == Some{v} : Maybe<&2, U32>}
21	
22	law be32_round_trip:
23	  for v: U32
24	  {B.be32_at(B.be32(v), 0n) == Some{v} : Maybe<&2, U32>}
25	
26	law le64_round_trip:
27	  for +v: W.W64
28	  {B.le64_at(B.le64(v), 0n) == Some{v} : Maybe<&2, W.W64>}
29	
30	law be64_round_trip:
31	  for +v: W.W64
32	  {B.be64_at(B.be64(v), 0n) == Some{v} : Maybe<&2, W.W64>}
33	
34	law byte_below_256:
35	  for b: U32
36	  {U32.is_lt(B.byte(b), 256) == True{} : Bool}
37	
38	law take_drop:
39	  for n: Nat
40	  for xs: List<&2, U32>
41	  {B.append(B.take(n, xs), B.drop(n, xs)) == xs : List<&2, U32>}
42	
43	# Vectors (0x12345678 = 305419896)
44	
45	law be32_order:
46	  {B.be32(305419896) == [18, 52, 86, 120] : List<&2, U32>}
47	
48	law le32_order:
49	  {B.le32(305419896) == [120, 86, 52, 18] : List<&2, U32>}
50	
51	law be64_order:
52	  {B.be64(W.W64.from_parts(16909060, 84281096)) == [1, 2, 3, 4, 5, 6, 7, 8] : List<&2, U32>}
53	
54	law le16_at_offset:
55	  {B.le16_at([9, 52, 18], 1n) == Some{4660} : Maybe<&2, U32>}
56	
57	law short_input:
58	  {B.le16_at([1, 2, 3], 2n) == None{} : Maybe<&2, U32>}
59	
60	law at_end:
61	  {B.at([7, 8], 2n) == None{} : Maybe<&2, U32>}
62	
63	law masks_elements:
64	  {B.at([7, 264], 1n) == Some{8} : Maybe<&2, U32>}
65	
66	law hex_text:
67	  {B.hex(B.of_string("Bend")) == "42656e64" : String}
68	
69	# The Octets interface: the same round trips, and slicing, on Octets
70	
71	law octets_le16_round_trip:
72	  for v: U32
73	  {B.Octets.le16_at(B.Octets.le16(v), 0n) == Some{B.low16(v)} : Maybe<&2, U32>}
74	
75	law octets_be16_round_trip:
76	  for v: U32
77	  {B.Octets.be16_at(B.Octets.be16(v), 0n) == Some{B.low16(v)} : Maybe<&2, U32>}
78	
79	law octets_le32_round_trip:
80	  for v: U32
81	  {B.Octets.le32_at(B.Octets.le32(v), 0n) == Some{v} : Maybe<&2, U32>}
82	
83	law octets_be32_round_trip:
84	  for v: U32
85	  {B.Octets.be32_at(B.Octets.be32(v), 0n) == Some{v} : Maybe<&2, U32>}
86	
87	law octets_le64_round_trip:
88	  for +v: W.W64
89	  {B.Octets.le64_at(B.Octets.le64(v), 0n) == Some{v} : Maybe<&2, W.W64>}
90	
91	law octets_be64_round_trip:
92	  for +v: W.W64
93	  {B.Octets.be64_at(B.Octets.be64(v), 0n) == Some{v} : Maybe<&2, W.W64>}
94	
95	law octets_take_drop:
96	  for n: Nat
97	  for o: B.Octets
98	  {B.Octets.append(B.Octets.take(n, o), B.Octets.drop(n, o)) == o : B.Octets}
99	
100	# of_list masks once: converting a byte string to a list and back changes nothing
101	law octets_of_list_idempotent:
102	  for xs: List<&2, U32>
103	  {B.Octets.of_list(B.Octets.to_list(B.Octets.of_list(xs))) == B.Octets.of_list(xs) : B.Octets}
104	
105	law octets_is_eq_refl:
106	  for o: B.Octets
107	  {B.Octets.is_eq(o, o) == True{} : Bool}
108	
109	law octets_masks:
110	  {B.Octets.hex(B.Octets.of_list([255, 256, 257])) == "ff0001" : String}
111	
112	law octets_slice:
113	  {B.Octets.to_string(B.Octets.slice(2n, 3n, B.Octets.of_string("bend-osdev"))) == "nd-" : String}
114	
115	# The interface laws other packages' proofs rely on: how Octets relates to
116	# lists, without depending on how Octets stores its bytes
117	
118	law octets_append_list:
119	  for a: B.Octets
120	  for b: B.Octets
121	  {B.Octets.to_list(B.Octets.append(a, b)) == B.append(B.Octets.to_list(a), B.Octets.to_list(b)) : List<&2, U32>}
122	
123	# every Octets is a valid byte string: to a list and back changes nothing
124	law octets_of_to:
125	  for o: B.Octets
126	  {B.Octets.of_list(B.Octets.to_list(o)) == o : B.Octets}
127	
128	# a list becomes Octets by masking each element to its low 8 bits
129	law octets_to_of:
130	  for xs: List<&2, U32>
131	  {B.Octets.to_list(B.Octets.of_list(xs)) == B.mask(xs) : List<&2, U32>}
132	
133	law octets_zeros_list:
134	  for n: Nat
135	  {B.Octets.to_list(B.Octets.zeros(n)) == B.zeros(n) : List<&2, U32>}
136	
137	law octets_cons_list:
138	  for b: U32
139	  for o: B.Octets
140	  {B.Octets.to_list(B.Octets.cons(b, o)) == Con{B.byte(b), B.Octets.to_list(o)} : List<&2, U32>}
141	
142	law octets_len_list:
143	  for o: B.Octets
144	  {B.Octets.len(o) == B.len(B.Octets.to_list(o)) : Nat}
145	
146	# a joined string splits back exactly where it was joined
147	law octets_take_append:
148	  for +a: B.Octets
149	  for b: B.Octets
150	  {B.Octets.take(B.Octets.len(a), B.Octets.append(a, b)) == a : B.Octets}
151	
152	law octets_drop_append:
153	  for a: B.Octets
154	  for +b: B.Octets
155	  {B.Octets.drop(B.Octets.len(a), B.Octets.append(a, b)) == b : B.Octets}
156	
157	law octets_split_at_append:
158	  for +a: B.Octets
159	  for +b: B.Octets
160	  {B.Octets.split_at(B.Octets.len(a), B.Octets.append(a, b)) == Some{B.OctetsSplit{a, b}} : Maybe<&2, B.OctetsSplit>}
161	
162	law octets_split_short:
163	  {B.Octets.split_at(4n, B.Octets.of_string("abc")) == None{} : Maybe<&2, B.OctetsSplit>}
164	
165	law octets_split_text:
166	  {B.Octets.split_at(2n, B.Octets.of_string("abc")) == Some{B.OctetsSplit{B.Octets.of_string("ab"), B.Octets.of_string("c")}} : Maybe<&2, B.OctetsSplit>}
167	
168	# The tail-recursive list layer: each fast form equals its structural form,
169	# for every input (stated structural == fast, the direction rewrites use, so
170	# that `%BL.len_fast(xs) : {... _ ...}` turns a fast form back into the one
171	# the other laws are about)
172	
173	law len_fast:
174	  for xs: List<&2, U32>
175	  {B.len(xs) == B.len.fast(xs) : Nat}
176	
177	law take_fast:
178	  for n: Nat
179	  for xs: List<&2, U32>
180	  {B.take(n, xs) == B.take.fast(n, xs) : List<&2, U32>}
181	
182	law append_fast:
183	  for xs: List<&2, U32>
184	  for ys: List<&2, U32>
185	  {B.append(xs, ys) == B.append.fast(xs, ys) : List<&2, U32>}
186	
187	law zeros_fast:
188	  for n: Nat
189	  {B.zeros(n) == B.zeros.fast(n) : List<&2, U32>}
190	
191	law mask_fast:
192	  for xs: List<&2, U32>
193	  {B.mask(xs) == B.mask.fast(xs) : List<&2, U32>}
194	
195	law of_string_fast:
196	  for s: String
197	  {B.of_string(s) == B.of_string.fast(s) : List<&2, U32>}
198	
199	law to_string_fast:
200	  for xs: List<&2, U32>
201	  {B.to_string(xs) == B.to_string.fast(xs) : String}
202	
203	law hex_fast:
204	  for xs: List<&2, U32>
205	  {B.hex(xs) == B.hex.fast(xs) : String}
206	
207	law list_eq_fast:
208	  for xs: List<&2, U32>
209	  for ys: List<&2, U32>
210	  {B.list_eq(xs, ys) == B.list_eq.fast(xs, ys) : Bool}
211	
212	law rev_rev:
213	  for xs: List<&2, U32>
214	  {B.rev(B.rev(xs)) == xs : List<&2, U32>}
215	
216	# Octets' text and hex are the list layer's, and concat joins in order
217	
218	law octets_hex_list:
219	  for o: B.Octets
220	  {B.Octets.hex(o) == B.hex(B.Octets.to_list(o)) : String}
221	
222	law octets_to_string_list:
223	  for o: B.Octets
224	  {B.Octets.to_string(o) == B.to_string(B.Octets.to_list(o)) : String}
225	
226	law octets_concat_nil:
227	  {B.Octets.concat(Nil{}) == B.Octets.empty() : B.Octets}
228	
229	law octets_concat_cons:
230	  for h: B.Octets
231	  for t: List<&2, B.Octets>
232	  {B.Octets.concat(Con{h, t}) == B.Octets.append(h, B.Octets.concat(t)) : B.Octets}
233	
234	# Reading at an offset: lengths, take and drop at offsets, and what a byte
235	# or a field read inside joined, cut or sliced bytes gives (for dependents'
236	# proofs: a field at offset i of a ++ b is read from a when it ends inside
237	# a, and at i of b when it starts at len(a) + i)
238	
239	law octets_len_append:
240	  for +a: B.Octets
241	  for +b: B.Octets
242	  {B.Octets.len(B.Octets.append(a, b)) == Nat.add(B.Octets.len(a), B.Octets.len(b)) : Nat}
243	
244	law octets_len_take:
245	  for +n: Nat
246	  for +o: B.Octets
247	  {B.Octets.len(B.Octets.take(n, o)) == Nat.min(n, B.Octets.len(o)) : Nat}
248	
249	law octets_len_take_le:
250	  for +n: Nat
251	  for +o: B.Octets
252	  for h: {Nat.is_le(n, B.Octets.len(o)) == True{} : Bool}
253	  {B.Octets.len(B.Octets.take(n, o)) == n : Nat}
254	
255	law octets_len_drop:
256	  for +n: Nat
257	  for +o: B.Octets
258	  {B.Octets.len(B.Octets.drop(n, o)) == Nat.sub(B.Octets.len(o), n) : Nat}
259	
260	law octets_len_slice:
261	  for +i: Nat
262	  for +n: Nat
263	  for +o: B.Octets
264	  {B.Octets.len(B.Octets.slice(i, n, o)) == Nat.min(n, Nat.sub(B.Octets.len(o), i)) : Nat}
265	
266	law octets_len_slice_le:
267	  for +i: Nat
268	  for +n: Nat
269	  for +o: B.Octets
270	  for h: {Nat.is_le(Nat.add(i, n), B.Octets.len(o)) == True{} : Bool}
271	  {B.Octets.len(B.Octets.slice(i, n, o)) == n : Nat}
272	
273	law octets_len_zeros:
274	  for +n: Nat
275	  {B.Octets.len(B.Octets.zeros(n)) == n : Nat}
276	
277	law octets_len_of_list:
278	  for +xs: List<&2, U32>
279	  {B.Octets.len(B.Octets.of_list(xs)) == B.len(xs) : Nat}
280	
281	law octets_append_assoc:
282	  for +a: B.Octets
283	  for +b: B.Octets
284	  for +c: B.Octets
285	  {B.Octets.append(B.Octets.append(a, b), c) == B.Octets.append(a, B.Octets.append(b, c)) : B.Octets}
286	
287	law octets_append_empty_l:
288	  for +o: B.Octets
289	  {B.Octets.append(B.Octets.empty(), o) == o : B.Octets}
290	
291	law octets_append_empty_r:
292	  for +o: B.Octets
293	  {B.Octets.append(o, B.Octets.empty()) == o : B.Octets}
294	
295	law octets_drop_zero:
296	  for +o: B.Octets
297	  {B.Octets.drop(0n, o) == o : B.Octets}
298	
299	law octets_take_len:
300	  for +o: B.Octets
301	  {B.Octets.take(B.Octets.len(o), o) == o : B.Octets}
302	
303	# take and drop composed
304	
305	law octets_drop_drop:
306	  for +j: Nat
307	  for +i: Nat
308	  for +o: B.Octets
309	  {B.Octets.drop(i, B.Octets.drop(j, o)) == B.Octets.drop(Nat.add(j, i), o) : B.Octets}
310	
311	law octets_take_take:
312	  for +i: Nat
313	  for +j: Nat
314	  for +o: B.Octets
315	  {B.Octets.take(i, B.Octets.take(j, o)) == B.Octets.take(Nat.min(i, j), o) : B.Octets}
316	
317	law octets_take_drop_comm:
318	  for +i: Nat
319	  for +j: Nat
320	  for +o: B.Octets
321	  {B.Octets.take(i, B.Octets.drop(j, o)) == B.Octets.drop(j, B.Octets.take(Nat.add(j, i), o)) : B.Octets}
322	
323	law octets_drop_take_comm:
324	  for +i: Nat
325	  for +j: Nat
326	  for +o: B.Octets
327	  {B.Octets.drop(i, B.Octets.take(j, o)) == B.Octets.take(Nat.sub(j, i), B.Octets.drop(i, o)) : B.Octets}
328	
329	# take and drop at offsets inside joined bytes
330	
331	law octets_take_append_le:
332	  for +n: Nat
333	  for +a: B.Octets
334	  for +b: B.Octets
335	  for h: {Nat.is_le(n, B.Octets.len(a)) == True{} : Bool}
336	  {B.Octets.take(n, B.Octets.append(a, b)) == B.Octets.take(n, a) : B.Octets}
337	
338	law octets_take_append_add:
339	  for +a: B.Octets
340	  for +n: Nat
341	  for +b: B.Octets
342	  {B.Octets.take(Nat.add(B.Octets.len(a), n), B.Octets.append(a, b)) == B.Octets.append(a, B.Octets.take(n, b)) : B.Octets}
343	
344	law octets_drop_append_le:
345	  for +n: Nat
346	  for +a: B.Octets
347	  for +b: B.Octets
348	  for h: {Nat.is_le(n, B.Octets.len(a)) == True{} : Bool}
349	  {B.Octets.drop(n, B.Octets.append(a, b)) == B.Octets.append(B.Octets.drop(n, a), b) : B.Octets}
350	
351	law octets_drop_append_add:
352	  for +a: B.Octets
353	  for +n: Nat
354	  for +b: B.Octets
355	  {B.Octets.drop(Nat.add(B.Octets.len(a), n), B.Octets.append(a, b)) == B.Octets.drop(n, b) : B.Octets}
356	
357	# slices
358	
359	law octets_slice_append_add:
360	  for +a: B.Octets
361	  for +i: Nat
362	  for +n: Nat
363	  for +b: B.Octets
364	  {B.Octets.slice(Nat.add(B.Octets.len(a), i), n, B.Octets.append(a, b)) == B.Octets.slice(i, n, b) : B.Octets}
365	
366	law octets_slice_append_le:
367	  for +i: Nat
368	  for +n: Nat
369	  for +a: B.Octets
370	  for +b: B.Octets
371	  for h: {Nat.is_le(Nat.add(i, n), B.Octets.len(a)) == True{} : Bool}
372	  {B.Octets.slice(i, n, B.Octets.append(a, b)) == B.Octets.slice(i, n, a) : B.Octets}
373	
374	law octets_slice_drop:
375	  for +j: Nat
376	  for +i: Nat
377	  for +n: Nat
378	  for +o: B.Octets
379	  {B.Octets.slice(i, n, B.Octets.drop(j, o)) == B.Octets.slice(Nat.add(j, i), n, o) : B.Octets}
380	
381	law octets_slice_take:
382	  for +m: Nat
383	  for +i: Nat
384	  for +n: Nat
385	  for +o: B.Octets
386	  for h: {Nat.is_le(Nat.add(i, n), m) == True{} : Bool}
387	  {B.Octets.slice(i, n, B.Octets.take(m, o)) == B.Octets.slice(i, n, o) : B.Octets}
388	
389	# a byte at an offset
390	
391	law octets_at_list:
392	  for +o: B.Octets
393	  for +i: Nat
394	  {B.Octets.at(o, i) == B.at(B.Octets.to_list(o), i) : Maybe<&2, U32>}
395	
396	law octets_at_append_add:
397	  for +a: B.Octets
398	  for +b: B.Octets
399	  for +i: Nat
400	  {B.Octets.at(B.Octets.append(a, b), Nat.add(B.Octets.len(a), i)) == B.Octets.at(b, i) : Maybe<&2, U32>}
401	
402	law octets_at_append_lt:
403	  for +a: B.Octets
404	  for +b: B.Octets
405	  for +i: Nat
406	  for h: {Nat.is_lt(i, B.Octets.len(a)) == True{} : Bool}
407	  {B.Octets.at(B.Octets.append(a, b), i) == B.Octets.at(a, i) : Maybe<&2, U32>}
408	
409	law octets_at_drop:
410	  for +j: Nat
411	  for +o: B.Octets
412	  for +i: Nat
413	  {B.Octets.at(B.Octets.drop(j, o), i) == B.Octets.at(o, Nat.add(j, i)) : Maybe<&2, U32>}
414	
415	law octets_at_take:
416	  for +n: Nat
417	  for +o: B.Octets
418	  for +i: Nat
419	  for h: {Nat.is_lt(i, n) == True{} : Bool}
420	  {B.Octets.at(B.Octets.take(n, o), i) == B.Octets.at(o, i) : Maybe<&2, U32>}
421	
422	# the list layer's at
423	
424	law at_append_add:
425	  for +a: List<&2, U32>
426	  for +b: List<&2, U32>
427	  for +i: Nat
428	  {B.at(B.append(a, b), Nat.add(B.len(a), i)) == B.at(b, i) : Maybe<&2, U32>}
429	
430	law at_append_lt:
431	  for +a: List<&2, U32>
432	  for +b: List<&2, U32>
433	  for +i: Nat
434	  for h: {Nat.is_lt(i, B.len(a)) == True{} : Bool}
435	  {B.at(B.append(a, b), i) == B.at(a, i) : Maybe<&2, U32>}
436	
437	law at_drop:
438	  for +j: Nat
439	  for +xs: List<&2, U32>
440	  for +i: Nat
441	  {B.at(B.drop(j, xs), i) == B.at(xs, Nat.add(j, i)) : Maybe<&2, U32>}
442	
443	law at_take:
444	  for +n: Nat
445	  for +xs: List<&2, U32>
446	  for +i: Nat
447	  for h: {Nat.is_lt(i, n) == True{} : Bool}
448	  {B.at(B.take(n, xs), i) == B.at(xs, i) : Maybe<&2, U32>}
449	
450	# the fields' widths, and each field read at an offset: inside joined bytes
451	# (past the first part, or ending inside it), and inside cut bytes
452	
453	law octets_len_le16:
454	  for +v: U32
455	  {B.Octets.len(B.Octets.le16(v)) == 2n : Nat}
456	
457	law octets_len_be16:
458	  for +v: U32
459	  {B.Octets.len(B.Octets.be16(v)) == 2n : Nat}
460	
461	law octets_len_le32:
462	  for +v: U32
463	  {B.Octets.len(B.Octets.le32(v)) == 4n : Nat}
464	
465	law octets_len_be32:
466	  for +v: U32
467	  {B.Octets.len(B.Octets.be32(v)) == 4n : Nat}
468	
469	law octets_len_le64:
470	  for +v: W.W64
471	  {B.Octets.len(B.Octets.le64(v)) == 8n : Nat}
472	
473	law octets_len_be64:
474	  for +v: W.W64
475	  {B.Octets.len(B.Octets.be64(v)) == 8n : Nat}
476	
477	law octets_le16_at_append_add:
478	  for +a: B.Octets
479	  for +b: B.Octets
480	  for +i: Nat
481	  {B.Octets.le16_at(B.Octets.append(a, b), Nat.add(B.Octets.len(a), i)) == B.Octets.le16_at(b, i) : Maybe<&2, U32>}
482	
483	law octets_le16_at_append_le:
484	  for +a: B.Octets
485	  for +b: B.Octets
486	  for +i: Nat
487	  for h: {Nat.is_le(Nat.add(i, 2n), B.Octets.len(a)) == True{} : Bool}
488	  {B.Octets.le16_at(B.Octets.append(a, b), i) == B.Octets.le16_at(a, i) : Maybe<&2, U32>}
489	
490	law octets_le16_at_drop:
491	  for +j: Nat
492	  for +o: B.Octets
493	  for +i: Nat
494	  {B.Octets.le16_at(B.Octets.drop(j, o), i) == B.Octets.le16_at(o, Nat.add(j, i)) : Maybe<&2, U32>}
495	
496	law octets_le16_at_take:
497	  for +n: Nat
498	  for +o: B.Octets
499	  for +i: Nat
500	  for h: {Nat.is_le(Nat.add(i, 2n), n) == True{} : Bool}
501	  {B.Octets.le16_at(B.Octets.take(n, o), i) == B.Octets.le16_at(o, i) : Maybe<&2, U32>}
502	
503	law octets_be16_at_append_add:
504	  for +a: B.Octets
505	  for +b: B.Octets
506	  for +i: Nat
507	  {B.Octets.be16_at(B.Octets.append(a, b), Nat.add(B.Octets.len(a), i)) == B.Octets.be16_at(b, i) : Maybe<&2, U32>}
508	
509	law octets_be16_at_append_le:
510	  for +a: B.Octets
511	  for +b: B.Octets
512	  for +i: Nat
513	  for h: {Nat.is_le(Nat.add(i, 2n), B.Octets.len(a)) == True{} : Bool}
514	  {B.Octets.be16_at(B.Octets.append(a, b), i) == B.Octets.be16_at(a, i) : Maybe<&2, U32>}
515	
516	law octets_be16_at_drop:
517	  for +j: Nat
518	  for +o: B.Octets
519	  for +i: Nat
520	  {B.Octets.be16_at(B.Octets.drop(j, o), i) == B.Octets.be16_at(o, Nat.add(j, i)) : Maybe<&2, U32>}
521	
522	law octets_be16_at_take:
523	  for +n: Nat
524	  for +o: B.Octets
525	  for +i: Nat
526	  for h: {Nat.is_le(Nat.add(i, 2n), n) == True{} : Bool}
527	  {B.Octets.be16_at(B.Octets.take(n, o), i) == B.Octets.be16_at(o, i) : Maybe<&2, U32>}
528	
529	law octets_le32_at_append_add:
530	  for +a: B.Octets
531	  for +b: B.Octets
532	  for +i: Nat
533	  {B.Octets.le32_at(B.Octets.append(a, b), Nat.add(B.Octets.len(a), i)) == B.Octets.le32_at(b, i) : Maybe<&2, U32>}
534	
535	law octets_le32_at_append_le:
536	  for +a: B.Octets
537	  for +b: B.Octets
538	  for +i: Nat
539	  for h: {Nat.is_le(Nat.add(i, 4n), B.Octets.len(a)) == True{} : Bool}
540	  {B.Octets.le32_at(B.Octets.append(a, b), i) == B.Octets.le32_at(a, i) : Maybe<&2, U32>}
541	
542	law octets_le32_at_drop:
543	  for +j: Nat
544	  for +o: B.Octets
545	  for +i: Nat
546	  {B.Octets.le32_at(B.Octets.drop(j, o), i) == B.Octets.le32_at(o, Nat.add(j, i)) : Maybe<&2, U32>}
547	
548	law octets_le32_at_take:
549	  for +n: Nat
550	  for +o: B.Octets
551	  for +i: Nat
552	  for h: {Nat.is_le(Nat.add(i, 4n), n) == True{} : Bool}
553	  {B.Octets.le32_at(B.Octets.take(n, o), i) == B.Octets.le32_at(o, i) : Maybe<&2, U32>}
554	
555	law octets_be32_at_append_add:
556	  for +a: B.Octets
557	  for +b: B.Octets
558	  for +i: Nat
559	  {B.Octets.be32_at(B.Octets.append(a, b), Nat.add(B.Octets.len(a), i)) == B.Octets.be32_at(b, i) : Maybe<&2, U32>}
560	
561	law octets_be32_at_append_le:
562	  for +a: B.Octets
563	  for +b: B.Octets
564	  for +i: Nat
565	  for h: {Nat.is_le(Nat.add(i, 4n), B.Octets.len(a)) == True{} : Bool}
566	  {B.Octets.be32_at(B.Octets.append(a, b), i) == B.Octets.be32_at(a, i) : Maybe<&2, U32>}
567	
568	law octets_be32_at_drop:
569	  for +j: Nat
570	  for +o: B.Octets
571	  for +i: Nat
572	  {B.Octets.be32_at(B.Octets.drop(j, o), i) == B.Octets.be32_at(o, Nat.add(j, i)) : Maybe<&2, U32>}
573	
574	law octets_be32_at_take:
575	  for +n: Nat
576	  for +o: B.Octets
577	  for +i: Nat
578	  for h: {Nat.is_le(Nat.add(i, 4n), n) == True{} : Bool}
579	  {B.Octets.be32_at(B.Octets.take(n, o), i) == B.Octets.be32_at(o, i) : Maybe<&2, U32>}
580	
581	law octets_le64_at_append_add:
582	  for +a: B.Octets
583	  for +b: B.Octets
584	  for +i: Nat
585	  {B.Octets.le64_at(B.Octets.append(a, b), Nat.add(B.Octets.len(a), i)) == B.Octets.le64_at(b, i) : Maybe<&2, W.W64>}
586	
587	law octets_le64_at_append_le:
588	  for +a: B.Octets
589	  for +b: B.Octets
590	  for +i: Nat
591	  for h: {Nat.is_le(Nat.add(i, 8n), B.Octets.len(a)) == True{} : Bool}
592	  {B.Octets.le64_at(B.Octets.append(a, b), i) == B.Octets.le64_at(a, i) : Maybe<&2, W.W64>}
593	
594	law octets_le64_at_drop:
595	  for +j: Nat
596	  for +o: B.Octets
597	  for +i: Nat
598	  {B.Octets.le64_at(B.Octets.drop(j, o), i) == B.Octets.le64_at(o, Nat.add(j, i)) : Maybe<&2, W.W64>}
599	
600	law octets_le64_at_take:
601	  for +n: Nat
602	  for +o: B.Octets
603	  for +i: Nat
604	  for h: {Nat.is_le(Nat.add(i, 8n), n) == True{} : Bool}
605	  {B.Octets.le64_at(B.Octets.take(n, o), i) == B.Octets.le64_at(o, i) : Maybe<&2, W.W64>}
606	
607	law octets_be64_at_append_add:
608	  for +a: B.Octets
609	  for +b: B.Octets
610	  for +i: Nat
611	  {B.Octets.be64_at(B.Octets.append(a, b), Nat.add(B.Octets.len(a), i)) == B.Octets.be64_at(b, i) : Maybe<&2, W.W64>}
612	
613	law octets_be64_at_append_le:
614	  for +a: B.Octets
615	  for +b: B.Octets
616	  for +i: Nat
617	  for h: {Nat.is_le(Nat.add(i, 8n), B.Octets.len(a)) == True{} : Bool}
618	  {B.Octets.be64_at(B.Octets.append(a, b), i) == B.Octets.be64_at(a, i) : Maybe<&2, W.W64>}
619	
620	law octets_be64_at_drop:
621	  for +j: Nat
622	  for +o: B.Octets
623	  for +i: Nat
624	  {B.Octets.be64_at(B.Octets.drop(j, o), i) == B.Octets.be64_at(o, Nat.add(j, i)) : Maybe<&2, W.W64>}
625	
626	law octets_be64_at_take:
627	  for +n: Nat
628	  for +o: B.Octets
629	  for +i: Nat
630	  for h: {Nat.is_le(Nat.add(i, 8n), n) == True{} : Bool}
631	  {B.Octets.be64_at(B.Octets.take(n, o), i) == B.Octets.be64_at(o, i) : Maybe<&2, W.W64>}
632	
633	# a value already masked to 16 bits is its own low16 (so a 16-bit field
634	# written from such a value reads back as that value)
635	
636	law low16_mask:
637	  for +v: U32
638	  {B.low16(U32.and(v, 65535)) == U32.and(v, 65535) : U32}