verify(falcon): v1.129 → P05 + OCI-P01 verified

artifacts/swreq/SWREQ-FALCON-MATHF32-P05.yaml

@@ -2,7 +2,7 @@ artifacts:
   - id: SWREQ-FALCON-MATHF32-P05
     type: sw-req
     title: "MATHF32-P05 — machine-checked reduced-range bound for the COSINE kernel (rounding + approximation)"
-    status: implemented
+    status: verified
     release: falcon-v1.129.0
     description: >
       The cosine analogue of the sine-kernel proof pair, both halves now built:

artifacts/swreq/SWREQ-FALCON-OCI-P01.yaml

@@ -2,7 +2,7 @@ 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
+    status: verified
     release: falcon-v1.129.0
     description: >
       The verified flight components shall be consumable by the system

artifacts/verification/FV-FALCON-MATHF32-005.yaml

@@ -0,0 +1,52 @@
+artifacts:
+  - id: FV-FALCON-MATHF32-005
+    type: sw-verification
+    title: "MATHF32-P05 — machine-checked rounding + approximation bounds for the f32 cosine kernel (v1.129)"
+    status: verified
+    release: falcon-v1.129.0
+    description: >
+      Verification of SWREQ-FALCON-MATHF32-P05, the cosine analogue of the sine
+      proof pair. Both halves are MACHINE-CHECKED and CI-enforced:
+
+      ROUNDING (Gappa -> Flocq/Rocq -> coqc): 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
+      versus the sine's 2^-24 is the additional `1 - 0.5*z` subtraction.
+      Non-vacuous: coqc ACCEPTS 1b-23 and REJECTS 1b-28.
+
+      APPROXIMATION (Coq-Interval -> coqc): the exact polynomial is within 1e-9
+      of true cosine over the same range. proofs/rocq/cos_approx.v, via the
+      `interval` tactic (i_bisect, i_taylor, i_degree 18) kernel-checked by the
+      withPackages coqc (rules_rocq_rust#43). Non-vacuous: proves 1e-9, FAILS
+      1e-10 even at i_degree 20 (and 1e-11 at i_degree 22).
+
+      Neither tool's own success is trusted — the coqc kernel-check is the
+      evidence (rivet CC-002). Both proofs run under the required
+      .github/workflows/rocq.yml gate (bazel test //proofs/rocq:all
+      //proofs/gappa:all), which includes cos_approx_test and
+      cos_poly_rounding_test, so they cannot rot silently. The Rocq + Gappa
+      gate ran and PASSED on the merge of #320, confirming the kernel-check on
+      CI infrastructure, not only locally.
+
+      COMPOSABILITY: 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 layers compose by triangle inequality.
+      Observation worth recording: 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 (honest): this verifies the two INGREDIENTS. The reduced-range
+      COMPOSITION (one kernel-checked |computed - cos r| <= 2^-23 + 1e-9 lemma)
+      and the Cody-Waite argument-reduction cancellation are scoped follow-ons
+      (P06), NOT verified here.
+    tags: [verification, falcon, relay-math, gappa, coq-interval, machine-checked, v1.129]
+    fields:
+      method: formal-verification
+      steps:
+        - run: bazel test //proofs/gappa:cos_poly_rounding_test
+        - run: bazel test //proofs/rocq:cos_approx_test
+        - run: bazel test //proofs/rocq:all //proofs/gappa:all
+    links:
+      - type: verifies
+        target: SWREQ-FALCON-MATHF32-P05

artifacts/verification/FV-FALCON-OCI-001.yaml

@@ -0,0 +1,68 @@
+artifacts:
+  - id: FV-FALCON-OCI-001
+    type: sw-verification
+    title: "OCI-P01 — signed per-component publish, WASI-free build, and through-wasm closed-loop proof (v1.129)"
+    status: verified
+    release: falcon-v1.129.0
+    description: >
+      Verification of SWREQ-FALCON-OCI-P01, the jess consumption contract
+      (jess#167 / DD-026). All three required properties are evidenced:
+
+      (a) DISTRIBUTION — .github/workflows/release.yml publishes each cascade
+      stage (flight, iekf, position, attitude, rate, mixer) to
+      ghcr.io/<owner>/falcon-<stage> on every tagged release via `wkg oci push`
+      (Component-Model OCI media type, not a generic blob), cosign-signed by
+      IMMUTABLE DIGEST, plus a :latest discovery tag that is deliberately left
+      unsigned. VALIDATED END-TO-END on the falcon-v1.127.0 and falcon-v1.128.0
+      releases: the push step's real conclusion was `success` (it is
+      continue-on-error, so the step conclusion — not the run conclusion — is
+      the evidence), and the published package was confirmed ANONYMOUSLY
+      pullable with config media type application/vnd.wasm.config.v0+json and a
+      cosign .sig tag present. Each component carries the embedded metadata
+      contract (description/license/source/keywords) that wasm.directory renders;
+      the `pulseengine` namespace is live and indexed.
+
+      (b) LOWERABLE (no WASI) — the rate component is built `no_std` on the
+      cargo-component path (single-threaded statics replacing thread_local!,
+      lol_alloc global allocator, panic handler), all gated to
+      not(feature = "bazel-bindings"). VERIFIED by disassembly: imports dropped
+      from 10 (incl. every wasi:* interface) to exactly ONE —
+      `import falcon:cascade/types@0.7.0` — with `export falcon:cascade/rate`.
+      Independently corroborated by jess's per-stage lowering sweep, in which
+      the (already WASI-free) mixer stage lowered to the Cortex-M7 with 0 skips,
+      0 external symbols and 0 WASI.
+
+      (c) LOOP-COMPLETE EVIDENCE — tests/rate-loop-proof is a WASI-less wasmtime
+      host that closes the control loop THROUGH the component's own WIT seam:
+      plant (omega_dot = torque / inertia) -> gyro into vehicle-state ->
+      rate.tick across the wasm boundary -> torque -> plant. Result: the body
+      rate tracks a 1 rad/s step, converging at 0.193 s with steady-state
+      |err| 0.0059 rad/s < 0.01 (I = 0.005 kg*m^2, dt = 1 ms,
+      RateGains::DEFAULT). This is the relay half of the agreed proof split and
+      is banked by jess as the SIL differential baseline for the on-target
+      (Renode) run after lowering.
+
+      SCOPE (honest): (a) is verified for the components published to date; the
+      per-component (six-ref) generalization merged in #318 and takes effect on
+      the next tagged release. (b) is verified for the rate component; the other
+      stages still link std and carry WASI imports until each receives the same
+      conversion — the pattern is proven and mechanical, and jess's per-stage
+      skip report prioritizes the order. Nothing here claims on-target lowering:
+      that is jess's half of the split.
+    tags: [verification, falcon, oci, wasm, component-model, jess-contract, v1.129]
+    fields:
+      method: test
+      steps:
+        # bench-only: cargo-component + wasm-tools + wasmtime are not installed
+        # in the verification-gate runner, and rate-loop-proof is a STANDALONE
+        # crate (its own [workspace], so wasmtime does not join the root
+        # workspace) — it cannot be addressed as `-p rate-loop-proof` from the
+        # repo root. Each step is the exact command that produced the recorded
+        # evidence; the CI-enforced half of this requirement is the release
+        # workflow's own publish + guard steps.
+        - run: "cd wasm/cm/rate && cargo component build --release --no-default-features  # bench-only"
+        - run: "wasm-tools component wit falcon_rate_cm.wasm  # bench-only: expect 1 import (falcon:cascade/types), no wasi:*"
+        - run: "cd tests/rate-loop-proof && cargo run --release -- \"$(find ../../wasm/cm/rate/target /Volumes/*/cargo-target -name falcon_rate_cm.wasm 2>/dev/null | head -1)\"  # bench-only: closed loop through the wasm seam"
+    links:
+      - type: verifies
+        target: SWREQ-FALCON-OCI-P01

scripts/run-falcon-verification.py

@@ -99,6 +99,9 @@
     # v1.56 — the component-bundle build scripts wrap `cargo component` (absent
     # on the gate runner); same bench-tool rationale as the cargo-component line.
     re.compile(r"\bbuild-(flight-)?components?\.sh\b"),
+    re.compile(r"\bwasm-tools\b"),                   # wasm-tools not on the gate runner
+    re.compile(r"\bcargo\s+component\b"),             # cargo-component (wasm32-wasip2) not provisioned
+    re.compile(r"\brate-loop-proof\b"),               # standalone crate; needs a pre-built .wasm argument
     re.compile(r"\bwasmtime\b"),
     re.compile(r"\bwasmtime-flight-test\b"),
 ]