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, tensor-valued gather/scatter indices, and selection on an inner axis return lowering errors.

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.

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) (outShape : Spec.Shape := t) : BuildM α (Ref α t)

Emit a unary IR operation with one parent node.

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) (outShape : Spec.Shape := sOut) : BuildM α (Ref α sOut)

Emit a matrix-multiplication IR node.

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.emitMultiHeadAttention {α : 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.emitLeadingSlice {α : 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))

Exact leading-axis slice expressed through the verifier's affine matrix fragment.

def NN.Verification.Builtin.emitLeadingConcat {α : 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.emitBatchedMultiHeadAttention {α : Type} [TorchLean.Storage α] [Context α] {batch 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 batch (Spec.Shape.dim n (Spec.Shape.dim dModel Spec.Shape.scalar)))) (mask : Option (TorchLean.Tensor Bool [n, n])) : BuildM α (Ref α (Spec.Shape.dim batch (Spec.Shape.dim n (Spec.Shape.dim dModel Spec.Shape.scalar))))

Lower batched attention as the leading-axis map of the single-sample verifier graph.

This is intentionally a semantic lowering rather than a claim that the verifier understands a new opaque fused kernel.

@[instance_reducible]

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