Backend Plan Audits

Inspection data for contract-carrying kernel plans.

The planner chooses capsules. The audit layer records what that choice means for trust boundaries: which provider was selected, which device it targets, how its shape, layout, value, and VJP obligations are supported, and whether a capsule has the trustedExternal classification. A checked LibTorch capsule still executes foreign code. These classifications distinguish the declared evidence, not whether Lean has proved the implementation. Audits are stored inside numerical certificates and compared on replay, so they must have decidable equality.

structure NN.Backend.KernelAudit : Type

Audit row for one selected backend kernel.

• op : BackendOp
• capsuleName : String
• provider : Provider
• device : Device
• trustLevel : TrustLevel
• vjpMode : VJPMode
• shapeContract : ContractDescriptor
• layoutContract : ContractDescriptor
• valueContract : ContractDescriptor
• vjpContract : ContractDescriptor
• numericalPolicy : NumericalPolicy

def NN.Backend.instDecidableEqKernelAudit.decEq (x✝ x✝¹ : KernelAudit) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance NN.Backend.instDecidableEqKernelAudit : DecidableEq KernelAudit

@[instance_reducible]

instance NN.Backend.instReprKernelAudit : Repr KernelAudit

def NN.Backend.instReprKernelAudit.repr : KernelAudit → Nat → Std.Format

def NN.Backend.KernelAudit.ofPlannedKernel (k : PlannedKernel) : KernelAudit

Build an audit row from a selected planner kernel.

def NN.Backend.KernelAudit.contracts (a : KernelAudit) : Array (ContractObligation × ContractDescriptor)

The four contract descriptors of the selected kernel, paired with the field each one fills.

structure NN.Backend.KernelPlanAudit : Type

Audit view of selected kernel capsules.

• kernels : Array KernelAudit

def NN.Backend.instDecidableEqKernelPlanAudit.decEq (x✝ x✝¹ : KernelPlanAudit) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance NN.Backend.instDecidableEqKernelPlanAudit : DecidableEq KernelPlanAudit

@[instance_reducible]

instance NN.Backend.instReprKernelPlanAudit : Repr KernelPlanAudit

def NN.Backend.instReprKernelPlanAudit.repr : KernelPlanAudit → Nat → Std.Format

def NN.Backend.KernelPlanAudit.capsuleNames (a : KernelPlanAudit) : Array String

Capsule names selected by the plan, in plan order.

def NN.Backend.KernelPlanAudit.hasTrustedExternal (a : KernelPlanAudit) : Bool

Whether any selected capsule has the trustedExternal evidence classification.

def NN.Backend.KernelPlan.audit (p : KernelPlan) : KernelPlanAudit

Audit a selected kernel plan.

def NN.Backend.KernelPlan.hasTrustedExternal (p : KernelPlan) : Bool

Whether any selected capsule has the trustedExternal evidence classification.

def NN.Backend.KernelPlan.trustedExternalOps (p : KernelPlan) : Array String

Operation names whose selected capsules are trusted external.