1	# DNS codec and host lookup. Source: https://github.com/paymog/bend-kit/tree/main/dns
2	import Base
3	import bend-kit-wire@0.4.6.2/wire.bend as Wire
4	import bend-kit-bytes@0.3.2.0/bytes.bend as Bytes
5	
6	# query, answer, and resolve.pure are pure; PROOF.bend covers them, not effs/.
7	# resolve.all uses the OS resolver (IPv4 and IPv6); resolve keeps the first address.
8	#   import bend-kit-dns@0.6.0.0/dns.bend as Dns
9	
10	# Query
11	# -----
12	
13	def label.ok(+l: String) -> Bool:
14	  +n = String.length(l)
15	  Bool.and(Nat.is_lt(0n, n), Nat.is_le(n, 63n))
16	
17	def label.ascii(s: String) -> Bool:
18	  match s:
19	    case SNil{}:
20	      True{}
21	    case SCon{Chr{c}, t}:
22	      Bool.and(U32.is_lt(c, 128), label.ascii(t))
23	
24	def labels.ok(xs: List<&2, String>) -> Bool:
25	  match xs:
26	    case Nil{}:
27	      True{}
28	    case Con{+l, t}:
29	      Bool.and(Bool.and(label.ok(l), label.ascii(l)), labels.ok(t))
30	
31	# QNAME's length without its final zero octet.
32	def labels.len(xs: List<&2, String>, +n: U32) -> U32:
33	  match xs:
34	    case Nil{}:
35	      n
36	    case Con{+l, t}:
37	      labels.len(t, (n + 1 + U32.from_nat(String.length(l)) : U32))
38	
39	# The query buffer is allocated to its exact size before writing.
40	def written(r: Bytes.Cursor & Bool) -> Bytes.Cursor:
41	  (c, ok) = r
42	  c
43	
44	def label.put(s: String, c: Bytes.Cursor) -> Bytes.Cursor:
45	  match s:
46	    case SNil{}:
47	      c
48	    case SCon{Chr{v}, t}:
49	      label.put(t, written(Bytes.Cursor.put.u8(c, v)))
50	
51	def labels.put(xs: List<&2, String>, c: Bytes.Cursor) -> Bytes.Cursor:
52	  match xs:
53	    case Nil{}:
54	      written(Bytes.Cursor.put.u8(c, 0))
55	    case Con{+l, t}:
56	      labels.put(t, label.put(l, written(Bytes.Cursor.put.u8(c, U32.from_nat(String.length(l))))))
57	
58	def query.done(r: Bytes.Bytes & U32) -> Maybe<&1, Bytes.Bytes>:
59	  (b, pos) = r
60	  Some{b}
61	
62	def query.if(+id: U32, +xs: List<&2, String>, ok: Bool) -> Maybe<&1, Bytes.Bytes>:
63	  match ok:
64	    case False{}:
65	      None{}
66	    case True{}:
67	      # header: id, RD, QDCOUNT 1; question: QNAME, QTYPE A, QCLASS IN.
68	      c = Bytes.Cursor.new(Bytes.new((labels.len(xs, 0) + 17 : U32)))
69	      c = written(Bytes.Cursor.put.u16be(c, id))
70	      c = written(Bytes.Cursor.put.u16be(c, 256))
71	      c = written(Bytes.Cursor.put.u16be(c, 1))
72	      c = written(Bytes.Cursor.skip(c, 6))
73	      c = labels.put(xs, c)
74	      c = written(Bytes.Cursor.put.u16be(c, 1))
75	      c = written(Bytes.Cursor.put.u16be(c, 1))
76	      query.done(Bytes.Cursor.finish(c))
77	
78	# §2.3.4: a name is at most 255 octets in wire form, its final zero octet included.
79	def query.labels(+id: U32, +xs: List<&2, String>) -> Maybe<&1, Bytes.Bytes>:
80	  query.if(id, xs, Bool.and(labels.ok(xs), U32.is_le(labels.len(xs, 0), 254)))
81	
82	def strip_dot.if(+s: String, dot: Bool) -> String:
83	  match dot:
84	    case True{}:
85	      String.reverse(String.drop(String.reverse(s), 1n))
86	    case False{}:
87	      s
88	
89	def strip_dot(+s: String) -> String:
90	  strip_dot.if(s, String.ends_with(s, "."))
91	
92	# RFC 1035 §4.1: a standard query for the A record of name.
93	def query(id: U32, name: String) -> Maybe<&1, Bytes.Bytes>:
94	  query.labels(id, String.split(strip_dot(name), '.'))
95	
96	# Answer
97	# ------
98	
99	# One step through a name: continue at the next label or stop after the name.
100	type Step is Data:
101	  Go{}
102	  Stop{ok: Bool}
103	
104	def name.advance(stop: Bool, r: Bytes.Cursor & Bool) -> Bytes.Cursor & Step:
105	  (c, ok) = r
106	  match ok:
107	    case False{}:
108	      (c, Stop{False{}})
109	    case True{}:
110	      (c, Bool.pick(Step, stop, Stop{True{}}, Go{}))
111	
112	# §4.1.4: zero terminates, 192..255 starts a pointer, 64..191 is reserved.
113	def name.label(ok: Bool, c: Bytes.Cursor, l: U32) -> Bytes.Cursor & Step:
114	  match ok:
115	    case False{}:
116	      (c, Stop{False{}})
117	    case True{}:
118	      name.advance(False{}, Bytes.Cursor.skip(c, l))
119	
120	def name.pointer(pointer: Bool, +l: U32, c: Bytes.Cursor) -> Bytes.Cursor & Step:
121	  match pointer:
122	    case True{}:
123	      name.advance(True{}, Bytes.Cursor.skip(c, 1))
124	    case False{}:
125	      name.label(U32.is_lt(l, 64), c, l)
126	
127	def name.step.of(+l: U32, c: Bytes.Cursor) -> Bytes.Cursor & Step:
128	  match l:
129	    case 0:
130	      (c, Stop{True{}})
131	    case _:
132	      name.pointer(U32.is_le(192, l), l, c)
133	
134	def name.step(r: Bytes.Cursor & Maybe<&2, U32>) -> Bytes.Cursor & Step:
135	  (c, m) = r
136	  match m:
137	    case None{}:
138	      (c, Stop{False{}})
139	    case Some{l}:
140	      name.step.of(l, c)
141	
142	def name.walk(fuel: Nat, r: Bytes.Cursor & Step) -> Bytes.Cursor & Bool:
143	  match fuel:
144	    case 0n:
145	      (c, s) = r
146	      (c, False{})
147	    case 1n+f:
148	      (c, s) = r
149	      match s:
150	        case Stop{ok}:
151	          (c, ok)
152	        case Go{}:
153	          name.walk(f, name.step(Bytes.Cursor.u8(c)))
154	
155	# §2.3.4: a name is at most 255 octets, so retain the 128-step limit.
156	def name.skip(c: Bytes.Cursor) -> Bytes.Cursor & Bool:
157	  name.walk(128n, name.step(Bytes.Cursor.u8(c)))
158	
159	type RR is Data:
160	  RRBad{}
161	  RRA{ip: String}
162	  RRSkip{}
163	
164	def dotted(+ip: U32) -> String:
165	  U32.show(U32.shrn(ip, 24n)) ++ "." ++ U32.show(Bytes.b8(U32.shrn(ip, 16n))) ++ "." ++ U32.show(Bytes.b8(U32.shrn(ip, 8n))) ++ "." ++ U32.show(Bytes.b8(ip))
166	
167	def rr.a(limit: Bytes.CursorLimit, r: Bytes.Cursor & Maybe<&2, U32>) -> Bytes.Cursor & RR:
168	  (c, m) = r
169	  match m:
170	    case None{}:
171	      (Bytes.Cursor.leave(c, limit), RRBad{})
172	    case Some{ip}:
173	      (Bytes.Cursor.leave(c, limit), RRA{dotted(ip)})
174	
175	def rr.data.some(a: Bool, c: Bytes.Cursor, limit: Bytes.CursorLimit) -> Bytes.Cursor & RR:
176	  match a:
177	    case True{}:
178	      rr.a(limit, Bytes.Cursor.u32be(c))
179	    case False{}:
180	      (Bytes.Cursor.leave(c, limit), RRSkip{})
181	
182	# Bound RDATA in the original packed buffer, then resume after the entire region.
183	def rr.data(a: Bool, r: Bytes.Cursor & Maybe<&1, Bytes.CursorLimit>) -> Bytes.Cursor & RR:
184	  (c, m) = r
185	  match m:
186	    case None{}:
187	      (c, RRBad{})
188	    case Some{limit}:
189	      rr.data.some(a, c, limit)
190	
191	def rr.len(+ty: U32, +cl: U32, r: Bytes.Cursor & Maybe<&2, U32>) -> Bytes.Cursor & RR:
192	  (c, m) = r
193	  match m:
194	    case None{}:
195	      (c, RRBad{})
196	    case Some{+len}:
197	      rr.data(Bool.and(Bool.and(U32.is_eq(ty, 1), U32.is_eq(cl, 1)), U32.is_eq(len, 4)), Bytes.Cursor.region(c, len))
198	
199	def rr.ttl(+ty: U32, +cl: U32, r: Bytes.Cursor & Bool) -> Bytes.Cursor & RR:
200	  (c, ok) = r
201	  match ok:
202	    case False{}:
203	      (c, RRBad{})
204	    case True{}:
205	      rr.len(ty, cl, Bytes.Cursor.u16be(c))
206	
207	def rr.cl(+ty: U32, r: Bytes.Cursor & Maybe<&2, U32>) -> Bytes.Cursor & RR:
208	  (c, m) = r
209	  match m:
210	    case None{}:
211	      (c, RRBad{})
212	    case Some{cl}:
213	      rr.ttl(ty, cl, Bytes.Cursor.skip(c, 4))
214	
215	def rr.ty(r: Bytes.Cursor & Maybe<&2, U32>) -> Bytes.Cursor & RR:
216	  (c, m) = r
217	  match m:
218	    case None{}:
219	      (c, RRBad{})
220	    case Some{ty}:
221	      rr.cl(ty, Bytes.Cursor.u16be(c))
222	
223	def rr.name(r: Bytes.Cursor & Bool) -> Bytes.Cursor & RR:
224	  (c, ok) = r
225	  match ok:
226	    case False{}:
227	      (c, RRBad{})
228	    case True{}:
229	      rr.ty(Bytes.Cursor.u16be(c))
230	
231	# §4.1.3: NAME, TYPE, CLASS, TTL, RDLENGTH, RDATA.
232	def rr(c: Bytes.Cursor) -> Bytes.Cursor & RR:
233	  rr.name(name.skip(c))
234	
235	# fuel = records left. The first A record wins; CNAMEs before it are skipped.
236	def answers.scan(fuel: Nat, r: Bytes.Cursor & RR) -> Maybe<&2, String>:
237	  match fuel:
238	    case 0n:
239	      None{}
240	    case 1n+f:
241	      (c, x) = r
242	      match x:
243	        case RRBad{}:
244	          None{}
245	        case RRA{ip}:
246	          Some{ip}
247	        case RRSkip{}:
248	          answers.scan(f, rr(c))
249	
250	# QTYPE and QCLASS follow the name.
251	def question.end(r: Bytes.Cursor & Bool) -> Bytes.Cursor & Bool:
252	  (c, ok) = r
253	  match ok:
254	    case False{}:
255	      (c, False{})
256	    case True{}:
257	      Bytes.Cursor.skip(c, 4)
258	
259	def questions(fuel: Nat, r: Bytes.Cursor & Bool) -> Bytes.Cursor & Bool:
260	  match fuel:
261	    case 0n:
262	      r
263	    case 1n+f:
264	      (c, ok) = r
265	      match ok:
266	        case False{}:
267	          (c, False{})
268	        case True{}:
269	          questions(f, question.end(name.skip(c)))
270	
271	def body.go(+an: U32, r: Bytes.Cursor & Bool) -> Maybe<&2, String>:
272	  (c, ok) = r
273	  match ok:
274	    case False{}:
275	      None{}
276	    case True{}:
277	      answers.scan(U32.to_nat(an), rr(c))
278	
279	# The header ends with NSCOUNT and ARCOUNT; questions follow.
280	def body.an(+qd: U32, r: Bytes.Cursor & Maybe<&2, U32>) -> Maybe<&2, String>:
281	  (c, m) = r
282	  match m:
283	    case None{}:
284	      None{}
285	    case Some{an}:
286	      body.go(an, questions(U32.to_nat(qd), Bytes.Cursor.skip(c, 4)))
287	
288	def body.qd(r: Bytes.Cursor & Maybe<&2, U32>) -> Maybe<&2, String>:
289	  (c, m) = r
290	  match m:
291	    case None{}:
292	      None{}
293	    case Some{qd}:
294	      body.an(qd, Bytes.Cursor.u16be(c))
295	
296	# §4.1.1: QR set, opcode QUERY, not truncated, RCODE 0.
297	def flags.ok(+f: U32) -> Bool:
298	  Bool.and(Bool.and(U32.is_eq(U32.and(f, 32768), 32768), U32.is_eq(U32.and(f, 30720), 0)), Bool.and(U32.is_eq(U32.and(f, 512), 0), U32.is_eq(U32.and(f, 15), 0)))
299	
300	def head.flags.if(ok: Bool, c: Bytes.Cursor) -> Maybe<&2, String>:
301	  match ok:
302	    case False{}:
303	      None{}
304	    case True{}:
305	      body.qd(Bytes.Cursor.u16be(c))
306	
307	def head.flags(r: Bytes.Cursor & Maybe<&2, U32>) -> Maybe<&2, String>:
308	  (c, m) = r
309	  match m:
310	    case None{}:
311	      None{}
312	    case Some{f}:
313	      head.flags.if(flags.ok(f), c)
314	
315	def head.id.if(ok: Bool, c: Bytes.Cursor) -> Maybe<&2, String>:
316	  match ok:
317	    case False{}:
318	      None{}
319	    case True{}:
320	      head.flags(Bytes.Cursor.u16be(c))
321	
322	def head.id(+id: U32, r: Bytes.Cursor & Maybe<&2, U32>) -> Maybe<&2, String>:
323	  (c, m) = r
324	  match m:
325	    case None{}:
326	      None{}
327	    case Some{got}:
328	      head.id.if(U32.is_eq(id, got), c)
329	
330	# The IPv4 address the response gives for the query with this id.
331	def answer(id: U32, msg: Bytes.Bytes) -> Maybe<&2, String>:
332	  head.id(id, Bytes.Cursor.u16be(Bytes.Cursor.new(msg)))
333	
334	# resolv.conf
335	# -----------
336	
337	def nameservers.add(+line: String, rest: List<&2, String>, hit: Bool) -> List<&2, String>:
338	  match hit:
339	    case False{}:
340	      rest
341	    case True{}:
342	      Con{String.trim(String.drop(line, 10n)), rest}
343	
344	def nameservers.go(xs: List<&2, String>) -> List<&2, String>:
345	  match xs:
346	    case Nil{}:
347	      Nil{}
348	    case Con{+line, t}:
349	      nameservers.add(line, nameservers.go(t), String.starts_with(line, "nameserver"))
350	
351	# Every nameserver line, in file order.
352	def nameservers(conf: String) -> List<&2, String>:
353	  nameservers.go(String.lines(conf))
354	
355	def nameserver.first(xs: List<&2, String>) -> Maybe<&2, String>:
356	  match xs:
357	    case Nil{}:
358	      None{}
359	    case Con{n, t}:
360	      Some{n}
361	
362	# The first nameserver line of a resolv.conf.
363	def nameserver(conf: String) -> Maybe<&2, String>:
364	  nameserver.first(nameservers(conf))
365	
366	# Resolve
367	# -------
368	
369	def none() -> IO(Maybe<&2, String>):
370	  IO.pure(Maybe<&2, String>, None{})
371	
372	def list.append(xs: List<&2, String>, ys: List<&2, String>) -> List<&2, String>:
373	  match xs:
374	    case Nil{}:
375	      ys
376	    case Con{+h, t}:
377	      h <> list.append(t, ys)
378	
379	def list.one(+x: String) -> List<&2, String>:
380	  x <> Nil{}
381	
382	def list.any(+xs: List<&2, String>) -> Bool:
383	  match xs:
384	    case Nil{}:
385	      False{}
386	    case Con{+_, +_}:
387	      True{}
388	
389	def list.first(xs: List<&2, String>) -> Maybe<&2, String>:
390	  match xs:
391	    case Nil{}:
392	      None{}
393	    case Con{+h, t}:
394	      Some{h}
395	
396	def ipv4.go(s: String) -> Bool:
397	  match s:
398	    case SNil{}:
399	      True{}
400	    case SCon{Chr{+c}, t}:
401	      Bool.and(Bool.or(U32.is_eq(c, 46), Bool.and(U32.is_le(48, c), U32.is_le(c, 57))), ipv4.go(t))
402	
403	# Digits and dots; TCP.connect rejects anything else that is not an address.
404	def ipv4(+s: String) -> Bool:
405	  Bool.and(Bool.not(String.is_empty(s)), ipv4.go(s))
406	
407	def ipv6.ch(+c: U32) -> Bool:
408	  Bool.or(
409	    Bool.and(U32.is_le(48, c), U32.is_le(c, 57)),
410	    Bool.or(
411	      Bool.and(U32.is_le(97, c), U32.is_le(c, 102)),
412	      Bool.and(U32.is_le(65, c), U32.is_le(c, 70))))
413	
414	def ipv6.go(s: String) -> Bool:
415	  match s:
416	    case SNil{}:
417	      True{}
418	    case SCon{Chr{+c}, t}:
419	      Bool.and(Bool.or(U32.is_eq(c, 58), ipv6.ch(c)), ipv6.go(t))
420	
421	def ipv6.has(s: String) -> Bool:
422	  match s:
423	    case SNil{}:
424	      False{}
425	    case SCon{Chr{+c}, t}:
426	      Bool.or(U32.is_eq(c, 58), ipv6.has(t))
427	
428	# Bracket-free IPv6 text; connect validates the address.
429	def ipv6(+s: String) -> Bool:
430	  Bool.and(Bool.and(Bool.not(String.is_empty(s)), ipv6.has(s)), ipv6.go(s))
431	
432	def ip(+s: String) -> Bool:
433	  Bool.or(ipv4(s), ipv6(s))
434	
435	# One attempt's outcome: try again, or this answer (None: no address).
436	type Try is Data:
437	  Again{}
438	  Got{ip: Maybe<&2, String>}
439	
440	def try.pure(s: Socket, t: Try) -> IO(Socket & Try):
441	  IO.pure(Socket & Try, (s, t))
442	
443	# A datagram from anyone but the nameserver's port 53 is ignored (retried).
444	def try.from(s: Socket, +ns: String, id: U32, hpd: String & U32 & (U32 & Array<U32>)) -> IO(Socket & Try):
445	  (h, +p, d) = hpd
446	  (n, w) = d
447	  try.pure(s, Bool.pick(Try, Bool.and(String.eq(h, ns), U32.is_eq(p, 53)), Got{answer(id, Bytes.Bytes{n, w})}, Again{}))
448	
449	def try.back(ns: String, id: U32, m: Socket & Result<&1, &1, U32 & String, String & U32 & (U32 & Array<U32>)>) -> IO(Socket & Try):
450	  (s, r) = m
451	  match r:
452	    case Fail{e}:
453	      try.pure(s, Again{})
454	    case Done{hpd}:
455	      try.from(s, ns, id, hpd)
456	
457	# §4.2.1 and resolv.conf defaults: 5 s per attempt.
458	def try.sent(ns: String, id: U32, m: Socket & Result<&1, &1, U32 & String, Unit>) -> IO(Socket & Try):
459	  (s, r) = m
460	  match r:
461	    case Fail{e}:
462	      try.pure(s, Again{})
463	    case Done{u}:
464	      do IO<Socket & Try>:
465	        back : Socket & Result<&1, &1, U32 & String, String & U32 & (U32 & Array<U32>)> <- Wire.recv_from.words(s, 512, 5000)
466	        try.back(ns, id, back)
467	
468	# Bytes cannot be copied, so each attempt builds its own query. A name that query rejects ends the tries.
469	def try.send(s: Socket, +ns: String, id: U32, q: Maybe<&1, Bytes.Bytes>) -> IO(Socket & Try):
470	  match q:
471	    case None{}:
472	      try.pure(s, Got{None{}})
473	    case Some{Bytes.Bytes{n, w}}:
474	      do IO<Socket & Try>:
475	        sent : Socket & Result<&1, &1, U32 & String, Unit> <- Wire.send_to.words(s, ns, 53, n, w)
476	        try.sent(ns, id, sent)
477	
478	def try.once(s: Socket, +ns: String, +id: U32, name: String) -> IO(Socket & Try):
479	  try.send(s, ns, id, query(id, name))
480	
481	def try.close(s: Socket, r: Maybe<&2, String>) -> IO(Maybe<&2, String>):
482	  do IO<Maybe<&2, String>>:
483	    Socket.close(s)
484	    return r
485	
486	def tries.end(st: Socket & Try) -> IO(Maybe<&2, String>):
487	  (s, t) = st
488	  match t:
489	    case Got{ip}:
490	      try.close(s, ip)
491	    case Again{}:
492	      try.close(s, None{})
493	
494	# fuel: attempts left (resolv.conf's default is 2).
495	def tries(fuel: Nat, +ns: String, +id: U32, +name: String, st: Socket & Try) -> IO(Maybe<&2, String>):
496	  match fuel:
497	    case 0n:
498	      tries.end(st)
499	    case 1n+f:
500	      (s, t) = st
501	      match t:
502	        case Got{ip}:
503	          try.close(s, ip)
504	        case Again{}:
505	          do IO<Maybe<&2, String>>:
506	            next : Socket & Try <- try.once(s, ns, id, name)
507	            tries(f, ns, id, name, next)
508	
509	def resolve.sock(ns: String, id: U32, name: String, r: Result<&1, &1, U32 & String, Socket>) -> IO(Maybe<&2, String>):
510	  match r:
511	    case Fail{e}:
512	      none()
513	    case Done{s}:
514	      tries(2n, ns, id, name, (s, Again{}))
515	
516	# §7.3: a random id makes forged answers harder to land.
517	def resolve.id(name: String, ns: String, r: Result<&1, &1, U32 & String, U32>) -> IO(Maybe<&2, String>):
518	  match r:
519	    case Fail{e}:
520	      none()
521	    case Done{x}:
522	      do IO<Maybe<&2, String>>:
523	        u : Result<&1, &1, U32 & String, Socket> <- UDP.bind("0.0.0.0", 0)
524	        resolve.sock(ns, U32.and(x, 65535), name, u)
525	
526	def resolve.ns(name: String, ns: Maybe<&2, String>) -> IO(Maybe<&2, String>):
527	  match ns:
528	    case None{}:
529	      none()
530	    case Some{n}:
531	      do IO<Maybe<&2, String>>:
532	        r : Result<&1, &1, U32 & String, U32> <- IO.random_u32()
533	        resolve.id(name, n, r)
534	
535	# Ask one nameserver. Tests use this; resolve reads /etc/resolv.conf.
536	def resolve.at(+host: String, ns: String) -> IO(Maybe<&2, String>):
537	  resolve.ns(host, Some{ns})
538	
539	def conf.text(r: Result<&1, &1, U32 & String, String>) -> String:
540	  match r:
541	    case Fail{e}:
542	      ""
543	    case Done{s}:
544	      s
545	
546	# ponytail: 3 nameservers; a longer resolv.conf ignores the rest
547	def resolve.n3(+name: String, xs: List<&2, String>) -> IO(Maybe<&2, String>):
548	  match xs:
549	    case Nil{}:
550	      none()
551	    case Con{+ns, t}:
552	      resolve.at(name, ns)
553	
554	def resolve.n2b(+name: String, rest: List<&2, String>, ip: Maybe<&2, String>) -> IO(Maybe<&2, String>):
555	  match ip:
556	    case Some{s}:
557	      IO.pure(Maybe<&2, String>, Some{s})
558	    case None{}:
559	      resolve.n3(name, rest)
560	
561	def resolve.n2(+name: String, xs: List<&2, String>) -> IO(Maybe<&2, String>):
562	  match xs:
563	    case Nil{}:
564	      none()
565	    case Con{+ns, t}:
566	      do IO<Maybe<&2, String>>:
567	        ip : Maybe<&2, String> <- resolve.at(name, ns)
568	        resolve.n2b(name, t, ip)
569	
570	def resolve.n1b(+name: String, rest: List<&2, String>, ip: Maybe<&2, String>) -> IO(Maybe<&2, String>):
571	  match ip:
572	    case Some{s}:
573	      IO.pure(Maybe<&2, String>, Some{s})
574	    case None{}:
575	      resolve.n2(name, rest)
576	
577	def resolve.list(+name: String, xs: List<&2, String>) -> IO(Maybe<&2, String>):
578	  match xs:
579	    case Nil{}:
580	      none()
581	    case Con{+ns, t}:
582	      do IO<Maybe<&2, String>>:
583	        ip : Maybe<&2, String> <- resolve.at(name, ns)
584	        resolve.n1b(name, t, ip)
585	
586	def resolve.read(name: String, m: File & Result<&1, &1, U32 & String, String>) -> IO(Maybe<&2, String>):
587	  (f, r) = m
588	  do IO<Maybe<&2, String>>:
589	    File.close(f)
590	    resolve.list(name, nameservers(conf.text(r)))
591	
592	def resolve.conf(name: String, r: Result<&1, &1, U32 & String, File>) -> IO(Maybe<&2, String>):
593	  match r:
594	    case Fail{e}:
595	      none()
596	    case Done{f}:
597	      do IO<Maybe<&2, String>>:
598	        m : File & Result<&1, &1, U32 & String, String> <- File.read(f, 65536)
599	        resolve.read(name, m)
600	
601	def resolve.dns(name: String) -> IO(Maybe<&2, String>):
602	  do IO<Maybe<&2, String>>:
603	    f : Result<&1, &1, U32 & String, File> <- File.open("/etc/resolv.conf", "r")
604	    resolve.conf(name, f)
605	
606	
607	def hosts.on_line(+name: String, ns: List<&2, String>) -> Bool:
608	  match ns:
609	    case Nil{}:
610	      False{}
611	    case Con{+n, t}:
612	      Bool.or(String.eq(String.to_lower(n), name), hosts.on_line(name, t))
613	
614	def hosts.line.all(+name: String, xs: List<&2, String>) -> List<&2, String>:
615	  match xs:
616	    case Nil{}:
617	      Nil{}
618	    case Con{+addr, ns}:
619	      Bool.pick(List<&2, String>, Bool.and(ip(addr), hosts.on_line(name, ns)), list.one(addr), Nil{})
620	
621	def hosts.sp(+c: U32, tab: Bool) -> U32:
622	  match tab:
623	    case True{}:
624	      32
625	    case False{}:
626	      c
627	
628	def hosts.flat(s: String) -> String:
629	  match s:
630	    case SNil{}:
631	      ""
632	    case SCon{Chr{+c}, t}:
633	      SCon{Chr{hosts.sp(c, U32.is_eq(c, 9))}, hosts.flat(t)}
634	
635	def hosts.scan.all(xs: List<&2, String>, +name: String, acc: List<&2, String>) -> List<&2, String>:
636	  match xs:
637	    case Nil{}:
638	      acc
639	    case Con{+line, t}:
640	      hosts.scan.all(t, name,
641	        list.append(acc, hosts.line.all(name, String.split(hosts.flat(line), ' '))))
642	
643	# Every address for name in an /etc/hosts file. The name is already lowercase.
644	def hosts.all(+name: String, text: String) -> List<&2, String>:
645	  hosts.scan.all(String.lines(text), name, Nil{})
646	
647	# First address for name in an /etc/hosts file. The name is already lowercase.
648	def hosts(+name: String, text: String) -> Maybe<&2, String>:
649	  list.first(hosts.all(name, text))
650	
651	def lookup.split(+s: String) -> List<&2, String>:
652	  List.filter(~String, ~(n => Bool.not(String.is_empty(n))), String.split(s, Chr{0}))
653	
654	# OS resolver: every address, NUL-separated in getaddrinfo order.
655	def lookup.all(host: String) -> IO(Result<&1, &1, U32 & String, String>):
656	  import "./effs/dns.c"
657	  import "./effs/dns.js"
658	
659	# Literals and localhost without the OS (for laws and fast paths).
660	def resolve.literal.all(+host: String) -> List<&2, String>:
661	  Bool.pick(List<&2, String>, ip(host), list.one(host),
662	    Bool.pick(List<&2, String>, String.eq(host, "localhost"),
663	      ["::1", "127.0.0.1"], Nil{}))
664	
665	def resolve.literal(+host: String) -> Maybe<&2, String>:
666	  list.first(resolve.literal.all(host))
667	
668	def resolve.all.got(r: Result<&1, &1, U32 & String, String>) -> IO(List<&2, String>):
669	  match r:
670	    case Fail{e}:
671	      IO.pure(List<&2, String>, Nil{})
672	    case Done{s}:
673	      IO.pure(List<&2, String>, lookup.split(s))
674	
675	def resolve.all.os(+name: String) -> IO(List<&2, String>):
676	  do IO<List<&2, String>>:
677	    r : Result<&1, &1, U32 & String, String> <- lookup.all(name)
678	    resolve.all.got(r)
679	
680	def resolve.all.dns.one(m: Maybe<&2, String>) -> IO(List<&2, String>):
681	  match m:
682	    case Some{ip}:
683	      IO.pure(List<&2, String>, list.one(ip))
684	    case None{}:
685	      IO.pure(List<&2, String>, Nil{})
686	
687	# ponytail: UDP path still asks for A records only
688	def resolve.all.dns(+name: String) -> IO(List<&2, String>):
689	  do IO<List<&2, String>>:
690	    m : Maybe<&2, String> <- resolve.dns(name)
691	    resolve.all.dns.one(m)
692	
693	def resolve.all.from(+name: String, +xs: List<&2, String>) -> IO(List<&2, String>):
694	  match xs:
695	    case Nil{}:
696	      resolve.all.dns(name)
697	    case Con{+_, +t}:
698	      IO.pure(List<&2, String>, xs)
699	
700	def resolve.all.text(+name: String, r: Result<&1, &1, U32 & String, String>) -> IO(List<&2, String>):
701	  match r:
702	    case Fail{e}:
703	      resolve.all.dns(name)
704	    case Done{s}:
705	      resolve.all.from(name, hosts.all(name, s))
706	
707	def resolve.all.opened(+name: String, m: File & Result<&1, &1, U32 & String, String>) -> IO(List<&2, String>):
708	  (f, r) = m
709	  do IO<List<&2, String>>:
710	    File.close(f)
711	    resolve.all.text(name, r)
712	
713	def resolve.all.hosts(+name: String, r: Result<&1, &1, U32 & String, File>) -> IO(List<&2, String>):
714	  match r:
715	    case Fail{e}:
716	      resolve.all.dns(name)
717	    case Done{f}:
718	      do IO<List<&2, String>>:
719	        m : File & Result<&1, &1, U32 & String, String> <- File.read(f, 65536)
720	        resolve.all.opened(name, m)
721	
722	def resolve.all.pick(+host: String, +xs: List<&2, String>) -> IO(List<&2, String>):
723	  match xs:
724	    case Nil{}:
725	      resolve.all.os(String.to_lower(host))
726	    case Con{+_, +t}:
727	      IO.pure(List<&2, String>, xs)
728	
729	def resolve.all(+host: String) -> IO(List<&2, String>):
730	  resolve.all.pick(host, resolve.literal.all(host))
731	
732	def resolve.all.ask(+name: String) -> IO(List<&2, String>):
733	  do IO<List<&2, String>>:
734	    f : Result<&1, &1, U32 & String, File> <- File.open("/etc/hosts", "r")
735	    resolve.all.hosts(name, f)
736	
737	def resolve.all.pure.pick(+host: String, +xs: List<&2, String>) -> IO(List<&2, String>):
738	  match xs:
739	    case Nil{}:
740	      resolve.all.ask(String.to_lower(host))
741	    case Con{+_, +t}:
742	      IO.pure(List<&2, String>, xs)
743	
744	def resolve.all.pure(+host: String) -> IO(List<&2, String>):
745	  resolve.all.pure.pick(host, resolve.literal.all(host))
746	
747	def resolve.pure(+host: String) -> IO(Maybe<&2, String>):
748	  do IO<Maybe<&2, String>>:
749	    xs : List<&2, String> <- resolve.all.pure(host)
750	    return list.first(xs)
751	
752	# First address from resolve.all (getaddrinfo order when the OS resolves).
753	def resolve(+host: String) -> IO(Maybe<&2, String>):
754	  do IO<Maybe<&2, String>>:
755	    xs : List<&2, String> <- resolve.all(host)
756	    return list.first(xs)