From 5aeaf0d069ed436fcc9a3de0cbaaf19177129cf7 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Mon, 27 Jul 2026 13:58:13 +0100
Subject: [PATCH] fix(check-trusted-base): make Lean sorry/axiom matching
 comment-aware

The Lean branch stripped only `"string literals"` from a single line before
matching, so it could not see Lean comments -- which nest and span lines. A
docstring that merely MENTIONS `sorry` was therefore reported as a
soundness-relevant escape hatch, and the repo was told to seed
docs/proof-debt.md for a hatch that does not exist.

Found in systemet, whose Audit.lean documents its own policy:

  "A theorem that elaborates but smuggles in an axiom or a `sorry` through
   an import fails the gate here, not in a status document."

  -> [INFO] Found 1 soundness-relevant escape hatch(es).
     [ERROR] No docs/proof-debt.md ... but 1 escape hatches exist.

That repo's axiom audit reports [propext, Quot.sound] for all 20 headline
items; there was no hatch. Any repo that documents its own sorry/axiom policy
in a docstring hits this -- i.e. exactly the repos taking the policy most
seriously. The pressure it creates is to declare debt that does not exist,
which is the opposite of what this gate is for.

Fix: strip_lean_noncode() blanks line comments (--), nesting block comments and
docstrings (/- -/, /-! -/, /-- -/) and string literals, preserving line numbers
so reported positions stay accurate. Markers still quote the ORIGINAL line.
Same comment-awareness fix scan-dangerous.sh already carries for Lean.

Failure direction is deliberate: string state is NOT carried across lines, so an
odd quote over-flags rather than blanking the rest of a file. For a soundness
gate, over-flagging is safe; under-flagging is not.

Verified with fixtures -- must catch real holes, must ignore prose:

  line 1  /-! docstring ... `sorry` ... -/          NOT flagged  (was the bug)
  line 2  -- line comment mentioning sorry/axiom     NOT flagged
  line 3  /- /- nested -/ sorry -/                   NOT flagged
  line 4  def s : String := "the word sorry ..."     NOT flagged
  line 5  theorem realHole : True := by sorry        FLAGGED
  line 6  axiom realAxiom : False                    FLAGGED
  line 7  theorem t : True := by sorry -- trailing   FLAGGED
  line 8  theorem fine : True := trivial             NOT flagged

3 found, all genuine. Before this change the same fixture also reported the
four comment/string lines. `bash -n` clean.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
---
 scripts/check-trusted-base.sh | 51 ++++++++++++++++++++++++++++++-----
 1 file changed, 44 insertions(+), 7 deletions(-)

diff --git a/scripts/check-trusted-base.sh b/scripts/check-trusted-base.sh
index d2de0aa0..40e727c7 100755
--- a/scripts/check-trusted-base.sh
+++ b/scripts/check-trusted-base.sh
@@ -100,15 +100,52 @@ echo "$proof_files" | grep -E '\.v$' | while read -r f; do
 done
 
 # Lean sorry / axiom
+#
+# Matching must be COMMENT-AWARE. The previous implementation stripped only
+# "string literals" from a single line, so a docstring that merely MENTIONS
+# `sorry` -- e.g. a repo documenting that its own gate rejects smuggled
+# sorries -- was reported as a soundness-relevant escape hatch, and the repo
+# was then told to seed docs/proof-debt.md for a hatch that does not exist.
+# Lean block comments nest and span lines, so per-line string stripping cannot
+# see them. strip_lean_noncode() blanks line comments (--), nesting block
+# comments and docstrings (/- -/, /-! -/, /-- -/) and string literals, while
+# preserving line numbers so reported line numbers stay accurate.
+#
+# Failure direction is deliberate: string state is NOT carried across lines, so
+# an odd quote over-flags rather than blanking the remainder of a file. For a
+# soundness gate, over-flagging is safe and under-flagging is not.
+strip_lean_noncode() {
+  awk '
+    {
+      line = $0; out = ""; i = 1; n = length(line); instr = 0
+      while (i <= n) {
+        c = substr(line, i, 1); c2 = substr(line, i, 2)
+        if (depth > 0) {
+          if (c2 == "-/") { depth--; i += 2; continue }
+          if (c2 == "/-") { depth++; i += 2; continue }
+          i++; continue
+        }
+        if (instr) {
+          if (c == "\\") { i += 2; continue }
+          if (c == "\"") { instr = 0; i++; continue }
+          i++; continue
+        }
+        if (c2 == "/-") { depth++; i += 2; continue }
+        if (c2 == "--") { break }
+        if (c == "\"") { instr = 1; i++; continue }
+        out = out c; i++
+      }
+      print out
+    }
+  ' "$1"
+}
+
 echo "$proof_files" | grep -E '\.lean$' | while read -r f; do
   [ -z "$f" ] && continue
-  grep -nE '\bsorry\b|^[[:space:]]*axiom[[:space:]]' "$f" 2>/dev/null | while IFS=: read -r ln rest; do
-    # Strip string literals to avoid false positives (e.g. from keyword tables or debug strings)
-    rest_no_strings="$(echo "$rest" | sed 's/"[^"]*"//g')"
-    if ! echo "$rest_no_strings" | grep -qE '\bsorry\b|^[[:space:]]*axiom[[:space:]]'; then
-      continue
-    fi
-    emit_marker "$f" "$ln" "lean-sorry-or-axiom" "$(echo "$rest" | head -c 80)"
+  strip_lean_noncode "$f" 2>/dev/null | grep -nE '\bsorry\b|^[[:space:]]*axiom[[:space:]]' | while IFS=: read -r ln rest; do
+    # Report the ORIGINAL line text (the stripped form is only for matching)
+    orig="$(sed -n "${ln}p" "$f" 2>/dev/null)"
+    emit_marker "$f" "$ln" "lean-sorry-or-axiom" "$(echo "$orig" | head -c 80)"
   done
 done