TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.Posit.Arithmetic.Word.Packed.Quotient.Proof

Correctness of packed native-word Posit division #

The packed divider is a storage adapter over the width-generic quotient-prefix kernel. These theorems connect its decoded field boundary to the model-valued quotient semantics and prove that both natural and UInt64 results are complete in-range Posit encodings.

Mathematical views and common-leading normalization #

source
def FloatLib.Floats.Formats.Posit.Model.NativeWordArithmetic.PackedQuotient.positiveDyadic (significand : UInt64) (exponent : ℤ) :
Numerics.Dyadic

Exact mathematical view of positive decoded native fields.

Instances For

    Quotient-prefix refinement #

    Positive and signed field rounding #

    source
    theorem FloatLib.Floats.Formats.Posit.Model.NativeWordArithmetic.PackedQuotient.roundPositiveCode_eq (format : Format) (heligible : NativeWord.Eligible format) (numeratorSignificand : UInt64) (numeratorExponent : ℤ) (denominatorSignificand : UInt64) (denominatorExponent : ℤ) :
    roundPositiveCode format numeratorSignificand numeratorExponent denominatorSignificand denominatorExponent = DirectDyadicQuotient.roundPositiveCode format (positiveDyadic numeratorSignificand numeratorExponent) (positiveDyadic denominatorSignificand denominatorExponent)

    The positive native kernel is the shared arbitrary-width quotient rounder.

    source
    theorem FloatLib.Floats.Formats.Posit.Model.NativeWordArithmetic.PackedQuotient.roundPositiveCodeWord_toNat (format : Format) (_heligible : NativeWord.Eligible format) (numeratorSignificand : UInt64) (numeratorExponent : ℤ) (denominatorSignificand : UInt64) (denominatorExponent : ℤ) :
    (roundPositiveCodeWord format numeratorSignificand numeratorExponent denominatorSignificand denominatorExponent).toNat = roundPositiveCode format numeratorSignificand numeratorExponent denominatorSignificand denominatorExponent

    The word-valued positive result is definitionally the natural API's code.

    source
    theorem FloatLib.Floats.Formats.Posit.Model.NativeWordArithmetic.PackedQuotient.roundFields_eq (format : Format) (heligible : NativeWord.Eligible format) (numeratorNegative : Bool) (numeratorSignificand : UInt64) (numeratorExponent : ℤ) (denominatorNegative : Bool) (denominatorSignificand : UInt64) (denominatorExponent : ℤ) :
    roundFields format numeratorNegative numeratorSignificand numeratorExponent denominatorNegative denominatorSignificand denominatorExponent = DirectDyadicQuotient.roundCode format { negative := numeratorNegative, significand := numeratorSignificand.toNat, exponent := numeratorExponent } { negative := denominatorNegative, significand := denominatorSignificand.toNat, exponent := denominatorExponent }

    Signed decoded-field rounding is the complete native-word quotient code.

    source
    theorem FloatLib.Floats.Formats.Posit.Model.NativeWordArithmetic.PackedQuotient.roundFieldsWord_toNat (format : Format) (_heligible : NativeWord.Eligible format) (numeratorNegative : Bool) (numeratorSignificand : UInt64) (numeratorExponent : ℤ) (denominatorNegative : Bool) (denominatorSignificand : UInt64) (denominatorExponent : ℤ) :
    (roundFieldsWord format numeratorNegative numeratorSignificand numeratorExponent denominatorNegative denominatorSignificand denominatorExponent).toNat = roundFields format numeratorNegative numeratorSignificand numeratorExponent denominatorNegative denominatorSignificand denominatorExponent

    The word-valued signed result contains the complete scalar code.

    Packed carrier boundary #

    source
    theorem FloatLib.Floats.Formats.Posit.Model.NativeWordArithmetic.PackedQuotient.divWordsCodeValid_eq {format : Format} (heligible : NativeWord.Eligible format) (left right : UInt64) (hleft : left.toNat < format.modulus) (hright : right.toNat < format.modulus) :
    divWordsCodeValid heligible left right hleft hright = match NativeWord.toDyadic? format left, NativeWord.toDyadic? format right with | some numerator, some denominator => DirectDyadicQuotient.roundCode format numerator denominator | x, x_1 => format.signMaskNat

    The packed scalar quotient is the native-word quotient of the decoded operands.

    source
    theorem FloatLib.Floats.Formats.Posit.Model.NativeWordArithmetic.PackedQuotient.divWordsCodeWordValid_toNat {format : Format} (heligible : NativeWord.Eligible format) (left right : UInt64) (hleft : left.toNat < format.modulus) (hright : right.toNat < format.modulus) :
    (divWordsCodeWordValid heligible left right hleft hright).toNat = divWordsCodeValid heligible left right hleft hright

    The carrier-facing quotient word contains the exact scalar packed quotient code.

    source
    theorem FloatLib.Floats.Formats.Posit.Model.NativeWordArithmetic.PackedQuotient.divWordsCodeValid_lt_modulus {format : Format} (heligible : NativeWord.Eligible format) (left right : UInt64) (hleft : left.toNat < format.modulus) (hright : right.toNat < format.modulus) :
    divWordsCodeValid heligible left right hleft hright < format.modulus

    Every packed quotient is a complete in-range Posit encoding.