Repository navigation
test(corpus): mark the two deliberate sorry fixtures as accepted detector inputs - #480
Conversation
…ctor inputs isabelle/Smoke.thy and minif2f/algebra.lean each keep one `sorry` on purpose: corpus_hazard_fixtures asserts the adapters flag it. panic-attack reports both as Critical ProofDrift, which is the last thing failing the static analysis gate once the scanner can complete coverage (#478). An inline `panic-attack: accepted` marker on the line above each sorry records the audit beside the evidence and suppresses only that occurrence; any other sorry in either file still fails the gate. The markers take effect with the line-anchored findings in hyperpolymath/panic-attack#278; with the current scanner they are inert comments. Checked with a build of that branch, scanned from another directory: both findings are suppressed at Smoke.thy:21 and algebra.lean:11, and static-analysis-evidence.sh scan + gate pass (critical 0, total 109). Both corpus_hazard_fixtures tests and the five corpus_estate_adapters tests still pass with the annotated files. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01JHfuPCv1pEiqkQGG5DQASb
|
Important Review skippedAuto reviews are disabled on base/target branches other than the default branch. Please check the settings in the CodeRabbit UI or the
 |
…aude/compassionate-fermat-9x7vpe-fixture-markers
…aude/compassionate-fermat-9x7vpe-fixture-markers
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: af075389a6
ℹ️ 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".
| (* A lemma left open with `sorry` — the corpus adapter must flag this | ||
| as a sorry hazard. *) | ||
| lemma double_mono: "n \<le> m \<Longrightarrow> double n \<le> double m" | ||
| (* panic-attack: accepted (detector fixture: the corpus adapter must flag this sorry) *) |
There was a problem hiding this comment.
In the checked panic-attack assail workflow, PANIC_ATTACK_REF remains pinned to f2a6a70, which does not implement these line-anchored acceptance markers, so this comment is inert and the existing sorry is still reported as an unsuppressed Critical finding. Since static-analysis-evidence.sh gate rejects any nonzero Critical count, this commit cannot make the required gate pass until the workflow is updated to a scanner revision that supports the marker; the same issue applies to the marker in algebra.lean.
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Correct, and it's the known open step. The PR body lists it as pending.
I'm deliberately not pinning PANIC_ATTACK_REF to the unmerged branch commit of hyperpolymath/panic-attack#278: the gate's scanner should be a reviewed commit on panic-attack main. Once #278 merges, I'll move the pin to the merged commit in this PR and re-run the gate. Locally, a build of #278's head already suppresses both findings and static-analysis-evidence.sh gate passes with critical: 0.
Leaving this thread open until the pin moves.
Generated by Claude Code
…ionale
Codex review (P2): both corpus adapters flag a hazard with a plain
`text.contains("sorry")` over the declaration, comments included. The marker
rationale said "...must flag this sorry", so the marker alone set
axiom_usage.sorry: with the real `sorry` replaced by a finished proof,
corpus_hazard_fixtures still passed, i.e. the fixture stopped testing
anything. The rationale now reads "...must flag the unfinished proof below",
which contains none of the adapters' hazard tokens (sorry, oops, admit,
Admitted, axiom, axiomatization, consts, nitpick, quickcheck).
Checked: with the real sorry present, corpus_hazard_fixtures passes (2/2);
with it replaced by a finished proof, both tests fail on "hazard
classification" (previously both still passed). panic-attack built from
hyperpolymath/panic-attack#278 still suppresses both findings at
Smoke.thy:21 and algebra.lean:11.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01JHfuPCv1pEiqkQGG5DQASb
|
c63cff9
into
claude/compassionate-fermat-9x7vpe-scanner-pin
…ource, playground template owner (#473) ## Summary Since #458, echidna's workflows run again, which exposed small reds on main and on every PR. This PR fixes them. Each was reproduced locally first, then shown fixed with the same tool CI uses. ## Changes - **`src/rust/proof_search.rs`: `cargo fmt`** with the repo's pinned 1.99.0 toolchain. - Rust CI on main (run 42351375993) fails only at the fmt step. - This is the only file the workspace-wide `cargo fmt --all` touches. - **`Cargo.lock`: `rmcp` and `rmcp-macros` 3.5.0 → 3.9.0** for RUSTSEC-2026-0457, -0461 and -0462. The newest was published 2026-11-05, after main last passed `Dependency audit`. - Ported from #465 so this PR doesn't wait on it: `cargo update -p rmcp --precise 3.9.0`, inside the existing `"3"` requirement. - The resulting `Cargo.lock` and `proof_search.rs` are byte-identical to #465's, so whichever merges first leaves the other a no-op. - **`.github/workflows/workflow-linter.yml`: rename `authority_sha` → `standards_rev`.** - gitleaks `generic-api-key` read the 40-hex commit id as a key only because the variable name contains "auth". - The fix is at the source, so no `.gitleaks.toml` entry is added. An earlier commit on this branch added one, and `Exemption ratchet` rejected the ledger growth (2 → 3). That entry is gone. - **`echidna-playground/ci-templates/governance.yml`: the never-run template now names `metadatastician/standards`.** It uses the same pin as root's live `governance.yml` (`a797d30`) instead of the old owner at `861b5e9`. ## RSR Quality Checklist ### Required - [x] Tests pass: - `cargo fmt --all -- --check` passes; - `cargo check -p echidna-mcp --locked` passes against rmcp 3.9.0 (the crate has no tests). - [x] Code is formatted: `cargo fmt --all -- --check` passes. - [x] Linter is clean: actionlint 1.7.7 reports 0 findings on both workflow files. - [x] No banned language patterns - [x] No `unsafe` blocks: none added - [x] No banned functions: none - [x] SPDX license headers present: unchanged - [x] No secrets, credentials, or `.env` files included ### As Applicable Nothing in this list applies. ## Testing **gitleaks.** CI-pinned gitleaks 8.18.4 (checksum-verified), with the estate baseline staged at the root exactly as `secret-scanner-reusable.yml` stages it: | Tree | Findings | |---|---| | old name `authority_sha`, no `.gitleaks.toml` entry | 1: `generic-api-key` at `workflow-linter.yml:80` | | this branch (`standards_rev`, no entry) | 0 | | this branch, plus a planted `api_token=ghp_…` beside it | 1: the plant, so it is still detected | **Dependency audit.** `scripts/ci/audit-dependencies.sh` with cargo-audit 0.22.2: - before: `Cargo.lock: FAILED`, with the three rmcp advisories; - after: `Cargo.lock` and `fuzz/Cargo.lock` both `PASSED`. **Rust CI.** I reproduced the fmt failure locally on main with toolchain 1.99.0; after this change `cargo fmt --all -- --check` passes. ## Checks red here, and not caused by this PR - **`Static Analysis / panic-attack assail`** has been red on main since #455. Two causes: - The pinned scanner can't finish a scan of this tree, which #478 fixes. - After that, the gate blocks on two deliberate `sorry` detector fixtures, which #480 handles together with hyperpolymath/panic-attack#278. ## Observed, not changed here - **`mirror.yml` is back on the pre-transfer pin `3c00687`.** - #455's merge restored it, with its old comment. - Main now pins standards at three SHAs: governance `a797d30`; hypatia, scorecard and spark `d3e4b48`; mirror `3c00687`. - The lock still closes, and lock-sync and coordinates pass. But `relock-standards-pin.sh` refuses mixed pins, so the next estate repin will stop here until mirror moves too. - **Mirror failures on main are forge configuration, not code.** The disroot, gitea and sourcehut jobs fail "Verify … SSH host" against the repo variables `*_SSH_FINGERPRINT`, and the bitbucket push fails. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_01JHfuPCv1pEiqkQGG5DQASb --------- Co-authored-by: Claude <noreply@anthropic.com>
Summary
Stacked on #478. With #478 the static analysis scan completes. Its only remaining Critical findings are the two deliberate
sorryfixtures thattests/corpus_hazard_fixtures.rsuses to check that the adapters flag unfinished proofs. This PR records that audit as an inlinepanic-attack: acceptedmarker beside each one.The owner chose this over a gate exemption list. A marker suppresses only the occurrence it sits above, so a real
sorryadded later to either file still fails the gate.Waits on hyperpolymath/panic-attack#278, which line-anchors these findings so a marker can apply. Under the current scanner the markers are inert comments. Once #278 merges I will move
PANIC_ATTACK_REFto the merged commit in this PR.Changes
tests/corpus_fixtures/isabelle/Smoke.thy:(* panic-attack: accepted (detector fixture: …) *)above thesorryindouble_mono.tests/corpus_fixtures/minif2f/algebra.lean:-- panic-attack: accepted (detector fixture: …)above thesorryinimo_1959_p1.PANIC_ATTACK_REFin.github/workflows/static-analysis-gate.yml.RSR Quality Checklist
Required
cargo test --test corpus_hazard_fixtures --test corpus_estate_adaptersgives 2 + 5 passed with the annotated filesunsafeblocks without// SAFETY:comments (none touched)sorrylines pre-exist and are deliberate detector inputs, now marked as such..envfiles includedAs Applicable
Testing
Run locally with a release build of panic-attack#278 (
--features http), against echidnamainwith these exact two edits (byte-identical):assail <echidna> --fail-on-incomplete, run from/tmpSmoke.thy:21andalgebra.lean:11bothsuppressed: true; 0 unsuppressed Criticalstatic-analysis-evidence.sh scan panic-attack+gatestatus: ran, exit 0,critical: 0, total 109 (111 minus the two fixtures); gate exit 0corpus_hazard_fixturessorrycorpus_estate_adaptersGenerated by Claude Code