1	import Base
2	import ../mac.bend as MAC
3	import ../keccak/keccak.bend as K
4	import ./limbs.bend as L
5	import ./field.bend as F
6	import ./scalar.bend as S
7	import ./point.bend as P
8	import ./bytes.bend as B
9	
10	# ECDSA over secp256k1 (SEC 1 v2 section 4.1) with deterministic nonces
11	# (RFC 6979 section 3.2, HMAC-SHA256) and low-S signatures (BIP 62 /
12	# Ethereum's homestead rule, libsecp256k1's secp256k1_ecdsa_sign), public
13	# key recovery (SEC 1 section 4.1.6, Ethereum's ecrecover) and the Ethereum
14	# address of a public key. The contract is spec/crypto/secp256k1/ecdsa.bend.
15	#
16	# Messages are 32-byte hashes (the caller hashes); keys and signatures are
17	# byte lists of their SEC 1 lengths, malformed ones are rejected as values.
18	
19	type Signature is Data:
20	  Signature{r: List<&2, U32>, s: List<&2, U32>, v: U32}
21	
22	# ---- scalars from bytes ----
23	
24	# 1 <= x < n
25	def scalar_ok(+x: List<&2, Nat>) -> Bool:
26	  Bool.and(Bool.not(S.is_zero(x)), S.lt_n(x))
27	
28	# a 32-byte string as a scalar mod n (bits2int with qlen = hlen = 256,
29	# reduced: SEC 1 section 4.1.3 step 5, RFC 6979 section 2.3.2)
30	def hash_scalar(+h: List<&2, U32>) -> List<&2, Nat>:
31	  S.reduce(B.of_be(h))
32	
33	# ---- RFC 6979 section 3.2, HMAC_DRBG with SHA-256 ----
34	
35	type Drbg is Data:
36	  Drbg{k: List<&2, U32>, v: List<&2, U32>}
37	
38	# (the key is looked at first, so that the proof checker keeps an unknown
39	# HMAC folded)
40	def hmac(key: List<&2, U32>, msg: List<&2, U32>) -> List<&2, U32>:
41	  match key:
42	    case Nil{}: MAC.sign(Nil{}, msg)
43	    case k <> t: MAC.sign(k <> t, msg)
44	
45	def cat(xs: List<&2, U32>, ys: List<&2, U32>) -> List<&2, U32>:
46	  List.append(&2, U32, xs, ys)
47	
48	def fill(n: Nat, +b: U32) -> List<&2, U32>:
49	  List.replicate(U32, n, b)
50	
51	def drbg_v(+k: List<&2, U32>, +v: List<&2, U32>) -> Drbg:
52	  Drbg{k, hmac(k, v)}
53	
54	# steps b-g: V = 0x01..., K = 0x00..., then two HMAC rounds over
55	# V || 0x00 || int2octets(x) || bits2octets(h1) and V || 0x01 || ...
56	def drbg_step(+k: List<&2, U32>, +v: List<&2, U32>, +tag: U32, +seed: List<&2, U32>) -> Drbg:
57	  drbg_v(hmac(k, cat(v, tag <> seed)), v)
58	
59	def drbg_second(d: Drbg, +seed: List<&2, U32>) -> Drbg:
60	  match d:
61	    case Drbg{k, v}: drbg_step(k, v, 1, seed)
62	
63	def drbg_init(+seed: List<&2, U32>) -> Drbg:
64	  drbg_second(drbg_step(fill(32n, 0), fill(32n, 1), 0, seed), seed)
65	
66	# step h.3: K = HMAC_K(V || 0x00), V = HMAC_K(V)
67	def drbg_next(+k: List<&2, U32>, +v: List<&2, U32>) -> Drbg:
68	  drbg_v(hmac(k, cat(v, [0])), v)
69	
70	# ---- signing ----
71	
72	def b2n(b: Bool) -> Nat:
73	  L.b2n(b)
74	
75	type Attempt is Data:
76	  ARetry{}
77	  ADone{sig: Signature}
78	
79	def finish_if(bad: Bool, +sig: Signature) -> Attempt:
80	  match bad:
81	    case True{}: ARetry{}
82	    case False{}: ADone{sig}
83	
84	# r = x(R) mod n, s = k^-1 (z + r d) mod n, made low (s > n / 2 is replaced
85	# by n - s, which flips the parity bit of the recovery id); the recovery
86	# id is the parity of y(R), plus 2 when x(R) >= n
87	def finish(+z: List<&2, Nat>, +d: List<&2, Nat>, +k: List<&2, Nat>, +x: List<&2, Nat>, +y: List<&2, Nat>) -> Attempt:
88	  +r = S.reduce(x)
89	  +s0 = S.mul(S.inv(k), S.add(z, S.mul(r, d)))
90	  +high = b2n(S.is_high(s0))
91	  +par = F.parity(y)
92	  +id = Nat.add(Nat.mul(b2n(Bool.not(S.lt_n(x))), 2n), Nat.sub(Nat.add(par, high), Nat.mul(Nat.mul(par, high), 2n)))
93	  finish_if(Bool.or(S.is_zero(r), S.is_zero(s0)), Signature{B.to_be(r), B.to_be(S.select(high, S.neg(s0), s0)), U32.from_nat(id)})
94	
95	def attempt_aff(+z: List<&2, Nat>, +d: List<&2, Nat>, +k: List<&2, Nat>, a: P.Affine) -> Attempt:
96	  match a:
97	    case P.Affine{x, y}: finish(z, d, k, x, y)
98	
99	def attempt_ok(+z: List<&2, Nat>, +d: List<&2, Nat>, +k: List<&2, Nat>, ok: Bool) -> Attempt:
100	  match ok:
101	    case True{}: attempt_aff(z, d, k, P.to_affine(P.mul(k, P.g())))
102	    case False{}: ARetry{}
103	
104	# the candidate k = bits2int(V) (RFC 6979 step h.3): used when 1 <= k < n
105	def attempt(+z: List<&2, Nat>, +d: List<&2, Nat>, +v: List<&2, U32>) -> Attempt:
106	  +k = B.of_be(v)
107	  attempt_ok(z, d, k, scalar_ok(k))
108	
109	# step h: the candidate V; a k outside [1, n - 1], or one giving r = 0 or
110	# s = 0 (SEC 1 section 4.1.3 steps 3 and 6), is replaced by the next
111	# candidate: K = HMAC_K(V || 0x00), V = HMAC_K(V), V = HMAC_K(V). The loop
112	# stops after `fuel` candidates (the chance that even 2 are needed is below
113	# 2^-127).
114	def sign_loop(fuel: Nat, +z: List<&2, Nat>, +d: List<&2, Nat>, +k: List<&2, U32>, +v: List<&2, U32>, att: Attempt) -> Maybe<&2, Signature>:
115	  match fuel att:
116	    case 0n ARetry{}: None{}
117	    case 0n ADone{sig}: Some{sig}
118	    case 1n+f ARetry{}:
119	      +k2 = hmac(k, cat(v, [0]))
120	      +v3 = hmac(k2, hmac(k2, v))
121	      sign_loop(f, z, d, k2, v3, attempt(z, d, v3))
122	    case 1n+f ADone{sig}: Some{sig}
123	
124	def sign_drbg(+z: List<&2, Nat>, +d: List<&2, Nat>, g: Drbg) -> Maybe<&2, Signature>:
125	  match g:
126	    case Drbg{+k, +v}:
127	      +v1 = hmac(k, v)
128	      sign_loop(16n, z, d, k, v1, attempt(z, d, v1))
129	
130	def secret_if(+d: List<&2, Nat>, ok: Bool) -> Maybe<&2, List<&2, Nat>>:
131	  match ok:
132	    case True{}: Some{d}
133	    case False{}: None{}
134	
135	# the secret key d, when 1 <= d < n
136	def secret(+sk: List<&2, U32>) -> Maybe<&2, List<&2, Nat>>:
137	  +d = B.of_be(sk)
138	  secret_if(d, Bool.and(B.has_len(32n, sk), scalar_ok(d)))
139	
140	# sign with a valid secret scalar d: x = int2octets(d),
141	# h1' = bits2octets(h) = int2octets(bits2int(h) mod n)
142	def sign_d(+h: List<&2, U32>, m: Maybe<&2, List<&2, Nat>>) -> Maybe<&2, Signature>:
143	  match m:
144	    case None{}: None{}
145	    case Some{+d}:
146	      +z = hash_scalar(h)
147	      sign_drbg(z, d, drbg_init(cat(B.to_be(d), B.to_be(z))))
148	
149	def sign_h(+sk: List<&2, U32>, +h: List<&2, U32>, ok: Bool) -> Maybe<&2, Signature>:
150	  match ok:
151	    case True{}: sign_d(h, secret(sk))
152	    case False{}: None{}
153	
154	# the low-S signature of a 32-byte hash under a 32-byte secret key
155	def sign(+sk: List<&2, U32>, +h: List<&2, U32>) -> Maybe<&2, Signature>:
156	  sign_h(sk, h, B.has_len(32n, h))
157	
158	# ---- public keys ----
159	
160	def public_point(+d: List<&2, Nat>) -> P.Point:
161	  P.mul(d, P.g())
162	
163	def pk_of(compressed: Bool, +q: P.Point) -> List<&2, U32>:
164	  match compressed:
165	    case True{}: P.encode_compressed(q)
166	    case False{}: P.encode_uncompressed(q)
167	
168	def public_key_d(compressed: Bool, m: Maybe<&2, List<&2, Nat>>) -> Maybe<&2, List<&2, U32>>:
169	  match m:
170	    case None{}: None{}
171	    case Some{d}: Some{pk_of(compressed, public_point(d))}
172	
173	# the SEC 1 encoding of [d] G (33 bytes compressed, 65 uncompressed)
174	def public_key(+sk: List<&2, U32>, compressed: Bool) -> Maybe<&2, List<&2, U32>>:
175	  public_key_d(compressed, secret(sk))
176	
177	# ---- verification (SEC 1 section 4.1.4) ----
178	
179	# u1 = z w, u2 = r w with w = s^-1; R = [u1] G + [u2] Q must not be the
180	# point at infinity and x(R) mod n must be r
181	def verify_rs(+q: P.Point, +z: List<&2, Nat>, +r: List<&2, Nat>, +s: List<&2, Nat>) -> Bool:
182	  +w = S.inv(s)
183	  +rr = P.add(P.mul(S.mul(z, w), P.g()), P.mul(S.mul(r, w), q))
184	  Bool.and(Bool.not(P.is_inf(rr)), S.eq(S.reduce(P.aff_x(P.to_affine(rr))), r))
185	
186	def verify_ok(+q: P.Point, +z: List<&2, Nat>, +r: List<&2, Nat>, +s: List<&2, Nat>, ok: Bool) -> Bool:
187	  match ok:
188	    case True{}: verify_rs(q, z, r, s)
189	    case False{}: False{}
190	
191	def verify_q(+h: List<&2, U32>, +sig: List<&2, U32>, strict: Bool, m: Maybe<&2, P.Point>) -> Bool:
192	  match m:
193	    case None{}: False{}
194	    case Some{+q}:
195	      +r = B.of_be(B.prefix(32n, sig))
196	      +s = B.of_be(B.suffix(32n, sig))
197	      verify_ok(q, hash_scalar(h), r, s, Bool.and(Bool.and(scalar_ok(r), scalar_ok(s)), Bool.or(Bool.not(strict), Bool.not(S.is_high(s)))))
198	
199	def verify_len(+pk: List<&2, U32>, +h: List<&2, U32>, +sig: List<&2, U32>, strict: Bool, ok: Bool) -> Bool:
200	  match ok:
201	    case True{}: verify_q(h, sig, strict, P.decode(pk))
202	    case False{}: False{}
203	
204	def verify_with(+pk: List<&2, U32>, +h: List<&2, U32>, +sig: List<&2, U32>, strict: Bool) -> Bool:
205	  verify_len(pk, h, sig, strict, Bool.and(B.has_len(32n, h), B.has_len(64n, sig)))
206	
207	# SEC 1 verification of a 64-byte r || s against a SEC 1 public key (33 or
208	# 65 bytes); high s is accepted, as SEC 1 and OpenSSL do
209	def verify(+pk: List<&2, U32>, +h: List<&2, U32>, +sig: List<&2, U32>) -> Bool:
210	  verify_with(pk, h, sig, False{})
211	
212	# the same, rejecting s > n / 2 (Bitcoin's BIP 62/146 LOW_S rule,
213	# Ethereum's homestead rule for transactions)
214	def verify_strict(+pk: List<&2, U32>, +h: List<&2, U32>, +sig: List<&2, U32>) -> Bool:
215	  verify_with(pk, h, sig, True{})
216	
217	# ---- recovery (SEC 1 section 4.1.6, Ethereum ecrecover) ----
218	
219	def recover_q(+q: P.Point, inf: Bool) -> Maybe<&2, List<&2, U32>>:
220	  match inf:
221	    case True{}: None{}
222	    case False{}: Some{P.encode_uncompressed(q)}
223	
224	# Q = r^-1 (s R - z G), with R the point of x-coordinate r + n j (j = id / 2)
225	# and y parity id mod 2
226	def recover_r(+z: List<&2, Nat>, +r: List<&2, Nat>, +s: List<&2, Nat>, m: Maybe<&2, P.Point>) -> Maybe<&2, List<&2, U32>>:
227	  match m:
228	    case None{}: None{}
229	    case Some{+pr}:
230	      +ri = S.inv(r)
231	      +q = P.add(P.mul(S.mul(S.neg(z), ri), P.g()), P.mul(S.mul(s, ri), pr))
232	      recover_q(q, P.is_inf(q))
233	
234	def recover_x(+z: List<&2, Nat>, +r: List<&2, Nat>, +s: List<&2, Nat>, +id: Nat, +x: List<&2, Nat>, ok: Bool) -> Maybe<&2, List<&2, U32>>:
235	  match ok:
236	    case True{}: recover_r(z, r, s, P.decompress(x, Nat.mod(id, 2n)))
237	    case False{}: None{}
238	
239	# c_n = 2^256 - n and c_p = 2^256 - p as 16-limb field elements
240	def cn_fe() -> List<&2, Nat>:
241	  [48831n, 12233n, 41331n, 16429n, 24516n, 20663n, 8985n, 17745n, 1n, 0n, 0n, 0n, 0n, 0n, 0n, 0n]
242	
243	def cp_fe() -> List<&2, Nat>:
244	  [977n, 0n, 1n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 0n]
245	
246	# (r + n) mod p = (r - c_n + 2^256) mod p = (r - c_n + c_p) mod p
247	def rn_fe(+r: List<&2, Nat>) -> List<&2, Nat>:
248	  F.add(F.sub(r, cn_fe()), cp_fe())
249	
250	# x = r + j n with j = id / 2. For j = 1, r + n must be below p: then
251	# (r + n) mod p = r + n >= n, while a wrapped r + n - p is below r < n
252	def recover_ok(+z: List<&2, Nat>, +r: List<&2, Nat>, +s: List<&2, Nat>, +id: Nat, ok: Bool) -> Maybe<&2, List<&2, U32>>:
253	  match ok:
254	    case True{}:
255	      +j = Nat.div(id, 2n)
256	      +x1 = rn_fe(r)
257	      recover_x(z, r, s, id, F.select(j, x1, r), Bool.or(Nat.is_eq(j, 0n), Bool.not(S.lt_n(x1))))
258	    case False{}: None{}
259	
260	def recover_sig(+h: List<&2, U32>, +sig: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
261	  +r = B.of_be(B.prefix(32n, sig))
262	  +s = B.of_be(B.prefix(32n, B.suffix(32n, sig)))
263	  +id = U32.to_nat(B.head(B.suffix(64n, sig)))
264	  recover_ok(hash_scalar(h), r, s, id, Bool.and(Bool.and(scalar_ok(r), scalar_ok(s)), Nat.is_lt(id, 4n)))
265	
266	def recover_len(+h: List<&2, U32>, +sig: List<&2, U32>, ok: Bool) -> Maybe<&2, List<&2, U32>>:
267	  match ok:
268	    case True{}: recover_sig(h, sig)
269	    case False{}: None{}
270	
271	# the 65-byte uncompressed public key that signed the 32-byte hash, from a
272	# 65-byte r || s || id with id in 0..3 (go-ethereum's crypto.Ecrecover;
273	# Ethereum's precompile passes id = v - 27); None when r or s is not in
274	# [1, n - 1], x(R) is not a field element on the curve, or Q is infinity.
275	# High s is accepted, as the precompile does.
276	def recover(+h: List<&2, U32>, +sig: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
277	  recover_len(h, sig, Bool.and(B.has_len(32n, h), B.has_len(65n, sig)))
278	
279	# ---- Ethereum addresses ----
280	
281	# little-endian U32 words of bytes (a missing byte reads as 0)
282	def word(+b0: U32, +b1: U32, +b2: U32, +b3: U32) -> U32:
283	  U32.or(U32.or(b0, U32.shln(b1, 8n)), U32.or(U32.shln(b2, 16n), U32.shln(b3, 24n)))
284	
285	def words(n: Nat, +bs: List<&2, U32>) -> List<&2, U32>:
286	  match n:
287	    case 0n: Nil{}
288	    case 1n+k: word(B.head(bs), B.head(B.tail(bs)), B.head(B.suffix(2n, bs)), B.head(B.suffix(3n, bs))) <> words(k, B.suffix(4n, bs))
289	
290	def pack(ws: List<&2, U32>, +i: U32, a: Array<U32>) -> Array<U32>:
291	  match ws:
292	    case Nil{}: a
293	    case w <> t: pack(t, U32.inc(i), Array.set(U32, a, i, w))
294	
295	def unpack(ws: List<&1, U32>) -> List<&2, U32>:
296	  match ws:
297	    case Nil{}: Nil{}
298	    case +w <> t: U32.and(w, 255) <> U32.and(U32.shrn(w, 8n), 255) <> U32.and(U32.shrn(w, 16n), 255) <> U32.shrn(w, 24n) <> unpack(t)
299	
300	def digest_bytes(m: Maybe<&1, Array<U32>>) -> List<&2, U32>:
301	  match m:
302	    case None{}: Nil{}
303	    case Some{a}: unpack(Array.to_list(~U32, a))
304	
305	# The hash of addresses, as a value (only Keccak-256 exists), so that the
306	# proofs can keep it folded
307	type Hash is Data:
308	  Keccak256{}
309	
310	def hash(+h: Hash, a: Array<U32>, length: Nat) -> Maybe<&1, Array<U32>>:
311	  match h:
312	    case Keccak256{}: K.keccak256(a, length)
313	
314	# the hash of 64 bytes
315	def keccak64(+h: Hash, +bs: List<&2, U32>) -> List<&2, U32>:
316	  digest_bytes(hash(h, pack(words(16n, bs), 0, Array.new(U32, 4n, 0)), 64n))
317	
318	def eth_if(ok: Bool, +dg: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
319	  match ok:
320	    case True{}: Some{B.suffix(12n, dg)}
321	    case False{}: None{}
322	
323	def eth_go(+h: Hash, +pk: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
324	  eth_if(Bool.and(B.has_len(65n, pk), U32.is_eq(B.head(pk), 4)), keccak64(h, B.tail(pk)))
325	
326	# (the key is looked at first, so that the proof checker keeps an unknown
327	# address folded)
328	def eth_with(+h: Hash, pk: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
329	  match pk:
330	    case Nil{}: eth_go(h, Nil{})
331	    case b <> t: eth_go(h, b <> t)
332	
333	# the 20-byte Ethereum address of a 65-byte uncompressed public key:
334	# the last 20 bytes of Keccak-256 of its 64 coordinate bytes
335	def eth_address(+pk: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
336	  eth_with(Keccak256{}, pk)
337	
338	# ---- Ethereum's ECRECOVER precompile (address 0x01) ----
339	
340	def zeros_ok(bs: List<&2, U32>) -> Bool:
341	  match bs:
342	    case Nil{}: True{}
343	    case b <> t: Bool.and(U32.is_eq(b, 0), zeros_ok(t))
344	
345	def eth_word(m: Maybe<&2, List<&2, U32>>) -> Maybe<&2, List<&2, U32>>:
346	  match m:
347	    case None{}: None{}
348	    case Some{a}: Some{cat(fill(12n, 0), a)}
349	
350	def addr_word(m: Maybe<&2, List<&2, U32>>) -> Maybe<&2, List<&2, U32>>:
351	  match m:
352	    case None{}: None{}
353	    case Some{pk}: eth_word(eth_address(pk))
354	
355	def ecrecover_v(+h: List<&2, U32>, +rs: List<&2, U32>, +v: U32, ok: Bool) -> Maybe<&2, List<&2, U32>>:
356	  match ok:
357	    case True{}: addr_word(recover(h, cat(rs, [U32.sub(v, 27)])))
358	    case False{}: None{}
359	
360	def ecrecover_in(+x: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
361	  +vw = B.prefix(32n, B.suffix(32n, x))
362	  +v = B.head(B.suffix(31n, vw))
363	  ecrecover_v(B.prefix(32n, x), B.suffix(64n, x), v, Bool.and(zeros_ok(B.prefix(31n, vw)), Bool.or(U32.is_eq(v, 27), U32.is_eq(v, 28))))
364	
365	# The precompile's semantics (Ethereum yellow paper appendix E): the input,
366	# zero-padded or cut to 128 bytes, is hash || v || r || s (32 bytes each,
367	# big-endian); v must be 27 or 28. The output is the 32-byte word holding
368	# the signer's address, or None (the precompile's empty output) when v, r
369	# or s is invalid or no key is recovered.
370	def ecrecover(input: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
371	  ecrecover_in(B.prefix(128n, cat(input, fill(128n, 0))))