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.Runtime.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.

GELU and stable log-softmax are rejected rather than replaced by numerically different expansions. The one-hot matrix encoding of slicing performs arithmetic instead of direct indexing; structural validation does not establish numerical equivalence for that encoding. Clamp preserves the source operand order, but rejects scalar contexts whose stopGradient? requires conditional differentiation-metadata clearing at the bounds.

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.lInfBall {α : Type} [TorchLean.Storage α] [Context α] [MLTheory.CROWN.BoundOps α] {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 α] [MLTheory.CROWN.BoundOps α] {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 α] [MLTheory.CROWN.BoundOps α] {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.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 α)

Compute CROWN output bounds on a selected input box. Exact-reassociation backends use a forward affine sweep; rounded backends request directed backward bounds for the output coordinates.

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.

@[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.

def NN.Verification.Builtin.lowerForwardToIR.constRefs {α : Type} [TorchLean.Storage α] {shapes : List Spec.Shape} : TorchLean.TensorPack α shapes → Runtime.Autograd.Torch.RefList (Ref α) shapes