def sk2

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

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/schnorr.bend as SS
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/schnorr.bend as SC
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/fwrap.bend as FW

261def sk2(+one: Nat, +h1: {one == 1n : Nat}, +d: List<&2, Nat>, +hd: {FS.reduced(one, FS.order(one), d) == True{} : Bool}, +pb: List<&2, U32>, +m: List<&2, U32>, +k0: List<&2, Nat>, +hk0: {FS.reduced(one, FS.order(one), k0) == True{} : Bool}) -> {SC.sign_nz(d, pb, m, k0, Bool.not(S.is_zero(k0))) == SS.sign_k(one, FS.value(one, d), pb, m, FS.value(one, k0)) : Maybe<&2, List<&2, U32>>}:
262  %Equal.sym(Bool, S.is_zero(k0), Nat.is_eq(FS.value(one, k0), 0n), FW.is_zero_s(one, h1, k0)) : {SC.sign_nz(d, pb, m, k0, Bool.not(_)) == SS.sign_kz(one, FS.value(one, d), pb, m, FS.value(one, k0), Nat.is_eq(FS.value(one, k0), 0n)) : Maybe<&2, List<&2, U32>>}
263  snz(one, h1, d, hd, pb, m, k0, hk0, Nat.is_eq(FS.value(one, k0), 0n))