1	import Base
2	import ./field.bend as F
3	
4	# X25519 (RFC 7748 section 5): the Montgomery ladder on Curve25519 over the
5	# field of field.bend. Scalars and u-coordinates are 32-byte little-endian
6	# lists (U32 values below 256); implementation == the RFC's pseudo-code
7	# (spec/crypto/curve25519/x25519.bend) is proved for every input.
8	#
9	# The ladder runs the same operations for every scalar: the conditional
10	# swap is arithmetic selection (field.bend `select`) driven by bit masks,
11	# bit t of the scalar is read at a public position, and the loop count is
12	# fixed (255). Bend has no timing model: this is branch-free by
13	# construction, not proved constant-time.
14	
15	type St is Data:
16	  St{x2: List<&2, U32>, z2: List<&2, U32>, x3: List<&2, U32>, z3: List<&2, U32>, swap: U32}
17	
18	# bit t of a little-endian byte string
19	def kbit(bs: List<&2, U32>, t: Nat) -> U32:
20	  match bs:
21	    case Nil{}:
22	      0
23	    case Con{b, bt}:
24	      match t:
25	        case 0n:
26	          U32.and(b, 1)
27	        case 1n:
28	          U32.and(U32.shrn(b, 1n), 1)
29	        case 2n:
30	          U32.and(U32.shrn(b, 2n), 1)
31	        case 3n:
32	          U32.and(U32.shrn(b, 3n), 1)
33	        case 4n:
34	          U32.and(U32.shrn(b, 4n), 1)
35	        case 5n:
36	          U32.and(U32.shrn(b, 5n), 1)
37	        case 6n:
38	          U32.and(U32.shrn(b, 6n), 1)
39	        case 7n:
40	          U32.and(U32.shrn(b, 7n), 1)
41	        case 8n+q:
42	          kbit(bt, q)
43	
44	# RFC 7748 decodeScalar25519's clamping: k[0] &= 248, k[31] &= 127, k[31] |= 64
45	def clamp_top(xs: List<&2, U32>) -> List<&2, U32>:
46	  match xs:
47	    case Nil{}:
48	      Nil{}
49	    case Con{x, xt}:
50	      match xt:
51	        case Nil{}:
52	          Con{U32.or(U32.and(x, 127), 64), Nil{}}
53	        case Con{y, yt}:
54	          Con{x, clamp_top(Con{y, yt})}
55	
56	def clamp(bs: List<&2, U32>) -> List<&2, U32>:
57	  match bs:
58	    case Nil{}:
59	      Nil{}
60	    case Con{b, bt}:
61	      clamp_top(Con{U32.and(b, 248), bt})
62	
63	# a24 = 121665 as a field element
64	def a24() -> List<&2, U32>:
65	  [65, 219, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,
66	   0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
67	
68	# one ladder step on the swapped pair (x2 : z2), (x3 : z3); c24 is a24
69	def step(+c24: List<&2, U32>, +x1: List<&2, U32>, +x2: List<&2, U32>, +z2: List<&2, U32>, +x3: List<&2, U32>, +z3: List<&2, U32>, kt: U32) -> St:
70	  +a = F.add(x2, z2)
71	  +aa = F.sq(a)
72	  +b = F.sub(x2, z2)
73	  +bb = F.sq(b)
74	  +e = F.sub(aa, bb)
75	  +c = F.add(x3, z3)
76	  +d = F.sub(x3, z3)
77	  +da = F.mul(d, a)
78	  +cb = F.mul(c, b)
79	  St{F.mul(aa, bb), F.mul(e, F.add(aa, F.mul(e, c24))), F.sq(F.add(da, cb)), F.mul(x1, F.sq(F.sub(da, cb))), kt}
80	
81	# swap ^= k_t; cswap; the step; swap = k_t
82	def rung(+c24: List<&2, U32>, +x1: List<&2, U32>, st: St, +kt: U32) -> St:
83	  match st:
84	    case St{+x2, +z2, +x3, +z3, swap}:
85	      +sw = U32.xor(swap, kt)
86	      step(c24, x1, F.select(sw, x2, x3), F.select(sw, z2, z3), F.select(sw, x3, x2), F.select(sw, z3, z2), kt)
87	
88	# the ladder's bit count, 8 len(k) - 1: 255 for a 32-byte scalar (RFC 7748
89	# `bits`). Taken from the scalar, it keeps the proof checker from unfolding
90	# the 255 steps for an unknown scalar.
91	def len(xs: List<&2, U32>) -> Nat:
92	  match xs:
93	    case Nil{}:
94	      0n
95	    case Con{x, xt}:
96	      1n+len(xt)
97	
98	# 8 len(xs), the bit count of a byte string
99	def bitlen(xs: List<&2, U32>) -> Nat:
100	  match xs:
101	    case Nil{}:
102	      0n
103	    case Con{x, xt}:
104	      Nat.add(8n, bitlen(xt))
105	
106	def nbits(+k: List<&2, U32>) -> Nat:
107	  Nat.sub(Nat.mul(8n, len(k)), 1n)
108	
109	# bits t = n - 1 down to 0
110	def ladder(n: Nat, +c24: List<&2, U32>, +k: List<&2, U32>, +x1: List<&2, U32>, st: St) -> St:
111	  match n:
112	    case 0n:
113	      st
114	    case 1n+ +t:
115	      ladder(t, c24, k, x1, rung(c24, x1, st, kbit(k, t)))
116	
117	# the final cswap, then x2 * z2^(p - 2), encoded
118	def finish(st: St) -> List<&2, U32>:
119	  match st:
120	    case St{+x2, +z2, +x3, +z3, +swap}:
121	      F.to_bytes(F.mul(F.select(swap, x2, x3), F.inv(F.select(swap, z2, z3))))
122	
123	# X25519 on two 32-byte strings of bytes below 256
124	def x25519_raw(+k: List<&2, U32>, u: List<&2, U32>) -> List<&2, U32>:
125	  +x1 = F.of_bytes(u)
126	  finish(ladder(nbits(k), a24(), clamp(k), x1, St{F.one(), F.zero(), x1, F.one(), 0}))
127	
128	# 32 values, each below 256
129	def valid_bytes(n: Nat, xs: List<&2, U32>) -> Bool:
130	  match n:
131	    case 0n:
132	      match xs:
133	        case Nil{}:
134	          True{}
135	        case Con{x, xt}:
136	          False{}
137	    case 1n+m:
138	      match xs:
139	        case Nil{}:
140	          False{}
141	        case Con{x, xt}:
142	          Bool.and(U32.is_lt(x, 256), valid_bytes(m, xt))
143	
144	def x25519_if(ok: Bool, k: List<&2, U32>, u: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
145	  match ok:
146	    case True{}:
147	      Some{x25519_raw(k, u)}
148	    case False{}:
149	      None{}
150	
151	# X25519(k, u); None unless both are 32 bytes below 256
152	def x25519(+k: List<&2, U32>, +u: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
153	  x25519_if(Bool.and(valid_bytes(32n, k), valid_bytes(32n, u)), k, u)
154	
155	# the base point u = 9
156	def base() -> List<&2, U32>:
157	  F.small(9)