1	import Base
2	import ./curve25519/field.bend as FS
3	import ./ed25519.bend as SE
4	import ../../src/crypto/sign.bend as SG
5	
6	# The contract of src/crypto/sign.bend (Ed25519 signatures, RFC 8032).
7	# `one` is the symbolic 1 of spec/crypto/curve25519/field.bend.
8	#
9	#   clause          statement
10	#   Sign.keypair    generate_keypair(seed) is the seed with the public key
11	#                   public_key(seed) of spec/crypto/ed25519.bend
12	#   Sign.sign       sign(sk, msg) is the RFC 8032 signature sign(sk, msg)
13	#   Sign.verify     verify(pk, msg, sig) is the RFC 8032 verdict
14	#   Sign.reject     a malformed seed, key or signature gives None / False
15	
16	def Sign.keypair(+one: Nat, +h1: {one == 1n : Nat}, +seed: List<&2, U32>, +hs: {FS.tight(seed) == True{} : Bool}) -> Type:
17	  {SG.generate_keypair(seed) == Some{SG.Keypair{seed, SE.public_key(one, seed)}} : Maybe<&2, SG.Keypair>}
18	
19	def Sign.sign(+one: Nat, +h1: {one == 1n : Nat}, +sk: List<&2, U32>, +msg: List<&2, U32>, +hs: {FS.tight(sk) == True{} : Bool}) -> Type:
20	  {SG.sign(sk, msg) == Some{SE.sign(one, sk, msg)} : Maybe<&2, List<&2, U32>>}
21	
22	def Sign.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:
23	  {SG.verify(pk, msg, sig) == SE.verify(one, pk, msg, sig) : Bool}
24	
25	def Sign.reject_seed(+seed: List<&2, U32>, +h: {FS.tight(seed) == False{} : Bool}) -> Type:
26	  {SG.generate_keypair(seed) == None{} : Maybe<&2, SG.Keypair>}
27	
28	def Sign.reject_key(+sk: List<&2, U32>, +msg: List<&2, U32>, +h: {FS.tight(sk) == False{} : Bool}) -> Type:
29	  {SG.sign(sk, msg) == None{} : Maybe<&2, List<&2, U32>>}
30	
31	def Sign.reject(+pk: List<&2, U32>, +msg: List<&2, U32>, +sig: List<&2, U32>, +h: {Bool.and(FS.tight(pk), FS.bytes_ok(64n, sig)) == False{} : Bool}) -> Type:
32	  {SG.verify(pk, msg, sig) == False{} : Bool}