Backend Contract Checks

The planner admits a capsule only when its operation, device, provider, gradient mode, trust level, and contract claims match the kernel policy. The contract audit then looks inside the selected capsules: each of the four descriptors must rest on evidence the assurance policy accepts.

Acceptance repeats both checks at the execution boundary. This matters because PlannedKernel is a public diagnostic record and can therefore be assembled directly by a caller. Accepted values carry the successful gate as a proof field, and graph acceptance derives its grouped audit plan from the graph plan instead of accepting unrelated groups from the caller.

structure NN.Backend.ObligationReport : Type

One contract obligation of one selected backend kernel.

• op : BackendOp
• capsuleName : String
• obligation : ContractObligation
• claim : ContractClaim
• evidence : ContractEvidence

def NN.Backend.instReprObligationReport.repr : ObligationReport → ℕ → Std.Format

@[instance_reducible]

instance NN.Backend.instReprObligationReport : Repr ObligationReport

inductive NN.Backend.ContractCheck : Type

Result of checking a plan audit against an assurance policy.

• accepted : ContractCheck
• rejected (reports : Array ObligationReport) : ContractCheck

@[instance_reducible]

instance NN.Backend.instReprContractCheck : Repr ContractCheck

def NN.Backend.instReprContractCheck.repr : ContractCheck → ℕ → Std.Format

def NN.Backend.KernelAudit.obligationReports (a : KernelAudit) : Array ObligationReport

All contract obligations of a selected kernel.

def NN.Backend.KernelPlanAudit.obligationReports (a : KernelPlanAudit) : Array ObligationReport

All contract obligations of all selected kernels.

def NN.Backend.KernelPlanAudit.rejectedReports (policy : AssurancePolicy) (a : KernelPlanAudit) : Array ObligationReport

Obligations whose evidence the policy does not accept.

def NN.Backend.KernelPlanAudit.checkContracts (policy : AssurancePolicy) (a : KernelPlanAudit) : ContractCheck

Check every obligation of a plan audit against an assurance policy.

def NN.Backend.KernelPlan.checkContracts (policy : AssurancePolicy) (p : KernelPlan) : ContractCheck

Check every obligation of a selected plan against an assurance policy.

def NN.Backend.GroupedKernelPlan.checkContracts (policy : AssurancePolicy) (p : GroupedKernelPlan) : ContractCheck

Check every obligation of a grouped graph plan against an assurance policy.

inductive NN.Backend.AcceptanceFailure : Type

One reason a planned kernel cannot cross the execution boundary.

• operationMismatch (planned capsule : BackendOp) : AcceptanceFailure

  The planned operation and the capsule's advertised operation differ.

• forwardUnsupported (op : BackendOp) (capsuleName : String) : AcceptanceFailure

  The capsule has no forward implementation.

• contractsMisaligned (op : BackendOp) (capsuleName : String) : AcceptanceFailure

  A contract descriptor states a claim for the wrong obligation.

• trustRejected (op : BackendOp) (capsuleName : String) (trust : TrustLevel) : AcceptanceFailure

  The selected assurance policy does not admit the capsule's trust level.

• providerRejected (op : BackendOp) (capsuleName : String) (provider : Provider) : AcceptanceFailure

  The provider policy excludes the capsule.

• deviceMismatch (op : BackendOp) (capsuleName : String) (requested actual : Device) : AcceptanceFailure

  The capsule targets a different device.

• vjpMismatch (op : BackendOp) (capsuleName : String) (requested actual : VJPMode) : AcceptanceFailure

  The capsule cannot satisfy the requested gradient mode.

• evidenceRejected (report : ObligationReport) : AcceptanceFailure

  One contract descriptor rests on evidence rejected by the assurance policy.

@[instance_reducible]

instance NN.Backend.instReprAcceptanceFailure : Repr AcceptanceFailure

def NN.Backend.instReprAcceptanceFailure.repr : AcceptanceFailure → ℕ → Std.Format

def NN.Backend.PlannedKernel.acceptable (policy : KernelPolicy) (kernel : PlannedKernel) : Bool

Whether a directly supplied planned kernel satisfies the complete policy and evidence gate.

def NN.Backend.PlannedKernel.acceptanceFailures (policy : KernelPolicy) (kernel : PlannedKernel) : Array AcceptanceFailure

Explain every failed part of the complete kernel acceptance gate.

def NN.Backend.GroupedKernelPlan.acceptanceFailures (policy : KernelPolicy) (plan : GroupedKernelPlan) : Array AcceptanceFailure

Explain every kernel that fails the complete policy and evidence gate.

def NN.Backend.GroupedKernelPlan.acceptable (policy : KernelPolicy) (plan : GroupedKernelPlan) : Bool

Whether every grouped kernel satisfies the complete policy and evidence gate.

structure NN.Backend.AcceptedKernel : Type

One planned operation whose capsule has passed the complete policy and evidence gate.

• op : BackendOp

  The operation the kernel implements.

• capsule : KernelCapsule

  The capsule that carries the kernel's contract claims and evidence.

• policy : KernelPolicy

  The policy the capsule was checked against.

• accepted : PlannedKernel.acceptable self.policy { op := self.op, capsule := self.capsule } = true

  Evidence that the complete policy and evidence gate accepted this kernel.

opaque NN.Backend.AcceptedKernel.Internal.create (op : BackendOp) (capsule : KernelCapsule) (policy : KernelPolicy) (accepted : PlannedKernel.acceptable policy { op := op, capsule := capsule } = true) : AcceptedKernel

Construct an accepted kernel after the execution-boundary check succeeds.

@[instance_reducible]

instance NN.Backend.instReprAcceptedKernel : Repr AcceptedKernel

def NN.Backend.PlannedKernel.accept (policy : KernelPolicy) (kernel : PlannedKernel) : Except (Array AcceptanceFailure) AcceptedKernel

Check a planned kernel and return a value that an executor can consume only on success.

structure NN.Backend.AcceptedGraphKernelPlan : Type

A graph kernel plan after grouping and contract checking.

• graphPlan : IR.GraphKernelPlan

  The node-level plan whose selected contracts were checked.

• groupedPlan : GroupedKernelPlan

  Audit groups derived from the node-level plan.

• grouped_eq : self.groupedPlan = self.graphPlan.toCoalescedGroups

  Grouping cannot substitute a different plan's contract evidence.

• policy : KernelPolicy

  The policy applied to every audit group.

• accepted : GroupedKernelPlan.acceptable self.policy self.groupedPlan = true

  Every group passes the complete policy and evidence gate.

opaque NN.Backend.AcceptedGraphKernelPlan.Internal.create (graphPlan : IR.GraphKernelPlan) (policy : KernelPolicy) (accepted : GroupedKernelPlan.acceptable policy graphPlan.toCoalescedGroups = true) : AcceptedGraphKernelPlan

Construct an accepted graph plan after every grouped kernel passes the execution gate.

@[instance_reducible]

instance NN.Backend.instReprAcceptedGraphKernelPlan : Repr AcceptedGraphKernelPlan

def NN.Backend.AcceptedGraphKernelPlan.nodeIds (p : AcceptedGraphKernelPlan) : Array ℕ

Source IR node ids covered by the accepted grouped plan.

def NN.Backend.AcceptedGraphKernelPlan.capsuleNames (p : AcceptedGraphKernelPlan) : Array String

Selected capsule names in accepted group order.

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

Audit for the accepted grouped plan.

inductive NN.Backend.GraphKernelPlanResult : Type

Result of planning, grouping, and checking a graph.

• accepted (plan : AcceptedGraphKernelPlan) : GraphKernelPlanResult
• rejected (groupedPlan : GroupedKernelPlan) (failures : Array AcceptanceFailure) : GraphKernelPlanResult

@[instance_reducible]

instance NN.Backend.instReprGraphKernelPlanResult : Repr GraphKernelPlanResult

def NN.Backend.instReprGraphKernelPlanResult.repr : GraphKernelPlanResult → ℕ → Std.Format

def NN.Backend.acceptGraphKernelPlan (graphPlan : IR.GraphKernelPlan) (policy : KernelPolicy) : GraphKernelPlanResult

Derive, check, and expose a grouped graph plan only when every selected kernel passes.

Deriving the groups here keeps the accepted audit tied to the exact graph plan that produced it.