feat(assail): line-anchor Lean/Isabelle sorry findings so inline markers apply

src/assail/analyzer.rs

@@ -3668,25 +3668,18 @@ impl Analyzer {
         // matching so that doc-comments documenting "no sorry" do not produce
         // false positives.
         let code = strip_proof_comments(content, "--", Some(("/-", "-/")));
-        // sorry — banned proof escape hatch: admits unproven propositions
-        let sorry_count = code.matches("sorry").count();
-        if sorry_count > 0 {
-            stats.unsafe_blocks += sorry_count;
-            weak_points.push(WeakPoint {
-                file: None,
-                line: None,
-                category: WeakPointCategory::ProofDrift,
-                location: Some(file_path.to_string()),
-                severity: Severity::Critical,
-                description: format!(
-                    "{} sorry (banned proof escape hatch — admits unproven proposition) in {}",
-                    sorry_count, file_path
-                ),
-                recommended_attack: vec![AttackAxis::Cpu],
-                suppressed: false,
-                test_context: None,
-            });
-        }
+        // sorry — banned proof escape hatch: admits unproven propositions.
+        // One finding per occurrence, anchored to its line, so an audited
+        // occurrence can carry an inline `panic-attack: accepted` marker
+        // without hiding any other sorry in the same file.
+        push_line_anchored_proof_drift(
+            &code,
+            "sorry",
+            "1 sorry (banned proof escape hatch — admits unproven proposition)",
+            file_path,
+            stats,
+            weak_points,
+        );
 
         // unsafeNativeIO — bypasses IO monad discipline
         let unsafe_io_count =
@@ -3847,25 +3840,16 @@ impl Analyzer {
         // proof-escape hatches. See #43.
         let without_blocks = strip_proof_comments(content, "", Some(("(*", "*)")));
         let code = strip_isabelle_prose(&without_blocks);
-        // sorry — Isabelle's admitted-proof escape hatch (banned estate-wide)
-        let sorry_count = code.matches("sorry").count();
-        if sorry_count > 0 {
-            stats.unsafe_blocks += sorry_count;
-            weak_points.push(WeakPoint {
-                file: None,
-                line: None,
-                category: WeakPointCategory::ProofDrift,
-                location: Some(file_path.to_string()),
-                severity: Severity::Critical,
-                description: format!(
-                    "{} sorry (banned — unfinished Isabelle proof admitted without verification) in {}",
-                    sorry_count, file_path
-                ),
-                recommended_attack: vec![AttackAxis::Cpu],
-                suppressed: false,
-                test_context: None,
-            });
-        }
+        // sorry — Isabelle's admitted-proof escape hatch (banned estate-wide).
+        // One line-anchored finding per occurrence (see analyze_lean).
+        push_line_anchored_proof_drift(
+            &code,
+            "sorry",
+            "1 sorry (banned — unfinished Isabelle proof admitted without verification)",
+            file_path,
+            stats,
+            weak_points,
+        );
 
         // oops — abandons an unfinished proof without even admitting it
         let oops_count = code.matches("oops").count();
@@ -5899,6 +5883,52 @@ fn strip_simple_double_quoted_strings(content: &str) -> String {
     out
 }
 
+/// Append only the newlines of a span that is being removed, so text after
+/// the span keeps its original line number.
+fn push_newlines_of(out: &mut String, removed: &str) {
+    out.extend(removed.chars().filter(|c| *c == '\n'));
+}
+
+/// 1-indexed line of every occurrence of `needle` in `code`. `code` must be
+/// a position-preserving rewrite of the file (every newline kept), as
+/// `strip_proof_comments` and `strip_isabelle_prose` produce.
+fn occurrence_lines(code: &str, needle: &str) -> Vec<u32> {
+    code.match_indices(needle)
+        .map(|(at, _)| code[..at].matches('\n').count() as u32 + 1)
+        .collect()
+}
+
+/// One Critical ProofDrift finding per occurrence of `needle` in `code`, each
+/// anchored to its line so an inline `panic-attack: accepted` marker can
+/// suppress exactly that occurrence. `code` must be position-preserving
+/// (see `occurrence_lines`).
+fn push_line_anchored_proof_drift(
+    code: &str,
+    needle: &str,
+    what: &str,
+    file_path: &str,
+    stats: &mut ProgramStatistics,
+    weak_points: &mut Vec<WeakPoint>,
+) {
+    let lines = occurrence_lines(code, needle);
+    stats.unsafe_blocks += lines.len();
+    for line in lines {
+        weak_points.push(WeakPoint {
+            file: None,
+            line: Some(line),
+            category: WeakPointCategory::ProofDrift,
+            location: Some(file_path.to_string()),
+            severity: Severity::Critical,
+            description: format!("{what} in {file_path}:{line}"),
+            recommended_attack: vec![AttackAxis::Cpu],
+            suppressed: false,
+            test_context: None,
+        });
+    }
+}
+
+/// Remove proof-language comments while keeping every newline, so a line
+/// number taken from the result is a line number in `content`.
 fn strip_proof_comments(content: &str, line_marker: &str, block: Option<(&str, &str)>) -> String {
     // First strip block comments greedily, left-to-right.
     let mut without_blocks = String::with_capacity(content.len());
@@ -5908,9 +5938,11 @@ fn strip_proof_comments(content: &str, line_marker: &str, block: Option<(&str, &
             without_blocks.push_str(&rest[..start]);
             let after_open = &rest[start + open.len()..];
             if let Some(end) = after_open.find(close) {
+                push_newlines_of(&mut without_blocks, &after_open[..end]);
                 rest = &after_open[end + close.len()..];
             } else {
-                // Unterminated block comment — drop the rest.
+                // Unterminated block comment — drop the rest, keep its lines.
+                push_newlines_of(&mut without_blocks, after_open);
                 rest = "";
                 break;
             }
@@ -5920,12 +5952,13 @@ fn strip_proof_comments(content: &str, line_marker: &str, block: Option<(&str, &
         without_blocks.push_str(content);
     }
 
-    // Then strip line comments.
+    // Then strip line comments. Split on '\n' (not `lines()`) so a trailing
+    // newline survives and the newline count is exactly preserved.
     if line_marker.is_empty() {
         return without_blocks;
     }
     let mut out = String::with_capacity(without_blocks.len());
-    for (i, line) in without_blocks.lines().enumerate() {
+    for (i, line) in without_blocks.split('\n').enumerate() {
         let kept = match line.find(line_marker) {
             Some(idx) => &line[..idx],
             None => line,
@@ -6050,6 +6083,7 @@ fn strip_isabelle_prose(content: &str) -> String {
 
         out.push_str(&rest[..next.0]);
         out.push(' ');
+        push_newlines_of(&mut out, &rest[next.0..next.1]);
         rest = &rest[next.1..];
     }
 }
@@ -8361,3 +8395,76 @@ pub fn safe_get_x() -> Option<String> {
         );
     }
 }
+
+#[cfg(test)]
+mod proof_line_anchor_tests {
+    use super::*;
+    use proptest::prelude::*;
+
+    /// Inputs built from the tokens the proof strippers react to, so the
+    /// generator actually reaches unterminated blocks, nested cartouches and
+    /// comments that span lines.
+    fn proof_source() -> impl Strategy<Value = String> {
+        let tokens = [
+            "(*",
+            "*)",
+            "/-",
+            "-/",
+            "--",
+            "//",
+            "text ",
+            "\\<open>",
+            "\\<close>",
+            "@{text ",
+            "}",
+            "{",
+            "\n",
+            "\r\n",
+            "sorry",
+            "a",
+            " ",
+        ];
+        proptest::collection::vec(proptest::sample::select(tokens.to_vec()), 0..60)
+            .prop_map(|parts| parts.concat())
+    }
+
+    proptest! {
+        // The invariant line anchoring rests on: stripping never adds,
+        // drops or reorders a newline, so the line of any surviving
+        // character is its line in the original file.
+        #[test]
+        fn proof_strippers_preserve_every_newline(src in proof_source()) {
+            let newlines = src.matches('\n').count();
+            for (line_marker, block) in [
+                ("--", Some(("/-", "-/"))),
+                ("", Some(("(*", "*)"))),
+                ("//", None),
+            ] {
+                let out = strip_proof_comments(&src, line_marker, block);
+                prop_assert_eq!(out.matches('\n').count(), newlines);
+            }
+            let isabelle = strip_isabelle_prose(&strip_proof_comments(&src, "", Some(("(*", "*)"))));
+            prop_assert_eq!(isabelle.matches('\n').count(), newlines);
+        }
+    }
+
+    #[test]
+    fn occurrence_lines_are_one_indexed_per_occurrence() {
+        assert_eq!(
+            occurrence_lines("sorry\nx\n  sorry sorry\n", "sorry"),
+            vec![1, 3, 3]
+        );
+        assert!(occurrence_lines("no escape here\n", "sorry").is_empty());
+    }
+
+    #[test]
+    fn sorry_after_multiline_comment_keeps_its_line() {
+        let lean = "/- a\n   b -/\ntheorem t : True := by\n  sorry\n";
+        let code = strip_proof_comments(lean, "--", Some(("/-", "-/")));
+        assert_eq!(occurrence_lines(&code, "sorry"), vec![4]);
+
+        let thy = "(* a\n   b *)\ntext \\<open>prose\n  sorry in prose\\<close>\nlemma l: True\n  sorry\n";
+        let code = strip_isabelle_prose(&strip_proof_comments(thy, "", Some(("(*", "*)"))));
+        assert_eq!(occurrence_lines(&code, "sorry"), vec![6]);
+    }
+}

src/assail/mod.rs

@@ -436,6 +436,15 @@ pub fn apply_v255_context_suppression(report: &mut AssailReport) -> usize {
     let mut newly_suppressed = 0usize;
     let mut content_cache: std::collections::HashMap<String, Option<String>> =
         std::collections::HashMap::new();
+    // Finding locations are relative to the scan root, not to the process
+    // working directory, so resolve them against the root. Without this,
+    // `assail <dir>` run from anywhere but <dir> silently ignored every
+    // inline marker.
+    let scan_root: Option<std::path::PathBuf> = if report.program_path.is_dir() {
+        Some(report.program_path.clone())
+    } else {
+        report.program_path.parent().map(Path::to_path_buf)
+    };
 
     for wp in &mut report.weak_points {
         // Determine the file path; prefer the structured `file` field,
@@ -455,7 +464,14 @@ pub fn apply_v255_context_suppression(report: &mut AssailReport) -> usize {
         // None so we don't repeatedly retry.
         let content_opt = content_cache
             .entry(file.clone())
-            .or_insert_with(|| std::fs::read_to_string(&file).ok())
+            .or_insert_with(|| {
+                let rel = Path::new(&file);
+                scan_root
+                    .as_deref()
+                    .filter(|_| rel.is_relative())
+                    .and_then(|root| std::fs::read_to_string(root.join(rel)).ok())
+                    .or_else(|| std::fs::read_to_string(rel).ok())
+            })
             .clone();
 
         // Always set test_context — even when the finding isn't a
@@ -891,3 +907,63 @@ mod v255_context_suppression_tests {
         );
     }
 }
+
+#[cfg(test)]
+mod proof_marker_tests {
+    use super::*;
+    use crate::types::WeakPointCategory;
+    use std::fs;
+    use tempfile::TempDir;
+
+    /// End to end through `analyze()`: each `sorry` is its own finding on
+    /// its own line, an inline marker suppresses only the occurrence it sits
+    /// above, and markers resolve against the scan root rather than the
+    /// process working directory (the test runs from the crate root).
+    #[test]
+    fn sorry_markers_suppress_only_the_marked_occurrence() {
+        let tmp = TempDir::new().unwrap();
+        fs::write(
+            tmp.path().join("Fix.lean"),
+            "theorem a : True := by\n  -- panic-attack: accepted (detector fixture)\n  sorry\n\n\
+             /- a\n   multi-line\n   comment -/\ntheorem b : True := by\n  sorry\n",
+        )
+        .unwrap();
+        fs::write(
+            tmp.path().join("Fix.thy"),
+            "theory Fix imports Main begin\n(* a\n   multi-line comment *)\n\
+             text \\<open>prose\n  over lines\\<close>\nlemma a: True\n  \
+             (* panic-attack: accepted (detector fixture) *)\n  sorry\nlemma b: True\n  sorry\nend\n",
+        )
+        .unwrap();
+
+        let report = analyze(tmp.path()).unwrap();
+        let mut got: Vec<(String, u32, bool)> = report
+            .weak_points
+            .iter()
+            .filter(|w| matches!(w.category, WeakPointCategory::ProofDrift))
+            .filter(|w| w.description.contains("sorry"))
+            .map(|w| {
+                let loc = w.location.clone().unwrap_or_default();
+                let name = Path::new(&loc)
+                    .file_name()
+                    .map(|n| n.to_string_lossy().into_owned())
+                    .unwrap_or(loc);
+                (
+                    name,
+                    w.line.expect("sorry findings are line-anchored"),
+                    w.suppressed,
+                )
+            })
+            .collect();
+        got.sort();
+        assert_eq!(
+            got,
+            vec![
+                ("Fix.lean".to_string(), 3, true),
+                ("Fix.lean".to_string(), 9, false),
+                ("Fix.thy".to_string(), 8, true),
+                ("Fix.thy".to_string(), 10, false),
+            ]
+        );
+    }
+}