LibTorch Backend Capsules

Maintained CUDA primitives implemented with LibTorch ATen tensor operations.

TorchLean owns tape traversal and selects each local VJP. Native forward and backward routines execute without recording a LibTorch autograd graph. The wrappers remain a foreign implementation boundary: shape/layout guards and named regression suites are engineering evidence, not Lean proofs of ATen, its dependencies, or compiled execution. Numerical reductions retain implementation-defined ordering. The CPU/reference capsules and their mathematical contracts are separate.

Local VJP ownership follows Engine.LibTorch.Ops: .torchLeanTape means Lean composes the derivative from numerical primitives; .backendVJP means it calls a native backward primitive. Both retain the LibTorch provider and TorchLean's global tape.

def NN.Backend.LibTorch.Internal.coverage (op : BackendOp) (vjp : Bool := false) : Option String

Retained CUDA comparisons, by operation. An absent entry leaves an explicit trust boundary.

def NN.Backend.LibTorch.Internal.evidence (op : BackendOp) (vjp : Bool := false) : ContractEvidence

Record the available comparison, or the untested native agreement being assumed.

def NN.Backend.LibTorch.Internal.trustLevel (op : BackendOp) (vjpMode : VJPMode) : TrustLevel

checked when the forward pass, and the VJP if there is one, have a retained CUDA comparison; otherwise an explicit trusted boundary.

def NN.Backend.LibTorch.Internal.capsule (name : String) (op : BackendOp) (valueSummary vjpSummary : String) (vjpMode : VJPMode) : KernelCapsule

Describe a maintained LibTorch primitive and the evidence required by its runtime contract.

def NN.Backend.LibTorch.Internal.pointwiseCapsule (op : BackendOp) (vjpMode : VJPMode) : KernelCapsule

Build the standard LibTorch CUDA capsule for a pointwise operation.

def NN.Backend.LibTorch.Internal.reductionCapsule (op : BackendOp) (vjpMode : VJPMode) : KernelCapsule

Build a LibTorch CUDA reduction capsule with implementation-defined reduction order.

def NN.Backend.LibTorch.Internal.accumulationCapsule (name : String) (op : BackendOp) (valueSummary vjpSummary : String) (vjpMode : VJPMode) : KernelCapsule

LibTorch CUDA kernel with an accumulation whose tree/order is selected by the implementation.

This covers matrix products, affine layers, convolutions, losses, and average pooling. ATen selects the accumulation implementation; the capsule does not promise the reference left fold. Deterministic execution settings do not strengthen this to a particular numerical schedule.

def NN.Backend.LibTorch.Internal.viewCapsule (op : BackendOp) (vjpMode : VJPMode) : KernelCapsule

Build the standard LibTorch CUDA capsule for a shape or layout transformation.

def NN.Backend.LibTorch.Internal.forwardOnlyCapsule (op : BackendOp) (valueSummary : String) : KernelCapsule

Build a LibTorch CUDA forward-only capsule with no registered reverse derivative.

def NN.Backend.LibTorch.matmul : KernelCapsule

LibTorch CUDA batched/matrix multiplication.

def NN.Backend.LibTorch.scaledMatmul : KernelCapsule

Scaled CUDA contractions with conservative range recovery from the original operands.

The recovery path synchronizes a flag and may run reference coefficient arithmetic on CPU. Neither this mixed execution path nor its VJP promises a fixed-left accumulation schedule.

def NN.Backend.LibTorch.softmaxMatmul : KernelCapsule

Lean-recorded normalized matrix product with conservative host range recovery.

def NN.Backend.LibTorch.relu : KernelCapsule

LibTorch CUDA ReLU activation.

def NN.Backend.LibTorch.gelu : KernelCapsule

LibTorch CUDA GELU activation.

def NN.Backend.LibTorch.add : KernelCapsule

LibTorch CUDA pointwise addition.

def NN.Backend.LibTorch.sub : KernelCapsule

LibTorch CUDA pointwise subtraction.

def NN.Backend.LibTorch.mul : KernelCapsule

LibTorch CUDA pointwise multiplication.

def NN.Backend.LibTorch.scale : KernelCapsule

LibTorch CUDA scalar multiplication.

def NN.Backend.LibTorch.abs : KernelCapsule

LibTorch CUDA pointwise absolute value.

def NN.Backend.LibTorch.sqrt : KernelCapsule

LibTorch CUDA pointwise square root.

def NN.Backend.LibTorch.clamp : KernelCapsule

LibTorch CUDA pointwise interval clamp.

def NN.Backend.LibTorch.max : KernelCapsule

LibTorch CUDA pointwise maximum.

def NN.Backend.LibTorch.min : KernelCapsule

LibTorch CUDA pointwise minimum.

def NN.Backend.LibTorch.sigmoid : KernelCapsule

LibTorch CUDA pointwise sigmoid.

def NN.Backend.LibTorch.silu : KernelCapsule

SiLU value and local gradient use the shared ATen adapter; TorchLean owns traversal.

def NN.Backend.LibTorch.tanh : KernelCapsule

LibTorch CUDA pointwise hyperbolic tangent.

def NN.Backend.LibTorch.softplus : KernelCapsule

LibTorch CUDA pointwise softplus.

def NN.Backend.LibTorch.exp : KernelCapsule

LibTorch CUDA pointwise exponential.

def NN.Backend.LibTorch.sin : KernelCapsule

LibTorch CUDA sine, with angles measured in radians.

def NN.Backend.LibTorch.cos : KernelCapsule

LibTorch CUDA cosine, with angles measured in radians.

def NN.Backend.LibTorch.log : KernelCapsule

LibTorch CUDA pointwise natural logarithm.

def NN.Backend.LibTorch.inv : KernelCapsule

LibTorch CUDA pointwise reciprocal.

def NN.Backend.LibTorch.div : KernelCapsule

Native quotient arithmetic with TorchLean's quotient-rule VJP.

def NN.Backend.LibTorch.neg : KernelCapsule

Native scalar negation with TorchLean's sign-reversing VJP.

def NN.Backend.LibTorch.safeLog : KernelCapsule

LibTorch CUDA smooth logarithm surrogate log (softplus x + epsilon).

def NN.Backend.LibTorch.logSoftmax : KernelCapsule

LibTorch CUDA log-softmax reduction and normalization.

def NN.Backend.LibTorch.softmax : KernelCapsule

LibTorch CUDA row/axis softmax kernels.

def NN.Backend.LibTorch.hardMaskedSoftmax : KernelCapsule

LibTorch CUDA hard-masked row softmax.

def NN.Backend.LibTorch.topKMask : KernelCapsule

LibTorch CUDA top-k routing mask.

def NN.Backend.LibTorch.reduceSum : KernelCapsule

LibTorch CUDA sum reduction.

def NN.Backend.LibTorch.reduceMean : KernelCapsule

LibTorch CUDA arithmetic-mean reduction.

def NN.Backend.LibTorch.reshape : KernelCapsule

LibTorch CUDA shape-preserving reshape view.

def NN.Backend.LibTorch.permute : KernelCapsule

LibTorch CUDA axis permutation.

def NN.Backend.LibTorch.broadcast : KernelCapsule

LibTorch CUDA tensor broadcasting.

def NN.Backend.LibTorch.concat : KernelCapsule

LibTorch CUDA tensor concatenation.

def NN.Backend.LibTorch.slice : KernelCapsule

LibTorch CUDA contiguous tensor slice.

def NN.Backend.LibTorch.gather : KernelCapsule

LibTorch CUDA indexed gather.

def NN.Backend.LibTorch.scatterAdd : KernelCapsule

LibTorch CUDA indexed scatter-add.

def NN.Backend.LibTorch.randUniform : KernelCapsule

LibTorch CUDA seeded uniform-random tensor generation.

def NN.Backend.LibTorch.bernoulliMask : KernelCapsule

LibTorch CUDA seeded Bernoulli-mask generation.

def NN.Backend.LibTorch.layerNorm : KernelCapsule

LibTorch CUDA layer normalization.

def NN.Backend.LibTorch.batchNorm : KernelCapsule

LibTorch CUDA batch normalization.

def NN.Backend.LibTorch.conv : KernelCapsule

LibTorch CUDA generic channel-first convolution.

def NN.Backend.LibTorch.convTranspose : KernelCapsule

LibTorch CUDA generic channel-first transpose convolution.

def NN.Backend.LibTorch.maxPool : KernelCapsule

LibTorch CUDA max pooling, skipping padded cells and retaining the first row-major winner.

def NN.Backend.LibTorch.smoothMaxPool : KernelCapsule

LibTorch CUDA smooth max pooling.

def NN.Backend.LibTorch.avgPool : KernelCapsule

LibTorch CUDA average pooling.

def NN.Backend.LibTorch.linear : KernelCapsule

LibTorch CUDA linear layer.

def NN.Backend.LibTorch.mseLoss : KernelCapsule

LibTorch CUDA mean-squared-error loss.

def NN.Backend.LibTorch.crossEntropy : KernelCapsule

Weighted logits cross-entropy and both local VJPs, evaluated without LibTorch autograd.

def NN.Backend.LibTorch.distill : KernelCapsule

Teacher-logit cross-entropy and its student VJP, evaluated with ATen operations under TorchLean's tape. No LibTorch autograd graph is recorded.

def NN.Backend.LibTorch.fftFno : KernelCapsule

LibTorch numerical FFTs with Lean adjoints and spectral-layer composition.

def NN.Backend.LibTorch.selectiveScan : KernelCapsule

LibTorch CUDA selective scan kernels.

def NN.Backend.LibTorch.attention : KernelCapsule

Lean-composed attention over LibTorch numerical primitives.

TorchLean composes forward and the local VJP and owns the saved Q/K/V and probability buffers. The existing capsule identity is retained for routing and audits. No native attention context or fused-provider selection is involved; full score matrices require quadratic sequence memory. Numerical primitives execute without a LibTorch autograd graph or a fixed reduction schedule.

def NN.Backend.LibTorch.capsules : Array KernelCapsule

LibTorch CUDA primitive contracts.