PROOF_checksum.bend
bend-osdev-acpi@0.1.2.0 · 277 lines · 0 definitions
1# The proof of LAWS_checksum.bend.
2#
3# AcpiChecksum.sum adds the bytes' low 8 bits in a U32 and keeps the low 8
4# bits of the total. Its value is low(8, ckp.ns(bytes)), ckp.ns being the
5# Nat sum of the bytes' low 8 bits (ckp.sumv): the low 8 bits of a U32 sum
6# do not see the 2^32 a wrap takes away (u32's u32_add_wrap, and low_add_dbl
7# with 2^32 = 2^8 2^24), nor the high bits of an addend (ckp.l1). fix(i, o)
8# is take(i, o) ++ [b] ++ drop(1 + i, o), and o itself is take(i, o) ++
9# [o_i] ++ drop(1 + i, o) (ckp.split, through bytes' take, drop and at
10# laws). With S the sum of o and T the sum of the bytes other than o_i,
11# byte_for computes w = S - o_i and b = 256 - w, each modulo 256 (U32
12# subtraction plus the subtrahend is the minuend plus 2^32 on a borrow,
13# u32_sub_wrap); so w = T and b + T = 0 modulo 256 (ckp.zero, by cancelling
14# o_i: ckp.cancel).
15import Base
16import bend-osdev-bytes@0.1.1.1/bytes.bend as B
17import bend-osdev-bytes@0.1.1.1/LAWS.bend as BL
18import bend-osdev-bytes@0.1.1.1/PROOF.bend as BP
19import bend-osdev-u32@0.1.0.0/u32.bend as U
20import bend-osdev-u32@0.1.0.0/LAWS.bend as UL
21import bend-osdev-u32@0.1.0.0/PROOF.bend as UP
22import bend-osdev-u32@0.1.0.0/LAWS_order.bend as UO
23import bend-osdev-u32@0.1.0.0/PROOF_order.bend as UOP
24import bend-osdev-acpi@0.1.2.0/checksum.bend as C
25import bend-osdev-acpi@0.1.2.0/LAWS_checksum.bend as Laws
26
27def ckp.bool(+b: Bool) -> Type:
28 match b:
29 case True{}:
30 Empty
31 case False{}:
32 Unit
33
34def ckp.ft(+e: {False{} == True{} : Bool}) -> Empty:
35 %e : ckp.bool(_)
36 Unit{}
37
38def ckp.isz(+n: Nat) -> Type:
39 match n:
40 case 0n:
41 Unit
42 case 1n+p:
43 Empty
44
45def ckp.nz0(+e: {0n == 1n : Nat}) -> Empty:
46 %e : ckp.isz(_)
47 Unit{}
48
49def ckp.is1(+n: Nat) -> Type:
50 match n:
51 case 0n:
52 Unit
53 case 1n+p:
54 match p:
55 case 0n:
56 Empty
57 case 1n+q:
58 Unit
59
60def ckp.nz1(-k: Nat, +e: {1n+1n+k == 1n : Nat}) -> Empty:
61 %e : ckp.is1(_)
62 Unit{}
63
64# a byte's low 8 bits, through bytes' byte, are its low 8 bits
65
66def ckp.bb2(+z: U32) -> {B.byte(U32.and(255, z)) == U32.and(255, z) : U32}:
67 match z:
68 case U32{WCon{z0, WCon{z1, WCon{z2, WCon{z3, WCon{z4, WCon{z5, WCon{z6, WCon{z7, WCon{z8, WCon{z9, WCon{z10, WCon{z11, WCon{z12, WCon{z13, WCon{z14, WCon{z15, WCon{z16, WCon{z17, WCon{z18, WCon{z19, WCon{z20, WCon{z21, WCon{z22, WCon{z23, WCon{z24, WCon{z25, WCon{z26, WCon{z27, WCon{z28, WCon{z29, WCon{z30, WCon{z31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
69 {==}
70
71def ckp.bb3(+z: U32) -> {U32.and(255, B.byte(z)) == U32.and(255, z) : U32}:
72 match z:
73 case U32{WCon{z0, WCon{z1, WCon{z2, WCon{z3, WCon{z4, WCon{z5, WCon{z6, WCon{z7, WCon{z8, WCon{z9, WCon{z10, WCon{z11, WCon{z12, WCon{z13, WCon{z14, WCon{z15, WCon{z16, WCon{z17, WCon{z18, WCon{z19, WCon{z20, WCon{z21, WCon{z22, WCon{z23, WCon{z24, WCon{z25, WCon{z26, WCon{z27, WCon{z28, WCon{z29, WCon{z30, WCon{z31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
74 {==}
75
76def ckp.bb(+z: U32) -> {U32.and(255, B.byte(U32.and(255, z))) == U32.and(255, z) : U32}:
77 match z:
78 case U32{WCon{z0, WCon{z1, WCon{z2, WCon{z3, WCon{z4, WCon{z5, WCon{z6, WCon{z7, WCon{z8, WCon{z9, WCon{z10, WCon{z11, WCon{z12, WCon{z13, WCon{z14, WCon{z15, WCon{z16, WCon{z17, WCon{z18, WCon{z19, WCon{z20, WCon{z21, WCon{z22, WCon{z23, WCon{z24, WCon{z25, WCon{z26, WCon{z27, WCon{z28, WCon{z29, WCon{z30, WCon{z31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
79 {==}
80
81# Nat arithmetic modulo 256
82
83def ckp.am(+z: U32) -> {U32.to_nat(U32.and(255, z)) == U.U32Nat.low(8n, U32.to_nat(z)) : Nat}:
84 %UL.u32_and_comm(z, 255) : {U32.to_nat(_) == U.U32Nat.low(8n, U32.to_nat(z)) : Nat}
85 UL.u32_and_mask(z, 255, 8n, {==})
86
87def ckp.l1(+x: Nat, +y: Nat) -> {U.U32Nat.low(8n, Nat.add(x, y)) == U.U32Nat.low(8n, Nat.add(U.U32Nat.low(8n, x), y)) : Nat}:
88 %UL.low_high(8n, x) : {U.U32Nat.low(8n, Nat.add(_, y)) == U.U32Nat.low(8n, Nat.add(U.U32Nat.low(8n, x), y)) : Nat}
89 %Equal.sym(Nat, Nat.add(Nat.add(U.U32Nat.low(8n, x), U.U32Nat.dbl(8n, U.U32Nat.high(8n, x))), y), Nat.add(U.U32Nat.low(8n, x), Nat.add(U.U32Nat.dbl(8n, U.U32Nat.high(8n, x)), y)), UL.nat_add_assoc(U.U32Nat.low(8n, x), U.U32Nat.dbl(8n, U.U32Nat.high(8n, x)), y)) : {U.U32Nat.low(8n, _) == U.U32Nat.low(8n, Nat.add(U.U32Nat.low(8n, x), y)) : Nat}
90 %UL.nat_add_comm(y, U.U32Nat.dbl(8n, U.U32Nat.high(8n, x))) : {U.U32Nat.low(8n, Nat.add(U.U32Nat.low(8n, x), _)) == U.U32Nat.low(8n, Nat.add(U.U32Nat.low(8n, x), y)) : Nat}
91 %UL.nat_add_assoc(U.U32Nat.low(8n, x), y, U.U32Nat.dbl(8n, U.U32Nat.high(8n, x))) : {U.U32Nat.low(8n, _) == U.U32Nat.low(8n, Nat.add(U.U32Nat.low(8n, x), y)) : Nat}
92 UL.low_add_dbl(8n, Nat.add(U.U32Nat.low(8n, x), y), U.U32Nat.high(8n, x))
93
94def ckp.l1r(+a: Nat, +b: Nat) -> {U.U32Nat.low(8n, Nat.add(a, b)) == U.U32Nat.low(8n, Nat.add(a, U.U32Nat.low(8n, b))) : Nat}:
95 %UL.nat_add_comm(b, a) : {U.U32Nat.low(8n, _) == U.U32Nat.low(8n, Nat.add(a, U.U32Nat.low(8n, b))) : Nat}
96 %UL.nat_add_comm(U.U32Nat.low(8n, b), a) : {U.U32Nat.low(8n, Nat.add(b, a)) == U.U32Nat.low(8n, _) : Nat}
97 ckp.l1(b, a)
98
99def ckp.l2(+z: Nat, +k: Nat) -> {U.U32Nat.low(8n, Nat.add(z, U.U32Nat.dbl(32n, k))) == U.U32Nat.low(8n, z) : Nat}:
100 %UL.dbl_dbl(8n, 24n, k) : {U.U32Nat.low(8n, Nat.add(z, _)) == U.U32Nat.low(8n, z) : Nat}
101 UL.low_add_dbl(8n, z, U.U32Nat.dbl(24n, k))
102
103def ckp.ll(+z: Nat) -> {U.U32Nat.low(8n, U.U32Nat.low(8n, z)) == U.U32Nat.low(8n, z) : Nat}:
104 UL.low_small(8n, U.U32Nat.low(8n, z), UL.low_lt(8n, z))
105
106# x + a and x + b agree modulo 256: so do a and b
107
108def ckp.cr(+x: Nat, +a: Nat, +b: Nat, +e: {U.U32Nat.low(8n, Nat.add(x, a)) == U.U32Nat.low(8n, Nat.add(x, b)) : Nat}) -> {Nat.add(x, Nat.add(a, U.U32Nat.dbl(8n, U.U32Nat.high(8n, Nat.add(x, b))))) == Nat.add(x, Nat.add(b, U.U32Nat.dbl(8n, U.U32Nat.high(8n, Nat.add(x, a))))) : Nat}:
109 %UL.nat_add_assoc(x, a, U.U32Nat.dbl(8n, U.U32Nat.high(8n, Nat.add(x, b)))) : {_ == Nat.add(x, Nat.add(b, U.U32Nat.dbl(8n, U.U32Nat.high(8n, Nat.add(x, a))))) : Nat}
110 %UL.low_high(8n, Nat.add(x, a)) : {Nat.add(_, U.U32Nat.dbl(8n, U.U32Nat.high(8n, Nat.add(x, b)))) == Nat.add(x, Nat.add(b, U.U32Nat.dbl(8n, U.U32Nat.high(8n, Nat.add(x, a))))) : Nat}
111 %UL.nat_add_assoc(x, b, U.U32Nat.dbl(8n, U.U32Nat.high(8n, Nat.add(x, a)))) : {Nat.add(Nat.add(U.U32Nat.low(8n, Nat.add(x, a)), U.U32Nat.dbl(8n, U.U32Nat.high(8n, Nat.add(x, a)))), U.U32Nat.dbl(8n, U.U32Nat.high(8n, Nat.add(x, b)))) == _ : Nat}
112 %UL.low_high(8n, Nat.add(x, b)) : {Nat.add(Nat.add(U.U32Nat.low(8n, Nat.add(x, a)), U.U32Nat.dbl(8n, U.U32Nat.high(8n, Nat.add(x, a)))), U.U32Nat.dbl(8n, U.U32Nat.high(8n, Nat.add(x, b)))) == Nat.add(_, U.U32Nat.dbl(8n, U.U32Nat.high(8n, Nat.add(x, a)))) : Nat}
113 %Equal.sym(Nat, U.U32Nat.low(8n, Nat.add(x, a)), U.U32Nat.low(8n, Nat.add(x, b)), e) : {Nat.add(Nat.add(_, U.U32Nat.dbl(8n, U.U32Nat.high(8n, Nat.add(x, a)))), U.U32Nat.dbl(8n, U.U32Nat.high(8n, Nat.add(x, b)))) == Nat.add(Nat.add(U.U32Nat.low(8n, Nat.add(x, b)), U.U32Nat.dbl(8n, U.U32Nat.high(8n, Nat.add(x, b)))), U.U32Nat.dbl(8n, U.U32Nat.high(8n, Nat.add(x, a)))) : Nat}
114 %Equal.sym(Nat, Nat.add(Nat.add(U.U32Nat.low(8n, Nat.add(x, b)), U.U32Nat.dbl(8n, U.U32Nat.high(8n, Nat.add(x, a)))), U.U32Nat.dbl(8n, U.U32Nat.high(8n, Nat.add(x, b)))), Nat.add(U.U32Nat.low(8n, Nat.add(x, b)), Nat.add(U.U32Nat.dbl(8n, U.U32Nat.high(8n, Nat.add(x, a))), U.U32Nat.dbl(8n, U.U32Nat.high(8n, Nat.add(x, b))))), UL.nat_add_assoc(U.U32Nat.low(8n, Nat.add(x, b)), U.U32Nat.dbl(8n, U.U32Nat.high(8n, Nat.add(x, a))), U.U32Nat.dbl(8n, U.U32Nat.high(8n, Nat.add(x, b))))) : {_ == Nat.add(Nat.add(U.U32Nat.low(8n, Nat.add(x, b)), U.U32Nat.dbl(8n, U.U32Nat.high(8n, Nat.add(x, b)))), U.U32Nat.dbl(8n, U.U32Nat.high(8n, Nat.add(x, a)))) : Nat}
115 %Equal.sym(Nat, Nat.add(Nat.add(U.U32Nat.low(8n, Nat.add(x, b)), U.U32Nat.dbl(8n, U.U32Nat.high(8n, Nat.add(x, b)))), U.U32Nat.dbl(8n, U.U32Nat.high(8n, Nat.add(x, a)))), Nat.add(U.U32Nat.low(8n, Nat.add(x, b)), Nat.add(U.U32Nat.dbl(8n, U.U32Nat.high(8n, Nat.add(x, b))), U.U32Nat.dbl(8n, U.U32Nat.high(8n, Nat.add(x, a))))), UL.nat_add_assoc(U.U32Nat.low(8n, Nat.add(x, b)), U.U32Nat.dbl(8n, U.U32Nat.high(8n, Nat.add(x, b))), U.U32Nat.dbl(8n, U.U32Nat.high(8n, Nat.add(x, a))))) : {Nat.add(U.U32Nat.low(8n, Nat.add(x, b)), Nat.add(U.U32Nat.dbl(8n, U.U32Nat.high(8n, Nat.add(x, a))), U.U32Nat.dbl(8n, U.U32Nat.high(8n, Nat.add(x, b))))) == _ : Nat}
116 %UL.nat_add_comm(U.U32Nat.dbl(8n, U.U32Nat.high(8n, Nat.add(x, a))), U.U32Nat.dbl(8n, U.U32Nat.high(8n, Nat.add(x, b)))) : {Nat.add(U.U32Nat.low(8n, Nat.add(x, b)), Nat.add(U.U32Nat.dbl(8n, U.U32Nat.high(8n, Nat.add(x, a))), U.U32Nat.dbl(8n, U.U32Nat.high(8n, Nat.add(x, b))))) == Nat.add(U.U32Nat.low(8n, Nat.add(x, b)), _) : Nat}
117 {==}
118
119def ckp.cancel(+x: Nat, +a: Nat, +b: Nat, +e: {U.U32Nat.low(8n, Nat.add(x, a)) == U.U32Nat.low(8n, Nat.add(x, b)) : Nat}) -> {U.U32Nat.low(8n, a) == U.U32Nat.low(8n, b) : Nat}:
120 %UL.low_add_dbl(8n, a, U.U32Nat.high(8n, Nat.add(x, b))) : {_ == U.U32Nat.low(8n, b) : Nat}
121 %UL.low_add_dbl(8n, b, U.U32Nat.high(8n, Nat.add(x, a))) : {U.U32Nat.low(8n, Nat.add(a, U.U32Nat.dbl(8n, U.U32Nat.high(8n, Nat.add(x, b))))) == _ : Nat}
122 %UL.nat_add_cancel(x, Nat.add(a, U.U32Nat.dbl(8n, U.U32Nat.high(8n, Nat.add(x, b)))), Nat.add(b, U.U32Nat.dbl(8n, U.U32Nat.high(8n, Nat.add(x, a)))), ckp.cr(x, a, b, e)) : {U.U32Nat.low(8n, Nat.add(a, U.U32Nat.dbl(8n, U.U32Nat.high(8n, Nat.add(x, b))))) == U.U32Nat.low(8n, _) : Nat}
123 {==}
124
125# w + x = A + (x + D) and c + w = 0 modulo 256: A + (c + D) = 0
126
127def ckp.e1x(+nA: Nat, +nD: Nat, +x: Nat, +w: Nat, +e1: {U.U32Nat.low(8n, Nat.add(w, x)) == U.U32Nat.low(8n, Nat.add(nA, Nat.add(x, nD))) : Nat}) -> {U.U32Nat.low(8n, Nat.add(x, w)) == U.U32Nat.low(8n, Nat.add(x, Nat.add(nA, nD))) : Nat}:
128 %UL.nat_add_comm(w, x) : {U.U32Nat.low(8n, _) == U.U32Nat.low(8n, Nat.add(x, Nat.add(nA, nD))) : Nat}
129 %UL.nat_add_left_comm(nA, x, nD) : {U.U32Nat.low(8n, Nat.add(w, x)) == U.U32Nat.low(8n, _) : Nat}
130 e1
131
132def ckp.zero(+nA: Nat, +nD: Nat, +x: Nat, +c: Nat, +w: Nat, +e1: {U.U32Nat.low(8n, Nat.add(w, x)) == U.U32Nat.low(8n, Nat.add(nA, Nat.add(x, nD))) : Nat}, +e2: {U.U32Nat.low(8n, Nat.add(c, w)) == 0n : Nat}) -> {U.U32Nat.low(8n, Nat.add(nA, Nat.add(c, nD))) == 0n : Nat}:
133 %UL.nat_add_left_comm(c, nA, nD) : {U.U32Nat.low(8n, _) == 0n : Nat}
134 %Equal.sym(Nat, U.U32Nat.low(8n, Nat.add(c, Nat.add(nA, nD))), U.U32Nat.low(8n, Nat.add(c, U.U32Nat.low(8n, Nat.add(nA, nD)))), ckp.l1r(c, Nat.add(nA, nD))) : {_ == 0n : Nat}
135 %ckp.cancel(x, w, Nat.add(nA, nD), ckp.e1x(nA, nD, x, w, e1)) : {U.U32Nat.low(8n, Nat.add(c, _)) == 0n : Nat}
136 %ckp.l1r(c, w) : {_ == 0n : Nat}
137 e2
138
139# The sum's value: low(8, ns(bytes))
140
141def ckp.ns(xs: List<&2, U32>) -> Nat:
142 match xs:
143 case Nil{}:
144 0n
145 case Con{h, t}:
146 Nat.add(U32.to_nat(U32.and(255, h)), ckp.ns(t))
147
148def ckp.go(+xs: List<&2, U32>, +acc: U32) -> {U.U32Nat.low(8n, U32.to_nat(C.ck.sum.go(xs, acc))) == U.U32Nat.low(8n, Nat.add(U32.to_nat(acc), ckp.ns(xs))) : Nat}:
149 match xs:
150 case Nil{}:
151 %Equal.sym(Nat, Nat.add(U32.to_nat(acc), 0n), U32.to_nat(acc), UL.nat_add_zero(U32.to_nat(acc))) : {U.U32Nat.low(8n, U32.to_nat(acc)) == U.U32Nat.low(8n, _) : Nat}
152 {==}
153 case Con{+h, +t}:
154 %Equal.sym(Nat, U.U32Nat.low(8n, U32.to_nat(C.ck.sum.go(t, U32.add(acc, U32.and(255, h))))), U.U32Nat.low(8n, Nat.add(U32.to_nat(U32.add(acc, U32.and(255, h))), ckp.ns(t))), ckp.go(t, U32.add(acc, U32.and(255, h)))) : {_ == U.U32Nat.low(8n, Nat.add(U32.to_nat(acc), Nat.add(U32.to_nat(U32.and(255, h)), ckp.ns(t)))) : Nat}
155 %UL.nat_add_assoc(U32.to_nat(acc), U32.to_nat(U32.and(255, h)), ckp.ns(t)) : {U.U32Nat.low(8n, Nat.add(U32.to_nat(U32.add(acc, U32.and(255, h))), ckp.ns(t))) == U.U32Nat.low(8n, _) : Nat}
156 %UL.u32_add_wrap(acc, U32.and(255, h)) : {U.U32Nat.low(8n, Nat.add(U32.to_nat(U32.add(acc, U32.and(255, h))), ckp.ns(t))) == U.U32Nat.low(8n, Nat.add(_, ckp.ns(t))) : Nat}
157 %Equal.sym(Nat, Nat.add(Nat.add(U32.to_nat(U32.add(acc, U32.and(255, h))), U.U32Nat.dbl(32n, U.U32Nat.bit(U32.is_lt(U32.add(acc, U32.and(255, h)), acc)))), ckp.ns(t)), Nat.add(U32.to_nat(U32.add(acc, U32.and(255, h))), Nat.add(U.U32Nat.dbl(32n, U.U32Nat.bit(U32.is_lt(U32.add(acc, U32.and(255, h)), acc))), ckp.ns(t))), UL.nat_add_assoc(U32.to_nat(U32.add(acc, U32.and(255, h))), U.U32Nat.dbl(32n, U.U32Nat.bit(U32.is_lt(U32.add(acc, U32.and(255, h)), acc))), ckp.ns(t))) : {U.U32Nat.low(8n, Nat.add(U32.to_nat(U32.add(acc, U32.and(255, h))), ckp.ns(t))) == U.U32Nat.low(8n, _) : Nat}
158 %UL.nat_add_comm(ckp.ns(t), U.U32Nat.dbl(32n, U.U32Nat.bit(U32.is_lt(U32.add(acc, U32.and(255, h)), acc)))) : {U.U32Nat.low(8n, Nat.add(U32.to_nat(U32.add(acc, U32.and(255, h))), ckp.ns(t))) == U.U32Nat.low(8n, Nat.add(U32.to_nat(U32.add(acc, U32.and(255, h))), _)) : Nat}
159 %UL.nat_add_assoc(U32.to_nat(U32.add(acc, U32.and(255, h))), ckp.ns(t), U.U32Nat.dbl(32n, U.U32Nat.bit(U32.is_lt(U32.add(acc, U32.and(255, h)), acc)))) : {U.U32Nat.low(8n, Nat.add(U32.to_nat(U32.add(acc, U32.and(255, h))), ckp.ns(t))) == U.U32Nat.low(8n, _) : Nat}
160 Equal.sym(Nat, U.U32Nat.low(8n, Nat.add(Nat.add(U32.to_nat(U32.add(acc, U32.and(255, h))), ckp.ns(t)), U.U32Nat.dbl(32n, U.U32Nat.bit(U32.is_lt(U32.add(acc, U32.and(255, h)), acc))))), U.U32Nat.low(8n, Nat.add(U32.to_nat(U32.add(acc, U32.and(255, h))), ckp.ns(t))), ckp.l2(Nat.add(U32.to_nat(U32.add(acc, U32.and(255, h))), ckp.ns(t)), U.U32Nat.bit(U32.is_lt(U32.add(acc, U32.and(255, h)), acc))))
161
162def ckp.sumv(+o: B.Octets) -> {U32.to_nat(C.AcpiChecksum.sum(o)) == U.U32Nat.low(8n, ckp.ns(B.Octets.to_list(o))) : Nat}:
163 %Equal.sym(Nat, U32.to_nat(U32.and(255, C.ck.sum.go(B.Octets.to_list(o), 0))), U.U32Nat.low(8n, U32.to_nat(C.ck.sum.go(B.Octets.to_list(o), 0))), ckp.am(C.ck.sum.go(B.Octets.to_list(o), 0))) : {_ == U.U32Nat.low(8n, ckp.ns(B.Octets.to_list(o))) : Nat}
164 ckp.go(B.Octets.to_list(o), 0)
165
166def ckp.nsapp(+xs: List<&2, U32>, +ys: List<&2, U32>) -> {ckp.ns(B.append(xs, ys)) == Nat.add(ckp.ns(xs), ckp.ns(ys)) : Nat}:
167 match xs:
168 case Nil{}:
169 {==}
170 case Con{+h, +t}:
171 %Equal.sym(Nat, ckp.ns(B.append(t, ys)), Nat.add(ckp.ns(t), ckp.ns(ys)), ckp.nsapp(t, ys)) : {Nat.add(U32.to_nat(U32.and(255, h)), _) == Nat.add(ckp.ns(Con{h, t}), ckp.ns(ys)) : Nat}
172 Equal.sym(Nat, Nat.add(Nat.add(U32.to_nat(U32.and(255, h)), ckp.ns(t)), ckp.ns(ys)), Nat.add(U32.to_nat(U32.and(255, h)), Nat.add(ckp.ns(t), ckp.ns(ys))), UL.nat_add_assoc(U32.to_nat(U32.and(255, h)), ckp.ns(t), ckp.ns(ys)))
173
174# A byte string with a byte at offset i: the bytes before it, it, and the
175# bytes after it
176
177def ckp.one(+l: List<&2, U32>, +hl: {B.len(l) == 1n : Nat}) -> {ckp.ns(l) == U32.to_nat(U32.and(255, Maybe.default(&2, U32, B.at(l, 0n), 0))) : Nat}:
178 match l:
179 case Nil{}:
180 Empty.absurd({ckp.ns(Nil{}) == U32.to_nat(U32.and(255, Maybe.default(&2, U32, B.at(Nil{}, 0n), 0))) : Nat}, ckp.nz0(hl))
181 case Con{+h, +t}:
182 match t:
183 case Nil{}:
184 %Equal.sym(U32, U32.and(255, B.byte(h)), U32.and(255, h), ckp.bb3(h)) : {Nat.add(U32.to_nat(U32.and(255, h)), 0n) == U32.to_nat(_) : Nat}
185 UL.nat_add_zero(U32.to_nat(U32.and(255, h)))
186 case Con{h2, t2}:
187 Empty.absurd({ckp.ns(Con{h, Con{h2, t2}}) == U32.to_nat(U32.and(255, Maybe.default(&2, U32, B.at(Con{h, Con{h2, t2}}, 0n), 0))) : Nat}, ckp.nz1(B.len(t2), hl))
188
189def ckp.head(+d: B.Octets, +hd: {Nat.is_le(1n, B.Octets.len(d)) == True{} : Bool}) -> {ckp.ns(B.Octets.to_list(d)) == Nat.add(U32.to_nat(U32.and(255, Maybe.default(&2, U32, B.Octets.at(d, 0n), 0))), ckp.ns(B.Octets.to_list(B.Octets.drop(1n, d)))) : Nat}:
190 %BL.octets_take_drop(1n, d) : {ckp.ns(B.Octets.to_list(_)) == Nat.add(U32.to_nat(U32.and(255, Maybe.default(&2, U32, B.Octets.at(d, 0n), 0))), ckp.ns(B.Octets.to_list(B.Octets.drop(1n, d)))) : Nat}
191 %Equal.sym(List<&2, U32>, B.Octets.to_list(B.Octets.append(B.Octets.take(1n, d), B.Octets.drop(1n, d))), B.append(B.Octets.to_list(B.Octets.take(1n, d)), B.Octets.to_list(B.Octets.drop(1n, d))), BL.octets_append_list(B.Octets.take(1n, d), B.Octets.drop(1n, d))) : {ckp.ns(_) == Nat.add(U32.to_nat(U32.and(255, Maybe.default(&2, U32, B.Octets.at(d, 0n), 0))), ckp.ns(B.Octets.to_list(B.Octets.drop(1n, d)))) : Nat}
192 %Equal.sym(Nat, ckp.ns(B.append(B.Octets.to_list(B.Octets.take(1n, d)), B.Octets.to_list(B.Octets.drop(1n, d)))), Nat.add(ckp.ns(B.Octets.to_list(B.Octets.take(1n, d))), ckp.ns(B.Octets.to_list(B.Octets.drop(1n, d)))), ckp.nsapp(B.Octets.to_list(B.Octets.take(1n, d)), B.Octets.to_list(B.Octets.drop(1n, d)))) : {_ == Nat.add(U32.to_nat(U32.and(255, Maybe.default(&2, U32, B.Octets.at(d, 0n), 0))), ckp.ns(B.Octets.to_list(B.Octets.drop(1n, d)))) : Nat}
193 %BL.octets_at_take(1n, d, 0n, {==}) : {Nat.add(ckp.ns(B.Octets.to_list(B.Octets.take(1n, d))), ckp.ns(B.Octets.to_list(B.Octets.drop(1n, d)))) == Nat.add(U32.to_nat(U32.and(255, Maybe.default(&2, U32, _, 0))), ckp.ns(B.Octets.to_list(B.Octets.drop(1n, d)))) : Nat}
194 %Equal.sym(Maybe<&2, U32>, B.Octets.at(B.Octets.take(1n, d), 0n), B.at(B.Octets.to_list(B.Octets.take(1n, d)), 0n), BL.octets_at_list(B.Octets.take(1n, d), 0n)) : {Nat.add(ckp.ns(B.Octets.to_list(B.Octets.take(1n, d))), ckp.ns(B.Octets.to_list(B.Octets.drop(1n, d)))) == Nat.add(U32.to_nat(U32.and(255, Maybe.default(&2, U32, _, 0))), ckp.ns(B.Octets.to_list(B.Octets.drop(1n, d)))) : Nat}
195 %ckp.one(B.Octets.to_list(B.Octets.take(1n, d)), Equal.trans(Nat, B.len(B.Octets.to_list(B.Octets.take(1n, d))), B.Octets.len(B.Octets.take(1n, d)), 1n, Equal.sym(Nat, B.Octets.len(B.Octets.take(1n, d)), B.len(B.Octets.to_list(B.Octets.take(1n, d))), BL.octets_len_list(B.Octets.take(1n, d))), BL.octets_len_take_le(1n, d, hd))) : {Nat.add(ckp.ns(B.Octets.to_list(B.Octets.take(1n, d))), ckp.ns(B.Octets.to_list(B.Octets.drop(1n, d)))) == Nat.add(_, ckp.ns(B.Octets.to_list(B.Octets.drop(1n, d)))) : Nat}
196 {==}
197
198def ckp.lt_sub(+i: Nat, +n: Nat, +h: {Nat.is_lt(i, n) == True{} : Bool}) -> {Nat.is_le(1n, Nat.sub(n, i)) == True{} : Bool}:
199 match i:
200 case 0n:
201 match n:
202 case 0n:
203 Empty.absurd({Nat.is_le(1n, Nat.sub(0n, 0n)) == True{} : Bool}, ckp.ft(h))
204 case 1n+p:
205 UO.nat_le_add_r(1n, p)
206 case 1n+ip:
207 match n:
208 case 0n:
209 Empty.absurd({Nat.is_le(1n, Nat.sub(0n, 1n+ip)) == True{} : Bool}, ckp.ft(h))
210 case 1n+p:
211 ckp.lt_sub(ip, p, h)
212
213def ckp.hdd(+i: Nat, +o: B.Octets, +h: {Nat.is_lt(i, B.Octets.len(o)) == True{} : Bool}) -> {Nat.is_le(1n, B.Octets.len(B.Octets.drop(i, o))) == True{} : Bool}:
214 %Equal.sym(Nat, B.Octets.len(B.Octets.drop(i, o)), Nat.sub(B.Octets.len(o), i), BL.octets_len_drop(i, o)) : {Nat.is_le(1n, _) == True{} : Bool}
215 ckp.lt_sub(i, B.Octets.len(o), h)
216
217def ckp.split(+i: Nat, +o: B.Octets, +h: {Nat.is_lt(i, B.Octets.len(o)) == True{} : Bool}) -> {ckp.ns(B.Octets.to_list(o)) == Nat.add(ckp.ns(B.Octets.to_list(B.Octets.take(i, o))), Nat.add(U32.to_nat(U32.and(255, Maybe.default(&2, U32, B.Octets.at(o, i), 0))), ckp.ns(B.Octets.to_list(B.Octets.drop(1n+i, o))))) : Nat}:
218 %BL.octets_take_drop(i, o) : {ckp.ns(B.Octets.to_list(_)) == Nat.add(ckp.ns(B.Octets.to_list(B.Octets.take(i, o))), Nat.add(U32.to_nat(U32.and(255, Maybe.default(&2, U32, B.Octets.at(o, i), 0))), ckp.ns(B.Octets.to_list(B.Octets.drop(1n+i, o))))) : Nat}
219 %Equal.sym(List<&2, U32>, B.Octets.to_list(B.Octets.append(B.Octets.take(i, o), B.Octets.drop(i, o))), B.append(B.Octets.to_list(B.Octets.take(i, o)), B.Octets.to_list(B.Octets.drop(i, o))), BL.octets_append_list(B.Octets.take(i, o), B.Octets.drop(i, o))) : {ckp.ns(_) == Nat.add(ckp.ns(B.Octets.to_list(B.Octets.take(i, o))), Nat.add(U32.to_nat(U32.and(255, Maybe.default(&2, U32, B.Octets.at(o, i), 0))), ckp.ns(B.Octets.to_list(B.Octets.drop(1n+i, o))))) : Nat}
220 %Equal.sym(Nat, ckp.ns(B.append(B.Octets.to_list(B.Octets.take(i, o)), B.Octets.to_list(B.Octets.drop(i, o)))), Nat.add(ckp.ns(B.Octets.to_list(B.Octets.take(i, o))), ckp.ns(B.Octets.to_list(B.Octets.drop(i, o)))), ckp.nsapp(B.Octets.to_list(B.Octets.take(i, o)), B.Octets.to_list(B.Octets.drop(i, o)))) : {_ == Nat.add(ckp.ns(B.Octets.to_list(B.Octets.take(i, o))), Nat.add(U32.to_nat(U32.and(255, Maybe.default(&2, U32, B.Octets.at(o, i), 0))), ckp.ns(B.Octets.to_list(B.Octets.drop(1n+i, o))))) : Nat}
221 %Equal.sym(Nat, ckp.ns(B.Octets.to_list(B.Octets.drop(i, o))), Nat.add(U32.to_nat(U32.and(255, Maybe.default(&2, U32, B.Octets.at(B.Octets.drop(i, o), 0n), 0))), ckp.ns(B.Octets.to_list(B.Octets.drop(1n, B.Octets.drop(i, o))))), ckp.head(B.Octets.drop(i, o), ckp.hdd(i, o, h))) : {Nat.add(ckp.ns(B.Octets.to_list(B.Octets.take(i, o))), _) == Nat.add(ckp.ns(B.Octets.to_list(B.Octets.take(i, o))), Nat.add(U32.to_nat(U32.and(255, Maybe.default(&2, U32, B.Octets.at(o, i), 0))), ckp.ns(B.Octets.to_list(B.Octets.drop(1n+i, o))))) : Nat}
222 %Equal.sym(Maybe<&2, U32>, B.Octets.at(B.Octets.drop(i, o), 0n), B.Octets.at(o, Nat.add(i, 0n)), BL.octets_at_drop(i, o, 0n)) : {Nat.add(ckp.ns(B.Octets.to_list(B.Octets.take(i, o))), Nat.add(U32.to_nat(U32.and(255, Maybe.default(&2, U32, _, 0))), ckp.ns(B.Octets.to_list(B.Octets.drop(1n, B.Octets.drop(i, o)))))) == Nat.add(ckp.ns(B.Octets.to_list(B.Octets.take(i, o))), Nat.add(U32.to_nat(U32.and(255, Maybe.default(&2, U32, B.Octets.at(o, i), 0))), ckp.ns(B.Octets.to_list(B.Octets.drop(1n+i, o))))) : Nat}
223 %Equal.sym(Nat, Nat.add(i, 0n), i, UL.nat_add_zero(i)) : {Nat.add(ckp.ns(B.Octets.to_list(B.Octets.take(i, o))), Nat.add(U32.to_nat(U32.and(255, Maybe.default(&2, U32, B.Octets.at(o, _), 0))), ckp.ns(B.Octets.to_list(B.Octets.drop(1n, B.Octets.drop(i, o)))))) == Nat.add(ckp.ns(B.Octets.to_list(B.Octets.take(i, o))), Nat.add(U32.to_nat(U32.and(255, Maybe.default(&2, U32, B.Octets.at(o, i), 0))), ckp.ns(B.Octets.to_list(B.Octets.drop(1n+i, o))))) : Nat}
224 %Equal.sym(B.Octets, B.Octets.drop(1n, B.Octets.drop(i, o)), B.Octets.drop(Nat.add(i, 1n), o), BL.octets_drop_drop(i, 1n, o)) : {Nat.add(ckp.ns(B.Octets.to_list(B.Octets.take(i, o))), Nat.add(U32.to_nat(U32.and(255, Maybe.default(&2, U32, B.Octets.at(o, i), 0))), ckp.ns(B.Octets.to_list(_)))) == Nat.add(ckp.ns(B.Octets.to_list(B.Octets.take(i, o))), Nat.add(U32.to_nat(U32.and(255, Maybe.default(&2, U32, B.Octets.at(o, i), 0))), ckp.ns(B.Octets.to_list(B.Octets.drop(1n+i, o))))) : Nat}
225 %UL.nat_add_comm(1n, i) : {Nat.add(ckp.ns(B.Octets.to_list(B.Octets.take(i, o))), Nat.add(U32.to_nat(U32.and(255, Maybe.default(&2, U32, B.Octets.at(o, i), 0))), ckp.ns(B.Octets.to_list(B.Octets.drop(_, o))))) == Nat.add(ckp.ns(B.Octets.to_list(B.Octets.take(i, o))), Nat.add(U32.to_nat(U32.and(255, Maybe.default(&2, U32, B.Octets.at(o, i), 0))), ckp.ns(B.Octets.to_list(B.Octets.drop(1n+i, o))))) : Nat}
226 {==}
227
228# The fixed bytes: the bytes before i, the checksum byte, the bytes after
229
230def ckp.fixsum(+i: Nat, +o: B.Octets, +h: {Nat.is_lt(i, B.Octets.len(o)) == True{} : Bool}) -> {ckp.ns(B.Octets.to_list(C.AcpiChecksum.fix(i, o))) == Nat.add(ckp.ns(B.Octets.to_list(B.Octets.take(i, o))), Nat.add(U32.to_nat(C.AcpiChecksum.byte_for(i, o)), ckp.ns(B.Octets.to_list(B.Octets.drop(1n+i, o))))) : Nat}:
231 %Equal.sym(Bool, Nat.is_lt(i, B.Octets.len(o)), True{}, h) : {ckp.ns(B.Octets.to_list(C.ck.fix.pick(_, i, o))) == Nat.add(ckp.ns(B.Octets.to_list(B.Octets.take(i, o))), Nat.add(U32.to_nat(C.AcpiChecksum.byte_for(i, o)), ckp.ns(B.Octets.to_list(B.Octets.drop(1n+i, o))))) : Nat}
232 %Equal.sym(B.Octets, B.Octets.concat(Con{B.Octets.take(i, o), [B.Octets.of_list([C.AcpiChecksum.byte_for(i, o)]), B.Octets.drop(1n+i, o)]}), B.Octets.append(B.Octets.take(i, o), B.Octets.concat([B.Octets.of_list([C.AcpiChecksum.byte_for(i, o)]), B.Octets.drop(1n+i, o)])), BL.octets_concat_cons(B.Octets.take(i, o), [B.Octets.of_list([C.AcpiChecksum.byte_for(i, o)]), B.Octets.drop(1n+i, o)])) : {ckp.ns(B.Octets.to_list(_)) == Nat.add(ckp.ns(B.Octets.to_list(B.Octets.take(i, o))), Nat.add(U32.to_nat(C.AcpiChecksum.byte_for(i, o)), ckp.ns(B.Octets.to_list(B.Octets.drop(1n+i, o))))) : Nat}
233 %Equal.sym(B.Octets, B.Octets.concat(Con{B.Octets.of_list([C.AcpiChecksum.byte_for(i, o)]), [B.Octets.drop(1n+i, o)]}), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, o)]), B.Octets.concat([B.Octets.drop(1n+i, o)])), BL.octets_concat_cons(B.Octets.of_list([C.AcpiChecksum.byte_for(i, o)]), [B.Octets.drop(1n+i, o)])) : {ckp.ns(B.Octets.to_list(B.Octets.append(B.Octets.take(i, o), _))) == Nat.add(ckp.ns(B.Octets.to_list(B.Octets.take(i, o))), Nat.add(U32.to_nat(C.AcpiChecksum.byte_for(i, o)), ckp.ns(B.Octets.to_list(B.Octets.drop(1n+i, o))))) : Nat}
234 %Equal.sym(B.Octets, B.Octets.concat(Con{B.Octets.drop(1n+i, o), Nil{}}), B.Octets.append(B.Octets.drop(1n+i, o), B.Octets.concat(Nil{})), BL.octets_concat_cons(B.Octets.drop(1n+i, o), Nil{})) : {ckp.ns(B.Octets.to_list(B.Octets.append(B.Octets.take(i, o), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, o)]), _)))) == Nat.add(ckp.ns(B.Octets.to_list(B.Octets.take(i, o))), Nat.add(U32.to_nat(C.AcpiChecksum.byte_for(i, o)), ckp.ns(B.Octets.to_list(B.Octets.drop(1n+i, o))))) : Nat}
235 %Equal.sym(B.Octets, B.Octets.concat(Nil{}), B.Octets.empty(), BL.octets_concat_nil()) : {ckp.ns(B.Octets.to_list(B.Octets.append(B.Octets.take(i, o), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, o)]), B.Octets.append(B.Octets.drop(1n+i, o), _))))) == Nat.add(ckp.ns(B.Octets.to_list(B.Octets.take(i, o))), Nat.add(U32.to_nat(C.AcpiChecksum.byte_for(i, o)), ckp.ns(B.Octets.to_list(B.Octets.drop(1n+i, o))))) : Nat}
236 %Equal.sym(B.Octets, B.Octets.append(B.Octets.drop(1n+i, o), B.Octets.empty()), B.Octets.drop(1n+i, o), BL.octets_append_empty_r(B.Octets.drop(1n+i, o))) : {ckp.ns(B.Octets.to_list(B.Octets.append(B.Octets.take(i, o), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, o)]), _)))) == Nat.add(ckp.ns(B.Octets.to_list(B.Octets.take(i, o))), Nat.add(U32.to_nat(C.AcpiChecksum.byte_for(i, o)), ckp.ns(B.Octets.to_list(B.Octets.drop(1n+i, o))))) : Nat}
237 %Equal.sym(List<&2, U32>, B.Octets.to_list(B.Octets.append(B.Octets.take(i, o), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, o)]), B.Octets.drop(1n+i, o)))), B.append(B.Octets.to_list(B.Octets.take(i, o)), B.Octets.to_list(B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, o)]), B.Octets.drop(1n+i, o)))), BL.octets_append_list(B.Octets.take(i, o), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, o)]), B.Octets.drop(1n+i, o)))) : {ckp.ns(_) == Nat.add(ckp.ns(B.Octets.to_list(B.Octets.take(i, o))), Nat.add(U32.to_nat(C.AcpiChecksum.byte_for(i, o)), ckp.ns(B.Octets.to_list(B.Octets.drop(1n+i, o))))) : Nat}
238 %Equal.sym(List<&2, U32>, B.Octets.to_list(B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, o)]), B.Octets.drop(1n+i, o))), B.append(B.Octets.to_list(B.Octets.of_list([C.AcpiChecksum.byte_for(i, o)])), B.Octets.to_list(B.Octets.drop(1n+i, o))), BL.octets_append_list(B.Octets.of_list([C.AcpiChecksum.byte_for(i, o)]), B.Octets.drop(1n+i, o))) : {ckp.ns(B.append(B.Octets.to_list(B.Octets.take(i, o)), _)) == Nat.add(ckp.ns(B.Octets.to_list(B.Octets.take(i, o))), Nat.add(U32.to_nat(C.AcpiChecksum.byte_for(i, o)), ckp.ns(B.Octets.to_list(B.Octets.drop(1n+i, o))))) : Nat}
239 %Equal.sym(List<&2, U32>, B.Octets.to_list(B.Octets.of_list([C.AcpiChecksum.byte_for(i, o)])), B.mask([C.AcpiChecksum.byte_for(i, o)]), BL.octets_to_of([C.AcpiChecksum.byte_for(i, o)])) : {ckp.ns(B.append(B.Octets.to_list(B.Octets.take(i, o)), B.append(_, B.Octets.to_list(B.Octets.drop(1n+i, o))))) == Nat.add(ckp.ns(B.Octets.to_list(B.Octets.take(i, o))), Nat.add(U32.to_nat(C.AcpiChecksum.byte_for(i, o)), ckp.ns(B.Octets.to_list(B.Octets.drop(1n+i, o))))) : Nat}
240 %Equal.sym(Nat, ckp.ns(B.append(B.Octets.to_list(B.Octets.take(i, o)), B.append(B.mask([C.AcpiChecksum.byte_for(i, o)]), B.Octets.to_list(B.Octets.drop(1n+i, o))))), Nat.add(ckp.ns(B.Octets.to_list(B.Octets.take(i, o))), ckp.ns(B.append(B.mask([C.AcpiChecksum.byte_for(i, o)]), B.Octets.to_list(B.Octets.drop(1n+i, o))))), ckp.nsapp(B.Octets.to_list(B.Octets.take(i, o)), B.append(B.mask([C.AcpiChecksum.byte_for(i, o)]), B.Octets.to_list(B.Octets.drop(1n+i, o))))) : {_ == Nat.add(ckp.ns(B.Octets.to_list(B.Octets.take(i, o))), Nat.add(U32.to_nat(C.AcpiChecksum.byte_for(i, o)), ckp.ns(B.Octets.to_list(B.Octets.drop(1n+i, o))))) : Nat}
241 %Equal.sym(U32, U32.and(255, B.byte(U32.and(255, U32.sub(256, U32.and(255, U32.sub(C.AcpiChecksum.sum(o), U32.and(255, Maybe.default(&2, U32, B.Octets.at(o, i), 0)))))))), U32.and(255, U32.sub(256, U32.and(255, U32.sub(C.AcpiChecksum.sum(o), U32.and(255, Maybe.default(&2, U32, B.Octets.at(o, i), 0)))))), ckp.bb(U32.sub(256, U32.and(255, U32.sub(C.AcpiChecksum.sum(o), U32.and(255, Maybe.default(&2, U32, B.Octets.at(o, i), 0))))))) : {Nat.add(ckp.ns(B.Octets.to_list(B.Octets.take(i, o))), Nat.add(U32.to_nat(_), ckp.ns(B.Octets.to_list(B.Octets.drop(1n+i, o))))) == Nat.add(ckp.ns(B.Octets.to_list(B.Octets.take(i, o))), Nat.add(U32.to_nat(C.AcpiChecksum.byte_for(i, o)), ckp.ns(B.Octets.to_list(B.Octets.drop(1n+i, o))))) : Nat}
242 {==}
243
244# w = S - o_i and b = 256 - w, modulo 256
245
246def ckp.e1g(+so: U32, +b: U32, +n: Nat, +ev: {U32.to_nat(so) == U.U32Nat.low(8n, n) : Nat}) -> {U.U32Nat.low(8n, Nat.add(U32.to_nat(U32.and(255, U32.sub(so, b))), U32.to_nat(b))) == U.U32Nat.low(8n, n) : Nat}:
247 %Equal.sym(Nat, U32.to_nat(U32.and(255, U32.sub(so, b))), U.U32Nat.low(8n, U32.to_nat(U32.sub(so, b))), ckp.am(U32.sub(so, b))) : {U.U32Nat.low(8n, Nat.add(_, U32.to_nat(b))) == U.U32Nat.low(8n, n) : Nat}
248 %ckp.l1(U32.to_nat(U32.sub(so, b)), U32.to_nat(b)) : {_ == U.U32Nat.low(8n, n) : Nat}
249 %Equal.sym(Nat, Nat.add(U32.to_nat(U32.sub(so, b)), U32.to_nat(b)), Nat.add(U32.to_nat(so), U.U32Nat.dbl(32n, U.U32Nat.bit(U32.is_lt(so, b)))), UL.u32_sub_wrap(so, b)) : {U.U32Nat.low(8n, _) == U.U32Nat.low(8n, n) : Nat}
250 %Equal.sym(Nat, U.U32Nat.low(8n, Nat.add(U32.to_nat(so), U.U32Nat.dbl(32n, U.U32Nat.bit(U32.is_lt(so, b))))), U.U32Nat.low(8n, U32.to_nat(so)), ckp.l2(U32.to_nat(so), U.U32Nat.bit(U32.is_lt(so, b)))) : {_ == U.U32Nat.low(8n, n) : Nat}
251 %Equal.sym(Nat, U32.to_nat(so), U.U32Nat.low(8n, n), ev) : {U.U32Nat.low(8n, _) == U.U32Nat.low(8n, n) : Nat}
252 ckp.ll(n)
253
254def ckp.e2g(+wu: U32) -> {U.U32Nat.low(8n, Nat.add(U32.to_nat(U32.and(255, U32.sub(256, wu))), U32.to_nat(wu))) == 0n : Nat}:
255 %Equal.sym(Nat, U32.to_nat(U32.and(255, U32.sub(256, wu))), U.U32Nat.low(8n, U32.to_nat(U32.sub(256, wu))), ckp.am(U32.sub(256, wu))) : {U.U32Nat.low(8n, Nat.add(_, U32.to_nat(wu))) == 0n : Nat}
256 %ckp.l1(U32.to_nat(U32.sub(256, wu)), U32.to_nat(wu)) : {_ == 0n : Nat}
257 %Equal.sym(Nat, Nat.add(U32.to_nat(U32.sub(256, wu)), U32.to_nat(wu)), Nat.add(U32.to_nat(256), U.U32Nat.dbl(32n, U.U32Nat.bit(U32.is_lt(256, wu)))), UL.u32_sub_wrap(256, wu)) : {U.U32Nat.low(8n, _) == 0n : Nat}
258 ckp.l2(U32.to_nat(256), U.U32Nat.bit(U32.is_lt(256, wu)))
259
260def ckp.e1(+i: Nat, +o: B.Octets, +h: {Nat.is_lt(i, B.Octets.len(o)) == True{} : Bool}) -> {U.U32Nat.low(8n, Nat.add(U32.to_nat(U32.and(255, U32.sub(C.AcpiChecksum.sum(o), U32.and(255, Maybe.default(&2, U32, B.Octets.at(o, i), 0))))), U32.to_nat(U32.and(255, Maybe.default(&2, U32, B.Octets.at(o, i), 0))))) == U.U32Nat.low(8n, Nat.add(ckp.ns(B.Octets.to_list(B.Octets.take(i, o))), Nat.add(U32.to_nat(U32.and(255, Maybe.default(&2, U32, B.Octets.at(o, i), 0))), ckp.ns(B.Octets.to_list(B.Octets.drop(1n+i, o)))))) : Nat}:
261 %ckp.split(i, o, h) : {U.U32Nat.low(8n, Nat.add(U32.to_nat(U32.and(255, U32.sub(C.AcpiChecksum.sum(o), U32.and(255, Maybe.default(&2, U32, B.Octets.at(o, i), 0))))), U32.to_nat(U32.and(255, Maybe.default(&2, U32, B.Octets.at(o, i), 0))))) == U.U32Nat.low(8n, _) : Nat}
262 ckp.e1g(C.AcpiChecksum.sum(o), U32.and(255, Maybe.default(&2, U32, B.Octets.at(o, i), 0)), ckp.ns(B.Octets.to_list(o)), ckp.sumv(o))
263
264def ckp.fixzero(+i: Nat, +o: B.Octets, +h: {Nat.is_lt(i, B.Octets.len(o)) == True{} : Bool}) -> {U32.to_nat(C.AcpiChecksum.sum(C.AcpiChecksum.fix(i, o))) == 0n : Nat}:
265 %Equal.sym(Nat, U32.to_nat(C.AcpiChecksum.sum(C.AcpiChecksum.fix(i, o))), U.U32Nat.low(8n, ckp.ns(B.Octets.to_list(C.AcpiChecksum.fix(i, o)))), ckp.sumv(C.AcpiChecksum.fix(i, o))) : {_ == 0n : Nat}
266 %Equal.sym(Nat, ckp.ns(B.Octets.to_list(C.AcpiChecksum.fix(i, o))), Nat.add(ckp.ns(B.Octets.to_list(B.Octets.take(i, o))), Nat.add(U32.to_nat(C.AcpiChecksum.byte_for(i, o)), ckp.ns(B.Octets.to_list(B.Octets.drop(1n+i, o))))), ckp.fixsum(i, o, h)) : {U.U32Nat.low(8n, _) == 0n : Nat}
267 ckp.zero(ckp.ns(B.Octets.to_list(B.Octets.take(i, o))), ckp.ns(B.Octets.to_list(B.Octets.drop(1n+i, o))), U32.to_nat(U32.and(255, Maybe.default(&2, U32, B.Octets.at(o, i), 0))), U32.to_nat(C.AcpiChecksum.byte_for(i, o)), U32.to_nat(U32.and(255, U32.sub(C.AcpiChecksum.sum(o), U32.and(255, Maybe.default(&2, U32, B.Octets.at(o, i), 0))))), ckp.e1(i, o, h), ckp.e2g(U32.and(255, U32.sub(C.AcpiChecksum.sum(o), U32.and(255, Maybe.default(&2, U32, B.Octets.at(o, i), 0))))))
268
269# The laws
270
271def Laws.fix_ok(i, o, h):
272 %Equal.sym(Bool, U32.is_eq(C.AcpiChecksum.sum(C.AcpiChecksum.fix(i, o)), 0), Nat.is_eq(U32.to_nat(C.AcpiChecksum.sum(C.AcpiChecksum.fix(i, o))), U32.to_nat(0)), UL.u32_eq_value(C.AcpiChecksum.sum(C.AcpiChecksum.fix(i, o)), 0)) : {_ == True{} : Bool}
273 %Equal.sym(Nat, U32.to_nat(C.AcpiChecksum.sum(C.AcpiChecksum.fix(i, o))), 0n, ckp.fixzero(i, o, h)) : {Nat.is_eq(_, U32.to_nat(0)) == True{} : Bool}
274 {==}
275
276def Laws.fix_example():
277 {==}