def encode_compressed_v
bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/penc.bend:56
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/penc.bend as Penc
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/src/crypto/secp256k1/point.bend as P
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/paff.bend as PA
56def encode_compressed_v(+one: Nat, +h1: {one == 1n : Nat}, +q: P.Point, +hq: {PT.pred(one, q) == True{} : Bool}) -> {P.encode_compressed(q) == CV.encode_compressed(FS.prime(one), PT.pv(one, q)) : List<&2, U32>}:
57 %Equal.sym(CV.SAffine, CV.to_affine(FS.prime(one), PT.pv(one, q)), PA.av(one, P.to_affine(q)), Equal.sym(CV.SAffine, PA.av(one, P.to_affine(q)), CV.to_affine(FS.prime(one), PT.pv(one, q)), PA.aff_v(one, h1, q, hq))) : {P.enc_c(P.to_affine(q)) == CV.enc_c(_) : List<&2, U32>}
58 enc_c_v(one, h1, P.to_affine(q), PA.aff_r(one, h1, q, hq))