A kernel capsule records an operation, provider, device, trust level (checked or trustedExternal), forward and VJP support, four contract descriptors (shape, layout, forward value, VJP), and a numerical policy. Each descriptor pairs a structured claim with its evidence: a runtime guard, a test suite, a named trusted boundary, or notApplicable. The capsule states the contract expected from an implementation; it does not prove that implementation.

The numerical policy of a capsule is its reduction order: fixedLeft for the left fold used by the canonical tensor semantics, implementationDefined for native and library accumulations, or notApplicable. Numerical certificates read this field so that a fixed-left range trace is not reused for an implementation-defined schedule. Rounding mode, subnormal handling, and multiply-add contraction are not recorded.

The distinction matters even for the same matrix dimensions: changing the accumulation tree changes the sequence of rounded additions. A shape proof cannot substitute for the missing numerical-policy match.

The contract check reads every obligation of a plan audit and rejects those whose evidence the assurance policy does not accept. The checked policy admits runtime guards, test suites, and notApplicable; only the external policy admits a trusted boundary. The result is a ContractCheck: either accepted or rejected with the failing obligation reports.

An accepted kernel is a planned operation whose capsule passed the complete kernel-policy gate, including the evidence check. Its proof field states PlannedKernel.acceptable policy = true: operation identity, forward support, contract alignment, trust, provider, device, and VJP mode must also agree. AcceptedGraphKernelPlan carries the corresponding check for groups derived from its stored graph plan.

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.

A typed shape supplies a logical element count; runtime validation compares it with the handle's reported length. This checks an observable interface condition without exposing the storage as a Lean array or deriving its contents from the type.

A backend profile stores a name, a kernel policy (device, provider preference, assurance policy, and VJP mode), the devices and providers declared available, and the capsule modules that form its planning registry. Capsule modules are validated for duplicate names when a graph is planned.

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.

The checked CPU profile instantiates the profile record with the maintained capsule modules, CPU-only availability, and the checked assurance policy.

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

A CUDA capsule paired with a CPU handler is rejected even when both declare matmul. Agreement on those labels permits dispatch; it does not inspect the handler's IO body.

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 groups those choices and runs the contract check under the profile's assurance policy, returning an accepted graph plan or the rejected obligations.

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.

Caching a selection reuses the admitted provider choice for this session, whose profile stays fixed. It does not cache tensor results or cotangents: later calls still execute with their current inputs, and the operation remains responsible for recording dependencies on those inputs.

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.

Objective 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 typed graph execution. Gradients are returned to callers; generic optimizer state is passed to and returned from update methods rather than stored here.

State shapes include persistent model buffers as well as trainable parameters. Differentiability flags determine which entries receive gradients, so possessing a state tensor does not by itself make that tensor an optimization variable.

Session owns a supervised update action and step counter behind the public step, stepBatch, and steps operations, together with evaluation-mode prediction and loss and the finish operation that packages the live state as a trained result.

A batch update and an evaluation may use the same parameters with different mode-dependent behavior, such as dropout. The step counter tracks updates; it is not a count of every forward call made for prediction or loss inspection.

Opening a trainer builds the stateful training loop around a scalar module. It selects the trainer's optimizer, applies an optional learning-rate schedule, and refreshes mode-dependent model buffers before each update.

NN.IR.OpTag identifies each IR operation constructor. Wire.opTag gives its fixed v1 kind string, and Wire.parseOpTag? reads that string back into a tag.

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.