IBPNodeCert

Per-node IBP certificate checking.

This is stronger than NN.Verification.IBPCert: instead of only comparing the final output bounds, we check that every node's bounds match what Lean's propagateIBPNode computes from the certificate bounds of its parents (plus the ParamStore parameters).

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.
• We allow a small tolerance due to decimal serialization in JSON.

def NN.Verification.IBPNodeCert.readIBPNodeCertificate (g : MLTheory.CROWN.Graph) (path : String) : IO (Array (Option (MLTheory.CROWN.FlatBox Float)))

Read an IBP node certificate from JSON on disk.

def NN.Verification.IBPNodeCert.checkIBPNode (g : MLTheory.CROWN.Graph) (ps : MLTheory.CROWN.Graph.ParamStore Float) (cert : Array (Option (MLTheory.CROWN.FlatBox Float))) (id : ℕ) (tol : Float) : IO Bool

Check the local IBP enclosure condition for one node against a certificate entry.

def NN.Verification.IBPNodeCert.checkIBPNodeCertificate (g : MLTheory.CROWN.Graph) (ps : MLTheory.CROWN.Graph.ParamStore Float) (path : String) (tol : Float := 1e-5) : IO Bool

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

Returns true iff every node's certificate bounds agree (within tol) with what Lean computes from the certificate parents + ParamStore.