From 704f506bd00c241bfaf5f892e46db06bfe7fa5a2 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 22 Jul 2026 18:04:55 +0200 Subject: [PATCH] feat(math): machine-checked rounding bound for the f32 COSINE kernel (MATHF32-P05, rounding half) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The cosine analogue of the shipped sin proof (MATHF32-P03): the f32 Horner evaluation of cos_poly is faithful to within 2^-23 of the exact real value of the same polynomial over the reduced range r ∈ [-0.8, 0.8]. Gappa (gappa -Bcoq) emits a Flocq/Rocq term; coqc KERNEL-CHECKS it — never trusting Gappa's own success (rules_rocq_rust gappa_proof, rivet CC-002). 2^-23 (not 2^-24 like sin): cos_poly carries the extra `1 - 0.5*z` subtraction, which contributes an additional rounding step. Verified green + NON-VACUOUS in a clean run — an impossible bound (2^-28) fails to build ("some properties were not satisfied"), so the pass has teeth. Auto-enforced by the required rocq.yml gate (//proofs/gappa:all). Drafted in parallel by a subagent and INDEPENDENTLY re-verified here (its own claim of the bound was not taken on trust — I re-ran the kernel-check and the negative test myself). This is the ROUNDING half of MATHF32-P05. The APPROXIMATION half (|Q(r)-cos r|, Coq-Interval) is BLOCKED on a toolchain gap: Coq-Interval won't load without mathcomp (rules_rocq_rust#43). P05 stays proposed until that half lands. Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG --- proofs/gappa/BUILD.bazel | 16 ++++++++ proofs/gappa/cos_poly_rounding.gappa | 60 ++++++++++++++++++++++++++++ 2 files changed, 76 insertions(+) create mode 100644 proofs/gappa/cos_poly_rounding.gappa diff --git a/proofs/gappa/BUILD.bazel b/proofs/gappa/BUILD.bazel index 80be099..015ff8e 100644 --- a/proofs/gappa/BUILD.bazel +++ b/proofs/gappa/BUILD.bazel @@ -18,3 +18,19 @@ rocq_proof_test( srcs = [], deps = [":sin_poly_rounding"], ) + +# MATHF32-P05 (rounding half) — the cos-polynomial evaluation is faithful to +# its exact mathematics over the reduced range. The APPROXIMATION half +# (|Q(r)-cos r|, Coq-Interval) is blocked on the mathcomp toolchain gap +# (rules_rocq_rust#43) and lands separately. +gappa_proof( + name = "cos_poly_rounding", + src = "cos_poly_rounding.gappa", + visibility = ["//visibility:public"], +) + +rocq_proof_test( + name = "cos_poly_rounding_test", + srcs = [], + deps = [":cos_poly_rounding"], +) diff --git a/proofs/gappa/cos_poly_rounding.gappa b/proofs/gappa/cos_poly_rounding.gappa new file mode 100644 index 0000000..b761210 --- /dev/null +++ b/proofs/gappa/cos_poly_rounding.gappa @@ -0,0 +1,60 @@ +# Machine-checked rounding-error bound for relay-math's f32 cos polynomial +# (the cosine analogue of sin_poly_rounding.gappa — MATHF32-P03 track, +# rules_rocq_rust#37/#41). +# +# CLAIM (rounding-error LAYER only): over the reduced range r in [-0.8, 0.8] +# — the interval the Cody-Waite reduction clamps to, containing [-pi/4,pi/4] +# — the f32 Horner evaluation of cos_poly differs from the EXACT real value +# of the SAME polynomial (same f32 coefficients, no rounding) by at most +# 2^-23 (one ULP at unit magnitude for cos, whose result sits in [0.69, 1] +# — the tight machine-checked bound: coqc accepts 2^-23, rejects 2^-24; +# Gappa's best provable bound is ~8.95e-8 = 1.5*2^-24, because the +# `1 - 0.5*z` subtraction AND the final add each contribute a half-ulp at +# magnitude ~1, unlike sin whose result passes through 0 with r). +# I.e. the floating-point evaluation is faithful to the +# mathematics it implements. The OTHER ingredient — that this polynomial +# approximates the true cosine (the minimax remainder |P(r)-cos r|) — is +# the Coq-Interval layer, tracked separately, NOT proven here. +# +# `gappa -Bcoq` emits a Flocq/Rocq proof term; gappa_proof (rules_rocq_rust) +# kernel-checks it with coqc — Gappa's own success is never trusted (CC-002). +# +# Kernel source: crates/relay-math/src/lib.rs, cos_poly(): +# z = r*r; 1.0 - 0.5*z + z*z*(C1 + z*(C2 + z*C3)) +# evaluated left-to-right in f32 (each op rounds to nearest-even). + +@rnd = float; + +# Exact f32 coefficients (bit-identical to the compiled constants). +C1 = 0x1.55554a0p-5; +C2 = -0x1.6c0c340p-10; +C3 = 0x1.99eb9c0p-16; + +# r is a float in the reduced range. +r = rnd(rin); + +# --- f32 evaluation, operation-for-operation with the kernel --- +z rnd= r * r; +h rnd= 0.5 * z; +a rnd= 1 - h; # 1.0 - 0.5*z +zz rnd= z * z; +t0 rnd= z * C3; +t1 rnd= C2 + t0; +t2 rnd= z * t1; +t3 rnd= C1 + t2; # inner = C1 + z*(C2 + z*C3) +p rnd= zz * t3; # z*z*inner +Mcos rnd= a + p; + +# --- exact real value of the SAME polynomial (same coefficients) --- +Ez = r * r; +Eh = 0.5 * Ez; +Ea = 1 - Eh; +Ezz = Ez * Ez; +Et0 = Ez * C3; +Et1 = C2 + Et0; +Et2 = Ez * Et1; +Et3 = C1 + Et2; +Ep = Ezz * Et3; +Ecos = Ea + Ep; + +{ rin in [-0.8, 0.8] -> |Mcos - Ecos| <= 1b-23 }