# BinFloat Conformance Data

The user-facing semantic claim is summarized in
[`doc/en_US/bin_float/conformance.md`](../../doc/en_US/bin_float/conformance.md);
this page remains the operational source for corpus provenance and commands.

This directory defines the reproducible, finite conformance gate for the
supported `bin_float` IEEE 754 operations. It deliberately separates a pinned
test contract from the unbounded stress modes offered by TestFloat.

## Commands

```sh
just conformance smoke binary
just conformance fetch binary
just conformance plan binary --level 1 --tininess after --tininess before
just conformance run binary --level 1 --tininess after --tininess before
just gate binary 8
```

`just conformance smoke binary` runs the committed 60-row TestFloat subset,
three hexadecimal sqrt witnesses, 120 MPFR-generated integer-power witnesses,
and 2,088 full-family elementary witnesses without downloading anything.
`just conformance fetch binary` verifies SHA-256 and
installs the external artifacts under `.tmp/`. `just gate binary` builds the reference
generator and the native interpreters, then runs the declared full gate.

## Declared Full Gate

The full TestFloat matrix is finite and deterministic:

- formats: binary16, binary32, binary64, binary128;
- operations: add, subtract, multiply, divide, square root;
- rounding: nearest-even, nearest-away, toward-zero, toward-negative,
  toward-positive;
- tininess detection: before and after rounding;
- TestFloat level: 1, seed: 1.

Its 200 tasks contain 7,461,360 vectors. The MPFR part executes every one of
the 1,055 executable rows in the pinned `tests/data/sqrt` file plus 2,088
hash-pinned cases covering 29 elementary operations, binary32/64/128
precisions, and all six `BinaryRoundingMode` values. The runner
requires exact encoded results and exception bits for non-NaN results. For a
NaN result it requires a quiet NaN class and the exact exception bits, because
IEEE 754 permits implementation choices for a generated NaN payload.

`--level 2` remains available as a much larger, deterministic stress suite.
It is intentionally not part of the published finite gate: it contains tens to
hundreds of millions of vectors per high-precision binary operation. The
runner streams it in bounded chunks, validates that every generated row was
executed, and never truncates or substitutes vectors.

As an additional stress result, the complete binary16 level-2 matrix (all five
operations, five rounding directions, and both tininess modes) executed
50,205,600 / 50,205,600 vectors successfully. This result demonstrates the
streaming path; it does not turn the much larger binary32/64/128 level-2 suite
into a published claim.

## Provenance

| Artifact | Pinned source | SHA-256 / revision |
| --- | --- | --- |
| Berkeley SoftFloat 3e | `https://www.jhauser.us/arithmetic/SoftFloat-3e.zip` | `21130ce885d35c1fe73fc1e1bf2244178167e05c6747cad5f450cc991714c746` |
| Berkeley TestFloat 3e | `https://www.jhauser.us/arithmetic/TestFloat-3e.zip` | `6d4bdf0096b48a653aa59fc203a9e5fe18b5a58d7a1b715107c7146776a0aad6` |
| GNU MPFR 4.2.2 sqrt data | MPFR commit `eaa57b856d814af32f97d5e5eb129fb986235323` | `c9baa569b7b5c91d07a528e722b92871d80deac05cb24b97359555801ab470be` |
| GNU MPFR 4.2.2 `pow_si` smoke | locally generated by `tools/generate_mpfr_pow_oracle.c` | MPFR 4.2.2 + GMP 6.3.0 |
| GNU MPFR 4.2.2 elementary matrix | locally generated by `tools/generate_mpfr_elementary_oracle.c`, seed `20260715` | `477a081f566d81c5d42cf083b706ac3610befc91063c1a5547423407494d4be5` |

The TestFloat smoke vectors are the first twelve rows generated for each
binary16 operation using the command recorded in their comment headers. They
are a fast regression fixture, not a replacement for the full gate.

## Interpreter Boundary

`src/frontend/testfloat_expr` parses TestFloat rows into typed binary interchange
values, creates the requested `BinaryContext`, and runs `BinFloat` directly.
`src/frontend/mpfr_expr` parses MPFR hexadecimal `data_check` sqrt rows, the
committed `pow_si` rows, and the elementary matrix. The elementary generator
uses MPFR's required `mpfr_round_nearest_away_begin/end` wrapper rather than
passing the explicitly forbidden `MPFR_RNDNA` value to general functions.
`tools/generate_mpfr_elementary_oracle.c 1852 20260715` produces at least
100,000 fixed-seed cases even for the smallest three-operation family; it is an
optional stress corpus and is not committed. The declared command executed
966,744/966,744 cases successfully. Python only fetches, streams,
shards, and aggregates; it does not implement or alter floating-point
arithmetic.

See the localized design and conformance documents under `doc/*/bin_float/`
for standards, algorithms, results, and explicit non-claims.