IBPNodeCert

Per-node IBP certificate checking.

Lean first computes the complete interval trace from the trusted input boxes and parameters. The untrusted artifact is then checked against that trace. In particular, no node is ever recomputed from certificate-supplied parent boxes.

Intended certificate JSON format:

{
  "ibp": [
    null,
    { "lo": [...], "hi": [...] },
    ...
  ]
}

The array length must equal g.nodes.size. Every entry must be an object whose lo and hi arrays have length equal to that node's flattened output dimension g.nodes[i]!.outShape.size. The parser reads null as a missing entry, and checkNode rejects it.

Trust boundary note:

• The certificate is untrusted; we accept it only if Lean recomputation matches.
• A certificate interval must contain the Lean-recomputed interval componentwise. Each decimal endpoint is first rounded outward into binary32 (see NodeReplay.parseFlatBox?), so an endpoint inward of Lean's by less than one binary32 ulp is read as Lean's value and accepted.

def NN.Verification.Cert.IBPNodeCert.read (g : MLTheory.CROWN.Graph) (path : String) : IO (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) read._proof_1 read._proof_2 read._proof_3 read._proof_4))))

Read an IBP node certificate from JSON on disk.

def NN.Verification.Cert.IBPNodeCert.checkNode (g : MLTheory.CROWN.Graph) (authoritative 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) read._proof_1 read._proof_2 read._proof_3 read._proof_4)))) (id : ℕ) : IO Bool

Check one artifact entry against the authoritative Lean IBP trace.

def NN.Verification.Cert.IBPNodeCert.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) read._proof_1 read._proof_2 read._proof_3 read._proof_4)) (path : String) : IO Bool

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

Returns true iff every node's certificate interval contains the interval recomputed from trusted inputs and parameters.