def pdbl_r

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

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

258def pdbl_r(+one: Nat, +h1: {one == 1n : Nat}, a: P.Point, +ha: {pred(one, a) == True{} : Bool}) -> {pred(one, P.dbl(a)) == True{} : Bool}:
259  match a:
260    case P.Point{+x, +y, +z}:
261      +hr = run_r(one, h1, P.dbl_prog(), [x, y, z, P.b3()], regs4(one, h1, x, y, z, ha))
262      +rs = P.run(P.dbl_prog(), [x, y, z, P.b3()])
263      pr3(one, P.nth(21n, rs), P.nth(18n, rs), P.nth(13n, rs), nth_r(one, h1, 21n, rs, hr), nth_r(one, h1, 18n, rs, hr), nth_r(one, h1, 13n, rs, hr))