1	import Base
2	import ../hash.bend as H
3	import ../curve25519/field.bend as F
4	import ../curve25519/x25519.bend as X
5	import ./scalar.bend as SC
6	import ./point.bend as PT
7	
8	# Ed25519 (RFC 8032 section 5.1): key generation (5.1.5), signing (5.1.6)
9	# and cofactorless verification (5.1.7: [S]B == R + [k]A', S < L checked)
10	# on byte strings (U32 values below 256); SHA-512 is ../hash.bend's (proved
11	# equal to FIPS 180-4).
12	
13	def cat(xs: List<&2, U32>, ys: List<&2, U32>) -> List<&2, U32>:
14	  match xs:
15	    case Nil{}:
16	      ys
17	    case Con{x, xt}:
18	      Con{x, cat(xt, ys)}
19	
20	# k = SHA-512(R || A || M) mod L
21	def hram(rb: List<&2, U32>, +a: List<&2, U32>, +msg: List<&2, U32>) -> List<&2, U32>:
22	  match rb:
23	    case Nil{}:
24	      SC.reduce(H.sha512(cat(Nil{}, cat(a, msg))))
25	    case Con{x, xt}:
26	      SC.reduce(H.sha512(cat(Con{x, xt}, cat(a, msg))))
27	
28	# the secret scalar s (pruned lower half of SHA-512(seed)) and the prefix
29	def secret(+h: List<&2, U32>) -> List<&2, U32>:
30	  X.clamp(F.take(32n, h))
31	
32	def prefix(+h: List<&2, U32>) -> List<&2, U32>:
33	  F.drop(32n, h)
34	
35	# xs: an input (the seed or the public key), which keeps the proof checker
36	# from computing the curve constants (see PT.lit)
37	def public_of(+c: PT.Cs, +xs: List<&2, U32>, +h: List<&2, U32>) -> List<&2, U32>:
38	  PT.encode(PT.mul(c, secret(h), PT.base(c, xs)))
39	
40	# A = [s]B, encoded
41	def public_key(+seed: List<&2, U32>) -> List<&2, U32>:
42	  public_of(PT.consts(seed), seed, H.sha512(seed))
43	
44	def sign_with(+c: PT.Cs, +xs: List<&2, U32>, +h: List<&2, U32>, +msg: List<&2, U32>) -> List<&2, U32>:
45	  +b = PT.base(c, xs)
46	  +a = public_of(c, xs, h)
47	  +r = SC.reduce(H.sha512(cat(prefix(h), msg)))
48	  +rb = PT.encode(PT.mul(c, r, b))
49	  +k = hram(rb, a, msg)
50	  cat(rb, SC.mul_add(k, SC.reduce(secret(h)), r))
51	
52	def sign_raw(+seed: List<&2, U32>, +msg: List<&2, U32>) -> List<&2, U32>:
53	  sign_with(PT.consts(seed), seed, H.sha512(seed), msg)
54	
55	def check(+c: PT.Cs, +sb: List<&2, U32>, +rb: List<&2, U32>, +pk: List<&2, U32>, +msg: List<&2, U32>, ra: Maybe<&2, PT.Pt>, aa: Maybe<&2, PT.Pt>) -> Bool:
56	  match ra aa:
57	    case Some{r} Some{+a}:
58	      +k = hram(rb, pk, msg)
59	      +b = PT.base(c, pk)
60	      PT.equal(PT.mul(c, sb, b), PT.add(c, r, PT.mul(c, k, a)))
61	    case _ _:
62	      False{}
63	
64	def verify_with(+c: PT.Cs, +pk: List<&2, U32>, +msg: List<&2, U32>, +rb: List<&2, U32>, +sb: List<&2, U32>, s_ok: Bool) -> Bool:
65	  match s_ok:
66	    case True{}:
67	      check(c, sb, rb, pk, msg, PT.decode(c, rb), PT.decode(c, pk))
68	    case False{}:
69	      False{}
70	
71	def verify_raw(+pk: List<&2, U32>, +msg: List<&2, U32>, +sig: List<&2, U32>) -> Bool:
72	  +sb = F.drop(32n, sig)
73	  verify_with(PT.consts(pk), pk, msg, F.take(32n, sig), sb, SC.lt_l(sb))