proofs/crypto/secp256k1/paff.bend source
proofs/crypto/secp256k1/paff.bend on the hub · documented module
# GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/paff.src; edit the .srcimport Baseimport ../../../spec/crypto/secp256k1/field.bend as FSimport ../../../spec/crypto/secp256k1/curve.bend as CVimport ../../../src/crypto/secp256k1/field.bend as Fimport ../../../src/crypto/secp256k1/point.bend as Pimport ../../lib/logic.bend as Lgimport ./fieldops.bend as FOimport ./fieldpow.bend as FPimport ./fwrap.bend as FWimport ./point.bend as PTimport ./sel.bend as PMimport ./lits.bend as LT# Affine coordinates, the point-at-infinity test and the generator of# src/crypto/secp256k1/point.bend against spec/crypto/secp256k1/curve.bend.def av(+one: Nat, a: P.Affine) -> CV.SAffine: match a: case P.Affine{x, y}: CV.SAffine{FS.value(one, x), FS.value(one, y)}def ared(+one: Nat, a: P.Affine) -> Bool: match a: case P.Affine{x, y}: Bool.and(PT.red(one, x), PT.red(one, y))def red3(+one: Nat, +x: List<&2, Nat>, +y: List<&2, Nat>, +z: List<&2, Nat>, +h: {PT.pred(one, P.Point{x, y, z}) == True{} : Bool}) -> {Bool.and(PT.red(one, x), Bool.and(PT.red(one, y), PT.red(one, z))) == True{} : Bool}: hdef rx(+one: Nat, +x: List<&2, Nat>, +y: List<&2, Nat>, +z: List<&2, Nat>, +h: {PT.pred(one, P.Point{x, y, z}) == True{} : Bool}) -> {PT.red(one, x) == True{} : Bool}: Lg.and_left(PT.red(one, x), Bool.and(PT.red(one, y), PT.red(one, z)), h)def ry(+one: Nat, +x: List<&2, Nat>, +y: List<&2, Nat>, +z: List<&2, Nat>, +h: {PT.pred(one, P.Point{x, y, z}) == True{} : Bool}) -> {PT.red(one, y) == True{} : Bool}: Lg.and_left(PT.red(one, y), PT.red(one, z), Lg.and_right(PT.red(one, x), Bool.and(PT.red(one, y), PT.red(one, z)), h))def rz(+one: Nat, +x: List<&2, Nat>, +y: List<&2, Nat>, +z: List<&2, Nat>, +h: {PT.pred(one, P.Point{x, y, z}) == True{} : Bool}) -> {PT.red(one, z) == True{} : Bool}: Lg.and_right(PT.red(one, y), PT.red(one, z), Lg.and_right(PT.red(one, x), Bool.and(PT.red(one, y), PT.red(one, z)), h))# (X / Z, Y / Z)def 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}: match a: case P.Point{+x, +y, +z}: +hx = rx(one, x, y, z, ha) +hy = ry(one, x, y, z, ha) +hz = rz(one, x, y, z, ha) %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} %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} %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} %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} {==}def 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}: match a: case P.Point{+x, +y, +z}: +hx = rx(one, x, y, z, ha) +hy = ry(one, x, y, z, ha) +hz = rz(one, x, y, z, ha) +hi = FP.inv_r(one, h1, z, hz) 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))def is_inf_v(+one: Nat, +h1: {one == 1n : Nat}, a: P.Point) -> {P.is_inf(a) == CV.is_inf(PT.pv(one, a)) : Bool}: match a: case P.Point{+x, +y, +z}: FW.is_zero_f(one, h1, z)# ---- the generator ----def gx_l(+one: Nat, +h1: {one == 1n : Nat}) -> {FS.limbs16(one, 16n, P.gx()) == True{} : Bool}: LT.lits16(one, h1, 16n, P.gx(), {==})def gy_l(+one: Nat, +h1: {one == 1n : Nat}) -> {FS.limbs16(one, 16n, P.gy()) == True{} : Bool}: LT.lits16(one, h1, 16n, P.gy(), {==})def lt_p_red(+one: Nat, +h1: {one == 1n : Nat}, +x: List<&2, Nat>, +hl: {FS.limbs16(one, 16n, x) == True{} : Bool}, +h: {F.lt_p(x) == True{} : Bool}) -> {PT.red(one, x) == True{} : Bool}: +hv = Equal.trans(Bool, Nat.is_lt(FS.value(one, x), FS.prime(one)), F.lt_p(x), True{}, Equal.sym(Bool, F.lt_p(x), Nat.is_lt(FS.value(one, x), FS.prime(one)), FW.lt_p_f(one, h1, x)), h) Lg.and_intro(FS.limbs16(one, 16n, x), Nat.is_lt(FS.value(one, x), FS.prime(one)), hl, hv)def g_r(+one: Nat, +h1: {one == 1n : Nat}) -> {PT.pred(one, P.g()) == True{} : Bool}: PT.pr3(one, P.gx(), P.gy(), F.one(), lt_p_red(one, h1, P.gx(), gx_l(one, h1), {==}), lt_p_red(one, h1, P.gy(), gy_l(one, h1), {==}), FO.small_r(one, h1, 1n, PM.one_lt(one, h1)))def g_v(+one: Nat, +h1: {one == 1n : Nat}) -> {PT.pv(one, P.g()) == CV.g(one) : CV.SPoint}: %Equal.sym(Nat, FS.value(one, F.small(1n)), 1n, FO.small_val(one, h1, 1n, PM.one_lt(one, h1))) : {CV.SPoint{FS.value(one, P.gx()), FS.value(one, P.gy()), _} == CV.g(one) : CV.SPoint} Equal.cong(Nat, CV.SPoint, z => CV.SPoint{FS.value(one, P.gx()), FS.value(one, P.gy()), z}, 1n, one, Equal.sym(Nat, one, 1n, h1))