1	# IPv4 and IPv6 address values: strict parsing, RFC 5952 text, and CIDR prefixes. Source: https://github.com/paymog/bend-kit/tree/main/netip
2	import Base
3	
4	# V4: the address as one big-endian word. V6: four network-order words, a first.
5	type 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.
10	def 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	
15	def 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	
22	def 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	
29	def 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.
37	def 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.
41	def 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	
48	def 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".
56	def 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	
63	def 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	
70	def 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	
77	def octet(+s: String) -> Maybe<&2, U32>:
78	  octet.ok(octet.lead(s), s)
79	
80	def 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.
93	def v4.word(s: String) -> Maybe<&2, U32>:
94	  v4.parts(String.split(s, '.'))
95	
96	def 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	
103	def 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.
107	type Walk is Data:
108	  NoGap{pre: List<&2, U32>}
109	  Gap{pre: List<&2, U32>, post: List<&2, U32>}
110	
111	def 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	
118	def 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 "::".
126	def 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	
133	def 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	
140	def 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 "::".
148	def 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.
156	def 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	
163	def 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	
170	def v6.last.text(w: Walk, +s: String) -> Maybe<&2, Walk>:
171	  v6.last.kind(String.contains(s, "."), w, s)
172	
173	def 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	
180	def 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.
188	def 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	
195	def 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.
203	def 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	
210	def 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	
218	def 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.
226	def 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	
237	def 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.
246	def parse(+s: String) -> Maybe<&2, Addr>:
247	  parse.fam(String.contains(s, ":"), s)
248	
249	# Hex fields contain no leading zeros.
250	def hex.char(+n: U32) -> String:
251	  SCon{Chr{Bool.pick(U32, U32.is_lt(n, 10), (n + 48 : U32), (n + 87 : U32))}, SNil{}}
252	
253	def hex.two(+n: U32) -> String:
254	  hex.char((n >> 4n : U32)) ++ hex.char((n .&. 15 : U32))
255	
256	def hex.three(+n: U32) -> String:
257	  hex.char((n >> 8n : U32)) ++ hex.two((n .&. 255 : U32))
258	
259	def hex.four(+n: U32) -> String:
260	  hex.char((n >> 12n : U32)) ++ hex.three((n .&. 4095 : U32))
261	
262	def 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	
269	def 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	
276	def 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	
283	def hex.group(+n: U32) -> String:
284	  hex.group.small(n, U32.is_lt(n, 16))
285	
286	def 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.
291	def 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	
302	def 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	
309	def 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	
313	def 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	
320	def 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	
325	def 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	
329	def 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.
337	def 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	
344	def 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	
353	type Prefix is Data:
354	  Prefix{addr: Addr, bits: U32}
355	
356	def 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	
363	def 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	
370	def 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	
377	def 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	
384	def 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	
391	def 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	
398	def prefix.parse(s: String) -> Maybe<&2, Prefix>:
399	  prefix.parts(String.split(s, '/'))
400	
401	def prefix.show(p: Prefix) -> String:
402	  Prefix{addr, bits} = p
403	  show(addr) ++ "/" ++ U32.show(bits)
404	
405	def mask(bits: U32) -> U32:
406	  U32.not(U32.shrn(4294967295, U32.to_nat(U32.min(bits, 32))))
407	
408	def leading(+bits: U32, +offset: U32) -> U32:
409	  Bool.pick(U32, U32.is_ge(bits, offset), U32.min((bits - offset : U32), 32), 0)
410	
411	def 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.
416	def 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{}