TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

NN.Proofs.RuntimeApprox.Rounding

Scalar Rounding Approximation #

Rounding-level approximation lemmas.

This module begins the runtime-to-spec bridge. It gives compositional error bounds for expressions evaluated under a declared Flocq.round rounded-real model such as NF. The NF operator and graph modules lift these scalar lemmas to tensors and end-to-end executions.

PyTorch correspondence / citations #

In ordinary PyTorch execution, floating-point ops are performed in a chosen dtype (e.g. float32) with hardware/IEEE-754 rounding. In TorchLean, Flocq.round/NF is a proof-relevant rounding model where each operation exposes an explicit ulp-style error bound suitable for composition. https://pytorch.org/docs/stable/tensor_attributes.html#torch.dtype

Scalar Approximation Predicate #

source
def Proofs.RuntimeRoundingApprox.scalarApprox (x xhat eps : ℝ) :
Prop

Absolute-error approximation for scalar real values.

scalarApprox x xhat eps means the rounded/interpreted value xhat is within absolute error eps of the ideal real value x.

Instances For
    source
    theorem Proofs.RuntimeRoundingApprox.scalarApprox_to_approxR_absOnly {x xhat eps : ℝ} (h : scalarApprox x xhat eps) :
    RuntimeApprox.approxR x xhat (RuntimeApprox.ApproxTol.absOnly eps)

    Convert the scalar rounding predicate to the shared ApproxTol.absOnly predicate.

    Single-Step Rounding Bounds #

    source
    noncomputable def Proofs.RuntimeRoundingApprox.roundR {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} (x : ℝ) :
    ℝ

    Interpret one rounded real operation as Flocq.round applied to a real input.

    Instances For
      source
      theorem Proofs.RuntimeRoundingApprox.roundR_abs_error {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidRndToNearest rnd] (x : ℝ) :
      |roundR x - x| ≤ FloatLib.Floats.Formats.Flocq.ulp β fexp x / 2

      One Flocq.round step is within half an ulp of the exact real input.

      Compositional Bounds For + And * #

      source
      noncomputable def Proofs.RuntimeRoundingApprox.roundedAdd {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} (x y : ℝ) :
      ℝ

      Rounded addition: compute roundR (x + y).

      Instances For
        source
        noncomputable def Proofs.RuntimeRoundingApprox.roundedMul {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} (x y : ℝ) :
        ℝ

        Rounded multiplication: compute roundR (x * y).

        Instances For
          source
          theorem Proofs.RuntimeRoundingApprox.scalarApprox_roundedAdd {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidRndToNearest rnd] {x y xhat yhat epsx epsy : ℝ} (hx : scalarApprox x xhat epsx) (hy : scalarApprox y yhat epsy) :
          scalarApprox (x + y) (roundedAdd xhat yhat) (epsx + epsy + FloatLib.Floats.Formats.Flocq.ulp β fexp (xhat + yhat) / 2)

          Compositional absolute-error bound for rounded addition.

          The output budget is the input budgets plus one fresh rounding term for the addition result.

          source
          theorem Proofs.RuntimeRoundingApprox.scalarApprox_roundedMul {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidRndToNearest rnd] {x y xhat yhat epsx epsy : ℝ} (hx : scalarApprox x xhat epsx) (hy : scalarApprox y yhat epsy) :
          scalarApprox (x * y) (roundedMul xhat yhat) ((|xhat| + epsx) * epsy + (|yhat| + epsy) * epsx + FloatLib.Floats.Formats.Flocq.ulp β fexp (xhat * yhat) / 2)

          Compositional absolute-error bound for rounded multiplication.

          Besides the fresh rounding term for xhat * yhat, the budget includes magnitude-weighted input errors and the conservative cross term 2 * epsx * epsy; it is not a first-order-only estimate.