TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.BinaryInterchange.Model.Fields.Optimized

Optimized field access for binary models #

The public field operations in Model.Carrier use exact-width bit vectors, which expose the storage layout cleanly to proofs. This module defines extensionally equal Nat implementations and registers their compiler substitutions. Each field decoder reads the natural-number storage pattern, and packing constructs one natural-number pattern with an erased proof that it fits the width.

The theorems here are execution certificates: they justify erased bounds or compiler rewrites. Semantic facts about the public field operations are in Model.Fields.Proof.

source
theorem FloatLib.Floats.Formats.BinaryInterchange.Model.packedFields_lt_storage (fmt : FloatFormat) (sign : Bool) (exponent fraction : ℕ) :
(if sign = true then Nat.shiftLeft 1 (fmt.expWidth + fmt.fracWidth) else 0) ||| (exponent &&& fmt.expAllOnesNat).shiftLeft fmt.fracWidth ||| fraction &&& fmt.fracMaskNat < 2 ^ fmt.bitWidth

Masked sign, exponent, and fraction fields always fit their declared storage word.

source
@[inline]
def FloatLib.Floats.Formats.BinaryInterchange.Model.Internal.signBit {fmt : FloatFormat} (x : Model fmt) :
Bool

Read the sign directly from the natural-number storage pattern.

Instances For
    source
    @[inline]
    def FloatLib.Floats.Formats.BinaryInterchange.Model.Internal.expField {fmt : FloatFormat} (x : Model fmt) :
    ℕ

    Decode the exponent after one conversion of the storage word to Nat.

    Instances For
      source
      @[inline]
      def FloatLib.Floats.Formats.BinaryInterchange.Model.Internal.fracField {fmt : FloatFormat} (x : Model fmt) :
      ℕ

      Decode the fraction after one conversion of the storage word to Nat.

      Instances For
        source
        theorem FloatLib.Floats.Formats.BinaryInterchange.Model.signBit_eq_internal_apply {fmt : FloatFormat} (x : Model fmt) :
        x.signBit = Internal.signBit x

        The direct natural-number sign decoder agrees with the public bit-vector definition.

        source
        @[csimp]
        theorem FloatLib.Floats.Formats.BinaryInterchange.Model.signBit_eq_internal :
        @signBit = @Internal.signBit

        The compiler reads the sign from the natural-number storage pattern.

        source
        theorem FloatLib.Floats.Formats.BinaryInterchange.Model.expField_eq_internal_apply {fmt : FloatFormat} (x : Model fmt) :
        x.expField = Internal.expField x

        The direct natural-number exponent decoder agrees with the public bit-vector definition.

        source
        @[csimp]
        theorem FloatLib.Floats.Formats.BinaryInterchange.Model.expField_eq_internal :
        @expField = @Internal.expField

        The compiler decodes the exponent through one conversion to Nat.

        source
        theorem FloatLib.Floats.Formats.BinaryInterchange.Model.fracField_eq_internal_apply {fmt : FloatFormat} (x : Model fmt) :
        x.fracField = Internal.fracField x

        The direct natural-number fraction decoder agrees with the public bit-vector definition.

        source
        @[csimp]
        theorem FloatLib.Floats.Formats.BinaryInterchange.Model.fracField_eq_internal :
        @fracField = @Internal.fracField

        The compiler decodes the fraction through one conversion to Nat.

        source
        @[inline]
        def FloatLib.Floats.Formats.BinaryInterchange.Model.Internal.mkBits (fmt : FloatFormat) (sign : Bool) (exponent fraction : ℕ) :
        fmt.ExecWord

        Pack fields as one natural-number bit pattern known to fit the exact storage width.

        The bound passed to BitVec.ofNatLT is erased from compiled code. This avoids the redundant modulus of BitVec.ofNat, since the masked fields already establish the width.

        Instances For
          source
          theorem FloatLib.Floats.Formats.BinaryInterchange.Model.mkBits_eq_internal_apply (fmt : FloatFormat) (sign : Bool) (exponent fraction : ℕ) :
          mkBits fmt sign exponent fraction = Internal.mkBits fmt sign exponent fraction

          The direct natural-number field packer agrees with the public mask-based definition.

          source
          @[csimp]
          theorem FloatLib.Floats.Formats.BinaryInterchange.Model.mkBits_eq_internal :
          mkBits = Internal.mkBits

          The compiler packs fields as one natural-number bit pattern.

          source
          @[inline]
          def FloatLib.Floats.Formats.BinaryInterchange.Model.Internal.ofFields (fmt : FloatFormat) (sign : Bool) (exponent fraction : ℕ) :
          Model fmt

          Construct a Model through the direct natural-number field packer.

          Instances For
            source
            @[csimp]
            theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ofFields_eq_internal :
            ofFields = Internal.ofFields

            The compiler builds ofFields through the direct natural-number packer.