src/crypto/curve25519/field.bend

bend-collections-laws-crypto@1.0.0.0 · 316 lines · 44 definitions

1import Base
2
3# Arithmetic in GF(p), p = 2^255 - 19, for X25519 and Ed25519.
4#
5# A field element is a list of 32 U32 limbs, little-endian in radix 2^8:
6# value(a) = a0 + 2^8 a1 + ... + 2^248 a31 (spec/crypto/curve25519/field.bend).
7# Every operation returns a "tight" element: 32 limbs, each below 2^8, so
8# its value is below 2^256 (not necessarily below p; `freeze` gives the
9# canonical representative, which is also its 32-byte encoding).
10#
11# Only U32 addition, multiplication, subtraction and division/remainder by
12# the constant 256 (a shift and a mask after compilation) are used, and no
13# intermediate reaches 2^32 (proved: proofs/crypto/curve25519). The schoolbook
14# product of two tight elements has limbs below 32 * 255^2 < 2^21; folding
15# the high half by 2^256 == 38 (mod p) keeps them below 2^27; three carry
16# passes bring the result back to tight (TweetNaCl's car25519, in radix
17# 2^8; Fiat-Crypto's unsaturated-limb reduction, Erbsen et al. 2019).
18#
19# No function branches on a limb value: selection is arithmetic
20# (a * (1 - s) + b * s), list shapes are fixed (32 limbs), and exponents
21# are public. Bend has no timing model, so constant time is by
22# construction, not proved.
23
24# ---- limb lists ----
25
26# limbwise sum; the longer tail is kept
27def addl(xs: List<&2, U32>, ys: List<&2, U32>) -> List<&2, U32>:
28  match xs:
29    case Nil{}:
30      ys
31    case Con{x, xt}:
32      match ys:
33        case Nil{}:
34          Con{x, xt}
35        case Con{y, yt}:
36          Con{U32.add(x, y), addl(xt, yt)}
37
38# every limb times a
39def scal(+a: U32, ys: List<&2, U32>) -> List<&2, U32>:
40  match ys:
41    case Nil{}:
42      Nil{}
43    case Con{y, yt}:
44      Con{U32.mul(a, y), scal(a, yt)}
45
46# the product polynomial: conv(x :: xs, ys) = x ys + 2^8 conv(xs, ys)
47def conv(xs: List<&2, U32>, +ys: List<&2, U32>) -> List<&2, U32>:
48  match xs:
49    case Nil{}:
50      Nil{}
51    case Con{x, xt}:
52      addl(scal(x, ys), Con{0, conv(xt, ys)})
53
54def take(n: Nat, xs: List<&2, U32>) -> List<&2, U32>:
55  match n:
56    case 0n:
57      Nil{}
58    case 1n+m:
59      match xs:
60        case Nil{}:
61          Nil{}
62        case Con{x, xt}:
63          Con{x, take(m, xt)}
64
65def drop(n: Nat, xs: List<&2, U32>) -> List<&2, U32>:
66  match n:
67    case 0n:
68      xs
69    case 1n+m:
70      match xs:
71        case Nil{}:
72          Nil{}
73        case Con{x, xt}:
74          drop(m, xt)
75
76# ---- carries ----
77
78# limbs and the carry out of the top one
79type Cr is Data:
80  Cr{limbs: List<&2, U32>, out: U32}
81
82def cr_limbs(r: Cr) -> List<&2, U32>:
83  match r:
84    case Cr{a, c}:
85      a
86
87def cr_out(r: Cr) -> U32:
88  match r:
89    case Cr{a, c}:
90      c
91
92def carry_con(l: U32, r: Cr) -> Cr:
93  match r:
94    case Cr{a, c}:
95      Cr{Con{l, a}, c}
96
97# one carry pass: limbs below 2^8 and the carry out of the top limb
98def carry(xs: List<&2, U32>, c: U32) -> Cr:
99  match xs:
100    case Nil{}:
101      Cr{Nil{}, c}
102    case Con{h, t}:
103      +s = U32.add(h, c)
104      carry_con(U32.mod(s, 256), carry(t, U32.div(s, 256)))
105
106# add k to the lowest limb
107def add0(xs: List<&2, U32>, k: U32) -> List<&2, U32>:
108  match xs:
109    case Nil{}:
110      Nil{}
111    case Con{x, xt}:
112      Con{U32.add(x, k), xt}
113
114# carry, then fold the carry out back in: 2^256 == 38 (mod p)
115def pass_fin(r: Cr) -> List<&2, U32>:
116  match r:
117    case Cr{a, c}:
118      add0(a, U32.mul(38, c))
119
120def pass(xs: List<&2, U32>) -> List<&2, U32>:
121  pass_fin(carry(xs, 0))
122
123# 32 limbs below 2^27 to a tight element of the same value mod p
124def reduce(xs: List<&2, U32>) -> List<&2, U32>:
125  pass(pass(pass(xs)))
126
127# ---- constants ----
128
129def zero() -> List<&2, U32>:
130  [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,
131   0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
132
133def one() -> List<&2, U32>:
134  [1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,
135   0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
136
137# a small constant k < 2^8 as an element
138def small(k: U32) -> List<&2, U32>:
139  [k, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,
140   0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
141
142# 8p limbwise: every limb at least 2^10 - 8, so a + 8p - b never borrows
143def eight_p() -> List<&2, U32>:
144  [1896, 2040, 2040, 2040, 2040, 2040, 2040, 2040,
145   2040, 2040, 2040, 2040, 2040, 2040, 2040, 2040,
146   2040, 2040, 2040, 2040, 2040, 2040, 2040, 2040,
147   2040, 2040, 2040, 2040, 2040, 2040, 2040, 1016]
148
149# 2^256 - p = 2^255 + 19
150def comp_p() -> List<&2, U32>:
151  [19, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,
152   0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 128]
153
154# ---- field operations (tight in, tight out) ----
155
156# a + k - b limbwise
157def subl(xs: List<&2, U32>, ys: List<&2, U32>, ks: List<&2, U32>) -> List<&2, U32>:
158  match xs:
159    case Nil{}:
160      Nil{}
161    case Con{x, xt}:
162      match ys:
163        case Nil{}:
164          Nil{}
165        case Con{y, yt}:
166          match ks:
167            case Nil{}:
168              Nil{}
169            case Con{k, kt}:
170              Con{U32.sub(U32.add(x, k), y), subl(xt, yt, kt)}
171
172def add(a: List<&2, U32>, b: List<&2, U32>) -> List<&2, U32>:
173  reduce(addl(a, b))
174
175def sub(a: List<&2, U32>, b: List<&2, U32>) -> List<&2, U32>:
176  reduce(subl(a, b, eight_p()))
177
178# fold the product: low 32 limbs + 38 * high limbs
179def wide(+zs: List<&2, U32>) -> List<&2, U32>:
180  addl(take(32n, zs), scal(38, drop(32n, zs)))
181
182def mul(a: List<&2, U32>, +b: List<&2, U32>) -> List<&2, U32>:
183  reduce(wide(conv(a, b)))
184
185def sq(+a: List<&2, U32>) -> List<&2, U32>:
186  mul(a, a)
187
188# a * k for a constant k < 2^17
189def mul_small(a: List<&2, U32>, +k: U32) -> List<&2, U32>:
190  reduce(scal(k, a))
191
192def neg(a: List<&2, U32>) -> List<&2, U32>:
193  sub(zero(), a)
194
195# ---- selection (s is 0 or 1) ----
196
197# s == 0: a; s == 1: b; limbwise a * (1 - s) + b * s
198def select(+s: U32, xs: List<&2, U32>, ys: List<&2, U32>) -> List<&2, U32>:
199  match xs:
200    case Nil{}:
201      Nil{}
202    case Con{x, xt}:
203      match ys:
204        case Nil{}:
205          Nil{}
206        case Con{y, yt}:
207          Con{U32.add(U32.mul(x, U32.sub(1, s)), U32.mul(y, s)), select(s, xt, yt)}
208
209# ---- powers (public exponents) ----
210#
211# The loops take the base x first and inspect it before their counter, so
212# the proof checker never unfolds a fixed-count loop over an unknown base
213# (it keeps pow_ones(x, 249n, x) as a call until x is known).
214
215# acc^(2^n) * x^(2^n - 1): n steps of acc = acc^2 * x
216def pow_ones(+x: List<&2, U32>, n: Nat, acc: List<&2, U32>) -> List<&2, U32>:
217  match x:
218    case Nil{}:
219      acc
220    case Con{h, t}:
221      match n:
222        case 0n:
223          acc
224        case 1n+m:
225          pow_ones(x, m, mul(sq(acc), x))
226
227# one bit of a public exponent, most significant first: acc^2 (* x)
228def pow_bit(b: Bool, +x: List<&2, U32>, acc: List<&2, U32>) -> List<&2, U32>:
229  match b:
230    case True{}:
231      mul(sq(acc), x)
232    case False{}:
233      sq(acc)
234
235def pow_bits(+x: List<&2, U32>, bs: List<&2, Bool>, acc: List<&2, U32>) -> List<&2, U32>:
236  match x:
237    case Nil{}:
238      acc
239    case Con{h, t}:
240      match bs:
241        case Nil{}:
242          acc
243        case Con{b, bt}:
244          pow_bits(x, bt, pow_bit(b, x, acc))
245
246# x^(p - 2) = x^(2^255 - 21): 250 one bits (x, then 249 steps), then 0 1 0 1 1
247def inv(+x: List<&2, U32>) -> List<&2, U32>:
248  pow_bits(x, [False{}, True{}, False{}, True{}, True{}], pow_ones(x, 249n, x))
249
250# x^((p - 5) / 8) = x^(2^252 - 3): 250 one bits, then 0 1
251def pow_p58(+x: List<&2, U32>) -> List<&2, U32>:
252  pow_bits(x, [False{}, True{}], pow_ones(x, 249n, x))
253
254# ---- canonical form ----
255
256def csub_fin(r: Cr, x: List<&2, U32>) -> List<&2, U32>:
257  match r:
258    case Cr{s, c}:
259      select(c, x, s)
260
261# x - p when x >= p, else x (x tight): x + 2^256 - p carries out iff x >= p
262def csub(+x: List<&2, U32>) -> List<&2, U32>:
263  csub_fin(carry(addl(x, comp_p()), 0), x)
264
265# the canonical representative, below p: 2^256 < 3p
266def freeze(+x: List<&2, U32>) -> List<&2, U32>:
267  csub(csub(x))
268
269# ---- bytes ----
270
271# the 32-byte little-endian encoding of a canonical element is its limbs
272def to_bytes(+x: List<&2, U32>) -> List<&2, U32>:
273  freeze(x)
274
275# the last byte with its top bit cleared (RFC 7748 decodeUCoordinate)
276def mask_top(xs: List<&2, U32>) -> List<&2, U32>:
277  match xs:
278    case Nil{}:
279      Nil{}
280    case Con{x, xt}:
281      match xt:
282        case Nil{}:
283          Con{U32.and(x, 127), Nil{}}
284        case Con{y, yt}:
285          Con{x, mask_top(Con{y, yt})}
286
287# bytes to an element, bit 255 ignored
288def of_bytes(bs: List<&2, U32>) -> List<&2, U32>:
289  mask_top(bs)
290
291# the sum of the limbs (below 2^13 for 32 bytes); no early exit
292def sum_all(xs: List<&2, U32>, acc: U32) -> U32:
293  match xs:
294    case Nil{}:
295      acc
296    case Con{x, xt}:
297      sum_all(xt, U32.add(acc, x))
298
299# x == 0 in the field: every byte of the canonical form is 0
300def is_zero(+x: List<&2, U32>) -> Bool:
301  U32.is_eq(sum_all(freeze(x), 0), 0)
302
303# a == b in the field
304def eq(+a: List<&2, U32>, +b: List<&2, U32>) -> Bool:
305  is_zero(sub(a, b))
306
307# the parity of the canonical representative (RFC 8032 x_0)
308def low_bit(xs: List<&2, U32>) -> U32:
309  match xs:
310    case Nil{}:
311      0
312    case Con{l, lt}:
313      U32.and(l, 1)
314
315def parity(+x: List<&2, U32>) -> U32:
316  low_bit(freeze(x))