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