From 62dc491b0351bd7fb10f80aa98509257dd136501 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Sun, 26 Jul 2026 17:48:07 +0100
Subject: [PATCH] test: add unit test for check-trusted-base.sh

fix: ignore string literals when matching Lean sorry/axiom

Resolves #517
---
 scripts/check-trusted-base.sh    |  5 ++++
 tests/test_check_trusted_base.sh | 43 ++++++++++++++++++++++++++++++++
 2 files changed, 48 insertions(+)
 create mode 100755 tests/test_check_trusted_base.sh

diff --git a/scripts/check-trusted-base.sh b/scripts/check-trusted-base.sh
index ef5121b5..d2de0aa0 100755
--- a/scripts/check-trusted-base.sh
+++ b/scripts/check-trusted-base.sh
@@ -103,6 +103,11 @@ done
 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)"
   done
 done
diff --git a/tests/test_check_trusted_base.sh b/tests/test_check_trusted_base.sh
new file mode 100755
index 00000000..4bf94f1c
--- /dev/null
+++ b/tests/test_check_trusted_base.sh
@@ -0,0 +1,43 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+
+set -euo pipefail
+
+SCRIPT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
+CHECK_SCRIPT="${SCRIPT_DIR}/../scripts/check-trusted-base.sh"
+
+TEST_DIR=$(mktemp -d)
+trap 'rm -rf "$TEST_DIR"' EXIT
+
+echo "Running check-trusted-base.sh tests..."
+
+# Test 1: Should ignore 'sorry' in string literals
+cat << 'EOF' > "${TEST_DIR}/string_literal.lean"
+def my_keywords : List String := ["sorry", "axiom"]
+EOF
+
+# Provide an empty proof-debt file to satisfy the script's basic requirements
+mkdir -p "${TEST_DIR}/docs"
+touch "${TEST_DIR}/docs/proof-debt.md"
+
+if "${CHECK_SCRIPT}" "${TEST_DIR}" > /dev/null; then
+  echo "PASS: Ignored 'sorry' in string literals."
+else
+  echo "FAIL: Matched 'sorry' in string literals incorrectly."
+  exit 1
+fi
+
+# Test 2: Should flag actual 'sorry'
+cat << 'EOF' > "${TEST_DIR}/actual_sorry.lean"
+theorem fermat : a ^ n + b ^ n = c ^ n := by
+  sorry
+EOF
+
+if "${CHECK_SCRIPT}" "${TEST_DIR}" > /dev/null; then
+  echo "FAIL: Failed to flag actual 'sorry'."
+  exit 1
+else
+  echo "PASS: Flagged actual 'sorry'."
+fi
+
+echo "All tests passed!"