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, the TorchLean runtime, native CUDA kernels, or LibTorch. 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

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

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

def NN.Backend.Device.parse? : String → Option Device

Parse an explicit backend device name. CLI layers may resolve policy names such as auto before calling this function.

def NN.Backend.Device.parse (value : String) : Except String Device

Parse an explicit backend device name or return a diagnostic suitable for command-line use.

inductive NN.Backend.Provider : Type

Concrete provider family used to execute a kernel capsule.

• reference : Provider
• torchLean : Provider
• nativeCuda : Provider
• libTorch : Provider
• 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
• scale : BackendOp
• abs : BackendOp
• sqrt : BackendOp
• clamp : BackendOp
• max : BackendOp
• min : BackendOp
• relu : BackendOp
• gelu : BackendOp
• sigmoid : BackendOp
• tanh : BackendOp
• softplus : BackendOp
• exp : BackendOp
• log : BackendOp
• sin : BackendOp
• cos : BackendOp
• inv : BackendOp
• safeLog : BackendOp
• logSoftmax : BackendOp
• softmax : BackendOp
• hardMaskedSoftmax : BackendOp
• reduceSum : BackendOp
• reduceMean : BackendOp
• reshape : BackendOp
• permute : BackendOp
• broadcast : BackendOp
• concat : BackendOp
• slice : BackendOp
• gather : BackendOp
• scatterAdd : BackendOp
• matmul : BackendOp
• linear : BackendOp
• mseLoss : BackendOp
• layerNorm : BackendOp
• batchNorm : BackendOp
• conv : BackendOp
• convTranspose : BackendOp
• maxPool : BackendOp
• smoothMaxPool : BackendOp
• avgPool : BackendOp
• fftFno : BackendOp
• selectiveScan : BackendOp
• scaledDotProductAttention : 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

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. 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.

trustedExternal is allowed, but it is intentionally loud: the contract names the boundary instead of silently treating an industrial kernel as though Lean had verified its source.

• checked : TrustLevel
• trustedExternal : TrustLevel

@[instance_reducible]

instance NN.Backend.instDecidableEqTrustLevel : DecidableEq TrustLevel

@[instance_reducible]

instance NN.Backend.instReprTrustLevel : Repr TrustLevel

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

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✝¹)

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

@[instance_reducible]

instance NN.Backend.instReprAssurancePolicy : Repr AssurancePolicy

def NN.Backend.AssurancePolicy.checked : AssurancePolicy

Maintained TorchLean runtime policy.

Checked implementations backed by runtime guards and regression evidence are accepted; trusted external implementations are not.

def NN.Backend.AssurancePolicy.external : AssurancePolicy

Explicit external-provider policy.

This is the policy used when a caller deliberately delegates a numerical kernel to LibTorch or another external implementation. 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 treats gradients.

• none : VJPMode
• torchLeanTape : VJPMode
• backendVJP : VJPMode

@[instance_reducible]

instance NN.Backend.instDecidableEqVJPMode : DecidableEq VJPMode

@[instance_reducible]

instance NN.Backend.instReprVJPMode : Repr VJPMode

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

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

@[instance_reducible]

instance NN.Backend.instDecidableEqProviderPreference : DecidableEq ProviderPreference

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

@[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