Backend Recheck Obligations

Plan audits say which backend capsules were selected. Recheck obligations unpack the contract fields inside those capsules: shape, layout, value, and VJP evidence.

This layer is intentionally data-level. It does not claim that a foreign kernel is proved. It records whether each obligation is backed by a theorem, checker, fuzz oracle, trusted boundary, or is missing evidence.

inductive NN.Backend.ContractObligation : Type

The contract obligation attached to a backend capsule.

• shape : ContractObligation
• layout : ContractObligation
• value : ContractObligation
• vjp : ContractObligation

@[implicit_reducible]

instance NN.Backend.instDecidableEqContractObligation : DecidableEq ContractObligation

def NN.Backend.instReprContractObligation.repr : ContractObligation → Nat → Std.Format

@[implicit_reducible]

instance NN.Backend.instReprContractObligation : Repr ContractObligation

inductive NN.Backend.EvidenceDisposition : Type

Normalized evidence class used by reports and policy filters.

• proved : EvidenceDisposition
• checked : EvidenceDisposition
• guarded : EvidenceDisposition
• tested : EvidenceDisposition
• fuzzed : EvidenceDisposition
• trusted : EvidenceDisposition
• missing : EvidenceDisposition

@[implicit_reducible]

instance NN.Backend.instDecidableEqEvidenceDisposition : DecidableEq EvidenceDisposition

@[implicit_reducible]

instance NN.Backend.instReprEvidenceDisposition : Repr EvidenceDisposition

def NN.Backend.instReprEvidenceDisposition.repr : EvidenceDisposition → Nat → Std.Format

def NN.Backend.ContractEvidence.disposition (e : ContractEvidence) : EvidenceDisposition

Convert detailed evidence into the coarse class used by recheck reports.

def NN.Backend.ContractEvidence.isProvided (e : ContractEvidence) : Bool

Whether this evidence gives any non-missing justification.

def NN.Backend.ContractEvidence.isTrustedBoundary (e : ContractEvidence) : Bool

Whether this evidence crosses a trusted boundary.

structure NN.Backend.ObligationReport : Type

Recheck row for one obligation of one selected backend kernel.

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

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

@[implicit_reducible]

instance NN.Backend.instReprObligationReport : Repr ObligationReport

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

Whether this obligation has no recorded evidence.

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

Whether this obligation is discharged only by a trusted boundary.

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

All contract obligations associated with a selected kernel.

def NN.Backend.KernelAudit.missingObligations (a : KernelAudit) : List ContractObligation

Obligations without any recorded evidence.

def NN.Backend.KernelAudit.trustedBoundaryObligations (a : KernelAudit) : List ContractObligation

Obligations discharged by a trusted boundary.

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

All recheck obligations for all selected kernels.

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

Recheck obligations with no recorded evidence.

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

Recheck obligations discharged by trusted external boundaries.

def NN.Backend.ExecutionAudit.hasNoMissingEvidence (a : ExecutionAudit) : Bool

Whether every obligation has a non-missing audit classification.

def NN.Backend.ExecutionPlan.hasNoMissingEvidence (p : ExecutionPlan) : Bool

Whether every selected backend contract obligation has a non-missing audit classification.

def NN.Backend.ExecutionPlan.missingReports (p : ExecutionPlan) : List ObligationReport

Missing recheck obligations for a selected plan.

def NN.Backend.ExecutionPlan.trustedBoundaryReports (p : ExecutionPlan) : List ObligationReport

Trusted-boundary recheck obligations for a selected plan.