dns.bend

bend-kit-dns@0.7.0.0 · 756 lines · 110 definitions

1# DNS codec and host lookup. Source: https://github.com/paymog/bend-kit/tree/main/dns
2import Base
3import bend-kit-wire@0.4.6.2/wire.bend as Wire
4import bend-kit-bytes@0.3.3.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
13def label.ok(+l: String) -> Bool:
14  +n = String.length(l)
15  Bool.and(Nat.is_lt(0n, n), Nat.is_le(n, 63n))
16
17def 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
24def 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.
32def 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.
40def written(r: Bytes.Cursor & Bool) -> Bytes.Cursor:
41  (c, ok) = r
42  c
43
44def 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
51def 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
58def query.done(r: Bytes.Bytes & U32) -> Maybe<&1, Bytes.Bytes>:
59  (b, pos) = r
60  Some{b}
61
62def 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.
79def 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
82def 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
89def 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.
93def 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.
100type Step is Data:
101  Go{}
102  Stop{ok: Bool}
103
104def 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.
113def 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
120def 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
127def 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
134def 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
142def 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.
156def name.skip(c: Bytes.Cursor) -> Bytes.Cursor & Bool:
157  name.walk(128n, name.step(Bytes.Cursor.u8(c)))
158
159type RR is Data:
160  RRBad{}
161  RRA{ip: String}
162  RRSkip{}
163
164def 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
167def 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
175def 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.
183def 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
191def 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
199def 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
207def 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
215def 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
223def 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.
232def 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.
236def 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.
251def 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
259def 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
271def 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.
280def 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
288def 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.
297def 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
300def 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
307def 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
315def 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
322def 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.
331def 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
337def 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
344def 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.
352def nameservers(conf: String) -> List<&2, String>:
353  nameservers.go(String.lines(conf))
354
355def 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.
363def nameserver(conf: String) -> Maybe<&2, String>:
364  nameserver.first(nameservers(conf))
365
366# Resolve
367# -------
368
369def none() -> IO(Maybe<&2, String>):
370  IO.pure(Maybe<&2, String>, None{})
371
372def 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
379def list.one(+x: String) -> List<&2, String>:
380  x <> Nil{}
381
382def list.any(+xs: List<&2, String>) -> Bool:
383  match xs:
384    case Nil{}:
385      False{}
386    case Con{+_, +_}:
387      True{}
388
389def 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
396def 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.
404def ipv4(+s: String) -> Bool:
405  Bool.and(Bool.not(String.is_empty(s)), ipv4.go(s))
406
407def 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
414def 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
421def 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.
429def ipv6(+s: String) -> Bool:
430  Bool.and(Bool.and(Bool.not(String.is_empty(s)), ipv6.has(s)), ipv6.go(s))
431
432def 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).
436type Try is Data:
437  Again{}
438  Got{ip: Maybe<&2, String>}
439
440def 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).
444def 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
449def 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.
458def 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.
469def 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
478def try.once(s: Socket, +ns: String, +id: U32, name: String) -> IO(Socket & Try):
479  try.send(s, ns, id, query(id, name))
480
481def 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
486def 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).
495def 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
509def 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.
517def 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
526def 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.
536def resolve.at(+host: String, ns: String) -> IO(Maybe<&2, String>):
537  resolve.ns(host, Some{ns})
538
539def 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
547def 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
554def 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
561def 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
570def 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
577def 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
586def 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
592def 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
601def 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
607def 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
614def 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
621def hosts.sp(+c: U32, tab: Bool) -> U32:
622  match tab:
623    case True{}:
624      32
625    case False{}:
626      c
627
628def 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
635def 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.
644def 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.
648def hosts(+name: String, text: String) -> Maybe<&2, String>:
649  list.first(hosts.all(name, text))
650
651def 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.
655def 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).
660def 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
665def resolve.literal(+host: String) -> Maybe<&2, String>:
666  list.first(resolve.literal.all(host))
667
668def 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
675def 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
680def 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
688def 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
693def 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
700def 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
707def 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
713def 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
722def 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
729def resolve.all(+host: String) -> IO(List<&2, String>):
730  resolve.all.pick(host, resolve.literal.all(host))
731
732def 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
737def 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
744def resolve.all.pure(+host: String) -> IO(List<&2, String>):
745  resolve.all.pure.pick(host, resolve.literal.all(host))
746
747def 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).
753def 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)