Pschn.vp: def of bend-collections-laws-crypto@1.0.0.0 Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pschn.bend as Pschn Lines 152-172 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pschn.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pschn.bend&start_line=152&end_line=172 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/schnorr.bend as SS 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/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/schnorr.bend as SC 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 def vp(+one: Nat, +h1: {one == 1n : Nat}, +pk: List<&2, U32>, +m: List<&2, U32>, +sig: List<&2, U32>, +hsig: {B.has_len(64n, sig) == True{} : Bool}, mp: Maybe<&2, P.Point>, +hmp: {PE.mpred(one, mp) == True{} : Bool}) -> {SC.verify_p(pk, m, sig, mp) == SS.verify_p(one, pk, m, sig, PE.mpv(one, mp)) : Bool}: match mp: case None{}: {==} case Some{+pp}: +hlr = BY.of_be_limbs(one, h1, CV.first(32n, sig), BL.pre_len(32n, 32n, sig, hsig)) +hls = BY.of_be_limbs(one, h1, CV.after(32n, sig), BL.suf_len(32n, 32n, sig, hsig)) %Equal.sym(List<&2, U32>, B.prefix(32n, sig), CV.first(32n, sig), BL.prefix_first(32n, sig)) : {SC.verify_ok(B.of_be(_), B.of_be(B.suffix(32n, sig)), S.reduce(B.of_be(SC.tagged(SC.tag_challenge(), List.append(&2, U32, B.prefix(32n, sig), List.append(&2, U32, pk, m))))), pp, Bool.and(F.lt_p(B.of_be(B.prefix(32n, sig))), S.lt_n(B.of_be(B.suffix(32n, sig))))) == SS.verify_ok(one, CV.os2ip(CV.first(32n, sig)), CV.os2ip(CV.after(32n, sig)), Nat.mod(CV.os2ip(SS.tagged(SS.tag_challenge(), List.append(&2, U32, CV.first(32n, sig), List.append(&2, U32, pk, m)))), FS.order(one)), PT.pv(one, pp), Bool.and(Nat.is_lt(CV.os2ip(CV.first(32n, sig)), FS.prime(one)), Nat.is_lt(CV.os2ip(CV.after(32n, sig)), FS.order(one)))) : Bool} %Equal.sym(List<&2, U32>, B.prefix(32n, sig), CV.first(32n, sig), BL.prefix_first(32n, sig)) : {SC.verify_ok(B.of_be(CV.first(32n, sig)), B.of_be(B.suffix(32n, sig)), S.reduce(B.of_be(SC.tagged(SC.tag_challenge(), List.append(&2, U32, _, List.append(&2, U32, pk, m))))), pp, Bool.and(F.lt_p(B.of_be(B.prefix(32n, sig))), S.lt_n(B.of_be(B.suffix(32n, sig))))) == SS.verify_ok(one, CV.os2ip(CV.first(32n, sig)), CV.os2ip(CV.after(32n, sig)), Nat.mod(CV.os2ip(SS.tagged(SS.tag_challenge(), List.append(&2, U32, CV.first(32n, sig), List.append(&2, U32, pk, m)))), FS.order(one)), PT.pv(one, pp), Bool.and(Nat.is_lt(CV.os2ip(CV.first(32n, sig)), FS.prime(one)), Nat.is_lt(CV.os2ip(CV.after(32n, sig)), FS.order(one)))) : Bool} %Equal.sym(List<&2, U32>, B.prefix(32n, sig), CV.first(32n, sig), BL.prefix_first(32n, sig)) : {SC.verify_ok(B.of_be(CV.first(32n, sig)), B.of_be(B.suffix(32n, sig)), S.reduce(B.of_be(SC.tagged(SC.tag_challenge(), List.append(&2, U32, CV.first(32n, sig), List.append(&2, U32, pk, m))))), pp, Bool.and(F.lt_p(B.of_be(_)), S.lt_n(B.of_be(B.suffix(32n, sig))))) == SS.verify_ok(one, CV.os2ip(CV.first(32n, sig)), CV.os2ip(CV.after(32n, sig)), Nat.mod(CV.os2ip(SS.tagged(SS.tag_challenge(), List.append(&2, U32, CV.first(32n, sig), List.append(&2, U32, pk, m)))), FS.order(one)), PT.pv(one, pp), Bool.and(Nat.is_lt(CV.os2ip(CV.first(32n, sig)), FS.prime(one)), Nat.is_lt(CV.os2ip(CV.after(32n, sig)), FS.order(one)))) : Bool} %Equal.sym(List<&2, U32>, B.suffix(32n, sig), CV.after(32n, sig), BL.suffix_after(32n, sig)) : {SC.verify_ok(B.of_be(CV.first(32n, sig)), B.of_be(_), S.reduce(B.of_be(SC.tagged(SC.tag_challenge(), List.append(&2, U32, CV.first(32n, sig), List.append(&2, U32, pk, m))))), pp, Bool.and(F.lt_p(B.of_be(CV.first(32n, sig))), S.lt_n(B.of_be(B.suffix(32n, sig))))) == SS.verify_ok(one, CV.os2ip(CV.first(32n, sig)), CV.os2ip(CV.after(32n, sig)), Nat.mod(CV.os2ip(SS.tagged(SS.tag_challenge(), List.append(&2, U32, CV.first(32n, sig), List.append(&2, U32, pk, m)))), FS.order(one)), PT.pv(one, pp), Bool.and(Nat.is_lt(CV.os2ip(CV.first(32n, sig)), FS.prime(one)), Nat.is_lt(CV.os2ip(CV.after(32n, sig)), FS.order(one)))) : Bool} %Equal.sym(List<&2, U32>, B.suffix(32n, sig), CV.after(32n, sig), BL.suffix_after(32n, sig)) : {SC.verify_ok(B.of_be(CV.first(32n, sig)), B.of_be(CV.after(32n, sig)), S.reduce(B.of_be(SC.tagged(SC.tag_challenge(), List.append(&2, U32, CV.first(32n, sig), List.append(&2, U32, pk, m))))), pp, Bool.and(F.lt_p(B.of_be(CV.first(32n, sig))), S.lt_n(B.of_be(_)))) == SS.verify_ok(one, CV.os2ip(CV.first(32n, sig)), CV.os2ip(CV.after(32n, sig)), Nat.mod(CV.os2ip(SS.tagged(SS.tag_challenge(), List.append(&2, U32, CV.first(32n, sig), List.append(&2, U32, pk, m)))), FS.order(one)), PT.pv(one, pp), Bool.and(Nat.is_lt(CV.os2ip(CV.first(32n, sig)), FS.prime(one)), Nat.is_lt(CV.os2ip(CV.after(32n, sig)), FS.order(one)))) : Bool} %Equal.sym(List<&2, U32>, SC.tag_challenge(), SS.tag_challenge(), tc()) : {SC.verify_ok(B.of_be(CV.first(32n, sig)), B.of_be(CV.after(32n, sig)), S.reduce(B.of_be(SC.tagged(_, List.append(&2, U32, CV.first(32n, sig), List.append(&2, U32, pk, m))))), pp, Bool.and(F.lt_p(B.of_be(CV.first(32n, sig))), S.lt_n(B.of_be(CV.after(32n, sig))))) == SS.verify_ok(one, CV.os2ip(CV.first(32n, sig)), CV.os2ip(CV.after(32n, sig)), Nat.mod(CV.os2ip(SS.tagged(SS.tag_challenge(), List.append(&2, U32, CV.first(32n, sig), List.append(&2, U32, pk, m)))), FS.order(one)), PT.pv(one, pp), Bool.and(Nat.is_lt(CV.os2ip(CV.first(32n, sig)), FS.prime(one)), Nat.is_lt(CV.os2ip(CV.after(32n, sig)), FS.order(one)))) : Bool} %Equal.sym(Bool, F.lt_p(B.of_be(CV.first(32n, sig))), Nat.is_lt(FS.value(one, B.of_be(CV.first(32n, sig))), FS.prime(one)), FW.lt_p_f(one, h1, B.of_be(CV.first(32n, sig)))) : {SC.verify_ok(B.of_be(CV.first(32n, sig)), B.of_be(CV.after(32n, sig)), S.reduce(B.of_be(SC.tagged(SS.tag_challenge(), List.append(&2, U32, CV.first(32n, sig), List.append(&2, U32, pk, m))))), pp, Bool.and(_, S.lt_n(B.of_be(CV.after(32n, sig))))) == SS.verify_ok(one, CV.os2ip(CV.first(32n, sig)), CV.os2ip(CV.after(32n, sig)), Nat.mod(CV.os2ip(SS.tagged(SS.tag_challenge(), List.append(&2, U32, CV.first(32n, sig), List.append(&2, U32, pk, m)))), FS.order(one)), PT.pv(one, pp), Bool.and(Nat.is_lt(CV.os2ip(CV.first(32n, sig)), FS.prime(one)), Nat.is_lt(CV.os2ip(CV.after(32n, sig)), FS.order(one)))) : Bool} %Equal.sym(Bool, S.lt_n(B.of_be(CV.after(32n, sig))), Nat.is_lt(FS.value(one, B.of_be(CV.after(32n, sig))), FS.order(one)), FW.lt_n_s(one, h1, B.of_be(CV.after(32n, sig)))) : {SC.verify_ok(B.of_be(CV.first(32n, sig)), B.of_be(CV.after(32n, sig)), S.reduce(B.of_be(SC.tagged(SS.tag_challenge(), List.append(&2, U32, CV.first(32n, sig), List.append(&2, U32, pk, m))))), pp, Bool.and(Nat.is_lt(FS.value(one, B.of_be(CV.first(32n, sig))), FS.prime(one)), _)) == SS.verify_ok(one, CV.os2ip(CV.first(32n, sig)), CV.os2ip(CV.after(32n, sig)), Nat.mod(CV.os2ip(SS.tagged(SS.tag_challenge(), List.append(&2, U32, CV.first(32n, sig), List.append(&2, U32, pk, m)))), FS.order(one)), PT.pv(one, pp), Bool.and(Nat.is_lt(CV.os2ip(CV.first(32n, sig)), FS.prime(one)), Nat.is_lt(CV.os2ip(CV.after(32n, sig)), FS.order(one)))) : Bool} %Equal.sym(Nat, Nat.mod(CV.os2ip(SS.tagged(SS.tag_challenge(), List.append(&2, U32, CV.first(32n, sig), List.append(&2, U32, pk, m)))), FS.order(one)), FS.value(one, S.reduce(B.of_be(SC.tagged(SS.tag_challenge(), List.append(&2, U32, CV.first(32n, sig), List.append(&2, U32, pk, m)))))), Equal.sym(Nat, FS.value(one, S.reduce(B.of_be(SC.tagged(SS.tag_challenge(), List.append(&2, U32, CV.first(32n, sig), List.append(&2, U32, pk, m)))))), Nat.mod(CV.os2ip(SS.tagged(SS.tag_challenge(), List.append(&2, U32, CV.first(32n, sig), List.append(&2, U32, pk, m)))), FS.order(one)), th_v(one, h1, SS.tag_challenge(), List.append(&2, U32, CV.first(32n, sig), List.append(&2, U32, pk, m))))) : {SC.verify_ok(B.of_be(CV.first(32n, sig)), B.of_be(CV.after(32n, sig)), S.reduce(B.of_be(SC.tagged(SS.tag_challenge(), List.append(&2, U32, CV.first(32n, sig), List.append(&2, U32, pk, m))))), pp, Bool.and(Nat.is_lt(FS.value(one, B.of_be(CV.first(32n, sig))), FS.prime(one)), Nat.is_lt(FS.value(one, B.of_be(CV.after(32n, sig))), FS.order(one)))) == SS.verify_ok(one, CV.os2ip(CV.first(32n, sig)), CV.os2ip(CV.after(32n, sig)), _, PT.pv(one, pp), Bool.and(Nat.is_lt(CV.os2ip(CV.first(32n, sig)), FS.prime(one)), Nat.is_lt(CV.os2ip(CV.after(32n, sig)), FS.order(one)))) : Bool} %Equal.sym(Nat, CV.os2ip(CV.first(32n, sig)), FS.value(one, B.of_be(CV.first(32n, sig))), Equal.sym(Nat, FS.value(one, B.of_be(CV.first(32n, sig))), CV.os2ip(CV.first(32n, sig)), BY.of_be_value(one, h1, CV.first(32n, sig)))) : {SC.verify_ok(B.of_be(CV.first(32n, sig)), B.of_be(CV.after(32n, sig)), S.reduce(B.of_be(SC.tagged(SS.tag_challenge(), List.append(&2, U32, CV.first(32n, sig), List.append(&2, U32, pk, m))))), pp, Bool.and(Nat.is_lt(FS.value(one, B.of_be(CV.first(32n, sig))), FS.prime(one)), Nat.is_lt(FS.value(one, B.of_be(CV.after(32n, sig))), FS.order(one)))) == SS.verify_ok(one, _, CV.os2ip(CV.after(32n, sig)), FS.value(one, S.reduce(B.of_be(SC.tagged(SS.tag_challenge(), List.append(&2, U32, CV.first(32n, sig), List.append(&2, U32, pk, m)))))), PT.pv(one, pp), Bool.and(Nat.is_lt(CV.os2ip(CV.first(32n, sig)), FS.prime(one)), Nat.is_lt(CV.os2ip(CV.after(32n, sig)), FS.order(one)))) : Bool} %Equal.sym(Nat, CV.os2ip(CV.first(32n, sig)), FS.value(one, B.of_be(CV.first(32n, sig))), Equal.sym(Nat, FS.value(one, B.of_be(CV.first(32n, sig))), CV.os2ip(CV.first(32n, sig)), BY.of_be_value(one, h1, CV.first(32n, sig)))) : {SC.verify_ok(B.of_be(CV.first(32n, sig)), B.of_be(CV.after(32n, sig)), S.reduce(B.of_be(SC.tagged(SS.tag_challenge(), List.append(&2, U32, CV.first(32n, sig), List.append(&2, U32, pk, m))))), pp, Bool.and(Nat.is_lt(FS.value(one, B.of_be(CV.first(32n, sig))), FS.prime(one)), Nat.is_lt(FS.value(one, B.of_be(CV.after(32n, sig))), FS.order(one)))) == SS.verify_ok(one, FS.value(one, B.of_be(CV.first(32n, sig))), CV.os2ip(CV.after(32n, sig)), FS.value(one, S.reduce(B.of_be(SC.tagged(SS.tag_challenge(), List.append(&2, U32, CV.first(32n, sig), List.append(&2, U32, pk, m)))))), PT.pv(one, pp), Bool.and(Nat.is_lt(_, FS.prime(one)), Nat.is_lt(CV.os2ip(CV.after(32n, sig)), FS.order(one)))) : Bool} %Equal.sym(Nat, CV.os2ip(CV.after(32n, sig)), FS.value(one, B.of_be(CV.after(32n, sig))), Equal.sym(Nat, FS.value(one, B.of_be(CV.after(32n, sig))), CV.os2ip(CV.after(32n, sig)), BY.of_be_value(one, h1, CV.after(32n, sig)))) : {SC.verify_ok(B.of_be(CV.first(32n, sig)), B.of_be(CV.after(32n, sig)), S.reduce(B.of_be(SC.tagged(SS.tag_challenge(), List.append(&2, U32, CV.first(32n, sig), List.append(&2, U32, pk, m))))), pp, Bool.and(Nat.is_lt(FS.value(one, B.of_be(CV.first(32n, sig))), FS.prime(one)), Nat.is_lt(FS.value(one, B.of_be(CV.after(32n, sig))), FS.order(one)))) == SS.verify_ok(one, FS.value(one, B.of_be(CV.first(32n, sig))), _, FS.value(one, S.reduce(B.of_be(SC.tagged(SS.tag_challenge(), List.append(&2, U32, CV.first(32n, sig), List.append(&2, U32, pk, m)))))), PT.pv(one, pp), Bool.and(Nat.is_lt(FS.value(one, B.of_be(CV.first(32n, sig))), FS.prime(one)), Nat.is_lt(CV.os2ip(CV.after(32n, sig)), FS.order(one)))) : Bool} %Equal.sym(Nat, CV.os2ip(CV.after(32n, sig)), FS.value(one, B.of_be(CV.after(32n, sig))), Equal.sym(Nat, FS.value(one, B.of_be(CV.after(32n, sig))), CV.os2ip(CV.after(32n, sig)), BY.of_be_value(one, h1, CV.after(32n, sig)))) : {SC.verify_ok(B.of_be(CV.first(32n, sig)), B.of_be(CV.after(32n, sig)), S.reduce(B.of_be(SC.tagged(SS.tag_challenge(), List.append(&2, U32, CV.first(32n, sig), List.append(&2, U32, pk, m))))), pp, Bool.and(Nat.is_lt(FS.value(one, B.of_be(CV.first(32n, sig))), FS.prime(one)), Nat.is_lt(FS.value(one, B.of_be(CV.after(32n, sig))), FS.order(one)))) == SS.verify_ok(one, FS.value(one, B.of_be(CV.first(32n, sig))), FS.value(one, B.of_be(CV.after(32n, sig))), FS.value(one, S.reduce(B.of_be(SC.tagged(SS.tag_challenge(), List.append(&2, U32, CV.first(32n, sig), List.append(&2, U32, pk, m)))))), PT.pv(one, pp), Bool.and(Nat.is_lt(FS.value(one, B.of_be(CV.first(32n, sig))), FS.prime(one)), Nat.is_lt(_, FS.order(one)))) : Bool} vok(one, h1, B.of_be(CV.first(32n, sig)), hlr, B.of_be(CV.after(32n, sig)), hls, S.reduce(B.of_be(SC.tagged(SS.tag_challenge(), List.append(&2, U32, CV.first(32n, sig), List.append(&2, U32, pk, m))))), th_r(one, h1, SS.tag_challenge(), List.append(&2, U32, CV.first(32n, sig), List.append(&2, U32, pk, m))), pp, hmp, Nat.is_lt(FS.value(one, B.of_be(CV.first(32n, sig))), FS.prime(one)), Nat.is_lt(FS.value(one, B.of_be(CV.after(32n, sig))), FS.order(one)), {==}, {==}) Uses (47): 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=List.append 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=Nat.mod 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=pre_len 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=suf_len 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_n_s 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/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/pschn.bend&name=tc https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pschn.bend&name=th_r https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pschn.bend&name=th_v https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pschn.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/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=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/spec/crypto/secp256k1/schnorr.bend&name=tag_challenge https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/schnorr.bend&name=tagged https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/schnorr.bend&name=verify_ok https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/schnorr.bend&name=verify_p 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=Point https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/scalar.bend&name=lt_n https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/scalar.bend&name=reduce https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/schnorr.bend&name=tag_challenge https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/schnorr.bend&name=tagged https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/schnorr.bend&name=verify_ok https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/schnorr.bend&name=verify_p