Trusted CUDA Runtime Boundary

This module contains the opaque CUDA buffer type and the single inhabitance axiom needed to make the external FFI type usable from Lean. It is intentionally compact: all declarations here are part of the TorchLean trusted computing base for CUDA execution.

opaque Runtime.Autograd.Cuda.Buffer : Type

Opaque handle to a contiguous float32 buffer (CUDA device memory when built with -K cuda=true, otherwise a CPU stub buffer).

Implementation:

• CUDA: csrc/cuda/tensor/torchlean_cuda_tensor.cu
• CPU stub (default lake build): csrc/cuda/tensor/torchlean_cuda_tensor_stub.c

axiom Runtime.Autograd.Cuda.instNonemptyBuffer : Nonempty Buffer