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.3.0/wire.bend as Wire
4	import bend-kit-bytes@0.3.1.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.5.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	def label.put(s: String, b: Bytes.Bytes, +i: U32) -> Bytes.Bytes:
40	  match s:
41	    case SNil{}:
42	      b
43	    case SCon{Chr{c}, t}:
44	      label.put(t, Bytes.set(b, i, c), (i + 1 : U32))
45	
46	# Each label as its length octet, then its octets. The zero octet that ends QNAME is already there.
47	def labels.put(xs: List<&2, String>, b: Bytes.Bytes, +i: U32) -> Bytes.Bytes:
48	  match xs:
49	    case Nil{}:
50	      b
51	    case Con{+l, t}:
52	      +n = U32.from_nat(String.length(l))
53	      labels.put(t, label.put(l, Bytes.set(b, i, n), (i + 1 : U32)), (i + 1 + n : U32))
54	
55	def query.if(+id: U32, +xs: List<&2, String>, ok: Bool) -> Maybe<&1, Bytes.Bytes>:
56	  match ok:
57	    case False{}:
58	      None{}
59	    case True{}:
60	      # header: id, RD, QDCOUNT 1; question: QNAME, QTYPE A, QCLASS IN. Other fields stay zero.
61	      +n = (labels.len(xs, 0) + 17 : U32)
62	      Some{Bytes.set.u16be(Bytes.set.u16be(labels.put(xs, Bytes.set.u16be(Bytes.set.u16be(Bytes.set.u16be(Bytes.new(n), 0, id), 2, 256), 4, 1), 12), (n - 4 : U32), 1), (n - 2 : U32), 1)}
63	
64	def query.labels(+id: U32, +xs: List<&2, String>) -> Maybe<&1, Bytes.Bytes>:
65	  query.if(id, xs, labels.ok(xs))
66	
67	def strip_dot.if(+s: String, dot: Bool) -> String:
68	  match dot:
69	    case True{}:
70	      String.reverse(String.drop(String.reverse(s), 1n))
71	    case False{}:
72	      s
73	
74	def strip_dot(+s: String) -> String:
75	  strip_dot.if(s, String.ends_with(s, "."))
76	
77	# RFC 1035 §4.1: a standard query for the A record of name.
78	def query(id: U32, name: String) -> Maybe<&1, Bytes.Bytes>:
79	  query.labels(id, String.split(strip_dot(name), '.'))
80	
81	# Answer
82	# ------
83	
84	# One step through a name: go on at the next label, or stop with the offset past the name.
85	type Step is Data:
86	  Go{at: U32}
87	  Stop{end: Maybe<&2, U32>}
88	
89	# §4.1.4: l, the octet at i, is 0 at the end, 192..255 for a two-octet pointer, 64..191 reserved.
90	def name.step.of(+i: U32, +l: U32) -> Step:
91	  Bool.pick(Step, U32.is_eq(l, 0), Stop{Some{(i + 1 : U32)}}, Bool.pick(Step, U32.is_le(192, l), Stop{Some{(i + 2 : U32)}}, Bool.pick(Step, U32.is_le(64, l), Stop{None{}}, Go{(i + 1 + l : U32)})))
92	
93	def name.step(+i: U32, r: Bytes.Bytes & Maybe<&2, U32>) -> Bytes.Bytes & Step:
94	  (b, m) = r
95	  match m:
96	    case None{}:
97	      (b, Stop{None{}})
98	    case Some{l}:
99	      (b, name.step.of(i, l))
100	
101	def name.walk(fuel: Nat, r: Bytes.Bytes & Step) -> Bytes.Bytes & Maybe<&2, U32>:
102	  match fuel:
103	    case 0n:
104	      (b, s) = r
105	      (b, None{})
106	    case 1n+f:
107	      (b, s) = r
108	      match s:
109	        case Stop{end}:
110	          (b, end)
111	        case Go{+at}:
112	          name.walk(f, name.step(at, Bytes.get(b, at)))
113	
114	# The offset past the name at i. §2.3.4: a name is at most 255 octets, so 128 steps are enough.
115	def name.skip(b: Bytes.Bytes, +i: U32) -> Bytes.Bytes & Maybe<&2, U32>:
116	  name.walk(128n, name.step(i, Bytes.get(b, i)))
117	
118	type RR is Data:
119	  RRBad{}
120	  RRA{ip: String}
121	  RRSkip{at: U32}
122	
123	def dotted(+ip: U32) -> String:
124	  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))
125	
126	def rr.a(r: Bytes.Bytes & Maybe<&2, U32>) -> Bytes.Bytes & RR:
127	  (b, m) = r
128	  match m:
129	    case None{}:
130	      (b, RRBad{})
131	    case Some{ip}:
132	      (b, RRA{dotted(ip)})
133	
134	# RDATA at i holds len octets. A skipped record past the end fails at the next read.
135	def rr.data(a: Bool, b: Bytes.Bytes, +i: U32, +len: U32) -> Bytes.Bytes & RR:
136	  match a:
137	    case True{}:
138	      rr.a(Bytes.get.u32be(b, i))
139	    case False{}:
140	      (b, RRSkip{(i + len : U32)})
141	
142	def rr.len(+o: U32, +ty: U32, +cl: U32, r: Bytes.Bytes & Maybe<&2, U32>) -> Bytes.Bytes & RR:
143	  (b, m) = r
144	  match m:
145	    case None{}:
146	      (b, RRBad{})
147	    case Some{+len}:
148	      rr.data(Bool.and(Bool.and(U32.is_eq(ty, 1), U32.is_eq(cl, 1)), U32.is_eq(len, 4)), b, (o + 10 : U32), len)
149	
150	def rr.cl(+o: U32, +ty: U32, r: Bytes.Bytes & Maybe<&2, U32>) -> Bytes.Bytes & RR:
151	  (b, m) = r
152	  match m:
153	    case None{}:
154	      (b, RRBad{})
155	    case Some{cl}:
156	      rr.len(o, ty, cl, Bytes.get.u16be(b, (o + 8 : U32)))
157	
158	def rr.ty(+o: U32, r: Bytes.Bytes & Maybe<&2, U32>) -> Bytes.Bytes & RR:
159	  (b, m) = r
160	  match m:
161	    case None{}:
162	      (b, RRBad{})
163	    case Some{ty}:
164	      rr.cl(o, ty, Bytes.get.u16be(b, (o + 2 : U32)))
165	
166	def rr.name(r: Bytes.Bytes & Maybe<&2, U32>) -> Bytes.Bytes & RR:
167	  (b, m) = r
168	  match m:
169	    case None{}:
170	      (b, RRBad{})
171	    case Some{+o}:
172	      rr.ty(o, Bytes.get.u16be(b, o))
173	
174	# §4.1.3: NAME, TYPE, CLASS, TTL, RDLENGTH, RDATA.
175	def rr(b: Bytes.Bytes, +i: U32) -> Bytes.Bytes & RR:
176	  rr.name(name.skip(b, i))
177	
178	# fuel = records left. The first A record wins; CNAMEs before it are skipped.
179	def answers.scan(fuel: Nat, r: Bytes.Bytes & RR) -> Maybe<&2, String>:
180	  match fuel:
181	    case 0n:
182	      None{}
183	    case 1n+f:
184	      (b, x) = r
185	      match x:
186	        case RRBad{}:
187	          None{}
188	        case RRA{ip}:
189	          Some{ip}
190	        case RRSkip{+at}:
191	          answers.scan(f, rr(b, at))
192	
193	# QTYPE and QCLASS follow the name.
194	def question.end(r: Bytes.Bytes & Maybe<&2, U32>) -> Bytes.Bytes & Maybe<&2, U32>:
195	  (b, m) = r
196	  match m:
197	    case None{}:
198	      (b, None{})
199	    case Some{e}:
200	      (b, Some{(e + 4 : U32)})
201	
202	def questions(fuel: Nat, r: Bytes.Bytes & Maybe<&2, U32>) -> Bytes.Bytes & Maybe<&2, U32>:
203	  match fuel:
204	    case 0n:
205	      (b, m) = r
206	      (b, m)
207	    case 1n+f:
208	      (b, m) = r
209	      match m:
210	        case None{}:
211	          (b, None{})
212	        case Some{+at}:
213	          questions(f, question.end(name.skip(b, at)))
214	
215	def body.go(+an: U32, r: Bytes.Bytes & Maybe<&2, U32>) -> Maybe<&2, String>:
216	  (b, m) = r
217	  match m:
218	    case None{}:
219	      None{}
220	    case Some{+at}:
221	      answers.scan(U32.to_nat(an), rr(b, at))
222	
223	# The 12-octet header ends with NSCOUNT and ARCOUNT; the questions follow.
224	def body.an(+qd: U32, r: Bytes.Bytes & Maybe<&2, U32>) -> Maybe<&2, String>:
225	  (b, m) = r
226	  match m:
227	    case None{}:
228	      None{}
229	    case Some{an}:
230	      body.go(an, questions(U32.to_nat(qd), (b, Some{12})))
231	
232	def body.qd(r: Bytes.Bytes & Maybe<&2, U32>) -> Maybe<&2, String>:
233	  (b, m) = r
234	  match m:
235	    case None{}:
236	      None{}
237	    case Some{qd}:
238	      body.an(qd, Bytes.get.u16be(b, 6))
239	
240	# §4.1.1: QR set, opcode QUERY, not truncated, RCODE 0.
241	def flags.ok(+f: U32) -> Bool:
242	  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)))
243	
244	def head.flags.if(ok: Bool, b: Bytes.Bytes) -> Maybe<&2, String>:
245	  match ok:
246	    case False{}:
247	      None{}
248	    case True{}:
249	      body.qd(Bytes.get.u16be(b, 4))
250	
251	def head.flags(r: Bytes.Bytes & Maybe<&2, U32>) -> Maybe<&2, String>:
252	  (b, m) = r
253	  match m:
254	    case None{}:
255	      None{}
256	    case Some{f}:
257	      head.flags.if(flags.ok(f), b)
258	
259	def head.id.if(ok: Bool, b: Bytes.Bytes) -> Maybe<&2, String>:
260	  match ok:
261	    case False{}:
262	      None{}
263	    case True{}:
264	      head.flags(Bytes.get.u16be(b, 2))
265	
266	def head.id(+id: U32, r: Bytes.Bytes & Maybe<&2, U32>) -> Maybe<&2, String>:
267	  (b, m) = r
268	  match m:
269	    case None{}:
270	      None{}
271	    case Some{got}:
272	      head.id.if(U32.is_eq(id, got), b)
273	
274	# The IPv4 address the response gives for the query with this id.
275	def answer(id: U32, msg: Bytes.Bytes) -> Maybe<&2, String>:
276	  head.id(id, Bytes.get.u16be(msg, 0))
277	
278	# resolv.conf
279	# -----------
280	
281	def nameservers.add(+line: String, rest: List<&2, String>, hit: Bool) -> List<&2, String>:
282	  match hit:
283	    case False{}:
284	      rest
285	    case True{}:
286	      Con{String.trim(String.drop(line, 10n)), rest}
287	
288	def nameservers.go(xs: List<&2, String>) -> List<&2, String>:
289	  match xs:
290	    case Nil{}:
291	      Nil{}
292	    case Con{+line, t}:
293	      nameservers.add(line, nameservers.go(t), String.starts_with(line, "nameserver"))
294	
295	# Every nameserver line, in file order.
296	def nameservers(conf: String) -> List<&2, String>:
297	  nameservers.go(String.lines(conf))
298	
299	def nameserver.first(xs: List<&2, String>) -> Maybe<&2, String>:
300	  match xs:
301	    case Nil{}:
302	      None{}
303	    case Con{n, t}:
304	      Some{n}
305	
306	# The first nameserver line of a resolv.conf.
307	def nameserver(conf: String) -> Maybe<&2, String>:
308	  nameserver.first(nameservers(conf))
309	
310	# Resolve
311	# -------
312	
313	def none() -> IO(Maybe<&2, String>):
314	  IO.pure(Maybe<&2, String>, None{})
315	
316	def list.append(xs: List<&2, String>, ys: List<&2, String>) -> List<&2, String>:
317	  match xs:
318	    case Nil{}:
319	      ys
320	    case Con{+h, t}:
321	      h <> list.append(t, ys)
322	
323	def list.one(+x: String) -> List<&2, String>:
324	  x <> Nil{}
325	
326	def list.any(+xs: List<&2, String>) -> Bool:
327	  match xs:
328	    case Nil{}:
329	      False{}
330	    case Con{+_, +_}:
331	      True{}
332	
333	def list.first(xs: List<&2, String>) -> Maybe<&2, String>:
334	  match xs:
335	    case Nil{}:
336	      None{}
337	    case Con{+h, t}:
338	      Some{h}
339	
340	def ipv4.go(s: String) -> Bool:
341	  match s:
342	    case SNil{}:
343	      True{}
344	    case SCon{Chr{+c}, t}:
345	      Bool.and(Bool.or(U32.is_eq(c, 46), Bool.and(U32.is_le(48, c), U32.is_le(c, 57))), ipv4.go(t))
346	
347	# Digits and dots; TCP.connect rejects anything else that is not an address.
348	def ipv4(+s: String) -> Bool:
349	  Bool.and(Bool.not(String.is_empty(s)), ipv4.go(s))
350	
351	def ipv6.ch(+c: U32) -> Bool:
352	  Bool.or(
353	    Bool.and(U32.is_le(48, c), U32.is_le(c, 57)),
354	    Bool.or(
355	      Bool.and(U32.is_le(97, c), U32.is_le(c, 102)),
356	      Bool.and(U32.is_le(65, c), U32.is_le(c, 70))))
357	
358	def ipv6.go(s: String) -> Bool:
359	  match s:
360	    case SNil{}:
361	      True{}
362	    case SCon{Chr{+c}, t}:
363	      Bool.and(Bool.or(U32.is_eq(c, 58), ipv6.ch(c)), ipv6.go(t))
364	
365	def ipv6.has(s: String) -> Bool:
366	  match s:
367	    case SNil{}:
368	      False{}
369	    case SCon{Chr{+c}, t}:
370	      Bool.or(U32.is_eq(c, 58), ipv6.has(t))
371	
372	# Bracket-free IPv6 text; connect validates the address.
373	def ipv6(+s: String) -> Bool:
374	  Bool.and(Bool.and(Bool.not(String.is_empty(s)), ipv6.has(s)), ipv6.go(s))
375	
376	def ip(+s: String) -> Bool:
377	  Bool.or(ipv4(s), ipv6(s))
378	
379	# One attempt's outcome: try again, or this answer (None: no address).
380	type Try is Data:
381	  Again{}
382	  Got{ip: Maybe<&2, String>}
383	
384	def try.pure(s: Socket, t: Try) -> IO(Socket & Try):
385	  IO.pure(Socket & Try, (s, t))
386	
387	# A datagram from anyone but the nameserver's port 53 is ignored (retried).
388	def try.from(s: Socket, +ns: String, id: U32, hpd: String & U32 & (U32 & Array<U32>)) -> IO(Socket & Try):
389	  (h, +p, d) = hpd
390	  (n, w) = d
391	  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{}))
392	
393	def try.back(ns: String, id: U32, m: Socket & Result<&1, &1, U32 & String, String & U32 & (U32 & Array<U32>)>) -> 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 & (U32 & Array<U32>)> <- Wire.recv_from.words(s, 512, 5000)
410	        try.back(ns, id, back)
411	
412	# Bytes cannot be copied, so each attempt builds its own query. A name that query rejects ends the tries.
413	def try.send(s: Socket, +ns: String, id: U32, q: Maybe<&1, Bytes.Bytes>) -> IO(Socket & Try):
414	  match q:
415	    case None{}:
416	      try.pure(s, Got{None{}})
417	    case Some{Bytes.Bytes{n, w}}:
418	      do IO<Socket & Try>:
419	        sent : Socket & Result<&1, &1, U32 & String, Unit> <- Wire.send_to.words(s, ns, 53, n, w)
420	        try.sent(ns, id, sent)
421	
422	def try.once(s: Socket, +ns: String, +id: U32, name: String) -> IO(Socket & Try):
423	  try.send(s, ns, id, query(id, name))
424	
425	def try.close(s: Socket, r: Maybe<&2, String>) -> IO(Maybe<&2, String>):
426	  do IO<Maybe<&2, String>>:
427	    Socket.close(s)
428	    return r
429	
430	def tries.end(st: Socket & Try) -> IO(Maybe<&2, String>):
431	  (s, t) = st
432	  match t:
433	    case Got{ip}:
434	      try.close(s, ip)
435	    case Again{}:
436	      try.close(s, None{})
437	
438	# fuel: attempts left (resolv.conf's default is 2).
439	def tries(fuel: Nat, +ns: String, +id: U32, +name: String, st: Socket & Try) -> IO(Maybe<&2, String>):
440	  match fuel:
441	    case 0n:
442	      tries.end(st)
443	    case 1n+f:
444	      (s, t) = st
445	      match t:
446	        case Got{ip}:
447	          try.close(s, ip)
448	        case Again{}:
449	          do IO<Maybe<&2, String>>:
450	            next : Socket & Try <- try.once(s, ns, id, name)
451	            tries(f, ns, id, name, next)
452	
453	def resolve.sock(ns: String, id: U32, name: String, r: Result<&1, &1, U32 & String, Socket>) -> IO(Maybe<&2, String>):
454	  match r:
455	    case Fail{e}:
456	      none()
457	    case Done{s}:
458	      tries(2n, ns, id, name, (s, Again{}))
459	
460	# §7.3: a random id makes forged answers harder to land.
461	def resolve.id(name: String, ns: String, r: Result<&1, &1, U32 & String, U32>) -> IO(Maybe<&2, String>):
462	  match r:
463	    case Fail{e}:
464	      none()
465	    case Done{x}:
466	      do IO<Maybe<&2, String>>:
467	        u : Result<&1, &1, U32 & String, Socket> <- UDP.bind("0.0.0.0", 0)
468	        resolve.sock(ns, U32.and(x, 65535), name, u)
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.on_line(+name: String, ns: List<&2, String>) -> Bool:
552	  match ns:
553	    case Nil{}:
554	      False{}
555	    case Con{+n, t}:
556	      Bool.or(String.eq(String.to_lower(n), name), hosts.on_line(name, t))
557	
558	def hosts.line.all(+name: String, xs: List<&2, String>) -> List<&2, String>:
559	  match xs:
560	    case Nil{}:
561	      Nil{}
562	    case Con{+addr, ns}:
563	      Bool.pick(List<&2, String>, Bool.and(ip(addr), hosts.on_line(name, ns)), list.one(addr), Nil{})
564	
565	def hosts.sp(+c: U32, tab: Bool) -> U32:
566	  match tab:
567	    case True{}:
568	      32
569	    case False{}:
570	      c
571	
572	def hosts.flat(s: String) -> String:
573	  match s:
574	    case SNil{}:
575	      ""
576	    case SCon{Chr{+c}, t}:
577	      SCon{Chr{hosts.sp(c, U32.is_eq(c, 9))}, hosts.flat(t)}
578	
579	def hosts.scan.all(xs: List<&2, String>, +name: String, acc: List<&2, String>) -> List<&2, String>:
580	  match xs:
581	    case Nil{}:
582	      acc
583	    case Con{+line, t}:
584	      hosts.scan.all(t, name,
585	        list.append(acc, hosts.line.all(name, String.split(hosts.flat(line), ' '))))
586	
587	# Every address for name in an /etc/hosts file. The name is already lowercase.
588	def hosts.all(+name: String, text: String) -> List<&2, String>:
589	  hosts.scan.all(String.lines(text), name, Nil{})
590	
591	# First address for name in an /etc/hosts file. The name is already lowercase.
592	def hosts(+name: String, text: String) -> Maybe<&2, String>:
593	  list.first(hosts.all(name, text))
594	
595	def lookup.split(+s: String) -> List<&2, String>:
596	  List.filter(~String, ~(n => Bool.not(String.is_empty(n))), String.split(s, Chr{0}))
597	
598	# OS resolver: every address, NUL-separated in getaddrinfo order.
599	def lookup.all(host: String) -> IO(Result<&1, &1, U32 & String, String>):
600	  import "./effs/dns.c"
601	  import "./effs/dns.js"
602	
603	# Literals and localhost without the OS (for laws and fast paths).
604	def resolve.literal.all(+host: String) -> List<&2, String>:
605	  Bool.pick(List<&2, String>, ip(host), list.one(host),
606	    Bool.pick(List<&2, String>, String.eq(host, "localhost"),
607	      ["::1", "127.0.0.1"], Nil{}))
608	
609	def resolve.literal(+host: String) -> Maybe<&2, String>:
610	  list.first(resolve.literal.all(host))
611	
612	def resolve.all.got(r: Result<&1, &1, U32 & String, String>) -> IO(List<&2, String>):
613	  match r:
614	    case Fail{e}:
615	      IO.pure(List<&2, String>, Nil{})
616	    case Done{s}:
617	      IO.pure(List<&2, String>, lookup.split(s))
618	
619	def resolve.all.os(+name: String) -> IO(List<&2, String>):
620	  do IO<List<&2, String>>:
621	    r : Result<&1, &1, U32 & String, String> <- lookup.all(name)
622	    resolve.all.got(r)
623	
624	def resolve.all.dns.one(m: Maybe<&2, String>) -> IO(List<&2, String>):
625	  match m:
626	    case Some{ip}:
627	      IO.pure(List<&2, String>, list.one(ip))
628	    case None{}:
629	      IO.pure(List<&2, String>, Nil{})
630	
631	# ponytail: UDP path still asks for A records only
632	def resolve.all.dns(+name: String) -> IO(List<&2, String>):
633	  do IO<List<&2, String>>:
634	    m : Maybe<&2, String> <- resolve.dns(name)
635	    resolve.all.dns.one(m)
636	
637	def resolve.all.from(+name: String, +xs: List<&2, String>) -> IO(List<&2, String>):
638	  match xs:
639	    case Nil{}:
640	      resolve.all.dns(name)
641	    case Con{+_, +t}:
642	      IO.pure(List<&2, String>, xs)
643	
644	def resolve.all.text(+name: String, r: Result<&1, &1, U32 & String, String>) -> IO(List<&2, String>):
645	  match r:
646	    case Fail{e}:
647	      resolve.all.dns(name)
648	    case Done{s}:
649	      resolve.all.from(name, hosts.all(name, s))
650	
651	def resolve.all.opened(+name: String, m: File & Result<&1, &1, U32 & String, String>) -> IO(List<&2, String>):
652	  (f, r) = m
653	  do IO<List<&2, String>>:
654	    File.close(f)
655	    resolve.all.text(name, r)
656	
657	def resolve.all.hosts(+name: String, r: Result<&1, &1, U32 & String, File>) -> IO(List<&2, String>):
658	  match r:
659	    case Fail{e}:
660	      resolve.all.dns(name)
661	    case Done{f}:
662	      do IO<List<&2, String>>:
663	        m : File & Result<&1, &1, U32 & String, String> <- File.read(f, 65536)
664	        resolve.all.opened(name, m)
665	
666	def resolve.all.pick(+host: String, +xs: List<&2, String>) -> IO(List<&2, String>):
667	  match xs:
668	    case Nil{}:
669	      resolve.all.os(String.to_lower(host))
670	    case Con{+_, +t}:
671	      IO.pure(List<&2, String>, xs)
672	
673	def resolve.all(+host: String) -> IO(List<&2, String>):
674	  resolve.all.pick(host, resolve.literal.all(host))
675	
676	def resolve.all.ask(+name: String) -> IO(List<&2, String>):
677	  do IO<List<&2, String>>:
678	    f : Result<&1, &1, U32 & String, File> <- File.open("/etc/hosts", "r")
679	    resolve.all.hosts(name, f)
680	
681	def resolve.all.pure.pick(+host: String, +xs: List<&2, String>) -> IO(List<&2, String>):
682	  match xs:
683	    case Nil{}:
684	      resolve.all.ask(String.to_lower(host))
685	    case Con{+_, +t}:
686	      IO.pure(List<&2, String>, xs)
687	
688	def resolve.all.pure(+host: String) -> IO(List<&2, String>):
689	  resolve.all.pure.pick(host, resolve.literal.all(host))
690	
691	def resolve.pure(+host: String) -> IO(Maybe<&2, String>):
692	  do IO<Maybe<&2, String>>:
693	    xs : List<&2, String> <- resolve.all.pure(host)
694	    return list.first(xs)
695	
696	# First address from resolve.all (getaddrinfo order when the OS resolves).
697	def resolve(+host: String) -> IO(Maybe<&2, String>):
698	  do IO<Maybe<&2, String>>:
699	    xs : List<&2, String> <- resolve.all(host)
700	    return list.first(xs)