def srun_is

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

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

142def srun_is(+p: Nat, prog: List<&2, CV.SOp>, rs: List<&2, Nat>) -> {CV.run(p, prog, rs) == CV.run_go(p, prog, rs) : List<&2, Nat>}:
143  match rs:
144    case Nil{}:
145      {==}
146    case 0n <> t:
147      {==}
148    case (1n+k) <> t:
149      {==}