1	import Base
2	import ../curve25519/field.bend as F
3	import ../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
20	def 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
25	def 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)
30	def csub(+x: List<&2, U32>) -> List<&2, U32>:
31	  F.csub_fin(F.carry(F.addl(x, comp_l()), 0), x)
32	
33	def 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)
37	def 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	
45	def reduce(+bs: List<&2, U32>) -> List<&2, U32>:
46	  mac(X.bitlen(bs), bs, F.one(), F.zero())
47	
48	def 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
52	def lt_l(+x: List<&2, U32>) -> Bool:
53	  U32.is_eq(F.cr_out(F.carry(F.addl(x, comp_l()), 0)), 0)