From d1bbb9d09965ad2660f24b7a7c80602c29139c18 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 29 Jul 2026 11:01:13 +0200 Subject: [PATCH 1/3] =?UTF-8?q?verify(falcon):=20v1.129=20=E2=86=92=20P05?= =?UTF-8?q?=20+=20OCI-P01=20verified=20(cos=20proof=20pair,=20component=20?= =?UTF-8?q?publish)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Two-commit rule, second commit (code-free). The implementations landed in #320 (cos approximation proof + OCI trace), #318 (per-component publish), #314 (WASI-free rate + through-wasm closed-loop proof), with the Rocq + Gappa gate green on CI. This promotes both requirements to `verified` and adds their verification artifacts. FV-FALCON-MATHF32-005 (verifies P05) — the cosine proof pair, both halves machine-checked and CI-enforced: rounding <= 2^-23 (Gappa, rejects 1b-28) and approximation <= 1e-9 (Coq-Interval, fails 1e-10 at i_degree 20). Coefficients byte-identical between them, so the layers compose. Records that the cosine core is ~10x more accurate than the sine core because cos_poly carries the exact `1 - 0.5*z` terms and only fits the residual. FV-FALCON-OCI-001 (verifies OCI-P01) — the jess consumption contract: (a) per-component signed publish, validated end-to-end on v1.127/v1.128 (the continue-on-error step's REAL conclusion, plus an anonymous pull confirming the wasm config media type and .sig tag); (b) WASI-free build, verified by disassembly (10 imports -> 1, no wasi:*) and corroborated by jess's mixer stage lowering with 0 skips/0 WASI; (c) loop-complete evidence — the loop closes THROUGH the wasm seam (converges 0.193 s, |err| 0.0059 rad/s), banked by jess as the SIL differential baseline. Both artifacts state their scope honestly: P05 delivers the two ingredients, not the composition (P06); OCI-P01's WASI-free property is verified for `rate`, with the other stages pending the same mechanical conversion. rivet validate: PASS. No source changes. Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG --- artifacts/swreq/SWREQ-FALCON-MATHF32-P05.yaml | 2 +- artifacts/swreq/SWREQ-FALCON-OCI-P01.yaml | 2 +- .../verification/FV-FALCON-MATHF32-005.yaml | 52 ++++++++++++++++ artifacts/verification/FV-FALCON-OCI-001.yaml | 61 +++++++++++++++++++ 4 files changed, 115 insertions(+), 2 deletions(-) create mode 100644 artifacts/verification/FV-FALCON-MATHF32-005.yaml create mode 100644 artifacts/verification/FV-FALCON-OCI-001.yaml diff --git a/artifacts/swreq/SWREQ-FALCON-MATHF32-P05.yaml b/artifacts/swreq/SWREQ-FALCON-MATHF32-P05.yaml index 0a1c24a..99b08b4 100644 --- a/artifacts/swreq/SWREQ-FALCON-MATHF32-P05.yaml +++ b/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: diff --git a/artifacts/swreq/SWREQ-FALCON-OCI-P01.yaml b/artifacts/swreq/SWREQ-FALCON-OCI-P01.yaml index d47d268..e529cde 100644 --- a/artifacts/swreq/SWREQ-FALCON-OCI-P01.yaml +++ b/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 diff --git a/artifacts/verification/FV-FALCON-MATHF32-005.yaml b/artifacts/verification/FV-FALCON-MATHF32-005.yaml new file mode 100644 index 0000000..6c3ab34 --- /dev/null +++ b/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 diff --git a/artifacts/verification/FV-FALCON-OCI-001.yaml b/artifacts/verification/FV-FALCON-OCI-001.yaml new file mode 100644 index 0000000..0256523 --- /dev/null +++ b/artifacts/verification/FV-FALCON-OCI-001.yaml @@ -0,0 +1,61 @@ +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//falcon- 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: + - run: cargo component build --release --no-default-features # wasm/cm/rate + - run: wasm-tools component wit falcon_rate_cm.wasm # expect 1 import, no wasi:* + - run: cargo run --release -p rate-loop-proof -- falcon_rate_cm.wasm + links: + - type: verifies + target: SWREQ-FALCON-OCI-P01 From 63b4b83f95774396db99f4cdbbe3c77e6d70e993 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 29 Jul 2026 12:18:36 +0200 Subject: [PATCH 2/3] fix(verify): make FV-FALCON-OCI-001's cited steps actually runnable MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The verification gate correctly rejected this artifact: error: package(s) `rate-loop-proof` not found in workspace tests/rate-loop-proof is a STANDALONE crate (its own [workspace], so pulling in wasmtime does not bloat the root workspace), so `cargo run -p rate-loop-proof` cannot resolve from the repo root. Cite the runnable `cd && ...` form instead, and mark the three steps `# bench-only` — cargo-component, wasm-tools and wasmtime are not installed on the gate runner, and the loop proof needs a pre-built .wasm argument the gate cannot supply. 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. Caught by the gate, not by me — exactly the "verify every cited command actually runs" discipline. (The P05 artifact's bazel targets were separately confirmed present in proofs/{rocq,gappa}/BUILD.bazel.) rivet validate: PASS. Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG --- artifacts/verification/FV-FALCON-OCI-001.yaml | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) diff --git a/artifacts/verification/FV-FALCON-OCI-001.yaml b/artifacts/verification/FV-FALCON-OCI-001.yaml index 0256523..1b2823f 100644 --- a/artifacts/verification/FV-FALCON-OCI-001.yaml +++ b/artifacts/verification/FV-FALCON-OCI-001.yaml @@ -53,9 +53,16 @@ artifacts: fields: method: test steps: - - run: cargo component build --release --no-default-features # wasm/cm/rate - - run: wasm-tools component wit falcon_rate_cm.wasm # expect 1 import, no wasi:* - - run: cargo run --release -p rate-loop-proof -- falcon_rate_cm.wasm + # 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 -- /falcon_rate_cm.wasm # bench-only: closed loop through the wasm seam" links: - type: verifies target: SWREQ-FALCON-OCI-P01 From 2f493fccf0e662e96f6eff5b04824b990a121c18 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 29 Jul 2026 13:09:47 +0200 Subject: [PATCH 3/3] fix(verify): teach the gate that wasm-tools/cargo-component/rate-loop-proof are bench-only MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Second gate rejection, second real bug of mine — and it corrected a wrong assumption: I marked the OCI evidence steps `# bench-only` expecting the comment to be honoured, but the runner explicitly does NOT read that marker ("rivet strips shell `# bench-only` comments at the YAML->JSON boundary, so we identify bench-only steps by command shape"). It matches BENCH_PATTERNS by command shape, and the list is designed to be extended as new infra-needs appear. So the gate ran them anyway: `wasm-tools: not found`, `cannot open path-to`. - scripts/run-falcon-verification.py: add three patterns for tools the gate runner genuinely lacks — `wasm-tools`, `cargo component` (wasm32-wasip2), and `rate-loop-proof` (a standalone crate whose proof needs a pre-built .wasm argument the gate cannot supply). Verified all three cited commands now match. - FV-FALCON-OCI-001: replace the `` placeholder with a real copy-pasteable command (it is the recorded evidence; a placeholder that cannot run anywhere is not evidence). Two-commit rule unaffected: the independence check scopes "implementation" to .rs files under crates/ and examples/; this is gate tooling. rivet validate: PASS. Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG --- artifacts/verification/FV-FALCON-OCI-001.yaml | 2 +- scripts/run-falcon-verification.py | 3 +++ 2 files changed, 4 insertions(+), 1 deletion(-) diff --git a/artifacts/verification/FV-FALCON-OCI-001.yaml b/artifacts/verification/FV-FALCON-OCI-001.yaml index 1b2823f..52d9c95 100644 --- a/artifacts/verification/FV-FALCON-OCI-001.yaml +++ b/artifacts/verification/FV-FALCON-OCI-001.yaml @@ -62,7 +62,7 @@ artifacts: # 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 -- /falcon_rate_cm.wasm # bench-only: closed loop through the wasm seam" + - 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 diff --git a/scripts/run-falcon-verification.py b/scripts/run-falcon-verification.py index 44e678b..541107b 100755 --- a/scripts/run-falcon-verification.py +++ b/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"), ]