def run_is

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/point.bend:132

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

132# run looks at its first register first
133def 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>>}:
134  match rs:
135    case Nil{}:
136      {==}
137    case Nil{} <> t:
138      {==}
139    case (y <> u) <> t:
140      {==}