Point.exec_r: 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 72-79 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=72&end_line=79

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

def exec_r(+one: Nat, +h1: {one == 1n : Nat}, op: P.Op, +rs: List<&2, List<&2, Nat>>, +h: {allred(one, rs) == True{} : Bool}) -> {red(one, P.exec(op, rs)) == True{} : Bool}:
  match op:
    case P.OAdd{+i, +j}:
      FO.add_r(one, h1, P.nth(i, rs), P.nth(j, rs), nth_r(one, h1, i, rs, h), nth_r(one, h1, j, rs, h))
    case P.OSub{+i, +j}:
      FO.sub_r(one, h1, P.nth(i, rs), P.nth(j, rs), nth_r(one, h1, i, rs, h), nth_r(one, h1, j, rs, h))
    case P.OMul{+i, +j}:
      FO.mul_r(one, h1, P.nth(i, rs), P.nth(j, rs), nth_r(one, h1, i, rs, h), nth_r(one, h1, j, rs, h))

Uses (12):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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/proofs/crypto/secp256k1/fieldops.bend&name=add_r
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/fieldops.bend&name=mul_r
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/fieldops.bend&name=sub_r
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/point.bend&name=allred
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/point.bend&name=nth_r
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/point.bend&name=red
  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=exec
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/point.bend&name=nth