Configuration for format-generic transcendental execution

IEEE 754 §9.2 recommends elementary operations with a correct-rounding contract; it does not require them in every implementation or prescribe their algorithms. These kernels provide deterministic approximations. Config records their integer approximation data, while accuracy and correct rounding require separate proofs. The binary32 configuration is pinned explicitly for reproducible results. Other formats use a generated configuration controlled by an explicit GenerationPolicy.

The default policy bounds the exponent range accepted by trigonometric reduction. The checked trigonometric entry points report inputs beyond this budget as failures; the value-only entry points return the format's invalid result. This prevents a wide exponent field from silently constructing constants with hundreds of thousands or billions of bits. generatedFullRange remains available as an explicit expensive choice.

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

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

Resource policy for generated transcendental approximation data.

trigExponentBudget bounds the destination exponent contribution to the fixed-point scale used for trigonometric reduction. Reduction rejects arguments beyond that budget instead of using an insufficiently precise approximation to pi / 2.

• guardBits : ℕ

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

• trigExponentBudget : ℕ

  Cap on the exponent-range contribution to trigonometric working precision.

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, also reserved after trigonometric reduction. log increases it near one.

• ln2Fixed : ℤ

  Fixed-point approximation to log 2.

• 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 and tanh; entry i is sinhDenominator / (2i+1)!.

• sinhDenominator : ℕ

  Positive common denominator for sinhCoeffsAsc.

• trigFixed : FixedPoint

  Working scale used for trigonometric argument reduction.

• halfPiFixed : ℤ

  Fixed-point approximation to pi / 2 at scale trigFixed.

• sinCoeffsAsc : List ℤ

  Ascending exact numerator coefficients for the reduced sine polynomial.

• sinDenominator : ℕ

  Positive common denominator for sinCoeffsAsc.

• cosCoeffsAsc : List ℤ

  Ascending exact numerator coefficients for the reduced cosine polynomial.

• cosDenominator : ℕ

  Positive common denominator for cosCoeffsAsc.

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

@[instance_reducible]

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

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

@[instance_reducible]

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

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Config.trigMaxExponent (config : Config) : ℤ

Largest leading input exponent accepted by trigonometric reduction.

Reserving fixed bits after reduction leaves trigFixed - fixed bits for the argument's exponent. For generated configurations this is exactly the capped exponent contribution. This resource check is not an accuracy certificate for the constants or polynomials.

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.oddReciprocalSeries (fixed : FixedPoint) (q terms : ℕ) (alternating : Bool) : ℤ

Approximate the first terms terms of the odd reciprocal series

sum_k sign(k) / ((2k+1) * q^(2k+1))

at the supplied fixed-point scale, with q > 1. The infinite series is atanh (1/q) when alternating = false and atan (1/q) when alternating = true. Each division rounds to the working scale.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Config.generateLn2FixedWith (guardBits scale : ℕ) : ℤ

Approximate log 2 * 2^scale using log 2 = 2 * atanh (1/3) and an explicit guard budget. The truncated fixed-point series is rounded back to the requested scale.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Config.generateLn2Fixed (scale : ℕ) : ℤ

Approximate log 2 * 2^scale with the default guard budget.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Config.generateHalfPiFixedWith (guardBits scale : ℕ) : ℤ

Approximate (pi/2) * 2^scale with Machin's formula pi/2 = 8 * atan (1/5) - 2 * atan (1/239) and an explicit guard budget.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Config.generateHalfPiFixed (scale : ℕ) : ℤ

Approximate (pi/2) * 2^scale with the default guard budget.

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.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 + 4). This condition comes from the usual Taylor-tail estimate for |x| ≤ 1/2, and 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 yet 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.generatedTrigScale (policy : GenerationPolicy) (fmt : FloatFormat) : ℕ

Fixed-point scale used for trigonometric reduction under policy.

The fraction width and guard bits contribute in full; the exponent-range contribution is capped.

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

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

The bounded trigonometric scale keeps ordinary generation practical for formats with wide exponent fields. This is a deterministic approximation policy and does not imply a proved error bound.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Config.trigMaxExponent_generatedWith (policy : GenerationPolicy) (fmt : FloatFormat) : (generatedWith policy fmt).trigMaxExponent = Int.ofNat (fmt.maxNormalExponent.toNat.min policy.trigExponentBudget)

Generated reduction data accepts exactly its declared exponent contribution.

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

Generate a configuration with the default bounded resource policy.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Config.generatedFullRangeWith (guardBits : ℕ) (fmt : FloatFormat) : Config

Generate a full-range configuration with a caller-selected guard budget.

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

Generate an unbounded full-exponent-range configuration.

For formats with wide exponent fields this can allocate extremely large integers. Callers should normally prefer generated.

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

Default configuration for a format.

Binary32 selects its pinned table; every other layout receives bounded generated data. Callers that need a different speed/accuracy point can use generatedWith, generatedFullRange, or construct and reuse an explicit Config.