LAWS.bend

bend-osdev-bytes@0.1.1.0 · 638 lines · 117 definitions

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.
4import Base
5import bend-osdev-word64@0.1.1.0/word64.bend as W
6import bend-osdev-bytes@0.1.1.0/bytes.bend as B
7
8# Properties, for every input
9
10law le16_round_trip:
11  for v: U32
12  {B.le16_at(B.le16(v), 0n) == Some{B.low16(v)} : Maybe<&2, U32>}
13
14law be16_round_trip:
15  for v: U32
16  {B.be16_at(B.be16(v), 0n) == Some{B.low16(v)} : Maybe<&2, U32>}
17
18law le32_round_trip:
19  for v: U32
20  {B.le32_at(B.le32(v), 0n) == Some{v} : Maybe<&2, U32>}
21
22law be32_round_trip:
23  for v: U32
24  {B.be32_at(B.be32(v), 0n) == Some{v} : Maybe<&2, U32>}
25
26law le64_round_trip:
27  for +v: W.W64
28  {B.le64_at(B.le64(v), 0n) == Some{v} : Maybe<&2, W.W64>}
29
30law be64_round_trip:
31  for +v: W.W64
32  {B.be64_at(B.be64(v), 0n) == Some{v} : Maybe<&2, W.W64>}
33
34law byte_below_256:
35  for b: U32
36  {U32.is_lt(B.byte(b), 256) == True{} : Bool}
37
38law 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
45law be32_order:
46  {B.be32(305419896) == [18, 52, 86, 120] : List<&2, U32>}
47
48law le32_order:
49  {B.le32(305419896) == [120, 86, 52, 18] : List<&2, U32>}
50
51law be64_order:
52  {B.be64(W.W64.from_parts(16909060, 84281096)) == [1, 2, 3, 4, 5, 6, 7, 8] : List<&2, U32>}
53
54law le16_at_offset:
55  {B.le16_at([9, 52, 18], 1n) == Some{4660} : Maybe<&2, U32>}
56
57law short_input:
58  {B.le16_at([1, 2, 3], 2n) == None{} : Maybe<&2, U32>}
59
60law at_end:
61  {B.at([7, 8], 2n) == None{} : Maybe<&2, U32>}
62
63law masks_elements:
64  {B.at([7, 264], 1n) == Some{8} : Maybe<&2, U32>}
65
66law 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
71law 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
75law 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
79law octets_le32_round_trip:
80  for v: U32
81  {B.Octets.le32_at(B.Octets.le32(v), 0n) == Some{v} : Maybe<&2, U32>}
82
83law octets_be32_round_trip:
84  for v: U32
85  {B.Octets.be32_at(B.Octets.be32(v), 0n) == Some{v} : Maybe<&2, U32>}
86
87law 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
91law 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
95law 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
101law 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
105law octets_is_eq_refl:
106  for o: B.Octets
107  {B.Octets.is_eq(o, o) == True{} : Bool}
108
109law octets_masks:
110  {B.Octets.hex(B.Octets.of_list([255, 256, 257])) == "ff0001" : String}
111
112law 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
118law 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
124law 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
129law 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
133law octets_zeros_list:
134  for n: Nat
135  {B.Octets.to_list(B.Octets.zeros(n)) == B.zeros(n) : List<&2, U32>}
136
137law 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
142law 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
147law 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
152law 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
157law 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
162law octets_split_short:
163  {B.Octets.split_at(4n, B.Octets.of_string("abc")) == None{} : Maybe<&2, B.OctetsSplit>}
164
165law 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
173law len_fast:
174  for xs: List<&2, U32>
175  {B.len(xs) == B.len.fast(xs) : Nat}
176
177law 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
182law 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
187law zeros_fast:
188  for n: Nat
189  {B.zeros(n) == B.zeros.fast(n) : List<&2, U32>}
190
191law mask_fast:
192  for xs: List<&2, U32>
193  {B.mask(xs) == B.mask.fast(xs) : List<&2, U32>}
194
195law of_string_fast:
196  for s: String
197  {B.of_string(s) == B.of_string.fast(s) : List<&2, U32>}
198
199law to_string_fast:
200  for xs: List<&2, U32>
201  {B.to_string(xs) == B.to_string.fast(xs) : String}
202
203law hex_fast:
204  for xs: List<&2, U32>
205  {B.hex(xs) == B.hex.fast(xs) : String}
206
207law 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
212law 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
218law octets_hex_list:
219  for o: B.Octets
220  {B.Octets.hex(o) == B.hex(B.Octets.to_list(o)) : String}
221
222law 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
226law octets_concat_nil:
227  {B.Octets.concat(Nil{}) == B.Octets.empty() : B.Octets}
228
229law 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
239law 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
244law 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
249law 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
255law 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
260law 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
266law 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
273law octets_len_zeros:
274  for +n: Nat
275  {B.Octets.len(B.Octets.zeros(n)) == n : Nat}
276
277law octets_len_of_list:
278  for +xs: List<&2, U32>
279  {B.Octets.len(B.Octets.of_list(xs)) == B.len(xs) : Nat}
280
281law 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
287law octets_append_empty_l:
288  for +o: B.Octets
289  {B.Octets.append(B.Octets.empty(), o) == o : B.Octets}
290
291law octets_append_empty_r:
292  for +o: B.Octets
293  {B.Octets.append(o, B.Octets.empty()) == o : B.Octets}
294
295law octets_drop_zero:
296  for +o: B.Octets
297  {B.Octets.drop(0n, o) == o : B.Octets}
298
299law 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
305law 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
311law 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
317law 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
323law 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
331law 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
338law 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
344law 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
351law 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
359law 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
366law 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
374law 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
381law 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
391law 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
396law 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
402law 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
409law 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
415law 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
424law 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
430law 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
437law 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
443law 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
453law octets_len_le16:
454  for +v: U32
455  {B.Octets.len(B.Octets.le16(v)) == 2n : Nat}
456
457law octets_len_be16:
458  for +v: U32
459  {B.Octets.len(B.Octets.be16(v)) == 2n : Nat}
460
461law octets_len_le32:
462  for +v: U32
463  {B.Octets.len(B.Octets.le32(v)) == 4n : Nat}
464
465law octets_len_be32:
466  for +v: U32
467  {B.Octets.len(B.Octets.be32(v)) == 4n : Nat}
468
469law octets_len_le64:
470  for +v: W.W64
471  {B.Octets.len(B.Octets.le64(v)) == 8n : Nat}
472
473law octets_len_be64:
474  for +v: W.W64
475  {B.Octets.len(B.Octets.be64(v)) == 8n : Nat}
476
477law 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
483law 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
490law 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
496law 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
503law 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
509law 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
516law 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
522law 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
529law 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
535law 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
542law 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
548law 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
555law 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
561law 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
568law 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
574law 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
581law 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
587law 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
594law 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
600law 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
607law 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
613law 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
620law 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
626law 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
636law low16_mask:
637  for +v: U32
638  {B.low16(U32.and(v, 65535)) == U32.and(v, 65535) : U32}