Ecdsa.finish: def of bend-collections@1.0.0.0
Import: import bend-collections@1.0.0.0/spec/crypto/secp256k1/ecdsa.bend as Ecdsa
Lines 95-106 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=95&end_line=106

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

# R = (x, y) = [k] G, r = x mod n, s = k^-1 (e + r d) mod n; r = 0 or
# s = 0 means another k. s > n / 2 (n is odd: n < 2 s) becomes n - s. The
# recovery id is (y mod 2) + 2 (x >= n), with its low bit flipped when s was
# replaced.
def finish(+one: Nat, +e: Nat, +d: Nat, +k: Nat, a: CV.SAffine) -> Attempt:
  match a:
    case CV.SAffine{+x, +y}:
      +m = n(one)
      +r = Nat.mod(x, m)
      +s = FS.mmul(m, FS.minv(m, k), FS.madd(m, e, FS.mmul(m, r, d)))
      +high = Nat.is_lt(m, Nat.double(s))
      finish_if(Bool.or(Nat.is_eq(r, 0n), Nat.is_eq(s, 0n)), cat(i2osp32(r), cat(i2osp32(low(high, m, s)), [U32.from_nat(Nat.add(ge2(Nat.is_lt(x, m)), flip(high, Nat.mod(y, 2n))))])))

Uses (21):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.or
  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=Base/base.bend&name=Nat.add
  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_eq
  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.from_nat
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/spec/crypto/secp256k1/curve.bend&name=SAffine
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/spec/crypto/secp256k1/ecdsa.bend&name=Attempt
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/spec/crypto/secp256k1/ecdsa.bend&name=cat
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/spec/crypto/secp256k1/ecdsa.bend&name=finish_if
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/spec/crypto/secp256k1/ecdsa.bend&name=flip
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/spec/crypto/secp256k1/ecdsa.bend&name=ge2
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/spec/crypto/secp256k1/ecdsa.bend&name=i2osp32
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/spec/crypto/secp256k1/ecdsa.bend&name=low
  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/field.bend&name=madd
  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