Verifier IR Lowering

This interpreter records the forward operations of a TorchLean Program in NN.IR.Graph. Tensor constants and layer weights go into a separate ParamStore, keyed by node identifier. The resulting graph can be passed to the interval and CROWN checkers, which first check whether their transfer rules support its operations and parameter payloads.

The builder handles arithmetic, shape operations, common activations, pooling, linear layers, and arbitrary-rank convolution. Composite operations such as multi-head attention produce several IR nodes. Training BatchNorm, transposed convolution, smooth max-pooling, tensor-valued gather/scatter indices, and selection on an inner axis return lowering errors. GELU also returns an error. A faithful lowering must keep its cubic association and its gate division, and the verifier fragment has no lowering or IBP/CROWN transfer for division. Expanding GELU into a different multiplication schedule can overflow a finite source result. Clamp retains the source's min/max operand order. Scalar contexts with differentiation metadata return a lowering error because the IR cannot conditionally clear their tangents at clamp bounds.

Log-softmax returns a lowering error until the verifier IR has a faithful stable operation. Replacing it by softmax followed by log changes finite-precision results even when every probability is positive. The eager runtime retains the stable source primitive.

Softplus and safeLog have dedicated operations that retain the scalar specification's stable branch. SafeLog stores epsilon as a scalar constant parent, so its value, including any dual components, reaches the evaluator unchanged. Its outer logarithm follows the source backend's semantics; certificate transfers separately check the domain needed for a sound enclosure.

LayerNorm stores the supplied epsilon, scale, and bias together in its parameter payload. We keep epsilon even when its scalar equality test reports the default value: for example, Dual equality compares the primal part, while its tangent may still differ. The IR evaluator uses the complete payload. Last-axis IBP and CROWN value bounds use directed arithmetic for the normalization and affine transform. The derivative passes leave these payloads unresolved until their rules account for the supplied parameters and the specification's variance calculation.

Leading-axis select receives a Fin index while constructing the graph. Reading coordinate zero of a state vector therefore becomes a constant one-hot projection followed by a reshape. indexSelect and scatterAdd receive their indices as tensor data and need separate lowering and transfer rules.

PyTorch weight and graph import is implemented under NN.Runtime.PyTorch.Import.

IR random nodes derive keys from node positions, while eager and typed execution count random calls. Lowering rejects random calls rather than silently choosing another draw. Evaluation-mode dropout emits no random call and is unaffected.

References (informal):

• IBP: Gowal et al. (2018).
• CROWN / DeepPoly-style linear relaxations: Zhang et al. (2018).
• LiRPA unification viewpoint: Xu et al. (2020).

IR builder

inductive NN.Verification.Builtin.Ref (α : Type) [TorchLean.Storage α] : Spec.Shape → Type

Reference produced while lowering a TorchLean program.

A value is either already materialized as an IR node, or it is still a compile-time tensor constant that can be inserted into the verifier ParamStore if a later operation needs a node parent.

• node {α : Type} [TorchLean.Storage α] {s : Spec.Shape} (id : ℕ) : Ref α s
• const {α : Type} [TorchLean.Storage α] {s : Spec.Shape} (t : TorchLean.Tensor α s) : Ref α s

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

Mutable builder state for translating a TorchLean program into verifier IR.

• nodes : Array IR.Node

  IR nodes emitted so far, in construction/topological order.

• ps : MLTheory.CROWN.Graph.ParamStore α

  Parameter payload accumulated for constant tensors and layer weights.

@[reducible, inline]

abbrev NN.Verification.Builtin.BuildM (α : Type) [TorchLean.Storage α] [Context α] : Type → Type

Builder monad used by TorchLean-to-IR lowering.

def NN.Verification.Builtin.fail {α : Type} [TorchLean.Storage α] [Context α] {β : Type} (msg : String) : BuildM α β

Raise a lowering error inside BuildM.

def NN.Verification.Builtin.requireContract {α : Type} [TorchLean.Storage α] [Context α] {β : Type} (r : Except String β) : BuildM α Unit

Run a shared IR shape contract and surface its error from lowering.

def NN.Verification.Builtin.pushNode {α : Type} [TorchLean.Storage α] [Context α] (n : IR.Node) : BuildM α Unit

Append a freshly constructed IR node to the builder state.

def NN.Verification.Builtin.freshId {α : Type} [TorchLean.Storage α] [Context α] : BuildM α ℕ

Return the next node identifier, which is the current node-array size.

def NN.Verification.Builtin.ensureNode {α : Type} [TorchLean.Storage α] [Context α] {s : Spec.Shape} (r : Ref α s) : BuildM α ℕ

Ensure a Ref is represented by an IR node.

Compile-time constants are materialized as .const nodes and recorded in the verifier ParamStore; existing graph nodes are returned unchanged.

def NN.Verification.Builtin.emitUnary {α : Type} [TorchLean.Storage α] [Context α] {s t : Spec.Shape} (kind : IR.OpKind) (x : Ref α s) : BuildM α (Ref α t)

Emit a unary IR operation with one parent node. The node's outShape is the typed result shape t, so the Ref index and the emitted IR node cannot disagree.

def NN.Verification.Builtin.emitBinary {α : Type} [TorchLean.Storage α] [Context α] {s : Spec.Shape} (kind : IR.OpKind) (a b : Ref α s) : BuildM α (Ref α s)

Emit a binary IR operation whose operands have the same shape.

def NN.Verification.Builtin.emitMatmul {α : Type} [TorchLean.Storage α] [Context α] {sA sB sOut : Spec.Shape} (a : Ref α sA) (b : Ref α sB) (scale : Option α := none) : BuildM α (Ref α sOut)

Emit a matrix-multiplication IR node whose outShape is the typed result shape sOut.

def NN.Verification.Builtin.emitInput {α : Type} [TorchLean.Storage α] [Context α] {s : Spec.Shape} : BuildM α (Ref α s)

Emit the designated verifier input node. We keep this at id 0 for bound seeding.

def NN.Verification.Builtin.getConst {α : Type} [TorchLean.Storage α] [Context α] {s : Spec.Shape} (r : Ref α s) : BuildM α (TorchLean.Tensor α s)

Read a compile-time constant tensor, failing if the value already depends on graph input.

def NN.Verification.Builtin.Internal.emitAttention {α : Type} [TorchLean.Storage α] [Context α] {n numHeads dModel headDim : ℕ} (wq wk wv : Ref α (Spec.Shape.dim dModel (Spec.Shape.dim (numHeads * headDim) Spec.Shape.scalar))) (wo : Ref α (Spec.Shape.dim (numHeads * headDim) (Spec.Shape.dim dModel Spec.Shape.scalar))) (x : Ref α (Spec.Shape.dim n (Spec.Shape.dim dModel Spec.Shape.scalar))) (mask : Option (TorchLean.Tensor Bool [n, n])) : BuildM α (Ref α (Spec.Shape.dim n (Spec.Shape.dim dModel Spec.Shape.scalar)))

Lower one sample of multi-head attention into the verifier IR.

def NN.Verification.Builtin.emitSlice {α : Type} [TorchLean.Storage α] [Context α] {n len : ℕ} {s : Spec.Shape} (start : ℕ) (_h : start + len ≤ n) (x : Ref α (Spec.Shape.dim n s)) : BuildM α (Ref α (Spec.Shape.dim len s))

Leading-axis slice encoded as a one-hot affine matrix followed by a reshape.

The matrix representation selects the intended coordinates over exact arithmetic. It also evaluates zero products and a reduction, unlike direct indexing; exceptional floating-point values and signed zeros can therefore behave differently.

def NN.Verification.Builtin.emitConcat {α : Type} [TorchLean.Storage α] [Context α] {n m : ℕ} {s : Spec.Shape} (a : Ref α (Spec.Shape.dim n s)) (b : Ref α (Spec.Shape.dim m s)) : BuildM α (Ref α (Spec.Shape.dim (n + m) s))

Emit a verifier-IR concatenation along the leading axis.

def NN.Verification.Builtin.emitAttention {α : Type} [TorchLean.Storage α] [Context α] {n numHeads dModel headDim : ℕ} (wq wk wv : Ref α [dModel, numHeads * headDim]) (wo : Ref α [numHeads * headDim, dModel]) (batch : Option ℕ := none) (x : Ref α (match batch with | none => [n, dModel] | some b => [b, n, dModel])) (mask : Option (TorchLean.Tensor Bool [n, n])) : BuildM α (Ref α (match batch with | none => [n, dModel] | some b => [b, n, dModel]))

Lower attention to the verifier's existing matrix and softmax operations.

Batched inputs use the shared balanced traversal. A singleton needs only reshapes around its attention graph; larger batches split into two parts without constructing a trailing empty graph.

@[instance_reducible]

instance NN.Verification.Builtin.instOpsBuildM {α : Type} [TorchLean.Storage α] [Context α] : Runtime.Autograd.Torch.Ops (BuildM α) α

def NN.Verification.Builtin.instOpsBuildM.repeatMask {rows keys : ℕ} (mask : TorchLean.Tensor Bool [rows, keys]) (batch : Spec.Shape) : TorchLean.Tensor Bool (batch.concat [rows, keys])