Repository navigation
proof(agda): model the speculative CAS + cancel-token race; replace the trivial cancellation-safety lemma - #470
Conversation
cargo audit fails on rmcp 3.5.0 (crates/echidna-mcp) with RUSTSEC-2026-0457 (fixed >=3.7.0), RUSTSEC-2026-0461 (>=3.6.0) and RUSTSEC-2026-0462 (>=3.9.0), published after main last passed the Dependency audit check. `cargo update -p rmcp` moves rmcp and rmcp-macros to 3.9.0, inside the existing "3" requirement; no other entry changes. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019a95kk88TZ1iegsBK3kox3
`cargo fmt --check` fails on main (2ab7574) in five places in src/rust/proof_search.rs, so rust-ci 'Cargo check + clippy + fmt' is red on every PR. Formatting only; no code change. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019a95kk88TZ1iegsBK3kox3
Hypatia's code_safety/zig_ptr_cast and zig_align_cast now flag the nine `@ptrCast(@aligncast(raw))` lines in src/zig_ffi/chapel_bridge.zig and src/zig_ffi/runtime_owner.zig as high, and the governance Hypatia baseline gate is red on main (2ab7574) as a result. Each of those lines recovers a callback's own `*@this()` from the type-erased `*anyopaque` it was registered with (runtime_owner.Work .context, or a std.mem.Allocator vtable's ptr), so the cast restores the original type and alignment. Fixed at source with a reasoned inline `hypatia: allow` per rule on each line, as the scanner documents, rather than a baseline entry. No code change: comments only. Checked by simulating ScannerSuppression.inline_allowed?/4 and directive_re at hypatia 82396d81 (the CI pin): 18 unsuppressed findings on main, 0 with this change. The scanner itself could not be built here (hex.pm is unreachable). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019a95kk88TZ1iegsBK3kox3
…oof-search' into claude/new-session-th4e9w-rustsec-rmcp
…st-audit' into claude/new-session-th4e9w-rustsec-rmcp
…he trivial cancellation-safety lemma The proof audit found ParallelSoundness weaker than its citations: `cancellation-safety : IsTrue (speculative (true ∷ bs))` held by `tt` (`true ∨ x = true`), covered only index 0 and modelled no CAS, token or interleaving, yet CLAUDE.md, the Chapel source and the L2.3 decision record cited it as the preemption proof. Layer B adds a small-step model of parallelProofSearchSpeculativeTelemetry: events `done i` (a prover returns; a prover that sees the token reports the preempted result) and `signal` (the CAS winner's cancel write), run over every interleaving. Proved for every schedule and any winner index: race-sound, winner-stable, preempted-inert, cancel-after-win, race-complete, winner-is-first, and race-agrees (with every prover finishing, "a winner exists" iff the any-true aggregation of layer A). Assumed boundary, stated in the header: sequentially consistent atomics, tryProver reports success=false once it observes the token, and coforall joins before the read. Checked with `agda --safe --without-K --cubical-compatible` on Agda 2.6.3 + stdlib 1.7.3 (the dogfood-proofs-ci profile): exit 0, zero postulates. Mutation check: a cancel write without a winner breaks the invariant, and a CAS that overwrites a winner breaks winner-stable; both fail to type-check. CLAUDE.md, the Chapel comment and the bench README now name the real theorems; the 2026-05-30 decision record gets a superseding note. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019a95kk88TZ1iegsBK3kox3
|
Warning Review limit reachedYou've used all free OSS reviews for now. Wait for the free limit to reset to keep reviewing this public repository. Next included review available in 7 minutes. View limit details
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. |
…c-rmcp' into claude/new-session-th4e9w-parallel-race-model
|
The proof gates for this change already pass on Generated by Claude Code |
`provers::chuffed::tests::version_rejects_failed_empty_or_stderr_only_help` failed in CI with "Failed to execute fzn-chuffed --help: Text file busy (os error 26)". The fixtures wrote a script and executed it at once. A fork on another test thread, taken while the write descriptor was open, keeps a copy until that child execs, and the kernel refuses to execute a file with a writer. New provers::test_fixture::write_executable creates the script with mode 0700, closes it, then runs it with a sentinel argument until the kernel accepts the exec. After one successful exec no writer remains and no later fork can inherit one. The chuffed, faial, gpuverify and version_probe fixtures use it; each fixture exits 64 on an unexpected argument, so the probe runs no fixture body. Also carries the rustfmt fix to proof_search.rs from #465, identical to it, so `cargo fmt --check` is green here. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019a95kk88TZ1iegsBK3kox3
…y-fixture' into claude/new-session-th4e9w-parallel-race-model
|
The cause is a race in four test fixtures that execute a script they have just written, while other test threads fork. The fix is in #487: a shared helper waits until the kernel will execute the fixture. I merged it into this branch as 256d025, so CI reruns with it. Once #487 lands, that merge leaves no change on Generated by Claude Code |
Codex Review Summary: ❌ FailedThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
|
This security review couldn’t start because the paying account has exhausted its Codex allowance and has insufficient available credits. The payer can check their balance and add credits in the Codex usage dashboard, then try again. If you do not manage the paying account, contact this repository's admins. |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 256d0256f5
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
Review on #470: in Chapel, tryProver's return and the CAS are separate statements, so a prover can return successfully, be descheduled and lose the CAS to one that returned later. The model's done i event is that prover's CAS attempt, the linearisation point. The gap before it changes nothing visible to other provers (results[i] and attempted[i] are its own slots, read only after the join), so it is just a later done i. The proofs are unchanged. The header, the theorem comments and the CLAUDE.md summary now say "first successful prover to reach the CAS", not "first successful finisher", which the code does not guarantee. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019a95kk88TZ1iegsBK3kox3
|
This security review couldn’t start because the paying account has exhausted its Codex allowance and has insufficient available credits. The payer can check their balance and add credits in the Codex usage dashboard, then try again. If you do not manage the paying account, contact this repository's admins. |
|
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 50ccfc0eb2
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| run : {n : ℕ} → Vec Bool n → State n → List (Event n) → State n | ||
| run rs s [] = s | ||
| run rs s (e ∷ es) = run rs (step rs s e) es |
There was a problem hiding this comment.
Because run accepts any event list without a trace-validity condition, it admits complete-looking schedules where a successful done installs a winner but no signal ever occurs, even after every prover has a done event. Such a schedule cannot be a completed Chapel execution: the CAS winner executes cancelToken.cancelled.write(true) before its coforall task can finish. Consequently the model proves only that cancellation implies a winner, not that a winner eventually triggers cancellation, leaving the advertised cancel-token/preemption behavior outside the proof; encode a pending signal in the state or restrict the theorems to valid schedules.
Useful? React with 👍 / 👎.
![github-advanced-security[bot]](https://avatars.githubusercontent.com/in/57789?s=60&v=4){kind=small}
| Err(error) if error.kind() == ErrorKind::ExecutableFileBusy => { | ||
| std::thread::sleep(Duration::from_millis(10)); | ||
| }, | ||
| Err(error) => panic!("fixture executable cannot run: {error}"), |
| .create_new(true) | ||
| .mode(0o700) | ||
| .open(path) | ||
| .expect("create fixture executable"); |
…ts (#487) ## Problem `rust-ci / Cargo test` failed intermittently with: ``` provers::chuffed::tests::version_rejects_failed_empty_or_stderr_only_help Failed to execute fzn-chuffed --help: Text file busy (os error 26) ``` It failed on #470, whose diff contains no Rust, and earlier in llvm-cov. The cause is a real race, not a flake. Four fixtures (chuffed, faial, gpuverify and version_probe) each write a shell script and execute it at once. If another test thread forks while the write descriptor is still open, the child keeps a copy of it until it reaches `exec` (Rust opens files close-on-exec). While any writer exists, the kernel refuses to execute the file with `ETXTBSY`. ## Fix New test-only helper, `provers::test_fixture::write_executable` (`cfg(all(test, unix))`). It: 1. creates the script with mode `0700` and closes it; 2. runs it with a sentinel argument until the kernel accepts the `exec` (up to 2 s, then it panics). After one successful `exec`, no writer remains and no later fork can inherit one, so the test's own spawn cannot hit `ETXTBSY`. Every fixture script exits 64 on an unexpected argument, so the probe never runs a fixture body. The four fixtures now use the helper. The PR also carries #465's rustfmt fix to `proof_search.rs`, byte-identical to it, so `cargo fmt --check` is green here as well. ## Checks run locally - `cargo test --lib -- provers::chuffed provers::faial provers::gpuverify provers::version_probe`: 58 passed. - `cargo clippy --lib --tests -- -D warnings`: clean. - `cargo fmt --check`: clean. Once this is open, I'll port it into the open PRs that hit the race (starting with #470). --- _Generated by [Claude Code](https://claude.ai/code/session_019a95kk88TZ1iegsBK3kox3)_ --------- Signed-off-by: Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com> Co-authored-by: Claude <noreply@anthropic.com>
… relabel the two corpus files (#471) ## Summary The 2026-11-09 proof audit found that E9 ("proof composition soundness") is evidenced by two files that don't prove it: - `proofs/agda/ProofComposition.agda` proves that list append is associative. - `proofs/agda/SoundnessPreservation.agda`'s `compose-sound` takes a `Conflicts` hypothesis and never uses it. It reduces to `a ≡ true → b ≡ true → a ∧ b ≡ true`. PROOF-STATUS R6 nevertheless called this evidence "good, merely misfiled". The owner asked for the proof to be strengthened directly. Companion to #470, which does the same for `ParallelSoundness`. ## Changes - **New `meta-checker/src/Echidna/Composition.agda`.** Theory over an arbitrary logic: formulae, models and satisfaction are module parameters, not postulates. - **`cut`:** composition preserves semantic soundness, using both premises. - **`weaken-left` / `weaken-right`:** adding axioms on either side preserves entailment. - **`explosion`:** inconsistent axioms entail every formula. So soundness preservation is vacuous unless there is a conflict check, which is exactly what the old file skipped. - **`compose-realised`:** with a *sound* conflict detector (no reported conflict implies the joined axioms have a model), every composite is realised. Some model satisfies all its axioms and its goal. - **`detector-must-flag`:** a sound detector cannot miss an inconsistent composition. - **`Literals`:** a concrete logic in which `pos 0` and `neg 0` clash, together with a genuine `cut` example. - **Scope:** no ECHIDNA Rust code composes proofs today, so the module states the obligation a future composer must meet and claims no implementation. - **`MetaChecker.agda`** imports the module, which puts it inside the `agda-meta-checker` closure: pinned Agda 2.7.0.1, canonical flags, fresh-interface check. - **`docs/PROOF-NEEDS.adoc` E9** now cites the new module. - **`docs/PROOF-STATUS.adoc` R6** is corrected and marked `proven` (Agda leg, pending the first CI receipt). Rocq/Lean rechecks are recorded as not started. - **`proofs/agda/ProofComposition.agda` and `SoundnessPreservation.agda`** stay where they are, as PROOF-POLICY §3 fixtures, with headers that say what they actually prove. ## RSR Quality Checklist ### Required - [x] Tests pass: the files type-check (see Testing). - [x] No banned functions: zero `postulate`, and `--safe` holds. - [x] SPDX headers are present. - [x] No secrets. ### As Applicable - [x] Documentation updated: PROOF-NEEDS, PROOF-STATUS and the corpus file headers. ## Testing - `agda --safe --without-K --cubical-compatible` on `Composition.agda`, on the full `MetaChecker.agda` closure, and on the two corpus files: exit 0 each. - These local runs use Agda 2.6.3 + stdlib 1.7.3. The pinned 2.7.0.1 + stdlib 2.1 run is the `agda-meta-checker` job's, because this environment can't install the pinned toolchain. - The new module imports only `Data.Bool`, `Data.Nat`, `Data.List`, `Data.Product`, `Data.Empty`, `Relation.Nullary` and `Relation.Binary.PropositionalEquality`, which have the same names in both stdlib versions. - **Mutation check:** replacing `SoundDetector` with a trivial property makes `compose-realised` fail to type-check, so the detector's soundness is load-bearing. --- _Generated by [Claude Code](https://claude.ai/code/session_019a95kk88TZ1iegsBK3kox3)_ --------- Co-authored-by: Claude <noreply@anthropic.com>
Summary
The proof audit of 2026-11-09 found
proofs/agda/ParallelSoundness.agdamuch weaker than the places that cite it.CLAUDE.md, the Chapel source and the L2.3 decision record all present it as the preemption proof. But the lemma was:That holds by definition (
true ∨ x = true). It covers index 0 only, and models no compare-and-swap, no cancel token and no interleaving. The owner asked for the proof to be strengthened directly, not relabelled.Changes
ParallelSoundness.agdaLayer A keeps the any-true aggregation, with soundness and completeness. Its header now says plainly that on its own this is not a concurrency result.
Layer B (new) is a small-step model of
parallelProofSearchSpeculativeTelemetry. It has two kinds of event, and runs over every interleaving of them:done i: proveri'stryProverreturns. A prover that has seen the token reports the preempted result. Otherwise it reports its outcome and attempts the CASwinnerIdx: -1 → i.signal: the CAS winner'scancelToken.cancelled.write(true), kept as a separate event so that every interleaving of the CAS and the cancel write is covered.Proved for every schedule and any winner index:
race-soundwinner-stablepreempted-inertcancel-after-winrace-completewinner-is-firstrace-agrees/race-agrees-soundWorked examples: index 2 winning a two-success race; a success that loses the CAS before the cancel write; the case with no successes.
Assumed boundary, stated in the header:
tryProverreturnssuccess = falseonce it observes the token.coforalljoins every task beforewinnerIdx.read().CLAUDE.mdChapel bullet, the comment insrc/chapel/parallel_proof_search.chpl, anddocs/bench/README.adoc.docs/decisions/2026-05-30-chapel-l23-cancel-token.adocgets a superseding note; the original record is left as written.RSR Quality Checklist
Required
postulate,believe_meoradmit, and--safeholds.As Applicable
CLAUDE.md, the bench README, the decision record and the Chapel comment.Testing
agda --safe --without-K --cubical-compatible ParallelSoundness.agdaon Agda 2.6.3 with stdlib 1.7.3, which is thedogfood-proofs-ci/just proofs-agdaprofile: exit 0. The only warnings are Cubical "not yet supported" notes, as before.signalled nothing c = true) breaks the invariant;cas (just w) i = just i) breakswinner-stable.The ProofComposition / SoundnessPreservation (E9) weaknesses from the same audit come in a separate PR.
Generated by Claude Code