proofs/crypto/secp256k1/pver.bend source
proofs/crypto/secp256k1/pver.bend on the hub · documented module
# GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/pver.src; edit the .srcimport Baseimport ../../../spec/crypto/secp256k1/field.bend as FSimport ../../../spec/crypto/secp256k1/curve.bend as CVimport ../../../spec/crypto/secp256k1/ecdsa.bend as ESimport ../../../src/crypto/secp256k1/scalar.bend as Simport ../../../src/crypto/secp256k1/bytes.bend as Bimport ../../../src/crypto/secp256k1/point.bend as Pimport ../../../src/crypto/secp256k1/ecdsa.bend as Eimport ../../lib/logic.bend as Lgimport ./scalarops.bend as SOimport ./scalarpow.bend as SPimport ./fwrap.bend as FWimport ./bytes.bend as BYimport ./point.bend as PTimport ./sel.bend as SLimport ./pmul.bend as PMimport ./paff.bend as PAimport ./penc.bend as PEimport ./pdec.bend as PDimport ./blist.bend as BLimport ./pscal.bend as SQ# ECDSA verification of src/crypto/secp256k1/ecdsa.bend (verify and# verify_strict) against spec/crypto/secp256k1/ecdsa.bend.def aff_x_v(+one: Nat, a: P.Affine) -> {FS.value(one, P.aff_x(a)) == CV.aff_x(PA.av(one, a)) : Nat}: match a: case P.Affine{x, y}: {==}def 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}: match a: case P.Affine{+x, +y}: SL.l16(one, x, Lg.and_left(PT.red(one, x), PT.red(one, y), ha))# R not the point at infinity and x(R) mod n = rdef 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}: +ha = PA.aff_r(one, h1, rr, hrr) +hx = aff_x_l(one, P.to_affine(rr), ha) %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} %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} %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} %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} %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} {==}def 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}: +hw = SP.inv_r(one, h1, s, hs) +hu1 = SO.mul_r(one, h1, z, S.inv(s), hz, hw) +hu2 = SO.mul_r(one, h1, r, S.inv(s), hr, hw) +hg = PA.g_r(one, h1) +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) +hp2 = PM.mul_r(one, h1, S.mul(r, S.inv(s)), q, SL.sl16(one, S.mul(r, S.inv(s)), hu2), hq) +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) %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} %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} %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} %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} %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} %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} %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} %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} %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} %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} %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} %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} %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} %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} %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} %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} %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} {==}# a valid scalar (1 <= x < n) is reduceddef 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}: 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))def 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}: match a b c: case True{} True{} True{}: vrs(one, h1, q, hq, z, hz, r, ok_red(one, r, hlr, ha), s, ok_red(one, s, hls, hb)) case True{} True{} False{}: {==} case True{} False{} _: {==} case False{} _ _: {==}def 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}: match m: case None{}: {==} case Some{+q}: +r = B.of_be(B.prefix(32n, sig)) +s = B.of_be(B.suffix(32n, sig)) +hlr = BY.of_be_limbs(one, h1, B.prefix(32n, sig), BL.pl32(sig, hsig)) +hls = BY.of_be_limbs(one, h1, B.suffix(32n, sig), BL.sl32(sig, hsig)) %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} %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} %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} %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} %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} %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} %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} %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} %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} %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} %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} %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} %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} %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} 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))))))), {==}, {==})def 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}: match a b: case True{} True{}: %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} vq(one, h1, h, ha, sig, hb, strict, P.decode(pk), PD.decode_r(one, h1, pk)) case True{} False{}: {==} case False{} _: {==}# verify (strict = False) and verify_strict (strict = True)def 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}: %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} %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} 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))