Common Certificate Helpers

Shared JSON/parsing and approximate-comparison utilities for node-wise verification certificates.

The IBP, α-CROWN, and α/β-CROWN checkers all consume the same basic artifact shapes: flat interval boxes, affine lower/upper bounds, and optional per-node vectors. We keep those format-level helpers here so the individual checkers can focus on their propagation rule:

• IBPNodeCert checks interval propagation;
• CROWNNodeCert checks affine CROWN propagation;
• CROWNNodeCertAlphaBeta checks affine CROWN propagation with β phase information.

The JSON artifact is always untrusted. These helpers only parse and compare data; acceptance still requires each checker to recompute the corresponding bound inside Lean. The float tolerances here exist because JSON stores decimal strings/numbers, not because the external producer is trusted.

def NN.Verification.Cert.Common.approxEqTensor {n : ℕ} (t u : Spec.Tensor Float (Spec.Shape.dim n Spec.Shape.scalar)) (tol : Float) : Bool

Approximate equality for flat scalar tensors (length-n vectors), up to an absolute tolerance.

This is used when comparing Lean-recomputed bounds to decimal-serialized JSON certificate values.

def NN.Verification.Cert.Common.approxEqMatrix {m n : ℕ} (A B : Spec.Tensor Float (Spec.Shape.dim m (Spec.Shape.dim n Spec.Shape.scalar))) (tol : Float) : Bool

Approximate equality for flat matrices (shape m × n), up to an absolute tolerance.

def NN.Verification.Cert.Common.approxEqFlatBox (B1 B2 : MLTheory.CROWN.FlatBox Float) (tol : Float) : Bool

Approximate equality for FlatBox bounds, componentwise on lo and hi.

def NN.Verification.Cert.Common.approxEqAffineVec {n m : ℕ} (a b : MLTheory.CROWN.AffineVec Float n m) (tol : Float) : Bool

Approximate equality for affine vectors, componentwise on matrix A and offset c.

def NN.Verification.Cert.Common.approxEqFlatAffineBounds (B1 B2 : MLTheory.CROWN.Graph.FlatAffineBounds Float) (tol : Float) : Bool

Approximate equality for flattened affine lower/upper bounds.

def NN.Verification.Cert.Common.parseFlatBox? (dim : ℕ) (j : Lean.Json) : IO (Option (MLTheory.CROWN.FlatBox Float))

Parse a flat interval box (two arrays of floats) from JSON.

def NN.Verification.Cert.Common.parseAlphaVec? (dim : ℕ) (j : Lean.Json) (ctx : String := "alpha[i]") : IO (Option (MLTheory.CROWN.Graph.FlatVec Float))

Parse an optional α vector for α-CROWN ReLU relaxations.

The soundness theorem for the lower ReLU relaxation assumes every α component is in [0, 1]. We enforce that contract at the JSON boundary, so a malformed external certificate cannot be accepted by executable checking while relying on proof hypotheses that are false.

def NN.Verification.Cert.Common.parseAffineBounds? (inDim outDim : ℕ) (j : Lean.Json) : IO (Option (MLTheory.CROWN.Graph.FlatAffineBounds Float))

Parse flattened affine bounds (lower/upper) from JSON.

structure NN.Verification.Cert.Common.CROWNNodeCoreCertificate : Type

Shared in-memory representation for node-wise CROWN-style certificates.

Plain α-CROWN uses these fields directly. α/β-CROWN extends the same core artifact with a β phase array, so parsing the common fields here keeps the two checkers from drifting apart.

• ctx : MLTheory.CROWN.Graph.AffineCtx

  Affine-propagation context, including the chosen input node and flattened input dimension.

• ibp : Array (Option (MLTheory.CROWN.FlatBox Float))

  Optional per-node interval bounds used by nonlinear CROWN steps.

• crown : Array (Option (MLTheory.CROWN.Graph.FlatAffineBounds Float))

  Optional per-node affine lower/upper bounds.

• alpha : Array (Option (MLTheory.CROWN.Graph.FlatVec Float))

  Optional per-node α values for ReLU lower relaxations.

def NN.Verification.Cert.Common.parseCROWNNodeCoreCertificate (g : MLTheory.CROWN.Graph) (topObj : Lean.Json) : IO CROWNNodeCoreCertificate

Parse the fields shared by α-CROWN and α/β-CROWN node certificates.

The producer may omit "alpha"; in that case we treat every node as having no custom α vector. Whenever α is present, parseAlphaVec? enforces the [0,1] side condition required by the ReLU relaxation proof.

def NN.Verification.Cert.Common.parentsOk {β : Type} (g : MLTheory.CROWN.Graph) (cert : Array (Option β)) (id : ℕ) : Bool

Check that an optional per-node certificate array contains all parents of node id.

def NN.Verification.Cert.Common.getFlatBox? (cert : Array (Option (MLTheory.CROWN.FlatBox Float))) (id : ℕ) : Option (MLTheory.CROWN.FlatBox Float)

Safe lookup for optional flat boxes used by certificate-side shape checks.

def NN.Verification.Cert.Common.binaryElementwiseBoxesMatchOutput (g : MLTheory.CROWN.Graph) (cert : Array (Option (MLTheory.CROWN.FlatBox Float))) (id : ℕ) : Bool

Check that binary elementwise parent boxes have the same flattened size as each other and as the node output. This closes the hole where a malformed certificate could make the runtime helper use the left box on a dimension mismatch.

def NN.Verification.Cert.Common.flatBoxStrictlyAbove (B : MLTheory.CROWN.FlatBox Float) (eps : Float) : Bool

Check whether a flat box is entirely inside the positive domain needed by true log.

def NN.Verification.Cert.Common.ibpNodePreconditionsOk (g : MLTheory.CROWN.Graph) (cert : Array (Option (MLTheory.CROWN.FlatBox Float))) (id : ℕ) : Bool

Domain and shape preconditions that must hold before a node-wise certificate checker replays a bound step. These are not proof shortcuts; they are the executable version of the side conditions that the mathematical rules need.

def NN.Verification.Cert.Common.prettyFlatBox (B : MLTheory.CROWN.FlatBox Float) : String

Pretty-printer for a flat box, used in certificate mismatch messages.

def NN.Verification.Cert.Common.prettyAffineBounds (B : MLTheory.CROWN.Graph.FlatAffineBounds Float) : String

Pretty-printer for affine bounds, used in certificate mismatch messages.

def NN.Verification.Cert.Common.checkCROWNLikeNode (label : String) (g : MLTheory.CROWN.Graph) (certIbp : Array (Option (MLTheory.CROWN.FlatBox Float))) (certCrown : Array (Option (MLTheory.CROWN.Graph.FlatAffineBounds Float))) (ctx : MLTheory.CROWN.Graph.AffineCtx) (id : ℕ) (tol : Float) (computed? : Option (MLTheory.CROWN.Graph.FlatAffineBounds Float)) : IO Bool

Common node-level checker for CROWN-style affine certificates.

The only difference between α-CROWN and α/β-CROWN is how the candidate affine bound is recomputed. Everything after that point is the same: parent availability, IBP side conditions, dimensions, approximate JSON equality, and diagnostic messages.