From d36dce35d0b83094365c9030d3f68a8ab1865bed Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 23 Jul 2026 07:26:54 +0200 Subject: [PATCH] =?UTF-8?q?verify(falcon):=20v1.128=20=E2=86=92=20P04=20ve?= =?UTF-8?q?rified=20=E2=80=94=20machine-checked=20f32=20sin=20approximatio?= =?UTF-8?q?n=20bound=20(MATHF32-P04)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Two-commit rule, second commit (code-free): the implementation (the Coq-Interval proof proofs/rocq/sin_approx.v) landed in #307 with its Rocq + Gappa gate green on CI; this promotes SWREQ-FALCON-MATHF32-P04 from `implemented` to `verified` and adds the verification artifact FV-FALCON-MATHF32-004. The approximation-error bound |P(r) - sin r| <= 1e-8 over r in [-0.8, 0.8] is machine-checked (Coq-Interval `interval` tactic, kernel-checked by the withPackages coqc; the tactic's own success never trusted, CC-002), non-vacuous (proves 1e-8, fails 8e-9 at i_degree 18), enforced by the required rocq.yml gate (//proofs/rocq:all includes sin_approx_test). Coefficients are byte-identical to the P03 Gappa proof, so the rounding and approximation layers compose. Scope: the approximation ingredient only — the reduced-range composition and Cody-Waite reduction remain P06. No source changes. Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG --- artifacts/swreq/SWREQ-FALCON-MATHF32-P04.yaml | 2 +- .../verification/FV-FALCON-MATHF32-004.yaml | 46 +++++++++++++++++++ 2 files changed, 47 insertions(+), 1 deletion(-) create mode 100644 artifacts/verification/FV-FALCON-MATHF32-004.yaml diff --git a/artifacts/swreq/SWREQ-FALCON-MATHF32-P04.yaml b/artifacts/swreq/SWREQ-FALCON-MATHF32-P04.yaml index ac0ccd6..4718363 100644 --- a/artifacts/swreq/SWREQ-FALCON-MATHF32-P04.yaml +++ b/artifacts/swreq/SWREQ-FALCON-MATHF32-P04.yaml @@ -2,7 +2,7 @@ artifacts: - id: SWREQ-FALCON-MATHF32-P04 type: sw-req title: "MATHF32-P04 — machine-checked APPROXIMATION bound for the f32 sin polynomial (Coq-Interval)" - status: implemented + status: verified release: falcon-v1.128.0 description: > Establish the second (approximation) half of the sine-kernel proof: the diff --git a/artifacts/verification/FV-FALCON-MATHF32-004.yaml b/artifacts/verification/FV-FALCON-MATHF32-004.yaml new file mode 100644 index 0000000..024a71b --- /dev/null +++ b/artifacts/verification/FV-FALCON-MATHF32-004.yaml @@ -0,0 +1,46 @@ +artifacts: + - id: FV-FALCON-MATHF32-004 + type: sw-verification + title: "MATHF32-P04 — machine-checked (Coq-Interval) approximation bound for the f32 sin polynomial (v1.128)" + status: verified + release: falcon-v1.128.0 + description: > + Verification of SWREQ-FALCON-MATHF32-P04. The APPROXIMATION-error bound + on the f32 sin kernel — the minimax remainder |P(r) - sin r| <= 1e-8 over + the reduced range r in [-0.8, 0.8] — is MACHINE-CHECKED: Coq-Interval's + `interval` tactic (i_bisect, i_taylor, i_degree 15) proves it and the + withPackages coqc (rules_rocq_rust#43 rocq_interval_proof) kernel-checks + the emitted Flocq/Coq-Interval term, never trusting the tactic's own + success (rivet CC-002). proofs/rocq/sin_approx.v. + + Non-vacuous (has teeth): `interval` proves 1e-8 but FAILS to prove 8e-9 + even at i_degree 18 (and 5e-9 at i_degree 22) — negative-tested; the + bound is the tight achievable value, not a loose one. Enforced in CI: the + required .github/workflows/rocq.yml runs `bazel test //proofs/rocq:all + //proofs/gappa:all`, which includes //proofs/rocq:sin_approx_test, so the + proof cannot rot silently. The Rocq + Gappa gate ran and PASSED on the + merge of #307 (0 failures), confirming the kernel-check on CI + infrastructure, not only locally. + + Composability: the coefficients are byte-identical to the P03 Gappa proof + (S1 = -0x1.5555460p-3, S2 = 0x1.11073c0p-7, S3 = -0x1.9943f20p-13), so + P equals Gappa's exact-arithmetic Esin — the rounding (P03) and + approximation (P04) layers reference the SAME real function and therefore + compose by triangle inequality. Sanity: 1e-8 is far below the exhaustive + total 1.19e-7 (MATHF32-P02), which is dominated by f32 rounding — as + expected for a good minimax polynomial. + + SCOPE (honest): this verifies the APPROXIMATION ingredient only. The + reduced-range COMPOSITION (chaining P03 + P04 into one kernel-checked + |computed - sin r| <= 1e-8 + 2^-24 lemma) and the Cody-Waite + argument-reduction cancellation are scoped follow-ons (P06), NOT verified + here. + tags: [verification, falcon, relay-math, coq-interval, flocq, machine-checked, v1.128] + fields: + method: formal-verification + steps: + - run: bazel test //proofs/rocq:sin_approx_test + - run: bazel test //proofs/rocq:all //proofs/gappa:all + links: + - type: verifies + target: SWREQ-FALCON-MATHF32-P04