From dee73e1b8643701f951e40485c32f6a0bf261ba7 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 29 Jul 2026 06:05:41 +0200 Subject: [PATCH] feat(math): machine-checked cos approximation bound (MATHF32-P05) + trace the OCI arc MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit v1.129 scope, planned in rivet before building (release-planning): P05 complete + close the traceability gap the plan surfaced. 1. COS APPROXIMATION PROOF (the missing half of P05). The rounding half already shipped (proofs/gappa/cos_poly_rounding.gappa, <= 2^-23) but was untraced; the approximation half did not exist. proofs/rocq/cos_approx.v now proves, kernel-checked by coqc via Coq-Interval: |Q(r) - cos r| <= 1e-9 for all r in [-0.8, 0.8] - Coefficients copied VERBATIM from the Gappa proof (C1 = 0x1.55554a0p-5, C2 = -0x1.6c0c340p-10, C3 = 0x1.99eb9c0p-16), so Ecos = Q as real functions and the rounding + approximation layers compose. Same correctness gate as the sine pair. - NON-VACUOUS (teeth): proves 1e-9 at i_degree 18, FAILS 1e-10 even at i_degree 20 (1e-11 fails at 22). - Wired into the required rocq.yml gate via //proofs/rocq:all; bazel test //proofs/rocq:cos_approx_test PASSED locally in relay's own bazel. - Cosine is ~10x more accurate than sine (1e-9 vs 1e-8) because cos_poly carries the exact `1 - 0.5*z` terms and only fits the residual. P05 -> implemented (two-commit rule; promotion is a separate code-free PR). Scope narrowed like P04: this delivers the two INGREDIENTS; the reduced-range composition lemma remains P06. 2. TRACE THE OCI ARC (SWREQ-FALCON-OCI-P01, new). The falcon-rate WASI-free conversion, the through-wasm closed-loop proof, and the per-component OCI publish all shipped with ZERO rivet artifacts — untracked work is invisible to the release plan. Records the three required properties (signed per-component distribution, no-WASI so it lowers, loop-complete evidence through the component's own seam) and ties them to the jess consumption contract (jess#167 / DD-026). rivet validate: PASS. Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG --- artifacts/swreq/SWREQ-FALCON-MATHF32-P05.yaml | 43 +++++++++---- artifacts/swreq/SWREQ-FALCON-OCI-P01.yaml | 53 ++++++++++++++++ proofs/rocq/BUILD.bazel | 16 +++++ proofs/rocq/cos_approx.v | 62 +++++++++++++++++++ 4 files changed, 163 insertions(+), 11 deletions(-) create mode 100644 artifacts/swreq/SWREQ-FALCON-OCI-P01.yaml create mode 100644 proofs/rocq/cos_approx.v diff --git a/artifacts/swreq/SWREQ-FALCON-MATHF32-P05.yaml b/artifacts/swreq/SWREQ-FALCON-MATHF32-P05.yaml index 2ac3fa8..0a1c24a 100644 --- a/artifacts/swreq/SWREQ-FALCON-MATHF32-P05.yaml +++ b/artifacts/swreq/SWREQ-FALCON-MATHF32-P05.yaml @@ -2,24 +2,45 @@ artifacts: - id: SWREQ-FALCON-MATHF32-P05 type: sw-req title: "MATHF32-P05 — machine-checked reduced-range bound for the COSINE kernel (rounding + approximation)" - status: proposed + status: implemented release: falcon-v1.129.0 description: > - Extend the sine-kernel proof method (MATHF32-P03 rounding + MATHF32-P04 - approximation, composed) to the f32 COSINE polynomial (cos_poly): a - Gappa rounding bound on the Horner evaluation plus a Coq-Interval bound - on |Q(r) - cos r|, composed to a kernel-checked reduced-range accuracy - bound for cosf. A small extension once the sine machinery exists — the - same two tools, the same composition, different coefficients and - reference function. + The cosine analogue of the sine-kernel proof pair, both halves now built: + (a) ROUNDING — a Gappa bound proving the f32 Horner evaluation of cos_poly + is within 2^-23 of the exact real value of the SAME polynomial over + r in [-0.8, 0.8] (proofs/gappa/cos_poly_rounding.gappa; the extra ulp vs + the sine's 2^-24 is the additional `1 - 0.5*z` subtraction); and + (b) APPROXIMATION — a Coq-Interval bound proving the exact polynomial is + within 1e-9 of true cosine over the same range + (proofs/rocq/cos_approx.v). Both are kernel-checked by coqc; neither + tool's own success is trusted (CC-002). The coefficients are byte-identical + between the two proofs (C1 = 0x1.55554a0p-5, C2 = -0x1.6c0c340p-10, + C3 = 0x1.99eb9c0p-16), so Ecos = Q as real functions and the two layers + compose by triangle inequality. + + The cosine core is ~an order of magnitude more accurate than the sine core + (1e-9 vs 1e-8, MATHF32-P04) because cos_poly carries the exact leading + terms `1 - 0.5*z` and only fits the residual. + + SCOPE (deliberately narrowed, mirroring P04): this delivers the two + INGREDIENTS. The reduced-range COMPOSITION — assembling them into one + coqc-checked |computed - cos r| <= 2^-23 + 1e-9 lemma — 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, gappa, coq-interval, machine-checked, v1.129] fields: req-type: non-functional priority: should verification-criteria: > - Gappa rounding proof + Coq-Interval approximation proof for cos_poly, - both coqc-kernel-checked and teeth-tested, composed to a reduced-range - |computed - cos r| bound; enforced under the rocq.yml gate. + Two kernel-checked proofs under the required rocq.yml gate + (bazel test //proofs/rocq:all //proofs/gappa:all): + bazel test //proofs/gappa:cos_poly_rounding_test (rounding, <= 2^-23) + and bazel test //proofs/rocq:cos_approx_test (approximation, <= 1e-9). + Both NON-VACUOUS (teeth-tested): the rounding proof passes 1b-23 and + FAILS 1b-28; the approximation proof passes 1e-9 at i_degree 18 and + FAILS 1e-10 even at i_degree 20. The composed reduced-range lemma is + NOT part of this requirement's evidence (see scope note; tracked as P06). links: - type: derives-from target: SYSREQ-FALCON-002 diff --git a/artifacts/swreq/SWREQ-FALCON-OCI-P01.yaml b/artifacts/swreq/SWREQ-FALCON-OCI-P01.yaml new file mode 100644 index 0000000..d47d268 --- /dev/null +++ b/artifacts/swreq/SWREQ-FALCON-OCI-P01.yaml @@ -0,0 +1,53 @@ +artifacts: + - id: SWREQ-FALCON-OCI-P01 + type: sw-req + title: "OCI-P01 — publish each verified cascade stage as a signed, lowerable OCI component" + status: implemented + release: falcon-v1.129.0 + description: > + The verified flight components shall be consumable by the system + integrator (jess) as individually addressable, signed artifacts — the + Level-1 fine-grained components of the consumption contract agreed in + pulseengine/jess#167 (jess DD-026): relay ships portable, minimal, + loop-complete components; jess owns the cross-core seam, fuses per core + (meld), lowers per ISA (loom -> synth -> gale-link) and signs the + flashable set. + + Three properties are required of a published component: + + (a) DISTRIBUTION — each cascade stage (flight, iekf, position, attitude, + rate, mixer) is pushed on every tagged release to + ghcr.io//falcon- with the Component-Model OCI media type + (via wkg, not a generic blob), cosign-signed by IMMUTABLE DIGEST (never a + mutable tag), and carries the embedded package metadata + (description/license/source/keywords) that makes its wasm.directory + listing meaningful. The push is non-blocking: a registry fault must never + fail the primary signed GitHub Release. + + (b) LOWERABLE — a published component should import NO WASI, so it can be + lowered to bare metal (synth -> gale) for the M4/M7/F100 partitions. The + cargo-component build links `std` by default (via thread_local!), which + drags in ~10 WASI imports; components are therefore built `no_std` on the + cargo-component path. + + (c) LOOP-COMPLETE EVIDENCE — a published component ships with a proof that + the control loop CLOSES THROUGH the component's own WIT seam (host drives + the real exported function, plant feeds back), not an open-loop smoke + test. This is the relay half of the agreed proof split: relay proves the + loop closes in source (SIL); jess proves it still closes after the + wasm->ARM lowering (Renode, on-target differential). + tags: [falcon, oci, wasm, component-model, distribution, jess-contract, v1.129] + fields: + req-type: interface + priority: should + verification-criteria: > + (a) release.yml publishes the six falcon- OCI refs, cosign-signed + by digest, each anonymously pullable with config media type + application/vnd.wasm.config.v0+json; (b) the rate component's built wasm + imports only falcon:cascade/types (zero wasi:* imports), checked with + wasm-tools; (c) tests/rate-loop-proof drives rate.tick across the wasm + boundary in a WASI-less wasmtime host and the body rate converges to a + 1 rad/s step within the documented budget. + links: + - type: derives-from + target: SYSREQ-FALCON-002 diff --git a/proofs/rocq/BUILD.bazel b/proofs/rocq/BUILD.bazel index f0e483c..6348bc0 100644 --- a/proofs/rocq/BUILD.bazel +++ b/proofs/rocq/BUILD.bazel @@ -98,3 +98,19 @@ rocq_proof_test( srcs = [], deps = [":sin_approx"], ) + +# ── f32 cos approximation-error bound (MATHF32-P05, Coq-Interval) ──────── +# The minimax-remainder half of the cos error: |Q(r) - cos r| <= 1e-9 over +# the reduced range, complementing the Gappa rounding bound in +# proofs/gappa/cos_poly_rounding.gappa. Cosine analogue of sin_approx. + +rocq_interval_proof( + name = "cos_approx", + srcs = ["cos_approx.v"], +) + +rocq_proof_test( + name = "cos_approx_test", + srcs = [], + deps = [":cos_approx"], +) diff --git a/proofs/rocq/cos_approx.v b/proofs/rocq/cos_approx.v new file mode 100644 index 0000000..be40344 --- /dev/null +++ b/proofs/rocq/cos_approx.v @@ -0,0 +1,62 @@ +(* Machine-checked APPROXIMATION-error bound for relay-math's f32 cos kernel + (MATHF32-P05, approximation half — the Coq-Interval layer). + + CLAIM (approximation 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 exact real value of the cos polynomial Q(r) differs + from the TRUE cosine by at most 1e-9: + |Q(r) - cos r| <= 1e-9 for all r in [-0.8, 0.8]. + This is the minimax remainder. The OTHER half — that the f32 Horner + evaluation is faithful to this same polynomial (the rounding remainder + |Mcos - Ecos| <= 2^-23) — is proven separately by Gappa in + proofs/gappa/cos_poly_rounding.gappa. Together they are the cosine + analogue of the sine pair (MATHF32-P03 rounding + MATHF32-P04 + approximation). + + COMPOSITION (not asserted here): because both proofs use the IDENTICAL f32 + coefficients (see below), Ecos = Q as real functions, so a triangle + inequality gives |Mcos - cos r| <= 2^-23 + 1e-9 ~= 1.2e-7 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. + + NON-VACUITY (teeth): the bound is tight and the tactic genuinely refutes a + tighter one. `interval` proves 1e-9 at i_degree 18; it FAILS to prove 1e-10 + even at i_degree 20 (and 1e-11 fails at i_degree 22). A bound that passes at + any value would prove nothing — this one stops passing just below 1e-9. + + Note the cosine core is ~an order of magnitude more accurate than the sine + core (1e-9 vs the sine's 1e-8, MATHF32-P04): cos_poly carries the exact + leading terms `1 - 0.5*z` and only fits the residual, so less of the value + comes from the minimax fit. + + Coefficients are the EXACT f32 dyadic values, copied verbatim from + proofs/gappa/cos_poly_rounding.gappa so the two layers compose: + C1 = 0x1.55554a0p-5 = 357913760 / 2^33 + C2 = -0x1.6c0c340p-10 = -381731648 / 2^38 + C3 = 0x1.99eb9c0p-16 = 429832640 / 2^44 + 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)) + + `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 C1 : R := 357913760 / 8589934592. +Definition C2 : R := -381731648 / 274877906944. +Definition C3 : R := 429832640 / 17592186044416. + +Definition Q (r : R) : R := + let z := r * r in + 1 - (1/2) * z + z * z * (C1 + z * (C2 + z * C3)). + +Theorem cos_approx_bound : + forall r : R, -8/10 <= r <= 8/10 -> Rabs (Q r - cos r) <= 1/1000000000. +Proof. + intros r Hr. unfold Q, C1, C2, C3. + interval with (i_bisect r, i_taylor r, i_degree 18). +Qed.