Verification IR Lowering

Public entry points for lowering TorchLean programs to the shared verifier IR and querying IBP and CROWN bounds. Graph construction lives in Lowering.Builder; this module contains the stable result type and the operations available on a lowered graph.

The broad lowerForwardToIR entry point runs a TorchLean.Program with the IR-building interpreter, then checks the graph's structure and shapes. A successful result is executable and ready for verifier passes, but does not by itself prove equality with the source program. The theorem-backed source fragment lives under NN.Verification.Builtin.Proved.

Public lowering entry points

structure NN.Verification.Builtin.LoweredIR (α : Type) [TorchLean.Storage α] [Context α] : Type

Result of lowering a TorchLean forward model to verifier IR.

This bundles:

• the produced IR graph (NN.IR.Graph),
• a CROWN/LiRPA-style ParamStore containing constants and layer parameters, and
• the distinguished input/output node ids (used by bound propagation and certificate checkers).

• graph : IR.Graph

  Lowered IR graph.

• ps : MLTheory.CROWN.Graph.ParamStore α

  Parameters/constants for verifier algorithms (IBP, CROWN, etc.).

• inputId : ℕ

  Distinguished input node id (kept stable as 0).

• outputId : ℕ

  Output node id.

def NN.Verification.Builtin.LoweredIR.seedInputBox {α : Type} [TorchLean.Storage α] [Context α] (lowered : LoweredIR α) (xB : MLTheory.CROWN.FlatBox α) : MLTheory.CROWN.Graph.ParamStore α

Seed the distinguished verifier input with an explicit flat input box.

def NN.Verification.Builtin.lInfBox {α : Type} [TorchLean.Storage α] [Context α] {s : Spec.Shape} (center radius : TorchLean.Tensor α s) : MLTheory.CROWN.FlatBox α

Flatten a shaped center/radius pair into the verifier input-box representation.

def NN.Verification.Builtin.lInfBall {α : Type} [TorchLean.Storage α] [Context α] {s : Spec.Shape} (center : TorchLean.Tensor α s) (eps : α) : MLTheory.CROWN.FlatBox α

Uniform $\ell^\infty$ box around a shaped TorchLean input tensor.

@[simp]

theorem NN.Verification.Builtin.lInfBall_dim {α : Type} [TorchLean.Storage α] [Context α] {s : Spec.Shape} (center : TorchLean.Tensor α s) (eps : α) : (lInfBall center eps).dim = s.size

Flattening an $\ell^\infty$ ball preserves the number of tensor entries as its dimension.

def NN.Verification.Builtin.LoweredIR.seedLInfBall {α : Type} [TorchLean.Storage α] [Context α] {s : Spec.Shape} (lowered : LoweredIR α) (center : TorchLean.Tensor α s) (eps : α) : MLTheory.CROWN.Graph.ParamStore α

Seed the distinguished verifier input with a uniform $\ell^\infty$ ball.

def NN.Verification.Builtin.LoweredIR.inputShape? {α : Type} [TorchLean.Storage α] [Context α] (lowered : LoweredIR α) : Except String Spec.Shape

Shape of the distinguished verifier input node.

def NN.Verification.Builtin.LoweredIR.inputDim? {α : Type} [TorchLean.Storage α] [Context α] (lowered : LoweredIR α) : Except String ℕ

Flattened dimension of the distinguished verifier input node.

def NN.Verification.Builtin.LoweredIR.affineCtx? {α : Type} [TorchLean.Storage α] [Context α] (lowered : LoweredIR α) : Except String MLTheory.CROWN.Graph.AffineCtx

Affine/CROWN context for the distinguished verifier input.

def NN.Verification.Builtin.LoweredIR.runIBP {α : Type} [TorchLean.Storage α] [Context α] [MLTheory.CROWN.BoundOps α] [MLTheory.CROWN.NonlinearBoundOps α] (lowered : LoweredIR α) (ps : MLTheory.CROWN.Graph.ParamStore α) : Array (Option (MLTheory.CROWN.FlatBox α))

Run IBP on a lowered verifier graph.

def NN.Verification.Builtin.LoweredIR.outputBox? {α : Type} [TorchLean.Storage α] [Context α] (lowered : LoweredIR α) (boxes : Array (Option (MLTheory.CROWN.FlatBox α))) : Except String (MLTheory.CROWN.FlatBox α)

Read the verifier output box from an IBP result array.

def NN.Verification.Builtin.LoweredIR.outputBoxOrThrow {α : Type} [TorchLean.Storage α] [Context α] (lowered : LoweredIR α) (boxes : Array (Option (MLTheory.CROWN.FlatBox α))) : IO (MLTheory.CROWN.FlatBox α)

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

def NN.Verification.Builtin.LoweredIR.outputAffine? {α : Type} [TorchLean.Storage α] [Context α] (lowered : LoweredIR α) (affs : Array (Option (MLTheory.CROWN.Graph.FlatAffine α))) : Except String (MLTheory.CROWN.Graph.FlatAffine α)

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

def NN.Verification.Builtin.LoweredIR.outputBoxCROWN? {α : Type} [TorchLean.Storage α] [Context α] [MLTheory.CROWN.BoundOps α] [MLTheory.CROWN.NonlinearBoundOps α] (lowered : LoweredIR α) (ps : MLTheory.CROWN.Graph.ParamStore α) (xB : MLTheory.CROWN.FlatBox α) : Except String (MLTheory.CROWN.FlatBox α)

Run forward CROWN and evaluate the lowered verifier output on a selected input box.

def NN.Verification.Builtin.LoweredIR.outputBoxCROWNOrThrow {α : Type} [TorchLean.Storage α] [Context α] [MLTheory.CROWN.BoundOps α] [MLTheory.CROWN.NonlinearBoundOps α] (lowered : LoweredIR α) (ps : MLTheory.CROWN.Graph.ParamStore α) (xB : MLTheory.CROWN.FlatBox α) : IO (MLTheory.CROWN.FlatBox α)

Run forward CROWN for a lowered verifier graph, throwing an IO.userError on failure.

def NN.Verification.Builtin.LoweredIR.backwardObjectiveBox? {α : Type} [TorchLean.Storage α] [Context α] [MLTheory.CROWN.BoundOps α] (lowered : LoweredIR α) (ps : MLTheory.CROWN.Graph.ParamStore α) (ibp : Array (Option (MLTheory.CROWN.FlatBox α))) (xB : MLTheory.CROWN.FlatBox α) (obj : MLTheory.CROWN.Graph.FlatTensor α) : Except String (MLTheory.CROWN.FlatBox α)

Run objective-dependent backward CROWN and evaluate the scalar objective on the input box.

def NN.Verification.Builtin.refListConstOfPack {α : Type} [TorchLean.Storage α] [Context α] {ss : List Spec.Shape} : TorchLean.TensorPack α ss → Runtime.Autograd.Torch.RefList (fun (s : Spec.Shape) => Ref α s) ss

Convert a parameter TorchLean.TensorPack into constant references for IR lowering.

@[noinline]

def NN.Verification.Builtin.lowerForwardToIR {α : Type} [TorchLean.Storage α] [Context α] {paramShapes : List Spec.Shape} {inShape outShape : Spec.Shape} (model : Runtime.Autograd.Model.Program α (paramShapes ++ [inShape]) outShape) (params : TorchLean.TensorPack α paramShapes) : Except String (LoweredIR α)

Lower a TorchLean forward model with one distinguished input, supplied as its last argument.

Success means that every encountered operation was supported and that the produced IR passed structural and shape validation. It does not attach a source-to-IR semantic theorem.