TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

NN.Floats.IEEEExec.Bridge.Finite

Finite binary32 arithmetic for reduction proofs #

FloatLib supplies the arithmetic kernels and their real rounding semantics. This module transports those theorems to FloatLib's configured binary32 values. A finite add or multiply result implies finite operands, so the public refinement statements need only the original result-finiteness hypothesis. No global relative-error assumption is made at subnormal values.

source
@[simp]
theorem TorchLean.Floats.IEEE754.IEEE32Exec.toModel_add (x y : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) toModel_add._proof_1 toModel_add._proof_2 toModel_add._proof_3 toModel_add._proof_4) :
FloatLib.Floats.ExecFloat.Binary.toModel (FloatLib.Floats.ExecFloat.add x y) = (FloatLib.Floats.ExecFloat.Binary.toModel x).add (FloatLib.Floats.ExecFloat.Binary.toModel y)

Configured addition decodes to FloatLib's proved model addition.

source
@[simp]
theorem TorchLean.Floats.IEEE754.IEEE32Exec.toModel_mul (x y : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) toModel_add._proof_1 toModel_add._proof_2 toModel_add._proof_3 toModel_add._proof_4) :
FloatLib.Floats.ExecFloat.Binary.toModel (FloatLib.Floats.ExecFloat.mul x y) = (FloatLib.Floats.ExecFloat.Binary.toModel x).mul (FloatLib.Floats.ExecFloat.Binary.toModel y)

Configured multiplication decodes to FloatLib's proved model multiplication.

source
theorem TorchLean.Floats.IEEE754.IEEE32Exec.model_isFinite_quietNaN (x : FloatLib.Floats.Formats.BinaryInterchange.Model FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32) :
x.quietNaN.isFinite = x.isFinite

Quieting a binary32 NaN preserves its non-finite classification.

source
theorem TorchLean.Floats.IEEE754.IEEE32Exec.model_isFinite_chooseNaN2 (x y n : FloatLib.Floats.Formats.BinaryInterchange.Model FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32) (h : x.chooseNaN2 y = some n) :
n.isFinite = false

A selected binary32 NaN cannot be finite.

source
@[reducible, inline]
noncomputable abbrev TorchLean.Floats.IEEE754.IEEE32Exec.fp32Round (x : ℝ) :
ℝ

Nearest-even real rounding with binary32 gradual underflow and no upper exponent bound.

Instances For
    source
    theorem TorchLean.Floats.IEEE754.IEEE32Exec.roundAt_binary32 (x : ℝ) :
    FloatLib.Floats.Formats.BinaryInterchange.Model.roundAt FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 x = fp32Round x

    FloatLib's binary32 real rounding is TorchLean's gradual-underflow rounding grid.

    source
    theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_add_eq_fp32Round_of_isFinite {x y : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) toModel_add._proof_1 toModel_add._proof_2 toModel_add._proof_3 toModel_add._proof_4} (hfin : FloatLib.Floats.ExecFloat.Binary.isFinite (FloatLib.Floats.ExecFloat.add x y) = true) :
    (FloatLib.Floats.ExecFloat.Binary.toModel (FloatLib.Floats.ExecFloat.add x y)).toReal = fp32Round ((FloatLib.Floats.ExecFloat.Binary.toModel x).toReal + (FloatLib.Floats.ExecFloat.Binary.toModel y).toReal)

    A finite executable sum is one binary32 rounding of the exact real sum.

    source
    theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_mul_eq_fp32Round_of_isFinite {x y : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) toModel_add._proof_1 toModel_add._proof_2 toModel_add._proof_3 toModel_add._proof_4} (hfin : FloatLib.Floats.ExecFloat.Binary.isFinite (FloatLib.Floats.ExecFloat.mul x y) = true) :
    (FloatLib.Floats.ExecFloat.Binary.toModel (FloatLib.Floats.ExecFloat.mul x y)).toReal = fp32Round ((FloatLib.Floats.ExecFloat.Binary.toModel x).toReal * (FloatLib.Floats.ExecFloat.Binary.toModel y).toReal)

    A finite executable product is one binary32 rounding of the exact real product.

    source
    theorem TorchLean.Floats.IEEE754.IEEE32Exec.fp32Round_eq_computed (z : ℝ) :
    fp32Round z = FloatLib.Floats.Formats.Flocq.toReal { mantissa := FloatLib.Floats.Formats.Flocq.nearestEvenMantissa (FloatLib.Floats.Formats.Flocq.scaledMantissa FloatLib.Numerics.binaryRadix fexp32 z), exponent := FloatLib.Floats.Formats.Flocq.cexp FloatLib.Numerics.binaryRadix fexp32 z }

    The rounded value has FloatLib's effective mantissa/exponent representation.

    source
    theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_mul_eq_computed_of_isFinite (x y : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) toModel_add._proof_1 toModel_add._proof_2 toModel_add._proof_3 toModel_add._proof_4) (hfin : FloatLib.Floats.ExecFloat.Binary.isFinite (FloatLib.Floats.ExecFloat.mul x y) = true) :
    (FloatLib.Floats.ExecFloat.Binary.toModel (FloatLib.Floats.ExecFloat.mul x y)).toReal = FloatLib.Floats.Formats.Flocq.toReal { mantissa := FloatLib.Floats.Formats.Flocq.nearestEvenMantissa (FloatLib.Floats.Formats.Flocq.scaledMantissa FloatLib.Numerics.binaryRadix fexp32 ((FloatLib.Floats.ExecFloat.Binary.toModel x).toReal * (FloatLib.Floats.ExecFloat.Binary.toModel y).toReal)), exponent := FloatLib.Floats.Formats.Flocq.cexp FloatLib.Numerics.binaryRadix fexp32 ((FloatLib.Floats.ExecFloat.Binary.toModel x).toReal * (FloatLib.Floats.ExecFloat.Binary.toModel y).toReal) }

    Effective representation of a finite executable product.