def padd_r

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

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

251def padd_r(+one: Nat, +h1: {one == 1n : Nat}, a: P.Point, b: P.Point, +ha: {pred(one, a) == True{} : Bool}, +hb: {pred(one, b) == True{} : Bool}) -> {pred(one, P.add(a, b)) == True{} : Bool}:
252  match a b:
253    case P.Point{+x1, +y1, +z1} P.Point{+x2, +y2, +z2}:
254      +hr = run_r(one, h1, P.add_prog(), [x1, y1, z1, x2, y2, z2, P.b3()], regs7(one, h1, x1, y1, z1, x2, y2, z2, ha, hb))
255      +rs = P.run(P.add_prog(), [x1, y1, z1, x2, y2, z2, P.b3()])
256      pr3(one, P.nth(33n, rs), P.nth(36n, rs), P.nth(39n, rs), nth_r(one, h1, 33n, rs, hr), nth_r(one, h1, 36n, rs, hr), nth_r(one, h1, 39n, rs, hr))