Binary64 implementation contracts

../binary64.tri owns the checked Word boundary and the application interface. The modules in this directory implement its private working values and arithmetic. See Binary64 arithmetic for supported usage and validation for executable checks.

Working value

A Value has the implementation shape (kind,(sign,(scale,payload))):

Kind	Meaning	Scale and payload
0	Signed zero	Both zero.
1	Nonzero finite	Scale 1178..3275; normalized 53-bit significand.
2	Signed infinity	Both zero.
3	NaN	Scale zero; nonzero 52-bit fraction containing its quiet bit.

The sign and all flags are canonical Booleans. Numeric fields are canonical LSB-first naturals. Finite magnitude is payload * 2^(scale-2304).

For scale <1230, the significand is divisible by 2^(1230-scale). These low padding zeros ensure that normalized subnormals remain exactly representable binary64 values. Arithmetic establishes this invariant after every operation.

fromBitsC checks a Word and returns its decoded Value through the contract Result. toBits packs a valid Value exactly. Arithmetic accepts Values produced by successful imports and preceding operations. Callers preserve this invariant when retaining or composing Values; Words provide the storage/interchange form.

Rounding

For an exact positive magnitude n * 2^(s-2304), the quantizer selects

cut = max(width(n)-53, 1230-s, 0)

It rounds once at that cut, shifts a 54-bit carry exactly, and normalizes a nonzero result to 53 significand bits. This combines the precision and minimum quantum requirements. Overflow yields the infinity kind.

Underflow requires inexactness and tininess after precision rounding with an unbounded exponent. Inexact stored subnormals and zero satisfy this condition. For a stored minimum-normal result, ieee.precisionTiny classifies the original magnitude at binary64 precision. That auxiliary result determines the flag; the combined-cut result supplies the value.

For example, minimum normal multiplied by the predecessor of one stores minimum normal and raises underflow plus inexact. At the exact tininess boundary 2^-1022 - 2^-1076, precision rounding reaches minimum normal and raises inexact.

Arithmetic kernels

Addition/subtraction order normalized magnitudes and align at the smaller scale. Gaps 0..7 use exact intermediates; gaps 8..54 use three additional bits and round-to-odd jamming. For a gap of at least 55, the dominant significand is the rounded result and inexact is true. Since the smaller scale is at least 1178, this branch has dominant scale at least 1233 and a normal result.

Multiplication forms the exact product with the ordered carry kernel, then quantizes it. Division produces 56 fractional quotient bits with an exact remainder and jams that remainder before final rounding. The jammed near/divide intermediates feed their immediate quantizer. Subsequent arithmetic receives the rounded binary64 Value.

NaN selection precedes subtraction's effective sign change. Both signaling predicates contribute to invalid. Each reply pairs a Value with five flags in invalid/divide-by-zero/overflow/underflow/inexact order. mergeFlags combines the flags componentwise.

Validation and demand

The Word validator observes low bits first, checking each bit before advancing to its tail. Each bit is exactly Leaf or Stem Leaf. Zero is Leaf; a positive canonical Word ends with a significant one bit.

A 64-digit budget bounds structural observations. At its limit, a preceding zero bit rejects immediately. A preceding one bit requires a Leaf tail. Malformed bit constructors and oversized Fork tails reject at their roots, leaving their children opaque. Validation returns the original Word or its decoded Value and preserves the supplied remainder.

Word operations validate left then right before arithmetic. A failed left check leaves the right argument opaque. Trusted arithmetic preserves selective demand: a left NaN can determine the value projection independently of the right value, while invalid can depend on signaling status from either operand.

These operations require each demanded tree observation to terminate. A bounded number of observations may still encounter a divergent computation producing one of those observations.

Source ownership and provenance

The library consists of the facade and eleven internal source modules. Their imports resolve within this directory and native_math. The preparation registry uses binary64 for the facade and binary64_NAME for each internal NAME.tri.

test/float-library-extraction.json records the initial declaration extraction: source hashes, selected definitions, exports and resulting library hashes. test/float_library_extract.py reproduces that extraction when invoked explicitly. The library files are maintained source. Run extraction in a disposable worktree and review its output before updating the maintained files. Token dependency scanning conservatively includes matching names, including names shadowed by local binders.