PROOF.bend
bend-osdev-acpi@0.1.0.0 · 2,653 lines · 0 definitions
1import Base
2import bend-osdev-word64@0.1.0.0/word64.bend as W
3import bend-osdev-bytes@0.1.0.0/bytes.bend as B
4import bend-osdev-bytes@0.1.0.0/LAWS.bend as BL
5import bend-osdev-bytes@0.1.0.0/PROOF.bend as BP
6import bend-osdev-acpi@0.1.0.0/error.bend as E
7import bend-osdev-acpi@0.1.0.0/aml_pkglength.bend as K
8import bend-osdev-acpi@0.1.0.0/aml_name.bend as N
9import bend-osdev-acpi@0.1.0.0/header.bend as H
10import bend-osdev-acpi@0.1.0.0/checksum.bend as C
11import bend-osdev-acpi@0.1.0.0/fields.bend as F
12import bend-osdev-acpi@0.1.0.0/rsdp.bend as P
13import bend-osdev-acpi@0.1.0.0/registry.bend as R
14import bend-osdev-acpi@0.1.0.0/aml_value.bend as V
15import bend-osdev-acpi@0.1.0.0/aml_host.bend as Hs
16import bend-osdev-acpi@0.1.0.0/aml_interp.bend as I
17import bend-osdev-acpi@0.1.0.0/aml.bend as A
18import bend-osdev-acpi@0.1.0.0/aml_term.bend as T
19import bend-osdev-acpi@0.1.0.0/aml_device.bend as Dv
20import bend-osdev-acpi@0.1.0.0/mcfg.bend as Mc
21import bend-osdev-acpi@0.1.0.0/example.bend as X
22import bend-osdev-acpi@0.1.0.0/LAWS.bend as Laws
23
24# The proofs reach Octets only through bytes' interface laws (octets_to_of,
25# octets_of_to, octets_append_list, octets_len_list, octets_split_at_append,
26# octets_le32_round_trip) and its list layer (B.append, B.mask, B.byte),
27# and W64 only through word64's public defs. The PkgLength proof and the
28# field lengths compute through B.mask and B.le32 on words split into their
29# bits, as bytes' own proofs do.
30
31# Contradictions
32
33def bdisc(+b: Bool) -> Type:
34 match b:
35 case True{}:
36 Empty
37 case False{}:
38 Unit
39
40def ft_absurd(+e: {False{} == True{} : Bool}) -> Empty:
41 %e : bdisc(_)
42 Unit{}
43
44# PkgLength: with the value split into its 32 bits, and the bits above the
45# highest one set taken one by one from the top, the encoder's choice of
46# form and the decoder's reading compute; values of 2^28 and up are refused
47# by the hypothesis
48
49def pk_abs(+v: U32, +r: List<&2, U32>, e: Empty) -> {K.pk.pub(K.pk.dec(B.append(B.mask(K.pk.enc(v)), r))) == Done{K.AmlPkgLen{v, B.Octets.of_list(r)}} : Result<&2, &2, E.AcpiError, K.AmlPkgLen>}:
50 Empty.absurd({K.pk.pub(K.pk.dec(B.append(B.mask(K.pk.enc(v)), r))) == Done{K.AmlPkgLen{v, B.Octets.of_list(r)}} : Result<&2, &2, E.AcpiError, K.AmlPkgLen>}, e)
51
52# the bits from the top down, so that they are matched in binder order
53def pk_bits(+b31: Bool, +b30: Bool, +b29: Bool, +b28: Bool, +b27: Bool, +b26: Bool, +b25: Bool, +b24: Bool, +b23: Bool, +b22: Bool, +b21: Bool, +b20: Bool, +b19: Bool, +b18: Bool, +b17: Bool, +b16: Bool, +b15: Bool, +b14: Bool, +b13: Bool, +b12: Bool, +b11: Bool, +b10: Bool, +b9: Bool, +b8: Bool, +b7: Bool, +b6: Bool, +b5: Bool, +b4: Bool, +b3: Bool, +b2: Bool, +b1: Bool, +b0: Bool, +r: List<&2, U32>, +fits: {K.AmlPkgLength.fits(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{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}) == True{} : Bool}) -> {K.pk.pub(K.pk.dec(B.append(B.mask(K.pk.enc(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{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}})), r))) == Done{K.AmlPkgLen{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{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, B.Octets.of_list(r)}} : Result<&2, &2, E.AcpiError, K.AmlPkgLen>}:
54 match b31:
55 case True{}:
56 pk_abs(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{True{}, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, r, ft_absurd(fits))
57 case False{}:
58 match b30:
59 case True{}:
60 pk_abs(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{True{}, WCon{False{}, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, r, ft_absurd(fits))
61 case False{}:
62 match b29:
63 case True{}:
64 pk_abs(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{True{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, r, ft_absurd(fits))
65 case False{}:
66 match b28:
67 case True{}:
68 pk_abs(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{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, r, ft_absurd(fits))
69 case False{}:
70 match b27:
71 case True{}:
72 {==}
73 case False{}:
74 match b26:
75 case True{}:
76 {==}
77 case False{}:
78 match b25:
79 case True{}:
80 {==}
81 case False{}:
82 match b24:
83 case True{}:
84 {==}
85 case False{}:
86 match b23:
87 case True{}:
88 {==}
89 case False{}:
90 match b22:
91 case True{}:
92 {==}
93 case False{}:
94 match b21:
95 case True{}:
96 {==}
97 case False{}:
98 match b20:
99 case True{}:
100 {==}
101 case False{}:
102 match b19:
103 case True{}:
104 {==}
105 case False{}:
106 match b18:
107 case True{}:
108 {==}
109 case False{}:
110 match b17:
111 case True{}:
112 {==}
113 case False{}:
114 match b16:
115 case True{}:
116 {==}
117 case False{}:
118 match b15:
119 case True{}:
120 {==}
121 case False{}:
122 match b14:
123 case True{}:
124 {==}
125 case False{}:
126 match b13:
127 case True{}:
128 {==}
129 case False{}:
130 match b12:
131 case True{}:
132 {==}
133 case False{}:
134 match b11:
135 case True{}:
136 {==}
137 case False{}:
138 match b10:
139 case True{}:
140 {==}
141 case False{}:
142 match b9:
143 case True{}:
144 {==}
145 case False{}:
146 match b8:
147 case True{}:
148 {==}
149 case False{}:
150 match b7:
151 case True{}:
152 {==}
153 case False{}:
154 match b6:
155 case True{}:
156 {==}
157 case False{}:
158 {==}
159
160def pk_rt(+v: U32, +r: List<&2, U32>, +fits: {K.AmlPkgLength.fits(v) == True{} : Bool}) -> {K.pk.pub(K.pk.dec(B.append(B.mask(K.pk.enc(v)), r))) == Done{K.AmlPkgLen{v, B.Octets.of_list(r)}} : Result<&2, &2, E.AcpiError, K.AmlPkgLen>}:
161 match v:
162 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{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
163 pk_bits(b31, b30, b29, b28, b27, b26, b25, b24, b23, b22, b21, b20, b19, b18, b17, b16, b15, b14, b13, b12, b11, b10, b9, b8, b7, b6, b5, b4, b3, b2, b1, b0, r, fits)
164
165# The SegCount of a MultiNamePath: a count below 256 survives being written
166# as a byte, by a chain of lemmas cnt.d (for k + d, d from 0 to 256), each a
167# closed computation or a step to the next
168
169def cnt_abs(+k: Nat, e: Empty) -> {U32.to_nat(B.byte(U32.from_nat(k))) == k : Nat}:
170 Empty.absurd({U32.to_nat(B.byte(U32.from_nat(k))) == k : Nat}, e)
171
172def cnt.d256(+k: Nat, +lt: {Nat.is_lt(Nat.add(256n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(256n, k)))) == Nat.add(256n, k) : Nat}:
173 match k:
174 case 0n:
175 cnt_abs(Nat.add(256n, 0n), ft_absurd(lt))
176 case 1n+p:
177 cnt_abs(Nat.add(256n, 1n+p), ft_absurd(lt))
178
179def cnt.d255(+k: Nat, +lt: {Nat.is_lt(Nat.add(255n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(255n, k)))) == Nat.add(255n, k) : Nat}:
180 match k:
181 case 0n:
182 {==}
183 case 1n+p:
184 cnt.d256(p, lt)
185
186def cnt.d254(+k: Nat, +lt: {Nat.is_lt(Nat.add(254n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(254n, k)))) == Nat.add(254n, k) : Nat}:
187 match k:
188 case 0n:
189 {==}
190 case 1n+p:
191 cnt.d255(p, lt)
192
193def cnt.d253(+k: Nat, +lt: {Nat.is_lt(Nat.add(253n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(253n, k)))) == Nat.add(253n, k) : Nat}:
194 match k:
195 case 0n:
196 {==}
197 case 1n+p:
198 cnt.d254(p, lt)
199
200def cnt.d252(+k: Nat, +lt: {Nat.is_lt(Nat.add(252n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(252n, k)))) == Nat.add(252n, k) : Nat}:
201 match k:
202 case 0n:
203 {==}
204 case 1n+p:
205 cnt.d253(p, lt)
206
207def cnt.d251(+k: Nat, +lt: {Nat.is_lt(Nat.add(251n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(251n, k)))) == Nat.add(251n, k) : Nat}:
208 match k:
209 case 0n:
210 {==}
211 case 1n+p:
212 cnt.d252(p, lt)
213
214def cnt.d250(+k: Nat, +lt: {Nat.is_lt(Nat.add(250n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(250n, k)))) == Nat.add(250n, k) : Nat}:
215 match k:
216 case 0n:
217 {==}
218 case 1n+p:
219 cnt.d251(p, lt)
220
221def cnt.d249(+k: Nat, +lt: {Nat.is_lt(Nat.add(249n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(249n, k)))) == Nat.add(249n, k) : Nat}:
222 match k:
223 case 0n:
224 {==}
225 case 1n+p:
226 cnt.d250(p, lt)
227
228def cnt.d248(+k: Nat, +lt: {Nat.is_lt(Nat.add(248n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(248n, k)))) == Nat.add(248n, k) : Nat}:
229 match k:
230 case 0n:
231 {==}
232 case 1n+p:
233 cnt.d249(p, lt)
234
235def cnt.d247(+k: Nat, +lt: {Nat.is_lt(Nat.add(247n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(247n, k)))) == Nat.add(247n, k) : Nat}:
236 match k:
237 case 0n:
238 {==}
239 case 1n+p:
240 cnt.d248(p, lt)
241
242def cnt.d246(+k: Nat, +lt: {Nat.is_lt(Nat.add(246n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(246n, k)))) == Nat.add(246n, k) : Nat}:
243 match k:
244 case 0n:
245 {==}
246 case 1n+p:
247 cnt.d247(p, lt)
248
249def cnt.d245(+k: Nat, +lt: {Nat.is_lt(Nat.add(245n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(245n, k)))) == Nat.add(245n, k) : Nat}:
250 match k:
251 case 0n:
252 {==}
253 case 1n+p:
254 cnt.d246(p, lt)
255
256def cnt.d244(+k: Nat, +lt: {Nat.is_lt(Nat.add(244n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(244n, k)))) == Nat.add(244n, k) : Nat}:
257 match k:
258 case 0n:
259 {==}
260 case 1n+p:
261 cnt.d245(p, lt)
262
263def cnt.d243(+k: Nat, +lt: {Nat.is_lt(Nat.add(243n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(243n, k)))) == Nat.add(243n, k) : Nat}:
264 match k:
265 case 0n:
266 {==}
267 case 1n+p:
268 cnt.d244(p, lt)
269
270def cnt.d242(+k: Nat, +lt: {Nat.is_lt(Nat.add(242n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(242n, k)))) == Nat.add(242n, k) : Nat}:
271 match k:
272 case 0n:
273 {==}
274 case 1n+p:
275 cnt.d243(p, lt)
276
277def cnt.d241(+k: Nat, +lt: {Nat.is_lt(Nat.add(241n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(241n, k)))) == Nat.add(241n, k) : Nat}:
278 match k:
279 case 0n:
280 {==}
281 case 1n+p:
282 cnt.d242(p, lt)
283
284def cnt.d240(+k: Nat, +lt: {Nat.is_lt(Nat.add(240n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(240n, k)))) == Nat.add(240n, k) : Nat}:
285 match k:
286 case 0n:
287 {==}
288 case 1n+p:
289 cnt.d241(p, lt)
290
291def cnt.d239(+k: Nat, +lt: {Nat.is_lt(Nat.add(239n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(239n, k)))) == Nat.add(239n, k) : Nat}:
292 match k:
293 case 0n:
294 {==}
295 case 1n+p:
296 cnt.d240(p, lt)
297
298def cnt.d238(+k: Nat, +lt: {Nat.is_lt(Nat.add(238n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(238n, k)))) == Nat.add(238n, k) : Nat}:
299 match k:
300 case 0n:
301 {==}
302 case 1n+p:
303 cnt.d239(p, lt)
304
305def cnt.d237(+k: Nat, +lt: {Nat.is_lt(Nat.add(237n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(237n, k)))) == Nat.add(237n, k) : Nat}:
306 match k:
307 case 0n:
308 {==}
309 case 1n+p:
310 cnt.d238(p, lt)
311
312def cnt.d236(+k: Nat, +lt: {Nat.is_lt(Nat.add(236n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(236n, k)))) == Nat.add(236n, k) : Nat}:
313 match k:
314 case 0n:
315 {==}
316 case 1n+p:
317 cnt.d237(p, lt)
318
319def cnt.d235(+k: Nat, +lt: {Nat.is_lt(Nat.add(235n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(235n, k)))) == Nat.add(235n, k) : Nat}:
320 match k:
321 case 0n:
322 {==}
323 case 1n+p:
324 cnt.d236(p, lt)
325
326def cnt.d234(+k: Nat, +lt: {Nat.is_lt(Nat.add(234n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(234n, k)))) == Nat.add(234n, k) : Nat}:
327 match k:
328 case 0n:
329 {==}
330 case 1n+p:
331 cnt.d235(p, lt)
332
333def cnt.d233(+k: Nat, +lt: {Nat.is_lt(Nat.add(233n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(233n, k)))) == Nat.add(233n, k) : Nat}:
334 match k:
335 case 0n:
336 {==}
337 case 1n+p:
338 cnt.d234(p, lt)
339
340def cnt.d232(+k: Nat, +lt: {Nat.is_lt(Nat.add(232n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(232n, k)))) == Nat.add(232n, k) : Nat}:
341 match k:
342 case 0n:
343 {==}
344 case 1n+p:
345 cnt.d233(p, lt)
346
347def cnt.d231(+k: Nat, +lt: {Nat.is_lt(Nat.add(231n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(231n, k)))) == Nat.add(231n, k) : Nat}:
348 match k:
349 case 0n:
350 {==}
351 case 1n+p:
352 cnt.d232(p, lt)
353
354def cnt.d230(+k: Nat, +lt: {Nat.is_lt(Nat.add(230n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(230n, k)))) == Nat.add(230n, k) : Nat}:
355 match k:
356 case 0n:
357 {==}
358 case 1n+p:
359 cnt.d231(p, lt)
360
361def cnt.d229(+k: Nat, +lt: {Nat.is_lt(Nat.add(229n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(229n, k)))) == Nat.add(229n, k) : Nat}:
362 match k:
363 case 0n:
364 {==}
365 case 1n+p:
366 cnt.d230(p, lt)
367
368def cnt.d228(+k: Nat, +lt: {Nat.is_lt(Nat.add(228n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(228n, k)))) == Nat.add(228n, k) : Nat}:
369 match k:
370 case 0n:
371 {==}
372 case 1n+p:
373 cnt.d229(p, lt)
374
375def cnt.d227(+k: Nat, +lt: {Nat.is_lt(Nat.add(227n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(227n, k)))) == Nat.add(227n, k) : Nat}:
376 match k:
377 case 0n:
378 {==}
379 case 1n+p:
380 cnt.d228(p, lt)
381
382def cnt.d226(+k: Nat, +lt: {Nat.is_lt(Nat.add(226n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(226n, k)))) == Nat.add(226n, k) : Nat}:
383 match k:
384 case 0n:
385 {==}
386 case 1n+p:
387 cnt.d227(p, lt)
388
389def cnt.d225(+k: Nat, +lt: {Nat.is_lt(Nat.add(225n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(225n, k)))) == Nat.add(225n, k) : Nat}:
390 match k:
391 case 0n:
392 {==}
393 case 1n+p:
394 cnt.d226(p, lt)
395
396def cnt.d224(+k: Nat, +lt: {Nat.is_lt(Nat.add(224n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(224n, k)))) == Nat.add(224n, k) : Nat}:
397 match k:
398 case 0n:
399 {==}
400 case 1n+p:
401 cnt.d225(p, lt)
402
403def cnt.d223(+k: Nat, +lt: {Nat.is_lt(Nat.add(223n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(223n, k)))) == Nat.add(223n, k) : Nat}:
404 match k:
405 case 0n:
406 {==}
407 case 1n+p:
408 cnt.d224(p, lt)
409
410def cnt.d222(+k: Nat, +lt: {Nat.is_lt(Nat.add(222n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(222n, k)))) == Nat.add(222n, k) : Nat}:
411 match k:
412 case 0n:
413 {==}
414 case 1n+p:
415 cnt.d223(p, lt)
416
417def cnt.d221(+k: Nat, +lt: {Nat.is_lt(Nat.add(221n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(221n, k)))) == Nat.add(221n, k) : Nat}:
418 match k:
419 case 0n:
420 {==}
421 case 1n+p:
422 cnt.d222(p, lt)
423
424def cnt.d220(+k: Nat, +lt: {Nat.is_lt(Nat.add(220n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(220n, k)))) == Nat.add(220n, k) : Nat}:
425 match k:
426 case 0n:
427 {==}
428 case 1n+p:
429 cnt.d221(p, lt)
430
431def cnt.d219(+k: Nat, +lt: {Nat.is_lt(Nat.add(219n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(219n, k)))) == Nat.add(219n, k) : Nat}:
432 match k:
433 case 0n:
434 {==}
435 case 1n+p:
436 cnt.d220(p, lt)
437
438def cnt.d218(+k: Nat, +lt: {Nat.is_lt(Nat.add(218n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(218n, k)))) == Nat.add(218n, k) : Nat}:
439 match k:
440 case 0n:
441 {==}
442 case 1n+p:
443 cnt.d219(p, lt)
444
445def cnt.d217(+k: Nat, +lt: {Nat.is_lt(Nat.add(217n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(217n, k)))) == Nat.add(217n, k) : Nat}:
446 match k:
447 case 0n:
448 {==}
449 case 1n+p:
450 cnt.d218(p, lt)
451
452def cnt.d216(+k: Nat, +lt: {Nat.is_lt(Nat.add(216n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(216n, k)))) == Nat.add(216n, k) : Nat}:
453 match k:
454 case 0n:
455 {==}
456 case 1n+p:
457 cnt.d217(p, lt)
458
459def cnt.d215(+k: Nat, +lt: {Nat.is_lt(Nat.add(215n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(215n, k)))) == Nat.add(215n, k) : Nat}:
460 match k:
461 case 0n:
462 {==}
463 case 1n+p:
464 cnt.d216(p, lt)
465
466def cnt.d214(+k: Nat, +lt: {Nat.is_lt(Nat.add(214n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(214n, k)))) == Nat.add(214n, k) : Nat}:
467 match k:
468 case 0n:
469 {==}
470 case 1n+p:
471 cnt.d215(p, lt)
472
473def cnt.d213(+k: Nat, +lt: {Nat.is_lt(Nat.add(213n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(213n, k)))) == Nat.add(213n, k) : Nat}:
474 match k:
475 case 0n:
476 {==}
477 case 1n+p:
478 cnt.d214(p, lt)
479
480def cnt.d212(+k: Nat, +lt: {Nat.is_lt(Nat.add(212n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(212n, k)))) == Nat.add(212n, k) : Nat}:
481 match k:
482 case 0n:
483 {==}
484 case 1n+p:
485 cnt.d213(p, lt)
486
487def cnt.d211(+k: Nat, +lt: {Nat.is_lt(Nat.add(211n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(211n, k)))) == Nat.add(211n, k) : Nat}:
488 match k:
489 case 0n:
490 {==}
491 case 1n+p:
492 cnt.d212(p, lt)
493
494def cnt.d210(+k: Nat, +lt: {Nat.is_lt(Nat.add(210n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(210n, k)))) == Nat.add(210n, k) : Nat}:
495 match k:
496 case 0n:
497 {==}
498 case 1n+p:
499 cnt.d211(p, lt)
500
501def cnt.d209(+k: Nat, +lt: {Nat.is_lt(Nat.add(209n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(209n, k)))) == Nat.add(209n, k) : Nat}:
502 match k:
503 case 0n:
504 {==}
505 case 1n+p:
506 cnt.d210(p, lt)
507
508def cnt.d208(+k: Nat, +lt: {Nat.is_lt(Nat.add(208n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(208n, k)))) == Nat.add(208n, k) : Nat}:
509 match k:
510 case 0n:
511 {==}
512 case 1n+p:
513 cnt.d209(p, lt)
514
515def cnt.d207(+k: Nat, +lt: {Nat.is_lt(Nat.add(207n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(207n, k)))) == Nat.add(207n, k) : Nat}:
516 match k:
517 case 0n:
518 {==}
519 case 1n+p:
520 cnt.d208(p, lt)
521
522def cnt.d206(+k: Nat, +lt: {Nat.is_lt(Nat.add(206n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(206n, k)))) == Nat.add(206n, k) : Nat}:
523 match k:
524 case 0n:
525 {==}
526 case 1n+p:
527 cnt.d207(p, lt)
528
529def cnt.d205(+k: Nat, +lt: {Nat.is_lt(Nat.add(205n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(205n, k)))) == Nat.add(205n, k) : Nat}:
530 match k:
531 case 0n:
532 {==}
533 case 1n+p:
534 cnt.d206(p, lt)
535
536def cnt.d204(+k: Nat, +lt: {Nat.is_lt(Nat.add(204n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(204n, k)))) == Nat.add(204n, k) : Nat}:
537 match k:
538 case 0n:
539 {==}
540 case 1n+p:
541 cnt.d205(p, lt)
542
543def cnt.d203(+k: Nat, +lt: {Nat.is_lt(Nat.add(203n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(203n, k)))) == Nat.add(203n, k) : Nat}:
544 match k:
545 case 0n:
546 {==}
547 case 1n+p:
548 cnt.d204(p, lt)
549
550def cnt.d202(+k: Nat, +lt: {Nat.is_lt(Nat.add(202n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(202n, k)))) == Nat.add(202n, k) : Nat}:
551 match k:
552 case 0n:
553 {==}
554 case 1n+p:
555 cnt.d203(p, lt)
556
557def cnt.d201(+k: Nat, +lt: {Nat.is_lt(Nat.add(201n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(201n, k)))) == Nat.add(201n, k) : Nat}:
558 match k:
559 case 0n:
560 {==}
561 case 1n+p:
562 cnt.d202(p, lt)
563
564def cnt.d200(+k: Nat, +lt: {Nat.is_lt(Nat.add(200n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(200n, k)))) == Nat.add(200n, k) : Nat}:
565 match k:
566 case 0n:
567 {==}
568 case 1n+p:
569 cnt.d201(p, lt)
570
571def cnt.d199(+k: Nat, +lt: {Nat.is_lt(Nat.add(199n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(199n, k)))) == Nat.add(199n, k) : Nat}:
572 match k:
573 case 0n:
574 {==}
575 case 1n+p:
576 cnt.d200(p, lt)
577
578def cnt.d198(+k: Nat, +lt: {Nat.is_lt(Nat.add(198n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(198n, k)))) == Nat.add(198n, k) : Nat}:
579 match k:
580 case 0n:
581 {==}
582 case 1n+p:
583 cnt.d199(p, lt)
584
585def cnt.d197(+k: Nat, +lt: {Nat.is_lt(Nat.add(197n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(197n, k)))) == Nat.add(197n, k) : Nat}:
586 match k:
587 case 0n:
588 {==}
589 case 1n+p:
590 cnt.d198(p, lt)
591
592def cnt.d196(+k: Nat, +lt: {Nat.is_lt(Nat.add(196n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(196n, k)))) == Nat.add(196n, k) : Nat}:
593 match k:
594 case 0n:
595 {==}
596 case 1n+p:
597 cnt.d197(p, lt)
598
599def cnt.d195(+k: Nat, +lt: {Nat.is_lt(Nat.add(195n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(195n, k)))) == Nat.add(195n, k) : Nat}:
600 match k:
601 case 0n:
602 {==}
603 case 1n+p:
604 cnt.d196(p, lt)
605
606def cnt.d194(+k: Nat, +lt: {Nat.is_lt(Nat.add(194n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(194n, k)))) == Nat.add(194n, k) : Nat}:
607 match k:
608 case 0n:
609 {==}
610 case 1n+p:
611 cnt.d195(p, lt)
612
613def cnt.d193(+k: Nat, +lt: {Nat.is_lt(Nat.add(193n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(193n, k)))) == Nat.add(193n, k) : Nat}:
614 match k:
615 case 0n:
616 {==}
617 case 1n+p:
618 cnt.d194(p, lt)
619
620def cnt.d192(+k: Nat, +lt: {Nat.is_lt(Nat.add(192n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(192n, k)))) == Nat.add(192n, k) : Nat}:
621 match k:
622 case 0n:
623 {==}
624 case 1n+p:
625 cnt.d193(p, lt)
626
627def cnt.d191(+k: Nat, +lt: {Nat.is_lt(Nat.add(191n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(191n, k)))) == Nat.add(191n, k) : Nat}:
628 match k:
629 case 0n:
630 {==}
631 case 1n+p:
632 cnt.d192(p, lt)
633
634def cnt.d190(+k: Nat, +lt: {Nat.is_lt(Nat.add(190n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(190n, k)))) == Nat.add(190n, k) : Nat}:
635 match k:
636 case 0n:
637 {==}
638 case 1n+p:
639 cnt.d191(p, lt)
640
641def cnt.d189(+k: Nat, +lt: {Nat.is_lt(Nat.add(189n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(189n, k)))) == Nat.add(189n, k) : Nat}:
642 match k:
643 case 0n:
644 {==}
645 case 1n+p:
646 cnt.d190(p, lt)
647
648def cnt.d188(+k: Nat, +lt: {Nat.is_lt(Nat.add(188n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(188n, k)))) == Nat.add(188n, k) : Nat}:
649 match k:
650 case 0n:
651 {==}
652 case 1n+p:
653 cnt.d189(p, lt)
654
655def cnt.d187(+k: Nat, +lt: {Nat.is_lt(Nat.add(187n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(187n, k)))) == Nat.add(187n, k) : Nat}:
656 match k:
657 case 0n:
658 {==}
659 case 1n+p:
660 cnt.d188(p, lt)
661
662def cnt.d186(+k: Nat, +lt: {Nat.is_lt(Nat.add(186n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(186n, k)))) == Nat.add(186n, k) : Nat}:
663 match k:
664 case 0n:
665 {==}
666 case 1n+p:
667 cnt.d187(p, lt)
668
669def cnt.d185(+k: Nat, +lt: {Nat.is_lt(Nat.add(185n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(185n, k)))) == Nat.add(185n, k) : Nat}:
670 match k:
671 case 0n:
672 {==}
673 case 1n+p:
674 cnt.d186(p, lt)
675
676def cnt.d184(+k: Nat, +lt: {Nat.is_lt(Nat.add(184n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(184n, k)))) == Nat.add(184n, k) : Nat}:
677 match k:
678 case 0n:
679 {==}
680 case 1n+p:
681 cnt.d185(p, lt)
682
683def cnt.d183(+k: Nat, +lt: {Nat.is_lt(Nat.add(183n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(183n, k)))) == Nat.add(183n, k) : Nat}:
684 match k:
685 case 0n:
686 {==}
687 case 1n+p:
688 cnt.d184(p, lt)
689
690def cnt.d182(+k: Nat, +lt: {Nat.is_lt(Nat.add(182n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(182n, k)))) == Nat.add(182n, k) : Nat}:
691 match k:
692 case 0n:
693 {==}
694 case 1n+p:
695 cnt.d183(p, lt)
696
697def cnt.d181(+k: Nat, +lt: {Nat.is_lt(Nat.add(181n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(181n, k)))) == Nat.add(181n, k) : Nat}:
698 match k:
699 case 0n:
700 {==}
701 case 1n+p:
702 cnt.d182(p, lt)
703
704def cnt.d180(+k: Nat, +lt: {Nat.is_lt(Nat.add(180n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(180n, k)))) == Nat.add(180n, k) : Nat}:
705 match k:
706 case 0n:
707 {==}
708 case 1n+p:
709 cnt.d181(p, lt)
710
711def cnt.d179(+k: Nat, +lt: {Nat.is_lt(Nat.add(179n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(179n, k)))) == Nat.add(179n, k) : Nat}:
712 match k:
713 case 0n:
714 {==}
715 case 1n+p:
716 cnt.d180(p, lt)
717
718def cnt.d178(+k: Nat, +lt: {Nat.is_lt(Nat.add(178n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(178n, k)))) == Nat.add(178n, k) : Nat}:
719 match k:
720 case 0n:
721 {==}
722 case 1n+p:
723 cnt.d179(p, lt)
724
725def cnt.d177(+k: Nat, +lt: {Nat.is_lt(Nat.add(177n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(177n, k)))) == Nat.add(177n, k) : Nat}:
726 match k:
727 case 0n:
728 {==}
729 case 1n+p:
730 cnt.d178(p, lt)
731
732def cnt.d176(+k: Nat, +lt: {Nat.is_lt(Nat.add(176n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(176n, k)))) == Nat.add(176n, k) : Nat}:
733 match k:
734 case 0n:
735 {==}
736 case 1n+p:
737 cnt.d177(p, lt)
738
739def cnt.d175(+k: Nat, +lt: {Nat.is_lt(Nat.add(175n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(175n, k)))) == Nat.add(175n, k) : Nat}:
740 match k:
741 case 0n:
742 {==}
743 case 1n+p:
744 cnt.d176(p, lt)
745
746def cnt.d174(+k: Nat, +lt: {Nat.is_lt(Nat.add(174n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(174n, k)))) == Nat.add(174n, k) : Nat}:
747 match k:
748 case 0n:
749 {==}
750 case 1n+p:
751 cnt.d175(p, lt)
752
753def cnt.d173(+k: Nat, +lt: {Nat.is_lt(Nat.add(173n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(173n, k)))) == Nat.add(173n, k) : Nat}:
754 match k:
755 case 0n:
756 {==}
757 case 1n+p:
758 cnt.d174(p, lt)
759
760def cnt.d172(+k: Nat, +lt: {Nat.is_lt(Nat.add(172n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(172n, k)))) == Nat.add(172n, k) : Nat}:
761 match k:
762 case 0n:
763 {==}
764 case 1n+p:
765 cnt.d173(p, lt)
766
767def cnt.d171(+k: Nat, +lt: {Nat.is_lt(Nat.add(171n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(171n, k)))) == Nat.add(171n, k) : Nat}:
768 match k:
769 case 0n:
770 {==}
771 case 1n+p:
772 cnt.d172(p, lt)
773
774def cnt.d170(+k: Nat, +lt: {Nat.is_lt(Nat.add(170n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(170n, k)))) == Nat.add(170n, k) : Nat}:
775 match k:
776 case 0n:
777 {==}
778 case 1n+p:
779 cnt.d171(p, lt)
780
781def cnt.d169(+k: Nat, +lt: {Nat.is_lt(Nat.add(169n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(169n, k)))) == Nat.add(169n, k) : Nat}:
782 match k:
783 case 0n:
784 {==}
785 case 1n+p:
786 cnt.d170(p, lt)
787
788def cnt.d168(+k: Nat, +lt: {Nat.is_lt(Nat.add(168n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(168n, k)))) == Nat.add(168n, k) : Nat}:
789 match k:
790 case 0n:
791 {==}
792 case 1n+p:
793 cnt.d169(p, lt)
794
795def cnt.d167(+k: Nat, +lt: {Nat.is_lt(Nat.add(167n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(167n, k)))) == Nat.add(167n, k) : Nat}:
796 match k:
797 case 0n:
798 {==}
799 case 1n+p:
800 cnt.d168(p, lt)
801
802def cnt.d166(+k: Nat, +lt: {Nat.is_lt(Nat.add(166n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(166n, k)))) == Nat.add(166n, k) : Nat}:
803 match k:
804 case 0n:
805 {==}
806 case 1n+p:
807 cnt.d167(p, lt)
808
809def cnt.d165(+k: Nat, +lt: {Nat.is_lt(Nat.add(165n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(165n, k)))) == Nat.add(165n, k) : Nat}:
810 match k:
811 case 0n:
812 {==}
813 case 1n+p:
814 cnt.d166(p, lt)
815
816def cnt.d164(+k: Nat, +lt: {Nat.is_lt(Nat.add(164n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(164n, k)))) == Nat.add(164n, k) : Nat}:
817 match k:
818 case 0n:
819 {==}
820 case 1n+p:
821 cnt.d165(p, lt)
822
823def cnt.d163(+k: Nat, +lt: {Nat.is_lt(Nat.add(163n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(163n, k)))) == Nat.add(163n, k) : Nat}:
824 match k:
825 case 0n:
826 {==}
827 case 1n+p:
828 cnt.d164(p, lt)
829
830def cnt.d162(+k: Nat, +lt: {Nat.is_lt(Nat.add(162n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(162n, k)))) == Nat.add(162n, k) : Nat}:
831 match k:
832 case 0n:
833 {==}
834 case 1n+p:
835 cnt.d163(p, lt)
836
837def cnt.d161(+k: Nat, +lt: {Nat.is_lt(Nat.add(161n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(161n, k)))) == Nat.add(161n, k) : Nat}:
838 match k:
839 case 0n:
840 {==}
841 case 1n+p:
842 cnt.d162(p, lt)
843
844def cnt.d160(+k: Nat, +lt: {Nat.is_lt(Nat.add(160n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(160n, k)))) == Nat.add(160n, k) : Nat}:
845 match k:
846 case 0n:
847 {==}
848 case 1n+p:
849 cnt.d161(p, lt)
850
851def cnt.d159(+k: Nat, +lt: {Nat.is_lt(Nat.add(159n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(159n, k)))) == Nat.add(159n, k) : Nat}:
852 match k:
853 case 0n:
854 {==}
855 case 1n+p:
856 cnt.d160(p, lt)
857
858def cnt.d158(+k: Nat, +lt: {Nat.is_lt(Nat.add(158n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(158n, k)))) == Nat.add(158n, k) : Nat}:
859 match k:
860 case 0n:
861 {==}
862 case 1n+p:
863 cnt.d159(p, lt)
864
865def cnt.d157(+k: Nat, +lt: {Nat.is_lt(Nat.add(157n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(157n, k)))) == Nat.add(157n, k) : Nat}:
866 match k:
867 case 0n:
868 {==}
869 case 1n+p:
870 cnt.d158(p, lt)
871
872def cnt.d156(+k: Nat, +lt: {Nat.is_lt(Nat.add(156n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(156n, k)))) == Nat.add(156n, k) : Nat}:
873 match k:
874 case 0n:
875 {==}
876 case 1n+p:
877 cnt.d157(p, lt)
878
879def cnt.d155(+k: Nat, +lt: {Nat.is_lt(Nat.add(155n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(155n, k)))) == Nat.add(155n, k) : Nat}:
880 match k:
881 case 0n:
882 {==}
883 case 1n+p:
884 cnt.d156(p, lt)
885
886def cnt.d154(+k: Nat, +lt: {Nat.is_lt(Nat.add(154n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(154n, k)))) == Nat.add(154n, k) : Nat}:
887 match k:
888 case 0n:
889 {==}
890 case 1n+p:
891 cnt.d155(p, lt)
892
893def cnt.d153(+k: Nat, +lt: {Nat.is_lt(Nat.add(153n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(153n, k)))) == Nat.add(153n, k) : Nat}:
894 match k:
895 case 0n:
896 {==}
897 case 1n+p:
898 cnt.d154(p, lt)
899
900def cnt.d152(+k: Nat, +lt: {Nat.is_lt(Nat.add(152n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(152n, k)))) == Nat.add(152n, k) : Nat}:
901 match k:
902 case 0n:
903 {==}
904 case 1n+p:
905 cnt.d153(p, lt)
906
907def cnt.d151(+k: Nat, +lt: {Nat.is_lt(Nat.add(151n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(151n, k)))) == Nat.add(151n, k) : Nat}:
908 match k:
909 case 0n:
910 {==}
911 case 1n+p:
912 cnt.d152(p, lt)
913
914def cnt.d150(+k: Nat, +lt: {Nat.is_lt(Nat.add(150n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(150n, k)))) == Nat.add(150n, k) : Nat}:
915 match k:
916 case 0n:
917 {==}
918 case 1n+p:
919 cnt.d151(p, lt)
920
921def cnt.d149(+k: Nat, +lt: {Nat.is_lt(Nat.add(149n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(149n, k)))) == Nat.add(149n, k) : Nat}:
922 match k:
923 case 0n:
924 {==}
925 case 1n+p:
926 cnt.d150(p, lt)
927
928def cnt.d148(+k: Nat, +lt: {Nat.is_lt(Nat.add(148n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(148n, k)))) == Nat.add(148n, k) : Nat}:
929 match k:
930 case 0n:
931 {==}
932 case 1n+p:
933 cnt.d149(p, lt)
934
935def cnt.d147(+k: Nat, +lt: {Nat.is_lt(Nat.add(147n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(147n, k)))) == Nat.add(147n, k) : Nat}:
936 match k:
937 case 0n:
938 {==}
939 case 1n+p:
940 cnt.d148(p, lt)
941
942def cnt.d146(+k: Nat, +lt: {Nat.is_lt(Nat.add(146n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(146n, k)))) == Nat.add(146n, k) : Nat}:
943 match k:
944 case 0n:
945 {==}
946 case 1n+p:
947 cnt.d147(p, lt)
948
949def cnt.d145(+k: Nat, +lt: {Nat.is_lt(Nat.add(145n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(145n, k)))) == Nat.add(145n, k) : Nat}:
950 match k:
951 case 0n:
952 {==}
953 case 1n+p:
954 cnt.d146(p, lt)
955
956def cnt.d144(+k: Nat, +lt: {Nat.is_lt(Nat.add(144n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(144n, k)))) == Nat.add(144n, k) : Nat}:
957 match k:
958 case 0n:
959 {==}
960 case 1n+p:
961 cnt.d145(p, lt)
962
963def cnt.d143(+k: Nat, +lt: {Nat.is_lt(Nat.add(143n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(143n, k)))) == Nat.add(143n, k) : Nat}:
964 match k:
965 case 0n:
966 {==}
967 case 1n+p:
968 cnt.d144(p, lt)
969
970def cnt.d142(+k: Nat, +lt: {Nat.is_lt(Nat.add(142n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(142n, k)))) == Nat.add(142n, k) : Nat}:
971 match k:
972 case 0n:
973 {==}
974 case 1n+p:
975 cnt.d143(p, lt)
976
977def cnt.d141(+k: Nat, +lt: {Nat.is_lt(Nat.add(141n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(141n, k)))) == Nat.add(141n, k) : Nat}:
978 match k:
979 case 0n:
980 {==}
981 case 1n+p:
982 cnt.d142(p, lt)
983
984def cnt.d140(+k: Nat, +lt: {Nat.is_lt(Nat.add(140n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(140n, k)))) == Nat.add(140n, k) : Nat}:
985 match k:
986 case 0n:
987 {==}
988 case 1n+p:
989 cnt.d141(p, lt)
990
991def cnt.d139(+k: Nat, +lt: {Nat.is_lt(Nat.add(139n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(139n, k)))) == Nat.add(139n, k) : Nat}:
992 match k:
993 case 0n:
994 {==}
995 case 1n+p:
996 cnt.d140(p, lt)
997
998def cnt.d138(+k: Nat, +lt: {Nat.is_lt(Nat.add(138n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(138n, k)))) == Nat.add(138n, k) : Nat}:
999 match k:
1000 case 0n:
1001 {==}
1002 case 1n+p:
1003 cnt.d139(p, lt)
1004
1005def cnt.d137(+k: Nat, +lt: {Nat.is_lt(Nat.add(137n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(137n, k)))) == Nat.add(137n, k) : Nat}:
1006 match k:
1007 case 0n:
1008 {==}
1009 case 1n+p:
1010 cnt.d138(p, lt)
1011
1012def cnt.d136(+k: Nat, +lt: {Nat.is_lt(Nat.add(136n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(136n, k)))) == Nat.add(136n, k) : Nat}:
1013 match k:
1014 case 0n:
1015 {==}
1016 case 1n+p:
1017 cnt.d137(p, lt)
1018
1019def cnt.d135(+k: Nat, +lt: {Nat.is_lt(Nat.add(135n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(135n, k)))) == Nat.add(135n, k) : Nat}:
1020 match k:
1021 case 0n:
1022 {==}
1023 case 1n+p:
1024 cnt.d136(p, lt)
1025
1026def cnt.d134(+k: Nat, +lt: {Nat.is_lt(Nat.add(134n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(134n, k)))) == Nat.add(134n, k) : Nat}:
1027 match k:
1028 case 0n:
1029 {==}
1030 case 1n+p:
1031 cnt.d135(p, lt)
1032
1033def cnt.d133(+k: Nat, +lt: {Nat.is_lt(Nat.add(133n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(133n, k)))) == Nat.add(133n, k) : Nat}:
1034 match k:
1035 case 0n:
1036 {==}
1037 case 1n+p:
1038 cnt.d134(p, lt)
1039
1040def cnt.d132(+k: Nat, +lt: {Nat.is_lt(Nat.add(132n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(132n, k)))) == Nat.add(132n, k) : Nat}:
1041 match k:
1042 case 0n:
1043 {==}
1044 case 1n+p:
1045 cnt.d133(p, lt)
1046
1047def cnt.d131(+k: Nat, +lt: {Nat.is_lt(Nat.add(131n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(131n, k)))) == Nat.add(131n, k) : Nat}:
1048 match k:
1049 case 0n:
1050 {==}
1051 case 1n+p:
1052 cnt.d132(p, lt)
1053
1054def cnt.d130(+k: Nat, +lt: {Nat.is_lt(Nat.add(130n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(130n, k)))) == Nat.add(130n, k) : Nat}:
1055 match k:
1056 case 0n:
1057 {==}
1058 case 1n+p:
1059 cnt.d131(p, lt)
1060
1061def cnt.d129(+k: Nat, +lt: {Nat.is_lt(Nat.add(129n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(129n, k)))) == Nat.add(129n, k) : Nat}:
1062 match k:
1063 case 0n:
1064 {==}
1065 case 1n+p:
1066 cnt.d130(p, lt)
1067
1068def cnt.d128(+k: Nat, +lt: {Nat.is_lt(Nat.add(128n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(128n, k)))) == Nat.add(128n, k) : Nat}:
1069 match k:
1070 case 0n:
1071 {==}
1072 case 1n+p:
1073 cnt.d129(p, lt)
1074
1075def cnt.d127(+k: Nat, +lt: {Nat.is_lt(Nat.add(127n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(127n, k)))) == Nat.add(127n, k) : Nat}:
1076 match k:
1077 case 0n:
1078 {==}
1079 case 1n+p:
1080 cnt.d128(p, lt)
1081
1082def cnt.d126(+k: Nat, +lt: {Nat.is_lt(Nat.add(126n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(126n, k)))) == Nat.add(126n, k) : Nat}:
1083 match k:
1084 case 0n:
1085 {==}
1086 case 1n+p:
1087 cnt.d127(p, lt)
1088
1089def cnt.d125(+k: Nat, +lt: {Nat.is_lt(Nat.add(125n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(125n, k)))) == Nat.add(125n, k) : Nat}:
1090 match k:
1091 case 0n:
1092 {==}
1093 case 1n+p:
1094 cnt.d126(p, lt)
1095
1096def cnt.d124(+k: Nat, +lt: {Nat.is_lt(Nat.add(124n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(124n, k)))) == Nat.add(124n, k) : Nat}:
1097 match k:
1098 case 0n:
1099 {==}
1100 case 1n+p:
1101 cnt.d125(p, lt)
1102
1103def cnt.d123(+k: Nat, +lt: {Nat.is_lt(Nat.add(123n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(123n, k)))) == Nat.add(123n, k) : Nat}:
1104 match k:
1105 case 0n:
1106 {==}
1107 case 1n+p:
1108 cnt.d124(p, lt)
1109
1110def cnt.d122(+k: Nat, +lt: {Nat.is_lt(Nat.add(122n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(122n, k)))) == Nat.add(122n, k) : Nat}:
1111 match k:
1112 case 0n:
1113 {==}
1114 case 1n+p:
1115 cnt.d123(p, lt)
1116
1117def cnt.d121(+k: Nat, +lt: {Nat.is_lt(Nat.add(121n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(121n, k)))) == Nat.add(121n, k) : Nat}:
1118 match k:
1119 case 0n:
1120 {==}
1121 case 1n+p:
1122 cnt.d122(p, lt)
1123
1124def cnt.d120(+k: Nat, +lt: {Nat.is_lt(Nat.add(120n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(120n, k)))) == Nat.add(120n, k) : Nat}:
1125 match k:
1126 case 0n:
1127 {==}
1128 case 1n+p:
1129 cnt.d121(p, lt)
1130
1131def cnt.d119(+k: Nat, +lt: {Nat.is_lt(Nat.add(119n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(119n, k)))) == Nat.add(119n, k) : Nat}:
1132 match k:
1133 case 0n:
1134 {==}
1135 case 1n+p:
1136 cnt.d120(p, lt)
1137
1138def cnt.d118(+k: Nat, +lt: {Nat.is_lt(Nat.add(118n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(118n, k)))) == Nat.add(118n, k) : Nat}:
1139 match k:
1140 case 0n:
1141 {==}
1142 case 1n+p:
1143 cnt.d119(p, lt)
1144
1145def cnt.d117(+k: Nat, +lt: {Nat.is_lt(Nat.add(117n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(117n, k)))) == Nat.add(117n, k) : Nat}:
1146 match k:
1147 case 0n:
1148 {==}
1149 case 1n+p:
1150 cnt.d118(p, lt)
1151
1152def cnt.d116(+k: Nat, +lt: {Nat.is_lt(Nat.add(116n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(116n, k)))) == Nat.add(116n, k) : Nat}:
1153 match k:
1154 case 0n:
1155 {==}
1156 case 1n+p:
1157 cnt.d117(p, lt)
1158
1159def cnt.d115(+k: Nat, +lt: {Nat.is_lt(Nat.add(115n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(115n, k)))) == Nat.add(115n, k) : Nat}:
1160 match k:
1161 case 0n:
1162 {==}
1163 case 1n+p:
1164 cnt.d116(p, lt)
1165
1166def cnt.d114(+k: Nat, +lt: {Nat.is_lt(Nat.add(114n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(114n, k)))) == Nat.add(114n, k) : Nat}:
1167 match k:
1168 case 0n:
1169 {==}
1170 case 1n+p:
1171 cnt.d115(p, lt)
1172
1173def cnt.d113(+k: Nat, +lt: {Nat.is_lt(Nat.add(113n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(113n, k)))) == Nat.add(113n, k) : Nat}:
1174 match k:
1175 case 0n:
1176 {==}
1177 case 1n+p:
1178 cnt.d114(p, lt)
1179
1180def cnt.d112(+k: Nat, +lt: {Nat.is_lt(Nat.add(112n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(112n, k)))) == Nat.add(112n, k) : Nat}:
1181 match k:
1182 case 0n:
1183 {==}
1184 case 1n+p:
1185 cnt.d113(p, lt)
1186
1187def cnt.d111(+k: Nat, +lt: {Nat.is_lt(Nat.add(111n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(111n, k)))) == Nat.add(111n, k) : Nat}:
1188 match k:
1189 case 0n:
1190 {==}
1191 case 1n+p:
1192 cnt.d112(p, lt)
1193
1194def cnt.d110(+k: Nat, +lt: {Nat.is_lt(Nat.add(110n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(110n, k)))) == Nat.add(110n, k) : Nat}:
1195 match k:
1196 case 0n:
1197 {==}
1198 case 1n+p:
1199 cnt.d111(p, lt)
1200
1201def cnt.d109(+k: Nat, +lt: {Nat.is_lt(Nat.add(109n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(109n, k)))) == Nat.add(109n, k) : Nat}:
1202 match k:
1203 case 0n:
1204 {==}
1205 case 1n+p:
1206 cnt.d110(p, lt)
1207
1208def cnt.d108(+k: Nat, +lt: {Nat.is_lt(Nat.add(108n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(108n, k)))) == Nat.add(108n, k) : Nat}:
1209 match k:
1210 case 0n:
1211 {==}
1212 case 1n+p:
1213 cnt.d109(p, lt)
1214
1215def cnt.d107(+k: Nat, +lt: {Nat.is_lt(Nat.add(107n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(107n, k)))) == Nat.add(107n, k) : Nat}:
1216 match k:
1217 case 0n:
1218 {==}
1219 case 1n+p:
1220 cnt.d108(p, lt)
1221
1222def cnt.d106(+k: Nat, +lt: {Nat.is_lt(Nat.add(106n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(106n, k)))) == Nat.add(106n, k) : Nat}:
1223 match k:
1224 case 0n:
1225 {==}
1226 case 1n+p:
1227 cnt.d107(p, lt)
1228
1229def cnt.d105(+k: Nat, +lt: {Nat.is_lt(Nat.add(105n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(105n, k)))) == Nat.add(105n, k) : Nat}:
1230 match k:
1231 case 0n:
1232 {==}
1233 case 1n+p:
1234 cnt.d106(p, lt)
1235
1236def cnt.d104(+k: Nat, +lt: {Nat.is_lt(Nat.add(104n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(104n, k)))) == Nat.add(104n, k) : Nat}:
1237 match k:
1238 case 0n:
1239 {==}
1240 case 1n+p:
1241 cnt.d105(p, lt)
1242
1243def cnt.d103(+k: Nat, +lt: {Nat.is_lt(Nat.add(103n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(103n, k)))) == Nat.add(103n, k) : Nat}:
1244 match k:
1245 case 0n:
1246 {==}
1247 case 1n+p:
1248 cnt.d104(p, lt)
1249
1250def cnt.d102(+k: Nat, +lt: {Nat.is_lt(Nat.add(102n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(102n, k)))) == Nat.add(102n, k) : Nat}:
1251 match k:
1252 case 0n:
1253 {==}
1254 case 1n+p:
1255 cnt.d103(p, lt)
1256
1257def cnt.d101(+k: Nat, +lt: {Nat.is_lt(Nat.add(101n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(101n, k)))) == Nat.add(101n, k) : Nat}:
1258 match k:
1259 case 0n:
1260 {==}
1261 case 1n+p:
1262 cnt.d102(p, lt)
1263
1264def cnt.d100(+k: Nat, +lt: {Nat.is_lt(Nat.add(100n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(100n, k)))) == Nat.add(100n, k) : Nat}:
1265 match k:
1266 case 0n:
1267 {==}
1268 case 1n+p:
1269 cnt.d101(p, lt)
1270
1271def cnt.d99(+k: Nat, +lt: {Nat.is_lt(Nat.add(99n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(99n, k)))) == Nat.add(99n, k) : Nat}:
1272 match k:
1273 case 0n:
1274 {==}
1275 case 1n+p:
1276 cnt.d100(p, lt)
1277
1278def cnt.d98(+k: Nat, +lt: {Nat.is_lt(Nat.add(98n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(98n, k)))) == Nat.add(98n, k) : Nat}:
1279 match k:
1280 case 0n:
1281 {==}
1282 case 1n+p:
1283 cnt.d99(p, lt)
1284
1285def cnt.d97(+k: Nat, +lt: {Nat.is_lt(Nat.add(97n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(97n, k)))) == Nat.add(97n, k) : Nat}:
1286 match k:
1287 case 0n:
1288 {==}
1289 case 1n+p:
1290 cnt.d98(p, lt)
1291
1292def cnt.d96(+k: Nat, +lt: {Nat.is_lt(Nat.add(96n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(96n, k)))) == Nat.add(96n, k) : Nat}:
1293 match k:
1294 case 0n:
1295 {==}
1296 case 1n+p:
1297 cnt.d97(p, lt)
1298
1299def cnt.d95(+k: Nat, +lt: {Nat.is_lt(Nat.add(95n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(95n, k)))) == Nat.add(95n, k) : Nat}:
1300 match k:
1301 case 0n:
1302 {==}
1303 case 1n+p:
1304 cnt.d96(p, lt)
1305
1306def cnt.d94(+k: Nat, +lt: {Nat.is_lt(Nat.add(94n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(94n, k)))) == Nat.add(94n, k) : Nat}:
1307 match k:
1308 case 0n:
1309 {==}
1310 case 1n+p:
1311 cnt.d95(p, lt)
1312
1313def cnt.d93(+k: Nat, +lt: {Nat.is_lt(Nat.add(93n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(93n, k)))) == Nat.add(93n, k) : Nat}:
1314 match k:
1315 case 0n:
1316 {==}
1317 case 1n+p:
1318 cnt.d94(p, lt)
1319
1320def cnt.d92(+k: Nat, +lt: {Nat.is_lt(Nat.add(92n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(92n, k)))) == Nat.add(92n, k) : Nat}:
1321 match k:
1322 case 0n:
1323 {==}
1324 case 1n+p:
1325 cnt.d93(p, lt)
1326
1327def cnt.d91(+k: Nat, +lt: {Nat.is_lt(Nat.add(91n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(91n, k)))) == Nat.add(91n, k) : Nat}:
1328 match k:
1329 case 0n:
1330 {==}
1331 case 1n+p:
1332 cnt.d92(p, lt)
1333
1334def cnt.d90(+k: Nat, +lt: {Nat.is_lt(Nat.add(90n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(90n, k)))) == Nat.add(90n, k) : Nat}:
1335 match k:
1336 case 0n:
1337 {==}
1338 case 1n+p:
1339 cnt.d91(p, lt)
1340
1341def cnt.d89(+k: Nat, +lt: {Nat.is_lt(Nat.add(89n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(89n, k)))) == Nat.add(89n, k) : Nat}:
1342 match k:
1343 case 0n:
1344 {==}
1345 case 1n+p:
1346 cnt.d90(p, lt)
1347
1348def cnt.d88(+k: Nat, +lt: {Nat.is_lt(Nat.add(88n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(88n, k)))) == Nat.add(88n, k) : Nat}:
1349 match k:
1350 case 0n:
1351 {==}
1352 case 1n+p:
1353 cnt.d89(p, lt)
1354
1355def cnt.d87(+k: Nat, +lt: {Nat.is_lt(Nat.add(87n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(87n, k)))) == Nat.add(87n, k) : Nat}:
1356 match k:
1357 case 0n:
1358 {==}
1359 case 1n+p:
1360 cnt.d88(p, lt)
1361
1362def cnt.d86(+k: Nat, +lt: {Nat.is_lt(Nat.add(86n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(86n, k)))) == Nat.add(86n, k) : Nat}:
1363 match k:
1364 case 0n:
1365 {==}
1366 case 1n+p:
1367 cnt.d87(p, lt)
1368
1369def cnt.d85(+k: Nat, +lt: {Nat.is_lt(Nat.add(85n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(85n, k)))) == Nat.add(85n, k) : Nat}:
1370 match k:
1371 case 0n:
1372 {==}
1373 case 1n+p:
1374 cnt.d86(p, lt)
1375
1376def cnt.d84(+k: Nat, +lt: {Nat.is_lt(Nat.add(84n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(84n, k)))) == Nat.add(84n, k) : Nat}:
1377 match k:
1378 case 0n:
1379 {==}
1380 case 1n+p:
1381 cnt.d85(p, lt)
1382
1383def cnt.d83(+k: Nat, +lt: {Nat.is_lt(Nat.add(83n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(83n, k)))) == Nat.add(83n, k) : Nat}:
1384 match k:
1385 case 0n:
1386 {==}
1387 case 1n+p:
1388 cnt.d84(p, lt)
1389
1390def cnt.d82(+k: Nat, +lt: {Nat.is_lt(Nat.add(82n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(82n, k)))) == Nat.add(82n, k) : Nat}:
1391 match k:
1392 case 0n:
1393 {==}
1394 case 1n+p:
1395 cnt.d83(p, lt)
1396
1397def cnt.d81(+k: Nat, +lt: {Nat.is_lt(Nat.add(81n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(81n, k)))) == Nat.add(81n, k) : Nat}:
1398 match k:
1399 case 0n:
1400 {==}
1401 case 1n+p:
1402 cnt.d82(p, lt)
1403
1404def cnt.d80(+k: Nat, +lt: {Nat.is_lt(Nat.add(80n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(80n, k)))) == Nat.add(80n, k) : Nat}:
1405 match k:
1406 case 0n:
1407 {==}
1408 case 1n+p:
1409 cnt.d81(p, lt)
1410
1411def cnt.d79(+k: Nat, +lt: {Nat.is_lt(Nat.add(79n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(79n, k)))) == Nat.add(79n, k) : Nat}:
1412 match k:
1413 case 0n:
1414 {==}
1415 case 1n+p:
1416 cnt.d80(p, lt)
1417
1418def cnt.d78(+k: Nat, +lt: {Nat.is_lt(Nat.add(78n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(78n, k)))) == Nat.add(78n, k) : Nat}:
1419 match k:
1420 case 0n:
1421 {==}
1422 case 1n+p:
1423 cnt.d79(p, lt)
1424
1425def cnt.d77(+k: Nat, +lt: {Nat.is_lt(Nat.add(77n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(77n, k)))) == Nat.add(77n, k) : Nat}:
1426 match k:
1427 case 0n:
1428 {==}
1429 case 1n+p:
1430 cnt.d78(p, lt)
1431
1432def cnt.d76(+k: Nat, +lt: {Nat.is_lt(Nat.add(76n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(76n, k)))) == Nat.add(76n, k) : Nat}:
1433 match k:
1434 case 0n:
1435 {==}
1436 case 1n+p:
1437 cnt.d77(p, lt)
1438
1439def cnt.d75(+k: Nat, +lt: {Nat.is_lt(Nat.add(75n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(75n, k)))) == Nat.add(75n, k) : Nat}:
1440 match k:
1441 case 0n:
1442 {==}
1443 case 1n+p:
1444 cnt.d76(p, lt)
1445
1446def cnt.d74(+k: Nat, +lt: {Nat.is_lt(Nat.add(74n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(74n, k)))) == Nat.add(74n, k) : Nat}:
1447 match k:
1448 case 0n:
1449 {==}
1450 case 1n+p:
1451 cnt.d75(p, lt)
1452
1453def cnt.d73(+k: Nat, +lt: {Nat.is_lt(Nat.add(73n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(73n, k)))) == Nat.add(73n, k) : Nat}:
1454 match k:
1455 case 0n:
1456 {==}
1457 case 1n+p:
1458 cnt.d74(p, lt)
1459
1460def cnt.d72(+k: Nat, +lt: {Nat.is_lt(Nat.add(72n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(72n, k)))) == Nat.add(72n, k) : Nat}:
1461 match k:
1462 case 0n:
1463 {==}
1464 case 1n+p:
1465 cnt.d73(p, lt)
1466
1467def cnt.d71(+k: Nat, +lt: {Nat.is_lt(Nat.add(71n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(71n, k)))) == Nat.add(71n, k) : Nat}:
1468 match k:
1469 case 0n:
1470 {==}
1471 case 1n+p:
1472 cnt.d72(p, lt)
1473
1474def cnt.d70(+k: Nat, +lt: {Nat.is_lt(Nat.add(70n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(70n, k)))) == Nat.add(70n, k) : Nat}:
1475 match k:
1476 case 0n:
1477 {==}
1478 case 1n+p:
1479 cnt.d71(p, lt)
1480
1481def cnt.d69(+k: Nat, +lt: {Nat.is_lt(Nat.add(69n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(69n, k)))) == Nat.add(69n, k) : Nat}:
1482 match k:
1483 case 0n:
1484 {==}
1485 case 1n+p:
1486 cnt.d70(p, lt)
1487
1488def cnt.d68(+k: Nat, +lt: {Nat.is_lt(Nat.add(68n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(68n, k)))) == Nat.add(68n, k) : Nat}:
1489 match k:
1490 case 0n:
1491 {==}
1492 case 1n+p:
1493 cnt.d69(p, lt)
1494
1495def cnt.d67(+k: Nat, +lt: {Nat.is_lt(Nat.add(67n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(67n, k)))) == Nat.add(67n, k) : Nat}:
1496 match k:
1497 case 0n:
1498 {==}
1499 case 1n+p:
1500 cnt.d68(p, lt)
1501
1502def cnt.d66(+k: Nat, +lt: {Nat.is_lt(Nat.add(66n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(66n, k)))) == Nat.add(66n, k) : Nat}:
1503 match k:
1504 case 0n:
1505 {==}
1506 case 1n+p:
1507 cnt.d67(p, lt)
1508
1509def cnt.d65(+k: Nat, +lt: {Nat.is_lt(Nat.add(65n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(65n, k)))) == Nat.add(65n, k) : Nat}:
1510 match k:
1511 case 0n:
1512 {==}
1513 case 1n+p:
1514 cnt.d66(p, lt)
1515
1516def cnt.d64(+k: Nat, +lt: {Nat.is_lt(Nat.add(64n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(64n, k)))) == Nat.add(64n, k) : Nat}:
1517 match k:
1518 case 0n:
1519 {==}
1520 case 1n+p:
1521 cnt.d65(p, lt)
1522
1523def cnt.d63(+k: Nat, +lt: {Nat.is_lt(Nat.add(63n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(63n, k)))) == Nat.add(63n, k) : Nat}:
1524 match k:
1525 case 0n:
1526 {==}
1527 case 1n+p:
1528 cnt.d64(p, lt)
1529
1530def cnt.d62(+k: Nat, +lt: {Nat.is_lt(Nat.add(62n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(62n, k)))) == Nat.add(62n, k) : Nat}:
1531 match k:
1532 case 0n:
1533 {==}
1534 case 1n+p:
1535 cnt.d63(p, lt)
1536
1537def cnt.d61(+k: Nat, +lt: {Nat.is_lt(Nat.add(61n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(61n, k)))) == Nat.add(61n, k) : Nat}:
1538 match k:
1539 case 0n:
1540 {==}
1541 case 1n+p:
1542 cnt.d62(p, lt)
1543
1544def cnt.d60(+k: Nat, +lt: {Nat.is_lt(Nat.add(60n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(60n, k)))) == Nat.add(60n, k) : Nat}:
1545 match k:
1546 case 0n:
1547 {==}
1548 case 1n+p:
1549 cnt.d61(p, lt)
1550
1551def cnt.d59(+k: Nat, +lt: {Nat.is_lt(Nat.add(59n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(59n, k)))) == Nat.add(59n, k) : Nat}:
1552 match k:
1553 case 0n:
1554 {==}
1555 case 1n+p:
1556 cnt.d60(p, lt)
1557
1558def cnt.d58(+k: Nat, +lt: {Nat.is_lt(Nat.add(58n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(58n, k)))) == Nat.add(58n, k) : Nat}:
1559 match k:
1560 case 0n:
1561 {==}
1562 case 1n+p:
1563 cnt.d59(p, lt)
1564
1565def cnt.d57(+k: Nat, +lt: {Nat.is_lt(Nat.add(57n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(57n, k)))) == Nat.add(57n, k) : Nat}:
1566 match k:
1567 case 0n:
1568 {==}
1569 case 1n+p:
1570 cnt.d58(p, lt)
1571
1572def cnt.d56(+k: Nat, +lt: {Nat.is_lt(Nat.add(56n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(56n, k)))) == Nat.add(56n, k) : Nat}:
1573 match k:
1574 case 0n:
1575 {==}
1576 case 1n+p:
1577 cnt.d57(p, lt)
1578
1579def cnt.d55(+k: Nat, +lt: {Nat.is_lt(Nat.add(55n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(55n, k)))) == Nat.add(55n, k) : Nat}:
1580 match k:
1581 case 0n:
1582 {==}
1583 case 1n+p:
1584 cnt.d56(p, lt)
1585
1586def cnt.d54(+k: Nat, +lt: {Nat.is_lt(Nat.add(54n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(54n, k)))) == Nat.add(54n, k) : Nat}:
1587 match k:
1588 case 0n:
1589 {==}
1590 case 1n+p:
1591 cnt.d55(p, lt)
1592
1593def cnt.d53(+k: Nat, +lt: {Nat.is_lt(Nat.add(53n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(53n, k)))) == Nat.add(53n, k) : Nat}:
1594 match k:
1595 case 0n:
1596 {==}
1597 case 1n+p:
1598 cnt.d54(p, lt)
1599
1600def cnt.d52(+k: Nat, +lt: {Nat.is_lt(Nat.add(52n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(52n, k)))) == Nat.add(52n, k) : Nat}:
1601 match k:
1602 case 0n:
1603 {==}
1604 case 1n+p:
1605 cnt.d53(p, lt)
1606
1607def cnt.d51(+k: Nat, +lt: {Nat.is_lt(Nat.add(51n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(51n, k)))) == Nat.add(51n, k) : Nat}:
1608 match k:
1609 case 0n:
1610 {==}
1611 case 1n+p:
1612 cnt.d52(p, lt)
1613
1614def cnt.d50(+k: Nat, +lt: {Nat.is_lt(Nat.add(50n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(50n, k)))) == Nat.add(50n, k) : Nat}:
1615 match k:
1616 case 0n:
1617 {==}
1618 case 1n+p:
1619 cnt.d51(p, lt)
1620
1621def cnt.d49(+k: Nat, +lt: {Nat.is_lt(Nat.add(49n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(49n, k)))) == Nat.add(49n, k) : Nat}:
1622 match k:
1623 case 0n:
1624 {==}
1625 case 1n+p:
1626 cnt.d50(p, lt)
1627
1628def cnt.d48(+k: Nat, +lt: {Nat.is_lt(Nat.add(48n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(48n, k)))) == Nat.add(48n, k) : Nat}:
1629 match k:
1630 case 0n:
1631 {==}
1632 case 1n+p:
1633 cnt.d49(p, lt)
1634
1635def cnt.d47(+k: Nat, +lt: {Nat.is_lt(Nat.add(47n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(47n, k)))) == Nat.add(47n, k) : Nat}:
1636 match k:
1637 case 0n:
1638 {==}
1639 case 1n+p:
1640 cnt.d48(p, lt)
1641
1642def cnt.d46(+k: Nat, +lt: {Nat.is_lt(Nat.add(46n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(46n, k)))) == Nat.add(46n, k) : Nat}:
1643 match k:
1644 case 0n:
1645 {==}
1646 case 1n+p:
1647 cnt.d47(p, lt)
1648
1649def cnt.d45(+k: Nat, +lt: {Nat.is_lt(Nat.add(45n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(45n, k)))) == Nat.add(45n, k) : Nat}:
1650 match k:
1651 case 0n:
1652 {==}
1653 case 1n+p:
1654 cnt.d46(p, lt)
1655
1656def cnt.d44(+k: Nat, +lt: {Nat.is_lt(Nat.add(44n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(44n, k)))) == Nat.add(44n, k) : Nat}:
1657 match k:
1658 case 0n:
1659 {==}
1660 case 1n+p:
1661 cnt.d45(p, lt)
1662
1663def cnt.d43(+k: Nat, +lt: {Nat.is_lt(Nat.add(43n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(43n, k)))) == Nat.add(43n, k) : Nat}:
1664 match k:
1665 case 0n:
1666 {==}
1667 case 1n+p:
1668 cnt.d44(p, lt)
1669
1670def cnt.d42(+k: Nat, +lt: {Nat.is_lt(Nat.add(42n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(42n, k)))) == Nat.add(42n, k) : Nat}:
1671 match k:
1672 case 0n:
1673 {==}
1674 case 1n+p:
1675 cnt.d43(p, lt)
1676
1677def cnt.d41(+k: Nat, +lt: {Nat.is_lt(Nat.add(41n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(41n, k)))) == Nat.add(41n, k) : Nat}:
1678 match k:
1679 case 0n:
1680 {==}
1681 case 1n+p:
1682 cnt.d42(p, lt)
1683
1684def cnt.d40(+k: Nat, +lt: {Nat.is_lt(Nat.add(40n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(40n, k)))) == Nat.add(40n, k) : Nat}:
1685 match k:
1686 case 0n:
1687 {==}
1688 case 1n+p:
1689 cnt.d41(p, lt)
1690
1691def cnt.d39(+k: Nat, +lt: {Nat.is_lt(Nat.add(39n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(39n, k)))) == Nat.add(39n, k) : Nat}:
1692 match k:
1693 case 0n:
1694 {==}
1695 case 1n+p:
1696 cnt.d40(p, lt)
1697
1698def cnt.d38(+k: Nat, +lt: {Nat.is_lt(Nat.add(38n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(38n, k)))) == Nat.add(38n, k) : Nat}:
1699 match k:
1700 case 0n:
1701 {==}
1702 case 1n+p:
1703 cnt.d39(p, lt)
1704
1705def cnt.d37(+k: Nat, +lt: {Nat.is_lt(Nat.add(37n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(37n, k)))) == Nat.add(37n, k) : Nat}:
1706 match k:
1707 case 0n:
1708 {==}
1709 case 1n+p:
1710 cnt.d38(p, lt)
1711
1712def cnt.d36(+k: Nat, +lt: {Nat.is_lt(Nat.add(36n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(36n, k)))) == Nat.add(36n, k) : Nat}:
1713 match k:
1714 case 0n:
1715 {==}
1716 case 1n+p:
1717 cnt.d37(p, lt)
1718
1719def cnt.d35(+k: Nat, +lt: {Nat.is_lt(Nat.add(35n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(35n, k)))) == Nat.add(35n, k) : Nat}:
1720 match k:
1721 case 0n:
1722 {==}
1723 case 1n+p:
1724 cnt.d36(p, lt)
1725
1726def cnt.d34(+k: Nat, +lt: {Nat.is_lt(Nat.add(34n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(34n, k)))) == Nat.add(34n, k) : Nat}:
1727 match k:
1728 case 0n:
1729 {==}
1730 case 1n+p:
1731 cnt.d35(p, lt)
1732
1733def cnt.d33(+k: Nat, +lt: {Nat.is_lt(Nat.add(33n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(33n, k)))) == Nat.add(33n, k) : Nat}:
1734 match k:
1735 case 0n:
1736 {==}
1737 case 1n+p:
1738 cnt.d34(p, lt)
1739
1740def cnt.d32(+k: Nat, +lt: {Nat.is_lt(Nat.add(32n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(32n, k)))) == Nat.add(32n, k) : Nat}:
1741 match k:
1742 case 0n:
1743 {==}
1744 case 1n+p:
1745 cnt.d33(p, lt)
1746
1747def cnt.d31(+k: Nat, +lt: {Nat.is_lt(Nat.add(31n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(31n, k)))) == Nat.add(31n, k) : Nat}:
1748 match k:
1749 case 0n:
1750 {==}
1751 case 1n+p:
1752 cnt.d32(p, lt)
1753
1754def cnt.d30(+k: Nat, +lt: {Nat.is_lt(Nat.add(30n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(30n, k)))) == Nat.add(30n, k) : Nat}:
1755 match k:
1756 case 0n:
1757 {==}
1758 case 1n+p:
1759 cnt.d31(p, lt)
1760
1761def cnt.d29(+k: Nat, +lt: {Nat.is_lt(Nat.add(29n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(29n, k)))) == Nat.add(29n, k) : Nat}:
1762 match k:
1763 case 0n:
1764 {==}
1765 case 1n+p:
1766 cnt.d30(p, lt)
1767
1768def cnt.d28(+k: Nat, +lt: {Nat.is_lt(Nat.add(28n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(28n, k)))) == Nat.add(28n, k) : Nat}:
1769 match k:
1770 case 0n:
1771 {==}
1772 case 1n+p:
1773 cnt.d29(p, lt)
1774
1775def cnt.d27(+k: Nat, +lt: {Nat.is_lt(Nat.add(27n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(27n, k)))) == Nat.add(27n, k) : Nat}:
1776 match k:
1777 case 0n:
1778 {==}
1779 case 1n+p:
1780 cnt.d28(p, lt)
1781
1782def cnt.d26(+k: Nat, +lt: {Nat.is_lt(Nat.add(26n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(26n, k)))) == Nat.add(26n, k) : Nat}:
1783 match k:
1784 case 0n:
1785 {==}
1786 case 1n+p:
1787 cnt.d27(p, lt)
1788
1789def cnt.d25(+k: Nat, +lt: {Nat.is_lt(Nat.add(25n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(25n, k)))) == Nat.add(25n, k) : Nat}:
1790 match k:
1791 case 0n:
1792 {==}
1793 case 1n+p:
1794 cnt.d26(p, lt)
1795
1796def cnt.d24(+k: Nat, +lt: {Nat.is_lt(Nat.add(24n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(24n, k)))) == Nat.add(24n, k) : Nat}:
1797 match k:
1798 case 0n:
1799 {==}
1800 case 1n+p:
1801 cnt.d25(p, lt)
1802
1803def cnt.d23(+k: Nat, +lt: {Nat.is_lt(Nat.add(23n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(23n, k)))) == Nat.add(23n, k) : Nat}:
1804 match k:
1805 case 0n:
1806 {==}
1807 case 1n+p:
1808 cnt.d24(p, lt)
1809
1810def cnt.d22(+k: Nat, +lt: {Nat.is_lt(Nat.add(22n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(22n, k)))) == Nat.add(22n, k) : Nat}:
1811 match k:
1812 case 0n:
1813 {==}
1814 case 1n+p:
1815 cnt.d23(p, lt)
1816
1817def cnt.d21(+k: Nat, +lt: {Nat.is_lt(Nat.add(21n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(21n, k)))) == Nat.add(21n, k) : Nat}:
1818 match k:
1819 case 0n:
1820 {==}
1821 case 1n+p:
1822 cnt.d22(p, lt)
1823
1824def cnt.d20(+k: Nat, +lt: {Nat.is_lt(Nat.add(20n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(20n, k)))) == Nat.add(20n, k) : Nat}:
1825 match k:
1826 case 0n:
1827 {==}
1828 case 1n+p:
1829 cnt.d21(p, lt)
1830
1831def cnt.d19(+k: Nat, +lt: {Nat.is_lt(Nat.add(19n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(19n, k)))) == Nat.add(19n, k) : Nat}:
1832 match k:
1833 case 0n:
1834 {==}
1835 case 1n+p:
1836 cnt.d20(p, lt)
1837
1838def cnt.d18(+k: Nat, +lt: {Nat.is_lt(Nat.add(18n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(18n, k)))) == Nat.add(18n, k) : Nat}:
1839 match k:
1840 case 0n:
1841 {==}
1842 case 1n+p:
1843 cnt.d19(p, lt)
1844
1845def cnt.d17(+k: Nat, +lt: {Nat.is_lt(Nat.add(17n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(17n, k)))) == Nat.add(17n, k) : Nat}:
1846 match k:
1847 case 0n:
1848 {==}
1849 case 1n+p:
1850 cnt.d18(p, lt)
1851
1852def cnt.d16(+k: Nat, +lt: {Nat.is_lt(Nat.add(16n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(16n, k)))) == Nat.add(16n, k) : Nat}:
1853 match k:
1854 case 0n:
1855 {==}
1856 case 1n+p:
1857 cnt.d17(p, lt)
1858
1859def cnt.d15(+k: Nat, +lt: {Nat.is_lt(Nat.add(15n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(15n, k)))) == Nat.add(15n, k) : Nat}:
1860 match k:
1861 case 0n:
1862 {==}
1863 case 1n+p:
1864 cnt.d16(p, lt)
1865
1866def cnt.d14(+k: Nat, +lt: {Nat.is_lt(Nat.add(14n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(14n, k)))) == Nat.add(14n, k) : Nat}:
1867 match k:
1868 case 0n:
1869 {==}
1870 case 1n+p:
1871 cnt.d15(p, lt)
1872
1873def cnt.d13(+k: Nat, +lt: {Nat.is_lt(Nat.add(13n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(13n, k)))) == Nat.add(13n, k) : Nat}:
1874 match k:
1875 case 0n:
1876 {==}
1877 case 1n+p:
1878 cnt.d14(p, lt)
1879
1880def cnt.d12(+k: Nat, +lt: {Nat.is_lt(Nat.add(12n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(12n, k)))) == Nat.add(12n, k) : Nat}:
1881 match k:
1882 case 0n:
1883 {==}
1884 case 1n+p:
1885 cnt.d13(p, lt)
1886
1887def cnt.d11(+k: Nat, +lt: {Nat.is_lt(Nat.add(11n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(11n, k)))) == Nat.add(11n, k) : Nat}:
1888 match k:
1889 case 0n:
1890 {==}
1891 case 1n+p:
1892 cnt.d12(p, lt)
1893
1894def cnt.d10(+k: Nat, +lt: {Nat.is_lt(Nat.add(10n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(10n, k)))) == Nat.add(10n, k) : Nat}:
1895 match k:
1896 case 0n:
1897 {==}
1898 case 1n+p:
1899 cnt.d11(p, lt)
1900
1901def cnt.d9(+k: Nat, +lt: {Nat.is_lt(Nat.add(9n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(9n, k)))) == Nat.add(9n, k) : Nat}:
1902 match k:
1903 case 0n:
1904 {==}
1905 case 1n+p:
1906 cnt.d10(p, lt)
1907
1908def cnt.d8(+k: Nat, +lt: {Nat.is_lt(Nat.add(8n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(8n, k)))) == Nat.add(8n, k) : Nat}:
1909 match k:
1910 case 0n:
1911 {==}
1912 case 1n+p:
1913 cnt.d9(p, lt)
1914
1915def cnt.d7(+k: Nat, +lt: {Nat.is_lt(Nat.add(7n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(7n, k)))) == Nat.add(7n, k) : Nat}:
1916 match k:
1917 case 0n:
1918 {==}
1919 case 1n+p:
1920 cnt.d8(p, lt)
1921
1922def cnt.d6(+k: Nat, +lt: {Nat.is_lt(Nat.add(6n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(6n, k)))) == Nat.add(6n, k) : Nat}:
1923 match k:
1924 case 0n:
1925 {==}
1926 case 1n+p:
1927 cnt.d7(p, lt)
1928
1929def cnt.d5(+k: Nat, +lt: {Nat.is_lt(Nat.add(5n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(5n, k)))) == Nat.add(5n, k) : Nat}:
1930 match k:
1931 case 0n:
1932 {==}
1933 case 1n+p:
1934 cnt.d6(p, lt)
1935
1936def cnt.d4(+k: Nat, +lt: {Nat.is_lt(Nat.add(4n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(4n, k)))) == Nat.add(4n, k) : Nat}:
1937 match k:
1938 case 0n:
1939 {==}
1940 case 1n+p:
1941 cnt.d5(p, lt)
1942
1943def cnt.d3(+k: Nat, +lt: {Nat.is_lt(Nat.add(3n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(3n, k)))) == Nat.add(3n, k) : Nat}:
1944 match k:
1945 case 0n:
1946 {==}
1947 case 1n+p:
1948 cnt.d4(p, lt)
1949
1950def cnt.d2(+k: Nat, +lt: {Nat.is_lt(Nat.add(2n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(2n, k)))) == Nat.add(2n, k) : Nat}:
1951 match k:
1952 case 0n:
1953 {==}
1954 case 1n+p:
1955 cnt.d3(p, lt)
1956
1957def cnt.d1(+k: Nat, +lt: {Nat.is_lt(Nat.add(1n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(1n, k)))) == Nat.add(1n, k) : Nat}:
1958 match k:
1959 case 0n:
1960 {==}
1961 case 1n+p:
1962 cnt.d2(p, lt)
1963
1964def cnt.d0(+k: Nat, +lt: {Nat.is_lt(Nat.add(0n, k), 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(Nat.add(0n, k)))) == Nat.add(0n, k) : Nat}:
1965 match k:
1966 case 0n:
1967 {==}
1968 case 1n+p:
1969 cnt.d1(p, lt)
1970
1971def cnt_rt(+k: Nat, +lt: {Nat.is_lt(k, 256n) == True{} : Bool}) -> {U32.to_nat(B.byte(U32.from_nat(k))) == k : Nat}:
1972 cnt.d0(k, lt)
1973
1974def Laws.pkglength_round_trip(v, rest, fits):
1975 %Equal.sym(List<&2, U32>, B.Octets.to_list(B.Octets.append(K.AmlPkgLength.encode(v), rest)), B.append(B.Octets.to_list(K.AmlPkgLength.encode(v)), B.Octets.to_list(rest)), BL.octets_append_list(K.AmlPkgLength.encode(v), rest)) : {K.pk.pub(K.pk.dec(_)) == Done{K.AmlPkgLen{v, rest}} : Result<&2, &2, E.AcpiError, K.AmlPkgLen>}
1976 %Equal.sym(List<&2, U32>, B.Octets.to_list(B.Octets.of_list(K.pk.enc(v))), B.mask(K.pk.enc(v)), BL.octets_to_of(K.pk.enc(v))) : {K.pk.pub(K.pk.dec(B.append(_, B.Octets.to_list(rest)))) == Done{K.AmlPkgLen{v, rest}} : Result<&2, &2, E.AcpiError, K.AmlPkgLen>}
1977 %BL.octets_of_to(rest) : {K.pk.pub(K.pk.dec(B.append(B.mask(K.pk.enc(v)), B.Octets.to_list(rest)))) == Done{K.AmlPkgLen{v, _}} : Result<&2, &2, E.AcpiError, K.AmlPkgLen>}
1978 pk_rt(v, B.Octets.to_list(rest), fits)
1979# Lists and masks
1980
1981def app_assoc(+a: List<&2, U32>, +b: List<&2, U32>, +c: List<&2, U32>) -> {B.append(a, B.append(b, c)) == B.append(B.append(a, b), c) : List<&2, U32>}:
1982 match a:
1983 case Nil{}:
1984 {==}
1985 case Con{h, t}:
1986 %app_assoc(t, b, c) : {Con{h, B.append(t, B.append(b, c))} == Con{h, _} : List<&2, U32>}
1987 {==}
1988
1989def mask_app(+a: List<&2, U32>, +b: List<&2, U32>) -> {B.append(B.mask(a), B.mask(b)) == B.mask(B.append(a, b)) : List<&2, U32>}:
1990 match a:
1991 case Nil{}:
1992 {==}
1993 case Con{h, t}:
1994 %mask_app(t, b) : {Con{B.byte(h), B.append(B.mask(t), B.mask(b))} == Con{B.byte(h), _} : List<&2, U32>}
1995 {==}
1996
1997def mask_tl(+o: B.Octets) -> {B.Octets.to_list(o) == B.mask(B.Octets.to_list(o)) : List<&2, U32>}:
1998 %BL.octets_to_of(B.Octets.to_list(o)) : {B.Octets.to_list(o) == _ : List<&2, U32>}
1999 %Equal.sym(B.Octets, B.Octets.of_list(B.Octets.to_list(o)), o, BL.octets_of_to(o)) : {B.Octets.to_list(o) == B.Octets.to_list(_) : List<&2, U32>}
2000 {==}
2001
2002def and_l(+a: Bool, +b: Bool, +e: {Bool.and(a, b) == True{} : Bool}) -> {a == True{} : Bool}:
2003 match a:
2004 case True{}:
2005 {==}
2006 case False{}:
2007 Empty.absurd({False{} == True{} : Bool}, ft_absurd(e))
2008
2009def and_r(+a: Bool, +b: Bool, +e: {Bool.and(a, b) == True{} : Bool}) -> {b == True{} : Bool}:
2010 match a:
2011 case True{}:
2012 e
2013 case False{}:
2014 Empty.absurd({b == True{} : Bool}, ft_absurd(e))
2015
2016# NameStrings. The encoder's bytes are bytes already: masking them changes
2017# nothing but the SegCount, which stays byte(from_nat(count)).
2018
2019def mask_segs(+ss: List<&2, B.Octets>) -> {N.nm.segs.list(ss) == B.mask(N.nm.segs.list(ss)) : List<&2, U32>}:
2020 match ss:
2021 case Nil{}:
2022 {==}
2023 case Con{s, t}:
2024 %mask_app(B.Octets.to_list(s), N.nm.segs.list(t)) : {B.append(B.Octets.to_list(s), N.nm.segs.list(t)) == _ : List<&2, U32>}
2025 %mask_tl(s) : {B.append(B.Octets.to_list(s), N.nm.segs.list(t)) == B.append(_, B.mask(N.nm.segs.list(t))) : List<&2, U32>}
2026 %mask_segs(t) : {B.append(B.Octets.to_list(s), N.nm.segs.list(t)) == B.append(B.Octets.to_list(s), _) : List<&2, U32>}
2027 {==}
2028
2029def mask_carets(+u: Nat) -> {N.nm.carets(u) == B.mask(N.nm.carets(u)) : List<&2, U32>}:
2030 match u:
2031 case 0n:
2032 {==}
2033 case 1n+p:
2034 %mask_carets(p) : {Con{94, N.nm.carets(p)} == Con{94, _} : List<&2, U32>}
2035 {==}
2036
2037def is_seg_t(+k: N.AmlLeadKind, +e: {N.AmlLead.is_seg(k) == True{} : Bool}) -> {N.AmlLSeg{} == k : N.AmlLeadKind}:
2038 match k:
2039 case N.AmlLSeg{}:
2040 {==}
2041 case N.AmlLRoot{}:
2042 Empty.absurd({N.AmlLSeg{} == N.AmlLRoot{} : N.AmlLeadKind}, ft_absurd(e))
2043 case N.AmlLParent{}:
2044 Empty.absurd({N.AmlLSeg{} == N.AmlLParent{} : N.AmlLeadKind}, ft_absurd(e))
2045 case N.AmlLDual{}:
2046 Empty.absurd({N.AmlLSeg{} == N.AmlLDual{} : N.AmlLeadKind}, ft_absurd(e))
2047 case N.AmlLMulti{}:
2048 Empty.absurd({N.AmlLSeg{} == N.AmlLMulti{} : N.AmlLeadKind}, ft_absurd(e))
2049 case N.AmlLNull{}:
2050 Empty.absurd({N.AmlLSeg{} == N.AmlLNull{} : N.AmlLeadKind}, ft_absurd(e))
2051 case N.AmlLOther{}:
2052 Empty.absurd({N.AmlLSeg{} == N.AmlLOther{} : N.AmlLeadKind}, ft_absurd(e))
2053
2054# a NameSeg's first byte is a LeadNameChar
2055def seg_kind(+c0: U32, +c1: U32, +c2: U32, +c3: U32, +ok: {N.nm.seg_ok4(c0, c1, c2, c3) == True{} : Bool}) -> {N.AmlLSeg{} == N.AmlLead.classify(c0) : N.AmlLeadKind}:
2056 is_seg_t(N.AmlLead.classify(c0), and_l(N.AmlLead.is_seg(N.AmlLead.classify(c0)), Bool.and(N.AmlName.name_char(c1), Bool.and(N.AmlName.name_char(c2), N.AmlName.name_char(c3))), ok))
2057
2058def seg_l(+s: B.Octets, +L: List<&2, U32>, +R: List<&2, U32>, +e: {B.Octets.to_list(s) == L : List<&2, U32>}, +ok: {N.nm.seg_ok.list(L) == True{} : Bool}) -> {Done{N.AmlSegL{s, R}} == N.nm.seg(B.append(L, R)) : Result<&2, &2, E.AcpiError, N.AmlSegL>}:
2059 match L:
2060 case Nil{}:
2061 Empty.absurd({Done{N.AmlSegL{s, R}} == N.nm.seg(B.append(Nil{}, R)) : Result<&2, &2, E.AcpiError, N.AmlSegL>}, ft_absurd(ok))
2062 case Con{c0, L1}:
2063 match L1:
2064 case Nil{}:
2065 Empty.absurd({Done{N.AmlSegL{s, R}} == N.nm.seg(B.append(Con{c0, Nil{}}, R)) : Result<&2, &2, E.AcpiError, N.AmlSegL>}, ft_absurd(ok))
2066 case Con{c1, L2}:
2067 match L2:
2068 case Nil{}:
2069 Empty.absurd({Done{N.AmlSegL{s, R}} == N.nm.seg(B.append(Con{c0, Con{c1, Nil{}}}, R)) : Result<&2, &2, E.AcpiError, N.AmlSegL>}, ft_absurd(ok))
2070 case Con{c2, L3}:
2071 match L3:
2072 case Nil{}:
2073 Empty.absurd({Done{N.AmlSegL{s, R}} == N.nm.seg(B.append(Con{c0, Con{c1, Con{c2, Nil{}}}}, R)) : Result<&2, &2, E.AcpiError, N.AmlSegL>}, ft_absurd(ok))
2074 case Con{c3, L4}:
2075 match L4:
2076 case Con{c4, L5}:
2077 Empty.absurd({Done{N.AmlSegL{s, R}} == N.nm.seg(B.append(Con{c0, Con{c1, Con{c2, Con{c3, Con{c4, L5}}}}}, R)) : Result<&2, &2, E.AcpiError, N.AmlSegL>}, ft_absurd(ok))
2078 case Nil{}:
2079 %Equal.sym(Bool, N.nm.seg_ok4(c0, c1, c2, c3), True{}, ok) : {Done{N.AmlSegL{s, R}} == N.nm.seg.pick(_, c0, c1, c2, c3, R) : Result<&2, &2, E.AcpiError, N.AmlSegL>}
2080 %BL.octets_of_to(s) : {Done{N.AmlSegL{_, R}} == Done{N.AmlSegL{B.Octets.of_list(Con{c0, Con{c1, Con{c2, Con{c3, Nil{}}}}}), R}} : Result<&2, &2, E.AcpiError, N.AmlSegL>}
2081 %e : {Done{N.AmlSegL{B.Octets.of_list(B.Octets.to_list(s)), R}} == Done{N.AmlSegL{B.Octets.of_list(_), R}} : Result<&2, &2, E.AcpiError, N.AmlSegL>}
2082 {==}
2083
2084def pth1_dpath(+s: B.Octets, +L: List<&2, U32>, +R: List<&2, U32>, +e: {B.Octets.to_list(s) == L : List<&2, U32>}, +ok: {N.nm.seg_ok.list(L) == True{} : Bool}) -> {Done{N.AmlSegsL{[s], R}} == N.nm.dpath(B.append(B.append(L, Nil{}), R)) : Result<&2, &2, E.AcpiError, N.AmlSegsL>}:
2085 match L:
2086 case Nil{}:
2087 Empty.absurd({Done{N.AmlSegsL{[s], R}} == N.nm.dpath(B.append(B.append(Nil{}, Nil{}), R)) : Result<&2, &2, E.AcpiError, N.AmlSegsL>}, ft_absurd(ok))
2088 case Con{c0, L1}:
2089 match L1:
2090 case Nil{}:
2091 Empty.absurd({Done{N.AmlSegsL{[s], R}} == N.nm.dpath(B.append(B.append(Con{c0, Nil{}}, Nil{}), R)) : Result<&2, &2, E.AcpiError, N.AmlSegsL>}, ft_absurd(ok))
2092 case Con{c1, L2}:
2093 match L2:
2094 case Nil{}:
2095 Empty.absurd({Done{N.AmlSegsL{[s], R}} == N.nm.dpath(B.append(B.append(Con{c0, Con{c1, Nil{}}}, Nil{}), R)) : Result<&2, &2, E.AcpiError, N.AmlSegsL>}, ft_absurd(ok))
2096 case Con{c2, L3}:
2097 match L3:
2098 case Nil{}:
2099 Empty.absurd({Done{N.AmlSegsL{[s], R}} == N.nm.dpath(B.append(B.append(Con{c0, Con{c1, Con{c2, Nil{}}}}, Nil{}), R)) : Result<&2, &2, E.AcpiError, N.AmlSegsL>}, ft_absurd(ok))
2100 case Con{c3, L4}:
2101 match L4:
2102 case Con{c4, L5}:
2103 Empty.absurd({Done{N.AmlSegsL{[s], R}} == N.nm.dpath(B.append(B.append(Con{c0, Con{c1, Con{c2, Con{c3, Con{c4, L5}}}}}, Nil{}), R)) : Result<&2, &2, E.AcpiError, N.AmlSegsL>}, ft_absurd(ok))
2104 case Nil{}:
2105 %seg_kind(c0, c1, c2, c3, ok) : {Done{N.AmlSegsL{[s], R}} == N.nm.path.k(_, c0, Con{c1, Con{c2, Con{c3, R}}}) : Result<&2, &2, E.AcpiError, N.AmlSegsL>}
2106 %seg_l(s, Con{c0, Con{c1, Con{c2, Con{c3, Nil{}}}}}, R, e, ok) : {Done{N.AmlSegsL{[s], R}} == N.nm.segs.go(0n, _) : Result<&2, &2, E.AcpiError, N.AmlSegsL>}
2107 {==}
2108
2109def pth1_dec(+s: B.Octets, +L: List<&2, U32>, +R: List<&2, U32>, +e: {B.Octets.to_list(s) == L : List<&2, U32>}, +ok: {N.nm.seg_ok.list(L) == True{} : Bool}) -> {Done{N.AmlNameL{N.AmlName{False{}, 0n, [s]}, R}} == N.nm.dec(B.append(B.append(L, Nil{}), R)) : Result<&2, &2, E.AcpiError, N.AmlNameL>}:
2110 match L:
2111 case Nil{}:
2112 Empty.absurd({Done{N.AmlNameL{N.AmlName{False{}, 0n, [s]}, R}} == N.nm.dec(B.append(B.append(Nil{}, Nil{}), R)) : Result<&2, &2, E.AcpiError, N.AmlNameL>}, ft_absurd(ok))
2113 case Con{c0, L1}:
2114 match L1:
2115 case Nil{}:
2116 Empty.absurd({Done{N.AmlNameL{N.AmlName{False{}, 0n, [s]}, R}} == N.nm.dec(B.append(B.append(Con{c0, Nil{}}, Nil{}), R)) : Result<&2, &2, E.AcpiError, N.AmlNameL>}, ft_absurd(ok))
2117 case Con{c1, L2}:
2118 match L2:
2119 case Nil{}:
2120 Empty.absurd({Done{N.AmlNameL{N.AmlName{False{}, 0n, [s]}, R}} == N.nm.dec(B.append(B.append(Con{c0, Con{c1, Nil{}}}, Nil{}), R)) : Result<&2, &2, E.AcpiError, N.AmlNameL>}, ft_absurd(ok))
2121 case Con{c2, L3}:
2122 match L3:
2123 case Nil{}:
2124 Empty.absurd({Done{N.AmlNameL{N.AmlName{False{}, 0n, [s]}, R}} == N.nm.dec(B.append(B.append(Con{c0, Con{c1, Con{c2, Nil{}}}}, Nil{}), R)) : Result<&2, &2, E.AcpiError, N.AmlNameL>}, ft_absurd(ok))
2125 case Con{c3, L4}:
2126 match L4:
2127 case Con{c4, L5}:
2128 Empty.absurd({Done{N.AmlNameL{N.AmlName{False{}, 0n, [s]}, R}} == N.nm.dec(B.append(B.append(Con{c0, Con{c1, Con{c2, Con{c3, Con{c4, L5}}}}}, Nil{}), R)) : Result<&2, &2, E.AcpiError, N.AmlNameL>}, ft_absurd(ok))
2129 case Nil{}:
2130 %seg_kind(c0, c1, c2, c3, ok) : {Done{N.AmlNameL{N.AmlName{False{}, 0n, [s]}, R}} == N.nm.dec.k(_, c0, Con{c1, Con{c2, Con{c3, R}}}) : Result<&2, &2, E.AcpiError, N.AmlNameL>}
2131 %seg_l(s, Con{c0, Con{c1, Con{c2, Con{c3, Nil{}}}}}, R, e, ok) : {Done{N.AmlNameL{N.AmlName{False{}, 0n, [s]}, R}} == N.nm.named(False{}, 0n, N.nm.segs.go(0n, _)) : Result<&2, &2, E.AcpiError, N.AmlNameL>}
2132 {==}
2133
2134def pth1_ups(+s: B.Octets, +L: List<&2, U32>, +R: List<&2, U32>, +e: {B.Octets.to_list(s) == L : List<&2, U32>}, +ok: {N.nm.seg_ok.list(L) == True{} : Bool}) -> {Done{N.AmlNameL{N.AmlName{False{}, 0n, [s]}, R}} == N.nm.ups(B.append(B.append(L, Nil{}), R), N.nm.head_kind(B.append(B.append(L, Nil{}), R))) : Result<&2, &2, E.AcpiError, N.AmlNameL>}:
2135 match L:
2136 case Nil{}:
2137 Empty.absurd({Done{N.AmlNameL{N.AmlName{False{}, 0n, [s]}, R}} == N.nm.ups(B.append(B.append(Nil{}, Nil{}), R), N.nm.head_kind(B.append(B.append(Nil{}, Nil{}), R))) : Result<&2, &2, E.AcpiError, N.AmlNameL>}, ft_absurd(ok))
2138 case Con{c0, L1}:
2139 match L1:
2140 case Nil{}:
2141 Empty.absurd({Done{N.AmlNameL{N.AmlName{False{}, 0n, [s]}, R}} == N.nm.ups(B.append(B.append(Con{c0, Nil{}}, Nil{}), R), N.nm.head_kind(B.append(B.append(Con{c0, Nil{}}, Nil{}), R))) : Result<&2, &2, E.AcpiError, N.AmlNameL>}, ft_absurd(ok))
2142 case Con{c1, L2}:
2143 match L2:
2144 case Nil{}:
2145 Empty.absurd({Done{N.AmlNameL{N.AmlName{False{}, 0n, [s]}, R}} == N.nm.ups(B.append(B.append(Con{c0, Con{c1, Nil{}}}, Nil{}), R), N.nm.head_kind(B.append(B.append(Con{c0, Con{c1, Nil{}}}, Nil{}), R))) : Result<&2, &2, E.AcpiError, N.AmlNameL>}, ft_absurd(ok))
2146 case Con{c2, L3}:
2147 match L3:
2148 case Nil{}:
2149 Empty.absurd({Done{N.AmlNameL{N.AmlName{False{}, 0n, [s]}, R}} == N.nm.ups(B.append(B.append(Con{c0, Con{c1, Con{c2, Nil{}}}}, Nil{}), R), N.nm.head_kind(B.append(B.append(Con{c0, Con{c1, Con{c2, Nil{}}}}, Nil{}), R))) : Result<&2, &2, E.AcpiError, N.AmlNameL>}, ft_absurd(ok))
2150 case Con{c3, L4}:
2151 match L4:
2152 case Con{c4, L5}:
2153 Empty.absurd({Done{N.AmlNameL{N.AmlName{False{}, 0n, [s]}, R}} == N.nm.ups(B.append(B.append(Con{c0, Con{c1, Con{c2, Con{c3, Con{c4, L5}}}}}, Nil{}), R), N.nm.head_kind(B.append(B.append(Con{c0, Con{c1, Con{c2, Con{c3, Con{c4, L5}}}}}, Nil{}), R))) : Result<&2, &2, E.AcpiError, N.AmlNameL>}, ft_absurd(ok))
2154 case Nil{}:
2155 %seg_kind(c0, c1, c2, c3, ok) : {Done{N.AmlNameL{N.AmlName{False{}, 0n, [s]}, R}} == N.nm.ups(Con{c0, Con{c1, Con{c2, Con{c3, R}}}}, _) : Result<&2, &2, E.AcpiError, N.AmlNameL>}
2156 %seg_l(s, Con{c0, Con{c1, Con{c2, Con{c3, Nil{}}}}}, R, e, ok) : {Done{N.AmlNameL{N.AmlName{False{}, 0n, [s]}, R}} == N.nm.named(False{}, 0n, N.nm.segs.go(0n, _)) : Result<&2, &2, E.AcpiError, N.AmlNameL>}
2157 {==}
2158
2159def seg_rt(+s: B.Octets, +R: List<&2, U32>, +ok: {N.AmlName.seg_ok(s) == True{} : Bool}) -> {Done{N.AmlSegL{s, R}} == N.nm.seg(B.append(B.Octets.to_list(s), R)) : Result<&2, &2, E.AcpiError, N.AmlSegL>}:
2160 seg_l(s, B.Octets.to_list(s), R, {==}, ok)
2161
2162# segments read back one after another
2163def segs_go_rt(+t: List<&2, B.Octets>, +s: B.Octets, +R: List<&2, U32>, +oks: {N.AmlName.segs_ok(Con{s, t}) == True{} : Bool}) -> {Done{N.AmlSegsL{Con{s, t}, R}} == N.nm.segs.go(N.nm.len(t), N.nm.seg(B.append(B.Octets.to_list(s), B.append(N.nm.segs.list(t), R)))) : Result<&2, &2, E.AcpiError, N.AmlSegsL>}:
2164 match t:
2165 case Nil{}:
2166 %seg_rt(s, R, and_l(N.AmlName.seg_ok(s), True{}, oks)) : {Done{N.AmlSegsL{[s], R}} == N.nm.segs.go(0n, _) : Result<&2, &2, E.AcpiError, N.AmlSegsL>}
2167 {==}
2168 case Con{s2, t2}:
2169 %seg_rt(s, B.append(N.nm.segs.list(Con{s2, t2}), R), and_l(N.AmlName.seg_ok(s), N.AmlName.segs_ok(Con{s2, t2}), oks)) : {Done{N.AmlSegsL{Con{s, Con{s2, t2}}, R}} == N.nm.segs.go(1n+N.nm.len(t2), _) : Result<&2, &2, E.AcpiError, N.AmlSegsL>}
2170 %app_assoc(B.Octets.to_list(s2), N.nm.segs.list(t2), R) : {Done{N.AmlSegsL{Con{s, Con{s2, t2}}, R}} == N.nm.cons(s, N.nm.segs.go(N.nm.len(t2), N.nm.seg(_))) : Result<&2, &2, E.AcpiError, N.AmlSegsL>}
2171 %segs_go_rt(t2, s2, R, and_r(N.AmlName.seg_ok(s), N.AmlName.segs_ok(Con{s2, t2}), oks)) : {Done{N.AmlSegsL{Con{s, Con{s2, t2}}, R}} == N.nm.cons(s, _) : Result<&2, &2, E.AcpiError, N.AmlSegsL>}
2172 {==}
2173
2174def segs_rt(+ss: List<&2, B.Octets>, +R: List<&2, U32>, +oks: {N.AmlName.segs_ok(ss) == True{} : Bool}) -> {Done{N.AmlSegsL{ss, R}} == N.nm.segs(N.nm.len(ss), B.append(N.nm.segs.list(ss), R)) : Result<&2, &2, E.AcpiError, N.AmlSegsL>}:
2175 match ss:
2176 case Nil{}:
2177 {==}
2178 case Con{s, t}:
2179 %app_assoc(B.Octets.to_list(s), N.nm.segs.list(t), R) : {Done{N.AmlSegsL{Con{s, t}, R}} == N.nm.segs.go(N.nm.len(t), N.nm.seg(_)) : Result<&2, &2, E.AcpiError, N.AmlSegsL>}
2180 segs_go_rt(t, s, R, oks)
2181
2182def pth_dpath(+ss: List<&2, B.Octets>, +R: List<&2, U32>, +oks: {N.AmlName.segs_ok(ss) == True{} : Bool}, +lt: {Nat.is_lt(N.nm.len(ss), 256n) == True{} : Bool}) -> {Done{N.AmlSegsL{ss, R}} == N.nm.dpath(B.append(B.mask(N.nm.path(ss)), R)) : Result<&2, &2, E.AcpiError, N.AmlSegsL>}:
2183 match ss:
2184 case Nil{}:
2185 {==}
2186 case Con{s, t}:
2187 match t:
2188 case Nil{}:
2189 %mask_segs(Con{s, Nil{}}) : {Done{N.AmlSegsL{Con{s, Nil{}}, R}} == N.nm.dpath(B.append(_, R)) : Result<&2, &2, E.AcpiError, N.AmlSegsL>}
2190 pth1_dpath(s, B.Octets.to_list(s), R, {==}, and_l(N.AmlName.seg_ok(s), True{}, oks))
2191 case Con{s2, t2}:
2192 match t2:
2193 case Nil{}:
2194 %mask_segs(Con{s, Con{s2, Nil{}}}) : {Done{N.AmlSegsL{Con{s, Con{s2, Nil{}}}, R}} == N.nm.dpath(B.append(Con{46, _}, R)) : Result<&2, &2, E.AcpiError, N.AmlSegsL>}
2195 segs_rt(Con{s, Con{s2, Nil{}}}, R, oks)
2196 case Con{s3, t3}:
2197 %mask_segs(Con{s, Con{s2, Con{s3, t3}}}) : {Done{N.AmlSegsL{Con{s, Con{s2, Con{s3, t3}}}, R}} == N.nm.dpath(B.append(Con{47, Con{B.byte(U32.from_nat(Nat.add(3n, N.nm.len(t3)))), _}}, R)) : Result<&2, &2, E.AcpiError, N.AmlSegsL>}
2198 %Equal.sym(Nat, U32.to_nat(B.byte(U32.from_nat(Nat.add(3n, N.nm.len(t3))))), Nat.add(3n, N.nm.len(t3)), cnt_rt(Nat.add(3n, N.nm.len(t3)), lt)) : {Done{N.AmlSegsL{Con{s, Con{s2, Con{s3, t3}}}, R}} == N.nm.multi.k(Nat.is_eq(_, 0n), _, B.append(N.nm.segs.list(Con{s, Con{s2, Con{s3, t3}}}), R)) : Result<&2, &2, E.AcpiError, N.AmlSegsL>}
2199 segs_rt(Con{s, Con{s2, Con{s3, t3}}}, R, oks)
2200
2201def pth_dec(+ss: List<&2, B.Octets>, +R: List<&2, U32>, +oks: {N.AmlName.segs_ok(ss) == True{} : Bool}, +lt: {Nat.is_lt(N.nm.len(ss), 256n) == True{} : Bool}) -> {Done{N.AmlNameL{N.AmlName{False{}, 0n, ss}, R}} == N.nm.dec(B.append(B.mask(N.nm.path(ss)), R)) : Result<&2, &2, E.AcpiError, N.AmlNameL>}:
2202 match ss:
2203 case Nil{}:
2204 {==}
2205 case Con{s, t}:
2206 match t:
2207 case Nil{}:
2208 %mask_segs(Con{s, Nil{}}) : {Done{N.AmlNameL{N.AmlName{False{}, 0n, Con{s, Nil{}}}, R}} == N.nm.dec(B.append(_, R)) : Result<&2, &2, E.AcpiError, N.AmlNameL>}
2209 pth1_dec(s, B.Octets.to_list(s), R, {==}, and_l(N.AmlName.seg_ok(s), True{}, oks))
2210 case Con{s2, t2}:
2211 match t2:
2212 case Nil{}:
2213 %mask_segs(Con{s, Con{s2, Nil{}}}) : {Done{N.AmlNameL{N.AmlName{False{}, 0n, Con{s, Con{s2, Nil{}}}}, R}} == N.nm.dec(B.append(Con{46, _}, R)) : Result<&2, &2, E.AcpiError, N.AmlNameL>}
2214 %segs_rt(Con{s, Con{s2, Nil{}}}, R, oks) : {Done{N.AmlNameL{N.AmlName{False{}, 0n, Con{s, Con{s2, Nil{}}}}, R}} == N.nm.named(False{}, 0n, _) : Result<&2, &2, E.AcpiError, N.AmlNameL>}
2215 {==}
2216 case Con{s3, t3}:
2217 %mask_segs(Con{s, Con{s2, Con{s3, t3}}}) : {Done{N.AmlNameL{N.AmlName{False{}, 0n, Con{s, Con{s2, Con{s3, t3}}}}, R}} == N.nm.dec(B.append(Con{47, Con{B.byte(U32.from_nat(Nat.add(3n, N.nm.len(t3)))), _}}, R)) : Result<&2, &2, E.AcpiError, N.AmlNameL>}
2218 %Equal.sym(Nat, U32.to_nat(B.byte(U32.from_nat(Nat.add(3n, N.nm.len(t3))))), Nat.add(3n, N.nm.len(t3)), cnt_rt(Nat.add(3n, N.nm.len(t3)), lt)) : {Done{N.AmlNameL{N.AmlName{False{}, 0n, Con{s, Con{s2, Con{s3, t3}}}}, R}} == N.nm.named(False{}, 0n, N.nm.multi.k(Nat.is_eq(_, 0n), _, B.append(N.nm.segs.list(Con{s, Con{s2, Con{s3, t3}}}), R))) : Result<&2, &2, E.AcpiError, N.AmlNameL>}
2219 %segs_rt(Con{s, Con{s2, Con{s3, t3}}}, R, oks) : {Done{N.AmlNameL{N.AmlName{False{}, 0n, Con{s, Con{s2, Con{s3, t3}}}}, R}} == N.nm.named(False{}, 0n, _) : Result<&2, &2, E.AcpiError, N.AmlNameL>}
2220 {==}
2221
2222def pth_ups(+ss: List<&2, B.Octets>, +R: List<&2, U32>, +oks: {N.AmlName.segs_ok(ss) == True{} : Bool}, +lt: {Nat.is_lt(N.nm.len(ss), 256n) == True{} : Bool}) -> {Done{N.AmlNameL{N.AmlName{False{}, 0n, ss}, R}} == N.nm.ups(B.append(B.mask(N.nm.path(ss)), R), N.nm.head_kind(B.append(B.mask(N.nm.path(ss)), R))) : Result<&2, &2, E.AcpiError, N.AmlNameL>}:
2223 match ss:
2224 case Nil{}:
2225 {==}
2226 case Con{s, t}:
2227 match t:
2228 case Nil{}:
2229 %mask_segs(Con{s, Nil{}}) : {Done{N.AmlNameL{N.AmlName{False{}, 0n, Con{s, Nil{}}}, R}} == N.nm.ups(B.append(_, R), N.nm.head_kind(B.append(_, R))) : Result<&2, &2, E.AcpiError, N.AmlNameL>}
2230 pth1_ups(s, B.Octets.to_list(s), R, {==}, and_l(N.AmlName.seg_ok(s), True{}, oks))
2231 case Con{s2, t2}:
2232 match t2:
2233 case Nil{}:
2234 %mask_segs(Con{s, Con{s2, Nil{}}}) : {Done{N.AmlNameL{N.AmlName{False{}, 0n, Con{s, Con{s2, Nil{}}}}, R}} == N.nm.ups(B.append(Con{46, _}, R), N.nm.head_kind(B.append(Con{46, _}, R))) : Result<&2, &2, E.AcpiError, N.AmlNameL>}
2235 %segs_rt(Con{s, Con{s2, Nil{}}}, R, oks) : {Done{N.AmlNameL{N.AmlName{False{}, 0n, Con{s, Con{s2, Nil{}}}}, R}} == N.nm.named(False{}, 0n, _) : Result<&2, &2, E.AcpiError, N.AmlNameL>}
2236 {==}
2237 case Con{s3, t3}:
2238 %mask_segs(Con{s, Con{s2, Con{s3, t3}}}) : {Done{N.AmlNameL{N.AmlName{False{}, 0n, Con{s, Con{s2, Con{s3, t3}}}}, R}} == N.nm.ups(B.append(Con{47, Con{B.byte(U32.from_nat(Nat.add(3n, N.nm.len(t3)))), _}}, R), N.nm.head_kind(B.append(Con{47, Con{B.byte(U32.from_nat(Nat.add(3n, N.nm.len(t3)))), _}}, R))) : Result<&2, &2, E.AcpiError, N.AmlNameL>}
2239 %Equal.sym(Nat, U32.to_nat(B.byte(U32.from_nat(Nat.add(3n, N.nm.len(t3))))), Nat.add(3n, N.nm.len(t3)), cnt_rt(Nat.add(3n, N.nm.len(t3)), lt)) : {Done{N.AmlNameL{N.AmlName{False{}, 0n, Con{s, Con{s2, Con{s3, t3}}}}, R}} == N.nm.named(False{}, 0n, N.nm.multi.k(Nat.is_eq(_, 0n), _, B.append(N.nm.segs.list(Con{s, Con{s2, Con{s3, t3}}}), R))) : Result<&2, &2, E.AcpiError, N.AmlNameL>}
2240 %segs_rt(Con{s, Con{s2, Con{s3, t3}}}, R, oks) : {Done{N.AmlNameL{N.AmlName{False{}, 0n, Con{s, Con{s2, Con{s3, t3}}}}, R}} == N.nm.named(False{}, 0n, _) : Result<&2, &2, E.AcpiError, N.AmlNameL>}
2241 {==}
2242
2243def ups_rt(+u: Nat, +ss: List<&2, B.Octets>, +R: List<&2, U32>, +oks: {N.AmlName.segs_ok(ss) == True{} : Bool}, +lt: {Nat.is_lt(N.nm.len(ss), 256n) == True{} : Bool}) -> {Done{N.AmlNameL{N.AmlName{False{}, u, ss}, R}} == N.nm.ups(B.append(N.nm.carets(u), B.append(B.mask(N.nm.path(ss)), R)), N.nm.head_kind(B.append(N.nm.carets(u), B.append(B.mask(N.nm.path(ss)), R)))) : Result<&2, &2, E.AcpiError, N.AmlNameL>}:
2244 match u:
2245 case 0n:
2246 pth_ups(ss, R, oks, lt)
2247 case 1n+p:
2248 %ups_rt(p, ss, R, oks, lt) : {Done{N.AmlNameL{N.AmlName{False{}, 1n+p, ss}, R}} == N.nm.up1(_) : Result<&2, &2, E.AcpiError, N.AmlNameL>}
2249 {==}
2250
2251def dec_rt(+n: N.AmlName, +R: List<&2, U32>, +ok: {N.AmlName.valid(n) == True{} : Bool}) -> {Done{N.AmlNameL{n, R}} == N.nm.dec(B.append(B.mask(N.nm.enc(n)), R)) : Result<&2, &2, E.AcpiError, N.AmlNameL>}:
2252 match n:
2253 case N.AmlName{r, u, ss}:
2254 match r:
2255 case True{}:
2256 match u:
2257 case 0n:
2258 %mask_app([92], N.nm.path(ss)) : {Done{N.AmlNameL{N.AmlName{True{}, 0n, ss}, R}} == N.nm.dec(B.append(_, R)) : Result<&2, &2, E.AcpiError, N.AmlNameL>}
2259 %pth_dpath(ss, R, and_l(N.AmlName.segs_ok(ss), Nat.is_lt(N.nm.len(ss), 256n), ok), and_r(N.AmlName.segs_ok(ss), Nat.is_lt(N.nm.len(ss), 256n), ok)) : {Done{N.AmlNameL{N.AmlName{True{}, 0n, ss}, R}} == N.nm.named(True{}, 0n, _) : Result<&2, &2, E.AcpiError, N.AmlNameL>}
2260 {==}
2261 case 1n+p:
2262 Empty.absurd({Done{N.AmlNameL{N.AmlName{True{}, 1n+p, ss}, R}} == N.nm.dec(B.append(B.mask(N.nm.enc(N.AmlName{True{}, 1n+p, ss})), R)) : Result<&2, &2, E.AcpiError, N.AmlNameL>}, ft_absurd(ok))
2263 case False{}:
2264 match u:
2265 case 0n:
2266 %mask_app(N.nm.carets(0n), N.nm.path(ss)) : {Done{N.AmlNameL{N.AmlName{False{}, 0n, ss}, R}} == N.nm.dec(B.append(_, R)) : Result<&2, &2, E.AcpiError, N.AmlNameL>}
2267 %mask_carets(0n) : {Done{N.AmlNameL{N.AmlName{False{}, 0n, ss}, R}} == N.nm.dec(B.append(B.append(_, B.mask(N.nm.path(ss))), R)) : Result<&2, &2, E.AcpiError, N.AmlNameL>}
2268 %app_assoc(N.nm.carets(0n), B.mask(N.nm.path(ss)), R) : {Done{N.AmlNameL{N.AmlName{False{}, 0n, ss}, R}} == N.nm.dec(_) : Result<&2, &2, E.AcpiError, N.AmlNameL>}
2269 pth_dec(ss, R, and_l(N.AmlName.segs_ok(ss), Nat.is_lt(N.nm.len(ss), 256n), ok), and_r(N.AmlName.segs_ok(ss), Nat.is_lt(N.nm.len(ss), 256n), ok))
2270 case 1n+p:
2271 %mask_app(N.nm.carets(1n+p), N.nm.path(ss)) : {Done{N.AmlNameL{N.AmlName{False{}, 1n+p, ss}, R}} == N.nm.dec(B.append(_, R)) : Result<&2, &2, E.AcpiError, N.AmlNameL>}
2272 %mask_carets(1n+p) : {Done{N.AmlNameL{N.AmlName{False{}, 1n+p, ss}, R}} == N.nm.dec(B.append(B.append(_, B.mask(N.nm.path(ss))), R)) : Result<&2, &2, E.AcpiError, N.AmlNameL>}
2273 %app_assoc(N.nm.carets(1n+p), B.mask(N.nm.path(ss)), R) : {Done{N.AmlNameL{N.AmlName{False{}, 1n+p, ss}, R}} == N.nm.dec(_) : Result<&2, &2, E.AcpiError, N.AmlNameL>}
2274 ups_rt(1n+p, ss, R, and_l(N.AmlName.segs_ok(ss), Nat.is_lt(N.nm.len(ss), 256n), ok), and_r(N.AmlName.segs_ok(ss), Nat.is_lt(N.nm.len(ss), 256n), ok))
2275
2276def Laws.namestring_round_trip(n, rest, ok):
2277 %Equal.sym(List<&2, U32>, B.Octets.to_list(B.Octets.append(N.AmlName.encode(n), rest)), B.append(B.Octets.to_list(N.AmlName.encode(n)), B.Octets.to_list(rest)), BL.octets_append_list(N.AmlName.encode(n), rest)) : {N.nm.pub(N.nm.dec(_)) == Done{N.AmlNameParsed{n, rest}} : Result<&2, &2, E.AcpiError, N.AmlNameParsed>}
2278 %Equal.sym(List<&2, U32>, B.Octets.to_list(B.Octets.of_list(N.nm.enc(n))), B.mask(N.nm.enc(n)), BL.octets_to_of(N.nm.enc(n))) : {N.nm.pub(N.nm.dec(B.append(_, B.Octets.to_list(rest)))) == Done{N.AmlNameParsed{n, rest}} : Result<&2, &2, E.AcpiError, N.AmlNameParsed>}
2279 %BL.octets_of_to(rest) : {N.nm.pub(N.nm.dec(B.append(B.mask(N.nm.enc(n)), B.Octets.to_list(rest)))) == Done{N.AmlNameParsed{n, _}} : Result<&2, &2, E.AcpiError, N.AmlNameParsed>}
2280 %dec_rt(n, B.Octets.to_list(rest), ok) : {N.nm.pub(_) == Done{N.AmlNameParsed{n, B.Octets.of_list(B.Octets.to_list(rest))}} : Result<&2, &2, E.AcpiError, N.AmlNameParsed>}
2281 {==}
2282# Octets lengths of the fields
2283
2284def le32_len(+v: U32) -> {B.Octets.len(B.Octets.le32(v)) == 4n : Nat}:
2285 match v:
2286 case U32{w}:
2287 %Equal.sym(Nat, B.Octets.len(B.Octets.le32(U32{w})), B.len(B.Octets.to_list(B.Octets.le32(U32{w}))), BL.octets_len_list(B.Octets.le32(U32{w}))) : {_ == 4n : Nat}
2288 %Equal.sym(List<&2, U32>, B.Octets.to_list(B.Octets.of_list(B.le32(U32{w}))), B.mask(B.le32(U32{w})), BL.octets_to_of(B.le32(U32{w}))) : {B.len(_) == 4n : Nat}
2289 {==}
2290
2291def byte_len(+v: U32) -> {B.Octets.len(B.Octets.of_list([v])) == 1n : Nat}:
2292 %Equal.sym(Nat, B.Octets.len(B.Octets.of_list([v])), B.len(B.Octets.to_list(B.Octets.of_list([v]))), BL.octets_len_list(B.Octets.of_list([v]))) : {_ == 1n : Nat}
2293 %Equal.sym(List<&2, U32>, B.Octets.to_list(B.Octets.of_list([v])), B.mask([v]), BL.octets_to_of([v])) : {B.len(_) == 1n : Nat}
2294 {==}
2295
2296def hdr_rt(+s: B.Octets, +l: U32, +r: U32, +c: U32, +o: B.Octets, +t: B.Octets, +orv: U32, +ci: B.Octets, +cr: U32, +sig4: {B.Octets.len(s) == 4n : Nat}, +oem6: {B.Octets.len(o) == 6n : Nat}, +tid8: {B.Octets.len(t) == 8n : Nat}, +cid4: {B.Octets.len(ci) == 4n : Nat}, +rev8: {B.byte(r) == r : U32}, +ck8: {B.byte(c) == c : U32}) -> {H.AcpiHeader.decode(H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr})) == Done{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}:
2297 %sig4 : {H.hd.d1(B.Octets.split_at(_, B.Octets.append(s, B.Octets.append(B.Octets.le32(l), B.Octets.append(H.hd.byte(r), B.Octets.append(H.hd.byte(c), B.Octets.append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr)))))))))), H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr})) == Done{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
2298 %Equal.sym(Maybe<&2, B.OctetsSplit>, B.Octets.split_at(B.Octets.len(s), B.Octets.append(s, B.Octets.append(B.Octets.le32(l), B.Octets.append(H.hd.byte(r), B.Octets.append(H.hd.byte(c), B.Octets.append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr)))))))))), Some{B.OctetsSplit{s, B.Octets.append(B.Octets.le32(l), B.Octets.append(H.hd.byte(r), B.Octets.append(H.hd.byte(c), B.Octets.append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr))))))))}}, BL.octets_split_at_append(s, B.Octets.append(B.Octets.le32(l), B.Octets.append(H.hd.byte(r), B.Octets.append(H.hd.byte(c), B.Octets.append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr)))))))))) : {H.hd.d1(_, H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr})) == Done{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
2299 %le32_len(l) : {H.hd.d2(B.Octets.split_at(_, B.Octets.append(B.Octets.le32(l), B.Octets.append(H.hd.byte(r), B.Octets.append(H.hd.byte(c), B.Octets.append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr))))))))), H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), s) == Done{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
2300 %Equal.sym(Maybe<&2, B.OctetsSplit>, B.Octets.split_at(B.Octets.len(B.Octets.le32(l)), B.Octets.append(B.Octets.le32(l), B.Octets.append(H.hd.byte(r), B.Octets.append(H.hd.byte(c), B.Octets.append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr))))))))), Some{B.OctetsSplit{B.Octets.le32(l), B.Octets.append(H.hd.byte(r), B.Octets.append(H.hd.byte(c), B.Octets.append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr)))))))}}, BL.octets_split_at_append(B.Octets.le32(l), B.Octets.append(H.hd.byte(r), B.Octets.append(H.hd.byte(c), B.Octets.append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr))))))))) : {H.hd.d2(_, H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), s) == Done{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
2301 %byte_len(r) : {H.hd.d3(B.Octets.split_at(_, B.Octets.append(H.hd.byte(r), B.Octets.append(H.hd.byte(c), B.Octets.append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr)))))))), H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), s, H.hd.u32(B.Octets.le32(l))) == Done{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
2302 %Equal.sym(Maybe<&2, B.OctetsSplit>, B.Octets.split_at(B.Octets.len(H.hd.byte(r)), B.Octets.append(H.hd.byte(r), B.Octets.append(H.hd.byte(c), B.Octets.append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr)))))))), Some{B.OctetsSplit{H.hd.byte(r), B.Octets.append(H.hd.byte(c), B.Octets.append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr))))))}}, BL.octets_split_at_append(H.hd.byte(r), B.Octets.append(H.hd.byte(c), B.Octets.append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr)))))))) : {H.hd.d3(_, H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), s, H.hd.u32(B.Octets.le32(l))) == Done{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
2303 %byte_len(c) : {H.hd.d4(B.Octets.split_at(_, B.Octets.append(H.hd.byte(c), B.Octets.append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr))))))), H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), s, H.hd.u32(B.Octets.le32(l)), H.hd.u8(H.hd.byte(r))) == Done{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
2304 %Equal.sym(Maybe<&2, B.OctetsSplit>, B.Octets.split_at(B.Octets.len(H.hd.byte(c)), B.Octets.append(H.hd.byte(c), B.Octets.append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr))))))), Some{B.OctetsSplit{H.hd.byte(c), B.Octets.append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr)))))}}, BL.octets_split_at_append(H.hd.byte(c), B.Octets.append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr))))))) : {H.hd.d4(_, H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), s, H.hd.u32(B.Octets.le32(l)), H.hd.u8(H.hd.byte(r))) == Done{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
2305 %oem6 : {H.hd.d5(B.Octets.split_at(_, B.Octets.append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr)))))), H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), s, H.hd.u32(B.Octets.le32(l)), H.hd.u8(H.hd.byte(r)), H.hd.u8(H.hd.byte(c))) == Done{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
2306 %Equal.sym(Maybe<&2, B.OctetsSplit>, B.Octets.split_at(B.Octets.len(o), B.Octets.append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr)))))), Some{B.OctetsSplit{o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr))))}}, BL.octets_split_at_append(o, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr)))))) : {H.hd.d5(_, H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), s, H.hd.u32(B.Octets.le32(l)), H.hd.u8(H.hd.byte(r)), H.hd.u8(H.hd.byte(c))) == Done{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
2307 %tid8 : {H.hd.d6(B.Octets.split_at(_, B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr))))), H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), s, H.hd.u32(B.Octets.le32(l)), H.hd.u8(H.hd.byte(r)), H.hd.u8(H.hd.byte(c)), o) == Done{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
2308 %Equal.sym(Maybe<&2, B.OctetsSplit>, B.Octets.split_at(B.Octets.len(t), B.Octets.append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr))))), Some{B.OctetsSplit{t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr)))}}, BL.octets_split_at_append(t, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr))))) : {H.hd.d6(_, H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), s, H.hd.u32(B.Octets.le32(l)), H.hd.u8(H.hd.byte(r)), H.hd.u8(H.hd.byte(c)), o) == Done{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
2309 %le32_len(orv) : {H.hd.d7(B.Octets.split_at(_, B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr)))), H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), s, H.hd.u32(B.Octets.le32(l)), H.hd.u8(H.hd.byte(r)), H.hd.u8(H.hd.byte(c)), o, t) == Done{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
2310 %Equal.sym(Maybe<&2, B.OctetsSplit>, B.Octets.split_at(B.Octets.len(B.Octets.le32(orv)), B.Octets.append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr)))), Some{B.OctetsSplit{B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr))}}, BL.octets_split_at_append(B.Octets.le32(orv), B.Octets.append(ci, B.Octets.le32(cr)))) : {H.hd.d7(_, H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), s, H.hd.u32(B.Octets.le32(l)), H.hd.u8(H.hd.byte(r)), H.hd.u8(H.hd.byte(c)), o, t) == Done{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
2311 %cid4 : {H.hd.d8(B.Octets.split_at(_, B.Octets.append(ci, B.Octets.le32(cr))), H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), s, H.hd.u32(B.Octets.le32(l)), H.hd.u8(H.hd.byte(r)), H.hd.u8(H.hd.byte(c)), o, t, H.hd.u32(B.Octets.le32(orv))) == Done{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
2312 %Equal.sym(Maybe<&2, B.OctetsSplit>, B.Octets.split_at(B.Octets.len(ci), B.Octets.append(ci, B.Octets.le32(cr))), Some{B.OctetsSplit{ci, B.Octets.le32(cr)}}, BL.octets_split_at_append(ci, B.Octets.le32(cr))) : {H.hd.d8(_, H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), s, H.hd.u32(B.Octets.le32(l)), H.hd.u8(H.hd.byte(r)), H.hd.u8(H.hd.byte(c)), o, t, H.hd.u32(B.Octets.le32(orv))) == Done{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
2313 %Equal.sym(Nat, B.Octets.len(B.Octets.le32(cr)), 4n, le32_len(cr)) : {H.hd.d9(Nat.is_le(4n, _), H.AcpiHeader.encode(H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}), s, H.hd.u32(B.Octets.le32(l)), H.hd.u8(H.hd.byte(r)), H.hd.u8(H.hd.byte(c)), o, t, H.hd.u32(B.Octets.le32(orv)), ci, B.Octets.le32(cr)) == Done{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
2314 %Equal.sym(Maybe<&2, U32>, B.Octets.le32_at(B.Octets.le32(l), 0n), Some{l}, BL.octets_le32_round_trip(l)) : {Done{H.AcpiHeader{s, Maybe.default(&2, U32, _, 0), H.hd.u8(H.hd.byte(r)), H.hd.u8(H.hd.byte(c)), o, t, H.hd.u32(B.Octets.le32(orv)), ci, H.hd.u32(B.Octets.le32(cr))}} == Done{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
2315 %Equal.sym(Maybe<&2, U32>, B.Octets.le32_at(B.Octets.le32(orv), 0n), Some{orv}, BL.octets_le32_round_trip(orv)) : {Done{H.AcpiHeader{s, l, H.hd.u8(H.hd.byte(r)), H.hd.u8(H.hd.byte(c)), o, t, Maybe.default(&2, U32, _, 0), ci, H.hd.u32(B.Octets.le32(cr))}} == Done{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
2316 %Equal.sym(Maybe<&2, U32>, B.Octets.le32_at(B.Octets.le32(cr), 0n), Some{cr}, BL.octets_le32_round_trip(cr)) : {Done{H.AcpiHeader{s, l, H.hd.u8(H.hd.byte(r)), H.hd.u8(H.hd.byte(c)), o, t, orv, ci, Maybe.default(&2, U32, _, 0)}} == Done{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
2317 %Equal.sym(List<&2, U32>, B.Octets.to_list(B.Octets.of_list([r])), B.mask([r]), BL.octets_to_of([r])) : {Done{H.AcpiHeader{s, l, H.hd.u8.list(_), H.hd.u8(H.hd.byte(c)), o, t, orv, ci, cr}} == Done{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
2318 %Equal.sym(List<&2, U32>, B.Octets.to_list(B.Octets.of_list([c])), B.mask([c]), BL.octets_to_of([c])) : {Done{H.AcpiHeader{s, l, B.byte(r), H.hd.u8.list(_), o, t, orv, ci, cr}} == Done{H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
2319 %rev8 : {Done{H.AcpiHeader{s, l, B.byte(r), B.byte(c), o, t, orv, ci, cr}} == Done{H.AcpiHeader{s, l, _, c, o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
2320 %ck8 : {Done{H.AcpiHeader{s, l, B.byte(r), B.byte(c), o, t, orv, ci, cr}} == Done{H.AcpiHeader{s, l, B.byte(r), _, o, t, orv, ci, cr}} : Result<&2, &2, E.AcpiError, H.AcpiHeader>}
2321 {==}
2322
2323def Laws.header_round_trip(h, sig4, oem6, tid8, cid4, rev8, ck8):
2324 match h:
2325 case H.AcpiHeader{s, l, r, c, o, t, orv, ci, cr}:
2326 hdr_rt(s, l, r, c, o, t, orv, ci, cr, sig4, oem6, tid8, cid4, rev8, ck8)
2327
2328# Checksums: a table is accepted only on the branch where its checksum was
2329# found to be zero. Each lemma follows one decision of the parser.
2330
2331def rdisc(-A: Data, +r: Result<&2, &2, E.AcpiError, A>) -> Type:
2332 match r:
2333 case Fail{x}:
2334 Unit
2335 case Done{x}:
2336 Empty
2337
2338def fd_absurd(-A: Data, -x: E.AcpiError, -y: A, +e: {Fail{x} == Done{y} : Result<&2, &2, E.AcpiError, A>}) -> Empty:
2339 %e : rdisc(A, _)
2340 Unit{}
2341
2342def done_inj(-A: Data, +a: A, +b: A, +e: {Done{a} == Done{b} : Result<&2, &2, E.AcpiError, A>}) -> {a == b : A}:
2343 Equal.cong(Result<&2, &2, E.AcpiError, A>, A, x => Result.default(&2, &2, E.AcpiError, A, x, a), Done{a}, Done{b}, e)
2344
2345def done_t(-A: Data, +r: Result<&2, &2, E.AcpiError, A>, +x: A, +e: {r == Done{x} : Result<&2, &2, E.AcpiError, A>}) -> {Result.is_done(&2, &2, E.AcpiError, A, r) == True{} : Bool}:
2346 %Equal.sym(Result<&2, &2, E.AcpiError, A>, r, Done{x}, e) : {Result.is_done(&2, &2, E.AcpiError, A, _) == True{} : Bool}
2347 {==}
2348
2349def c3_ok(+b: Bool, +r: B.Octets, +raw: B.Octets, +eb: {C.AcpiChecksum.ok(r) == b : Bool}, +e: {H.sdt.c3(b, r) == Done{raw} : Result<&2, &2, E.AcpiError, B.Octets>}) -> {C.AcpiChecksum.ok(raw) == True{} : Bool}:
2350 match b:
2351 case True{}:
2352 %done_inj(B.Octets, r, raw, e) : {C.AcpiChecksum.ok(_) == True{} : Bool}
2353 eb
2354 case False{}:
2355 Empty.absurd({C.AcpiChecksum.ok(raw) == True{} : Bool}, fd_absurd(B.Octets, E.AcpiBadChecksum{C.AcpiChecksum.sum(r)}, raw, e))
2356
2357def c2_ok(+b: Bool, +l: U32, +o: B.Octets, +raw: B.Octets, +e: {H.sdt.c2(b, l, o) == Done{raw} : Result<&2, &2, E.AcpiError, B.Octets>}) -> {C.AcpiChecksum.ok(raw) == True{} : Bool}:
2358 match b:
2359 case True{}:
2360 c3_ok(C.AcpiChecksum.ok(B.Octets.take(U32.to_nat(l), o)), B.Octets.take(U32.to_nat(l), o), raw, {==}, e)
2361 case False{}:
2362 Empty.absurd({C.AcpiChecksum.ok(raw) == True{} : Bool}, fd_absurd(B.Octets, E.AcpiBadLength{l}, raw, e))
2363
2364def c1_ok(+m: Maybe<&2, U32>, +o: B.Octets, +raw: B.Octets, +e: {H.sdt.c1(m, o) == Done{raw} : Result<&2, &2, E.AcpiError, B.Octets>}) -> {C.AcpiChecksum.ok(raw) == True{} : Bool}:
2365 match m:
2366 case None{}:
2367 Empty.absurd({C.AcpiChecksum.ok(raw) == True{} : Bool}, fd_absurd(B.Octets, E.AcpiTooShort{36n, B.Octets.len(o)}, raw, e))
2368 case Some{l}:
2369 c2_ok(Bool.and(Nat.is_le(36n, U32.to_nat(l)), Nat.is_le(U32.to_nat(l), B.Octets.len(o))), l, o, raw, e)
2370
2371def Laws.sdt_check_sums(o, raw, e):
2372 c1_ok(B.Octets.le32_at(o, 4n), o, raw, e)
2373
2374# the same decisions, from "the check succeeded", to the table's bytes
2375
2376def c3_d(+b: Bool, +r: B.Octets, +eb: {C.AcpiChecksum.ok(r) == b : Bool}, +e: {Result.is_done(&2, &2, E.AcpiError, B.Octets, H.sdt.c3(b, r)) == True{} : Bool}) -> {C.AcpiChecksum.ok(r) == True{} : Bool}:
2377 match b:
2378 case True{}:
2379 eb
2380 case False{}:
2381 Empty.absurd({C.AcpiChecksum.ok(r) == True{} : Bool}, ft_absurd(e))
2382
2383def c2_d(+b: Bool, +l: U32, +o: B.Octets, +e: {Result.is_done(&2, &2, E.AcpiError, B.Octets, H.sdt.c2(b, l, o)) == True{} : Bool}) -> {C.AcpiChecksum.ok(B.Octets.take(U32.to_nat(l), o)) == True{} : Bool}:
2384 match b:
2385 case True{}:
2386 c3_d(C.AcpiChecksum.ok(B.Octets.take(U32.to_nat(l), o)), B.Octets.take(U32.to_nat(l), o), {==}, e)
2387 case False{}:
2388 Empty.absurd({C.AcpiChecksum.ok(B.Octets.take(U32.to_nat(l), o)) == True{} : Bool}, ft_absurd(e))
2389
2390def c1_d(+m: Maybe<&2, U32>, +o: B.Octets, +e: {Result.is_done(&2, &2, E.AcpiError, B.Octets, H.sdt.c1(m, o)) == True{} : Bool}) -> {C.AcpiChecksum.ok(B.Octets.take(U32.to_nat(Maybe.default(&2, U32, m, 4294967295)), o)) == True{} : Bool}:
2391 match m:
2392 case None{}:
2393 Empty.absurd({C.AcpiChecksum.ok(B.Octets.take(U32.to_nat(Maybe.default(&2, U32, None{}, 4294967295)), o)) == True{} : Bool}, ft_absurd(e))
2394 case Some{l}:
2395 c2_d(Bool.and(Nat.is_le(36n, U32.to_nat(l)), Nat.is_le(U32.to_nat(l), B.Octets.len(o))), l, o, e)
2396
2397def check_d(+o: B.Octets, +e: {Result.is_done(&2, &2, E.AcpiError, B.Octets, H.AcpiSdt.check(o)) == True{} : Bool}) -> {C.AcpiChecksum.ok(H.AcpiSdt.bytes(o)) == True{} : Bool}:
2398 c1_d(B.Octets.le32_at(o, 4n), o, e)
2399
2400def sdt_go_d(+c: Result<&2, &2, E.AcpiError, B.Octets>, +e: {Result.is_done(&2, &2, E.AcpiError, H.AcpiSdt, H.sdt.parse.go(c)) == True{} : Bool}) -> {Result.is_done(&2, &2, E.AcpiError, B.Octets, c) == True{} : Bool}:
2401 match c:
2402 case Fail{x}:
2403 Empty.absurd({Result.is_done(&2, &2, E.AcpiError, B.Octets, Fail{x}) == True{} : Bool}, ft_absurd(e))
2404 case Done{raw}:
2405 {==}
2406
2407def reg_go_d(+reg: R.AcpiRegistry, +r: Result<&2, &2, E.AcpiError, H.AcpiSdt>, +t: R.AcpiTable<R.AcpiNoExt>, +e: {R.reg.go(~R.AcpiNoExt, ~R.AcpiNoExt.parse, reg, r) == Done{t} : Result<&2, &2, E.AcpiError, R.AcpiTable<R.AcpiNoExt>>}) -> {Result.is_done(&2, &2, E.AcpiError, H.AcpiSdt, r) == True{} : Bool}:
2408 match r:
2409 case Fail{x}:
2410 Empty.absurd({Result.is_done(&2, &2, E.AcpiError, H.AcpiSdt, Fail{x}) == True{} : Bool}, fd_absurd(R.AcpiTable<R.AcpiNoExt>, x, t, e))
2411 case Done{x}:
2412 {==}
2413
2414def Laws.table_checksums(reg, o, t, e):
2415 check_d(o, sdt_go_d(H.AcpiSdt.check(o), reg_go_d(reg, H.AcpiSdt.parse(o), t, e)))
2416
2417# The RSDP
2418
2419def rp3_d(+b: Bool, +o: B.Octets, +e: {Result.is_done(&2, &2, E.AcpiError, P.AcpiRsdp, P.rs.p3(b, o)) == True{} : Bool}) -> {b == True{} : Bool}:
2420 match b:
2421 case True{}:
2422 {==}
2423 case False{}:
2424 Empty.absurd({False{} == True{} : Bool}, ft_absurd(e))
2425
2426def rp2_d(+b: Bool, +o: B.Octets, +e: {Result.is_done(&2, &2, E.AcpiError, P.AcpiRsdp, P.rs.p2(b, o)) == True{} : Bool}) -> {C.AcpiChecksum.ok(B.Octets.take(20n, o)) == True{} : Bool}:
2427 match b:
2428 case True{}:
2429 rp3_d(C.AcpiChecksum.ok(B.Octets.take(20n, o)), o, e)
2430 case False{}:
2431 Empty.absurd({C.AcpiChecksum.ok(B.Octets.take(20n, o)) == True{} : Bool}, ft_absurd(e))
2432
2433def rp1_d(+b: Bool, +o: B.Octets, +e: {Result.is_done(&2, &2, E.AcpiError, P.AcpiRsdp, P.rs.p1(b, o)) == True{} : Bool}) -> {C.AcpiChecksum.ok(B.Octets.take(20n, o)) == True{} : Bool}:
2434 match b:
2435 case True{}:
2436 rp2_d(B.Octets.is_eq(B.Octets.take(8n, o), P.AcpiRsdp.signature()), o, e)
2437 case False{}:
2438 Empty.absurd({C.AcpiChecksum.ok(B.Octets.take(20n, o)) == True{} : Bool}, ft_absurd(e))
2439
2440def Laws.rsdp_checksum(o, r, e):
2441 rp1_d(Nat.is_le(20n, B.Octets.len(o)), o, done_t(P.AcpiRsdp, P.AcpiRsdp.parse(o), r, e))
2442
2443# the extended checksum: followed to the structure answered, whose checked
2444# length is the one summed
2445
2446def rx7(+b: Bool, +l: U32, +o: B.Octets, +r: P.AcpiRsdp, +eb: {C.AcpiChecksum.ok(B.Octets.take(U32.to_nat(l), o)) == b : Bool}, +e: {P.rs.p7(b, l, o) == Done{r} : Result<&2, &2, E.AcpiError, P.AcpiRsdp>}) -> {C.AcpiChecksum.ok(B.Octets.take(P.AcpiRsdp.checked(r), o)) == True{} : Bool}:
2447 match b:
2448 case True{}:
2449 %done_inj(P.AcpiRsdp, P.AcpiRsdp{F.AcpiF.bytes(o, 9n, 6n), F.AcpiF.u8(o, 15n), F.AcpiF.u32(o, 16n), Some{P.AcpiRsdpExt{l, F.AcpiF.u64(o, 24n)}}}, r, e) : {C.AcpiChecksum.ok(B.Octets.take(P.AcpiRsdp.checked(_), o)) == True{} : Bool}
2450 eb
2451 case False{}:
2452 Empty.absurd({C.AcpiChecksum.ok(B.Octets.take(P.AcpiRsdp.checked(r), o)) == True{} : Bool}, fd_absurd(P.AcpiRsdp, E.AcpiRsdpBadExtChecksum{C.AcpiChecksum.sum(B.Octets.take(U32.to_nat(l), o))}, r, e))
2453
2454def rx6(+b: Bool, +l: U32, +o: B.Octets, +r: P.AcpiRsdp, +e: {P.rs.p6(b, l, o) == Done{r} : Result<&2, &2, E.AcpiError, P.AcpiRsdp>}) -> {C.AcpiChecksum.ok(B.Octets.take(P.AcpiRsdp.checked(r), o)) == True{} : Bool}:
2455 match b:
2456 case True{}:
2457 rx7(C.AcpiChecksum.ok(B.Octets.take(U32.to_nat(l), o)), l, o, r, {==}, e)
2458 case False{}:
2459 Empty.absurd({C.AcpiChecksum.ok(B.Octets.take(P.AcpiRsdp.checked(r), o)) == True{} : Bool}, fd_absurd(P.AcpiRsdp, E.AcpiBadLength{l}, r, e))
2460
2461def rx5(+b: Bool, +o: B.Octets, +r: P.AcpiRsdp, +e: {P.rs.p5(b, o) == Done{r} : Result<&2, &2, E.AcpiError, P.AcpiRsdp>}) -> {C.AcpiChecksum.ok(B.Octets.take(P.AcpiRsdp.checked(r), o)) == True{} : Bool}:
2462 match b:
2463 case True{}:
2464 rx6(Bool.and(Nat.is_le(36n, U32.to_nat(F.AcpiF.u32(o, 20n))), Nat.is_le(U32.to_nat(F.AcpiF.u32(o, 20n)), B.Octets.len(o))), F.AcpiF.u32(o, 20n), o, r, e)
2465 case False{}:
2466 Empty.absurd({C.AcpiChecksum.ok(B.Octets.take(P.AcpiRsdp.checked(r), o)) == True{} : Bool}, fd_absurd(P.AcpiRsdp, E.AcpiTooShort{36n, B.Octets.len(o)}, r, e))
2467
2468def rx4(+b: Bool, +o: B.Octets, +r: P.AcpiRsdp, +ok20: {C.AcpiChecksum.ok(B.Octets.take(20n, o)) == True{} : Bool}, +e: {P.rs.p4(b, o) == Done{r} : Result<&2, &2, E.AcpiError, P.AcpiRsdp>}) -> {C.AcpiChecksum.ok(B.Octets.take(P.AcpiRsdp.checked(r), o)) == True{} : Bool}:
2469 match b:
2470 case True{}:
2471 %done_inj(P.AcpiRsdp, P.AcpiRsdp{F.AcpiF.bytes(o, 9n, 6n), F.AcpiF.u8(o, 15n), F.AcpiF.u32(o, 16n), None{}}, r, e) : {C.AcpiChecksum.ok(B.Octets.take(P.AcpiRsdp.checked(_), o)) == True{} : Bool}
2472 ok20
2473 case False{}:
2474 rx5(Nat.is_le(36n, B.Octets.len(o)), o, r, e)
2475
2476def rx3(+b: Bool, +o: B.Octets, +r: P.AcpiRsdp, +eb: {C.AcpiChecksum.ok(B.Octets.take(20n, o)) == b : Bool}, +e: {P.rs.p3(b, o) == Done{r} : Result<&2, &2, E.AcpiError, P.AcpiRsdp>}) -> {C.AcpiChecksum.ok(B.Octets.take(P.AcpiRsdp.checked(r), o)) == True{} : Bool}:
2477 match b:
2478 case True{}:
2479 rx4(U32.is_lt(F.AcpiF.u8(o, 15n), 2), o, r, eb, e)
2480 case False{}:
2481 Empty.absurd({C.AcpiChecksum.ok(B.Octets.take(P.AcpiRsdp.checked(r), o)) == True{} : Bool}, fd_absurd(P.AcpiRsdp, E.AcpiRsdpBadChecksum{C.AcpiChecksum.sum(B.Octets.take(20n, o))}, r, e))
2482
2483def rx2(+b: Bool, +o: B.Octets, +r: P.AcpiRsdp, +e: {P.rs.p2(b, o) == Done{r} : Result<&2, &2, E.AcpiError, P.AcpiRsdp>}) -> {C.AcpiChecksum.ok(B.Octets.take(P.AcpiRsdp.checked(r), o)) == True{} : Bool}:
2484 match b:
2485 case True{}:
2486 rx3(C.AcpiChecksum.ok(B.Octets.take(20n, o)), o, r, {==}, e)
2487 case False{}:
2488 Empty.absurd({C.AcpiChecksum.ok(B.Octets.take(P.AcpiRsdp.checked(r), o)) == True{} : Bool}, fd_absurd(P.AcpiRsdp, E.AcpiBadSignature{B.Octets.take(8n, o)}, r, e))
2489
2490def rx1(+b: Bool, +o: B.Octets, +r: P.AcpiRsdp, +e: {P.rs.p1(b, o) == Done{r} : Result<&2, &2, E.AcpiError, P.AcpiRsdp>}) -> {C.AcpiChecksum.ok(B.Octets.take(P.AcpiRsdp.checked(r), o)) == True{} : Bool}:
2491 match b:
2492 case True{}:
2493 rx2(B.Octets.is_eq(B.Octets.take(8n, o), P.AcpiRsdp.signature()), o, r, e)
2494 case False{}:
2495 Empty.absurd({C.AcpiChecksum.ok(B.Octets.take(P.AcpiRsdp.checked(r), o)) == True{} : Bool}, fd_absurd(P.AcpiRsdp, E.AcpiTooShort{20n, B.Octets.len(o)}, r, e))
2496
2497def Laws.rsdp_ext_checksum(o, r, e):
2498 rx1(Nat.is_le(20n, B.Octets.len(o)), o, r, e)
2499
2500# The step bound: AmlM.run.go counts each step it takes, and stops when its
2501# fuel runs out
2502
2503def le_refl(+u: Nat) -> {Nat.is_le(u, u) == True{} : Bool}:
2504 match u:
2505 case 0n:
2506 {==}
2507 case 1n+p:
2508 le_refl(p)
2509
2510def le_step(+a: Nat, +b: Nat, +e: {Nat.is_le(a, b) == True{} : Bool}) -> {Nat.is_le(a, 1n+b) == True{} : Bool}:
2511 match a b:
2512 case 0n _:
2513 {==}
2514 case 1n+ap 0n:
2515 Empty.absurd({Nat.is_le(1n+ap, 1n+0n) == True{} : Bool}, ft_absurd(e))
2516 case 1n+ap 1n+bp:
2517 le_step(ap, bp, e)
2518
2519def le_add(+p: Nat, +u: Nat) -> {Nat.is_le(u, Nat.add(p, u)) == True{} : Bool}:
2520 match p:
2521 case 0n:
2522 le_refl(u)
2523 case 1n+q:
2524 le_step(u, Nat.add(q, u), le_add(q, u))
2525
2526def add_succ(+a: Nat, +b: Nat) -> {1n+Nat.add(a, b) == Nat.add(a, 1n+b) : Nat}:
2527 match a:
2528 case 0n:
2529 {==}
2530 case 1n+p:
2531 %add_succ(p, b) : {1n+1n+Nat.add(p, b) == 1n+_ : Nat}
2532 {==}
2533
2534def add_zero(+a: Nat) -> {Nat.add(a, 0n) == a : Nat}:
2535 match a:
2536 case 0n:
2537 {==}
2538 case 1n+p:
2539 %add_zero(p) : {1n+Nat.add(p, 0n) == 1n+_ : Nat}
2540 {==}
2541
2542def run_go_le(+n: Nat, +h: Bool, +m: I.AmlMachine<Hs.AmlMemHost>, +u: Nat) -> {Nat.is_le(I.AmlRun.steps(Hs.AmlMemHost, I.AmlM.run.go(~Hs.AmlMemHost, ~Hs.AmlMemHost.io, n, h, m, u)), Nat.add(n, u)) == True{} : Bool}:
2543 match n:
2544 case 0n:
2545 le_refl(u)
2546 case 1n+p:
2547 match h:
2548 case True{}:
2549 le_step(u, Nat.add(p, u), le_add(p, u))
2550 case False{}:
2551 %Equal.sym(Nat, 1n+Nat.add(p, u), Nat.add(p, 1n+u), add_succ(p, u)) : {Nat.is_le(I.AmlRun.steps(Hs.AmlMemHost, I.AmlM.run.go(~Hs.AmlMemHost, ~Hs.AmlMemHost.io, p, I.AmlMachine.halted(Hs.AmlMemHost, I.AmlM.step(~Hs.AmlMemHost, ~Hs.AmlMemHost.io, m)), I.AmlM.step(~Hs.AmlMemHost, ~Hs.AmlMemHost.io, m), 1n+u)), _) == True{} : Bool}
2552 run_go_le(p, I.AmlMachine.halted(Hs.AmlMemHost, I.AmlM.step(~Hs.AmlMemHost, ~Hs.AmlMemHost.io, m)), I.AmlM.step(~Hs.AmlMemHost, ~Hs.AmlMemHost.io, m), 1n+u)
2553
2554def Laws.run_steps_bound(n, m):
2555 %add_zero(n) : {Nat.is_le(I.AmlRun.steps(Hs.AmlMemHost, I.AmlM.run.go(~Hs.AmlMemHost, ~Hs.AmlMemHost.io, n, I.AmlMachine.halted(Hs.AmlMemHost, m), m, 0n)), _) == True{} : Bool}
2556 run_go_le(n, I.AmlMachine.halted(Hs.AmlMemHost, m), m, 0n)
2557
2558# an outcome counts the steps of its run
2559def outcome_steps(+r: I.AmlRun<Hs.AmlMemHost>) -> {I.AmlRun.steps(Hs.AmlMemHost, r) == A.AmlOutcome.steps(Hs.AmlMemHost, A.AmlOutcome.of_run(Hs.AmlMemHost, r)) : Nat}:
2560 match r:
2561 case I.AmlRun{m, s}:
2562 match m:
2563 case I.AmlMachine{md, c, fs, w}:
2564 match w:
2565 case I.AmlWorld{ctx, ns, h, e}:
2566 match e:
2567 case I.AmlEnv{wd, o, nts, d, cl}:
2568 {==}
2569
2570def Laws.load_steps_bound(s, aml, n):
2571 %outcome_steps(I.AmlM.run(~Hs.AmlMemHost, ~Hs.AmlMemHost.io, n, A.AmlSystem.loader(Hs.AmlMemHost, s, aml))) : {Nat.is_le(_, n) == True{} : Bool}
2572 Laws.run_steps_bound(n, A.AmlSystem.loader(Hs.AmlMemHost, s, aml))
2573
2574def Laws.eval_steps_bound(s, p, args, n):
2575 %outcome_steps(I.AmlM.run(~Hs.AmlMemHost, ~Hs.AmlMemHost.io, n, A.AmlSystem.caller(~Hs.AmlMemHost, ~Hs.AmlMemHost.io, s, p, args))) : {Nat.is_le(_, n) == True{} : Bool}
2576 Laws.run_steps_bound(n, A.AmlSystem.caller(~Hs.AmlMemHost, ~Hs.AmlMemHost.io, s, p, args))
2577
2578# Witnesses and vectors: by computation
2579
2580def Laws.pkglength_example():
2581 Laws.pkglength_round_trip(1000, B.Octets.of_string("AML"), {==})
2582
2583def Laws.namestring_example():
2584 Laws.namestring_round_trip(N.AmlName.of_text("\\_SB.PCI0.LPCB"), B.Octets.of_string("x"), {==})
2585
2586def Laws.header_example():
2587 Laws.header_round_trip(X.ex.hdr("APIC", 5), {==}, {==}, {==}, {==}, {==}, {==})
2588
2589def Laws.check_example():
2590 {==}
2591
2592def Laws.parse_example():
2593 {==}
2594
2595def Laws.rsdp_example():
2596 {==}
2597
2598def Laws.rsdp_v1_example():
2599 {==}
2600
2601def Laws.pkglength_63():
2602 {==}
2603
2604def Laws.pkglength_64():
2605 {==}
2606
2607def Laws.pkglength_4095():
2608 {==}
2609
2610def Laws.pkglength_4096():
2611 {==}
2612
2613def Laws.pkglength_max():
2614 {==}
2615
2616def Laws.pkglength_reserved():
2617 {==}
2618
2619def Laws.name_dual():
2620 {==}
2621
2622def Laws.name_multi():
2623 {==}
2624
2625def Laws.name_parents():
2626 {==}
2627
2628def Laws.name_root():
2629 {==}
2630
2631def Laws.name_bad_seg():
2632 {==}
2633
2634def Laws.eisaid_power_button():
2635 {==}
2636
2637def Laws.eisaid_pci():
2638 {==}
2639
2640def Laws.aml_name_hid():
2641 {==}
2642
2643def Laws.aml_method_sta():
2644 {==}
2645
2646def Laws.checksum_built():
2647 {==}
2648
2649def Laws.checksum_broken():
2650 {==}
2651
2652def Laws.aml_eval_sta():
2653 {==}