src/crypto/ed25519/point.bend

bend-collections-laws-crypto@1.0.0.0 · 190 lines · 27 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/field.bend as F
3import bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/x25519.bend as X
4
5# edwards25519 points (RFC 8032 section 5.1): -x^2 + y^2 = 1 + d x^2 y^2
6# over GF(2^255 - 19), in extended homogeneous coordinates (X : Y : Z : T),
7# x = X / Z, y = Y / Z, x y = T / Z. Addition and doubling are the RFC's
8# formulas (section 5.1.4), encoding and decoding sections 5.1.2 and 5.1.3.
9# The curve constants are computed once from small integers by the proved
10# field operations and passed along (Cs).
11
12type Pt is Data:
13  Pt{x: List<&2, U32>, y: List<&2, U32>, z: List<&2, U32>, t: List<&2, U32>}
14
15# d = -121665 / 121666, 2 d, sqrt(-1) = 2^((p - 1) / 4)
16type Cs is Data:
17  Cs{d: List<&2, U32>, d2: List<&2, U32>, sqm1: List<&2, U32>}
18
19def c121665() -> List<&2, U32>:
20  [65, 219, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,
21   0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
22
23def c121666() -> List<&2, U32>:
24  [66, 219, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,
25   0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
26
27# 2^((p - 1) / 4), (p - 1) / 4 = 2^253 - 5: 250 one bits, then 0 1 1
28def pow_p14(+x: List<&2, U32>) -> List<&2, U32>:
29  F.pow_bits(x, [False{}, True{}, True{}], F.pow_ones(x, 249n, x))
30
31def cs_d(c: Cs) -> List<&2, U32>:
32  match c:
33    case Cs{d, d2, s}:
34      d
35
36def cs_d2(c: Cs) -> List<&2, U32>:
37  match c:
38    case Cs{d, d2, s}:
39      d2
40
41def cs_s(c: Cs) -> List<&2, U32>:
42  match c:
43    case Cs{d, d2, s}:
44      s
45
46# k itself; taking an input list xs keeps the proof checker from computing
47# with the constant k while xs is unknown (it would otherwise evaluate the
48# whole field arithmetic on constants whenever it compares two terms)
49def lit(xs: List<&2, U32>, k: List<&2, U32>) -> List<&2, U32>:
50  match xs:
51    case Nil{}:
52      k
53    case Con{h, t}:
54      k
55
56def cs_of(+d: List<&2, U32>, +xs: List<&2, U32>) -> Cs:
57  Cs{d, F.add(d, d), pow_p14(lit(xs, F.small(2)))}
58
59# the curve constants, computed (xs is any input, see lit)
60def consts(+xs: List<&2, U32>) -> Cs:
61  cs_of(F.mul(F.neg(lit(xs, c121665())), F.inv(lit(xs, c121666()))), xs)
62
63def identity() -> Pt:
64  Pt{F.zero(), F.one(), F.one(), F.zero()}
65
66# RFC 8032 5.1.4, addition
67def add(+c: Cs, p: Pt, q: Pt) -> Pt:
68  match p q:
69    case Pt{+x1, +y1, +z1, +t1} Pt{+x2, +y2, +z2, +t2}:
70      +a = F.mul(F.sub(y1, x1), F.sub(y2, x2))
71      +b = F.mul(F.add(y1, x1), F.add(y2, x2))
72      +cc = F.mul(F.mul(t1, cs_d2(c)), t2)
73      +dd = F.mul(F.add(z1, z1), z2)
74      +e = F.sub(b, a)
75      +f = F.sub(dd, cc)
76      +g = F.add(dd, cc)
77      +h = F.add(b, a)
78      Pt{F.mul(e, f), F.mul(g, h), F.mul(f, g), F.mul(e, h)}
79
80# RFC 8032 5.1.4, doubling
81def double(p: Pt) -> Pt:
82  match p:
83    case Pt{+x1, +y1, +z1, t1}:
84      +a = F.sq(x1)
85      +b = F.sq(y1)
86      +zz = F.sq(z1)
87      +cc = F.add(zz, zz)
88      +h = F.add(a, b)
89      +e = F.sub(h, F.sq(F.add(x1, y1)))
90      +g = F.sub(a, b)
91      +f = F.add(cc, g)
92      Pt{F.mul(e, f), F.mul(g, h), F.mul(f, g), F.mul(e, h)}
93
94# s == 0: p; s == 1: q
95def select(+s: U32, p: Pt, q: Pt) -> Pt:
96  match p q:
97    case Pt{x1, y1, z1, t1} Pt{x2, y2, z2, t2}:
98      Pt{F.select(s, x1, x2), F.select(s, y1, y2), F.select(s, z1, z2), F.select(s, t1, t2)}
99
100# [bits t = n - 1 .. 0 of bs] p added to 2^n q: double, add, select
101def smul(n: Nat, +c: Cs, +bs: List<&2, U32>, +p: Pt, q: Pt) -> Pt:
102  match n:
103    case 0n:
104      q
105    case 1n+ +t:
106      +q2 = double(q)
107      smul(t, c, bs, p, select(X.kbit(bs, t), q2, add(c, q2, p)))
108
109# [k] p for a byte-string scalar k
110def mul(+c: Cs, +k: List<&2, U32>, +p: Pt) -> Pt:
111  smul(X.bitlen(k), c, k, p, identity())
112
113# the last byte with bit 7 set to b (the canonical y has it clear)
114def set_top(xs: List<&2, U32>, +b: U32) -> List<&2, U32>:
115  match xs:
116    case Nil{}:
117      Nil{}
118    case Con{x, xt}:
119      match xt:
120        case Nil{}:
121          Con{U32.or(x, U32.shln(b, 7n)), Nil{}}
122        case Con{y, yt}:
123          Con{x, set_top(Con{y, yt}, b)}
124
125# RFC 8032 5.1.2
126def encode(p: Pt) -> List<&2, U32>:
127  match p:
128    case Pt{+x, +y, +z, t}:
129      +zi = F.inv(z)
130      set_top(F.to_bytes(F.mul(y, zi)), F.parity(F.mul(x, zi)))
131
132# y >= p: the carry of y + 2^256 - p is not 0
133def ge_p(+y: List<&2, U32>) -> Bool:
134  Bool.not(U32.is_eq(F.cr_out(F.carry(F.addl(y, F.comp_p()), 0)), 0))
135
136def dec_fin(+x: List<&2, U32>, +y: List<&2, U32>, +x0: U32, fail: Bool) -> Maybe<&2, Pt>:
137  match fail:
138    case True{}:
139      None{}
140    case False{}:
141      +x2 = F.select(U32.xor(F.parity(x), x0), x, F.neg(x))
142      Some{Pt{x2, y, F.one(), F.mul(x2, y)}}
143
144def dec_root(+c: Cs, +x: List<&2, U32>, +y: List<&2, U32>, +x0: U32, +u: List<&2, U32>, +vxx: List<&2, U32>, is_u: Bool, is_nu: Bool) -> Maybe<&2, Pt>:
145  match is_u:
146    case True{}:
147      dec_fin(x, y, x0, Bool.and(F.is_zero(x), U32.is_eq(x0, 1)))
148    case False{}:
149      match is_nu:
150        case True{}:
151          +x1 = F.mul(x, cs_s(c))
152          dec_fin(x1, y, x0, Bool.and(F.is_zero(x1), U32.is_eq(x0, 1)))
153        case False{}:
154          None{}
155
156def dec_y(+c: Cs, +y: List<&2, U32>, +x0: U32, bad: Bool) -> Maybe<&2, Pt>:
157  match bad:
158    case True{}:
159      None{}
160    case False{}:
161      +yy = F.sq(y)
162      +u = F.sub(yy, F.one())
163      +v = F.add(F.mul(cs_d(c), yy), F.one())
164      +v3 = F.mul(F.sq(v), v)
165      +v7 = F.mul(F.sq(v3), v)
166      +x = F.mul(F.mul(u, v3), F.pow_p58(F.mul(u, v7)))
167      +vxx = F.mul(v, F.sq(x))
168      dec_root(c, x, y, x0, u, vxx, F.eq(vxx, u), F.eq(vxx, F.neg(u)))
169
170# RFC 8032 5.1.3 on 32 bytes below 256
171def decode(+c: Cs, +bs: List<&2, U32>) -> Maybe<&2, Pt>:
172  +y = F.of_bytes(bs)
173  dec_y(c, y, X.kbit(bs, 255n), ge_p(y))
174
175# the same point: X1 Z2 == X2 Z1 and Y1 Z2 == Y2 Z1
176def equal(p: Pt, q: Pt) -> Bool:
177  match p q:
178    case Pt{+x1, +y1, +z1, t1} Pt{+x2, +y2, +z2, t2}:
179      Bool.and(F.eq(F.mul(x1, z2), F.mul(x2, z1)), F.eq(F.mul(y1, z2), F.mul(y2, z1)))
180
181# the base point: y = 4 / 5, x even
182def base_of(m: Maybe<&2, Pt>) -> Pt:
183  match m:
184    case None{}:
185      identity()
186    case Some{p}:
187      p
188
189def base(+c: Cs, +xs: List<&2, U32>) -> Pt:
190  base_of(decode(c, F.to_bytes(F.mul(lit(xs, F.small(4)), F.inv(lit(xs, F.small(5)))))))