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.13.0.0/hairpin.bend as Hairpin
5	import bend-kit-http@0.38.0.0/http.bend as Http
6	import bend-kit-json@0.7.0.0/json.bend as Json
7	import bend-kit-bytes@0.3.3.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	def str(m: Maybe<&2, Lit>) -> Maybe<&2, String>:
246	  match m:
247	    case Some{LStr{s}}:
248	      Some{s}
249	    case _:
250	      None{}
251	
252	# ---- parsing
253	
254	# A compact JWS: the header and claim members, the claims, the signing input, and the signature.
255	type Parts is Type:
256	  Parts{head: List<&2, Field>, facts: List<&2, Field>, claims: Json.Val, input: Bytes.Bytes, sig: Bytes.Bytes}
257	
258	# RFC 7515 §5.2 allows rejecting repeated names; a second "alg" is how parsers come to disagree.
259	# parse.claims rejects them at every depth with Json.unique.parsed before members get here.
260	def parse.json(h: Maybe<&1, Json.Val>, f: Maybe<&1, Json.Val>, c: Maybe<&1, Json.Val>, input: Bytes.Bytes, sig: Bytes.Bytes) ->
261	    Result<&1, &1, Err, Parts>:
262	  match h f c:
263	    case Some{Json.Obj{hk}} Some{Json.Obj{fk}} Some{cv}:
264	      Done{Parts{fields(hk, Nil{}), fields(fk, Nil{}), cv, input, sig}}
265	    case _ _ _:
266	      Fail{Malformed{}}
267	
268	def parse.claims(hb: Bytes.Bytes, r: Bytes.Bytes & Bytes.Bytes, input: Bytes.Bytes, sig: Bytes.Bytes) -> Result<&1, &1, Err, Parts>:
269	  (c1, c2) = r
270	  parse.json(Json.unique.parsed(Json.parse.bytes(hb)), Json.unique.parsed(Json.parse.bytes(c1)), Json.parse.bytes(c2), input, sig)
271	
272	def parse.segs(h: Maybe<&1, Bytes.Bytes>, c: Maybe<&1, Bytes.Bytes>, s: Maybe<&1, Bytes.Bytes>, input: Bytes.Bytes) ->
273	    Result<&1, &1, Err, Parts>:
274	  match h c s:
275	    case Some{hb} Some{cb} Some{sb}:
276	      parse.claims(hb, Bytes.slice(cb, 0, 4294967295), input, sb)
277	    case _ _ _:
278	      Fail{Malformed{}}
279	
280	def parse.split(xs: List<&2, String>) -> Result<&1, &1, Err, Parts>:
281	  match xs:
282	    case Con{+h, Con{+c, Con{+s, Nil{}}}}:
283	      parse.segs(unb64u(h), unb64u(c), unb64u(s), Bytes.from_string(h ++ "." ++ c))
284	    case _:
285	      Fail{Malformed{}}
286	
287	# Three strict base64url segments, the first two JSON objects with no repeated names.
288	def parse(token: String) -> Result<&1, &1, Err, Parts>:
289	  parse.split(String.split(token, '.'))
290	
291	# ---- checks
292	
293	def fail.if(bad: Bool, +e: Err) -> Result<&1, &1, Err, Unit>:
294	  match bad:
295	    case True{}:
296	      Fail{e}
297	    case False{}:
298	      Done{Unit{}}
299	
300	def head.alg(m: Maybe<&2, Lit>) -> Result<&1, &1, Err, String>:
301	  match m:
302	    case Some{LStr{s}}:
303	      Done{s}
304	    case _:
305	      Fail{Malformed{}}
306	
307	# The header's alg is exactly the pinned one, and it asks for no extension: crit (RFC 7515 §4.1.11) and
308	# b64 (RFC 7797) change how the token must be read, and neither is implemented.
309	def head.check(+a: Alg, +h: List<&2, Field>) -> Result<&1, &1, Err, Unit>:
310	  do Result<&1, &1, Err, Unit>:
311	    got : String <- head.alg(field(h, "alg"))
312	    u : Unit <- fail.if(Bool.not(String.eq(got, alg.name(a))), AlgMismatch{})
313	    fail.if(Bool.or(has(h, "crit"), has(h, "b64")), Crit{})
314	
315	def when(m: Maybe<&2, Lit>) -> Result<&1, &1, Err, Maybe<&2, U32>>:
316	  match m:
317	    case None{}:
318	      Done{None{}}
319	    case Some{LNum{Some{t}}}:
320	      Done{Some{t}}
321	    case Some{_}:
322	      Fail{BadClaim{}}
323	
324	def text(m: Maybe<&2, Lit>) -> Result<&1, &1, Err, Maybe<&2, String>>:
325	  match m:
326	    case None{}:
327	      Done{None{}}
328	    case Some{LStr{s}}:
329	      Done{Some{s}}
330	    case Some{_}:
331	      Fail{BadClaim{}}
332	
333	# RFC 7519 §4.1.3: aud is one string or an array of them.
334	def auds(m: Maybe<&2, Lit>) -> Result<&1, &1, Err, Maybe<&2, List<&2, String>>>:
335	  match m:
336	    case None{}:
337	      Done{None{}}
338	    case Some{LStr{s}}:
339	      Done{Some{[s]}}
340	    case Some{LStrs{Some{xs}}}:
341	      Done{Some{xs}}
342	    case Some{_}:
343	      Fail{BadClaim{}}
344	
345	# exp (RFC 7519 §4.1.4): now must be before it; late by at least leeway fails.
346	def late(+now: U32, +lw: U32, m: Maybe<&2, U32>) -> Bool:
347	  match m:
348	    case None{}:
349	      False{}
350	    case Some{+t}:
351	      Bool.and(U32.is_le(t, now), U32.is_le(lw, (now - t : U32)))
352	
353	# nbf and iat: at most leeway seconds in the future.
354	def early(+now: U32, +lw: U32, m: Maybe<&2, U32>) -> Bool:
355	  match m:
356	    case None{}:
357	      False{}
358	    case Some{+t}:
359	      Bool.and(U32.is_lt(now, t), U32.is_lt(lw, (t - now : U32)))
360	
361	def octets(s: String) -> String:
362	  Bytes.to_string(Json.utf8(s))
363	
364	def iss.bad(want: Maybe<&2, String>, got: Maybe<&2, String>) -> Bool:
365	  match want got:
366	    case None{} _:
367	      False{}
368	    case Some{w} Some{g}:
369	      Bool.not(String.eq(octets(w), g))
370	    case Some{w} None{}:
371	      True{}
372	
373	def aud.has(l: List<&2, String>, +a: String) -> Bool:
374	  match l:
375	    case Nil{}:
376	      False{}
377	    case x <> t:
378	      Bool.or(String.eq(x, a), aud.has(t, a))
379	
380	# 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.
381	def aud.bad(want: Maybe<&2, String>, got: Maybe<&2, List<&2, String>>) -> Bool:
382	  match want got:
383	    case None{} None{}:
384	      False{}
385	    case None{} Some{l}:
386	      True{}
387	    case Some{w} None{}:
388	      True{}
389	    case Some{w} Some{l}:
390	      Bool.not(aud.has(l, octets(w)))
391	
392	# The registered claims of c at unix time now.
393	def claims.check(p: Policy, +now: U32, +c: List<&2, Field>) -> Result<&1, &1, Err, Unit>:
394	  Policy{a, +wi, +wa, +lw} = p
395	  do Result<&1, &1, Err, Unit>:
396	    exp : Maybe<&2, U32> <- when(field(c, "exp"))
397	    nbf : Maybe<&2, U32> <- when(field(c, "nbf"))
398	    iat : Maybe<&2, U32> <- when(field(c, "iat"))
399	    gi : Maybe<&2, String> <- text(field(c, "iss"))
400	    ga : Maybe<&2, List<&2, String>> <- auds(field(c, "aud"))
401	    u1 : Unit <- fail.if(late(now, lw, exp), Expired{})
402	    u2 : Unit <- fail.if(early(now, lw, nbf), NotYet{})
403	    u3 : Unit <- fail.if(early(now, lw, iat), Future{})
404	    u4 : Unit <- fail.if(iss.bad(wi, gi), BadIss{})
405	    fail.if(aud.bad(wa, ga), BadAud{})
406	
407	def inspect.parts(+p: Policy, +now: U32, r: Result<&1, &1, Err, Parts>) -> Result<&1, &1, Err, Unit>:
408	  match r:
409	    case Fail{e}:
410	      Fail{e}
411	    case Done{Parts{+h, +f, v, input, sig}}:
412	      do Result<&1, &1, Err, Unit>:
413	        u : Unit <- head.check(policy.alg(p), h)
414	        claims.check(p, now, f)
415	
416	# The header and claims of token, without its signature: the pure half of verify.
417	def inspect(p: Policy, token: String, +now: U32) -> Result<&1, &1, Err, Unit>:
418	  inspect.parts(p, now, parse(token))
419	
420	# ---- signatures
421	
422	def crypto.bytes(r: Result<&1, &1, U32 & String, U32 & Array<U32>>) -> Result<&1, &1, Err, Bytes.Bytes>:
423	  match r:
424	    case Fail{(c, w)}:
425	      Fail{Crypto{c, w}}
426	    case Done{(n, b)}:
427	      Done{Bytes.Bytes{n, b}}
428	
429	def crypto.ok(r: Result<&1, &1, U32 & String, Bool>) -> Result<&1, &1, Err, Bool>:
430	  match r:
431	    case Fail{(c, w)}:
432	      Fail{Crypto{c, w}}
433	    case Done{b}:
434	      Done{b}
435	
436	def mac.if(weak: Bool, +alg: String, +kn: U32, kb: Array<U32>, +dn: U32, db: Array<U32>) ->
437	    IO(Result<&1, &1, Err, Bytes.Bytes>):
438	  match weak:
439	    case True{}:
440	      IO.pure(Result<&1, &1, Err, Bytes.Bytes>, Fail{WeakKey{}})
441	    case False{}:
442	      do IO<Result<&1, &1, Err, Bytes.Bytes>>:
443	        r : Result<&1, &1, U32 & String, U32 & Array<U32>> <- Crypto.hmac.words(alg, kn, kb, dn, db)
444	        return crypto.bytes(r)
445	
446	def mac(+alg: String, +min: U32, k: Bytes.Bytes, input: Bytes.Bytes) -> IO(Result<&1, &1, Err, Bytes.Bytes>):
447	  Bytes.Bytes{+kn, kb} = k
448	  Bytes.Bytes{+dn, db} = input
449	  mac.if(U32.is_lt(kn, min), alg, kn, kb, dn, db)
450	
451	def mac.cmp(m: Result<&1, &1, Err, Bytes.Bytes>, sig: Bytes.Bytes) -> IO(Result<&1, &1, Err, Bool>):
452	  match m:
453	    case Fail{e}:
454	      IO.pure(Result<&1, &1, Err, Bool>, Fail{e})
455	    case Done{Bytes.Bytes{+mn, mb}}:
456	      Bytes.Bytes{+sn, sb} = sig
457	      do IO<Result<&1, &1, Err, Bool>>:
458	        ok : Bool <- Crypto.eq.ct.words(mn, mb, sn, sb)
459	        return Done{ok}
460	
461	# The MAC compares in constant time.
462	def mac.check(+alg: String, +min: U32, k: Bytes.Bytes, input: Bytes.Bytes, sig: Bytes.Bytes) -> IO(Result<&1, &1, Err, Bool>):
463	  do IO<Result<&1, &1, Err, Bool>>:
464	    m : Result<&1, &1, Err, Bytes.Bytes> <- mac(alg, min, k, input)
465	    mac.cmp(m, sig)
466	
467	def rsa.pem(p: Bytes.Bytes, input: Bytes.Bytes, sig: Bytes.Bytes) -> IO(Result<&1, &1, Err, Bool>):
468	  Bytes.Bytes{+pn, pb} = p
469	  Bytes.Bytes{+dn, db} = input
470	  Bytes.Bytes{+sn, sb} = sig
471	  do IO<Result<&1, &1, Err, Bool>>:
472	    r : Result<&1, &1, U32 & String, Bool> <- Crypto.rsa.verify.words("SHA256", pn, pb, dn, db, sn, sb)
473	    return crypto.ok(r)
474	
475	def rsa.jwk(n: Bytes.Bytes, e: Bytes.Bytes, input: Bytes.Bytes, sig: Bytes.Bytes) -> IO(Result<&1, &1, Err, Bool>):
476	  Bytes.Bytes{+nn, nb} = n
477	  Bytes.Bytes{+en, eb} = e
478	  Bytes.Bytes{+dn, db} = input
479	  Bytes.Bytes{+sn, sb} = sig
480	  do IO<Result<&1, &1, Err, Bool>>:
481	    r : Result<&1, &1, U32 & String, Bool> <- Crypto.rsa.verify.jwk.words("SHA256", nn, nb, en, eb, dn, db, sn, sb)
482	    return crypto.ok(r)
483	
484	def ec.pem(p: Bytes.Bytes, input: Bytes.Bytes, sig: Bytes.Bytes) -> IO(Result<&1, &1, Err, Bool>):
485	  Bytes.Bytes{+pn, pb} = p
486	  Bytes.Bytes{+dn, db} = input
487	  Bytes.Bytes{+sn, sb} = sig
488	  do IO<Result<&1, &1, Err, Bool>>:
489	    r : Result<&1, &1, U32 & String, Bool> <- Crypto.ecdsa.verify.words("SHA256", pn, pb, dn, db, sn, sb)
490	    return crypto.ok(r)
491	
492	def ec.jwk(x: Bytes.Bytes, y: Bytes.Bytes, input: Bytes.Bytes, sig: Bytes.Bytes) -> IO(Result<&1, &1, Err, Bool>):
493	  Bytes.Bytes{+xn, xb} = x
494	  Bytes.Bytes{+yn, yb} = y
495	  Bytes.Bytes{+dn, db} = input
496	  Bytes.Bytes{+sn, sb} = sig
497	  do IO<Result<&1, &1, Err, Bool>>:
498	    r : Result<&1, &1, U32 & String, Bool> <- Crypto.ecdsa.verify.jwk.words("SHA256", xn, xb, yn, yb, dn, db, sn, sb)
499	    return crypto.ok(r)
500	
501	# Does sig sign input under key for alg? A key of the wrong kind fails with KeyType before any crypto.
502	def sig.check(a: Alg, key: Key, input: Bytes.Bytes, sig: Bytes.Bytes) -> IO(Result<&1, &1, Err, Bool>):
503	  match a key:
504	    case HS256{} Hmac{k}:
505	      mac.check("SHA256", 32, k, input, sig)
506	    case HS384{} Hmac{k}:
507	      mac.check("SHA384", 48, k, input, sig)
508	    case HS512{} Hmac{k}:
509	      mac.check("SHA512", 64, k, input, sig)
510	    case RS256{} Pem{p}:
511	      rsa.pem(p, input, sig)
512	    case RS256{} Rsa{n, e}:
513	      rsa.jwk(n, e, input, sig)
514	    case ES256{} Pem{p}:
515	      ec.pem(p, input, sig)
516	    case ES256{} Ec{x, y}:
517	      ec.jwk(x, y, input, sig)
518	    case _ _:
519	      IO.pure(Result<&1, &1, Err, Bool>, Fail{KeyType{}})
520	
521	def rsa.sign(p: Bytes.Bytes, input: Bytes.Bytes) -> IO(Result<&1, &1, Err, Bytes.Bytes>):
522	  Bytes.Bytes{+pn, pb} = p
523	  Bytes.Bytes{+dn, db} = input
524	  do IO<Result<&1, &1, Err, Bytes.Bytes>>:
525	    r : Result<&1, &1, U32 & String, U32 & Array<U32>> <- Crypto.rsa.sign.words("SHA256", pn, pb, dn, db)
526	    return crypto.bytes(r)
527	
528	def ec.sign(p: Bytes.Bytes, input: Bytes.Bytes) -> IO(Result<&1, &1, Err, Bytes.Bytes>):
529	  Bytes.Bytes{+pn, pb} = p
530	  Bytes.Bytes{+dn, db} = input
531	  do IO<Result<&1, &1, Err, Bytes.Bytes>>:
532	    r : Result<&1, &1, U32 & String, U32 & Array<U32>> <- Crypto.ecdsa.sign.words("SHA256", pn, pb, dn, db)
533	    return crypto.bytes(r)
534	
535	# The signature of input under key for alg. RS256 and ES256 sign with a PEM private key.
536	def sig.make(a: Alg, key: Key, input: Bytes.Bytes) -> IO(Result<&1, &1, Err, Bytes.Bytes>):
537	  match a key:
538	    case HS256{} Hmac{k}:
539	      mac("SHA256", 32, k, input)
540	    case HS384{} Hmac{k}:
541	      mac("SHA384", 48, k, input)
542	    case HS512{} Hmac{k}:
543	      mac("SHA512", 64, k, input)
544	    case RS256{} Pem{p}:
545	      rsa.sign(p, input)
546	    case ES256{} Pem{p}:
547	      ec.sign(p, input)
548	    case _ _:
549	      IO.pure(Result<&1, &1, Err, Bytes.Bytes>, Fail{KeyType{}})
550	
551	# ---- sign and verify
552	
553	def header.kid(m: Maybe<&2, String>) -> List<&1, Bytes.Bytes & Json.Val>:
554	  match m:
555	    case None{}:
556	      Nil{}
557	    case Some{k}:
558	      [(Json.utf8("kid"), Json.Str{Json.utf8(k)})]
559	
560	# {"alg":..,"typ":"JWT"}, then "kid" when given.
561	def header(a: Alg, kid: Maybe<&2, String>) -> Json.Val:
562	  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)}}}
563	
564	# header.body in base64url, body being the compact JSON claims: the text the signature covers.
565	def signing.input(a: Alg, kid: Maybe<&2, String>, body: Bytes.Bytes) -> String:
566	  b64u(Json.encode.bytes(header(a, kid))) ++ "." ++ b64u(body)
567	
568	def sign.done(+input: String, s: Result<&1, &1, Err, Bytes.Bytes>) -> Result<&1, &1, Err, String>:
569	  match s:
570	    case Fail{e}:
571	      Fail{e}
572	    case Done{b}:
573	      Done{input ++ "." ++ b64u(b)}
574	
575	# verify accepts only an object with no repeated names, so sign makes no other kind.
576	def sign.obj(m: Maybe<&1, Json.Val>) -> Bool:
577	  match m:
578	    case Some{Json.Obj{kvs}}:
579	      True{}
580	    case _:
581	      False{}
582	
583	def sign.if(ok: Bool, +a: Alg, key: Key, kid: Maybe<&2, String>, body: Bytes.Bytes) -> IO(Result<&1, &1, Err, String>):
584	  match ok:
585	    case False{}:
586	      IO.pure(Result<&1, &1, Err, String>, Fail{BadClaim{}})
587	    case True{}:
588	      +input = signing.input(a, kid, body)
589	      do IO<Result<&1, &1, Err, String>>:
590	        s : Result<&1, &1, Err, Bytes.Bytes> <- sig.make(a, key, Bytes.from_string(input))
591	        return sign.done(input, s)
592	
593	def sign.body(+a: Alg, key: Key, kid: Maybe<&2, String>, r: Bytes.Bytes & Bytes.Bytes) -> IO(Result<&1, &1, Err, String>):
594	  (body, copy) = r
595	  sign.if(sign.obj(Json.unique.parsed(Json.parse.bytes(copy))), a, key, kid, body)
596	
597	# A compact token of claims signed with key for a; kid names the key in the header. Claims that are not
598	# an object, or repeat a name, fail with BadClaim.
599	def sign(+a: Alg, key: Key, kid: Maybe<&2, String>, claims: Json.Val) -> IO(Result<&1, &1, Err, String>):
600	  sign.body(a, key, kid, Bytes.slice(Json.encode.bytes(claims), 0, 4294967295))
601	
602	def claims.done(r: Result<&1, &1, Err, Unit>, v: Json.Val) -> Result<&1, &1, Err, Json.Val>:
603	  match r:
604	    case Fail{e}:
605	      Fail{e}
606	    case Done{u}:
607	      Done{v}
608	
609	def check.sig(ok: Bool, +p: Policy, +now: U32, +f: List<&2, Field>, v: Json.Val) -> Result<&1, &1, Err, Json.Val>:
610	  match ok:
611	    case False{}:
612	      Fail{BadSig{}}
613	    case True{}:
614	      claims.done(claims.check(p, now, f), v)
615	
616	def check.done(s: Result<&1, &1, Err, Bool>, +p: Policy, +now: U32, +f: List<&2, Field>, v: Json.Val) ->
617	    Result<&1, &1, Err, Json.Val>:
618	  match s:
619	    case Fail{e}:
620	      Fail{e}
621	    case Done{ok}:
622	      check.sig(ok, p, now, f, v)
623	
624	def check.pinned(ok: Result<&1, &1, Err, Unit>, +p: Policy, key: Key, +now: U32, +f: List<&2, Field>, v: Json.Val,
625	    input: Bytes.Bytes, sig: Bytes.Bytes) -> IO(Result<&1, &1, Err, Json.Val>):
626	  match ok:
627	    case Fail{e}:
628	      IO.pure(Result<&1, &1, Err, Json.Val>, Fail{e})
629	    case Done{u}:
630	      do IO<Result<&1, &1, Err, Json.Val>>:
631	        s : Result<&1, &1, Err, Bool> <- sig.check(policy.alg(p), key, input, sig)
632	        return check.done(s, p, now, f, v)
633	
634	# The pinned alg, then the signature, then the claims.
635	def check(+p: Policy, key: Key, +now: U32, parts: Parts) -> IO(Result<&1, &1, Err, Json.Val>):
636	  Parts{+h, +f, v, input, sig} = parts
637	  check.pinned(head.check(policy.alg(p), h), p, key, now, f, v, input, sig)
638	
639	def verify.parsed(+p: Policy, key: Key, +now: U32, r: Result<&1, &1, Err, Parts>) -> IO(Result<&1, &1, Err, Json.Val>):
640	  match r:
641	    case Fail{e}:
642	      IO.pure(Result<&1, &1, Err, Json.Val>, Fail{e})
643	    case Done{parts}:
644	      check(p, key, now, parts)
645	
646	# The claims of token when it is signed by key under p's alg and its claims hold at unix time now.
647	def verify(+p: Policy, key: Key, token: String, +now: U32) -> IO(Result<&1, &1, Err, Json.Val>):
648	  verify.parsed(p, key, now, parse(token))
649	
650	# ---- JWKS (RFC 7517)
651	
652	# A usable public key from a set: its kid, RSA or EC P-256, its alg ("" when the set gives none), and its
653	# two base64url parts (n and e, or x and y).
654	type Jwk is Data:
655	  Jwk{kid: String, rsa: Bool, alg: String, a: String, b: String}
656	
657	def jwk.two(+rsa: Bool, +kid: String, +alg: String, a: Maybe<&2, String>, b: Maybe<&2, String>) -> Maybe<&2, Jwk>:
658	  match a b:
659	    case Some{x} Some{y}:
660	      Some{Jwk{kid, rsa, alg, x, y}}
661	    case _ _:
662	      None{}
663	
664	# An alg member that is not a string can match no pinned alg.
665	def jwk.alg(m: Maybe<&2, Lit>) -> String:
666	  match m:
667	    case None{}:
668	      ""
669	    case Some{LStr{s}}:
670	      s
671	    case Some{_}:
672	      "?"
673	
674	def jwk.use(m: Maybe<&2, Lit>) -> Maybe<&2, Unit>:
675	  match m:
676	    case None{}:
677	      Some{Unit{}}
678	    case Some{LStr{s}}:
679	      Bool.pick(Maybe<&2, Unit>, String.eq(s, "sig"), Some{Unit{}}, None{})
680	    case Some{_}:
681	      None{}
682	
683	def jwk.kty(+kty: String, +kid: String, +f: List<&2, Field>) -> Maybe<&2, Jwk>:
684	  +alg = jwk.alg(field(f, "alg"))
685	  +ec = Bool.and(String.eq(kty, "EC"), String.eq(Maybe.default(&2, String, str(field(f, "crv")), ""), "P-256"))
686	  Bool.pick(Maybe<&2, Jwk>, String.eq(kty, "RSA"), jwk.two(True{}, kid, alg, str(field(f, "n")), str(field(f, "e"))),
687	    Bool.pick(Maybe<&2, Jwk>, ec, jwk.two(False{}, kid, alg, str(field(f, "x")), str(field(f, "y"))), None{}))
688	
689	def jwk.fields(+f: List<&2, Field>) -> Maybe<&2, Jwk>:
690	  do Maybe<&2, Jwk>:
691	    kty : String <- str(field(f, "kty"))
692	    kid : String <- str(field(f, "kid"))
693	    s : Unit <- jwk.use(field(f, "use"))
694	    jwk.kty(kty, kid, f)
695	
696	def jwk.obj(m: Maybe<&1, Json.Val>) -> Maybe<&2, Jwk>:
697	  match m:
698	    case Some{Json.Obj{kvs}}:
699	      jwk.fields(fields(kvs, Nil{}))
700	    case _:
701	      None{}
702	
703	# A key whose members repeat a name, at any depth, is skipped.
704	def jwk.of(v: Json.Val) -> Maybe<&2, Jwk>:
705	  jwk.obj(Json.unique.parsed(Some{v}))
706	
707	def jwk.push(m: Maybe<&2, Jwk>, acc: List<&2, Jwk>) -> List<&2, Jwk>:
708	  match m:
709	    case None{}:
710	      acc
711	    case Some{k}:
712	      Con{k, acc}
713	
714	def jwks.go(xs: List<&1, Json.Val>, acc: List<&2, Jwk>) -> List<&2, Jwk>:
715	  match xs:
716	    case Nil{}:
717	      List.reverse(&2, Jwk, acc)
718	    case x <> t:
719	      jwks.go(t, jwk.push(jwk.of(x), acc))
720	
721	def jwks.arr(m: Maybe<&1, Json.Val>) -> Maybe<&2, List<&2, Jwk>>:
722	  match m:
723	    case Some{Json.Arr{xs}}:
724	      Some{jwks.go(xs, Nil{})}
725	    case _:
726	      None{}
727	
728	def jwks.doc(m: Maybe<&1, Json.Val>) -> Maybe<&2, List<&2, Jwk>>:
729	  match m:
730	    case Some{v}:
731	      jwks.arr(Json.get(v, "keys"))
732	    case None{}:
733	      None{}
734	
735	# The signing keys of a JWK Set document; members it cannot use (enc keys, other curves, oct) are skipped.
736	# None when the document is not {"keys": [...]}.
737	def jwks.parse(b: Bytes.Bytes) -> Maybe<&2, List<&2, Jwk>>:
738	  jwks.doc(Json.parse.bytes(b))
739	
740	def fam(a: Alg) -> U32:
741	  match a:
742	    case RS256{}:
743	      1
744	    case ES256{}:
745	      2
746	    case _:
747	      0
748	
749	def jwk.fits(k: Jwk, +kid: String, +a: Alg) -> Bool:
750	  Jwk{k2, +rsa, +ka, x, y} = k
751	  Bool.and(Bool.and(String.eq(k2, kid), U32.is_eq(fam(a), Bool.pick(U32, rsa, 1, 2))),
752	    Bool.or(String.eq(ka, ""), String.eq(ka, alg.name(a))))
753	
754	# The first key named kid that can check alg a. RFC 7515 §4.1.4 leaves kid matching to exact comparison.
755	def jwk.pick(ks: List<&2, Jwk>, +kid: String, +a: Alg) -> Maybe<&2, Jwk>:
756	  match ks:
757	    case Nil{}:
758	      None{}
759	    case Con{+k, t}:
760	      Bool.pick(Maybe<&2, Jwk>, jwk.fits(k, kid, a), Some{k}, jwk.pick(t, kid, a))
761	
762	def jwk.key.of(rsa: Bool, a: Maybe<&1, Bytes.Bytes>, b: Maybe<&1, Bytes.Bytes>) -> Result<&1, &1, Err, Key>:
763	  match rsa a b:
764	    case True{} Some{n} Some{e}:
765	      Done{Rsa{n, e}}
766	    case False{} Some{x} Some{y}:
767	      Done{Ec{x, y}}
768	    case _ _ _:
769	      Fail{Malformed{}}
770	
771	# A set member as a verify key.
772	def jwk.key(k: Jwk) -> Result<&1, &1, Err, Key>:
773	  Jwk{kid, +rsa, alg, +a, +b} = k
774	  jwk.key.of(rsa, unb64u(a), unb64u(b))
775	
776	def jwk.found(m: Maybe<&2, Jwk>) -> Result<&1, &1, Err, Key>:
777	  match m:
778	    case None{}:
779	      Fail{NoKey{}}
780	    case Some{k}:
781	      jwk.key(k)
782	
783	# A cached key set from the caller's own trusted url; a token never picks the url (jku and x5u are ignored).
784	# live: fetched once; at: the unix time of the last good fetch; ttl: seconds it stays fresh;
785	# tried: the unix time of the last fetch, good or not.
786	type Jwks is Data:
787	  Jwks{url: String, ttl: U32, live: Bool, at: U32, tried: Maybe<&2, U32>, keys: List<&2, Jwk>}
788	
789	def jwks(url: String, +ttl: U32) -> Jwks:
790	  Jwks{url, ttl, False{}, 0, None{}, Nil{}}
791	
792	def jwks.keys(s: Jwks) -> List<&2, Jwk>:
793	  Jwks{u, t, l, a, tr, ks} = s
794	  ks
795	
796	def fetch.keys(m: Maybe<&2, List<&2, Jwk>>, c: Hairpin.Client, s: Jwks, +now: U32) -> Hairpin.Client & Jwks & Result<&1, &1, Err, Unit>:
797	  match m:
798	    case None{}:
799	      (c, s, Fail{Malformed{}})
800	    case Some{ks}:
801	      Jwks{url, ttl, live, at, tried, old} = s
802	      (c, Jwks{url, ttl, True{}, now, tried, ks}, Done{Unit{}})
803	
804	def fetch.body(ok: Bool, +status: U32, c: Hairpin.Client, s: Jwks, +now: U32, b: Bytes.Bytes) ->
805	    Hairpin.Client & Jwks & Result<&1, &1, Err, Unit>:
806	  match ok:
807	    case False{}:
808	      (c, s, Fail{Status{status}})
809	    case True{}:
810	      fetch.keys(jwks.parse(b), c, s, now)
811	
812	def fetch.res(c: Hairpin.Client, s: Jwks, +now: U32, r: Result<&1, &1, Hairpin.Err, Http.Res>) ->
813	    Hairpin.Client & Jwks & Result<&1, &1, Err, Unit>:
814	  match r:
815	    case Fail{e}:
816	      (c, s, Fail{Net{e}})
817	    case Done{Http.Res{+status, h, b}}:
818	      fetch.body(U32.is_eq(status, 200), status, c, s, now, b)
819	
820	def fetch.done(s: Jwks, +now: U32, x: Hairpin.Client & Result<&1, &1, Hairpin.Err, Http.Res>) ->
821	    Hairpin.Client & Jwks & Result<&1, &1, Err, Unit>:
822	  (c, r) = x
823	  fetch.res(c, s, now, r)
824	
825	# GET the set now. On any failure the client and the old keys come back, with only tried moved to now.
826	def fetch(c: Hairpin.Client, s: Jwks, +now: U32) -> IO(Hairpin.Client & Jwks & Result<&1, &1, Err, Unit>):
827	  Jwks{+url, ttl, live, at, old, ks} = s
828	  do IO<Hairpin.Client & Jwks & Result<&1, &1, Err, Unit>>:
829	    x : Hairpin.Client & Result<&1, &1, Hairpin.Err, Http.Res> <- Hairpin.get(c, url)
830	    return fetch.done(Jwks{url, ttl, live, at, Some{now}, ks}, now, x)
831	
832	def key.after.r(r: Result<&1, &1, Err, Unit>, c: Hairpin.Client, +s: Jwks, +kid: String, +a: Alg) ->
833	    Hairpin.Client & Jwks & Result<&1, &1, Err, Key>:
834	  match r:
835	    case Fail{e}:
836	      (c, s, Fail{e})
837	    case Done{u}:
838	      (c, s, jwk.found(jwk.pick(jwks.keys(s), kid, a)))
839	
840	def key.after(+kid: String, +a: Alg, x: Hairpin.Client & Jwks & Result<&1, &1, Err, Unit>) ->
841	    Hairpin.Client & Jwks & Result<&1, &1, Err, Key>:
842	  (c, s, r) = x
843	  key.after.r(r, c, s, kid, a)
844	
845	def key.refetch(go: Bool, c: Hairpin.Client, s: Jwks, +kid: String, +a: Alg, +now: U32) ->
846	    IO(Hairpin.Client & Jwks & Result<&1, &1, Err, Key>):
847	  match go:
848	    case False{}:
849	      IO.pure(Hairpin.Client & Jwks & Result<&1, &1, Err, Key>, (c, s, Fail{NoKey{}}))
850	    case True{}:
851	      do IO<Hairpin.Client & Jwks & Result<&1, &1, Err, Key>>:
852	        x : Hairpin.Client & Jwks & Result<&1, &1, Err, Unit> <- fetch(c, s, now)
853	        return key.after(kid, a, x)
854	
855	def key.go(cached: Bool, +go: Bool, c: Hairpin.Client, s: Jwks, found: Maybe<&2, Jwk>, +kid: String, +a: Alg, +now: U32) ->
856	    IO(Hairpin.Client & Jwks & Result<&1, &1, Err, Key>):
857	  match cached:
858	    case True{}:
859	      IO.pure(Hairpin.Client & Jwks & Result<&1, &1, Err, Key>, (c, s, jwk.found(found)))
860	    case False{}:
861	      key.refetch(go, c, s, kid, a, now)
862	
863	def since(+now: U32, m: Maybe<&2, U32>) -> U32:
864	  match m:
865	    case None{}:
866	      4294967295
867	    case Some{+t}:
868	      Bool.pick(U32, U32.is_le(t, now), (now - t : U32), 0)
869	
870	# The verify key named kid for alg a. A known key stays usable through the 60 s fetch cooldown even
871	# when ttl is shorter. After that, refresh a stale set or an unknown kid at most once a minute.
872	# ponytail: fixed 60 s cooldown; make it a Jwks field if an issuer rotates faster.
873	def key(c: Hairpin.Client, s: Jwks, +kid: String, +a: Alg, +now: U32) -> IO(Hairpin.Client & Jwks & Result<&1, &1, Err, Key>):
874	  Jwks{+url, +ttl, +live, +at, +tried, +ks} = s
875	  +found = jwk.pick(ks, kid, a)
876	  +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))))
877	  +cached = Bool.and(fresh, Maybe.is_some(&2, Jwk, found))
878	  key.go(cached, U32.is_le(60, since(now, tried)), c, Jwks{url, ttl, live, at, tried, ks}, found, kid, a, now)
879	
880	def jwks.run(r: Result<&1, &1, Err, Key>, c: Hairpin.Client, s: Jwks, +p: Policy, +now: U32, parts: Parts) ->
881	    IO(Hairpin.Client & Jwks & Result<&1, &1, Err, Json.Val>):
882	  match r:
883	    case Fail{e}:
884	      IO.pure(Hairpin.Client & Jwks & Result<&1, &1, Err, Json.Val>, (c, s, Fail{e}))
885	    case Done{k}:
886	      do IO<Hairpin.Client & Jwks & Result<&1, &1, Err, Json.Val>>:
887	        v : Result<&1, &1, Err, Json.Val> <- check(p, k, now, parts)
888	        return (c, s, v)
889	
890	def jwks.keyed(+p: Policy, +now: U32, parts: Parts, x: Hairpin.Client & Jwks & Result<&1, &1, Err, Key>) ->
891	    IO(Hairpin.Client & Jwks & Result<&1, &1, Err, Json.Val>):
892	  (c, s, r) = x
893	  jwks.run(r, c, s, p, now, parts)
894	
895	def jwks.kid(k: Maybe<&2, String>, +p: Policy, c: Hairpin.Client, s: Jwks, +now: U32, parts: Parts) ->
896	    IO(Hairpin.Client & Jwks & Result<&1, &1, Err, Json.Val>):
897	  match k:
898	    case None{}:
899	      IO.pure(Hairpin.Client & Jwks & Result<&1, &1, Err, Json.Val>, (c, s, Fail{NoKey{}}))
900	    case Some{+kid}:
901	      do IO<Hairpin.Client & Jwks & Result<&1, &1, Err, Json.Val>>:
902	        x : Hairpin.Client & Jwks & Result<&1, &1, Err, Key> <- key(c, s, kid, policy.alg(p), now)
903	        jwks.keyed(p, now, parts, x)
904	
905	def jwks.pinned(ok: Result<&1, &1, Err, Unit>, +p: Policy, c: Hairpin.Client, s: Jwks, +now: U32, +h: List<&2, Field>,
906	    parts: Parts) -> IO(Hairpin.Client & Jwks & Result<&1, &1, Err, Json.Val>):
907	  match ok:
908	    case Fail{e}:
909	      IO.pure(Hairpin.Client & Jwks & Result<&1, &1, Err, Json.Val>, (c, s, Fail{e}))
910	    case Done{u}:
911	      jwks.kid(str(field(h, "kid")), p, c, s, now, parts)
912	
913	def jwks.parsed(+p: Policy, c: Hairpin.Client, s: Jwks, +now: U32, r: Result<&1, &1, Err, Parts>) ->
914	    IO(Hairpin.Client & Jwks & Result<&1, &1, Err, Json.Val>):
915	  match r:
916	    case Fail{e}:
917	      IO.pure(Hairpin.Client & Jwks & Result<&1, &1, Err, Json.Val>, (c, s, Fail{e}))
918	    case Done{Parts{+h, f, v, input, sig}}:
919	      jwks.pinned(head.check(policy.alg(p), h), p, c, s, now, h, Parts{h, f, v, input, sig})
920	
921	# verify with the key the token's kid names in the set. The alg is pinned before any fetch.
922	# The client and the set (refreshed or not) always come back.
923	def verify.jwks(+p: Policy, c: Hairpin.Client, s: Jwks, token: String, +now: U32) ->
924	    IO(Hairpin.Client & Jwks & Result<&1, &1, Err, Json.Val>):
925	  jwks.parsed(p, c, s, now, parse(token))