def rq_b

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/prec.bend:47

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/ecdsa.bend as ES
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/ecdsa.bend as E
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/penc.bend as PE

47def rq_b(+one: Nat, +h1: {one == 1n : Nat}, +q: P.Point, +hq: {PT.pred(one, q) == True{} : Bool}, b: Bool) -> {E.recover_q(q, b) == ES.recover_q_if(one, PT.pv(one, q), b) : Maybe<&2, List<&2, U32>>}:
48  match b:
49    case True{}:
50      {==}
51    case False{}:
52      Equal.cong(List<&2, U32>, Maybe<&2, List<&2, U32>>, l => Some{l}, P.encode_uncompressed(q), CV.encode_uncompressed(FS.prime(one), PT.pv(one, q)), PE.encode_uncompressed_v(one, h1, q, hq))