CROWNNodeCert #

Per-node α-CROWN certificate checking (graph dialect), with optional ReLU phases.

This mirrors NN.Verification.Cert.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
  "phases": [ null | [-1,0,1,...], ... ]  // optional per-node ReLU phases
}

A phase is -1 (inactive, $z\leq0$), 0 (unconstrained) or 1 (active, $0\leq z$), and it is accepted only when the IBP pre-activation interval already proves it. Phases therefore carry no information beyond IBP: with none given the replay is plain α-CROWN, and with phases it is α-CROWN with those ReLUs fixed. No β multipliers or branch splits run.

Trust boundary notes:

The certificate is untrusted; we accept it only if its binary32 affine transcript exactly matches Lean recomputation.
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, require exact binary32 agreement for affine replay data, and check parent and shape requirements. Acceptance proves local replay consistency, not a real-input enclosure on its own.

source

def NN.Verification.Cert.CROWNNodeCert.read (g : MLTheory.CROWN.Graph) (path : String) :

IO NodeReplay.CROWNCertificate

Read a CROWN node certificate from JSON on disk.

Instances For

source

IO Bool

The per-node part of the check. Every supplied IBP box must contain Lean's authoritative interval, and every node's affine entry must equal the bound step replays from the nodes before it; label names the checker in its messages. The result is the diagnosticsOk input of accepts.

check passes replayStep, the function whose acceptance theorem is proved below, so this loop and the pure acceptance decision replay the same rule.

Instances For

source

def NN.Verification.Cert.CROWNNodeCert.replayStep (g : MLTheory.CROWN.Graph) (ps : MLTheory.CROWN.Graph.ParamStore (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) checkNodeEntries._proof_1 checkNodeEntries._proof_2 checkNodeEntries._proof_3 checkNodeEntries._proof_4)) (authoritativeIbp : Array (Option (MLTheory.CROWN.FlatBox (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) checkNodeEntries._proof_1 checkNodeEntries._proof_2 checkNodeEntries._proof_3 checkNodeEntries._proof_4)))) (cert : NodeReplay.CROWNCertificate) :

The replay of a parsed certificate: α-CROWN, with the certificate's ReLU phases if any.

Instances For

source

def NN.Verification.Cert.CROWNNodeCert.accepts (cert : NodeReplay.CROWNCertificate) (g : MLTheory.CROWN.Graph) (ps : MLTheory.CROWN.Graph.ParamStore (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) checkNodeEntries._proof_1 checkNodeEntries._proof_2 checkNodeEntries._proof_3 checkNodeEntries._proof_4)) (authoritativeIbp : Array (Option (MLTheory.CROWN.FlatBox (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) checkNodeEntries._proof_1 checkNodeEntries._proof_2 checkNodeEntries._proof_3 checkNodeEntries._proof_4)))) (diagnosticsOk : Bool) :

Bool

The final in-memory acceptance decision.

diagnosticsOk records parsing-independent IBP, shape, domain, and incremental-replay checks. The second conjunct establishes local replay consistency. Semantic enclosure additionally requires coverage of the relevant graph nodes and proved transfer rules for their operations.

Instances For

source

theorem NN.Verification.Cert.CROWNNodeCert.accepts_eq_true (cert : NodeReplay.CROWNCertificate) (g : MLTheory.CROWN.Graph) (ps : MLTheory.CROWN.Graph.ParamStore (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) checkNodeEntries._proof_1 checkNodeEntries._proof_2 checkNodeEntries._proof_3 checkNodeEntries._proof_4)) (authoritativeIbp : Array (Option (MLTheory.CROWN.FlatBox (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) checkNodeEntries._proof_1 checkNodeEntries._proof_2 checkNodeEntries._proof_3 checkNodeEntries._proof_4)))) (diagnosticsOk : Bool) (haccept : accepts cert g ps authoritativeIbp diagnosticsOk = true) :

MLTheory.CROWN.Graph.CrownCertSoundness.CrownCertLocalOK g (replayStep g ps authoritativeIbp cert) cert.crown

Acceptance supplies graph-level local consistency of the replay.

source

def NN.Verification.Cert.CROWNNodeCert.check (g : MLTheory.CROWN.Graph) (ps : MLTheory.CROWN.Graph.ParamStore (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) checkNodeEntries._proof_1 checkNodeEntries._proof_2 checkNodeEntries._proof_3 checkNodeEntries._proof_4)) (path : String) :

IO Bool

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

Returns true iff every supplied IBP box contains Lean's authoritative recomputation and every node's affine replay data agrees exactly with Lean's step.

The per-node loop is part of the verdict: it checks IBP containment, parent coverage, shape and domain preconditions, and dimensions, which the pure replay in accepts does not. The pure replay runs only when the loop passes. The certificate's ibp boxes are only checked for containment; replay uses Lean's own IBP pass, so they add no information to the affine check.

Instances For