Backend Profiles

Named backend profiles bundle the choices that should move together:

• target/build availability,
• execution configuration,
• capsule registry,
• graph lowering mode,
• and acceptance policy.

This gives downstream APIs one object to pass around instead of separately threading flags such as "CUDA", "LibTorch enabled", "trusted external allowed", and "coalesce adjacent graph nodes".

inductive NN.Backend.RegistryMode : Type

Which capsule registry a profile uses.

• default : RegistryMode
• withLibTorch : RegistryMode

@[implicit_reducible]

instance NN.Backend.instDecidableEqRegistryMode : DecidableEq RegistryMode

def NN.Backend.instReprRegistryMode.repr : RegistryMode → ℕ → Std.Format

@[implicit_reducible]

instance NN.Backend.instReprRegistryMode : Repr RegistryMode

def NN.Backend.RegistryMode.capsules : RegistryMode → List KernelCapsule

Capsule registry selected by a registry mode.

inductive NN.Backend.LoweringMode : Type

How graph-node plans are lowered to backend execution groups.

• singleton : LoweringMode
• coalesced : LoweringMode

@[implicit_reducible]

instance NN.Backend.instDecidableEqLoweringMode : DecidableEq LoweringMode

@[implicit_reducible]

instance NN.Backend.instReprLoweringMode : Repr LoweringMode

def NN.Backend.instReprLoweringMode.repr : LoweringMode → ℕ → Std.Format

structure NN.Backend.BackendProfile : Type

One named backend execution profile.

• name : String
• config : ExecutionConfig
• target : Target
• registryMode : RegistryMode
• loweringMode : LoweringMode
• acceptancePolicy : AcceptancePolicy

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

@[implicit_reducible]

instance NN.Backend.instReprBackendProfile : Repr BackendProfile

def NN.Backend.BackendProfile.availability (p : BackendProfile) : Availability

Planner capabilities declared by the profile target; runtime execution probes separately.

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

Capsule registry selected by the profile.

def NN.Backend.BackendProfile.planOps (p : BackendProfile) (ops : List BackendOp) : Except String ExecutionPlan

Plan operations using the profile registry, target, and execution config.

def NN.Backend.BackendProfile.gateOps (p : BackendProfile) (ops : List BackendOp) : Except String GateResult

Gate a planned operation sequence under the profile's acceptance policy.

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

Plan runtime-relevant IR nodes using the profile registry, target, and execution config.

def NN.Backend.BackendProfile.lowerGraphPlan (p : BackendProfile) (plan : IR.GraphExecutionPlan) : GraphLoweringPlan

Lower a graph-node execution plan according to the profile's lowering mode.

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

Plan, lower, and gate 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.checkedCpuTarget (os : OperatingSystem) (arch : Architecture := Architecture.unknown) : BackendProfile

Checked CPU/reference profile for a named operating system and architecture.

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.libTorchAutogradCuda : BackendProfile

Explicit LibTorch autograd scaling profile. Trusted external backward boundaries are visible.

def NN.Backend.BackendProfile.macOSCpu : BackendProfile

Checked macOS CPU/reference profile.

def NN.Backend.BackendProfile.windowsCpu : BackendProfile

Checked Windows CPU/reference profile. Used for CI bring-up before native Windows kernels exist.

def NN.Backend.BackendProfile.future (name : String) (device : Device) (target : Target) (backend : BackendPreference := BackendPreference.auto) (trustPolicy : TrustPolicy := TrustPolicy.checked) (vjpMode : VJPMode := VJPMode.torchLeanTape) (acceptancePolicy : AcceptancePolicy := AcceptancePolicy.strict) : BackendProfile

Construct a named target whose runtime capsules are not implemented yet.

def NN.Backend.BackendProfile.futureMetal : BackendProfile

Future Metal/MPS profile.

The target and device are named now, but the default registry has no Metal capsules yet. Planning a non-reference op under this profile therefore fails with a missing-capsule error instead of falling back silently to CUDA or CPU.

def NN.Backend.BackendProfile.futureRocm : BackendProfile

Future ROCm profile. It is a named planning target until HIP/ROCm capsules are added.

def NN.Backend.BackendProfile.futureWasm : BackendProfile

Future WebGPU/WASM profile. It is a named planning target until WebGPU capsules are added.

def NN.Backend.BackendProfile.futureTpu : BackendProfile

Future TPU/XLA profile. It is a named planning target until TPU capsules are added.

def NN.Backend.BackendProfile.futureTrainium : BackendProfile

Future AWS Trainium/Neuron profile. It is a named planning target until Neuron capsules exist.

def NN.Backend.BackendProfile.futureCustomChip : BackendProfile

Future first-party/lab custom accelerator profile.

def NN.Backend.BackendProfile.futureExternal : BackendProfile

Future caller-supplied external accelerator profile.