Native execution of generated custom operations

CUDA source is generated from typed expressions, not accepted as caller-provided text. NVRTC compiles it with the native bridge's fixed floating-point policy. The bridge caches a bounded number of modules per process, keys them by source and context, and launches on LibTorch's current stream. Input buffers and the module remain alive until the bounds record is checked.

This is an explicit foreign-code boundary, not a Lean theorem about NVRTC or device execution. LibTorch continues to own tensor storage and its established numerical operations. CPU-only builds resolve the same extern symbols but report an ordinary IO error instead of executing CUDA.

def NN.Kernel.Internal.runBytes {α : Type} (scalar : Scalar α) (expr : Expr α [Ty.index] Ty.scalar) (inputs : Array ByteArray) (count : UInt64) : IO ByteArray

Execute with complete scalar encodings. Wide binary values never pass through native floats.

def NN.Kernel.Internal.runBuffers {α : Type} (format : Cuda.Format) (bits : α → UInt64) (expr : Expr α [Ty.index] Ty.scalar) (inputs : Array Runtime.Autograd.LibTorch.Buffer) (count : UInt64) : IO Runtime.Autograd.LibTorch.Buffer

Run a generated operation on existing resident binary32 buffers.

Inputs are borrowed and never mutated. Bounds errors and compilation failures are returned before an output buffer is exposed. This helper is binary32-specific; other precisions use tensor execution.