Backend Capsules

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

The capsule does not prove the foreign implementation. It records the contract TorchLean expects from that implementation: which op it implements, which spec it refines, what layout and shape conventions are assumed, how the value/VJP claims are justified, and what trust level the planner must account for.

structure NN.Backend.SourceRef : Type

A source file inside the TorchLean checkout that supports a backend contract.

• path : String

@[implicit_reducible]

instance NN.Backend.instDecidableEqSourceRef : DecidableEq SourceRef

def NN.Backend.instDecidableEqSourceRef.decEq (x✝ x✝¹ : SourceRef) : Decidable (x✝ = x✝¹)

@[implicit_reducible]

instance NN.Backend.instBEqSourceRef : BEq SourceRef

def NN.Backend.instBEqSourceRef.beq : SourceRef → SourceRef → Bool

def NN.Backend.instReprSourceRef.repr : SourceRef → Nat → Std.Format

@[implicit_reducible]

instance NN.Backend.instReprSourceRef : Repr SourceRef

structure NN.Backend.NativeSymbolRef : Type

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

The 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

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

@[implicit_reducible]

instance NN.Backend.instDecidableEqNativeSymbolRef : DecidableEq NativeSymbolRef

@[implicit_reducible]

instance NN.Backend.instBEqNativeSymbolRef : BEq NativeSymbolRef

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

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

@[implicit_reducible]

instance NN.Backend.instReprNativeSymbolRef : Repr NativeSymbolRef

inductive NN.Backend.RuntimeSupport : Type

Whether a selected capsule is wired to an executable runtime path.

• eager : RuntimeSupport

  The capsule can be selected by an eager runtime path.

• testOnly : RuntimeSupport

  The capsule has a direct bridge/check, but is not selected by the eager runtime yet.

• plannerOnly : RuntimeSupport

  The capsule is useful for planning/auditing only.

• notWired : RuntimeSupport

  The capsule is intentionally registered before runtime wiring exists.

@[implicit_reducible]

instance NN.Backend.instDecidableEqRuntimeSupport : DecidableEq RuntimeSupport

def NN.Backend.instReprRuntimeSupport.repr : RuntimeSupport → Nat → Std.Format

@[implicit_reducible]

instance NN.Backend.instReprRuntimeSupport : Repr RuntimeSupport

inductive NN.Backend.ContractProvenance : Type

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

• sourceFile (ref : SourceRef) : ContractProvenance
• nativeSymbol (ref : NativeSymbolRef) : ContractProvenance
• note (text : String) : ContractProvenance

@[implicit_reducible]

instance NN.Backend.instDecidableEqContractProvenance : DecidableEq ContractProvenance

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

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

@[implicit_reducible]

instance NN.Backend.instBEqContractProvenance : BEq ContractProvenance

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

@[implicit_reducible]

instance NN.Backend.instDecidableEqTensorLayout : DecidableEq TensorLayout

@[implicit_reducible]

instance NN.Backend.instReprTensorLayout : Repr TensorLayout

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

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) (specName : String) : ContractClaim

  Forward execution refines the named mathematical specification.

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

  Local backward execution refines the named VJP specification.

@[implicit_reducible]

instance NN.Backend.instDecidableEqContractClaim : DecidableEq ContractClaim

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

@[implicit_reducible]

instance NN.Backend.instReprContractClaim : Repr ContractClaim

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

inductive NN.Backend.ContractEvidence : Type

How a capsule justifies one part of its contract.

runtimeGuard and testSuite record useful engineering assurance but do not discharge a theorem. Only theorem and checker contain proof terms.

• theorem (theoremName : String) (statement : Prop) (proof : statement) : ContractEvidence
• checker (checkerName : String) (statement : Prop) (accepted : Bool) (sound : accepted = true → statement) (acceptanceProof : accepted = true) : ContractEvidence
• runtimeGuard (name : String) : ContractEvidence
• testSuite (name : String) : ContractEvidence
• fuzzOracle (name : String) : ContractEvidence
• trustedBoundary (reason : String) : ContractEvidence
• notProvided : ContractEvidence

@[implicit_reducible]

instance NN.Backend.instReprContractEvidence : Repr ContractEvidence

structure NN.Backend.ContractDescriptor : Type

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

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

@[implicit_reducible]

instance NN.Backend.instReprContractDescriptor : Repr ContractDescriptor

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

A contract claim enforced by a named runtime guard.

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

A contract claim covered by a named regression suite.

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

A contract claim delegated to an explicitly named trusted boundary.

inductive NN.Backend.ContractObligationKind : Type

The four contract fields carried by every kernel capsule.

• shape : ContractObligationKind
• layout : ContractObligationKind
• value : ContractObligationKind
• vjp : ContractObligationKind

@[implicit_reducible]

instance NN.Backend.instDecidableEqContractObligationKind : DecidableEq ContractObligationKind

def NN.Backend.instReprContractObligationKind.repr : ContractObligationKind → Nat → Std.Format

@[implicit_reducible]

instance NN.Backend.instReprContractObligationKind : Repr ContractObligationKind

def NN.Backend.ContractClaim.matchesObligation (op : BackendOp) (vjpMode : VJPMode) : ContractObligationKind → 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
• op : BackendOp
• provider : Provider
• device : Device
• specName : String
• trustLevel : TrustLevel
• supportsForward : Bool
• vjpMode : VJPMode
• runtimeSupport : RuntimeSupport
• shapeContract : ContractDescriptor
• layoutContract : ContractDescriptor
• valueContract : ContractDescriptor
• vjpContract : ContractDescriptor
• notes : String

@[implicit_reducible]

instance NN.Backend.instReprKernelCapsule : Repr KernelCapsule

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

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

Whether each descriptor states the obligation advertised by its field.

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

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

Stable identity used when adjacent graph nodes select the same registered capsule.

def NN.Backend.KernelCapsule.allowedBy (cfg : ExecutionConfig) (c : KernelCapsule) : Bool

Whether the trust policy admits this capsule.

def NN.Backend.KernelCapsule.matchesPreference (cfg : ExecutionConfig) (c : KernelCapsule) : Bool

Whether the backend preference admits this capsule's provider.

def NN.Backend.KernelCapsule.matchesDevice (cfg : ExecutionConfig) (c : KernelCapsule) : Bool

Whether this capsule is available on the selected device.

def NN.Backend.KernelCapsule.matchesVJP (cfg : ExecutionConfig) (c : KernelCapsule) : Bool

Whether the capsule's gradient boundary is compatible with the requested execution config.

none is inference mode, so any forward-capable capsule is suitable even when it also advertises a VJP. externalAutograd is intentionally opt-in. A native backend VJP is still compatible with the normal TorchLean tape mode: the TorchLean tape owns the node and calls the backend for the local VJP.

def NN.Backend.KernelCapsule.admissible (cfg : ExecutionConfig) (c : KernelCapsule) : Bool

Planner-side admissibility predicate for a single capsule.

def NN.Backend.chooseCapsuleFor? (cfg : ExecutionConfig) (op : BackendOp) (capsules : List KernelCapsule) : Option KernelCapsule

Pick the first admissible capsule for a typed operation.