Repository navigation
proof(agda): real E9 composition soundness in the gated meta-checker; relabel the two corpus files - #471
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
… relabel the two corpus files
The proof audit found E9 ("proof composition soundness") evidenced by
two corpus files that do not prove it: ProofComposition.agda proves
list-append associativity, and SoundnessPreservation.agda's compose-sound
discharges a Bool flag with `∧` while ignoring its Conflicts hypothesis.
PROOF-STATUS R6 called that evidence "good, merely misfiled".
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), weakening, explosion (inconsistent axioms entail everything,
so soundness preservation is vacuous without a conflict check),
compose-realised (a sound conflict detector makes every composite
realised), detector-must-flag, and a concrete literal logic where pos 0
and neg 0 clash and entail an unrelated goal. It is imported by
MetaChecker.agda, so agda-meta-checker (pinned Agda 2.7.0.1, canonical
flags) gates it. No Rust code composes proofs; none is claimed.
PROOF-NEEDS E9 now cites the new module; PROOF-STATUS R6 is corrected.
The two corpus files keep their place as §3 fixtures with headers that
say what they actually prove.
Checked locally with agda --safe --without-K --cubical-compatible on
Agda 2.6.3 + stdlib 1.7.3: Composition and the full MetaChecker closure
exit 0. The pinned 2.7.0.1 run is CI's. Mutation check: replacing
SoundDetector with a trivial property makes compose-realised fail.
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 22 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-e9-composition
|
Generated by Claude Code |
The owner chose #477's reading of PROOF-POLICY §1 for the split. Generic theory (Receipt; E9 composition in #471) stays in Agda. Echidna-specific statements are verified on the Rust with Creusot/Pearlite and Verus, not restated in Idris 2. Each meta-checker module retires once its Rust contracts carry a receipt. R1 now points at #477's trust kernel as the first Creusot target. R10 has no Rust target (there is no clamp_trust), so it retires with its module. The Lean re-homing note distinguishes Rust behaviour (Creusot/Verus) from API/ABI properties (Idris 2). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015jzCHZx4Rt65NDaGLDrjLp
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. |
![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: 50d22e0ed8
ℹ️ 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 #471 (Codex): - Composition.agda: for an arbitrary Set-valued Conflicts relation the old detector-must-flag gave only ¬¬ Conflicts, not a reportable witness. It is renamed detector-cannot-miss and kept, and a new detector-must-flag takes a decision procedure (Dec) and returns the Conflicts witness itself. MetaChecker, PROOF-NEEDS E9 and R6 say so. - scripts/ci/check-agda.sh: the agda-meta-checker job now prints a source-bound receipt (toolchain, flags, library descriptors, SHA-256 of every source), so a CI run can stand as the receipt PROOF-POLICY §8 needs. - PROOF-STATUS R6: argued, not proven, until that job's receipt on main exists. The local check used Agda 2.6.3, not the pin. - PROOF-STATUS R4: records that MetaChecker.agda now imports Composition (ten modules). The nine receipted modules are unchanged, so the row stands for them; the new entrypoint digest awaits the same CI receipt. - The "Not obligations" note no longer describes R6 as a corpus placement defect; R6 cites the meta-checker module and the corpus files disclaim E9. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019a95kk88TZ1iegsBK3kox3
|
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 9f1eec111f
ℹ️ 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".
|
|
||
| # Source-bound receipt (PROOF-POLICY §8): toolchain, flags and the SHA-256 of | ||
| # every first-party source and library descriptor this run checked. | ||
| echo "receipt: $version; commit ${GITHUB_SHA:-$(git -C "$repo_root" rev-parse HEAD)}" |
There was a problem hiding this comment.
On pull_request runs, the workflow checks out github.event.pull_request.head.sha, while GitHub defines GITHUB_SHA for this event as the pull request's merge-branch commit. Because GITHUB_SHA is set, the fallback never runs and the new receipt attributes the checked source hashes to a different commit. Use the checked-out HEAD (or pass the checkout ref explicitly) so archived PR receipts have accurate provenance.
Useful? React with 👍 / 👎.
| |Soundness preservation, axiom conflict detection |Agda | ||
| |E9 Proof composition soundness |`+meta-checker/src/Echidna/Composition.agda+` | ||
| |Cut preserves semantic soundness; explosion shows a conflict check is | ||
| load-bearing; a sound detector realises every composite, and a sound |
There was a problem hiding this comment.
The new theorem does not show that a sound detector realises every composite: compose-realised additionally requires ¬ Conflicts Γ₁ Γ₂. For a composite the detector flags—especially the inconsistent example introduced in this module—that premise is unavailable and no common model can exist. Describe this as realising every unflagged composite so the authoritative proof narrative matches the theorem.
Useful? React with 👍 / 👎.
…ROOF-POLICY §1.2/§8 (#482) ## Summary The 2026-11-09 proof audit found `docs/PROOF-STATUS.adoc` out of date in two ways. Some rows don't match the CI receipts, and the ledger predates the PROOF-POLICY changes of 2026-11-04 (§8, Proof Witness Grades) and 2026-11-07 (§1.2: Creusot, Pearlite and Verus as the default Rust toolset). This PR brings it into line. It only changes documentation: proof sources and CI are untouched. ## Changes - **R2, Idris 2 ABI and verification:** `argued` → `proven`. - Cites the green `Idris2 (verification)` and `Type-check Idris2 ABI definitions` runs on `a2a8643`, whose `verification/` and `src/abi/` trees are byte-identical to `main` `2ab7574` (checked with `git diff`). - Names the nine files at the `src/abi/` root that sit outside the package. - Points to #472 for `CapnSchemas`. - **R3, Lean:** - The 2026-05-18 note "all five fail to compile" is stale. `Lean 4 (verification)` builds all five on the pinned 4.13.0, and `#print axioms` shows no `sorryAx`. The Lean leg is now `proven`. - **Still open, as an owner call:** where these proofs belong. They state properties of ECHIDNA's own types, so §1 assigns them to Idris 2 (or Creusot/Verus). No §4 exception record exists beside them, so either write those records or move the proofs. - **R1, Rust:** now maps to Creusot with Pearlite, and Verus (§1.2). It records that `crates/echidna-core-creusot` is a parallel model rather than the shipped code, and that Verus work has not started. - **R12, SPARK (new):** the four GPR projects had no row at all. The row is `open`: - no CI job runs `gnatprove`; - `Axiom_C_Bridge` (`SPARK_Mode => Off`) is recorded as an `ASSUMED` boundary. - **Grades:** the old "Mathesis Grade N" wording is replaced by the §8 `PWG-` labels. - Engineering rows carry no PWG (§8.1). - Only R11, the receipt/warrant theory theorem, is at `PWG-3`. - Nothing is higher, because no Rocq or Lean recheck has been attempted (R5). - **`CLAUDE.md`:** the proof-policy pointer now names Pearlite and Verus. The file itself requires this pointer to move whenever the mapping changes. This PR touches different rows from #471, which corrects R6, so the two should merge cleanly in either order. ## RSR Quality Checklist ### Required - [x] Documentation only; no code, proofs or CI changed. - [x] No secrets. ### As Applicable - [x] Documentation updated. ## Testing Every receipt cited is a live GitHub Actions job URL. Tree identity was checked with `git diff --quiet origin/main a2a8643 -- verification src/abi`. The SPARK facts come from `find . -name '*.gpr'`, `grep gnatprove` over the `Justfile` and workflows, and the `SPARK_Mode => Off` lines at `src/ada/spark/axiom_c_bridge.ads:23` and `.adb:16`. --- _Generated by [Claude Code](https://claude.ai/code/session_019a95kk88TZ1iegsBK3kox3)_ --------- Co-authored-by: Claude <noreply@anthropic.com>
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.agdaproves that list append is associative.proofs/agda/SoundnessPreservation.agda'scompose-soundtakes aConflictshypothesis and never uses it. It reduces toa ≡ 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
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 whichpos 0andneg 0clash, together with a genuinecutexample.MetaChecker.agdaimports the module, which puts it inside theagda-meta-checkerclosure: pinned Agda 2.7.0.1, canonical flags, fresh-interface check.docs/PROOF-NEEDS.adocE9 now cites the new module.docs/PROOF-STATUS.adocR6 is corrected and markedproven(Agda leg, pending the first CI receipt). Rocq/Lean rechecks are recorded as not started.proofs/agda/ProofComposition.agdaandSoundnessPreservation.agdastay where they are, as PROOF-POLICY §3 fixtures, with headers that say what they actually prove.RSR Quality Checklist
Required
postulate, and--safeholds.As Applicable
Testing
agda --safe --without-K --cubical-compatibleonComposition.agda, on the fullMetaChecker.agdaclosure, and on the two corpus files: exit 0 each.agda-meta-checkerjob's, because this environment can't install the pinned toolchain.Data.Bool,Data.Nat,Data.List,Data.Product,Data.Empty,Relation.NullaryandRelation.Binary.PropositionalEquality, which have the same names in both stdlib versions.SoundDetectorwith a trivial property makescompose-realisedfail to type-check, so the detector's soundness is load-bearing.Generated by Claude Code