Node-Certificate Replay #
Parsing, exact comparison, and local replay 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 operations here so the individual checkers can focus on their propagation rule:
IBPNodeCertchecks interval propagation;CROWNNodeCertchecks affine CROWN propagation;CROWNNodeCertAlphaBetachecks 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. Interval claims are checked by outward containment, while affine replay transcripts must match the executable binary32 result exactly.
Bitwise equality for shape-indexed binary32 tensors.
Instances For
A successful bitwise tensor comparison proves equality at every rank.
Whether outer contains inner componentwise.
This deliberately has no tolerance. A lower endpoint may be rounded farther down and an upper endpoint farther up, but a serialized certificate may never move either endpoint inward. This is the relation used for interval claims.
Instances For
Bitwise equality for affine vectors, componentwise on matrix A and offset c.
Instances For
A successful bitwise affine-vector comparison proves equality of both affine components.
Bitwise equality for flattened affine lower/upper bounds.
Instances For
A successful bitwise affine-bound comparison proves equality of the dependent records, including their input and output dimensions.
Bitwise equality for optional affine bounds, used by the pure replay checker.
Instances For
Successful optional comparison proves equality of the optional affine bounds.
Proved local replay #
The diagnostic node checkers below replay bounds incrementally so that they can report the first
bad node. The final acceptance decision also runs this pure check against the complete imported
certificate. Its soundness theorem supplies exactly the CrownCertLocalOK hypothesis expected by
the graph-level CROWN theorem.
Check that every affine entry is exactly the result of applying step to the imported certificate.
This is intentionally narrower than the complete certificate checker: parsing, IBP containment,
shape checks, and domain checks remain separate executable obligations. This predicate is the
local-replay component whose proposition-level meaning is CrownCertLocalOK.
Instances For
Successful pure replay constructs the local-consistency hypothesis used by CROWN soundness.
Combine the diagnostic checks with pure local replay. Acceptance of the combined decision always supplies the proposition-level local CROWN consistency condition.
Instances For
The complete Boolean acceptance decision implies local CROWN consistency.
Parse a flat interval box (two arrays of floats) from JSON.
Instances For
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.
Instances For
Parse flattened affine bounds (lower/upper) from JSON.
Instances For
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.
Affine-propagation context, including the chosen input node and flattened input dimension.
- ibp : 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) exactEqTensor._proof_1 exactEqTensor._proof_2 exactEqTensor._proof_3 exactEqTensor._proof_4)))
Optional per-node interval bounds used by nonlinear CROWN steps.
- crown : Array (Option (MLTheory.CROWN.Graph.FlatAffineBounds (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) exactEqTensor._proof_1 exactEqTensor._proof_2 exactEqTensor._proof_3 exactEqTensor._proof_4)))
Optional per-node affine lower/upper bounds.
- alpha : Array (Option (MLTheory.CROWN.Graph.FlatTensor (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) exactEqTensor._proof_1 exactEqTensor._proof_2 exactEqTensor._proof_3 exactEqTensor._proof_4)))
Optional per-node α values for ReLU lower relaxations.
Instances For
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.
Instances For
Check that an optional per-node certificate array contains all parents of node id.
Instances For
Safe lookup for optional flat boxes used by certificate-side shape checks.
Instances For
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.
Instances For
Check whether a flat box is entirely inside the positive domain needed by true log.
Instances For
Check that every coordinate interval lies strictly on one side of zero.
Instances For
Domain and shape preconditions that must hold before a node-wise certificate checker replays a bound step. These executable checks mirror the side conditions that the mathematical rules need.
Instances For
Pretty-printer for a flat box, used in certificate mismatch messages.
Instances For
Pretty-printer for affine bounds, used in certificate mismatch messages.
Instances For
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, exact binary32 transcript equality, and diagnostic messages.