Backend Kernel Groups

GraphKernelPlan chooses a capsule for each runtime-relevant IR node. A GroupedKernelPlan places adjacent choices with the same operation and complete capsule in one audit group, so a graph with twenty consecutive ReLU nodes produces one audit row instead of twenty. Grouping does not translate graph semantics, fuse operations, or claim that a group executes as one kernel launch.

structure NN.Backend.KernelGroup : Type

One audit group, with source IR node ids retained for diagnostics.

• nodeIds : Array ℕ
• op : BackendOp
• capsule : KernelCapsule

def NN.Backend.instReprKernelGroup.repr : KernelGroup → ℕ → Std.Format

@[instance_reducible]

instance NN.Backend.instReprKernelGroup : Repr KernelGroup

structure NN.Backend.GroupedKernelPlan : Type

A node-level graph plan grouped for trust-boundary audit.

• groups : Array KernelGroup

def NN.Backend.instReprGroupedKernelPlan.repr : GroupedKernelPlan → ℕ → Std.Format

@[instance_reducible]

instance NN.Backend.instReprGroupedKernelPlan : Repr GroupedKernelPlan

def NN.Backend.KernelGroup.toPlannedKernel (g : KernelGroup) : PlannedKernel

Project the operation and capsule selected for this group.

def NN.Backend.KernelGroup.canAppend (g : KernelGroup) (k : IR.PlannedNodeKernel) : Bool

Whether a planned node can share this audit group without losing contract evidence.

Matching dispatch identities alone is insufficient: a caller can supply capsules with the same name, operation, provider, and device but different trust or numerical policies.

def NN.Backend.KernelGroup.appendNode (g : KernelGroup) (k : IR.PlannedNodeKernel) : KernelGroup

Append a node to an existing group, preserving source-node provenance.

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

Source IR node ids covered by the grouped plan, in graph order.

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

Selected capsule names, in group order.

def NN.Backend.GroupedKernelPlan.toKernelPlan (p : GroupedKernelPlan) : KernelPlan

Project groups to the capsule rows consumed by the contract check.

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

Audit the selected backend boundaries of the grouped plan.

def NN.Backend.IR.PlannedNodeKernel.toSingletonGroup (k : PlannedNodeKernel) : KernelGroup

Place one graph-planned node in its own group.

def NN.Backend.IR.GraphKernelPlan.pushKernel (groups : Array KernelGroup) (k : PlannedNodeKernel) : Array KernelGroup

Add one planned node, sharing the preceding group when the boundary is identical.

def NN.Backend.IR.GraphKernelPlan.toCoalescedGroups (p : GraphKernelPlan) : GroupedKernelPlan

Adjacent nodes with the same backend boundary share one audit group.