# `bin_float` Conformance

This page records the `0.7.1` binary floating-point semantic and test
boundary. It is evidence for a stated, finite corpus; it is not a proof that
any implementation can be correct for every real input.

## Normative And Research Sources

- IEEE, *IEEE Standard for Floating-Point Arithmetic*, IEEE 754-2019:
  interchange formats, rounding-direction attributes, NaNs/infinities/signed
  zeros, exceptions, and tininess detection.
- S. Fousse, G. Hanrot, V. Lefèvre, P. Pélissier, and P. Zimmermann,
  [MPFR: A Multiple-Precision Binary Floating-Point Library with Correct Rounding](https://doi.org/10.1145/1236463.1236468),
  ACM TOMS 33(2), 2007. MPFR supplies the exact-result-then-one-rounding model
  used for arbitrary precisions.
- John Hauser's Berkeley [SoftFloat](https://www.jhauser.us/arithmetic/SoftFloat.html)
  and [TestFloat](https://www.jhauser.us/arithmetic/TestFloat.html), release
  3e, provide the independently generated IEEE result/flag vectors.

## Mathematical Model

A finite nonzero `BinFloat` denotes the dyadic real

`(-1)^negative * coefficient * 2^exponent2`, where `coefficient` is a
non-negative `BinCoeff`.

The finite coefficient is normalized by removing factors of two, while the
sign of zero remains observable. Infinity, qNaN, sNaN, NaN payload, and NaN
sign are explicit states rather than sentinel finite values.

For `add_ctx`, `sub_ctx`, `mul_ctx`, `div_ctx`, `sqrt_ctx`, and `pow_int_ctx`:

1. IEEE special cases are resolved before finite arithmetic.
2. Finite addition, subtraction, and multiplication use their exact dyadic
   result; division uses an exact integer quotient/remainder decision; square
   root brackets the exact real root with integer-square-root bounds.
3. The exact result is rounded once to the requested precision and rounding
   direction, then exponent-range/subnormal quantization is applied.
4. The returned `BinaryFlags` is derived from that mathematical result:
   inexact, underflow, overflow, division-by-zero, and invalid-operation.

This order matters. For example, binary16 `0x0400 * 0x3BFF` produces
`0x0400` with `inexact | underflow`; after-rounding tininess is determined from
the precision-rounded unbounded value, not merely from the final normal
interchange encoding.

No operation branches on test identifiers, test values, or corpus format.
The corpus interpreter is an adapter around the public contextual operations.

## Interchange And Context

`BinaryInterchange` decodes and encodes IEEE binary16, binary32, binary64, and
binary128 bit patterns. `BinaryContext` carries precision, rounding direction,
paired exponent limits, and before/after tininess detection. Encoding and
contextual arithmetic both return status flags; ordinary operators use an
unbounded nearest-even context and intentionally do not expose those flags.

NaN comparisons in the TestFloat adapter are class-based only when an expected
result is NaN. This is not a weakened finite-value comparison: non-NaN encoded
bits and all exception bits must match exactly. It reflects IEEE's permitted
choice of a newly generated NaN payload. The implementation itself preserves
the selected input NaN's sign/payload and quiets signaling NaNs.

## Declared Corpus And Results

The pinned full gate is documented in
[`testdata/bin_float/README.md`](../../../testdata/bin_float/README.md).

| Source | Scope | Result |
| --- | --- | --- |
| TestFloat 3e level 1, seed 1 | 4 formats × 5 operations × 5 rounding directions × 2 tininess modes | 7,461,360 / 7,461,360 |
| MPFR 4.2.2 `tests/data/sqrt` | all executable hexadecimal sqrt rows | 1,055 / 1,055 |
| MPFR 4.2.2 `pow_si` fixture | 4 precisions × 5 supported roundings × 6 inputs | 120 / 120 |
| MPFR 4.2.2 elementary fixture | 29 operations × 3 precisions × 6 roundings × 4 fixed-seed inputs | 2,088 / 2,088 |
| Optional MPFR elementary stress, seed 20260715 | at least 100,000 cases per three-operation-or-larger family | 966,744 / 966,744 |
| Committed smoke | TestFloat, sqrt, `pow_si`, and elementary witnesses | 2,271 / 2,271 |
| TestFloat 3e level 2 | binary16, all declared operations/directions/tininess modes | 50,205,600 / 50,205,600 |

The level-2 binary16 result is additional streaming stress evidence, not a
claim for the much larger binary32/64/128 level-2 suites. The archives/files
and digests are pinned in
[`testdata/bin_float/corpora.json`](../../../testdata/bin_float/corpora.json).
The runner streams TestFloat level 2 in verified bounded chunks, but level 2
is an optional stress suite and is not included in the result claim above.
The 966,744-row MPFR run is likewise optional generated stress evidence; the
2,088-row hash-pinned fixture remains the reproducible release boundary.

## Scope Of The Claim

## Stability Of The Evidence

The pinned matrix is the release evidence boundary; adding a new operation requires a new corpus contract and independent oracle.

The results cover contextual add, subtract, multiply, divide, and square root
for the four IEEE interchange formats and stated rounding/tininess modes, plus
the declared 29-function elementary surface at 24, 53, and 113 bits under all
six project rounding modes.
They do not claim TestFloat conformance for fused multiply-add, remainder,
conversions, comparisons, min/max, total ordering, decimal formats, or every
IEEE 754 operation or every real input. The elementary generator implements
nearest-away through MPFR's required `mpfr_round_nearest_away_begin/end`
protocol; it never passes the explicitly forbidden `MPFR_RNDNA` value to a
general elementary function.

Run `just conformance smoke binary` for the checked-in gate and `just gate binary` for the full
pinned gate.