1	import Base
2	import ../lib/common.bend as C
3	import ./curve25519/field.bend as FS
4	import ./curve25519/x25519.bend as SX
5	import ./sha512.bend as SHA
6	import ../../src/crypto/ed25519/ed25519.bend as E
7	import ../../src/crypto/ed25519/scalar.bend as ESC
8	
9	# Ed25519, RFC 8032 section 5.1, over the natural numbers: a transcription
10	# of the RFC's encoding (5.1.2), decoding (5.1.3), point addition and
11	# doubling in extended coordinates (5.1.4), key generation (5.1.5),
12	# signing (5.1.6) and verification (5.1.7, the cofactorless equation
13	# [S]B == R + [k]A', with S < L required), every field operation mod p
14	# (FS.fadd, ...), every scalar mod L, the hash FIPS 180-4 SHA-512
15	# (spec/crypto/sha512.bend). Scalar multiplication is double-and-add over
16	# the scalar's bits, most significant first (HACL*'s Spec.Ed25519 fixes an
17	# algorithm in the same way). `one` is the symbolic 1 of
18	# spec/crypto/curve25519/field.bend: every constant above 2^13 is written
19	# with it (L, 121665, 121666).
20	#
21	#   clause             statement
22	#   Scalar.reduce      ESC.reduce(bs) has the value value(bs) mod L
23	#   Scalar.mul_add     ESC.mul_add(k, s, r) has the value (r + k s) mod L
24	#   Ed25519.public     the implementation's public key is public_key(seed)
25	#   Ed25519.sign       the implementation's signature is sign(seed, msg)
26	#   Ed25519.verify     the implementation's verdict is verify(pk, msg, sig)
27	
28	# ---- scalars ----
29	
30	# L = 2^252 + 27742317777372353535851937790883648493, little-endian bytes
31	def ell_bytes() -> List<&2, U32>:
32	  [237, 211, 245, 92, 26, 99, 18, 88, 214, 156, 247, 162, 222, 249, 222, 20,
33	   0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 16]
34	
35	def ell(+one: Nat) -> Nat:
36	  FS.uvalue(one, ell_bytes())
37	
38	# ---- the curve ----
39	
40	type EPt is Data:
41	  EPt{x: Nat, y: Nat, z: Nat, t: Nat}
42	
43	# d = -121665 / 121666
44	def dconst(+one: Nat, +p: Nat) -> Nat:
45	  FS.fmul(p, FS.fsub(p, 0n, FS.digits(one, [65n, 219n, 1n])), FS.finv(p, FS.digits(one, [66n, 219n, 1n])))
46	
47	# 2^((p - 1) / 4), a square root of -1
48	def sqm1(+p: Nat) -> Nat:
49	  FS.fpow(p, 2n, Nat.div(Nat.sub(p, 1n), 4n))
50	
51	def identity() -> EPt:
52	  EPt{0n, 1n, 1n, 0n}
53	
54	# 5.1.4: A = (Y1-X1)(Y2-X2), B = (Y1+X1)(Y2+X2), C = T1 2d T2, D = Z1 2 Z2,
55	# E = B-A, F = D-C, G = D+C, H = B+A, X3 = EF, Y3 = GH, T3 = EH, Z3 = FG
56	def add(+p: Nat, +d: Nat, a: EPt, b: EPt) -> EPt:
57	  match a b:
58	    case EPt{+x1, +y1, +z1, +t1} EPt{+x2, +y2, +z2, +t2}:
59	      +ea = FS.fmul(p, FS.fsub(p, y1, x1), FS.fsub(p, y2, x2))
60	      +eb = FS.fmul(p, FS.fadd(p, y1, x1), FS.fadd(p, y2, x2))
61	      +ec = FS.fmul(p, FS.fmul(p, t1, FS.fadd(p, d, d)), t2)
62	      +ed = FS.fmul(p, FS.fadd(p, z1, z1), z2)
63	      +ee = FS.fsub(p, eb, ea)
64	      +ef = FS.fsub(p, ed, ec)
65	      +eg = FS.fadd(p, ed, ec)
66	      +eh = FS.fadd(p, eb, ea)
67	      EPt{FS.fmul(p, ee, ef), FS.fmul(p, eg, eh), FS.fmul(p, ef, eg), FS.fmul(p, ee, eh)}
68	
69	# 5.1.4: A = X1^2, B = Y1^2, C = 2 Z1^2, H = A+B, E = H-(X1+Y1)^2, G = A-B,
70	# F = C+G, X3 = EF, Y3 = GH, T3 = EH, Z3 = FG
71	def double(+p: Nat, a: EPt) -> EPt:
72	  match a:
73	    case EPt{+x1, +y1, +z1, t1}:
74	      +ea = FS.fmul(p, x1, x1)
75	      +eb = FS.fmul(p, y1, y1)
76	      +zz = FS.fmul(p, z1, z1)
77	      +ec = FS.fadd(p, zz, zz)
78	      +eh = FS.fadd(p, ea, eb)
79	      +xy = FS.fadd(p, x1, y1)
80	      +ee = FS.fsub(p, eh, FS.fmul(p, xy, xy))
81	      +eg = FS.fsub(p, ea, eb)
82	      +ef = FS.fadd(p, ec, eg)
83	      EPt{FS.fmul(p, ee, ef), FS.fmul(p, eg, eh), FS.fmul(p, ef, eg), FS.fmul(p, ee, eh)}
84	
85	def pick(b: Nat, q: EPt, r: EPt) -> EPt:
86	  match b:
87	    case 0n:
88	      q
89	    case 1n+c:
90	      r
91	
92	# bits t = n - 1 .. 0 of k: q = 2 q, plus a on a one bit
93	def smul(+p: Nat, +d: Nat, n: Nat, +k: Nat, +a: EPt, q: EPt) -> EPt:
94	  match n:
95	    case 0n:
96	      q
97	    case 1n+ +t:
98	      +q2 = double(p, q)
99	      smul(p, d, t, k, a, pick(SX.kbit(k, t), q2, add(p, d, q2, a)))
100	
101	# [k] a for a scalar below 2^256: 256 bits, written 2^8 one (one == 1), so
102	# the proof checker never unrolls the loop
103	def mul(+one: Nat, +p: Nat, +d: Nat, +k: Nat, +a: EPt) -> EPt:
104	  smul(p, d, C.shift(8n, one), k, a, identity())
105	
106	# ---- encoding, 5.1.2 ----
107	
108	# the most significant bit of the final octet set to b
109	def set_msb(xs: List<&2, U32>, +b: U32) -> List<&2, U32>:
110	  match xs:
111	    case Nil{}:
112	      Nil{}
113	    case Con{x, xt}:
114	      match xt:
115	        case Nil{}:
116	          Con{U32.or(x, U32.shln(b, 7n)), Nil{}}
117	        case Con{y, yt}:
118	          Con{x, set_msb(Con{y, yt}, b)}
119	
120	# n = 32 bytes
121	def encode_n(n: Nat, +p: Nat, a: EPt) -> List<&2, U32>:
122	  match a:
123	    case EPt{+x, +y, +z, t}:
124	      +zi = FS.finv(p, z)
125	      set_msb(SX.le_bytes(n, FS.fmul(p, y, zi)), U32.from_nat(Nat.mod(FS.fmul(p, x, zi), 2n)))
126	
127	# 32 bytes, written 2^5 one (one == 1): the byte count stays symbolic, so the
128	# checker never expands an encoding (and the SHA-512 over it) into bytes
129	def encode(+one: Nat, +p: Nat, a: EPt) -> List<&2, U32>:
130	  encode_n(C.shift(5n, one), p, a)
131	
132	# ---- decoding, 5.1.3 ----
133	
134	def dec_fin(+p: Nat, +x: Nat, +y: Nat, +x0: Nat, fail: Bool) -> Maybe<&2, EPt>:
135	  match fail:
136	    case True{}:
137	      None{}
138	    case False{}:
139	      +x2 = SX.cs_fst(SX.bxor(Nat.mod(x, 2n), x0), x, FS.fsub(p, 0n, x))
140	      Some{EPt{x2, y, 1n, FS.fmul(p, x2, y)}}
141	
142	def dec_root(+p: Nat, +x: Nat, +y: Nat, +x0: Nat, is_u: Bool, is_nu: Bool) -> Maybe<&2, EPt>:
143	  match is_u:
144	    case True{}:
145	      dec_fin(p, x, y, x0, Bool.and(Nat.is_eq(x, 0n), Nat.is_eq(x0, 1n)))
146	    case False{}:
147	      match is_nu:
148	        case True{}:
149	          +x1 = FS.fmul(p, x, sqm1(p))
150	          dec_fin(p, x1, y, x0, Bool.and(Nat.is_eq(x1, 0n), Nat.is_eq(x0, 1n)))
151	        case False{}:
152	          None{}
153	
154	# u = y^2 - 1, v = d y^2 + 1, x = u v^3 (u v^7)^((p-5)/8); x or x sqrt(-1)
155	# when v x^2 is u or -u; fail when x = 0 and x_0 = 1; x = p - x (here as
156	# -x mod p) when x mod 2 != x_0
157	def dec_y(+p: Nat, +d: Nat, +y: Nat, +x0: Nat, bad: Bool) -> Maybe<&2, EPt>:
158	  match bad:
159	    case True{}:
160	      None{}
161	    case False{}:
162	      +yy = FS.fmul(p, y, y)
163	      +u = FS.fsub(p, yy, 1n)
164	      +v = FS.fadd(p, FS.fmul(p, d, yy), 1n)
165	      +v3 = FS.fmul(p, FS.fmul(p, v, v), v)
166	      +v7 = FS.fmul(p, FS.fmul(p, v3, v3), v)
167	      +x = FS.fmul(p, FS.fmul(p, u, v3), FS.fpow(p, FS.fmul(p, u, v7), Nat.div(Nat.sub(p, 5n), 8n)))
168	      +vxx = FS.fmul(p, v, FS.fmul(p, x, x))
169	      dec_root(p, x, y, x0, Nat.is_eq(vxx, u), Nat.is_eq(vxx, FS.fsub(p, 0n, u)))
170	
171	# bit 255 is x_0; the rest is y, rejected when y >= p
172	def decode(+p: Nat, +d: Nat, +bs: List<&2, U32>) -> Maybe<&2, EPt>:
173	  +y = FS.value(SX.mask_last(bs))
174	  dec_y(p, d, y, SX.kbit(FS.value(bs), 255n), Bool.not(Nat.is_lt(y, p)))
175	
176	# ---- the base point: y = 4/5, x even ----
177	
178	def base_of(m: Maybe<&2, EPt>) -> EPt:
179	  match m:
180	    case None{}:
181	      identity()
182	    case Some{a}:
183	      a
184	
185	def base(+p: Nat, +d: Nat) -> EPt:
186	  base_of(decode(p, d, SX.le_bytes(32n, FS.fmul(p, 4n, FS.finv(p, 5n)))))
187	
188	# the same point: X1 Z2 == X2 Z1 and Y1 Z2 == Y2 Z1
189	def equal(+p: Nat, a: EPt, b: EPt) -> Bool:
190	  match a b:
191	    case EPt{+x1, +y1, +z1, t1} EPt{+x2, +y2, +z2, t2}:
192	      Bool.and(Nat.is_eq(FS.fmul(p, x1, z2), FS.fmul(p, x2, z1)), Nat.is_eq(FS.fmul(p, y1, z2), FS.fmul(p, y2, z1)))
193	
194	# ---- bytes ----
195	
196	def first(n: Nat, xs: List<&2, U32>) -> List<&2, U32>:
197	  match n:
198	    case 0n:
199	      Nil{}
200	    case 1n+m:
201	      match xs:
202	        case Nil{}:
203	          Nil{}
204	        case Con{x, xt}:
205	          Con{x, first(m, xt)}
206	
207	def rest(n: Nat, xs: List<&2, U32>) -> List<&2, U32>:
208	  match n:
209	    case 0n:
210	      xs
211	    case 1n+m:
212	      match xs:
213	        case Nil{}:
214	          Nil{}
215	        case Con{x, xt}:
216	          rest(m, xt)
217	
218	def cat(xs: List<&2, U32>, ys: List<&2, U32>) -> List<&2, U32>:
219	  match xs:
220	    case Nil{}:
221	      ys
222	    case Con{x, xt}:
223	      Con{x, cat(xt, ys)}
224	
225	# k = SHA-512(R || A || M) mod L; a function of R first, so a comparison of
226	# two such terms compares R, A and M once instead of walking the digest
227	def hram(+one: Nat, rb: List<&2, U32>, +a: List<&2, U32>, +msg: List<&2, U32>) -> Nat:
228	  match rb:
229	    case Nil{}:
230	      Nat.mod(FS.value(SHA.sha512_bytes(cat(Nil{}, cat(a, msg)))), ell(one))
231	    case Con{x, xt}:
232	      Nat.mod(FS.value(SHA.sha512_bytes(cat(Con{x, xt}, cat(a, msg)))), ell(one))
233	
234	# ---- 5.1.5 key generation ----
235	
236	def secret(+h: List<&2, U32>) -> Nat:
237	  FS.value(SX.clamp(first(32n, h)))
238	
239	def public_body(+one: Nat, +p: Nat, +d: Nat, +h: List<&2, U32>) -> List<&2, U32>:
240	  encode(one, p, mul(one, p, d, secret(h), base(p, d)))
241	
242	# the same, a function of d first (d = dconst(one, p) is symbolic, so the
243	# checker keeps it a call instead of expanding it on every comparison)
244	def public_of(+one: Nat, +p: Nat, d: Nat, +h: List<&2, U32>) -> List<&2, U32>:
245	  match d:
246	    case 0n:
247	      public_body(one, p, 0n, h)
248	    case 1n+ +e:
249	      public_body(one, p, 1n+e, h)
250	
251	# at p = prime(one); a function of p first, so the checker keeps it a call
252	# (p is symbolic) instead of expanding it whenever it compares two of them
253	def public_key_at(+one: Nat, p: Nat, +seed: List<&2, U32>) -> List<&2, U32>:
254	  match p:
255	    case 0n:
256	      public_of(one, 0n, dconst(one, 0n), SHA.sha512_bytes(seed))
257	    case 1n+ +q:
258	      public_of(one, 1n+q, dconst(one, 1n+q), SHA.sha512_bytes(seed))
259	
260	def public_key(+one: Nat, +seed: List<&2, U32>) -> List<&2, U32>:
261	  public_key_at(one, FS.prime(one), seed)
262	
263	# ---- 5.1.6 signing ----
264	
265	def sign_body(+one: Nat, +p: Nat, +d: Nat, +h: List<&2, U32>, +msg: List<&2, U32>) -> List<&2, U32>:
266	  +el = ell(one)
267	  +a = public_of(one, p, d, h)
268	  +r = Nat.mod(FS.value(SHA.sha512_bytes(cat(rest(32n, h), msg))), el)
269	  +rb = encode(one, p, mul(one, p, d, r, base(p, d)))
270	  +k = hram(one, rb, a, msg)
271	  cat(rb, SX.le_bytes(C.shift(5n, one), Nat.mod(Nat.add(r, Nat.mul(k, secret(h))), el)))
272	
273	def sign_with(+one: Nat, +p: Nat, d: Nat, +h: List<&2, U32>, +msg: List<&2, U32>) -> List<&2, U32>:
274	  match d:
275	    case 0n:
276	      sign_body(one, p, 0n, h, msg)
277	    case 1n+ +e:
278	      sign_body(one, p, 1n+e, h, msg)
279	
280	def sign_at(+one: Nat, p: Nat, +seed: List<&2, U32>, +msg: List<&2, U32>) -> List<&2, U32>:
281	  match p:
282	    case 0n:
283	      sign_with(one, 0n, dconst(one, 0n), SHA.sha512_bytes(seed), msg)
284	    case 1n+ +q:
285	      sign_with(one, 1n+q, dconst(one, 1n+q), SHA.sha512_bytes(seed), msg)
286	
287	def sign(+one: Nat, +seed: List<&2, U32>, +msg: List<&2, U32>) -> List<&2, U32>:
288	  sign_at(one, FS.prime(one), seed, msg)
289	
290	# ---- 5.1.7 verification (cofactorless) ----
291	
292	def check(+one: Nat, +p: Nat, +d: Nat, +s: Nat, +rb: List<&2, U32>, +pk: List<&2, U32>, +msg: List<&2, U32>, ra: Maybe<&2, EPt>, aa: Maybe<&2, EPt>) -> Bool:
293	  match ra aa:
294	    case Some{r} Some{+a}:
295	      +k = hram(one, rb, pk, msg)
296	      equal(p, mul(one, p, d, s, base(p, d)), add(p, d, r, mul(one, p, d, k, a)))
297	    case _ _:
298	      False{}
299	
300	def verify_with(+one: Nat, +p: Nat, +d: Nat, +pk: List<&2, U32>, +msg: List<&2, U32>, +rb: List<&2, U32>, +s: Nat, s_ok: Bool) -> Bool:
301	  match s_ok:
302	    case True{}:
303	      check(one, p, d, s, rb, pk, msg, decode(p, d, rb), decode(p, d, pk))
304	    case False{}:
305	      False{}
306	
307	def verify(+one: Nat, +pk: List<&2, U32>, +msg: List<&2, U32>, +sig: List<&2, U32>) -> Bool:
308	  +p = FS.prime(one)
309	  +s = FS.value(rest(32n, sig))
310	  verify_with(one, p, dconst(one, p), pk, msg, first(32n, sig), s, Nat.is_lt(s, ell(one)))
311	
312	# ---- clauses ----
313	
314	def Scalar.reduce(+one: Nat, +h1: {one == 1n : Nat}, +bs: List<&2, U32>, +hb: {FS.bytes_ok(64n, bs) == True{} : Bool}) -> Type:
315	  {FS.value(ESC.reduce(bs)) == Nat.mod(FS.value(bs), ell(one)) : Nat}
316	
317	def Scalar.mul_add(+one: Nat, +h1: {one == 1n : Nat}, +k: List<&2, U32>, +s: List<&2, U32>, +r: List<&2, U32>, +hk: {FS.tight(k) == True{} : Bool}, +hs: {FS.tight(s) == True{} : Bool}, +hr: {FS.tight(r) == True{} : Bool}, +hsl: {Nat.is_lt(FS.value(s), ell(one)) == True{} : Bool}, +hrl: {Nat.is_lt(FS.value(r), ell(one)) == True{} : Bool}) -> Type:
318	  {FS.value(ESC.mul_add(k, s, r)) == Nat.mod(Nat.add(FS.value(r), Nat.mul(FS.value(k), FS.value(s))), ell(one)) : Nat}
319	
320	def Ed25519.public(+one: Nat, +h1: {one == 1n : Nat}, +seed: List<&2, U32>, +hs: {FS.tight(seed) == True{} : Bool}) -> Type:
321	  {E.public_key(seed) == public_key(one, seed) : List<&2, U32>}
322	
323	def Ed25519.sign(+one: Nat, +h1: {one == 1n : Nat}, +seed: List<&2, U32>, +msg: List<&2, U32>, +hs: {FS.tight(seed) == True{} : Bool}) -> Type:
324	  {E.sign_raw(seed, msg) == sign(one, seed, msg) : List<&2, U32>}
325	
326	def Ed25519.verify(+one: Nat, +h1: {one == 1n : Nat}, +pk: List<&2, U32>, +msg: List<&2, U32>, +sig: List<&2, U32>, +hp: {FS.tight(pk) == True{} : Bool}, +hg: {FS.bytes_ok(64n, sig) == True{} : Bool}) -> Type:
327	  {E.verify_raw(pk, msg, sig) == verify(one, pk, msg, sig) : Bool}