4.4. Soundness and Completeness🔗

The parser is characterized by the same guarantees as the other verified extension parsers. The specification is independent of the parser: IsWfIPNet describes the accepted grammar, while v4Value and v6Value give the value of witnessing components. The proof connects those definitions to the hand-written parser, including IPv4's precedence over IPv6.

Soundness: whenever parsing succeeds, the input is well-formed and the returned IPNet is the value of either witnessing IPv4 or IPv6 components.

theorem

Cedar.Thm.IPAddr.parse_sound (str : String)
  (net : Cedar.Spec.Ext.IPAddr.IPNet)
  (h : Cedar.Spec.Ext.IPAddr.ip str = some net) :
  IsWfIPNet str ∧
    ((∃ v pre, net = v4Value v pre) ∨ ∃ v pre, net = v6Value v pre)
Cedar.Thm.IPAddr.parse_sound
  (str : String)
  (net : Cedar.Spec.Ext.IPAddr.IPNet)
  (h :
    Cedar.Spec.Ext.IPAddr.ip str =
      some net) :
  IsWfIPNet str ∧
    ((∃ v pre, net = v4Value v pre) ∨
      ∃ v pre, net = v6Value v pre)

Soundness of IPAddr.ip: if parsing succeeds, the input is a well-formed IP-net string, and the returned net is the value of its witnessing components.

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 well-formed IP-net string is accepted.

theorem

Cedar.Thm.IPAddr.parse_complete (str : String) (h : IsWfIPNet str) :
  (Cedar.Spec.Ext.IPAddr.ip str).isSome = true
Cedar.Thm.IPAddr.parse_complete
  (str : String) (h : IsWfIPNet str) :
  (Cedar.Spec.Ext.IPAddr.ip str).isSome =
    true

Completeness of IPAddr.ip: every well-formed IP-net string is accepted (with the value of its witnessing components).

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.)