You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
{{ message }}
Repository navigation
fix(audits): classify the two deliberate corpus-fixture sorrys - #489
On main: coverage is complete and deposit passes. But the panic-attack assail job fails with "Critical scanner findings block merge". The only 2 critical findings are PA021 ProofDrift: one open sorry each, in tests/corpus_fixtures/isabelle/Smoke.thy and tests/corpus_fixtures/minif2f/algebra.lean.
This PR fixes item 2.
Changes
audits/assail-classifications.a2ml: add 2 entries, one per fixture, with category ProofDrift. The sorrys are deliberate: tests/corpus_hazard_fixtures.rs checks that the corpus adapters flag them as hazards, and those tests fail if they are removed. Each entry names its test.
This is an addition only. No existing entry and no licence header changes.
RSR Quality Checklist
Required
No banned functions added. The 2 sorrys are existing fixtures; this PR only classifies them.
No secrets, credentials, or .env files included
Testing
I built panic-attack main (4f51cca, --locked --features http) and ran it on echidna main with this change:
The Static Analysis Gate on main fails with "Critical scanner findings
block merge". Coverage is complete with the pinned panic-attack; the
only criticals are two PA021 ProofDrift findings, one open `sorry` each
in tests/corpus_fixtures/isabelle/Smoke.thy and
tests/corpus_fixtures/minif2f/algebra.lean.
Both are deliberate test inputs: tests/corpus_hazard_fixtures.rs asserts
that the corpus adapters flag them as sorry hazards, so removing them
would break those tests. Record them in the panic-attack classification
registry, which suppresses exactly these file and category pairs. No
existing entry changes.
Checked with panic-attack main (4f51cca, --features http): assail exits
0 with coverage complete 913/913 and 0 unsuppressed critical findings.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_0136P7ZnmBahbhfkFEP6ark4
No actionable comments were generated in the recent review.
Summary
Summary by CodeRabbit
Documentation
Added classifications for the Isabelle and MiniF2F fixtures, noting that they contain intentionally incomplete proofs and are test inputs rather than proofs used by ECHIDNA.
The entries also document checks that confirm each fixture is marked as a hazard. These changes update audit records; no user-facing behavior changes are noted.
The audit registry adds ProofDrift classifications for the Isabelle and MiniF2F fixtures. Each entry documents its deliberate open sorry and references a test that checks hazard detection.
Adds ProofDrift classifications for the Isabelle and MiniF2F fixtures. Each entry describes the deliberate open sorry and cites its hazard-fixture test.
hyperpolymath/echidna#455: Adds hazard-fixture tests for the same Isabelle and MiniF2F fixtures classified here.
Merge Risk: Minimal · up to ea1af
The fixture classifications are ready to merge after normal checks.
Pre-merge checks: 5
Check name
Status
Explanation
Title check
The title clearly describes the main change: classifying the two deliberate corpus-fixture sorrys.
Description check
The description explains the problem, changes, and reported test results. It includes the required sections, but the RSR Quality Checklist is only partially completed; several required items are unmar…
Docstring Coverage
No eligible functions found in the changed files. Skipping docstring coverage check. Docstring coverage is scoped to functions touched by this diff with cyclomatic complexity of at least 2. Documentat…
Linked Issues check
Check skipped because no linked issues were found for this pull request.
Out of Scope Changes check
Check skipped because no linked issues were found for this pull request.
Full details: Description check
Explanation
The description explains the problem, changes, and reported test results. It includes the required sections, but the RSR Quality Checklist is only partially completed; several required items are unmarked.
Full details: Docstring Coverage
Explanation
No eligible functions found in the changed files. Skipping docstring coverage check. Docstring coverage is scoped to functions touched by this diff with cyclomatic complexity of at least 2. Documentation-only edits and deletions within surviving functions are included; unchanged diff context and fully deleted functions are excluded. Analyzed 0 functions across 0 files. (1 skipped: 1 unsupported.)
Autofix · Keep fixing CodeRabbit findings and required CI, and resolving merge conflicts
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.
File: No configuration file from this repository applied
Commit: Unavailable
Layers: Organization UI
Review profile: ASSERTIVE
Plan: Advanced
Run ID: 8eb04d00-616b-4632-9395-4c005938ef69
Commits
Reviewing files that changed from the base of the PR and between b6ff166 and ea1afde.
Files selected for processing: 1
audits/assail-classifications.a2ml
Included review availability: This review used your included allowance. Your plan provides up to 1 included review per hour; 0 remain after this review.
Recent review details
Context from checks skipped due to timeout: 5
GitHub Check: rust-ci / Cargo test
GitHub Check: CodeRabbit
GitHub Check: panic-attack assail
GitHub Check: rust-ci / llvm-cov line coverage
GitHub Check: PR (address)
Additional context used
Code guidelines: 1
CLAUDE.md — auto-discovered
Path-based instructions: 1
Source excerpt: **Version + release history**: [`CHANGELOG.adoc`](CHANGELOG.adoc) (single source of truth; do not duplicate version strings elsewhere)
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.
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
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.
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
Summary
The Static Analysis Gate fails in two different ways, depending on the branch.
panic-attack assailexits 2 withincomplete coverage (partial). Thendepositfails with "Incomplete scanner evidence". The branch still pins panic-attack410a8f8, which predates panic-attack ci(server): server boot gate — convert 'compiles' into 'boots' #258. That version has no adapter for TOML, YAML, JSON, Containerfile, Justfile, HTML, CSS or Forth, so it marks 190 of echidna's 908 candidate files "unsupported". main already fixes this: it pinsf2a6a70, which includes ci(server): server boot gate — convert 'compiles' into 'boots' #258. Those branches need main merged in.depositpasses. But thepanic-attack assailjob fails with "Critical scanner findings block merge". The only 2 critical findings are PA021 ProofDrift: one opensorryeach, intests/corpus_fixtures/isabelle/Smoke.thyandtests/corpus_fixtures/minif2f/algebra.lean.This PR fixes item 2.
Changes
audits/assail-classifications.a2ml: add 2 entries, one per fixture, with categoryProofDrift. Thesorrys are deliberate:tests/corpus_hazard_fixtures.rschecks that the corpus adapters flag them as hazards, and those tests fail if they are removed. Each entry names its test.RSR Quality Checklist
Required
sorrys are existing fixtures; this PR only classifies them..envfiles includedTesting
I built panic-attack main (
4f51cca,--locked --features http) and ran it on echidna main with this change:assail --fail-on-incomplete: exit 0, coveragecomplete913/913, unsuppressed findings: 0 critical, 43 high, 65 medium, 1 low.scripts/ci/static-analysis-evidence.sh's panic-attack contract (schema2.6).bridge triage: exit 0, schema0.3.0,vulnerability_data: queried. This matches the Patch Bridge contract.Generated by Claude Code