From ac91747f685201bf5b09de2bd868083a4c3869db Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Sat, 29 Aug 2026 13:47:13 +0100
Subject: [PATCH 1/3] fix(governance): ignore Coq multiline comments

---
 scripts/check-trusted-base.sh            | 28 ++++++++++++++++++--
 scripts/tests/check-trusted-base-test.sh | 33 ++++++++++++++++++++++++
 2 files changed, 59 insertions(+), 2 deletions(-)

diff --git a/scripts/check-trusted-base.sh b/scripts/check-trusted-base.sh
index 40e727c7..3e62104f 100755
--- a/scripts/check-trusted-base.sh
+++ b/scripts/check-trusted-base.sh
@@ -91,11 +91,35 @@ emit_marker() {
   printf '%s\t%s\t%s\t%s\n' "$1" "$2" "$3" "$4" >> "$markers_tsv"
 }
 
+# Coq comments nest and may span lines. A line-oriented grep sees prose inside
+# `(* ... *)` as code whenever the interior line does not begin with a comment
+# delimiter. Strip nested block comments while preserving line count before
+# looking for proof escape hatches.
+strip_coq_noncode() {
+  awk '
+    {
+      line = $0; out = ""; i = 1; n = length(line)
+      while (i <= n) {
+        pair = substr(line, i, 2)
+        if (depth > 0) {
+          if (pair == "(*") { depth++; i += 2; continue }
+          if (pair == "*)") { depth--; i += 2; continue }
+          i++; continue
+        }
+        if (pair == "(*") { depth++; i += 2; continue }
+        out = out substr(line, i, 1); i++
+      }
+      print out
+    }
+  ' "$1"
+}
+
 # Coq Axiom / Admitted
 echo "$proof_files" | grep -E '\.v$' | while read -r f; do
   [ -z "$f" ] && continue
-  grep -nE '^[[:space:]]*(Axiom|Admitted|admit\.)' "$f" 2>/dev/null | while IFS=: read -r ln rest; do
-    emit_marker "$f" "$ln" "coq-axiom-or-admit" "$(echo "$rest" | head -c 80)"
+  strip_coq_noncode "$f" 2>/dev/null | grep -nE '^[[:space:]]*(Axiom|Admitted|admit\.)' | while IFS=: read -r ln rest; do
+    orig="$(sed -n "${ln}p" "$f" 2>/dev/null)"
+    emit_marker "$f" "$ln" "coq-axiom-or-admit" "$(echo "$orig" | head -c 80)"
   done
 done
 
diff --git a/scripts/tests/check-trusted-base-test.sh b/scripts/tests/check-trusted-base-test.sh
index 66f27ee6..3b099863 100755
--- a/scripts/tests/check-trusted-base-test.sh
+++ b/scripts/tests/check-trusted-base-test.sh
@@ -185,6 +185,33 @@ test/fixtures/
 EOF
 }
 
+setup_coq_multiline_comments_only() {
+  mkdir -p formal
+  cat > formal/Commentary.v <<'EOF'
+(** A documentation block may discuss old proof state.
+    Admitted markers in prior revisions are not executable here.
+    (* Nested comments may also mention:
+       admit.
+    *)
+    Axiom references in prose are not declarations. *)
+Theorem closed : True.
+Proof. exact I. Qed.
+EOF
+}
+
+setup_coq_comment_then_real_admitted() {
+  mkdir -p formal docs
+  cat > formal/ActualDebt.v <<'EOF'
+(* Admitted. inside a comment must not count. *)
+Theorem open_obligation : True.
+Admitted.
+EOF
+  cat > docs/proof-debt.md <<'EOF'
+# Proof Debt
+(Intentionally empty: the real marker must fail this positive control.)
+EOF
+}
+
 # Existing behaviour must still work.
 run_case "marker with no docs and no ignore fails (early exit)" \
   1 "No docs/proof-debt.md (or equivalent) found" setup_marker_no_docs
@@ -211,6 +238,12 @@ run_case "ignore pattern that does not match still fails" \
 run_case "mixed: one marker exempted, one documented in proof-debt" \
   0 "1 marker(s) exempted via .trusted-base-ignore" setup_mixed_exempt_and_documented
 
+run_case "Coq nested multiline comment prose is not executable debt" \
+  0 "No soundness-relevant escape hatches detected" setup_coq_multiline_comments_only
+
+run_case "real Coq Admitted after a comment still fails" \
+  1 "1/1 escape hatch(es) are undocumented" setup_coq_comment_then_real_admitted
+
 echo
 echo "PASS=$PASS FAIL=$FAIL"
 if [[ "$FAIL" -gt 0 ]]; then

From e6fbdf14e6b28dd1bb293f5f5ff73435a1f0a057 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Sat, 29 Aug 2026 13:53:19 +0100
Subject: [PATCH 2/3] fix(governance): prevent Coq scanner under-flags

---
 scripts/check-trusted-base.sh            | 23 +++++++++++++-----
 scripts/tests/check-trusted-base-test.sh | 31 ++++++++++++++++++++++++
 2 files changed, 48 insertions(+), 6 deletions(-)

diff --git a/scripts/check-trusted-base.sh b/scripts/check-trusted-base.sh
index 3e62104f..ca56fad1 100755
--- a/scripts/check-trusted-base.sh
+++ b/scripts/check-trusted-base.sh
@@ -93,21 +93,29 @@ emit_marker() {
 
 # Coq comments nest and may span lines. A line-oriented grep sees prose inside
 # `(* ... *)` as code whenever the interior line does not begin with a comment
-# delimiter. Strip nested block comments while preserving line count before
-# looking for proof escape hatches.
+# delimiter. Strip nested block comments and strings while preserving line
+# count before looking for proof escape hatches. String state deliberately
+# resets on each line: malformed input must over-flag, never hide the remainder
+# of a file from this soundness gate. Coq escapes a quote as `""` in strings.
 strip_coq_noncode() {
   awk '
     {
-      line = $0; out = ""; i = 1; n = length(line)
+      line = $0; out = ""; i = 1; n = length(line); instr = 0
       while (i <= n) {
-        pair = substr(line, i, 2)
+        c = substr(line, i, 1); pair = substr(line, i, 2)
         if (depth > 0) {
           if (pair == "(*") { depth++; i += 2; continue }
           if (pair == "*)") { depth--; i += 2; continue }
           i++; continue
         }
+        if (instr) {
+          if (pair == "\"\"") { i += 2; continue }
+          if (c == "\"") { instr = 0; i++; continue }
+          i++; continue
+        }
         if (pair == "(*") { depth++; i += 2; continue }
-        out = out substr(line, i, 1); i++
+        if (c == "\"") { instr = 1; i++; continue }
+        out = out c; i++
       }
       print out
     }
@@ -119,7 +127,10 @@ echo "$proof_files" | grep -E '\.v$' | while read -r f; do
   [ -z "$f" ] && continue
   strip_coq_noncode "$f" 2>/dev/null | grep -nE '^[[:space:]]*(Axiom|Admitted|admit\.)' | while IFS=: read -r ln rest; do
     orig="$(sed -n "${ln}p" "$f" 2>/dev/null)"
-    emit_marker "$f" "$ln" "coq-axiom-or-admit" "$(echo "$orig" | head -c 80)"
+    # The language-aware pass already removed comments. Do not feed the
+    # original line through the generic prefix heuristic: `(* note *) Admitted.`
+    # is executable debt even though its original text begins with a comment.
+    printf '%s\t%s\t%s\t%s\n' "$f" "$ln" "coq-axiom-or-admit" "$(echo "$orig" | head -c 80)" >> "$markers_tsv"
   done
 done
 
diff --git a/scripts/tests/check-trusted-base-test.sh b/scripts/tests/check-trusted-base-test.sh
index 3b099863..e40a9bc1 100755
--- a/scripts/tests/check-trusted-base-test.sh
+++ b/scripts/tests/check-trusted-base-test.sh
@@ -212,6 +212,31 @@ EOF
 EOF
 }
 
+setup_coq_string_delimiters_then_real_marker() {
+  mkdir -p formal docs
+  cat > formal/StringDelimiter.v <<'EOF'
+From Coq Require Import Strings.String.
+Definition opening_delimiter : string := "(* not a comment".
+Definition escaped_quote : string := "text "" (* still a string".
+Axiom string_delimiters_do_not_hide_this : True.
+EOF
+  cat > docs/proof-debt.md <<'EOF'
+# Proof Debt
+(Intentionally empty: a string delimiter must not hide the real axiom.)
+EOF
+}
+
+setup_coq_leading_comment_then_real_marker() {
+  mkdir -p formal docs
+  cat > formal/LeadingComment.v <<'EOF'
+(* explanatory prefix *) Admitted.
+EOF
+  cat > docs/proof-debt.md <<'EOF'
+# Proof Debt
+(Intentionally empty: a leading comment must not hide the real marker.)
+EOF
+}
+
 # Existing behaviour must still work.
 run_case "marker with no docs and no ignore fails (early exit)" \
   1 "No docs/proof-debt.md (or equivalent) found" setup_marker_no_docs
@@ -244,6 +269,12 @@ run_case "Coq nested multiline comment prose is not executable debt" \
 run_case "real Coq Admitted after a comment still fails" \
   1 "1/1 escape hatch(es) are undocumented" setup_coq_comment_then_real_admitted
 
+run_case "Coq comment delimiters inside strings cannot hide a later axiom" \
+  1 "1/1 escape hatch(es) are undocumented" setup_coq_string_delimiters_then_real_marker
+
+run_case "real Coq marker after a same-line leading comment still fails" \
+  1 "1/1 escape hatch(es) are undocumented" setup_coq_leading_comment_then_real_marker
+
 echo
 echo "PASS=$PASS FAIL=$FAIL"
 if [[ "$FAIL" -gt 0 ]]; then

From 92d65376014218f55c3b0cf9f4bb2ddcfaa0469a Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Sat, 29 Aug 2026 13:56:29 +0100
Subject: [PATCH 3/3] fix(governance): track multiline Coq strings

---
 scripts/check-trusted-base.sh            | 24 ++++++++++++++----------
 scripts/tests/check-trusted-base-test.sh | 23 +++++++++++++++++++++++
 2 files changed, 37 insertions(+), 10 deletions(-)

diff --git a/scripts/check-trusted-base.sh b/scripts/check-trusted-base.sh
index ca56fad1..39893352 100755
--- a/scripts/check-trusted-base.sh
+++ b/scripts/check-trusted-base.sh
@@ -94,31 +94,35 @@ emit_marker() {
 # Coq comments nest and may span lines. A line-oriented grep sees prose inside
 # `(* ... *)` as code whenever the interior line does not begin with a comment
 # delimiter. Strip nested block comments and strings while preserving line
-# count before looking for proof escape hatches. String state deliberately
-# resets on each line: malformed input must over-flag, never hide the remainder
-# of a file from this soundness gate. Coq escapes a quote as `""` in strings.
+# count before looking for proof escape hatches. Coq permits multiline strings
+# and escapes a quote as `""`, so string state spans lines and takes precedence
+# over comment delimiters. An unterminated string emits a synthetic marker so
+# malformed input fails closed instead of hiding the remainder of the file.
 strip_coq_noncode() {
   awk '
     {
-      line = $0; out = ""; i = 1; n = length(line); instr = 0
+      line = $0; out = ""; i = 1; n = length(line)
       while (i <= n) {
         c = substr(line, i, 1); pair = substr(line, i, 2)
-        if (depth > 0) {
-          if (pair == "(*") { depth++; i += 2; continue }
-          if (pair == "*)") { depth--; i += 2; continue }
-          i++; continue
-        }
         if (instr) {
           if (pair == "\"\"") { i += 2; continue }
           if (c == "\"") { instr = 0; i++; continue }
           i++; continue
         }
-        if (pair == "(*") { depth++; i += 2; continue }
         if (c == "\"") { instr = 1; i++; continue }
+        if (depth > 0) {
+          if (pair == "(*") { depth++; i += 2; continue }
+          if (pair == "*)") { depth--; i += 2; continue }
+          i++; continue
+        }
+        if (pair == "(*") { depth++; i += 2; continue }
         out = out c; i++
       }
       print out
     }
+    END {
+      if (instr) print "Axiom __unterminated_coq_string"
+    }
   ' "$1"
 }
 
diff --git a/scripts/tests/check-trusted-base-test.sh b/scripts/tests/check-trusted-base-test.sh
index e40a9bc1..eb859bcf 100755
--- a/scripts/tests/check-trusted-base-test.sh
+++ b/scripts/tests/check-trusted-base-test.sh
@@ -218,6 +218,13 @@ setup_coq_string_delimiters_then_real_marker() {
 From Coq Require Import Strings.String.
 Definition opening_delimiter : string := "(* not a comment".
 Definition escaped_quote : string := "text "" (* still a string".
+Definition multiline_delimiters : string := "first line
+(* neither opens a comment
+nor does this close one *)
+last line".
+(* A quoted delimiter inside a real comment must not change its depth:
+   "(*"
+*)
 Axiom string_delimiters_do_not_hide_this : True.
 EOF
   cat > docs/proof-debt.md <<'EOF'
@@ -226,6 +233,19 @@ EOF
 EOF
 }
 
+setup_coq_unterminated_string() {
+  mkdir -p formal docs
+  cat > formal/UnterminatedString.v <<'EOF'
+From Coq Require Import Strings.String.
+Definition malformed : string := "this never closes
+Admitted.
+EOF
+  cat > docs/proof-debt.md <<'EOF'
+# Proof Debt
+(Intentionally empty: malformed input must fail closed.)
+EOF
+}
+
 setup_coq_leading_comment_then_real_marker() {
   mkdir -p formal docs
   cat > formal/LeadingComment.v <<'EOF'
@@ -275,6 +295,9 @@ run_case "Coq comment delimiters inside strings cannot hide a later axiom" \
 run_case "real Coq marker after a same-line leading comment still fails" \
   1 "1/1 escape hatch(es) are undocumented" setup_coq_leading_comment_then_real_marker
 
+run_case "unterminated Coq string fails closed instead of hiding the file" \
+  1 "1/1 escape hatch(es) are undocumented" setup_coq_unterminated_string
+
 echo
 echo "PASS=$PASS FAIL=$FAIL"
 if [[ "$FAIL" -gt 0 ]]; then