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, LibTorch, ATen, cuBLAS/cuDNN/cuFFT, TPU/XLA, AWS Neuron/Trainium, or future platform-specific providers. 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

@[implicit_reducible]

instance NN.Backend.instDecidableEqDevice : DecidableEq Device

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

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

@[implicit_reducible]

instance NN.Backend.instDecidableEqProvider : DecidableEq Provider

@[implicit_reducible]

instance NN.Backend.instReprProvider : Repr Provider

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

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
• sum : BackendOp
• reduceSum : BackendOp
• reduceMean : BackendOp
• flatten : BackendOp
• reshape : BackendOp
• permute : BackendOp
• transpose2d : BackendOp
• swapAdjacentAtDepth : BackendOp
• transpose3dFirstToLast : BackendOp
• transpose3dLastToFirst : BackendOp
• transpose3dLastTwo : BackendOp
• broadcastTo : BackendOp
• concatVectors : BackendOp
• concatLeadingAxis : BackendOp
• sliceLeadingAxisRange : BackendOp
• gatherScalar : BackendOp
• gatherScalarNat : BackendOp
• gatherRow : BackendOp
• gatherVecNat : BackendOp
• gatherRowsNat : BackendOp
• scatterAddVec : BackendOp
• scatterAddRow : BackendOp
• matmul : BackendOp
• bmm : BackendOp
• linear : BackendOp
• mseLoss : BackendOp
• layerNorm : BackendOp
• batchNorm : BackendOp
• batchNormChannelFirst : BackendOp
• conv : BackendOp
• conv2d : BackendOp
• convTranspose : BackendOp
• convTranspose2d : BackendOp
• maxPool : BackendOp
• maxPool2d : BackendOp
• maxPool2dPad : BackendOp
• smoothMaxPool : BackendOp
• smoothMaxPool2d : BackendOp
• avgPool : BackendOp
• avgPool2d : BackendOp
• avgPool2dPad : BackendOp
• fftFno : BackendOp
• selectiveScan : BackendOp
• scaledDotProductAttention : BackendOp

@[implicit_reducible]

instance NN.Backend.instDecidableEqBackendOp : DecidableEq BackendOp

@[implicit_reducible]

instance NN.Backend.instBEqBackendOp : BEq BackendOp

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

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

@[implicit_reducible]

instance NN.Backend.instReprBackendOp : Repr BackendOp

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

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

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

• verified : TrustLevel
• checked : TrustLevel
• fuzzed : TrustLevel
• trustedExternal : TrustLevel

@[implicit_reducible]

instance NN.Backend.instDecidableEqTrustLevel : DecidableEq TrustLevel

@[implicit_reducible]

instance NN.Backend.instReprTrustLevel : Repr TrustLevel

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

inductive NN.Backend.TrustPolicy : Type

User- or CI-selected policy for which backend capsules may be used.

• verifiedOnly : TrustPolicy
• checked : TrustPolicy
• fuzzedOk : TrustPolicy
• allowTrustedExternal : TrustPolicy

@[implicit_reducible]

instance NN.Backend.instDecidableEqTrustPolicy : DecidableEq TrustPolicy

def NN.Backend.instReprTrustPolicy.repr : TrustPolicy → Nat → Std.Format

@[implicit_reducible]

instance NN.Backend.instReprTrustPolicy : Repr TrustPolicy

def NN.Backend.TrustPolicy.accepts : TrustPolicy → TrustLevel → Bool

Whether a policy admits a capsule at the given trust level.

inductive NN.Backend.VJPMode : Type

How a backend capsule treats gradients.

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

@[implicit_reducible]

instance NN.Backend.instDecidableEqVJPMode : DecidableEq VJPMode

@[implicit_reducible]

instance NN.Backend.instReprVJPMode : Repr VJPMode

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

inductive NN.Backend.BackendPreference : Type

Backend preference requested by a runtime configuration.

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

def NN.Backend.instDecidableEqBackendPreference.decEq (x✝ x✝¹ : BackendPreference) : Decidable (x✝ = x✝¹)

@[implicit_reducible]

instance NN.Backend.instDecidableEqBackendPreference : DecidableEq BackendPreference

def NN.Backend.instReprBackendPreference.repr : BackendPreference → Nat → Std.Format

@[implicit_reducible]

instance NN.Backend.instReprBackendPreference : Repr BackendPreference

structure NN.Backend.ExecutionConfig : Type

Runtime-level backend configuration. Public APIs can wrap this with friendlier defaults.

• device : Device
• backend : BackendPreference
• trustPolicy : TrustPolicy
• vjpMode : VJPMode

@[implicit_reducible]

instance NN.Backend.instReprExecutionConfig : Repr ExecutionConfig

def NN.Backend.instReprExecutionConfig.repr : ExecutionConfig → Nat → Std.Format