feat(lint): add escape-hatch + tab-mix rules

Rounds out the v0.1 rule pack with the two cheap, high-value rules from
the spec/plan that need no external tooling.

- `escape-hatch` (warn): surfaces soundness escape hatches — the
  termination-checker overrides (`TERMINATING`, `NON_TERMINATING`,
  `NO_TERMINATION_CHECK`) and the trust primitives
  (`believe_me`/`primTrustMe`). Warn, not hard-block: these are
  sometimes legitimately budgeted (echo-types' quarantine discipline),
  so the rule makes them visible without blocking promotion. Precise:
  it ignores the words in `--` comments and only matches whole tokens
  (so `believe_me_helper` does not trip it).
- `tab-mix` (warn): a tab in leading whitespace (Agda style is spaces).

Verification
- cargo fmt/clippy(-D warnings)/test clean; 28 tests (+7 unit).
- Re-dogfooded on echo-types: 0 escape-hatch/tab-mix hits, confirmed a
  TRUE negative by ground-truth grep — the only two `.agda` files
  containing the word "TERMINATING" carry it in `-- TERMINATING
  CONDITION` comments, not pragmas, which the rule correctly skips. A
  synthetic file with a real `{-# TERMINATING #-}` + `believe_me`
  produces exactly two warns.

`missing-without-k` is intentionally not added: `missing-safe-pragma`
already reports a missing `--without-K`. Still deferred:
`unpinned-headline` (needs Smoke.agda parsing + configurable regex),
`unused-import` (shells out to agda-unused), content-hash invalidation,
the Groove manifest, and the `.machine_readable/` RSR retrofit.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019GiSiEfgZCte35dyykgBHs

Author: claude

README.md

@@ -19,6 +19,10 @@ record.
     reachability is the *union*, so a module verified from any root is not
     an orphan)
   - `unjustified-postulate` — `postulate` without an adjacent `-- JUSTIFY:` comment
+  - `escape-hatch` (warn) — termination overrides (`TERMINATING`,
+    `NON_TERMINATING`, `NO_TERMINATION_CHECK`) and trust primitives
+    (`believe_me`/`primTrustMe`)
+  - `tab-mix` (warn) — a tab in leading whitespace
 - Workspace state machine — transitions are file moves, each logged to
   `.arghda/events.jsonl` (`claim`, `promote`, `reject`, `requeue`,
   `invalidate`)
@@ -40,9 +44,11 @@ plus standalone scratch files. `scan` also flags the files deliberately
 outside the `--safe --without-K` kernel cone (`Fidelity.agda`, the cubical
 island, the postulated shadow).
 
-Not yet: the remaining lint rules (`missing-without-k`, `unpinned-headline`,
-`unused-import`, `tab-mix`), content-hash invalidation of `proven`, the
-Groove service manifest, and the `.machine_readable/` RSR retrofit.
+Not yet: `unpinned-headline` (needs `Smoke.agda` parsing + a configurable
+regex) and `unused-import` (shells out to `agda-unused`); content-hash
+invalidation of `proven`; the Groove service manifest; and the
+`.machine_readable/` RSR retrofit. (`missing-without-k` is subsumed by
+`missing-safe-pragma`, which already reports a missing `--without-K`.)
 
 ## Build
 

src/lint/escape_hatch.rs

@@ -0,0 +1,132 @@
+//! `escape-hatch` (warn) — surface soundness escape hatches.
+//!
+//! Flags termination-checker overrides (`{-# TERMINATING #-}`,
+//! `NON_TERMINATING`, `NO_TERMINATION_CHECK`) and the trust primitives
+//! `believe_me` / `primTrustMe`. These are sometimes legitimately budgeted
+//! (see echo-types' quarantine discipline), so this is a *warn*, not a
+//! hard-block: it makes the hatch visible to the operator / visual layer
+//! without blocking promotion. The postulate case is handled separately by
+//! `unjustified-postulate` (hard-block when there is no `-- JUSTIFY:`).
+
+use super::{LintContext, LintRule};
+use crate::diagnostic::{Diagnostic, LintReport, Severity};
+use anyhow::{Context, Result};
+use std::fs;
+use std::path::Path;
+
+pub struct EscapeHatch;
+
+const TERMINATION_PRAGMAS: &[&str] = &["TERMINATING", "NON_TERMINATING", "NO_TERMINATION_CHECK"];
+const TRUST_PRIMS: &[&str] = &["believe_me", "primTrustMe"];
+
+impl LintRule for EscapeHatch {
+    fn name(&self) -> &'static str {
+        "escape-hatch"
+    }
+
+    fn run(&self, file: &Path, _ctx: &LintContext<'_>, report: &mut LintReport) -> Result<()> {
+        let contents =
+            fs::read_to_string(file).with_context(|| format!("reading {}", file.display()))?;
+        for (i, line) in contents.lines().enumerate() {
+            let trimmed = line.trim_start();
+            if trimmed.starts_with("--") {
+                continue; // whole-line comment
+            }
+            // Termination-checker override pragmas.
+            if trimmed.starts_with("{-#") {
+                for p in TERMINATION_PRAGMAS {
+                    if line.contains(p) {
+                        report.push(warn(
+                            self.name(),
+                            file,
+                            i + 1,
+                            format!("termination escape pragma `{p}`"),
+                        ));
+                    }
+                }
+            }
+            // Trust primitives, ignoring any trailing line comment.
+            let code = line.split(" --").next().unwrap_or(line);
+            for prim in TRUST_PRIMS {
+                if has_token(code, prim) {
+                    report.push(warn(
+                        self.name(),
+                        file,
+                        i + 1,
+                        format!("trust primitive `{prim}`"),
+                    ));
+                }
+            }
+        }
+        Ok(())
+    }
+}
+
+fn warn(rule: &str, file: &Path, line: usize, message: String) -> Diagnostic {
+    Diagnostic {
+        rule: rule.to_string(),
+        severity: Severity::Warn,
+        file: file.to_path_buf(),
+        message,
+        line: Some(line),
+    }
+}
+
+/// `tok` appears in `s` as a whitespace/paren-delimited token (so a longer
+/// identifier like `believe_me_helper` does not match).
+fn has_token(s: &str, tok: &str) -> bool {
+    s.split(|c: char| c.is_whitespace() || "(){};,".contains(c))
+        .any(|w| w == tok)
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use crate::lint::run_lints;
+    use std::path::PathBuf;
+
+    fn lint_str(body: &str) -> LintReport {
+        let tmp = tempfile::NamedTempFile::new().unwrap();
+        std::fs::write(tmp.path(), body).unwrap();
+        let roots: [PathBuf; 0] = [];
+        let ctx = LintContext {
+            include_root: tmp.path().parent().unwrap(),
+            entry_modules: &roots,
+        };
+        let rules: Vec<Box<dyn LintRule>> = vec![Box::new(EscapeHatch)];
+        run_lints(tmp.path(), &ctx, &rules).unwrap()
+    }
+
+    #[test]
+    fn terminating_pragma_is_warned() {
+        let r = lint_str("module M where\n{-# TERMINATING #-}\nf : Set\n");
+        assert!(!r.has_hard_block());
+        assert_eq!(r.warns().count(), 1);
+        assert!(r.diagnostics[0].message.contains("TERMINATING"));
+    }
+
+    #[test]
+    fn believe_me_token_is_warned() {
+        let r = lint_str("module M where\nx = believe_me 0\n");
+        assert_eq!(r.warns().count(), 1);
+        assert!(r.diagnostics[0].message.contains("believe_me"));
+    }
+
+    #[test]
+    fn believe_me_in_comment_is_ignored() {
+        let r = lint_str("module M where\nx = 0 -- todo: avoid believe_me here\n");
+        assert!(r.diagnostics.is_empty());
+    }
+
+    #[test]
+    fn longer_identifier_does_not_match() {
+        let r = lint_str("module M where\nbelieve_me_helper = 0\n");
+        assert!(r.diagnostics.is_empty());
+    }
+
+    #[test]
+    fn clean_file_is_silent() {
+        let r = lint_str("module M where\nf : Set\nf = Set\n");
+        assert!(r.diagnostics.is_empty());
+    }
+}

src/lint/mod.rs

@@ -2,9 +2,11 @@ use crate::diagnostic::LintReport;
 use anyhow::Result;
 use std::path::{Path, PathBuf};
 
+pub mod escape_hatch;
 pub mod orphan_module;
 pub mod postulate;
 pub mod safe_pragma;
+pub mod tab_mix;
 
 /// Context handed to every rule.
 #[derive(Clone, Debug)]
@@ -28,6 +30,8 @@ pub fn default_rules() -> Vec<Box<dyn LintRule>> {
         Box::new(safe_pragma::SafePragma),
         Box::new(orphan_module::OrphanModule),
         Box::new(postulate::UnjustifiedPostulate),
+        Box::new(escape_hatch::EscapeHatch),
+        Box::new(tab_mix::TabMix),
     ]
 }
 

src/lint/tab_mix.rs

@@ -0,0 +1,75 @@
+//! `tab-mix` (warn) — flag tabs used for indentation.
+//!
+//! Agda's layout rule and the estate style use spaces; a stray tab in
+//! leading whitespace breaks alignment and, inside a layout block, can
+//! change how the file parses. Reported once per file (first offending
+//! line) to keep the signal quiet.
+
+use super::{LintContext, LintRule};
+use crate::diagnostic::{Diagnostic, LintReport, Severity};
+use anyhow::{Context, Result};
+use std::fs;
+use std::path::Path;
+
+pub struct TabMix;
+
+impl LintRule for TabMix {
+    fn name(&self) -> &'static str {
+        "tab-mix"
+    }
+
+    fn run(&self, file: &Path, _ctx: &LintContext<'_>, report: &mut LintReport) -> Result<()> {
+        let contents =
+            fs::read_to_string(file).with_context(|| format!("reading {}", file.display()))?;
+        for (i, line) in contents.lines().enumerate() {
+            let leading_has_tab = line
+                .chars()
+                .take_while(|c| *c == ' ' || *c == '\t')
+                .any(|c| c == '\t');
+            if leading_has_tab {
+                report.push(Diagnostic {
+                    rule: self.name().to_string(),
+                    severity: Severity::Warn,
+                    file: file.to_path_buf(),
+                    message: "tab in leading whitespace (Agda style is spaces)".to_string(),
+                    line: Some(i + 1),
+                });
+                break; // one report per file is enough signal
+            }
+        }
+        Ok(())
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use crate::lint::run_lints;
+    use std::path::PathBuf;
+
+    fn lint_str(body: &str) -> LintReport {
+        let tmp = tempfile::NamedTempFile::new().unwrap();
+        std::fs::write(tmp.path(), body).unwrap();
+        let roots: [PathBuf; 0] = [];
+        let ctx = LintContext {
+            include_root: tmp.path().parent().unwrap(),
+            entry_modules: &roots,
+        };
+        let rules: Vec<Box<dyn LintRule>> = vec![Box::new(TabMix)];
+        run_lints(tmp.path(), &ctx, &rules).unwrap()
+    }
+
+    #[test]
+    fn leading_tab_is_warned_not_blocked() {
+        let r = lint_str("module M where\n\tx = 1\n");
+        assert!(!r.has_hard_block());
+        assert_eq!(r.warns().count(), 1);
+        assert_eq!(r.diagnostics[0].line, Some(2));
+    }
+
+    #[test]
+    fn space_indented_is_clean() {
+        let r = lint_str("module M where\n  x = 1\n");
+        assert!(r.diagnostics.is_empty());
+    }
+}