def vq
bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/pver.bend:90
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pver.bend as Pver
import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend as FS
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend as CV
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/ecdsa.bend as ES
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/scalar.bend as S
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/bytes.bend as B
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/point.bend as P
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/ecdsa.bend as E
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/fwrap.bend as FW
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bytes.bend as BY
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/point.bend as PT
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/penc.bend as PE
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/blist.bend as BL
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pscal.bend as SQ
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))))))), {==}, {==})