TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.BinaryInterchange.Arithmetic.FiniteSemantics

Correctness of finite arithmetic #

The arithmetic layer decodes represented inputs to exact dyadics, performs one exact operation, and quantizes once under the selected output policy. These theorems expose that contract through the family-independent NumericalSystem and Operation interfaces.

Subtraction needs one format-specific convention. IEEE, OCP E4M3, FP4, and FP6 retain signed zero, so negation toggles the sign of zero. FNUZ has only one zero encoding, so its exact semantic negation canonicalizes zero to positive zero.

source
@[inline]
def FloatLib.Floats.Formats.BinaryInterchange.Model.quantizedValue (fmt : FloatFormat) (policy : Numerics.QuantizationPolicy) (entropy : ℕ) (value : Numerics.Dyadic) :
Numerics.NumericalValue Numerics.Dyadic

Complete denotation produced by quantizing one exact dyadic.

Instances For
    source
    def FloatLib.Floats.Formats.BinaryInterchange.Model.quantizedRatValue (fmt : FloatFormat) (policy : Numerics.QuantizationPolicy) (entropy : ℕ) (sign : Bool) (num den : ℕ) :
    Numerics.NumericalValue Numerics.Dyadic

    Complete denotation produced by quantizing one exact rational magnitude.

    Instances For
      source
      def FloatLib.Floats.Formats.BinaryInterchange.Model.divValue (fmt : FloatFormat) (policy : Numerics.QuantizationPolicy) (entropy : ℕ) (left right : Numerics.Dyadic) :
      Numerics.NumericalValue Numerics.Dyadic

      Denotation of the quantized exact quotient, or undefined for a zero divisor.

      Instances For
        source
        theorem FloatLib.Floats.Formats.BinaryInterchange.Model.negExact_refines (fmt : FloatFormat) :
        Numerics.Operation.Finite1 (exactNumericalSystem fmt) (exactNumericalSystem fmt) neg (negDyadic fmt)

        Negation refines format-aware exact dyadic negation on every represented finite input.

        source
        theorem FloatLib.Floats.Formats.BinaryInterchange.Model.addFinite_refines (fmt : FloatFormat) (policy : Numerics.QuantizationPolicy) (entropy : ℕ) :
        Numerics.Operation.Checked2 (exactNumericalSystem fmt) (exactNumericalSystem fmt) (exactNumericalSystem fmt) (addFinite? fmt policy entropy) fun (left right : (exactNumericalSystem fmt).Scalar) => quantizedValue fmt policy entropy (addDyadic left right)

        Finite addition performs exact dyadic addition followed by one quantization.

        source
        theorem FloatLib.Floats.Formats.BinaryInterchange.Model.subFinite_refines (fmt : FloatFormat) (policy : Numerics.QuantizationPolicy) (entropy : ℕ) :
        Numerics.Operation.Checked2 (exactNumericalSystem fmt) (exactNumericalSystem fmt) (exactNumericalSystem fmt) (subFinite? fmt policy entropy) fun (left right : (exactNumericalSystem fmt).Scalar) => quantizedValue fmt policy entropy (addDyadic left (negDyadic fmt right))

        Finite subtraction performs exact format-aware negation and addition, then quantizes once.

        source
        theorem FloatLib.Floats.Formats.BinaryInterchange.Model.mulFinite_refines (fmt : FloatFormat) (policy : Numerics.QuantizationPolicy) (entropy : ℕ) :
        Numerics.Operation.Checked2 (exactNumericalSystem fmt) (exactNumericalSystem fmt) (exactNumericalSystem fmt) (mulFinite? fmt policy entropy) fun (left right : (exactNumericalSystem fmt).Scalar) => quantizedValue fmt policy entropy (mulDyadic left right)

        Finite multiplication performs an exact dyadic product followed by one quantization.

        source
        theorem FloatLib.Floats.Formats.BinaryInterchange.Model.fmaFinite_refines (fmt : FloatFormat) (policy : Numerics.QuantizationPolicy) (entropy : ℕ) :
        Numerics.Operation.Checked3 (exactNumericalSystem fmt) (exactNumericalSystem fmt) (exactNumericalSystem fmt) (exactNumericalSystem fmt) (fmaFinite? fmt policy entropy) fun (x y z : (exactNumericalSystem fmt).Scalar) => quantizedValue fmt policy entropy (addDyadic (mulDyadic x y) z)

        Finite fused multiply-add has one quantization after the exact product and sum.

        source
        theorem FloatLib.Floats.Formats.BinaryInterchange.Model.mulAddFinite_refines (storage accumulator : FloatFormat) (policy : Numerics.QuantizationPolicy) (entropy : ℕ) :
        Numerics.Operation.Checked3 (exactNumericalSystem storage) (exactNumericalSystem storage) (exactNumericalSystem accumulator) (exactNumericalSystem accumulator) (mulAddFinite? storage accumulator policy entropy) fun (x y : (exactNumericalSystem storage).Scalar) (acc : (exactNumericalSystem accumulator).Scalar) => quantizedValue accumulator policy entropy (addDyadic (mulDyadic x y) acc)

        Mixed-format multiply-add decodes storage operands and quantizes once into the accumulator.

        source
        theorem FloatLib.Floats.Formats.BinaryInterchange.Model.divFinite_refines (fmt : FloatFormat) (policy : Numerics.QuantizationPolicy) (entropy : ℕ) :
        Numerics.Operation.Checked2On (exactNumericalSystem fmt) (exactNumericalSystem fmt) (exactNumericalSystem fmt) (divFinite? fmt policy entropy) (divValue fmt policy entropy) fun (x right : (exactNumericalSystem fmt).Scalar) => right.significand ≠ 0

        Finite division refines exact rational division whenever the divisor is nonzero.

        source
        theorem FloatLib.Floats.Formats.BinaryInterchange.Model.castFinite_refines (src dst : FloatFormat) (policy : Numerics.QuantizationPolicy) (entropy : ℕ) :
        Numerics.Operation.Checked1 (exactNumericalSystem src) (exactNumericalSystem dst) (Policy.castFinite? src dst policy entropy) (quantizedValue dst policy entropy)

        Finite casts decode exactly and quantize once into the destination format.