1 # GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/paff.src; edit the .src 2 import Base 3 import ../../../spec/crypto/secp256k1/field.bend as FS 4 import ../../../spec/crypto/secp256k1/curve.bend as CV 5 import ../../../src/crypto/secp256k1/field.bend as F 6 import ../../../src/crypto/secp256k1/point.bend as P 7 import ../../lib/logic.bend as Lg 8 import ./fieldops.bend as FO 9 import ./fieldpow.bend as FP 10 import ./fwrap.bend as FW 11 import ./point.bend as PT 12 import ./sel.bend as PM 13 import ./lits.bend as LT 14 15 # Affine coordinates, the point-at-infinity test and the generator of 16 # src/crypto/secp256k1/point.bend against spec/crypto/secp256k1/curve.bend. 17 18 def av(+one: Nat, a: P.Affine) -> CV.SAffine: 19 match a: 20 case P.Affine{x, y}: CV.SAffine{FS.value(one, x), FS.value(one, y)} 21 22 def ared(+one: Nat, a: P.Affine) -> Bool: 23 match a: 24 case P.Affine{x, y}: Bool.and(PT.red(one, x), PT.red(one, y)) 25 26 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}: 27 h 28 29 def 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}: 30 Lg.and_left(PT.red(one, x), Bool.and(PT.red(one, y), PT.red(one, z)), h) 31 32 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}: 33 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)) 34 35 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}: 36 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)) 37 38 # (X / Z, Y / Z) 39 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}: 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 {==} 50 51 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}: 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)) 59 60 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}: 61 match a: 62 case P.Point{+x, +y, +z}: 63 FW.is_zero_f(one, h1, z) 64 65 # ---- the generator ---- 66 67 def gx_l(+one: Nat, +h1: {one == 1n : Nat}) -> {FS.limbs16(one, 16n, P.gx()) == True{} : Bool}: 68 LT.lits16(one, h1, 16n, P.gx(), {==}) 69 70 def gy_l(+one: Nat, +h1: {one == 1n : Nat}) -> {FS.limbs16(one, 16n, P.gy()) == True{} : Bool}: 71 LT.lits16(one, h1, 16n, P.gy(), {==}) 72 73 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}: 74 +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) 75 Lg.and_intro(FS.limbs16(one, 16n, x), Nat.is_lt(FS.value(one, x), FS.prime(one)), hl, hv) 76 77 def g_r(+one: Nat, +h1: {one == 1n : Nat}) -> {PT.pred(one, P.g()) == True{} : Bool}: 78 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))) 79 80 def g_v(+one: Nat, +h1: {one == 1n : Nat}) -> {PT.pv(one, P.g()) == CV.g(one) : CV.SPoint}: 81 %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} 82 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))