Verified Cedar Extension Parsers in Lean 4

4.6. Roundtrip Theorem🔗

Parsing the canonical string representation of any IPNet recovers the original value. This is the headline user-facing property: IPAddr.ip and toString are mutually inverse on IP-net values, and it is what underpins toString_injective above.

🔗theorem
Cedar.Thm.IPAddr.parse_toString_roundtrip
  (net : Cedar.Spec.Ext.IPAddr.IPNet) :
  Cedar.Spec.Ext.IPAddr.ip (toString net) = some net
Cedar.Thm.IPAddr.parse_toString_roundtrip
  (net : Cedar.Spec.Ext.IPAddr.IPNet) :
  Cedar.Spec.Ext.IPAddr.ip
      (toString net) =
    some net

parse ∘ toString roundtrip: parsing the canonical representation recovers the original IP-net.

The proof constructs well-formed canonical IPv4 or IPv6 components from the stored address and prefix, applies completeness, and shows that the packed BitVec address and prefix are recovered exactly.

All theorems above are machine-checked, contain no proof placeholders, and rely only on the three standard axioms (propext, Classical.choice, Quot.sound).