mixle.engines.error_tracing module

Sound error tracing via interval arithmetic.

An Interval carries [lo, hi] enclosing a true value. Every operation rounds the bounds outward (one ULP via numpy.nextafter()), so the enclosure provably contains the exact result despite float64 round-off – the interval certifies the numerical error rather than hoping it is small. The width is a guaranteed error bound; a precision-allocation pass reads it to pick the lowest-cost format that keeps the width under a target (pair with mixle.engines.formats.min_float_mantissa_bits()).

Interval arithmetic is sound but pessimistic because it ignores correlations between operands. Affine arithmetic can tighten the bound when that extra complexity is justified. This module provides the vectorized, dependency-free core.

Soundness invariants, enforced at construction (Interval.__init__()): endpoints are never NaN (a NaN bound cannot certify anything) and lo <= hi always holds (+/-inf endpoints are legal – [-inf, inf] and degenerate points like [inf, inf] both pass – only NaN and reversed order are rejected). Every operation is written to either produce a result that satisfies those invariants or to raise, rather than let IEEE-754’s indeterminate forms (0 * inf, inf - inf) leak a NaN bound out as if it were a valid enclosure. See _ivl_mul() for the 0 * inf = 0 extended-real rule multiplication relies on.

class Interval(lo, hi)

Bases: object

A guaranteed enclosure [lo, hi] of a value (scalar or numpy array), outward-rounded.

Parameters:

• lo (Any)

• hi (Any)

classmethod exact(x)

A degenerate interval [x, x] for an exactly-represented value.

Parameters:

x (Any)

Return type:

Interval

classmethod from_quantized(original, fmt)

Enclose original using the quantized format’s error bound.

max_rel_error is a duck-typed, self-reported claim: nothing here enforces that an implementer’s static bound actually holds for every value fmt might quantize, only that it is offered as one. A format that flushes underflowing values to exactly zero, or saturates on overflow, would still report a fixed max_rel_error while its true error at those magnitudes no longer scales with it – the analytic pad below would then be too narrow, silently returning an interval that does not actually enclose original ( FloatFormat avoids this today by staying mantissa-only with an unbounded exponent, so its max_rel_error genuinely is universal – see that class’s docstring – but nothing here depends on every format that will ever be passed in honoring that same discipline). Guard against a format that breaks the assumption by cross-checking the analytic pad against the error actually measured on original – already in hand, it is quantized right here – and padding by whichever is WIDER. This needs nothing new from fmt beyond round_trip, which every caller already requires, and is a no-op whenever max_rel_error genuinely does bound this data (the analytic pad is then always >= the measured one, by construction).

Parameters:

• original (Any)

• fmt (Any)

Return type:

Interval

width()

The guaranteed error bound: hi - lo (outward-rounded).

A degenerate point exactly at +/-inf (lo == hi == +/-inf, legal per the constructor) has zero width by definition – but IEEE-754 computes inf - inf == NaN for it, which would otherwise leak a NaN out of this function with no constructor downstream to catch it. Special-case that one pattern directly; every other case (including an ordinary, non- degenerate unbounded interval like [0, inf], whose width is correctly inf) is unaffected.

Return type:

ndarray

max_width()

Return the largest interval width.

Return type:

float

midpoint()

Return interval midpoints.

Same inf - inf gap as width(): a degenerate point at +/-inf is its own midpoint by definition, computed directly rather than via the subtraction that would otherwise produce NaN.

Return type:

ndarray

contains(value)

Return a boolean mask for values inside the interval.

Parameters:

value (Any)

Return type:

ndarray

sum_error_bound(x)

Return a certified bound on the float64 error of sum(x).

The standard a-priori bound |fl(sum) - sum| <= gamma_{n-1} * sum|x_i| with gamma_k = k*u / (1 - k*u) and u = 2**-53. It is sound for any summation order. A bound that is large relative to |sum x| means the sum is ill-conditioned (cancellation) and warrants the double-double mixle.engines.extended.dd_sum(); a tight one means float64 already suffices and no extra compute is justified.

Parameters:

x (Any)

Return type:

float

sum_enclosure(x)

Return an outward-rounded interval enclosing the true sum(x).

Parameters:

x (Any)

Return type:

Interval

float64_sum_is_accurate(x, target_rel_error=1e-12)

Return whether float64 summation is accurate to target_rel_error.

Reads the certified bound relative to the magnitude of the result – precision allocation in one call.

Parameters:

• x (Any)

• target_rel_error (float)

Return type:

bool