Convolution and Normalization IR Lowering

Checked lowering for pooling, convolution, batch normalization, and layer normalization.

Pooling, convolution, and batch normalization validate the pooling plan, payload, and shapes once while lowering. The closures then apply the typed specification operators directly to the typed parent value, transporting along the shape equalities established by those checks. They do not call the dynamic IR evaluator and cannot fail at runtime.

Each operation has its own small lower* definition. lowerConvolutionNormalization only dispatches on the operation kind, and the lowerConvolutionNormalization_* equation lemmas let correctness proofs reduce a dispatch to the branch they care about without unfolding the whole dispatcher.

def Runtime.Autograd.IRExec.Internal.lowerMaxPool {α : Type} [TorchLean.Storage α] [Context α] {Γ : List Spec.Shape} (ctx : NodeLoweringContext α Γ) (config : NN.IR.WindowConfig) : NodeLoweringResult ctx

Checked lowering for .maxPool config over the spatial suffix selected by the pooling plan.

def Runtime.Autograd.IRExec.Internal.lowerAvgPool {α : Type} [TorchLean.Storage α] [Context α] {Γ : List Spec.Shape} (ctx : NodeLoweringContext α Γ) (config : NN.IR.WindowConfig) : NodeLoweringResult ctx

Checked lowering for .avgPool config over the spatial suffix selected by the pooling plan.

def Runtime.Autograd.IRExec.Internal.lowerConv {α : Type} [TorchLean.Storage α] [Context α] {Γ : List Spec.Shape} (ctx : NodeLoweringContext α Γ) (config : NN.IR.ConvConfig) : NodeLoweringResult ctx

Checked lowering for .conv config with a payload-backed kernel over any leading shape.

def Runtime.Autograd.IRExec.Internal.lowerBatchNormEval {α : Type} [TorchLean.Storage α] [Context α] {Γ : List Spec.Shape} (ctx : NodeLoweringContext α Γ) (channelAxis channels : ℕ) : NodeLoweringResult ctx

Checked lowering for .batchNormEval channelAxis channels with fixed statistics.

def Runtime.Autograd.IRExec.Internal.lowerLayernorm {α : Type} [TorchLean.Storage α] [Context α] {Γ : List Spec.Shape} (ctx : NodeLoweringContext α Γ) (axis : ℕ) : NodeLoweringResult ctx

Checked lowering for .layernorm axis through the matrix view of the normalized suffix.

def Runtime.Autograd.IRExec.Internal.lowerConvolutionNormalization {α : Type} [TorchLean.Storage α] [Context α] {Γ : List Spec.Shape} (ctx : NodeLoweringContext α Γ) (kind : NN.IR.OpKind) : NodeLoweringResult ctx

Checked lowering for pooling, convolution, batch normalization, and layer normalization.

@[simp]

theorem Runtime.Autograd.IRExec.Internal.lowerConvolutionNormalization_maxPool {α : Type} [TorchLean.Storage α] [Context α] {Γ : List Spec.Shape} (ctx : NodeLoweringContext α Γ) (config : NN.IR.WindowConfig) : lowerConvolutionNormalization ctx (NN.IR.OpKind.maxPool config) = lowerMaxPool ctx config

Dispatch equation for .maxPool config.

@[simp]

theorem Runtime.Autograd.IRExec.Internal.lowerConvolutionNormalization_avgPool {α : Type} [TorchLean.Storage α] [Context α] {Γ : List Spec.Shape} (ctx : NodeLoweringContext α Γ) (config : NN.IR.WindowConfig) : lowerConvolutionNormalization ctx (NN.IR.OpKind.avgPool config) = lowerAvgPool ctx config

Dispatch equation for .avgPool config.

@[simp]

theorem Runtime.Autograd.IRExec.Internal.lowerConvolutionNormalization_conv {α : Type} [TorchLean.Storage α] [Context α] {Γ : List Spec.Shape} (ctx : NodeLoweringContext α Γ) (config : NN.IR.ConvConfig) : lowerConvolutionNormalization ctx (NN.IR.OpKind.conv config) = lowerConv ctx config

Dispatch equation for .conv config.

@[simp]

theorem Runtime.Autograd.IRExec.Internal.lowerConvolutionNormalization_batchNormEval {α : Type} [TorchLean.Storage α] [Context α] {Γ : List Spec.Shape} (ctx : NodeLoweringContext α Γ) (channelAxis channels : ℕ) : lowerConvolutionNormalization ctx (NN.IR.OpKind.batchNormEval channelAxis channels) = lowerBatchNormEval ctx channelAxis channels

Dispatch equation for .batchNormEval channelAxis channels.

@[simp]

theorem Runtime.Autograd.IRExec.Internal.lowerConvolutionNormalization_layernorm {α : Type} [TorchLean.Storage α] [Context α] {Γ : List Spec.Shape} (ctx : NodeLoweringContext α Γ) (axis : ℕ) : lowerConvolutionNormalization ctx (NN.IR.OpKind.layernorm axis) = lowerLayernorm ctx axis

Dispatch equation for .layernorm axis.