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. Each non-null entry must have lo and hi arrays of length equal to that node's flattened output dimension g.nodes[i]!.outShape.size.

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. Decimal serialization may widen an endpoint, but it may not move an endpoint inward.

def NN.Verification.IBPNodeCert.readIBPNodeCertificate (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) readIBPNodeCertificate._proof_1 readIBPNodeCertificate._proof_2 readIBPNodeCertificate._proof_3 readIBPNodeCertificate._proof_4))))

Read an IBP node certificate from JSON on disk.

def NN.Verification.IBPNodeCert.checkIBPNode (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) readIBPNodeCertificate._proof_1 readIBPNodeCertificate._proof_2 readIBPNodeCertificate._proof_3 readIBPNodeCertificate._proof_4)))) (id : ℕ) : IO Bool

Check one artifact entry against the authoritative Lean IBP trace.

def NN.Verification.IBPNodeCert.checkIBPNodeCertificate (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) readIBPNodeCertificate._proof_1 readIBPNodeCertificate._proof_2 readIBPNodeCertificate._proof_3 readIBPNodeCertificate._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.