4.4. Soundness and Completeness🔗

The parser is characterized by the same guarantees as the other verified extension parsers. The proof connects IsIPNetValue to the hand-written parser, including IPv4's precedence over IPv6.

Soundness: whenever parsing succeeds, the grammar relation assigns the input exactly the returned IPNet. By wf_iff_exists_value, this also certifies well-formedness.

theorem

Cedar.Thm.IPAddr.parse_sound (str : String)
  (net : Cedar.Spec.Ext.IPAddr.IPNet)
  (h : Cedar.Spec.Ext.IPAddr.ip str = some net) : IsIPNetValue str net
Cedar.Thm.IPAddr.parse_sound
  (str : String)
  (net : Cedar.Spec.Ext.IPAddr.IPNet)
  (h :
    Cedar.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 is exact for each address family: well-formed IPv4 and IPv6 renderings parse to their component values.

theorem

Cedar.Thm.IPAddr.parse_complete_v4 {v : V4Components}
  {pre : Option String} (hsyn : v.syntaxWf) (hcon : v.constraintsWf)
  (hpre :
    IsWfOptionalPrefix 2
      (Cedar.Spec.Ext.IPAddr.ADDR_SIZE Cedar.Spec.Ext.IPAddr.V4_WIDTH)
      pre) :
  Cedar.Spec.Ext.IPAddr.ip
      (v.asString ++
        match pre, hpre with
        | none, hpre => ""
        | some p, hpre => "/" ++ p) =
    some (v4Value v pre)
Cedar.Thm.IPAddr.parse_complete_v4
  {v : V4Components} {pre : Option String}
  (hsyn : v.syntaxWf)
  (hcon : v.constraintsWf)
  (hpre :
    IsWfOptionalPrefix 2
      (Cedar.Spec.Ext.IPAddr.ADDR_SIZE
        Cedar.Spec.Ext.IPAddr.V4_WIDTH)
      pre) :
  Cedar.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.

theorem

Cedar.Thm.IPAddr.parse_complete_v6 {v : V6Components}
  {pre : Option String} (hsyn : v.syntaxWf)
  (hpre :
    IsWfOptionalPrefix 3
      (Cedar.Spec.Ext.IPAddr.ADDR_SIZE Cedar.Spec.Ext.IPAddr.V6_WIDTH)
      pre) :
  Cedar.Spec.Ext.IPAddr.ip
      (v.asString ++
        match pre, hpre with
        | none, hpre => ""
        | some p, hpre => "/" ++ p) =
    some (v6Value v pre)
Cedar.Thm.IPAddr.parse_complete_v6
  {v : V6Components} {pre : Option String}
  (hsyn : v.syntaxWf)
  (hpre :
    IsWfOptionalPrefix 3
      (Cedar.Spec.Ext.IPAddr.ADDR_SIZE
        Cedar.Spec.Ext.IPAddr.V6_WIDTH)
      pre) :
  Cedar.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.

The family-independent form states that every relational value witness is accepted as that exact IPNet.

theorem

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

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

Together, soundness and completeness give a direct parser characterization:

theorem

Cedar.Thm.IPAddr.parse_eq_some_iff_isIPNetValue (str : String)
  (net : Cedar.Spec.Ext.IPAddr.IPNet) :
  Cedar.Spec.Ext.IPAddr.ip str = some net ↔ IsIPNetValue str net
Cedar.Thm.IPAddr.parse_eq_some_iff_isIPNetValue
  (str : String)
  (net : Cedar.Spec.Ext.IPAddr.IPNet) :
  Cedar.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.

Together, soundness and completeness characterize failure completely. There is no separate overflow case: the octet, hextet, and prefix bounds are already part of the grammar.

theorem

Cedar.Thm.IPAddr.parse_eq_none_iff (str : String) :
  Cedar.Spec.Ext.IPAddr.ip str = none ↔ ¬IsWfIPNet str
Cedar.Thm.IPAddr.parse_eq_none_iff
  (str : String) :
  Cedar.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.)