feat(math): machine-checked cos approximation bound (MATHF32-P05) + trace the OCI arc

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

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/<owner>/falcon-<stage> 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-<stage> 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

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"],
+)

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.