def aff_r

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/paff.bend:51

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/field.bend as F
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/lib/logic.bend as Lg
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/fieldops.bend as FO
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/fieldpow.bend as FP
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/point.bend as PT

51def aff_r(+one: Nat, +h1: {one == 1n : Nat}, a: P.Point, +ha: {PT.pred(one, a) == True{} : Bool}) -> {ared(one, P.to_affine(a)) == True{} : Bool}:
52  match a:
53    case P.Point{+x, +y, +z}:
54      +hx = rx(one, x, y, z, ha)
55      +hy = ry(one, x, y, z, ha)
56      +hz = rz(one, x, y, z, ha)
57      +hi = FP.inv_r(one, h1, z, hz)
58      Lg.and_intro(PT.red(one, F.mul(x, F.inv(z))), PT.red(one, F.mul(y, F.inv(z))), FO.mul_r(one, h1, x, F.inv(z), hx, hi), FO.mul_r(one, h1, y, F.inv(z), hy, hi))