Pure specifications for CUDA float32 kernels #
This file is the proof layer companion to NN.Runtime.Autograd.Engine.LibTorch.*.
The LibTorch CUDA backend is an FFI boundary. These theorems describe explicit Lean functions; applying them to a compiled native operation requires a refinement contract. The interface has three layers:
- Pure Lean kernel specs in this file: row-major indexing, elementwise maps, fixed-order reductions, gather/scatter, and batched matmul are ordinary Lean functions over finite indices.
- Scalar float32 facts from
Float32Contract: if native result bits matchExecFloat.Binary 8 23, then the existingconfigured binary32 → FP32-on-ℝtheorems apply. - Native validation / trust boundary: LibTorch, its CUDA dependencies, compiler flags, GPU hardware, and driver behavior are validated by tests and documented assumptions, not proved by Lean.
This split is deliberate. It lets us prove the algorithm/indexing contracts that TorchLean owns, without claiming that the Lean kernel can inspect NVIDIA's compiler, runtime, or device ISA.
External references for the assumptions named here:
- IEEE 754-2019 defines binary32 arithmetic and special values: https://standards.ieee.org/ieee/754/6210/
- NVIDIA CUDA C Programming Guide documents the CUDA execution/memory model: https://docs.nvidia.com/cuda/cuda-c-programming-guide/
- ATen supplies batched matrix multiplication and selects its native implementation: https://docs.pytorch.org/docs/stable/generated/torch.bmm.html
- PyTorch's tensor docs are a useful user-facing analogue for row-major/strided tensor operations: https://pytorch.org/docs/stable/tensors.html
Flat row-major buffers #
A pure Lean view of a contiguous float32 buffer of length n.
Native LibTorch.Buffer is opaque and mutable outside Lean. FlatBuffer n is the spec counterpart:
every valid linear index has a reference scalar value.
Instances For
A native-result buffer represented only by raw binary32 bits.
Instances For
Reinterpret a native bit buffer as reference ExecFloat.Binary 8 23 values.
Instances For
Total lookup for flat-buffer specs that decode indices from arithmetic.
Well-formed kernel preconditions should make the in-bounds branch fire. The fallback keeps the spec total in Lean, and later layout proofs can discharge the bounds separately.
Instances For
Extract reference bits pointwise.
Instances For
A buffer of reference scalars survives a round trip through its bits.
And a buffer of bits survives a round trip through reference scalars, so kernel specs may be stated on whichever side reads better and transported to the other.
Elementwise kernels #
Pure spec for a unary elementwise CUDA kernel.
Instances For
Pure spec for a binary elementwise CUDA kernel.
Instances For
Elementwise addition reference spec.
Instances For
Elementwise multiplication reference spec.
Instances For
Elementwise division reference spec.
Instances For
Elementwise square-root reference spec.
Instances For
If every native result bit agrees with reference addition, the whole native elementwise-add buffer
agrees extensionally with addSpec.
Elementwise multiplication version of fromNativeBitsBuffer_eq_addSpec_of_bits.
Elementwise division version of fromNativeBitsBuffer_eq_addSpec_of_bits.
Elementwise square-root version of fromNativeBitsBuffer_eq_addSpec_of_bits.
Pointwise real-error bound inherited by an elementwise-add buffer after bit agreement.
Pointwise real-error bound inherited by a native elementwise-multiply buffer after bit agreement.
Pointwise real-error bound inherited by a native elementwise-division buffer after bit agreement.
Pointwise real-error bound inherited by a native elementwise-square-root buffer after bit agreement.
Fixed-order reductions #
Sequential left-fold reduction over a flat buffer.
This is a deterministic algorithmic spec, not a claim about CUDA atomics. Native atomic reductions
only refine this spec under an additional ordering/agreement assumption. The deterministic
settings in Controls require repeatable algorithms; they do not establish this sequential order
or discharge the agreement assumption.
Instances For
Explicit assumption package for a native reduction implementation.
Use this when a native CUDA reduction has been proved or validated to agree bitwise with
reduceSumLeftSpec. A fixed reduction tree can be deterministic without matching this left fold;
enabling deterministic algorithms alone does not supply this contract.
Instances For
Native fixed-order reduction inherits the reduceSumLeftSpec reference value.
Gather/scatter indexing #
Scatter-add a length-k value buffer into a length-n input buffer.
Repeated indices are accumulated in increasing source-index order. This mirrors the mathematical contract of scatter-add; a native parallel implementation must separately justify or validate its accumulation order when bitwise reproducibility matters.
Instances For
Batched row-major matrix multiplication #
Linear index for either BMM input, viewed as row-major (batch, rows, cols) storage.
Instances For
Pure row-major batched matrix multiplication spec.
For each output element C[b,i,j], this folds over k = 0..n-1 using ExecFloat.mul followed by
ExecFloat.add. This fixes a specific accumulation order. LibTorch may use a different
tree/FMA strategy, so bit-for-bit agreement with this spec is an explicit native contract, not a
free theorem.
Instances For
Agreement assumption for a native BMM implementation.
The scalar result bits must match bmmSpec at every output element. This is stronger
than "numerically close": it is the bitwise contract needed to reuse exact ExecFloat.Binary 8 23
proofs.
For a LibTorch implementation this assumption includes:
- row-major TorchLean buffers are interpreted with the intended tensor dimensions;
- the accumulation tree/FMA behavior agrees with the selected reference spec;
- input and output strides match
(batch,m,n),(batch,n,p), and(batch,m,p)row-major layout.
Instances For
Native BMM inherits the pure row-major bmmSpec when the bitwise agreement contract holds.