Executable floating-point powers

Model.pow provides one deterministic power policy for every FloatFormat. For an IEEE descriptor, a finite nonzero base and a finite integral exponent give a correctly rounded result whenever that result is finite: its decoded value is nearest-even rounding of the exact power, as for Model.powInt. Small exact powers are computed by powInt itself. Larger ones use directed enclosures of |x|^n built by binary exponentiation at a working precision derived from the format. Repeated squaring stops once the enclosure lies beyond the overflow threshold or below half the least subnormal, so the exponent is never expanded into an integer when the answer is already an overflow or a zero. An enclosure whose endpoints round to different values is refined at a higher precision, and exact evaluation is the last resort.

Integer exponents are classified from their dyadic representation. The classifier records sign, parity, and an optional bounded magnitude without constructing an integer whose bit length is controlled by the floating-point exponent field, which formats with wide exponent fields need.

A finite positive base with any other finite exponent uses Transcendentals.Certified.pow, which refines proved enclosures of exp (y * log x) until both endpoints round to the same finite value, so an accepted result is nearest-even rounding of the real power. A certified range failure delivers positive overflow directly. Other failures (an exact result on a rounding boundary, an exhausted budget, or a descriptor other than IEEE) fall back to the approximate composition of the generic exp, mul and log kernels. Operations.PowerProof proves both correctly rounded finite cases under the IEEE and finiteness hypotheses above.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Power.smallPowLimit : ℕ

Largest integer magnitude that classifyInteger? records in smallMagnitude?.

structure FloatLib.Floats.Formats.BinaryInterchange.Model.Power.IntegerExponent : Type

Information needed to evaluate a finite integral floating-point exponent.

smallMagnitude? is populated exactly when the magnitude is at most smallPowLimit.

• negative : Bool

  Whether the nonzero integer is negative.

• odd : Bool

  Whether its magnitude is odd.

• smallMagnitude? : Option ℕ

  Its magnitude when small enough for direct evaluation.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Power.instReprIntegerExponent.repr : IntegerExponent → ℕ → Std.Format

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.Model.Power.instReprIntegerExponent : Repr IntegerExponent

def FloatLib.Floats.Formats.BinaryInterchange.Model.Power.instDecidableEqIntegerExponent.decEq (x✝ x✝¹ : IntegerExponent) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.Model.Power.instDecidableEqIntegerExponent : DecidableEq IntegerExponent

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.Power.smallMagnitude (magnitude : ℕ) : Option ℕ

Return a magnitude when it is within the direct evaluation limit.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Power.classifyIntegerDyadic? (value : Numerics.Dyadic) : Option IntegerExponent

Classify a finite dyadic as an integer.

For a nonnegative dyadic exponent, the left shift is bounded by log₂ smallPowLimit, and the shifted magnitude is then checked against the limit. For a negative exponent, divisibility is checked only when the right shift is no greater than the significand's leading bit index.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.Power.classifyInteger? {fmt : FloatFormat} (value : Model fmt) : Option IntegerExponent

Classify an executable finite value as an integer exponent.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Power.powNatLinear {fmt : FloatFormat} (base : Model fmt) : ℕ → Model fmt

Repeated rounded multiplication with recurrence p₀ = 1, pₙ₊₁ = base * pₙ.

Each step rounds, so this is not the correctly rounded power. pow uses integerPower?.

Correctly rounded integral exponents

structure FloatLib.Floats.Formats.BinaryInterchange.Model.Power.Endpoint : Type

A nonnegative dyadic mantissa * 2^exponent, used as one endpoint of a power enclosure.

Only the mantissa and the exponent are stored, so the value is never materialized as a rational while its exponent may be far outside the destination range.

• mantissa : ℕ

  Natural significand.

• exponent : ℤ

  Power-of-two scale.

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.Model.Power.instReprEndpoint : Repr Endpoint

def FloatLib.Floats.Formats.BinaryInterchange.Model.Power.instReprEndpoint.repr : Endpoint → ℕ → Std.Format

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.Model.Power.instDecidableEqEndpoint : DecidableEq Endpoint

def FloatLib.Floats.Formats.BinaryInterchange.Model.Power.instDecidableEqEndpoint.decEq (x✝ x✝¹ : Endpoint) : Decidable (x✝ = x✝¹)

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.Power.Endpoint.toRat (x : Endpoint) : ℚ

Exact rational value of an endpoint.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.Power.Endpoint.one : Endpoint

The endpoint with value one.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.Power.Endpoint.mul (x y : Endpoint) : Endpoint

Exact product of two endpoints.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.Power.Endpoint.excess (precision : ℕ) (x : Endpoint) : ℕ

Number of low mantissa bits above a budget of precision significant bits.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.Power.Endpoint.truncDown (precision : ℕ) (x : Endpoint) : Endpoint

Truncate toward zero to at most precision significant bits.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.Power.Endpoint.truncUp (precision : ℕ) (x : Endpoint) : Endpoint

Truncate away from zero to at most precision significant bits, plus a possible carry.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.Power.Endpoint.geTwoPow (x : Endpoint) (bound : ℤ) : Bool

A sufficient test for 2^bound ≤ x, read from the leading bit.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.Power.Endpoint.leTwoPow (x : Endpoint) (bound : ℤ) : Bool

A sufficient test for x ≤ 2^bound, read from the leading bit.

@[irreducible]

def FloatLib.Floats.Formats.BinaryInterchange.Model.Power.powBounds (precision : ℕ) (base : Endpoint) (exponent : ℕ) : Endpoint × Endpoint

Directed enclosure of base ^ exponent by binary exponentiation.

The first component is rounded down and the second up at every product, each to at most precision significant bits.

inductive FloatLib.Floats.Formats.BinaryInterchange.Model.Power.Screen : Type

Result of repeated squaring of an enclosure against the destination range.

• above : Screen

  The exact power is at least 2 ^ above.

• below : Screen

  The exact power is at most 2 ^ below.

• bounds (lower upper : Endpoint) : Screen

  The exact power lies between the two endpoints.

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.Model.Power.instReprScreen : Repr Screen

def FloatLib.Floats.Formats.BinaryInterchange.Model.Power.instReprScreen.repr : Screen → ℕ → Std.Format

def FloatLib.Floats.Formats.BinaryInterchange.Model.Power.instDecidableEqScreen.decEq (x✝ x✝¹ : Screen) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.Model.Power.instDecidableEqScreen : DecidableEq Screen

def FloatLib.Floats.Formats.BinaryInterchange.Model.Power.squareScreen (precision : ℕ) (above below : ℤ) : ℕ → Endpoint → Endpoint → Screen

Square an enclosure remaining times, stopping early once it lies beyond 2 ^ above (with above ≥ 0) or below 2 ^ below (with below ≤ 0). Both regions are closed under squaring, so an early stop also decides every further squaring.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.Power.roundEnclosure? (fmt : FloatFormat) (lower upper : ℚ) : Option (Model fmt)

Accept a signed rational enclosure [lower, upper] when both endpoints round to the same finite value.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.Power.workingPrecisions (fmt : FloatFormat) : List ℕ

Working precisions tried in turn: a first guess from the format, then three doublings.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Power.attempt (fmt : FloatFormat) (precision : ℕ) (negative reciprocal : Bool) (base : Endpoint) (magnitude shift : ℕ) : Option (Model fmt)

One enclosure attempt for (base ^ (magnitude * 2^shift)) ^ (±1) at a fixed precision.

reciprocal selects the negative exponent and negative the sign of the result. Screening returns an overflow or a signed zero. Otherwise both enclosure endpoints must round to the same finite value. For an IEEE descriptor, every finite result is nearest-even rounding of the exact target. Every other outcome is none.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.Power.integralValue (negative : Bool) (magnitude shift : ℕ) : ℤ

The integer (-1)^negative * magnitude * 2^shift, materialized only for powInt.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Power.exactBitBudget : ℕ

Exact results are computed through powInt while their exact size is below this bit count.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Power.integralParts? (value : Numerics.Dyadic) : Option (ℕ × ℕ)

Decompose an integral dyadic as ±magnitude * 2^shift, returning none for a non-integer. The sign is the dyadic's sign field.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Power.integerPowerWith {fmt : FloatFormat} (exactBudget : ℕ) (base : Model fmt) (b : Numerics.Dyadic) (negativeExponent : Bool) (magnitude shift : ℕ) : Model fmt

Integer power of a finite nonzero base with dyadic representation b, for the integer (-1)^negativeExponent * magnitude * 2^shift. For an IEEE descriptor, a finite result is correctly rounded.

Small exact results use powInt. A base of magnitude one gives a signed one. Otherwise directed enclosures are refined through workingPrecisions, and if none decides the result, powInt computes it exactly. exactBudget bounds the exact work in the first case.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Power.integerPower? {fmt : FloatFormat} (base exponent : Model fmt) : Option (Model fmt)

Power of a finite base by a finite integral exponent, or none when either input is nonfinite or the exponent is not an integer. For an IEEE descriptor and a nonzero base, a finite result is nearest-even rounding of the exact real power.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Power.certifiedOptions : Transcendentals.Certified.Options

Refinement budget of the certified search in pow: eight refinement attempts after the overflow and underflow screens. When the argument grid limits the width, the schedule doubles the working precision every second attempt and ends near eight times the first precision. An exact result on a rounding boundary generally does not settle, and the budget bounds the time spent before the fallback.

def FloatLib.Floats.Formats.BinaryInterchange.Model.pow {fmt : FloatFormat} (base exponent : Model fmt) : Model fmt

Deterministic executable floating-point exponentiation.

The special cases, in branch order:

• x^(+-0) = 1, including a quiet-NaN base; a signaling-NaN base is quieted (IEEE 754-2019 §9.2.1 and §6.2);
• 1^y = 1 except for a signaling-NaN exponent;
• infinite exponents are classified by |x| relative to one;
• signed zero and infinite bases give a zero or an overflow, negative exactly for a negative base and an odd integer exponent;
• a finite nonzero base with a finite integral exponent uses Power.integerPower?; for an IEEE descriptor, a finite result is correctly rounded;
• otherwise a finite negative base is invalid, and a positive one uses the certified enclosure search Transcendentals.Certified.pow, whose accepted results are correctly rounded, with positive overflow for a certified range failure and exp (y * log x) as the fallback for other failures.