CROWNNodeCert

Per-node α-CROWN certificate checking (graph dialect).

This mirrors NN.Verification.IBPNodeCert, but for affine bounds produced by a CROWN/DeepPoly pass with optional α-parameters for the ReLU lower relaxation (α-CROWN).

Certificate JSON format:

{
  "ctx": { "inputId": 0, "inputDim": 2 },
  "ibp": [ null | { "lo": [...], "hi": [...] }, ... ],
  "crown": [
    null |
      {
        "loA": [[...], ...], "loC": [...],
        "hiA": [[...], ...], "hiC": [...]
      },
    ...
  ],
  "alpha": [ null | [...], ... ] // optional per-node ReLU α vector
}

Trust boundary notes:

• The certificate is untrusted; we accept it only if Lean recomputation matches (within a float tolerance due to JSON decimal serialization).
• Transcendental relaxations are checked only via structural recomputation, not via a formal "libm is correct" guarantee.

The helpers below are the JSON-facing boundary for the CROWN certificate checkers. They parse the artifact, compare decimal-serialized floats with an explicit tolerance, and check parent/shape requirements before invoking the semantic checker.

@[reducible, inline]

abbrev NN.Verification.CROWNNodeCert.CROWNNodeCertificate : Type

In-memory representation of a node-wise α-CROWN certificate read from JSON.

def NN.Verification.CROWNNodeCert.readCROWNNodeCertificate (g : MLTheory.CROWN.Graph) (path : String) : IO CROWNNodeCertificate

Read a CROWN node certificate from JSON on disk.

def NN.Verification.CROWNNodeCert.checkCROWNNode (g : MLTheory.CROWN.Graph) (ps : MLTheory.CROWN.Graph.ParamStore Float) (certIbp : Array (Option (MLTheory.CROWN.FlatBox Float))) (certAlpha : Array (Option (MLTheory.CROWN.Graph.FlatVec Float))) (certCrown : Array (Option (MLTheory.CROWN.Graph.FlatAffineBounds Float))) (ctx : MLTheory.CROWN.Graph.AffineCtx) (id : ℕ) (tol : Float) : IO Bool

Check the local CROWN enclosure condition for one node against a certificate entry.

def NN.Verification.CROWNNodeCert.checkCROWNNodeCertificate (g : MLTheory.CROWN.Graph) (ps : MLTheory.CROWN.Graph.ParamStore Float) (path : String) (tol : Float := 1e-4) : IO Bool

Check a per-node α-CROWN certificate against Lean's propagation rules.

Returns true iff every node's certificate affine bounds agree (within tol) with what Lean computes from the certificate parents + ParamStore.