Backend Profiles

Named backend profiles bundle the choices that should move together: build availability, kernel-selection policy, and the ordered capsule modules. This gives downstream APIs one object to pass around instead of separately threading device availability, provider preference, and permission to accept trusted-boundary evidence.

structure NN.Backend.BackendProfile : Type

A named kernel-selection profile for one device.

• name : String

  Human-readable profile name used in diagnostics and reports.

• policy : KernelPolicy

  Device, provider preference, assurance policy, and VJP ownership.

• availability : Availability

  Devices and providers the build declares available to planning.

• capsuleModules : Array Registry.CapsuleModule

  Capsule modules used to construct and validate the profile's planning registry.

@[instance_reducible]

instance NN.Backend.instReprBackendProfile : Repr BackendProfile

def NN.Backend.instReprBackendProfile.repr : BackendProfile → ℕ → Std.Format

def NN.Backend.BackendProfile.withCapsuleModules (p : BackendProfile) (modules : Array Registry.CapsuleModule) : BackendProfile

Extend a profile with operation/provider capsule modules without changing model semantics, availability, or assurance policy.

A new contribution replaces an existing module with the same name. Duplicate names within modules are still rejected when the profile is planned.

def NN.Backend.BackendProfile.registry (p : BackendProfile) : Array KernelCapsule

Capsule registry selected by the profile.

def NN.Backend.BackendProfile.planOps (p : BackendProfile) (ops : Array BackendOp) : Except String KernelPlan

Select capsules using the profile registry, availability, and kernel policy.

def NN.Backend.BackendProfile.planGraphNodes (p : BackendProfile) (g : IR.Graph) : Except String IR.GraphKernelPlan

Select a capsule for every runtime-relevant IR node.

def NN.Backend.BackendProfile.acceptGraph (p : BackendProfile) (g : IR.Graph) : Except String GraphKernelPlanResult

Plan, group, and contract-check a graph under the profile.

def NN.Backend.BackendProfile.checkedCpu : BackendProfile

Maintained portable CPU/reference profile with runtime guards and regression evidence.

def NN.Backend.BackendProfile.checkedCuda : BackendProfile

Strict LibTorch CUDA profile with TorchLean tape traversal and selected local VJPs.

Only capsules with retained regression evidence and runtime guards are admitted. Operations whose dedicated CUDA checks were removed require libTorchCuda or an explicit external policy. No LibTorch autograd graph is recorded.

def NN.Backend.BackendProfile.libTorchCuda : BackendProfile

Default GPU profile, admitting explicitly recorded LibTorch implementation assumptions.

Runtime guards still check the bridge. Numerical comparisons are named only for operations covered by the retained suite; the other capsules declare their external trust boundary. Use checkedCuda to reject those untested operations instead.

def NN.Backend.BackendProfile.maintainedForDevice? : Device → Option BackendProfile

Maintained execution profile for a device, when TorchLean currently provides one.

Other named devices remain expressible through caller-supplied profiles. They are not silently converted into profiles with empty registries.

def NN.Backend.BackendProfile.hasDeviceCapsule (profile : BackendProfile) : Bool

Whether this profile registers at least one capsule for its selected device.