dns.bend
bend-kit-dns@0.5.0.0 · 700 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.3.0/wire.bend as Wire
4import 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
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
39def 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.
47def 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
55def 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
64def query.labels(+id: U32, +xs: List<&2, String>) -> Maybe<&1, Bytes.Bytes>:
65 query.if(id, xs, labels.ok(xs))
66
67def 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
74def 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.
78def 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.
85type 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.
90def 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
93def 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
101def 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.
115def name.skip(b: Bytes.Bytes, +i: U32) -> Bytes.Bytes & Maybe<&2, U32>:
116 name.walk(128n, name.step(i, Bytes.get(b, i)))
117
118type RR is Data:
119 RRBad{}
120 RRA{ip: String}
121 RRSkip{at: U32}
122
123def 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
126def 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.
135def 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
142def 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
150def 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
158def 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
166def 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.
175def 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.
179def 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.
194def 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
202def 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
215def 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.
224def 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
232def 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.
241def 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
244def 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
251def 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
259def 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
266def 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.
275def answer(id: U32, msg: Bytes.Bytes) -> Maybe<&2, String>:
276 head.id(id, Bytes.get.u16be(msg, 0))
277
278# resolv.conf
279# -----------
280
281def 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
288def 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.
296def nameservers(conf: String) -> List<&2, String>:
297 nameservers.go(String.lines(conf))
298
299def 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.
307def nameserver(conf: String) -> Maybe<&2, String>:
308 nameserver.first(nameservers(conf))
309
310# Resolve
311# -------
312
313def none() -> IO(Maybe<&2, String>):
314 IO.pure(Maybe<&2, String>, None{})
315
316def 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
323def list.one(+x: String) -> List<&2, String>:
324 x <> Nil{}
325
326def list.any(+xs: List<&2, String>) -> Bool:
327 match xs:
328 case Nil{}:
329 False{}
330 case Con{+_, +_}:
331 True{}
332
333def 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
340def 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.
348def ipv4(+s: String) -> Bool:
349 Bool.and(Bool.not(String.is_empty(s)), ipv4.go(s))
350
351def 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
358def 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
365def 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.
373def ipv6(+s: String) -> Bool:
374 Bool.and(Bool.and(Bool.not(String.is_empty(s)), ipv6.has(s)), ipv6.go(s))
375
376def 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).
380type Try is Data:
381 Again{}
382 Got{ip: Maybe<&2, String>}
383
384def 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).
388def 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
393def 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.
402def 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.
413def 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
422def try.once(s: Socket, +ns: String, +id: U32, name: String) -> IO(Socket & Try):
423 try.send(s, ns, id, query(id, name))
424
425def 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
430def 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).
439def 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
453def 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.
461def 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
470def 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.
480def resolve.at(+host: String, ns: String) -> IO(Maybe<&2, String>):
481 resolve.ns(host, Some{ns})
482
483def 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
491def 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
498def 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
505def 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
514def 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
521def 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
530def 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
536def 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
545def 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
551def 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
558def 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
565def hosts.sp(+c: U32, tab: Bool) -> U32:
566 match tab:
567 case True{}:
568 32
569 case False{}:
570 c
571
572def 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
579def 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.
588def 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.
592def hosts(+name: String, text: String) -> Maybe<&2, String>:
593 list.first(hosts.all(name, text))
594
595def 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.
599def 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).
604def 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
609def resolve.literal(+host: String) -> Maybe<&2, String>:
610 list.first(resolve.literal.all(host))
611
612def 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
619def 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
624def 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
632def 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
637def 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
644def 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
651def 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
657def 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
666def 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
673def resolve.all(+host: String) -> IO(List<&2, String>):
674 resolve.all.pick(host, resolve.literal.all(host))
675
676def 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
681def 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
688def resolve.all.pure(+host: String) -> IO(List<&2, String>):
689 resolve.all.pure.pick(host, resolve.literal.all(host))
690
691def 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).
697def 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)