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 flags such as "CUDA", "LibTorch enabled", and "trusted external allowed".

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

Checked native CUDA profile. External trusted providers are not admitted.

def NN.Backend.BackendProfile.libTorchForwardCuda : BackendProfile

LibTorch forward scaling profile.

LibTorch is allowed to provide selected forward values, but TorchLean still records the graph/tape boundary and does not hand local backward ownership to LibTorch autograd.

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.