def sfin

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/pschn.bend:223

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/schnorr.bend as SS
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/schnorr.bend as SC

223def sfin(+one: Nat, +h1: {one == 1n : Nat}, +pb: List<&2, U32>, +m: List<&2, U32>, +sig: List<&2, U32>) -> {SC.sign_fin(pb, m, sig) == SS.sign_fin(one, pb, m, sig) : Maybe<&2, List<&2, U32>>}:
224  %Equal.sym(Bool, SC.verify(pb, m, sig), SS.verify(one, pb, m, sig), verify_v(one, h1, pb, m, sig)) : {SC.sign_ok(sig, _) == SS.sign_if(sig, SS.verify(one, pb, m, sig)) : Maybe<&2, List<&2, U32>>}
225  sok(sig, SS.verify(one, pb, m, sig))