Point.run_is: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/point.bend as Point
Lines 132-140 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/point.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/point.bend&start_line=132&end_line=140

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/point.bend as P

# run looks at its first register first
def run_is(prog: List<&2, P.Op>, rs: List<&2, List<&2, Nat>>) -> {P.run(prog, rs) == P.run_go(prog, rs) : List<&2, List<&2, Nat>>}:
  match rs:
    case Nil{}:
      {==}
    case Nil{} <> t:
      {==}
    case (y <> u) <> t:
      {==}

Uses (5):
  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/src/crypto/secp256k1/point.bend&name=Op
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/point.bend&name=run
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/point.bend&name=run_go