Need
relay's flight-math seam (relay-math) now ships f32 sin/cos kernels with an EXHAUSTIVELY established accuracy bound (all ~2.2e9 envelope f32 vs an f64 reference: worst abs error 1.19e-7 = 1 ulp-of-unity; ≤2 ulp off-zeros — falcon MATHF32-P02). That is the qualified-single-precision empirical standard (CORE-MATH/crlibm). The next assurance level is a machine-checked error-bound proof — and the current Rocq toolchain here cannot express it: the flake bundles Rocq + rocq-of-rust but no Flocq, no Gappa, no Coq-Interval, and the existing Rocq proofs are abstract-over-Z invariants (no reals, no floating-point).
Assessment: Gappa vs base Rocq (asked by the relay maintainer)
- Gappa is the right tool for the rounding-error layer (f32 op accumulation through Cody–Waite reduction + Horner) — semi-automatic (interval arithmetic + rewriting DB), and it emits a Flocq/Coq proof term the kernel checks. Dramatically less labor than hand Rocq for this layer. It does NOT replace Rocq — it plugs into it.
- Gappa does not cover the approximation-error layer (|P(r) − sin r| ≤ ε on [−π/4, π/4], the minimax remainder). That needs Coq-Interval (Taylor-model/interval bounds on the real function) or a Sollya supnorm certificate checked in Coq.
- Base Rocq + Flocq alone (no Gappa/Interval) = maximally flexible but hundreds of manual lines per function; not recommended as the primary path.
So a complete kernel bound = Gappa (rounding) + Coq-Interval (approximation) + Flocq (fp model), with the argument-reduction cancellation proof being the genuinely hard part (the crlibm/CORE-MATH papers are exactly this — a multi-week effort even with the tools).
Ask
- Add to the toolchain flake:
coq-flocq, coq-gappa + the gappa binary, coq-interval, coq-coquelicot (reals). Pin versions against the bundled Rocq.
- Expose their
.vo/include paths so rocq_library can depend on them (or a thin gappa_proof rule wrapping the gappa→Coq flow).
- A minimal example proving one f32 rounding bound end-to-end, kernel-checked, as the template.
Priority
Enabling, not blocking: the exhaustive-enumeration bound is itself an accepted certification method, so the proof is a raise-assurance investment. This issue is the prerequisite the relay maintainer correctly anticipated ("first enhance rules_rocq_rust").
🤖 Generated with Claude Code
https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG
Need
relay's flight-math seam (relay-math) now ships f32 sin/cos kernels with an EXHAUSTIVELY established accuracy bound (all ~2.2e9 envelope f32 vs an f64 reference: worst abs error 1.19e-7 = 1 ulp-of-unity; ≤2 ulp off-zeros — falcon MATHF32-P02). That is the qualified-single-precision empirical standard (CORE-MATH/crlibm). The next assurance level is a machine-checked error-bound proof — and the current Rocq toolchain here cannot express it: the flake bundles Rocq + rocq-of-rust but no Flocq, no Gappa, no Coq-Interval, and the existing Rocq proofs are abstract-over-Z invariants (no reals, no floating-point).
Assessment: Gappa vs base Rocq (asked by the relay maintainer)
So a complete kernel bound = Gappa (rounding) + Coq-Interval (approximation) + Flocq (fp model), with the argument-reduction cancellation proof being the genuinely hard part (the crlibm/CORE-MATH papers are exactly this — a multi-week effort even with the tools).
Ask
coq-flocq,coq-gappa+ thegappabinary,coq-interval,coq-coquelicot(reals). Pin versions against the bundled Rocq..vo/include paths sorocq_librarycan depend on them (or a thingappa_proofrule wrapping the gappa→Coq flow).Priority
Enabling, not blocking: the exhaustive-enumeration bound is itself an accepted certification method, so the proof is a raise-assurance investment. This issue is the prerequisite the relay maintainer correctly anticipated ("first enhance rules_rocq_rust").
🤖 Generated with Claude Code
https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG