8.4. Backends and Training
Backend selection is an audited planning step. A capsule names the operation, provider, device, numerical policy, and evidence. Eager execution matches the selected capsule to a handler with the same identity. Graph-level lowering produces checked planning data, not an execution engine.
A kernel capsule records an operation, provider, device, forward and VJP support, numerical policy, and evidence for its shape, layout, value, and VJP claims. It states the contract expected from an implementation; it does not prove that implementation.
Lean code for Definition8.4.1●1 definition
Associated Lean declarations
-
NN.Backend.KernelCapsule[complete]
-
NN.Backend.KernelCapsule[complete]
-
structuredefined in NN/Backend/Capsule.leancomplete
structure NN.Backend.KernelCapsule : Type
structure NN.Backend.KernelCapsule : Type
A contract-carrying fast kernel or reference implementation.
Fields
name : String
Name used in selection reports and runtime errors.
op : NN.Backend.BackendOp
Backend operation implemented by this capsule.
provider : NN.Backend.Provider
Provider responsible for the implementation.
device : NN.Backend.Device
Device on which the implementation runs.
trustLevel : NN.Backend.TrustLevel
Assurance level the planner must accept before selection.
supportsForward : Bool
Whether the capsule supplies forward execution.
vjpMode : NN.Backend.VJPMode
Form of reverse-mode support supplied by the capsule.
shapeContract : NN.Backend.ContractDescriptor
Shape-safety claim and its evidence.
layoutContract : NN.Backend.ContractDescriptor
Tensor-layout claim and its evidence.
valueContract : NN.Backend.ContractDescriptor
Forward-value refinement claim and its evidence.
vjpContract : NN.Backend.ContractDescriptor
Reverse-mode refinement claim and its evidence.
numericalPolicy : NN.Backend.NumericalPolicy
Floating-point behavior advertised for numerical audits.
notes : String
Optional human-readable details not used by selection.
A proof-carrying kernel packages a typed implementation with a pointwise proof that it equals one explicit Lean specification. The typed verified planner retains that proof; converting the object to ordinary capsule metadata does not.
Lean code for Definition8.4.2●1 definition
Associated Lean declarations
-
NN.Backend.ProofCarryingKernel[complete]
-
NN.Backend.ProofCarryingKernel[complete]
-
structuredefined in NN/Backend/Capsule.leancomplete
structure NN.Backend.ProofCarryingKernel.{u, v} (ι : Type u) (ο : Type v) (op : NN.Backend.BackendOp) (specification : ι → ο) : Type (max u v)
structure NN.Backend.ProofCarryingKernel.{u, v} (ι : Type u) (ο : Type v) (op : NN.Backend.BackendOp) (specification : ι → ο) : Type (max u v)
A kernel implementation accompanied by a proof of its typed semantics. `specification` is an explicit parameter of the type, so the refinement theorem cannot be detached from the function it justifies. The operation tag is a planner identity; the equality below states the exact Lean semantics that have actually been proved. The input and output types may describe a forward result alone or a bundle containing both a forward value and a VJP. Extracting `capsule` deliberately loses the proof. Metadata-only planning therefore rejects capsules marked `verified`; consumers that require verified execution must retain the complete `ProofCarryingKernel` value through the typed verified planner.
Fields
capsule : NN.Backend.KernelCapsule
Metadata used by ordinary backend reports and device selection.
implementation : ι → ο
Typed implementation whose semantics are proved below.
operation_matches : self.capsule.op = op
The metadata names the operation indexed by this proof object.
trust_verified : self.capsule.trustLevel = NN.Backend.TrustLevel.verified
The capsule advertises the trust level supplied by this proof object.
contracts_aligned : self.capsule.contractsAligned = true
Each metadata descriptor states the obligation belonging to its field.
refines : ∀ (input : ι), self.implementation input = specification input
Pointwise refinement of the implementation to the canonical specification.
Executing a kernel selected by the typed verified planner returns the value of the specification that indexes the selected kernel.
Lean code for Theorem8.4.3●1 theorem
Associated Lean declarations
-
theoremdefined in NN/Backend/Planner.leancomplete
theorem NN.Backend.VerifiedPlannedKernel.run_eq_specification.{u, v} {ι : Type u} {ο : Type v} {op : NN.Backend.BackendOp} {specification : ι → ο} {cfg : NN.Backend.ExecutionConfig} (planned : NN.Backend.VerifiedPlannedKernel ι ο op specification cfg) (input : ι) : planned.run input = specification input
theorem NN.Backend.VerifiedPlannedKernel.run_eq_specification.{u, v} {ι : Type u} {ο : Type v} {op : NN.Backend.BackendOp} {specification : ι → ο} {cfg : NN.Backend.ExecutionConfig} (planned : NN.Backend.VerifiedPlannedKernel ι ο op specification cfg) (input : ι) : planned.run input = specification input
Verified planning preserves the kernel's exact Lean specification.
The selected object retains the original refinement field, so the result follows by applying that field to the input.
Cuda.Buffer is an opaque handle to a contiguous float32 buffer. A CUDA build stores device
memory behind the handle; the default stub keeps parity storage on the host. Lean code cannot
inspect either representation directly.
Lean code for Definition8.4.4●1 definition
Associated Lean declarations
-
Runtime.Autograd.Cuda.Buffer[complete]
-
Runtime.Autograd.Cuda.Buffer[complete]
-
defdefined in NN/Runtime/Autograd/Engine/Cuda/Trusted.leancomplete
def Runtime.Autograd.Cuda.Buffer : Type
def Runtime.Autograd.Cuda.Buffer : Type
Runtime representation used for native CUDA buffer handles. The `NonemptyType` wrapper is Lean's standard representation for external resources: it gives extern declarations a nonempty result type while preserving reference-counting information in compiled code. The underlying value is still created only by the native buffer constructors.
A backend profile stores a name, execution configuration, target, capsule modules, and graph lowering mode. Target availability and the registry are derived from those fields, and capsule modules are validated when a graph is planned.
Lean code for Definition8.4.5●1 definition
Associated Lean declarations
-
NN.Backend.BackendProfile[complete]
-
NN.Backend.BackendProfile[complete]
-
structuredefined in NN/Backend/Profile.leancomplete
structure NN.Backend.BackendProfile : Type
structure NN.Backend.BackendProfile : Type
One named backend execution profile.
Fields
name : String
Human-readable profile name used in diagnostics and reports.
config : NN.Backend.ExecutionConfig
Device, provider preference, assurance policy, and VJP execution mode.
target : NN.Backend.Target
Operating-system, architecture, and accelerator capabilities available to planning.
capsuleModules : List NN.Backend.Registry.CapsuleModule
Capsule modules used to construct and validate the profile's planning registry.
loweringMode : NN.Backend.LoweringMode
Whether accepted nodes remain separate or are combined into compatible execution groups.
The maintained registry collects contract capsules contributed by the attention, native CUDA, and reference modules. It contains planning metadata, not executable handlers. Profiles add the separate LibTorch module when requested.
Lean code for Definition8.4.6●1 definition
Associated Lean declarations
-
NN.Backend.Registry.maintainedModules[complete]
-
NN.Backend.Registry.maintainedModules[complete]
-
defdefined in NN/Backend/Registry.leancomplete
def NN.Backend.Registry.maintainedModules : List NN.Backend.Registry.CapsuleModule
def NN.Backend.Registry.maintainedModules : List NN.Backend.Registry.CapsuleModule
Maintained operation/provider modules. A new architecture does not modify this list; only a new primitive implementation or provider does.
The checked CPU profile instantiates the profile record with the maintained capsule modules, a portable CPU target, coalesced lowering, and the checked assurance policy.
Lean code for Definition8.4.7●1 definition
Associated Lean declarations
-
NN.Backend.BackendProfile.checkedCpu[complete]
-
NN.Backend.BackendProfile.checkedCpu[complete]
-
defdefined in NN/Backend/Profile.leancomplete
def NN.Backend.BackendProfile.checkedCpu : NN.Backend.BackendProfile
def NN.Backend.BackendProfile.checkedCpu : NN.Backend.BackendProfile
Maintained portable CPU/reference profile with runtime guards and regression evidence.
Binding a selected capsule to a handler checks that their operation, provider, and device agree. The resulting executable kernel carries those identity equalities; binding does not strengthen the capsule's numerical evidence.
Lean code for Definition8.4.8●1 definition
Associated Lean declarations
-
NN.Backend.KernelCapsule.bind[complete]
-
NN.Backend.KernelCapsule.bind[complete]
-
defdefined in NN/Backend/Capsule.leancomplete
def NN.Backend.KernelCapsule.bind {β : Type} (c : NN.Backend.KernelCapsule) (handler : NN.Backend.KernelHandler β) : Except String (NN.Backend.ExecutableKernel β)
def NN.Backend.KernelCapsule.bind {β : Type} (c : NN.Backend.KernelCapsule) (handler : NN.Backend.KernelHandler β) : Except String (NN.Backend.ExecutableKernel β)
Pair a selected contract with the runtime handler that will execute it. The returned equalities prevent an executor for one operation or provider from being presented as another merely because both happen to share a Lean result type.
A backend profile validates its configured capsule modules, requires a structurally well-formed IR graph, and selects a capsule for each runtime-relevant node. It then lowers those choices as singleton or coalesced groups and gates their evidence under the profile's assurance policy.
Lean code for Definition8.4.9●1 definition
Associated Lean declarations
-
NN.Backend.BackendProfile.acceptGraph[complete]
-
NN.Backend.BackendProfile.acceptGraph[complete]
-
defdefined in NN/Backend/Profile.leancomplete
def NN.Backend.BackendProfile.acceptGraph (p : NN.Backend.BackendProfile) (g : NN.IR.Graph) : Except String NN.Backend.AcceptedPlanResult
def NN.Backend.BackendProfile.acceptGraph (p : NN.Backend.BackendProfile) (g : NN.IR.Graph) : Except String NN.Backend.AcceptedPlanResult
Plan, lower, and gate a graph under the profile.
For one eager operation, the session selects and caches an admitted capsule, finds a handler with the same operation, provider, and device, and runs it through the checked binding. This dispatcher does not append an autograd node; each operation implementation records its own forward value and VJP.
Lean code for Definition8.4.10●1 definition
Associated Lean declarations
-
defdefined in NN/Runtime/Autograd/Torch/Core/Session.leancomplete
def Runtime.Autograd.Torch.Internal.EagerSession.executeSelected {α β : Type} (s : Runtime.Autograd.Torch.Internal.EagerSession α) (op : NN.Backend.BackendOp) (handlers : List (NN.Backend.KernelHandler β)) : IO β
def Runtime.Autograd.Torch.Internal.EagerSession.executeSelected {α β : Type} (s : Runtime.Autograd.Torch.Internal.EagerSession α) (op : NN.Backend.BackendOp) (handlers : List (NN.Backend.KernelHandler β)) : IO β
Execute an operation through a handler that matches the selected capsule. The planner may know about providers that are not linked into a particular runtime build. Such a selection fails here instead of recording one provider while silently running another. The `ExecutableKernel` equalities certify dispatch identity; the selected capsule still states the strength of the numerical evidence.
The CUDA tape stores device buffers, parent ids, and local VJP
closures in evaluation order. requireValue, requireGrad, and backward accumulation check shape
tags and native buffer lengths. Dense backward returns one buffer per node; sparse backward retains
owned buffers only for selected node ids and requires the caller to release them.
Lean code for Definition8.4.11●1 definition
Associated Lean declarations
-
Runtime.Autograd.Cuda.Tape[complete]
-
Runtime.Autograd.Cuda.Tape[complete]
-
structuredefined in NN/Runtime/Autograd/Engine/Cuda/Tape.leancomplete
structure Runtime.Autograd.Cuda.Tape : Type
structure Runtime.Autograd.Cuda.Tape : Type
CUDA autograd tape: a grow-only array of nodes. Node ids are array indices.
Fields
nodes : Array Runtime.Autograd.Cuda.Node
Tape nodes in evaluation order (id = index).
Given the stated native bit-agreement hypothesis, decoded native scalar addition equals
IEEE32Exec.add. The hypothesis remains visible in the theorem type.
Lean code for Theorem8.4.12●1 theorem
Associated Lean declarations
-
theoremdefined in NN/Runtime/Autograd/Engine/Cuda/Float32Contract.leancomplete
theorem Runtime.Autograd.Cuda.Float32Contract.native_add_eq_ieee32 {native : Runtime.Autograd.Cuda.Float32Contract.NativePrimitiveBits} (h : Runtime.Autograd.Cuda.Float32Contract.NativePrimitiveAgreement native) (x y : Runtime.Autograd.Cuda.Float32Contract.RefScalar) : Runtime.Autograd.Cuda.Float32Contract.fromNativeBits (native.addBits x y) = TorchLean.Floats.IEEE754.IEEE32Exec.add x y
theorem Runtime.Autograd.Cuda.Float32Contract.native_add_eq_ieee32 {native : Runtime.Autograd.Cuda.Float32Contract.NativePrimitiveBits} (h : Runtime.Autograd.Cuda.Float32Contract.NativePrimitiveAgreement native) (x y : Runtime.Autograd.Cuda.Float32Contract.RefScalar) : Runtime.Autograd.Cuda.Float32Contract.fromNativeBits (native.addBits x y) = TorchLean.Floats.IEEE754.IEEE32Exec.add x y
Native addition agrees with the reference value when its result bits satisfy the contract.
The proof rewrites the supplied native result bits to the executable binary32 result. It does not prove the external kernel implementation from source.
ScalarModule wraps a scalar trainer, its runtime options, and the selected host/device tensor
conversion. The trainer owns a shape-indexed mutable parameter pack and runs its scalar-loss
program through eager execution or
the compiled backend. Gradients are returned to callers;
generic optimizer state is passed to and returned from update methods rather than stored here.
Lean code for Definition8.4.13●1 definition
Associated Lean declarations
-
structuredefined in NN/Runtime/Autograd/TorchLean/Module.leancomplete
structure Runtime.Autograd.TorchLean.Module.ScalarModule (α : Type) [Context α] [DecidableEq Spec.Shape] (paramShapes inputShapes : List Spec.Shape) (natInputShapes : List Spec.Shape := []) : Type
structure Runtime.Autograd.TorchLean.Module.ScalarModule (α : Type) [Context α] [DecidableEq Spec.Shape] (paramShapes inputShapes : List Spec.Shape) (natInputShapes : List Spec.Shape := []) : Type
Runtime module instance (the thing you "run"). This wraps `Torch.ScalarTrainer`, but exposes a more `Module`-like set of methods.
Fields
trainer : Runtime.Autograd.Torch.ScalarTrainer α paramShapes inputShapes natInputShapes
Trainer that owns the parameters and runs the scalar-loss program.
opts : Runtime.Autograd.Torch.Options
Runtime options used to instantiate the module.
tensorConv : Runtime.Autograd.Torch.Internal.CudaBridge.TensorConv α
Concrete host/device tensor conversion selected when the module was instantiated.
Stepper holds a supervised runner, a one-sample update closure, an epoch-over-list closure, and
a step counter.
Lean code for Definition8.4.14●1 definition
Associated Lean declarations
-
TorchLean.Trainer.Manual.Stepper[complete]
-
TorchLean.Trainer.Manual.Stepper[complete]
-
structuredefined in NN/API/Trainer/Manual/Stepper.leancomplete
structure TorchLean.Trainer.Manual.Stepper (α : Type) [Context α] [DecidableEq Spec.Shape] {σ τ : Spec.Shape} (task : TorchLean.Trainer.Manual.SeqTask σ τ) : Type
structure TorchLean.Trainer.Manual.Stepper (α : Type) [Context α] [DecidableEq Spec.Shape] {σ τ : Spec.Shape} (task : TorchLean.Trainer.Manual.SeqTask σ τ) : Type
Stateful training loop object: a `Runner` plus an optimizer state and a step counter. It packages the model runner with the state needed to step on successive batches.
Fields
runner : TorchLean.Trainer.Manual.Runner α task
Underlying task runner (module + compiled forward artifacts/losses).
stepSample : Runtime.Autograd.Torch.TList α [σ, τ] → IO α
Run a single optimization step on one supervised sample, returning the loss value.
epochSamples : List (Runtime.Autograd.Torch.TList α [σ, τ]) → IO (List α)
Run an epoch over an explicit list of samples, returning the per-step loss values.
stepCount : IO ℕ
Read the total number of `stepSample` calls performed so far.
The supervised stepper constructor builds the stateful training loop around a scalar module. It selects an optimizer, applies an optional learning-rate schedule, and refreshes mode-dependent model buffers before each update.
Lean code for Definition8.4.15●1 definition
Associated Lean declarations
-
TorchLean.Trainer.Manual.stepper[complete]
-
TorchLean.Trainer.Manual.stepper[complete]
-
defdefined in NN/API/Trainer/Manual/Stepper.leancomplete
def TorchLean.Trainer.Manual.stepper {σ τ : Spec.Shape} {task : TorchLean.Trainer.Manual.SeqTask σ τ} {α : Type} [Context α] [DecidableEq Spec.Shape] [ToString α] [TorchLean.Runtime.FromFloat α] (runner : TorchLean.Trainer.Manual.Runner α task) (optimizer : TorchLean.Trainer.Manual.OptimizerConfig) (scheduler : Option TorchLean.Trainer.Scheduler.Config := none) : IO (TorchLean.Trainer.Manual.Stepper α task)
def TorchLean.Trainer.Manual.stepper {σ τ : Spec.Shape} {task : TorchLean.Trainer.Manual.SeqTask σ τ} {α : Type} [Context α] [DecidableEq Spec.Shape] [ToString α] [TorchLean.Runtime.FromFloat α] (runner : TorchLean.Trainer.Manual.Runner α task) (optimizer : TorchLean.Trainer.Manual.OptimizerConfig) (scheduler : Option TorchLean.Trainer.Scheduler.Config := none) : IO (TorchLean.Trainer.Manual.Stepper α task)
Construct a `Stepper` for a runner, optimizer config, and optional scheduler. This is the recommended way to build custom training loops without reimplementing the optimizer logic: call `stepper`, then choose `stepSample` for single batches or `epochSamples` for explicit sample lists.
-
Import.PyTorch.TorchExport.parseGraph[complete]
The torch.export adapter parses TorchLean's captured graph schema, lowers its supported values to
the shared IR, runs shape validation, and checks that the named input
and output nodes exist.
Lean code for Definition8.4.16●1 definition
Associated Lean declarations
-
Import.PyTorch.TorchExport.parseGraph[complete]
-
Import.PyTorch.TorchExport.parseGraph[complete]
-
defdefined in NN/Runtime/PyTorch/Import/TorchExport.leancomplete
def Import.PyTorch.TorchExport.parseGraph (j : Lean.Json) : Except String Import.PyTorch.TorchExport.CapturedGraph
def Import.PyTorch.TorchExport.parseGraph (j : Lean.Json) : Except String Import.PyTorch.TorchExport.CapturedGraph
Parse and validate a captured PyTorch graph. Success means: - the JSON uses the TorchLean graph-artifact schema, - every op is in the supported TorchLean IR subset, - node ids are disciplined and topologically ordered, - arities are valid, and - declared output shapes match `NN.IR.Infer`.
Every graph returned successfully by the torch.export parser
satisfies TorchLean's executable shape check.
Lean code for Theorem8.4.17●1 theorem
Associated Lean declarations
-
theoremdefined in NN/Runtime/PyTorch/Import/TorchExport.leancomplete
theorem Import.PyTorch.TorchExport.parseGraph_wellShaped {j : Lean.Json} {cg : Import.PyTorch.TorchExport.CapturedGraph} (h : Import.PyTorch.TorchExport.parseGraph j = Except.ok cg) : cg.graph.WellShaped
theorem Import.PyTorch.TorchExport.parseGraph_wellShaped {j : Lean.Json} {cg : Import.PyTorch.TorchExport.CapturedGraph} (h : Import.PyTorch.TorchExport.parseGraph j = Except.ok cg) : cg.graph.WellShaped
Guarantee exposed by the parser: a successfully parsed graph is well-shaped. This theorem is compact but important. It is the theorem downstream verification/export code can quote when it receives a graph artifact through this importer.
The proof unfolds the parser, rules out each rejected branch, and returns the successful shape check.