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.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

Lean requires a nonempty result type for opaque extern declarations such as Buffer.zeros : UInt32 -> Buffer.

This witness is part of the FFI trust boundary. It does not allocate a runtime buffer; real CUDA buffers still come only from explicit native constructors/copy operations.