Backend Targets

Cross-platform target descriptions for backend planning.

ExecutionConfig says what a run wants. Availability says which devices and providers a planner may consider. Target describes declared platform/build capabilities: CPU-only Linux, CUDA Linux, Apple Metal, TPU/XLA, AWS Trainium/Neuron, WASM, or a caller-supplied accelerator all map into the same capsule planner. A target declaration is not runtime discovery; executable paths must still probe the linked runtime before launching work.

inductive NN.Backend.OperatingSystem : Type

Operating-system family relevant to backend packaging and dynamic-library loading.

• linux : OperatingSystem
• macOS : OperatingSystem
• windows : OperatingSystem
• wasi : OperatingSystem
• unknown : OperatingSystem

@[implicit_reducible]

instance NN.Backend.instDecidableEqOperatingSystem : DecidableEq OperatingSystem

@[implicit_reducible]

instance NN.Backend.instReprOperatingSystem : Repr OperatingSystem

def NN.Backend.instReprOperatingSystem.repr : OperatingSystem → Nat → Std.Format

inductive NN.Backend.Architecture : Type

Machine architecture relevant to native extension availability.

• x86_64 : Architecture
• aarch64 : Architecture
• wasm32 : Architecture
• unknown : Architecture

@[implicit_reducible]

instance NN.Backend.instDecidableEqArchitecture : DecidableEq Architecture

def NN.Backend.instReprArchitecture.repr : Architecture → Nat → Std.Format

@[implicit_reducible]

instance NN.Backend.instReprArchitecture : Repr Architecture

inductive NN.Backend.Accelerator : Type

Primary accelerator family for a build or machine.

• none : Accelerator
• cuda : Accelerator
• rocm : Accelerator
• metal : Accelerator
• wasm : Accelerator
• tpu : Accelerator
• trainium : Accelerator
• custom : Accelerator
• external : Accelerator

@[implicit_reducible]

instance NN.Backend.instDecidableEqAccelerator : DecidableEq Accelerator

@[implicit_reducible]

instance NN.Backend.instReprAccelerator : Repr Accelerator

def NN.Backend.instReprAccelerator.repr : Accelerator → Nat → Std.Format

inductive NN.Backend.BuildFeature : Type

Optional backend feature compiled into or discoverable from a build.

• nativeCuda : BuildFeature
• libTorch : BuildFeature
• aten : BuildFeature
• mps : BuildFeature
• webGpu : BuildFeature
• cuBLAS : BuildFeature
• cuDNN : BuildFeature
• cuFFT : BuildFeature
• xla : BuildFeature
• neuron : BuildFeature
• customChip : BuildFeature
• externalProvider : BuildFeature

@[implicit_reducible]

instance NN.Backend.instDecidableEqBuildFeature : DecidableEq BuildFeature

@[implicit_reducible]

instance NN.Backend.instReprBuildFeature : Repr BuildFeature

def NN.Backend.instReprBuildFeature.repr : BuildFeature → Nat → Std.Format

structure NN.Backend.Target : Type

Platform/build description used to produce backend availability.

• os : OperatingSystem
• arch : Architecture
• accelerator : Accelerator
• features : List BuildFeature

def NN.Backend.instReprTarget.repr : Target → Nat → Std.Format

@[implicit_reducible]

instance NN.Backend.instReprTarget : Repr Target

def NN.Backend.BuildFeature.provider? : BuildFeature → Option Provider

Provider exposed by a build feature, if it corresponds to one.

def NN.Backend.Accelerator.device? : Accelerator → Option Device

Device exposed by an accelerator target. CPU is added separately by Target.devices.

def NN.Backend.Target.devices (t : Target) : List Device

Device set exposed by the target. CPU/reference remains available unless a caller filters it.

def NN.Backend.Target.providers (t : Target) : List Provider

Providers exposed by the target and its compiled/discovered features.

def NN.Backend.Target.declaredAvailability (t : Target) : Availability

Convert a target declaration to planner capabilities; this does not probe the current machine.

def NN.Backend.Target.portableCpu (os : OperatingSystem := OperatingSystem.unknown) (arch : Architecture := Architecture.unknown) : Target

Portable CPU/reference target.

def NN.Backend.Target.linuxCpu (arch : Architecture := Architecture.x86_64) : Target

Linux CPU/reference target.

def NN.Backend.Target.macOSCpu (arch : Architecture := Architecture.aarch64) : Target

macOS CPU/reference target.

def NN.Backend.Target.windowsCpu (arch : Architecture := Architecture.x86_64) : Target

Windows CPU/reference target.

def NN.Backend.Target.linuxCuda (enableLibTorch : Bool := false) : Target

Linux CUDA target with native CUDA provider features.

def NN.Backend.Target.windowsCuda (enableLibTorch : Bool := false) : Target

Windows CUDA target shape. Native support depends on the future Windows build/test pass.

def NN.Backend.Target.linuxRocm : Target

Linux ROCm target shape for future AMD/HIP capsules.

def NN.Backend.Target.macOSMetal : Target

macOS target for future Metal/MPS capsules.

def NN.Backend.Target.wasm : Target

WASM target for browser or WASI-style execution.

def NN.Backend.Target.linuxTpu : Target

TPU/XLA target shape for future accelerator capsules.

def NN.Backend.Target.linuxTrainium : Target

AWS Trainium/Neuron target shape for future accelerator capsules.

def NN.Backend.Target.customChip (os : OperatingSystem := OperatingSystem.linux) (arch : Architecture := Architecture.unknown) : Target

Target shape for a first-party or lab-specific accelerator with its own capsule provider.

def NN.Backend.Target.external (os : OperatingSystem := OperatingSystem.unknown) (arch : Architecture := Architecture.unknown) : Target

Target shape for a caller-supplied accelerator provider.