TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.P3109.Arithmetic.Instances

Public P3109 arithmetic capabilities #

Every valid P3109 descriptor supplies addition, subtraction, multiplication, division, square root, and fused multiply-add through common ExecFloat dispatch. Each has one exact arithmetic kernel followed by the report projection. The supplied backend planning policy is retained.

Context-free operations use FloatLib's nearest-even, no-saturation projection policy. Explicit rounding, stochastic random words, saturation, and mixed-format destinations remain available through ExecFloat.P3109.*To. These operations neither raise nor synthesize IEEE exception flags.

The rational real-embedding and decoding proofs are in Arithmetic.Proof; the irrational-root refinement and decoding proofs are in Arithmetic.Sqrt.Proof.

source
def FloatLib.Floats.ExecFloat.P3109.Plan.estimate (format : Formats.P3109.Format) (operation : Backend.Operation) :
Backend.Candidate

Planner metadata for the exact arithmetic implementation.

The storage class describes the encoded operand, not an intermediate-size bound. Exact rational arithmetic can allocate integers whose sizes depend on the descriptor's exponent range.

Instances For
    source
    @[instance_reducible, always_inline]
    def FloatLib.Floats.ExecFloat.P3109.Plan.capability {format : Formats.P3109.Format} [Backend.PolicyFor (Codebook.Family format.codebook)] (operation : Backend.Operation) (kernel : OperationSignature (Codebook.Family format.codebook) operation) :
    Capability (Codebook.Family format.codebook) operation

    Package the single exact kernel without changing the caller's planning policy.

    Instances For
      source
      @[instance_reducible]
      instance FloatLib.Floats.ExecFloat.P3109.negInstance {format : Formats.P3109.Format} :
      Neg (P3109 format)

      Report-default negation, including projection of unsigned results.

      source
      @[instance_reducible, always_inline]
      instance FloatLib.Floats.ExecFloat.P3109.addCapability {format : Formats.P3109.Format} [Backend.PolicyFor (Codebook.Family format.codebook)] :
      Add (Codebook.Family format.codebook)

      Exact addition with one nearest-even report projection.

      source
      @[instance_reducible, always_inline]
      instance FloatLib.Floats.ExecFloat.P3109.subCapability {format : Formats.P3109.Format} [Backend.PolicyFor (Codebook.Family format.codebook)] :
      Sub (Codebook.Family format.codebook)

      Exact subtraction with one nearest-even report projection.

      source
      @[instance_reducible, always_inline]
      instance FloatLib.Floats.ExecFloat.P3109.mulCapability {format : Formats.P3109.Format} [Backend.PolicyFor (Codebook.Family format.codebook)] :
      Mul (Codebook.Family format.codebook)

      Exact multiplication with one nearest-even report projection.

      source
      @[instance_reducible, always_inline]
      instance FloatLib.Floats.ExecFloat.P3109.divCapability {format : Formats.P3109.Format} [Backend.PolicyFor (Codebook.Family format.codebook)] :
      Div (Codebook.Family format.codebook)

      Exact division with the report's NaN result for every zero denominator.

      source
      @[instance_reducible, always_inline]
      instance FloatLib.Floats.ExecFloat.P3109.sqrtCapability {format : Formats.P3109.Format} [Backend.PolicyFor (Codebook.Family format.codebook)] :
      Sqrt (Codebook.Family format.codebook)

      Square root rounded by exact comparisons with the irrational result.

      source
      @[instance_reducible, always_inline]
      instance FloatLib.Floats.ExecFloat.P3109.fmaCapability {format : Formats.P3109.Format} [Backend.PolicyFor (Codebook.Family format.codebook)] :
      Fma (Codebook.Family format.codebook)

      Fused multiply-add with no rounded or saturated intermediate product.