TorchLean Verification Facade

Public verification APIs reachable from the NN umbrella.

@[reducible, inline]

abbrev TorchLean.Verification.CompiledIR (α : Type) [Context α] : Type

TorchLean-to-verifier compiled IR bundle.

@[reducible, inline]

abbrev TorchLean.Verification.ParamStore (α : Type) [Context α] : Type

Verifier-side parameter store used by IBP/CROWN workflows.

@[reducible, inline]

abbrev TorchLean.Verification.FlatBox (α : Type) [Context α] : Type

Flat input box used to seed verifier input bounds.

@[reducible, inline]

abbrev TorchLean.Verification.AffineCtx : Type

Input-node metadata required by affine/CROWN verifier passes.

@[reducible, inline]

abbrev TorchLean.Verification.FlatAffine (α : Type) [Context α] : Type

Output of the forward affine pass for one verifier node.

@[reducible, inline]

abbrev TorchLean.Verification.FlatAffineBounds (α : Type) [Context α] : Type

Output of the CROWN forward pass for one verifier node.

def TorchLean.Verification.compileForward1 {α : Type} [NN.API.Semantics.Scalar α] [DecidableEq Shape] {σ τ : Shape} (model : SequentialModel σ τ) (params : ParamTensors α (modelParamShapes model)) : Except String (CompiledIR α)

Compile a sequential TorchLean model into verifier IR with one distinguished input.

This is the public bridge for the common “train a model, then run IBP/CROWN on its forward pass” workflow.

def TorchLean.Verification.compileProgram1 {α : Type} [NN.API.Semantics.Scalar α] [DecidableEq Shape] {paramShapes : List Shape} {σ τ : Shape} (program : Runtime.Autograd.TorchLean.Program α (paramShapes ++ [σ]) τ) (params : ParamTensors α paramShapes) : Except String (CompiledIR α)

Compile a custom TorchLean forward program into verifier IR with one distinguished input.

Use this when the checked verification target is not a plain nn.Sequential, for example a hand-written TorchLean loss program or an attention fragment built directly from TorchLean.Ops.

def TorchLean.Verification.seedInputBox {α : Type} [NN.API.Semantics.Scalar α] (compiled : CompiledIR α) (xB : FlatBox α) : ParamStore α

Seed the distinguished verifier input with an explicit input box.

This is the standard follow-up after compileForward1: insert the box at compiled.inputId and hand the returned store to IBP/CROWN passes.

def TorchLean.Verification.lInfBox {α : Type} [NN.API.Semantics.Scalar α] {s : Shape} (center radius : Spec.Tensor α s) : FlatBox α

Flatten a center tensor and radius tensor into the verifier-side FlatBox expected by IBP/CROWN.

This is the standard public API for turning a shaped TorchLean input plus a shaped perturbation radius into a verifier input box.

def TorchLean.Verification.lInfBall {α : Type} [NN.API.Semantics.Scalar α] {s : Shape} (center : Spec.Tensor α s) (eps : α) : FlatBox α

Build a uniform ℓ∞ box around a shaped TorchLean input tensor.

This fills the input shape with the scalar radius eps and then flattens the result into the verifier-side FlatBox.

def TorchLean.Verification.seedLInfBall {α : Type} [NN.API.Semantics.Scalar α] {s : Shape} (compiled : CompiledIR α) (center : Spec.Tensor α s) (eps : α) : ParamStore α

Seed the compiled verifier input with a uniform ℓ∞ box around a shaped TorchLean input tensor.

def TorchLean.Verification.inputShape? {α : Type} [Context α] (compiled : CompiledIR α) : Except String Shape

Shape of the distinguished verifier input node.

def TorchLean.Verification.inputDim? {α : Type} [Context α] (compiled : CompiledIR α) : Except String ℕ

Flattened dimension of the distinguished verifier input node.

def TorchLean.Verification.affineCtx? {α : Type} [Context α] (compiled : CompiledIR α) : Except String AffineCtx

Checked affine context for the distinguished verifier input.

def TorchLean.Verification.affineCtx {α : Type} [Context α] (compiled : CompiledIR α) : AffineCtx

Compatibility affine context for the distinguished verifier input.

def TorchLean.Verification.runIBP {α : Type} [Context α] [NN.MLTheory.CROWN.BoundOps α] (compiled : CompiledIR α) (ps : ParamStore α) : Array (Option (FlatBox α))

Run IBP on a compiled verifier graph.

def TorchLean.Verification.outputBox? {α : Type} [Context α] (compiled : CompiledIR α) (boxes : Array (Option (FlatBox α))) : Except String (FlatBox α)

Read the verifier output box from an IBP result array.

def TorchLean.Verification.outputBoxOrThrow {α : Type} [Context α] (compiled : CompiledIR α) (boxes : Array (Option (FlatBox α))) : IO (FlatBox α)

Read the verifier output box, throwing an IO.userError if it is missing.

def TorchLean.Verification.runAffine {α : Type} [Context α] [NN.MLTheory.CROWN.BoundOps α] (compiled : CompiledIR α) (ps : ParamStore α) (ibp : Array (Option (FlatBox α))) : Array (Option (FlatAffine α))

Run the forward affine pass on a compiled verifier graph.

def TorchLean.Verification.runAffine? {α : Type} [Context α] [NN.MLTheory.CROWN.BoundOps α] (compiled : CompiledIR α) (ps : ParamStore α) (ibp : Array (Option (FlatBox α))) : Except String (Array (Option (FlatAffine α)))

Checked variant of runAffine that validates the compiled input node first.

def TorchLean.Verification.outputAffine? {α : Type} [Context α] (compiled : CompiledIR α) (affs : Array (Option (FlatAffine α))) : Except String (FlatAffine α)

Read the verifier output affine form from a forward affine result array.

def TorchLean.Verification.runCROWN {α : Type} [Context α] [NN.MLTheory.CROWN.BoundOps α] (compiled : CompiledIR α) (ps : ParamStore α) (ibp : Array (Option (FlatBox α))) : Array (Option (FlatAffineBounds α))

Run CROWN on a compiled verifier graph.

def TorchLean.Verification.runCROWN? {α : Type} [Context α] [NN.MLTheory.CROWN.BoundOps α] (compiled : CompiledIR α) (ps : ParamStore α) (ibp : Array (Option (FlatBox α))) : Except String (Array (Option (FlatAffineBounds α)))

Checked variant of runCROWN that validates the compiled input node first.

def TorchLean.Verification.outputCROWN? {α : Type} [Context α] (compiled : CompiledIR α) (bounds : Array (Option (FlatAffineBounds α))) : Except String (FlatAffineBounds α)

Read the verifier output CROWN bounds from a CROWN result array.

def TorchLean.Verification.outputBoxCROWN? {α : Type} [Context α] [NN.MLTheory.CROWN.BoundOps α] (compiled : CompiledIR α) (ps : ParamStore α) (xB : FlatBox α) : Except String (FlatBox α)

Run forward CROWN and evaluate the verifier output bounds on the compiled input box.

def TorchLean.Verification.outputBoxCROWNOrThrow {α : Type} [Context α] [NN.MLTheory.CROWN.BoundOps α] (compiled : CompiledIR α) (ps : ParamStore α) (xB : FlatBox α) : IO (FlatBox α)

Run forward CROWN and return the evaluated verifier output box, throwing on failure.

def TorchLean.Verification.backwardObjectiveBox? {α : Type} [Context α] [NN.MLTheory.CROWN.BoundOps α] (compiled : CompiledIR α) (ps : ParamStore α) (ibp : Array (Option (FlatBox α))) (xB : FlatBox α) (obj : NN.MLTheory.CROWN.Graph.FlatVec α) : Except String (FlatBox α)

Run backward CROWN for a scalar objective and evaluate it on the compiled input box.

def TorchLean.Verification.backwardObjectiveBoxOrThrow {α : Type} [Context α] [NN.MLTheory.CROWN.BoundOps α] (compiled : CompiledIR α) (ps : ParamStore α) (ibp : Array (Option (FlatBox α))) (xB : FlatBox α) (obj : NN.MLTheory.CROWN.Graph.FlatVec α) : IO (FlatBox α)

IO version of backwardObjectiveBox?.

def TorchLean.Verification.twoClassMarginLowerBound {α : Type} [Context α] {n : ℕ} (lo hi : Spec.Tensor α (Spec.Shape.dim n Spec.Shape.scalar)) (class0 class1 : Fin n) : α

Compute the conservative two-class margin lower bound lo[class0] - hi[class1].

This is the usual public robustness check for binary logits: if the result is positive, class class0 is certified against class1 over the input box.

def TorchLean.Verification.certifiesTwoClassMargin {α : Type} [Context α] {n : ℕ} (lo hi : Spec.Tensor α (Spec.Shape.dim n Spec.Shape.scalar)) (class0 class1 : Fin n) : Bool

Decide whether the two-class margin lower bound is strictly positive.