TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.Posit.Configured.Core

Configured posit semantic core #

Configured posit operations lift the exact model through the statically selected public carrier. These specifications are independent of optimized execution backends: clients that only need the configured type and its independent specification should not depend on planner or kernel implementation details.

Carrier packing is proved inverse to model decoding in Configured.Storage.Family.Proof. Consequently these definitions do not depend on whether a closed width selected UInt8, UInt16, UInt32, UInt64, two limbs, or the exact-width wide model.

source
@[noinline]
def FloatLib.Floats.Formats.Posit.Configured.Spec.add {format : Format} {plan : StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] (left right : ExecFloat (Family format code plan)) :
ExecFloat (Family format code plan)

Independent exact configured addition specification.

Instances For
    source
    @[noinline]
    def FloatLib.Floats.Formats.Posit.Configured.Spec.sub {format : Format} {plan : StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] (left right : ExecFloat (Family format code plan)) :
    ExecFloat (Family format code plan)

    Independent exact configured subtraction specification.

    Instances For
      source
      @[noinline]
      def FloatLib.Floats.Formats.Posit.Configured.Spec.mul {format : Format} {plan : StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] (left right : ExecFloat (Family format code plan)) :
      ExecFloat (Family format code plan)

      Independent exact configured multiplication specification.

      Instances For
        source
        @[noinline]
        def FloatLib.Floats.Formats.Posit.Configured.Spec.div {format : Format} {plan : StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] (left right : ExecFloat (Family format code plan)) :
        ExecFloat (Family format code plan)

        Independent exact configured division specification.

        Instances For
          source
          @[noinline]
          def FloatLib.Floats.Formats.Posit.Configured.Spec.sqrt {format : Format} {plan : StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] (value : ExecFloat (Family format code plan)) :
          ExecFloat (Family format code plan)

          Independent exact configured square-root specification.

          Instances For
            source
            @[noinline]
            def FloatLib.Floats.Formats.Posit.Configured.Spec.fma {format : Format} {plan : StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] (left right third : ExecFloat (Family format code plan)) :
            ExecFloat (Family format code plan)

            Independent exact configured fused-multiply-add specification.

            Instances For