def paff

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

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/point.bend as P
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/schnorr.bend as SC
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/paff.bend as PA

331def paff(+one: Nat, +h1: {one == 1n : Nat}, a: P.Affine, +ha: {PA.ared(one, a) == True{} : Bool}) -> {SC.pubkey_aff(a) == SS.pub_of(PA.av(one, a)) : List<&2, U32>}:
332  match a:
333    case P.Affine{+x, +y}:
334      tbv(one, h1, x, ax_l(one, x, y, ha))