TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

NN.Examples.DeepDives.Floats.EffectiveRounding

Effective Rounding in Tensor Semantics #

This example uses the same shape-indexed tensor operation twice. The FP32 tensor gives the proof-oriented rounded-real semantics. The IEEE32Exec tensor executes binary32 arithmetic from bits. On a finite result, the IEEE bridge and the effective rounding calculation identify the same canonical mantissa and exponent.

source
def NN.Examples.DeepDives.Floats.EffectiveRounding.width :
ℕ
Instances For
    source
    @[reducible, inline]
    abbrev NN.Examples.DeepDives.Floats.EffectiveRounding.vectorShape :
    Spec.Shape
    Instances For
      source
      def NN.Examples.DeepDives.Floats.EffectiveRounding.runtimeOnes :
      Spec.Tensor TorchLean.Floats.IEEE754.IEEE32Exec vectorShape

      Executable binary32 tensors used by the example.

      Instances For
        source
        def NN.Examples.DeepDives.Floats.EffectiveRounding.runtimeTwos :
        Spec.Tensor TorchLean.Floats.IEEE754.IEEE32Exec vectorShape
        Instances For
          source
          def NN.Examples.DeepDives.Floats.EffectiveRounding.runtimeSum :
          Spec.Tensor TorchLean.Floats.IEEE754.IEEE32Exec vectorShape

          This addition executes pointwise in the bit-level IEEE32 model.

          Instances For
            source
            noncomputable def NN.Examples.DeepDives.Floats.EffectiveRounding.specOne :
            TorchLean.Floats.FP32

            Proof-oriented tensors use the same tensor API with rounded-real FP32 scalars.

            Instances For
              source
              noncomputable def NN.Examples.DeepDives.Floats.EffectiveRounding.specTwo :
              TorchLean.Floats.FP32
              Instances For
                source
                noncomputable def NN.Examples.DeepDives.Floats.EffectiveRounding.specOnes :
                Spec.Tensor TorchLean.Floats.FP32 vectorShape
                Instances For
                  source
                  noncomputable def NN.Examples.DeepDives.Floats.EffectiveRounding.specTwos :
                  Spec.Tensor TorchLean.Floats.FP32 vectorShape
                  Instances For
                    source
                    noncomputable def NN.Examples.DeepDives.Floats.EffectiveRounding.specSum :
                    Spec.Tensor TorchLean.Floats.FP32 vectorShape
                    Instances For
                      source
                      theorem NN.Examples.DeepDives.Floats.EffectiveRounding.specSum_entry_computed (i : Fin width) :
                      (specSum.vecGet i).toReal = TorchLean.Floats.neuralToReal { mantissa := TorchLean.Floats.neuralNearestEvenMantissa (TorchLean.Floats.neuralScaledMantissa TorchLean.Floats.binaryRadix TorchLean.Floats.fexp32 (specOne.val + specTwo.val)), exponent := TorchLean.Floats.neuralCexp TorchLean.Floats.binaryRadix TorchLean.Floats.fexp32 (specOne.val + specTwo.val) }

                      Every proof-oriented tensor entry exposes the effective nearest-even representation.

                      source
                      theorem NN.Examples.DeepDives.Floats.EffectiveRounding.runtimeSum_entry_computed (i : Fin width) :
                      (runtimeSum.vecGet i).toReal = TorchLean.Floats.neuralToReal { mantissa := TorchLean.Floats.neuralNearestEvenMantissa (TorchLean.Floats.neuralScaledMantissa TorchLean.Floats.binaryRadix TorchLean.Floats.fexp32 (TorchLean.Floats.IEEE754.IEEE32Exec.posOne.toReal + (TorchLean.Floats.IEEE754.IEEE32Exec.ofBits 1073741824).toReal)), exponent := TorchLean.Floats.neuralCexp TorchLean.Floats.binaryRadix TorchLean.Floats.fexp32 (TorchLean.Floats.IEEE754.IEEE32Exec.posOne.toReal + (TorchLean.Floats.IEEE754.IEEE32Exec.ofBits 1073741824).toReal) }

                      Every executable tensor entry reaches the same effective representation once finiteness is checked. The finiteness premise is discharged by computation for the concrete $1+2$ example.

                      Exact subtraction, local spacing, and absorption #

                      source
                      theorem NN.Examples.DeepDives.Floats.EffectiveRounding.two_sub_one_exact :
                      TorchLean.Floats.round₃₂ (2 - 1) = 2 - 1

                      Sterbenz's lemma certifies the concrete binary32 subtraction $2-1$ as exact.

                      source
                      theorem NN.Examples.DeepDives.Floats.EffectiveRounding.runtime_two_sub_one_exact :
                      ((TorchLean.Floats.IEEE754.IEEE32Exec.ofBits 1073741824).sub TorchLean.Floats.IEEE754.IEEE32Exec.posOne).toReal = (TorchLean.Floats.IEEE754.IEEE32Exec.ofBits 1073741824).toReal - TorchLean.Floats.IEEE754.IEEE32Exec.posOne.toReal

                      The corresponding executable binary32 operation also denotes the exact real subtraction.

                      source
                      theorem NN.Examples.DeepDives.Floats.EffectiveRounding.posOne_ulpExp :
                      TorchLean.Floats.IEEE754.IEEE32Exec.posOne.ulpExp? = some (-23)

                      The executable ULP exponent at 1.0 is -23.

                      source
                      theorem NN.Examples.DeepDives.Floats.EffectiveRounding.posOne_ulp :
                      TorchLean.Floats.neuralBpow TorchLean.Floats.binaryRadix (-23) = TorchLean.Floats.ulp₃₂ TorchLean.Floats.IEEE754.IEEE32Exec.posOne.toReal

                      The computed exponent therefore denotes the mathematical ULP at 1.0.

                      source
                      theorem NN.Examples.DeepDives.Floats.EffectiveRounding.posInf_ulpExp :
                      TorchLean.Floats.IEEE754.IEEE32Exec.posInf.ulpExp? = none

                      NaN and infinity have no finite ULP exponent.

                      source
                      theorem NN.Examples.DeepDives.Floats.EffectiveRounding.posOne_absorbs_posMinSubnormal :
                      TorchLean.Floats.IEEE754.IEEE32Exec.posOne.absorbs TorchLean.Floats.IEEE754.IEEE32Exec.posMinSubnormal = true

                      Adding the smallest positive subnormal does not change executable binary32 1.0.

                      source
                      theorem NN.Examples.DeepDives.Floats.EffectiveRounding.posOne_add_posMinSubnormal_rounds_to_posOne :
                      TorchLean.Floats.round₃₂ (TorchLean.Floats.IEEE754.IEEE32Exec.posOne.toReal + TorchLean.Floats.IEEE754.IEEE32Exec.posMinSubnormal.toReal) = TorchLean.Floats.IEEE754.IEEE32Exec.posOne.toReal

                      The executable absorption result transports to the rounded-real binary32 specification.

                      Named rounding modes and fused enclosures #

                      source
                      noncomputable def NN.Examples.DeepDives.Floats.EffectiveRounding.oneThirdDown :
                      ℝ

                      The public mode API avoids passing a raw integer-rounding function at each call site.

                      Instances For
                        source
                        theorem NN.Examples.DeepDives.Floats.EffectiveRounding.oneThirdDown_le :
                        oneThirdDown ≤ 1 / 3

                        Directed rounding gives a certified lower endpoint, not merely a differently named value.

                        source
                        def NN.Examples.DeepDives.Floats.EffectiveRounding.fusedLower :
                        TorchLean.Floats.IEEE754.IEEE32Exec

                        A concrete fused multiply-add lower endpoint, computed directly from binary32 inputs.

                        Instances For
                          source
                          def NN.Examples.DeepDives.Floats.EffectiveRounding.fusedUpper :
                          TorchLean.Floats.IEEE754.IEEE32Exec

                          The corresponding upper endpoint.

                          Instances For
                            source
                            theorem NN.Examples.DeepDives.Floats.EffectiveRounding.fused_enclosure :
                            fusedLower.toEReal ≤ ↑(TorchLean.Floats.IEEE754.IEEE32Exec.posOne.toReal * (TorchLean.Floats.IEEE754.IEEE32Exec.ofBits 1073741824).toReal + (TorchLean.Floats.IEEE754.IEEE32Exec.ofBits 1048576000).toReal) ∧ ↑(TorchLean.Floats.IEEE754.IEEE32Exec.posOne.toReal * (TorchLean.Floats.IEEE754.IEEE32Exec.ofBits 1073741824).toReal + (TorchLean.Floats.IEEE754.IEEE32Exec.ofBits 1048576000).toReal) ≤ fusedUpper.toEReal

                            The executable directed FMA endpoints enclose the exact single-rounding expression.

                            source
                            def NN.Examples.DeepDives.Floats.EffectiveRounding.sqrtLower :
                            TorchLean.Floats.IEEE754.IEEE32Exec

                            Directed binary32 square-root endpoints for the exact input 2.

                            Instances For
                              source
                              def NN.Examples.DeepDives.Floats.EffectiveRounding.sqrtUpper :
                              TorchLean.Floats.IEEE754.IEEE32Exec
                              Instances For
                                source
                                theorem NN.Examples.DeepDives.Floats.EffectiveRounding.sqrt_enclosure :
                                sqrtLower.toEReal ≤ ↑√(TorchLean.Floats.IEEE754.IEEE32Exec.ofBits 1073741824).toReal ∧ ↑√(TorchLean.Floats.IEEE754.IEEE32Exec.ofBits 1073741824).toReal ≤ sqrtUpper.toEReal

                                The executable endpoints enclose the exact real value sqrt 2.

                                Fixed grids, quantization, and double rounding #

                                source
                                noncomputable def NN.Examples.DeepDives.Floats.EffectiveRounding.signedQuarterQuantizer :
                                TorchLean.Floats.Quantization.AffineQuantizer

                                A signed affine code set with quarter-unit spacing. The construction is not tied to a tensor layout or storage width; those choices only determine the integer code bounds.

                                Instances For
                                  source
                                  theorem NN.Examples.DeepDives.Floats.EffectiveRounding.signedQuarterQuantizer_roundtrip {code : ℤ} (hlo : -128 ≤ code) (hhi : code ≤ 127) :
                                  signedQuarterQuantizer.quantize TorchLean.Floats.neuralNearestEven (signedQuarterQuantizer.dequantize code) = code

                                  Every in-range code is recovered exactly after dequantization and requantization.

                                  source
                                  theorem NN.Examples.DeepDives.Floats.EffectiveRounding.signedQuarterQuantizer_error (x : ℝ) (hlo : signedQuarterQuantizer.qmin ≤ signedQuarterQuantizer.rawCode TorchLean.Floats.neuralNearestEven x) (hhi : signedQuarterQuantizer.rawCode TorchLean.Floats.neuralNearestEven x ≤ signedQuarterQuantizer.qmax) :
                                  |signedQuarterQuantizer.dequantize (signedQuarterQuantizer.quantize TorchLean.Floats.neuralNearestEven x) - x| ≤ 1 / 8

                                  When saturation is inactive, nearest-even reconstruction is within half a quantization step.

                                  source
                                  def NN.Examples.DeepDives.Floats.EffectiveRounding.quarterCodes :
                                  Spec.Tensor ℤ vectorShape

                                  Four valid codes, represented with the same shape-indexed tensor used by TorchLean models.

                                  Instances For
                                    source
                                    theorem NN.Examples.DeepDives.Floats.EffectiveRounding.quarterCodes_roundtrip :
                                    signedQuarterQuantizer.quantizeTensor TorchLean.Floats.neuralNearestEven (signedQuarterQuantizer.dequantizeTensor quarterCodes) = quarterCodes

                                    Pointwise tensor Q/DQ is exact on an in-range code tensor.

                                    source
                                    theorem NN.Examples.DeepDives.Floats.EffectiveRounding.quarterGrid_doubleRounding_safe (extra : ℕ) (x : ℝ) :
                                    TorchLean.Floats.neuralRoundAtScale TorchLean.Floats.neuralNearestEven (1 / 4) signedQuarterQuantizer._proof_1 (TorchLean.Floats.neuralRoundAtScale TorchLean.Floats.neuralOddRound (1 / 4 / 2 ^ (extra + 2)) ⋯ x) = TorchLean.Floats.neuralRoundAtScale TorchLean.Floats.neuralNearestEven (1 / 4) signedQuarterQuantizer._proof_1 x

                                    Round-to-odd on a sufficiently fine binary grid prevents double rounding on the quarter grid.

                                    IEEE exception status #

                                    source
                                    theorem NN.Examples.DeepDives.Floats.EffectiveRounding.one_div_zero_status :
                                    (TorchLean.Floats.IEEE754.IEEE32Exec.posOne.divWithStatus TorchLean.Floats.IEEE754.IEEE32Exec.posZero).status.divideByZero = true ∧ (TorchLean.Floats.IEEE754.IEEE32Exec.posOne.divWithStatus TorchLean.Floats.IEEE754.IEEE32Exec.posZero).status.invalid = false

                                    The status-bearing API records division by zero separately from invalid operation.

                                    A training-shaped reduction #

                                    source
                                    def NN.Examples.DeepDives.Floats.EffectiveRounding.runtimeDotTree :
                                    TorchLean.Floats.IEEE754.SumTree (TorchLean.Floats.IEEE754.IEEE32Exec × TorchLean.Floats.IEEE754.IEEE32Exec)

                                    A fixed two-term dot-product tree. Its shape records the accumulation order.

                                    Instances For
                                      source
                                      theorem NN.Examples.DeepDives.Floats.EffectiveRounding.runtimeDotTree_finite :
                                      TorchLean.Floats.IEEE754.IEEE32Exec.FiniteEvalDot runtimeDotTree

                                      Every intermediate product and addition in the example remains finite.

                                      source
                                      theorem NN.Examples.DeepDives.Floats.EffectiveRounding.runtimeDotTree_computed :
                                      (TorchLean.Floats.IEEE754.IEEE32Exec.evalDotIEEE runtimeDotTree).toReal = TorchLean.Floats.neuralToReal { mantissa := TorchLean.Floats.neuralNearestEvenMantissa (TorchLean.Floats.neuralScaledMantissa TorchLean.Floats.binaryRadix TorchLean.Floats.fexp32 (TorchLean.Floats.IEEE754.IEEE32Exec.evalRealDotIEEE (TorchLean.Floats.IEEE754.SumTree.leaf (TorchLean.Floats.IEEE754.IEEE32Exec.posOne, TorchLean.Floats.IEEE754.IEEE32Exec.ofBits 1073741824)) + TorchLean.Floats.IEEE754.IEEE32Exec.evalRealDotIEEE (TorchLean.Floats.IEEE754.SumTree.leaf (TorchLean.Floats.IEEE754.IEEE32Exec.ofBits 1077936128, TorchLean.Floats.IEEE754.IEEE32Exec.ofBits 1082130432)))), exponent := TorchLean.Floats.neuralCexp TorchLean.Floats.binaryRadix TorchLean.Floats.fexp32 (TorchLean.Floats.IEEE754.IEEE32Exec.evalRealDotIEEE (TorchLean.Floats.IEEE754.SumTree.leaf (TorchLean.Floats.IEEE754.IEEE32Exec.posOne, TorchLean.Floats.IEEE754.IEEE32Exec.ofBits 1073741824)) + TorchLean.Floats.IEEE754.IEEE32Exec.evalRealDotIEEE (TorchLean.Floats.IEEE754.SumTree.leaf (TorchLean.Floats.IEEE754.IEEE32Exec.ofBits 1077936128, TorchLean.Floats.IEEE754.IEEE32Exec.ofBits 1082130432))) }

                                      The executable dot product decodes to the computed mantissa/exponent representation of its final rounded accumulation. The two leaf multiplications are rounded before this final addition.