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.

Convolution and pooling

@[inline]

def Runtime.Autograd.LibTorch.Tape.Internal.validateSpatialGeometry {d : ℕ} (opName : String) (kernel stride : TorchLean.Tensor ℕ [d]) : Result Unit

Shared rank, kernel, and stride checks, in the order required by every native spatial op.

@[inline]

def Runtime.Autograd.LibTorch.Tape.Internal.spatialMetadata {d : ℕ} (opName : String) (inSpatial kernel stride padding : TorchLean.Tensor ℕ [d]) : Result (Array ℕ × Array ℕ × Array ℕ × Array ℕ)

Convert spatial metadata to the native ABI, checking axis sizes before element counts.

@[inline]

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

One-, two-, or three-dimensional convolution through LibTorch.

@[inline]

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

One-, two-, or three-dimensional transpose convolution through LibTorch.

@[inline]

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

One-, two-, or three-dimensional max pooling through LibTorch.

@[inline]

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

One-, two-, or three-dimensional smooth max pooling.

beta is checked in the input dtype, where conversion can underflow a nonzero value to zero or overflow a finite value to infinity.

@[inline]

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

One-, two-, or three-dimensional average pooling through LibTorch.