Pschn.vrs: 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 121-129 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=121&end_line=129

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/scalar.bend as S
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/scalarops.bend as SO
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/ptwo.bend as TW

def vrs(+one: Nat, +h1: {one == 1n : Nat}, +r: List<&2, Nat>, +hr: {FS.limbs16(one, 16n, r) == True{} : Bool}, +s: List<&2, Nat>, +hs: {FS.reduced(one, FS.order(one), s) == True{} : Bool}, +e: List<&2, Nat>, +he: {FS.reduced(one, FS.order(one), e) == True{} : Bool}, +pp: P.Point, +hp: {PT.pred(one, pp) == True{} : Bool}) -> {SC.verify_r(r, P.add(P.mul(s, P.g()), P.mul(S.neg(e), pp))) == SS.verify_rs(one, FS.value(one, r), FS.value(one, s), FS.value(one, e), PT.pv(one, pp)) : Bool}:
  +hn = SO.neg_r(one, h1, e, he)
  +hq = TW.two_r(one, h1, s, hs, S.neg(e), hn, pp, hp)
  %Equal.sym(Bool, SC.verify_r(r, P.add(P.mul(s, P.g()), P.mul(S.neg(e), pp))), SS.check_r(FS.value(one, r), CV.is_inf(PT.pv(one, P.add(P.mul(s, P.g()), P.mul(S.neg(e), pp)))), CV.to_affine(FS.prime(one), PT.pv(one, P.add(P.mul(s, P.g()), P.mul(S.neg(e), pp))))), vr(one, h1, r, hr, P.add(P.mul(s, P.g()), P.mul(S.neg(e), pp)), hq)) : {_ == SS.check_r(FS.value(one, r), CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, s), CV.g(one)), CV.pmul(FS.prime(one), FS.mneg(FS.order(one), FS.value(one, e)), PT.pv(one, pp)))), CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, s), CV.g(one)), CV.pmul(FS.prime(one), FS.mneg(FS.order(one), FS.value(one, e)), PT.pv(one, pp))))) : Bool}
  %Equal.sym(CV.SPoint, PT.pv(one, P.add(P.mul(s, P.g()), P.mul(S.neg(e), pp))), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, s), CV.g(one)), CV.pmul(FS.prime(one), FS.value(one, S.neg(e)), PT.pv(one, pp))), TW.two_v(one, h1, s, hs, S.neg(e), hn, pp, hp)) : {SS.check_r(FS.value(one, r), CV.is_inf(_), CV.to_affine(FS.prime(one), PT.pv(one, P.add(P.mul(s, P.g()), P.mul(S.neg(e), pp))))) == SS.check_r(FS.value(one, r), CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, s), CV.g(one)), CV.pmul(FS.prime(one), FS.mneg(FS.order(one), FS.value(one, e)), PT.pv(one, pp)))), CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, s), CV.g(one)), CV.pmul(FS.prime(one), FS.mneg(FS.order(one), FS.value(one, e)), PT.pv(one, pp))))) : Bool}
  %Equal.sym(CV.SPoint, PT.pv(one, P.add(P.mul(s, P.g()), P.mul(S.neg(e), pp))), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, s), CV.g(one)), CV.pmul(FS.prime(one), FS.value(one, S.neg(e)), PT.pv(one, pp))), TW.two_v(one, h1, s, hs, S.neg(e), hn, pp, hp)) : {SS.check_r(FS.value(one, r), CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, s), CV.g(one)), CV.pmul(FS.prime(one), FS.value(one, S.neg(e)), PT.pv(one, pp)))), CV.to_affine(FS.prime(one), _)) == SS.check_r(FS.value(one, r), CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, s), CV.g(one)), CV.pmul(FS.prime(one), FS.mneg(FS.order(one), FS.value(one, e)), PT.pv(one, pp)))), CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, s), CV.g(one)), CV.pmul(FS.prime(one), FS.mneg(FS.order(one), FS.value(one, e)), PT.pv(one, pp))))) : Bool}
  %Equal.sym(Nat, FS.value(one, S.neg(e)), FS.mneg(FS.order(one), FS.value(one, e)), SO.neg_v(one, h1, e, he)) : {SS.check_r(FS.value(one, r), CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, s), CV.g(one)), CV.pmul(FS.prime(one), _, PT.pv(one, pp)))), CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, s), CV.g(one)), CV.pmul(FS.prime(one), FS.value(one, S.neg(e)), PT.pv(one, pp))))) == SS.check_r(FS.value(one, r), CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, s), CV.g(one)), CV.pmul(FS.prime(one), FS.mneg(FS.order(one), FS.value(one, e)), PT.pv(one, pp)))), CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, s), CV.g(one)), CV.pmul(FS.prime(one), FS.mneg(FS.order(one), FS.value(one, e)), PT.pv(one, pp))))) : Bool}
  %Equal.sym(Nat, FS.value(one, S.neg(e)), FS.mneg(FS.order(one), FS.value(one, e)), SO.neg_v(one, h1, e, he)) : {SS.check_r(FS.value(one, r), CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, s), CV.g(one)), CV.pmul(FS.prime(one), FS.mneg(FS.order(one), FS.value(one, e)), PT.pv(one, pp)))), CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, s), CV.g(one)), CV.pmul(FS.prime(one), _, PT.pv(one, pp))))) == SS.check_r(FS.value(one, r), CV.is_inf(CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, s), CV.g(one)), CV.pmul(FS.prime(one), FS.mneg(FS.order(one), FS.value(one, e)), PT.pv(one, pp)))), CV.to_affine(FS.prime(one), CV.padd(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, s), CV.g(one)), CV.pmul(FS.prime(one), FS.mneg(FS.order(one), FS.value(one, e)), PT.pv(one, pp))))) : Bool}
  {==}

Uses (31):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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=Nat
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/point.bend&name=pred
  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=vr
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/ptwo.bend&name=two_r
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/ptwo.bend&name=two_v
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/scalarops.bend&name=neg_r
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/scalarops.bend&name=neg_v
  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=g
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend&name=is_inf
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend&name=padd
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend&name=pmul
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend&name=to_affine
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend&name=limbs16
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend&name=mneg
  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=reduced
  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=check_r
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/schnorr.bend&name=verify_rs
  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/point.bend&name=add
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/point.bend&name=g
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/point.bend&name=mul
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/scalar.bend&name=neg
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/schnorr.bend&name=verify_r