def snz

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

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/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/point.bend as PT
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/sel.bend as SL
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pmul.bend as PM
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/paff.bend as PA

249def snz(+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}, z: Bool) -> {SC.sign_nz(d, pb, m, k0, Bool.not(z)) == SS.sign_kz(one, FS.value(one, d), pb, m, FS.value(one, k0), z) : Maybe<&2, List<&2, U32>>}:
250  match z:
251    case True{}:
252      {==}
253    case False{}:
254      +hg = PA.g_r(one, h1)
255      +hm = PM.mul_r(one, h1, k0, P.g(), SL.sl16(one, k0, hk0), hg)
256      %Equal.sym(CV.SPoint, CV.g(one), PT.pv(one, P.g()), Equal.sym(CV.SPoint, PT.pv(one, P.g()), CV.g(one), PA.g_v(one, h1))) : {SC.sign_k(d, pb, m, k0, P.to_affine(P.mul(k0, P.g()))) == SS.sign_r(one, FS.value(one, d), pb, m, FS.value(one, k0), CV.to_affine(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, k0), _))) : Maybe<&2, List<&2, U32>>}
257      %Equal.sym(CV.SPoint, CV.pmul(FS.prime(one), FS.value(one, k0), PT.pv(one, P.g())), PT.pv(one, P.mul(k0, P.g())), Equal.sym(CV.SPoint, PT.pv(one, P.mul(k0, P.g())), CV.pmul(FS.prime(one), FS.value(one, k0), PT.pv(one, P.g())), PM.mul_v(one, h1, k0, P.g(), SL.sl16(one, k0, hk0), hg))) : {SC.sign_k(d, pb, m, k0, P.to_affine(P.mul(k0, P.g()))) == SS.sign_r(one, FS.value(one, d), pb, m, FS.value(one, k0), CV.to_affine(FS.prime(one), _)) : Maybe<&2, List<&2, U32>>}
258      %Equal.sym(CV.SAffine, CV.to_affine(FS.prime(one), PT.pv(one, P.mul(k0, P.g()))), PA.av(one, P.to_affine(P.mul(k0, P.g()))), Equal.sym(CV.SAffine, PA.av(one, P.to_affine(P.mul(k0, P.g()))), CV.to_affine(FS.prime(one), PT.pv(one, P.mul(k0, P.g()))), PA.aff_v(one, h1, P.mul(k0, P.g()), hm))) : {SC.sign_k(d, pb, m, k0, P.to_affine(P.mul(k0, P.g()))) == SS.sign_r(one, FS.value(one, d), pb, m, FS.value(one, k0), _) : Maybe<&2, List<&2, U32>>}
259      sk_v(one, h1, d, hd, pb, m, k0, hk0, P.to_affine(P.mul(k0, P.g())), PA.aff_r(one, h1, P.mul(k0, P.g()), hm))