PROOF.bend

bend-osdev-bytes@0.1.1.0 · 1,514 lines · 156 definitions

1import Base
2import bend-osdev-word64@0.1.1.0/word64.bend as W
3import bend-osdev-word64@0.1.1.0/LAWS.bend as WL
4import bend-osdev-word64@0.1.1.0/PROOF.bend as WP
5import bend-osdev-bytes@0.1.1.0/bytes.bend as B
6import bend-osdev-bytes@0.1.1.0/LAWS.bend as Laws
7import bend-osdev-u32@0.1.0.0/LAWS.bend as UL
8import bend-osdev-u32@0.1.0.0/LAWS_order.bend as UO
9import bend-osdev-u32@0.1.0.0/PROOF.bend as UP
10import bend-osdev-u32@0.1.0.0/PROOF_order.bend as UOP
11
12def Laws.le16_round_trip(v):
13  match v:
14    case U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
15      {==}
16
17def Laws.be16_round_trip(v):
18  match v:
19    case U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
20      {==}
21
22def Laws.le32_round_trip(v):
23  match v:
24    case U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
25      {==}
26
27def Laws.be32_round_trip(v):
28  match v:
29    case U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
30      {==}
31
32# Reading a 32-bit field at the head of a longer string, and skipping it
33def le32_head_app(x: U32, r: List<&2, U32>) -> {B.le32.head(B.append(B.le32(x), r)) == Some{x} : Maybe<&2, U32>}:
34  match x:
35    case U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
36      {==}
37
38def be32_head_app(x: U32, r: List<&2, U32>) -> {B.be32.head(B.append(B.be32(x), r)) == Some{x} : Maybe<&2, U32>}:
39  match x:
40    case U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
41      {==}
42
43def drop4_le32(x: U32, r: List<&2, U32>) -> {B.drop(4n, B.append(B.le32(x), r)) == r : List<&2, U32>}:
44  match x:
45    case U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
46      {==}
47
48def drop4_be32(x: U32, r: List<&2, U32>) -> {B.drop(4n, B.append(B.be32(x), r)) == r : List<&2, U32>}:
49  match x:
50    case U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
51      {==}
52
53def Laws.le64_round_trip(v):
54  %Equal.sym(Maybe<&2, U32>, B.le32_at(B.le64(v), 0n), Some{W.W64.lo(v)}, le32_head_app(W.W64.lo(v), B.le32(W.W64.hi(v)))) : {B.le64.join(_, B.le32_at(B.le64(v), 4n)) == Some{v} : Maybe<&2, W.W64>}
55  %Equal.sym(Maybe<&2, U32>, B.le32_at(B.le64(v), 4n), Some{W.W64.hi(v)}, Equal.trans(Maybe<&2, U32>, B.le32_at(B.le64(v), 4n), B.le32.head(B.le32(W.W64.hi(v))), Some{W.W64.hi(v)}, Equal.cong(List<&2, U32>, Maybe<&2, U32>, l => B.le32.head(l), B.drop(4n, B.le64(v)), B.le32(W.W64.hi(v)), drop4_le32(W.W64.lo(v), B.le32(W.W64.hi(v)))), Laws.le32_round_trip(W.W64.hi(v)))) : {B.le64.join(Some{W.W64.lo(v)}, _) == Some{v} : Maybe<&2, W.W64>}
56  %WL.parts_of(v) : {Some{W.W64.from_parts(W.W64.hi(v), W.W64.lo(v))} == Some{_} : Maybe<&2, W.W64>}
57  {==}
58
59def Laws.be64_round_trip(v):
60  %Equal.sym(Maybe<&2, U32>, B.be32_at(B.be64(v), 0n), Some{W.W64.hi(v)}, be32_head_app(W.W64.hi(v), B.be32(W.W64.lo(v)))) : {B.le64.join(B.be32_at(B.be64(v), 4n), _) == Some{v} : Maybe<&2, W.W64>}
61  %Equal.sym(Maybe<&2, U32>, B.be32_at(B.be64(v), 4n), Some{W.W64.lo(v)}, Equal.trans(Maybe<&2, U32>, B.be32_at(B.be64(v), 4n), B.be32.head(B.be32(W.W64.lo(v))), Some{W.W64.lo(v)}, Equal.cong(List<&2, U32>, Maybe<&2, U32>, l => B.be32.head(l), B.drop(4n, B.be64(v)), B.be32(W.W64.lo(v)), drop4_be32(W.W64.hi(v), B.be32(W.W64.lo(v)))), Laws.be32_round_trip(W.W64.lo(v)))) : {B.le64.join(_, Some{W.W64.hi(v)}) == Some{v} : Maybe<&2, W.W64>}
62  %WL.parts_of(v) : {Some{W.W64.from_parts(W.W64.hi(v), W.W64.lo(v))} == Some{_} : Maybe<&2, W.W64>}
63  {==}
64
65def Laws.byte_below_256(b):
66  match b:
67    case U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
68      {==}
69
70def Laws.take_drop(n, xs):
71  match n xs:
72    case 0n _:
73      {==}
74    case 1n+p Nil{}:
75      {==}
76    case 1n+p Con{h, t}:
77      %Laws.take_drop(p, t) : {Con{h, B.append(B.take(p, t), B.drop(p, t))} == Con{h, _} : List<&2, U32>}
78      {==}
79
80def Laws.be32_order():
81  {==}
82
83def Laws.le32_order():
84  {==}
85
86def Laws.be64_order():
87  {==}
88
89def Laws.le16_at_offset():
90  {==}
91
92def Laws.short_input():
93  {==}
94
95def Laws.at_end():
96  {==}
97
98def Laws.masks_elements():
99  {==}
100
101def Laws.hex_text():
102  {==}
103
104def Laws.octets_le16_round_trip(v):
105  match v:
106    case U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
107      {==}
108
109def Laws.octets_be16_round_trip(v):
110  match v:
111    case U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
112      {==}
113
114def Laws.octets_le32_round_trip(v):
115  match v:
116    case U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
117      {==}
118
119def Laws.octets_be32_round_trip(v):
120  match v:
121    case U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
122      {==}
123
124# the eight bytes of two le32 fields come back unchanged through Octets
125def field64_le(x: U32, y: U32) -> {B.w8s.to_list.fast(B.w8s.take.fast(8n, B.w8s.of_list.fast(B.append(B.le32(x), B.le32(y))))) == B.append(B.le32(x), B.le32(y)) : List<&2, U32>}:
126  match x y:
127    case U32{WCon{x0, WCon{x1, WCon{x2, WCon{x3, WCon{x4, WCon{x5, WCon{x6, WCon{x7, WCon{x8, WCon{x9, WCon{x10, WCon{x11, WCon{x12, WCon{x13, WCon{x14, WCon{x15, WCon{x16, WCon{x17, WCon{x18, WCon{x19, WCon{x20, WCon{x21, WCon{x22, WCon{x23, WCon{x24, WCon{x25, WCon{x26, WCon{x27, WCon{x28, WCon{x29, WCon{x30, WCon{x31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{y0, WCon{y1, WCon{y2, WCon{y3, WCon{y4, WCon{y5, WCon{y6, WCon{y7, WCon{y8, WCon{y9, WCon{y10, WCon{y11, WCon{y12, WCon{y13, WCon{y14, WCon{y15, WCon{y16, WCon{y17, WCon{y18, WCon{y19, WCon{y20, WCon{y21, WCon{y22, WCon{y23, WCon{y24, WCon{y25, WCon{y26, WCon{y27, WCon{y28, WCon{y29, WCon{y30, WCon{y31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
128      {==}
129
130# the eight bytes of two be32 fields come back unchanged through Octets
131def field64_be(x: U32, y: U32) -> {B.w8s.to_list.fast(B.w8s.take.fast(8n, B.w8s.of_list.fast(B.append(B.be32(x), B.be32(y))))) == B.append(B.be32(x), B.be32(y)) : List<&2, U32>}:
132  match x y:
133    case U32{WCon{x0, WCon{x1, WCon{x2, WCon{x3, WCon{x4, WCon{x5, WCon{x6, WCon{x7, WCon{x8, WCon{x9, WCon{x10, WCon{x11, WCon{x12, WCon{x13, WCon{x14, WCon{x15, WCon{x16, WCon{x17, WCon{x18, WCon{x19, WCon{x20, WCon{x21, WCon{x22, WCon{x23, WCon{x24, WCon{x25, WCon{x26, WCon{x27, WCon{x28, WCon{x29, WCon{x30, WCon{x31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{y0, WCon{y1, WCon{y2, WCon{y3, WCon{y4, WCon{y5, WCon{y6, WCon{y7, WCon{y8, WCon{y9, WCon{y10, WCon{y11, WCon{y12, WCon{y13, WCon{y14, WCon{y15, WCon{y16, WCon{y17, WCon{y18, WCon{y19, WCon{y20, WCon{y21, WCon{y22, WCon{y23, WCon{y24, WCon{y25, WCon{y26, WCon{y27, WCon{y28, WCon{y29, WCon{y30, WCon{y31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
134      {==}
135
136def Laws.octets_le64_round_trip(v):
137  %Equal.sym(List<&2, U32>, B.w8s.to_list.fast(B.w8s.take.fast(8n, B.w8s.of_list.fast(B.le64(v)))), B.le64(v), field64_le(W.W64.lo(v), W.W64.hi(v))) : {B.le64_at(_, 0n) == Some{v} : Maybe<&2, W.W64>}
138  Laws.le64_round_trip(v)
139
140def Laws.octets_be64_round_trip(v):
141  %Equal.sym(List<&2, U32>, B.w8s.to_list.fast(B.w8s.take.fast(8n, B.w8s.of_list.fast(B.be64(v)))), B.be64(v), field64_be(W.W64.hi(v), W.W64.lo(v))) : {B.be64_at(_, 0n) == Some{v} : Maybe<&2, W.W64>}
142  Laws.be64_round_trip(v)
143
144# Word lists: the lemmas the Octets laws are built from
145
146def bits8_of_bits8(w: B.OctByte) -> {B.oct.of(B.oct.to(w)) == w : B.OctByte}:
147  match w:
148    case B.OctByte{a0, a1, a2, a3, a4, a5, a6, a7}:
149      {==}
150
151def w8s_of_to(ws: List<&2, B.OctByte>) -> {B.w8s.of_list(B.w8s.to_list(ws)) == ws : List<&2, B.OctByte>}:
152  match ws:
153    case Nil{}:
154      {==}
155    case Con{h, t}:
156      %bits8_of_bits8(h) : {Con{B.oct.of(B.oct.to(h)), B.w8s.of_list(B.w8s.to_list(t))} == Con{_, t} : List<&2, B.OctByte>}
157      %w8s_of_to(t) : {Con{B.oct.of(B.oct.to(h)), B.w8s.of_list(B.w8s.to_list(t))} == Con{B.oct.of(B.oct.to(h)), _} : List<&2, B.OctByte>}
158      {==}
159
160# a word through one OctByte and back is its byte
161def oct_byte(h: U32) -> {B.oct.to(B.oct.of(h)) == B.byte(h) : U32}:
162  match h:
163    case U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
164      {==}
165
166def w8s_to_of(xs: List<&2, U32>) -> {B.w8s.to_list(B.w8s.of_list(xs)) == B.mask(xs) : List<&2, U32>}:
167  match xs:
168    case Nil{}:
169      {==}
170    case Con{h, t}:
171      %w8s_to_of(t) : {Con{B.oct.to(B.oct.of(h)), B.w8s.to_list(B.w8s.of_list(t))} == Con{B.byte(h), _} : List<&2, U32>}
172      %oct_byte(h) : {Con{B.oct.to(B.oct.of(h)), B.w8s.to_list(B.w8s.of_list(t))} == Con{_, B.w8s.to_list(B.w8s.of_list(t))} : List<&2, U32>}
173      {==}
174
175def w8s_to_app(xs: List<&2, B.OctByte>, ys: List<&2, B.OctByte>) -> {B.w8s.to_list(List.append(&2, B.OctByte, xs, ys)) == B.append(B.w8s.to_list(xs), B.w8s.to_list(ys)) : List<&2, U32>}:
176  match xs:
177    case Nil{}:
178      {==}
179    case Con{h, t}:
180      %w8s_to_app(t, ys) : {Con{B.oct.to(h), B.w8s.to_list(List.append(&2, B.OctByte, t, ys))} == Con{B.oct.to(h), _} : List<&2, U32>}
181      {==}
182
183def w8s_len(ws: List<&2, B.OctByte>) -> {List.length(&2, B.OctByte, ws) == List.length(&2, U32, B.w8s.to_list(ws)) : Nat}:
184  match ws:
185    case Nil{}:
186      {==}
187    case Con{h, t}:
188      Equal.cong(Nat, Nat, k => 1n+k, List.length(&2, B.OctByte, t), List.length(&2, U32, B.w8s.to_list(t)), w8s_len(t))
189
190def w8s_take_drop(n: Nat, ws: List<&2, B.OctByte>) -> {List.append(&2, B.OctByte, B.w8s.take(n, ws), B.w8s.drop(n, ws)) == ws : List<&2, B.OctByte>}:
191  match n ws:
192    case 0n _:
193      {==}
194    case 1n+p Nil{}:
195      {==}
196    case 1n+p Con{h, t}:
197      %w8s_take_drop(p, t) : {Con{h, List.append(&2, B.OctByte, B.w8s.take(p, t), B.w8s.drop(p, t))} == Con{h, _} : List<&2, B.OctByte>}
198      {==}
199
200def w8s_take_app(xs: List<&2, B.OctByte>, ys: List<&2, B.OctByte>) -> {B.w8s.take(List.length(&2, B.OctByte, xs), List.append(&2, B.OctByte, xs, ys)) == xs : List<&2, B.OctByte>}:
201  match xs:
202    case Nil{}:
203      {==}
204    case Con{h, t}:
205      %w8s_take_app(t, ys) : {Con{h, B.w8s.take(List.length(&2, B.OctByte, t), List.append(&2, B.OctByte, t, ys))} == Con{h, _} : List<&2, B.OctByte>}
206      {==}
207
208def w8s_drop_app(xs: List<&2, B.OctByte>, ys: List<&2, B.OctByte>) -> {B.w8s.drop(List.length(&2, B.OctByte, xs), List.append(&2, B.OctByte, xs, ys)) == ys : List<&2, B.OctByte>}:
209  match xs:
210    case Nil{}:
211      {==}
212    case Con{h, t}:
213      w8s_drop_app(t, ys)
214
215def w8s_len_app(xs: List<&2, B.OctByte>, ys: List<&2, B.OctByte>) -> {List.length(&2, B.OctByte, List.append(&2, B.OctByte, xs, ys)) == Nat.add(List.length(&2, B.OctByte, xs), List.length(&2, B.OctByte, ys)) : Nat}:
216  match xs:
217    case Nil{}:
218      {==}
219    case Con{h, t}:
220      Equal.cong(Nat, Nat, k => 1n+k, List.length(&2, B.OctByte, List.append(&2, B.OctByte, t, ys)), Nat.add(List.length(&2, B.OctByte, t), List.length(&2, B.OctByte, ys)), w8s_len_app(t, ys))
221
222# Fast forms equal structural forms, for every input. bytes.bend's Octets
223# runs the tail-recursive *.fast defs; these lemmas (each stated
224# ref == fast, the direction rewrites use) carry every law proved about the
225# structural defs over to them.
226
227def r8_rr(ws: List<&2, B.OctByte>, acc: List<&2, B.OctByte>, b: List<&2, B.OctByte>) -> {B.w8s.rev_onto(B.w8s.rev_onto(ws, acc), b) == B.w8s.rev_onto(acc, List.append(&2, B.OctByte, ws, b)) : List<&2, B.OctByte>}:
228  match ws:
229    case Nil{}:
230      {==}
231    case Con{h, t}:
232      r8_rr(t, Con{h, acc}, b)
233
234def ru_rr(xs: List<&2, U32>, acc: List<&2, U32>, b: List<&2, U32>) -> {B.rev_onto(B.rev_onto(xs, acc), b) == B.rev_onto(acc, List.append(&2, U32, xs, b)) : List<&2, U32>}:
235  match xs:
236    case Nil{}:
237      {==}
238    case Con{h, t}:
239      ru_rr(t, Con{h, acc}, b)
240
241def app_nil8(+ws: List<&2, B.OctByte>) -> {List.append(&2, B.OctByte, ws, Nil{}) == ws : List<&2, B.OctByte>}:
242  match ws:
243    case Nil{}:
244      {==}
245    case Con{h, t}:
246      Equal.cong(List<&2, B.OctByte>, List<&2, B.OctByte>, l => Con{h, l}, List.append(&2, B.OctByte, t, Nil{}), t, app_nil8(t))
247
248def app_nilu(+xs: List<&2, U32>) -> {List.append(&2, U32, xs, Nil{}) == xs : List<&2, U32>}:
249  match xs:
250    case Nil{}:
251      {==}
252    case Con{h, t}:
253      Equal.cong(List<&2, U32>, List<&2, U32>, l => Con{h, l}, List.append(&2, U32, t, Nil{}), t, app_nilu(t))
254
255def g_of(xs: List<&2, U32>, acc: List<&2, B.OctByte>) -> {B.w8s.of_list.go(xs, acc) == B.w8s.rev_onto(B.w8s.of_list(xs), acc) : List<&2, B.OctByte>}:
256  match xs:
257    case Nil{}:
258      {==}
259    case Con{h, t}:
260      g_of(t, Con{B.oct.of(h), acc})
261
262def F_of(+xs: List<&2, U32>) -> {B.w8s.of_list(xs) == B.w8s.of_list.fast(xs) : List<&2, B.OctByte>}:
263  Equal.sym(List<&2, B.OctByte>, B.w8s.of_list.fast(xs), B.w8s.of_list(xs),
264    Equal.trans(List<&2, B.OctByte>, B.w8s.of_list.fast(xs), B.w8s.rev_onto(B.w8s.rev_onto(B.w8s.of_list(xs), Nil{}), Nil{}), B.w8s.of_list(xs),
265      Equal.cong(List<&2, B.OctByte>, List<&2, B.OctByte>, l => B.w8s.rev_onto(l, Nil{}), B.w8s.of_list.go(xs, Nil{}), B.w8s.rev_onto(B.w8s.of_list(xs), Nil{}), g_of(xs, Nil{})),
266      Equal.trans(List<&2, B.OctByte>, B.w8s.rev_onto(B.w8s.rev_onto(B.w8s.of_list(xs), Nil{}), Nil{}), List.append(&2, B.OctByte, B.w8s.of_list(xs), Nil{}), B.w8s.of_list(xs),
267        r8_rr(B.w8s.of_list(xs), Nil{}, Nil{}), app_nil8(B.w8s.of_list(xs)))))
268
269def g_to(ws: List<&2, B.OctByte>, acc: List<&2, U32>) -> {B.w8s.to_list.go(ws, acc) == B.rev_onto(B.w8s.to_list(ws), acc) : List<&2, U32>}:
270  match ws:
271    case Nil{}:
272      {==}
273    case Con{h, t}:
274      g_to(t, Con{B.oct.to(h), acc})
275
276def F_to(+ws: List<&2, B.OctByte>) -> {B.w8s.to_list(ws) == B.w8s.to_list.fast(ws) : List<&2, U32>}:
277  Equal.sym(List<&2, U32>, B.w8s.to_list.fast(ws), B.w8s.to_list(ws),
278    Equal.trans(List<&2, U32>, B.w8s.to_list.fast(ws), B.rev_onto(B.rev_onto(B.w8s.to_list(ws), Nil{}), Nil{}), B.w8s.to_list(ws),
279      Equal.cong(List<&2, U32>, List<&2, U32>, l => B.rev_onto(l, Nil{}), B.w8s.to_list.go(ws, Nil{}), B.rev_onto(B.w8s.to_list(ws), Nil{}), g_to(ws, Nil{})),
280      Equal.trans(List<&2, U32>, B.rev_onto(B.rev_onto(B.w8s.to_list(ws), Nil{}), Nil{}), List.append(&2, U32, B.w8s.to_list(ws), Nil{}), B.w8s.to_list(ws),
281        ru_rr(B.w8s.to_list(ws), Nil{}, Nil{}), app_nilu(B.w8s.to_list(ws)))))
282
283def g_take(n: Nat, ws: List<&2, B.OctByte>, acc: List<&2, B.OctByte>) -> {B.w8s.take.go(n, ws, acc) == B.w8s.rev_onto(B.w8s.take(n, ws), acc) : List<&2, B.OctByte>}:
284  match n ws:
285    case 0n _:
286      {==}
287    case 1n+p Nil{}:
288      {==}
289    case 1n+p Con{h, t}:
290      g_take(p, t, Con{h, acc})
291
292def F_take(+n: Nat, +ws: List<&2, B.OctByte>) -> {B.w8s.take(n, ws) == B.w8s.take.fast(n, ws) : List<&2, B.OctByte>}:
293  Equal.sym(List<&2, B.OctByte>, B.w8s.take.fast(n, ws), B.w8s.take(n, ws),
294    Equal.trans(List<&2, B.OctByte>, B.w8s.take.fast(n, ws), B.w8s.rev_onto(B.w8s.rev_onto(B.w8s.take(n, ws), Nil{}), Nil{}), B.w8s.take(n, ws),
295      Equal.cong(List<&2, B.OctByte>, List<&2, B.OctByte>, l => B.w8s.rev_onto(l, Nil{}), B.w8s.take.go(n, ws, Nil{}), B.w8s.rev_onto(B.w8s.take(n, ws), Nil{}), g_take(n, ws, Nil{})),
296      Equal.trans(List<&2, B.OctByte>, B.w8s.rev_onto(B.w8s.rev_onto(B.w8s.take(n, ws), Nil{}), Nil{}), List.append(&2, B.OctByte, B.w8s.take(n, ws), Nil{}), B.w8s.take(n, ws),
297        r8_rr(B.w8s.take(n, ws), Nil{}, Nil{}), app_nil8(B.w8s.take(n, ws)))))
298
299def F_app(+xs: List<&2, B.OctByte>, +ys: List<&2, B.OctByte>) -> {List.append(&2, B.OctByte, xs, ys) == B.w8s.append.fast(xs, ys) : List<&2, B.OctByte>}:
300  Equal.sym(List<&2, B.OctByte>, B.w8s.append.fast(xs, ys), List.append(&2, B.OctByte, xs, ys), r8_rr(xs, Nil{}, ys))
301
302def g_len(+ws: List<&2, B.OctByte>, +n: Nat) -> {B.w8s.len.go(ws, n) == Nat.add(List.length(&2, B.OctByte, ws), n) : Nat}:
303  match ws:
304    case Nil{}:
305      {==}
306    case Con{h, t}:
307      Equal.trans(Nat, B.w8s.len.go(t, 1n+n), Nat.add(List.length(&2, B.OctByte, t), 1n+n), 1n+Nat.add(List.length(&2, B.OctByte, t), n),
308        g_len(t, 1n+n), UL.nat_add_succ(List.length(&2, B.OctByte, t), n))
309
310def F_len(+ws: List<&2, B.OctByte>) -> {List.length(&2, B.OctByte, ws) == B.w8s.len.fast(ws) : Nat}:
311  Equal.sym(Nat, B.w8s.len.fast(ws), List.length(&2, B.OctByte, ws),
312    Equal.trans(Nat, B.w8s.len.go(ws, 0n), Nat.add(List.length(&2, B.OctByte, ws), 0n), List.length(&2, B.OctByte, ws),
313      g_len(ws, 0n), UL.nat_add_zero(List.length(&2, B.OctByte, ws))))
314
315def zeros_cons(+p: Nat, +acc: List<&2, B.OctByte>) -> {List.append(&2, B.OctByte, B.w8s.zeros(p), Con{B.oct.zero(), acc}) == Con{B.oct.zero(), List.append(&2, B.OctByte, B.w8s.zeros(p), acc)} : List<&2, B.OctByte>}:
316  match p:
317    case 0n:
318      {==}
319    case 1n+q:
320      Equal.cong(List<&2, B.OctByte>, List<&2, B.OctByte>, l => Con{B.oct.zero(), l}, List.append(&2, B.OctByte, B.w8s.zeros(q), Con{B.oct.zero(), acc}), Con{B.oct.zero(), List.append(&2, B.OctByte, B.w8s.zeros(q), acc)}, zeros_cons(q, acc))
321
322def g_zeros(+n: Nat, +acc: List<&2, B.OctByte>) -> {B.w8s.zeros.go(n, acc) == List.append(&2, B.OctByte, B.w8s.zeros(n), acc) : List<&2, B.OctByte>}:
323  match n:
324    case 0n:
325      {==}
326    case 1n+p:
327      Equal.trans(List<&2, B.OctByte>, B.w8s.zeros.go(p, Con{B.oct.zero(), acc}), List.append(&2, B.OctByte, B.w8s.zeros(p), Con{B.oct.zero(), acc}), Con{B.oct.zero(), List.append(&2, B.OctByte, B.w8s.zeros(p), acc)},
328        g_zeros(p, Con{B.oct.zero(), acc}), zeros_cons(p, acc))
329
330def F_zeros(+n: Nat) -> {B.w8s.zeros(n) == B.w8s.zeros.fast(n) : List<&2, B.OctByte>}:
331  Equal.sym(List<&2, B.OctByte>, B.w8s.zeros.fast(n), B.w8s.zeros(n),
332    Equal.trans(List<&2, B.OctByte>, B.w8s.zeros.go(n, Nil{}), List.append(&2, B.OctByte, B.w8s.zeros(n), Nil{}), B.w8s.zeros(n),
333      g_zeros(n, Nil{}), app_nil8(B.w8s.zeros(n))))
334
335def w8s_zeros_list(+n: Nat) -> {B.w8s.to_list(B.w8s.zeros(n)) == B.zeros(n) : List<&2, U32>}:
336  match n:
337    case 0n:
338      {==}
339    case 1n+p:
340      Equal.cong(List<&2, U32>, List<&2, U32>, l => Con{0, l}, B.w8s.to_list(B.w8s.zeros(p)), B.zeros(p), w8s_zeros_list(p))
341
342# The Octets laws: each rewrites Octets' fast forms to the structural ones,
343# then uses the word-list lemmas
344
345def p_octets_take_drop(+n: Nat, +o: B.Octets) -> {B.Octets.append(B.Octets.take(n, o), B.Octets.drop(n, o)) == o : B.Octets}:
346  match o:
347    case B.Octets{+ws}:
348      %F_app(B.w8s.take.fast(n, ws), B.w8s.drop(n, ws)) : {B.Octets{_} == B.Octets{ws} : B.Octets}
349      %F_take(n, ws) : {B.Octets{List.append(&2, B.OctByte, _, B.w8s.drop(n, ws))} == B.Octets{ws} : B.Octets}
350      Equal.cong(List<&2, B.OctByte>, B.Octets, l => B.Octets{l}, List.append(&2, B.OctByte, B.w8s.take(n, ws), B.w8s.drop(n, ws)), ws, w8s_take_drop(n, ws))
351
352def Laws.octets_take_drop(n, o):
353  p_octets_take_drop(n, o)
354
355def p_octets_of_to(+o: B.Octets) -> {B.Octets.of_list(B.Octets.to_list(o)) == o : B.Octets}:
356  match o:
357    case B.Octets{+ws}:
358      %F_of(B.w8s.to_list.fast(ws)) : {B.Octets{_} == B.Octets{ws} : B.Octets}
359      %F_to(ws) : {B.Octets{B.w8s.of_list(_)} == B.Octets{ws} : B.Octets}
360      Equal.cong(List<&2, B.OctByte>, B.Octets, l => B.Octets{l}, B.w8s.of_list(B.w8s.to_list(ws)), ws, w8s_of_to(ws))
361
362def Laws.octets_of_to(o):
363  p_octets_of_to(o)
364
365def p_octets_to_of(+xs: List<&2, U32>) -> {B.Octets.to_list(B.Octets.of_list(xs)) == B.mask(xs) : List<&2, U32>}:
366  %F_to(B.w8s.of_list.fast(xs)) : {_ == B.mask(xs) : List<&2, U32>}
367  %F_of(xs) : {B.w8s.to_list(_) == B.mask(xs) : List<&2, U32>}
368  w8s_to_of(xs)
369
370def Laws.octets_to_of(xs):
371  p_octets_to_of(xs)
372
373def Laws.octets_of_list_idempotent(xs):
374  Laws.octets_of_to(B.Octets.of_list(xs))
375
376def u32_eq_self(a: U32) -> {U32.is_eq(a, a) == True{} : Bool}:
377  match a:
378    case U32{+w}:
379      %Equal.sym(Cmp, Word.cmp(32n, w, w), EQ{}, UO.word_cmp_refl(32n, w)) : {Cmp.is_eq(_) == True{} : Bool}
380      {==}
381
382def list_eq_self(xs: List<&2, U32>) -> {B.list_eq(xs, xs) == True{} : Bool}:
383  match xs:
384    case Nil{}:
385      {==}
386    case Con{+h, +t}:
387      %Equal.sym(Bool, U32.is_eq(h, h), True{}, u32_eq_self(h)) : {Bool.and(_, B.list_eq(t, t)) == True{} : Bool}
388      list_eq_self(t)
389
390def w8s_eq_self(ws: List<&2, B.OctByte>) -> {B.w8s.eq(ws, ws, True{}) == True{} : Bool}:
391  match ws:
392    case Nil{}:
393      {==}
394    case Con{+h, +t}:
395      %Equal.sym(Bool, U32.is_eq(B.oct.to(h), B.oct.to(h)), True{}, u32_eq_self(B.oct.to(h))) : {B.w8s.eq(t, t, Bool.and(True{}, _)) == True{} : Bool}
396      w8s_eq_self(t)
397
398def Laws.octets_is_eq_refl(o):
399  match o:
400    case B.Octets{+ws}:
401      w8s_eq_self(ws)
402
403def Laws.octets_masks():
404  {==}
405
406def Laws.octets_slice():
407  {==}
408
409def p_octets_append_list(+a: B.Octets, +b: B.Octets) -> {B.Octets.to_list(B.Octets.append(a, b)) == B.append(B.Octets.to_list(a), B.Octets.to_list(b)) : List<&2, U32>}:
410  match a b:
411    case B.Octets{+xs} B.Octets{+ys}:
412      %F_to(B.w8s.append.fast(xs, ys)) : {_ == B.append(B.w8s.to_list.fast(xs), B.w8s.to_list.fast(ys)) : List<&2, U32>}
413      %F_app(xs, ys) : {B.w8s.to_list(_) == B.append(B.w8s.to_list.fast(xs), B.w8s.to_list.fast(ys)) : List<&2, U32>}
414      %F_to(xs) : {B.w8s.to_list(List.append(&2, B.OctByte, xs, ys)) == B.append(_, B.w8s.to_list.fast(ys)) : List<&2, U32>}
415      %F_to(ys) : {B.w8s.to_list(List.append(&2, B.OctByte, xs, ys)) == B.append(B.w8s.to_list(xs), _) : List<&2, U32>}
416      w8s_to_app(xs, ys)
417
418def Laws.octets_append_list(a, b):
419  p_octets_append_list(a, b)
420
421def p_octets_len_list(+o: B.Octets) -> {B.Octets.len(o) == B.len(B.Octets.to_list(o)) : Nat}:
422  match o:
423    case B.Octets{+ws}:
424      %F_len(ws) : {_ == B.len(B.w8s.to_list.fast(ws)) : Nat}
425      %F_to(ws) : {List.length(&2, B.OctByte, ws) == B.len(_) : Nat}
426      w8s_len(ws)
427
428def Laws.octets_len_list(o):
429  p_octets_len_list(o)
430
431def p_octets_take_append(+a: B.Octets, +b: B.Octets) -> {B.Octets.take(B.Octets.len(a), B.Octets.append(a, b)) == a : B.Octets}:
432  match a b:
433    case B.Octets{+xs} B.Octets{+ys}:
434      %F_take(B.w8s.len.fast(xs), B.w8s.append.fast(xs, ys)) : {B.Octets{_} == B.Octets{xs} : B.Octets}
435      %F_len(xs) : {B.Octets{B.w8s.take(_, B.w8s.append.fast(xs, ys))} == B.Octets{xs} : B.Octets}
436      %F_app(xs, ys) : {B.Octets{B.w8s.take(List.length(&2, B.OctByte, xs), _)} == B.Octets{xs} : B.Octets}
437      Equal.cong(List<&2, B.OctByte>, B.Octets, l => B.Octets{l}, B.w8s.take(List.length(&2, B.OctByte, xs), List.append(&2, B.OctByte, xs, ys)), xs, w8s_take_app(xs, ys))
438
439def Laws.octets_take_append(a, b):
440  p_octets_take_append(a, b)
441
442def p_octets_drop_append(+a: B.Octets, +b: B.Octets) -> {B.Octets.drop(B.Octets.len(a), B.Octets.append(a, b)) == b : B.Octets}:
443  match a b:
444    case B.Octets{+xs} B.Octets{+ys}:
445      %F_len(xs) : {B.Octets{B.w8s.drop(_, B.w8s.append.fast(xs, ys))} == B.Octets{ys} : B.Octets}
446      %F_app(xs, ys) : {B.Octets{B.w8s.drop(List.length(&2, B.OctByte, xs), _)} == B.Octets{ys} : B.Octets}
447      Equal.cong(List<&2, B.OctByte>, B.Octets, l => B.Octets{l}, B.w8s.drop(List.length(&2, B.OctByte, xs), List.append(&2, B.OctByte, xs, ys)), ys, w8s_drop_app(xs, ys))
448
449def Laws.octets_drop_append(a, b):
450  p_octets_drop_append(a, b)
451
452def p_octets_split_at_append(+a: B.Octets, +b: B.Octets) -> {B.Octets.split_at(B.Octets.len(a), B.Octets.append(a, b)) == Some{B.OctetsSplit{a, b}} : Maybe<&2, B.OctetsSplit>}:
453  match a b:
454    case B.Octets{+xs} B.Octets{+ys}:
455      %F_app(xs, ys) : {B.Octets.split_at.pick(Nat.is_le(B.w8s.len.fast(xs), B.w8s.len.fast(_)), B.w8s.len.fast(xs), B.Octets{B.w8s.append.fast(xs, ys)}) == Some{B.OctetsSplit{B.Octets{xs}, B.Octets{ys}}} : Maybe<&2, B.OctetsSplit>}
456      %F_app(xs, ys) : {B.Octets.split_at.pick(Nat.is_le(B.w8s.len.fast(xs), B.w8s.len.fast(List.append(&2, B.OctByte, xs, ys))), B.w8s.len.fast(xs), B.Octets{_}) == Some{B.OctetsSplit{B.Octets{xs}, B.Octets{ys}}} : Maybe<&2, B.OctetsSplit>}
457      %F_len(List.append(&2, B.OctByte, xs, ys)) : {B.Octets.split_at.pick(Nat.is_le(B.w8s.len.fast(xs), _), B.w8s.len.fast(xs), B.Octets{List.append(&2, B.OctByte, xs, ys)}) == Some{B.OctetsSplit{B.Octets{xs}, B.Octets{ys}}} : Maybe<&2, B.OctetsSplit>}
458      %F_len(xs) : {B.Octets.split_at.pick(Nat.is_le(_, List.length(&2, B.OctByte, List.append(&2, B.OctByte, xs, ys))), B.w8s.len.fast(xs), B.Octets{List.append(&2, B.OctByte, xs, ys)}) == Some{B.OctetsSplit{B.Octets{xs}, B.Octets{ys}}} : Maybe<&2, B.OctetsSplit>}
459      %F_len(xs) : {B.Octets.split_at.pick(Nat.is_le(List.length(&2, B.OctByte, xs), List.length(&2, B.OctByte, List.append(&2, B.OctByte, xs, ys))), _, B.Octets{List.append(&2, B.OctByte, xs, ys)}) == Some{B.OctetsSplit{B.Octets{xs}, B.Octets{ys}}} : Maybe<&2, B.OctetsSplit>}
460      %Equal.sym(Nat, List.length(&2, B.OctByte, List.append(&2, B.OctByte, xs, ys)), Nat.add(List.length(&2, B.OctByte, xs), List.length(&2, B.OctByte, ys)), w8s_len_app(xs, ys)) : {B.Octets.split_at.pick(Nat.is_le(List.length(&2, B.OctByte, xs), _), List.length(&2, B.OctByte, xs), B.Octets{List.append(&2, B.OctByte, xs, ys)}) == Some{B.OctetsSplit{B.Octets{xs}, B.Octets{ys}}} : Maybe<&2, B.OctetsSplit>}
461      %Equal.sym(Bool, Nat.is_le(List.length(&2, B.OctByte, xs), Nat.add(List.length(&2, B.OctByte, xs), List.length(&2, B.OctByte, ys))), True{}, UO.nat_le_add_r(List.length(&2, B.OctByte, xs), List.length(&2, B.OctByte, ys))) : {B.Octets.split_at.pick(_, List.length(&2, B.OctByte, xs), B.Octets{List.append(&2, B.OctByte, xs, ys)}) == Some{B.OctetsSplit{B.Octets{xs}, B.Octets{ys}}} : Maybe<&2, B.OctetsSplit>}
462      %F_take(List.length(&2, B.OctByte, xs), List.append(&2, B.OctByte, xs, ys)) : {Some{B.OctetsSplit{B.Octets{_}, B.Octets{B.w8s.drop(List.length(&2, B.OctByte, xs), List.append(&2, B.OctByte, xs, ys))}}} == Some{B.OctetsSplit{B.Octets{xs}, B.Octets{ys}}} : Maybe<&2, B.OctetsSplit>}
463      %w8s_take_app(xs, ys) : {Some{B.OctetsSplit{B.Octets{B.w8s.take(List.length(&2, B.OctByte, xs), List.append(&2, B.OctByte, xs, ys))}, B.Octets{B.w8s.drop(List.length(&2, B.OctByte, xs), List.append(&2, B.OctByte, xs, ys))}}} == Some{B.OctetsSplit{B.Octets{_}, B.Octets{ys}}} : Maybe<&2, B.OctetsSplit>}
464      %w8s_drop_app(xs, ys) : {Some{B.OctetsSplit{B.Octets{B.w8s.take(List.length(&2, B.OctByte, xs), List.append(&2, B.OctByte, xs, ys))}, B.Octets{B.w8s.drop(List.length(&2, B.OctByte, xs), List.append(&2, B.OctByte, xs, ys))}}} == Some{B.OctetsSplit{B.Octets{B.w8s.take(List.length(&2, B.OctByte, xs), List.append(&2, B.OctByte, xs, ys))}, B.Octets{_}}} : Maybe<&2, B.OctetsSplit>}
465      {==}
466
467def Laws.octets_split_at_append(a, b):
468  p_octets_split_at_append(a, b)
469
470def Laws.octets_split_short():
471  {==}
472
473def Laws.octets_split_text():
474  {==}
475
476def p_octets_zeros_list(+n: Nat) -> {B.Octets.to_list(B.Octets.zeros(n)) == B.zeros(n) : List<&2, U32>}:
477  %F_to(B.w8s.zeros.fast(n)) : {_ == B.zeros(n) : List<&2, U32>}
478  %F_zeros(n) : {B.w8s.to_list(_) == B.zeros(n) : List<&2, U32>}
479  w8s_zeros_list(n)
480
481def Laws.octets_zeros_list(n):
482  p_octets_zeros_list(n)
483
484def p_octets_cons_list(+b: U32, +o: B.Octets) -> {B.Octets.to_list(B.Octets.cons(b, o)) == Con{B.byte(b), B.Octets.to_list(o)} : List<&2, U32>}:
485  match o:
486    case B.Octets{+ws}:
487      %F_to(Con{B.oct.of(b), ws}) : {_ == Con{B.byte(b), B.w8s.to_list.fast(ws)} : List<&2, U32>}
488      %F_to(ws) : {Con{B.oct.to(B.oct.of(b)), B.w8s.to_list(ws)} == Con{B.byte(b), _} : List<&2, U32>}
489      %oct_byte(b) : {Con{B.oct.to(B.oct.of(b)), B.w8s.to_list(ws)} == Con{_, B.w8s.to_list(ws)} : List<&2, U32>}
490      {==}
491
492def Laws.octets_cons_list(b, o):
493  p_octets_cons_list(b, o)
494
495# The tail-recursive list layer equals the structural one
496
497def ru_app_nil(+xs: List<&2, U32>) -> {List.append(&2, U32, xs, Nil{}) == xs : List<&2, U32>}:
498  app_nilu(xs)
499
500def g_lenu(+xs: List<&2, U32>, +n: Nat) -> {B.len.go(xs, n) == Nat.add(B.len(xs), n) : Nat}:
501  match xs:
502    case Nil{}:
503      {==}
504    case Con{h, t}:
505      Equal.trans(Nat, B.len.go(t, 1n+n), Nat.add(B.len(t), 1n+n), 1n+Nat.add(B.len(t), n),
506        g_lenu(t, 1n+n), UL.nat_add_succ(B.len(t), n))
507
508def p_len_fast(+xs: List<&2, U32>) -> {B.len(xs) == B.len.fast(xs) : Nat}:
509  Equal.sym(Nat, B.len.fast(xs), B.len(xs),
510    Equal.trans(Nat, B.len.go(xs, 0n), Nat.add(B.len(xs), 0n), B.len(xs), g_lenu(xs, 0n), UL.nat_add_zero(B.len(xs))))
511
512def Laws.len_fast(xs):
513  p_len_fast(xs)
514
515# a structural list, reversed onto Nil and back, is itself
516def rr_back(+zs: List<&2, U32>) -> {B.rev_onto(B.rev_onto(zs, Nil{}), Nil{}) == zs : List<&2, U32>}:
517  Equal.trans(List<&2, U32>, B.rev_onto(B.rev_onto(zs, Nil{}), Nil{}), List.append(&2, U32, zs, Nil{}), zs, ru_rr(zs, Nil{}, Nil{}), app_nilu(zs))
518
519def g_takeu(+n: Nat, +xs: List<&2, U32>, +acc: List<&2, U32>) -> {B.take.go(n, xs, acc) == B.rev_onto(B.take(n, xs), acc) : List<&2, U32>}:
520  match n xs:
521    case 0n _:
522      {==}
523    case 1n+p Nil{}:
524      {==}
525    case 1n+p Con{h, t}:
526      g_takeu(p, t, Con{h, acc})
527
528def p_take_fast(+n: Nat, +xs: List<&2, U32>) -> {B.take(n, xs) == B.take.fast(n, xs) : List<&2, U32>}:
529  Equal.sym(List<&2, U32>, B.take.fast(n, xs), B.take(n, xs),
530    Equal.trans(List<&2, U32>, B.take.fast(n, xs), B.rev_onto(B.rev_onto(B.take(n, xs), Nil{}), Nil{}), B.take(n, xs),
531      Equal.cong(List<&2, U32>, List<&2, U32>, l => B.rev_onto(l, Nil{}), B.take.go(n, xs, Nil{}), B.rev_onto(B.take(n, xs), Nil{}), g_takeu(n, xs, Nil{})),
532      rr_back(B.take(n, xs))))
533
534def Laws.take_fast(n, xs):
535  p_take_fast(n, xs)
536
537def p_append_fast(+xs: List<&2, U32>, +ys: List<&2, U32>) -> {B.append(xs, ys) == B.append.fast(xs, ys) : List<&2, U32>}:
538  Equal.sym(List<&2, U32>, B.append.fast(xs, ys), B.append(xs, ys), ru_rr(xs, Nil{}, ys))
539
540def Laws.append_fast(xs, ys):
541  p_append_fast(xs, ys)
542
543def zeros_consu(+p: Nat, +acc: List<&2, U32>) -> {List.append(&2, U32, B.zeros(p), Con{0, acc}) == Con{0, List.append(&2, U32, B.zeros(p), acc)} : List<&2, U32>}:
544  match p:
545    case 0n:
546      {==}
547    case 1n+q:
548      Equal.cong(List<&2, U32>, List<&2, U32>, l => Con{0, l}, List.append(&2, U32, B.zeros(q), Con{0, acc}), Con{0, List.append(&2, U32, B.zeros(q), acc)}, zeros_consu(q, acc))
549
550def g_zerosu(+n: Nat, +acc: List<&2, U32>) -> {B.zeros.go(n, acc) == List.append(&2, U32, B.zeros(n), acc) : List<&2, U32>}:
551  match n:
552    case 0n:
553      {==}
554    case 1n+p:
555      Equal.trans(List<&2, U32>, B.zeros.go(p, Con{0, acc}), List.append(&2, U32, B.zeros(p), Con{0, acc}), Con{0, List.append(&2, U32, B.zeros(p), acc)},
556        g_zerosu(p, Con{0, acc}), zeros_consu(p, acc))
557
558def p_zeros_fast(+n: Nat) -> {B.zeros(n) == B.zeros.fast(n) : List<&2, U32>}:
559  Equal.sym(List<&2, U32>, B.zeros.fast(n), B.zeros(n),
560    Equal.trans(List<&2, U32>, B.zeros.go(n, Nil{}), List.append(&2, U32, B.zeros(n), Nil{}), B.zeros(n), g_zerosu(n, Nil{}), app_nilu(B.zeros(n))))
561
562def Laws.zeros_fast(n):
563  p_zeros_fast(n)
564
565def g_mask(+xs: List<&2, U32>, +acc: List<&2, U32>) -> {B.mask.go(xs, acc) == B.rev_onto(B.mask(xs), acc) : List<&2, U32>}:
566  match xs:
567    case Nil{}:
568      {==}
569    case Con{h, t}:
570      g_mask(t, Con{B.byte(h), acc})
571
572def p_mask_fast(+xs: List<&2, U32>) -> {B.mask(xs) == B.mask.fast(xs) : List<&2, U32>}:
573  Equal.sym(List<&2, U32>, B.mask.fast(xs), B.mask(xs),
574    Equal.trans(List<&2, U32>, B.mask.fast(xs), B.rev_onto(B.rev_onto(B.mask(xs), Nil{}), Nil{}), B.mask(xs),
575      Equal.cong(List<&2, U32>, List<&2, U32>, l => B.rev_onto(l, Nil{}), B.mask.go(xs, Nil{}), B.rev_onto(B.mask(xs), Nil{}), g_mask(xs, Nil{})),
576      rr_back(B.mask(xs))))
577
578def Laws.mask_fast(xs):
579  p_mask_fast(xs)
580
581def g_of_string(+s: String, +acc: List<&2, U32>) -> {B.of_string.go(s, acc) == B.rev_onto(B.of_string(s), acc) : List<&2, U32>}:
582  match s:
583    case SNil{}:
584      {==}
585    case SCon{Chr{c}, t}:
586      g_of_string(t, Con{B.byte(c), acc})
587
588def p_of_string_fast(+s: String) -> {B.of_string(s) == B.of_string.fast(s) : List<&2, U32>}:
589  Equal.sym(List<&2, U32>, B.of_string.fast(s), B.of_string(s),
590    Equal.trans(List<&2, U32>, B.of_string.fast(s), B.rev_onto(B.rev_onto(B.of_string(s), Nil{}), Nil{}), B.of_string(s),
591      Equal.cong(List<&2, U32>, List<&2, U32>, l => B.rev_onto(l, Nil{}), B.of_string.go(s, Nil{}), B.rev_onto(B.of_string(s), Nil{}), g_of_string(s, Nil{})),
592      rr_back(B.of_string(s))))
593
594def Laws.of_string_fast(s):
595  p_of_string_fast(s)
596
597# text: building from the back onto acc is the structural cat
598def t_go(+xs: List<&2, U32>, +r: List<&2, U32>, +acc: String) -> {B.to_string.go(B.rev_onto(xs, r), acc) == B.to_string.go(r, B.to_string.cat(xs, acc)) : String}:
599  match xs:
600    case Nil{}:
601      {==}
602    case Con{h, t}:
603      t_go(t, Con{h, r}, acc)
604
605def t_cat(+xs: List<&2, U32>) -> {B.to_string.cat(xs, SNil{}) == B.to_string(xs) : String}:
606  match xs:
607    case Nil{}:
608      {==}
609    case Con{h, t}:
610      Equal.cong(String, String, x => SCon{Chr{B.byte(h)}, x}, B.to_string.cat(t, SNil{}), B.to_string(t), t_cat(t))
611
612def p_to_string_fast(+xs: List<&2, U32>) -> {B.to_string(xs) == B.to_string.fast(xs) : String}:
613  Equal.sym(String, B.to_string.fast(xs), B.to_string(xs),
614    Equal.trans(String, B.to_string.go(B.rev_onto(xs, Nil{}), SNil{}), B.to_string.cat(xs, SNil{}), B.to_string(xs), t_go(xs, Nil{}, SNil{}), t_cat(xs)))
615
616def Laws.to_string_fast(xs):
617  p_to_string_fast(xs)
618
619def h_go(+xs: List<&2, U32>, +r: List<&2, U32>, +acc: String) -> {B.hex.go(B.rev_onto(xs, r), acc) == B.hex.go(r, B.hex.cat(xs, acc)) : String}:
620  match xs:
621    case Nil{}:
622      {==}
623    case Con{h, t}:
624      h_go(t, Con{h, r}, acc)
625
626def h_cat(+xs: List<&2, U32>) -> {B.hex.cat(xs, SNil{}) == B.hex(xs) : String}:
627  match xs:
628    case Nil{}:
629      {==}
630    case Con{h, t}:
631      Equal.cong(String, String, x => SCon{B.hex.digit(U32.shrn(B.byte(h), 4n)), SCon{B.hex.digit(U32.and(B.byte(h), 15)), x}}, B.hex.cat(t, SNil{}), B.hex(t), h_cat(t))
632
633def p_hex_fast(+xs: List<&2, U32>) -> {B.hex(xs) == B.hex.fast(xs) : String}:
634  Equal.sym(String, B.hex.fast(xs), B.hex(xs),
635    Equal.trans(String, B.hex.go(B.rev_onto(xs, Nil{}), SNil{}), B.hex.cat(xs, SNil{}), B.hex(xs), h_go(xs, Nil{}, SNil{}), h_cat(xs)))
636
637def Laws.hex_fast(xs):
638  p_hex_fast(xs)
639
640def eq_go(+xs: List<&2, U32>, +ys: List<&2, U32>, +ok: Bool) -> {B.list_eq.go(xs, ys, ok) == Bool.and(ok, B.list_eq(xs, ys)) : Bool}:
641  match xs ys:
642    case Nil{} Nil{}:
643      match ok:
644        case True{}:
645          {==}
646        case False{}:
647          {==}
648    case Con{a, s} Con{b, t}:
649      match ok:
650        case True{}:
651          eq_go(s, t, U32.is_eq(a, b))
652        case False{}:
653          eq_go(s, t, False{})
654    case Nil{} Con{b, t}:
655      match ok:
656        case True{}:
657          {==}
658        case False{}:
659          {==}
660    case Con{a, s} Nil{}:
661      match ok:
662        case True{}:
663          {==}
664        case False{}:
665          {==}
666
667def p_list_eq_fast(+xs: List<&2, U32>, +ys: List<&2, U32>) -> {B.list_eq(xs, ys) == B.list_eq.fast(xs, ys) : Bool}:
668  Equal.sym(Bool, B.list_eq.fast(xs, ys), B.list_eq(xs, ys), eq_go(xs, ys, True{}))
669
670def Laws.list_eq_fast(xs, ys):
671  p_list_eq_fast(xs, ys)
672
673def Laws.rev_rev(xs):
674  rr_back(xs)
675
676# Octets' text and hex: each word read through bits8/of_bits8 is its byte
677def w_t_go(+ws: List<&2, B.OctByte>, +r: List<&2, B.OctByte>, +acc: String) -> {B.w8s.text.go(B.w8s.rev_onto(ws, r), acc) == B.w8s.text.go(r, B.to_string.cat(B.w8s.to_list(ws), acc)) : String}:
678  match ws:
679    case Nil{}:
680      {==}
681    case Con{B.OctByte{a0, a1, a2, a3, a4, a5, a6, a7}, t}:
682      w_t_go(t, Con{B.OctByte{a0, a1, a2, a3, a4, a5, a6, a7}, r}, acc)
683
684def p_octets_to_string_list(+o: B.Octets) -> {B.Octets.to_string(o) == B.to_string(B.Octets.to_list(o)) : String}:
685  match o:
686    case B.Octets{+ws}:
687      %F_to(ws) : {B.w8s.text.go(B.w8s.rev_onto(ws, Nil{}), SNil{}) == B.to_string(_) : String}
688      Equal.trans(String, B.w8s.text.go(B.w8s.rev_onto(ws, Nil{}), SNil{}), B.to_string.cat(B.w8s.to_list(ws), SNil{}), B.to_string(B.w8s.to_list(ws)), w_t_go(ws, Nil{}, SNil{}), t_cat(B.w8s.to_list(ws)))
689
690def Laws.octets_to_string_list(o):
691  p_octets_to_string_list(o)
692
693def w_h_go(+ws: List<&2, B.OctByte>, +r: List<&2, B.OctByte>, +acc: String) -> {B.w8s.hex.go(B.w8s.rev_onto(ws, r), acc) == B.w8s.hex.go(r, B.hex.cat(B.w8s.to_list(ws), acc)) : String}:
694  match ws:
695    case Nil{}:
696      {==}
697    case Con{B.OctByte{a0, a1, a2, a3, a4, a5, a6, a7}, t}:
698      w_h_go(t, Con{B.OctByte{a0, a1, a2, a3, a4, a5, a6, a7}, r}, acc)
699
700def p_octets_hex_list(+o: B.Octets) -> {B.Octets.hex(o) == B.hex(B.Octets.to_list(o)) : String}:
701  match o:
702    case B.Octets{+ws}:
703      %F_to(ws) : {B.w8s.hex.go(B.w8s.rev_onto(ws, Nil{}), SNil{}) == B.hex(_) : String}
704      Equal.trans(String, B.w8s.hex.go(B.w8s.rev_onto(ws, Nil{}), SNil{}), B.hex.cat(B.w8s.to_list(ws), SNil{}), B.hex(B.w8s.to_list(ws)), w_h_go(ws, Nil{}, SNil{}), h_cat(B.w8s.to_list(ws)))
705
706def Laws.octets_hex_list(o):
707  p_octets_hex_list(o)
708
709# concat: pushing each piece's words is reversing the joined words
710def rev_app8(+xs: List<&2, B.OctByte>, +ys: List<&2, B.OctByte>, +acc: List<&2, B.OctByte>) -> {B.w8s.rev_onto(List.append(&2, B.OctByte, xs, ys), acc) == B.w8s.rev_onto(ys, B.w8s.rev_onto(xs, acc)) : List<&2, B.OctByte>}:
711  match xs:
712    case Nil{}:
713      {==}
714    case Con{h, t}:
715      rev_app8(t, ys, Con{h, acc})
716
717def concat_step(+ws: List<&2, B.OctByte>, +c: B.Octets, +acc: List<&2, B.OctByte>) -> {B.w8s.rev_onto(B.Octets.words(c), B.w8s.rev_onto(ws, acc)) == B.w8s.rev_onto(B.Octets.words(B.Octets.append(B.Octets{ws}, c)), acc) : List<&2, B.OctByte>}:
718  match c:
719    case B.Octets{+zs}:
720      %F_app(ws, zs) : {B.w8s.rev_onto(zs, B.w8s.rev_onto(ws, acc)) == B.w8s.rev_onto(_, acc) : List<&2, B.OctByte>}
721      Equal.sym(List<&2, B.OctByte>, B.w8s.rev_onto(List.append(&2, B.OctByte, ws, zs), acc), B.w8s.rev_onto(zs, B.w8s.rev_onto(ws, acc)), rev_app8(ws, zs, acc))
722
723def concat_go(+os: List<&2, B.Octets>, +acc: List<&2, B.OctByte>) -> {B.w8s.concat.go(os, acc) == B.w8s.rev_onto(B.Octets.words(B.Octets.concat.ref(os)), acc) : List<&2, B.OctByte>}:
724  match os:
725    case Nil{}:
726      {==}
727    case Con{B.Octets{+ws}, t}:
728      Equal.trans(List<&2, B.OctByte>, B.w8s.concat.go(t, B.w8s.rev_onto(ws, acc)), B.w8s.rev_onto(B.Octets.words(B.Octets.concat.ref(t)), B.w8s.rev_onto(ws, acc)), B.w8s.rev_onto(B.Octets.words(B.Octets.append(B.Octets{ws}, B.Octets.concat.ref(t))), acc),
729        concat_go(t, B.w8s.rev_onto(ws, acc)), concat_step(ws, B.Octets.concat.ref(t), acc))
730
731def octets_eta(+o: B.Octets) -> {B.Octets{B.Octets.words(o)} == o : B.Octets}:
732  match o:
733    case B.Octets{ws}:
734      {==}
735
736def rr8_back(+zs: List<&2, B.OctByte>) -> {B.w8s.rev_onto(B.w8s.rev_onto(zs, Nil{}), Nil{}) == zs : List<&2, B.OctByte>}:
737  Equal.trans(List<&2, B.OctByte>, B.w8s.rev_onto(B.w8s.rev_onto(zs, Nil{}), Nil{}), List.append(&2, B.OctByte, zs, Nil{}), zs, r8_rr(zs, Nil{}, Nil{}), app_nil8(zs))
738
739def concat_ref(+os: List<&2, B.Octets>) -> {B.Octets.concat(os) == B.Octets.concat.ref(os) : B.Octets}:
740  Equal.trans(B.Octets, B.Octets.concat(os), B.Octets{B.Octets.words(B.Octets.concat.ref(os))}, B.Octets.concat.ref(os),
741    Equal.cong(List<&2, B.OctByte>, B.Octets, l => B.Octets{l}, B.w8s.rev_onto(B.w8s.concat.go(os, Nil{}), Nil{}), B.Octets.words(B.Octets.concat.ref(os)),
742      Equal.trans(List<&2, B.OctByte>, B.w8s.rev_onto(B.w8s.concat.go(os, Nil{}), Nil{}), B.w8s.rev_onto(B.w8s.rev_onto(B.Octets.words(B.Octets.concat.ref(os)), Nil{}), Nil{}), B.Octets.words(B.Octets.concat.ref(os)),
743        Equal.cong(List<&2, B.OctByte>, List<&2, B.OctByte>, l => B.w8s.rev_onto(l, Nil{}), B.w8s.concat.go(os, Nil{}), B.w8s.rev_onto(B.Octets.words(B.Octets.concat.ref(os)), Nil{}), concat_go(os, Nil{})),
744        rr8_back(B.Octets.words(B.Octets.concat.ref(os))))),
745    octets_eta(B.Octets.concat.ref(os)))
746
747def Laws.octets_concat_nil():
748  {==}
749
750def p_octets_concat_cons(+h: B.Octets, +t: List<&2, B.Octets>) -> {B.Octets.concat(Con{h, t}) == B.Octets.append(h, B.Octets.concat(t)) : B.Octets}:
751  %Equal.sym(B.Octets, B.Octets.concat(t), B.Octets.concat.ref(t), concat_ref(t)) : {B.Octets.concat(Con{h, t}) == B.Octets.append(h, _) : B.Octets}
752  concat_ref(Con{h, t})
753
754def Laws.octets_concat_cons(h, t):
755  p_octets_concat_cons(h, t)
756
757# Reading at offsets: lemmas
758
759def off.disc(b: Bool) -> Type:
760  match b:
761    case True{}:
762      Unit
763    case False{}:
764      Empty
765
766def off.clash(h: {False{} == True{} : Bool}) -> Empty:
767  %Equal.sym(Bool, False{}, True{}, h) : off.disc(_)
768  Unit{}
769
770def off.absurd(-A: Type, e: Empty) -> A:
771  match e:
772
773def off.no(-A: Type, h: {False{} == True{} : Bool}) -> A:
774  off.absurd(A, off.clash(h))
775
776# Natural numbers
777
778def off.le_zero(+m: Nat) -> {Nat.is_le(0n, m) == True{} : Bool}:
779  match m:
780    case 0n:
781      {==}
782    case 1n+p:
783      {==}
784
785# i + n <= m: i <= m
786def off.le_add_l(+i: Nat, +n: Nat, +m: Nat) -> {Nat.is_le(Nat.add(i, n), m) == True{} : Bool} -> {Nat.is_le(i, m) == True{} : Bool}:
787  match i m:
788    case 0n _:
789      h => off.le_zero(m)
790    case 1n+p 0n:
791      h => off.no({Nat.is_le(1n+p, 0n) == True{} : Bool}, h)
792    case 1n+p 1n+q:
793      h => off.le_add_l(p, n, q, h)
794
795# i + n <= m: n <= m - i
796def off.le_sub(+i: Nat, +n: Nat, +m: Nat) -> {Nat.is_le(Nat.add(i, n), m) == True{} : Bool} -> {Nat.is_le(n, Nat.sub(m, i)) == True{} : Bool}:
797  match i m:
798    case 0n 0n:
799      h => h
800    case 0n 1n+q:
801      h => h
802    case 1n+p 0n:
803      h => off.no({Nat.is_le(n, Nat.sub(0n, 1n+p)) == True{} : Bool}, h)
804    case 1n+p 1n+q:
805      h => off.le_sub(p, n, q, h)
806
807# n <= k: min(n, k) == n
808def off.min_le(+n: Nat, +k: Nat) -> {Nat.is_le(n, k) == True{} : Bool} -> {Nat.min(n, k) == n : Nat}:
809  match n k:
810    case 0n _:
811      h => {==}
812    case 1n+p 0n:
813      h => off.no({Nat.min(1n+p, 0n) == 1n+p : Nat}, h)
814    case 1n+p 1n+q:
815      h => Equal.cong(Nat, Nat, x => 1n+x, Nat.min(p, q), p, off.min_le(p, q, h))
816
817# Word lists
818
819def off.drop_nil(+i: Nat) -> {B.w8s.drop(i, Nil{}) == Nil{} : List<&2, B.OctByte>}:
820  match i:
821    case 0n:
822      {==}
823    case 1n+p:
824      {==}
825
826def off.take_nil(+i: Nat) -> {B.w8s.take(i, Nil{}) == Nil{} : List<&2, B.OctByte>}:
827  match i:
828    case 0n:
829      {==}
830    case 1n+p:
831      {==}
832
833def off.drop_app_add(xs: List<&2, B.OctByte>, +n: Nat, +ys: List<&2, B.OctByte>) -> {B.w8s.drop(Nat.add(List.length(&2, B.OctByte, xs), n), List.append(&2, B.OctByte, xs, ys)) == B.w8s.drop(n, ys) : List<&2, B.OctByte>}:
834  match xs:
835    case Nil{}:
836      {==}
837    case Con{h, t}:
838      off.drop_app_add(t, n, ys)
839
840def off.take_app_add(xs: List<&2, B.OctByte>, +n: Nat, +ys: List<&2, B.OctByte>) -> {B.w8s.take(Nat.add(List.length(&2, B.OctByte, xs), n), List.append(&2, B.OctByte, xs, ys)) == List.append(&2, B.OctByte, xs, B.w8s.take(n, ys)) : List<&2, B.OctByte>}:
841  match xs:
842    case Nil{}:
843      {==}
844    case Con{h, t}:
845      Equal.cong(List<&2, B.OctByte>, List<&2, B.OctByte>, l => Con{h, l}, B.w8s.take(Nat.add(List.length(&2, B.OctByte, t), n), List.append(&2, B.OctByte, t, ys)), List.append(&2, B.OctByte, t, B.w8s.take(n, ys)), off.take_app_add(t, n, ys))
846
847def off.take_app_le(+n: Nat, xs: List<&2, B.OctByte>, +ys: List<&2, B.OctByte>) -> {Nat.is_le(n, List.length(&2, B.OctByte, xs)) == True{} : Bool} -> {B.w8s.take(n, List.append(&2, B.OctByte, xs, ys)) == B.w8s.take(n, xs) : List<&2, B.OctByte>}:
848  match n xs:
849    case 0n _:
850      h => {==}
851    case 1n+p Nil{}:
852      h => off.no({B.w8s.take(1n+p, ys) == Nil{} : List<&2, B.OctByte>}, h)
853    case 1n+p Con{x, t}:
854      h => Equal.cong(List<&2, B.OctByte>, List<&2, B.OctByte>, l => Con{x, l}, B.w8s.take(p, List.append(&2, B.OctByte, t, ys)), B.w8s.take(p, t), off.take_app_le(p, t, ys, h))
855
856def off.drop_app_le(+n: Nat, xs: List<&2, B.OctByte>, +ys: List<&2, B.OctByte>) -> {Nat.is_le(n, List.length(&2, B.OctByte, xs)) == True{} : Bool} -> {B.w8s.drop(n, List.append(&2, B.OctByte, xs, ys)) == List.append(&2, B.OctByte, B.w8s.drop(n, xs), ys) : List<&2, B.OctByte>}:
857  match n xs:
858    case 0n _:
859      h => {==}
860    case 1n+p Nil{}:
861      h => off.no({B.w8s.drop(1n+p, ys) == ys : List<&2, B.OctByte>}, h)
862    case 1n+p Con{x, t}:
863      h => off.drop_app_le(p, t, ys, h)
864
865def off.drop_drop(+j: Nat, +i: Nat, ws: List<&2, B.OctByte>) -> {B.w8s.drop(i, B.w8s.drop(j, ws)) == B.w8s.drop(Nat.add(j, i), ws) : List<&2, B.OctByte>}:
866  match j ws:
867    case 0n _:
868      {==}
869    case 1n+q Nil{}:
870      off.drop_nil(i)
871    case 1n+q Con{x, t}:
872      off.drop_drop(q, i, t)
873
874def off.take_take(+i: Nat, +j: Nat, ws: List<&2, B.OctByte>) -> {B.w8s.take(i, B.w8s.take(j, ws)) == B.w8s.take(Nat.min(i, j), ws) : List<&2, B.OctByte>}:
875  match i j ws:
876    case 0n _ _:
877      {==}
878    case 1n+p 0n _:
879      {==}
880    case 1n+p 1n+q Nil{}:
881      {==}
882    case 1n+p 1n+q Con{x, t}:
883      Equal.cong(List<&2, B.OctByte>, List<&2, B.OctByte>, l => Con{x, l}, B.w8s.take(p, B.w8s.take(q, t)), B.w8s.take(Nat.min(p, q), t), off.take_take(p, q, t))
884
885def off.take_drop(+i: Nat, +j: Nat, ws: List<&2, B.OctByte>) -> {B.w8s.take(i, B.w8s.drop(j, ws)) == B.w8s.drop(j, B.w8s.take(Nat.add(j, i), ws)) : List<&2, B.OctByte>}:
886  match j ws:
887    case 0n _:
888      {==}
889    case 1n+q Nil{}:
890      off.take_nil(i)
891    case 1n+q Con{x, t}:
892      off.take_drop(i, q, t)
893
894def off.drop_take(+i: Nat, +j: Nat, ws: List<&2, B.OctByte>) -> {B.w8s.drop(i, B.w8s.take(j, ws)) == B.w8s.take(Nat.sub(j, i), B.w8s.drop(i, ws)) : List<&2, B.OctByte>}:
895  match i j ws:
896    case 0n 0n _:
897      {==}
898    case 0n 1n+q _:
899      {==}
900    case 1n+p 0n _:
901      {==}
902    case 1n+p 1n+q Nil{}:
903      Equal.sym(List<&2, B.OctByte>, B.w8s.take(Nat.sub(q, p), Nil{}), Nil{}, off.take_nil(Nat.sub(q, p)))
904    case 1n+p 1n+q Con{x, t}:
905      off.drop_take(p, q, t)
906
907def off.len_take(+n: Nat, ws: List<&2, B.OctByte>) -> {List.length(&2, B.OctByte, B.w8s.take(n, ws)) == Nat.min(n, List.length(&2, B.OctByte, ws)) : Nat}:
908  match n ws:
909    case 0n _:
910      {==}
911    case 1n+p Nil{}:
912      {==}
913    case 1n+p Con{x, t}:
914      Equal.cong(Nat, Nat, k => 1n+k, List.length(&2, B.OctByte, B.w8s.take(p, t)), Nat.min(p, List.length(&2, B.OctByte, t)), off.len_take(p, t))
915
916def off.len_drop(+n: Nat, ws: List<&2, B.OctByte>) -> {List.length(&2, B.OctByte, B.w8s.drop(n, ws)) == Nat.sub(List.length(&2, B.OctByte, ws), n) : Nat}:
917  match n ws:
918    case 0n Nil{}:
919      {==}
920    case 0n Con{x, t}:
921      {==}
922    case 1n+p Nil{}:
923      {==}
924    case 1n+p Con{x, t}:
925      off.len_drop(p, t)
926
927def off.len_zeros(+n: Nat) -> {List.length(&2, B.OctByte, B.w8s.zeros(n)) == n : Nat}:
928  match n:
929    case 0n:
930      {==}
931    case 1n+p:
932      Equal.cong(Nat, Nat, k => 1n+k, List.length(&2, B.OctByte, B.w8s.zeros(p)), p, off.len_zeros(p))
933
934def off.len_of(xs: List<&2, U32>) -> {List.length(&2, B.OctByte, B.w8s.of_list(xs)) == B.len(xs) : Nat}:
935  match xs:
936    case Nil{}:
937      {==}
938    case Con{h, t}:
939      Equal.cong(Nat, Nat, k => 1n+k, List.length(&2, B.OctByte, B.w8s.of_list(t)), B.len(t), off.len_of(t))
940
941def off.app_assoc(xs: List<&2, B.OctByte>, +ys: List<&2, B.OctByte>, +zs: List<&2, B.OctByte>) -> {List.append(&2, B.OctByte, List.append(&2, B.OctByte, xs, ys), zs) == List.append(&2, B.OctByte, xs, List.append(&2, B.OctByte, ys, zs)) : List<&2, B.OctByte>}:
942  match xs:
943    case Nil{}:
944      {==}
945    case Con{h, t}:
946      Equal.cong(List<&2, B.OctByte>, List<&2, B.OctByte>, l => Con{h, l}, List.append(&2, B.OctByte, List.append(&2, B.OctByte, t, ys), zs), List.append(&2, B.OctByte, t, List.append(&2, B.OctByte, ys, zs)), off.app_assoc(t, ys, zs))
947
948# a byte: at the head of what is left after the offset
949
950def off.at_app_lt(+i: Nat, xs: List<&2, B.OctByte>, +ys: List<&2, B.OctByte>) -> {Nat.is_lt(i, List.length(&2, B.OctByte, xs)) == True{} : Bool} -> {B.w8s.at(B.w8s.drop(i, List.append(&2, B.OctByte, xs, ys))) == B.w8s.at(B.w8s.drop(i, xs)) : Maybe<&2, U32>}:
951  match i xs:
952    case 0n Nil{}:
953      h => off.no({B.w8s.at(ys) == None{} : Maybe<&2, U32>}, h)
954    case 1n+p Nil{}:
955      h => off.no({B.w8s.at(B.w8s.drop(1n+p, ys)) == None{} : Maybe<&2, U32>}, h)
956    case 0n Con{x, t}:
957      h => {==}
958    case 1n+p Con{x, t}:
959      h => off.at_app_lt(p, t, ys, h)
960
961def off.at_take(+i: Nat, +n: Nat, ws: List<&2, B.OctByte>) -> {Nat.is_lt(i, n) == True{} : Bool} -> {B.w8s.at(B.w8s.drop(i, B.w8s.take(n, ws))) == B.w8s.at(B.w8s.drop(i, ws)) : Maybe<&2, U32>}:
962  match i n ws:
963    case 0n 0n _:
964      h => off.no({B.w8s.at(Nil{}) == B.w8s.at(ws) : Maybe<&2, U32>}, h)
965    case 1n+p 0n _:
966      h => off.no({B.w8s.at(B.w8s.drop(1n+p, Nil{})) == B.w8s.at(B.w8s.drop(1n+p, ws)) : Maybe<&2, U32>}, h)
967    case 0n 1n+q Nil{}:
968      h => {==}
969    case 0n 1n+q Con{x, t}:
970      h => {==}
971    case 1n+p 1n+q Nil{}:
972      h => {==}
973    case 1n+p 1n+q Con{x, t}:
974      h => off.at_take(p, q, t, h)
975
976def off.at_to(+i: Nat, ws: List<&2, B.OctByte>) -> {B.w8s.at(B.w8s.drop(i, ws)) == B.at(B.w8s.to_list(ws), i) : Maybe<&2, U32>}:
977  match i ws:
978    case 0n Nil{}:
979      {==}
980    case 1n+p Nil{}:
981      {==}
982    case 0n Con{B.OctByte{a0, a1, a2, a3, a4, a5, a6, a7}, t}:
983      {==}
984    case 1n+p Con{x, t}:
985      off.at_to(p, t)
986
987# The list layer
988
989def off.ldrop_app_add(a: List<&2, U32>, +n: Nat, +b: List<&2, U32>) -> {B.drop(Nat.add(B.len(a), n), B.append(a, b)) == B.drop(n, b) : List<&2, U32>}:
990  match a:
991    case Nil{}:
992      {==}
993    case Con{h, t}:
994      off.ldrop_app_add(t, n, b)
995
996def off.lat_app_lt(+i: Nat, a: List<&2, U32>, +b: List<&2, U32>) -> {Nat.is_lt(i, B.len(a)) == True{} : Bool} -> {B.at(B.append(a, b), i) == B.at(a, i) : Maybe<&2, U32>}:
997  match i a:
998    case 0n Nil{}:
999      h => off.no({B.at(b, 0n) == None{} : Maybe<&2, U32>}, h)
1000    case 1n+p Nil{}:
1001      h => off.no({B.at(b, 1n+p) == B.at(Nil{}, 1n+p) : Maybe<&2, U32>}, h)
1002    case 0n Con{x, t}:
1003      h => {==}
1004    case 1n+p Con{x, t}:
1005      h => off.lat_app_lt(p, t, b, h)
1006
1007def off.ldrop_nil(+i: Nat) -> {B.drop(i, Nil{}) == Nil{} : List<&2, U32>}:
1008  match i:
1009    case 0n:
1010      {==}
1011    case 1n+p:
1012      {==}
1013
1014def off.ldrop_drop(+j: Nat, +i: Nat, xs: List<&2, U32>) -> {B.drop(i, B.drop(j, xs)) == B.drop(Nat.add(j, i), xs) : List<&2, U32>}:
1015  match j xs:
1016    case 0n _:
1017      {==}
1018    case 1n+q Nil{}:
1019      off.ldrop_nil(i)
1020    case 1n+q Con{x, t}:
1021      off.ldrop_drop(q, i, t)
1022
1023def off.lat_take(+i: Nat, +n: Nat, xs: List<&2, U32>) -> {Nat.is_lt(i, n) == True{} : Bool} -> {B.at(B.take(n, xs), i) == B.at(xs, i) : Maybe<&2, U32>}:
1024  match i n xs:
1025    case 0n 0n _:
1026      h => off.no({B.at(Nil{}, 0n) == B.at(xs, 0n) : Maybe<&2, U32>}, h)
1027    case 1n+p 0n _:
1028      h => off.no({B.at(Nil{}, 1n+p) == B.at(xs, 1n+p) : Maybe<&2, U32>}, h)
1029    case 0n 1n+q Nil{}:
1030      h => {==}
1031    case 0n 1n+q Con{x, t}:
1032      h => {==}
1033    case 1n+p 1n+q Nil{}:
1034      h => {==}
1035    case 1n+p 1n+q Con{x, t}:
1036      h => off.lat_take(p, q, t, h)
1037
1038def off.llen_app(a: List<&2, U32>, +b: List<&2, U32>) -> {B.len(B.append(a, b)) == Nat.add(B.len(a), B.len(b)) : Nat}:
1039  match a:
1040    case Nil{}:
1041      {==}
1042    case Con{h, t}:
1043      Equal.cong(Nat, Nat, k => 1n+k, B.len(B.append(t, b)), Nat.add(B.len(t), B.len(b)), off.llen_app(t, b))
1044
1045def off.llen_le32(+v: U32) -> {B.len(B.le32(v)) == 4n : Nat}:
1046  match v:
1047    case U32{w}:
1048      {==}
1049
1050def off.llen_be32(+v: U32) -> {B.len(B.be32(v)) == 4n : Nat}:
1051  match v:
1052    case U32{w}:
1053      {==}
1054
1055def off.llen_le16(+v: U32) -> {B.len(B.le16(v)) == 2n : Nat}:
1056  match v:
1057    case U32{w}:
1058      {==}
1059
1060def off.llen_be16(+v: U32) -> {B.len(B.be16(v)) == 2n : Nat}:
1061  match v:
1062    case U32{w}:
1063      {==}
1064
1065def off.add_le32(+x: U32, +y: U32) -> {Nat.add(B.len(B.le32(x)), B.len(B.le32(y))) == 8n : Nat}:
1066  match x y:
1067    case U32{a} U32{b}:
1068      {==}
1069
1070def off.add_be32(+x: U32, +y: U32) -> {Nat.add(B.len(B.be32(x)), B.len(B.be32(y))) == 8n : Nat}:
1071  match x y:
1072    case U32{a} U32{b}:
1073      {==}
1074
1075def off.llen_le64(+v: W.W64) -> {B.len(B.le64(v)) == 8n : Nat}:
1076  Equal.trans(Nat, B.len(B.le64(v)), Nat.add(B.len(B.le32(W.W64.lo(v))), B.len(B.le32(W.W64.hi(v)))), 8n, off.llen_app(B.le32(W.W64.lo(v)), B.le32(W.W64.hi(v))), off.add_le32(W.W64.lo(v), W.W64.hi(v)))
1077
1078def off.llen_be64(+v: W.W64) -> {B.len(B.be64(v)) == 8n : Nat}:
1079  Equal.trans(Nat, B.len(B.be64(v)), Nat.add(B.len(B.be32(W.W64.hi(v))), B.len(B.be32(W.W64.lo(v)))), 8n, off.llen_app(B.be32(W.W64.hi(v)), B.be32(W.W64.lo(v))), off.add_be32(W.W64.hi(v), W.W64.lo(v)))
1080
1081# Octets: lengths
1082
1083def p_len_append(+a: B.Octets, +b: B.Octets) -> {B.Octets.len(B.Octets.append(a, b)) == Nat.add(B.Octets.len(a), B.Octets.len(b)) : Nat}:
1084  match a b:
1085    case B.Octets{+xs} B.Octets{+ys}:
1086      %F_app(xs, ys) : {B.w8s.len.fast(_) == Nat.add(B.w8s.len.fast(xs), B.w8s.len.fast(ys)) : Nat}
1087      %F_len(List.append(&2, B.OctByte, xs, ys)) : {_ == Nat.add(B.w8s.len.fast(xs), B.w8s.len.fast(ys)) : Nat}
1088      %F_len(xs) : {List.length(&2, B.OctByte, List.append(&2, B.OctByte, xs, ys)) == Nat.add(_, B.w8s.len.fast(ys)) : Nat}
1089      %F_len(ys) : {List.length(&2, B.OctByte, List.append(&2, B.OctByte, xs, ys)) == Nat.add(List.length(&2, B.OctByte, xs), _) : Nat}
1090      w8s_len_app(xs, ys)
1091
1092def p_len_take(+n: Nat, +o: B.Octets) -> {B.Octets.len(B.Octets.take(n, o)) == Nat.min(n, B.Octets.len(o)) : Nat}:
1093  match o:
1094    case B.Octets{+ws}:
1095      %F_take(n, ws) : {B.w8s.len.fast(_) == Nat.min(n, B.w8s.len.fast(ws)) : Nat}
1096      %F_len(B.w8s.take(n, ws)) : {_ == Nat.min(n, B.w8s.len.fast(ws)) : Nat}
1097      %F_len(ws) : {List.length(&2, B.OctByte, B.w8s.take(n, ws)) == Nat.min(n, _) : Nat}
1098      off.len_take(n, ws)
1099
1100def p_len_drop(+n: Nat, +o: B.Octets) -> {B.Octets.len(B.Octets.drop(n, o)) == Nat.sub(B.Octets.len(o), n) : Nat}:
1101  match o:
1102    case B.Octets{+ws}:
1103      %F_len(B.w8s.drop(n, ws)) : {_ == Nat.sub(B.w8s.len.fast(ws), n) : Nat}
1104      %F_len(ws) : {List.length(&2, B.OctByte, B.w8s.drop(n, ws)) == Nat.sub(_, n) : Nat}
1105      off.len_drop(n, ws)
1106
1107def p_len_take_le(+n: Nat, +o: B.Octets, h: {Nat.is_le(n, B.Octets.len(o)) == True{} : Bool}) -> {B.Octets.len(B.Octets.take(n, o)) == n : Nat}:
1108  Equal.trans(Nat, B.Octets.len(B.Octets.take(n, o)), Nat.min(n, B.Octets.len(o)), n, p_len_take(n, o), off.min_le(n, B.Octets.len(o), h))
1109
1110def p_len_slice(+i: Nat, +n: Nat, +o: B.Octets) -> {B.Octets.len(B.Octets.slice(i, n, o)) == Nat.min(n, Nat.sub(B.Octets.len(o), i)) : Nat}:
1111  Equal.trans(Nat, B.Octets.len(B.Octets.take(n, B.Octets.drop(i, o))), Nat.min(n, B.Octets.len(B.Octets.drop(i, o))), Nat.min(n, Nat.sub(B.Octets.len(o), i)),
1112    p_len_take(n, B.Octets.drop(i, o)),
1113    Equal.cong(Nat, Nat, k => Nat.min(n, k), B.Octets.len(B.Octets.drop(i, o)), Nat.sub(B.Octets.len(o), i), p_len_drop(i, o)))
1114
1115def p_len_slice_le(+i: Nat, +n: Nat, +o: B.Octets, h: {Nat.is_le(Nat.add(i, n), B.Octets.len(o)) == True{} : Bool}) -> {B.Octets.len(B.Octets.slice(i, n, o)) == n : Nat}:
1116  Equal.trans(Nat, B.Octets.len(B.Octets.slice(i, n, o)), Nat.min(n, Nat.sub(B.Octets.len(o), i)), n, p_len_slice(i, n, o), off.min_le(n, Nat.sub(B.Octets.len(o), i), off.le_sub(i, n, B.Octets.len(o), h)))
1117
1118def p_len_zeros(+n: Nat) -> {B.Octets.len(B.Octets.zeros(n)) == n : Nat}:
1119  %F_zeros(n) : {B.w8s.len.fast(_) == n : Nat}
1120  %F_len(B.w8s.zeros(n)) : {_ == n : Nat}
1121  off.len_zeros(n)
1122
1123def p_len_of_list(+xs: List<&2, U32>) -> {B.Octets.len(B.Octets.of_list(xs)) == B.len(xs) : Nat}:
1124  %F_of(xs) : {B.w8s.len.fast(_) == B.len(xs) : Nat}
1125  %F_len(B.w8s.of_list(xs)) : {_ == B.len(xs) : Nat}
1126  off.len_of(xs)
1127
1128def p_append_assoc(+a: B.Octets, +b: B.Octets, +c: B.Octets) -> {B.Octets.append(B.Octets.append(a, b), c) == B.Octets.append(a, B.Octets.append(b, c)) : B.Octets}:
1129  match a b c:
1130    case B.Octets{+xs} B.Octets{+ys} B.Octets{+zs}:
1131      %F_app(xs, ys) : {B.Octets{B.w8s.append.fast(_, zs)} == B.Octets{B.w8s.append.fast(xs, B.w8s.append.fast(ys, zs))} : B.Octets}
1132      %F_app(ys, zs) : {B.Octets{B.w8s.append.fast(List.append(&2, B.OctByte, xs, ys), zs)} == B.Octets{B.w8s.append.fast(xs, _)} : B.Octets}
1133      %F_app(List.append(&2, B.OctByte, xs, ys), zs) : {B.Octets{_} == B.Octets{B.w8s.append.fast(xs, List.append(&2, B.OctByte, ys, zs))} : B.Octets}
1134      %F_app(xs, List.append(&2, B.OctByte, ys, zs)) : {B.Octets{List.append(&2, B.OctByte, List.append(&2, B.OctByte, xs, ys), zs)} == B.Octets{_} : B.Octets}
1135      Equal.cong(List<&2, B.OctByte>, B.Octets, l => B.Octets{l}, List.append(&2, B.OctByte, List.append(&2, B.OctByte, xs, ys), zs), List.append(&2, B.OctByte, xs, List.append(&2, B.OctByte, ys, zs)), off.app_assoc(xs, ys, zs))
1136
1137# Octets: take and drop composed
1138
1139def p_drop_drop(+j: Nat, +i: Nat, +o: B.Octets) -> {B.Octets.drop(i, B.Octets.drop(j, o)) == B.Octets.drop(Nat.add(j, i), o) : B.Octets}:
1140  match o:
1141    case B.Octets{+ws}:
1142      Equal.cong(List<&2, B.OctByte>, B.Octets, l => B.Octets{l}, B.w8s.drop(i, B.w8s.drop(j, ws)), B.w8s.drop(Nat.add(j, i), ws), off.drop_drop(j, i, ws))
1143
1144def p_take_take(+i: Nat, +j: Nat, +o: B.Octets) -> {B.Octets.take(i, B.Octets.take(j, o)) == B.Octets.take(Nat.min(i, j), o) : B.Octets}:
1145  match o:
1146    case B.Octets{+ws}:
1147      %F_take(j, ws) : {B.Octets{B.w8s.take.fast(i, _)} == B.Octets{B.w8s.take.fast(Nat.min(i, j), ws)} : B.Octets}
1148      %F_take(i, B.w8s.take(j, ws)) : {B.Octets{_} == B.Octets{B.w8s.take.fast(Nat.min(i, j), ws)} : B.Octets}
1149      %F_take(Nat.min(i, j), ws) : {B.Octets{B.w8s.take(i, B.w8s.take(j, ws))} == B.Octets{_} : B.Octets}
1150      Equal.cong(List<&2, B.OctByte>, B.Octets, l => B.Octets{l}, B.w8s.take(i, B.w8s.take(j, ws)), B.w8s.take(Nat.min(i, j), ws), off.take_take(i, j, ws))
1151
1152def p_take_drop(+i: Nat, +j: Nat, +o: B.Octets) -> {B.Octets.take(i, B.Octets.drop(j, o)) == B.Octets.drop(j, B.Octets.take(Nat.add(j, i), o)) : B.Octets}:
1153  match o:
1154    case B.Octets{+ws}:
1155      %F_take(i, B.w8s.drop(j, ws)) : {B.Octets{_} == B.Octets{B.w8s.drop(j, B.w8s.take.fast(Nat.add(j, i), ws))} : B.Octets}
1156      %F_take(Nat.add(j, i), ws) : {B.Octets{B.w8s.take(i, B.w8s.drop(j, ws))} == B.Octets{B.w8s.drop(j, _)} : B.Octets}
1157      Equal.cong(List<&2, B.OctByte>, B.Octets, l => B.Octets{l}, B.w8s.take(i, B.w8s.drop(j, ws)), B.w8s.drop(j, B.w8s.take(Nat.add(j, i), ws)), off.take_drop(i, j, ws))
1158
1159def p_drop_take(+i: Nat, +j: Nat, +o: B.Octets) -> {B.Octets.drop(i, B.Octets.take(j, o)) == B.Octets.take(Nat.sub(j, i), B.Octets.drop(i, o)) : B.Octets}:
1160  match o:
1161    case B.Octets{+ws}:
1162      %F_take(j, ws) : {B.Octets{B.w8s.drop(i, _)} == B.Octets{B.w8s.take.fast(Nat.sub(j, i), B.w8s.drop(i, ws))} : B.Octets}
1163      %F_take(Nat.sub(j, i), B.w8s.drop(i, ws)) : {B.Octets{B.w8s.drop(i, B.w8s.take(j, ws))} == B.Octets{_} : B.Octets}
1164      Equal.cong(List<&2, B.OctByte>, B.Octets, l => B.Octets{l}, B.w8s.drop(i, B.w8s.take(j, ws)), B.w8s.take(Nat.sub(j, i), B.w8s.drop(i, ws)), off.drop_take(i, j, ws))
1165
1166# Octets: take and drop inside joined bytes
1167
1168def off.len_fast_le(+n: Nat, +xs: List<&2, B.OctByte>, h: {Nat.is_le(n, B.w8s.len.fast(xs)) == True{} : Bool}) -> {Nat.is_le(n, List.length(&2, B.OctByte, xs)) == True{} : Bool}:
1169  Equal.trans(Bool, Nat.is_le(n, List.length(&2, B.OctByte, xs)), Nat.is_le(n, B.w8s.len.fast(xs)), True{}, Equal.cong(Nat, Bool, k => Nat.is_le(n, k), List.length(&2, B.OctByte, xs), B.w8s.len.fast(xs), F_len(xs)), h)
1170
1171def off.len_fast_lt(+n: Nat, +xs: List<&2, B.OctByte>, h: {Nat.is_lt(n, B.w8s.len.fast(xs)) == True{} : Bool}) -> {Nat.is_lt(n, List.length(&2, B.OctByte, xs)) == True{} : Bool}:
1172  Equal.trans(Bool, Nat.is_lt(n, List.length(&2, B.OctByte, xs)), Nat.is_lt(n, B.w8s.len.fast(xs)), True{}, Equal.cong(Nat, Bool, k => Nat.is_lt(n, k), List.length(&2, B.OctByte, xs), B.w8s.len.fast(xs), F_len(xs)), h)
1173
1174def q_take_app_le(+n: Nat, +xs: List<&2, B.OctByte>, +ys: List<&2, B.OctByte>, h: {Nat.is_le(n, List.length(&2, B.OctByte, xs)) == True{} : Bool}) -> {B.Octets{B.w8s.take.fast(n, B.w8s.append.fast(xs, ys))} == B.Octets{B.w8s.take.fast(n, xs)} : B.Octets}:
1175  %F_app(xs, ys) : {B.Octets{B.w8s.take.fast(n, _)} == B.Octets{B.w8s.take.fast(n, xs)} : B.Octets}
1176  %F_take(n, List.append(&2, B.OctByte, xs, ys)) : {B.Octets{_} == B.Octets{B.w8s.take.fast(n, xs)} : B.Octets}
1177  %F_take(n, xs) : {B.Octets{B.w8s.take(n, List.append(&2, B.OctByte, xs, ys))} == B.Octets{_} : B.Octets}
1178  Equal.cong(List<&2, B.OctByte>, B.Octets, l => B.Octets{l}, B.w8s.take(n, List.append(&2, B.OctByte, xs, ys)), B.w8s.take(n, xs), off.take_app_le(n, xs, ys, h))
1179
1180def p_take_append_le(+n: Nat, +a: B.Octets, +b: B.Octets) -> {Nat.is_le(n, B.Octets.len(a)) == True{} : Bool} -> {B.Octets.take(n, B.Octets.append(a, b)) == B.Octets.take(n, a) : B.Octets}:
1181  match a b:
1182    case B.Octets{+xs} B.Octets{+ys}:
1183      h => q_take_app_le(n, xs, ys, off.len_fast_le(n, xs, h))
1184
1185def p_take_append_add(+a: B.Octets, +n: Nat, +b: B.Octets) -> {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}:
1186  match a b:
1187    case B.Octets{+xs} B.Octets{+ys}:
1188      %F_app(xs, ys) : {B.Octets{B.w8s.take.fast(Nat.add(B.w8s.len.fast(xs), n), _)} == B.Octets{B.w8s.append.fast(xs, B.w8s.take.fast(n, ys))} : B.Octets}
1189      %F_len(xs) : {B.Octets{B.w8s.take.fast(Nat.add(_, n), List.append(&2, B.OctByte, xs, ys))} == B.Octets{B.w8s.append.fast(xs, B.w8s.take.fast(n, ys))} : B.Octets}
1190      %F_take(Nat.add(List.length(&2, B.OctByte, xs), n), List.append(&2, B.OctByte, xs, ys)) : {B.Octets{_} == B.Octets{B.w8s.append.fast(xs, B.w8s.take.fast(n, ys))} : B.Octets}
1191      %F_take(n, ys) : {B.Octets{B.w8s.take(Nat.add(List.length(&2, B.OctByte, xs), n), List.append(&2, B.OctByte, xs, ys))} == B.Octets{B.w8s.append.fast(xs, _)} : B.Octets}
1192      %F_app(xs, B.w8s.take(n, ys)) : {B.Octets{B.w8s.take(Nat.add(List.length(&2, B.OctByte, xs), n), List.append(&2, B.OctByte, xs, ys))} == B.Octets{_} : B.Octets}
1193      Equal.cong(List<&2, B.OctByte>, B.Octets, l => B.Octets{l}, B.w8s.take(Nat.add(List.length(&2, B.OctByte, xs), n), List.append(&2, B.OctByte, xs, ys)), List.append(&2, B.OctByte, xs, B.w8s.take(n, ys)), off.take_app_add(xs, n, ys))
1194
1195def q_drop_app_le(+n: Nat, +xs: List<&2, B.OctByte>, +ys: List<&2, B.OctByte>, h: {Nat.is_le(n, List.length(&2, B.OctByte, xs)) == True{} : Bool}) -> {B.Octets{B.w8s.drop(n, B.w8s.append.fast(xs, ys))} == B.Octets{B.w8s.append.fast(B.w8s.drop(n, xs), ys)} : B.Octets}:
1196  %F_app(xs, ys) : {B.Octets{B.w8s.drop(n, _)} == B.Octets{B.w8s.append.fast(B.w8s.drop(n, xs), ys)} : B.Octets}
1197  %F_app(B.w8s.drop(n, xs), ys) : {B.Octets{B.w8s.drop(n, List.append(&2, B.OctByte, xs, ys))} == B.Octets{_} : B.Octets}
1198  Equal.cong(List<&2, B.OctByte>, B.Octets, l => B.Octets{l}, B.w8s.drop(n, List.append(&2, B.OctByte, xs, ys)), List.append(&2, B.OctByte, B.w8s.drop(n, xs), ys), off.drop_app_le(n, xs, ys, h))
1199
1200def p_drop_append_le(+n: Nat, +a: B.Octets, +b: B.Octets) -> {Nat.is_le(n, B.Octets.len(a)) == True{} : Bool} -> {B.Octets.drop(n, B.Octets.append(a, b)) == B.Octets.append(B.Octets.drop(n, a), b) : B.Octets}:
1201  match a b:
1202    case B.Octets{+xs} B.Octets{+ys}:
1203      h => q_drop_app_le(n, xs, ys, off.len_fast_le(n, xs, h))
1204
1205def p_drop_append_add(+a: B.Octets, +n: Nat, +b: B.Octets) -> {B.Octets.drop(Nat.add(B.Octets.len(a), n), B.Octets.append(a, b)) == B.Octets.drop(n, b) : B.Octets}:
1206  match a b:
1207    case B.Octets{+xs} B.Octets{+ys}:
1208      %F_app(xs, ys) : {B.Octets{B.w8s.drop(Nat.add(B.w8s.len.fast(xs), n), _)} == B.Octets{B.w8s.drop(n, ys)} : B.Octets}
1209      %F_len(xs) : {B.Octets{B.w8s.drop(Nat.add(_, n), List.append(&2, B.OctByte, xs, ys))} == B.Octets{B.w8s.drop(n, ys)} : B.Octets}
1210      Equal.cong(List<&2, B.OctByte>, B.Octets, l => B.Octets{l}, B.w8s.drop(Nat.add(List.length(&2, B.OctByte, xs), n), List.append(&2, B.OctByte, xs, ys)), B.w8s.drop(n, ys), off.drop_app_add(xs, n, ys))
1211
1212# Octets: slices
1213
1214def p_slice_append_add(+a: B.Octets, +i: Nat, +n: Nat, +b: B.Octets) -> {B.Octets.slice(Nat.add(B.Octets.len(a), i), n, B.Octets.append(a, b)) == B.Octets.slice(i, n, b) : B.Octets}:
1215  Equal.cong(B.Octets, B.Octets, x => B.Octets.take(n, x), B.Octets.drop(Nat.add(B.Octets.len(a), i), B.Octets.append(a, b)), B.Octets.drop(i, b), p_drop_append_add(a, i, b))
1216
1217def p_slice_append_le(+i: Nat, +n: Nat, +a: B.Octets, +b: B.Octets, +h: {Nat.is_le(Nat.add(i, n), B.Octets.len(a)) == True{} : Bool}) -> {B.Octets.slice(i, n, B.Octets.append(a, b)) == B.Octets.slice(i, n, a) : B.Octets}:
1218  Equal.trans(B.Octets, B.Octets.take(n, B.Octets.drop(i, B.Octets.append(a, b))), B.Octets.take(n, B.Octets.append(B.Octets.drop(i, a), b)), B.Octets.take(n, B.Octets.drop(i, a)),
1219    Equal.cong(B.Octets, B.Octets, x => B.Octets.take(n, x), B.Octets.drop(i, B.Octets.append(a, b)), B.Octets.append(B.Octets.drop(i, a), b), p_drop_append_le(i, a, b, off.le_add_l(i, n, B.Octets.len(a), h))),
1220    p_take_append_le(n, B.Octets.drop(i, a), b,
1221      Equal.trans(Bool, Nat.is_le(n, B.Octets.len(B.Octets.drop(i, a))), Nat.is_le(n, Nat.sub(B.Octets.len(a), i)), True{},
1222        Equal.cong(Nat, Bool, k => Nat.is_le(n, k), B.Octets.len(B.Octets.drop(i, a)), Nat.sub(B.Octets.len(a), i), p_len_drop(i, a)),
1223        off.le_sub(i, n, B.Octets.len(a), h))))
1224
1225def p_slice_drop(+j: Nat, +i: Nat, +n: Nat, +o: B.Octets) -> {B.Octets.slice(i, n, B.Octets.drop(j, o)) == B.Octets.slice(Nat.add(j, i), n, o) : B.Octets}:
1226  Equal.cong(B.Octets, B.Octets, x => B.Octets.take(n, x), B.Octets.drop(i, B.Octets.drop(j, o)), B.Octets.drop(Nat.add(j, i), o), p_drop_drop(j, i, o))
1227
1228def p_slice_take(+m: Nat, +i: Nat, +n: Nat, +o: B.Octets, +h: {Nat.is_le(Nat.add(i, n), m) == True{} : Bool}) -> {B.Octets.slice(i, n, B.Octets.take(m, o)) == B.Octets.slice(i, n, o) : B.Octets}:
1229  Equal.trans(B.Octets, B.Octets.take(n, B.Octets.drop(i, B.Octets.take(m, o))), B.Octets.take(n, B.Octets.take(Nat.sub(m, i), B.Octets.drop(i, o))), B.Octets.take(n, B.Octets.drop(i, o)),
1230    Equal.cong(B.Octets, B.Octets, x => B.Octets.take(n, x), B.Octets.drop(i, B.Octets.take(m, o)), B.Octets.take(Nat.sub(m, i), B.Octets.drop(i, o)), p_drop_take(i, m, o)),
1231    Equal.trans(B.Octets, B.Octets.take(n, B.Octets.take(Nat.sub(m, i), B.Octets.drop(i, o))), B.Octets.take(Nat.min(n, Nat.sub(m, i)), B.Octets.drop(i, o)), B.Octets.take(n, B.Octets.drop(i, o)),
1232      p_take_take(n, Nat.sub(m, i), B.Octets.drop(i, o)),
1233      Equal.cong(Nat, B.Octets, k => B.Octets.take(k, B.Octets.drop(i, o)), Nat.min(n, Nat.sub(m, i)), n, off.min_le(n, Nat.sub(m, i), off.le_sub(i, n, m, h)))))
1234
1235# Octets: a byte at an offset
1236
1237def p_at_list(+o: B.Octets, +i: Nat) -> {B.Octets.at(o, i) == B.at(B.Octets.to_list(o), i) : Maybe<&2, U32>}:
1238  match o:
1239    case B.Octets{+ws}:
1240      %F_to(ws) : {B.w8s.at(B.w8s.drop(i, ws)) == B.at(_, i) : Maybe<&2, U32>}
1241      off.at_to(i, ws)
1242
1243def p_at_append_add(+a: B.Octets, +b: B.Octets, +i: Nat) -> {B.Octets.at(B.Octets.append(a, b), Nat.add(B.Octets.len(a), i)) == B.Octets.at(b, i) : Maybe<&2, U32>}:
1244  match a b:
1245    case B.Octets{+xs} B.Octets{+ys}:
1246      %F_app(xs, ys) : {B.w8s.at(B.w8s.drop(Nat.add(B.w8s.len.fast(xs), i), _)) == B.w8s.at(B.w8s.drop(i, ys)) : Maybe<&2, U32>}
1247      %F_len(xs) : {B.w8s.at(B.w8s.drop(Nat.add(_, i), List.append(&2, B.OctByte, xs, ys))) == B.w8s.at(B.w8s.drop(i, ys)) : Maybe<&2, U32>}
1248      Equal.cong(List<&2, B.OctByte>, Maybe<&2, U32>, l => B.w8s.at(l), B.w8s.drop(Nat.add(List.length(&2, B.OctByte, xs), i), List.append(&2, B.OctByte, xs, ys)), B.w8s.drop(i, ys), off.drop_app_add(xs, i, ys))
1249
1250def q_at_app_lt(+i: Nat, +xs: List<&2, B.OctByte>, +ys: List<&2, B.OctByte>, h: {Nat.is_lt(i, List.length(&2, B.OctByte, xs)) == True{} : Bool}) -> {B.w8s.at(B.w8s.drop(i, B.w8s.append.fast(xs, ys))) == B.w8s.at(B.w8s.drop(i, xs)) : Maybe<&2, U32>}:
1251  %F_app(xs, ys) : {B.w8s.at(B.w8s.drop(i, _)) == B.w8s.at(B.w8s.drop(i, xs)) : Maybe<&2, U32>}
1252  off.at_app_lt(i, xs, ys, h)
1253
1254def p_at_append_lt(+a: B.Octets, +b: B.Octets, +i: Nat) -> {Nat.is_lt(i, B.Octets.len(a)) == True{} : Bool} -> {B.Octets.at(B.Octets.append(a, b), i) == B.Octets.at(a, i) : Maybe<&2, U32>}:
1255  match a b:
1256    case B.Octets{+xs} B.Octets{+ys}:
1257      h => q_at_app_lt(i, xs, ys, off.len_fast_lt(i, xs, h))
1258
1259def p_at_drop(+j: Nat, +o: B.Octets, +i: Nat) -> {B.Octets.at(B.Octets.drop(j, o), i) == B.Octets.at(o, Nat.add(j, i)) : Maybe<&2, U32>}:
1260  match o:
1261    case B.Octets{+ws}:
1262      Equal.cong(List<&2, B.OctByte>, Maybe<&2, U32>, l => B.w8s.at(l), B.w8s.drop(i, B.w8s.drop(j, ws)), B.w8s.drop(Nat.add(j, i), ws), off.drop_drop(j, i, ws))
1263
1264def p_at_take(+n: Nat, +o: B.Octets, +i: Nat, h: {Nat.is_lt(i, n) == True{} : Bool}) -> {B.Octets.at(B.Octets.take(n, o), i) == B.Octets.at(o, i) : Maybe<&2, U32>}:
1265  match o:
1266    case B.Octets{+ws}:
1267      %F_take(n, ws) : {B.w8s.at(B.w8s.drop(i, _)) == B.w8s.at(B.w8s.drop(i, ws)) : Maybe<&2, U32>}
1268      off.at_take(i, n, ws, h)
1269
1270# Every word ANDed with zero is zero (for low16_mask)
1271
1272def off.band_f(+b: Bool) -> {Bool.and(b, False{}) == False{} : Bool}:
1273  match b:
1274    case True{}:
1275      {==}
1276    case False{}:
1277      {==}
1278
1279def off.wand_zero(+n: Nat, w: Word(n)) -> {Word.and(n, w, Word.zero(n)) == Word.zero(n) : Word(n)}:
1280  match n:
1281    case 0n:
1282      {==}
1283    case 1n+p:
1284      match w:
1285        case WCon{+b, t}:
1286          %Equal.sym(Bool, Bool.and(b, False{}), False{}, off.band_f(b)) : {WCon{_, Word.and(p, t, Word.zero(p))} == Word.zero(1n+p) : Word(1n+p)}
1287          Equal.cong(Word(p), Word(1n+p), z => WCon{False{}, z}, Word.and(p, t, Word.zero(p)), Word.zero(p), off.wand_zero(p, t))
1288
1289# The laws
1290
1291def Laws.octets_len_append(a, b):
1292  p_len_append(a, b)
1293
1294def Laws.octets_len_take(n, o):
1295  p_len_take(n, o)
1296
1297def Laws.octets_len_take_le(n, o, h):
1298  p_len_take_le(n, o, h)
1299
1300def Laws.octets_len_drop(n, o):
1301  p_len_drop(n, o)
1302
1303def Laws.octets_len_slice(i, n, o):
1304  p_len_slice(i, n, o)
1305
1306def Laws.octets_len_slice_le(i, n, o, h):
1307  p_len_slice_le(i, n, o, h)
1308
1309def Laws.octets_len_zeros(n):
1310  p_len_zeros(n)
1311
1312def Laws.octets_len_of_list(xs):
1313  p_len_of_list(xs)
1314
1315def Laws.octets_append_assoc(a, b, c):
1316  p_append_assoc(a, b, c)
1317
1318def p_append_empty_l(+o: B.Octets) -> {B.Octets.append(B.Octets.empty(), o) == o : B.Octets}:
1319  match o:
1320    case B.Octets{+ws}:
1321      %F_app(Nil{}, ws) : {B.Octets{_} == B.Octets{ws} : B.Octets}
1322      {==}
1323
1324def p_append_empty_r(+o: B.Octets) -> {B.Octets.append(o, B.Octets.empty()) == o : B.Octets}:
1325  match o:
1326    case B.Octets{+ws}:
1327      %F_app(ws, Nil{}) : {B.Octets{_} == B.Octets{ws} : B.Octets}
1328      Equal.cong(List<&2, B.OctByte>, B.Octets, l => B.Octets{l}, List.append(&2, B.OctByte, ws, Nil{}), ws, app_nil8(ws))
1329
1330def off.take_len(ws: List<&2, B.OctByte>) -> {B.w8s.take(List.length(&2, B.OctByte, ws), ws) == ws : List<&2, B.OctByte>}:
1331  match ws:
1332    case Nil{}:
1333      {==}
1334    case Con{h, t}:
1335      Equal.cong(List<&2, B.OctByte>, List<&2, B.OctByte>, l => Con{h, l}, B.w8s.take(List.length(&2, B.OctByte, t), t), t, off.take_len(t))
1336
1337def p_take_len(+o: B.Octets) -> {B.Octets.take(B.Octets.len(o), o) == o : B.Octets}:
1338  match o:
1339    case B.Octets{+ws}:
1340      %F_take(B.w8s.len.fast(ws), ws) : {B.Octets{_} == B.Octets{ws} : B.Octets}
1341      %F_len(ws) : {B.Octets{B.w8s.take(_, ws)} == B.Octets{ws} : B.Octets}
1342      Equal.cong(List<&2, B.OctByte>, B.Octets, l => B.Octets{l}, B.w8s.take(List.length(&2, B.OctByte, ws), ws), ws, off.take_len(ws))
1343
1344def Laws.octets_drop_zero(o):
1345  match o:
1346    case B.Octets{ws}:
1347      {==}
1348
1349def Laws.octets_take_len(o):
1350  p_take_len(o)
1351
1352def Laws.octets_append_empty_l(o):
1353  p_append_empty_l(o)
1354
1355def Laws.octets_append_empty_r(o):
1356  p_append_empty_r(o)
1357
1358def Laws.octets_drop_drop(j, i, o):
1359  p_drop_drop(j, i, o)
1360
1361def Laws.octets_take_take(i, j, o):
1362  p_take_take(i, j, o)
1363
1364def Laws.octets_take_drop_comm(i, j, o):
1365  p_take_drop(i, j, o)
1366
1367def Laws.octets_drop_take_comm(i, j, o):
1368  p_drop_take(i, j, o)
1369
1370def Laws.octets_take_append_le(n, a, b, h):
1371  p_take_append_le(n, a, b, h)
1372
1373def Laws.octets_take_append_add(a, n, b):
1374  p_take_append_add(a, n, b)
1375
1376def Laws.octets_drop_append_le(n, a, b, h):
1377  p_drop_append_le(n, a, b, h)
1378
1379def Laws.octets_drop_append_add(a, n, b):
1380  p_drop_append_add(a, n, b)
1381
1382def Laws.octets_slice_append_add(a, i, n, b):
1383  p_slice_append_add(a, i, n, b)
1384
1385def Laws.octets_slice_append_le(i, n, a, b, h):
1386  p_slice_append_le(i, n, a, b, h)
1387
1388def Laws.octets_slice_drop(j, i, n, o):
1389  p_slice_drop(j, i, n, o)
1390
1391def Laws.octets_slice_take(m, i, n, o, h):
1392  p_slice_take(m, i, n, o, h)
1393
1394def Laws.octets_at_list(o, i):
1395  p_at_list(o, i)
1396
1397def Laws.octets_at_append_add(a, b, i):
1398  p_at_append_add(a, b, i)
1399
1400def Laws.octets_at_append_lt(a, b, i, h):
1401  p_at_append_lt(a, b, i, h)
1402
1403def Laws.octets_at_drop(j, o, i):
1404  p_at_drop(j, o, i)
1405
1406def Laws.octets_at_take(n, o, i, h):
1407  p_at_take(n, o, i, h)
1408
1409def Laws.at_append_add(a, b, i):
1410  Equal.cong(List<&2, U32>, Maybe<&2, U32>, l => B.at.head(l), B.drop(Nat.add(B.len(a), i), B.append(a, b)), B.drop(i, b), off.ldrop_app_add(a, i, b))
1411
1412def Laws.at_append_lt(a, b, i, h):
1413  off.lat_app_lt(i, a, b, h)
1414
1415def Laws.at_drop(j, xs, i):
1416  Equal.cong(List<&2, U32>, Maybe<&2, U32>, l => B.at.head(l), B.drop(i, B.drop(j, xs)), B.drop(Nat.add(j, i), xs), off.ldrop_drop(j, i, xs))
1417
1418def Laws.at_take(n, xs, i, h):
1419  off.lat_take(i, n, xs, h)
1420
1421def Laws.octets_len_le16(v):
1422  Equal.trans(Nat, B.Octets.len(B.Octets.of_list(B.le16(v))), B.len(B.le16(v)), 2n, p_len_of_list(B.le16(v)), off.llen_le16(v))
1423
1424def Laws.octets_len_be16(v):
1425  Equal.trans(Nat, B.Octets.len(B.Octets.of_list(B.be16(v))), B.len(B.be16(v)), 2n, p_len_of_list(B.be16(v)), off.llen_be16(v))
1426
1427def Laws.octets_len_le32(v):
1428  Equal.trans(Nat, B.Octets.len(B.Octets.of_list(B.le32(v))), B.len(B.le32(v)), 4n, p_len_of_list(B.le32(v)), off.llen_le32(v))
1429
1430def Laws.octets_len_be32(v):
1431  Equal.trans(Nat, B.Octets.len(B.Octets.of_list(B.be32(v))), B.len(B.be32(v)), 4n, p_len_of_list(B.be32(v)), off.llen_be32(v))
1432
1433def Laws.octets_len_le64(v):
1434  Equal.trans(Nat, B.Octets.len(B.Octets.of_list(B.le64(v))), B.len(B.le64(v)), 8n, p_len_of_list(B.le64(v)), off.llen_le64(v))
1435
1436def Laws.octets_len_be64(v):
1437  Equal.trans(Nat, B.Octets.len(B.Octets.of_list(B.be64(v))), B.len(B.be64(v)), 8n, p_len_of_list(B.be64(v)), off.llen_be64(v))
1438
1439def Laws.octets_le16_at_append_add(a, b, i):
1440  Equal.cong(B.Octets, Maybe<&2, U32>, s => B.le16.head(B.Octets.to_list(s)), B.Octets.slice(Nat.add(B.Octets.len(a), i), 2n, B.Octets.append(a, b)), B.Octets.slice(i, 2n, b), p_slice_append_add(a, i, 2n, b))
1441
1442def Laws.octets_le16_at_append_le(a, b, i, h):
1443  Equal.cong(B.Octets, Maybe<&2, U32>, s => B.le16.head(B.Octets.to_list(s)), B.Octets.slice(i, 2n, B.Octets.append(a, b)), B.Octets.slice(i, 2n, a), p_slice_append_le(i, 2n, a, b, h))
1444
1445def Laws.octets_le16_at_drop(j, o, i):
1446  Equal.cong(B.Octets, Maybe<&2, U32>, s => B.le16.head(B.Octets.to_list(s)), B.Octets.slice(i, 2n, B.Octets.drop(j, o)), B.Octets.slice(Nat.add(j, i), 2n, o), p_slice_drop(j, i, 2n, o))
1447
1448def Laws.octets_le16_at_take(n, o, i, h):
1449  Equal.cong(B.Octets, Maybe<&2, U32>, s => B.le16.head(B.Octets.to_list(s)), B.Octets.slice(i, 2n, B.Octets.take(n, o)), B.Octets.slice(i, 2n, o), p_slice_take(n, i, 2n, o, h))
1450
1451def Laws.octets_be16_at_append_add(a, b, i):
1452  Equal.cong(B.Octets, Maybe<&2, U32>, s => B.be16.head(B.Octets.to_list(s)), B.Octets.slice(Nat.add(B.Octets.len(a), i), 2n, B.Octets.append(a, b)), B.Octets.slice(i, 2n, b), p_slice_append_add(a, i, 2n, b))
1453
1454def Laws.octets_be16_at_append_le(a, b, i, h):
1455  Equal.cong(B.Octets, Maybe<&2, U32>, s => B.be16.head(B.Octets.to_list(s)), B.Octets.slice(i, 2n, B.Octets.append(a, b)), B.Octets.slice(i, 2n, a), p_slice_append_le(i, 2n, a, b, h))
1456
1457def Laws.octets_be16_at_drop(j, o, i):
1458  Equal.cong(B.Octets, Maybe<&2, U32>, s => B.be16.head(B.Octets.to_list(s)), B.Octets.slice(i, 2n, B.Octets.drop(j, o)), B.Octets.slice(Nat.add(j, i), 2n, o), p_slice_drop(j, i, 2n, o))
1459
1460def Laws.octets_be16_at_take(n, o, i, h):
1461  Equal.cong(B.Octets, Maybe<&2, U32>, s => B.be16.head(B.Octets.to_list(s)), B.Octets.slice(i, 2n, B.Octets.take(n, o)), B.Octets.slice(i, 2n, o), p_slice_take(n, i, 2n, o, h))
1462
1463def Laws.octets_le32_at_append_add(a, b, i):
1464  Equal.cong(B.Octets, Maybe<&2, U32>, s => B.le32.head(B.Octets.to_list(s)), B.Octets.slice(Nat.add(B.Octets.len(a), i), 4n, B.Octets.append(a, b)), B.Octets.slice(i, 4n, b), p_slice_append_add(a, i, 4n, b))
1465
1466def Laws.octets_le32_at_append_le(a, b, i, h):
1467  Equal.cong(B.Octets, Maybe<&2, U32>, s => B.le32.head(B.Octets.to_list(s)), B.Octets.slice(i, 4n, B.Octets.append(a, b)), B.Octets.slice(i, 4n, a), p_slice_append_le(i, 4n, a, b, h))
1468
1469def Laws.octets_le32_at_drop(j, o, i):
1470  Equal.cong(B.Octets, Maybe<&2, U32>, s => B.le32.head(B.Octets.to_list(s)), B.Octets.slice(i, 4n, B.Octets.drop(j, o)), B.Octets.slice(Nat.add(j, i), 4n, o), p_slice_drop(j, i, 4n, o))
1471
1472def Laws.octets_le32_at_take(n, o, i, h):
1473  Equal.cong(B.Octets, Maybe<&2, U32>, s => B.le32.head(B.Octets.to_list(s)), B.Octets.slice(i, 4n, B.Octets.take(n, o)), B.Octets.slice(i, 4n, o), p_slice_take(n, i, 4n, o, h))
1474
1475def Laws.octets_be32_at_append_add(a, b, i):
1476  Equal.cong(B.Octets, Maybe<&2, U32>, s => B.be32.head(B.Octets.to_list(s)), B.Octets.slice(Nat.add(B.Octets.len(a), i), 4n, B.Octets.append(a, b)), B.Octets.slice(i, 4n, b), p_slice_append_add(a, i, 4n, b))
1477
1478def Laws.octets_be32_at_append_le(a, b, i, h):
1479  Equal.cong(B.Octets, Maybe<&2, U32>, s => B.be32.head(B.Octets.to_list(s)), B.Octets.slice(i, 4n, B.Octets.append(a, b)), B.Octets.slice(i, 4n, a), p_slice_append_le(i, 4n, a, b, h))
1480
1481def Laws.octets_be32_at_drop(j, o, i):
1482  Equal.cong(B.Octets, Maybe<&2, U32>, s => B.be32.head(B.Octets.to_list(s)), B.Octets.slice(i, 4n, B.Octets.drop(j, o)), B.Octets.slice(Nat.add(j, i), 4n, o), p_slice_drop(j, i, 4n, o))
1483
1484def Laws.octets_be32_at_take(n, o, i, h):
1485  Equal.cong(B.Octets, Maybe<&2, U32>, s => B.be32.head(B.Octets.to_list(s)), B.Octets.slice(i, 4n, B.Octets.take(n, o)), B.Octets.slice(i, 4n, o), p_slice_take(n, i, 4n, o, h))
1486
1487def Laws.octets_le64_at_append_add(a, b, i):
1488  Equal.cong(B.Octets, Maybe<&2, W.W64>, s => B.le64_at(B.Octets.to_list(s), 0n), B.Octets.slice(Nat.add(B.Octets.len(a), i), 8n, B.Octets.append(a, b)), B.Octets.slice(i, 8n, b), p_slice_append_add(a, i, 8n, b))
1489
1490def Laws.octets_le64_at_append_le(a, b, i, h):
1491  Equal.cong(B.Octets, Maybe<&2, W.W64>, s => B.le64_at(B.Octets.to_list(s), 0n), B.Octets.slice(i, 8n, B.Octets.append(a, b)), B.Octets.slice(i, 8n, a), p_slice_append_le(i, 8n, a, b, h))
1492
1493def Laws.octets_le64_at_drop(j, o, i):
1494  Equal.cong(B.Octets, Maybe<&2, W.W64>, s => B.le64_at(B.Octets.to_list(s), 0n), B.Octets.slice(i, 8n, B.Octets.drop(j, o)), B.Octets.slice(Nat.add(j, i), 8n, o), p_slice_drop(j, i, 8n, o))
1495
1496def Laws.octets_le64_at_take(n, o, i, h):
1497  Equal.cong(B.Octets, Maybe<&2, W.W64>, s => B.le64_at(B.Octets.to_list(s), 0n), B.Octets.slice(i, 8n, B.Octets.take(n, o)), B.Octets.slice(i, 8n, o), p_slice_take(n, i, 8n, o, h))
1498
1499def Laws.octets_be64_at_append_add(a, b, i):
1500  Equal.cong(B.Octets, Maybe<&2, W.W64>, s => B.be64_at(B.Octets.to_list(s), 0n), B.Octets.slice(Nat.add(B.Octets.len(a), i), 8n, B.Octets.append(a, b)), B.Octets.slice(i, 8n, b), p_slice_append_add(a, i, 8n, b))
1501
1502def Laws.octets_be64_at_append_le(a, b, i, h):
1503  Equal.cong(B.Octets, Maybe<&2, W.W64>, s => B.be64_at(B.Octets.to_list(s), 0n), B.Octets.slice(i, 8n, B.Octets.append(a, b)), B.Octets.slice(i, 8n, a), p_slice_append_le(i, 8n, a, b, h))
1504
1505def Laws.octets_be64_at_drop(j, o, i):
1506  Equal.cong(B.Octets, Maybe<&2, W.W64>, s => B.be64_at(B.Octets.to_list(s), 0n), B.Octets.slice(i, 8n, B.Octets.drop(j, o)), B.Octets.slice(Nat.add(j, i), 8n, o), p_slice_drop(j, i, 8n, o))
1507
1508def Laws.octets_be64_at_take(n, o, i, h):
1509  Equal.cong(B.Octets, Maybe<&2, W.W64>, s => B.be64_at(B.Octets.to_list(s), 0n), B.Octets.slice(i, 8n, B.Octets.take(n, o)), B.Octets.slice(i, 8n, o), p_slice_take(n, i, 8n, o, h))
1510
1511def Laws.low16_mask(v):
1512  match v:
1513    case U32{WCon{x0, WCon{x1, WCon{x2, WCon{x3, WCon{x4, WCon{x5, WCon{x6, WCon{x7, WCon{x8, WCon{x9, WCon{x10, WCon{x11, WCon{x12, WCon{x13, WCon{x14, WCon{x15, t}}}}}}}}}}}}}}}}}:
1514      Equal.cong(Word(16n), U32, z => U32{WCon{Bool.and(x0, True{}), WCon{Bool.and(x1, True{}), WCon{Bool.and(x2, True{}), WCon{Bool.and(x3, True{}), WCon{Bool.and(x4, True{}), WCon{Bool.and(x5, True{}), WCon{Bool.and(x6, True{}), WCon{Bool.and(x7, True{}), WCon{Bool.and(x8, True{}), WCon{Bool.and(x9, True{}), WCon{Bool.and(x10, True{}), WCon{Bool.and(x11, True{}), WCon{Bool.and(x12, True{}), WCon{Bool.and(x13, True{}), WCon{Bool.and(x14, True{}), WCon{Bool.and(x15, True{}), z}}}}}}}}}}}}}}}}}, Word.zero(16n), Word.and(16n, t, Word.zero(16n)), Equal.sym(Word(16n), Word.and(16n, t, Word.zero(16n)), Word.zero(16n), off.wand_zero(16n, t)))