def run
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/point.bend as Pointimport Base
50# The first register is looked at before the program runs, so that the
51# proof checker stops at once on unknown inputs (the result is run_go's).
52def run(prog: List<&2, Op>, regs: List<&2, List<&2, Nat>>) -> List<&2, List<&2, Nat>>:
53 match regs:
54 case Nil{}: run_go(prog, Nil{})
55 case Nil{} <> t: run_go(prog, Nil{} <> t)
56 case (y <> u) <> t: run_go(prog, (y <> u) <> t)
Uses (4)
Used by (9)
- bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/point:add
- bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/point:dbl
- bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/point:padd_r
- bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/point:padd_v
- bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/point:pdbl_r
- …