Bundled logit-bound report CLI

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

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

Bundled report generated by the robustness export script.

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

Check a logit-bound report with timing disabled.

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

Check a logit-bound report with optional per-example timing.

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

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