~/jendhub

def sign_v

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

import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pschn.bend as Pschn
import Base
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/schnorr.bend as SS
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/schnorr.bend as SC
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/blist.bend as BL

324# BIP-340 signing
325def sign_v(+one: Nat, +h1: {one == 1n : Nat}, +sk: List<&2, U32>, +m: List<&2, U32>, +aux: List<&2, U32>) -> {SC.sign(sk, m, aux) == SS.sign(one, sk, m, aux) : Maybe<&2, List<&2, U32>>}:
326  %Equal.sym(Bool, B.has_len(32n, aux), CV.length_is(32n, aux), BL.hl_is(32n, aux)) : {SC.sign_len(sk, m, aux, _) == SS.sign_ok(one, sk, m, aux, Bool.and(CV.length_is(32n, aux), SS.secret_ok(one, sk))) : Maybe<&2, List<&2, U32>>}
327  s1(one, h1, sk, m, aux, CV.length_is(32n, aux), BL.hl_is(32n, aux))

Uses (16)

Used by (1)