IR Payloads

Shared payload records for IR evaluators and verifier backends.

The graph stores operation tags 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) [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 : Spec.Tensor α (Spec.Shape.dim self.n Spec.Shape.scalar)

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

structure NN.IR.LinearWB (α : Type) [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 : Spec.Tensor α (Spec.Shape.dim self.outDim (Spec.Shape.dim self.inDim Spec.Shape.scalar))

  Weight matrix in the PyTorch convention outDim × inDim.

• b : Spec.Tensor α (Spec.Shape.dim self.outDim Spec.Shape.scalar)

  Bias vector added after matrix-vector multiplication.

structure NN.IR.Conv2DParams (α : Type) [Context α] : Type

Payload record for a conv2d node.

The spec-layer Conv2DSpec carries the typed kernel and bias. The cached dimensions let verifier passes reconstruct flat shapes without unpacking the spec package at every use site.

• inC : ℕ

  Input channels.

• outC : ℕ

  Output channels.

• kH : ℕ

  Kernel height.

• kW : ℕ

  Kernel width.

• stride : ℕ

  Stride.

• padding : ℕ

  Padding size.

• inH : ℕ

  Input height.

• inW : ℕ

  Input width.

• hIn : self.inC ≠ 0

  Proof that the input channel count is nonzero, required by the spec convolution layer.

• hKH : self.kH ≠ 0

  Proof that the kernel height is nonzero.

• hKW : self.kW ≠ 0

  Proof that the kernel width is nonzero.

• spec : Spec.Conv2DSpec self.inC self.outC self.kH self.kW self.stride self.padding α ⋯ ⋯ ⋯

  Spec-layer convolution package containing weights, bias, and convolution metadata.

structure NN.IR.BatchNorm2DNchwEvalParams (α : Type) [Context α] : Type

Payload record for eval-mode BatchNorm2d over N×C×H×W tensors.

• c : ℕ

  Channel count.

• gamma : Spec.Tensor α (Spec.Shape.dim self.c Spec.Shape.scalar)

  Affine scale.

• beta : Spec.Tensor α (Spec.Shape.dim self.c Spec.Shape.scalar)

  Affine bias.

• mean : Spec.Tensor α (Spec.Shape.dim self.c Spec.Shape.scalar)

  Running mean.

• var : Spec.Tensor α (Spec.Shape.dim self.c Spec.Shape.scalar)

  Running variance.

• eps : α

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

structure NN.IR.Payload (α : Type) [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-facing 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.

• conv2d? : ℕ → Option (Conv2DParams α)

  Convolution parameters keyed by the conv2d node id.

• batchNorm2dNchwEval? : ℕ → Option (BatchNorm2DNchwEvalParams α)

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