def decode_v

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/pdec.bend:142

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/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/proofs/crypto/secp256k1/penc.bend as PE
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/blist.bend as BL

142def decode_v(+one: Nat, +h1: {one == 1n : Nat}, +bs: List<&2, U32>) -> {PE.mpv(one, P.decode(bs)) == CV.decode(FS.prime(one), bs) : Maybe<&2, CV.SPoint>}:
143  %Equal.sym(Bool, B.has_len(33n, bs), CV.length_is(33n, bs), BL.hl_is(33n, bs)) : {PE.mpv(one, P.decode_len(bs, _, B.has_len(65n, bs))) == CV.decode_len(FS.prime(one), bs, CV.length_is(33n, bs), CV.length_is(65n, bs)) : Maybe<&2, CV.SPoint>}
144  %Equal.sym(Bool, B.has_len(65n, bs), CV.length_is(65n, bs), BL.hl_is(65n, bs)) : {PE.mpv(one, P.decode_len(bs, CV.length_is(33n, bs), _)) == CV.decode_len(FS.prime(one), bs, CV.length_is(33n, bs), CV.length_is(65n, bs)) : Maybe<&2, CV.SPoint>}
145  dl(one, h1, bs, CV.length_is(33n, bs), CV.length_is(65n, bs), BL.hl_is(33n, bs), BL.hl_is(65n, bs))