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