dns.bend source
dns.bend on the hub · documented module
# DNS codec and host lookup. Source: https://github.com/paymog/bend-kit/tree/main/dnsimport Baseimport bend-kit-wire@0.4.3.0/wire.bend as Wireimport bend-kit-bytes@0.3.2.0/bytes.bend as Bytes# query, answer, and resolve.pure are pure; PROOF.bend covers them, not effs/.# resolve.all uses the OS resolver (IPv4 and IPv6); resolve keeps the first address.# import bend-kit-dns@0.6.0.0/dns.bend as Dns# Query# -----def label.ok(+l: String) -> Bool: +n = String.length(l) Bool.and(Nat.is_lt(0n, n), Nat.is_le(n, 63n))def label.ascii(s: String) -> Bool: match s: case SNil{}: True{} case SCon{Chr{c}, t}: Bool.and(U32.is_lt(c, 128), label.ascii(t))def labels.ok(xs: List<&2, String>) -> Bool: match xs: case Nil{}: True{} case Con{+l, t}: Bool.and(Bool.and(label.ok(l), label.ascii(l)), labels.ok(t))# QNAME's length without its final zero octet.def labels.len(xs: List<&2, String>, +n: U32) -> U32: match xs: case Nil{}: n case Con{+l, t}: labels.len(t, (n + 1 + U32.from_nat(String.length(l)) : U32))# The query buffer is allocated to its exact size before writing.def written(r: Bytes.Cursor & Bool) -> Bytes.Cursor: (c, ok) = r cdef label.put(s: String, c: Bytes.Cursor) -> Bytes.Cursor: match s: case SNil{}: c case SCon{Chr{v}, t}: label.put(t, written(Bytes.Cursor.put.u8(c, v)))def labels.put(xs: List<&2, String>, c: Bytes.Cursor) -> Bytes.Cursor: match xs: case Nil{}: written(Bytes.Cursor.put.u8(c, 0)) case Con{+l, t}: labels.put(t, label.put(l, written(Bytes.Cursor.put.u8(c, U32.from_nat(String.length(l))))))def query.done(r: Bytes.Bytes & U32) -> Maybe<&1, Bytes.Bytes>: (b, pos) = r Some{b}def query.if(+id: U32, +xs: List<&2, String>, ok: Bool) -> Maybe<&1, Bytes.Bytes>: match ok: case False{}: None{} case True{}: # header: id, RD, QDCOUNT 1; question: QNAME, QTYPE A, QCLASS IN. c = Bytes.Cursor.new(Bytes.new((labels.len(xs, 0) + 17 : U32))) c = written(Bytes.Cursor.put.u16be(c, id)) c = written(Bytes.Cursor.put.u16be(c, 256)) c = written(Bytes.Cursor.put.u16be(c, 1)) c = written(Bytes.Cursor.skip(c, 6)) c = labels.put(xs, c) c = written(Bytes.Cursor.put.u16be(c, 1)) c = written(Bytes.Cursor.put.u16be(c, 1)) query.done(Bytes.Cursor.finish(c))def query.labels(+id: U32, +xs: List<&2, String>) -> Maybe<&1, Bytes.Bytes>: query.if(id, xs, labels.ok(xs))def strip_dot.if(+s: String, dot: Bool) -> String: match dot: case True{}: String.reverse(String.drop(String.reverse(s), 1n)) case False{}: sdef strip_dot(+s: String) -> String: strip_dot.if(s, String.ends_with(s, "."))# RFC 1035 §4.1: a standard query for the A record of name.def query(id: U32, name: String) -> Maybe<&1, Bytes.Bytes>: query.labels(id, String.split(strip_dot(name), '.'))# Answer# ------# One step through a name: continue at the next label or stop after the name.type Step is Data: Go{} Stop{ok: Bool}def name.advance(stop: Bool, r: Bytes.Cursor & Bool) -> Bytes.Cursor & Step: (c, ok) = r match ok: case False{}: (c, Stop{False{}}) case True{}: (c, Bool.pick(Step, stop, Stop{True{}}, Go{}))# §4.1.4: zero terminates, 192..255 starts a pointer, 64..191 is reserved.def name.label(ok: Bool, c: Bytes.Cursor, l: U32) -> Bytes.Cursor & Step: match ok: case False{}: (c, Stop{False{}}) case True{}: name.advance(False{}, Bytes.Cursor.skip(c, l))def name.pointer(pointer: Bool, +l: U32, c: Bytes.Cursor) -> Bytes.Cursor & Step: match pointer: case True{}: name.advance(True{}, Bytes.Cursor.skip(c, 1)) case False{}: name.label(U32.is_lt(l, 64), c, l)def name.step.of(+l: U32, c: Bytes.Cursor) -> Bytes.Cursor & Step: match l: case 0: (c, Stop{True{}}) case _: name.pointer(U32.is_le(192, l), l, c)def name.step(r: Bytes.Cursor & Maybe<&2, U32>) -> Bytes.Cursor & Step: (c, m) = r match m: case None{}: (c, Stop{False{}}) case Some{l}: name.step.of(l, c)def name.walk(fuel: Nat, r: Bytes.Cursor & Step) -> Bytes.Cursor & Bool: match fuel: case 0n: (c, s) = r (c, False{}) case 1n+f: (c, s) = r match s: case Stop{ok}: (c, ok) case Go{}: name.walk(f, name.step(Bytes.Cursor.u8(c)))# §2.3.4: a name is at most 255 octets, so retain the 128-step limit.def name.skip(c: Bytes.Cursor) -> Bytes.Cursor & Bool: name.walk(128n, name.step(Bytes.Cursor.u8(c)))type RR is Data: RRBad{} RRA{ip: String} RRSkip{}def dotted(+ip: U32) -> String: 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))def rr.a(limit: Bytes.CursorLimit, r: Bytes.Cursor & Maybe<&2, U32>) -> Bytes.Cursor & RR: (c, m) = r match m: case None{}: (Bytes.Cursor.leave(c, limit), RRBad{}) case Some{ip}: (Bytes.Cursor.leave(c, limit), RRA{dotted(ip)})def rr.data.some(a: Bool, c: Bytes.Cursor, limit: Bytes.CursorLimit) -> Bytes.Cursor & RR: match a: case True{}: rr.a(limit, Bytes.Cursor.u32be(c)) case False{}: (Bytes.Cursor.leave(c, limit), RRSkip{})# Bound RDATA in the original packed buffer, then resume after the entire region.def rr.data(a: Bool, r: Bytes.Cursor & Maybe<&1, Bytes.CursorLimit>) -> Bytes.Cursor & RR: (c, m) = r match m: case None{}: (c, RRBad{}) case Some{limit}: rr.data.some(a, c, limit)def rr.len(+ty: U32, +cl: U32, r: Bytes.Cursor & Maybe<&2, U32>) -> Bytes.Cursor & RR: (c, m) = r match m: case None{}: (c, RRBad{}) case Some{+len}: 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))def rr.ttl(+ty: U32, +cl: U32, r: Bytes.Cursor & Bool) -> Bytes.Cursor & RR: (c, ok) = r match ok: case False{}: (c, RRBad{}) case True{}: rr.len(ty, cl, Bytes.Cursor.u16be(c))def rr.cl(+ty: U32, r: Bytes.Cursor & Maybe<&2, U32>) -> Bytes.Cursor & RR: (c, m) = r match m: case None{}: (c, RRBad{}) case Some{cl}: rr.ttl(ty, cl, Bytes.Cursor.skip(c, 4))def rr.ty(r: Bytes.Cursor & Maybe<&2, U32>) -> Bytes.Cursor & RR: (c, m) = r match m: case None{}: (c, RRBad{}) case Some{ty}: rr.cl(ty, Bytes.Cursor.u16be(c))def rr.name(r: Bytes.Cursor & Bool) -> Bytes.Cursor & RR: (c, ok) = r match ok: case False{}: (c, RRBad{}) case True{}: rr.ty(Bytes.Cursor.u16be(c))# §4.1.3: NAME, TYPE, CLASS, TTL, RDLENGTH, RDATA.def rr(c: Bytes.Cursor) -> Bytes.Cursor & RR: rr.name(name.skip(c))# fuel = records left. The first A record wins; CNAMEs before it are skipped.def answers.scan(fuel: Nat, r: Bytes.Cursor & RR) -> Maybe<&2, String>: match fuel: case 0n: None{} case 1n+f: (c, x) = r match x: case RRBad{}: None{} case RRA{ip}: Some{ip} case RRSkip{}: answers.scan(f, rr(c))# QTYPE and QCLASS follow the name.def question.end(r: Bytes.Cursor & Bool) -> Bytes.Cursor & Bool: (c, ok) = r match ok: case False{}: (c, False{}) case True{}: Bytes.Cursor.skip(c, 4)def questions(fuel: Nat, r: Bytes.Cursor & Bool) -> Bytes.Cursor & Bool: match fuel: case 0n: r case 1n+f: (c, ok) = r match ok: case False{}: (c, False{}) case True{}: questions(f, question.end(name.skip(c)))def body.go(+an: U32, r: Bytes.Cursor & Bool) -> Maybe<&2, String>: (c, ok) = r match ok: case False{}: None{} case True{}: answers.scan(U32.to_nat(an), rr(c))# The header ends with NSCOUNT and ARCOUNT; questions follow.def body.an(+qd: U32, r: Bytes.Cursor & Maybe<&2, U32>) -> Maybe<&2, String>: (c, m) = r match m: case None{}: None{} case Some{an}: body.go(an, questions(U32.to_nat(qd), Bytes.Cursor.skip(c, 4)))def body.qd(r: Bytes.Cursor & Maybe<&2, U32>) -> Maybe<&2, String>: (c, m) = r match m: case None{}: None{} case Some{qd}: body.an(qd, Bytes.Cursor.u16be(c))# §4.1.1: QR set, opcode QUERY, not truncated, RCODE 0.def flags.ok(+f: U32) -> Bool: 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)))def head.flags.if(ok: Bool, c: Bytes.Cursor) -> Maybe<&2, String>: match ok: case False{}: None{} case True{}: body.qd(Bytes.Cursor.u16be(c))def head.flags(r: Bytes.Cursor & Maybe<&2, U32>) -> Maybe<&2, String>: (c, m) = r match m: case None{}: None{} case Some{f}: head.flags.if(flags.ok(f), c)def head.id.if(ok: Bool, c: Bytes.Cursor) -> Maybe<&2, String>: match ok: case False{}: None{} case True{}: head.flags(Bytes.Cursor.u16be(c))def head.id(+id: U32, r: Bytes.Cursor & Maybe<&2, U32>) -> Maybe<&2, String>: (c, m) = r match m: case None{}: None{} case Some{got}: head.id.if(U32.is_eq(id, got), c)# The IPv4 address the response gives for the query with this id.def answer(id: U32, msg: Bytes.Bytes) -> Maybe<&2, String>: head.id(id, Bytes.Cursor.u16be(Bytes.Cursor.new(msg)))# resolv.conf# -----------def nameservers.add(+line: String, rest: List<&2, String>, hit: Bool) -> List<&2, String>: match hit: case False{}: rest case True{}: Con{String.trim(String.drop(line, 10n)), rest}def nameservers.go(xs: List<&2, String>) -> List<&2, String>: match xs: case Nil{}: Nil{} case Con{+line, t}: nameservers.add(line, nameservers.go(t), String.starts_with(line, "nameserver"))# Every nameserver line, in file order.def nameservers(conf: String) -> List<&2, String>: nameservers.go(String.lines(conf))def nameserver.first(xs: List<&2, String>) -> Maybe<&2, String>: match xs: case Nil{}: None{} case Con{n, t}: Some{n}# The first nameserver line of a resolv.conf.def nameserver(conf: String) -> Maybe<&2, String>: nameserver.first(nameservers(conf))# Resolve# -------def none() -> IO(Maybe<&2, String>): IO.pure(Maybe<&2, String>, None{})def list.append(xs: List<&2, String>, ys: List<&2, String>) -> List<&2, String>: match xs: case Nil{}: ys case Con{+h, t}: h <> list.append(t, ys)def list.one(+x: String) -> List<&2, String>: x <> Nil{}def list.any(+xs: List<&2, String>) -> Bool: match xs: case Nil{}: False{} case Con{+_, +_}: True{}def list.first(xs: List<&2, String>) -> Maybe<&2, String>: match xs: case Nil{}: None{} case Con{+h, t}: Some{h}def ipv4.go(s: String) -> Bool: match s: case SNil{}: True{} case SCon{Chr{+c}, t}: Bool.and(Bool.or(U32.is_eq(c, 46), Bool.and(U32.is_le(48, c), U32.is_le(c, 57))), ipv4.go(t))# Digits and dots; TCP.connect rejects anything else that is not an address.def ipv4(+s: String) -> Bool: Bool.and(Bool.not(String.is_empty(s)), ipv4.go(s))def ipv6.ch(+c: U32) -> Bool: Bool.or( Bool.and(U32.is_le(48, c), U32.is_le(c, 57)), Bool.or( Bool.and(U32.is_le(97, c), U32.is_le(c, 102)), Bool.and(U32.is_le(65, c), U32.is_le(c, 70))))def ipv6.go(s: String) -> Bool: match s: case SNil{}: True{} case SCon{Chr{+c}, t}: Bool.and(Bool.or(U32.is_eq(c, 58), ipv6.ch(c)), ipv6.go(t))def ipv6.has(s: String) -> Bool: match s: case SNil{}: False{} case SCon{Chr{+c}, t}: Bool.or(U32.is_eq(c, 58), ipv6.has(t))# Bracket-free IPv6 text; connect validates the address.def ipv6(+s: String) -> Bool: Bool.and(Bool.and(Bool.not(String.is_empty(s)), ipv6.has(s)), ipv6.go(s))def ip(+s: String) -> Bool: Bool.or(ipv4(s), ipv6(s))# One attempt's outcome: try again, or this answer (None: no address).type Try is Data: Again{} Got{ip: Maybe<&2, String>}def try.pure(s: Socket, t: Try) -> IO(Socket & Try): IO.pure(Socket & Try, (s, t))# A datagram from anyone but the nameserver's port 53 is ignored (retried).def try.from(s: Socket, +ns: String, id: U32, hpd: String & U32 & (U32 & Array<U32>)) -> IO(Socket & Try): (h, +p, d) = hpd (n, w) = d 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{}))def try.back(ns: String, id: U32, m: Socket & Result<&1, &1, U32 & String, String & U32 & (U32 & Array<U32>)>) -> IO(Socket & Try): (s, r) = m match r: case Fail{e}: try.pure(s, Again{}) case Done{hpd}: try.from(s, ns, id, hpd)# §4.2.1 and resolv.conf defaults: 5 s per attempt.def try.sent(ns: String, id: U32, m: Socket & Result<&1, &1, U32 & String, Unit>) -> IO(Socket & Try): (s, r) = m match r: case Fail{e}: try.pure(s, Again{}) case Done{u}: do IO<Socket & Try>: back : Socket & Result<&1, &1, U32 & String, String & U32 & (U32 & Array<U32>)> <- Wire.recv_from.words(s, 512, 5000) try.back(ns, id, back)# Bytes cannot be copied, so each attempt builds its own query. A name that query rejects ends the tries.def try.send(s: Socket, +ns: String, id: U32, q: Maybe<&1, Bytes.Bytes>) -> IO(Socket & Try): match q: case None{}: try.pure(s, Got{None{}}) case Some{Bytes.Bytes{n, w}}: do IO<Socket & Try>: sent : Socket & Result<&1, &1, U32 & String, Unit> <- Wire.send_to.words(s, ns, 53, n, w) try.sent(ns, id, sent)def try.once(s: Socket, +ns: String, +id: U32, name: String) -> IO(Socket & Try): try.send(s, ns, id, query(id, name))def try.close(s: Socket, r: Maybe<&2, String>) -> IO(Maybe<&2, String>): do IO<Maybe<&2, String>>: Socket.close(s) return rdef tries.end(st: Socket & Try) -> IO(Maybe<&2, String>): (s, t) = st match t: case Got{ip}: try.close(s, ip) case Again{}: try.close(s, None{})# fuel: attempts left (resolv.conf's default is 2).def tries(fuel: Nat, +ns: String, +id: U32, +name: String, st: Socket & Try) -> IO(Maybe<&2, String>): match fuel: case 0n: tries.end(st) case 1n+f: (s, t) = st match t: case Got{ip}: try.close(s, ip) case Again{}: do IO<Maybe<&2, String>>: next : Socket & Try <- try.once(s, ns, id, name) tries(f, ns, id, name, next)def resolve.sock(ns: String, id: U32, name: String, r: Result<&1, &1, U32 & String, Socket>) -> IO(Maybe<&2, String>): match r: case Fail{e}: none() case Done{s}: tries(2n, ns, id, name, (s, Again{}))# §7.3: a random id makes forged answers harder to land.def resolve.id(name: String, ns: String, r: Result<&1, &1, U32 & String, U32>) -> IO(Maybe<&2, String>): match r: case Fail{e}: none() case Done{x}: do IO<Maybe<&2, String>>: u : Result<&1, &1, U32 & String, Socket> <- UDP.bind("0.0.0.0", 0) resolve.sock(ns, U32.and(x, 65535), name, u)def resolve.ns(name: String, ns: Maybe<&2, String>) -> IO(Maybe<&2, String>): match ns: case None{}: none() case Some{n}: do IO<Maybe<&2, String>>: r : Result<&1, &1, U32 & String, U32> <- IO.random_u32() resolve.id(name, n, r)# Ask one nameserver. Tests use this; resolve reads /etc/resolv.conf.def resolve.at(+host: String, ns: String) -> IO(Maybe<&2, String>): resolve.ns(host, Some{ns})def conf.text(r: Result<&1, &1, U32 & String, String>) -> String: match r: case Fail{e}: "" case Done{s}: s# ponytail: 3 nameservers; a longer resolv.conf ignores the restdef resolve.n3(+name: String, xs: List<&2, String>) -> IO(Maybe<&2, String>): match xs: case Nil{}: none() case Con{+ns, t}: resolve.at(name, ns)def resolve.n2b(+name: String, rest: List<&2, String>, ip: Maybe<&2, String>) -> IO(Maybe<&2, String>): match ip: case Some{s}: IO.pure(Maybe<&2, String>, Some{s}) case None{}: resolve.n3(name, rest)def resolve.n2(+name: String, xs: List<&2, String>) -> IO(Maybe<&2, String>): match xs: case Nil{}: none() case Con{+ns, t}: do IO<Maybe<&2, String>>: ip : Maybe<&2, String> <- resolve.at(name, ns) resolve.n2b(name, t, ip)def resolve.n1b(+name: String, rest: List<&2, String>, ip: Maybe<&2, String>) -> IO(Maybe<&2, String>): match ip: case Some{s}: IO.pure(Maybe<&2, String>, Some{s}) case None{}: resolve.n2(name, rest)def resolve.list(+name: String, xs: List<&2, String>) -> IO(Maybe<&2, String>): match xs: case Nil{}: none() case Con{+ns, t}: do IO<Maybe<&2, String>>: ip : Maybe<&2, String> <- resolve.at(name, ns) resolve.n1b(name, t, ip)def resolve.read(name: String, m: File & Result<&1, &1, U32 & String, String>) -> IO(Maybe<&2, String>): (f, r) = m do IO<Maybe<&2, String>>: File.close(f) resolve.list(name, nameservers(conf.text(r)))def resolve.conf(name: String, r: Result<&1, &1, U32 & String, File>) -> IO(Maybe<&2, String>): match r: case Fail{e}: none() case Done{f}: do IO<Maybe<&2, String>>: m : File & Result<&1, &1, U32 & String, String> <- File.read(f, 65536) resolve.read(name, m)def resolve.dns(name: String) -> IO(Maybe<&2, String>): do IO<Maybe<&2, String>>: f : Result<&1, &1, U32 & String, File> <- File.open("/etc/resolv.conf", "r") resolve.conf(name, f)def hosts.on_line(+name: String, ns: List<&2, String>) -> Bool: match ns: case Nil{}: False{} case Con{+n, t}: Bool.or(String.eq(String.to_lower(n), name), hosts.on_line(name, t))def hosts.line.all(+name: String, xs: List<&2, String>) -> List<&2, String>: match xs: case Nil{}: Nil{} case Con{+addr, ns}: Bool.pick(List<&2, String>, Bool.and(ip(addr), hosts.on_line(name, ns)), list.one(addr), Nil{})def hosts.sp(+c: U32, tab: Bool) -> U32: match tab: case True{}: 32 case False{}: cdef hosts.flat(s: String) -> String: match s: case SNil{}: "" case SCon{Chr{+c}, t}: SCon{Chr{hosts.sp(c, U32.is_eq(c, 9))}, hosts.flat(t)}def hosts.scan.all(xs: List<&2, String>, +name: String, acc: List<&2, String>) -> List<&2, String>: match xs: case Nil{}: acc case Con{+line, t}: hosts.scan.all(t, name, list.append(acc, hosts.line.all(name, String.split(hosts.flat(line), ' '))))# Every address for name in an /etc/hosts file. The name is already lowercase.def hosts.all(+name: String, text: String) -> List<&2, String>: hosts.scan.all(String.lines(text), name, Nil{})# First address for name in an /etc/hosts file. The name is already lowercase.def hosts(+name: String, text: String) -> Maybe<&2, String>: list.first(hosts.all(name, text))def lookup.split(+s: String) -> List<&2, String>: List.filter(~String, ~(n => Bool.not(String.is_empty(n))), String.split(s, Chr{0}))# OS resolver: every address, NUL-separated in getaddrinfo order.def lookup.all(host: String) -> IO(Result<&1, &1, U32 & String, String>): import "./effs/dns.c" import "./effs/dns.js"# Literals and localhost without the OS (for laws and fast paths).def resolve.literal.all(+host: String) -> List<&2, String>: Bool.pick(List<&2, String>, ip(host), list.one(host), Bool.pick(List<&2, String>, String.eq(host, "localhost"), ["::1", "127.0.0.1"], Nil{}))def resolve.literal(+host: String) -> Maybe<&2, String>: list.first(resolve.literal.all(host))def resolve.all.got(r: Result<&1, &1, U32 & String, String>) -> IO(List<&2, String>): match r: case Fail{e}: IO.pure(List<&2, String>, Nil{}) case Done{s}: IO.pure(List<&2, String>, lookup.split(s))def resolve.all.os(+name: String) -> IO(List<&2, String>): do IO<List<&2, String>>: r : Result<&1, &1, U32 & String, String> <- lookup.all(name) resolve.all.got(r)def resolve.all.dns.one(m: Maybe<&2, String>) -> IO(List<&2, String>): match m: case Some{ip}: IO.pure(List<&2, String>, list.one(ip)) case None{}: IO.pure(List<&2, String>, Nil{})# ponytail: UDP path still asks for A records onlydef resolve.all.dns(+name: String) -> IO(List<&2, String>): do IO<List<&2, String>>: m : Maybe<&2, String> <- resolve.dns(name) resolve.all.dns.one(m)def resolve.all.from(+name: String, +xs: List<&2, String>) -> IO(List<&2, String>): match xs: case Nil{}: resolve.all.dns(name) case Con{+_, +t}: IO.pure(List<&2, String>, xs)def resolve.all.text(+name: String, r: Result<&1, &1, U32 & String, String>) -> IO(List<&2, String>): match r: case Fail{e}: resolve.all.dns(name) case Done{s}: resolve.all.from(name, hosts.all(name, s))def resolve.all.opened(+name: String, m: File & Result<&1, &1, U32 & String, String>) -> IO(List<&2, String>): (f, r) = m do IO<List<&2, String>>: File.close(f) resolve.all.text(name, r)def resolve.all.hosts(+name: String, r: Result<&1, &1, U32 & String, File>) -> IO(List<&2, String>): match r: case Fail{e}: resolve.all.dns(name) case Done{f}: do IO<List<&2, String>>: m : File & Result<&1, &1, U32 & String, String> <- File.read(f, 65536) resolve.all.opened(name, m)def resolve.all.pick(+host: String, +xs: List<&2, String>) -> IO(List<&2, String>): match xs: case Nil{}: resolve.all.os(String.to_lower(host)) case Con{+_, +t}: IO.pure(List<&2, String>, xs)def resolve.all(+host: String) -> IO(List<&2, String>): resolve.all.pick(host, resolve.literal.all(host))def resolve.all.ask(+name: String) -> IO(List<&2, String>): do IO<List<&2, String>>: f : Result<&1, &1, U32 & String, File> <- File.open("/etc/hosts", "r") resolve.all.hosts(name, f)def resolve.all.pure.pick(+host: String, +xs: List<&2, String>) -> IO(List<&2, String>): match xs: case Nil{}: resolve.all.ask(String.to_lower(host)) case Con{+_, +t}: IO.pure(List<&2, String>, xs)def resolve.all.pure(+host: String) -> IO(List<&2, String>): resolve.all.pure.pick(host, resolve.literal.all(host))def resolve.pure(+host: String) -> IO(Maybe<&2, String>): do IO<Maybe<&2, String>>: xs : List<&2, String> <- resolve.all.pure(host) return list.first(xs)# First address from resolve.all (getaddrinfo order when the OS resolves).def resolve(+host: String) -> IO(Maybe<&2, String>): do IO<Maybe<&2, String>>: xs : List<&2, String> <- resolve.all(host) return list.first(xs)