1	# JSON Web Tokens: HS256/384/512, RS256, and ES256 compact JWS sign and verify, claim checks, and JWKS keys over Hairpin. Source: https://github.com/paymog/bend-kit/tree/main/jwt
2	import Base
3	import bend-kit-crypto@0.2.0.0/crypto.bend as Crypto
4	import bend-kit-hairpin@0.2.1.0/hairpin.bend as Hairpin
5	import bend-kit-http@0.23.0.1/http.bend as Http
6	# By hash, as hairpin imports them: bend-kit-json@0.5.0.1, -bytes@0.3.0.0.
7	import 0x584fc27920487ceab242392391418d7f/json.bend as Json
8	import 0x49814d83de8f70993a43e1002be29ecd/bytes.bend as Bytes
9	
10	# RFC 7519 JWTs as RFC 7515 compact JWS. A token is ASCII text; header and claims are JSON objects.
11	# Times are unix seconds as U32 (to 2106). verify pins one alg: a header alg of "none", or of any other
12	# alg, fails. Each key kind serves only its algs, so a PEM public key can never become an HMAC secret.
13	
14	type Alg is Data:
15	  HS256{}
16	  HS384{}
17	  HS512{}
18	  RS256{}
19	  ES256{}
20	
21	# Hmac: the shared secret, at least the digest's size (RFC 7518 §3.2).
22	# Pem: a PEM "PUBLIC KEY" to verify, or an unencrypted PEM private key to sign.
23	# Rsa, Ec: JWK public key parts as big-endian octets (RFC 7518 §6.3, §6.2 on P-256).
24	type Key is Type:
25	  Hmac{secret: Bytes.Bytes}
26	  Pem{pem: Bytes.Bytes}
27	  Rsa{n: Bytes.Bytes, e: Bytes.Bytes}
28	  Ec{x: Bytes.Bytes, y: Bytes.Bytes}
29	
30	type Err is Data:
31	  Malformed{}
32	  AlgMismatch{}
33	  Crit{}
34	  KeyType{}
35	  WeakKey{}
36	  BadSig{}
37	  BadClaim{}
38	  Expired{}
39	  NotYet{}
40	  Future{}
41	  BadIss{}
42	  BadAud{}
43	  NoKey{}
44	  Crypto{code: U32, why: String}
45	  Net{e: Hairpin.Err}
46	  Status{code: U32}
47	
48	# What verify accepts: the one alg, the issuer and audience when Some, and leeway seconds of clock skew.
49	type Policy is Data:
50	  Policy{alg: Alg, iss: Maybe<&2, String>, aud: Maybe<&2, String>, leeway: U32}
51	
52	def policy(a: Alg) -> Policy:
53	  Policy{a, None{}, None{}, 0}
54	
55	def iss(p: Policy, s: String) -> Policy:
56	  Policy{a, old, u, l} = p
57	  Policy{a, Some{s}, u, l}
58	
59	def aud(p: Policy, s: String) -> Policy:
60	  Policy{a, i, old, l} = p
61	  Policy{a, i, Some{s}, l}
62	
63	def leeway(p: Policy, +n: U32) -> Policy:
64	  Policy{a, i, u, old} = p
65	  Policy{a, i, u, n}
66	
67	def policy.alg(p: Policy) -> Alg:
68	  Policy{a, i, u, l} = p
69	  a
70	
71	def alg.name(a: Alg) -> String:
72	  match a:
73	    case HS256{}:
74	      "HS256"
75	    case HS384{}:
76	      "HS384"
77	    case HS512{}:
78	      "HS512"
79	    case RS256{}:
80	      "RS256"
81	    case ES256{}:
82	      "ES256"
83	
84	# ---- base64url (RFC 4648 §5), unpadded, as RFC 7515 §2 requires
85	
86	def b64u.push(+c: U32, acc: String) -> String:
87	  match c:
88	    case 61:
89	      acc
90	    case 43:
91	      SCon{'-', acc}
92	    case 47:
93	      SCon{'_', acc}
94	    case _:
95	      SCon{Chr{c}, acc}
96	
97	def b64u.go(s: String, acc: String) -> String:
98	  match s:
99	    case SNil{}:
100	      String.reverse(acc)
101	    case SCon{Chr{+c}, t}:
102	      b64u.go(t, b64u.push(c, acc))
103	
104	def b64u(b: Bytes.Bytes) -> String:
105	  b64u.go(Bytes.to_base64(b), SNil{})
106	
107	# The standard alphabet's char for c. '+', '/', '=' and NUL become NUL, which no decoder accepts.
108	def unb64u.c(+c: U32) -> U32:
109	  match c:
110	    case 45:
111	      43
112	    case 95:
113	      47
114	    case 43:
115	      0
116	    case 47:
117	      0
118	    case 61:
119	      0
120	    case _:
121	      c
122	
123	# Padding for n mod 4 chars; 1 is never a whole group, so it gets a NUL.
124	def unb64u.pad(+r: U32, acc: String) -> String:
125	  match r:
126	    case 2:
127	      SCon{'=', SCon{'=', acc}}
128	    case 3:
129	      SCon{'=', acc}
130	    case 1:
131	      SCon{Chr{0}, acc}
132	    case _:
133	      acc
134	
135	def unb64u.go(s: String, acc: String, +n: U32) -> String:
136	  match s:
137	    case SNil{}:
138	      String.reverse(unb64u.pad((n .&. 3 : U32), acc))
139	    case SCon{Chr{+c}, t}:
140	      unb64u.go(t, SCon{Chr{unb64u.c(c)}, acc}, (n + 1 : U32))
141	
142	def unb64u.same(+s: String, r: Bytes.Bytes & Bytes.Bytes) -> Maybe<&1, Bytes.Bytes>:
143	  (b, c) = r
144	  Bool.pick(Maybe<&1, Bytes.Bytes>, String.eq(b64u(c), s), Some{b}, None{})
145	
146	def unb64u.canon(+s: String, m: Maybe<&1, Bytes.Bytes>) -> Maybe<&1, Bytes.Bytes>:
147	  match m:
148	    case None{}:
149	      None{}
150	    case Some{b}:
151	      unb64u.same(s, Bytes.slice(b, 0, 4294967295))
152	
153	# Strict: only the URL-safe alphabet, no '=', and only the canonical text of its octets, so pad bits are 0.
154	def unb64u(+s: String) -> Maybe<&1, Bytes.Bytes>:
155	  unb64u.canon(s, Bytes.from_base64(unb64u.go(s, SNil{}, 0)))
156	
157	# ---- JSON members as copyable facts
158	
159	# A NumericDate (RFC 7519 §2) rounded up to whole seconds and capped at the U32 top, or None when it is
160	# negative or has an exponent. Up is exact against a whole now: now >= t iff now >= ceil(t).
161	type Lit is Data:
162	  LStr{s: String}
163	  LNum{t: Maybe<&2, U32>}
164	  LStrs{xs: Maybe<&2, List<&2, String>>}
165	  LOther{}
166	
167	# One member: its name as octets, and what the checks need of its value.
168	type Field is Data:
169	  Field{name: String, val: Lit}
170	
171	def secs.digit(+acc: U32, +d: U32) -> U32:
172	  Bool.pick(U32, Bool.or(U32.is_lt(429496729, acc), Bool.and(U32.is_eq(acc, 429496729), U32.is_lt(5, d))), 4294967295, (acc * 10 + d : U32))
173	
174	def secs.up(+acc: U32, frac: Bool) -> U32:
175	  Bool.pick(U32, Bool.and(frac, U32.is_lt(acc, 4294967295)), (acc + 1 : U32), acc)
176	
177	# The JSON parser has checked the grammar, so only digits and one '.' need telling apart.
178	def secs.go(s: String, +acc: U32, +frac: Bool, +point: Bool, +ok: Bool) -> Maybe<&2, U32>:
179	  match s:
180	    case SNil{}:
181	      Bool.pick(Maybe<&2, U32>, ok, Some{secs.up(acc, frac)}, None{})
182	    case SCon{Chr{+c}, t}:
183	      +d = Bool.and(U32.is_le(48, c), U32.is_le(c, 57))
184	      +dot = U32.is_eq(c, 46)
185	      secs.go(t, Bool.pick(U32, Bool.or(point, Bool.not(d)), acc, secs.digit(acc, (c - 48 : U32))),
186	        Bool.or(frac, Bool.and(point, Bool.and(d, U32.is_ne(c, 48)))), Bool.or(point, dot),
187	        Bool.and(ok, Bool.or(d, Bool.and(dot, Bool.not(point)))))
188	
189	def secs(s: String) -> Maybe<&2, U32>:
190	  secs.go(s, 0, False{}, False{}, True{})
191	
192	def str.of(v: Json.Val) -> Maybe<&2, String>:
193	  match v:
194	    case Json.Str{s}:
195	      Some{Bytes.to_string(s)}
196	    case _:
197	      None{}
198	
199	def strs.push(s: Maybe<&2, String>, acc: Maybe<&2, List<&2, String>>) -> Maybe<&2, List<&2, String>>:
200	  match s acc:
201	    case Some{x} Some{l}:
202	      Some{Con{x, l}}
203	    case _ _:
204	      None{}
205	
206	def strs(xs: List<&1, Json.Val>, acc: Maybe<&2, List<&2, String>>) -> Maybe<&2, List<&2, String>>:
207	  match xs:
208	    case Nil{}:
209	      acc
210	    case x <> t:
211	      strs(t, strs.push(str.of(x), acc))
212	
213	def lit(v: Json.Val) -> Lit:
214	  match v:
215	    case Json.Str{s}:
216	      LStr{Bytes.to_string(s)}
217	    case Json.Num{s}:
218	      LNum{secs(Bytes.to_string(s))}
219	    case Json.Arr{xs}:
220	      LStrs{strs(xs, Some{Nil{}})}
221	    case _:
222	      LOther{}
223	
224	# An object's members, names as octets, last first.
225	def fields(kvs: List<&1, Bytes.Bytes & Json.Val>, acc: List<&2, Field>) -> List<&2, Field>:
226	  match kvs:
227	    case Nil{}:
228	      acc
229	    case (k, v) <> t:
230	      fields(t, Con{Field{Bytes.to_string(k), lit(v)}, acc})
231	
232	def field(l: List<&2, Field>, +k: String) -> Maybe<&2, Lit>:
233	  match l:
234	    case Nil{}:
235	      None{}
236	    case Field{n, x} <> t:
237	      Bool.pick(Maybe<&2, Lit>, String.eq(n, k), Some{x}, field(t, k))
238	
239	def has(l: List<&2, Field>, +k: String) -> Bool:
240	  match l:
241	    case Nil{}:
242	      False{}
243	    case Field{n, x} <> t:
244	      Bool.or(String.eq(n, k), has(t, k))
245	
246	# RFC 7515 §5.2 allows rejecting repeated names; a second "alg" is how parsers come to disagree.
247	def dup(l: List<&2, Field>) -> Bool:
248	  match l:
249	    case Nil{}:
250	      False{}
251	    case Con{Field{+n, x}, +t}:
252	      Bool.or(has(t, n), dup(t))
253	
254	def str(m: Maybe<&2, Lit>) -> Maybe<&2, String>:
255	  match m:
256	    case Some{LStr{s}}:
257	      Some{s}
258	    case _:
259	      None{}
260	
261	# ---- parsing
262	
263	# A compact JWS: the header and claim members, the claims, the signing input, and the signature.
264	type Parts is Type:
265	  Parts{head: List<&2, Field>, facts: List<&2, Field>, claims: Json.Val, input: Bytes.Bytes, sig: Bytes.Bytes}
266	
267	def parse.objs(hf: List<&2, Field>, ff: List<&2, Field>, cv: Json.Val, input: Bytes.Bytes, sig: Bytes.Bytes) ->
268	    Result<&1, &1, Err, Parts>:
269	  +h = hf
270	  +f = ff
271	  Bool.pick(Result<&1, &1, Err, Parts>, Bool.or(dup(h), dup(f)), Fail{Malformed{}}, Done{Parts{h, f, cv, input, sig}})
272	
273	def parse.json(h: Maybe<&1, Json.Val>, f: Maybe<&1, Json.Val>, c: Maybe<&1, Json.Val>, input: Bytes.Bytes, sig: Bytes.Bytes) ->
274	    Result<&1, &1, Err, Parts>:
275	  match h f c:
276	    case Some{Json.Obj{hk}} Some{Json.Obj{fk}} Some{cv}:
277	      parse.objs(fields(hk, Nil{}), fields(fk, Nil{}), cv, input, sig)
278	    case _ _ _:
279	      Fail{Malformed{}}
280	
281	def parse.claims(hb: Bytes.Bytes, r: Bytes.Bytes & Bytes.Bytes, input: Bytes.Bytes, sig: Bytes.Bytes) -> Result<&1, &1, Err, Parts>:
282	  (c1, c2) = r
283	  parse.json(Json.parse.bytes(hb), Json.parse.bytes(c1), Json.parse.bytes(c2), input, sig)
284	
285	def parse.segs(h: Maybe<&1, Bytes.Bytes>, c: Maybe<&1, Bytes.Bytes>, s: Maybe<&1, Bytes.Bytes>, input: Bytes.Bytes) ->
286	    Result<&1, &1, Err, Parts>:
287	  match h c s:
288	    case Some{hb} Some{cb} Some{sb}:
289	      parse.claims(hb, Bytes.slice(cb, 0, 4294967295), input, sb)
290	    case _ _ _:
291	      Fail{Malformed{}}
292	
293	def parse.split(xs: List<&2, String>) -> Result<&1, &1, Err, Parts>:
294	  match xs:
295	    case Con{+h, Con{+c, Con{+s, Nil{}}}}:
296	      parse.segs(unb64u(h), unb64u(c), unb64u(s), Bytes.from_string(h ++ "." ++ c))
297	    case _:
298	      Fail{Malformed{}}
299	
300	# Three strict base64url segments, the first two JSON objects with no repeated names.
301	def parse(token: String) -> Result<&1, &1, Err, Parts>:
302	  parse.split(String.split(token, '.'))
303	
304	# ---- checks
305	
306	def fail.if(bad: Bool, +e: Err) -> Result<&1, &1, Err, Unit>:
307	  match bad:
308	    case True{}:
309	      Fail{e}
310	    case False{}:
311	      Done{Unit{}}
312	
313	def head.alg(m: Maybe<&2, Lit>) -> Result<&1, &1, Err, String>:
314	  match m:
315	    case Some{LStr{s}}:
316	      Done{s}
317	    case _:
318	      Fail{Malformed{}}
319	
320	# The header's alg is exactly the pinned one, and it asks for no extension: crit (RFC 7515 §4.1.11) and
321	# b64 (RFC 7797) change how the token must be read, and neither is implemented.
322	def head.check(+a: Alg, +h: List<&2, Field>) -> Result<&1, &1, Err, Unit>:
323	  do Result<&1, &1, Err, Unit>:
324	    got : String <- head.alg(field(h, "alg"))
325	    u : Unit <- fail.if(Bool.not(String.eq(got, alg.name(a))), AlgMismatch{})
326	    fail.if(Bool.or(has(h, "crit"), has(h, "b64")), Crit{})
327	
328	def when(m: Maybe<&2, Lit>) -> Result<&1, &1, Err, Maybe<&2, U32>>:
329	  match m:
330	    case None{}:
331	      Done{None{}}
332	    case Some{LNum{Some{t}}}:
333	      Done{Some{t}}
334	    case Some{_}:
335	      Fail{BadClaim{}}
336	
337	def text(m: Maybe<&2, Lit>) -> Result<&1, &1, Err, Maybe<&2, String>>:
338	  match m:
339	    case None{}:
340	      Done{None{}}
341	    case Some{LStr{s}}:
342	      Done{Some{s}}
343	    case Some{_}:
344	      Fail{BadClaim{}}
345	
346	# RFC 7519 §4.1.3: aud is one string or an array of them.
347	def auds(m: Maybe<&2, Lit>) -> Result<&1, &1, Err, Maybe<&2, List<&2, String>>>:
348	  match m:
349	    case None{}:
350	      Done{None{}}
351	    case Some{LStr{s}}:
352	      Done{Some{[s]}}
353	    case Some{LStrs{Some{xs}}}:
354	      Done{Some{xs}}
355	    case Some{_}:
356	      Fail{BadClaim{}}
357	
358	# exp (RFC 7519 §4.1.4): now must be before it; late by at least leeway fails.
359	def late(+now: U32, +lw: U32, m: Maybe<&2, U32>) -> Bool:
360	  match m:
361	    case None{}:
362	      False{}
363	    case Some{+t}:
364	      Bool.and(U32.is_le(t, now), U32.is_le(lw, (now - t : U32)))
365	
366	# nbf and iat: at most leeway seconds in the future.
367	def early(+now: U32, +lw: U32, m: Maybe<&2, U32>) -> Bool:
368	  match m:
369	    case None{}:
370	      False{}
371	    case Some{+t}:
372	      Bool.and(U32.is_lt(now, t), U32.is_lt(lw, (t - now : U32)))
373	
374	def octets(s: String) -> String:
375	  Bytes.to_string(Json.utf8(s))
376	
377	def iss.bad(want: Maybe<&2, String>, got: Maybe<&2, String>) -> Bool:
378	  match want got:
379	    case None{} _:
380	      False{}
381	    case Some{w} Some{g}:
382	      Bool.not(String.eq(octets(w), g))
383	    case Some{w} None{}:
384	      True{}
385	
386	def aud.has(l: List<&2, String>, +a: String) -> Bool:
387	  match l:
388	    case Nil{}:
389	      False{}
390	    case x <> t:
391	      Bool.or(String.eq(x, a), aud.has(t, a))
392	
393	# RFC 7519 §4.1.3: a token with an aud that does not name us fails, as does one without aud when we want one.
394	def aud.bad(want: Maybe<&2, String>, got: Maybe<&2, List<&2, String>>) -> Bool:
395	  match want got:
396	    case None{} None{}:
397	      False{}
398	    case None{} Some{l}:
399	      True{}
400	    case Some{w} None{}:
401	      True{}
402	    case Some{w} Some{l}:
403	      Bool.not(aud.has(l, octets(w)))
404	
405	# The registered claims of c at unix time now.
406	def claims.check(p: Policy, +now: U32, +c: List<&2, Field>) -> Result<&1, &1, Err, Unit>:
407	  Policy{a, +wi, +wa, +lw} = p
408	  do Result<&1, &1, Err, Unit>:
409	    exp : Maybe<&2, U32> <- when(field(c, "exp"))
410	    nbf : Maybe<&2, U32> <- when(field(c, "nbf"))
411	    iat : Maybe<&2, U32> <- when(field(c, "iat"))
412	    gi : Maybe<&2, String> <- text(field(c, "iss"))
413	    ga : Maybe<&2, List<&2, String>> <- auds(field(c, "aud"))
414	    u1 : Unit <- fail.if(late(now, lw, exp), Expired{})
415	    u2 : Unit <- fail.if(early(now, lw, nbf), NotYet{})
416	    u3 : Unit <- fail.if(early(now, lw, iat), Future{})
417	    u4 : Unit <- fail.if(iss.bad(wi, gi), BadIss{})
418	    fail.if(aud.bad(wa, ga), BadAud{})
419	
420	def inspect.parts(+p: Policy, +now: U32, r: Result<&1, &1, Err, Parts>) -> Result<&1, &1, Err, Unit>:
421	  match r:
422	    case Fail{e}:
423	      Fail{e}
424	    case Done{Parts{+h, +f, v, input, sig}}:
425	      do Result<&1, &1, Err, Unit>:
426	        u : Unit <- head.check(policy.alg(p), h)
427	        claims.check(p, now, f)
428	
429	# The header and claims of token, without its signature: the pure half of verify.
430	def inspect(p: Policy, token: String, +now: U32) -> Result<&1, &1, Err, Unit>:
431	  inspect.parts(p, now, parse(token))
432	
433	# ---- signatures
434	
435	def crypto.bytes(r: Result<&1, &1, U32 & String, U32 & Array<U32>>) -> Result<&1, &1, Err, Bytes.Bytes>:
436	  match r:
437	    case Fail{(c, w)}:
438	      Fail{Crypto{c, w}}
439	    case Done{(n, b)}:
440	      Done{Bytes.Bytes{n, b}}
441	
442	def crypto.ok(r: Result<&1, &1, U32 & String, Bool>) -> Result<&1, &1, Err, Bool>:
443	  match r:
444	    case Fail{(c, w)}:
445	      Fail{Crypto{c, w}}
446	    case Done{b}:
447	      Done{b}
448	
449	def mac.if(weak: Bool, +alg: String, +kn: U32, kb: Array<U32>, +dn: U32, db: Array<U32>) ->
450	    IO(Result<&1, &1, Err, Bytes.Bytes>):
451	  match weak:
452	    case True{}:
453	      IO.pure(Result<&1, &1, Err, Bytes.Bytes>, Fail{WeakKey{}})
454	    case False{}:
455	      do IO<Result<&1, &1, Err, Bytes.Bytes>>:
456	        r : Result<&1, &1, U32 & String, U32 & Array<U32>> <- Crypto.hmac.words(alg, kn, kb, dn, db)
457	        return crypto.bytes(r)
458	
459	def mac(+alg: String, +min: U32, k: Bytes.Bytes, input: Bytes.Bytes) -> IO(Result<&1, &1, Err, Bytes.Bytes>):
460	  Bytes.Bytes{+kn, kb} = k
461	  Bytes.Bytes{+dn, db} = input
462	  mac.if(U32.is_lt(kn, min), alg, kn, kb, dn, db)
463	
464	def mac.cmp(m: Result<&1, &1, Err, Bytes.Bytes>, sig: Bytes.Bytes) -> IO(Result<&1, &1, Err, Bool>):
465	  match m:
466	    case Fail{e}:
467	      IO.pure(Result<&1, &1, Err, Bool>, Fail{e})
468	    case Done{Bytes.Bytes{+mn, mb}}:
469	      Bytes.Bytes{+sn, sb} = sig
470	      do IO<Result<&1, &1, Err, Bool>>:
471	        ok : Bool <- Crypto.eq.ct.words(mn, mb, sn, sb)
472	        return Done{ok}
473	
474	# The MAC compares in constant time.
475	def mac.check(+alg: String, +min: U32, k: Bytes.Bytes, input: Bytes.Bytes, sig: Bytes.Bytes) -> IO(Result<&1, &1, Err, Bool>):
476	  do IO<Result<&1, &1, Err, Bool>>:
477	    m : Result<&1, &1, Err, Bytes.Bytes> <- mac(alg, min, k, input)
478	    mac.cmp(m, sig)
479	
480	def rsa.pem(p: Bytes.Bytes, input: Bytes.Bytes, sig: Bytes.Bytes) -> IO(Result<&1, &1, Err, Bool>):
481	  Bytes.Bytes{+pn, pb} = p
482	  Bytes.Bytes{+dn, db} = input
483	  Bytes.Bytes{+sn, sb} = sig
484	  do IO<Result<&1, &1, Err, Bool>>:
485	    r : Result<&1, &1, U32 & String, Bool> <- Crypto.rsa.verify.words("SHA256", pn, pb, dn, db, sn, sb)
486	    return crypto.ok(r)
487	
488	def rsa.jwk(n: Bytes.Bytes, e: Bytes.Bytes, input: Bytes.Bytes, sig: Bytes.Bytes) -> IO(Result<&1, &1, Err, Bool>):
489	  Bytes.Bytes{+nn, nb} = n
490	  Bytes.Bytes{+en, eb} = e
491	  Bytes.Bytes{+dn, db} = input
492	  Bytes.Bytes{+sn, sb} = sig
493	  do IO<Result<&1, &1, Err, Bool>>:
494	    r : Result<&1, &1, U32 & String, Bool> <- Crypto.rsa.verify.jwk.words("SHA256", nn, nb, en, eb, dn, db, sn, sb)
495	    return crypto.ok(r)
496	
497	def ec.pem(p: Bytes.Bytes, input: Bytes.Bytes, sig: Bytes.Bytes) -> IO(Result<&1, &1, Err, Bool>):
498	  Bytes.Bytes{+pn, pb} = p
499	  Bytes.Bytes{+dn, db} = input
500	  Bytes.Bytes{+sn, sb} = sig
501	  do IO<Result<&1, &1, Err, Bool>>:
502	    r : Result<&1, &1, U32 & String, Bool> <- Crypto.ecdsa.verify.words("SHA256", pn, pb, dn, db, sn, sb)
503	    return crypto.ok(r)
504	
505	def ec.jwk(x: Bytes.Bytes, y: Bytes.Bytes, input: Bytes.Bytes, sig: Bytes.Bytes) -> IO(Result<&1, &1, Err, Bool>):
506	  Bytes.Bytes{+xn, xb} = x
507	  Bytes.Bytes{+yn, yb} = y
508	  Bytes.Bytes{+dn, db} = input
509	  Bytes.Bytes{+sn, sb} = sig
510	  do IO<Result<&1, &1, Err, Bool>>:
511	    r : Result<&1, &1, U32 & String, Bool> <- Crypto.ecdsa.verify.jwk.words("SHA256", xn, xb, yn, yb, dn, db, sn, sb)
512	    return crypto.ok(r)
513	
514	# Does sig sign input under key for alg? A key of the wrong kind fails with KeyType before any crypto.
515	def sig.check(a: Alg, key: Key, input: Bytes.Bytes, sig: Bytes.Bytes) -> IO(Result<&1, &1, Err, Bool>):
516	  match a key:
517	    case HS256{} Hmac{k}:
518	      mac.check("SHA256", 32, k, input, sig)
519	    case HS384{} Hmac{k}:
520	      mac.check("SHA384", 48, k, input, sig)
521	    case HS512{} Hmac{k}:
522	      mac.check("SHA512", 64, k, input, sig)
523	    case RS256{} Pem{p}:
524	      rsa.pem(p, input, sig)
525	    case RS256{} Rsa{n, e}:
526	      rsa.jwk(n, e, input, sig)
527	    case ES256{} Pem{p}:
528	      ec.pem(p, input, sig)
529	    case ES256{} Ec{x, y}:
530	      ec.jwk(x, y, input, sig)
531	    case _ _:
532	      IO.pure(Result<&1, &1, Err, Bool>, Fail{KeyType{}})
533	
534	def rsa.sign(p: Bytes.Bytes, input: Bytes.Bytes) -> IO(Result<&1, &1, Err, Bytes.Bytes>):
535	  Bytes.Bytes{+pn, pb} = p
536	  Bytes.Bytes{+dn, db} = input
537	  do IO<Result<&1, &1, Err, Bytes.Bytes>>:
538	    r : Result<&1, &1, U32 & String, U32 & Array<U32>> <- Crypto.rsa.sign.words("SHA256", pn, pb, dn, db)
539	    return crypto.bytes(r)
540	
541	def ec.sign(p: Bytes.Bytes, input: Bytes.Bytes) -> IO(Result<&1, &1, Err, Bytes.Bytes>):
542	  Bytes.Bytes{+pn, pb} = p
543	  Bytes.Bytes{+dn, db} = input
544	  do IO<Result<&1, &1, Err, Bytes.Bytes>>:
545	    r : Result<&1, &1, U32 & String, U32 & Array<U32>> <- Crypto.ecdsa.sign.words("SHA256", pn, pb, dn, db)
546	    return crypto.bytes(r)
547	
548	# The signature of input under key for alg. RS256 and ES256 sign with a PEM private key.
549	def sig.make(a: Alg, key: Key, input: Bytes.Bytes) -> IO(Result<&1, &1, Err, Bytes.Bytes>):
550	  match a key:
551	    case HS256{} Hmac{k}:
552	      mac("SHA256", 32, k, input)
553	    case HS384{} Hmac{k}:
554	      mac("SHA384", 48, k, input)
555	    case HS512{} Hmac{k}:
556	      mac("SHA512", 64, k, input)
557	    case RS256{} Pem{p}:
558	      rsa.sign(p, input)
559	    case ES256{} Pem{p}:
560	      ec.sign(p, input)
561	    case _ _:
562	      IO.pure(Result<&1, &1, Err, Bytes.Bytes>, Fail{KeyType{}})
563	
564	# ---- sign and verify
565	
566	def header.kid(m: Maybe<&2, String>) -> List<&1, Bytes.Bytes & Json.Val>:
567	  match m:
568	    case None{}:
569	      Nil{}
570	    case Some{k}:
571	      [(Json.utf8("kid"), Json.Str{Json.utf8(k)})]
572	
573	# {"alg":..,"typ":"JWT"}, then "kid" when given.
574	def header(a: Alg, kid: Maybe<&2, String>) -> Json.Val:
575	  Json.Obj{Con{(Json.utf8("alg"), Json.Str{Json.utf8(alg.name(a))}), Con{(Json.utf8("typ"), Json.Str{Json.utf8("JWT")}), header.kid(kid)}}}
576	
577	# header.body in base64url, body being the compact JSON claims: the text the signature covers.
578	def signing.input(a: Alg, kid: Maybe<&2, String>, body: Bytes.Bytes) -> String:
579	  b64u(Json.encode.bytes(header(a, kid))) ++ "." ++ b64u(body)
580	
581	def sign.done(+input: String, s: Result<&1, &1, Err, Bytes.Bytes>) -> Result<&1, &1, Err, String>:
582	  match s:
583	    case Fail{e}:
584	      Fail{e}
585	    case Done{b}:
586	      Done{input ++ "." ++ b64u(b)}
587	
588	# verify accepts only an object with no repeated names, so sign makes no other kind.
589	def sign.obj(m: Maybe<&1, Json.Val>) -> Bool:
590	  match m:
591	    case Some{Json.Obj{kvs}}:
592	      Bool.not(dup(fields(kvs, Nil{})))
593	    case _:
594	      False{}
595	
596	def sign.if(ok: Bool, +a: Alg, key: Key, kid: Maybe<&2, String>, body: Bytes.Bytes) -> IO(Result<&1, &1, Err, String>):
597	  match ok:
598	    case False{}:
599	      IO.pure(Result<&1, &1, Err, String>, Fail{BadClaim{}})
600	    case True{}:
601	      +input = signing.input(a, kid, body)
602	      do IO<Result<&1, &1, Err, String>>:
603	        s : Result<&1, &1, Err, Bytes.Bytes> <- sig.make(a, key, Bytes.from_string(input))
604	        return sign.done(input, s)
605	
606	def sign.body(+a: Alg, key: Key, kid: Maybe<&2, String>, r: Bytes.Bytes & Bytes.Bytes) -> IO(Result<&1, &1, Err, String>):
607	  (body, copy) = r
608	  sign.if(sign.obj(Json.parse.bytes(copy)), a, key, kid, body)
609	
610	# A compact token of claims signed with key for a; kid names the key in the header. Claims that are not
611	# an object, or repeat a name, fail with BadClaim.
612	def sign(+a: Alg, key: Key, kid: Maybe<&2, String>, claims: Json.Val) -> IO(Result<&1, &1, Err, String>):
613	  sign.body(a, key, kid, Bytes.slice(Json.encode.bytes(claims), 0, 4294967295))
614	
615	def claims.done(r: Result<&1, &1, Err, Unit>, v: Json.Val) -> Result<&1, &1, Err, Json.Val>:
616	  match r:
617	    case Fail{e}:
618	      Fail{e}
619	    case Done{u}:
620	      Done{v}
621	
622	def check.sig(ok: Bool, +p: Policy, +now: U32, +f: List<&2, Field>, v: Json.Val) -> Result<&1, &1, Err, Json.Val>:
623	  match ok:
624	    case False{}:
625	      Fail{BadSig{}}
626	    case True{}:
627	      claims.done(claims.check(p, now, f), v)
628	
629	def check.done(s: Result<&1, &1, Err, Bool>, +p: Policy, +now: U32, +f: List<&2, Field>, v: Json.Val) ->
630	    Result<&1, &1, Err, Json.Val>:
631	  match s:
632	    case Fail{e}:
633	      Fail{e}
634	    case Done{ok}:
635	      check.sig(ok, p, now, f, v)
636	
637	def check.pinned(ok: Result<&1, &1, Err, Unit>, +p: Policy, key: Key, +now: U32, +f: List<&2, Field>, v: Json.Val,
638	    input: Bytes.Bytes, sig: Bytes.Bytes) -> IO(Result<&1, &1, Err, Json.Val>):
639	  match ok:
640	    case Fail{e}:
641	      IO.pure(Result<&1, &1, Err, Json.Val>, Fail{e})
642	    case Done{u}:
643	      do IO<Result<&1, &1, Err, Json.Val>>:
644	        s : Result<&1, &1, Err, Bool> <- sig.check(policy.alg(p), key, input, sig)
645	        return check.done(s, p, now, f, v)
646	
647	# The pinned alg, then the signature, then the claims.
648	def check(+p: Policy, key: Key, +now: U32, parts: Parts) -> IO(Result<&1, &1, Err, Json.Val>):
649	  Parts{+h, +f, v, input, sig} = parts
650	  check.pinned(head.check(policy.alg(p), h), p, key, now, f, v, input, sig)
651	
652	def verify.parsed(+p: Policy, key: Key, +now: U32, r: Result<&1, &1, Err, Parts>) -> IO(Result<&1, &1, Err, Json.Val>):
653	  match r:
654	    case Fail{e}:
655	      IO.pure(Result<&1, &1, Err, Json.Val>, Fail{e})
656	    case Done{parts}:
657	      check(p, key, now, parts)
658	
659	# The claims of token when it is signed by key under p's alg and its claims hold at unix time now.
660	def verify(+p: Policy, key: Key, token: String, +now: U32) -> IO(Result<&1, &1, Err, Json.Val>):
661	  verify.parsed(p, key, now, parse(token))
662	
663	# ---- JWKS (RFC 7517)
664	
665	# A usable public key from a set: its kid, RSA or EC P-256, its alg ("" when the set gives none), and its
666	# two base64url parts (n and e, or x and y).
667	type Jwk is Data:
668	  Jwk{kid: String, rsa: Bool, alg: String, a: String, b: String}
669	
670	def jwk.two(+rsa: Bool, +kid: String, +alg: String, a: Maybe<&2, String>, b: Maybe<&2, String>) -> Maybe<&2, Jwk>:
671	  match a b:
672	    case Some{x} Some{y}:
673	      Some{Jwk{kid, rsa, alg, x, y}}
674	    case _ _:
675	      None{}
676	
677	# An alg member that is not a string can match no pinned alg.
678	def jwk.alg(m: Maybe<&2, Lit>) -> String:
679	  match m:
680	    case None{}:
681	      ""
682	    case Some{LStr{s}}:
683	      s
684	    case Some{_}:
685	      "?"
686	
687	def jwk.use(m: Maybe<&2, Lit>) -> Maybe<&2, Unit>:
688	  match m:
689	    case None{}:
690	      Some{Unit{}}
691	    case Some{LStr{s}}:
692	      Bool.pick(Maybe<&2, Unit>, String.eq(s, "sig"), Some{Unit{}}, None{})
693	    case Some{_}:
694	      None{}
695	
696	def jwk.kty(+kty: String, +kid: String, +f: List<&2, Field>) -> Maybe<&2, Jwk>:
697	  +alg = jwk.alg(field(f, "alg"))
698	  +ec = Bool.and(String.eq(kty, "EC"), String.eq(Maybe.default(&2, String, str(field(f, "crv")), ""), "P-256"))
699	  Bool.pick(Maybe<&2, Jwk>, String.eq(kty, "RSA"), jwk.two(True{}, kid, alg, str(field(f, "n")), str(field(f, "e"))),
700	    Bool.pick(Maybe<&2, Jwk>, ec, jwk.two(False{}, kid, alg, str(field(f, "x")), str(field(f, "y"))), None{}))
701	
702	def jwk.fields(+f: List<&2, Field>) -> Maybe<&2, Jwk>:
703	  do Maybe<&2, Jwk>:
704	    u : Unit <- Bool.pick(Maybe<&2, Unit>, dup(f), None{}, Some{Unit{}})
705	    kty : String <- str(field(f, "kty"))
706	    kid : String <- str(field(f, "kid"))
707	    s : Unit <- jwk.use(field(f, "use"))
708	    jwk.kty(kty, kid, f)
709	
710	def jwk.of(v: Json.Val) -> Maybe<&2, Jwk>:
711	  match v:
712	    case Json.Obj{kvs}:
713	      jwk.fields(fields(kvs, Nil{}))
714	    case _:
715	      None{}
716	
717	def jwk.push(m: Maybe<&2, Jwk>, acc: List<&2, Jwk>) -> List<&2, Jwk>:
718	  match m:
719	    case None{}:
720	      acc
721	    case Some{k}:
722	      Con{k, acc}
723	
724	def jwks.go(xs: List<&1, Json.Val>, acc: List<&2, Jwk>) -> List<&2, Jwk>:
725	  match xs:
726	    case Nil{}:
727	      List.reverse(&2, Jwk, acc)
728	    case x <> t:
729	      jwks.go(t, jwk.push(jwk.of(x), acc))
730	
731	def jwks.arr(m: Maybe<&1, Json.Val>) -> Maybe<&2, List<&2, Jwk>>:
732	  match m:
733	    case Some{Json.Arr{xs}}:
734	      Some{jwks.go(xs, Nil{})}
735	    case _:
736	      None{}
737	
738	def jwks.doc(m: Maybe<&1, Json.Val>) -> Maybe<&2, List<&2, Jwk>>:
739	  match m:
740	    case Some{v}:
741	      jwks.arr(Json.get(v, "keys"))
742	    case None{}:
743	      None{}
744	
745	# The signing keys of a JWK Set document; members it cannot use (enc keys, other curves, oct) are skipped.
746	# None when the document is not {"keys": [...]}.
747	def jwks.parse(b: Bytes.Bytes) -> Maybe<&2, List<&2, Jwk>>:
748	  jwks.doc(Json.parse.bytes(b))
749	
750	def fam(a: Alg) -> U32:
751	  match a:
752	    case RS256{}:
753	      1
754	    case ES256{}:
755	      2
756	    case _:
757	      0
758	
759	def jwk.fits(k: Jwk, +kid: String, +a: Alg) -> Bool:
760	  Jwk{k2, +rsa, +ka, x, y} = k
761	  Bool.and(Bool.and(String.eq(k2, kid), U32.is_eq(fam(a), Bool.pick(U32, rsa, 1, 2))),
762	    Bool.or(String.eq(ka, ""), String.eq(ka, alg.name(a))))
763	
764	# The first key named kid that can check alg a. RFC 7515 §4.1.4 leaves kid matching to exact comparison.
765	def jwk.pick(ks: List<&2, Jwk>, +kid: String, +a: Alg) -> Maybe<&2, Jwk>:
766	  match ks:
767	    case Nil{}:
768	      None{}
769	    case Con{+k, t}:
770	      Bool.pick(Maybe<&2, Jwk>, jwk.fits(k, kid, a), Some{k}, jwk.pick(t, kid, a))
771	
772	def jwk.key.of(rsa: Bool, a: Maybe<&1, Bytes.Bytes>, b: Maybe<&1, Bytes.Bytes>) -> Result<&1, &1, Err, Key>:
773	  match rsa a b:
774	    case True{} Some{n} Some{e}:
775	      Done{Rsa{n, e}}
776	    case False{} Some{x} Some{y}:
777	      Done{Ec{x, y}}
778	    case _ _ _:
779	      Fail{Malformed{}}
780	
781	# A set member as a verify key.
782	def jwk.key(k: Jwk) -> Result<&1, &1, Err, Key>:
783	  Jwk{kid, +rsa, alg, +a, +b} = k
784	  jwk.key.of(rsa, unb64u(a), unb64u(b))
785	
786	def jwk.found(m: Maybe<&2, Jwk>) -> Result<&1, &1, Err, Key>:
787	  match m:
788	    case None{}:
789	      Fail{NoKey{}}
790	    case Some{k}:
791	      jwk.key(k)
792	
793	# A cached key set from the caller's own trusted url; a token never picks the url (jku and x5u are ignored).
794	# live: fetched once; at: the unix time of the last good fetch; ttl: seconds it stays fresh;
795	# tried: the unix time of the last fetch, good or not.
796	type Jwks is Data:
797	  Jwks{url: String, ttl: U32, live: Bool, at: U32, tried: Maybe<&2, U32>, keys: List<&2, Jwk>}
798	
799	def jwks(url: String, +ttl: U32) -> Jwks:
800	  Jwks{url, ttl, False{}, 0, None{}, Nil{}}
801	
802	def jwks.keys(s: Jwks) -> List<&2, Jwk>:
803	  Jwks{u, t, l, a, tr, ks} = s
804	  ks
805	
806	def fetch.keys(m: Maybe<&2, List<&2, Jwk>>, c: Hairpin.Client, s: Jwks, +now: U32) -> Hairpin.Client & Jwks & Result<&1, &1, Err, Unit>:
807	  match m:
808	    case None{}:
809	      (c, s, Fail{Malformed{}})
810	    case Some{ks}:
811	      Jwks{url, ttl, live, at, tried, old} = s
812	      (c, Jwks{url, ttl, True{}, now, tried, ks}, Done{Unit{}})
813	
814	def fetch.body(ok: Bool, +status: U32, c: Hairpin.Client, s: Jwks, +now: U32, b: Bytes.Bytes) ->
815	    Hairpin.Client & Jwks & Result<&1, &1, Err, Unit>:
816	  match ok:
817	    case False{}:
818	      (c, s, Fail{Status{status}})
819	    case True{}:
820	      fetch.keys(jwks.parse(b), c, s, now)
821	
822	def fetch.res(c: Hairpin.Client, s: Jwks, +now: U32, r: Result<&1, &1, Hairpin.Err, Http.Res>) ->
823	    Hairpin.Client & Jwks & Result<&1, &1, Err, Unit>:
824	  match r:
825	    case Fail{e}:
826	      (c, s, Fail{Net{e}})
827	    case Done{Http.Res{+status, h, b}}:
828	      fetch.body(U32.is_eq(status, 200), status, c, s, now, b)
829	
830	def fetch.done(s: Jwks, +now: U32, x: Hairpin.Client & Result<&1, &1, Hairpin.Err, Http.Res>) ->
831	    Hairpin.Client & Jwks & Result<&1, &1, Err, Unit>:
832	  (c, r) = x
833	  fetch.res(c, s, now, r)
834	
835	# GET the set now. On any failure the client and the old keys come back, with only tried moved to now.
836	def fetch(c: Hairpin.Client, s: Jwks, +now: U32) -> IO(Hairpin.Client & Jwks & Result<&1, &1, Err, Unit>):
837	  Jwks{+url, ttl, live, at, old, ks} = s
838	  do IO<Hairpin.Client & Jwks & Result<&1, &1, Err, Unit>>:
839	    x : Hairpin.Client & Result<&1, &1, Hairpin.Err, Http.Res> <- Hairpin.get(c, url)
840	    return fetch.done(Jwks{url, ttl, live, at, Some{now}, ks}, now, x)
841	
842	def key.after.r(r: Result<&1, &1, Err, Unit>, c: Hairpin.Client, +s: Jwks, +kid: String, +a: Alg) ->
843	    Hairpin.Client & Jwks & Result<&1, &1, Err, Key>:
844	  match r:
845	    case Fail{e}:
846	      (c, s, Fail{e})
847	    case Done{u}:
848	      (c, s, jwk.found(jwk.pick(jwks.keys(s), kid, a)))
849	
850	def key.after(+kid: String, +a: Alg, x: Hairpin.Client & Jwks & Result<&1, &1, Err, Unit>) ->
851	    Hairpin.Client & Jwks & Result<&1, &1, Err, Key>:
852	  (c, s, r) = x
853	  key.after.r(r, c, s, kid, a)
854	
855	def key.refetch(go: Bool, c: Hairpin.Client, s: Jwks, +kid: String, +a: Alg, +now: U32) ->
856	    IO(Hairpin.Client & Jwks & Result<&1, &1, Err, Key>):
857	  match go:
858	    case False{}:
859	      IO.pure(Hairpin.Client & Jwks & Result<&1, &1, Err, Key>, (c, s, Fail{NoKey{}}))
860	    case True{}:
861	      do IO<Hairpin.Client & Jwks & Result<&1, &1, Err, Key>>:
862	        x : Hairpin.Client & Jwks & Result<&1, &1, Err, Unit> <- fetch(c, s, now)
863	        return key.after(kid, a, x)
864	
865	def key.go(cached: Bool, +go: Bool, c: Hairpin.Client, s: Jwks, found: Maybe<&2, Jwk>, +kid: String, +a: Alg, +now: U32) ->
866	    IO(Hairpin.Client & Jwks & Result<&1, &1, Err, Key>):
867	  match cached:
868	    case True{}:
869	      IO.pure(Hairpin.Client & Jwks & Result<&1, &1, Err, Key>, (c, s, jwk.found(found)))
870	    case False{}:
871	      key.refetch(go, c, s, kid, a, now)
872	
873	def since(+now: U32, m: Maybe<&2, U32>) -> U32:
874	  match m:
875	    case None{}:
876	      4294967295
877	    case Some{+t}:
878	      Bool.pick(U32, U32.is_le(t, now), (now - t : U32), 0)
879	
880	# The verify key named kid for alg a. A known key stays usable through the 60 s fetch cooldown even
881	# when ttl is shorter. After that, refresh a stale set or an unknown kid at most once a minute.
882	# ponytail: fixed 60 s cooldown; make it a Jwks field if an issuer rotates faster.
883	def key(c: Hairpin.Client, s: Jwks, +kid: String, +a: Alg, +now: U32) -> IO(Hairpin.Client & Jwks & Result<&1, &1, Err, Key>):
884	  Jwks{+url, +ttl, +live, +at, +tried, +ks} = s
885	  +found = jwk.pick(ks, kid, a)
886	  +fresh = Bool.and(live, Bool.and(U32.is_le(at, now), U32.is_lt((now - at : U32), Bool.pick(U32, U32.is_lt(ttl, 60), 60, ttl))))
887	  +cached = Bool.and(fresh, Maybe.is_some(&2, Jwk, found))
888	  key.go(cached, U32.is_le(60, since(now, tried)), c, Jwks{url, ttl, live, at, tried, ks}, found, kid, a, now)
889	
890	def jwks.run(r: Result<&1, &1, Err, Key>, c: Hairpin.Client, s: Jwks, +p: Policy, +now: U32, parts: Parts) ->
891	    IO(Hairpin.Client & Jwks & Result<&1, &1, Err, Json.Val>):
892	  match r:
893	    case Fail{e}:
894	      IO.pure(Hairpin.Client & Jwks & Result<&1, &1, Err, Json.Val>, (c, s, Fail{e}))
895	    case Done{k}:
896	      do IO<Hairpin.Client & Jwks & Result<&1, &1, Err, Json.Val>>:
897	        v : Result<&1, &1, Err, Json.Val> <- check(p, k, now, parts)
898	        return (c, s, v)
899	
900	def jwks.keyed(+p: Policy, +now: U32, parts: Parts, x: Hairpin.Client & Jwks & Result<&1, &1, Err, Key>) ->
901	    IO(Hairpin.Client & Jwks & Result<&1, &1, Err, Json.Val>):
902	  (c, s, r) = x
903	  jwks.run(r, c, s, p, now, parts)
904	
905	def jwks.kid(k: Maybe<&2, String>, +p: Policy, c: Hairpin.Client, s: Jwks, +now: U32, parts: Parts) ->
906	    IO(Hairpin.Client & Jwks & Result<&1, &1, Err, Json.Val>):
907	  match k:
908	    case None{}:
909	      IO.pure(Hairpin.Client & Jwks & Result<&1, &1, Err, Json.Val>, (c, s, Fail{NoKey{}}))
910	    case Some{+kid}:
911	      do IO<Hairpin.Client & Jwks & Result<&1, &1, Err, Json.Val>>:
912	        x : Hairpin.Client & Jwks & Result<&1, &1, Err, Key> <- key(c, s, kid, policy.alg(p), now)
913	        jwks.keyed(p, now, parts, x)
914	
915	def jwks.pinned(ok: Result<&1, &1, Err, Unit>, +p: Policy, c: Hairpin.Client, s: Jwks, +now: U32, +h: List<&2, Field>,
916	    parts: Parts) -> IO(Hairpin.Client & Jwks & Result<&1, &1, Err, Json.Val>):
917	  match ok:
918	    case Fail{e}:
919	      IO.pure(Hairpin.Client & Jwks & Result<&1, &1, Err, Json.Val>, (c, s, Fail{e}))
920	    case Done{u}:
921	      jwks.kid(str(field(h, "kid")), p, c, s, now, parts)
922	
923	def jwks.parsed(+p: Policy, c: Hairpin.Client, s: Jwks, +now: U32, r: Result<&1, &1, Err, Parts>) ->
924	    IO(Hairpin.Client & Jwks & Result<&1, &1, Err, Json.Val>):
925	  match r:
926	    case Fail{e}:
927	      IO.pure(Hairpin.Client & Jwks & Result<&1, &1, Err, Json.Val>, (c, s, Fail{e}))
928	    case Done{Parts{+h, f, v, input, sig}}:
929	      jwks.pinned(head.check(policy.alg(p), h), p, c, s, now, h, Parts{h, f, v, input, sig})
930	
931	# verify with the key the token's kid names in the set. The alg is pinned before any fetch.
932	# The client and the set (refreshed or not) always come back.
933	def verify.jwks(+p: Policy, c: Hairpin.Client, s: Jwks, token: String, +now: U32) ->
934	    IO(Hairpin.Client & Jwks & Result<&1, &1, Err, Json.Val>):
935	  jwks.parsed(p, c, s, now, parse(token))