Node-Certificate Replay

Parsing, exact comparison, and local replay for node-wise verification certificates.

The IBP and CROWN checkers 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 each checker can focus on its propagation rule:

• IBPNodeCert checks interval propagation;
• CROWNNodeCert checks affine α-CROWN propagation, with optional ReLU phases.

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 containment after rounding each decimal endpoint outward into binary32, while affine replay transcripts must match the executable binary32 result exactly after rounding each decimal coefficient to nearest.

def NN.Verification.Cert.NodeReplay.finiteVec (n : ℕ) (v : Fin n → Float) : Bool

Whether every entry of a fixed-size vector is finite.

def NN.Verification.Cert.NodeReplay.finiteMatrix (rows cols : ℕ) (A : Fin rows → Fin cols → Float) : Bool

Whether every entry of a fixed-size matrix is finite.

def NN.Verification.Cert.NodeReplay.exactEqTensor {s : Spec.Shape} : TorchLean.Tensor (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) s → TorchLean.Tensor (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) s → Bool

Bitwise equality for shape-indexed binary32 tensors.

theorem NN.Verification.Cert.NodeReplay.exactEqTensor_eq_true {s : Spec.Shape} {t u : TorchLean.Tensor (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) s} (h : exactEqTensor t u = true) : t = u

A successful bitwise tensor comparison proves equality at every rank.

def NN.Verification.Cert.NodeReplay.flatBoxContains (outer inner : 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)) : Bool

Whether outer contains inner componentwise.

This deliberately has no tolerance after decimal decoding. The decoded lower endpoint may be farther down and the upper endpoint farther up, but neither may lie inward of the recomputed box.

def NN.Verification.Cert.NodeReplay.exactEqAffineVec {n m : ℕ} (a b : MLTheory.CROWN.AffineVec (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) n m) : Bool

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

theorem NN.Verification.Cert.NodeReplay.exactEqAffineVec_eq_true {n m : ℕ} {a b : MLTheory.CROWN.AffineVec (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) n m} (h : exactEqAffineVec a b = true) : a = b

A successful bitwise affine-vector comparison proves equality of both affine components.

def NN.Verification.Cert.NodeReplay.exactEqFlatAffineBounds (B1 B2 : 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)) : Bool

Bitwise equality for flattened affine lower/upper bounds.

theorem NN.Verification.Cert.NodeReplay.exactEqFlatAffineBounds_eq_true {B1 B2 : 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)} (h : exactEqFlatAffineBounds B1 B2 = true) : B1 = B2

A successful bitwise affine-bound comparison proves equality of the dependent records, including their input and output dimensions.

def NN.Verification.Cert.NodeReplay.exactEqOptionalAffineBounds (a b : 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))) : Bool

Bitwise equality for optional affine bounds, used by the pure replay checker.

theorem NN.Verification.Cert.NodeReplay.exactEqOptionalAffineBounds_eq_true {a b : 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))} (h : exactEqOptionalAffineBounds a b = true) : a = b

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.

def NN.Verification.Cert.NodeReplay.crownLocalReplayAccepts (g : MLTheory.CROWN.Graph) (step : 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))) → ℕ → 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))) (cert : 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)))) : Bool

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.

theorem NN.Verification.Cert.NodeReplay.crownLocalReplayAccepts_eq_true (g : MLTheory.CROWN.Graph) (step : 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))) → ℕ → 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))) (cert : 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)))) (haccept : crownLocalReplayAccepts g step cert = true) : MLTheory.CROWN.Graph.CrownCertSoundness.CrownCertLocalOK g step cert

Successful pure replay constructs the local-consistency hypothesis used by CROWN soundness.

def NN.Verification.Cert.NodeReplay.crownCertificateAccepts (g : MLTheory.CROWN.Graph) (step : 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))) → ℕ → 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))) (cert : 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)))) (diagnosticsOk : Bool) : Bool

Combine the diagnostic checks with pure local replay. Acceptance of the combined decision always supplies the proposition-level local CROWN consistency condition.

theorem NN.Verification.Cert.NodeReplay.crownCertificateAccepts_eq_true (g : MLTheory.CROWN.Graph) (step : 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))) → ℕ → 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))) (cert : 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)))) (diagnosticsOk : Bool) (haccept : crownCertificateAccepts g step cert diagnosticsOk = true) : MLTheory.CROWN.Graph.CrownCertSoundness.CrownCertLocalOK g step cert

The complete Boolean acceptance decision implies local CROWN consistency.

def NN.Verification.Cert.NodeReplay.binary32Vec (ctx : String) (mode : FloatLib.Floats.Formats.BinaryInterchange.Model.IEEERoundingMode) (dim : ℕ) (j : Lean.Json) : IO (TorchLean.Tensor (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) [dim])

Read a length-dim JSON vector into binary32, rounding each exact decimal once with mode. Callers validate the JSON entries through host binary64 first. This conversion itself does not check finiteness after rounding into binary32, whose smaller range can overflow.

def NN.Verification.Cert.NodeReplay.binary32Matrix (ctx : String) (rows cols : ℕ) (j : Lean.Json) : IO (TorchLean.Tensor (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) [rows, cols])

Read a rows × cols JSON matrix into binary32, rounding each exact decimal once.

def NN.Verification.Cert.NodeReplay.parseFlatBox? (dim : ℕ) (j : Lean.Json) : IO (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)))

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

Each decimal endpoint is rounded once into binary32: lower endpoints toward -∞ and upper endpoints toward +∞. The parsed box is therefore the smallest binary32 box containing the decimal box the artifact states. Containment is then checked exactly on binary32 values, so a decimal endpoint that lies inward of Lean's endpoint by less than one binary32 ulp is read as Lean's value. Serializations that print the shortest round-trip decimal of each endpoint still check.

def NN.Verification.Cert.NodeReplay.parseAlphaVec? (dim : ℕ) (j : Lean.Json) (ctx : String := "alpha[i]") : IO (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)))

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. Each entry is rounded once to the nearest binary32 value; rounding is monotone and 0 and 1 are exact, so the range survives the conversion.

def NN.Verification.Cert.NodeReplay.parseAffineBounds? (inDim outDim : ℕ) (j : Lean.Json) : IO (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)))

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

The affine transcript must equal Lean's binary32 replay bit for bit, so each decimal coefficient is read as the binary32 value nearest to it, with a single rounding from the exact decimal.

def NN.Verification.Cert.NodeReplay.parsePerNode {β : Type} (g : MLTheory.CROWN.Graph) (label : String) (arr : Array Lean.Json) (parse : MLTheory.CROWN.Graph.Node → Lean.Json → IO β) : IO (Array β)

Parse one JSON entry per graph node. The array must have exactly g.nodes.size entries; each entry is parsed together with its node so entry parsers can use the node's output dimension.

structure NN.Verification.Cert.NodeReplay.CROWNCertificate : Type

A node-wise CROWN certificate: the affine context, the interval and affine bounds per node, the optional α vectors of the ReLU lower relaxations, and optional ReLU phases.

• ctx : MLTheory.CROWN.Graph.AffineCtx

  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.

• phases : Array (Option (Array ℤ))

  Optional per-node ReLU phases: -1 inactive, 0 unconstrained, 1 active. A phase counts only when the IBP interval already proves it.

def NN.Verification.Cert.NodeReplay.parseInt? (j : Lean.Json) : Option ℤ

An integer from JSON, as a number or a string.

def NN.Verification.Cert.NodeReplay.parsePhases? (dim : ℕ) (j : Lean.Json) : IO (Option (Array ℤ))

One node's ReLU phases from JSON: null, or dim entries each -1, 0 or 1.

def NN.Verification.Cert.NodeReplay.parseCROWNCertificate (g : MLTheory.CROWN.Graph) (topObj : Lean.Json) : IO CROWNCertificate

Parse a CROWN node certificate.

The producer may omit "alpha" and "phases"; then no node has a custom α vector or a phase. The field "beta", the former name of "phases", is rejected rather than ignored, so an older certificate cannot silently lose its phases. Whenever α is present, parseAlphaVec? enforces the [0,1] side condition required by the ReLU relaxation proof.

def NN.Verification.Cert.NodeReplay.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.NodeReplay.getFlatBox? (cert : 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)))) (id : ℕ) : 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))

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

def NN.Verification.Cert.NodeReplay.binaryElementwiseBoxesMatchOutput (g : MLTheory.CROWN.Graph) (cert : 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)))) (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.NodeReplay.flatBoxStrictlyAbove (B : 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)) (eps : 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) : Bool

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

def NN.Verification.Cert.NodeReplay.flatBoxExcludesZero (B : 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)) : Bool

Check that every coordinate interval lies strictly on one side of zero.

def NN.Verification.Cert.NodeReplay.ibpNodePreconditionsOk (g : MLTheory.CROWN.Graph) (cert : 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)))) (id : ℕ) : Bool

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.

def NN.Verification.Cert.NodeReplay.prettyFlatBox (B : 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)) : String

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

def NN.Verification.Cert.NodeReplay.prettyAffineBounds (B : 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)) : String

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

def NN.Verification.Cert.NodeReplay.checkCROWNNode (label : String) (g : MLTheory.CROWN.Graph) (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) exactEqTensor._proof_1 exactEqTensor._proof_2 exactEqTensor._proof_3 exactEqTensor._proof_4)))) (authoritativeCrown certCrown : 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)))) (ctx : MLTheory.CROWN.Graph.AffineCtx) (id : ℕ) (computed? : 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))) : IO Bool

Check one node of a CROWN affine certificate against the bound computed? that Lean replayed: parent availability, IBP side conditions, dimensions, exact binary32 transcript equality, and diagnostic messages.