Real And Floating-Point Semantics🔗

A real-valued proof does not account for the arithmetic used to evaluate its formulas. Rounding, cancellation, overflow, reduction order, fused kernels, and domain guards can affect an execution; Goldberg (1991) explains these effects in floating-point arithmetic. A softmax implementation, for example, combines max-subtraction, exponent approximations, a finite sum, and division. Its error depends on how those operations are carried out and how their errors interact.

To transfer a real-arithmetic guarantee to execution, we need to:

1. prove the claim over the reals or over the spec;

2. prove an approximation relation between runtime tensors and spec tensors;

3. inflate margins, enclosures, or certificates by the approximation budget;

4. leave native hardware assumptions explicit when they are outside Lean.

This matches standard numerical analysis practice; see Higham's Accuracy and Stability of Numerical Algorithms (https://epubs.siam.org/doi/book/10.1137/1.9780898718027) for the classical background. It also matches the caution needed in neural network verification, where a tiny rounding gap can matter if the verified margin is tiny.

There are two sources of discrepancy to follow through this process. A stored weight may already differ from the intended real weight before evaluation starts. Even when every input agrees exactly, arithmetic can introduce new error at each node. A useful local theorem accepts the first kind of error as an input and adds the second kind to its conclusion. This is why a graph bound needs both initial approximation evidence and rules for the operations; proving that the initial tensors are close would leave the rounding inside the graph unaccounted for.

The Core Relation: Spec Tensors And Tolerances🔗

The small vocabulary is defined by runtime approximation core, spec approximation, and tolerances.

The spec approximation layer defines the basic tensor relation. Given a conversion toSpec : α → SpecScalar, a runtime tensor approximates a spec tensor when every component is close after conversion to the spec scalar. The key names are:

• tensorToSpec: pointwise conversion from runtime tensor values to spec scalars.

• linfNorm: max style tensor norm used for error statements.

• approxWith: absolute tensor approximation using an explicit error tensor.

• approxWithTol: approximation using a tolerance object.

• approxTensorWithTol: packaged tensor tolerance relation.

• Witness: a small record for carrying a runtime value and its error evidence.

The tolerance API defines ApproxTol, with absolute, relative, and slack components. ApproxTol.absOnly, approxBound, and approxR let later proofs move between simple absolute error statements and more scale aware claims.

For a single scalar, the scale-aware shape is:

|r-s| \le \varepsilon_{\mathrm{slack}}\bigl(\varepsilon_{\mathrm{abs}} +\varepsilon_{\mathrm{rel}}\max(|r|,|s|)\bigr).

The choice is practical. An absolute tolerance of 1e-6 may be meaningful near zero and irrelevant near 1e9. A relative tolerance captures "small compared with the scale of the value." TorchLean uses both styles, but it makes the choice explicit instead of burying it in test thresholds.

Since approxBound is a real function, the difference between the two readings can simply be computed. Read 1e-6 as an absolute budget and it stays 1e-6 no matter how large the values are:

Read the same 1e-6 as a relative budget at the same scale and it is a thousand:

The relative budget grows with the operands: at this scale it permits an absolute difference of one thousand. The absolute budget remains one millionth. Both use the literal 1e-6, so a claim must identify which tolerance field it supplies.

Near a zero reference value, a purely relative comparison deserves particular care. With zero absolute tolerance and slack one, comparing a nonzero value to zero would require its magnitude to be at most rel times that same magnitude. For a relative tolerance below one, this cannot hold. The absolute component supplies room for small discrepancies near zero, while the relative component scales the allowance for large values. These are different jobs, so an application should choose them from the claim it needs rather than treat the two fields as interchangeable.

@tensorToSpec : {α : Type} →
  [inst : TorchLean.Storage α] → {s : Spec.Shape} → (α → Spec.SpecScalar) → TorchLean.Tensor α s → Spec.SpecTensor s

@approxTensorWithTol : {α : Type} →
  [inst : TorchLean.Storage α] →
    {s : Spec.Shape} → (α → Spec.SpecScalar) → Spec.SpecTensor s → TorchLean.Tensor α s → ApproxTol → Prop

approxBound : ApproxTol → ℝ → ℝ → ℝ

Forward Graph Approximation🔗

The forward graph theorem is in NN.Proofs.RuntimeApprox.Graph.ForwardApprox API. It mirrors the structure of the autograd tape proof, but the invariant is approximation rather than derivative soundness.

The main objects are:

• EList: list of scalar error budgets indexed by shape.

• approxCtx: approximation relation for a whole context.

• FwdNode: a node with spec forward, runtime forward, bound, and local soundness.

• FwdGraph: a snoc list graph of forward nodes that carry approximation evidence.

• FwdGraph.eval_approx: theorem for the whole forward graph.

The local theorem on a FwdNode says: if each runtime input approximates the corresponding spec input, then the runtime output approximates the spec output within this node's bound.

FwdGraph.eval_approx composes those local statements. When a graph appends a node, the proof uses the node's local sound theorem, appends the new bound to the error context, and continues. It uses the same architecture as the autograd soundness theorem: local correctness first, then a global induction over the graph.

A tiny example is multiplication. The spec value is the real product, while the runtime value is the rounded product computed by the chosen scalar model.

If x_{\mathrm{run}} is within \varepsilon_x of x_{\mathrm{real}}, and y_{\mathrm{run}} is within \varepsilon_y of y_{\mathrm{real}}, the local multiplication lemma supplies a bound for z_{\mathrm{run}} versus z_{\mathrm{real}}. The graph theorem then lets that new bound feed the next node.

Write the interpreted runtime inputs as x+dx and y+dy,

(x+dx)(y+dy)-xy=x\,dy+y\,dx+dx\,dy.

The first two terms describe how each input error is scaled by the other exact operand. The third accounts for the interaction of the two errors. The identity can be checked directly:

Hence input uncertainty alone contributes at most

|x|\,\varepsilon_y+|y|\,\varepsilon_x +\varepsilon_x\varepsilon_y.

The triangle inequality bounds the sum by the sum of the three magnitudes. Applying |ab|=|a||b| and the two input-error bounds gives the estimate:

If x=2, y=3, \varepsilon_x=0.01, and \varepsilon_y=0.02, that bound is a number:

The local rule then adds the rounding error of the multiplication itself. The number is not meant as a universal tolerance; it shows why the graph carries operand scale and incoming error rather than attaching one unexplained epsilon to every multiplication.

The product term in the multiplication estimate makes it a finite-perturbation bound rather than only a first-order sensitivity calculation. Dropping that term would be justified for a derivative limit, but would understate this particular finite error budget. The graph carries these bounds for all available values, not just the newest output. If a later node reuses an earlier activation, its local theorem retrieves the bound attached to that activation. The context invariant therefore follows the same data dependencies as the computation, including values that bypass several intervening nodes.

Backward Graph Approximation🔗

Backward approximation is developed in the backward approximation API. This file is the runtime approximation analogue of reverse mode AD.

The key objects are:

• RevNode: a forward node plus spec/runtime VJP functions and a VJP error transformer.

• RevGraph: reverse graph with local approximation evidence.

• RevGraph.eval_approx: forward approximation inherited from the forward graph.

• RevGraph.backprop_approx: theorem for reverse accumulation across the whole graph.

The theorem RevGraph.backprop_approx states that the runtime reverse pass approximates the spec reverse pass, provided the input context, forward tape, and seed cotangents are appropriately related. Addition during gradient accumulation is not treated as automatic; the theorem takes an explicit addBound and addSound describing how accumulation affects error.

Backward passes are often dominated by sums: cotangents from fanout, reductions, convolution gradients, and parameter gradient accumulation. Floating point addition is not associative, and accumulation order matters. By making addition soundness an explicit parameter, the theorem states the arithmetic model being used.

For a shared parameter, two individually accurate incoming cotangents still need an accurate addition before their sum becomes its gradient. Their existing errors add, and the rounded addition introduces another contribution. Forward-tape error also enters the local VJP: a multiplication backward rule uses a saved operand, whose rounded value may already differ from the real one. The seed has its own budget because changing the seed changes the linear functional being differentiated. These three sources explain why the backward theorem asks for more than approximation of the final forward output.

Autograd Algebra Correspondence🔗

The bridge file NN.Proofs.RuntimeApprox.Graph.LinkAutogradAlgebra API connects the runtime approximation graph shape back to the autograd algebra graph.

This bridge is structural. The runtime approximation layer uses the same shape-indexed tensor-context idea that the typed API exposes as TensorPack, so the conversion is not a semantic reinterpretation. The file defines toNodeData and toGraphData, then proves:

• evalRuntime_of_toGraphData;

• backpropRuntime_of_toGraphData.

In words, the runtime approximation graph can be viewed as an autograd algebra graph by forgetting the approximation evidence and keeping the same forward/VJP structure. That means the two layers compose cleanly:

autograd algebra: the reverse pass is the correct ideal VJP; runtime approximation: the executable reverse pass stays close to that ideal VJP.

To compose these results, the spec reverse pass must be the one identified with the derivative by the autograd proof. Approximation of an arbitrary supplied VJP would establish numerical agreement without establishing derivative correctness.

The erasure equalities are useful when connecting those premises. They let a proof about a RevGraph refer to the forward and backward functions executed by its erased GraphData, without reproving the traversal. They preserve the supplied scalar functions as well as the graph structure. An application can therefore combine a local derivative certificate and a local rounding certificate for the same rule. If the two certificates concern different guards, parameter orders, or selected slopes, the erasure equality cannot make those rules coincide.

Numerical Traces For The Canonical IR🔗

The proof-relevant FwdGraph and RevGraph explain how local approximation theorems compose. Model export and kernel selection, however, use the canonical op-tagged NN.IR.Graph. TorchLean connects that graph directly to executable binary32 through the graph numerical certificate checker. It does not introduce a second deployment graph or a second interval type.

A certificate contains source enclosures, one derived range per IR node, the name of the range registry, and the existing backend execution audit. A successful check stores the graph inside RegistryCheckedCertificate; later replay cannot silently substitute a different graph or rule set. Checking performs three independent executable validations:

1. validate that source and derived endpoints are finite and ordered;

2. reconstruct every supported range transfer from the graph;

3. re-run kernel selection and compare the selected capsules and numerical policies.

GraphRangeRegistry dispatches by primitive operation, not model family. The built-in transfers cover source and shape-only nodes, pooling, arithmetic, inverse, ReLU, absolute value, directed square root with a checked nonnegative domain, fixed-left reductions, matrix multiplication, MSE, LayerNorm, softmax, sigmoid, tanh, sine, and cosine. Exponential is currently unsupported. An unsupported operation fails at its node id; it is not replaced by an uninformative whole interval.

generateChecked : NN.Backend.BackendProfile → NN.IR.Graph → Array SourceRange → Except String RegistryCheckedCertificate

ProvedRealEnclosure : RegistryCheckedCertificate → Type

The generator's Except result preserves a diagnostic on failure, such as a node id whose operation has no registered rule. That message helps locate unsupported operations; it provides no semantic evidence about the supported ones.

ProvedRealEnclosure is indexed by RegistryCheckedCertificate, so its evidence refers to the same artifact used by replay. This prevents accidental substitution of evidence for another certificate. The fields still have to prove the required real-semantic facts.

The other checked names describe the stages between these two types. numericalCoverage reports whether each operation has a registry entry; it can locate a missing transfer before range propagation begins. A registered transfer can still reject the actual domain it receives. executeIEEE32 then needs concrete payloads and inputs to produce a checked execution. tensor_error_le_width_of_check supplies the coordinatewise interval-width argument, and execution_error_trace_of_check applies that argument to related arrays of node values. RangeCheckedExecution.error_trace packages it for the certificate's real enclosure and replay. Thus operation coverage, successful evaluation, and a proved error trace answer successive, different questions.

GraphRangeContract.derive is an executable range transformer, not a soundness theorem. generateChecked and check establish that the stored trace is exactly the trace reconstructed by the selected registry and kernel plan; they do not establish that every reconstructed interval encloses the graph's real denotation.

executeIEEE32 evaluates the same NN.IR.Graph with FloatLib's configured binary32 through the FloatLib binary32 context and checks every intermediate value against the stored ranges, rejecting NaN and infinity. This is a reference replay, not an agreement theorem for a high-throughput backend. ProvedRealEnclosure carries the separate semantic evidence: its fields require both the real denotation equality and a pointwise real enclosure proof. When that evidence is supplied, RangeCheckedExecution.error_trace combines the real enclosure with the successful IEEE replay to prove a pointwise error trace whose bound is the interval width. For each coordinate, both the real value and the interpreted IEEE value lie between the same two endpoints; their distance is therefore at most the upper endpoint minus the lower endpoint. This argument requires enclosure of both values. Checking the rounded replay alone leaves the real half of the argument unproved.

Reduction order is read from the selected capsule. The portable reference capsules advertise the fixed left fold used by the canonical tensor semantics. Native CUDA and LibTorch accumulations are marked implementation-defined, so a fixed-left certificate cannot accidentally certify a cuBLAS, cuDNN, fused-attention, or parallel-reduction schedule. Those paths require the order-independent reduction bounds described in the floating-point chapter or a stronger backend-specific contract.

The local interval lemmas for arithmetic and selected nonlinear operations follow the inclusion principle of IEEE 1788-2015. The current registry does not yet compose those lemmas into a theorem that every accepted graph trace encloses exact graph semantics. The separation between local rounding facts and a composed global error follows the standard treatment in Higham, Accuracy and Stability of Numerical Algorithms, 2nd edition.

The canonical NN.IR.Graph lowering currently proves forward semantic preservation only. Its IR nodes do not yet carry proved VJPs, so this certificate should not be described as a canonical-IR backward certificate. Backward numerical theorems use the proof-bearing RevGraph path below, which erases to executable autograd GraphData without discarding its VJP rules. An autograd-capable lowering from canonical IR would need an additional correspondence theorem.

An interval-width bound is deliberately coarse when the two executions share information that the interval forgets. If both values lie in [2,3], their distance is at most one, even when they are actually identical. Narrowing the interval improves this estimate only if both enclosure premises remain valid. This gives the range producer a concrete objective: keep intervals tight enough for the downstream margin while preserving the real inclusion proof and successful rounded replay. Merely shrinking a stored endpoint would invalidate one of those checks.

MLP Numerical Certificate Example🔗

The executable example GraphNumericalCertificate.lean ends with a two-layer MLP rather than a single isolated operator. Run it from the repository root:

# Run generation and replay for the primitive-composed MLP
# certificate.
lake exe torchlean numerical_certificate

The model is a matrix pipeline with shapes that remain visible in the IR:

-- Each matrix and bias stage contributes its own node
-- range.
input [1,2]
  -> matmul [2,3]
  -> add bias [1,3]
  -> ReLU
  -> matmul [3,1]
  -> add bias [1,1]

The report captured before the FloatLib migration shows generation, replay, and one deliberately corrupted artifact. It is a record of that run, not a validation of the migrated executable:

TorchLean numerical runtime certificate
  ok  base certificate
  ok  base IEEE replay
  ok  tampered range rejected
  ok  two-layer MLP certificate
  ok  two-layer MLP IEEE replay
All numerical certificate checks passed.

The tampered-range check replaces the addition interval with [0,0]. The checker regenerates the range trace and rejects the mismatch. This establishes that this corrupted artifact is refused; it does not establish soundness of every registered transfer.

mlpCertificate checks that all ten graph nodes have a registered numerical rule. It derives every range, selects the CPU capsules, and stores the graph, registry identity, source assumptions, ranges, and backend audit in one artifact. mlpReplay then supplies concrete weights, biases, and input values, executes the stored graph with FloatLib binary32, and checks every intermediate tensor. The same file demonstrates rejection of a tampered range. These Boolean and Except checks are useful regression evidence; the example does not construct a ProvedRealEnclosure, so it is not by itself a proof that the MLP's exact real execution is enclosed.

There is no MLP-specific branch in this process. The checker sees input, constant, matrix multiplication, addition, and ReLU nodes. Other architectures can use the same walk when their primitive operations are covered. New primitives extend the executable registry with a GraphRangeContract; a semantic certificate additionally needs a theorem connecting that contract's derived interval to the operation's real semantics.

The complete numerical-runtime walkthrough shows the model definitions, the five replay stages, the backend-capsule audit, and the handoff to backward and optimizer bounds. It also states the current lowering boundary explicitly: canonical IR has checked forward replay, while backward and optimizer composition currently begins from a proof-bearing RevGraph.

Read the five successful lines as checks of two concrete artifacts and one rejection case. The base and MLP generation lines concern reconstruction of their ranges and execution plans; their replay lines concern the supplied values at every intermediate node. The tampering line confirms that changing a stored range is detected. These observations exercise different parts of the checker, which is why the example keeps them separate. None of the lines supplies the real denotation and enclosure fields required by the proof-bearing record above.

NF Operations: Rounded Real Arithmetic🔗

The largest collection of local rules is NN.Proofs.RuntimeApprox.NF.Ops API. These rules use FloatLib's Floats.Formats.Flocq.NF, a noncomputable rounded-real model. Its radix, exponent function, and valid rounder determine the representable values and arithmetic. This is the rounded-real style used by Boldo and Melquiond (2011) in Rocq. Expressing an operation as rounding a real result makes its error available directly to real analysis. A bit-level model can support such reasoning, but first needs decoding and a theorem relating the decoded operation to rounding.

The local tensor, graph, and optimizer rules compose those imported scalar facts. Selecting ExecFloat.Binary e f for a program does not instantiate an NF error theorem automatically: the proof must connect the chosen bit format to the same rounding model and account for finite range and exceptional values. Likewise, an NF exponential denotes rounding the real exponential; it is not a theorem about the accuracy of a configured software approximation to that function.

The file includes scalar and tensor approximation lemmas for common operations:

• arithmetic: approx_add_nf, approx_sub_nf, approx_mul_nf, approx_div_nf_of_pos_lb;

• unary functions: approx_exp_nf, approx_tanh_nf, approx_abs_nf, approx_neg_nf;

• guarded operations: safeLog, safeDiv, safe_log;

• tensor rules: approxTensor_add_spec, approxTensor_mul_spec, approxTensor_exp_spec, approxTensor_relu_spec;

• graph nodes: addNode, mulNode, expNode, reluNode, safeDivNode, softmaxNode, sumNode.

Several of these lemmas make the numerical analysis tradeoff visible. Division requires a positive lower bound on the exact denominator that survives rounding (approx_div_nf_of_pos_lb) or a guarded form (safeDiv). The division budget has a name, divPosErrorBound: the numerator error scaled by the effective margin, the denominator error scaled by the squared margin, and half an ULP of the quotient. The sigmoid, logistic, and mean bounds are built on that one definition. reciprocal_sigmoid_bound_scalar_le_one bounds the budget for the rounded sequence 1/(1+\exp(-x)) by one under explicit small-error hypotheses. mean_row_bound_of_exact gives the closed form of the row-mean budget when the row count is exactly representable.

The public sigmoid uses 1/(1+\exp(-x)) on positive inputs and \exp(x)/(1+\exp(x)) otherwise. Both formulas describe the same real function, but their rounded arithmetic differs: the second sequence also rounds the numerator exponential. approx_sigmoid_nf uses the budget for the branch selected by the rounded input. Its proof allows the real input and rounded input to lie on different sides of zero, because each branch approximates the same real sigmoid.

Square root and log need domain protection. Exponential uses a mean value bound. Multiplication propagates both input errors and a product term. These are the exact places where a proof over real numbers would be too optimistic if copied directly onto a float implementation.

@divPosErrorBound : {β : Radix} → {fexp : ℤ → ℤ} → [ValidExp fexp] → ℝ → ℝ → ℝ → ℝ → ℝ → ℝ

The displayed divPosErrorBound signature makes the budget's dependencies explicit.

The five real arguments are the exact denominator lower bound η, the input-error budgets epsx and epsy, and the interpreted runtime operands xhat and yhat. The associated theorem requires epsy < η: denominator error leaves an effective separation η - epsy from zero. The budget scales the numerator error by the reciprocal of that separation and the denominator error by its squared reciprocal, then adds rounding of the quotient.

As the surviving separation shrinks, the bound grows. A caller can compare this explicit expression with a desired margin, but it is a noncomputable real-valued bound, not an executable estimator. Its ULP terms also need not be smooth.

For example, an exact denominator lower bound of two and denominator error at most one quarter leave a rounded denominator at least seven quarters. That surviving margin is what permits the reciprocal estimate. Letting the error approach two would remove this argument even if one particular rounded denominator happened to remain positive. The theorem uses a uniform bound that must justify every value admitted by its premises, rather than inspecting only a favorable sample. The squared reciprocal in the denominator-error term makes this loss of separation especially costly.

The remaining names in nfOps specialize this reasoning in different ways. The reciprocal sigmoid budget theorem bounds the old evaluation sequence under its stated small-error conditions. The stable sigmoid theorem instead follows the branch of the public implementation, including the exponential used as a numerator in the negative branch. The exact-count mean lemma removes uncertainty about representing the divisor; it still accounts for the rounded sum and final division. A closed form for one of these budgets is useful only with the hypotheses belonging to that particular sequence.

A safe division example has three pieces: the mathematical value is a guarded division, the runtime value is computed by safeDivR eps xR yR, and the theorem states that the runtime value approximates the guarded spec value under the declared tolerance.

The theorem covers the guarded function, including its declared behavior at y=0. To use it for ordinary division, a caller must additionally show that neither execution activates the guard.

@approxTensor_reduce_sum_rows : ∀ {β : Radix} {fexp : ℤ → ℤ} [inst : ValidExp fexp] {rnd : ℝ → ℤ}
  [ValidRndToNearest rnd] {m n : ℕ} {xS : Spec.SpecTensor [m, n]} {xR : TorchLean.Tensor (NF β fexp rnd) [m, n]}
  {eps : ℝ},
  approxTensor toSpec xS xR eps →
    ∀ (hRed : Spec.Shape.NonemptyAxis 1 [m, n]),
      approxTensor toSpec (TorchLean.Tensor.reduceSum 1 xS hRed) (TorchLean.Tensor.reduceSum 1 xR hRed)
        (linfNorm (sumRowBoundVec eps xR))

@approxTensor_reduce_mean_rows : ∀ {β : Radix} {fexp : ℤ → ℤ} [inst : ValidExp fexp] {rnd : ℝ → ℤ}
  [ValidRndToNearest rnd] {m n : ℕ} {xS : Spec.SpecTensor [m, n]} {xR : TorchLean.Tensor (NF β fexp rnd) [m, n]}
  {eps : ℝ},
  approxTensor toSpec xS xR eps →
    ∀ (hRed : Spec.Shape.NonemptyAxis 1 [m, n]),
      approxTensor toSpec (TorchLean.Tensor.reduceMean 1 xS hRed) (TorchLean.Tensor.reduceMean 1 xR hRed)
        (linfNorm (meanRowBoundVec eps xR))

@approxTensor_reduce_sum_columns : ∀ {β : Radix} {fexp : ℤ → ℤ} [inst : ValidExp fexp] {rnd : ℝ → ℤ}
  [ValidRndToNearest rnd] {m n : ℕ} {xS : Spec.SpecTensor [m, n]} {xR : TorchLean.Tensor (NF β fexp rnd) [m, n]}
  {eps : ℝ},
  approxTensor toSpec xS xR eps →
    ∀ (hRed : Spec.Shape.NonemptyAxis 0 [m, n]),
      approxTensor toSpec (TorchLean.Tensor.reduceSum 0 xS hRed) (TorchLean.Tensor.reduceSum 0 xR hRed)
        (linfNorm (sumColumnBoundVec eps xR))

(2.000000, 2.000000)

(1.000000, 0.000000)