Bundled margin-certificate CLI

Command entry point for checking the bundled robustness margin certificate. The JSON checker lives in NN.Verification.Robustness.MarginCert; this module supplies the repository default artifact path used by lake exe verify -- margin-cert.

def NN.Verification.Robustness.MarginCertCLI.defaultPath : String

Bundled certificate generated by the robustness export script.

def NN.Verification.Robustness.MarginCertCLI.check (path : String) : IO Unit

Check a margin certificate with timing disabled.

def NN.Verification.Robustness.MarginCertCLI.checkWithTiming (path : String) (timing : Bool) (timingEvery : ℕ) : IO Unit

Check a margin certificate with optional per-example timing.

def NN.Verification.Robustness.MarginCertCLI.run (args : List String) : IO Unit

CLI entry point for lake exe verify -- margin-cert [cert.json].