Ecdsa.verify_rs: def of bend-collections@1.0.0.0
Import: import bend-collections@1.0.0.0/spec/crypto/secp256k1/ecdsa.bend as Ecdsa
Lines 165-171 of bend-collections@1.0.0.0/spec/crypto/secp256k1/ecdsa.bend: https://jend.leeeet.dev/read.txt?path=bend-collections@1.0.0.0/spec/crypto/secp256k1/ecdsa.bend&start_line=165&end_line=171

import Base
import bend-collections@1.0.0.0/spec/crypto/secp256k1/field.bend as FS
import bend-collections@1.0.0.0/spec/crypto/secp256k1/curve.bend as CV

# u1 = e s^-1, u2 = r s^-1, R = [u1] G + [u2] Q; valid when R is not the
# point at infinity and x(R) mod n = r
def verify_rs(+one: Nat, +q: CV.SPoint, +e: Nat, +r: Nat, +s: Nat) -> Bool:
  +m = n(one)
  +w = FS.minv(m, s)
  +rr = CV.padd(p(one), CV.pmul(p(one), FS.mmul(m, e, w), CV.g(one)), CV.pmul(p(one), FS.mmul(m, r, w), q))
  Bool.and(Bool.not(CV.is_inf(rr)), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(p(one), rr)), m), r))

Uses (17):
  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=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mod
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/spec/crypto/secp256k1/curve.bend&name=SPoint
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/spec/crypto/secp256k1/curve.bend&name=aff_x
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/spec/crypto/secp256k1/curve.bend&name=g
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/spec/crypto/secp256k1/curve.bend&name=is_inf
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/spec/crypto/secp256k1/curve.bend&name=padd
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/spec/crypto/secp256k1/curve.bend&name=pmul
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/spec/crypto/secp256k1/curve.bend&name=to_affine
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/spec/crypto/secp256k1/ecdsa.bend&name=n
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/spec/crypto/secp256k1/ecdsa.bend&name=p
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/spec/crypto/secp256k1/field.bend&name=minv
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/spec/crypto/secp256k1/field.bend&name=mmul