CLI

Unified verification CLI registry.

The repository exposes several verification entry points: LiRPA-style bound checks, PINN certificate recomputation, α,β-CROWN leaf artifact checks, robustness margin certificates, ODE enclosure checks, and model-to-IR bound propagation workflows.

This file defines a single dispatcher so users can run everything from: lake exe verify -- <tool> [args...]

References (background on the verifier families exposed here):

• IBP (interval bound propagation): arXiv:1810.12715.
• CROWN / α,β-CROWN style linear relaxations: see arXiv:1811.00866 and arXiv:2103.06624.
• VNN-COMP (benchmark format / suites): see the VNN-COMP competition pages and papers.

Tool registry

We represent each runnable verifier or checker as a Tool record, then expose a simple dispatcher over a list of tools.

structure NN.Verification.CLI.Tool : Type

A single entry in the unified verification CLI.

Each Tool corresponds to one command name (e.g. torchlean-ibp) and a handler run : List String → IO Unit.

Design notes:

• Tools with includeInAll = false are interactive or long-running workflows and are excluded from the all command.
• Tools may declare a default path argument for convenience.

• name : String

  Command-line name (first positional arg) used to select this tool.

• description : String

  Short help text shown in list output.

• defaultArg : Option String

  Default file/path argument, if the tool expects a path.

• includeInAll : Bool

  Whether lake exe verify -- all should run this tool.

• run : List String → IO Unit

  Implementation: run the tool with the remaining CLI args.

def NN.Verification.CLI.toolUsage (t : Tool) : String

One-line usage string for a single tool in the unified verification CLI.

def NN.Verification.CLI.usage (tools : List Tool) : String

Usage string for the unified verification CLI dispatcher.

def NN.Verification.CLI.getPathOrDefault (args : List String) (defaultPath : String) : String

Extract a path argument if present; otherwise fall back to a default path.

def NN.Verification.CLI.lirpaTools : List Tool

Tool group: LiRPA-style bound propagation and certificate checking.

def NN.Verification.CLI.otherTools : List Tool

Tool group: other verification-related utilities.

def NN.Verification.CLI.tools : List Tool

The full list of registered verification tools (LiRPA plus other workflows/checkers).

def NN.Verification.CLI.findTool? (name : String) : Option Tool

Look up a tool by its command-line name.

def NN.Verification.CLI.dispatch (args : List String) : IO Unit

Dispatch a unified verification command.

Supported invocations:

• list: show usage and tool list
• all: run all non-interactive tools (ignores extra args)
• <tool> [args...]: run a named tool

lake exe verify executes the unqualified main.

We keep the implementation namespaced and provide a thin root-level wrapper so the Lake executable entrypoint remains stable.

def main (args : List String) : IO Unit

lake exe verify entry point.

This is a thin wrapper around the unified dispatcher NN.Verification.CLI.dispatch.