Backend Capsules

A backend capsule is TorchLean's unit of delegation to fast code.

The capsule records the contract TorchLean expects from a foreign implementation: which operation it implements, what layout and shape conventions are assumed, how refinement of the operation's canonical value and VJP semantics is justified, and what trust level the planner must account for. The contract does not prove the implementation. At runtime, a capsule is paired with a typed handler whose operation, provider, and device must agree with the selected contract.

structure NN.Backend.NativeSymbolRef : Type

Reference to a native/FFI symbol used by a backend capsule.

The repository linter checks that path exists, that symbol occurs in that source file, and that buildTarget?, when present, names a Lake target in lakefile.lean.

• path : String
• symbol : String
• buildTarget? : Option String

@[instance_reducible]

instance NN.Backend.instDecidableEqNativeSymbolRef : DecidableEq NativeSymbolRef

def NN.Backend.instDecidableEqNativeSymbolRef.decEq (x✝ x✝¹ : NativeSymbolRef) : Decidable (x✝ = x✝¹)

def NN.Backend.instBEqNativeSymbolRef.beq : NativeSymbolRef → NativeSymbolRef → Bool

@[instance_reducible]

instance NN.Backend.instBEqNativeSymbolRef : BEq NativeSymbolRef

def NN.Backend.instReprNativeSymbolRef.repr : NativeSymbolRef → Nat → Std.Format

@[instance_reducible]

instance NN.Backend.instReprNativeSymbolRef : Repr NativeSymbolRef

inductive NN.Backend.ContractProvenance : Type

Source-level provenance for a contract descriptor. Provenance is not correctness evidence.

• nativeSymbol (ref : NativeSymbolRef) : ContractProvenance

@[instance_reducible]

instance NN.Backend.instDecidableEqContractProvenance : DecidableEq ContractProvenance

def NN.Backend.instDecidableEqContractProvenance.decEq (x✝ x✝¹ : ContractProvenance) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance NN.Backend.instBEqContractProvenance : BEq ContractProvenance

def NN.Backend.instBEqContractProvenance.beq : ContractProvenance → ContractProvenance → Bool

@[instance_reducible]

instance NN.Backend.instReprContractProvenance : Repr ContractProvenance

def NN.Backend.instReprContractProvenance.repr : ContractProvenance → Nat → Std.Format

inductive NN.Backend.TensorLayout : Type

Concrete tensor-layout convention named by a backend contract.

• canonicalTensor : TensorLayout

  TorchLean's ordinary typed tensor representation.

• flatRowMajor : TensorLayout

  Contiguous flat storage with the last axis varying fastest.

• libTorchCudaView : TensorLayout

  A contiguous CUDA tensor view owned by LibTorch.

@[instance_reducible]

instance NN.Backend.instDecidableEqTensorLayout : DecidableEq TensorLayout

def NN.Backend.instReprTensorLayout.repr : TensorLayout → Nat → Std.Format

@[instance_reducible]

instance NN.Backend.instReprTensorLayout : Repr TensorLayout

inductive NN.Backend.ContractObligation : Type

The four contract fields carried by every kernel capsule.

• shape : ContractObligation
• layout : ContractObligation
• value : ContractObligation
• vjp : ContractObligation

@[instance_reducible]

instance NN.Backend.instDecidableEqContractObligation : DecidableEq ContractObligation

def NN.Backend.instReprContractObligation.repr : ContractObligation → Nat → Std.Format

@[instance_reducible]

instance NN.Backend.instReprContractObligation : Repr ContractObligation

inductive NN.Backend.ContractClaim : Type

A structured backend obligation, independent of how evidence for it is obtained.

• shapeSafety (op : BackendOp) : ContractClaim

  Inputs and outputs satisfy the shape rule associated with an operation.

• layoutCompatibility (op : BackendOp) (layout : TensorLayout) : ContractClaim

  Runtime buffers use the declared layout for an operation.

• valueRefinement (op : BackendOp) : ContractClaim

  Forward execution refines the canonical semantics of the operation.

• vjpRefinement (op : BackendOp) (mode : VJPMode) : ContractClaim

  Local backward execution refines the canonical VJP semantics of the operation.

• vjpUnavailable (op : BackendOp) : ContractClaim

  The capsule intentionally supplies no reverse-mode implementation.

def NN.Backend.instDecidableEqContractClaim.decEq (x✝ x✝¹ : ContractClaim) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance NN.Backend.instDecidableEqContractClaim : DecidableEq ContractClaim

def NN.Backend.instReprContractClaim.repr : ContractClaim → Nat → Std.Format

@[instance_reducible]

instance NN.Backend.instReprContractClaim : Repr ContractClaim

inductive NN.Backend.ContractEvidence : Type

How a capsule justifies one part of its contract.

These constructors record engineering evidence and explicit trust boundaries. They do not turn a foreign implementation into a proved refinement.

• runtimeGuard (name : String) : ContractEvidence
• testSuite (name : String) : ContractEvidence
• trustedBoundary (reason : String) : ContractEvidence
• notApplicable : ContractEvidence

@[instance_reducible]

instance NN.Backend.instDecidableEqContractEvidence : DecidableEq ContractEvidence

def NN.Backend.instDecidableEqContractEvidence.decEq (x✝ x✝¹ : ContractEvidence) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance NN.Backend.instReprContractEvidence : Repr ContractEvidence

def NN.Backend.AssurancePolicy.acceptsEvidence (policy : AssurancePolicy) : ContractEvidence → Bool

Whether the policy admits contract evidence of this kind.

structure NN.Backend.ContractDescriptor : Type

A structured contract claim together with its evidence and human-readable explanation.

• claim : ContractClaim
• summary : String
• evidence : ContractEvidence
• provenance : Array ContractProvenance

@[instance_reducible]

instance NN.Backend.instDecidableEqContractDescriptor : DecidableEq ContractDescriptor

def NN.Backend.instDecidableEqContractDescriptor.decEq (x✝ x✝¹ : ContractDescriptor) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance NN.Backend.instReprContractDescriptor : Repr ContractDescriptor

def NN.Backend.ContractDescriptor.guarded (claim : ContractClaim) (summary guard : String) (provenance : Array ContractProvenance := #[]) : ContractDescriptor

A contract claim enforced by a named runtime guard.

def NN.Backend.ContractDescriptor.tested (claim : ContractClaim) (summary suite : String) (provenance : Array ContractProvenance := #[]) : ContractDescriptor

A contract claim covered by a named regression suite.

def NN.Backend.ContractDescriptor.trusted (claim : ContractClaim) (summary reason : String) (provenance : Array ContractProvenance := #[]) : ContractDescriptor

A contract claim delegated to an explicitly named trusted boundary.

def NN.Backend.ContractDescriptor.vjpUnavailable (op : BackendOp) (summary : String) (provenance : Array ContractProvenance := #[]) : ContractDescriptor

Record that a forward-only capsule intentionally has no reverse-mode implementation.

inductive NN.Backend.ReductionPolicy : Type

Ordering contract for reductions. Different valid orders need not be bitwise equal.

The fixed-left graph certificate propagates a reduction only when the selected capsule promises the same left fold as the canonical tensor semantics.

• fixedLeft : ReductionPolicy
• implementationDefined : ReductionPolicy
• notApplicable : ReductionPolicy

@[instance_reducible]

instance NN.Backend.instDecidableEqReductionPolicy : DecidableEq ReductionPolicy

def NN.Backend.instReprReductionPolicy.repr : ReductionPolicy → Nat → Std.Format

@[instance_reducible]

instance NN.Backend.instReprReductionPolicy : Repr ReductionPolicy

def NN.Backend.ReductionPolicy.label : ReductionPolicy → String

Stable report label for reduction order.

structure NN.Backend.NumericalPolicy : Type

Floating-point choices attached to one kernel capsule that numerical certificates consume.

• reduction : ReductionPolicy

  The order a reduction may use, which fixes whether summation is reproducible.

def NN.Backend.instDecidableEqNumericalPolicy.decEq (x✝ x✝¹ : NumericalPolicy) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance NN.Backend.instDecidableEqNumericalPolicy : DecidableEq NumericalPolicy

@[instance_reducible]

instance NN.Backend.instReprNumericalPolicy : Repr NumericalPolicy

def NN.Backend.instReprNumericalPolicy.repr : NumericalPolicy → Nat → Std.Format

def NN.Backend.ContractClaim.matchesObligation (op : BackendOp) (vjpMode : VJPMode) : ContractObligation → ContractClaim → Bool

Whether a claim has the expected kind and operation for a capsule contract field.

structure NN.Backend.KernelCapsule : Type

A contract-carrying fast kernel or reference implementation.

• name : String

  Name used in selection reports and runtime errors.

• op : BackendOp

  Backend operation implemented by this capsule.

• provider : Provider

  Provider responsible for the implementation.

• device : Device

  Device on which the implementation runs.

• trustLevel : TrustLevel

  Assurance level the planner must accept before selection.

• supportsForward : Bool

  Whether the capsule supplies forward execution.

• vjpMode : VJPMode

  Form of reverse-mode support supplied by the capsule.

• shapeContract : ContractDescriptor

  Shape-safety claim and its evidence.

• layoutContract : ContractDescriptor

  Tensor-layout claim and its evidence.

• valueContract : ContractDescriptor

  Forward-value refinement claim and its evidence.

• vjpContract : ContractDescriptor

  Reverse-mode refinement claim and its evidence.

• numericalPolicy : NumericalPolicy

  Floating-point behavior consumed by numerical certificates.

@[instance_reducible]

instance NN.Backend.instDecidableEqKernelCapsule : DecidableEq KernelCapsule

def NN.Backend.instDecidableEqKernelCapsule.decEq (x✝ x✝¹ : KernelCapsule) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance NN.Backend.instReprKernelCapsule : Repr KernelCapsule

def NN.Backend.instReprKernelCapsule.repr : KernelCapsule → Nat → Std.Format

structure NN.Backend.KernelHandler (β : Type) : Type

An executable implementation for one backend operation.

The result type is local to the call site, so this structure also accommodates operations whose Lean signatures differ. The capsule argument gives specialized handlers access to the provider and VJP mode after the common identity checks have succeeded.

• name : String
• op : BackendOp
• provider : Provider
• device : Device
• execute : KernelCapsule → IO β

structure NN.Backend.ExecutableKernel (β : Type) : Type

A selected capsule paired with a handler for the same operation, provider, and device.

These equalities certify dispatch identity only. Numerical correctness remains exactly as strong as the capsule's ContractEvidence; binding a handler does not turn tests or a trusted boundary into a proof.

• capsule : KernelCapsule
• handler : KernelHandler β
• operation_matches : self.handler.op = self.capsule.op
• provider_matches : self.handler.provider = self.capsule.provider
• device_matches : self.handler.device = self.capsule.device

def NN.Backend.KernelHandler.matchesCapsule {β : Type} (handler : KernelHandler β) (capsule : KernelCapsule) : Bool

Whether a runtime handler has the identity advertised by a selected capsule.

def NN.Backend.KernelCapsule.contractsAligned (c : KernelCapsule) : Bool

Whether each descriptor states the obligation advertised by its field.

Evidence is useful only when it supports the right claim. This guard prevents, for example, a value-refinement test from being placed in the shape field and then accepted as shape evidence.

def NN.Backend.KernelCapsule.sameIdentity (a b : KernelCapsule) : Bool

Compare registration identity only. This ignores contracts and numerical policy; use full capsule equality when grouping kernels or comparing assurance evidence.

def NN.Backend.KernelCapsule.validateEagerRequest (c : KernelCapsule) (op : BackendOp) (device : Device) : Except String Unit

Validate the common part of an eager executor request.

This does not decide how an operation invokes a provider. It prevents every runtime operation from reimplementing the op, device, and wiring checks before interpreting the capsule locally.

def NN.Backend.KernelCapsule.bind {β : Type} (c : KernelCapsule) (handler : KernelHandler β) : Except String (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.

def NN.Backend.KernelCapsule.allowedBy (policy : KernelPolicy) (c : KernelCapsule) : Bool

Whether the assurance policy admits this capsule's trust level.

def NN.Backend.KernelCapsule.matchesPreference (policy : KernelPolicy) (c : KernelCapsule) : Bool

Whether the provider preference admits this capsule.

def NN.Backend.KernelCapsule.matchesDevice (policy : KernelPolicy) (c : KernelCapsule) : Bool

Whether this capsule is available on the selected device.

def NN.Backend.KernelCapsule.matchesVJP (policy : KernelPolicy) (c : KernelCapsule) : Bool

Whether the capsule's gradient boundary is compatible with the requested kernel policy.

none is inference mode, so any forward-capable capsule is suitable even when it also advertises a VJP. In torchLeanTape mode TorchLean owns the global tape and backward traversal. A capsule may still implement its local VJP either as TorchLean operations or as a named backend kernel; backendVJP requests the latter specifically.

def NN.Backend.KernelCapsule.admissible (policy : KernelPolicy) (c : KernelCapsule) : Bool

Planner-side admissibility predicate for a single capsule.

def NN.Backend.ExecutableKernel.run {β : Type} (kernel : ExecutableKernel β) : IO β

Invoke the handler bound to a selected capsule.

def NN.Backend.chooseCapsuleFor? (policy : KernelPolicy) (op : BackendOp) (capsules : Array KernelCapsule) : Option KernelCapsule

Pick an admissible capsule for a typed operation.

An .only preference filters the catalog through admissible. An .auto preference preserves catalog order. A .prefer provider request first searches that provider and then falls back to the ordinary catalog, so preference does not depend on module registration order.