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; 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 belong 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.signBitImpl {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.expFieldImpl {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.fracFieldImpl {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_signBitImpl_apply {fmt : FloatFormat} (x : Model fmt) :
        x.signBit = x.signBitImpl

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

        source
        @[csimp]
        theorem FloatLib.Floats.Formats.BinaryInterchange.Model.signBit_eq_signBitImpl :
        @signBit = @signBitImpl

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

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

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

        source
        @[csimp]
        theorem FloatLib.Floats.Formats.BinaryInterchange.Model.expField_eq_expFieldImpl :
        @expField = @expFieldImpl

        The compiler decodes the exponent through one conversion to Nat.

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

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

        source
        @[csimp]
        theorem FloatLib.Floats.Formats.BinaryInterchange.Model.fracField_eq_fracFieldImpl :
        @fracField = @fracFieldImpl

        The compiler decodes the fraction through one conversion to Nat.

        source
        @[inline]
        def FloatLib.Floats.Formats.BinaryInterchange.Model.mkBitsImpl (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. Unlike BitVec.ofNat, this avoids computing a redundant modulus after the masked fields have already established the width.

        Instances For
          source
          theorem FloatLib.Floats.Formats.BinaryInterchange.Model.mkBits_eq_mkBitsImpl_apply (fmt : FloatFormat) (sign : Bool) (exponent fraction : ℕ) :
          mkBits fmt sign exponent fraction = mkBitsImpl 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_mkBitsImpl :
          mkBits = mkBitsImpl

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

          source
          @[inline]
          def FloatLib.Floats.Formats.BinaryInterchange.Model.ofFieldsImpl (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_ofFieldsImpl :
            ofFields = ofFieldsImpl

            The compiler constructs explicit fields through the direct natural-number packer.