ArghDA M4 follow-on: Idris2 totality-hole + partial lint (M4 → 100%)

.machine_readable/6a2/STATE.a2ml

@@ -44,7 +44,7 @@ milestones = [
   { name = "M1: Backend trait (Assistant|Solver kinds; Outcome/Verdict); agda.rs -> prover/agda.rs; graph/dag take &dyn Backend (pure refactor, 50 tests stay green)", completion = 100 },
   { name = "M2: Cubical-Agda variant (Agda::cubical(), --cubical --safe island)", completion = 100 },
   { name = "M3: Flying-Logic reasoning graph (src/reason: And|Or juncts, demote-only cycle-safe Verdict propagation, additive studio JSON)", completion = 100 },
-  { name = "M4: Idris2 adapter (core/ABI language: .ipkg/--check/totality; escape-hatches)", completion = 95 },
+  { name = "M4: Idris2 adapter (core/ABI language: .ipkg/--check/totality; escape-hatches)", completion = 100 },
   { name = "M5: SMT solver backends (Z3, CVC5): SMT-LIB2 -> sat/unsat/unknown -> Verdict", completion = 100 },
   { name = "M6: Lean4 adapter (lake build + #print axioms audit)", completion = 100 },
   { name = "M7: Echidna dispatch seam (optional route to orchestrator :8090, same Outcome)", completion = 70 },
@@ -114,6 +114,22 @@ milestones = [
 # --backend idris2` over an ipkg fixture → crt_roots ['App'], App+Helper wired.
 # M4 now 95% (remaining: totality-hole `?name` + per-def `partial` lint).
 #
+# M4 FOLLOW-ON landed 2026-07-01 (M4 → 100%): the Idris2 escape-hatch lint now
+# also flags a per-definition `partial` modifier (totality opt-out, distinct
+# from the already-handled file-wide `%default partial` directive) and totality
+# holes `?name` (incomplete terms/proofs). src/lint/idris2.rs: `holes()` finds a
+# `?` that begins a token (start / after ws / ([{,;= ) and is followed by an
+# identifier — so a hole `?goal` matches but a user operator `<?>` does not;
+# `strip_strings()` blanks double-quoted literals (honouring \" ) first so a
+# `"?x"` in a string is not a false hole. All under the shared `escape-hatch`
+# rule name → the reason graph caps hits at amber. 173 tests (+5 idris2 lint
+# unit: per-def partial, hole, hole-in-string ignored, `<?>` not a hole, `total`
+# not flagged). DOGFOODED vs real idris2 0.7.0: a file with `partial loop` +
+# `f = ?rhs` — `idris2 --check --source-dir` exits 0 (the silent-failure class);
+# `arghda scan --backend idris2` flags both (partial + ?rhs); `reason --check
+# --backend idris2` → Holey self=admitted, effective=admitted, evidence
+# "prover: proven; escape-hatch → admitted" (green exit correctly capped amber).
+#
 # M6 FOLLOW-ON landed 2026-07-01 (M6 → 100%): lake-env import resolution — the
 # Lean audit now reaches IMPORTED files, not just import-free ones. When a
 # `lakefile.lean`/`lakefile.toml` is found at/above the file (`lake_root`), both
@@ -392,12 +408,12 @@ actions = [
   "ENGINE-SPINE DELIVERABLE COMPLETE: M0-M7 + M11 all landed. v0.1 spec closed. Six backends (agda, agda-cubical, idris2, lean4 Assistant; z3, cvc5 Solver) + reasoning graph + doctor + groove + dispatch seam. Remaining work is refinement + the heavy tail:",
   "M7 follow-on: the real Echidna orchestrator HTTP client (feature-gated), once Echidna's API is confirmed — only Dispatch::run changes.",
   "M6 follow-on: DONE (M6 → 100%) — lake-env resolution (`lake env lean` under a lakefile) so IMPORTED Lean files elaborate + get #print-axioms-audited too, not just import-free ones. Dogfooded on a built lake project.",
-  "M4 follow-on: .ipkg-declared roots DONE; remaining = totality-hole (?name) + per-def `partial` lint.",
+  "M4 follow-on: DONE (M4 → 100%) — totality-hole (?name) + per-def `partial` lint added to the Idris2 escape-hatch rule; dogfooded vs real idris2 0.7.0 (green --check exit correctly capped to amber).",
   "M3 follow-on: DONE — `reason --workspace <ws>` sources real verdicts from a `proven/` state (workspace_verdicts) + demotes stale-proven via the content-hash closure. Refinement follow-ons bucket now complete.",
   "M8 (Coq/Rocq): DONE (90%) — coqc 8.18.0 provisioned + adapter built + dogfooded (proven/admitted/postulated/error) with Section-aware postulate classifier. Remaining: _CoqProject logical paths + dependency-ordered compilation.",
   "M9 (Isabelle): DONE (90%) — Isabelle2025 provisioned + adapter built + dogfooded (proven/admitted/postulated/error) via session-build; ROOT-based roots, imports-clause edges. Remaining: session-qualified imports + dependency-ordered multi-session builds.",
   "M10 (Mizar): DONE (85%) — turned out to be a REAL verify, not detect-only: static i386 verifier runs on x86_64; provisioned + adapter (accom+verifier+.err) + dogfooded (proven/error). HEAVY TAIL M8-M10 COMPLETE. Remaining: local-article prel export.",
-  "Next, climb up: M4 (totality-hole ?name + per-def partial lint for Idris2), M7 (real Echidna HTTP client, feature-gated — but FIRST confirm Echidna's API actually exists; if not, keep the honest stub). Each its own focused draft PR, gate green, real-tool dogfood where installed.",
+  "Only M7 remains: the real Echidna HTTP client (feature-gated) — but FIRST confirm Echidna's API actually exists (search estate/GitHub for an echidna repo with a documented HTTP API); if it does not, keep the honest Unavailable stub and say so plainly rather than invent a contract. After M7 the roadmap's tractable items are exhausted.",
 ]
 
 [maintenance-status]
@@ -406,9 +422,10 @@ last-result = "pass"  # unknown | pass | warn | fail
 open-warnings = 0
 open-failures = 0
 # `just check` (fmt-check + clippy -D warnings + build + test + SPDX) green
-# post-M6-followon: 125 lib + 43 integration = 168 tests pass. M6 lake-env
-# import resolution dogfooded vs real Lean 4.13.0 + Lake 5.0.0 (imported file in
-# a built lake project → proven; outside → error). codeql.yml added
+# post-M4-followon: 130 lib + 43 integration = 173 tests pass. M4 totality-hole
+# + partial lint dogfooded vs real idris2 0.7.0 (green --check capped to amber).
+# M6 lake-env import resolution dogfooded vs real Lean 4.13.0 + Lake 5.0.0
+# (imported file in a built lake project → proven; outside → error). codeql.yml added
 # (code-scanning gate fix). M10 Mizar adapter dogfooded vs real Mizar 8.1.15
 # (proven/error via accom+verifier+.err; MIZFILES=/opt/mizar; doctor [OK]
 # mizar). M9 Isabelle dogfooded vs Isabelle2025; M8 Coq dogfooded vs coqc

src/lint/idris2.rs

@@ -9,11 +9,12 @@
 //! in Idris2 and a `believe_me` in Agda get the same honest treatment.
 //!
 //! Flags the Idris2 trust/escape primitives `believe_me`, `assert_total`,
-//! `assert_smaller`, `idris_crash`, and the `%default partial` directive.
-//! Idris2 `--check` exits 0 even when these are present, so without this rule
-//! they would silently ride along in an otherwise-green verdict — exactly the
-//! silent-failure class arghda exists to surface. Totality holes (`?name`)
-//! and per-def `partial` modifiers are a documented follow-on.
+//! `assert_smaller`, `idris_crash`, the `%default partial` directive, a
+//! per-definition `partial` modifier (opts that definition out of totality
+//! checking), and totality holes `?name` (incomplete terms/proofs). Idris2
+//! `--check` exits 0 even when these are present, so without this rule they
+//! would silently ride along in an otherwise-green verdict — exactly the
+//! silent-failure class arghda exists to surface.
 
 use super::{LintContext, LintRule};
 use crate::diagnostic::{Diagnostic, LintReport, Severity};
@@ -45,17 +46,29 @@ impl LintRule for Idris2EscapeHatch {
             if trimmed.starts_with("--") {
                 continue; // whole-line comment
             }
-            // The `%default partial` directive turns off totality checking.
+            // Everything below ignores a trailing line comment.
+            let code = line.split(" --").next().unwrap_or(line);
+            // The `%default partial` directive turns off totality checking
+            // file-wide.
             if trimmed.starts_with("%default") && trimmed.contains("partial") {
                 report.push(warn(
                     self.name(),
                     file,
                     i + 1,
                     "totality escape directive `%default partial`".to_string(),
                 ));
+            } else if has_token(code, "partial") {
+                // A per-definition `partial` modifier opts that definition out
+                // of totality checking (distinct from the file-wide directive
+                // above, which is already reported).
+                report.push(warn(
+                    self.name(),
+                    file,
+                    i + 1,
+                    "totality opt-out `partial` modifier".to_string(),
+                ));
             }
-            // Trust/escape primitives, ignoring any trailing line comment.
-            let code = line.split(" --").next().unwrap_or(line);
+            // Trust/escape primitives.
             for tok in ESCAPE_TOKENS {
                 if has_token(code, tok) {
                     report.push(warn(
@@ -66,11 +79,80 @@ impl LintRule for Idris2EscapeHatch {
                     ));
                 }
             }
+            // Totality holes `?name` — incomplete terms/proofs that `--check`
+            // defers rather than rejects. String literals are blanked first so
+            // a `"?x"` inside a string does not match.
+            for hole in holes(&strip_strings(code)) {
+                report.push(warn(
+                    self.name(),
+                    file,
+                    i + 1,
+                    format!("totality hole `?{hole}`"),
+                ));
+            }
         }
         Ok(())
     }
 }
 
+/// Blank out double-quoted string literals (content → spaces), honouring `\"`
+/// escapes, so a `?name` inside a string is not mistaken for a hole.
+fn strip_strings(line: &str) -> String {
+    let mut out = String::with_capacity(line.len());
+    let mut in_str = false;
+    let mut escaped = false;
+    for c in line.chars() {
+        if in_str {
+            if escaped {
+                escaped = false;
+            } else if c == '\\' {
+                escaped = true;
+            } else if c == '"' {
+                in_str = false;
+            }
+            out.push(' ');
+        } else if c == '"' {
+            in_str = true;
+            out.push(' ');
+        } else {
+            out.push(c);
+        }
+    }
+    out
+}
+
+/// The hole names in `code`: a `?` that begins a token (start of line or after
+/// whitespace / an opening bracket / a separator / `=`) and is followed by an
+/// identifier. This distinguishes a hole `?goal` from a user operator like
+/// `<?>` (where `?` is surrounded by symbol chars).
+fn holes(code: &str) -> Vec<String> {
+    let b = code.as_bytes();
+    let mut out = Vec::new();
+    let mut i = 0;
+    while i < b.len() {
+        if b[i] == b'?' {
+            let prev_ok = i == 0
+                || matches!(
+                    b[i - 1],
+                    b' ' | b'\t' | b'(' | b'[' | b'{' | b',' | b';' | b'='
+                );
+            let next_ok = i + 1 < b.len() && (b[i + 1].is_ascii_alphabetic() || b[i + 1] == b'_');
+            if prev_ok && next_ok {
+                let mut j = i + 1;
+                while j < b.len() && (b[j].is_ascii_alphanumeric() || b[j] == b'_' || b[j] == b'\'')
+                {
+                    j += 1;
+                }
+                out.push(code[i + 1..j].to_string());
+                i = j;
+                continue;
+            }
+        }
+        i += 1;
+    }
+    out
+}
+
 fn warn(rule: &str, file: &Path, line: usize, message: String) -> Diagnostic {
     Diagnostic {
         rule: rule.to_string(),
@@ -137,4 +219,38 @@ mod tests {
         let r = lint_str("module M\n\ngreeting : String\ngreeting = \"hi\"\n");
         assert!(r.diagnostics.is_empty());
     }
+
+    #[test]
+    fn per_def_partial_modifier_is_warned() {
+        let r = lint_str("module M\n\npartial\nloop : Nat -> Nat\nloop x = loop x\n");
+        assert_eq!(r.warns().count(), 1);
+        assert!(r.diagnostics[0].message.contains("partial"));
+    }
+
+    #[test]
+    fn totality_hole_is_warned() {
+        let r = lint_str("module M\n\nf : Nat\nf = ?rhs\n");
+        assert_eq!(r.warns().count(), 1);
+        assert_eq!(r.diagnostics[0].rule, "escape-hatch");
+        assert!(r.diagnostics[0].message.contains("?rhs"));
+    }
+
+    #[test]
+    fn hole_inside_a_string_is_not_flagged() {
+        let r = lint_str("module M\n\nmsg : String\nmsg = \"what is ?this\"\n");
+        assert!(r.diagnostics.is_empty());
+    }
+
+    #[test]
+    fn question_operator_is_not_a_hole() {
+        // A user operator like `<?>` has `?` between symbol chars — not a hole.
+        let r = lint_str("module M\n\n(<?>) : Maybe a -> a -> a\n");
+        assert!(r.diagnostics.is_empty());
+    }
+
+    #[test]
+    fn total_modifier_is_not_flagged() {
+        let r = lint_str("module M\n\ntotal\ng : Nat -> Nat\ng x = x\n");
+        assert!(r.diagnostics.is_empty());
+    }
 }