PROOF.bend
bend-osdev-bytes@0.1.1.1 · 1,514 lines · 0 definitions
1import Base
2import bend-osdev-word64@0.1.1.1/word64.bend as W
3import bend-osdev-word64@0.1.1.1/LAWS.bend as WL
4import bend-osdev-word64@0.1.1.1/PROOF.bend as WP
5import bend-osdev-bytes@0.1.1.1/bytes.bend as B
6import bend-osdev-bytes@0.1.1.1/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)))