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.

The rest of this docstring is the map from native translation units to the Lean modules that call them. DocGen documents Lean modules, not C or CUDA files, so the map lives here, on the module that is the trust boundary, rather than in a separate source browser.

Trust boundary

The CUDA backend crosses a C++/LibTorch FFI boundary. Lean does not prove the compiled native implementation correct. The trusted pieces include LibTorch and ATen, their CUDA libraries, compiler and runtime, GPU hardware, and Lean's external-object ABI and finalizers.

TorchLean retains its own tape and selected local VJPs. ATen computes tensor values and local backward operations with autograd recording disabled. Proof-facing kernel specifications, float32 agreement hypotheses, and graph semantics remain Lean definitions. Runtime regression and numerical parity tests provide evidence for a particular build and set of inputs.

Native source groups

• csrc/libtorch/torchlean_libtorch.h Shared boxed-buffer ABI, size checks, device guards, and the no-autograd call boundary. Lean modules: LibTorch.Trusted, LibTorch.Buffer, and LibTorch.

• csrc/libtorch/torchlean.cpp Shared implementation of storage ownership, allocation, transfers, seeded random values, runtime controls, tensor operations, and explicit backward calls through ATen. It implements elementwise operations, reductions, indexing, matrix multiplication, normalization, Fourier transforms, scans, and convolution/pooling. Lean composes attention in LibTorch.Ops.Attention and retains Q/K/V and probability buffers on its tape; the native buffer has no attention context. LibTorch owns the CUDA allocator; TorchLean's payload counters track logical ownership. Native buffers carry binary32 or binary64 according to the executable scalar type.

• csrc/libtorch/operations.h Common operation list used to generate LibTorch exports and unavailable-build signatures.

• csrc/libtorch/unavailable.c The same symbols for builds without LibTorch. The runtime status is .notLinked, IO calls return an error, and pure buffer operations abort with a message to rebuild with -K cuda=true. User CUDA sessions are rejected before any of them runs.

The GPU random stream is evaluated with ATen integer operations and checked against the seeded contract.

inductive Runtime.Autograd.LibTorch.Dtype : Type

Storage representation of a tape buffer. Encoded values retain a complete format descriptor on their handle, rather than narrowing to one of the native dtypes.

• float32 : Dtype
• float64 : Dtype
• encoded : Dtype

@[instance_reducible]

instance Runtime.Autograd.LibTorch.instReprDtype : Repr Dtype

def Runtime.Autograd.LibTorch.instReprDtype.repr : Dtype → Nat → Std.Format

@[instance_reducible]

instance Runtime.Autograd.LibTorch.instDecidableEqDtype : DecidableEq Dtype

def Runtime.Autograd.LibTorch.instBEqDtype.beq : Dtype → Dtype → Bool

@[instance_reducible]

instance Runtime.Autograd.LibTorch.instBEqDtype : BEq Dtype

instance Runtime.Autograd.LibTorch.instNonemptyDtype : Nonempty Dtype

def Runtime.Autograd.LibTorch.Dtype.bytes : Dtype → Nat

Bytes per native scalar. Encoded buffers require their format descriptor for a word width and cannot use the native checkpoint framing.

opaque Runtime.Autograd.LibTorch.BufferImpl : NonemptyType

Opaque handle to a contiguous, dtype-carrying CUDA buffer in csrc/libtorch/torchlean.cpp. Builds without -K cuda=true cannot create one.

def Runtime.Autograd.LibTorch.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.LibTorch.instNonemptyBuffer : Nonempty Buffer