4.3. Parser
IPAddr.ip (a.k.a. parse) returns some net when the input string is valid, and none otherwise. It tries the IPv4 grammar first, falling through to IPv6 (shown here directly from source in Cedar.Spec.Ext.IPAddr):
private def parse (str : String) : Option IPNet :=
let ip := parseIPv4Net str
if ip.isSome then ip else parseIPv6Net str
The IPv4 path splits off an optional '/' prefix, then parses four '.'-separated decimal groups; each group parser parseNumV4 enforces the length, leading-zero, and ≤ 255 rules:
private def parseNumV4 (str : String) : Option (BitVec 8) :=
let len := str.length
if 0 < len && len ≤ 3 && (str.startsWith "0" → str = "0")
then do
let n ← toNat?' str
if n ≤ 0xff then .some n else .none
else .none
The IPv6 path handles :: compression by splitting on "::": with no :: the address must be
exactly eight ':'-separated groups; with one :: the two sides are padded with zero groups to
reach eight (and are rejected if they already total eight):
private def parseSegsV6 (str : String) : Option IPv6Addr := do
let segs ←
match splitDoubleColon str with
| [s₁] => parseNumSegsV6 s₁
| [s₁, s₂] => do
let ns₁ ← parseNumSegsV6 s₁
let ns₂ ← parseNumSegsV6 s₂
let len := ns₁.length + ns₂.length
if len < 8
then .some (ns₁ ++ (List.replicate (8 - len) 0) ++ ns₂)
else .none
| _ => .none
match segs with
| [a₀, a₁, a₂, a₃, a₄, a₅, a₆, a₇] =>
.some (IPv6Addr.mk a₀ a₁ a₂ a₃ a₄ a₅ a₆ a₇)
| _ => .noneFor example:
#eval (ip "192.168.0.1/32").map toString -- valid V4 with prefix
#eval (ip "F:AE::F:5:F:F:0").map toString -- valid V6 with `::`
#eval ip "256.0.0.1" -- octet out of range
#eval ip "::ffff:127.0.0.1" -- no embedded IPv4