Core Tape Convolution and Pooling

This file implements the pure tape nodes for convolution, transposed convolution, and pooling. These nodes are backend-independent: they record forward values, parents, and backward closures using the spec-layer definitions before CUDA or typed graph execution enters the picture.

def Runtime.Autograd.Tape.conv {α : Type} [TorchLean.Storage α] [Context α] [DecidableRel fun (x1 x2 : α) => x1 > x2] {d inC outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (t : Tape α) (kernelId biasId inputId : ℕ) (name : String := "conv") : Result (Tape α × ℕ)

N-D convolution for channels-first tensors (inC, spatial...) (no batch axis).

The spatial rank and every geometric parameter are encoded by vectors of the same length.

def Runtime.Autograd.Tape.convTranspose {α : Type} [TorchLean.Storage α] [Context α] [DecidableRel fun (x1 x2 : α) => x1 > x2] {d inC outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (t : Tape α) (kernelId biasId inputId : ℕ) (name : String := "conv_transpose") : Result (Tape α × ℕ)

N-D transpose convolution for channels-first tensors (inC, spatial...) (no batch axis).

Kernel layout matches the spec/PyTorch convention (inC, outC, kernel[0], ..., kernel[d-1]).

PyTorch comparison: torch.nn.functional.conv_transpose{d}d specialized to a single sample (no batch axis).

def Runtime.Autograd.Tape.maxPool {α : Type} [TorchLean.Storage α] [Context α] {d C : ℕ} {inSpatial kernel stride padding : TorchLean.Tensor ℕ [d]} (t : Tape α) (xId : ℕ) : Result (Tape α × ℕ)

N-D max pooling for channels-first tensors (C, spatial...) (no batch axis).

Padding is symmetric per-axis and uses zeros. To model unpadded pooling, pass padding := 0 on every axis.

def Runtime.Autograd.Tape.avgPool {α : Type} [TorchLean.Storage α] [Context α] {d C : ℕ} {inSpatial kernel stride padding : TorchLean.Tensor ℕ [d]} (t : Tape α) (xId : ℕ) : Result (Tape α × ℕ)

N-D average pooling for channels-first tensors (C, spatial...) (no batch axis).

Padding is symmetric per-axis and uses zeros; pooling uses count_include_pad=true semantics.

def Runtime.Autograd.Tape.smoothMaxPool {α : Type} [TorchLean.Storage α] [Context α] [DecidableEq α] {d C : ℕ} {inSpatial kernel stride padding : TorchLean.Tensor ℕ [d]} (t : Tape α) (xId : ℕ) (beta : α) : Result (Tape α × ℕ)

N-D smooth max pooling (log-sum-exp surrogate) for channels-first tensors (C, spatial...).

The executable tape requires a finite, nonzero beta. Finiteness is checked through the scalar arithmetic contract: finite scalar backends satisfy beta - beta == 0, whereas IEEE NaN and infinity do not. At least one spatial dimension is required, matching the native runtime contract.