Repository navigation
docs(proofs): refresh PROOF-STATUS against the 2026-11-09 audit and PROOF-POLICY §1.2/§8 - #482
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
…ROOF-POLICY §1.2/§8 The proof audit found the ledger behind both the receipts and the policy: - R2 (Idris 2 ABI/verification): `argued` -> `proven`, citing 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. Names the nine src/abi root files outside the package and the CapnSchemas fix (#472). - R3 (Lean): the "all five fail" record of 2026-05-18 is stale; "Lean 4 (verification)" builds all five on the pinned 4.13.0 and #print axioms shows no sorryAx. Lean leg `proven`; verifier placement stays open, because the statements are about echidna's own types and no §4 exception record exists (owner call). - R1: Rust maps to Creusot with Pearlite, and Verus (§1.2, owner ruling 2026-11-07); records that the Creusot crate is a parallel model, not the shipped code, and that Verus has not started. - New R12: the four SPARK projects had no row. `open`: no gnatprove run in CI; Axiom_C_Bridge is SPARK_Mode => Off and recorded as a boundary. - Grades: Mathesis "Grade N" replaced by §8 PWG labels; engineering rows carry no PWG (§8.1); only R11 is at PWG-3. CLAUDE.md's proof-policy pointer moves with the §1.2 mapping, as it requires. 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 20 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-proof-status-refresh
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: 0b794386d2
ℹ️ 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 #482 (Codex): - R2 said idris2-abi-ci enforces zero believe_me / assert_total / postulate. It greps src/abi/ only, for believe_me, assert_total, unsafePerformIO and prim__crash, and checks neither postulate nor verification/proofs/idris2/. The row now records the 2026-11-09 audit (no such declarations in either package) as a receipt-time audit. - R3 carried a proven token while its verifier placement is unresolved; the file says the §1 mapping decides which verifier may carry a row. R3 is open; the passing Lean build stays recorded. 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: cf1ee048ac
ℹ️ 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".
| |R2. Idris 2 interface/ABI obligations (E2, E3, E5, E6, E7, E12, Stage 8a, | ||
| VQL-UT, extensive ABI) | ||
| |`+argued+` | ||
| |`+proven+` |
There was a problem hiding this comment.
When consumers apply this authoritative token to every obligation named in R2, it marks VQL-UT query safety as fully discharged, but docs/PROOF-NEEDS.adoc:119-120 explicitly records the deeper-layer E8 VQL-UT obligation as only partially covered by VqlUt.idr. The cited receipt establishes that the package type-checks, not that the uncovered portion is complete; narrow this row to the proved L3/L5 properties or keep the aggregate obligation from being proven.
Useful? React with 👍 / 👎.
| builds `+verification/proofs/idris2/echidna-verif-proofs.ipkg+` and | ||
| https://github.com/hyperpolymath/echidna/actions/runs/42624461712/job/129184533713[Type-check Idris2 ABI definitions] | ||
| builds `+src/abi/echidnaabi.ipkg+`, both on Idris 2 0.8.0, both success. | ||
| `+%default total+`. A 2026-11-09 audit of both packages found no `+believe_me+`, |
There was a problem hiding this comment.
When R2 relies on %default total as evidence for its proven token, the claim is not true package-wide: verification/proofs/idris2/echidna-verif-proofs.ipkg includes NatLte, but verification/proofs/idris2/NatLte.idr has neither %default total nor per-definition total modifiers, and its lteLit helper feeds several of the recorded proofs. Add the directive and obtain a fresh receipt, or qualify the totality claim so the successful package build is not presented as enforcing this condition on every included module.
Useful? React with 👍 / 👎.
|
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: cf8f09d16a
ℹ️ 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".
| Grades are derived from receipts, never asserted, and are never flattened into | ||
| a percentage. See R5 and R6. |
There was a problem hiding this comment.
After replacing the Mathesis grades with PWG, this cross-reference directs readers to R5 and R6, which discuss independent rechecks and proof placement rather than percentage flattening. The applicable guidance is in R7, which still retains the obsolete Mathesis wording; point this summary to R7 and update that row to the new §5/§8 terminology so readers can locate the stated rule.
Useful? React with 👍 / 👎.
| * *Engineering proofs are not graded* (§8.1). Creusot, Verus, SPARK and Idris 2 | ||
| results, and Agda statements about ECHIDNA's own functions and types, use the | ||
| §5 tokens only. In this file that covers R1, R2, R3, R9, R10, R12 and most of | ||
| R4. A theory theorem below `+PWG-3+` is `+ungraded+`. |
There was a problem hiding this comment.
Once this paragraph classifies R9, R10, and most of R4 as engineering properties, their Agda checks cannot continue carrying proven tokens without recorded exceptions: the normative mapping assigns repository-specific engineering properties to Idris2, or to the implementation verifier when they concern Rust/Ada behavior. This commit applies that rule to keep R3 open but leaves these analogous Agda rows and the final summary marked proven; split out any genuine theory theorems and leave the engineering rows open until they are moved or receive §4 records. PROOF-POLICY §1
Useful? React with 👍 / 👎.
| https://github.com/hyperpolymath/echidna/actions/runs/42624461538/job/129184535654[Idris2 (verification)] | ||
| builds `+verification/proofs/idris2/echidna-verif-proofs.ipkg+` and | ||
| https://github.com/hyperpolymath/echidna/actions/runs/42624461712/job/129184533713[Type-check Idris2 ABI definitions] | ||
| builds `+src/abi/echidnaabi.ipkg+`, both on Idris 2 0.8.0, both success. |
There was a problem hiding this comment.
The two receipts cited for R2 come from workflows that install Idris2 through Ubuntu apt or a downloaded source archive (dogfood-proofs-ci.yml and idris2-abi-ci.yml), rather than through the repository's Guix manifest or container, but neither workflow nor this ledger records the §6 deviation required for that installation path. Under the cited policy, silence about such an out-of-band CI toolchain is explicitly noncompliant, so record the tool/version/digest and mismatch gate or obtain a compliant receipt before presenting this as a policy-conformant promotion. PROOF-POLICY §6
Useful? React with 👍 / 👎.
| shipped code. *Verus:* not started; no Verus specification or proof exists. | ||
| Row stays `+open+` until a Creusot or Verus run on shipped code yields a receipt | ||
| with a commit hash. |
There was a problem hiding this comment.
If a Creusot run succeeds while Verus remains unstarted, this next-step condition permits the aggregate R1 row to be promoted even though one member of the default Rust toolset is still pending. §1.2 requires scopes for both Creusot/Pearlite and Verus by default and says an unrun required proof remains open; split the verifier legs or require results for both unless one receives a recorded exception. PROOF-POLICY §1.2
Useful? React with 👍 / 👎.
| assigns to those statements until the placement is decided. Only theory theorems are graded (§8.1): R11 is at | ||
| `+PWG-3+`; the engineering rows carry no PWG. Every *independent* leg is still | ||
| `+open+`: R5 has never been attempted, which is why nothing here is above | ||
| `+PWG-3+`. Proven in one kernel is exactly what `+PWG-3+` means, and neither fact |
There was a problem hiding this comment.
R11 contains multiple theorem declarations, but this summary is the only place that assigns them a grade: neither the R11 row nor R5 records a per-theorem pwg, foundation_diverse, leg route, §5 token, correspondence state, or receipt-lineage state. §8.5 requires those fields for each theorem so the grade can be derived rather than asserted; add the individual records or leave these theorems ungraded. PROOF-POLICY §8.5
Useful? React with 👍 / 👎.
Summary
The 2026-11-09 proof audit found
docs/PROOF-STATUS.adocout 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
argued→proven.Idris2 (verification)andType-check Idris2 ABI definitionsruns ona2a8643, whoseverification/andsrc/abi/trees are byte-identical tomain2ab7574(checked withgit diff).src/abi/root that sit outside the package.CapnSchemas.Lean 4 (verification)builds all five on the pinned 4.13.0, and#print axiomsshows nosorryAx. The Lean leg is nowproven.crates/echidna-core-creusotis a parallel model rather than the shipped code, and that Verus work has not started.open:gnatprove;Axiom_C_Bridge(SPARK_Mode => Off) is recorded as anASSUMEDboundary.PWG-labels.PWG-3.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
As Applicable
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 fromfind . -name '*.gpr',grep gnatproveover theJustfileand workflows, and theSPARK_Mode => Offlines atsrc/ada/spark/axiom_c_bridge.ads:23and.adb:16.Generated by Claude Code