Attention Backend Capsules

Attention is the first place where the backend-contract distinction matters in practice.

The proof-facing FlashAttention spec and every registered runtime provider use hard-mask semantics: blocked entries have exactly zero softmax numerator. Additive attention biases are a separate operation and are never used to encode a boolean mask.

def NN.Backend.Attention.scaledDotProductOp : BackendOp

Shared op tag for scaled dot-product attention capsules.

def NN.Backend.Attention.torchLeanComposed : KernelCapsule

Composed TorchLean attention path: slower, but aligned with the hard-mask spec.

def NN.Backend.Attention.nativeFlashAttention : KernelCapsule

Native fused attention path: faster than the composed fallback, still a CUDA runtime boundary.

def NN.Backend.Attention.libTorchSDPAForward : KernelCapsule

LibTorch SDPA forward provider while TorchLean keeps the graph/tape boundary.

def NN.Backend.Attention.libTorchSDPAAutograd : KernelCapsule

LibTorch SDPA provider where LibTorch also owns the local autograd VJP.

def NN.Backend.Attention.cudaCandidates : List KernelCapsule

Candidate capsules in default CUDA planner order.

def NN.Backend.Attention.cudaCandidatesWithLibTorch : List KernelCapsule

Candidate capsules when the optional LibTorch backend is enabled by policy/config.

def NN.Backend.Attention.cudaUsesNativeFlash (c : KernelCapsule) : Except String Bool

Runtime implementation selector for CUDA attention.

true means call the fused native CUDA attention kernels. false means use the composed TorchLean expression (bmm -> softmax -> bmm) on the CUDA tape. External providers such as LibTorch intentionally fail here until their runtime bridge is wired through an explicit capsule.