float-validation.md (6947B)
Binary64 validation
The binary64 tests check complete result trees, canonical input structure, private-value invariants, rounding, exception flags and demand. They use a retained compiler and fresh workspaces. Run Python with assertions enabled.
Source-library checks
Select the host executable explicitly and choose fresh output directories:
HOST=/path/to/tricu
python3 test/float_boundary_test.py
python3 test/float_boundary.py "$HOST" --library --directory /tmp/binary64-boundary
python3 test/float_library_acceptance.py "$HOST" \
--boundary-run /tmp/binary64-boundary --directory /tmp/binary64-application
The boundary runner copies the library sources and its test driver into a flat
workspace, compiles with bootstrap/build-stable.arboricx, and checks:
- canonical Words, every small tree through eight nodes, malformed bits/tails, redundant high zeros and the 64/65-bit boundary;
- Word contracts, transforming imports, exact transport and remainder preservation;
- all four arithmetic corpora, including signed zeros, NaNs, infinities, rounding boundaries and overflow/underflow;
- rejection of each malformed Word on either side of every checked operation;
- arithmetic chains with prefix observations, subnormal reuse and named flag projections.
Demand probes exercise malformed left operands, malformed bits, oversized tails, a zero 64th bit with an opaque tail, an unused remainder, checked NaN-input validation and trusted left-NaN value projection. The standalone Python tests also exhaust trees through ten nodes and audit the library's initial extraction.
The application runner authenticates the boundary run's source receipt, compiles
demos/binary64.tri, and exercises transforming contract composition through
base.pairOf. It checks x*y+x on class and rounding-boundary pairs and checks
malformed outer pairs and Words.
Three small-workload checks cover four affine values, four 16-addition chains and four 4-division chains. Each batch has a two-second local acceptance budget. Treat this budget as a host-specific resource check and use the recorded samples when choosing budgets for other environments.
Published-artifact checks
Supply --support-bundle /path/to/support-library.arboricx to both the boundary
and application runners, alongside the source-library arguments above. Each run
uses an isolated workspace. Complete providers are projected from the selected
artifact and imported indexed; the reports bind their bundle, selected transport
and manifest identities. The boundary driver exercises compiled binary64 and
binary64_kernels; the application driver exercises compiled demos_binary64.
The application runner requires the same support bundle as its boundary run.
python3 test/float_publication_test.py checks the publisher's closed cohort,
source identities and ownership. The independent Haskell fixture verifier checks
all thirteen members and their rebuild receipts, including rejection controls
for missing members, changed paths, duplicate ownership and incomplete rebuilds.
Independent arithmetic reference
Build the C reference using a compiler with binary64 double and working fenv
support:
cc -O0 -std=c11 -frounding-math -fno-fast-math \
test/float_ieee_host.c -lm -o /tmp/binary64-reference
python3 test/float_ieee_host.py /tmp/binary64-reference \
--directory /tmp/binary64-reference-check
TRICU_FLOAT_HOST=/tmp/binary64-reference python3 test/float_working_test.py
TRICU_FLOAT_HOST=/tmp/binary64-reference python3 test/float_chains_test.py
python3 test/float_ieee_test.py
The C helper uses volatile doubles, memcpy bit transport, FE_TONEAREST, and
immediate flag reads. The exact Python oracle chooses neighboring IEEE values
using rational arithmetic. Reference checks compare all five flags and exact
finite/infinite/zero words. For NaNs, C supplies quiet-class and flag checks;
the explicit policy oracle supplies the chosen sign/payload expectations.
float_ieee_test.py also uses the Python host fenv adapter on its supported
platform. The separate C runner includes zero-divisor cases. C and Python host
arithmetic run as independent validation processes; the tricu implementation
computes through its source kernels.
Working values and regression controls
python3 test/float_working.py "$HOST" --directory /tmp/binary64-working
python3 test/float_chains.py "$HOST" --directory /tmp/binary64-chains
The working-value runner compares full private results against canonical class/sign/scale/significand expectations, including subnormal padding zeros. It also checks direct quantization, transport, demand, and working-value versus word-backed chains. The chain corpus includes prefixes and isolated primitive steps with clear flags so each step's value and flags remain observable.
Earlier component runners cover layouts, significands, exact alignment, near
jamming, quantization, finite operations and product/quotient kernels. Their
--help output describes required artifact/directory arguments. Preserve the
input contracts associated with each component.
Flag models in component controls
The earlier float_quantize, float_quantize_fast, float_aligned_quantize,
float_near_jam, float_finite, and float_finite_product_quotient controls track
a stored-tininess flag: inexact and stored magnitude below minimum normal.
Their result schemas and oracles reproduce that component model.
Full IEEE flag acceptance uses float_ieee, float_working, and the library
boundary runners. These classify tininess after precision rounding with an
unbounded exponent. Some inexact values that store minimum normal still raise
underflow. The retained storedMultiplies/storedDivides controls and their
counterexamples expose the difference between these two flag models.
Measurement and receipts
Each timed call uses a fresh process, one capability and a 2 GiB heap cap. Invocation timing ends after sharing-aware full-result forcing, before rendering. Allocation counts are cumulative. RTS maximum-live values are sampled at major collections across the whole process. RSS polling records an observed lower bound on peak resident memory; short jobs can finish between polls.
Output directories contain input trees, output trees, compiler bundles, process
logs, samples and JSON reports. Reports identify source/compiler/runtime hashes
and compare complete outputs against independent expectations. Retained
bench/float-*-results.json files describe their recorded source snapshots.
Compare each report with its receipts when evaluating a later source revision.
The initial extraction receipt is test/float-library-extraction.json.
bench/float-library-results.json records the library, application and independent
reference checks. Documentation-only source edits can be audited using their
executable-body fingerprints while preserving the original byte hashes.