Cel.Format recognizer laws, and audit the last generated example

The conformance battery is finitely many labelled points; these are properties
that hold for every input. The load-bearing one is ipv4Value?_lt — the value an
accepted IPv4 address denotes really is below 2^32, which is exactly what
isIpPrefix's host-bit masking (v % 2 ^ (32 - len)) assumes. The rest pin
documented shape claims (four dotted parts, the 253-character hostname bound,
the port range, and that only versions 0/4/6 are ever accepted) so they cannot
drift out of the implementation unnoticed.

//lean:format_laws_assurance audits their axiom closures.
//examples/common:money_valid_assurance closes the last generated example
without one: shipping consumes Money through valid_deps, so its theorems are
now audited at their source too.

The URI, email and IPv6 grammars carry no laws; the README says so.

Author: petersonbill64

README.md

@@ -96,15 +96,17 @@ which downstream code can project and rewrite along without re-running any
 checks. `Test/PredSchemeTest.lean` keeps a hand-written mirror of the emission
 scheme compiling.
 
-Three `lean_assurance_test` targets audit axiom closures at compile time (no
+Five `lean_assurance_test` targets audit axiom closures at compile time (no
 `sorryAx`, standard axioms only), covering both the instances and the scheme
-they instantiate:
+they instantiate. Every generated example in the repo is audited:
 
 | target | principal theorems |
 |---|---|
 | `//lean:runtime_assurance` | the generic `Decision` lemmas (`pred_of_toExcept_ok`, `toExcept_isOk`, `decodeThenValidate_sound`), the presence plumbing, `size_mapArray` — plus a scan of the whole `Protovalidate.Cel`/`Runtime` surface the generated propositions are stated over |
+| `//lean:format_laws_assurance` | the `Cel.Format` recognizer laws (see [format assurance](#format-assurance-what-the-battery-does-and-does-not-say)), headed by `ipv4Value?_lt` |
 | `//examples/shipping:shipping_valid_assurance` | `shipping.v1.Valid.{Order,Item}` (soundness, completeness, decode) and the validated `Order.payer_Type` sum |
 | `//examples/shipping:inventory_valid_assurance` | `catalog.v1.Valid.{Product,Payment}` and the `Payment.method_Type` sum (standard rules, enums, element rules, validated oneof) |
+| `//examples/common:money_valid_assurance` | `common.v1.Valid.Money` — the cross-target embed, audited at its source |
 
 A repeated-message field's own rules are stated over the *validated* array
 (`Protovalidate.mapArray b.f Elem.ofPred h.f_elems`), because those rules may
@@ -513,14 +515,26 @@ checking in URI hosts. All are fixed; the corpus is what keeps them fixed.
   `well_known_regex`) are rejected at generation time, so they have no
   corpus rows.
 
+**Proved, not sampled.** `Cel.Format`'s recognizer laws
+(`lean/Protovalidate/Cel/FormatLaws.lean`, audited by
+`//lean:format_laws_assurance`) carry the complementary kind of evidence —
+properties holding for *every* input rather than for corpus points. The
+load-bearing one is `ipv4Value?_lt`: the value an accepted IPv4 address denotes
+really is below `2 ^ 32`, which is exactly what `isIpPrefix`'s host-bit masking
+(`v % 2 ^ (32 - len)`) assumes. The others pin documented shape claims
+(`ipv4Value?_length`, `isHostname_length`, `isPort_le`, `isIp_version` — only
+versions 0/4/6 are ever accepted). The URI, email and IPv6 grammars carry no
+such laws; they rest on the corpus alone.
+
 ## Layout
 
 ```
 celtolean/            Go library: CEL AST → Lean expression (golden tests)
 cmd/cel2lean/         CLI: single expression, -json, -batch corpus→Lean
 cmd/protoc-gen-lean-protovalidate/  protoc plugin entry point
 leanvalidate/         plugin codegen: descriptors + buf.validate rules → Lean
-lean/Protovalidate/   Lean runtime (modules Protovalidate.Cel, .Runtime)
+lean/Protovalidate/   Lean runtime (modules Protovalidate.Cel, .Runtime) plus
+                      Cel/FormatLaws.lean (recognizer theorems, not runtime)
 protovalidate/        Starlark API: lean_protovalidate_library (defs.bzl)
 Test/                 corpus TSV + genrule compiling every translation with
                       Decidable assertions (build_test) + stand-in msg types.
@@ -569,6 +583,7 @@ non-generated, option-only proto dependencies such as
    per-pattern differential batteries (see
    [regex assurance](#regex-assurance-what-the-guards-do-and-do-not-say)), nor
    between `Cel.Format`'s grammars and their RFCs beyond the conformance
-   battery (see
+   battery and the IPv4/hostname/port recognizer laws (see
    [format assurance](#format-assurance-what-the-battery-does-and-does-not-say)).
-   Both corpora are vendored snapshots of upstream references.
+   Both corpora are vendored snapshots of upstream references; the URI, email
+   and IPv6 grammars carry no laws yet.

examples/common/BUILD.bazel

@@ -3,6 +3,7 @@
 consumed by //examples/shipping via proto_deps/valid_deps."""
 
 load("@protobuf//bazel:proto_library.bzl", "proto_library")
+load("@rules_lean//lean:defs.bzl", "lean_assurance_test")
 load("@rules_lean_grpc//:defs.bzl", "lean_proto_library")
 load("//protovalidate:defs.bzl", "lean_protovalidate_library")
 
@@ -24,3 +25,16 @@ lean_protovalidate_library(
     lean_proto = ":money_lean",
     proto = ":money_proto",
 )
+
+# The last generated example without an axiom audit: the target //examples/
+# shipping consumes through valid_deps, so the cross-target embed's theorems
+# are audited at their source too.
+lean_assurance_test(
+    name = "money_valid_assurance",
+    principal_theorems = [
+        "common.v1.Valid.Money.validate_sound",
+        "common.v1.Valid.Money.validate_complete",
+        "common.v1.Valid.Money.decodeValid_sound",
+    ],
+    deps = [":money_valid"],
+)

lean/BUILD.bazel

@@ -34,6 +34,16 @@ lean_library(
     strip_module_prefix = "lean",
 )
 
+# Recognizer laws for Cel.Format: properties that hold for every input, as
+# opposed to the conformance battery's finitely many labelled points. Not part
+# of the runtime library — nothing generated depends on them.
+lean_library(
+    name = "protovalidate_format_laws",
+    srcs = ["Protovalidate/Cel/FormatLaws.lean"],
+    strip_module_prefix = "lean",
+    deps = [":protovalidate_cel"],
+)
+
 # Compile-time audit of the proof scheme itself. Every generated
 # validate_sound / validate_complete / decodeValid_sound is a one-line instance
 # of a lemma below, so this is the root of trust the per-message audits stand
@@ -62,3 +72,20 @@ lean_assurance_test(
         ":protovalidate_runtime",
     ],
 )
+
+# The Cel.Format recognizer laws must be theorems closing over no axiom beyond
+# the standard three. `ipv4Value?_lt` is the load-bearing one: isIpPrefix's
+# host-bit masking assumes exactly it.
+lean_assurance_test(
+    name = "format_laws_assurance",
+    principal_theorems = [
+        "Cel.Format.ipv4Value?_lt",
+        "Cel.Format.ipv4Octet?_le_255",
+        "Cel.Format.ipv4Value?_length",
+        "Cel.Format.isIpv4_splitOn_length",
+        "Cel.Format.isHostname_length",
+        "Cel.Format.isPort_le",
+        "Cel.Format.isIp_version",
+    ],
+    deps = [":protovalidate_format_laws"],
+)

lean/Protovalidate/Cel/FormatLaws.lean

@@ -0,0 +1,116 @@
+module
+
+public import Protovalidate.Cel.Format
+import all Protovalidate.Cel.Format
+
+/-!
+Kernel-checked recognizer laws for `Protovalidate.Cel.Format`.
+
+The formats are trusted code: what ties them to protovalidate is the
+conformance battery (`//Test:format_corpus_test`), which is differential
+testing over a finite corpus. These theorems are the complementary kind of
+evidence — properties that hold for *every* input, proved once.
+
+They cover the tractable formats. The headline is `ipv4Value?_lt`: the value an
+accepted IPv4 address denotes really is a 32-bit number, which is what
+`isIpPrefix`'s host-bit masking (`v % 2 ^ (32 - len)`) silently assumes. The
+rest pin down documented shape claims (four dotted parts, the 253-character
+hostname bound, the port range, the accepted IP versions) so they cannot drift
+out of the implementation unnoticed.
+
+Not covered: the URI grammar, the email grammar, and IPv6 — each would need
+substantially more machinery, and none has a comparable arithmetic assumption
+riding on it.
+-/
+
+@[expose] public section
+
+namespace Cel.Format
+
+/-! ## IPv4 -/
+
+/-- An octet is at most 255 — the strictness `ipv4Octet?`'s final guard states. -/
+theorem ipv4Octet?_le_255 {p : String} {v : Nat} (h : ipv4Octet? p = some v) : v ≤ 255 := by
+  simp only [ipv4Octet?] at h
+  repeat' first | split at h | cases h
+  omega
+
+/-- Accumulating octets base-256 keeps the running value under `256 ^ n`
+(stated with the accumulator general so it inducts). -/
+theorem ipv4Fold_bound (l : List String) : ∀ (acc v : Nat),
+    l.foldlM (fun acc p => (ipv4Octet? p).map (acc * 256 + ·)) acc = some v →
+    v + 1 ≤ (acc + 1) * 256 ^ l.length := by
+  induction l with
+  | nil =>
+    intro acc v h
+    simp only [List.foldlM] at h
+    simp only [pure] at h
+    injection h with h
+    subst h
+    simp
+  | cons p rest ih =>
+    intro acc v h
+    simp only [List.foldlM] at h
+    cases ho : ipv4Octet? p with
+    | none => rw [ho] at h; simp at h
+    | some o =>
+      rw [ho] at h
+      simp only [Option.map_some] at h
+      simp only [bind, Option.bind] at h
+      have hb := ih _ _ h
+      have h255 := ipv4Octet?_le_255 ho
+      calc v + 1 ≤ (acc * 256 + o + 1) * 256 ^ rest.length := hb
+        _ ≤ (acc + 1) * 256 * 256 ^ rest.length := Nat.mul_le_mul_right _ (by omega)
+        _ = (acc + 1) * 256 ^ (rest.length + 1) := by rw [Nat.pow_succ]; ac_rfl
+
+/-- An address that parses has exactly four dot-separated parts. -/
+theorem ipv4Value?_length {s : String} {v : Nat} (h : ipv4Value? s = some v) :
+    (s.splitOn ".").length = 4 := by
+  simp only [ipv4Value?] at h
+  split at h
+  · exact absurd h (by simp)
+  · rename_i hlen
+    simp only [bne_iff_ne, ne_eq, Decidable.not_not] at hlen
+    exact hlen
+
+/-- **The value an accepted IPv4 address denotes is a 32-bit number.** This is
+what `isIpPrefix` assumes when it masks host bits with `v % 2 ^ (32 - len)`. -/
+theorem ipv4Value?_lt {s : String} {v : Nat} (h : ipv4Value? s = some v) : v < 2 ^ 32 := by
+  have hlen := ipv4Value?_length h
+  simp only [ipv4Value?] at h
+  split at h
+  · exact absurd h (by simp)
+  · have hb := ipv4Fold_bound _ 0 v h
+    rw [hlen] at hb
+    have h256 : (0 + 1) * (256 : Nat) ^ 4 = 2 ^ 32 := by decide
+    omega
+
+theorem isIpv4_splitOn_length {s : String} (h : isIpv4 s = true) :
+    (s.splitOn ".").length = 4 := by
+  simp only [isIpv4, Option.isSome_iff_exists] at h
+  obtain ⟨v, hv⟩ := h
+  exact ipv4Value?_length hv
+
+/-! ## Hostnames, ports, versions -/
+
+/-- The documented 253-character bound really is enforced (trailing dot
+included, as protovalidate counts it). -/
+theorem isHostname_length {s : String} (h : isHostname s = true) : s.length ≤ 253 := by
+  simp only [isHostname, Bool.and_eq_true, decide_eq_true_eq] at h
+  exact h.1
+
+/-- An accepted port denotes a number in the 16-bit range. -/
+theorem isPort_le {s : String} (h : isPort s = true) :
+    s.toList.foldl (fun acc c => acc * 10 + (c.toNat - 48)) 0 ≤ 65535 := by
+  simp only [isPort, Bool.and_eq_true, decide_eq_true_eq] at h
+  exact h.2
+
+/-- Only versions 0, 4 and 6 are ever accepted: `isIp(s, 5)` is false for every
+`s`, matching protovalidate (whose conformance suite tests exactly that). -/
+theorem isIp_version {s : String} {version : Int} (h : isIp s version = true) :
+    version = 0 ∨ version = 4 ∨ version = 6 := by
+  simp only [isIp] at h
+  repeat' first | split at h | cases h
+  all_goals simp_all
+
+end Cel.Format