1	import Base
2	import ./curve25519/field.bend as FS
3	import ./curve25519/x25519.bend as S
4	import ../../src/crypto/kex.bend as K
5	
6	# The contract of src/crypto/kex.bend (X25519 key exchange, RFC 7748).
7	# `one` is the symbolic 1 of spec/crypto/curve25519/field.bend.
8	#
9	#   clause          statement
10	#   Kex.public      generate_keypair(seed) has the public key X25519(seed, 9)
11	#   Kex.shared      shared_secret(sk, pk) is X25519(sk, pk), or None when it
12	#                   is all zero (RFC 7748 section 6.1)
13	#   Kex.reject      malformed input gives None
14	
15	def base() -> List<&2, U32>:
16	  [9, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,
17	   0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
18	
19	def unless_zero(ss: List<&2, U32>, z: Bool) -> Maybe<&2, List<&2, U32>>:
20	  match z:
21	    case True{}:
22	      None{}
23	    case False{}:
24	      Some{ss}
25	
26	def Kex.public(+one: Nat, +h1: {one == 1n : Nat}, +seed: List<&2, U32>, +hs: {FS.tight(seed) == True{} : Bool}) -> Type:
27	  {K.generate_keypair(seed) == Some{K.Keypair{seed, S.x25519(one, seed, base())}} : Maybe<&2, K.Keypair>}
28	
29	def Kex.shared(+one: Nat, +h1: {one == 1n : Nat}, +sk: List<&2, U32>, +pk: List<&2, U32>, +hs: {FS.tight(sk) == True{} : Bool}, +hp: {FS.tight(pk) == True{} : Bool}) -> Type:
30	  {K.shared_secret(sk, pk) == unless_zero(S.x25519(one, sk, pk), Nat.is_eq(FS.value(S.x25519(one, sk, pk)), 0n)) : Maybe<&2, List<&2, U32>>}
31	
32	def Kex.reject(+sk: List<&2, U32>, +pk: List<&2, U32>, +h: {Bool.and(FS.tight(sk), FS.tight(pk)) == False{} : Bool}) -> Type:
33	  {K.shared_secret(sk, pk) == None{} : Maybe<&2, List<&2, U32>>}