feat(math): machine-checked cos approximation bound (MATHF32-P05) + trace the OCI arc - #320
Merged
Conversation
…race the OCI arc
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 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG
avrabe
enabled auto-merge (squash)
July 29, 2026 04:06
avrabe
added a commit
that referenced
this pull request
Jul 29, 2026
* verify(falcon): v1.129 → P05 + OCI-P01 verified (cos proof pair, component 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 * fix(verify): make FV-FALCON-OCI-001's cited steps actually runnable 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 * fix(verify): teach the gate that wasm-tools/cargo-component/rate-loop-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 --------- Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
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.
v1.129, planned in rivet before building. The plan surfaced that P05 was half-built and that a whole shipped arc was untraced — both addressed here.
1. Cos approximation proof (the missing half of P05)
The rounding half already shipped (
proofs/gappa/cos_poly_rounding.gappa, ≤ 2⁻²³) but was untraced; the approximation half didn't exist.proofs/rocq/cos_approx.vnow proves, kernel-checked by coqc via Coq-Interval:C1 = 0x1.55554a0p-5,C2 = -0x1.6c0c340p-10,C3 = 0x1.99eb9c0p-16) →Ecos = Qas real functions, so the two layers compose by triangle inequality. Same correctness gate as the sine pair — different coefficients wouldn't chain.1e-9ati_degree 18, fails1e-10even ati_degree 20(1e-11fails at 22).rocq.ymlgate via//proofs/rocq:all;bazel test //proofs/rocq:cos_approx_testPASSED locally in relay's own bazel.cos_polycarries the exact1 − 0.5·zterms and only fits the residual.Scope, narrowed like P04: delivers the two ingredients. The reduced-range composition lemma stays P06. Status →
implemented(two-commit rule; promotion is a separate code-free PR).2. Trace the OCI arc (
SWREQ-FALCON-OCI-P01, new)The falcon-rate WASI-free conversion (#314), the through-wasm closed-loop proof, and the per-component OCI publish (#318) all shipped with zero rivet artifacts — untracked work is invisible to the release plan and resurfaces as a gate surprise. This records the three required properties and ties them to the jess consumption contract (jess#167 / DD-026):
falcon-<stage>OCI refs, Component-Model media type, cosign by immutable digest, metadata contract;rivet validate: PASS.🤖 Generated with Claude Code