4.2. Formal Specification🔗

We formalize the validity of an input string by the predicate IsWfIPNet (well-formed syntax of the grammar) and the value functions v4Value/v6Value (the IPNet a well-formed string denotes). Unlike the decimal grammar, whose value is a single Int, an IP-net's value is an IPNet, so soundness and completeness are phrased per witnessing components rather than through a single computeValue.

The building block for numeric groups is IsCanonicalNat, which captures a non-empty digit string with the grammar's "no leading zeros" rule (str.startsWith "0" → str = "0"), building on the shared IsDigits predicate:

public def IsCanonicalNat (s : String) : Prop :=
  IsDigits s ∧ (s.startsWith "0" → s = "0")

An IPv4 address is four decimal groups; syntaxWf pins each group to a canonical Digit{1,3} string and constraintsWf bounds each value by 255:

public def V4Components.syntaxWf (v : V4Components) : Prop :=
  (IsCanonicalNat v.g₀ ∧ v.g₀.length ≤ 3) ∧
  (IsCanonicalNat v.g₁ ∧ v.g₁.length ≤ 3) ∧
  (IsCanonicalNat v.g₂ ∧ v.g₂.length ≤ 3) ∧
  (IsCanonicalNat v.g₃ ∧ v.g₃.length ≤ 3)

public def V4Components.constraintsWf (v : V4Components) : Prop :=
  numValue v.g₀ ≤ 255 ∧ numValue v.g₁ ≤ 255 ∧ numValue v.g₂ ≤ 255 ∧ numValue v.g₃ ≤ 255

An IPv6 address is modelled on the grammar's :: structure — either a full list of eight groups, or a gap form whose two sides straddle the :: and whose total is strictly fewer than eight groups (the gap expanding to the missing zero groups). This mirrors how the parser (next section) splits on "::":

public inductive V6Components where
  | full (gs : List String)
  | gap  (l r : List String)

public def V6Components.syntaxWf : V6Components → Prop
  | .full gs => gs.length = 8 ∧ ∀ s ∈ gs, IsHexGroup s
  | .gap l r => l.length + r.length < 8 ∧ (∀ s ∈ l, IsHexGroup s) ∧ (∀ s ∈ r, IsHexGroup s)

The optional CIDR prefix is a canonical decimal number bounded by the address width, with absence denoting the full-width prefix:

public def IsWfOptionalPrefix (digits size : Nat) : Option String → Prop
  | none        => True
  | some p      => IsCanonicalNat p ∧ p.length ≤ digits ∧ numValue p ≤ size

Well-formedness of the whole string then reads off the grammar — a well-formed V4 rendering or a well-formed V6 rendering, each phrased existentially over the components' asString (which bakes in the separators, group count, and ::-placement):

public def IsWfV4 (str : String) : Prop :=
  ∃ (v : V4Components) (pre : Option String),
    v.syntaxWf ∧ v.constraintsWf ∧
    IsWfOptionalPrefix 2 (ADDR_SIZE V4_WIDTH) pre ∧
    str = v.asString ++ (match pre with | none => "" | some p => "/" ++ p)

public def IsWfIPNet (str : String) : Prop :=
  IsWfV4 str ∨ IsWfV6 str