Pdec.d65: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pdec.bend as Pdec
Lines 89-106 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pdec.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pdec.bend&start_line=89&end_line=106

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

def d65(+one: Nat, +h1: {one == 1n : Nat}, +pre: U32, +rest: List<&2, U32>, +hl: {B.has_len(64n, rest) == True{} : Bool}) -> {PE.mpv(one, P.decode_65(pre, rest)) == CV.decode_u(FS.prime(one), pre, CV.os2ip(CV.first(32n, rest)), CV.os2ip(CV.after(32n, rest))) : Maybe<&2, CV.SPoint>}:
  +hlx = BY.of_be_limbs(one, h1, B.prefix(32n, rest), BL.pl32(rest, hl))
  +hly = BY.of_be_limbs(one, h1, B.suffix(32n, rest), BL.sl32(rest, hl))
  %Equal.sym(Bool, F.lt_p(B.of_be(B.prefix(32n, rest))), Nat.is_lt(FS.value(one, B.of_be(B.prefix(32n, rest))), FS.prime(one)), FW.lt_p_f(one, h1, B.of_be(B.prefix(32n, rest)))) : {PE.mpv(one, P.decode_u(B.of_be(B.prefix(32n, rest)), B.of_be(B.suffix(32n, rest)), Bool.and(Bool.and(U32.is_eq(pre, 4), Bool.and(_, F.lt_p(B.of_be(B.suffix(32n, rest))))), P.on_curve(B.of_be(B.prefix(32n, rest)), B.of_be(B.suffix(32n, rest)))))) == CV.decompress_if(CV.os2ip(CV.first(32n, rest)), CV.os2ip(CV.after(32n, rest)), Bool.and(Bool.and(U32.is_eq(pre, 4), Bool.and(Nat.is_lt(CV.os2ip(CV.first(32n, rest)), FS.prime(one)), Nat.is_lt(CV.os2ip(CV.after(32n, rest)), FS.prime(one)))), CV.on_curve(FS.prime(one), CV.os2ip(CV.first(32n, rest)), CV.os2ip(CV.after(32n, rest))))) : Maybe<&2, CV.SPoint>}
  %Equal.sym(Bool, F.lt_p(B.of_be(B.suffix(32n, rest))), Nat.is_lt(FS.value(one, B.of_be(B.suffix(32n, rest))), FS.prime(one)), FW.lt_p_f(one, h1, B.of_be(B.suffix(32n, rest)))) : {PE.mpv(one, P.decode_u(B.of_be(B.prefix(32n, rest)), B.of_be(B.suffix(32n, rest)), Bool.and(Bool.and(U32.is_eq(pre, 4), Bool.and(Nat.is_lt(FS.value(one, B.of_be(B.prefix(32n, rest))), FS.prime(one)), _)), P.on_curve(B.of_be(B.prefix(32n, rest)), B.of_be(B.suffix(32n, rest)))))) == CV.decompress_if(CV.os2ip(CV.first(32n, rest)), CV.os2ip(CV.after(32n, rest)), Bool.and(Bool.and(U32.is_eq(pre, 4), Bool.and(Nat.is_lt(CV.os2ip(CV.first(32n, rest)), FS.prime(one)), Nat.is_lt(CV.os2ip(CV.after(32n, rest)), FS.prime(one)))), CV.on_curve(FS.prime(one), CV.os2ip(CV.first(32n, rest)), CV.os2ip(CV.after(32n, rest))))) : Maybe<&2, CV.SPoint>}
  %Equal.sym(List<&2, U32>, CV.first(32n, rest), B.prefix(32n, rest), Equal.sym(List<&2, U32>, B.prefix(32n, rest), CV.first(32n, rest), BL.prefix_first(32n, rest))) : {PE.mpv(one, P.decode_u(B.of_be(B.prefix(32n, rest)), B.of_be(B.suffix(32n, rest)), Bool.and(Bool.and(U32.is_eq(pre, 4), Bool.and(Nat.is_lt(FS.value(one, B.of_be(B.prefix(32n, rest))), FS.prime(one)), Nat.is_lt(FS.value(one, B.of_be(B.suffix(32n, rest))), FS.prime(one)))), P.on_curve(B.of_be(B.prefix(32n, rest)), B.of_be(B.suffix(32n, rest)))))) == CV.decompress_if(CV.os2ip(_), CV.os2ip(CV.after(32n, rest)), Bool.and(Bool.and(U32.is_eq(pre, 4), Bool.and(Nat.is_lt(CV.os2ip(CV.first(32n, rest)), FS.prime(one)), Nat.is_lt(CV.os2ip(CV.after(32n, rest)), FS.prime(one)))), CV.on_curve(FS.prime(one), CV.os2ip(CV.first(32n, rest)), CV.os2ip(CV.after(32n, rest))))) : Maybe<&2, CV.SPoint>}
  %Equal.sym(List<&2, U32>, CV.first(32n, rest), B.prefix(32n, rest), Equal.sym(List<&2, U32>, B.prefix(32n, rest), CV.first(32n, rest), BL.prefix_first(32n, rest))) : {PE.mpv(one, P.decode_u(B.of_be(B.prefix(32n, rest)), B.of_be(B.suffix(32n, rest)), Bool.and(Bool.and(U32.is_eq(pre, 4), Bool.and(Nat.is_lt(FS.value(one, B.of_be(B.prefix(32n, rest))), FS.prime(one)), Nat.is_lt(FS.value(one, B.of_be(B.suffix(32n, rest))), FS.prime(one)))), P.on_curve(B.of_be(B.prefix(32n, rest)), B.of_be(B.suffix(32n, rest)))))) == CV.decompress_if(CV.os2ip(B.prefix(32n, rest)), CV.os2ip(CV.after(32n, rest)), Bool.and(Bool.and(U32.is_eq(pre, 4), Bool.and(Nat.is_lt(CV.os2ip(_), FS.prime(one)), Nat.is_lt(CV.os2ip(CV.after(32n, rest)), FS.prime(one)))), CV.on_curve(FS.prime(one), CV.os2ip(CV.first(32n, rest)), CV.os2ip(CV.after(32n, rest))))) : Maybe<&2, CV.SPoint>}
  %Equal.sym(List<&2, U32>, CV.first(32n, rest), B.prefix(32n, rest), Equal.sym(List<&2, U32>, B.prefix(32n, rest), CV.first(32n, rest), BL.prefix_first(32n, rest))) : {PE.mpv(one, P.decode_u(B.of_be(B.prefix(32n, rest)), B.of_be(B.suffix(32n, rest)), Bool.and(Bool.and(U32.is_eq(pre, 4), Bool.and(Nat.is_lt(FS.value(one, B.of_be(B.prefix(32n, rest))), FS.prime(one)), Nat.is_lt(FS.value(one, B.of_be(B.suffix(32n, rest))), FS.prime(one)))), P.on_curve(B.of_be(B.prefix(32n, rest)), B.of_be(B.suffix(32n, rest)))))) == CV.decompress_if(CV.os2ip(B.prefix(32n, rest)), CV.os2ip(CV.after(32n, rest)), Bool.and(Bool.and(U32.is_eq(pre, 4), Bool.and(Nat.is_lt(CV.os2ip(B.prefix(32n, rest)), FS.prime(one)), Nat.is_lt(CV.os2ip(CV.after(32n, rest)), FS.prime(one)))), CV.on_curve(FS.prime(one), CV.os2ip(_), CV.os2ip(CV.after(32n, rest))))) : Maybe<&2, CV.SPoint>}
  %Equal.sym(List<&2, U32>, CV.after(32n, rest), B.suffix(32n, rest), Equal.sym(List<&2, U32>, B.suffix(32n, rest), CV.after(32n, rest), BL.suffix_after(32n, rest))) : {PE.mpv(one, P.decode_u(B.of_be(B.prefix(32n, rest)), B.of_be(B.suffix(32n, rest)), Bool.and(Bool.and(U32.is_eq(pre, 4), Bool.and(Nat.is_lt(FS.value(one, B.of_be(B.prefix(32n, rest))), FS.prime(one)), Nat.is_lt(FS.value(one, B.of_be(B.suffix(32n, rest))), FS.prime(one)))), P.on_curve(B.of_be(B.prefix(32n, rest)), B.of_be(B.suffix(32n, rest)))))) == CV.decompress_if(CV.os2ip(B.prefix(32n, rest)), CV.os2ip(_), Bool.and(Bool.and(U32.is_eq(pre, 4), Bool.and(Nat.is_lt(CV.os2ip(B.prefix(32n, rest)), FS.prime(one)), Nat.is_lt(CV.os2ip(CV.after(32n, rest)), FS.prime(one)))), CV.on_curve(FS.prime(one), CV.os2ip(B.prefix(32n, rest)), CV.os2ip(CV.after(32n, rest))))) : Maybe<&2, CV.SPoint>}
  %Equal.sym(List<&2, U32>, CV.after(32n, rest), B.suffix(32n, rest), Equal.sym(List<&2, U32>, B.suffix(32n, rest), CV.after(32n, rest), BL.suffix_after(32n, rest))) : {PE.mpv(one, P.decode_u(B.of_be(B.prefix(32n, rest)), B.of_be(B.suffix(32n, rest)), Bool.and(Bool.and(U32.is_eq(pre, 4), Bool.and(Nat.is_lt(FS.value(one, B.of_be(B.prefix(32n, rest))), FS.prime(one)), Nat.is_lt(FS.value(one, B.of_be(B.suffix(32n, rest))), FS.prime(one)))), P.on_curve(B.of_be(B.prefix(32n, rest)), B.of_be(B.suffix(32n, rest)))))) == CV.decompress_if(CV.os2ip(B.prefix(32n, rest)), CV.os2ip(B.suffix(32n, rest)), Bool.and(Bool.and(U32.is_eq(pre, 4), Bool.and(Nat.is_lt(CV.os2ip(B.prefix(32n, rest)), FS.prime(one)), Nat.is_lt(CV.os2ip(_), FS.prime(one)))), CV.on_curve(FS.prime(one), CV.os2ip(B.prefix(32n, rest)), CV.os2ip(CV.after(32n, rest))))) : Maybe<&2, CV.SPoint>}
  %Equal.sym(List<&2, U32>, CV.after(32n, rest), B.suffix(32n, rest), Equal.sym(List<&2, U32>, B.suffix(32n, rest), CV.after(32n, rest), BL.suffix_after(32n, rest))) : {PE.mpv(one, P.decode_u(B.of_be(B.prefix(32n, rest)), B.of_be(B.suffix(32n, rest)), Bool.and(Bool.and(U32.is_eq(pre, 4), Bool.and(Nat.is_lt(FS.value(one, B.of_be(B.prefix(32n, rest))), FS.prime(one)), Nat.is_lt(FS.value(one, B.of_be(B.suffix(32n, rest))), FS.prime(one)))), P.on_curve(B.of_be(B.prefix(32n, rest)), B.of_be(B.suffix(32n, rest)))))) == CV.decompress_if(CV.os2ip(B.prefix(32n, rest)), CV.os2ip(B.suffix(32n, rest)), Bool.and(Bool.and(U32.is_eq(pre, 4), Bool.and(Nat.is_lt(CV.os2ip(B.prefix(32n, rest)), FS.prime(one)), Nat.is_lt(CV.os2ip(B.suffix(32n, rest)), FS.prime(one)))), CV.on_curve(FS.prime(one), CV.os2ip(B.prefix(32n, rest)), CV.os2ip(_)))) : Maybe<&2, CV.SPoint>}
  %Equal.sym(Nat, CV.os2ip(B.prefix(32n, rest)), FS.value(one, B.of_be(B.prefix(32n, rest))), Equal.sym(Nat, FS.value(one, B.of_be(B.prefix(32n, rest))), CV.os2ip(B.prefix(32n, rest)), BY.of_be_value(one, h1, B.prefix(32n, rest)))) : {PE.mpv(one, P.decode_u(B.of_be(B.prefix(32n, rest)), B.of_be(B.suffix(32n, rest)), Bool.and(Bool.and(U32.is_eq(pre, 4), Bool.and(Nat.is_lt(FS.value(one, B.of_be(B.prefix(32n, rest))), FS.prime(one)), Nat.is_lt(FS.value(one, B.of_be(B.suffix(32n, rest))), FS.prime(one)))), P.on_curve(B.of_be(B.prefix(32n, rest)), B.of_be(B.suffix(32n, rest)))))) == CV.decompress_if(_, CV.os2ip(B.suffix(32n, rest)), Bool.and(Bool.and(U32.is_eq(pre, 4), Bool.and(Nat.is_lt(CV.os2ip(B.prefix(32n, rest)), FS.prime(one)), Nat.is_lt(CV.os2ip(B.suffix(32n, rest)), FS.prime(one)))), CV.on_curve(FS.prime(one), CV.os2ip(B.prefix(32n, rest)), CV.os2ip(B.suffix(32n, rest))))) : Maybe<&2, CV.SPoint>}
  %Equal.sym(Nat, CV.os2ip(B.prefix(32n, rest)), FS.value(one, B.of_be(B.prefix(32n, rest))), Equal.sym(Nat, FS.value(one, B.of_be(B.prefix(32n, rest))), CV.os2ip(B.prefix(32n, rest)), BY.of_be_value(one, h1, B.prefix(32n, rest)))) : {PE.mpv(one, P.decode_u(B.of_be(B.prefix(32n, rest)), B.of_be(B.suffix(32n, rest)), Bool.and(Bool.and(U32.is_eq(pre, 4), Bool.and(Nat.is_lt(FS.value(one, B.of_be(B.prefix(32n, rest))), FS.prime(one)), Nat.is_lt(FS.value(one, B.of_be(B.suffix(32n, rest))), FS.prime(one)))), P.on_curve(B.of_be(B.prefix(32n, rest)), B.of_be(B.suffix(32n, rest)))))) == CV.decompress_if(FS.value(one, B.of_be(B.prefix(32n, rest))), CV.os2ip(B.suffix(32n, rest)), Bool.and(Bool.and(U32.is_eq(pre, 4), Bool.and(Nat.is_lt(_, FS.prime(one)), Nat.is_lt(CV.os2ip(B.suffix(32n, rest)), FS.prime(one)))), CV.on_curve(FS.prime(one), CV.os2ip(B.prefix(32n, rest)), CV.os2ip(B.suffix(32n, rest))))) : Maybe<&2, CV.SPoint>}
  %Equal.sym(Nat, CV.os2ip(B.prefix(32n, rest)), FS.value(one, B.of_be(B.prefix(32n, rest))), Equal.sym(Nat, FS.value(one, B.of_be(B.prefix(32n, rest))), CV.os2ip(B.prefix(32n, rest)), BY.of_be_value(one, h1, B.prefix(32n, rest)))) : {PE.mpv(one, P.decode_u(B.of_be(B.prefix(32n, rest)), B.of_be(B.suffix(32n, rest)), Bool.and(Bool.and(U32.is_eq(pre, 4), Bool.and(Nat.is_lt(FS.value(one, B.of_be(B.prefix(32n, rest))), FS.prime(one)), Nat.is_lt(FS.value(one, B.of_be(B.suffix(32n, rest))), FS.prime(one)))), P.on_curve(B.of_be(B.prefix(32n, rest)), B.of_be(B.suffix(32n, rest)))))) == CV.decompress_if(FS.value(one, B.of_be(B.prefix(32n, rest))), CV.os2ip(B.suffix(32n, rest)), Bool.and(Bool.and(U32.is_eq(pre, 4), Bool.and(Nat.is_lt(FS.value(one, B.of_be(B.prefix(32n, rest))), FS.prime(one)), Nat.is_lt(CV.os2ip(B.suffix(32n, rest)), FS.prime(one)))), CV.on_curve(FS.prime(one), _, CV.os2ip(B.suffix(32n, rest))))) : Maybe<&2, CV.SPoint>}
  %Equal.sym(Nat, CV.os2ip(B.suffix(32n, rest)), FS.value(one, B.of_be(B.suffix(32n, rest))), Equal.sym(Nat, FS.value(one, B.of_be(B.suffix(32n, rest))), CV.os2ip(B.suffix(32n, rest)), BY.of_be_value(one, h1, B.suffix(32n, rest)))) : {PE.mpv(one, P.decode_u(B.of_be(B.prefix(32n, rest)), B.of_be(B.suffix(32n, rest)), Bool.and(Bool.and(U32.is_eq(pre, 4), Bool.and(Nat.is_lt(FS.value(one, B.of_be(B.prefix(32n, rest))), FS.prime(one)), Nat.is_lt(FS.value(one, B.of_be(B.suffix(32n, rest))), FS.prime(one)))), P.on_curve(B.of_be(B.prefix(32n, rest)), B.of_be(B.suffix(32n, rest)))))) == CV.decompress_if(FS.value(one, B.of_be(B.prefix(32n, rest))), _, Bool.and(Bool.and(U32.is_eq(pre, 4), Bool.and(Nat.is_lt(FS.value(one, B.of_be(B.prefix(32n, rest))), FS.prime(one)), Nat.is_lt(CV.os2ip(B.suffix(32n, rest)), FS.prime(one)))), CV.on_curve(FS.prime(one), FS.value(one, B.of_be(B.prefix(32n, rest))), CV.os2ip(B.suffix(32n, rest))))) : Maybe<&2, CV.SPoint>}
  %Equal.sym(Nat, CV.os2ip(B.suffix(32n, rest)), FS.value(one, B.of_be(B.suffix(32n, rest))), Equal.sym(Nat, FS.value(one, B.of_be(B.suffix(32n, rest))), CV.os2ip(B.suffix(32n, rest)), BY.of_be_value(one, h1, B.suffix(32n, rest)))) : {PE.mpv(one, P.decode_u(B.of_be(B.prefix(32n, rest)), B.of_be(B.suffix(32n, rest)), Bool.and(Bool.and(U32.is_eq(pre, 4), Bool.and(Nat.is_lt(FS.value(one, B.of_be(B.prefix(32n, rest))), FS.prime(one)), Nat.is_lt(FS.value(one, B.of_be(B.suffix(32n, rest))), FS.prime(one)))), P.on_curve(B.of_be(B.prefix(32n, rest)), B.of_be(B.suffix(32n, rest)))))) == CV.decompress_if(FS.value(one, B.of_be(B.prefix(32n, rest))), FS.value(one, B.of_be(B.suffix(32n, rest))), Bool.and(Bool.and(U32.is_eq(pre, 4), Bool.and(Nat.is_lt(FS.value(one, B.of_be(B.prefix(32n, rest))), FS.prime(one)), Nat.is_lt(_, FS.prime(one)))), CV.on_curve(FS.prime(one), FS.value(one, B.of_be(B.prefix(32n, rest))), CV.os2ip(B.suffix(32n, rest))))) : Maybe<&2, CV.SPoint>}
  %Equal.sym(Nat, CV.os2ip(B.suffix(32n, rest)), FS.value(one, B.of_be(B.suffix(32n, rest))), Equal.sym(Nat, FS.value(one, B.of_be(B.suffix(32n, rest))), CV.os2ip(B.suffix(32n, rest)), BY.of_be_value(one, h1, B.suffix(32n, rest)))) : {PE.mpv(one, P.decode_u(B.of_be(B.prefix(32n, rest)), B.of_be(B.suffix(32n, rest)), Bool.and(Bool.and(U32.is_eq(pre, 4), Bool.and(Nat.is_lt(FS.value(one, B.of_be(B.prefix(32n, rest))), FS.prime(one)), Nat.is_lt(FS.value(one, B.of_be(B.suffix(32n, rest))), FS.prime(one)))), P.on_curve(B.of_be(B.prefix(32n, rest)), B.of_be(B.suffix(32n, rest)))))) == CV.decompress_if(FS.value(one, B.of_be(B.prefix(32n, rest))), FS.value(one, B.of_be(B.suffix(32n, rest))), Bool.and(Bool.and(U32.is_eq(pre, 4), Bool.and(Nat.is_lt(FS.value(one, B.of_be(B.prefix(32n, rest))), FS.prime(one)), Nat.is_lt(FS.value(one, B.of_be(B.suffix(32n, rest))), FS.prime(one)))), CV.on_curve(FS.prime(one), FS.value(one, B.of_be(B.prefix(32n, rest))), _))) : Maybe<&2, CV.SPoint>}
  du(one, h1, B.of_be(B.prefix(32n, rest)), B.of_be(B.suffix(32n, rest)), hlx, hly, U32.is_eq(pre, 4), Nat.is_lt(FS.value(one, B.of_be(B.prefix(32n, rest))), FS.prime(one)), Nat.is_lt(FS.value(one, B.of_be(B.suffix(32n, rest))), FS.prime(one)), {==}, {==})

Uses (35):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_eq
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/blist.bend&name=pl32
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/blist.bend&name=prefix_first
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/blist.bend&name=sl32
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/blist.bend&name=suffix_after
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bytes.bend&name=of_be_limbs
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bytes.bend&name=of_be_value
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/fwrap.bend&name=lt_p_f
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pdec.bend&name=du
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/penc.bend&name=mpv
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend&name=SPoint
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend&name=after
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend&name=decode_u
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend&name=decompress_if
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend&name=first
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend&name=on_curve
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend&name=os2ip
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend&name=prime
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend&name=value
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/bytes.bend&name=has_len
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/bytes.bend&name=of_be
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/bytes.bend&name=prefix
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/bytes.bend&name=suffix
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/field.bend&name=lt_p
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/point.bend&name=decode_65
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/point.bend&name=decode_u
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/point.bend&name=on_curve