fix(assail): PA021 Isabelle detector skips prose blocks + antiquotations (closes #43) by hyperpolymath · Pull Request #49 · hyperpolymath/panic-attack

hyperpolymath · 2026-05-26T10:00:14Z

Summary

Closes #43. PA021 ProofDrift was matching sorry/oops keywords inside Isabelle prose constructs (docstrings discussing the keywords, not invoking them), producing false positives.

Evidence pattern (from the bug report)

File:line	Match context
`Tropical_Kleene.thy:663`	`"zero @{text sorry}."`
`Tropical_Ordinal.thy:15`	`"with \<open>oops\<close> are..."`
`Tropical_Matrices_Clean.thy:24`	`"zero @{text sorry}."`
`Tropical_CNO.thy:29`	`text \<open>All sorry placeholders...\<close>`

The existing strip_proof_comments helper only handles (* ... *) block comments — it left the three modern Isabelle prose constructs intact, hence the FPs.

Fix

New strip_isabelle_prose helper in src/assail/analyzer.rs, called after strip_proof_comments in analyze_isabelle. Strips:

@{text ...} antiquotations — brace-balanced (nested braces handled).
Prose-block cartouches following chapter, section, subsection, subsubsection, paragraph, text keywords. Cartouches (\<open>...\<close>) nest, so depth-counted.

Conservative: only cartouches that follow a recognised prose-block keyword are stripped — string-literal cartouches inside tactics (rare) stay visible. Word-boundary check on the keyword prevents mysection_lemma from matching section.

Regression coverage

8 new unit tests in assail::analyzer::tests:

isabelle_strip_text_antiquotation_inside_block_comment — case 1
isabelle_strip_cartouche_after_text_keyword — case 4
isabelle_strip_section_cartouche — case 2 (cartouche after section)
isabelle_strip_subsection_subsubsection_paragraph_chapter — parametrised over the other prose keywords
isabelle_preserve_real_sorry_outside_prose — inverse invariant: a genuine sorry tactic still gets flagged
isabelle_nested_cartouches — \<open>outer \<open>inner sorry\<close>\<close> handled by depth-counting
isabelle_antiquotation_with_nested_braces — @{text "{ x = 1 }"} handled
isabelle_keyword_not_at_word_boundary — mysection_lemma does NOT trip the section keyword

Test plan

cargo test --bin panic-attack --features signing,http — 226 passed, 0 failed (218 existing + 8 new)
cargo clippy --all-targets --features signing,http -- -D warnings — clean
cargo fmt --check — clean
GPG-signed commit

Follow-ups (mentioned in the issue, not in scope here)

Comparable Agda/Coq/Idris detectors should be re-audited for the same blind spot.

Filed as out-of-scope for #43; can be tackled language-by-language in follow-up PRs.

🤖 Generated with Claude Code

Closes #43. The PA021 ProofDrift detector was matching `sorry`/`oops` keywords inside Isabelle prose constructs that document the keywords rather than invoke them, producing false positives like: Tropical_Kleene.thy:663 "zero @{text sorry}." Tropical_Ordinal.thy:15 "with \<open>oops\<close> are..." Tropical_Matrices_Clean.thy "zero @{text sorry}." Tropical_CNO.thy:29 text \<open>All sorry placeholders... The existing `strip_proof_comments` helper only handles `(* ... *)` block comments, leaving the three modern Isabelle prose constructs untouched. Fix: new `strip_isabelle_prose` helper, called after `strip_proof_comments` in `analyze_isabelle`. Strips: - `@{text ...}` antiquotations (brace-balanced, can contain nested braces) - Prose-block cartouches following `chapter`, `section`, `subsection`, `subsubsection`, `paragraph`, `text` keywords (`\<open>...\<close>` cartouches are nesting-aware) Conservative: only cartouches that follow a recognised prose-block keyword are stripped — string-literal cartouches inside tactics (rare) are kept. Word-boundary check on the keyword prevents `mysection_lemma` from matching `section`. Regression coverage: 8 unit tests in `assail::analyzer::tests` covering all 4 evidence patterns from the bug report plus nesting, word-boundary, and the "real sorry tactic must still be detected" invariant. All 226 binary tests pass. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

github-actions · 2026-05-26T10:01:57Z

🔍 Hypatia Security Scan

Findings: 49 issues detected

Severity	Count
🔴 Critical	4
🟠 High	16
🟡 Medium	29

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Action hyperpolymath/standards/.github/workflows/governance-reusable.yml@main needs attention",
    "type": "unpinned_action",
    "file": "governance.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Nickel file missing SPDX-License-Identifier header (1 occurrences, CWE-1104)",
    "type": "ncl_missing_spdx",
    "file": "/home/runner/work/panic-attack/panic-attack/reports/panic-attack-20260211180017.ncl",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "expect() in hot path (2 occurrences, CWE-754)",
    "type": "expect_in_hot_path",
    "file": "/home/runner/work/panic-attack/panic-attack/src/attestation/chain.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "unwrap_or(0) with dangerous default (1 occurrences, CWE-754)",
    "type": "unwrap_dangerous_default",
    "file": "/home/runner/work/panic-attack/panic-attack/src/attestation/evidence.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "critical"
  },
  {
    "reason": "unwrap_or(0) with dangerous default (1 occurrences, CWE-754)",
    "type": "unwrap_dangerous_default",
    "file": "/home/runner/work/panic-attack/panic-attack/src/ambush/mod.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "critical"
  },
  {
    "reason": "unwrap_or(0) with dangerous default (3 occurrences, CWE-754)",
    "type": "unwrap_dangerous_default",
    "file": "/home/runner/work/panic-attack/panic-attack/src/kanren/strategy.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "critical"
  },
  {
    "reason": "unwrap_or(0) with dangerous default (3 occurrences, CWE-754)",
    "type": "unwrap_dangerous_default",
    "file": "/home/runner/work/panic-attack/panic-attack/src/axial/mod.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "critical"
  },
  {
    "reason": "expect() in hot path (4 occurrences, CWE-754)",
    "type": "expect_in_hot_path",
    "file": "/home/runner/work/panic-attack/panic-attack/src/assail/analyzer.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "unwrap() without prior check -- DoS via panic (4 occurrences, CWE-754)",
    "type": "unwrap_without_check",
    "file": "/home/runner/work/panic-attack/panic-attack/benches/scan_bench.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "high"
  },
  {
    "reason": "expect() in hot path (2 occurrences, CWE-754)",
    "type": "expect_in_hot_path",
    "file": "/home/runner/work/panic-attack/panic-attack/benches/scan_bench.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

github-actions · 2026-05-26T10:05:49Z

🔍 Hypatia Security Scan

Findings: 49 issues detected

Severity	Count
🔴 Critical	4
🟠 High	16
🟡 Medium	29

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Action hyperpolymath/standards/.github/workflows/governance-reusable.yml@main needs attention",
    "type": "unpinned_action",
    "file": "governance.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Nickel file missing SPDX-License-Identifier header (1 occurrences, CWE-1104)",
    "type": "ncl_missing_spdx",
    "file": "/home/runner/work/panic-attack/panic-attack/reports/panic-attack-20260211180017.ncl",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "expect() in hot path (2 occurrences, CWE-754)",
    "type": "expect_in_hot_path",
    "file": "/home/runner/work/panic-attack/panic-attack/src/attestation/chain.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "unwrap_or(0) with dangerous default (1 occurrences, CWE-754)",
    "type": "unwrap_dangerous_default",
    "file": "/home/runner/work/panic-attack/panic-attack/src/attestation/evidence.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "critical"
  },
  {
    "reason": "unwrap_or(0) with dangerous default (1 occurrences, CWE-754)",
    "type": "unwrap_dangerous_default",
    "file": "/home/runner/work/panic-attack/panic-attack/src/ambush/mod.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "critical"
  },
  {
    "reason": "unwrap_or(0) with dangerous default (3 occurrences, CWE-754)",
    "type": "unwrap_dangerous_default",
    "file": "/home/runner/work/panic-attack/panic-attack/src/kanren/strategy.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "critical"
  },
  {
    "reason": "unwrap_or(0) with dangerous default (3 occurrences, CWE-754)",
    "type": "unwrap_dangerous_default",
    "file": "/home/runner/work/panic-attack/panic-attack/src/axial/mod.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "critical"
  },
  {
    "reason": "expect() in hot path (4 occurrences, CWE-754)",
    "type": "expect_in_hot_path",
    "file": "/home/runner/work/panic-attack/panic-attack/src/assail/analyzer.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "unwrap() without prior check -- DoS via panic (4 occurrences, CWE-754)",
    "type": "unwrap_without_check",
    "file": "/home/runner/work/panic-attack/panic-attack/benches/scan_bench.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "high"
  },
  {
    "reason": "expect() in hot path (2 occurrences, CWE-754)",
    "type": "expect_in_hot_path",
    "file": "/home/runner/work/panic-attack/panic-attack/benches/scan_bench.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

…regression from #49) (#65) ## Summary `skip_cartouche_end` advanced its byte index by 1 in the no-open / no-close branch, which puts `j` inside a multi-byte UTF-8 sequence when the cartouche body contains non-ASCII (`¬`, `∀`, `⟹`, `🎉`, etc.). The next iteration's `haystack[j..].starts_with(open)` then panics: ``` thread 'main' panicked at src/assail/analyzer.rs:5648:20: start byte index 89 is not a char boundary; it is inside '¬' (bytes 88..90) ``` ## Discovery `./target/release/panic-attack assail /home/hyperpolymath/developer/repos/echidna` from the 2026-05-26 estate reconnaissance crashed on a real `.thy` file inside echidna: ``` text \<open> Double negation elimination: ¬¬A is equivalent to A. ... \<close> ``` Subsetting echidna to `src/` worked around it; this is the proper fix. ## Fix In the no-open / no-close branch, advance by `len_utf8()` of the current char rather than 1 byte. `chars().next()` is guaranteed non-empty there because `j < haystack.len()`. ## Tests Two new regression tests in `assail::analyzer::tests`: - `isabelle_cartouche_with_non_ascii_does_not_panic` — sampled body from the actual crash (`¬¬A`, `∀x`, `⟹`). - `isabelle_cartouche_emoji_grapheme_clusters` — 4-byte UTF-8 (🎉) exercises the full multi-byte range, including the path that 2/3-byte chars wouldn't catch. ## Test plan - [x] `cargo test --lib assail::analyzer::tests::isabelle` — **10/10 pass** (8 existing + 2 new). - [x] `cargo build --release` clean. - [x] Reproducer: `./target/release/panic-attack assail /home/hyperpolymath/developer/repos/echidna` now completes cleanly with **44 weak points** (was: panic). - [ ] CI on this PR. Regression from #49 (Isabelle prose-stripper added in 2026-05-26). 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

hyperpolymath enabled auto-merge (squash) May 26, 2026 10:00

Merge branch 'main' into fix/isabelle-prose-fp-43

73114be

hyperpolymath merged commit db0e1b7 into main May 26, 2026
26 checks passed

hyperpolymath deleted the fix/isabelle-prose-fp-43 branch May 26, 2026 10:07

hyperpolymath mentioned this pull request May 26, 2026

fix(assail): char-boundary-aware advance in Isabelle cartouche skip (regression from #49) #65

Merged

4 tasks

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

fix(assail): PA021 Isabelle detector skips prose blocks + antiquotations (closes #43)#49

fix(assail): PA021 Isabelle detector skips prose blocks + antiquotations (closes #43)#49
hyperpolymath merged 2 commits into
mainfrom
fix/isabelle-prose-fp-43

hyperpolymath commented May 26, 2026

Uh oh!

github-actions Bot commented May 26, 2026

Uh oh!

github-actions Bot commented May 26, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

hyperpolymath commented May 26, 2026

Summary

Evidence pattern (from the bug report)

Fix

Regression coverage

Test plan

Follow-ups (mentioned in the issue, not in scope here)

Uh oh!

github-actions Bot commented May 26, 2026

🔍 Hypatia Security Scan

Uh oh!

github-actions Bot commented May 26, 2026

🔍 Hypatia Security Scan

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant