Verification Execution

Implementation support for the public trained.verify operation. The public named arguments are lowered into a verifier input region and returned as a validated Verification.Report. The bounds concern the recorded verifier graph. The broad lowering does not attach a finite-precision source-equivalence theorem: one-hot slicing and leading-axis selection can change signed zeros and exceptional values, including in multi-sample attention. Applying a report to the original execution needs that separate correspondence argument.

Applications should import NN.API.Verification and call trained.verify center (radius := r) (norm := linf). Direct verifier graph construction remains in NN.API.Verification.Lowering.

def TorchLean.Verification.Internal.readBounds {α : Type} [Storage α] [Context α] [Runtime.Autograd.Torch.TensorTransfer α] (box : NN.MLTheory.CROWN.FlatBox α) : IO Bounds

Convert an internal flat interval into the public host-Float bounds representation.

def TorchLean.Verification.Internal.inputBoxFromFloat {α : Type} [Storage α] [Context α] [Runtime.FromFloat α] {σ : Shape} (center : Tensor Float σ) (radius : Float) : NN.MLTheory.CROWN.FlatBox α

Enclose the requested binary64 ball before converting its endpoints to the runtime scalar.

Rounding the center and radius separately can shrink the region, especially when subtraction cancels most of the center. The directed conversion requires a faithful roundForValidation hook, supplied by both arithmetic backends used by ordinary trained results.

def TorchLean.Verification.Internal.forState {σ τ : Shape} {α : Type} [Storage α] [Context α] [Runtime.FromFloat α] [Runtime.Autograd.Torch.TensorTransfer α] [NN.MLTheory.CROWN.BoundOps α] [NN.MLTheory.CROWN.NonlinearBoundOps α] (trainer : Trainer σ τ) (modelState : nn.State α (Runtime.Autograd.Model.Layers.Seq.stateShapes trainer.model)) (center : Tensor Float σ) (radius : Float) (norm : Norm) (property : Property) (algorithm : Algorithm) : IO Report

Build the verification closure retained by an ordinary trained result.

The closure captures the completed parameter snapshot, so subsequent updates to the training session cannot change the model being verified. The returned report describes the lowered graph; it does not resolve the source-correspondence restriction on its one-hot slicing and selection operations. It names the algorithm that ran: alphaCrown on a rounded scalar runs directed CROWN, so the report says crown.