TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.ExecFloat.Spec.Arithmetic

Reference arithmetic for ExecFloat #

Names for the six reference operations supplied by arithmetic capabilities. Use them with the refinement equations in ExecFloat.Proof to reason about an executable arithmetic expression.

Each reference operation is the spec field of the format's Capability, and Capability is indexed by the planning policy [Backend.PolicyFor F] because the same class also stores the selected implementation. Each refinement theorem refers to the specification in the current instance. Policy independence across distinct instances requires them to supply the same specification; the capability class imposes no separate law relating those instances. The default PolicyFor instance is normally inferred at use sites.

source
def FloatLib.Floats.ExecFloat.Spec.add {F : Type u} [Backend.PolicyFor F] [Numerics.EncodedFormat F] [Add F] (left right : ExecFloat F) :
ExecFloat F

Reference definition of addition for this format.

Proofs use this definition to state the required result. Numerical code should normally call ExecFloat.add or use +.

Instances For
    source
    def FloatLib.Floats.ExecFloat.Spec.sub {F : Type u} [Backend.PolicyFor F] [Numerics.EncodedFormat F] [Sub F] (left right : ExecFloat F) :
    ExecFloat F

    Reference definition of subtraction for this format.

    Proofs use this definition to state the required result. Numerical code should normally call ExecFloat.sub or use -.

    Instances For
      source
      def FloatLib.Floats.ExecFloat.Spec.mul {F : Type u} [Backend.PolicyFor F] [Numerics.EncodedFormat F] [Mul F] (left right : ExecFloat F) :
      ExecFloat F

      Reference definition of multiplication for this format.

      Proofs use this definition to state the required result. Numerical code should normally call ExecFloat.mul or use *.

      Instances For
        source
        def FloatLib.Floats.ExecFloat.Spec.div {F : Type u} [Backend.PolicyFor F] [Numerics.EncodedFormat F] [Div F] (left right : ExecFloat F) :
        ExecFloat F

        Reference definition of division for this format.

        Proofs use this definition to state the required result. Numerical code should normally call ExecFloat.div or use /.

        Instances For
          source
          def FloatLib.Floats.ExecFloat.Spec.sqrt {F : Type u} [Backend.PolicyFor F] [Numerics.EncodedFormat F] [Sqrt F] (value : ExecFloat F) :
          ExecFloat F

          Reference definition of square root for this format.

          Proofs use this definition to state the required result. Numerical code should normally call ExecFloat.sqrt or use .sqrt.

          Instances For
            source
            def FloatLib.Floats.ExecFloat.Spec.fma {F : Type u} [Backend.PolicyFor F] [Numerics.EncodedFormat F] [Fma F] (left right addend : ExecFloat F) :
            ExecFloat F

            Reference definition of fused multiply-add for this format.

            Proofs use this definition to state the result required by the installed capability. Numerical code should normally call ExecFloat.fma.

            Instances For