Repository navigation
feat(assail): line-anchor Lean/Isabelle sorry findings so inline markers apply - #278
Merged
hyperpolymath merged 3 commits intoNov 10, 2026
Merged
Conversation
…ers apply Lean and Isabelle `sorry` produced one ProofDrift finding per file with a count and line: None. The inline `panic-attack: accepted` pass only runs on findings with a line, so these could be suppressed only through the retired A2ML classification registry, file- and category-wide. echidna's deliberate detector fixtures (a `sorry` its corpus adapter must flag) therefore kept its static analysis gate red with no supported way to record the audit. - Each sorry occurrence is its own finding with its line. The per-file count in stats.unsafe_blocks is unchanged. - strip_proof_comments and strip_isabelle_prose keep every newline of a removed span (and the line-comment pass splits on '\n'), so lines taken from stripped text are lines in the file. occurrence_lines maps matches to 1-indexed lines. - `(*` is a start-of-line marker leader (Isabelle, Coq/Rocq, OCaml, SML, F*); a trailing `*)` is dropped from the reason. - The marker pass resolves finding locations against the scan root before the working directory. They are root-relative, so `assail <dir>` run from elsewhere silently ignored every inline marker. Tests: a proptest that both strippers preserve every newline; unit tests for occurrence_lines, multi-line comments and prose, and the new leader; an end-to-end analyze() over a temp dir with one marked and one unmarked sorry in each language, run from the crate root. Five mutants are each killed: markers-read-cwd-only, block-drops-newlines, prose-drops-newlines, no-ml-leader, unterminated-drops-lines. Full suite with --features http: 791 passed, 0 failed; clippy --all-targets: 0 warnings. Checked against echidna main with its two fixtures annotated: both findings are suppressed at the right lines, and echidna's own static-analysis evidence scan plus gate passes (critical 0). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01JHfuPCv1pEiqkQGG5DQASb
Contributor
|
Caution Review failedThe pull request is closed.
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. |
This was referenced Nov 9, 2026
The Lean and Isabelle sorry detectors each carried the same 18-line per-occurrence loop, differing only in the description; SonarCloud's quality gate failed on it (5.1% duplication on new code, limit 3%). Both now call push_line_anchored_proof_drift(code, needle, what, ...), which is also the shape #280 needs for the remaining escape hatches. No behaviour change: descriptions keep the "<what> in <file>:<line>" form. cargo test --features http: 791 passed, 0 failed; clippy --all-targets: 0 warnings. Mutants helper-drops-line, block-drops-newlines and prose-drops-newlines are each killed. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01JHfuPCv1pEiqkQGG5DQASb
hyperpolymath
pushed a commit
to hyperpolymath/echidna
that referenced
this pull request
Nov 9, 2026
…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
hyperpolymath
marked this pull request as ready for review
November 9, 2026 15:46
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. |
|
You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard. |
hyperpolymath
added a commit
to hyperpolymath/echidna
that referenced
this pull request
Nov 9, 2026
…ctor inputs (#480) ## Summary Stacked on #478. With #478 the static analysis scan completes. Its only remaining Critical findings are the two deliberate `sorry` fixtures that `tests/corpus_hazard_fixtures.rs` uses to check that the adapters flag unfinished proofs. This PR records that audit as an inline `panic-attack: accepted` marker beside each one. The owner chose this over a gate exemption list. A marker suppresses only the occurrence it sits above, so a real `sorry` added 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_REF` to the merged commit in this PR. ## Changes - `tests/corpus_fixtures/isabelle/Smoke.thy`: `(* panic-attack: accepted (detector fixture: …) *)` above the `sorry` in `double_mono`. - `tests/corpus_fixtures/minif2f/algebra.lean`: `-- panic-attack: accepted (detector fixture: …)` above the `sorry` in `imo_1959_p1`. - *(pending #278)*: `PANIC_ATTACK_REF` in `.github/workflows/static-analysis-gate.yml`. ## RSR Quality Checklist ### Required - [x] Tests pass: `cargo test --test corpus_hazard_fixtures --test corpus_estate_adapters` gives 2 + 5 passed with the annotated files - [x] Code is formatted (comment lines only) - [x] Linter is clean - [x] No banned language patterns - [x] No `unsafe` blocks without `// SAFETY:` comments (none touched) - [x] No banned functions introduced. The two `sorry` lines pre-exist and are deliberate detector inputs, now marked as such. - [x] SPDX license headers present (unchanged) - [x] No secrets, credentials, or `.env` files included ### As Applicable - n/a. ## Testing Run locally with a release build of panic-attack#278 (`--features http`), against echidna `main` with these exact two edits (byte-identical): | Check | Result | |---|---| | `assail <echidna> --fail-on-incomplete`, run from `/tmp` | exit 0; `Smoke.thy:21` and `algebra.lean:11` both `suppressed: true`; 0 unsuppressed Critical | | `static-analysis-evidence.sh scan panic-attack` + `gate` | `status: ran`, exit 0, `critical: 0`, total 109 (111 minus the two fixtures); gate exit 0 | | `corpus_hazard_fixtures` | 2 passed: both adapters still flag their `sorry` | | `corpus_estate_adapters` | 5 passed | --- _Generated by [Claude Code](https://claude.ai/code/session_01JHfuPCv1pEiqkQGG5DQASb)_ --------- Co-authored-by: Claude <noreply@anthropic.com>
hyperpolymath
added a commit
to hyperpolymath/echidna
that referenced
this pull request
Nov 9, 2026
…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>
hyperpolymath
enabled auto-merge (squash)
November 9, 2026 23:22
…t-lines Signed-off-by: Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com>
hyperpolymath
disabled auto-merge
November 10, 2026 02:00
hyperpolymath
deleted the
claude/compassionate-fermat-9x7vpe-proofdrift-lines
branch
November 10, 2026 02:00
|
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
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.
Why
Lean and Isabelle
sorryproduced one ProofDrift finding per file, with a count andline: None. The inlinepanic-attack: acceptedpass only runs on findings that carry a line. So the only way to record an auditedsorrywas the A2ML classification registry, which is retired estate-wide and matches a whole file and category.That left hyperpolymath/echidna's static analysis gate red with no supported way out. Its corpus adapters keep deliberate detector fixtures: a
sorrythey must flag. hyperpolymath/echidna#478 bumps echidna to the scanner commit that can complete coverage, and these two fixtures are then its only Critical findings.What
sorryis its own Critical ProofDrift finding with itsline.stats.unsafe_blockscounts the same as before. A severity gate's pass/fail is unchanged, though a file with Nsorrynow contributes N findings.strip_proof_commentsandstrip_isabelle_prosenow keep every newline of a removed comment or prose span, and the line-comment pass splits on'\n'instead oflines(). Line numbers taken from the stripped text are therefore line numbers in the file (cf. proofs(Layer 1.0 follow-up): block-comment + string-literal stripping + composition + position-preservation #114). The newoccurrence_linesmaps matches to 1-indexed lines.(*marker leader, recognised at the start of a line only, for Isabelle, Coq/Rocq, OCaml, SML and F*. A trailing*)is dropped from the reason. Mid-line(*is excluded because it is also a C dereference or a Python splat.assail <dir>run from anywhere else silently ignored every inline marker, in all languages. It now resolves against the scan root first and falls back to the working directory.Evidence
cargo test --features http: 791 passed, 0 failed.cargo clippy --features http --all-targets: 0 warnings.cargo fmtis clean.New tests:
proptestthat both strippers preserve every newline, over generated inputs built from comment, prose and cartouche tokens (including unterminated blocks and\r\n);occurrence_lines, for asorryafter multi-line comments and prose, and for the new leader (start-of-line only, previous-line suppression);analyze()over a temp dir: one marked and one unmarkedsorryper language, behind multi-line comments and prose. It runs from the crate root, so it also covers the root resolution.Mutants, each killed by the new tests:
Against echidna
main, with its two fixtures annotated ((* panic-attack: accepted (…) *)above the Isabellesorry,-- panic-attack: accepted (…)above the Lean one), scanned from/tmp:Smoke.thy:21andalgebra.lean:11;static-analysis-evidence.sh scan+gatepasses:status: ran, exit 0,critical: 0, total 109, which is 111 minus the two fixtures.Not in this PR
oops, CoqAdmitted, Agdapostulate, Idrisbelieve_me, and so on) are still per-file and unanchored. The sameoccurrence_linespattern applies, but each needs its own position check, so they are left to a follow-up rather than widening this PR.Generated by Claude Code