TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

NN.Floats.IEEEExec.Bridge.Finite

Finite configured arithmetic for reduction proofs #

FloatLib supplies the arithmetic kernels and their real rounding semantics. This module transports those theorems to configured values for any IEEE format and model codec. A finite add or multiply result implies finite operands, so their refinement statements need only result finiteness. The binary32 declarations specialize this shared bridge for existing reduction proofs. No global relative-error assumption is made at subnormal values.

source
@[simp]
theorem TorchLean.Floats.IEEEExec.toModel_add {format : FloatLib.Floats.Formats.BinaryInterchange.FloatFormat} {plan : FloatLib.Floats.Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [FloatLib.Floats.ExecFloat.ModelCodec plan (FloatLib.Floats.Formats.BinaryInterchange.Model format) code] (x y : FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)) :
FloatLib.Floats.ExecFloat.Binary.toModel (x.add 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.IEEEExec.toModel_mul {format : FloatLib.Floats.Formats.BinaryInterchange.FloatFormat} {plan : FloatLib.Floats.Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [FloatLib.Floats.ExecFloat.ModelCodec plan (FloatLib.Floats.Formats.BinaryInterchange.Model format) code] (x y : FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)) :
FloatLib.Floats.ExecFloat.Binary.toModel (x.mul 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.IEEEExec.model_isFinite_quietNaN {format : FloatLib.Floats.Formats.BinaryInterchange.FloatFormat} (hformat : format.isIEEE = true) (x : FloatLib.Floats.Formats.BinaryInterchange.Model format) :
x.quietNaN.isFinite = x.isFinite

Quieting a NaN preserves its non-finite classification.

source
theorem TorchLean.Floats.IEEEExec.model_isFinite_chooseNaN2 {format : FloatLib.Floats.Formats.BinaryInterchange.FloatFormat} (hformat : format.isIEEE = true) (x y n : FloatLib.Floats.Formats.BinaryInterchange.Model format) (h : x.chooseNaN2 y = some n) :
n.isFinite = false

A selected IEEE NaN cannot be finite.

source
theorem TorchLean.Floats.IEEEExec.model_isFinite_invalidResult {format : FloatLib.Floats.Formats.BinaryInterchange.FloatFormat} (hformat : format.isIEEE = true) :
(FloatLib.Floats.Formats.BinaryInterchange.Model.invalidResult format).isFinite = false

An IEEE invalid operation produces a non-finite value.

source
theorem TorchLean.Floats.IEEEExec.model_isFinite_nativeOverflow {format : FloatLib.Floats.Formats.BinaryInterchange.FloatFormat} (hformat : format.isIEEE = true) (sign : Bool) :
(FloatLib.Floats.Formats.BinaryInterchange.Model.nativeOverflow format sign).isFinite = false

Overflow in an IEEE format produces a non-finite value with either sign.

source
theorem TorchLean.Floats.IEEEExec.toReal_add_eq_round_of_isFinite {format : FloatLib.Floats.Formats.BinaryInterchange.FloatFormat} {plan : FloatLib.Floats.Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [FloatLib.Floats.ExecFloat.ModelCodec plan (FloatLib.Floats.Formats.BinaryInterchange.Model format) code] (hformat : format.isIEEE = true) {x y : FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)} (hfin : FloatLib.Floats.ExecFloat.Binary.isFinite (x.add y) = true) :
(FloatLib.Floats.ExecFloat.Binary.toModel (x.add y)).toReal = FloatLib.Floats.Formats.BinaryInterchange.Model.roundAt format ((FloatLib.Floats.ExecFloat.Binary.toModel x).toReal + (FloatLib.Floats.ExecFloat.Binary.toModel y).toReal)

A finite executable sum is one rounding in the selected IEEE format of the exact real sum.

source
theorem TorchLean.Floats.IEEEExec.toReal_mul_eq_round_of_isFinite {format : FloatLib.Floats.Formats.BinaryInterchange.FloatFormat} {plan : FloatLib.Floats.Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [FloatLib.Floats.ExecFloat.ModelCodec plan (FloatLib.Floats.Formats.BinaryInterchange.Model format) code] (hformat : format.isIEEE = true) {x y : FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)} (hfin : FloatLib.Floats.ExecFloat.Binary.isFinite (x.mul y) = true) :
(FloatLib.Floats.ExecFloat.Binary.toModel (x.mul y)).toReal = FloatLib.Floats.Formats.BinaryInterchange.Model.roundAt format ((FloatLib.Floats.ExecFloat.Binary.toModel x).toReal * (FloatLib.Floats.ExecFloat.Binary.toModel y).toReal)

A finite executable product is one rounding in the selected IEEE format of the exact real product.

source
theorem TorchLean.Floats.IEEEExec.toModel_sub {format : FloatLib.Floats.Formats.BinaryInterchange.FloatFormat} {plan : FloatLib.Floats.Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [FloatLib.Floats.ExecFloat.ModelCodec plan (FloatLib.Floats.Formats.BinaryInterchange.Model format) code] (x y : FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)) :
FloatLib.Floats.ExecFloat.Binary.toModel (x.sub y) = (FloatLib.Floats.ExecFloat.Binary.toModel x).sub (FloatLib.Floats.ExecFloat.Binary.toModel y)

Configured subtraction decodes to FloatLib’s proved model subtraction.

source
theorem TorchLean.Floats.IEEEExec.toReal_sub_eq_round_of_isFinite {format : FloatLib.Floats.Formats.BinaryInterchange.FloatFormat} {plan : FloatLib.Floats.Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [FloatLib.Floats.ExecFloat.ModelCodec plan (FloatLib.Floats.Formats.BinaryInterchange.Model format) code] (hformat : format.isIEEE = true) {x y : FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)} (hx : FloatLib.Floats.ExecFloat.Binary.isFinite x = true) (hy : FloatLib.Floats.ExecFloat.Binary.isFinite y = true) (hfin : FloatLib.Floats.ExecFloat.Binary.isFinite (x.sub y) = true) :
(FloatLib.Floats.ExecFloat.Binary.toModel (x.sub y)).toReal = FloatLib.Floats.Formats.BinaryInterchange.Model.roundAt format ((FloatLib.Floats.ExecFloat.Binary.toModel x).toReal - (FloatLib.Floats.ExecFloat.Binary.toModel y).toReal)

Finite subtraction refines one nearest-even rounding of the real difference.

source
@[simp]
theorem TorchLean.Floats.IEEEExec.toModel_zero {format : FloatLib.Floats.Formats.BinaryInterchange.FloatFormat} {plan : FloatLib.Floats.Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [FloatLib.Floats.ExecFloat.ModelCodec plan (FloatLib.Floats.Formats.BinaryInterchange.Model format) code] :
FloatLib.Floats.ExecFloat.Binary.toModel 0 = FloatLib.Floats.Formats.BinaryInterchange.Model.zero format false

The configured zero literal decodes to positive model zero.

source
@[simp]
theorem TorchLean.Floats.IEEEExec.toReal_zero {format : FloatLib.Floats.Formats.BinaryInterchange.FloatFormat} {plan : FloatLib.Floats.Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [FloatLib.Floats.ExecFloat.ModelCodec plan (FloatLib.Floats.Formats.BinaryInterchange.Model format) code] :
(FloatLib.Floats.ExecFloat.Binary.toModel 0).toReal = 0

The configured zero literal denotes real zero.

source
theorem TorchLean.Floats.IEEEExec.isFinite_zero {format : FloatLib.Floats.Formats.BinaryInterchange.FloatFormat} {plan : FloatLib.Floats.Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [FloatLib.Floats.ExecFloat.ModelCodec plan (FloatLib.Floats.Formats.BinaryInterchange.Model format) code] :
FloatLib.Floats.ExecFloat.Binary.isFinite 0 = true

The configured zero literal is finite.

source
theorem TorchLean.Floats.IEEEExec.toReal_maximum_eq_max_of_isFinite {format : FloatLib.Floats.Formats.BinaryInterchange.FloatFormat} {plan : FloatLib.Floats.Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [FloatLib.Floats.ExecFloat.ModelCodec plan (FloatLib.Floats.Formats.BinaryInterchange.Model format) code] {x y : FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)} (hx : FloatLib.Floats.ExecFloat.Binary.isFinite x = true) (hy : FloatLib.Floats.ExecFloat.Binary.isFinite y = true) :
(x ⊔ y).toModel.toReal = max (FloatLib.Floats.ExecFloat.Binary.toModel x).toReal (FloatLib.Floats.ExecFloat.Binary.toModel y).toReal

IEEE maximum agrees with real maximum on finite operands, including signed zeros.

source
theorem TorchLean.Floats.IEEEExec.toReal_roundDyadic_eq_round {format : FloatLib.Floats.Formats.BinaryInterchange.FloatFormat} {plan : FloatLib.Floats.Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [FloatLib.Floats.ExecFloat.ModelCodec plan (FloatLib.Floats.Formats.BinaryInterchange.Model format) code] (hformat : format.isIEEE = true) {d : FloatLib.Numerics.Dyadic} (hfin : (FloatLib.Floats.ExecFloat.Binary.ofModel (FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadic format d)).isFinite = true) :
(FloatLib.Floats.ExecFloat.Binary.ofModel (FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadic format d)).toModel.toReal = FloatLib.Floats.Formats.BinaryInterchange.Model.roundAt format d.toReal

Finite dyadic conversion refines rounding of the exact dyadic real value.

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) = x.toModel.add y.toModel

Configured addition decodes to FloatLib's proved model addition.

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
theorem TorchLean.Floats.IEEE754.IEEE32Exec.model_isFinite_invalidResult :
(FloatLib.Floats.Formats.BinaryInterchange.Model.invalidResult FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32).isFinite = false

The invalid-operation result is a non-finite binary32 value.

source
theorem TorchLean.Floats.IEEE754.IEEE32Exec.model_isFinite_nativeOverflow (sign : Bool) :
(FloatLib.Floats.Formats.BinaryInterchange.Model.nativeOverflow FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 sign).isFinite = false

Binary32 overflow produces a non-finite value with either sign.

source
theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_add_eq_round_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 = FloatLib.Floats.Formats.BinaryInterchange.Model.roundAt FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 (x.toModel.toReal + y.toModel.toReal)

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

source
theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_mul_eq_round_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.BinaryInterchange.Model.roundAt FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 (x.toModel.toReal * y.toModel.toReal)

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

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 (FloatLib.Floats.Formats.BinaryInterchange.Model.fexpOf FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32) (x.toModel.toReal * y.toModel.toReal)), exponent := FloatLib.Floats.Formats.Flocq.cexp FloatLib.Numerics.binaryRadix (FloatLib.Floats.Formats.BinaryInterchange.Model.fexpOf FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32) (x.toModel.toReal * y.toModel.toReal) }

Effective representation of a finite executable product.