Backend Types

Small vocabulary for backend selection and trust boundaries.

TorchLean owns the spec, graph, and proof-facing contracts. Backends are execution providers for parts of that graph: a Lean reference path, a TorchLean composition, or LibTorch ATen operations. This file deliberately contains only data. It should stay cheap to import from specs, runtime wrappers, docs generators, and tests.

inductive NN.Backend.Device : Type

Hardware or execution target visible to the planner.

• cpu : Device
• cuda : Device
• rocm : Device
• metal : Device
• wasm : Device
• tpu : Device
• trainium : Device
• custom : Device
• external : Device

@[instance_reducible]

instance NN.Backend.instDecidableEqDevice : DecidableEq Device

def NN.Backend.instReprDevice.repr : Device → Nat → Std.Format

@[instance_reducible]

instance NN.Backend.instReprDevice : Repr Device

@[reducible, inline]

abbrev NN.Backend.Device.gpu : Device

Request the supported GPU target. Currently this is CUDA through LibTorch. Runtime initialization fails if it is unavailable; this does not fall back to CPU.

def NN.Backend.Device.cliName : Device → String

Stable spelling used in profile names, reports, and CLI bridges.

def NN.Backend.Device.parse : String → Except String Device

Parse an explicit backend device name, with a diagnostic suitable for command-line use. CLI layers resolve policy names such as auto before calling this function.

inductive NN.Backend.Provider : Type

Concrete provider family used to execute a kernel capsule.

• reference : Provider
• torchLean : Provider
• libTorch : Provider

  LibTorch ATen execution; this provider does not imply LibTorch autograd ownership.

• aten : Provider
• mps : Provider
• webGpu : Provider
• cuBLAS : Provider
• cuDNN : Provider
• cuFFT : Provider
• xla : Provider
• neuron : Provider
• customChip : Provider
• external : Provider

@[instance_reducible]

instance NN.Backend.instDecidableEqProvider : DecidableEq Provider

def NN.Backend.instReprProvider.repr : Provider → Nat → Std.Format

@[instance_reducible]

instance NN.Backend.instReprProvider : Repr Provider

inductive NN.Backend.BackendOp : Type

Stable operation vocabulary used by backend capsules, graph planning, and runtime guards.

This is deliberately a closed vocabulary. New backend-visible operations should be added here and then wired through the IR adapter and capsule registry. Runtime tape/debug labels may still be strings, but the backend planner should not accept arbitrary stringly-typed operation names.

• randUniform : BackendOp
• bernoulliMask : BackendOp
• add : BackendOp
• sub : BackendOp
• mul : BackendOp
• div : BackendOp
• neg : BackendOp
• scale : BackendOp
• abs : BackendOp
• sqrt : BackendOp
• clamp : BackendOp
• max : BackendOp
• min : BackendOp
• relu : BackendOp
• gelu : BackendOp
• sigmoid : BackendOp
• silu : BackendOp
• tanh : BackendOp
• softplus : BackendOp
• exp : BackendOp
• log : BackendOp
• sin : BackendOp
• cos : BackendOp
• inv : BackendOp
• safeLog : BackendOp
• logSoftmax : BackendOp
• softmax : BackendOp
• hardMaskedSoftmax : BackendOp
• topKMask : BackendOp
• reduceSum : BackendOp
• reduceMean : BackendOp
• reshape : BackendOp
• permute : BackendOp
• broadcast : BackendOp
• concat : BackendOp
• slice : BackendOp
• gather : BackendOp
• scatterAdd : BackendOp
• matmul : BackendOp
• scaledMatmul : BackendOp
• softmaxMatmul : BackendOp
• linear : BackendOp
• mseLoss : BackendOp
• crossEntropy : BackendOp
• distill : BackendOp
• layerNorm : BackendOp
• batchNorm : BackendOp
• conv : BackendOp
• convTranspose : BackendOp
• maxPool : BackendOp
• smoothMaxPool : BackendOp
• avgPool : BackendOp
• fftFno : BackendOp
• selectiveScan : BackendOp
• attention : BackendOp
• custom : BackendOp

@[instance_reducible]

instance NN.Backend.instDecidableEqBackendOp : DecidableEq BackendOp

@[instance_reducible]

instance NN.Backend.instBEqBackendOp : BEq BackendOp

def NN.Backend.instBEqBackendOp.beq : BackendOp → BackendOp → Bool

instance NN.Backend.instReflBEqBackendOp : ReflBEq BackendOp

instance NN.Backend.instLawfulBEqBackendOp : LawfulBEq BackendOp

def NN.Backend.instReprBackendOp.repr : BackendOp → Nat → Std.Format

@[instance_reducible]

instance NN.Backend.instReprBackendOp : Repr BackendOp

def NN.Backend.BackendOp.name : BackendOp → String

Stable spelling used in reports, capsule names, and CLI diagnostics.

@[instance_reducible]

instance NN.Backend.BackendOp.instToString : ToString BackendOp

def NN.Backend.BackendOp.requiresVJP : BackendOp → Bool

Whether training through this operation requires a registered local VJP.

Random sources create values but are not themselves differentiated, and neither is top-k routing, whose mask is constant away from ties. Every other backend-visible operation must provide a compatible VJP whenever gradient tracking is requested.

inductive NN.Backend.TrustLevel : Type

How much TorchLean knows about an implementation.

checked records maintained runtime guards and regression evidence, including for wrappers around LibTorch. It is not a proof of an implementation. trustedExternal records a boundary accepted without that maintained evidence; the assurance policy must explicitly admit it.

• checked : TrustLevel
• trustedExternal : TrustLevel

@[instance_reducible]

instance NN.Backend.instDecidableEqTrustLevel : DecidableEq TrustLevel

def NN.Backend.instReprTrustLevel.repr : TrustLevel → Nat → Std.Format

@[instance_reducible]

instance NN.Backend.instReprTrustLevel : Repr TrustLevel

structure NN.Backend.AssurancePolicy : Type

Which trust boundaries a kernel plan may cross.

The same record decides both which capsules the planner may select (by trust level) and which contract evidence the selected capsules may rely on (by evidence kind). Keeping the decision in one place prevents a profile from selecting a capsule under one policy and checking it under another.

• allowTrustedExternal : Bool

  Whether capsules and evidence that delegate to an external implementation are admitted.

@[instance_reducible]

instance NN.Backend.instDecidableEqAssurancePolicy : DecidableEq AssurancePolicy

def NN.Backend.instDecidableEqAssurancePolicy.decEq (x✝ x✝¹ : AssurancePolicy) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance NN.Backend.instReprAssurancePolicy : Repr AssurancePolicy

def NN.Backend.instReprAssurancePolicy.repr : AssurancePolicy → Nat → Std.Format

def NN.Backend.AssurancePolicy.checked : AssurancePolicy

Maintained TorchLean runtime policy.

Implementations backed by maintained runtime guards and regression evidence are accepted. This includes LibTorch wrappers with retained CUDA comparisons; it does not verify LibTorch, the FFI, or compiled code. Capsules classified as trustedExternal and named trusted-boundary evidence are not admitted.

def NN.Backend.AssurancePolicy.external : AssurancePolicy

Explicit external-provider policy.

This policy also admits capsules and contract descriptors supported by an explicit external agreement assumption. The selected boundary remains visible in the execution audit.

def NN.Backend.AssurancePolicy.acceptsTrust (policy : AssurancePolicy) : TrustLevel → Bool

Whether the policy admits a capsule with the given implementation trust level.

inductive NN.Backend.VJPMode : Type

How a backend capsule supplies a local reverse rule to the TorchLean tape.

• none : VJPMode

  No reverse rule is supplied.

• torchLeanTape : VJPMode

  TorchLean composes the local VJP from runtime operations.

• backendVJP : VJPMode

  The native bridge supplies the selected local VJP, without recording an autograd graph.

@[instance_reducible]

instance NN.Backend.instDecidableEqVJPMode : DecidableEq VJPMode

def NN.Backend.instReprVJPMode.repr : VJPMode → Nat → Std.Format

@[instance_reducible]

instance NN.Backend.instReprVJPMode : Repr VJPMode

inductive NN.Backend.ProviderPreference : Type

Provider preference used when selecting an implementation for an operation.

• auto : ProviderPreference
• prefer (provider : Provider) : ProviderPreference
• only (provider : Provider) : ProviderPreference

def NN.Backend.instDecidableEqProviderPreference.decEq (x✝ x✝¹ : ProviderPreference) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance NN.Backend.instDecidableEqProviderPreference : DecidableEq ProviderPreference

@[instance_reducible]

instance NN.Backend.instReprProviderPreference : Repr ProviderPreference

def NN.Backend.instReprProviderPreference.repr : ProviderPreference → Nat → Std.Format

structure NN.Backend.KernelPolicy : Type

Policy used to select kernel capsules for a device and assurance boundary.

• device : Device
• provider : ProviderPreference
• assurance : AssurancePolicy
• vjpMode : VJPMode

def NN.Backend.instReprKernelPolicy.repr : KernelPolicy → Nat → Std.Format

@[instance_reducible]

instance NN.Backend.instReprKernelPolicy : Repr KernelPolicy