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 sanity-checks 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.leBool (x y : Float) : Bool

Boolean ≤ on Float (used for array-wise box comparisons).

def NN.Verification.Cert.AbCrownLeafCert.ltBool (x y : Float) : Bool

Boolean < on Float (used for strict refutation checks).

def NN.Verification.Cert.AbCrownLeafCert.boxWithin (rootLo rootHi lo hi : Array Float) : Bool

Check that a leaf box [lo, hi] is nested within a declared root box [rootLo, rootHi].

All arrays are interpreted pointwise.

def NN.Verification.Cert.AbCrownLeafCert.leafVerified (lb thr : Array Float) : Bool

Check that a leaf is verified by a lower-bound vector lb against an unsafe threshold thr.

Interpretation: lb is a certified lower bound on some "violation score". If lb[i] > thr[i] for some index i, then that unsafe constraint is refuted.

def NN.Verification.Cert.AbCrownLeafCert.leafVerifiedAt (lb thr : Array Float) (witnessIdx : Nat) : Bool

Like leafVerified, but first try a supplied witness index.

If the witness index is out of range, this returns false (callers usually fall back to leafVerified).

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/.