4.5. Canonical String Representation🔗

toString converts an IPNet back to a canonical string: an IPv4 net prints its four decimal octets and prefix; an IPv6 net prints all eight groups as four-digit lowercase hextets (no :: elision) and prefix.

"0001:0002:0003:0004:000a:000b:000c:000d/128"#eval toString ((ip "1:2:3:4:a:b:c:d/128").get!)

"0001:0002:0003:0004:000a:000b:000c:000d/128"

normalize composes parsing and serialization: it accepts any valid IP-net string and returns its canonical form.

def

Cedar.Thm.IPAddr.normalize (str : String) : Option String
Cedar.Thm.IPAddr.normalize
  (str : String) : Option String

Canonical-form normalizer: parse the string and re-serialize. Returns none for malformed inputs.

theorem

Cedar.Thm.IPAddr.toString_injective
  (net net' : Cedar.Spec.Ext.IPAddr.IPNet)
  (h : toString net = toString net') : net = net'
Cedar.Thm.IPAddr.toString_injective
  (net net' : Cedar.Spec.Ext.IPAddr.IPNet)
  (h : toString net = toString net') :
  net = net'

toString is injective: distinct IP-nets produce distinct canonical strings.

theorem

Cedar.Thm.IPAddr.normalize_eq_iff_parse_eq (str str' : String) :
  normalize str = normalize str' ↔
    Cedar.Spec.Ext.IPAddr.ip str = Cedar.Spec.Ext.IPAddr.ip str'
Cedar.Thm.IPAddr.normalize_eq_iff_parse_eq
  (str str' : String) :
  normalize str = normalize str' ↔
    Cedar.Spec.Ext.IPAddr.ip str =
      Cedar.Spec.Ext.IPAddr.ip str'

Equal normal form iff equal value: normalization decides IP-net equality.