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