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