proofs/crypto/curve25519/canon.bend
bend-collections-laws-crypto@1.0.0.0 · 198 lines · 24 definitions
1import Base
2import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
3import bend-collections-laws-crypto@1.0.0.0/spec/crypto/curve25519/field.bend as FS
4import bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/field.bend as F
5import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
6import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
7import bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend as WD
8import bend-collections-laws-crypto@1.0.0.0/proofs/lib/arith.bend as AR
9import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32.bend as U
10import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
11import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as NR
12import bend-collections-laws-crypto@1.0.0.0/proofs/math/u64/u64div.bend as PD
13import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/num.bend as M
14import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend as LM
15import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/poly.bend as PL
16import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/fold.bend as FD
17import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/reduce.bend as RD
18import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/consts.bend as K
19import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/fieldops.bend as FO
20import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/cong.bend as G
21import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/freeze.bend as FZ
22import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/mulw.bend as MW
23
24
25
26
27def v(+x: U32) -> Nat:
28 U32.to_nat(x)
29
30
31
32def by_okb(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +x: List<&2, U32>, +cp: List<&2, U32>, +hx: {LM.okb(32n, x, 255n) == True{} : Bool}, +hk: {LM.okb(32n, cp, 128n) == True{} : Bool}, +hv: {K.valo(one, cp) == Nat.add(1n+pp, 38n) : Nat}, +b: Bool, +hb: {Nat.is_lt(v(LM.cc(F.carry(F.addl(x, cp), 0))), one) == b : Bool}) -> {LM.okb(32n, FZ.csg(x, cp), 255n) == True{} : Bool}:
33 match b:
34 case True{}:
35 %Equal.sym(List<&2, U32>, FZ.csg(x, cp), x, FZ.cs_zero(one, h1, x, cp, hx, hk, hb)) : {LM.okb(32n, _, 255n) == True{} : Bool}
36 hx
37 case False{}:
38 %Equal.sym(List<&2, U32>, FZ.csg(x, cp), LM.cl(F.carry(F.addl(x, cp), 0)), FZ.cs_one(one, h1, pp, hP, x, cp, hx, hk, hv, hb)) : {LM.okb(32n, _, 255n) == True{} : Bool}
39 FD.cr_okb(one, h1, F.addl(x, cp), FZ.ad_okb(one, h1, x, cp, hx, hk))
40
41def by_ceq(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +x: List<&2, U32>, +cp: List<&2, U32>, +hx: {LM.okb(32n, x, 255n) == True{} : Bool}, +hk: {LM.okb(32n, cp, 128n) == True{} : Bool}, +hv: {K.valo(one, cp) == Nat.add(1n+pp, 38n) : Nat}, +b: Bool, +hb: {Nat.is_lt(v(LM.cc(F.carry(F.addl(x, cp), 0))), one) == b : Bool}) -> G.ceq(pp, FS.value(FZ.csg(x, cp)), FS.value(x)):
42 match b:
43 case True{}:
44 %Equal.sym(List<&2, U32>, FZ.csg(x, cp), x, FZ.cs_zero(one, h1, x, cp, hx, hk, hb)) : G.ceq(pp, FS.value(_), FS.value(x))
45 G.c_refl(pp, FS.value(x))
46 case False{}:
47 +s = LM.cl(F.carry(F.addl(x, cp), 0))
48 %Equal.sym(List<&2, U32>, FZ.csg(x, cp), s, FZ.cs_one(one, h1, pp, hP, x, cp, hx, hk, hv, hb)) : G.ceq(pp, FS.value(_), FS.value(x))
49 +e1 = FZ.o_case(one, h1, pp, hP, x, cp, hx, hk, hv, hb)
50 +e2 = Equal.trans(Nat, Nat.add(Nat.mul(1n, 1n+pp), FS.value(s)), Nat.add(1n+pp, FS.value(s)), FS.value(x), M.cong_l(Nat.mul(1n, 1n+pp), 1n+pp, FS.value(s), AR.one_mul(1n+pp)), Equal.trans(Nat, Nat.add(1n+pp, FS.value(s)), Nat.add(FS.value(s), 1n+pp), FS.value(x), NA.add_comm(1n+pp, FS.value(s)), e1))
51 +e3 = NR.absorb(pp, 1n, FS.value(s))
52 G.c_sym(pp, FS.value(x), FS.value(s), G.c_trans(pp, FS.value(x), Nat.add(Nat.mul(1n, 1n+pp), FS.value(s)), FS.value(s), G.c_eq(pp, FS.value(x), Nat.add(Nat.mul(1n, 1n+pp), FS.value(s)), Equal.sym(Nat, Nat.add(Nat.mul(1n, 1n+pp), FS.value(s)), FS.value(x), e2)), e3))
53
54def by_lt(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +x: List<&2, U32>, +cp: List<&2, U32>, +hx: {LM.okb(32n, x, 255n) == True{} : Bool}, +hk: {LM.okb(32n, cp, 128n) == True{} : Bool}, +hv: {K.valo(one, cp) == Nat.add(1n+pp, 38n) : Nat}, +bB: Nat, +q: Nat, +hxB: {Nat.is_lt(FS.value(x), Nat.add(1n+pp, bB)) == True{} : Bool}, +hPQ: {Nat.is_le(1n+pp, q) == True{} : Bool}, +hBQ: {Nat.is_le(bB, q) == True{} : Bool}, +b: Bool, +hb: {Nat.is_lt(v(LM.cc(F.carry(F.addl(x, cp), 0))), one) == b : Bool}) -> {Nat.is_lt(FS.value(FZ.csg(x, cp)), q) == True{} : Bool}:
55 match b:
56 case True{}:
57 %Equal.sym(List<&2, U32>, FZ.csg(x, cp), x, FZ.cs_zero(one, h1, x, cp, hx, hk, hb)) : {Nat.is_lt(FS.value(_), q) == True{} : Bool}
58 N.lt_le_trans(FS.value(x), 1n+pp, q, FZ.z_case(one, h1, pp, hP, x, cp, hx, hk, hv, hb), hPQ)
59 case False{}:
60 +s = LM.cl(F.carry(F.addl(x, cp), 0))
61 %Equal.sym(List<&2, U32>, FZ.csg(x, cp), s, FZ.cs_one(one, h1, pp, hP, x, cp, hx, hk, hv, hb)) : {Nat.is_lt(FS.value(_), q) == True{} : Bool}
62 +e1 = FZ.o_case(one, h1, pp, hP, x, cp, hx, hk, hv, hb)
63 +l1 = L.subst(Nat, z => {Nat.is_lt(z, Nat.add(1n+pp, bB)) == True{} : Bool}, FS.value(x), Nat.add(FS.value(s), 1n+pp), Equal.sym(Nat, Nat.add(FS.value(s), 1n+pp), FS.value(x), e1), hxB)
64 +l2 = L.subst(Nat, z => {Nat.is_lt(Nat.add(FS.value(s), 1n+pp), z) == True{} : Bool}, Nat.add(1n+pp, bB), Nat.add(bB, 1n+pp), NA.add_comm(1n+pp, bB), l1)
65 N.lt_le_trans(FS.value(s), bB, q, RD.lt_cancel_r(FS.value(s), bB, 1n+pp, l2), hBQ)
66
67def cs_c(+one: Nat, +x: List<&2, U32>, +cp: List<&2, U32>) -> Nat:
68 v(LM.cc(F.carry(F.addl(x, cp), 0)))
69
70
71
72def csub_okb(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +x: List<&2, U32>, +hx: {LM.okb(32n, x, 255n) == True{} : Bool}) -> {LM.okb(32n, F.csub(x), 255n) == True{} : Bool}:
73 by_okb(one, h1, pp, hP, x, F.comp_p(), hx, FZ.comp_p_okb(), FZ.comp_p_val(one, h1, pp, hP), Nat.is_lt(cs_c(one, x, F.comp_p()), one), {==})
74
75def csub_ceq(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +x: List<&2, U32>, +hx: {LM.okb(32n, x, 255n) == True{} : Bool}) -> G.ceq(pp, FS.value(F.csub(x)), FS.value(x)):
76 by_ceq(one, h1, pp, hP, x, F.comp_p(), hx, FZ.comp_p_okb(), FZ.comp_p_val(one, h1, pp, hP), Nat.is_lt(cs_c(one, x, F.comp_p()), one), {==})
77
78def csub_lt(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +x: List<&2, U32>, +hx: {LM.okb(32n, x, 255n) == True{} : Bool}, +bB: Nat, +q: Nat, +hxB: {Nat.is_lt(FS.value(x), Nat.add(1n+pp, bB)) == True{} : Bool}, +hPQ: {Nat.is_le(1n+pp, q) == True{} : Bool}, +hBQ: {Nat.is_le(bB, q) == True{} : Bool}) -> {Nat.is_lt(FS.value(F.csub(x)), q) == True{} : Bool}:
79 by_lt(one, h1, pp, hP, x, F.comp_p(), hx, FZ.comp_p_okb(), FZ.comp_p_val(one, h1, pp, hP), bB, q, hxB, hPQ, hBQ, Nat.is_lt(cs_c(one, x, F.comp_p()), one), {==})
80
81def freeze_okb(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +x: List<&2, U32>, +hx: {LM.okb(32n, x, 255n) == True{} : Bool}) -> {LM.okb(32n, F.freeze(x), 255n) == True{} : Bool}:
82 csub_okb(one, h1, pp, hP, F.csub(x), csub_okb(one, h1, pp, hP, x, hx))
83
84def freeze_ceq(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +x: List<&2, U32>, +hx: {LM.okb(32n, x, 255n) == True{} : Bool}) -> G.ceq(pp, FS.value(F.freeze(x)), FS.value(x)):
85 G.c_trans(pp, FS.value(F.csub(F.csub(x))), FS.value(F.csub(x)), FS.value(x), csub_ceq(one, h1, pp, hP, F.csub(x), csub_okb(one, h1, pp, hP, x, hx)), csub_ceq(one, h1, pp, hP, x, hx))
86
87def freeze_lt(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +x: List<&2, U32>, +hx: {LM.okb(32n, x, 255n) == True{} : Bool}) -> {Nat.is_lt(FS.value(F.freeze(x)), 1n+pp) == True{} : Bool}:
88 +P = {1n+pp : Nat}
89 +t1 = RD.val_lt(one, h1, 32n, x, hx)
90 +t2 = L.subst(Nat, z => {Nat.is_lt(FS.value(x), z) == True{} : Bool}, LM.shn(32n, one), Nat.add(P, Nat.add(P, 38n)), Equal.trans(Nat, LM.shn(32n, one), Nat.add(Nat.add(P, P), 38n), Nat.add(P, Nat.add(P, 38n)), FZ.t_val(one, h1, pp, hP), NA.add_assoc(P, P, 38n)), t1)
91 +y1 = csub_lt(one, h1, pp, hP, x, hx, Nat.add(P, 38n), Nat.add(P, 38n), t2, N.le_add_right(P, 38n), N.le_refl(Nat.add(P, 38n)))
92 csub_lt(one, h1, pp, hP, F.csub(x), csub_okb(one, h1, pp, hP, x, hx), 38n, P, y1, N.le_refl(P), FZ.p38(one, h1, pp, hP))
93
94
95def freeze_val(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +x: List<&2, U32>, +hx: {LM.okb(32n, x, 255n) == True{} : Bool}) -> {FS.value(F.freeze(x)) == Nat.mod(FS.value(x), 1n+pp) : Nat}:
96 +r = FS.value(F.freeze(x))
97 +e1 = Equal.sym(Nat, Nat.mod(r, 1n+pp), r, NR.mod_of(0n, pp, r, freeze_lt(one, h1, pp, hP, x, hx)))
98 Equal.trans(Nat, r, Nat.mod(r, 1n+pp), Nat.mod(FS.value(x), 1n+pp), e1, freeze_ceq(one, h1, pp, hP, x, hx))
99
100
101
102def sumv(xs: List<&2, U32>) -> Nat:
103 match xs:
104 case Nil{}:
105 0n
106 case Con{x, xt}:
107 Nat.add(U32.to_nat(x), sumv(xt))
108
109def sum_v(+one: Nat, +h1: {one == 1n : Nat}, +n: Nat, +xs: List<&2, U32>, +acc: U32, +e: {LM.okb(n, xs, 255n) == True{} : Bool}, +ha: {Nat.is_lt(Nat.add(v(acc), PL.cbn(n, WD.sc(8n, one))), WD.sc(32n, one)) == True{} : Bool}) -> {v(F.sum_all(xs, acc)) == Nat.add(v(acc), sumv(xs)) : Nat}:
110 match n xs:
111 case 0n Nil{}:
112 Equal.sym(Nat, Nat.add(v(acc), 0n), v(acc), N.add_zero(v(acc)))
113 case 0n Con{y, yt}:
114 Empty.absurd({v(F.sum_all(Con{y, yt}, acc)) == Nat.add(v(acc), sumv(Con{y, yt})) : Nat}, L.false_true(e))
115 case 1n+m Nil{}:
116 Empty.absurd({v(acc) == Nat.add(v(acc), 0n) : Nat}, L.false_true(e))
117 case 1n+ +m Con{+y, +yt}:
118 +hy = N.le_trans(v(y), 255n, WD.sc(8n, one), LM.okb_head(m, y, yt, 255n, e), FD.le255(one, h1, 0n))
119 +b1 = N.le_lt_trans(Nat.add(v(acc), v(y)), Nat.add(v(acc), Nat.add(WD.sc(8n, one), PL.cbn(m, WD.sc(8n, one)))), WD.sc(32n, one), N.le_add_left(v(y), Nat.add(WD.sc(8n, one), PL.cbn(m, WD.sc(8n, one))), v(acc), N.le_trans(v(y), WD.sc(8n, one), Nat.add(WD.sc(8n, one), PL.cbn(m, WD.sc(8n, one))), hy, N.le_add_right(WD.sc(8n, one), PL.cbn(m, WD.sc(8n, one))))), ha)
120 +ea = LM.add_v(one, h1, acc, y, b1)
121 +b2a = M.le_add_r(Nat.add(v(acc), v(y)), Nat.add(v(acc), WD.sc(8n, one)), PL.cbn(m, WD.sc(8n, one)), N.le_add_left(v(y), WD.sc(8n, one), v(acc), hy))
122 +b2b = L.subst(Nat, z => {Nat.is_le(Nat.add(Nat.add(v(acc), v(y)), PL.cbn(m, WD.sc(8n, one))), z) == True{} : Bool}, Nat.add(Nat.add(v(acc), WD.sc(8n, one)), PL.cbn(m, WD.sc(8n, one))), Nat.add(v(acc), Nat.add(WD.sc(8n, one), PL.cbn(m, WD.sc(8n, one)))), NA.add_assoc(v(acc), WD.sc(8n, one), PL.cbn(m, WD.sc(8n, one))), b2a)
123 +b2 = L.subst(Nat, z => {Nat.is_lt(Nat.add(z, PL.cbn(m, WD.sc(8n, one))), WD.sc(32n, one)) == True{} : Bool}, Nat.add(v(acc), v(y)), v(U32.add(acc, y)), Equal.sym(Nat, v(U32.add(acc, y)), Nat.add(v(acc), v(y)), ea), N.le_lt_trans(Nat.add(Nat.add(v(acc), v(y)), PL.cbn(m, WD.sc(8n, one))), Nat.add(v(acc), Nat.add(WD.sc(8n, one), PL.cbn(m, WD.sc(8n, one)))), WD.sc(32n, one), b2b, ha))
124 +ih = sum_v(one, h1, m, yt, U32.add(acc, y), LM.okb_tail(m, y, yt, 255n, e), b2)
125 Equal.trans(Nat, v(F.sum_all(yt, U32.add(acc, y))), Nat.add(v(U32.add(acc, y)), sumv(yt)), Nat.add(v(acc), Nat.add(v(y), sumv(yt))), ih, Equal.trans(Nat, Nat.add(v(U32.add(acc, y)), sumv(yt)), Nat.add(Nat.add(v(acc), v(y)), sumv(yt)), Nat.add(v(acc), Nat.add(v(y), sumv(yt))), M.cong_l(v(U32.add(acc, y)), Nat.add(v(acc), v(y)), sumv(yt), ea), NA.add_assoc(v(acc), v(y), sumv(yt))))
126
127def iz_add(+a: Nat, +b: Nat) -> {Nat.is_eq(Nat.add(a, b), 0n) == Bool.and(Nat.is_eq(a, 0n), Nat.is_eq(b, 0n)) : Bool}:
128 match a:
129 case 0n:
130 {==}
131 case 1n+q:
132 {==}
133
134def iz_dbl(+x: Nat) -> {Nat.is_eq(Nat.double(x), 0n) == Nat.is_eq(x, 0n) : Bool}:
135 match x:
136 case 0n:
137 {==}
138 case 1n+q:
139 {==}
140
141def iz_sc(+k: Nat, +x: Nat) -> {Nat.is_eq(WD.sc(k, x), 0n) == Nat.is_eq(x, 0n) : Bool}:
142 match k:
143 case 0n:
144 {==}
145 case 1n+ +q:
146 Equal.trans(Bool, Nat.is_eq(Nat.double(WD.sc(q, x)), 0n), Nat.is_eq(WD.sc(q, x), 0n), Nat.is_eq(x, 0n), iz_dbl(WD.sc(q, x)), iz_sc(q, x))
147
148def iz_sum(+xs: List<&2, U32>) -> {Nat.is_eq(sumv(xs), 0n) == Nat.is_eq(FS.value(xs), 0n) : Bool}:
149 match xs:
150 case Nil{}:
151 {==}
152 case Con{+y, +yt}:
153 +e1 = iz_add(v(y), sumv(yt))
154 +e2 = iz_add(v(y), C.shift(8n, FS.value(yt)))
155 +e3 = Equal.trans(Bool, Nat.is_eq(C.shift(8n, FS.value(yt)), 0n), Nat.is_eq(FS.value(yt), 0n), Nat.is_eq(sumv(yt), 0n), iz_sc(8n, FS.value(yt)), Equal.sym(Bool, Nat.is_eq(sumv(yt), 0n), Nat.is_eq(FS.value(yt), 0n), iz_sum(yt)))
156 Equal.trans(Bool, Nat.is_eq(Nat.add(v(y), sumv(yt)), 0n), Bool.and(Nat.is_eq(v(y), 0n), Nat.is_eq(sumv(yt), 0n)), Nat.is_eq(Nat.add(v(y), C.shift(8n, FS.value(yt))), 0n), e1, Equal.trans(Bool, Bool.and(Nat.is_eq(v(y), 0n), Nat.is_eq(sumv(yt), 0n)), Bool.and(Nat.is_eq(v(y), 0n), Nat.is_eq(C.shift(8n, FS.value(yt)), 0n)), Nat.is_eq(Nat.add(v(y), C.shift(8n, FS.value(yt))), 0n), Equal.cong(Bool, Bool, z => Bool.and(Nat.is_eq(v(y), 0n), z), Nat.is_eq(sumv(yt), 0n), Nat.is_eq(C.shift(8n, FS.value(yt)), 0n), Equal.sym(Bool, Nat.is_eq(C.shift(8n, FS.value(yt)), 0n), Nat.is_eq(sumv(yt), 0n), e3)), Equal.sym(Bool, Nat.is_eq(Nat.add(v(y), C.shift(8n, FS.value(yt))), 0n), Bool.and(Nat.is_eq(v(y), 0n), Nat.is_eq(C.shift(8n, FS.value(yt)), 0n)), e2)))
157
158def u32_iz(+a: U32) -> {U32.is_eq(a, 0) == Nat.is_eq(v(a), 0n) : Bool}:
159 Equal.cong(Cmp, Bool, c => Cmp.is_eq(c), U32.cmp(a, 0), Nat.cmp(v(a), 0n), U.u32_cmp(a, 0))
160
161def cb32_lt(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_lt(Nat.add(v(0), PL.cbn(32n, WD.sc(8n, one))), WD.sc(32n, one)) == True{} : Bool}:
162 +b = MW.cbn_pow(5n, WD.sc(8n, one))
163 L.subst(Nat, z => {Nat.is_lt(z, WD.sc(32n, one)) == True{} : Bool}, WD.sc(5n, WD.sc(8n, one)), PL.cbn(32n, WD.sc(8n, one)), Equal.sym(Nat, PL.cbn(32n, WD.sc(8n, one)), WD.sc(5n, WD.sc(8n, one)), b), LM.sc_lt(18n, 13n, one, h1))
164
165def is_zero_val(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +x: List<&2, U32>, +hx: {LM.okb(32n, x, 255n) == True{} : Bool}) -> {F.is_zero(x) == Nat.is_eq(Nat.mod(FS.value(x), 1n+pp), 0n) : Bool}:
166 +y = F.freeze(x)
167 +hy = freeze_okb(one, h1, pp, hP, x, hx)
168 +e1 = u32_iz(F.sum_all(y, 0))
169 +e2 = Equal.cong(Nat, Bool, z => Nat.is_eq(z, 0n), v(F.sum_all(y, 0)), sumv(y), sum_v(one, h1, 32n, y, 0, hy, cb32_lt(one, h1)))
170 +e3 = iz_sum(y)
171 +e4 = Equal.cong(Nat, Bool, z => Nat.is_eq(z, 0n), FS.value(y), Nat.mod(FS.value(x), 1n+pp), freeze_val(one, h1, pp, hP, x, hx))
172 Equal.trans(Bool, U32.is_eq(F.sum_all(y, 0), 0), Nat.is_eq(v(F.sum_all(y, 0)), 0n), Nat.is_eq(Nat.mod(FS.value(x), 1n+pp), 0n), e1, Equal.trans(Bool, Nat.is_eq(v(F.sum_all(y, 0)), 0n), Nat.is_eq(sumv(y), 0n), Nat.is_eq(Nat.mod(FS.value(x), 1n+pp), 0n), e2, Equal.trans(Bool, Nat.is_eq(sumv(y), 0n), Nat.is_eq(FS.value(y), 0n), Nat.is_eq(Nat.mod(FS.value(x), 1n+pp), 0n), e3, e4)))
173
174
175
176def and1(+one: Nat, +h1: {one == 1n : Nat}, +l: U32) -> {v(U32.and(l, 1)) == Nat.mod(v(l), 2n) : Nat}:
177 +a = PD.and32(1n, l, 1, {==})
178 +b = PD.and32_lt(1n, one, h1, l, 1, {==})
179 +hp = PD.hp32(1n, l)
180 +b2 = L.subst(Nat, o => {Nat.is_lt(v(U32.and(l, 1)), WD.sc(1n, o)) == True{} : Bool}, one, 1n, h1, b)
181 +e1 = Equal.trans(Nat, v(l), Nat.add(v(U32.and(l, 1)), WD.sc(1n, hp)), Nat.add(Nat.mul(hp, 2n), v(U32.and(l, 1))), a, Equal.trans(Nat, Nat.add(v(U32.and(l, 1)), WD.sc(1n, hp)), Nat.add(WD.sc(1n, hp), v(U32.and(l, 1))), Nat.add(Nat.mul(hp, 2n), v(U32.and(l, 1))), NA.add_comm(v(U32.and(l, 1)), WD.sc(1n, hp)), M.cong_l(WD.sc(1n, hp), Nat.mul(hp, 2n), v(U32.and(l, 1)), Equal.trans(Nat, Nat.double(hp), Nat.mul(2n, hp), Nat.mul(hp, 2n), NA.double_mul(hp), NA.mul_comm(2n, hp)))))
182 Equal.sym(Nat, Nat.mod(v(l), 2n), v(U32.and(l, 1)), Equal.trans(Nat, Nat.mod(v(l), 2n), Nat.mod(Nat.add(Nat.mul(hp, 2n), v(U32.and(l, 1))), 2n), v(U32.and(l, 1)), M.cong_mod(2n, v(l), Nat.add(Nat.mul(hp, 2n), v(U32.and(l, 1))), e1), NR.mod_of(hp, 1n, v(U32.and(l, 1)), b2)))
183
184
185def low_bit_val(+one: Nat, +h1: {one == 1n : Nat}, +ys: List<&2, U32>, +e: {LM.okb(32n, ys, 255n) == True{} : Bool}) -> {v(F.low_bit(ys)) == Nat.mod(FS.value(ys), 2n) : Nat}:
186 match ys:
187 case Nil{}:
188 Empty.absurd({0n == Nat.mod(0n, 2n) : Nat}, L.false_true(e))
189 case Con{+l, +t}:
190 +V = FS.value(t)
191 +q = WD.sc(7n, V)
192 +e1 = Equal.trans(Nat, Nat.add(v(l), C.shift(8n, V)), Nat.add(C.shift(8n, V), v(l)), Nat.add(Nat.mul(q, 2n), v(l)), NA.add_comm(v(l), C.shift(8n, V)), M.cong_l(C.shift(8n, V), Nat.mul(q, 2n), v(l), Equal.trans(Nat, Nat.double(q), Nat.mul(2n, q), Nat.mul(q, 2n), NA.double_mul(q), NA.mul_comm(2n, q))))
193 +e2 = Equal.trans(Nat, Nat.mod(Nat.add(v(l), C.shift(8n, V)), 2n), Nat.mod(Nat.add(Nat.mul(q, 2n), v(l)), 2n), Nat.mod(v(l), 2n), M.cong_mod(2n, Nat.add(v(l), C.shift(8n, V)), Nat.add(Nat.mul(q, 2n), v(l)), e1), NR.absorb(1n, q, v(l)))
194 Equal.trans(Nat, v(U32.and(l, 1)), Nat.mod(v(l), 2n), Nat.mod(Nat.add(v(l), C.shift(8n, V)), 2n), and1(one, h1, l), Equal.sym(Nat, Nat.mod(Nat.add(v(l), C.shift(8n, V)), 2n), Nat.mod(v(l), 2n), e2))
195
196def parity_val(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +x: List<&2, U32>, +hx: {LM.okb(32n, x, 255n) == True{} : Bool}) -> {v(F.parity(x)) == Nat.mod(Nat.mod(FS.value(x), 1n+pp), 2n) : Nat}:
197 +y = F.freeze(x)
198 Equal.trans(Nat, v(F.low_bit(y)), Nat.mod(FS.value(y), 2n), Nat.mod(Nat.mod(FS.value(x), 1n+pp), 2n), low_bit_val(one, h1, y, freeze_okb(one, h1, pp, hP, x, hx)), M.cong_mod(2n, FS.value(y), Nat.mod(FS.value(x), 1n+pp), freeze_val(one, h1, pp, hP, x, hx)))