Backend Acceptance Gates

Policy gates for contract-carrying backend plans.

The planner can select a backend capsule and the audit/recheck layers can report its obligations. The gate layer turns those reports into an explicit yes/no decision before a plan is accepted for a particular run mode.

structure NN.Backend.AcceptancePolicy : Type

Policy used to accept or reject a selected backend plan after audit/recheck.

• requireEvidence : Bool
• allowRuntimeGuards : Bool
• allowTestEvidence : Bool
• allowTrustedBoundaries : Bool
• allowFuzzEvidence : Bool

@[implicit_reducible]

instance NN.Backend.instReprAcceptancePolicy : Repr AcceptancePolicy

def NN.Backend.instReprAcceptancePolicy.repr : AcceptancePolicy → ℕ → Std.Format

def NN.Backend.AcceptancePolicy.strict : AcceptancePolicy

Strict verification-oriented policy: no missing, fuzz-only, or trusted-boundary evidence.

def NN.Backend.AcceptancePolicy.checkedRuntime : AcceptancePolicy

Runtime policy for maintained paths with guards and regression coverage.

def NN.Backend.AcceptancePolicy.allowTrustedRuntime : AcceptancePolicy

Runtime scaling policy: guards/tests are admitted and trusted external boundaries are explicit.

def NN.Backend.AcceptancePolicy.acceptsDisposition (p : AcceptancePolicy) (d : EvidenceDisposition) : Bool

Whether an obligation disposition is admitted by this policy.

inductive NN.Backend.GateFailure : Type

Why a candidate plan was rejected by an acceptance gate.

• missingEvidence (reports : List ObligationReport) : GateFailure
• runtimeGuardEvidence (reports : List ObligationReport) : GateFailure
• testEvidence (reports : List ObligationReport) : GateFailure
• trustedBoundary (reports : List ObligationReport) : GateFailure
• fuzzEvidence (reports : List ObligationReport) : GateFailure

def NN.Backend.instReprGateFailure.repr : GateFailure → ℕ → Std.Format

@[implicit_reducible]

instance NN.Backend.instReprGateFailure : Repr GateFailure

inductive NN.Backend.GateResult : Type

Result of applying an acceptance policy to an execution audit.

• accepted : GateResult
• rejected (failures : List GateFailure) : GateResult

def NN.Backend.instReprGateResult.repr : GateResult → ℕ → Std.Format

@[implicit_reducible]

instance NN.Backend.instReprGateResult : Repr GateResult

def NN.Backend.ObligationReport.acceptedBy (policy : AcceptancePolicy) (r : ObligationReport) : Bool

Whether this obligation report is admitted by an acceptance policy.

def NN.Backend.ObligationReport.isFuzzed (r : ObligationReport) : Bool

Whether this obligation is fuzz-backed.

def NN.Backend.ObligationReport.isGuarded (r : ObligationReport) : Bool

def NN.Backend.ObligationReport.isTested (r : ObligationReport) : Bool

def NN.Backend.ExecutionAudit.guardedReports (a : ExecutionAudit) : List ObligationReport

def NN.Backend.ExecutionAudit.testedReports (a : ExecutionAudit) : List ObligationReport

def NN.Backend.ExecutionAudit.fuzzReports (a : ExecutionAudit) : List ObligationReport

Fuzz-backed recheck obligations.

def NN.Backend.ExecutionAudit.gateFailures (policy : AcceptancePolicy) (a : ExecutionAudit) : List GateFailure

Gate failures induced by an acceptance policy.

def NN.Backend.ExecutionAudit.gate (policy : AcceptancePolicy) (a : ExecutionAudit) : GateResult

Apply an acceptance policy to an execution audit.

theorem NN.Backend.ExecutionAudit.gate_eq_accepted_iff_gateFailures_eq_nil (policy : AcceptancePolicy) (a : ExecutionAudit) : gate policy a = GateResult.accepted ↔ gateFailures policy a = []

An audit is accepted by a policy exactly when the policy reports no gate failures.

def NN.Backend.ExecutionPlan.gate (policy : AcceptancePolicy) (p : ExecutionPlan) : GateResult

Apply an acceptance policy to a selected execution plan.

def NN.Backend.ExecutionPlan.acceptedBy (policy : AcceptancePolicy) (p : ExecutionPlan) : Bool

Whether a selected execution plan is accepted by a policy.

structure NN.Backend.AcceptedKernel : Type

One planned operation whose capsule has passed an acceptance policy.

• op : BackendOp
• capsule : KernelCapsule
• policy : AcceptancePolicy
• gateProof : ExecutionPlan.gate self.policy { kernels := [{ op := self.op, capsule := self.capsule }] } = GateResult.accepted

@[implicit_reducible]

instance NN.Backend.instReprAcceptedKernel : Repr AcceptedKernel

def NN.Backend.PlannedKernel.accept (policy : AcceptancePolicy) (k : PlannedKernel) : Except (List GateFailure) AcceptedKernel

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

def NN.Backend.GraphLoweringPlan.gate (policy : AcceptancePolicy) (p : GraphLoweringPlan) : GateResult

Apply an acceptance policy to a lowered backend plan.

def NN.Backend.GraphLoweringPlan.acceptedBy (policy : AcceptancePolicy) (p : GraphLoweringPlan) : Bool

Whether a lowered backend plan is accepted by a policy.