Numerical certificate contracts

Canonical local range rules, numerical operation contracts, contract registries, and graph range trace construction. Most users should import NN.Proofs.RuntimeApprox.Graph.NumericalCertificate.

Canonical local transfer rules

inductive Proofs.RuntimeApprox.NumericalCertificate.RangeRule : Type

How a node enclosure was obtained from source assumptions or earlier nodes.

The rule is recorded to make certificate diagnostics useful. It is not accepted on faith: check reconstructs the rule and endpoints from the graph.

• source : RangeRule
• preserve (parent : ℕ) : RangeRule
• add (left right : ℕ) : RangeRule
• sub (left right : ℕ) : RangeRule
• mul (left right : ℕ) : RangeRule
• inv (parent : ℕ) : RangeRule
• hull (parents : Array ℕ) : RangeRule
• hullZero (parent : ℕ) : RangeRule
• sumLeft (parent count : ℕ) : RangeRule
• meanLeft (parent count : ℕ) : RangeRule
• matmulLeft (left right innerDim : ℕ) : RangeRule
• averageWindowLeft (parent windowSize : ℕ) (includesPadding : Bool) : RangeRule
• mseLeft (prediction target count : ℕ) : RangeRule
• layerNormLeft (parent axis normalizedSize : ℕ) : RangeRule
• softmaxUnit (parent axis : ℕ) : RangeRule
• relu (parent : ℕ) : RangeRule
• abs (parent : ℕ) : RangeRule
• sqrtNonnegative (parent : ℕ) : RangeRule
• unitBound (parent : ℕ) : RangeRule
• signedUnitBound (parent : ℕ) : RangeRule

@[instance_reducible]

instance Proofs.RuntimeApprox.NumericalCertificate.instDecidableEqRangeRule : DecidableEq RangeRule

def Proofs.RuntimeApprox.NumericalCertificate.instDecidableEqRangeRule.decEq (x✝ x✝¹ : RangeRule) : Decidable (x✝ = x✝¹)

def Proofs.RuntimeApprox.NumericalCertificate.instReprRangeRule.repr : RangeRule → ℕ → Std.Format

@[instance_reducible]

instance Proofs.RuntimeApprox.NumericalCertificate.instReprRangeRule : Repr RangeRule

structure Proofs.RuntimeApprox.NumericalCertificate.NodeRange : Type

Proof-free data for one graph node's numerical range.

• nodeId : ℕ
• outShape : Spec.Shape
• rule : RangeRule
• enclosure : TorchLean.Floats.IEEE754.IEEE32Exec.Interval32

@[instance_reducible]

instance Proofs.RuntimeApprox.NumericalCertificate.instReprNodeRange : Repr NodeRange

def Proofs.RuntimeApprox.NumericalCertificate.instReprNodeRange.repr : NodeRange → ℕ → Std.Format

structure Proofs.RuntimeApprox.NumericalCertificate.CheckedNodeRangeextends Proofs.RuntimeApprox.NumericalCertificate.NodeRange : Type

A node range whose executable interval has passed the finite/order check.

• nodeId : ℕ
• outShape : Spec.Shape
• rule : RangeRule
• enclosure : TorchLean.Floats.IEEE754.IEEE32Exec.Interval32
• valid : self.enclosure.Valid

@[instance_reducible]

instance Proofs.RuntimeApprox.NumericalCertificate.instReprCheckedNodeRange : Repr CheckedNodeRange

def Proofs.RuntimeApprox.NumericalCertificate.dvalWithinRange (range : CheckedNodeRange) (value : Spec.SomeTensor (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) dvalWithinRange._proof_1 dvalWithinRange._proof_2 dvalWithinRange._proof_3 dvalWithinRange._proof_4)) : Bool

Check a dynamic graph value against the declared shape and interval of one certificate row.

def Proofs.RuntimeApprox.NumericalCertificate.SomeTensorEnclosed (range : CheckedNodeRange) (value : Spec.SomeTensor ℝ) : Prop

A real dynamic graph value has the shape declared by a certificate row and is enclosed by its interval. The equality witness makes the dependent tensor cast explicit.

def Proofs.RuntimeApprox.NumericalCertificate.SomeTensorErrorLe (range : CheckedNodeRange) (exact : Spec.SomeTensor ℝ) (computed : Spec.SomeTensor (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) dvalWithinRange._proof_1 dvalWithinRange._proof_2 dvalWithinRange._proof_3 dvalWithinRange._proof_4)) : Prop

Pointwise approximation relation for real and IEEE dynamic graph values at one certificate row.

theorem Proofs.RuntimeApprox.NumericalCertificate.dval_error_le_of_range_check {range : CheckedNodeRange} {exact : Spec.SomeTensor ℝ} {computed : Spec.SomeTensor (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) dvalWithinRange._proof_1 dvalWithinRange._proof_2 dvalWithinRange._proof_3 dvalWithinRange._proof_4)} (hexact : SomeTensorEnclosed range exact) (hcomputed : dvalWithinRange range computed = true) : SomeTensorErrorLe range exact computed

One successful dynamic replay row yields a pointwise error bound whenever the corresponding real graph value has the proved enclosure.

def Proofs.RuntimeApprox.NumericalCertificate.executionWithinRanges (ranges : Array CheckedNodeRange) (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) dvalWithinRange._proof_1 dvalWithinRange._proof_2 dvalWithinRange._proof_3 dvalWithinRange._proof_4))) : Bool

Check every value produced by IR.Graph.denoteAll against the corresponding certificate row.

def Proofs.RuntimeApprox.NumericalCertificate.ArraysRelated {α β : Type} (relation : α → β → Prop) (xs : Array α) (ys : Array β) : Prop

Pointwise relation between two equally sized runtime arrays.

theorem Proofs.RuntimeApprox.NumericalCertificate.executionWithinRanges_eq_true_iff (ranges : Array CheckedNodeRange) (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) dvalWithinRange._proof_1 dvalWithinRange._proof_2 dvalWithinRange._proof_3 dvalWithinRange._proof_4))) : executionWithinRanges ranges values = true ↔ ArraysRelated (fun (range : CheckedNodeRange) (value : Spec.SomeTensor (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) dvalWithinRange._proof_1 dvalWithinRange._proof_2 dvalWithinRange._proof_3 dvalWithinRange._proof_4)) => dvalWithinRange range value = true) ranges values

A successful replay check is exactly a size match plus a successful check at every node.

def Proofs.RuntimeApprox.NumericalCertificate.ExecutionErrorTrace (ranges : Array CheckedNodeRange) (exact : Array (Spec.SomeTensor ℝ)) (computed : 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) dvalWithinRange._proof_1 dvalWithinRange._proof_2 dvalWithinRange._proof_3 dvalWithinRange._proof_4))) : Prop

Graph-wide pointwise approximation evidence, one row per intermediate value.

theorem Proofs.RuntimeApprox.NumericalCertificate.execution_error_trace_of_check {ranges : Array CheckedNodeRange} {exact : Array (Spec.SomeTensor ℝ)} {computed : 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) dvalWithinRange._proof_1 dvalWithinRange._proof_2 dvalWithinRange._proof_3 dvalWithinRange._proof_4))} (hexact : ArraysRelated SomeTensorEnclosed ranges exact) (hcomputed : executionWithinRanges ranges computed = true) : ExecutionErrorTrace ranges exact computed

Compose real enclosure proofs and successful IEEE replay checks into an error trace.

def Proofs.RuntimeApprox.NumericalCertificate.sameNodeRange (checked : CheckedNodeRange) (raw : NodeRange) : Bool

Compare a checked canonical row with untrusted raw certificate data.

def Proofs.RuntimeApprox.NumericalCertificate.parentRange (ranges : Array CheckedNodeRange) (nodeId : ℕ) : Except String TorchLean.Floats.IEEE754.IEEE32Exec.Interval32

Read a previously checked parent enclosure. Graph well-formedness guarantees that successful lookups refer only to earlier rows; the explicit error still protects this API when called alone.

def Proofs.RuntimeApprox.NumericalCertificate.parentNodeRange (ranges : Array CheckedNodeRange) (nodeId : ℕ) : Except String CheckedNodeRange

Read the complete checked row for a parent node.

def Proofs.RuntimeApprox.NumericalCertificate.sumLeftRange (count : ℕ) (range : TorchLean.Floats.IEEE754.IEEE32Exec.Interval32) : TorchLean.Floats.IEEE754.IEEE32Exec.Interval32

Outward-rounded left-fold range for a sum of count values from one enclosure. The initial point interval at positive zero matches Tensor.sumSpec.

def Proofs.RuntimeApprox.NumericalCertificate.meanLeftRange (count : ℕ) (range : TorchLean.Floats.IEEE754.IEEE32Exec.Interval32) : TorchLean.Floats.IEEE754.IEEE32Exec.Interval32

Left-fold mean range, using the same binary32 conversion of the divisor as the tensor context.

def Proofs.RuntimeApprox.NumericalCertificate.nodeNumericalPolicy (plan : NN.Backend.AcceptedGraphKernelPlan) (nodeId : ℕ) : Option NN.Backend.NumericalPolicy

Numerical policy selected for a runtime-relevant graph node.

def Proofs.RuntimeApprox.NumericalCertificate.requireFixedLeftReduction (plan : NN.Backend.AcceptedGraphKernelPlan) (node : NN.IR.Node) : Except String Unit

Reductions are propagated only when the selected capsule promises the same fixed left fold as the canonical tensor semantics. Other schedules need the order-independent reduction bound from NN.Proofs.RuntimeApprox.Reductions.IEEE32 and are rejected here rather than mislabeled as deterministic.

def Proofs.RuntimeApprox.NumericalCertificate.matmulInnerDim (left right : Spec.Shape) : Except String ℕ

Inner accumulation length for the rank-2 and batched rank-3 matrix products implemented by IR.Graph.denoteAll. The graph shape checker has already validated matching dimensions; retaining the checks here gives callers of deriveNodeRange a precise error instead of relying on that ambient invariant.

def Proofs.RuntimeApprox.NumericalCertificate.hullParents (ranges : Array CheckedNodeRange) (parents : Array ℕ) : Except String TorchLean.Floats.IEEE754.IEEE32Exec.Interval32

Hull of a nonempty array of parent ranges.

Graph range contracts

Architectures do not participate in range propagation directly. They lower to NN.IR.Graph, and each graph node is handled by a reusable operation contract. This keeps MLPs, convolutional networks, transformers, and future model families on one checker path: adding a model requires no new certificate traversal, while adding a genuinely new primitive requires one local contract.

The registry is an explicit value rather than global mutable state. Certificate generation and checking therefore use the same inspectable rule set, and downstream projects may extend it without changing TorchLean's graph walker.

inductive Proofs.RuntimeApprox.NumericalCertificate.NumericalOpKey : Type

Stable key for a numerical range contract.

Input-like nodes share the source contract, detach uses the structural identity contract, and runtime operations use the same BackendOp vocabulary as kernel capsules and execution plans.

• source : NumericalOpKey
• structural : NumericalOpKey
• wholeSum : NumericalOpKey
• maxPool : NumericalOpKey
• maxPoolPad : NumericalOpKey
• averagePool : NumericalOpKey
• averagePoolPad : NumericalOpKey
• backend (op : NN.Backend.BackendOp) : NumericalOpKey
• unclassified : NumericalOpKey

@[instance_reducible]

instance Proofs.RuntimeApprox.NumericalCertificate.instDecidableEqNumericalOpKey : DecidableEq NumericalOpKey

def Proofs.RuntimeApprox.NumericalCertificate.instDecidableEqNumericalOpKey.decEq (x✝ x✝¹ : NumericalOpKey) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Proofs.RuntimeApprox.NumericalCertificate.instReprNumericalOpKey : Repr NumericalOpKey

def Proofs.RuntimeApprox.NumericalCertificate.instReprNumericalOpKey.repr : NumericalOpKey → ℕ → Std.Format

def Proofs.RuntimeApprox.NumericalCertificate.numericalOpKey : NN.IR.OpKind → NumericalOpKey

Classify an IR operation for numerical-contract lookup.

structure Proofs.RuntimeApprox.NumericalCertificate.NumericalRangeContext : Type

Read-only state supplied to one local range transfer.

• sources : Array CheckedSourceRange
• plan : NN.Backend.AcceptedGraphKernelPlan
• ranges : Array CheckedNodeRange

@[reducible, inline]

abbrev Proofs.RuntimeApprox.NumericalCertificate.RangeTransferResult : Type

Result computed by one numerical operation contract.

structure Proofs.RuntimeApprox.NumericalCertificate.GraphRangeContract : Type

Executable range transfer for one operation family.

The proof-facing meaning of the resulting row remains SomeTensorEnclosed; local soundness lemmas for interval arithmetic and NF approximation are kept in their mathematical modules. The contract contains only executable dispatch and a stable key, so serializable certificates cannot inject proof evidence.

• key : NumericalOpKey
• name : String
• derive : NumericalRangeContext → NN.IR.Node → Except String RangeTransferResult

structure Proofs.RuntimeApprox.NumericalCertificate.GraphRangeRegistry : Type

Deterministic registry used by graph certificate generation and replay.

• name : String
• contracts : Array GraphRangeContract

def Proofs.RuntimeApprox.NumericalCertificate.GraphRangeRegistry.empty (name : String) : GraphRangeRegistry

Empty named registry for downstream composition.

def Proofs.RuntimeApprox.NumericalCertificate.GraphRangeRegistry.find? (registry : GraphRangeRegistry) (key : NumericalOpKey) : Option GraphRangeContract

Find the unique contract associated with a numerical operation key.

def Proofs.RuntimeApprox.NumericalCertificate.GraphRangeRegistry.register (registry : GraphRangeRegistry) (contract : GraphRangeContract) : Except String GraphRangeRegistry

Add one contract, rejecting duplicate keys so dispatch never depends on registration order.

def Proofs.RuntimeApprox.NumericalCertificate.GraphRangeRegistry.ofArray (name : String) (contracts : Array GraphRangeContract) : Except String GraphRangeRegistry

Build a registry while checking key uniqueness.

structure Proofs.RuntimeApprox.NumericalCertificate.MissingNumericalContract : Type

One graph node for which a numerical registry has no local transfer.

• nodeId : ℕ
• operation : String
• key : NumericalOpKey

@[instance_reducible]

instance Proofs.RuntimeApprox.NumericalCertificate.instReprMissingNumericalContract : Repr MissingNumericalContract

def Proofs.RuntimeApprox.NumericalCertificate.instReprMissingNumericalContract.repr : MissingNumericalContract → ℕ → Std.Format

structure Proofs.RuntimeApprox.NumericalCertificate.NumericalCoverageReport : Type

Architecture-independent coverage report obtained after lowering a model to NN.IR.Graph.

• registryName : String
• nodeCount : ℕ
• coveredCount : ℕ
• missing : Array MissingNumericalContract

@[instance_reducible]

instance Proofs.RuntimeApprox.NumericalCertificate.instReprNumericalCoverageReport : Repr NumericalCoverageReport

def Proofs.RuntimeApprox.NumericalCertificate.instReprNumericalCoverageReport.repr : NumericalCoverageReport → ℕ → Std.Format

def Proofs.RuntimeApprox.NumericalCertificate.numericalCoverage (registry : GraphRangeRegistry) (graph : NN.IR.Graph) : NumericalCoverageReport

Inspect contract coverage without attempting interval propagation.

def Proofs.RuntimeApprox.NumericalCertificate.requireNumericalCoverage (registry : GraphRangeRegistry) (graph : NN.IR.Graph) : Except String NumericalCoverageReport

Reject a graph before propagation when any primitive lacks a numerical contract.

def Proofs.RuntimeApprox.NumericalCertificate.arityError (contractName : String) (node : NN.IR.Node) (expected : String) : String

Standard diagnostic for a contract whose graph arity does not match its operation.

def Proofs.RuntimeApprox.NumericalCertificate.sourceContract : GraphRangeContract

Shared source-node contract. The source interval remains an explicit certificate assumption.

def Proofs.RuntimeApprox.NumericalCertificate.structuralContract : GraphRangeContract

Structural identity used by detach.

def Proofs.RuntimeApprox.NumericalCertificate.preserveContract (op : NN.Backend.BackendOp) : GraphRangeContract

Reusable contract constructor for value-preserving graph operations.

def Proofs.RuntimeApprox.NumericalCertificate.binaryContract (op : NN.Backend.BackendOp) (rule : ℕ → ℕ → RangeRule) (transfer : TorchLean.Floats.IEEE754.IEEE32Exec.Interval32 → TorchLean.Floats.IEEE754.IEEE32Exec.Interval32 → TorchLean.Floats.IEEE754.IEEE32Exec.Interval32) : GraphRangeContract

Reusable contract constructor for pointwise binary interval operations.

def Proofs.RuntimeApprox.NumericalCertificate.hullContract (op : NN.Backend.BackendOp) : GraphRangeContract

Reusable contract for operations whose output is enclosed by the hull of their parents.

def Proofs.RuntimeApprox.NumericalCertificate.maxPoolContract : GraphRangeContract

Max pooling without padding selects existing values and therefore preserves the input hull.

def Proofs.RuntimeApprox.NumericalCertificate.maxPoolPadContract : GraphRangeContract

Padded max pooling may additionally select the padding value zero.

def Proofs.RuntimeApprox.NumericalCertificate.averagePoolContract (padded : Bool) : GraphRangeContract

Shared average-pooling contract constructor.

def Proofs.RuntimeApprox.NumericalCertificate.inverseContract : GraphRangeContract

Reciprocal contract with an explicit nonzero-domain check.

def Proofs.RuntimeApprox.NumericalCertificate.sumContract : GraphRangeContract

Whole-tensor fixed-left sum contract.

def Proofs.RuntimeApprox.NumericalCertificate.axisReductionContract (mean : Bool) : GraphRangeContract

Axis reduction contract shared by sum and mean.

def Proofs.RuntimeApprox.NumericalCertificate.matmulContract : GraphRangeContract

Matrix multiplication contract using the selected fixed-left accumulation schedule.

def Proofs.RuntimeApprox.NumericalCertificate.mseContract : GraphRangeContract

Mean-squared-error contract with nonnegativity restored after dependent squaring.

def Proofs.RuntimeApprox.NumericalCertificate.layerNormContract : GraphRangeContract

Pure LayerNorm contract over an arbitrary normalized suffix.

def Proofs.RuntimeApprox.NumericalCertificate.softmaxContract : GraphRangeContract

Softmax contract: exact-real outputs lie in the unit interval on every nonempty axis.

def Proofs.RuntimeApprox.NumericalCertificate.reluContract : GraphRangeContract

ReLU interval contract.

def Proofs.RuntimeApprox.NumericalCertificate.absContract : GraphRangeContract

Absolute-value interval contract.

def Proofs.RuntimeApprox.NumericalCertificate.sqrtContract : GraphRangeContract

Square-root contract with a checked nonnegative domain.

def Proofs.RuntimeApprox.NumericalCertificate.boundedUnaryContract (op : NN.Backend.BackendOp) (rule : ℕ → RangeRule) (enclosure : TorchLean.Floats.IEEE754.IEEE32Exec.Interval32) : GraphRangeContract

Constructor for bounded transcendental contracts.

def Proofs.RuntimeApprox.NumericalCertificate.defaultContracts : Array GraphRangeContract

Built-in numerical contracts. Grouping is by operation semantics, never by architecture.

def Proofs.RuntimeApprox.NumericalCertificate.defaultRegistry : Except String GraphRangeRegistry

TorchLean's built-in numerical registry. Construction is checked once at use sites so a future duplicate produces an explicit configuration failure.

def Proofs.RuntimeApprox.NumericalCertificate.deriveNodeRangeWith (registry : GraphRangeRegistry) (sources : Array CheckedSourceRange) (plan : NN.Backend.AcceptedGraphKernelPlan) (ranges : Array CheckedNodeRange) (node : NN.IR.Node) : Except String RangeTransferResult

Compute one node range using an explicit numerical contract registry.

def Proofs.RuntimeApprox.NumericalCertificate.deriveNodeRange (sources : Array CheckedSourceRange) (plan : NN.Backend.AcceptedGraphKernelPlan) (ranges : Array CheckedNodeRange) (node : NN.IR.Node) : Except String RangeTransferResult

Compute one node range using TorchLean's built-in registry.

def Proofs.RuntimeApprox.NumericalCertificate.buildRangeTraceWith (registry : GraphRangeRegistry) (graph : NN.IR.Graph) (sources : Array CheckedSourceRange) (plan : NN.Backend.AcceptedGraphKernelPlan) : Except String (Array CheckedNodeRange)

Construct and validate the canonical range trace using an explicit contract registry.

def Proofs.RuntimeApprox.NumericalCertificate.buildRangeTrace (graph : NN.IR.Graph) (sources : Array CheckedSourceRange) (plan : NN.Backend.AcceptedGraphKernelPlan) : Except String (Array CheckedNodeRange)

Construct and validate the canonical range trace using TorchLean's built-in contracts.

def Proofs.RuntimeApprox.NumericalCertificate.eraseRangeTrace (ranges : Array CheckedNodeRange) : Array NodeRange

Erase validity proofs from a checked trace.

def Proofs.RuntimeApprox.NumericalCertificate.sameRangeTrace (checked : Array CheckedNodeRange) (raw : Array NodeRange) : Bool

Compare a canonical checked trace with untrusted raw rows.