Maintained CUDA attention selection

The default profile selects a capsule declaring Lean-composed attention over LibTorch primitives. Its declared VJP ownership matches the TorchLean tape policy; reduction order remains implementation-defined. This does not select or verify an ATen flash, efficient, cuDNN, or math implementation.

theorem NN.Backend.BackendProfile.checkedCuda_attention_choice : chooseCapsuleFor? checkedCuda.policy BackendOp.attention (checkedCuda.availability.filterCapsules checkedCuda.registry) = some LibTorch.attention

The maintained CUDA registry and policy select the Lean-composed LibTorch attention capsule.

theorem NN.Backend.BackendProfile.checkedCuda_attention_plan {plan : KernelPlan} (hplan : checkedCuda.planOps #[BackendOp.attention] = Except.ok plan) : plan.kernels = #[{ op := BackendOp.attention, capsule := LibTorch.attention }]

A successful default attention plan retains exactly the selected Lean-composed capsule.

theorem NN.Backend.BackendProfile.checkedCuda_attention_contract : LibTorch.attention.provider = Provider.libTorch ∧ LibTorch.attention.vjpMode = VJPMode.torchLeanTape ∧ checkedCuda.policy.vjpMode = VJPMode.torchLeanTape ∧ KernelCapsule.matchesVJP checkedCuda.policy LibTorch.attention = true ∧ LibTorch.attention.numericalPolicy.reduction = ReductionPolicy.implementationDefined

The LibTorch attention capsule, which checkedCuda_attention_choice selects, declares a Lean-composed local VJP compatible with the TorchLean tape request. Its numerical policy does not promise a fixed reduction order.