TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.Codebook.Configured.Catalog

Configured catalog-codebook operations #

Named codebooks expose only the arithmetic justified by their complete denotation. The bipolar table has total negation and multiplication; the ternary table uses checked operations because one word is reserved.

source
@[reducible, inline]
abbrev FloatLib.Floats.ExecFloat.Codebook.Catalog.bipolar1.Value :
Type

Configured one-bit {-1, +1} lookup encoding.

Instances For
    source
    @[inline]
    def FloatLib.Floats.ExecFloat.Codebook.Catalog.bipolar1.negativeOne :
    Value

    Construct the bipolar value negative one without exposing its stored bit.

    Instances For
      source
      @[inline]
      def FloatLib.Floats.ExecFloat.Codebook.Catalog.bipolar1.positiveOne :
      Value

      Construct the bipolar value positive one without exposing its stored bit.

      Instances For
        source
        @[simp]
        theorem FloatLib.Floats.ExecFloat.Codebook.Catalog.bipolar1.decode_negativeOne :
        decode negativeOne = Numerics.NumericalValue.finite (-1)

        The named negative bipolar value has exact integer meaning -1.

        source
        @[simp]
        theorem FloatLib.Floats.ExecFloat.Codebook.Catalog.bipolar1.decode_positiveOne :
        decode positiveOne = Numerics.NumericalValue.finite 1

        The named positive bipolar value has exact integer meaning 1.

        source
        @[inline]
        def FloatLib.Floats.ExecFloat.Codebook.Catalog.bipolar1.neg (value : Value) :
        Value

        Exact additive inverse of a configured bipolar value.

        Instances For
          source
          @[inline]
          def FloatLib.Floats.ExecFloat.Codebook.Catalog.bipolar1.mul (left right : Value) :
          Value

          Exact multiplication of configured bipolar values.

          Instances For
            source
            @[instance_reducible]
            instance FloatLib.Floats.ExecFloat.Codebook.Catalog.bipolar1.instNegValue :
            Neg Value
            source
            def FloatLib.Floats.ExecFloat.Codebook.Catalog.bipolar1.Plan.mulEstimate :
            Backend.Candidate

            Planner estimate for exact one-bit bipolar multiplication.

            Instances For
              source
              def FloatLib.Floats.ExecFloat.Codebook.Catalog.bipolar1.Plan.mulCertified :
              Backend.Certified mul

              Certified bipolar multiplication candidate used by common ExecFloat dispatch.

              Instances For
                source
                @[instance_reducible, always_inline]
                instance FloatLib.Floats.ExecFloat.Codebook.Catalog.bipolar1.instMulFamilyIntBipolar1 [planning : Backend.PolicyFor (Family Formats.Codebook.Catalog.bipolar1)] :
                Mul (Family Formats.Codebook.Catalog.bipolar1)

                The proved bipolar multiplication kernel participates in common ExecFloat dispatch.

                source
                @[reducible, inline]
                abbrev FloatLib.Floats.ExecFloat.Codebook.Catalog.ternary2.Value :
                Type

                Configured two-bit {0, +1, -1, reserved} lookup encoding.

                Instances For
                  source
                  @[inline]
                  def FloatLib.Floats.ExecFloat.Codebook.Catalog.ternary2.zero :
                  Value

                  Construct the ternary codebook's zero without exposing its stored word.

                  Instances For
                    source
                    @[inline]
                    def FloatLib.Floats.ExecFloat.Codebook.Catalog.ternary2.positiveOne :
                    Value

                    Construct the ternary codebook's positive one without exposing its stored word.

                    Instances For
                      source
                      @[inline]
                      def FloatLib.Floats.ExecFloat.Codebook.Catalog.ternary2.negativeOne :
                      Value

                      Construct the ternary codebook's negative one without exposing its stored word.

                      Instances For
                        source
                        @[inline]
                        def FloatLib.Floats.ExecFloat.Codebook.Catalog.ternary2.reserved :
                        Value

                        Construct the ternary codebook's reserved exceptional value.

                        Instances For
                          source
                          @[simp]
                          theorem FloatLib.Floats.ExecFloat.Codebook.Catalog.ternary2.decode_zero :
                          decode zero = Numerics.NumericalValue.finite 0

                          The named ternary zero has exact integer meaning 0.

                          source
                          @[simp]
                          theorem FloatLib.Floats.ExecFloat.Codebook.Catalog.ternary2.decode_positiveOne :
                          decode positiveOne = Numerics.NumericalValue.finite 1

                          The named positive ternary value has exact integer meaning 1.

                          source
                          @[simp]
                          theorem FloatLib.Floats.ExecFloat.Codebook.Catalog.ternary2.decode_negativeOne :
                          decode negativeOne = Numerics.NumericalValue.finite (-1)

                          The named negative ternary value has exact integer meaning -1.

                          source
                          @[simp]
                          theorem FloatLib.Floats.ExecFloat.Codebook.Catalog.ternary2.decode_reserved :
                          decode reserved = Numerics.NumericalValue.exceptional (Numerics.ExceptionalValue.reserved (some 3))

                          The named reserved ternary value denotes the catalog's exceptional observation.

                          source
                          @[inline]
                          def FloatLib.Floats.ExecFloat.Codebook.Catalog.ternary2.neg? (value : Value) :
                          Option Value

                          Exact negation, returning none for the reserved word.

                          Instances For
                            source
                            @[inline]
                            def FloatLib.Floats.ExecFloat.Codebook.Catalog.ternary2.mul? (left right : Value) :
                            Option Value

                            Exact multiplication, returning none if either operand is the reserved word.

                            Instances For