proofs/crypto/secp256k1/paff.bend
bend-collections-laws-crypto@1.0.0.0 · 82 lines · 14 definitions
1
2import Base
3import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend as FS
4import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend as CV
5import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/field.bend as F
6import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/point.bend as P
7import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as Lg
8import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/fieldops.bend as FO
9import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/fieldpow.bend as FP
10import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/fwrap.bend as FW
11import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/point.bend as PT
12import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/sel.bend as PM
13import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/lits.bend as LT
14
15
16
17
18def 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
22def 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
26def 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
29def 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
32def 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
35def 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
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 {==}
50
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))
59
60def 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
66
67def 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
70def 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
73def 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
77def 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
80def 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))