4.2. Formal Specification🔗

As with Decimal and Duration, the public specification separates productions, well-formedness, component denotation, and a relational value statement. V4Production and V6Production relate renderings to their components, IsWfIPNet hides those components existentially, v4Value and v6Value give their denotation, and IsIPNetValue str net ties each production to its IPNet.

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 :=
  natOf v.g₀ ≤ 255 ∧ natOf v.g₁ ≤ 255 ∧ natOf v.g₂ ≤ 255 ∧ natOf 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 ∧ natOf p ≤ size

The family productions combine address components with an optional CIDR prefix and the complete rendering:

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

public def V6Production (str : String) (v : V6Components) (pre : Option String) : Prop :=
  v.syntaxWf ∧
  IsWfOptionalPrefix 3 (ADDR_SIZE V6_WIDTH) pre ∧
  str = v.asString ++ (match pre with | none => "" | some p => "/" ++ p)

Well-formedness existentially hides those witnesses:

public def IsWfV4 (str : String) : Prop :=
  ∃ (v : V4Components) (pre : Option String), V4Production str v pre

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

The family-specific value functions construct an IPNet from already identified address and prefix components:

public def v4Value (v : V4Components) (pre : Option String) : IPNet :=
  IPNet.V4 ⟨v.toAddr, prefixValue V4_WIDTH pre⟩

public def v6Value (v : V6Components) (pre : Option String) : IPNet :=
  IPNet.V6 ⟨v.toAddr, prefixValue V6_WIDTH pre⟩

IsV4Value and IsV6Value extend the corresponding syntax witnesses with their denotation; IsIPNetValue combines the two productions:

public def IsV4Value (str : String) (net : IPNet) : Prop :=
  ∃ (v : V4Components) (pre : Option String),
    V4Production str v pre ∧
    net = v4Value v pre

public def IsV6Value (str : String) (net : IPNet) : Prop :=
  ∃ (v : V6Components) (pre : Option String),
    V6Production str v pre ∧
    net = v6Value v pre

public def IsIPNetValue (str : String) (net : IPNet) : Prop :=
  IsV4Value str net ∨ IsV6Value str net

The syntax and value views agree: an input is well-formed exactly when it denotes some IPNet.

theorem

Cedar.Thm.IPAddr.wf_iff_exists_value {str : String} :
  IsWfIPNet str ↔ ∃ net, IsIPNetValue str net
Cedar.Thm.IPAddr.wf_iff_exists_value
  {str : String} :
  IsWfIPNet str ↔
    ∃ net, IsIPNetValue str net

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

The relation is also single-valued, including across the V4/V6 alternatives.

theorem

Cedar.Thm.IPAddr.isIPNetValue_unique {str : String}
  {net₁ net₂ : Cedar.Spec.Ext.IPAddr.IPNet} (h₁ : IsIPNetValue str net₁)
  (h₂ : IsIPNetValue str net₂) : net₁ = net₂
Cedar.Thm.IPAddr.isIPNetValue_unique
  {str : String}
  {net₁ net₂ :
    Cedar.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.