Accepted Backend Plans

One entry point for the backend-contract pipeline.

This module ties together target availability, graph planning, conservative lowering, recheck, and acceptance gates. It is intentionally still data-level: it produces a lowered plan that has passed a policy gate, or it returns the gate failures. Execution backends can consume the accepted lowered plan without manually repeating the trust-boundary checks.

structure NN.Backend.AcceptedGraphPlan : Type

A graph backend plan after planning, lowering, and acceptance-gate checking.

• graphPlan : IR.GraphExecutionPlan
• loweringPlan : GraphLoweringPlan
• policy : AcceptancePolicy
• gateProof : GraphLoweringPlan.gate self.policy self.loweringPlan = GateResult.accepted

@[implicit_reducible]

instance NN.Backend.instReprAcceptedGraphPlan : Repr AcceptedGraphPlan

def NN.Backend.AcceptedGraphPlan.nodeIds (p : AcceptedGraphPlan) : List ℕ

Source IR node ids covered by the accepted lowering.

def NN.Backend.AcceptedGraphPlan.capsuleNames (p : AcceptedGraphPlan) : List String

Selected capsule names in accepted lowering order.

def NN.Backend.AcceptedGraphPlan.audit (p : AcceptedGraphPlan) : ExecutionAudit

Audit for the accepted lowering.

def NN.Backend.AcceptedGraphPlan.obligationReports (p : AcceptedGraphPlan) : List ObligationReport

Recheck reports for the accepted lowering.

inductive NN.Backend.AcceptedPlanResult : Type

Result of planning/lowering/gating a graph.

• accepted (plan : AcceptedGraphPlan) : AcceptedPlanResult
• rejected (loweringPlan : GraphLoweringPlan) (failures : List GateFailure) : AcceptedPlanResult

@[implicit_reducible]

instance NN.Backend.instReprAcceptedPlanResult : Repr AcceptedPlanResult

def NN.Backend.instReprAcceptedPlanResult.repr : AcceptedPlanResult → ℕ → Std.Format

def NN.Backend.AcceptedPlanResult.isAccepted : AcceptedPlanResult → Bool

Whether the pipeline returned an accepted plan.

def NN.Backend.AcceptedPlanResult.failures : AcceptedPlanResult → List GateFailure

Gate failures when the pipeline rejected the plan.

def NN.Backend.acceptGraphPlan (graphPlan : IR.GraphExecutionPlan) (loweringPlan : GraphLoweringPlan) (policy : AcceptancePolicy) : AcceptedPlanResult

Gate a graph lowering and expose an accepted plan only when every obligation passes policy.