CUDA Tape Operations: Convolution and Pooling

Every entry point rejects zero strides and geometry that cannot cross the UInt32 ABI, validates input lengths through requireValue, and checks forward native outputs before recording them on the tape. Pointer lifetime and device ownership remain responsibilities of the native buffer layer.

Arbitrary-rank convolution and pooling

def Runtime.Autograd.Cuda.Tape.conv {d inC outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (t : Tape) (kernelId biasId inputId : ℕ) : Result (Tape × ℕ)

Rank-polymorphic convolution via the CUDA ConvPool FFI (spatial rank $\le 8$).

def Runtime.Autograd.Cuda.Tape.convTranspose {d inC outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (t : Tape) (kernelId biasId inputId : ℕ) : Result (Tape × ℕ)

Rank-polymorphic transpose convolution via the CUDA ConvPool FFI (spatial rank $\le 8$).

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

Rank-polymorphic max pooling via the CUDA ConvPool FFI (spatial rank $\le 8$).

def Runtime.Autograd.Cuda.Tape.smoothMaxPool {d C : ℕ} {inSpatial kernel stride padding : TorchLean.Tensor ℕ [d]} (t : Tape) (xId : ℕ) (beta : Float) : Result (Tape × ℕ)

Rank-polymorphic smooth max pooling via the CUDA ConvPool FFI (spatial rank at most eight).

beta is checked after conversion to Float32, because conversion can underflow a nonzero Float to zero or overflow a finite one to infinity.

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

Rank-polymorphic average pooling via the CUDA ConvPool FFI (spatial rank $\le 8$).