Building With LibTorch🔗

An ordinary CPU build links one unavailable-backend shim and needs no LibTorch SDK. It lets CPU users import the same Lean modules, but cannot open native CUDA sessions. A CUDA build needs a CUDA-enabled LibTorch SDK:

Use device := gpu in Lean and --device gpu on the command line. Currently these select CUDA through LibTorch, the supported GPU target. For a supported native scalar carrier, an unavailable runtime is an error. Ordinary model sessions use the CPU tape for carriers without native tensor support, with a diagnostic and without losing precision. Custom computations also support configured binary formats, including binary128 values and gradients recorded on the same GPU tape. The custom computations chapter explains which operations we can record. Types outside the custom GPU interface use CPU with a diagnostic. Neither path hides compilation or execution errors behind a fallback. Use cuda to name the device explicitly; the default plain build still runs on CPU.

scripts/lake.sh -Kcuda=true \
  -Klibtorch_home=/path/to/libtorch build

Run this command from the repository root. Replace the path with the SDK directory containing include, lib, and share/cmake/Torch/TorchConfig.cmake. The builder also accepts TORCHLEAN_LIBTORCH_HOME; without either setting it looks for libtorch/ in the repository.

The build compiles TorchLean's C++ adapter and uses the selected SDK's CMake package for compiler flags, C++ ABI, and library dependencies. ATen supplies the model-operation kernels; custom computations also need the CUDA toolkit's NVRTC and driver libraries. Keep the same SDK selection on later build, exe, and env commands. The build helper records SDK and compiler inputs so that a changed native configuration cannot silently reuse an incompatible adapter.

Compilation and session creation answer different questions. A linked adapter still needs a visible, supported GPU to open a CUDA session. A CPU build does not execute the CUDA adapter, so its success provides no execution evidence about that backend.

To run two optimizer steps and print the selected kernel contracts:

scripts/lake.sh -Kcuda=true \
  -Klibtorch_home=/path/to/libtorch exe torchlean quickstart_mlp \
  --device cuda --steps 2 --seed 2026 --show-backend

The report identifies capsules such as libtorch.matmul, libtorch.add, and libtorch.relu, together with the evidence for their contracts. The model description contains two linear layers. Each becomes a sequence of reshapes, permutations, matrix multiplications, broadcasts, and additions, so the report names operations below the level of a whole layer. Each capsule describes the implementation selected for an operation; the report is not a trace of native calls or kernel launches. The reported numerical field is the reduction policy; a native accumulation is marked implementation-defined so that a fixed-left range certificate cannot be applied to it.

Two linear layers can reuse the same matmul capsule, and one operation can launch more than one ATen kernel. The report's row count therefore measures neither layers nor launches. Measuring speed requires timing the workload with its SDK, shapes, device, and runtime settings recorded.

Linear Layer Execution🔗

For an unbatched input x : [2] and weight W : [8,2], the eager CUDA path proceeds roughly as:

typed Tensor α [2]
    ↓ upload / existing CUDA handle
opaque contiguous buffer retaining its binary32 or binary64 dtype
    ↓ reshape and matrix-layout preparation
libtorch.matmul
    ↓ broadcast bias [8] to output shape
libtorch.add
    ↓
typed runtime Tensor α [8]

In this path, the weight has eight rows of two elements. Multiplication turns the two input coordinates into eight outputs, and the final addition uses one bias for each output. The Lean wrapper knows these logical shapes and element counts. The device buffer is opaque; Lean does not inspect its contents by reducing a theorem. Before each FFI call, wrappers check the conditions they can observe:

• the session really targets CUDA;

• the selected capsule implements the requested operation;

• flat lengths match the logical shapes;

• every shape axis, runtime index, and element count fits the UInt32 CUDA ABI;

• ranks, axes, strides, and operation-specific dimensions are supported.

Shape-erased values, output seeds, and supplied gradients pass through SomeBuffer.validate before shape-derived indexing. Convolution and pooling also check spatial products independently, so a zero channel dimension cannot hide an overflowing spatial shape. Their forward wrappers validate the native output length immediately after the FFI returns, before storing the result on the tape.

Those checks prevent many ABI and memory errors. They do not prove that ATen and its compiled kernels compute the correct arithmetic expression.

The backward shapes make the same division of responsibility concrete. If the output cotangent is δ : [8], the input cotangent has shape [2] and is mathematically Wᵀδ. The weight cotangent has shape [8,2], with entry δ[i] * x[j], and the bias cotangent is δ itself. These formulas explain which operands backward must retain. A buffer with the right length is necessary for all three computations, but length alone cannot show that the right operands or transpose flags were used.

For a concrete row, take weights [1, 2], input [0.25, -0.75], and bias 0.1. That neuron's preactivation is -1.15. With cotangent one, its contribution to the input gradient is [1, 2] and its weight gradient is [0.25, -0.75]. If the next operation is ReLU, however, the negative preactivation makes the incoming cotangent zero. The tape must compose those local rules in the right order to obtain the model's gradient.

Kernel Capsules🔗

A KernelCapsule is the audit record for one operation-provider pair:

-- The record keeps dispatch identity separate from the
-- evidence for each obligation.
structure KernelCapsule where
  name             : String
  op               : BackendOp
  provider         : Provider
  device           : Device
  trustLevel       : TrustLevel
  supportsForward  : Bool
  vjpMode          : VJPMode
  shapeContract    : ContractDescriptor
  layoutContract   : ContractDescriptor
  valueContract    : ContractDescriptor
  vjpContract      : ContractDescriptor
  numericalPolicy  : NumericalPolicy

The source gives two fields defaults omitted from this listing: supportsForward defaults to true and vjpMode to .none. A capsule that leaves these fields at their defaults therefore claims forward execution and no backward support. Registering it still requires evidence for the forward claim.

The four descriptors separate shape, storage layout, forward values, and backward values. The registered LibTorch matmul capsule shows how each obligation is recorded:

libtorch.matmul
shape: guarded at runtime by LibTorch bridge size/rank checks at the Lean/native boundary
layout: guarded at runtime by LibTorch bridge dtype, device, contiguity, and element-count checks
value: covered by test suite NN.Tests.Runtime.Cuda.Attention
vjp: covered by test suite NN.Tests.Runtime.Cuda.Attention

Every claim in that record is paired with its evidence. Shape and layout name the runtime check that runs at the boundary. Value and VJP name NN.Tests.Runtime.Cuda.Attention. These entries give two different kinds of assurance: a guard checks the current call, while a test suite compares results on its selected cases. Printing a suite's name does not execute it or certify that a particular build passed. There is no theorem entry claiming that ATen refines the specification. The implementationDefined reduction policy further limits which arithmetic certificates can apply, as we will see below.

-- Binding compares these declared identities before calling
-- the stored IO action.
structure KernelHandler (β : Type) where
  name     : String
  op       : BackendOp
  provider : Provider
  device   : Device
  execute  : KernelCapsule → IO β

structure ExecutableKernel (β : Type) where
  capsule             : KernelCapsule
  handler             : KernelHandler β
  operation_matches   : handler.op = capsule.op
  provider_matches    : handler.provider = capsule.provider
  device_matches      : handler.device = capsule.device

capsule : libtorch.matmul @ cuda
handler : reference_cpu.matmul @ cpu
bindable: false

as registered : true
evidence moved: false
planner admits: false

Planning, Selection, And Execution🔗

Selection proceeds from descriptions to an executable call:

registry
  all known capsule descriptions
       ↓ profile + availability + contract check
accepted plan
  capsules allowed under this policy
       ↓ bind matching typed handler
executable kernel
  operation/provider/device identities agree
       ↓ provider-aware runtime dispatch
executed operation
  the native symbol actually called

At the first transition, BackendProfile.acceptGraph exposes an AcceptedGraphKernelPlan only after planning, grouping, and the contract check accept every obligation. Binding then checks the handler identities shown above. Neither step probes the hardware: a profile's Availability declares which devices and providers planning may consider, while CUDA session creation calls LibTorch.Buffer.requireNativeRuntime to distinguish native CUDA, a native build with no visible GPU, and a build without LibTorch.

We can inspect profiles and plans on a machine with no GPU. The default profiles are:

profile=checked_cpu device=cpu assurance=checked vjp=torchlean-tape
profile=libtorch_cuda device=cuda assurance=external vjp=torchlean-tape

Both profiles retain TorchLean's tape. The default GPU profile admits explicitly recorded LibTorch assumptions for operations without retained CUDA comparisons. Tested operations name their comparison source. BackendProfile.checkedCuda remains available when we want to reject untested operations rather than accept that external boundary.

The profile describes who assembles and traverses the whole backward computation. Each capsule also records how one node computes its contribution. For matmul, Lean composes the two matrix products in the local derivative, so both entries say vjp=torchlean-tape. An operation such as convolution uses vjp=backend-vjp because its local rule calls a native backward primitive.

The CUDA matmul plan can also be printed on this CPU build:

profile=checked_cuda device=cuda assurance=checked vjp=torchlean-tape
trusted-external capsules: none
  matmul: libtorch.matmul provider=libtorch trust=checked vjp=torchlean-tape reduction=implementation-defined
    shape: shape safety for matmul; guarded at runtime by LibTorch bridge size/rank checks at the Lean/native boundary
    layout: libtorch-cuda-view layout compatibility for matmul; guarded at runtime by LibTorch bridge dtype, device, contiguity, and element-count checks
    value: matmul forward refines its TorchLean semantics; covered by test suite NN.Tests.Runtime.Cuda.Attention
    vjp: matmul torchlean-tape VJP refines its TorchLean semantics; covered by test suite NN.Tests.Runtime.Cuda.Attention

The report names two runtime guards and two test suites. Its checked label must be read together with those fields; it does not mean that matmul's native implementation has been proved correct. The line trusted-external capsules: none means that no selected capsule has the trustedExternal trust level. That list does not enumerate foreign code: the checked LibTorch capsule still calls ATen. ATen, its dependencies, and compiled execution remain outside the Lean proof. The value contract has no theorem variant to select.

Availability and dispatch are checked at different points:

1. a plan rejects providers marked unavailable in its supplied availability metadata;

2. provider-aware wrappers reject a selected provider they have not wired up.

CUDA wrappers, including attention, require the LibTorch provider. If a profile selects an unwired provider, execution fails with an error. There is no hidden CPU fallback for an unsupported CUDA operation, because moving a tensor between devices behind the user's back would change both performance and the execution claim.

Runtime Availability Errors🔗

Build without native CUDA and request it:

# Show that a build without LibTorch rejects a requested
# CUDA session.
scripts/lake.sh build
scripts/lake.sh exe torchlean quickstart_mlp --device cuda --steps 1

Without LibTorch, session initialization rejects the request. The CLI's Device.cuda value describes the requested target, while LibTorch.Buffer.requireNativeRuntime probes whether this build can execute it.

Likewise, names such as metal, rocm, tpu, and trainium parse as devices so profiles and future integrations can describe them. The maintained profile lookup currently returns no runtime for those devices. Selecting one produces a clear “no maintained runtime profile” error rather than running on CPU.

The maintained profile lookup exposes that distinction directly:

cpu: checked_cpu
cuda: libtorch_cuda
metal: no maintained runtime profile
rocm: no maintained runtime profile
tpu: no maintained runtime profile

The return type of maintainedForDevice? is an Option: parsing a device name can succeed even when profile lookup returns none. Callers must handle that case, and maintained runtime entrypoints report the unsupported selection.

ATen And The CUDA Libraries🔗

For the maintained model operations, the CUDA provider is LibTorch. The adapter calls ATen, and ATen dispatches their implementations using the tensor shapes, dtype, device, and runtime settings. Vendor libraries such as cuBLAS, cuDNN, and cuFFT sit below that interface.

This makes the boundary easier to locate: the Lean wrapper states the operation, the C++ adapter expresses it through ATen, and the selected SDK supplies its kernels. A single ATen operator may perform several launches, and a TorchLean operation may require a composition of ATen operators. The capsule identifies the provider and contract; it does not report an exact kernel schedule or predict its speed.

Maintained CUDA Operations🔗

The eager CUDA tape currently covers elementwise arithmetic and activations, reductions and broadcasting, shape transforms, gather/scatter, dense and batched matrix multiplication, normalization and softmax, one-, two-, and three-dimensional convolution and transposed convolution, max/average/smooth-max pooling, attention, and spectral convolution. TorchLean records backward rules as tape nodes. Differentiable real FFT, inverse real FFT, and selective scan also have ATen routes, with generic differentiable reference implementations for interpreters that do not provide these runtime hooks.

Layer normalization and tanh-approximate GELU are examples of the distinction between semantics and scheduling. Each is one operation on the TorchLean tape, with a local forward rule and VJP. The adapter can use an upstream operation or compose its formula from tensor operations without changing who walks the tape. Matrix derivatives follow the same rule: TorchLean selects products such as A^\mathsf{T}B and AB^\mathsf{T}, and ATen evaluates them. Calling those products does not ask LibTorch autograd to reconstruct the model's graph.

Convolution, transposed convolution, max pooling, and average pooling follow LibTorch's one-, two-, and three-dimensional operator families. The adapter handles TorchLean's typed shapes and tape ABI, then delegates the numerical work and explicit backward operation to ATen. It does not emulate higher-dimensional kernels or repair ATen's selection rules. Smooth-max pooling is the one deliberate composition here because PyTorch has no corresponding primitive; it uses the same one-to-three spatial-rank boundary and accepts finite nonzero values of \beta in the input dtype, including negative values.

This list does not mean every TorchLean operation has a CUDA implementation. Provider-aware wrappers reject unsupported capsules and shapes; they do not copy a tensor to CPU and continue silently. The native source map on NN.Runtime.Autograd.Engine.LibTorch.Trusted identifies the Lean declarations and the corresponding implementation boundary. The CUDA adapter sources live under csrc/libtorch.

The registry gives the capsule count and identifies operations with no registered VJP:

registered: 55
forward only: 3
  libtorch.top_k_mask
  libtorch.rand_uniform
  libtorch.bernoulli_mask

The count includes attention alongside the other LibTorch operations.

Two of the forward-only entries create random uniform buffers and Bernoulli masks from a seed; they have no differentiable tensor inputs. The third is the top-k mask that routes tokens in a mixture of experts. It is piecewise constant, so its derivative is zero wherever it exists, and the gradient reaches the router through the kept probabilities instead.

Selective scan has a backward recurrence for its coefficients, inputs, and initial state. When coefficients are shared across tokens, their gradients accumulate across time. The eager CUDA path records that recurrence on the tape; generic interpreters compose the differentiable scalar and tensor operations.

For a diagonal scan, a time step has the form h[t] = A[t] * h[t-1] + B[t] * x[t], with products taken coordinatewise. Backward must account for an input's immediate contribution and its effect on later states. If A[t] or B[t] came from an input projection, returning their cotangents lets the surrounding tape continue through that projection. Treating them as constants would preserve the forward recurrence while dropping part of the model's derivative.

The Fourier route has a different bookkeeping issue. A real input of length n stores only n / 2 + 1 complex bins, represented by a final real/imaginary axis of length two. The inverse accepts n explicitly because lengths four and five both store three bins. Its normalization and conjugate completion are part of the operation, so its adjoint must include their scaling. The imaginary DC coordinate, and the imaginary Nyquist coordinate for even lengths, have zero contribution and derivative over the reals. Generic execution uses dense specification matrices; their zero-coefficient products still propagate NaN and infinity. The CUDA route uses ATen's Fourier operators. Matching the real-valued operation does not fix floating-point order or nonfinite-value behavior.

Spectral layers compose these transforms with frequency selection and learned channel mixing in Lean, then call the inverse transform. LibTorch supplies the FFT and tensor primitives; TorchLean retains model composition, the local reverse calculation, and the buffers needed by its tape.

The public nn.functional.rfft and nn.functional.irfft operations transform the last axis and preserve any leading batch dimensions. For example, a real tensor with shape [2, 3, 5] produces packed coefficients with shape [2, 3, 3, 2]: there are six independent length-five transforms, each storing three complex bins. Pass batch := [2, 3] and the positive-length witness; the inverse also takes n := 5. Both operations accept path := denseReference when you want the dense calculation explicitly. An empty batch is allowed, but the transform length must be positive.

Batched Attention🔗

A transformer block receives a tensor of shape (batch, tokens, modelDim). The mathematical operation applies the same attention layer to every batch entry, with shared projection matrices. TorchLean keeps that description in the specification and typed graph. Each sample is expressed through the existing attention node, so its forward map, JVP, and VJP are the same definitions used for unbatched attention.

The eager CUDA runtime schedules the work differently. It flattens (batch, tokens) for the four shared projections and folds (batch, head) into the batch axis of the matrix multiplications. LibTorch supplies the local native tensor computations. TorchLean retains the hard-mask semantics and sums the four projection-matrix gradients across the full batch.

The verifier lowers batched attention to the per-sample graph, while CUDA executes one batch-aware tape node. Regression tests compare the batched forward value, input gradient, and shared weight gradients with repeated single-sample attention. The comparison is runtime evidence; the ATen calls and native floating-point behavior remain covered by the capsule's stated boundary.

Shared weights are the reason the comparison must inspect parameter gradients as well as output values. Each batch entry contributes to the same projection matrix. A backward implementation that kept only the last sample's contribution could still produce correct forward values and input gradients. Summing those contributions is the layer's job; any division by batch size comes from the surrounding loss reduction and must not be added a second time inside attention.

Forward Values And Backward Ownership🔗

GPU attention is registered as LibTorch.attention and composed in Ops/Attention.lean. For Q, K, and V shaped (batch, n, d), Buffer.attentionForward takes an optional support mask, the dimensions, and a scale. It forms the scores, computes the probabilities P, and multiplies P by V. Its Except result contains both the output and P; the tape retains Q/K/V and P for backward.

Given output cotangent G, Buffer.attentionBackward composes the local rule in Lean:

\mathrm dP = GV^\mathsf{T},\qquad \mathrm dS = P \odot \left(\mathrm dP - \operatorname{rowsum}(P \odot \mathrm dP)\right),

\mathrm dQ = \mathrm{scale}\,\mathrm dS K,\qquad \mathrm dK = \mathrm{scale}\,\mathrm dS^\mathsf{T} Q,\qquad \mathrm dV = P^\mathsf{T}G.

The row sum is broadcast across each row. Masked positions contribute zero, and fully blocked rows have zero cotangents. Keeping the forward probabilities ensures that this rule uses the same softmax values as forward. LibTorch executes the matrix products and numerical primitives with gradient recording disabled; the tape owns and releases the saved buffers.

This implementation materializes the full score and probability matrices. With B batch entries, H heads, and n tokens, P alone contains BHn^2 values: 4BHn^2 bytes for Float32, or 8BHn^2 bytes for Float. Scores, backward temporaries, projections, and a mask add further storage. Doubling sequence length quadruples the probability storage. There is no fused attention selection or tiled-memory guarantee. Lean composition still needs value and VJP evidence for its native primitives.

Hard Attention Masks🔗

TorchLean's boolean attention meaning is:

true  = this key participates
false = this key has exactly zero softmax numerator

A fully blocked row returns zero. The CPU reference and CUDA composition preserve this convention. The CUDA path broadcasts the Boolean support mask over the folded batch-head axis and applies hard-masked softmax to the score rows.

Replacing blocked logits by a finite sentinel such as -1000 can fail when surviving logits are smaller than the replacement. If an allowed logit is -5000 and a blocked one is set to -1000, the blocked entry becomes the largest score in the row and takes almost all the weight:

finite sentinel : [0.000000, 1.000000]
hard mask       : [1.000000, 0.000000]

Position 0 is the only key allowed to participate. A hard mask removes the other entry from normalization, leaving weight one on the allowed key. The sentinel version includes both scores in softmax, where their difference makes the blocked key dominate; the allowed weight prints as zero. Large score differences can expose this failure; training duration alone does not imply them. Negative infinity expresses a hard support restriction, with a separate convention needed for fully blocked rows. A finite additive bias can approximate that restriction when the remaining score differences make the blocked weights negligible. PyTorch's attention interface supports both boolean masks and floating-point additive masks (Paszke et al. (2019)).

The specification also defines the result when no key participates:

[[0.268941, 0.731059, 0.000000], [0.000000, 0.000000, 0.000000]]

The first row renormalizes over the two surviving keys, and the blocked entry is exactly 0. The second row has no surviving keys and returns zeros rather than dividing by zero. Returning zero is the chosen convention; rejecting fully blocked rows is another possible API. Spec.hardMaskedSoftmaxSpec records the zero-row convention in its docstring. The attention regression cases compare the runtime routes against that same definition.

For scores one and two, the exponential ratio is 1 : exp(1), giving the first row's weights approximately 0.269 and 0.731. The attention VJP holds the Boolean mask fixed while differentiating the numerical inputs, including the defined all-blocked case.

The attention regression suite includes masked forward values, \mathrm dQ, \mathrm dK, \mathrm dV, and fully blocked rows. Those are tests of concrete cases. The pure FlashAttention theorem separately identifies its denotation with ordinary attention. The current named tiled definition delegates to the full attention formula and does not prove a separately implemented tiled online-softmax algorithm correct.

Reduction Order In The Numerical Contract🔗

Every capsule carries a NumericalPolicy, and the reduction field is the part the certificates actually consume. Compare the CPU reference capsule with the CUDA one for the same operation:

reference.matmul: reduction=fixed-left
libtorch.matmul: reduction=implementation-defined

fixed-left says the reference sums in one pinned order, so its result is reproducible and a proof may quantify over that fold. implementation-defined leaves the CUDA reduction tree to the implementation, including its block and warp geometry. A certificate for a fixed-left fold cannot assume that this kernel performs the same sequence of rounded additions.

Reduction order is one of several choices that affect native floating-point values:

• Hardware operations usually round to nearest-even, subject to instruction and library choices.

• Subnormal inputs may be preserved or flushed depending on hardware mode and kernel.

• Multiplication and addition may be contracted into FMA.

• Parallel reductions can choose a tree that differs from the pure interpreter's order.

The input and accumulator precision matter too. The LibTorch controls below let a run permit TF32 for matrix products or cuDNN convolutions, or request IEEE input precision. Those settings constrain eligible implementations; they do not specify every intermediate rounding or the reduction tree. A native result's repeatability, accuracy, and relationship to the real-valued specification are separate questions.

The reason a reduction tree matters at all is that floating-point addition is not associative:

(a+b)+c \ne a+(b+c).

With three decimal literals, changing the parentheses changes the stored result even though the default printer shows the same decimal text:

left  = 0.600000
right = 0.600000
equal = false
apart = 1 ulp

The equality check compares the stored values and returns false; the bit-pattern difference shows they are one ULP apart. Six printed digits hide that difference ((Goldberg, 1991)). FloatLib makes the format and rounding operations explicit; Float32 Soundness explains how those values connect to rounded-real error analysis.

This example uses Lean Float, so it demonstrates binary64 rounding rather than directly running the CUDA binary32 kernel. The same need to specify evaluation order applies to both formats. Here the positive finite results have adjacent bit patterns, making the subtraction a useful ULP count. It is not a general distance formula for arbitrary signed values, infinities, or NaNs.

To cover different reduction trees, a numerical certificate needs an error model that permits their different rounding steps, or a policy that fixes the steps it assumes.

Runtime Precision And Determinism🔗

The controls in LibTorch configure the linked SDK. Set them before opening concurrent work, and record their readbacks with a numerical experiment. This definition configures a run when called; elaborating it does not touch a GPU:

The adapter initializes matrix multiplication and cuDNN convolution with IEEE precision requested. setMatmulPrecision .tf32 and setConvPrecision .tf32 permit TF32 for the corresponding binary32 operations. These are runtime permissions, not changes to the tensor's stored dtype; binary64 buffers remain binary64. Neither .ieee nor .tf32 establishes agreement with a FloatLib evaluation or fixes every intermediate rounding step. Arbitrary FloatLib formats remain available to the numerical specifications and interpreters; these controls do not make CUDA tensors arbitrary-precision.

setDeterministic true requests strict deterministic algorithms and disables cuDNN benchmarking. An unsupported deterministic operation must report an error rather than silently proceed with a warning. The setting does not impose the reference left fold, guarantee equal bits across SDK versions or GPU models, or make seeded randomness unnecessary. setCuDNNBenchmark true is rejected while strict determinism is enabled. setCuDNNEnabled separately controls whether the native context may use cuDNN.

The distinction between repeatability and accuracy survives a deterministic implementation. Repeating a sum in one order can reproduce the same bits every time while differing from a sum in higher precision. To investigate that distinction, keep the input tensor and index map fixed, repeat the operation, and collect result bits rather than rounded decimal strings. Compare those results with a reference over the same stored inputs and state its precision. A count of distinct outputs measures repeatability; an error against the reference measures something else. Neither measurement on its own measures speed.

Reading CUDA Memory Usage🔗

The LibTorch allocator owns device storage and its reuse policy. TorchLean's counters answer a related but different question: which logical payloads and Lean buffer wrappers remain owned? Read both levels at the point in the workload whose lifetime matters:

liveBytes and peakBytes count logical payloads owned by TorchLean handles. A view can share storage with another handle, so these counts can count the same storage twice. Conversely, an ATen temporary or library workspace can own storage without a separate TorchLean handle. allocCount and freeCount count payload lifetimes, not calls to the CUDA allocator. The wrapper counters also include empty and explicitly released objects until Lean finalizes those wrappers. These ownership counters are process-wide.

allocatedBytes and reservedBytes come from the LibTorch allocator for the selected CUDA device. Allocations include library workspaces, such as a cuBLAS workspace, that can outlive every TorchLean handle. Zero ownership counters therefore need not imply zero allocated bytes. The corresponding peaks are peakAllocatedBytes and peakReservedBytes. Reservation includes storage retained for reuse, but subtracting allocated bytes does not give a promise of immediately reclaimable memory. deviceFreeBytes and deviceTotalBytes report the driver's view of that same device. Without LibTorch these device counters are zero. The fields are read separately, so concurrent activity can make the report differ from an atomic snapshot.

For example, retiring a temporary tensor can reduce allocated bytes while leaving reserved bytes unchanged. That is compatible with an allocator keeping storage for another operation. An attention tape node also retains Q/K/V and probabilities for backward; dropping an unrelated local handle does not retire those saved buffers. Reading only free device memory would conflate allocator reuse with values that the tape still needs.

An application can set the selected device's allocation limit and later release unused cache:

The fraction must be finite and lie in (0, 1]. It configures the upstream allocator's limit; it is neither a cache-only allowance nor a reservation against other processes. Read it back with getMemoryFraction, allowing for native byte granularity. It does not release live tensors.

emptyCache releases unused allocator blocks. Live parameters, optimizer state, saved forward state, and library workspaces remain allocated, so both allocated and reserved bytes may remain after the call. Calling it after every operation can throw away useful reuse. For timing a completed phase, Runtime.Autograd.LibTorch.synchronize waits for the selected device's work; record whether that synchronization is included in a measurement.

CUDA Test Coverage🔗

Build against the SDK selected for the run, then execute the maintained device checks:

export TORCHLEAN_LIBTORCH_HOME=/path/to/libtorch
scripts/lake.sh -Kcuda=true build
TORCHLEAN_REQUIRE_CUDA=1 scripts/lake.sh -Kcuda=true test
scripts/lake.sh -Kcuda=true lint

The retained CUDA suite checks buffer ownership, transfers, selected pointwise operations, softmax, attention, selective scan, FFTs, parameter sharing, and a small training run. Attention checks inspect forward values and input cotangents, including hard masks and fully blocked rows. Each check covers its specific inputs and configuration.

Convolution, pooling, normalization, and gather/scatter use LibTorch implementations. The maintained suite does not independently compare their GPU values and gradients with the Lean reference.

A capsule names its test source; it does not store a passing result for the current build. To assess a run, keep its complete test output with the revision, SDK, driver, GPU, and relevant settings. The chapter's executable planner examples and scalar calculations establish only what those examples evaluate.

Passing device checks establishes that their cases worked on the recorded configuration. A claim that ATen, its dependencies, the compiler, and the GPU refine every TorchLean specification would require a further argument. Those components remain part of the implementation boundary described in docs/TRUST_BOUNDARIES.md and in the capsule records.