def pk3

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

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/bytes.bend as B
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/bytes.bend as BY
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/pmul.bend as PM
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/paff.bend as PA

336def pk3(+one: Nat, +h1: {one == 1n : Nat}, +sk: List<&2, U32>, +hl: {B.has_len(32n, sk) == True{} : Bool}, c: Bool) -> {SC.pubkey_d(SC.secret_if(B.of_be(sk), c)) == SS.pubkey_ok(one, sk, c) : Maybe<&2, List<&2, U32>>}:
337  match c:
338    case True{}:
339      +hdl = BY.of_be_limbs(one, h1, sk, hl)
340      +hg = PA.g_r(one, h1)
341      +hm = PM.mul_r(one, h1, B.of_be(sk), P.g(), hdl, hg)
342      %Equal.sym(Nat, CV.os2ip(sk), FS.value(one, B.of_be(sk)), Equal.sym(Nat, FS.value(one, B.of_be(sk)), CV.os2ip(sk), BY.of_be_value(one, h1, sk))) : {Some{SC.pubkey_aff(P.to_affine(P.mul(B.of_be(sk), P.g())))} == Some{SS.pub_of(CV.to_affine(FS.prime(one), CV.pmul(FS.prime(one), _, CV.g(one))))} : Maybe<&2, List<&2, U32>>}
343      %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))) : {Some{SC.pubkey_aff(P.to_affine(P.mul(B.of_be(sk), P.g())))} == Some{SS.pub_of(CV.to_affine(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, B.of_be(sk)), _)))} : Maybe<&2, List<&2, U32>>}
344      %Equal.sym(CV.SPoint, CV.pmul(FS.prime(one), FS.value(one, B.of_be(sk)), PT.pv(one, P.g())), PT.pv(one, P.mul(B.of_be(sk), P.g())), Equal.sym(CV.SPoint, PT.pv(one, P.mul(B.of_be(sk), P.g())), CV.pmul(FS.prime(one), FS.value(one, B.of_be(sk)), PT.pv(one, P.g())), PM.mul_v(one, h1, B.of_be(sk), P.g(), hdl, hg))) : {Some{SC.pubkey_aff(P.to_affine(P.mul(B.of_be(sk), P.g())))} == Some{SS.pub_of(CV.to_affine(FS.prime(one), _))} : Maybe<&2, List<&2, U32>>}
345      %Equal.sym(CV.SAffine, CV.to_affine(FS.prime(one), PT.pv(one, P.mul(B.of_be(sk), P.g()))), PA.av(one, P.to_affine(P.mul(B.of_be(sk), P.g()))), Equal.sym(CV.SAffine, PA.av(one, P.to_affine(P.mul(B.of_be(sk), P.g()))), CV.to_affine(FS.prime(one), PT.pv(one, P.mul(B.of_be(sk), P.g()))), PA.aff_v(one, h1, P.mul(B.of_be(sk), P.g()), hm))) : {Some{SC.pubkey_aff(P.to_affine(P.mul(B.of_be(sk), P.g())))} == Some{SS.pub_of(_)} : Maybe<&2, List<&2, U32>>}
346      %Equal.sym(List<&2, U32>, SC.pubkey_aff(P.to_affine(P.mul(B.of_be(sk), P.g()))), SS.pub_of(PA.av(one, P.to_affine(P.mul(B.of_be(sk), P.g())))), paff(one, h1, P.to_affine(P.mul(B.of_be(sk), P.g())), PA.aff_r(one, h1, P.mul(B.of_be(sk), P.g()), hm))) : {Some{_} == Some{SS.pub_of(PA.av(one, P.to_affine(P.mul(B.of_be(sk), P.g()))))} : Maybe<&2, List<&2, U32>>}
347      {==}
348    case False{}:
349      {==}