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.

Conv2D + pooling (ConvPool FFI)

def Runtime.Autograd.Cuda.Tape.conv2d {inC outC kH kW stride padding inH inW : ℕ} {h1 : inC ≠ 0} {h2 : kH ≠ 0} {h3 : kW ≠ 0} (t : Tape) (kernelId biasId inputId : ℕ) : Result (Tape × ℕ)

Conv2D forward/backward via ConvPool FFI (single image, channels-first).

ConvTranspose2D (ConvPool FFI)

def Runtime.Autograd.Cuda.Tape.convTranspose2d {inC outC kH kW stride padding inH inW : ℕ} {h1 : inC ≠ 0} {h2 : kH ≠ 0} {h3 : kW ≠ 0} (t : Tape) (kernelId biasId inputId : ℕ) : Result (Tape × ℕ)

ConvTranspose2D forward/backward via ConvPool FFI (single image, channels-first).

Generic naming wrappers

The CUDA tape exposes conv/max_pool/avg_pool/smooth_max_pool using the same names as the CPU tape. These dispatch to the ConvPool CUDA FFI entrypoints that take per-axis parameters as Array Nat (rank $\le 8$).

The *2d* wrappers remain as concise convenience names for the common rank-2 case.

def Runtime.Autograd.Cuda.Tape.conv {d inC outC : ℕ} {kernel stride padding inSpatial : Vector ℕ d} (t : Tape) (kernelId biasId inputId : ℕ) (hInC : inC ≠ 0) (hKernel : ∀ (i : Fin d), kernel.get i ≠ 0) : Result (Tape × ℕ)

N-D convolution (CUDA) via ConvPool FFI (rank $\le 8$).

def Runtime.Autograd.Cuda.Tape.convTranspose {d inC outC : ℕ} {kernel stride padding inSpatial : Vector ℕ d} (t : Tape) (kernelId biasId inputId : ℕ) (hInC : inC ≠ 0) (hKernel : ∀ (i : Fin d), kernel.get i ≠ 0) : Result (Tape × ℕ)

N-D transposed convolution (CUDA) via ConvPool FFI (rank $\le 8$).

def Runtime.Autograd.Cuda.Tape.maxPool2d {kH kW inH inW inC stride : ℕ} {h1 : kH ≠ 0} {h2 : kW ≠ 0} (t : Tape) (xId : ℕ) : Result (Tape × ℕ)

MaxPool2D via ConvPool FFI (no padding).

def Runtime.Autograd.Cuda.Tape.maxPool2dPad {kH kW inH inW inC stride padding : ℕ} {h1 : kH ≠ 0} {h2 : kW ≠ 0} (t : Tape) (xId : ℕ) : Result (Tape × ℕ)

MaxPool2D via ConvPool FFI (with symmetric padding).

def Runtime.Autograd.Cuda.Tape.maxPool {d C : ℕ} {inSpatial kernel stride padding : Vector ℕ d} {hKernel : ∀ (i : Fin d), kernel.get i ≠ 0} (t : Tape) (xId : ℕ) : Result (Tape × ℕ)

N-D max pooling (CUDA) via ConvPool FFI (rank $\le 8$).

def Runtime.Autograd.Cuda.Tape.smoothMaxPool2d {kH kW inH inW inC stride : ℕ} {h1 : kH ≠ 0} {h2 : kW ≠ 0} (t : Tape) (xId : ℕ) (beta : Float) : Result (Tape × ℕ)

Smooth max-pool2d (log-sum-exp surrogate) via ConvPool FFI, without padding.

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.smoothMaxPool2dPad {kH kW inH inW inC stride padding : ℕ} {h1 : kH ≠ 0} {h2 : kW ≠ 0} (t : Tape) (xId : ℕ) (beta : Float) : Result (Tape × ℕ)

Smooth max-pool2d (log-sum-exp surrogate) via ConvPool FFI, with symmetric padding.

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.smoothMaxPool {d C : ℕ} {inSpatial kernel stride padding : Vector ℕ d} {hKernel : ∀ (i : Fin d), kernel.get i ≠ 0} (t : Tape) (xId : ℕ) (beta : Float) : Result (Tape × ℕ)

N-D smooth max pooling via the CUDA ConvPool FFI (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.avgPool2d {kH kW inH inW inC stride : ℕ} (h1 : kH ≠ 0) (h2 : kW ≠ 0) (t : Tape) (xId : ℕ) : Result (Tape × ℕ)

AvgPool2D via ConvPool FFI (no padding).

def Runtime.Autograd.Cuda.Tape.avgPool2dPad {kH kW inH inW inC stride padding : ℕ} (h1 : kH ≠ 0) (h2 : kW ≠ 0) (t : Tape) (xId : ℕ) : Result (Tape × ℕ)

AvgPool2D via ConvPool FFI (with symmetric padding).

def Runtime.Autograd.Cuda.Tape.avgPool {d C : ℕ} {inSpatial kernel stride padding : Vector ℕ d} (hKernel : ∀ (i : Fin d), kernel.get i ≠ 0) (t : Tape) (xId : ℕ) : Result (Tape × ℕ)

N-D average pooling (CUDA) via ConvPool FFI (rank $\le 8$).