Backend Reports

Small human-readable reports for contract-carrying backend plans.

The planner data is intentionally precise; these helpers are the user-facing explanation layer. They are useful in examples, command-line choosers, docs, and debugging output.

def NN.Backend.Provider.label : Provider → String

Short stable spelling for a backend provider.

def NN.Backend.TrustLevel.label : TrustLevel → String

Short stable spelling for a capsule trust level.

def NN.Backend.AssurancePolicy.label (policy : AssurancePolicy) : String

Short stable spelling for a profile assurance policy.

def NN.Backend.VJPMode.label : VJPMode → String

Short stable spelling for how a capsule handles backward/VJP.

def NN.Backend.TensorLayout.label : TensorLayout → String

Short stable spelling for a tensor-layout contract.

def NN.Backend.ContractClaim.label : ContractClaim → String

Human-readable statement of a structured backend obligation.

def NN.Backend.ContractEvidence.label : ContractEvidence → String

Concise description of the evidence attached to a contract claim.

def NN.Backend.ContractDescriptor.reportLine (field : String) (d : ContractDescriptor) : String

One report line for a named contract field.

def NN.Backend.KernelAudit.reportLine (a : KernelAudit) : String

One-line summary for a selected backend capsule.

def NN.Backend.KernelAudit.detailedReportLines (a : KernelAudit) : List String

Full contract report for a selected backend capsule.

def NN.Backend.ExecutionAudit.reportLines (a : ExecutionAudit) : List String

Human-readable lines for all selected capsules.

def NN.Backend.ExecutionAudit.detailedReportLines (a : ExecutionAudit) : List String

Human-readable contract details for all selected capsules.

def NN.Backend.ExecutionPlan.reportLines (p : ExecutionPlan) : List String

Human-readable lines for a selected backend plan.

def NN.Backend.ExecutionPlan.detailedReportLines (p : ExecutionPlan) : List String

Human-readable contract details for a selected backend plan.

def NN.Backend.BackendProfile.summary (p : BackendProfile) : String

One-line profile description for logs and interactive choosers.

def NN.Backend.BackendProfile.planReport (p : BackendProfile) (ops : List BackendOp) : Except String String

Plan a list of backend ops and format the selected capsules.