def aff_v

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

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend as FS
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend as CV
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/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

38# (X / Z, Y / Z)
39def aff_v(+one: Nat, +h1: {one == 1n : Nat}, a: P.Point, +ha: {PT.pred(one, a) == True{} : Bool}) -> {av(one, P.to_affine(a)) == CV.to_affine(FS.prime(one), PT.pv(one, a)) : CV.SAffine}:
40  match a:
41    case P.Point{+x, +y, +z}:
42      +hx = rx(one, x, y, z, ha)
43      +hy = ry(one, x, y, z, ha)
44      +hz = rz(one, x, y, z, ha)
45      %Equal.sym(Nat, FS.value(one, F.mul(x, F.inv(z))), FS.mmul(FS.prime(one), FS.value(one, x), FS.value(one, F.inv(z))), FO.mul_v(one, h1, x, F.inv(z), hx, FP.inv_r(one, h1, z, hz))) : {CV.SAffine{_, FS.value(one, F.mul(y, F.inv(z)))} == CV.SAffine{FS.mmul(FS.prime(one), FS.value(one, x), FS.minv(FS.prime(one), FS.value(one, z))), FS.mmul(FS.prime(one), FS.value(one, y), FS.minv(FS.prime(one), FS.value(one, z)))} : CV.SAffine}
46      %Equal.sym(Nat, FS.value(one, F.mul(y, F.inv(z))), FS.mmul(FS.prime(one), FS.value(one, y), FS.value(one, F.inv(z))), FO.mul_v(one, h1, y, F.inv(z), hy, FP.inv_r(one, h1, z, hz))) : {CV.SAffine{FS.mmul(FS.prime(one), FS.value(one, x), FS.value(one, F.inv(z))), _} == CV.SAffine{FS.mmul(FS.prime(one), FS.value(one, x), FS.minv(FS.prime(one), FS.value(one, z))), FS.mmul(FS.prime(one), FS.value(one, y), FS.minv(FS.prime(one), FS.value(one, z)))} : CV.SAffine}
47      %Equal.sym(Nat, FS.value(one, F.inv(z)), FS.minv(FS.prime(one), FS.value(one, z)), FP.inv_v(one, h1, z, hz)) : {CV.SAffine{FS.mmul(FS.prime(one), FS.value(one, x), _), FS.mmul(FS.prime(one), FS.value(one, y), FS.value(one, F.inv(z)))} == CV.SAffine{FS.mmul(FS.prime(one), FS.value(one, x), FS.minv(FS.prime(one), FS.value(one, z))), FS.mmul(FS.prime(one), FS.value(one, y), FS.minv(FS.prime(one), FS.value(one, z)))} : CV.SAffine}
48      %Equal.sym(Nat, FS.value(one, F.inv(z)), FS.minv(FS.prime(one), FS.value(one, z)), FP.inv_v(one, h1, z, hz)) : {CV.SAffine{FS.mmul(FS.prime(one), FS.value(one, x), FS.minv(FS.prime(one), FS.value(one, z))), FS.mmul(FS.prime(one), FS.value(one, y), _)} == CV.SAffine{FS.mmul(FS.prime(one), FS.value(one, x), FS.minv(FS.prime(one), FS.value(one, z))), FS.mmul(FS.prime(one), FS.value(one, y), FS.minv(FS.prime(one), FS.value(one, z)))} : CV.SAffine}
49      {==}