src/crypto/ed25519/scalar.bend

bend-collections-laws-crypto@1.0.0.0 · 53 lines · 8 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# Scalars mod L = 2^252 + 27742317777372353535851937790883648493 (RFC 8032
6# section 5.1), as 32 tight limbs (the field element representation of
7# ../curve25519/field.bend), every value below L.
8#
9#   addm(a, b)          (a + b) mod L for a, b < L: the sum, then one
10#                       conditional subtraction of L (carry of a + 2^256 - L)
11#   mac(n, bs, s, acc)  acc 2^n + s * bits(n bits of bs, most significant
12#                       first) mod L: double, then add s or 0 by selection
13#   reduce(bs)          value(bs) mod L (a 64-byte SHA-512 digest, say)
14#   mul_add(k, s, r)    (r + k s) mod L
15#
16# Every step is the same for every value (selection, fixed bit counts from
17# the input's length): branch-free by construction.
18
19# L, little-endian bytes
20def ell() -> List<&2, U32>:
21  [237, 211, 245, 92, 26, 99, 18, 88, 214, 156, 247, 162, 222, 249, 222, 20,
22   0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 16]
23
24# 2^256 - L
25def comp_l() -> List<&2, U32>:
26  [19, 44, 10, 163, 229, 156, 237, 167, 41, 99, 8, 93, 33, 6, 33, 235,
27   255, 255, 255, 255, 255, 255, 255, 255, 255, 255, 255, 255, 255, 255, 255, 239]
28
29# x - L when x >= L, else x (x tight, x < 2 L)
30def csub(+x: List<&2, U32>) -> List<&2, U32>:
31  F.csub_fin(F.carry(F.addl(x, comp_l()), 0), x)
32
33def addm(a: List<&2, U32>, b: List<&2, U32>) -> List<&2, U32>:
34  csub(F.cr_limbs(F.carry(F.addl(a, b), 0)))
35
36# bits t = n - 1 down to 0 of bs: acc = 2 acc + bit s (mod L)
37def mac(n: Nat, +bs: List<&2, U32>, +s: List<&2, U32>, +acc: List<&2, U32>) -> List<&2, U32>:
38  match n:
39    case 0n:
40      acc
41    case 1n+ +t:
42      +a2 = addm(acc, acc)
43      mac(t, bs, s, addm(a2, F.select(X.kbit(bs, t), F.zero(), s)))
44
45def reduce(+bs: List<&2, U32>) -> List<&2, U32>:
46  mac(X.bitlen(bs), bs, F.one(), F.zero())
47
48def mul_add(+k: List<&2, U32>, +s: List<&2, U32>, r: List<&2, U32>) -> List<&2, U32>:
49  addm(mac(X.bitlen(k), k, s, F.zero()), r)
50
51# x < L: the carry of x + 2^256 - L is 0
52def lt_l(+x: List<&2, U32>) -> Bool:
53  U32.is_eq(F.cr_out(F.carry(F.addl(x, comp_l()), 0)), 0)