dns.bend
bend-kit-dns@0.6.0.2 · 755 lines · 0 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.1/wire.bend as Wire
4import 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
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
78def query.labels(+id: U32, +xs: List<&2, String>) -> Maybe<&1, Bytes.Bytes>:
79 query.if(id, xs, labels.ok(xs))
80
81def 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
88def 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.
92def 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.
99type Step is Data:
100 Go{}
101 Stop{ok: Bool}
102
103def 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.
112def 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
119def 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
126def 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
133def 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
141def 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.
155def name.skip(c: Bytes.Cursor) -> Bytes.Cursor & Bool:
156 name.walk(128n, name.step(Bytes.Cursor.u8(c)))
157
158type RR is Data:
159 RRBad{}
160 RRA{ip: String}
161 RRSkip{}
162
163def 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
166def 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
174def 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.
182def 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
190def 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
198def 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
206def 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
214def 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
222def 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.
231def 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.
235def 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.
250def 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
258def 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
270def 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.
279def 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
287def 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.
296def 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
299def 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
306def 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
314def 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
321def 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.
330def 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
336def 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
343def 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.
351def nameservers(conf: String) -> List<&2, String>:
352 nameservers.go(String.lines(conf))
353
354def 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.
362def nameserver(conf: String) -> Maybe<&2, String>:
363 nameserver.first(nameservers(conf))
364
365# Resolve
366# -------
367
368def none() -> IO(Maybe<&2, String>):
369 IO.pure(Maybe<&2, String>, None{})
370
371def 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
378def list.one(+x: String) -> List<&2, String>:
379 x <> Nil{}
380
381def list.any(+xs: List<&2, String>) -> Bool:
382 match xs:
383 case Nil{}:
384 False{}
385 case Con{+_, +_}:
386 True{}
387
388def 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
395def 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.
403def ipv4(+s: String) -> Bool:
404 Bool.and(Bool.not(String.is_empty(s)), ipv4.go(s))
405
406def 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
413def 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
420def 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.
428def ipv6(+s: String) -> Bool:
429 Bool.and(Bool.and(Bool.not(String.is_empty(s)), ipv6.has(s)), ipv6.go(s))
430
431def 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).
435type Try is Data:
436 Again{}
437 Got{ip: Maybe<&2, String>}
438
439def 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).
443def 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
448def 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.
457def 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.
468def 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
477def try.once(s: Socket, +ns: String, +id: U32, name: String) -> IO(Socket & Try):
478 try.send(s, ns, id, query(id, name))
479
480def 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
485def 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).
494def 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
508def 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.
516def 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
525def 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.
535def resolve.at(+host: String, ns: String) -> IO(Maybe<&2, String>):
536 resolve.ns(host, Some{ns})
537
538def 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
546def 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
553def 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
560def 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
569def 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
576def 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
585def 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
591def 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
600def 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
606def 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
613def 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
620def hosts.sp(+c: U32, tab: Bool) -> U32:
621 match tab:
622 case True{}:
623 32
624 case False{}:
625 c
626
627def 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
634def 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.
643def 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.
647def hosts(+name: String, text: String) -> Maybe<&2, String>:
648 list.first(hosts.all(name, text))
649
650def 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.
654def 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).
659def 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
664def resolve.literal(+host: String) -> Maybe<&2, String>:
665 list.first(resolve.literal.all(host))
666
667def 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
674def 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
679def 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
687def 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
692def 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
699def 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
706def 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
712def 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
721def 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
728def resolve.all(+host: String) -> IO(List<&2, String>):
729 resolve.all.pick(host, resolve.literal.all(host))
730
731def 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
736def 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
743def resolve.all.pure(+host: String) -> IO(List<&2, String>):
744 resolve.all.pure.pick(host, resolve.literal.all(host))
745
746def 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).
752def 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)