TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.BinaryInterchange.Descriptor.Backends

Certified execution backends for binary descriptors #

Descriptor planning uses width-generic, native-word, and fixed-limb kernels with refinement theorems. Backend choice is separate: Descriptor.Plan constructs the candidate set and the universal selector makes that decision.

Width-generic kernels #

source
@[inline]
def FloatLib.Floats.Formats.BinaryInterchange.Descriptor.Backend.genericAdd {format : FloatFormat} (left right : ExecFloat (Descriptor format)) :
ExecFloat (Descriptor format)

Width-generic proved addition.

Instances For
    source
    @[inline]
    def FloatLib.Floats.Formats.BinaryInterchange.Descriptor.Backend.genericSub {format : FloatFormat} (left right : ExecFloat (Descriptor format)) :
    ExecFloat (Descriptor format)

    Width-generic proved subtraction.

    Instances For
      source
      @[inline]
      def FloatLib.Floats.Formats.BinaryInterchange.Descriptor.Backend.genericMul {format : FloatFormat} (left right : ExecFloat (Descriptor format)) :
      ExecFloat (Descriptor format)

      Width-generic proved multiplication.

      Instances For
        source
        @[inline]
        def FloatLib.Floats.Formats.BinaryInterchange.Descriptor.Backend.genericDiv {format : FloatFormat} (left right : ExecFloat (Descriptor format)) :
        ExecFloat (Descriptor format)

        Width-generic proved division.

        Instances For
          source
          @[inline]
          def FloatLib.Floats.Formats.BinaryInterchange.Descriptor.Backend.genericSqrt {format : FloatFormat} (value : ExecFloat (Descriptor format)) :
          ExecFloat (Descriptor format)

          Width-generic proved square root.

          Instances For
            source
            @[inline]
            def FloatLib.Floats.Formats.BinaryInterchange.Descriptor.Backend.genericFma {format : FloatFormat} (left right third : ExecFloat (Descriptor format)) :
            ExecFloat (Descriptor format)

            Width-generic proved fused multiply-add.

            Instances For
              source
              theorem FloatLib.Floats.Formats.BinaryInterchange.Descriptor.Backend.genericAdd_eq_spec {format : FloatFormat} (left right : ExecFloat (Descriptor format)) :
              genericAdd left right = Spec.add left right

              Width-generic addition agrees with the descriptor reference specification.

              source
              theorem FloatLib.Floats.Formats.BinaryInterchange.Descriptor.Backend.genericSub_eq_spec {format : FloatFormat} (left right : ExecFloat (Descriptor format)) :
              genericSub left right = Spec.sub left right

              Width-generic subtraction agrees with the descriptor reference specification.

              source
              theorem FloatLib.Floats.Formats.BinaryInterchange.Descriptor.Backend.genericMul_eq_spec {format : FloatFormat} (left right : ExecFloat (Descriptor format)) :
              genericMul left right = Spec.mul left right

              Width-generic multiplication agrees with the descriptor reference specification.

              source
              theorem FloatLib.Floats.Formats.BinaryInterchange.Descriptor.Backend.genericDiv_eq_spec {format : FloatFormat} (left right : ExecFloat (Descriptor format)) :
              genericDiv left right = Spec.div left right

              Width-generic division agrees with the descriptor reference specification.

              source
              theorem FloatLib.Floats.Formats.BinaryInterchange.Descriptor.Backend.genericSqrt_eq_spec {format : FloatFormat} (value : ExecFloat (Descriptor format)) :
              genericSqrt value = Spec.sqrt value

              Width-generic square root agrees with the descriptor reference specification.

              source
              theorem FloatLib.Floats.Formats.BinaryInterchange.Descriptor.Backend.genericFma_eq_spec {format : FloatFormat} (left right addend : ExecFloat (Descriptor format)) :
              genericFma left right addend = Spec.fma left right addend

              Width-generic fused multiply-add agrees with the descriptor reference specification.

              Fixed-format and native-word routes #

              source
              @[inline]
              def FloatLib.Floats.Formats.BinaryInterchange.Descriptor.Backend.wordAdd {format : FloatFormat} (left right : ExecFloat (Descriptor format)) :
              ExecFloat (Descriptor format)

              Proved fixed-format/native-word addition route.

              The candidate planner offers this route when the descriptor satisfies its eligibility predicate. For closed descriptors, the compiler can specialize the format tests.

              Instances For
                source
                @[inline]
                def FloatLib.Floats.Formats.BinaryInterchange.Descriptor.Backend.wordSub {format : FloatFormat} (left right : ExecFloat (Descriptor format)) :
                ExecFloat (Descriptor format)

                Proved fixed-format/native-word subtraction route.

                Instances For
                  source
                  @[inline]
                  def FloatLib.Floats.Formats.BinaryInterchange.Descriptor.Backend.wordMul {format : FloatFormat} (left right : ExecFloat (Descriptor format)) :
                  ExecFloat (Descriptor format)

                  Proved fixed-format/native-word/fixed-limb multiplication route.

                  Instances For
                    source
                    @[inline]
                    def FloatLib.Floats.Formats.BinaryInterchange.Descriptor.Backend.wordDiv {format : FloatFormat} (left right : ExecFloat (Descriptor format)) :
                    ExecFloat (Descriptor format)

                    Proved fixed-format/native-word/fixed-limb division route.

                    Instances For
                      source
                      @[inline]
                      def FloatLib.Floats.Formats.BinaryInterchange.Descriptor.Backend.wordSqrt {format : FloatFormat} (value : ExecFloat (Descriptor format)) :
                      ExecFloat (Descriptor format)

                      Proved fixed-format/native-word square-root route.

                      Instances For
                        source
                        @[inline]
                        def FloatLib.Floats.Formats.BinaryInterchange.Descriptor.Backend.wordFma {format : FloatFormat} (left right third : ExecFloat (Descriptor format)) :
                        ExecFloat (Descriptor format)

                        Proved fixed-format/native-word fused multiply-add route.

                        Instances For
                          source
                          @[inline]
                          def FloatLib.Floats.Formats.BinaryInterchange.Descriptor.Backend.fixedLimbSqrt {format : FloatFormat} (value : ExecFloat (Descriptor format)) :
                          ExecFloat (Descriptor format)

                          Square-root dispatcher, including eligible fixed-limb kernels.

                          Instances For
                            source
                            @[inline]
                            def FloatLib.Floats.Formats.BinaryInterchange.Descriptor.Backend.fixedLimbFma {format : FloatFormat} (left right third : ExecFloat (Descriptor format)) :
                            ExecFloat (Descriptor format)

                            Fused multiply-add dispatcher, including eligible fixed-limb kernels.

                            Instances For
                              source
                              theorem FloatLib.Floats.Formats.BinaryInterchange.Descriptor.Backend.wordAdd_eq_spec {format : FloatFormat} (left right : ExecFloat (Descriptor format)) :
                              wordAdd left right = Spec.add left right

                              Native-word addition agrees with the descriptor reference specification.

                              source
                              theorem FloatLib.Floats.Formats.BinaryInterchange.Descriptor.Backend.wordSub_eq_spec {format : FloatFormat} (left right : ExecFloat (Descriptor format)) :
                              wordSub left right = Spec.sub left right

                              Native-word subtraction agrees with the descriptor reference specification.

                              source
                              theorem FloatLib.Floats.Formats.BinaryInterchange.Descriptor.Backend.wordMul_eq_spec {format : FloatFormat} (left right : ExecFloat (Descriptor format)) :
                              wordMul left right = Spec.mul left right

                              Native-word or fixed-limb multiplication agrees with the descriptor reference specification.

                              source
                              theorem FloatLib.Floats.Formats.BinaryInterchange.Descriptor.Backend.wordDiv_eq_spec {format : FloatFormat} (left right : ExecFloat (Descriptor format)) :
                              wordDiv left right = Spec.div left right

                              Native-word or fixed-limb division agrees with the descriptor reference specification.

                              source
                              theorem FloatLib.Floats.Formats.BinaryInterchange.Descriptor.Backend.wordSqrt_eq_spec {format : FloatFormat} (value : ExecFloat (Descriptor format)) :
                              wordSqrt value = Spec.sqrt value

                              Native-word square root agrees with the descriptor reference specification.

                              source
                              theorem FloatLib.Floats.Formats.BinaryInterchange.Descriptor.Backend.wordFma_eq_spec {format : FloatFormat} (left right addend : ExecFloat (Descriptor format)) :
                              wordFma left right addend = Spec.fma left right addend

                              Native-word fused multiply-add agrees with the descriptor reference specification.

                              source
                              theorem FloatLib.Floats.Formats.BinaryInterchange.Descriptor.Backend.fixedLimbSqrt_eq_spec {format : FloatFormat} (value : ExecFloat (Descriptor format)) :
                              fixedLimbSqrt value = Spec.sqrt value

                              The square-root dispatcher agrees with the reference specification.

                              source
                              theorem FloatLib.Floats.Formats.BinaryInterchange.Descriptor.Backend.fixedLimbFma_eq_spec {format : FloatFormat} (left right addend : ExecFloat (Descriptor format)) :
                              fixedLimbFma left right addend = Spec.fma left right addend

                              The fused multiply-add dispatcher agrees with the reference specification.