tricu

A lazy functional language based on Tree Calculus
Log | Files | Refs | README | LICENSE

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:

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.