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