netip.bend

bend-kit-netip@0.1.0.0 · 425 lines · 67 definitions

1# IPv4 and IPv6 address values: strict parsing, RFC 5952 text, and CIDR prefixes. Source: https://github.com/paymog/bend-kit/tree/main/netip
2import Base
3
4# V4: the address as one big-endian word. V6: four network-order words, a first.
5type Addr is Data:
6  V4{word: U32}
7  V6{a: U32, b: U32, c: U32, d: U32}
8
9# A hex digit's value, or 16 when c is not one.
10def hexval(+c: U32) -> U32:
11  Bool.pick(U32, Bool.and(U32.is_le(48, c), U32.is_le(c, 57)), (c - 48 : U32),
12    Bool.pick(U32, Bool.and(U32.is_le(97, c), U32.is_le(c, 102)), (c - 87 : U32),
13      Bool.pick(U32, Bool.and(U32.is_le(65, c), U32.is_le(c, 70)), (c - 55 : U32), 16)))
14
15def hex.step(+d: U32, acc: Maybe<&2, U32>) -> Maybe<&2, U32>:
16  match acc:
17    case None{}:
18      None{}
19    case Some{v}:
20      Bool.pick(Maybe<&2, U32>, U32.is_lt(d, 16), Some{(v * 16 + d : U32)}, None{})
21
22def hex.go(s: String, acc: Maybe<&2, U32>) -> Maybe<&2, U32>:
23  match s:
24    case SNil{}:
25      acc
26    case SCon{Chr{c}, t}:
27      hex.go(t, hex.step(hexval(c), acc))
28
29def hextet.ok(ok: Bool, s: String) -> Maybe<&2, U32>:
30  match ok:
31    case True{}:
32      hex.go(s, Some{0})
33    case False{}:
34      None{}
35
36# One IPv6 group: 1 to 4 hex digits, either case.
37def hextet(+s: String) -> Maybe<&2, U32>:
38  hextet.ok(Bool.and(Bool.not(String.is_empty(s)), Nat.is_le(String.length(s), 4n)), s)
39
40# A non-digit wraps past 9 in (c - 48), so it fails the digit test.
41def dec.step(+d: U32, acc: Maybe<&2, U32>) -> Maybe<&2, U32>:
42  match acc:
43    case None{}:
44      None{}
45    case Some{v}:
46      Bool.pick(Maybe<&2, U32>, U32.is_lt(d, 10), Some{(v * 10 + d : U32)}, None{})
47
48def dec.go(s: String, acc: Maybe<&2, U32>) -> Maybe<&2, U32>:
49  match s:
50    case SNil{}:
51      acc
52    case SCon{Chr{c}, t}:
53      dec.go(t, dec.step((c - 48 : U32), acc))
54
55# 1 to 3 characters, and no leading zero unless the octet is "0".
56def octet.lead(s: String) -> Bool:
57  match s:
58    case SNil{}:
59      False{}
60    case SCon{Chr{c}, +t}:
61      Bool.and(Nat.is_le(String.length(t), 2n), Bool.or(Bool.not(U32.is_eq(c, 48)), String.is_empty(t)))
62
63def octet.max(m: Maybe<&2, U32>) -> Maybe<&2, U32>:
64  match m:
65    case None{}:
66      None{}
67    case Some{+v}:
68      Bool.pick(Maybe<&2, U32>, U32.is_le(v, 255), Some{v}, None{})
69
70def octet.ok(ok: Bool, s: String) -> Maybe<&2, U32>:
71  match ok:
72    case True{}:
73      octet.max(dec.go(s, Some{0}))
74    case False{}:
75      None{}
76
77def octet(+s: String) -> Maybe<&2, U32>:
78  octet.ok(octet.lead(s), s)
79
80def v4.parts(ps: List<&2, String>) -> Maybe<&2, U32>:
81  match ps:
82    case Con{a, Con{b, Con{c, Con{d, Nil{}}}}}:
83      do Maybe<&2, U32>:
84        w : U32 <- octet(a)
85        x : U32 <- octet(b)
86        y : U32 <- octet(c)
87        z : U32 <- octet(d)
88        return (w * 16777216 + x * 65536 + y * 256 + z : U32)
89    case _:
90      None{}
91
92# Dotted-decimal IPv4 as its big-endian word.
93def v4.word(s: String) -> Maybe<&2, U32>:
94  v4.parts(String.split(s, '.'))
95
96def v4.wrap(m: Maybe<&2, U32>) -> Maybe<&2, Addr>:
97  match m:
98    case None{}:
99      None{}
100    case Some{w}:
101      Some{V4{w}}
102
103def v4(s: String) -> Maybe<&2, Addr>:
104  v4.wrap(v4.word(s))
105
106# Groups read so far, each list newest first. Gap: "::" was seen; post holds the groups after it.
107type Walk is Data:
108  NoGap{pre: List<&2, U32>}
109  Gap{pre: List<&2, U32>, post: List<&2, U32>}
110
111def walk.push(st: Walk, +g: U32) -> Walk:
112  match st:
113    case NoGap{pre}:
114      NoGap{g <> pre}
115    case Gap{pre, post}:
116      Gap{pre, g <> post}
117
118def v6.hex(w: Walk, m: Maybe<&2, U32>) -> Maybe<&2, Walk>:
119  match m:
120    case None{}:
121      None{}
122    case Some{g}:
123      Some{walk.push(w, g)}
124
125# An empty inner segment is the one "::".
126def v6.gap(w: Walk) -> Maybe<&2, Walk>:
127  match w:
128    case NoGap{pre}:
129      Some{Gap{pre, Nil{}}}
130    case Gap{pre, post}:
131      None{}
132
133def v6.mid.seg(h: String, w: Walk) -> Maybe<&2, Walk>:
134  match h:
135    case SNil{}:
136      v6.gap(w)
137    case SCon{c, t}:
138      v6.hex(w, hextet(SCon{c, t}))
139
140def v6.mid(st: Maybe<&2, Walk>, h: String) -> Maybe<&2, Walk>:
141  match st:
142    case None{}:
143      None{}
144    case Some{w}:
145      v6.mid.seg(h, w)
146
147# An empty last segment is the second colon of a trailing "::".
148def v6.trail(w: Walk) -> Maybe<&2, Walk>:
149  match w:
150    case Gap{pre, Nil{}}:
151      Some{Gap{pre, Nil{}}}
152    case _:
153      None{}
154
155# Embedded dotted IPv4 fills the last two groups.
156def v6.dot(w: Walk, m: Maybe<&2, U32>) -> Maybe<&2, Walk>:
157  match m:
158    case None{}:
159      None{}
160    case Some{+x}:
161      Some{walk.push(walk.push(w, (x / 65536 : U32)), (x % 65536 : U32))}
162
163def v6.last.kind(dot: Bool, w: Walk, s: String) -> Maybe<&2, Walk>:
164  match dot:
165    case True{}:
166      v6.dot(w, v4.word(s))
167    case False{}:
168      v6.hex(w, hextet(s))
169
170def v6.last.text(w: Walk, +s: String) -> Maybe<&2, Walk>:
171  v6.last.kind(String.contains(s, "."), w, s)
172
173def v6.last.seg(h: String, w: Walk) -> Maybe<&2, Walk>:
174  match h:
175    case SNil{}:
176      v6.trail(w)
177    case SCon{c, t}:
178      v6.last.text(w, SCon{c, t})
179
180def v6.last(st: Maybe<&2, Walk>, h: String) -> Maybe<&2, Walk>:
181  match st:
182    case None{}:
183      None{}
184    case Some{w}:
185      v6.last.seg(h, w)
186
187# h: the current segment; t: the segments after it.
188def v6.go(t: List<&2, String>, h: String, st: Maybe<&2, Walk>) -> Maybe<&2, Walk>:
189  match t:
190    case Nil{}:
191      v6.last(st, h)
192    case Con{h2, t2}:
193      v6.go(t2, h2, v6.mid(st, h))
194
195def v6.words(gs: List<&2, U32>) -> Maybe<&2, Addr>:
196  match gs:
197    case Con{a, Con{b, Con{c, Con{d, Con{e, Con{f, Con{g, Con{h, Nil{}}}}}}}}}:
198      Some{V6{(a * 65536 + b : U32), (c * 65536 + d : U32), (e * 65536 + f : U32), (g * 65536 + h : U32)}}
199    case _:
200      None{}
201
202# "::" stands for at least one zero group.
203def v6.pad(ok: Bool, pre: List<&2, U32>, post: List<&2, U32>, n: Nat) -> Maybe<&2, Addr>:
204  match ok:
205    case True{}:
206      v6.words(List.append(&2, U32, List.reverse(&2, U32, pre), List.append(&2, U32, List.replicate(U32, Nat.sub(8n, n), 0), List.reverse(&2, U32, post))))
207    case False{}:
208      None{}
209
210def v6.fill(w: Walk) -> Maybe<&2, Addr>:
211  match w:
212    case NoGap{pre}:
213      v6.words(List.reverse(&2, U32, pre))
214    case Gap{+pre, +post}:
215      +n = (List.length(&2, U32, pre) + List.length(&2, U32, post) : Nat)
216      v6.pad(Nat.is_le(n, 7n), pre, post, n)
217
218def v6.fin(m: Maybe<&2, Walk>) -> Maybe<&2, Addr>:
219  match m:
220    case None{}:
221      None{}
222    case Some{w}:
223      v6.fill(w)
224
225# The ":"-split segments. Only a leading "::" may start with an empty segment.
226def v6(ps: List<&2, String>) -> Maybe<&2, Addr>:
227  match ps:
228    case Con{SNil{}, Con{SNil{}, Con{h, t}}}:
229      v6.fin(v6.go(t, h, Some{Gap{Nil{}, Nil{}}}))
230    case Con{SNil{}, t}:
231      None{}
232    case Con{h, t}:
233      v6.fin(v6.go(t, h, Some{NoGap{Nil{}}}))
234    case Nil{}:
235      None{}
236
237def parse.fam(colon: Bool, s: String) -> Maybe<&2, Addr>:
238  match colon:
239    case True{}:
240      v6(String.split(s, ':'))
241    case False{}:
242      v4(s)
243
244# Strict address text: 4 dotted-decimal octets, or RFC 4291 IPv6 with at most one "::" and an optional
245# trailing dotted IPv4. No brackets, zones, ports, or surrounding space.
246def parse(+s: String) -> Maybe<&2, Addr>:
247  parse.fam(String.contains(s, ":"), s)
248
249# Hex fields contain no leading zeros.
250def hex.char(+n: U32) -> String:
251  SCon{Chr{Bool.pick(U32, U32.is_lt(n, 10), (n + 48 : U32), (n + 87 : U32))}, SNil{}}
252
253def hex.two(+n: U32) -> String:
254  hex.char((n >> 4n : U32)) ++ hex.char((n .&. 15 : U32))
255
256def hex.three(+n: U32) -> String:
257  hex.char((n >> 8n : U32)) ++ hex.two((n .&. 255 : U32))
258
259def hex.four(+n: U32) -> String:
260  hex.char((n >> 12n : U32)) ++ hex.three((n .&. 4095 : U32))
261
262def hex.many(n: U32, small: Bool) -> String:
263  match small:
264    case True{}:
265      hex.three(n)
266    case False{}:
267      hex.four(n)
268
269def hex.more(+n: U32, small: Bool) -> String:
270  match small:
271    case True{}:
272      hex.two(n)
273    case False{}:
274      hex.many(n, U32.is_lt(n, 4096))
275
276def hex.group.small(+n: U32, small: Bool) -> String:
277  match small:
278    case True{}:
279      hex.char(n)
280    case False{}:
281      hex.more(n, U32.is_lt(n, 256))
282
283def hex.group(+n: U32) -> String:
284  hex.group.small(n, U32.is_lt(n, 16))
285
286def groups(+a: U32, +b: U32, +c: U32, +d: U32) -> List<&2, U32>:
287  [(a >> 16n : U32), (a .&. 65535 : U32), (b >> 16n : U32), (b .&. 65535 : U32),
288   (c >> 16n : U32), (c .&. 65535 : U32), (d >> 16n : U32), (d .&. 65535 : U32)]
289
290# Keep the first run when two longest zero runs tie.
291def zeros.best(xs: List<&2, U32>, +i: U32, +run: U32, +start: U32, +best: U32, +length: U32) -> U32 & U32:
292  match xs:
293    case Nil{}:
294      (best, length)
295    case Con{h, t}:
296      +next = Bool.pick(U32, U32.is_zero(h), (run + 1 : U32), 0)
297      +begin = Bool.pick(U32, U32.is_zero(run), i, start)
298      +longer = U32.is_gt(next, length)
299      zeros.best(t, (i + 1 : U32), next, begin, Bool.pick(U32, longer, begin, best),
300        Bool.pick(U32, longer, next, length))
301
302def v6.field.if(inside: Bool, n: U32, +i: U32, start: U32, end: U32) -> String:
303  match inside:
304    case True{}:
305      Bool.pick(String, U32.is_eq(i, start), "::", "")
306    case False{}:
307      Bool.pick(String, Bool.or(U32.is_zero(i), U32.is_eq(i, end)), "", ":") ++ hex.group(n)
308
309def v6.field(n: U32, +i: U32, +start: U32, +length: U32) -> String:
310  +end = (start + length : U32)
311  v6.field.if(Bool.and(U32.is_ge(i, start), U32.is_lt(i, end)), n, i, start, end)
312
313def v6.render(xs: List<&2, U32>, +i: U32, +start: U32, +length: U32) -> String:
314  match xs:
315    case Nil{}:
316      ""
317    case Con{h, t}:
318      v6.field(h, i, start, length) ++ v6.render(t, (i + 1 : U32), start, length)
319
320def v6.show.run(+a: U32, +b: U32, +c: U32, +d: U32, run: U32 & U32) -> String:
321  (+start, +length) = run
322  v6.render(groups(a, b, c, d), 0, Bool.pick(U32, U32.is_ge(length, 2), start, 8),
323    Bool.pick(U32, U32.is_ge(length, 2), length, 0))
324
325def v4.show(+w: U32) -> String:
326  U32.show((w >> 24n : U32)) ++ "." ++ U32.show(((w >> 16n : U32) .&. 255 : U32)) ++ "." ++
327  U32.show(((w >> 8n : U32) .&. 255 : U32)) ++ "." ++ U32.show((w .&. 255 : U32))
328
329def v6.show.mapped(mapped: Bool, +a: U32, +b: U32, +c: U32, +d: U32) -> String:
330  match mapped:
331    case True{}:
332      "::ffff:" ++ v4.show(d)
333    case False{}:
334      v6.show.run(a, b, c, d, zeros.best(groups(a, b, c, d), 0, 0, 0, 0, 0))
335
336# RFC 5952: lowercase, shortest hex groups, longest leftmost "::" run.
337def show(addr: Addr) -> String:
338  match addr:
339    case V4{w}:
340      v4.show(w)
341    case V6{+a, +b, +c, +d}:
342      v6.show.mapped(Bool.and(U32.is_zero(a), Bool.and(U32.is_zero(b), U32.is_eq(c, 65535))), a, b, c, d)
343
344def eq(x: Addr, y: Addr) -> Bool:
345  match x y:
346    case V4{a} V4{b}:
347      U32.is_eq(a, b)
348    case V6{a, b, c, d} V6{e, f, g, h}:
349      Bool.and(U32.is_eq(a, e), Bool.and(U32.is_eq(b, f), Bool.and(U32.is_eq(c, g), U32.is_eq(d, h))))
350    case _ _:
351      False{}
352
353type Prefix is Data:
354  Prefix{addr: Addr, bits: U32}
355
356def prefix.digits(s: String) -> Bool:
357  match s:
358    case SNil{}:
359      True{}
360    case SCon{Chr{+c}, t}:
361      Bool.and(Bool.and(U32.is_le(48, c), U32.is_le(c, 57)), prefix.digits(t))
362
363def prefix.limit(addr: Addr, +bits: U32) -> Maybe<&2, Prefix>:
364  match addr:
365    case V4{w}:
366      Bool.pick(Maybe<&2, Prefix>, U32.is_le(bits, 32), Some{Prefix{V4{w}, bits}}, None{})
367    case V6{a, b, c, d}:
368      Bool.pick(Maybe<&2, Prefix>, U32.is_le(bits, 128), Some{Prefix{V6{a, b, c, d}, bits}}, None{})
369
370def prefix.valid(addr: Addr, bits: U32, valid: Bool) -> Maybe<&2, Prefix>:
371  match valid:
372    case True{}:
373      prefix.limit(addr, bits)
374    case False{}:
375      None{}
376
377def prefix.number(addr: Addr, +text: String, parsed: Maybe<&2, U32>) -> Maybe<&2, Prefix>:
378  match parsed:
379    case None{}:
380      None{}
381    case Some{+bits}:
382      prefix.valid(addr, bits, Bool.and(prefix.digits(text), String.eq(U32.show(bits), text)))
383
384def prefix.addr(text: String, +suffix: String, parsed: Maybe<&2, Addr>) -> Maybe<&2, Prefix>:
385  match parsed:
386    case None{}:
387      None{}
388    case Some{addr}:
389      prefix.number(addr, suffix, U32.read(suffix))
390
391def prefix.parts(parts: List<&2, String>) -> Maybe<&2, Prefix>:
392  match parts:
393    case Con{+addr, Con{suffix, Nil{}}}:
394      prefix.addr(addr, suffix, parse(addr))
395    case _:
396      None{}
397
398def prefix.parse(s: String) -> Maybe<&2, Prefix>:
399  prefix.parts(String.split(s, '/'))
400
401def prefix.show(p: Prefix) -> String:
402  Prefix{addr, bits} = p
403  show(addr) ++ "/" ++ U32.show(bits)
404
405def mask(bits: U32) -> U32:
406  U32.not(U32.shrn(4294967295, U32.to_nat(U32.min(bits, 32))))
407
408def leading(+bits: U32, +offset: U32) -> U32:
409  Bool.pick(U32, U32.is_ge(bits, offset), U32.min((bits - offset : U32), 32), 0)
410
411def word.contains(+a: U32, +b: U32, bits: U32) -> Bool:
412  +m = mask(bits)
413  U32.is_eq((a .&. m : U32), (b .&. m : U32))
414
415# Address and prefix families must match. The supplied prefix address keeps its host bits.
416def contains(p: Prefix, addr: Addr) -> Bool:
417  match p addr:
418    case Prefix{V4{a}, +bits} V4{b}:
419      Bool.and(U32.is_le(bits, 32), word.contains(a, b, bits))
420    case Prefix{V6{a, b, c, d}, +bits} V6{e, f, g, h}:
421      Bool.and(U32.is_le(bits, 128), Bool.and(word.contains(a, e, leading(bits, 0)),
422        Bool.and(word.contains(b, f, leading(bits, 32)),
423          Bool.and(word.contains(c, g, leading(bits, 64)), word.contains(d, h, leading(bits, 96))))))
424    case _ _:
425      False{}