TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.Block.Configured.Conversion.Runtime

Shared-scale block conversion runtime #

Conversion takes the common binary exponent as an explicit Int context and rounds each lane to the corresponding grid. Conversion.Instances installs this contextual quantizer without a DefaultQuantizer instance.

source
@[inline]
def FloatLib.Floats.ExecFloat.SharedScale.Conversion.status {lanes : ℕ} (exact : Vector ℚ lanes) (rounded : SharedScale lanes) :
ConversionStatus

Conversion status records whether any lane changed at the selected shared scale.

Instances For
    source
    @[inline]
    def FloatLib.Floats.ExecFloat.SharedScale.Conversion.run {lanes : ℕ} (exponent : ℤ) :
    Numerics.NumericalValue (Vector ℚ lanes) → ConversionOutcome (SharedScale lanes)

    Quantize a complete block observation at an explicitly supplied shared exponent.

    Instances For
      source
      def FloatLib.Floats.ExecFloat.SharedScale.Conversion.spec {lanes : ℕ} (exponent : ℤ) (input : Numerics.NumericalValue (Vector ℚ lanes)) (outcome : ConversionOutcome (SharedScale lanes)) :
      Prop

      Relational shared-scale conversion contract.

      Finite success must satisfy the lane-wise nearest-even QuantizesAt relation. Non-finite inputs are rejected because this unbounded block family has no corresponding codes.

      Instances For
        source
        @[instance_reducible]
        instance FloatLib.Floats.ExecFloat.SharedScale.Conversion.exactDecoder {lanes : ℕ} :
        ExactDecoder (SharedScale lanes) (Vector ℚ lanes)

        Shared-scale values decode to their exact rational vector.