feat(falcon): v1.126 — exhaustive worst-case accuracy bound for the f32 kernels (MATHF32-P02) - #293
Merged
Merged
Conversation
…32 kernels (MATHF32-P02) "Did we prove the math?" — no, and the v1.125 sampled conformance was weaker than its wording: a 4M-point grid cannot bound worst-case error over a continuum (it stepped over the near-zero arguments, the same way the grid stepped over the notch coefficients earlier). Replaced with an EXHAUSTIVE sweep — every f32 in the envelope |x| ≤ 128 (~2.2e9 values) against an f64 reference (near-true; strictly better than libm's own ~1 ulp f32 sinf), parallel, ~seconds in release. The qualified-single- precision standard (CORE-MATH/crlibm), a real bound not a sample. Result (honest, flight-relevant): worst ABSOLUTE error 1.19e-7 = 1 ulp at unit magnitude over ALL inputs; ≤ 2 ulp wherever |value| ≥ 1e-3. The exhaustive sweep DID surface what the sample hid — up to ~14 ulp near the function zeros — but that is the ulp-inflates-on-a-vanishing- magnitude artifact, not accuracy loss: the absolute error there is still ≤ 1.19e-7, and so3_exp / mixer geometry / notch coefficients consume the VALUES, not a ulp. The fast 4M test now uses the same honest off-zeros metric (it was asserting a ≤2 ulp it could not uphold near zeros). SWREQ-FALCON-MATHF32-P02 → implemented (refines P01; verify PR follows). The machine-checked error-bound PROOF (Gappa+Coq-Interval+Flocq) is a separate track — see the rules_rocq_rust enhancement issue. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Verify-Filter: (has-tag "v1.126")
Implements MATHF32-P02 (→
implemented). Answers "how do we ensure the math, not just test it" for the v1.125 f32 kernels.Why
The v1.125 conformance was a 4M-point sampled sweep asserting ≤2 ulp — and a sample cannot bound worst-case error over a continuum. It was stepping over the near-zero arguments (the same failure mode that hid the notch coefficient behaviour earlier). Not good enough for a qualification item.
What
Exhaustive enumeration: every f32 in |x| ≤ 128 (~2.2e9 values) against an f64 reference (near-true — strictly better than libm's own ~1 ulp f32
sinf). Parallel, seconds in release, ignored/nightly. This is the qualified-single-precision standard (CORE-MATH / crlibm) — a real bound.Result (honest, flight-relevant)
so3_exp/ mixer geometry / notch coefficients use the values. The fast 4M test now uses the same honest off-zeros metric (it was asserting a ≤2 ulp it couldn't uphold near zeros).The proof track (your Gappa question)
A machine-checked error-bound proof is a separate effort and needs tooling the repo doesn't have yet — Gappa (fp rounding-error, semi-automatic, emits Flocq/Coq) + Coq-Interval (the polynomial approximation remainder Gappa doesn't cover) + Flocq.
rules_rocq_rust's toolchain currently bundles none of these. Filed as the enabling enhancement; assessment in the issue. The exhaustive bound here is the empirical foundation such a proof would certify.Gates
relay-math tests pass (fast); exhaustive on-demand green (1.19e-7 / 2 ulp); clippy
-D warningsclean; float gate green;rivet validatePASS.🤖 Generated with Claude Code
https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG