proofs/crypto/secp256k1/pver.bend

bend-collections-laws-crypto@1.0.0.0 · 129 lines · 9 definitions

1# GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/pver.src; edit the .src
2import Base
3import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend as FS
4import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend as CV
5import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/ecdsa.bend as ES
6import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/scalar.bend as S
7import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/bytes.bend as B
8import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/point.bend as P
9import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/ecdsa.bend as E
10import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as Lg
11import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/scalarops.bend as SO
12import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/scalarpow.bend as SP
13import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/fwrap.bend as FW
14import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bytes.bend as BY
15import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/point.bend as PT
16import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/sel.bend as SL
17import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pmul.bend as PM
18import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/paff.bend as PA
19import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/penc.bend as PE
20import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pdec.bend as PD
21import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/blist.bend as BL
22import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pscal.bend as SQ
23
24# ECDSA verification of src/crypto/secp256k1/ecdsa.bend (verify and
25# verify_strict) against spec/crypto/secp256k1/ecdsa.bend.
26
27def aff_x_v(+one: Nat, a: P.Affine) -> {FS.value(one, P.aff_x(a)) == CV.aff_x(PA.av(one, a)) : Nat}:
28  match a:
29    case P.Affine{x, y}:
30      {==}
31
32def aff_x_l(+one: Nat, a: P.Affine, +ha: {PA.ared(one, a) == True{} : Bool}) -> {FS.limbs16(one, 16n, P.aff_x(a)) == True{} : Bool}:
33  match a:
34    case P.Affine{+x, +y}:
35      SL.l16(one, x, Lg.and_left(PT.red(one, x), PT.red(one, y), ha))
36
37# R not the point at infinity and x(R) mod n = r
38def vfin(+one: Nat, +h1: {one == 1n : Nat}, +rr: P.Point, +hrr: {PT.pred(one, rr) == True{} : Bool}, +r: List<&2, Nat>, +hr: {FS.reduced(one, FS.order(one), r) == True{} : Bool}) -> {Bool.and(Bool.not(P.is_inf(rr)), S.eq(S.reduce(P.aff_x(P.to_affine(rr))), r)) == Bool.and(Bool.not(CV.is_inf(PT.pv(one, rr))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), PT.pv(one, rr))), FS.order(one)), FS.value(one, r))) : Bool}:
39  +ha = PA.aff_r(one, h1, rr, hrr)
40  +hx = aff_x_l(one, P.to_affine(rr), ha)
41  %Equal.sym(Bool, P.is_inf(rr), CV.is_inf(PT.pv(one, rr)), PA.is_inf_v(one, h1, rr)) : {Bool.and(Bool.not(_), S.eq(S.reduce(P.aff_x(P.to_affine(rr))), r)) == Bool.and(Bool.not(CV.is_inf(PT.pv(one, rr))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), PT.pv(one, rr))), FS.order(one)), FS.value(one, r))) : Bool}
42  %Equal.sym(Bool, S.eq(S.reduce(P.aff_x(P.to_affine(rr))), r), Nat.is_eq(FS.value(one, S.reduce(P.aff_x(P.to_affine(rr)))), FS.value(one, r)), FW.eq_s(one, h1, S.reduce(P.aff_x(P.to_affine(rr))), r, SL.sl16(one, S.reduce(P.aff_x(P.to_affine(rr))), SQ.sred_r(one, h1, P.aff_x(P.to_affine(rr)), hx)), SL.sl16(one, r, hr))) : {Bool.and(Bool.not(CV.is_inf(PT.pv(one, rr))), _) == Bool.and(Bool.not(CV.is_inf(PT.pv(one, rr))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), PT.pv(one, rr))), FS.order(one)), FS.value(one, r))) : Bool}
43  %Equal.sym(Nat, FS.value(one, S.reduce(P.aff_x(P.to_affine(rr)))), Nat.mod(FS.value(one, P.aff_x(P.to_affine(rr))), FS.order(one)), SQ.sred_v(one, h1, P.aff_x(P.to_affine(rr)), hx)) : {Bool.and(Bool.not(CV.is_inf(PT.pv(one, rr))), Nat.is_eq(_, FS.value(one, r))) == Bool.and(Bool.not(CV.is_inf(PT.pv(one, rr))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), PT.pv(one, rr))), FS.order(one)), FS.value(one, r))) : Bool}
44  %Equal.sym(Nat, FS.value(one, P.aff_x(P.to_affine(rr))), CV.aff_x(PA.av(one, P.to_affine(rr))), aff_x_v(one, P.to_affine(rr))) : {Bool.and(Bool.not(CV.is_inf(PT.pv(one, rr))), Nat.is_eq(Nat.mod(_, FS.order(one)), FS.value(one, r))) == Bool.and(Bool.not(CV.is_inf(PT.pv(one, rr))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), PT.pv(one, rr))), FS.order(one)), FS.value(one, r))) : Bool}
45  %Equal.sym(CV.SAffine, PA.av(one, P.to_affine(rr)), CV.to_affine(FS.prime(one), PT.pv(one, rr)), PA.aff_v(one, h1, rr, hrr)) : {Bool.and(Bool.not(CV.is_inf(PT.pv(one, rr))), Nat.is_eq(Nat.mod(CV.aff_x(_), FS.order(one)), FS.value(one, r))) == Bool.and(Bool.not(CV.is_inf(PT.pv(one, rr))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), PT.pv(one, rr))), FS.order(one)), FS.value(one, r))) : Bool}
46  {==}
47
48def vrs(+one: Nat, +h1: {one == 1n : Nat}, +q: P.Point, +hq: {PT.pred(one, q) == True{} : Bool}, +z: List<&2, Nat>, +hz: {FS.reduced(one, FS.order(one), z) == True{} : Bool}, +r: List<&2, Nat>, +hr: {FS.reduced(one, FS.order(one), r) == True{} : Bool}, +s: List<&2, Nat>, +hs: {FS.reduced(one, FS.order(one), s) == True{} : Bool}) -> {E.verify_rs(q, z, r, s) == ES.verify_rs(one, PT.pv(one, q), FS.value(one, z), FS.value(one, r), FS.value(one, s)) : Bool}:
49  +hw = SP.inv_r(one, h1, s, hs)
50  +hu1 = SO.mul_r(one, h1, z, S.inv(s), hz, hw)
51  +hu2 = SO.mul_r(one, h1, r, S.inv(s), hr, hw)
52  +hg = PA.g_r(one, h1)
53  +hp1 = PM.mul_r(one, h1, S.mul(z, S.inv(s)), P.g(), SL.sl16(one, S.mul(z, S.inv(s)), hu1), hg)
54  +hp2 = PM.mul_r(one, h1, S.mul(r, S.inv(s)), q, SL.sl16(one, S.mul(r, S.inv(s)), hu2), hq)
55  +hrr = PT.padd_r(one, h1, P.mul(S.mul(z, S.inv(s)), P.g()), P.mul(S.mul(r, S.inv(s)), q), hp1, hp2)
56  %Equal.sym(Bool, Bool.and(Bool.not(P.is_inf(P.add(P.mul(S.mul(z, S.inv(s)), P.g()), P.mul(S.mul(r, S.inv(s)), q)))), S.eq(S.reduce(P.aff_x(P.to_affine(P.add(P.mul(S.mul(z, S.inv(s)), P.g()), P.mul(S.mul(r, S.inv(s)), q))))), r)), Bool.and(Bool.not(CV.is_inf(PT.pv(one, P.add(P.mul(S.mul(z, S.inv(s)), P.g()), P.mul(S.mul(r, S.inv(s)), q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), PT.pv(one, P.add(P.mul(S.mul(z, S.inv(s)), P.g()), P.mul(S.mul(r, S.inv(s)), q))))), FS.order(one)), FS.value(one, r))), vfin(one, h1, P.add(P.mul(S.mul(z, S.inv(s)), P.g()), P.mul(S.mul(r, S.inv(s)), q)), hrr, r, hr)) : {_ == Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) : Bool}
57  %Equal.sym(CV.SPoint, PT.pv(one, P.add(P.mul(S.mul(z, S.inv(s)), P.g()), P.mul(S.mul(r, S.inv(s)), q))), CV.padd(FS.prime(one), PT.pv(one, P.mul(S.mul(z, S.inv(s)), P.g())), PT.pv(one, P.mul(S.mul(r, S.inv(s)), q))), PT.padd_v(one, h1, P.mul(S.mul(z, S.inv(s)), P.g()), P.mul(S.mul(r, S.inv(s)), q), hp1, hp2)) : {Bool.and(Bool.not(CV.is_inf(_)), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), PT.pv(one, P.add(P.mul(S.mul(z, S.inv(s)), P.g()), P.mul(S.mul(r, S.inv(s)), q))))), FS.order(one)), FS.value(one, r))) == Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) : Bool}
58  %Equal.sym(CV.SPoint, PT.pv(one, P.add(P.mul(S.mul(z, S.inv(s)), P.g()), P.mul(S.mul(r, S.inv(s)), q))), CV.padd(FS.prime(one), PT.pv(one, P.mul(S.mul(z, S.inv(s)), P.g())), PT.pv(one, P.mul(S.mul(r, S.inv(s)), q))), PT.padd_v(one, h1, P.mul(S.mul(z, S.inv(s)), P.g()), P.mul(S.mul(r, S.inv(s)), q), hp1, hp2)) : {Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), PT.pv(one, P.mul(S.mul(z, S.inv(s)), P.g())), PT.pv(one, P.mul(S.mul(r, S.inv(s)), q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), _)), FS.order(one)), FS.value(one, r))) == Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) : Bool}
59  %Equal.sym(CV.SPoint, PT.pv(one, P.mul(S.mul(z, S.inv(s)), P.g())), CV.pmul(FS.prime(one), FS.value(one, S.mul(z, S.inv(s))), PT.pv(one, P.g())), PM.mul_v(one, h1, S.mul(z, S.inv(s)), P.g(), SL.sl16(one, S.mul(z, S.inv(s)), hu1), hg)) : {Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), _, PT.pv(one, P.mul(S.mul(r, S.inv(s)), q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), PT.pv(one, P.mul(S.mul(z, S.inv(s)), P.g())), PT.pv(one, P.mul(S.mul(r, S.inv(s)), q))))), FS.order(one)), FS.value(one, r))) == Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) : Bool}
60  %Equal.sym(CV.SPoint, PT.pv(one, P.mul(S.mul(z, S.inv(s)), P.g())), CV.pmul(FS.prime(one), FS.value(one, S.mul(z, S.inv(s))), PT.pv(one, P.g())), PM.mul_v(one, h1, S.mul(z, S.inv(s)), P.g(), SL.sl16(one, S.mul(z, S.inv(s)), hu1), hg)) : {Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, S.mul(z, S.inv(s))), PT.pv(one, P.g())), PT.pv(one, P.mul(S.mul(r, S.inv(s)), q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), _, PT.pv(one, P.mul(S.mul(r, S.inv(s)), q))))), FS.order(one)), FS.value(one, r))) == Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) : Bool}
61  %Equal.sym(CV.SPoint, PT.pv(one, P.mul(S.mul(r, S.inv(s)), q)), CV.pmul(FS.prime(one), FS.value(one, S.mul(r, S.inv(s))), PT.pv(one, q)), PM.mul_v(one, h1, S.mul(r, S.inv(s)), q, SL.sl16(one, S.mul(r, S.inv(s)), hu2), hq)) : {Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, S.mul(z, S.inv(s))), PT.pv(one, P.g())), _))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, S.mul(z, S.inv(s))), PT.pv(one, P.g())), PT.pv(one, P.mul(S.mul(r, S.inv(s)), q))))), FS.order(one)), FS.value(one, r))) == Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) : Bool}
62  %Equal.sym(CV.SPoint, PT.pv(one, P.mul(S.mul(r, S.inv(s)), q)), CV.pmul(FS.prime(one), FS.value(one, S.mul(r, S.inv(s))), PT.pv(one, q)), PM.mul_v(one, h1, S.mul(r, S.inv(s)), q, SL.sl16(one, S.mul(r, S.inv(s)), hu2), hq)) : {Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, S.mul(z, S.inv(s))), PT.pv(one, P.g())), CV.pmul(FS.prime(one), FS.value(one, S.mul(r, S.inv(s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, S.mul(z, S.inv(s))), PT.pv(one, P.g())), _))), FS.order(one)), FS.value(one, r))) == Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) : Bool}
63  %Equal.sym(CV.SPoint, PT.pv(one, P.g()), CV.g(one), PA.g_v(one, h1)) : {Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, S.mul(z, S.inv(s))), _), CV.pmul(FS.prime(one), FS.value(one, S.mul(r, S.inv(s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, S.mul(z, S.inv(s))), PT.pv(one, P.g())), CV.pmul(FS.prime(one), FS.value(one, S.mul(r, S.inv(s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) == Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) : Bool}
64  %Equal.sym(CV.SPoint, PT.pv(one, P.g()), CV.g(one), PA.g_v(one, h1)) : {Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, S.mul(z, S.inv(s))), CV.g(one)), CV.pmul(FS.prime(one), FS.value(one, S.mul(r, S.inv(s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, S.mul(z, S.inv(s))), _), CV.pmul(FS.prime(one), FS.value(one, S.mul(r, S.inv(s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) == Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) : Bool}
65  %Equal.sym(Nat, FS.value(one, S.mul(z, S.inv(s))), FS.mmul(FS.order(one), FS.value(one, z), FS.value(one, S.inv(s))), SO.mul_v(one, h1, z, S.inv(s), hz, hw)) : {Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), _, CV.g(one)), CV.pmul(FS.prime(one), FS.value(one, S.mul(r, S.inv(s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, S.mul(z, S.inv(s))), CV.g(one)), CV.pmul(FS.prime(one), FS.value(one, S.mul(r, S.inv(s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) == Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) : Bool}
66  %Equal.sym(Nat, FS.value(one, S.mul(z, S.inv(s))), FS.mmul(FS.order(one), FS.value(one, z), FS.value(one, S.inv(s))), SO.mul_v(one, h1, z, S.inv(s), hz, hw)) : {Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.value(one, S.inv(s))), CV.g(one)), CV.pmul(FS.prime(one), FS.value(one, S.mul(r, S.inv(s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), _, CV.g(one)), CV.pmul(FS.prime(one), FS.value(one, S.mul(r, S.inv(s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) == Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) : Bool}
67  %Equal.sym(Nat, FS.value(one, S.mul(r, S.inv(s))), FS.mmul(FS.order(one), FS.value(one, r), FS.value(one, S.inv(s))), SO.mul_v(one, h1, r, S.inv(s), hr, hw)) : {Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.value(one, S.inv(s))), CV.g(one)), CV.pmul(FS.prime(one), _, PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.value(one, S.inv(s))), CV.g(one)), CV.pmul(FS.prime(one), FS.value(one, S.mul(r, S.inv(s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) == Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) : Bool}
68  %Equal.sym(Nat, FS.value(one, S.mul(r, S.inv(s))), FS.mmul(FS.order(one), FS.value(one, r), FS.value(one, S.inv(s))), SO.mul_v(one, h1, r, S.inv(s), hr, hw)) : {Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.value(one, S.inv(s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.value(one, S.inv(s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.value(one, S.inv(s))), CV.g(one)), CV.pmul(FS.prime(one), _, PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) == Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) : Bool}
69  %Equal.sym(Nat, FS.value(one, S.inv(s)), FS.minv(FS.order(one), FS.value(one, s)), SP.inv_v(one, h1, s, hs)) : {Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), _), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.value(one, S.inv(s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.value(one, S.inv(s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.value(one, S.inv(s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) == Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) : Bool}
70  %Equal.sym(Nat, FS.value(one, S.inv(s)), FS.minv(FS.order(one), FS.value(one, s)), SP.inv_v(one, h1, s, hs)) : {Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), _), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.value(one, S.inv(s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.value(one, S.inv(s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) == Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) : Bool}
71  %Equal.sym(Nat, FS.value(one, S.inv(s)), FS.minv(FS.order(one), FS.value(one, s)), SP.inv_v(one, h1, s, hs)) : {Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), _), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.value(one, S.inv(s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) == Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) : Bool}
72  %Equal.sym(Nat, FS.value(one, S.inv(s)), FS.minv(FS.order(one), FS.value(one, s)), SP.inv_v(one, h1, s, hs)) : {Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), _), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) == Bool.and(Bool.not(CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, z), FS.minv(FS.order(one), FS.value(one, s))), CV.g(one)), CV.pmul(FS.prime(one), FS.mmul(FS.order(one), FS.value(one, r), FS.minv(FS.order(one), FS.value(one, s))), PT.pv(one, q))))), FS.order(one)), FS.value(one, r))) : Bool}
73  {==}
74
75# a valid scalar (1 <= x < n) is reduced
76def ok_red(+one: Nat, +x: List<&2, Nat>, +hl: {FS.limbs16(one, 16n, x) == True{} : Bool}, +h: {ES.scalar_ok(one, FS.value(one, x)) == True{} : Bool}) -> {FS.reduced(one, FS.order(one), x) == True{} : Bool}:
77  Lg.and_intro(FS.limbs16(one, 16n, x), Nat.is_lt(FS.value(one, x), FS.order(one)), hl, Lg.and_right(Bool.not(Nat.is_eq(FS.value(one, x), 0n)), Nat.is_lt(FS.value(one, x), FS.order(one)), h))
78
79def vok(+one: Nat, +h1: {one == 1n : Nat}, +q: P.Point, +hq: {PT.pred(one, q) == True{} : Bool}, +z: List<&2, Nat>, +hz: {FS.reduced(one, FS.order(one), z) == True{} : Bool}, +r: List<&2, Nat>, +hlr: {FS.limbs16(one, 16n, r) == True{} : Bool}, +s: List<&2, Nat>, +hls: {FS.limbs16(one, 16n, s) == True{} : Bool}, a: Bool, b: Bool, c: Bool, +ha: {ES.scalar_ok(one, FS.value(one, r)) == a : Bool}, +hb: {ES.scalar_ok(one, FS.value(one, s)) == b : Bool}) -> {E.verify_ok(q, z, r, s, Bool.and(Bool.and(a, b), c)) == ES.verify_ok(one, PT.pv(one, q), FS.value(one, z), FS.value(one, r), FS.value(one, s), Bool.and(Bool.and(a, b), c)) : Bool}:
80  match a b c:
81    case True{} True{} True{}:
82      vrs(one, h1, q, hq, z, hz, r, ok_red(one, r, hlr, ha), s, ok_red(one, s, hls, hb))
83    case True{} True{} False{}:
84      {==}
85    case True{} False{} _:
86      {==}
87    case False{} _ _:
88      {==}
89
90def vq(+one: Nat, +h1: {one == 1n : Nat}, +h: List<&2, U32>, +hh: {B.has_len(32n, h) == True{} : Bool}, +sig: List<&2, U32>, +hsig: {B.has_len(64n, sig) == True{} : Bool}, strict: Bool, m: Maybe<&2, P.Point>, +hm: {PE.mpred(one, m) == True{} : Bool}) -> {E.verify_q(h, sig, strict, m) == ES.verify_q(one, h, sig, strict, PE.mpv(one, m)) : Bool}:
91  match m:
92    case None{}:
93      {==}
94    case Some{+q}:
95      +r = B.of_be(B.prefix(32n, sig))
96      +s = B.of_be(B.suffix(32n, sig))
97      +hlr = BY.of_be_limbs(one, h1, B.prefix(32n, sig), BL.pl32(sig, hsig))
98      +hls = BY.of_be_limbs(one, h1, B.suffix(32n, sig), BL.sl32(sig, hsig))
99      %Equal.sym(Bool, E.scalar_ok(B.of_be(B.prefix(32n, sig))), ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), SQ.scalar_ok_v(one, h1, B.of_be(B.prefix(32n, sig)))) : {E.verify_ok(q, E.hash_scalar(h), B.of_be(B.prefix(32n, sig)), B.of_be(B.suffix(32n, sig)), Bool.and(Bool.and(_, E.scalar_ok(B.of_be(B.suffix(32n, sig)))), Bool.or(Bool.not(strict), Bool.not(S.is_high(B.of_be(B.suffix(32n, sig))))))) == ES.verify_ok(one, PT.pv(one, q), ES.hash_scalar(one, h), CV.os2ip(CV.first(32n, sig)), CV.os2ip(CV.after(32n, sig)), Bool.and(Bool.and(ES.scalar_ok(one, CV.os2ip(CV.first(32n, sig))), ES.scalar_ok(one, CV.os2ip(CV.after(32n, sig)))), Bool.or(Bool.not(strict), Bool.not(Nat.is_lt(FS.order(one), Nat.double(CV.os2ip(CV.after(32n, sig)))))))) : Bool}
100      %Equal.sym(Bool, E.scalar_ok(B.of_be(B.suffix(32n, sig))), ES.scalar_ok(one, FS.value(one, B.of_be(B.suffix(32n, sig)))), SQ.scalar_ok_v(one, h1, B.of_be(B.suffix(32n, sig)))) : {E.verify_ok(q, E.hash_scalar(h), B.of_be(B.prefix(32n, sig)), B.of_be(B.suffix(32n, sig)), Bool.and(Bool.and(ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), _), Bool.or(Bool.not(strict), Bool.not(S.is_high(B.of_be(B.suffix(32n, sig))))))) == ES.verify_ok(one, PT.pv(one, q), ES.hash_scalar(one, h), CV.os2ip(CV.first(32n, sig)), CV.os2ip(CV.after(32n, sig)), Bool.and(Bool.and(ES.scalar_ok(one, CV.os2ip(CV.first(32n, sig))), ES.scalar_ok(one, CV.os2ip(CV.after(32n, sig)))), Bool.or(Bool.not(strict), Bool.not(Nat.is_lt(FS.order(one), Nat.double(CV.os2ip(CV.after(32n, sig)))))))) : Bool}
101      %Equal.sym(Bool, S.is_high(B.of_be(B.suffix(32n, sig))), Nat.is_lt(FS.order(one), Nat.double(FS.value(one, B.of_be(B.suffix(32n, sig))))), FW.is_high_s(one, h1, B.of_be(B.suffix(32n, sig)))) : {E.verify_ok(q, E.hash_scalar(h), B.of_be(B.prefix(32n, sig)), B.of_be(B.suffix(32n, sig)), Bool.and(Bool.and(ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), ES.scalar_ok(one, FS.value(one, B.of_be(B.suffix(32n, sig))))), Bool.or(Bool.not(strict), Bool.not(_)))) == ES.verify_ok(one, PT.pv(one, q), ES.hash_scalar(one, h), CV.os2ip(CV.first(32n, sig)), CV.os2ip(CV.after(32n, sig)), Bool.and(Bool.and(ES.scalar_ok(one, CV.os2ip(CV.first(32n, sig))), ES.scalar_ok(one, CV.os2ip(CV.after(32n, sig)))), Bool.or(Bool.not(strict), Bool.not(Nat.is_lt(FS.order(one), Nat.double(CV.os2ip(CV.after(32n, sig)))))))) : Bool}
102      %Equal.sym(Nat, ES.hash_scalar(one, h), FS.value(one, E.hash_scalar(h)), Equal.sym(Nat, FS.value(one, E.hash_scalar(h)), ES.hash_scalar(one, h), SQ.hash_v(one, h1, h, hh))) : {E.verify_ok(q, E.hash_scalar(h), B.of_be(B.prefix(32n, sig)), B.of_be(B.suffix(32n, sig)), Bool.and(Bool.and(ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), ES.scalar_ok(one, FS.value(one, B.of_be(B.suffix(32n, sig))))), Bool.or(Bool.not(strict), Bool.not(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, B.of_be(B.suffix(32n, sig))))))))) == ES.verify_ok(one, PT.pv(one, q), _, CV.os2ip(CV.first(32n, sig)), CV.os2ip(CV.after(32n, sig)), Bool.and(Bool.and(ES.scalar_ok(one, CV.os2ip(CV.first(32n, sig))), ES.scalar_ok(one, CV.os2ip(CV.after(32n, sig)))), Bool.or(Bool.not(strict), Bool.not(Nat.is_lt(FS.order(one), Nat.double(CV.os2ip(CV.after(32n, sig)))))))) : Bool}
103      %Equal.sym(List<&2, U32>, CV.first(32n, sig), B.prefix(32n, sig), Equal.sym(List<&2, U32>, B.prefix(32n, sig), CV.first(32n, sig), BL.prefix_first(32n, sig))) : {E.verify_ok(q, E.hash_scalar(h), B.of_be(B.prefix(32n, sig)), B.of_be(B.suffix(32n, sig)), Bool.and(Bool.and(ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), ES.scalar_ok(one, FS.value(one, B.of_be(B.suffix(32n, sig))))), Bool.or(Bool.not(strict), Bool.not(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, B.of_be(B.suffix(32n, sig))))))))) == ES.verify_ok(one, PT.pv(one, q), FS.value(one, E.hash_scalar(h)), CV.os2ip(_), CV.os2ip(CV.after(32n, sig)), Bool.and(Bool.and(ES.scalar_ok(one, CV.os2ip(CV.first(32n, sig))), ES.scalar_ok(one, CV.os2ip(CV.after(32n, sig)))), Bool.or(Bool.not(strict), Bool.not(Nat.is_lt(FS.order(one), Nat.double(CV.os2ip(CV.after(32n, sig)))))))) : Bool}
104      %Equal.sym(List<&2, U32>, CV.first(32n, sig), B.prefix(32n, sig), Equal.sym(List<&2, U32>, B.prefix(32n, sig), CV.first(32n, sig), BL.prefix_first(32n, sig))) : {E.verify_ok(q, E.hash_scalar(h), B.of_be(B.prefix(32n, sig)), B.of_be(B.suffix(32n, sig)), Bool.and(Bool.and(ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), ES.scalar_ok(one, FS.value(one, B.of_be(B.suffix(32n, sig))))), Bool.or(Bool.not(strict), Bool.not(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, B.of_be(B.suffix(32n, sig))))))))) == ES.verify_ok(one, PT.pv(one, q), FS.value(one, E.hash_scalar(h)), CV.os2ip(B.prefix(32n, sig)), CV.os2ip(CV.after(32n, sig)), Bool.and(Bool.and(ES.scalar_ok(one, CV.os2ip(_)), ES.scalar_ok(one, CV.os2ip(CV.after(32n, sig)))), Bool.or(Bool.not(strict), Bool.not(Nat.is_lt(FS.order(one), Nat.double(CV.os2ip(CV.after(32n, sig)))))))) : Bool}
105      %Equal.sym(List<&2, U32>, CV.after(32n, sig), B.suffix(32n, sig), Equal.sym(List<&2, U32>, B.suffix(32n, sig), CV.after(32n, sig), BL.suffix_after(32n, sig))) : {E.verify_ok(q, E.hash_scalar(h), B.of_be(B.prefix(32n, sig)), B.of_be(B.suffix(32n, sig)), Bool.and(Bool.and(ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), ES.scalar_ok(one, FS.value(one, B.of_be(B.suffix(32n, sig))))), Bool.or(Bool.not(strict), Bool.not(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, B.of_be(B.suffix(32n, sig))))))))) == ES.verify_ok(one, PT.pv(one, q), FS.value(one, E.hash_scalar(h)), CV.os2ip(B.prefix(32n, sig)), CV.os2ip(_), Bool.and(Bool.and(ES.scalar_ok(one, CV.os2ip(B.prefix(32n, sig))), ES.scalar_ok(one, CV.os2ip(CV.after(32n, sig)))), Bool.or(Bool.not(strict), Bool.not(Nat.is_lt(FS.order(one), Nat.double(CV.os2ip(CV.after(32n, sig)))))))) : Bool}
106      %Equal.sym(List<&2, U32>, CV.after(32n, sig), B.suffix(32n, sig), Equal.sym(List<&2, U32>, B.suffix(32n, sig), CV.after(32n, sig), BL.suffix_after(32n, sig))) : {E.verify_ok(q, E.hash_scalar(h), B.of_be(B.prefix(32n, sig)), B.of_be(B.suffix(32n, sig)), Bool.and(Bool.and(ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), ES.scalar_ok(one, FS.value(one, B.of_be(B.suffix(32n, sig))))), Bool.or(Bool.not(strict), Bool.not(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, B.of_be(B.suffix(32n, sig))))))))) == ES.verify_ok(one, PT.pv(one, q), FS.value(one, E.hash_scalar(h)), CV.os2ip(B.prefix(32n, sig)), CV.os2ip(B.suffix(32n, sig)), Bool.and(Bool.and(ES.scalar_ok(one, CV.os2ip(B.prefix(32n, sig))), ES.scalar_ok(one, CV.os2ip(_))), Bool.or(Bool.not(strict), Bool.not(Nat.is_lt(FS.order(one), Nat.double(CV.os2ip(CV.after(32n, sig)))))))) : Bool}
107      %Equal.sym(List<&2, U32>, CV.after(32n, sig), B.suffix(32n, sig), Equal.sym(List<&2, U32>, B.suffix(32n, sig), CV.after(32n, sig), BL.suffix_after(32n, sig))) : {E.verify_ok(q, E.hash_scalar(h), B.of_be(B.prefix(32n, sig)), B.of_be(B.suffix(32n, sig)), Bool.and(Bool.and(ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), ES.scalar_ok(one, FS.value(one, B.of_be(B.suffix(32n, sig))))), Bool.or(Bool.not(strict), Bool.not(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, B.of_be(B.suffix(32n, sig))))))))) == ES.verify_ok(one, PT.pv(one, q), FS.value(one, E.hash_scalar(h)), CV.os2ip(B.prefix(32n, sig)), CV.os2ip(B.suffix(32n, sig)), Bool.and(Bool.and(ES.scalar_ok(one, CV.os2ip(B.prefix(32n, sig))), ES.scalar_ok(one, CV.os2ip(B.suffix(32n, sig)))), Bool.or(Bool.not(strict), Bool.not(Nat.is_lt(FS.order(one), Nat.double(CV.os2ip(_))))))) : Bool}
108      %Equal.sym(Nat, CV.os2ip(B.prefix(32n, sig)), FS.value(one, B.of_be(B.prefix(32n, sig))), Equal.sym(Nat, FS.value(one, B.of_be(B.prefix(32n, sig))), CV.os2ip(B.prefix(32n, sig)), BY.of_be_value(one, h1, B.prefix(32n, sig)))) : {E.verify_ok(q, E.hash_scalar(h), B.of_be(B.prefix(32n, sig)), B.of_be(B.suffix(32n, sig)), Bool.and(Bool.and(ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), ES.scalar_ok(one, FS.value(one, B.of_be(B.suffix(32n, sig))))), Bool.or(Bool.not(strict), Bool.not(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, B.of_be(B.suffix(32n, sig))))))))) == ES.verify_ok(one, PT.pv(one, q), FS.value(one, E.hash_scalar(h)), _, CV.os2ip(B.suffix(32n, sig)), Bool.and(Bool.and(ES.scalar_ok(one, CV.os2ip(B.prefix(32n, sig))), ES.scalar_ok(one, CV.os2ip(B.suffix(32n, sig)))), Bool.or(Bool.not(strict), Bool.not(Nat.is_lt(FS.order(one), Nat.double(CV.os2ip(B.suffix(32n, sig)))))))) : Bool}
109      %Equal.sym(Nat, CV.os2ip(B.prefix(32n, sig)), FS.value(one, B.of_be(B.prefix(32n, sig))), Equal.sym(Nat, FS.value(one, B.of_be(B.prefix(32n, sig))), CV.os2ip(B.prefix(32n, sig)), BY.of_be_value(one, h1, B.prefix(32n, sig)))) : {E.verify_ok(q, E.hash_scalar(h), B.of_be(B.prefix(32n, sig)), B.of_be(B.suffix(32n, sig)), Bool.and(Bool.and(ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), ES.scalar_ok(one, FS.value(one, B.of_be(B.suffix(32n, sig))))), Bool.or(Bool.not(strict), Bool.not(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, B.of_be(B.suffix(32n, sig))))))))) == ES.verify_ok(one, PT.pv(one, q), FS.value(one, E.hash_scalar(h)), FS.value(one, B.of_be(B.prefix(32n, sig))), CV.os2ip(B.suffix(32n, sig)), Bool.and(Bool.and(ES.scalar_ok(one, _), ES.scalar_ok(one, CV.os2ip(B.suffix(32n, sig)))), Bool.or(Bool.not(strict), Bool.not(Nat.is_lt(FS.order(one), Nat.double(CV.os2ip(B.suffix(32n, sig)))))))) : Bool}
110      %Equal.sym(Nat, CV.os2ip(B.suffix(32n, sig)), FS.value(one, B.of_be(B.suffix(32n, sig))), Equal.sym(Nat, FS.value(one, B.of_be(B.suffix(32n, sig))), CV.os2ip(B.suffix(32n, sig)), BY.of_be_value(one, h1, B.suffix(32n, sig)))) : {E.verify_ok(q, E.hash_scalar(h), B.of_be(B.prefix(32n, sig)), B.of_be(B.suffix(32n, sig)), Bool.and(Bool.and(ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), ES.scalar_ok(one, FS.value(one, B.of_be(B.suffix(32n, sig))))), Bool.or(Bool.not(strict), Bool.not(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, B.of_be(B.suffix(32n, sig))))))))) == ES.verify_ok(one, PT.pv(one, q), FS.value(one, E.hash_scalar(h)), FS.value(one, B.of_be(B.prefix(32n, sig))), _, Bool.and(Bool.and(ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), ES.scalar_ok(one, CV.os2ip(B.suffix(32n, sig)))), Bool.or(Bool.not(strict), Bool.not(Nat.is_lt(FS.order(one), Nat.double(CV.os2ip(B.suffix(32n, sig)))))))) : Bool}
111      %Equal.sym(Nat, CV.os2ip(B.suffix(32n, sig)), FS.value(one, B.of_be(B.suffix(32n, sig))), Equal.sym(Nat, FS.value(one, B.of_be(B.suffix(32n, sig))), CV.os2ip(B.suffix(32n, sig)), BY.of_be_value(one, h1, B.suffix(32n, sig)))) : {E.verify_ok(q, E.hash_scalar(h), B.of_be(B.prefix(32n, sig)), B.of_be(B.suffix(32n, sig)), Bool.and(Bool.and(ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), ES.scalar_ok(one, FS.value(one, B.of_be(B.suffix(32n, sig))))), Bool.or(Bool.not(strict), Bool.not(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, B.of_be(B.suffix(32n, sig))))))))) == ES.verify_ok(one, PT.pv(one, q), FS.value(one, E.hash_scalar(h)), FS.value(one, B.of_be(B.prefix(32n, sig))), FS.value(one, B.of_be(B.suffix(32n, sig))), Bool.and(Bool.and(ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), ES.scalar_ok(one, _)), Bool.or(Bool.not(strict), Bool.not(Nat.is_lt(FS.order(one), Nat.double(CV.os2ip(B.suffix(32n, sig)))))))) : Bool}
112      %Equal.sym(Nat, CV.os2ip(B.suffix(32n, sig)), FS.value(one, B.of_be(B.suffix(32n, sig))), Equal.sym(Nat, FS.value(one, B.of_be(B.suffix(32n, sig))), CV.os2ip(B.suffix(32n, sig)), BY.of_be_value(one, h1, B.suffix(32n, sig)))) : {E.verify_ok(q, E.hash_scalar(h), B.of_be(B.prefix(32n, sig)), B.of_be(B.suffix(32n, sig)), Bool.and(Bool.and(ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), ES.scalar_ok(one, FS.value(one, B.of_be(B.suffix(32n, sig))))), Bool.or(Bool.not(strict), Bool.not(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, B.of_be(B.suffix(32n, sig))))))))) == ES.verify_ok(one, PT.pv(one, q), FS.value(one, E.hash_scalar(h)), FS.value(one, B.of_be(B.prefix(32n, sig))), FS.value(one, B.of_be(B.suffix(32n, sig))), Bool.and(Bool.and(ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), ES.scalar_ok(one, FS.value(one, B.of_be(B.suffix(32n, sig))))), Bool.or(Bool.not(strict), Bool.not(Nat.is_lt(FS.order(one), Nat.double(_)))))) : Bool}
113      vok(one, h1, q, hm, E.hash_scalar(h), SQ.hash_r(one, h1, h, hh), B.of_be(B.prefix(32n, sig)), hlr, B.of_be(B.suffix(32n, sig)), hls, ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), ES.scalar_ok(one, FS.value(one, B.of_be(B.suffix(32n, sig)))), Bool.or(Bool.not(strict), Bool.not(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, B.of_be(B.suffix(32n, sig))))))), {==}, {==})
114
115def vlen(+one: Nat, +h1: {one == 1n : Nat}, +pk: List<&2, U32>, +h: List<&2, U32>, +sig: List<&2, U32>, strict: Bool, a: Bool, b: Bool, +ha: {B.has_len(32n, h) == a : Bool}, +hb: {B.has_len(64n, sig) == b : Bool}) -> {E.verify_len(pk, h, sig, strict, Bool.and(a, b)) == ES.verify_len(one, pk, h, sig, strict, Bool.and(a, b)) : Bool}:
116  match a b:
117    case True{} True{}:
118      %Equal.sym(Maybe<&2, CV.SPoint>, CV.decode(FS.prime(one), pk), PE.mpv(one, P.decode(pk)), Equal.sym(Maybe<&2, CV.SPoint>, PE.mpv(one, P.decode(pk)), CV.decode(FS.prime(one), pk), PD.decode_v(one, h1, pk))) : {E.verify_q(h, sig, strict, P.decode(pk)) == ES.verify_q(one, h, sig, strict, _) : Bool}
119      vq(one, h1, h, ha, sig, hb, strict, P.decode(pk), PD.decode_r(one, h1, pk))
120    case True{} False{}:
121      {==}
122    case False{} _:
123      {==}
124
125# verify (strict = False) and verify_strict (strict = True)
126def verify_v(+one: Nat, +h1: {one == 1n : Nat}, +pk: List<&2, U32>, +h: List<&2, U32>, +sig: List<&2, U32>, strict: Bool) -> {E.verify_with(pk, h, sig, strict) == ES.verify(one, pk, h, sig, strict) : Bool}:
127  %Equal.sym(Bool, B.has_len(32n, h), CV.length_is(32n, h), BL.hl_is(32n, h)) : {E.verify_len(pk, h, sig, strict, Bool.and(_, B.has_len(64n, sig))) == ES.verify_len(one, pk, h, sig, strict, Bool.and(CV.length_is(32n, h), CV.length_is(64n, sig))) : Bool}
128  %Equal.sym(Bool, B.has_len(64n, sig), CV.length_is(64n, sig), BL.hl_is(64n, sig)) : {E.verify_len(pk, h, sig, strict, Bool.and(CV.length_is(32n, h), _)) == ES.verify_len(one, pk, h, sig, strict, Bool.and(CV.length_is(32n, h), CV.length_is(64n, sig))) : Bool}
129  vlen(one, h1, pk, h, sig, strict, CV.length_is(32n, h), CV.length_is(64n, sig), BL.hl_is(32n, h), BL.hl_is(64n, sig))