def run_v

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

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

155def run_v(+one: Nat, +h1: {one == 1n : Nat}, +prog: List<&2, P.Op>, +rs: List<&2, List<&2, Nat>>, +h: {allred(one, rs) == True{} : Bool}) -> {vals(one, P.run(prog, rs)) == CV.run(FS.prime(one), cprog(prog), vals(one, rs)) : List<&2, Nat>}:
156  %Equal.sym(List<&2, List<&2, Nat>>, P.run(prog, rs), P.run_go(prog, rs), run_is(prog, rs)) : {vals(one, _) == CV.run(FS.prime(one), cprog(prog), vals(one, rs)) : List<&2, Nat>}
157  %Equal.sym(List<&2, Nat>, CV.run(FS.prime(one), cprog(prog), vals(one, rs)), CV.run_go(FS.prime(one), cprog(prog), vals(one, rs)), srun_is(FS.prime(one), cprog(prog), vals(one, rs))) : {vals(one, P.run_go(prog, rs)) == _ : List<&2, Nat>}
158  run_go_v(one, h1, prog, rs, h)