1	import Base
2	import ./curve25519/x25519.bend as X
3	import ./curve25519/field.bend as F
4	
5	# Key exchange: X25519 (RFC 7748). Keys and secrets are 32-byte lists of U32
6	# values below 256; malformed input is rejected as a value (None).
7	#
8	#   generate_keypair(seed)   the secret is the 32-byte seed (clamped inside
9	#                            X25519), the public key X25519(secret, 9)
10	#   generate_keypair_os()    the same from 32 bytes of IO.random_u32
11	#   shared_secret(sk, pk)    X25519(sk, pk); None when either input is
12	#                            malformed or the result is all zero (a
13	#                            small-order peer key, RFC 7748 section 6.1)
14	#
15	# Correctness against RFC 7748 is proved (spec/crypto/kex.bend,
16	# proofs/crypto/curve25519). The ladder is branch-free on secrets; Bend
17	# has no timing model, so constant time is by construction, not proved.
18	
19	type Keypair is Data:
20	  Keypair{secret: List<&2, U32>, public: List<&2, U32>}
21	
22	def keypair_of(+seed: List<&2, U32>, m: Maybe<&2, List<&2, U32>>) -> Maybe<&2, Keypair>:
23	  match m:
24	    case None{}:
25	      None{}
26	    case Some{pk}:
27	      Some{Keypair{seed, pk}}
28	
29	def generate_keypair(+seed: List<&2, U32>) -> Maybe<&2, Keypair>:
30	  keypair_of(seed, X.x25519(seed, X.base()))
31	
32	# 32 bytes from 8 words, little-endian
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 nonzero(ss: List<&2, U32>, z: Bool) -> Maybe<&2, List<&2, U32>>:
52	  match z:
53	    case True{}:
54	      None{}
55	    case False{}:
56	      Some{ss}
57	
58	def shared_of(m: Maybe<&2, List<&2, U32>>) -> Maybe<&2, List<&2, U32>>:
59	  match m:
60	    case None{}:
61	      None{}
62	    case Some{+ss}:
63	      nonzero(ss, U32.is_eq(F.sum_all(ss, 0), 0))
64	
65	def shared_secret(+sk: List<&2, U32>, +pk: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
66	  shared_of(X.x25519(sk, pk))