1	import Base
2	import ./secp256k1/ecdsa.bend as E
3	import ./secp256k1/schnorr.bend as Sch
4	
5	# secp256k1 signatures: ECDSA (SEC 1 v2 section 4.1) with RFC 6979
6	# deterministic nonces and low-S output, public key recovery (Ethereum's
7	# ecrecover), Ethereum addresses, and BIP-340 Schnorr signatures.
8	#
9	# Byte convention: bytes are U32 values below 256; keys, hashes and
10	# signatures are byte lists of their standard lengths, and a malformed one
11	# is rejected as a value (None / False), never a crash.
12	#
13	#   generate_keypair(seed)        secret = the 32-byte seed if 1 <= seed < n,
14	#                                 public = its 33-byte compressed SEC 1 key
15	#   generate_keypair_os()         the same from IO.random_u32 (drawn again
16	#                                 while the seed is not a valid key)
17	#   public_key(sk, compressed)    33-byte (02/03) or 65-byte (04) SEC 1 key
18	#   sign(sk, hash32)              Signature{r, s, v}: RFC 6979 nonce, low s,
19	#                                 v the recovery id 0..3
20	#   sign_compact(sk, hash32)      r || s || v, 65 bytes
21	#   verify(pk, hash32, sig64)     SEC 1 verification of r || s (high s allowed)
22	#   verify_strict(pk, h, sig64)   the same, high s rejected (BIP 146 LOW_S)
23	#   recover(hash32, sig65)        the 65-byte public key of r || s || id
24	#   eth_address(pk65)             the 20-byte Ethereum address
25	#   ecrecover(input)              Ethereum's precompile 0x01: 128 bytes
26	#                                 hash || v || r || s -> the address word
27	#   schnorr_pubkey(sk)            BIP-340 32-byte x-only public key
28	#   schnorr_sign(sk, msg, aux32)  BIP-340 64-byte signature
29	#   schnorr_verify(pk32, msg, sig64)
30	#
31	# Every function is proved equal to its specification
32	# (spec/crypto/secp256k1/, transcribed from SEC 1/SEC 2, RFC 6979 and
33	# BIP-340) for every input: proofs/crypto/secp256k1/, clauses in
34	# docs/CRYPTO_CONTRACTS.md. Scalar multiplication by secrets and all
35	# secret-dependent arithmetic are branch-free (masked selection over
36	# complete formulas); Bend has no timing model, so constant time is by
37	# construction, not proved.
38	
39	type Keypair is Data:
40	  Keypair{secret: List<&2, U32>, public: List<&2, U32>}
41	
42	def keypair_of(+seed: List<&2, U32>, m: Maybe<&2, List<&2, U32>>) -> Maybe<&2, Keypair>:
43	  match m:
44	    case None{}: None{}
45	    case Some{pk}: Some{Keypair{seed, pk}}
46	
47	def generate_keypair(+seed: List<&2, U32>) -> Maybe<&2, Keypair>:
48	  keypair_of(seed, E.public_key(seed, True{}))
49	
50	def word_bytes(+w: U32, rest: List<&2, U32>) -> List<&2, U32>:
51	  U32.and(w, 255) <> U32.and(U32.shrn(w, 8n), 255) <> U32.and(U32.shrn(w, 16n), 255) <> U32.shrn(w, 24n) <> rest
52	
53	def random_bytes(n: Nat, acc: List<&2, U32>) -> IO(List<&2, U32>):
54	  match n:
55	    case 0n:
56	      IO.pure(List<&2, U32>, acc)
57	    case 1n+m:
58	      do IO<List<&2, U32>>:
59	        w : U32 <- IO.try(U32, IO.random_u32())
60	        rest : List<&2, U32> <- random_bytes(m, acc)
61	        return word_bytes(w, rest)
62	
63	def os_retry(fuel: Nat, m: Maybe<&2, Keypair>) -> IO(Maybe<&2, Keypair>):
64	  match fuel m:
65	    case _ Some{kp}:
66	      IO.pure(Maybe<&2, Keypair>, Some{kp})
67	    case 0n None{}:
68	      IO.pure(Maybe<&2, Keypair>, None{})
69	    case 1n+f None{}:
70	      do IO<Maybe<&2, Keypair>>:
71	        seed : List<&2, U32> <- random_bytes(8n, Nil{})
72	        kp : Maybe<&2, Keypair> <- os_retry(f, generate_keypair(seed))
73	        return kp
74	
75	# 32 bytes of the operating system's random source (getrandom, arc4random,
76	# crypto.getRandomValues) as the seed; a seed outside [1, n - 1] (chance
77	# 2^-128) is drawn again, up to 8 times
78	def generate_keypair_os() -> IO(Maybe<&2, Keypair>):
79	  os_retry(8n, None{})
80	
81	def public_key(+sk: List<&2, U32>, compressed: Bool) -> Maybe<&2, List<&2, U32>>:
82	  E.public_key(sk, compressed)
83	
84	def sign(+sk: List<&2, U32>, +hash: List<&2, U32>) -> Maybe<&2, E.Signature>:
85	  E.sign(sk, hash)
86	
87	def compact(m: Maybe<&2, E.Signature>) -> Maybe<&2, List<&2, U32>>:
88	  match m:
89	    case None{}: None{}
90	    case Some{E.Signature{r, s, v}}: Some{List.append(&2, U32, r, List.append(&2, U32, s, [v]))}
91	
92	def sign_compact(+sk: List<&2, U32>, +hash: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
93	  compact(E.sign(sk, hash))
94	
95	def verify(+pk: List<&2, U32>, +hash: List<&2, U32>, +sig: List<&2, U32>) -> Bool:
96	  E.verify(pk, hash, sig)
97	
98	def verify_strict(+pk: List<&2, U32>, +hash: List<&2, U32>, +sig: List<&2, U32>) -> Bool:
99	  E.verify_strict(pk, hash, sig)
100	
101	def recover(+hash: List<&2, U32>, +sig: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
102	  E.recover(hash, sig)
103	
104	def eth_address(+pk: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
105	  E.eth_address(pk)
106	
107	def ecrecover(input: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
108	  E.ecrecover(input)
109	
110	def schnorr_pubkey(+sk: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
111	  Sch.pubkey(sk)
112	
113	def schnorr_sign(+sk: List<&2, U32>, +msg: List<&2, U32>, +aux: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
114	  Sch.sign(sk, msg, aux)
115	
116	def schnorr_verify(+pk: List<&2, U32>, +msg: List<&2, U32>, +sig: List<&2, U32>) -> Bool:
117	  Sch.verify(pk, msg, sig)