Module expansion 

Floating-point expansions: exact values represented as sums of f64 components.

An expansion is a slice of f64 whose exact, unrounded sum is the value it represents. Every function here requires its expansion inputs to satisfy, and guarantees for its output, these invariants:

• no component is zero, so the value zero is the empty slice;
• components are sorted by strictly increasing magnitude;
• components are nonoverlapping: the highest set bit of each lies strictly below the lowest set bit of the next.

The components below the last one then add up to less than it in magnitude, so the last component has the sign of the value. Expansions built only with this module always satisfy the invariants.

Results are written to the start of a caller-provided buffer out, and the length written is returned. Each function documents its capacity, the longest result it can produce. Debug builds panic if out is shorter than the capacity; release builds panic only if the actual result does not fit. Nothing is ever written outside out, and nothing allocates.

The functions also require that:

• every input component and scalar operand has magnitude below 2^1020, which rules out overflow;
• operands of products (from_two_product and scale) lie in the product domain of eft::in_product_domain, which debug builds check;
• the floating-point rounding mode is the default round-to-nearest, which the correctness proofs depend on.

These magnitude bounds are not closed under chaining: the output of an operation whose inputs satisfy them can have components outside the product domain or close to overflow, so a computation that chains operations must bound the magnitudes it produces.

Gradual underflow is harmless: sums of floating-point values are exact whenever they are subnormal.

The algorithms are from Shewchuk, “Adaptive Precision Floating-Point Arithmetic and Fast Robust Geometric Predicates” (1997), all with zero elimination: grow is GROW-EXPANSION (Theorem 10), sum and diff are LINEAR-EXPANSION-SUM (Theorem 24) and scale is SCALE-EXPANSION (Theorem 19). For each one the paper proves that nonoverlapping inputs give a nonoverlapping output.

Functions

diff

Writes the expansion of e - f, reading f without copying or modifying it.

estimate

Returns a floating-point approximation of the value of the valid expansion e: its components added from smallest to largest. Use sign for the exact sign.

from_f64

Writes the expansion of a: empty if a is zero of either sign, [a] otherwise.

from_two_diff

Writes the expansion of the exact difference a - b.

from_two_product

Writes the expansion of the exact product a * b.

from_two_sum

Writes the expansion of the exact sum a + b.

grow

Writes the expansion of e + b.

negate

Negates the valid expansion e in place. Negation is exact and keeps the invariants.

scale

Writes the expansion of e * b.

sign

Returns the exact sign of the value of the valid expansion e (see the module documentation): the sign of its last component, which outweighs all the others together.

sum

Writes the expansion of e + f.