IR Payloads

Shared payload records for IR evaluators and verifier backends.

The graph stores operation names and edges. Tensor-valued constants, weights, convolution kernels, and BatchNorm running statistics live in a separate payload keyed by node id, matching the way formats such as ONNX keep graph structure separate from initializers.

structure NN.IR.ConstFlat (α : Type) [TorchLean.Storage α] [Context α] : Type

Payload record for a const node.

Constants are stored in a flat representation so backends can use one vector container and let IR evaluation reshape the data to the node's declared output shape.

• n : ℕ

  Number of scalar entries stored in the flat constant payload.

• v : TorchLean.Tensor α [self.n]

  Constant values stored as a vector before evaluation reshapes them to the IR node shape.

structure NN.IR.LinearWB (α : Type) [TorchLean.Storage α] [Context α] : Type

Payload record for a linear node: weight matrix W and bias vector b.

The node's input x comes from the graph edge; W,b live in the external Payload, similar to ONNX initializers or a PyTorch state_dict.

• outDim : ℕ

  Output dimension.

• inDim : ℕ

  Input dimension.

• W : TorchLean.Tensor α [self.outDim, self.inDim]

  Weight matrix in the PyTorch convention outDim × inDim.

• b : TorchLean.Tensor α [self.outDim]

  Bias vector added after matrix-vector multiplication.

structure NN.IR.ConvParams (α : Type) [TorchLean.Storage α] [Context α] : Type

Payload for an arbitrary-dimensional convolution node.

• spatialRank : ℕ

  Number of spatial axes.

• inChannels : ℕ

  Input channels.

• outChannels : ℕ

  Output channels.

• kernel : TorchLean.Tensor ℕ [self.spatialRank]

  Per-axis kernel extents.

• stride : TorchLean.Tensor ℕ [self.spatialRank]

  Per-axis strides.

• padding : TorchLean.Tensor ℕ [self.spatialRank]

  Zero padding before each spatial axis.

• dilation : TorchLean.Tensor ℕ [self.spatialRank]

  Spacing between adjacent kernel samples.

• paddingAfter : TorchLean.Tensor ℕ [self.spatialRank]

  Zero padding after each spatial axis. padding is the padding before the input.

• groups : ℕ

  Number of independent channel groups.

• inputSpatial : TorchLean.Tensor ℕ [self.spatialRank]

  Spatial shape of one input sample.

• kernelNonzero (i : Fin self.spatialRank) : self.kernel.getScalar i ≠ 0

  Every kernel extent is nonzero.

• strideNonzero (i : Fin self.spatialRank) : self.stride.getScalar i ≠ 0

  Every stride is nonzero.

• spec : Spec.ConvSpec self.spatialRank self.inChannels self.outChannels self.kernel self.stride self.padding α

  Typed weights, bias, and convolution geometry.

def NN.IR.ConvParams.matchesConfig {α : Type} [TorchLean.Storage α] [Context α] (params : ConvParams α) (config : ConvConfig) : Bool

Whether a convolution payload implements the geometry declared by an IR node.

def NN.IR.ConvParams.input {α : Type} [TorchLean.Storage α] [Context α] (params : ConvParams α) (leading : Spec.Shape) : Spec.Shape

Input shape expected by a convolution payload after preserving the graph's leading axes.

def NN.IR.ConvParams.output {α : Type} [TorchLean.Storage α] [Context α] (params : ConvParams α) (leading : Spec.Shape) : Spec.Shape

Output shape produced by the typed convolution payload for the given leading axes.

structure NN.IR.BatchNormEvalParams (α : Type) [TorchLean.Storage α] [Context α] : Type

Payload for eval-mode BatchNorm along a channel axis selected by the graph node.

• c : ℕ

  Channel count.

• gamma : TorchLean.Tensor α [self.c]

  Affine scale.

• beta : TorchLean.Tensor α [self.c]

  Affine bias.

• mean : TorchLean.Tensor α [self.c]

  Running mean.

• var : TorchLean.Tensor α [self.c]

  Running variance.

• eps : α

  Epsilon added to the running variance before taking the square root.

structure NN.IR.LayerNormParams (α : Type) [TorchLean.Storage α] [Context α] : Type

Affine parameters and epsilon for LayerNorm over an arbitrary normalized suffix.

• normalizedShape : Spec.Shape

  Shape of the suffix normalized by the corresponding node.

• gamma : TorchLean.Tensor α self.normalizedShape

  Learned elementwise scale over normalizedShape.

• beta : TorchLean.Tensor α self.normalizedShape

  Learned elementwise bias over normalizedShape.

• eps : α

  Epsilon added to the variance before taking the square root.

structure NN.IR.Payload (α : Type) [TorchLean.Storage α] [Context α] : Type

External parameter payloads keyed by IR node id.

This is focused on denotational IR evaluation. Runtime backends may store tensors differently, but their proof layer semantics pass through this shape-indexed boundary.

• const? : ℕ → Option (ConstFlat α)

  Flat constants keyed by the const node id.

• linear? : ℕ → Option (LinearWB α)

  Linear weights and bias keyed by the linear node id.

• conv? : ℕ → Option (ConvParams α)

  Convolution parameters keyed by the conv node id.

• batchNormEval? : ℕ → Option (BatchNormEvalParams α)

  Eval-mode BatchNorm parameters keyed by the batchNormEval node id.

• layerNorm? : ℕ → Option (LayerNormParams α)

  Affine LayerNorm parameters keyed by the layernorm node id.