verify(falcon): v1.129 → P05 + OCI-P01 verified - #322
Merged
Conversation
…onent publish) 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 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG
avrabe
enabled auto-merge (squash)
July 29, 2026 09:01
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 <dir> && ...` 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 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG
…-proof are bench-only
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 `<path-to>` 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 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Two-commit rule — the code-free verify half of v1.129
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 PR contains no source changes — it promotes the two requirements to
verifiedand adds their verification artifacts.FV-FALCON-MATHF32-005→ verifies P05 (the cosine proof pair)i_degree 20Coefficients byte-identical between the two proofs → the layers compose. Both run under the required
rocq.ymlgate. Notes the finding that cosine is ~10× more accurate than sine (exact1 − 0.5·zterms, only the residual is fitted).FV-FALCON-OCI-001→ verifies OCI-P01 (the jess contract)continue-on-error, so the run being green is not the evidence) plus an anonymous pull confirmingvnd.wasm.config.v0+jsonand the.sigtag.wasi:*. Corroborated by jess's sweep, where the mixer stage lowered to the M7 with 0 skips / 0 WASI.Honest scope (in both artifacts)
P05 delivers the two ingredients, not the composition (P06). OCI-P01's WASI-free property is verified for
rate; the other stages still linkstduntil each gets the same mechanical conversion.rivet validate: PASS. All four artifacts in thefalcon-v1.129.0scope are nowverified— the release is cuttable.🤖 Generated with Claude Code