1 import 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 27 def 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 39 def 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) 47 def 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 54 def 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 65 def 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 79 type Cr is Data: 80 Cr{limbs: List<&2, U32>, out: U32} 81 82 def cr_limbs(r: Cr) -> List<&2, U32>: 83 match r: 84 case Cr{a, c}: 85 a 86 87 def cr_out(r: Cr) -> U32: 88 match r: 89 case Cr{a, c}: 90 c 91 92 def 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 98 def 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 107 def 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) 115 def pass_fin(r: Cr) -> List<&2, U32>: 116 match r: 117 case Cr{a, c}: 118 add0(a, U32.mul(38, c)) 119 120 def 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 124 def reduce(xs: List<&2, U32>) -> List<&2, U32>: 125 pass(pass(pass(xs))) 126 127 # ---- constants ---- 128 129 def 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 133 def 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 138 def 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 143 def 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 150 def 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 157 def 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 172 def add(a: List<&2, U32>, b: List<&2, U32>) -> List<&2, U32>: 173 reduce(addl(a, b)) 174 175 def 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 179 def wide(+zs: List<&2, U32>) -> List<&2, U32>: 180 addl(take(32n, zs), scal(38, drop(32n, zs))) 181 182 def mul(a: List<&2, U32>, +b: List<&2, U32>) -> List<&2, U32>: 183 reduce(wide(conv(a, b))) 184 185 def sq(+a: List<&2, U32>) -> List<&2, U32>: 186 mul(a, a) 187 188 # a * k for a constant k < 2^17 189 def mul_small(a: List<&2, U32>, +k: U32) -> List<&2, U32>: 190 reduce(scal(k, a)) 191 192 def 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 198 def 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 216 def 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) 228 def 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 235 def 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 247 def 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 251 def 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 256 def 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 262 def 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 266 def 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 272 def 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) 276 def 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 288 def 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 292 def 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 300 def is_zero(+x: List<&2, U32>) -> Bool: 301 U32.is_eq(sum_all(freeze(x), 0), 0) 302 303 # a == b in the field 304 def 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) 308 def 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 315 def parity(+x: List<&2, U32>) -> U32: 316 low_bit(freeze(x))