IPAddr parser correctness #

parse_sound, parse_complete, and parse_eq_none_iff characterize exactly when Cedar.Spec.Ext.IPAddr.ip (a.k.a. ip) succeeds, in terms of the grammar-level IsWfIPNet predicate and declarative IsIPNetValue relation. Its two branches use v4Value and v6Value to give the denotation of the same components that witness the input rendering. The parser-independent bridge lemmas they build on live in Cedar.Thm.Ext.IPAddr.Lemmas.

Well-formedness and valuation #

source

theorem Cedar.Thm.IPAddr.wf_iff_exists_value {str : String} :

IsWfIPNet str ↔ ∃ (net : Spec.Ext.IPAddr.IPNet ), IsIPNetValue str net

Well-formed IP-net syntax is exactly syntax to which the grammar assigns some IPNet.

Soundness #

source

theorem Cedar.Thm.IPAddr.parse_sound (str : String) (net : Spec.Ext.IPAddr.IPNet) (h : Spec.Ext.IPAddr.ip str = some net) :

IsIPNetValue str net

Soundness of IPAddr.ip: if parsing succeeds, the declarative grammar relation assigns the input exactly the returned IPNet.

Completeness #

source

theorem Cedar.Thm.IPAddr.parse_complete_v4 {v : V4Components} {pre : Option String} (hsyn : v.syntaxWf) (hcon : v.constraintsWf) (hpre : IsWfOptionalPrefix 2 (Spec.Ext.IPAddr.ADDR_SIZE Spec.Ext.IPAddr.V4_WIDTH) pre) :

Spec.Ext.IPAddr.ip (v.asString ++ match pre, hpre with | none, hpre => "" | some p, hpre => "/" ++ p) = some (v4Value v pre)

Completeness for the V4 form: a well-formed V4 string parses to its v4Value.

source

theorem Cedar.Thm.IPAddr.parse_complete_v6 {v : V6Components} {pre : Option String} (hsyn : v.syntaxWf) (hpre : IsWfOptionalPrefix 3 (Spec.Ext.IPAddr.ADDR_SIZE Spec.Ext.IPAddr.V6_WIDTH) pre) :

Spec.Ext.IPAddr.ip (v.asString ++ match pre, hpre with | none, hpre => "" | some p, hpre => "/" ++ p) = some (v6Value v pre)

Completeness for the V6 form: a well-formed V6 string parses to its v6Value.

source

theorem Cedar.Thm.IPAddr.parse_complete (str : String) (net : Spec.Ext.IPAddr.IPNet) (h : IsIPNetValue str net) :

Spec.Ext.IPAddr.ip str = some net

Completeness of IPAddr.ip: if the grammar assigns str the value net, parsing returns that exact IPNet.

source

theorem Cedar.Thm.IPAddr.parse_eq_some_iff_isIPNetValue (str : String) (net : Spec.Ext.IPAddr.IPNet) :

Spec.Ext.IPAddr.ip str = some net ↔ IsIPNetValue str net

Exact parser characterization: parsing succeeds with net precisely when the declarative grammar relation assigns the input that IPNet.

source

theorem Cedar.Thm.IPAddr.isIPNetValue_unique {str : String} {net₁ net₂ : Spec.Ext.IPAddr.IPNet} (h₁ : IsIPNetValue str net₁) (h₂ : IsIPNetValue str net₂) :

net₁ = net₂

The relational value specification is single-valued: an IP-net string denotes at most one IPNet.

Failure characterization #

source

theorem Cedar.Thm.IPAddr.parse_eq_none_iff (str : String) :

Spec.Ext.IPAddr.ip str = none ↔ ¬IsWfIPNet str

Failure characterization: IPAddr.ip rejects exactly the strings that are not well-formed IP-nets. (There is no overflow condition — the grammar's field bounds already exclude out-of-range values.)

Roundtrip #

source

theorem Cedar.Thm.IPAddr.parse_toString_roundtrip (net : Spec.Ext.IPAddr.IPNet) :

Spec.Ext.IPAddr.ip (toString net) = some net

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

source

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

net = net'

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

source

theorem Cedar.Thm.IPAddr.normalize_eq_iff_parse_eq (str str' : String) :

normalize str = normalize str' ↔ Spec.Ext.IPAddr.ip str = Spec.Ext.IPAddr.ip str'

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