AbCrown Leaf Certificate

Alpha-beta-CROWN (AbCrown) leaf-certificate checker.

This module checks a small JSON certificate format (abcrown_leaf_cert_v0_1) exported by a Python verification pipeline. It does not run bound propagation itself; instead it validates that:

• each leaf input box is nested inside the declared root input box, and
• each leaf contains a witness that refutes the unsafe threshold (lb[i] > threshold[i] for some i).

This is useful for:

• regression testing JSON export/import paths, and
• reviewer-friendly certificate validation workflows.

References:

• beta-CROWN paper (NeurIPS 2021): https://arxiv.org/abs/2103.06624
• alpha-beta-CROWN implementation: https://github.com/Verified-Intelligence/alpha-beta-CROWN

Run: lake exe verify -- abcrown-leaf [path/to/cert.json]

def NN.Verification.Cert.AbCrownLeafCert.defaultCertPath : String

Bundled sample alpha-beta-CROWN leaf certificate.

def NN.Verification.Cert.AbCrownLeafCert.checkAbCrownLeafCertV01 (path : String) : IO Unit

Parse and validate a abcrown_leaf_cert_v0_1 JSON certificate.

On failure this throws IO.userError with a brief message.

def NN.Verification.Cert.AbCrownLeafCert.run (args : List String) : IO Unit

CLI entry point: lake exe verify -- abcrown-leaf [cert.json].

If no path is provided, checks a small bundled sample certificate under NN/Examples/Verification/AbCrown/.