1	import Base
2	import ./curve25519/x25519.bend as X
3	import ./ed25519/ed25519.bend as E
4	
5	# Signatures: Ed25519 (RFC 8032). Keys and signatures are byte lists (U32
6	# values below 256) of the RFC lengths; malformed ones are rejected as
7	# values.
8	#
9	#   generate_keypair(seed)   secret = the 32-byte seed, public = [s]B
10	#   generate_keypair_os()    the same from 32 bytes of IO.random_u32
11	#   sign(sk, msg)            the 64-byte signature, None for a bad key
12	#   verify(pk, msg, sig)     True iff sig is valid (cofactorless check,
13	#                            non-canonical S >= L rejected)
14	#
15	# Correctness against RFC 8032 is proved (spec/crypto/sign.bend,
16	# proofs/crypto/ed25519). Scalar multiplication and scalar arithmetic are
17	# branch-free on secrets; Bend has no timing model, so constant time is by
18	# construction, not proved.
19	
20	type Keypair is Data:
21	  Keypair{secret: List<&2, U32>, public: List<&2, U32>}
22	
23	def keypair_if(+seed: List<&2, U32>, ok: Bool) -> Maybe<&2, Keypair>:
24	  match ok:
25	    case True{}:
26	      Some{Keypair{seed, E.public_key(seed)}}
27	    case False{}:
28	      None{}
29	
30	def generate_keypair(+seed: List<&2, U32>) -> Maybe<&2, Keypair>:
31	  keypair_if(seed, X.valid_bytes(32n, seed))
32	
33	def word_bytes(+w: U32, rest: List<&2, U32>) -> List<&2, U32>:
34	  Con{U32.and(w, 255), Con{U32.and(U32.shrn(w, 8n), 255), Con{U32.and(U32.shrn(w, 16n), 255), Con{U32.shrn(w, 24n), rest}}}}
35	
36	def random_bytes(n: Nat, acc: List<&2, U32>) -> IO(List<&2, U32>):
37	  match n:
38	    case 0n:
39	      IO.pure(List<&2, U32>, acc)
40	    case 1n+m:
41	      do IO<List<&2, U32>>:
42	        w : U32 <- IO.try(U32, IO.random_u32())
43	        rest : List<&2, U32> <- random_bytes(m, acc)
44	        return word_bytes(w, rest)
45	
46	def generate_keypair_os() -> IO(Maybe<&2, Keypair>):
47	  do IO<Maybe<&2, Keypair>>:
48	    seed : List<&2, U32> <- random_bytes(8n, Nil{})
49	    return generate_keypair(seed)
50	
51	def sign_if(+sk: List<&2, U32>, +msg: List<&2, U32>, ok: Bool) -> Maybe<&2, List<&2, U32>>:
52	  match ok:
53	    case True{}:
54	      Some{E.sign_raw(sk, msg)}
55	    case False{}:
56	      None{}
57	
58	def sign(+sk: List<&2, U32>, +msg: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
59	  sign_if(sk, msg, X.valid_bytes(32n, sk))
60	
61	def verify_if(+pk: List<&2, U32>, +msg: List<&2, U32>, +sig: List<&2, U32>, ok: Bool) -> Bool:
62	  match ok:
63	    case True{}:
64	      E.verify_raw(pk, msg, sig)
65	    case False{}:
66	      False{}
67	
68	def verify(+pk: List<&2, U32>, +msg: List<&2, U32>, +sig: List<&2, U32>) -> Bool:
69	  verify_if(pk, msg, sig, Bool.and(X.valid_bytes(32n, pk), X.valid_bytes(64n, sig)))