1	import Base
2	import ../hmac.bend as HM
3	import ../keccak/main.bend as KS
4	import ./field.bend as FS
5	import ./curve.bend as CV
6	
7	# ECDSA over secp256k1, transcribed from SEC 1 v2 section 4.1 (signing
8	# 4.1.3, verification 4.1.4, public key recovery 4.1.6) with the nonce of
9	# RFC 6979 section 3.2 (HMAC_DRBG over HMAC-SHA256, spec/crypto/hmac.bend,
10	# with qlen = hlen = 256, so bits2int is OS2IP and int2octets is I2OSP(32)),
11	# the low-S rule of BIP 62 / libsecp256k1 (s > n / 2 is replaced by n - s,
12	# flipping the recovery id's parity) and Ethereum's address and ECRECOVER
13	# precompile. Over the natural numbers; nothing of the implementation is
14	# used. Messages are 32-byte hashes. Every function takes `one` (with
15	# one == 1 in every clause, see field.bend) to write p, n and G.
16	#
17	# Signatures are r || s || v (32 + 32 + 1 bytes, v the recovery id 0..3).
18	
19	def p(+one: Nat) -> Nat:
20	  FS.prime(one)
21	
22	def n(+one: Nat) -> Nat:
23	  FS.order(one)
24	
25	def cat(xs: List<&2, U32>, ys: List<&2, U32>) -> List<&2, U32>:
26	  List.append(&2, U32, xs, ys)
27	
28	def fill(k: Nat, +b: U32) -> List<&2, U32>:
29	  List.replicate(U32, k, b)
30	
31	def i2osp32(+x: Nat) -> List<&2, U32>:
32	  CV.i2osp(32n, x)
33	
34	# 1 <= x < n
35	def scalar_ok(+one: Nat, +x: Nat) -> Bool:
36	  Bool.and(Bool.not(Nat.is_eq(x, 0n)), Nat.is_lt(x, n(one)))
37	
38	# e = bits2int(H) mod n (SEC 1 4.1.3 step 5; RFC 6979 2.3.2)
39	def hash_scalar(+one: Nat, +h: List<&2, U32>) -> Nat:
40	  Nat.mod(CV.os2ip(h), n(one))
41	
42	# ---- RFC 6979 section 3.2 ----
43	
44	type Drbg is Data:
45	  Drbg{k: List<&2, U32>, v: List<&2, U32>}
46	
47	# HMAC-SHA256 (the key is looked at first; the value is HM.hmac's)
48	def hmac(key: List<&2, U32>, msg: List<&2, U32>) -> List<&2, U32>:
49	  match key:
50	    case Nil{}: HM.hmac(Nil{}, msg)
51	    case k <> t: HM.hmac(k <> t, msg)
52	
53	def update_v(+k: List<&2, U32>, +v: List<&2, U32>) -> Drbg:
54	  Drbg{k, hmac(k, v)}
55	
56	# K = HMAC_K(V || tag || seed), V = HMAC_K(V)
57	def update(+k: List<&2, U32>, +v: List<&2, U32>, +tag: U32, +seed: List<&2, U32>) -> Drbg:
58	  update_v(hmac(k, cat(v, tag <> seed)), v)
59	
60	def update2(d: Drbg, +seed: List<&2, U32>) -> Drbg:
61	  match d:
62	    case Drbg{k, v}: update(k, v, 1, seed)
63	
64	# steps b-g, with seed = int2octets(x) || bits2octets(h1)
65	def drbg_init(+seed: List<&2, U32>) -> Drbg:
66	  update2(update(fill(32n, 0), fill(32n, 1), 0, seed), seed)
67	
68	# ---- signing (SEC 1 4.1.3) ----
69	
70	type Attempt is Data:
71	  Retry{}
72	  Sig{sig: List<&2, U32>}
73	
74	# 0 or 1 when b is
75	def flip(b: Bool, +par: Nat) -> Nat:
76	  match b:
77	    case True{}: Nat.sub(1n, par)
78	    case False{}: par
79	
80	def low(high: Bool, +m: Nat, +s: Nat) -> Nat:
81	  match high:
82	    case True{}: FS.mneg(m, s)
83	    case False{}: s
84	
85	def ge2(b: Bool) -> Nat:
86	  match b:
87	    case True{}: 0n
88	    case False{}: 2n
89	
90	def finish_if(bad: Bool, +sig: List<&2, U32>) -> Attempt:
91	  match bad:
92	    case True{}: Retry{}
93	    case False{}: Sig{sig}
94	
95	# R = (x, y) = [k] G, r = x mod n, s = k^-1 (e + r d) mod n; r = 0 or
96	# s = 0 means another k. s > n / 2 (n is odd: n < 2 s) becomes n - s. The
97	# recovery id is (y mod 2) + 2 (x >= n), with its low bit flipped when s was
98	# replaced.
99	def finish(+one: Nat, +e: Nat, +d: Nat, +k: Nat, a: CV.SAffine) -> Attempt:
100	  match a:
101	    case CV.SAffine{+x, +y}:
102	      +m = n(one)
103	      +r = Nat.mod(x, m)
104	      +s = FS.mmul(m, FS.minv(m, k), FS.madd(m, e, FS.mmul(m, r, d)))
105	      +high = Nat.is_lt(m, Nat.double(s))
106	      finish_if(Bool.or(Nat.is_eq(r, 0n), Nat.is_eq(s, 0n)), cat(i2osp32(r), cat(i2osp32(low(high, m, s)), [U32.from_nat(Nat.add(ge2(Nat.is_lt(x, m)), flip(high, Nat.mod(y, 2n))))])))
107	
108	def attempt_ok(+one: Nat, +e: Nat, +d: Nat, +k: Nat, ok: Bool) -> Attempt:
109	  match ok:
110	    case True{}: finish(one, e, d, k, CV.to_affine(p(one), CV.pmul(p(one), k, CV.g(one))))
111	    case False{}: Retry{}
112	
113	# step h.3: k = bits2int(T) with T = V, used when 1 <= k < n
114	def attempt(+one: Nat, +e: Nat, +d: Nat, +v: List<&2, U32>) -> Attempt:
115	  +k = CV.os2ip(v)
116	  attempt_ok(one, e, d, k, scalar_ok(one, k))
117	
118	# step h, with the retry of step h.3 (K = HMAC_K(V || 0x00),
119	# V = HMAC_K(V)) before the next V = HMAC_K(V); at most `fuel` candidates
120	def sign_loop(fuel: Nat, +one: Nat, +e: Nat, +d: Nat, +k: List<&2, U32>, +v: List<&2, U32>, att: Attempt) -> Maybe<&2, List<&2, U32>>:
121	  match fuel att:
122	    case 0n Retry{}: None{}
123	    case 0n Sig{sig}: Some{sig}
124	    case 1n+f Retry{}:
125	      +k2 = hmac(k, cat(v, [0]))
126	      +v3 = hmac(k2, hmac(k2, v))
127	      sign_loop(f, one, e, d, k2, v3, attempt(one, e, d, v3))
128	    case 1n+f Sig{sig}: Some{sig}
129	
130	def sign_drbg(+one: Nat, +e: Nat, +d: Nat, g: Drbg) -> Maybe<&2, List<&2, U32>>:
131	  match g:
132	    case Drbg{+k, +v}:
133	      +v1 = hmac(k, v)
134	      sign_loop(16n, one, e, d, k, v1, attempt(one, e, d, v1))
135	
136	def sign_d(+one: Nat, +h: List<&2, U32>, +d: Nat, ok: Bool) -> Maybe<&2, List<&2, U32>>:
137	  match ok:
138	    case True{}:
139	      +e = hash_scalar(one, h)
140	      sign_drbg(one, e, d, drbg_init(cat(i2osp32(d), i2osp32(e))))
141	    case False{}: None{}
142	
143	# sign(sk, H): d = OS2IP(sk) must be a 32-byte key with 1 <= d < n, H 32 bytes
144	def sign(+one: Nat, +sk: List<&2, U32>, +h: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
145	  sign_d(one, h, CV.os2ip(sk), Bool.and(CV.length_is(32n, h), Bool.and(CV.length_is(32n, sk), scalar_ok(one, CV.os2ip(sk)))))
146	
147	# ---- public keys ----
148	
149	def pk_of(+one: Nat, compressed: Bool, +q: CV.SPoint) -> List<&2, U32>:
150	  match compressed:
151	    case True{}: CV.encode_compressed(p(one), q)
152	    case False{}: CV.encode_uncompressed(p(one), q)
153	
154	def public_d(+one: Nat, compressed: Bool, +d: Nat, ok: Bool) -> Maybe<&2, List<&2, U32>>:
155	  match ok:
156	    case True{}: Some{pk_of(one, compressed, CV.pmul(p(one), d, CV.g(one)))}
157	    case False{}: None{}
158	
159	# the SEC 1 encoding of Q = [d] G
160	def public_key(+one: Nat, +sk: List<&2, U32>, compressed: Bool) -> Maybe<&2, List<&2, U32>>:
161	  public_d(one, compressed, CV.os2ip(sk), Bool.and(CV.length_is(32n, sk), scalar_ok(one, CV.os2ip(sk))))
162	
163	# ---- verification (SEC 1 4.1.4) ----
164	
165	# u1 = e s^-1, u2 = r s^-1, R = [u1] G + [u2] Q; valid when R is not the
166	# point at infinity and x(R) mod n = r
167	def verify_rs(+one: Nat, +q: CV.SPoint, +e: Nat, +r: Nat, +s: Nat) -> Bool:
168	  +m = n(one)
169	  +w = FS.minv(m, s)
170	  +rr = CV.padd(p(one), CV.pmul(p(one), FS.mmul(m, e, w), CV.g(one)), CV.pmul(p(one), FS.mmul(m, r, w), q))
171	  Bool.and(Bool.not(CV.is_inf(rr)), Nat.is_eq(Nat.mod(CV.aff_x(CV.to_affine(p(one), rr)), m), r))
172	
173	def verify_ok(+one: Nat, +q: CV.SPoint, +e: Nat, +r: Nat, +s: Nat, ok: Bool) -> Bool:
174	  match ok:
175	    case True{}: verify_rs(one, q, e, r, s)
176	    case False{}: False{}
177	
178	# r and s in [1, n - 1]; strict verification also rejects s > n / 2
179	def verify_q(+one: Nat, +h: List<&2, U32>, +sig: List<&2, U32>, strict: Bool, mq: Maybe<&2, CV.SPoint>) -> Bool:
180	  match mq:
181	    case None{}: False{}
182	    case Some{+q}:
183	      +r = CV.os2ip(CV.first(32n, sig))
184	      +s = CV.os2ip(CV.after(32n, sig))
185	      verify_ok(one, q, hash_scalar(one, h), r, s, Bool.and(Bool.and(scalar_ok(one, r), scalar_ok(one, s)), Bool.or(Bool.not(strict), Bool.not(Nat.is_lt(n(one), Nat.double(s))))))
186	
187	def verify_len(+one: Nat, +pk: List<&2, U32>, +h: List<&2, U32>, +sig: List<&2, U32>, strict: Bool, ok: Bool) -> Bool:
188	  match ok:
189	    case True{}: verify_q(one, h, sig, strict, CV.decode(p(one), pk))
190	    case False{}: False{}
191	
192	# verify(Q, H, r || s): Q a SEC 1 public key, H 32 bytes, r || s 64 bytes
193	def verify(+one: Nat, +pk: List<&2, U32>, +h: List<&2, U32>, +sig: List<&2, U32>, strict: Bool) -> Bool:
194	  verify_len(one, pk, h, sig, strict, Bool.and(CV.length_is(32n, h), CV.length_is(64n, sig)))
195	
196	# ---- public key recovery (SEC 1 4.1.6) ----
197	
198	def recover_q_if(+one: Nat, +q: CV.SPoint, inf: Bool) -> Maybe<&2, List<&2, U32>>:
199	  match inf:
200	    case True{}: None{}
201	    case False{}: Some{CV.encode_uncompressed(p(one), q)}
202	
203	def recover_q(+one: Nat, +q: CV.SPoint) -> Maybe<&2, List<&2, U32>>:
204	  recover_q_if(one, q, CV.is_inf(q))
205	
206	# Q = r^-1 (s R - e G) = [-e r^-1] G + [s r^-1] R
207	def recover_r(+one: Nat, +e: Nat, +r: Nat, +s: Nat, mr: Maybe<&2, CV.SPoint>) -> Maybe<&2, List<&2, U32>>:
208	  match mr:
209	    case None{}: None{}
210	    case Some{+pr}:
211	      +m = n(one)
212	      +ri = FS.minv(m, r)
213	      recover_q(one, CV.padd(p(one), CV.pmul(p(one), FS.mmul(m, FS.mneg(m, e), ri), CV.g(one)), CV.pmul(p(one), FS.mmul(m, s, ri), pr)))
214	
215	# R: the point of x-coordinate x = r + j n (j = id / 2, x < p) whose y has
216	# parity id mod 2
217	def recover_x_if(+one: Nat, +e: Nat, +r: Nat, +s: Nat, +id: Nat, +x: Nat, ok: Bool) -> Maybe<&2, List<&2, U32>>:
218	  match ok:
219	    case True{}: recover_r(one, e, r, s, CV.decompress(p(one), x, Nat.mod(id, 2n)))
220	    case False{}: None{}
221	
222	def recover_x(+one: Nat, +e: Nat, +r: Nat, +s: Nat, +id: Nat) -> Maybe<&2, List<&2, U32>>:
223	  +x = Nat.add(r, Nat.mul(Nat.div(id, 2n), n(one)))
224	  recover_x_if(one, e, r, s, id, x, Nat.is_lt(x, p(one)))
225	
226	def recover_ok(+one: Nat, +e: Nat, +r: Nat, +s: Nat, +id: Nat, ok: Bool) -> Maybe<&2, List<&2, U32>>:
227	  match ok:
228	    case True{}: recover_x(one, e, r, s, id)
229	    case False{}: None{}
230	
231	def recover_len(+one: Nat, +h: List<&2, U32>, +sig: List<&2, U32>, ok: Bool) -> Maybe<&2, List<&2, U32>>:
232	  match ok:
233	    case True{}:
234	      +r = CV.os2ip(CV.first(32n, sig))
235	      +s = CV.os2ip(CV.first(32n, CV.after(32n, sig)))
236	      +id = U32.to_nat(CV.head(CV.after(64n, sig)))
237	      recover_ok(one, hash_scalar(one, h), r, s, id, Bool.and(Bool.and(scalar_ok(one, r), scalar_ok(one, s)), Nat.is_lt(id, 4n)))
238	    case False{}: None{}
239	
240	# the 65-byte uncompressed key recovered from H (32 bytes) and
241	# r || s || id (65 bytes, id in 0..3)
242	def recover(+one: Nat, +h: List<&2, U32>, +sig: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
243	  recover_len(one, h, sig, Bool.and(CV.length_is(32n, h), CV.length_is(65n, sig)))
244	
245	# ---- Ethereum ----
246	
247	# Keccak-256 (spec/crypto/keccak/main.bend) of bytes packed into
248	# little-endian U32 words, as its interface takes them
249	def word(+b0: U32, +b1: U32, +b2: U32, +b3: U32) -> U32:
250	  U32.or(U32.or(b0, U32.shln(b1, 8n)), U32.or(U32.shln(b2, 16n), U32.shln(b3, 24n)))
251	
252	def words(k: Nat, +bs: List<&2, U32>) -> List<&2, U32>:
253	  match k:
254	    case 0n: Nil{}
255	    case 1n+j: word(CV.head(bs), CV.head(CV.after(1n, bs)), CV.head(CV.after(2n, bs)), CV.head(CV.after(3n, bs))) <> words(j, CV.after(4n, bs))
256	
257	def pack(ws: List<&2, U32>, +i: U32, a: Array<U32>) -> Array<U32>:
258	  match ws:
259	    case Nil{}: a
260	    case w <> t: pack(t, U32.inc(i), Array.set(U32, a, i, w))
261	
262	def unpack(ws: List<&1, U32>) -> List<&2, U32>:
263	  match ws:
264	    case Nil{}: Nil{}
265	    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)
266	
267	def digest_bytes(m: Maybe<&1, Array<U32>>) -> List<&2, U32>:
268	  match m:
269	    case None{}: Nil{}
270	    case Some{a}: unpack(Array.to_list(~U32, a))
271	
272	# The hash of addresses: Keccak-256 (spec/crypto/keccak/main.bend, 24
273	# rounds), named by a value so that the proofs can keep it folded
274	type Hash is Data:
275	  Keccak256{}
276	
277	def hash(+h: Hash, a: Array<U32>, length: Nat) -> Maybe<&1, Array<U32>>:
278	  match h:
279	    case Keccak256{}: KS.keccak256_rounds(24n, a, length)
280	
281	def keccak64(+h: Hash, +bs: List<&2, U32>) -> List<&2, U32>:
282	  digest_bytes(hash(h, pack(words(16n, bs), 0, Array.new(U32, 4n, 0)), 64n))
283	
284	# address = the last 20 bytes of Keccak-256(x || y) of an uncompressed key
285	def eth_if(ok: Bool, +dg: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
286	  match ok:
287	    case True{}: Some{CV.after(12n, dg)}
288	    case False{}: None{}
289	
290	def eth_go(+h: Hash, +pk: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
291	  eth_if(Bool.and(CV.length_is(65n, pk), U32.is_eq(CV.head(pk), 4)), keccak64(h, CV.after(1n, pk)))
292	
293	# (the key is looked at first, so that the proof checker keeps an unknown
294	# address folded)
295	def eth_with(+h: Hash, pk: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
296	  match pk:
297	    case Nil{}: eth_go(h, Nil{})
298	    case b <> t: eth_go(h, b <> t)
299	
300	def eth_address(+pk: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
301	  eth_with(Keccak256{}, pk)
302	
303	def word_of(m: Maybe<&2, List<&2, U32>>) -> Maybe<&2, List<&2, U32>>:
304	  match m:
305	    case None{}: None{}
306	    case Some{a}: Some{cat(fill(12n, 0), a)}
307	
308	def addr_word(m: Maybe<&2, List<&2, U32>>) -> Maybe<&2, List<&2, U32>>:
309	  match m:
310	    case None{}: None{}
311	    case Some{pk}: word_of(eth_address(pk))
312	
313	def all_zero(bs: List<&2, U32>) -> Bool:
314	  match bs:
315	    case Nil{}: True{}
316	    case b <> t: Bool.and(U32.is_eq(b, 0), all_zero(t))
317	
318	def ecrecover_v(+one: Nat, +h: List<&2, U32>, +rs: List<&2, U32>, +v: U32, ok: Bool) -> Maybe<&2, List<&2, U32>>:
319	  match ok:
320	    case True{}: addr_word(recover(one, h, cat(rs, [U32.sub(v, 27)])))
321	    case False{}: None{}
322	
323	def ecrecover_in(+one: Nat, +x: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
324	  +vw = CV.first(32n, CV.after(32n, x))
325	  +v = CV.head(CV.after(31n, vw))
326	  ecrecover_v(one, CV.first(32n, x), CV.after(64n, x), v, Bool.and(all_zero(CV.first(31n, vw)), Bool.or(U32.is_eq(v, 27), U32.is_eq(v, 28))))
327	
328	# ECRECOVER (precompile 0x01): the input zero-padded or cut to 128 bytes is
329	# H || v || r || s, v a 32-byte big-endian word that must be 27 or 28;
330	# the output is the address word (12 zero bytes, then the address) of the
331	# key recovered with id v - 27, or nothing
332	def ecrecover(+one: Nat, input: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
333	  ecrecover_in(one, CV.first(128n, cat(input, fill(128n, 0))))