Backend-linked graph numerical certificates

Certificate data, backend-plan linkage, generation, checking, and checked execution interfaces. Most users should import NN.Proofs.RuntimeApprox.Graph.NumericalCertificate.

Backend-linked graph certificates

structure Proofs.RuntimeApprox.NumericalCertificate.GraphNumericalCertificate : Type

Untrusted certificate data.

The audit field records the data selected by kernel selection. The checker replans the graph under profileName and compares the complete audit, so an artifact cannot choose its own provider, trust level, or evidence classification.

• profileName : String

  Backend profile the artifact claims to have been planned under.

• registryName : String

  Numerical operation registry the artifact claims produced its range rows.

• sources : Array SourceRange

  Interval assumptions on the graph's external sources.

• ranges : Array NodeRange

  Claimed node-by-node range rows; the checker replays and compares them.

• audit : NN.Backend.KernelPlanAudit

  Claimed kernel-plan audit; the checker replans the graph and compares it.

@[instance_reducible]

instance Proofs.RuntimeApprox.NumericalCertificate.instReprGraphNumericalCertificate : Repr GraphNumericalCertificate

structure Proofs.RuntimeApprox.NumericalCertificate.RegistryCheckedCertificate : Type

Result returned after registry replay and backend-plan checking.

The checker reconstructs the range rows and proves that the artifact matches that reconstruction. This structure does not by itself prove that the rows enclose the graph's real denotation; that semantic statement is carried separately by ProvedRealEnclosure.

• graph : NN.IR.Graph

  The exact graph whose ranges and kernel plan were reconstructed by the checker.

• raw : GraphNumericalCertificate

  The untrusted artifact supplied to the checker, retained for inspection and serialization.

• sources : Array CheckedSourceRange

  Source assumptions whose interval endpoints have been proved finite and ordered.

• ranges : Array CheckedNodeRange

  The canonical node-by-node range trace reconstructed from the graph.

• backendPlan : NN.Backend.AcceptedGraphKernelPlan

  The kernel plan accepted when the checker replanned graph.

• rangesMatch : sameRangeTrace self.ranges self.raw.ranges = true

  Proof that the reconstructed trace matches every range row claimed by raw.

• auditMatch : self.backendPlan.audit = self.raw.audit

  Proof that the accepted plan's audit is the one stored in raw.

@[instance_reducible]

instance Proofs.RuntimeApprox.NumericalCertificate.instReprRegistryCheckedCertificate : Repr RegistryCheckedCertificate

structure Proofs.RuntimeApprox.NumericalCertificate.RangeCheckedExecution : Type

Result of executing the canonical IR with bit-level binary32 semantics and checking every intermediate value against a registry-replayed range trace.

• certificate : RegistryCheckedCertificate

  The registry-checked certificate the replay was checked against.

• values : Array (Spec.SomeTensor (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) _proof_1 _proof_2 _proof_3 _proof_4))

  Bit-level binary32 node values. executeIEEE32 obtains these from graph replay; this structure does not itself carry a denotation equality for independently supplied values.

• withinRanges : executionWithinRanges self.certificate.ranges self.values = true

  Proof that every replayed value lies in its checked range row.

def Proofs.RuntimeApprox.NumericalCertificate.ofCheckedTrace (profile : NN.Backend.BackendProfile) (registry : GraphRangeRegistry) (sources : Array SourceRange) (ranges : Array CheckedNodeRange) (plan : NN.Backend.AcceptedGraphKernelPlan) : GraphNumericalCertificate

Convert an accepted kernel plan and checked range trace into raw certificate data.

def Proofs.RuntimeApprox.NumericalCertificate.acceptedPlan (profile : NN.Backend.BackendProfile) (graph : NN.IR.Graph) : Except String NN.Backend.AcceptedGraphKernelPlan

Obtain an accepted kernel plan or report the acceptance-gate failures.

def Proofs.RuntimeApprox.NumericalCertificate.generateWith (registry : GraphRangeRegistry) (profile : NN.Backend.BackendProfile) (graph : NN.IR.Graph) (sources : Array SourceRange) : Except String GraphNumericalCertificate

Generate a canonical certificate using an explicit numerical operation registry.

def Proofs.RuntimeApprox.NumericalCertificate.generate (profile : NN.Backend.BackendProfile) (graph : NN.IR.Graph) (sources : Array SourceRange) : Except String GraphNumericalCertificate

Generate a canonical certificate using TorchLean's built-in numerical contracts.

def Proofs.RuntimeApprox.NumericalCertificate.checkWith (registry : GraphRangeRegistry) (profile : NN.Backend.BackendProfile) (graph : NN.IR.Graph) (raw : GraphNumericalCertificate) : Except String RegistryCheckedCertificate

Check an untrusted certificate with an explicit numerical operation registry.

def Proofs.RuntimeApprox.NumericalCertificate.check (profile : NN.Backend.BackendProfile) (graph : NN.IR.Graph) (raw : GraphNumericalCertificate) : Except String RegistryCheckedCertificate

Check an untrusted certificate using TorchLean's built-in numerical contracts.

def Proofs.RuntimeApprox.NumericalCertificate.generateChecked (profile : NN.Backend.BackendProfile) (graph : NN.IR.Graph) (sources : Array SourceRange) : Except String RegistryCheckedCertificate

Generate and immediately check a certificate. This is convenient for in-process callers and ensures examples exercise exactly the same checker used for imported artifacts.

def Proofs.RuntimeApprox.NumericalCertificate.executeIEEE32 (payload : NN.IR.Payload (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) RangeCheckedExecution._proof_1 RangeCheckedExecution._proof_2 RangeCheckedExecution._proof_3 RangeCheckedExecution._proof_4)) (input : Spec.SomeTensor (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) RangeCheckedExecution._proof_1 RangeCheckedExecution._proof_2 RangeCheckedExecution._proof_3 RangeCheckedExecution._proof_4)) (certificate : RegistryCheckedCertificate) : Except String RangeCheckedExecution

Execute a graph under ExecFloat.Binary 8 23 and check all intermediate tensors against the certificate.

This reference replay path gives imported runtime artifacts a bit-level oracle. The backend audit records the capsules and numerical policies selected when the graph is replanned. The audit is not runtime provenance and does not prove that those kernels produced the imported values.

structure Proofs.RuntimeApprox.NumericalCertificate.ProvedRealEnclosure (certificate : RegistryCheckedCertificate) : Type

Exact-real execution evidence for the graph stored in a registry-checked certificate.

The numerical checker reconstructs interval transfers, while a semantic proof establishes that the real graph trace lies in those intervals. Keeping this proof separate prevents successful endpoint replay from being mistaken for a theorem about an unsupported real operation.

• payload : NN.IR.Payload ℝ

  Real-valued constants and external tensors used by the graph execution.

• input : Spec.SomeTensor ℝ

  Real-valued graph input.

• values : Array (Spec.SomeTensor ℝ)

  Complete real-valued node trace, in graph order.

• denotation : certificate.graph.denoteAll self.payload self.input = Except.ok self.values

  Evidence that values is exactly the graph's denotational execution trace.

• enclosed : ArraysRelated SomeTensorEnclosed certificate.ranges self.values

  Pointwise evidence that every real node value lies in its checked interval.

theorem Proofs.RuntimeApprox.NumericalCertificate.RangeCheckedExecution.error_trace (execution : RangeCheckedExecution) (exact : ProvedRealEnclosure execution.certificate) : ExecutionErrorTrace execution.certificate.ranges exact.values execution.values

Pair range-checked binary32 values with a proved real enclosure trace to obtain a graph-wide, pointwise error trace. Each node's error budget is its interval width. The bound follows from shared enclosure; it does not require or establish native execution provenance.