Explicit Verification Lowering

Low-level access to TorchLean's verifier graph. Most applications should import NN.API.Verification, train with trainer.train, then call trained.verify center (radius := r) (norm := linf); import this module only when constructing or inspecting graph-level IBP/CROWN workflows directly.

These entry points check the generated graph's structure and shapes, not its numerical equality with the source model. Slicing and leading-axis selection currently become one-hot matrix products; they can change signed zeros or propagate an unselected NaN or infinity. Multi-sample attention uses those slices. Bounds on the resulting graph need a separate source correspondence argument before being used as guarantees about the original finite-precision execution.

def TorchLean.Verification.lowerForwardToIR {α : Type} [Storage α] [Context α] {σ τ : Shape} (model : nn.Sequential σ τ) (state : nn.State α (Runtime.Autograd.Model.Layers.Seq.stateShapes model)) : Except String (LoweredIR α)

Lower a sequential model into structurally checked verifier IR with one distinguished input. This does not establish finite-precision source equivalence; see the slicing restriction above.

def TorchLean.Verification.lowerProgramToIR {α : Type} [Storage α] [Context α] {paramShapes : List Shape} {σ τ : Shape} (forwardProgram : Runtime.Autograd.Model.Program α (paramShapes ++ [σ]) τ) (state : nn.State α paramShapes) : Except String (LoweredIR α)

Lower a custom forward program into structurally checked verifier IR with one distinguished input. Source equivalence remains separate from graph validation.

def TorchLean.Verification.runAffine {α : Type} [Storage α] [Context α] [NN.MLTheory.CROWN.BoundOps α] (lowered : LoweredIR α) (parameters : ParamStore α) (intervalBounds : Array (Option (FlatBox α))) : Except String (Array (Option (FlatAffine α)))

Compute upper affine bounds after validating the lowered verifier input.

The engine retains both sides internally so negative coefficients use the correct parent bound.

def TorchLean.Verification.runCROWN {α : Type} [Storage α] [Context α] [NN.MLTheory.CROWN.BoundOps α] [NN.MLTheory.CROWN.NonlinearBoundOps α] (lowered : LoweredIR α) (parameters : ParamStore α) (intervalBounds : Array (Option (FlatBox α))) : Except String (Array (Option (FlatAffineBounds α)))

Compute nodewise CROWN bounds after validating the lowered verifier input.