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 the plan crosses a trusted-external boundary. Audits are stored inside numerical certificates and compared on replay, so they must have decidable equality.

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

Whether this capsule crosses a trusted external boundary.

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

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

@[instance_reducible]

instance NN.Backend.instReprKernelAudit : Repr KernelAudit

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

Build an audit row from a selected planner kernel.

def NN.Backend.KernelAudit.isTrustedExternal (a : KernelAudit) : Bool

Whether this selected kernel crosses a trusted external boundary.

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

@[instance_reducible]

instance NN.Backend.instDecidableEqKernelPlanAudit : DecidableEq KernelPlanAudit

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

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

@[instance_reducible]

instance NN.Backend.instReprKernelPlanAudit : Repr KernelPlanAudit

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

Capsule names selected by the plan, in plan order.

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

Operation names whose selected capsule is trusted external.

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

Whether the plan crosses any trusted external boundary.

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

Audit a selected kernel plan.

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

Whether a selected kernel plan crosses any trusted external boundary.

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

Operation names whose selected capsules are trusted external.