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.parseFlatVec? (dim : ℕ) (j : Lean.Json) (ctx : String := "alpha[i]") : IO (Option (MLTheory.CROWN.Graph.FlatVec Float))

Parse a flat vector from JSON, accepting null as an absent optional vector.

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.

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.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.