From 4683ee1f3543d2cd37806f138361a9d401b697d3 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 22 Jul 2026 21:20:46 +0200 Subject: [PATCH] feat(math): machine-checked approximation bound for the f32 sin kernel (MATHF32-P04) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The "not yet proven" half from the f32/f64 story: the minimax remainder |P(r) - sin r|, the approximation-layer companion to the P03 Gappa rounding bound. Proven with Coq-Interval, now that rules_rocq_rust#43 wired the withPackages env that resolves Interval's full closure (mathcomp-boot/fingroup, hierarchy-builder, coq-elpi) — empirically confirmed: the `interval` tactic runs end-to-end, not just fetched. proofs/rocq/sin_approx.v proves, kernel-checked by coqc: |P(r) - sin r| <= 1e-8 for all r in [-0.8, 0.8] over the range reduce() actually clamps to (the kernel doc comment says pi/4 ~ 0.785; the clamp is 0.8 — we prove the wider clamp range). - Coefficients are byte-identical to proofs/gappa/sin_poly_rounding.gappa (S1 = -0x1.5555460p-3, etc.), so P equals Gappa's exact-arithmetic Esin — the rounding and approximation layers reference the SAME real function and therefore compose (triangle inequality). This coefficient match is the correctness gate, not a nicety: with different coefficients the bounds do not chain. - NON-VACUOUS (teeth): `interval` proves 1e-8 at i_degree 15 but FAILS to prove 8e-9 even at i_degree 18 (5e-9 fails at i_degree 22). The pass is not achievable at an arbitrary bound. Mirrors P03's "coqc rejects 2^-25". - Wired into the required rocq.yml gate via //proofs/rocq:all (bazel test //proofs/rocq:sin_approx_test PASSED locally in relay's bazel). - MODULE.bazel: use_repo rocq_interval_env (the rocq_interval_proof rule defaults to @rocq_interval_env//:coqc). Scope, stated honestly (two-commit rule — status set to `implemented`, not `verified`): this delivers the approximation INGREDIENT. The reduced-range COMPOSITION into one |computed - sin r| <= 1e-8 + 2^-24 lemma is deferred to the P06 composition step; P04's scope is narrowed accordingly and the artifact does not claim the composition is done. Sanity: approximation (1e-8) is far below the exhaustive total (1.19e-7), which is dominated by f32 rounding — as expected for a good minimax polynomial. Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG --- MODULE.bazel | 7 +++ artifacts/swreq/SWREQ-FALCON-MATHF32-P04.yaml | 59 ++++++++++++------- proofs/rocq/BUILD.bazel | 20 ++++++- proofs/rocq/sin_approx.v | 58 ++++++++++++++++++ 4 files changed, 122 insertions(+), 22 deletions(-) create mode 100644 proofs/rocq/sin_approx.v diff --git a/MODULE.bazel b/MODULE.bazel index 4d19ca7..212490e 100644 --- a/MODULE.bazel +++ b/MODULE.bazel @@ -85,6 +85,13 @@ use_repo( "rocq_gappalib", "rocq_interval", "rocq_coquelicot", + # Coq-Interval approximation-bound env (rules_rocq_rust#43, DD-003): a + # coq_9_0.withPackages(...) composition resolving Interval's full closure + # (mathcomp-boot/fingroup, hierarchy-builder, coq-elpi). The + # rocq_interval_proof rule defaults to @rocq_interval_env//:coqc — without + # this use_repo, proofs/rocq/sin_approx.v (MATHF32-P04) can't resolve + # `Require Import Interval.Tactic`. + "rocq_interval_env", ) register_toolchains("@rocq_toolchains//:all") diff --git a/artifacts/swreq/SWREQ-FALCON-MATHF32-P04.yaml b/artifacts/swreq/SWREQ-FALCON-MATHF32-P04.yaml index 382dfb7..ac0ccd6 100644 --- a/artifacts/swreq/SWREQ-FALCON-MATHF32-P04.yaml +++ b/artifacts/swreq/SWREQ-FALCON-MATHF32-P04.yaml @@ -1,34 +1,51 @@ artifacts: - id: SWREQ-FALCON-MATHF32-P04 type: sw-req - title: "MATHF32-P04 — machine-checked APPROXIMATION bound for the sin polynomial (Coq-Interval) + reduced-range composition" - status: proposed + title: "MATHF32-P04 — machine-checked APPROXIMATION bound for the f32 sin polynomial (Coq-Interval)" + status: implemented release: falcon-v1.128.0 description: > - Establish the second (approximation) half of the sine-kernel proof and - COMPOSE it with the rounding half (MATHF32-P03) to give a machine-checked - bound on the reduced-range accuracy of the f32 sine kernel. Two parts: - (a) using Coq-Interval (now wired via rules_rocq_rust #41), prove the - minimax remainder |P(r) - sin r| <= eps over the reduced range r in - [-0.8, 0.8] (containing [-pi/4, pi/4]), where P is the exact real value - of the kernel's f32-coefficient polynomial; (b) compose it with the - P03 Gappa rounding bound |computed - P(r)| <= 2^-24 via the triangle - inequality to obtain a kernel-checked |computed - sin r| <= (eps + - 2^-24) for the REDUCED range. This turns "rounding proven" into - "reduced-range sine kernel proven." It does NOT cover the full input - range — the Cody-Waite argument-reduction cancellation (MATHF32-P06) is - the remaining ingredient for that. + Establish the second (approximation) half of the sine-kernel proof: the + minimax remainder between the kernel polynomial and true sine. Using + Coq-Interval (wired via rules_rocq_rust #41/#43 — the withPackages env + that resolves Interval's full closure, DD-003), prove + |P(r) - sin r| <= 1e-8 over the reduced range r in [-0.8, 0.8] (the + interval the Cody-Waite reduction clamps to, containing [-pi/4, pi/4]), + where P is the EXACT real value of the kernel's f32-coefficient + polynomial. The coefficients are byte-identical to those in the P03 + Gappa proof (S1 = -0x1.5555460p-3, S2 = 0x1.11073c0p-7, + S3 = -0x1.9943f20p-13), so P equals Gappa's exact-arithmetic polynomial + Esin — the two layers reference the SAME real function. This is the + OTHER ingredient (with the P03 rounding bound) behind the exhaustive + 1.19e-7 (~2^-23) absolute-error bound (MATHF32-P02), now proven by + construction rather than by enumeration. + + SCOPE (deliberately narrowed from the original P04 draft): this + requirement delivers the approximation INGREDIENT only. The reduced-range + COMPOSITION — chaining this bound with the P03 rounding bound via the + triangle inequality to a single kernel-checked + |computed - sin r| <= 1e-8 + 2^-24 (~6.9e-8) — is valid precisely + because the coefficients are identical, but assembling it as one + coqc-checked Rocq lemma (integrating the Gappa-emitted term with the + Interval term) is deferred to the P06 composition step, where the + reduced-range pieces are combined with the argument-reduction bound for + FULL-range accuracy. This artifact does not claim the composition is done. tags: [falcon, relay-math, f32, coq-interval, flocq, machine-checked, qualification, v1.128] fields: req-type: non-functional priority: should verification-criteria: > - A Coq-Interval proof of |P(r) - sin r| <= eps over [-0.8, 0.8], - kernel-checked by coqc, with a NON-VACUOUS (teeth-tested) eps — coqc - rejects a bound tighter than achievable. A composed Rocq lemma - deriving |computed - sin r| <= eps + 2^-24 from P04 and P03. Both run - under the required rocq.yml gate (bazel test //proofs/rocq:all - //proofs/gappa:all, extended to the interval proof). + proofs/rocq/sin_approx.v proves |P(r) - sin r| <= 1e-8 over + [-0.8, 0.8] via the Coq-Interval `interval` tactic (i_bisect, i_taylor, + i_degree 15), kernel-checked by the withPackages coqc + (rocq_interval_proof); the tactic's own success is never trusted + (CC-002). The bound has teeth — it is NON-VACUOUS: `interval` proves + 1e-8 but FAILS to prove 8e-9 even at i_degree 18 (and 5e-9 at + i_degree 22), so the 1e-8 pass is not achievable at an arbitrary + bound. Runs as `bazel test //proofs/rocq:sin_approx_test`, included in + the required rocq.yml gate (//proofs/rocq:all). The composed + reduced-range lemma is NOT part of this requirement's evidence (see + scope note; tracked under P06). links: - type: derives-from target: SYSREQ-FALCON-002 diff --git a/proofs/rocq/BUILD.bazel b/proofs/rocq/BUILD.bazel index e5f8f31..f0e483c 100644 --- a/proofs/rocq/BUILD.bazel +++ b/proofs/rocq/BUILD.bazel @@ -9,7 +9,7 @@ # these are PURE ABSTRACT proofs — they use only Stdlib.ZArith and # do not depend on any translation infrastructure. -load("@rules_rocq_rust//rocq:defs.bzl", "rocq_library", "rocq_proof_test") +load("@rules_rocq_rust//rocq:defs.bzl", "rocq_interval_proof", "rocq_library", "rocq_proof_test") # ── Limit Checker proofs ──────────────────────────────────────────────── @@ -80,3 +80,21 @@ rocq_proof_test( srcs = ["cfdp_proofs.v"], deps = [":cfdp_proofs"], ) + +# ── f32 sin approximation-error bound (MATHF32-P04, Coq-Interval) ───────── +# The minimax-remainder half of the sin error: |P(r) - sin r| <= 1e-8 over +# the reduced range, complementing the Gappa rounding bound in +# proofs/gappa/sin_poly_rounding.gappa. Uses the withPackages Interval env +# (rules_rocq_rust#43); the kernel-check is the point, the tactic is not +# trusted (CC-002). + +rocq_interval_proof( + name = "sin_approx", + srcs = ["sin_approx.v"], +) + +rocq_proof_test( + name = "sin_approx_test", + srcs = [], + deps = [":sin_approx"], +) diff --git a/proofs/rocq/sin_approx.v b/proofs/rocq/sin_approx.v new file mode 100644 index 0000000..edffe59 --- /dev/null +++ b/proofs/rocq/sin_approx.v @@ -0,0 +1,58 @@ +(* Machine-checked APPROXIMATION-error bound for relay-math's f32 sin kernel + (MATHF32-P04 — the Coq-Interval layer, rules_rocq_rust#41/#43). + + CLAIM (approximation LAYER only): over the reduced range r in [-0.8, 0.8] + — the interval the Cody-Waite reduction clamps to; note sin_poly's doc + comment says |r| <= pi/4 (~0.785) but reduce() actually clamps to 0.8, so + we prove the wider CLAMP range, which contains [-pi/4, pi/4] — the exact + real value of the sin polynomial P(r) differs from the TRUE sine by at + most 1e-8: + |P(r) - sin r| <= 1e-8 for all r in [-0.8, 0.8]. + This is the minimax remainder — the OTHER ingredient behind the exhaustive + 1.19e-7 absolute-error bound (MATHF32-P02). The FIRST ingredient — that the + f32 Horner evaluation is faithful to this same polynomial (the rounding + remainder |Msin - Esin| <= 2^-24) — is proven separately by Gappa in + proofs/gappa/sin_poly_rounding.gappa (MATHF32-P03). + + COMPOSITION (not asserted here): because both proofs use the IDENTICAL f32 + coefficients (see below), Esin = P as real functions, so a triangle + inequality gives |Msin - sin r| <= 2^-24 + 1e-8 ~= 6.9e-8 over the reduced + range. Assembling that total (and carrying the reduction cancellation, + MATHF32-P06) is a further step; this file proves ONLY the approximation + remainder. Do not read it as closing the whole envelope error. + + NON-VACUITY (teeth): the bound is tight and the tactic genuinely refutes a + tighter one. `interval` proves 1e-8 at i_degree 15; it FAILS to prove 8e-9 + even at i_degree 18 (and 5e-9 fails at i_degree 22). A bound that passes at + any value would prove nothing — this one stops passing just below 1e-8. + + Coefficients are the EXACT f32 dyadic values, copied verbatim from + proofs/gappa/sin_poly_rounding.gappa so the two layers compose: + S1 = -0x1.5555460p-3 = -357913696 / 2^31 + S2 = 0x1.11073c0p-7 = 286290880 / 2^35 + S3 = -0x1.9943f20p-13 = -429145888 / 2^41 + Kernel source: crates/relay-math/src/lib.rs, sin_poly(): + z = r*r; r + r*z*(S1 + z*(S2 + z*S3)) + + `interval` emits a Flocq/Coq-Interval proof term; rocq_interval_proof + (rules_rocq_rust) kernel-checks it with the withPackages coqc — the tactic's + own success is never trusted (CC-002). *) + +Require Import Reals. +Require Import Interval.Tactic. +Local Open Scope R_scope. + +Definition S1 : R := -357913696 / 2147483648. +Definition S2 : R := 286290880 / 34359738368. +Definition S3 : R := -429145888 / 2199023255552. + +Definition P (r : R) : R := + let z := r * r in + r + r * z * (S1 + z * (S2 + z * S3)). + +Theorem sin_approx_bound : + forall r : R, -8/10 <= r <= 8/10 -> Rabs (P r - sin r) <= 1/100000000. +Proof. + intros r Hr. unfold P, S1, S2, S3. + interval with (i_bisect r, i_taylor r, i_degree 15). +Qed.