Pver.vq: def of bend-collections-laws-crypto@1.0.0.0 Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pver.bend as Pver Lines 90-113 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pver.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pver.bend&start_line=90&end_line=113 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/scalar.bend as S 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/ecdsa.bend as E 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/point.bend as PT 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 import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pscal.bend as SQ def vq(+one: Nat, +h1: {one == 1n : Nat}, +h: List<&2, U32>, +hh: {B.has_len(32n, h) == True{} : Bool}, +sig: List<&2, U32>, +hsig: {B.has_len(64n, sig) == True{} : Bool}, strict: Bool, m: Maybe<&2, P.Point>, +hm: {PE.mpred(one, m) == True{} : Bool}) -> {E.verify_q(h, sig, strict, m) == ES.verify_q(one, h, sig, strict, PE.mpv(one, m)) : Bool}: match m: case None{}: {==} case Some{+q}: +r = B.of_be(B.prefix(32n, sig)) +s = B.of_be(B.suffix(32n, sig)) +hlr = BY.of_be_limbs(one, h1, B.prefix(32n, sig), BL.pl32(sig, hsig)) +hls = BY.of_be_limbs(one, h1, B.suffix(32n, sig), BL.sl32(sig, hsig)) %Equal.sym(Bool, E.scalar_ok(B.of_be(B.prefix(32n, sig))), ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), SQ.scalar_ok_v(one, h1, B.of_be(B.prefix(32n, sig)))) : {E.verify_ok(q, E.hash_scalar(h), B.of_be(B.prefix(32n, sig)), B.of_be(B.suffix(32n, sig)), Bool.and(Bool.and(_, E.scalar_ok(B.of_be(B.suffix(32n, sig)))), Bool.or(Bool.not(strict), Bool.not(S.is_high(B.of_be(B.suffix(32n, sig))))))) == ES.verify_ok(one, PT.pv(one, q), ES.hash_scalar(one, h), CV.os2ip(CV.first(32n, sig)), CV.os2ip(CV.after(32n, sig)), Bool.and(Bool.and(ES.scalar_ok(one, CV.os2ip(CV.first(32n, sig))), ES.scalar_ok(one, CV.os2ip(CV.after(32n, sig)))), Bool.or(Bool.not(strict), Bool.not(Nat.is_lt(FS.order(one), Nat.double(CV.os2ip(CV.after(32n, sig)))))))) : Bool} %Equal.sym(Bool, E.scalar_ok(B.of_be(B.suffix(32n, sig))), ES.scalar_ok(one, FS.value(one, B.of_be(B.suffix(32n, sig)))), SQ.scalar_ok_v(one, h1, B.of_be(B.suffix(32n, sig)))) : {E.verify_ok(q, E.hash_scalar(h), B.of_be(B.prefix(32n, sig)), B.of_be(B.suffix(32n, sig)), Bool.and(Bool.and(ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), _), Bool.or(Bool.not(strict), Bool.not(S.is_high(B.of_be(B.suffix(32n, sig))))))) == ES.verify_ok(one, PT.pv(one, q), ES.hash_scalar(one, h), CV.os2ip(CV.first(32n, sig)), CV.os2ip(CV.after(32n, sig)), Bool.and(Bool.and(ES.scalar_ok(one, CV.os2ip(CV.first(32n, sig))), ES.scalar_ok(one, CV.os2ip(CV.after(32n, sig)))), Bool.or(Bool.not(strict), Bool.not(Nat.is_lt(FS.order(one), Nat.double(CV.os2ip(CV.after(32n, sig)))))))) : Bool} %Equal.sym(Bool, S.is_high(B.of_be(B.suffix(32n, sig))), Nat.is_lt(FS.order(one), Nat.double(FS.value(one, B.of_be(B.suffix(32n, sig))))), FW.is_high_s(one, h1, B.of_be(B.suffix(32n, sig)))) : {E.verify_ok(q, E.hash_scalar(h), B.of_be(B.prefix(32n, sig)), B.of_be(B.suffix(32n, sig)), Bool.and(Bool.and(ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), ES.scalar_ok(one, FS.value(one, B.of_be(B.suffix(32n, sig))))), Bool.or(Bool.not(strict), Bool.not(_)))) == ES.verify_ok(one, PT.pv(one, q), ES.hash_scalar(one, h), CV.os2ip(CV.first(32n, sig)), CV.os2ip(CV.after(32n, sig)), Bool.and(Bool.and(ES.scalar_ok(one, CV.os2ip(CV.first(32n, sig))), ES.scalar_ok(one, CV.os2ip(CV.after(32n, sig)))), Bool.or(Bool.not(strict), Bool.not(Nat.is_lt(FS.order(one), Nat.double(CV.os2ip(CV.after(32n, sig)))))))) : Bool} %Equal.sym(Nat, ES.hash_scalar(one, h), FS.value(one, E.hash_scalar(h)), Equal.sym(Nat, FS.value(one, E.hash_scalar(h)), ES.hash_scalar(one, h), SQ.hash_v(one, h1, h, hh))) : {E.verify_ok(q, E.hash_scalar(h), B.of_be(B.prefix(32n, sig)), B.of_be(B.suffix(32n, sig)), Bool.and(Bool.and(ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), ES.scalar_ok(one, FS.value(one, B.of_be(B.suffix(32n, sig))))), Bool.or(Bool.not(strict), Bool.not(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, B.of_be(B.suffix(32n, sig))))))))) == ES.verify_ok(one, PT.pv(one, q), _, CV.os2ip(CV.first(32n, sig)), CV.os2ip(CV.after(32n, sig)), Bool.and(Bool.and(ES.scalar_ok(one, CV.os2ip(CV.first(32n, sig))), ES.scalar_ok(one, CV.os2ip(CV.after(32n, sig)))), Bool.or(Bool.not(strict), Bool.not(Nat.is_lt(FS.order(one), Nat.double(CV.os2ip(CV.after(32n, sig)))))))) : Bool} %Equal.sym(List<&2, U32>, CV.first(32n, sig), B.prefix(32n, sig), Equal.sym(List<&2, U32>, B.prefix(32n, sig), CV.first(32n, sig), BL.prefix_first(32n, sig))) : {E.verify_ok(q, E.hash_scalar(h), B.of_be(B.prefix(32n, sig)), B.of_be(B.suffix(32n, sig)), Bool.and(Bool.and(ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), ES.scalar_ok(one, FS.value(one, B.of_be(B.suffix(32n, sig))))), Bool.or(Bool.not(strict), Bool.not(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, B.of_be(B.suffix(32n, sig))))))))) == ES.verify_ok(one, PT.pv(one, q), FS.value(one, E.hash_scalar(h)), CV.os2ip(_), CV.os2ip(CV.after(32n, sig)), Bool.and(Bool.and(ES.scalar_ok(one, CV.os2ip(CV.first(32n, sig))), ES.scalar_ok(one, CV.os2ip(CV.after(32n, sig)))), Bool.or(Bool.not(strict), Bool.not(Nat.is_lt(FS.order(one), Nat.double(CV.os2ip(CV.after(32n, sig)))))))) : Bool} %Equal.sym(List<&2, U32>, CV.first(32n, sig), B.prefix(32n, sig), Equal.sym(List<&2, U32>, B.prefix(32n, sig), CV.first(32n, sig), BL.prefix_first(32n, sig))) : {E.verify_ok(q, E.hash_scalar(h), B.of_be(B.prefix(32n, sig)), B.of_be(B.suffix(32n, sig)), Bool.and(Bool.and(ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), ES.scalar_ok(one, FS.value(one, B.of_be(B.suffix(32n, sig))))), Bool.or(Bool.not(strict), Bool.not(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, B.of_be(B.suffix(32n, sig))))))))) == ES.verify_ok(one, PT.pv(one, q), FS.value(one, E.hash_scalar(h)), CV.os2ip(B.prefix(32n, sig)), CV.os2ip(CV.after(32n, sig)), Bool.and(Bool.and(ES.scalar_ok(one, CV.os2ip(_)), ES.scalar_ok(one, CV.os2ip(CV.after(32n, sig)))), Bool.or(Bool.not(strict), Bool.not(Nat.is_lt(FS.order(one), Nat.double(CV.os2ip(CV.after(32n, sig)))))))) : Bool} %Equal.sym(List<&2, U32>, CV.after(32n, sig), B.suffix(32n, sig), Equal.sym(List<&2, U32>, B.suffix(32n, sig), CV.after(32n, sig), BL.suffix_after(32n, sig))) : {E.verify_ok(q, E.hash_scalar(h), B.of_be(B.prefix(32n, sig)), B.of_be(B.suffix(32n, sig)), Bool.and(Bool.and(ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), ES.scalar_ok(one, FS.value(one, B.of_be(B.suffix(32n, sig))))), Bool.or(Bool.not(strict), Bool.not(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, B.of_be(B.suffix(32n, sig))))))))) == ES.verify_ok(one, PT.pv(one, q), FS.value(one, E.hash_scalar(h)), CV.os2ip(B.prefix(32n, sig)), CV.os2ip(_), Bool.and(Bool.and(ES.scalar_ok(one, CV.os2ip(B.prefix(32n, sig))), ES.scalar_ok(one, CV.os2ip(CV.after(32n, sig)))), Bool.or(Bool.not(strict), Bool.not(Nat.is_lt(FS.order(one), Nat.double(CV.os2ip(CV.after(32n, sig)))))))) : Bool} %Equal.sym(List<&2, U32>, CV.after(32n, sig), B.suffix(32n, sig), Equal.sym(List<&2, U32>, B.suffix(32n, sig), CV.after(32n, sig), BL.suffix_after(32n, sig))) : {E.verify_ok(q, E.hash_scalar(h), B.of_be(B.prefix(32n, sig)), B.of_be(B.suffix(32n, sig)), Bool.and(Bool.and(ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), ES.scalar_ok(one, FS.value(one, B.of_be(B.suffix(32n, sig))))), Bool.or(Bool.not(strict), Bool.not(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, B.of_be(B.suffix(32n, sig))))))))) == ES.verify_ok(one, PT.pv(one, q), FS.value(one, E.hash_scalar(h)), CV.os2ip(B.prefix(32n, sig)), CV.os2ip(B.suffix(32n, sig)), Bool.and(Bool.and(ES.scalar_ok(one, CV.os2ip(B.prefix(32n, sig))), ES.scalar_ok(one, CV.os2ip(_))), Bool.or(Bool.not(strict), Bool.not(Nat.is_lt(FS.order(one), Nat.double(CV.os2ip(CV.after(32n, sig)))))))) : Bool} %Equal.sym(List<&2, U32>, CV.after(32n, sig), B.suffix(32n, sig), Equal.sym(List<&2, U32>, B.suffix(32n, sig), CV.after(32n, sig), BL.suffix_after(32n, sig))) : {E.verify_ok(q, E.hash_scalar(h), B.of_be(B.prefix(32n, sig)), B.of_be(B.suffix(32n, sig)), Bool.and(Bool.and(ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), ES.scalar_ok(one, FS.value(one, B.of_be(B.suffix(32n, sig))))), Bool.or(Bool.not(strict), Bool.not(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, B.of_be(B.suffix(32n, sig))))))))) == ES.verify_ok(one, PT.pv(one, q), FS.value(one, E.hash_scalar(h)), CV.os2ip(B.prefix(32n, sig)), CV.os2ip(B.suffix(32n, sig)), Bool.and(Bool.and(ES.scalar_ok(one, CV.os2ip(B.prefix(32n, sig))), ES.scalar_ok(one, CV.os2ip(B.suffix(32n, sig)))), Bool.or(Bool.not(strict), Bool.not(Nat.is_lt(FS.order(one), Nat.double(CV.os2ip(_))))))) : Bool} %Equal.sym(Nat, CV.os2ip(B.prefix(32n, sig)), FS.value(one, B.of_be(B.prefix(32n, sig))), Equal.sym(Nat, FS.value(one, B.of_be(B.prefix(32n, sig))), CV.os2ip(B.prefix(32n, sig)), BY.of_be_value(one, h1, B.prefix(32n, sig)))) : {E.verify_ok(q, E.hash_scalar(h), B.of_be(B.prefix(32n, sig)), B.of_be(B.suffix(32n, sig)), Bool.and(Bool.and(ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), ES.scalar_ok(one, FS.value(one, B.of_be(B.suffix(32n, sig))))), Bool.or(Bool.not(strict), Bool.not(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, B.of_be(B.suffix(32n, sig))))))))) == ES.verify_ok(one, PT.pv(one, q), FS.value(one, E.hash_scalar(h)), _, CV.os2ip(B.suffix(32n, sig)), Bool.and(Bool.and(ES.scalar_ok(one, CV.os2ip(B.prefix(32n, sig))), ES.scalar_ok(one, CV.os2ip(B.suffix(32n, sig)))), Bool.or(Bool.not(strict), Bool.not(Nat.is_lt(FS.order(one), Nat.double(CV.os2ip(B.suffix(32n, sig)))))))) : Bool} %Equal.sym(Nat, CV.os2ip(B.prefix(32n, sig)), FS.value(one, B.of_be(B.prefix(32n, sig))), Equal.sym(Nat, FS.value(one, B.of_be(B.prefix(32n, sig))), CV.os2ip(B.prefix(32n, sig)), BY.of_be_value(one, h1, B.prefix(32n, sig)))) : {E.verify_ok(q, E.hash_scalar(h), B.of_be(B.prefix(32n, sig)), B.of_be(B.suffix(32n, sig)), Bool.and(Bool.and(ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), ES.scalar_ok(one, FS.value(one, B.of_be(B.suffix(32n, sig))))), Bool.or(Bool.not(strict), Bool.not(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, B.of_be(B.suffix(32n, sig))))))))) == ES.verify_ok(one, PT.pv(one, q), FS.value(one, E.hash_scalar(h)), FS.value(one, B.of_be(B.prefix(32n, sig))), CV.os2ip(B.suffix(32n, sig)), Bool.and(Bool.and(ES.scalar_ok(one, _), ES.scalar_ok(one, CV.os2ip(B.suffix(32n, sig)))), Bool.or(Bool.not(strict), Bool.not(Nat.is_lt(FS.order(one), Nat.double(CV.os2ip(B.suffix(32n, sig)))))))) : Bool} %Equal.sym(Nat, CV.os2ip(B.suffix(32n, sig)), FS.value(one, B.of_be(B.suffix(32n, sig))), Equal.sym(Nat, FS.value(one, B.of_be(B.suffix(32n, sig))), CV.os2ip(B.suffix(32n, sig)), BY.of_be_value(one, h1, B.suffix(32n, sig)))) : {E.verify_ok(q, E.hash_scalar(h), B.of_be(B.prefix(32n, sig)), B.of_be(B.suffix(32n, sig)), Bool.and(Bool.and(ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), ES.scalar_ok(one, FS.value(one, B.of_be(B.suffix(32n, sig))))), Bool.or(Bool.not(strict), Bool.not(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, B.of_be(B.suffix(32n, sig))))))))) == ES.verify_ok(one, PT.pv(one, q), FS.value(one, E.hash_scalar(h)), FS.value(one, B.of_be(B.prefix(32n, sig))), _, Bool.and(Bool.and(ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), ES.scalar_ok(one, CV.os2ip(B.suffix(32n, sig)))), Bool.or(Bool.not(strict), Bool.not(Nat.is_lt(FS.order(one), Nat.double(CV.os2ip(B.suffix(32n, sig)))))))) : Bool} %Equal.sym(Nat, CV.os2ip(B.suffix(32n, sig)), FS.value(one, B.of_be(B.suffix(32n, sig))), Equal.sym(Nat, FS.value(one, B.of_be(B.suffix(32n, sig))), CV.os2ip(B.suffix(32n, sig)), BY.of_be_value(one, h1, B.suffix(32n, sig)))) : {E.verify_ok(q, E.hash_scalar(h), B.of_be(B.prefix(32n, sig)), B.of_be(B.suffix(32n, sig)), Bool.and(Bool.and(ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), ES.scalar_ok(one, FS.value(one, B.of_be(B.suffix(32n, sig))))), Bool.or(Bool.not(strict), Bool.not(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, B.of_be(B.suffix(32n, sig))))))))) == ES.verify_ok(one, PT.pv(one, q), FS.value(one, E.hash_scalar(h)), FS.value(one, B.of_be(B.prefix(32n, sig))), FS.value(one, B.of_be(B.suffix(32n, sig))), Bool.and(Bool.and(ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), ES.scalar_ok(one, _)), Bool.or(Bool.not(strict), Bool.not(Nat.is_lt(FS.order(one), Nat.double(CV.os2ip(B.suffix(32n, sig)))))))) : Bool} %Equal.sym(Nat, CV.os2ip(B.suffix(32n, sig)), FS.value(one, B.of_be(B.suffix(32n, sig))), Equal.sym(Nat, FS.value(one, B.of_be(B.suffix(32n, sig))), CV.os2ip(B.suffix(32n, sig)), BY.of_be_value(one, h1, B.suffix(32n, sig)))) : {E.verify_ok(q, E.hash_scalar(h), B.of_be(B.prefix(32n, sig)), B.of_be(B.suffix(32n, sig)), Bool.and(Bool.and(ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), ES.scalar_ok(one, FS.value(one, B.of_be(B.suffix(32n, sig))))), Bool.or(Bool.not(strict), Bool.not(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, B.of_be(B.suffix(32n, sig))))))))) == ES.verify_ok(one, PT.pv(one, q), FS.value(one, E.hash_scalar(h)), FS.value(one, B.of_be(B.prefix(32n, sig))), FS.value(one, B.of_be(B.suffix(32n, sig))), Bool.and(Bool.and(ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), ES.scalar_ok(one, FS.value(one, B.of_be(B.suffix(32n, sig))))), Bool.or(Bool.not(strict), Bool.not(Nat.is_lt(FS.order(one), Nat.double(_)))))) : Bool} vok(one, h1, q, hm, E.hash_scalar(h), SQ.hash_r(one, h1, h, hh), B.of_be(B.prefix(32n, sig)), hlr, B.of_be(B.suffix(32n, sig)), hls, ES.scalar_ok(one, FS.value(one, B.of_be(B.prefix(32n, sig)))), ES.scalar_ok(one, FS.value(one, B.of_be(B.suffix(32n, sig)))), Bool.or(Bool.not(strict), Bool.not(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, B.of_be(B.suffix(32n, sig))))))), {==}, {==}) Uses (44): 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=Bool.not https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.or 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.double 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=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=is_high_s https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/penc.bend&name=mpred 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/proofs/crypto/secp256k1/point.bend&name=pv https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pscal.bend&name=hash_r https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pscal.bend&name=hash_v https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pscal.bend&name=scalar_ok_v https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pver.bend&name=vok 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=first 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/ecdsa.bend&name=hash_scalar https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/ecdsa.bend&name=scalar_ok https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/ecdsa.bend&name=verify_ok https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/ecdsa.bend&name=verify_q https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend&name=order 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/ecdsa.bend&name=hash_scalar https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/ecdsa.bend&name=scalar_ok https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/ecdsa.bend&name=verify_ok https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/ecdsa.bend&name=verify_q https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/point.bend&name=Point https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/scalar.bend&name=is_high