Configuration for format-generic transcendental execution

IEEE 754 §9.2 recommends elementary operations with a correct-rounding contract, but it does not require them in every implementation or prescribe their algorithms. These kernels provide deterministic approximations. Config records their integer approximation data, and accuracy and correct rounding need their own proofs. The binary32 configuration is pinned for reproducible results, and other formats use a configuration generated under a GenerationPolicy.

Generated configurations depend on the fraction width only, never on the exponent range: trigonometric reduction and the reduction of large exponential arguments take their extra precision from the shared constants cache of Numerics.Enclosure.Constants at the size each argument needs. The generated log 2 is its ln2Faithful read, proved within one unit.

Generated data is an execution policy, not an accuracy theorem. Real-error claims are separate approximation contracts.

structure FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.GenerationPolicy : Type

Resource policy for generated transcendental approximation data.

• guardBits : ℕ

  Extra fixed-point precision used for generated constants and working arithmetic.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.instReprGenerationPolicy.repr : GenerationPolicy → ℕ → Std.Format

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.instReprGenerationPolicy : Repr GenerationPolicy

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.instDecidableEqGenerationPolicy.decEq (x✝ x✝¹ : GenerationPolicy) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.instDecidableEqGenerationPolicy : DecidableEq GenerationPolicy

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.GenerationPolicy.standard : GenerationPolicy

Default bounded generation policy.

structure FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Config : Type

Integer approximation data consumed by the transcendental kernels.

The fields store coefficients and scales without proofs of their accuracy or validity. binary32 and generatedWith supply the Taylor coefficients and positive denominators described below. Callers constructing their own configurations must establish the properties they need.

• fixed : FixedPoint

  Base working scale for exp and log, which log increases near one.

• ln2Fixed : ℤ

  Fixed-point approximation to log 2 at scale fixed.

• invLn2Fixed : ℤ

  Fixed-point approximation to 1 / log 2.

• exp2PolyCoeffsDesc : List ℤ

  Descending fixed-point coefficients for the reduced 2 ^ x polynomial.

• logTerms : ℕ

  Number of odd atanh-series terms used by log.

• sinhCoeffsAsc : List ℤ

  Ascending exact numerator coefficients of the odd Taylor polynomial in x ^ 2 shared by the small-argument branches of sinh, cosh and tanh. Entry i is sinhDenominator / (2i+1)!.

• sinhDenominator : ℕ

  Positive common denominator for sinhCoeffsAsc.

• sinCoeffsAsc : List ℤ

  Ascending exact numerator coefficients of the alternating Taylor series of sine in x ^ 2; entry i is (-1)^i * sinDenominator / (2i+1)!. The kernel evaluates a prefix of the list whose length it chooses from the argument, and the whole list for tiny arguments.

• sinDenominator : ℕ

  Positive common denominator for sinCoeffsAsc.

• cosCoeffsAsc : List ℤ

  Ascending exact numerator coefficients of the alternating Taylor series of cosine in x ^ 2; entry i is (-1)^i * cosDenominator / (2i)!. The kernel evaluates a prefix of the list whose length it chooses from the argument.

• cosDenominator : ℕ

  Positive common denominator for cosCoeffsAsc.

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.instReprConfig : Repr Config

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.instReprConfig.repr : Config → ℕ → Std.Format

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.instDecidableEqConfig : DecidableEq Config

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.instDecidableEqConfig.decEq (x✝ x✝¹ : Config) : Decidable (x✝ = x✝¹)

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Config.factorial : ℕ → ℕ

Factorial used to construct exact common-denominator Taylor polynomials.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Config.generateExp2CoeffsDesc (fixed : FixedPoint) (ln2Fixed : ℤ) (degree : ℕ) : List ℤ

Generate descending coefficients for a Taylor polynomial approximating 2 ^ x.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Config.sinTaylorData (terms : ℕ) : ℕ × List ℤ

Exact common-denominator coefficients for sum i in [0, max terms 1), (-1)^i x^(2i+1)/(2i+1)!.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Config.sinhTaylorData (terms : ℕ) : ℕ × List ℤ

Exact common-denominator coefficients for the odd series sum i in [0, max terms 1), x^(2i+1)/(2i+1)! of sinh. With n = max terms 1, the pair is ((2*n - 1)!, coefficients), with every coefficient positive.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Config.sinhTermsAux (target : ℕ) : ℕ → ℕ → ℕ

Search upward from count for the first term count whose truncation target is met. fuel bounds the search so the definition is structurally total.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Config.sinhGuardBits : ℕ

Bits kept beyond the destination fraction width by the small-argument sinh series.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Config.sinhTerms (fracWidth : ℕ) : ℕ

Number of odd Taylor terms of sinh selected for a fraction width.

The search targets the first n ≥ 1 with 2^(2n) * (2n+1)! ≥ 2^(fracWidth + sinhGuardBits), so for |x| ≤ 1/2 the first omitted term is below 2^-(fracWidth + sinhGuardBits + 1). The small-argument branches of sinh, cosh and tanh share this series, and a target only four bits beyond the fraction width misrounded binary128 results near one half. The linear fuel budget is chosen to exceed the point where the power-of-two factor alone reaches the target. The corresponding analytic error argument is not formalized as a theorem in this library.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Config.cosTaylorData (terms : ℕ) : ℕ × List ℤ

Exact common-denominator coefficients for sum i in [0, max terms 1), (-1)^i x^(2i)/(2i)!.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Config.binary32 : Config

Pinned binary32 configuration for stable, reproducible transcendental results.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Config.generatedWith (policy : GenerationPolicy) (fmt : FloatFormat) : Config

Generate a deterministic configuration sized for fmt under a resource policy.

Every field depends on the fraction width only. log 2 comes from the shared constants cache and is within one unit of its exact scaled value. The other fields are a deterministic approximation policy and carry no proved error bound.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Config.generated (fmt : FloatFormat) : Config

Generate a configuration with the default resource policy.

@[never_extract, noinline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Config.Internal.generate (fmt : FloatFormat) : Config

generated fmt, kept out of line and out of closed-term extraction so the cached catalog configurations below are generated on first use rather than at module initialization.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Config.Internal.generatedBinary16 : Thunk Config

Generated binary16 configuration, computed on first use and then reused.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Config.Internal.generatedBFloat16 : Thunk Config

Generated bfloat16 configuration, computed on first use and then reused.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Config.Internal.generatedBinary64 : Thunk Config

Generated binary64 configuration, computed on first use and then reused.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Config.Internal.generatedBinary128 : Thunk Config

Generated binary128 configuration, computed on first use and then reused.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Config.Internal.generatedBinary256 : Thunk Config

Generated binary256 configuration, computed on first use and then reused.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Config.forFormat (fmt : FloatFormat) : Config

Default configuration for a format.

Binary32 selects its pinned table. The other catalog binary formats reuse one generated configuration per program run, and every other layout generates its data on each call. The result equals generated fmt for every layout except binary32. Callers that need a different speed/accuracy point can use generatedWith, or build and reuse a Config.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Config.forFormat_eq (fmt : FloatFormat) : forFormat fmt = if fmt = FloatFormat.binary32 then binary32 else generated fmt

The cached catalog configurations are the generated ones.