Trusted CUDA Runtime Boundary

This module contains the opaque CUDA buffer type used by the native runtime. Buffers are created by explicit FFI allocation/copy functions. The nonemptiness witness below is only what Lean needs to declare extern functions returning Buffer; it is not a default CUDA allocation and should not be used as one.

opaque Runtime.Autograd.Cuda.BufferImpl : NonemptyType

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

def Runtime.Autograd.Cuda.Buffer : Type

Runtime representation used for native CUDA buffer handles.

The NonemptyType wrapper is Lean's standard representation for external resources: it gives extern declarations a nonempty result type while preserving reference-counting information in compiled code. The underlying value is still created only by the native buffer constructors.

instance Runtime.Autograd.Cuda.instNonemptyBuffer : Nonempty Buffer