IPAddr grammar: definitions

This file contains only the grammar-level definitions: the well-formedness predicates, component value functions, and relational value specification. IsWfIPNet states the syntax, v4Value/v6Value give the denotation of identified components, and IsIPNetValue str net combines those same witnesses to say that str denotes net. The lemmas connecting these definitions to IPAddr.parse live in Cedar.Thm.Ext.IPAddr.Lemmas.

The accepted syntax (transcribed from the spec parser) is, informally:

IPNet    ::= V4Net | V6Net          -- V4 tried first; a string is V6 only if it is not V4
V4Net    ::= V4Addr ['/' V4Prefix]
V4Addr   ::= NumV4 '.' NumV4 '.' NumV4 '.' NumV4
NumV4    ::= Digit{1,3}             -- no leading zeros unless the group is exactly "0"; value ≤ 255
V4Prefix ::= Digit{1,2}            -- no leading zeros unless exactly "0"; value ≤ 32

V6Net    ::= V6Addr ['/' V6Prefix]
V6Addr   ::= a `::`-compressed sequence of hextets that expands to exactly 8 groups
NumV6    ::= HexDigit{1,4}          -- value ≤ 0xffff (automatic from ≤ 4 hex digits)
V6Prefix ::= Digit{1,3}            -- no leading zeros unless exactly "0"; value ≤ 128

The :: compression may appear at most once and denotes a run of zero hextets that pads the total to 8 groups.

Shared digit/number-token predicates

def Cedar.Thm.IPAddr.IsCanonicalNat (s : String) : Prop

A Digit⁺ string that additionally forbids a leading zero unless it is exactly "0" — the "no leading zeros" rule the spec parser enforces on every numeric group and prefix (str.startsWith "0" → str = "0").

Equations

• Cedar.Thm.IPAddr.IsCanonicalNat s = (s.IsDigits ∧ (s.startsWith "0" = true → s = "0"))

IPv4 grammar

V4Addr is four dot-separated groups, each a canonical 1–3 digit number ≤ 255; the optional prefix is a canonical 1–2 digit number ≤ 32.

structure Cedar.Thm.IPAddr.V4Components : Type

The grammar's V4Addr ::= NumV4 '.' NumV4 '.' NumV4 '.' NumV4: four decimal groups.

• g₀ : String
• g₁ : String
• g₂ : String
• g₃ : String

def Cedar.Thm.IPAddr.V4Components.syntaxWf (v : V4Components) : Prop

Each group is a canonical number of at most 3 digits.

Equations

• One or more equations did not get rendered due to their size.

def Cedar.Thm.IPAddr.V4Components.constraintsWf (v : V4Components) : Prop

Each group's value is at most 255 (0xff).

Equations

• v.constraintsWf = (v.g₀.natOf ≤ 255 ∧ v.g₁.natOf ≤ 255 ∧ v.g₂.natOf ≤ 255 ∧ v.g₃.natOf ≤ 255)

def Cedar.Thm.IPAddr.V4Components.asString (v : V4Components) : String

Render a V4Addr as g₀ '.' g₁ '.' g₂ '.' g₃.

Equations

• v.asString = v.g₀ ++ "." ++ v.g₁ ++ "." ++ v.g₂ ++ "." ++ v.g₃

def Cedar.Thm.IPAddr.V4Components.toAddr (v : V4Components) : Spec.Ext.IPAddr.IPv4Addr

The IPv4Addr value of well-formed V4 groups.

Equations

• v.toAddr = Cedar.Spec.Ext.IPAddr.IPv4Addr.mk ↑v.g₀.natOf ↑v.g₁.natOf ↑v.g₂.natOf ↑v.g₃.natOf

IPv6 grammar

V6Addr is a ::-compressed sequence of hextets. Rather than model the compression syntactically here, a V6Components record holds the eight expanded hextets together with the rendering (the concrete ::-form string), and well-formedness is phrased existentially over that rendering (as in the duration/datetime grammars). Each hextet is a 1–4 character hex-digit string.

def Cedar.Thm.IPAddr.IsHexGroup (s : String) : Prop

A Digit⁺-style predicate for hex groups: a non-empty string all of whose characters are hex digits, of length at most 4.

Equations

• Cedar.Thm.IPAddr.IsHexGroup s = (0 < s.length ∧ s.length ≤ 4 ∧ ∀ (c : Char), c ∈ s.toList → Cedar.Spec.Ext.IPAddr.isHexDigit✝ c = true)

def Cedar.Thm.IPAddr.hexValue (s : String) : Nat

Numeric value of a hex group (Σ digit · 16ⁱ), matching the spec parser's foldl.

Equations

• Cedar.Thm.IPAddr.hexValue s = String.foldl (fun (n : Nat) (c : Char) => n * 16 + Cedar.Spec.Ext.IPAddr.toHexNat✝ c) 0 s

inductive Cedar.Thm.IPAddr.V6Components : Type

A V6 address, as the spec parser accepts it: either a full list of hextets with no :: compression, or a ::-compressed form with a left and right list of hextets and an implicit run of zero hextets between them. This mirrors parseSegsV6's splitOn "::":

• full gs ↔ the string has no ::; gs is the ':'-separated hextet list;
• gap l r ↔ the string is l₀:…:lₘ '::' r₀:…:rₙ; the gap expands to 8 − (|l|+|r|) zero hextets.

• full (gs : List String) : V6Components
• gap (l r : List String) : V6Components

def Cedar.Thm.IPAddr.V6Components.expand : V6Components → List String

The eight expanded hextet strings a V6Components denotes: the full list itself, or the two sides padded with the appropriate number of "0" hextets between them.

Equations

• (Cedar.Thm.IPAddr.V6Components.full gs).expand = gs
• (Cedar.Thm.IPAddr.V6Components.gap l r).expand = l ++ List.replicate (8 - (l.length + r.length)) "0" ++ r

def Cedar.Thm.IPAddr.V6Components.syntaxWf : V6Components → Prop

Syntactic well-formedness of a V6 address:

• every present hextet is a valid 1–4 digit hex group;
• the full form has exactly 8 hextets (no :: ⇒ splitToList ':' must give 8);
• the gap form's two sides total strictly fewer than 8 (so the :: denotes ≥ 1 zero hextet — parseSegsV6 requires len < 8).

Equations

• (Cedar.Thm.IPAddr.V6Components.full gs).syntaxWf = (gs.length = 8 ∧ ∀ (s : String), s ∈ gs → Cedar.Thm.IPAddr.IsHexGroup s)
• (Cedar.Thm.IPAddr.V6Components.gap l r).syntaxWf = (l.length + r.length < 8 ∧ (∀ (s : String), s ∈ l → Cedar.Thm.IPAddr.IsHexGroup s) ∧ ∀ (s : String), s ∈ r → Cedar.Thm.IPAddr.IsHexGroup s)

def Cedar.Thm.IPAddr.V6Components.asString : V6Components → String

Render a V6 address to its concrete string: hextets joined by ':', with "::" at the gap. (intercalate ":" matches the parser's splitToList (· = ':') / splitOn "::" inverse.)

Equations

• (Cedar.Thm.IPAddr.V6Components.full gs).asString = ":".intercalate gs
• (Cedar.Thm.IPAddr.V6Components.gap l r).asString = ":".intercalate l ++ "::" ++ ":".intercalate r

def Cedar.Thm.IPAddr.V6Components.toAddr (v : V6Components) : Spec.Ext.IPAddr.IPv6Addr

The IPv6Addr value: the eight expanded hextets' hex values. Well-formedness guarantees expand has length 8; on other lengths this defaults the missing groups to 0.

Equations

• One or more equations did not get rendered due to their size.

Prefix grammar

An optional CIDR suffix '/' Prefix, where Prefix is a canonical decimal number bounded by the address width (≤ 32 for V4, ≤ 128 for V6). Absence of the suffix denotes the full-width prefix (ADDR_SIZE).

def Cedar.Thm.IPAddr.IsWfOptionalPrefix (digits size : Nat) : Option String → Prop

The optional prefix, with its digit-count and value bounds (digits, size) ((2, 32) for V4, (3, 128) for V6). none is the implicit full-width prefix.

Equations

• Cedar.Thm.IPAddr.IsWfOptionalPrefix digits size none = True
• Cedar.Thm.IPAddr.IsWfOptionalPrefix digits size (some p) = (Cedar.Thm.IPAddr.IsCanonicalNat p ∧ p.length ≤ digits ∧ p.natOf ≤ size)

def Cedar.Thm.IPAddr.prefixValue (w : Nat) : Option String → Spec.Ext.IPAddr.IPNetPrefix w

The IPNetPrefix value of an optional prefix string: none maps to the full-width prefix.

Equations

• Cedar.Thm.IPAddr.prefixValue w none = Cedar.Spec.Ext.IPAddr.IPNetPrefix.ofNat✝ w (Cedar.Spec.Ext.IPAddr.ADDR_SIZE w)
• Cedar.Thm.IPAddr.prefixValue w (some p) = Cedar.Spec.Ext.IPAddr.IPNetPrefix.ofNat✝ w p.natOf

Top-level well-formedness

An IP-net string is well-formed when it is either a well-formed V4 rendering or a well-formed V6 rendering (with V4 taking precedence, mirroring the parser's if ipv4.isSome then … else …). Both are phrased existentially over the components' asString rendering (as in the duration/datetime grammars), baking the separators, group count, and ::-compression rules into the witness.

def Cedar.Thm.IPAddr.V4Production (str : String) (v : V4Components) (pre : Option String) : Prop

The IPv4 grammar production witnessed by address components and an optional CIDR prefix.

Equations

• One or more equations did not get rendered due to their size.

def Cedar.Thm.IPAddr.IsWfV4 (str : String) : Prop

A well-formed IPv4-net string has a valid IPv4 grammar production.

Equations

• Cedar.Thm.IPAddr.IsWfV4 str = ∃ (v : Cedar.Thm.IPAddr.V4Components), ∃ (pre : Option String), Cedar.Thm.IPAddr.V4Production str v pre

def Cedar.Thm.IPAddr.V6Production (str : String) (v : V6Components) (pre : Option String) : Prop

The IPv6 grammar production witnessed by address components and an optional CIDR prefix.

Equations

• One or more equations did not get rendered due to their size.

def Cedar.Thm.IPAddr.IsWfV6 (str : String) : Prop

A well-formed IPv6-net string has a valid IPv6 grammar production.

Equations

• Cedar.Thm.IPAddr.IsWfV6 str = ∃ (v : Cedar.Thm.IPAddr.V6Components), ∃ (pre : Option String), Cedar.Thm.IPAddr.V6Production str v pre

def Cedar.Thm.IPAddr.IsWfIPNet (str : String) : Prop

A string is a well-formed IP-net iff it is a well-formed V4 or V6 net. Because the parser tries V4 first and only falls through to V6 when V4 fails, and the two grammars are disjoint on their accepted strings, this disjunction faithfully characterizes acceptance.

Equations

• Cedar.Thm.IPAddr.IsWfIPNet str = (Cedar.Thm.IPAddr.IsWfV4 str ∨ Cedar.Thm.IPAddr.IsWfV6 str)

Value relation

The component value functions are independent of the parser. The relational definitions below tie those values to the same witnesses used by the syntax predicates, so no second string decoder is needed.

def Cedar.Thm.IPAddr.v4Value (v : V4Components) (pre : Option String) : Spec.Ext.IPAddr.IPNet

The IPNet value of a well-formed V4 string's components.

Equations

• Cedar.Thm.IPAddr.v4Value v pre = Cedar.Spec.Ext.IPAddr.IPNet.V4 { addr := v.toAddr, pre := Cedar.Thm.IPAddr.prefixValue Cedar.Spec.Ext.IPAddr.V4_WIDTH pre }

def Cedar.Thm.IPAddr.v6Value (v : V6Components) (pre : Option String) : Spec.Ext.IPAddr.IPNet

The IPNet value of a well-formed V6 string's components.

Equations

• Cedar.Thm.IPAddr.v6Value v pre = Cedar.Spec.Ext.IPAddr.IPNet.V6 { addr := v.toAddr, pre := Cedar.Thm.IPAddr.prefixValue Cedar.Spec.Ext.IPAddr.V6_WIDTH pre }

def Cedar.Thm.IPAddr.IsV4Value (str : String) (net : Spec.Ext.IPAddr.IPNet) : Prop

net is the value of a well-formed IPv4-net rendering.

Equations

• Cedar.Thm.IPAddr.IsV4Value str net = ∃ (v : Cedar.Thm.IPAddr.V4Components), ∃ (pre : Option String), Cedar.Thm.IPAddr.V4Production str v pre ∧ net = Cedar.Thm.IPAddr.v4Value v pre

def Cedar.Thm.IPAddr.IsV6Value (str : String) (net : Spec.Ext.IPAddr.IPNet) : Prop

net is the value of a well-formed IPv6-net rendering.

Equations

• Cedar.Thm.IPAddr.IsV6Value str net = ∃ (v : Cedar.Thm.IPAddr.V6Components), ∃ (pre : Option String), Cedar.Thm.IPAddr.V6Production str v pre ∧ net = Cedar.Thm.IPAddr.v6Value v pre

def Cedar.Thm.IPAddr.IsIPNetValue (str : String) (net : Spec.Ext.IPAddr.IPNet) : Prop

net is the value of the IP-net literal str, through either the V4 or V6 production.

Equations

• Cedar.Thm.IPAddr.IsIPNetValue str net = (Cedar.Thm.IPAddr.IsV4Value str net ∨ Cedar.Thm.IPAddr.IsV6Value str net)

def Cedar.Thm.IPAddr.normalize (str : String) : Option String

Canonical-form normalizer: parse the string and re-serialize. Returns none for malformed inputs.

Equations

• Cedar.Thm.IPAddr.normalize str = Option.map toString (Cedar.Spec.Ext.IPAddr.ip str)