IPAddr grammar bridge lemmas

These lemmas connect the parser-independent grammar definitions in Cedar.Thm.Ext.IPAddr.Grammar (IsWfIPNet, IsIPNetValue, and the component value functions) to the actual Cedar.Spec.Ext.IPAddr.parse. They culminate in the per-form parse characterizations the aggregator parse_sound/parse_complete build on.

The parser structure (from Cedar.Spec.Ext.IPAddr) is:

• parse str = if (parseIPv4Net str).isSome then parseIPv4Net str else parseIPv6Net str;
• parseIPv4Net splits on '/', parses four parseNumV4 groups (split on '.') and an optional parsePrefixNat prefix;
• parseIPv6Net splits on '/', parses the address via parseSegsV6 (which handles :: via splitOn "::" and pads to eight hextets) and an optional parsePrefixNat prefix.

Each numeric primitive (parseNumV4, parseNumV6, parsePrefixNat) enforces the length / leading-zero / range side conditions that the grammar predicates transcribe.

Numeric-token bridges

IPv4 form

IPv6 form

Specialized model of String.splitOn "::"

def Cedar.Thm.IPAddr.splitDoubleColonModel (str : String) : List String

The proof-layer model of String.splitOn "::".

Equations

• Cedar.Thm.IPAddr.splitDoubleColonModel str = Cedar.Thm.IPAddr.splitDoubleColonModelAux✝ [] str.toList

theorem Cedar.Thm.IPAddr.splitOn_doubleColon_eq (s : String) : s.splitOn "::" = splitDoubleColonModel s

String.splitOn "::" agrees with the proof-layer character-list model on every string.

theorem Cedar.Thm.IPAddr.isWfV4_iff_exists_value {str : String} : IsWfV4 str ↔ ∃ (net : Spec.Ext.IPAddr.IPNet), IsV4Value str net

Well-formed IPv4 syntax is exactly syntax to which the grammar assigns some V4 value.

theorem Cedar.Thm.IPAddr.isWfV6_iff_exists_value {str : String} : IsWfV6 str ↔ ∃ (net : Spec.Ext.IPAddr.IPNet), IsV6Value str net

Well-formed IPv6 syntax is exactly syntax to which the grammar assigns some V6 value.

Canonical-rendering lemmas