Backend Availability

Machine- and build-dependent availability for backend capsules.

ExecutionConfig says what a run is allowed to use. Availability says what this checkout/machine can actually provide. Keeping those separate is the cross-platform story: CPU-only builds, CUDA builds, and optional LibTorch builds all use the same semantic registry, but expose different available capsule subsets to the planner.

structure NN.Backend.Availability : Type

Runtime/build capabilities visible to backend planning.

• devices : List Device
• providers : List Provider

@[implicit_reducible]

instance NN.Backend.instReprAvailability : Repr Availability

def NN.Backend.instReprAvailability.repr : Availability → Nat → Std.Format

def NN.Backend.Availability.hasDevice (a : Availability) (d : Device) : Bool

Whether a device is available on this machine/build.

def NN.Backend.Availability.hasProvider (a : Availability) (p : Provider) : Bool

Whether a provider is available.

def NN.Backend.Availability.admitsCapsule (a : Availability) (c : KernelCapsule) : Bool

Whether a capsule can even be considered on this machine/build.

def NN.Backend.Availability.filterCapsules (a : Availability) (capsules : List KernelCapsule) : List KernelCapsule

Keep only capsules available on this machine/build.

def NN.Backend.Availability.cpu : Availability

CPU/reference-only availability.

def NN.Backend.Availability.cudaNative : Availability

CUDA availability without optional external providers.

def NN.Backend.Availability.cudaWithLibTorch : Availability

CUDA availability with optional LibTorch enabled and installed.