Skip to content

README.md

Latest commit

 

History

History
89 lines (72 loc) · 4.67 KB

README.md

File metadata and controls

89 lines (72 loc) · 4.67 KB
Raw

BinFloat Conformance Data

The user-facing semantic claim is summarized in 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

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.