1	import Base
2	import ../sha.bend as FIPS
3	import ./field.bend as FS
4	import ./curve.bend as CV
5	
6	# BIP-340 Schnorr signatures, transcribed from the BIP's "Default Signing"
7	# and "Verification" sections (and its reference.py), over the natural
8	# numbers and the FIPS 180-4 SHA-256 specification spec/crypto/sha.bend.
9	# Nothing of the implementation is used. Every function takes `one`
10	# (one == 1 in every clause, see field.bend) to write p, n and G.
11	
12	def p(+one: Nat) -> Nat:
13	  FS.prime(one)
14	
15	def n(+one: Nat) -> Nat:
16	  FS.order(one)
17	
18	def cat(xs: List<&2, U32>, ys: List<&2, U32>) -> List<&2, U32>:
19	  List.append(&2, U32, xs, ys)
20	
21	def bytes32(+x: Nat) -> List<&2, U32>:
22	  CV.i2osp(32n, x)
23	
24	def tagged_h(+th: List<&2, U32>, x: List<&2, U32>) -> List<&2, U32>:
25	  FIPS.sha256_bytes(cat(th, cat(th, x)))
26	
27	# hash_name(x) = SHA256(SHA256(name) || SHA256(name) || x), name in ASCII
28	def tagged(tag: List<&2, U32>, x: List<&2, U32>) -> List<&2, U32>:
29	  tagged_h(FIPS.sha256_bytes(tag), x)
30	
31	# "BIP0340/aux", "BIP0340/nonce", "BIP0340/challenge"
32	def tag_aux() -> List<&2, U32>:
33	  [66, 73, 80, 48, 51, 52, 48, 47, 97, 117, 120]
34	
35	def tag_nonce() -> List<&2, U32>:
36	  [66, 73, 80, 48, 51, 52, 48, 47, 110, 111, 110, 99, 101]
37	
38	def tag_challenge() -> List<&2, U32>:
39	  [66, 73, 80, 48, 51, 52, 48, 47, 99, 104, 97, 108, 108, 101, 110, 103, 101]
40	
41	def xor_bytes(xs: List<&2, U32>, ys: List<&2, U32>) -> List<&2, U32>:
42	  match xs ys:
43	    case x <> xt y <> yt: U32.xor(x, y) <> xor_bytes(xt, yt)
44	    case _ _: Nil{}
45	
46	# n - x when y is odd (the key or nonce whose point has even y)
47	def even_b(+m: Nat, b: Nat, +x: Nat) -> Nat:
48	  match b:
49	    case 0n: x
50	    case 1n+k: FS.mneg(m, x)
51	
52	def even(+m: Nat, +y: Nat, +x: Nat) -> Nat:
53	  even_b(m, Nat.mod(y, 2n), x)
54	
55	# ---- verification ----
56	
57	# lift_x(x): the point with x-coordinate x and even y, if x < p and
58	# x^3 + 7 is a square
59	def lift_if(+one: Nat, +x: Nat, ok: Bool) -> Maybe<&2, CV.SPoint>:
60	  match ok:
61	    case True{}: CV.decompress(p(one), x, 0n)
62	    case False{}: None{}
63	
64	def lift_x(+one: Nat, +x: Nat) -> Maybe<&2, CV.SPoint>:
65	  lift_if(one, x, Nat.is_lt(x, p(one)))
66	
67	# fail if is_infinite(R) or not has_even_y(R) or x(R) != r
68	def check_r(+r: Nat, inf: Bool, a: CV.SAffine) -> Bool:
69	  match a:
70	    case CV.SAffine{x, y}: Bool.and(Bool.not(inf), Bool.and(Nat.is_eq(Nat.mod(y, 2n), 0n), Nat.is_eq(x, r)))
71	
72	# R = s G - e P with e = int(hash_challenge(r || pk || m)) mod n
73	def verify_rs(+one: Nat, +r: Nat, +s: Nat, +e: Nat, +pp: CV.SPoint) -> Bool:
74	  +rr = CV.padd(p(one), CV.pmul(p(one), s, CV.g(one)), CV.pmul(p(one), FS.mneg(n(one), e), pp))
75	  check_r(r, CV.is_inf(rr), CV.to_affine(p(one), rr))
76	
77	def verify_ok(+one: Nat, +r: Nat, +s: Nat, +e: Nat, +pp: CV.SPoint, ok: Bool) -> Bool:
78	  match ok:
79	    case True{}: verify_rs(one, r, s, e, pp)
80	    case False{}: False{}
81	
82	# fail if r >= p or s >= n
83	def verify_p(+one: Nat, +pk: List<&2, U32>, +m: List<&2, U32>, +sig: List<&2, U32>, mp: Maybe<&2, CV.SPoint>) -> Bool:
84	  match mp:
85	    case None{}: False{}
86	    case Some{+pp}:
87	      +r = CV.os2ip(CV.first(32n, sig))
88	      +s = CV.os2ip(CV.after(32n, sig))
89	      +e = Nat.mod(CV.os2ip(tagged(tag_challenge(), cat(CV.first(32n, sig), cat(pk, m)))), n(one))
90	      verify_ok(one, r, s, e, pp, Bool.and(Nat.is_lt(r, p(one)), Nat.is_lt(s, n(one))))
91	
92	def verify_len(+one: Nat, +pk: List<&2, U32>, +m: List<&2, U32>, +sig: List<&2, U32>, ok: Bool) -> Bool:
93	  match ok:
94	    case True{}: verify_p(one, pk, m, sig, lift_x(one, CV.os2ip(pk)))
95	    case False{}: False{}
96	
97	# Verify(pk, m, sig): pk 32 bytes, sig 64 bytes, m any length
98	def verify(+one: Nat, +pk: List<&2, U32>, +m: List<&2, U32>, +sig: List<&2, U32>) -> Bool:
99	  verify_len(one, pk, m, sig, Bool.and(CV.length_is(32n, pk), CV.length_is(64n, sig)))
100	
101	# ---- signing ----
102	
103	# d' = int(sk), 1 <= d' <= n - 1
104	def secret_ok(+one: Nat, +sk: List<&2, U32>) -> Bool:
105	  Bool.and(CV.length_is(32n, sk), Bool.and(Bool.not(Nat.is_eq(CV.os2ip(sk), 0n)), Nat.is_lt(CV.os2ip(sk), n(one))))
106	
107	def pub_of(a: CV.SAffine) -> List<&2, U32>:
108	  match a:
109	    case CV.SAffine{x, y}: bytes32(x)
110	
111	def pubkey_ok(+one: Nat, +sk: List<&2, U32>, ok: Bool) -> Maybe<&2, List<&2, U32>>:
112	  match ok:
113	    case True{}: Some{pub_of(CV.to_affine(p(one), CV.pmul(p(one), CV.os2ip(sk), CV.g(one))))}
114	    case False{}: None{}
115	
116	# PubKey(sk) = bytes(d' G)
117	def pubkey(+one: Nat, +sk: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
118	  pubkey_ok(one, sk, secret_ok(one, sk))
119	
120	# sig = bytes(R) || bytes((k + e d) mod n); if Verify(bytes(P), m, sig)
121	# fails, abort
122	def sign_if(+sig: List<&2, U32>, ok: Bool) -> Maybe<&2, List<&2, U32>>:
123	  match ok:
124	    case True{}: Some{sig}
125	    case False{}: None{}
126	
127	def sign_fin(+one: Nat, +pb: List<&2, U32>, +m: List<&2, U32>, +sig: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
128	  sign_if(sig, verify(one, pb, m, sig))
129	
130	# R = k' G; k = k' if has_even_y(R), otherwise n - k';
131	# e = int(hash_challenge(bytes(R) || bytes(P) || m)) mod n
132	def sign_r(+one: Nat, +d: Nat, +pb: List<&2, U32>, +m: List<&2, U32>, +k0: Nat, ra: CV.SAffine) -> Maybe<&2, List<&2, U32>>:
133	  match ra:
134	    case CV.SAffine{rx, +ry}:
135	      +k = even(n(one), ry, k0)
136	      +rb = bytes32(rx)
137	      +e = Nat.mod(CV.os2ip(tagged(tag_challenge(), cat(rb, cat(pb, m)))), n(one))
138	      sign_fin(one, pb, m, cat(rb, bytes32(FS.madd(n(one), k, FS.mmul(n(one), e, d)))))
139	
140	# k' = int(rand) mod n; fail if k' = 0
141	def sign_kz(+one: Nat, +d: Nat, +pb: List<&2, U32>, +m: List<&2, U32>, +k0: Nat, zero: Bool) -> Maybe<&2, List<&2, U32>>:
142	  match zero:
143	    case True{}: None{}
144	    case False{}: sign_r(one, d, pb, m, k0, CV.to_affine(p(one), CV.pmul(p(one), k0, CV.g(one))))
145	
146	def sign_k(+one: Nat, +d: Nat, +pb: List<&2, U32>, +m: List<&2, U32>, +k0: Nat) -> Maybe<&2, List<&2, U32>>:
147	  sign_kz(one, d, pb, m, k0, Nat.is_eq(k0, 0n))
148	
149	# P = d' G; d = d' if has_even_y(P), otherwise n - d';
150	# t = bytes(d) xor hash_aux(a); rand = hash_nonce(t || bytes(P) || m)
151	def sign_p(+one: Nat, +d0: Nat, +m: List<&2, U32>, +aux: List<&2, U32>, pa: CV.SAffine) -> Maybe<&2, List<&2, U32>>:
152	  match pa:
153	    case CV.SAffine{px, +py}:
154	      +d = even(n(one), py, d0)
155	      +pb = bytes32(px)
156	      +t = xor_bytes(bytes32(d), tagged(tag_aux(), aux))
157	      sign_k(one, d, pb, m, Nat.mod(CV.os2ip(tagged(tag_nonce(), cat(t, cat(pb, m)))), n(one)))
158	
159	def sign_ok(+one: Nat, +sk: List<&2, U32>, +m: List<&2, U32>, +aux: List<&2, U32>, ok: Bool) -> Maybe<&2, List<&2, U32>>:
160	  match ok:
161	    case True{}:
162	      +d0 = CV.os2ip(sk)
163	      sign_p(one, d0, m, aux, CV.to_affine(p(one), CV.pmul(p(one), d0, CV.g(one))))
164	    case False{}: None{}
165	
166	# Sign(sk, m, a): sk and a 32 bytes, m any length
167	def sign(+one: Nat, +sk: List<&2, U32>, +m: List<&2, U32>, +aux: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
168	  sign_ok(one, sk, m, aux, Bool.and(CV.length_is(32n, aux), secret_ok(one, sk)))