Toolchain: add Flocq + Gappa + Coq-Interval to enable machine-checked floating-point error-bound proofs

[avrabe]

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

1. Add to the toolchain flake: coq-flocq, coq-gappa + the gappa binary, coq-interval, coq-coquelicot (reals). Pin versions against the bundled Rocq.
2. Expose their .vo/include paths so rocq_library can depend on them (or a thin gappa_proof rule wrapping the gappa→Coq flow).
3. 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

[avrabe]

Triaged and accepted. This is real toolchain work (new Nix deps + Bazel wiring + a template proof), so it's now driven through rivet for traceability rather than done ad hoc:

• Bootstrapped a rivet project for this repo (it had none) — PR feat: bootstrap rivet verification scaffolding, seed hazard analysis for #37 #40
• REQ-002 / DD-001 / FEAT-001 capture your own Gappa+Coq-Interval+Flocq architecture assessment as the accepted design
• Also seeded H-002 / CC-002: whatever wraps Gappa must always kernel-replay its emitted Flocq proof term through Rocq — Gappa's own certificate success is never sufficient by itself. That's now a tracked constraint, not just an implicit assumption.

Next: once #40 merges, the actual flake/Bazel work (adding coq-flocq, coq-gappa + the gappa binary, coq-interval, coq-coquelicot, and the minimal end-to-end example) gets built against FEAT-001.

🤖 Generated with Claude Code

[avrabe]

Implemented in PR #41 (built on the rivet scaffolding from #40):

• `coqPackages.flocq`/`interval`/`coquelicot` added via nixpkgs (already built against this toolchain's exact Rocq 9.0.1)
• The standalone `gappa` binary added (it's an external CLI, not a Coq plugin)
• One correction to the original ask: nixpkgs has no `coq-gappa` package at this pin (verified by enumerating `coqPackages`). Gappa's Rocq support library (`gappalib-coq`, the `Gappa.Gappa_library` that `gappa -Bcoq` output `Require Import`s) is built from source against Flocq instead — the same pattern this repo already uses for `smpl`.
• A new `gappa_proof` Bazel macro wraps the gappa→Rocq flow. Per CC-002, Gappa's CLI output is never trusted directly: the macro always compiles the emitted proof term with `rocq_library`, so it fails like any other Rocq proof if the kernel rejects what Gappa produced.
• A minimal end-to-end example (`examples/gappa_proof`) proves one f32 rounding bound and is verified locally: `bazel test //examples/gappa_proof:rounding_bound_test` — PASSED.

This is the template for relay's kernels — once merged, the next step on relay's side would be writing the actual kernel-specific `.gappa` statements for the sin/cos rounding bounds.

🤖 Generated with Claude Code