ci(proof): comment-aware honesty-guard, replace brittle inline scan

scripts/honesty-guard.sh strips Idris line/doc/block comments (and is
string-literal aware) before scanning for proof-escape smells: believe_me,
really_believe_me, postulate, assert_total, assert_smaller, idris_crash,
sorry, ?holes, partial. Reports file:line; exit 1 + count on any hit,
exit 0 + "Clean." otherwise. Default scope src/, accepts file/dir args.

Wires it into .github/workflows/proof-corpus.yml in place of the inline
grep, which only filtered comments matched at line start (missed mid-line
-- and {- -} blocks). Same Phase-1 corpus scope. Local invocation noted in
VERIFICATION-STANCE.adoc.

Verified: Clean on the corpus and all of src/; fault-injection confirms it
catches a real believe_me and ?hole while ignoring the same tokens in --,
|||, and {- -} comments.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

.github/workflows/proof-corpus.yml

@@ -57,22 +57,22 @@ jobs:
           echo "$HOME/.idris2/bin" >> "$GITHUB_PATH"
           echo "IDRIS2_PREFIX=$HOME/.idris2" >> "$GITHUB_ENV"
 
-      - name: Proof-escape audit (no believe_me / postulate / assert_* / sorry)
+      - name: Proof-escape audit (honesty guard)
         run: |
           set -euo pipefail
-          # Strip line/block comments, then scan the corpus sources.
-          files="src/core/Grammar.idr src/core/Schema.idr src/core/Decide.idr \
-                 src/core/Levels.idr src/core/Checker.idr \
-                 src/core/Composition.idr src/core/Epistemic.idr \
-                 src/interface/abi/Types.idr src/interface/abi/Layout.idr \
-                 src/interface/abi/LayoutProofs.idr \
-                 src/interface/WireDecode.idr src/interface/WireConformance.idr"
-          if grep -nE '\b(believe_me|really_believe_me|assert_total|assert_smaller|idris_crash|postulate|sorry)\b' \
-               $files | grep -vE ':\s*(--|\|\|\|)' ; then
-            echo "::error::proof-escape symbol found in the Phase-1 corpus"
-            exit 1
-          fi
-          echo "OK: zero proof-escape symbols outside comments"
+          # Robust, comment-aware scan (line --, doc |||, nested {- -}, and
+          # string-literal-aware): scripts/honesty-guard.sh. Scoped to the
+          # Phase-1 corpus sources — the same module set vclut-core.ipkg builds
+          # below. Exits 1 on any believe_me / really_believe_me / postulate /
+          # assert_total / assert_smaller / idris_crash / sorry / ?hole /
+          # partial appearing outside a comment.
+          sh scripts/honesty-guard.sh \
+            src/core/Grammar.idr src/core/Schema.idr src/core/Decide.idr \
+            src/core/Levels.idr src/core/Checker.idr \
+            src/core/Composition.idr src/core/Epistemic.idr \
+            src/interface/abi/Types.idr src/interface/abi/Layout.idr \
+            src/interface/abi/LayoutProofs.idr \
+            src/interface/WireDecode.idr src/interface/WireConformance.idr
 
       - name: Build the proof corpus
         run: |

scripts/honesty-guard.sh

@@ -0,0 +1,101 @@
+#!/bin/sh
+# SPDX-License-Identifier: MPL-2.0
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# honesty-guard.sh — advisory scan for fake-success "proof-escape" smells in
+# the Idris2 corpus. These symbols let a broken proof typecheck and claim a
+# green that it has not earned:
+#
+#   believe_me / really_believe_me   assert any type with zero proof content
+#   postulate                        axiom with no proof
+#   assert_total                     suppress the totality (coverage) checker
+#   assert_smaller                   suppress the termination checker
+#   idris_crash                      runtime abort masquerading as a value
+#   sorry                            unfilled placeholder (Idris2 accepts it)
+#   ?name                            unsolved metavariable / open hole
+#   partial / %default partial       disable coverage+termination checking
+#
+# The scan STRIPS Idris comments first — line (`--`), doc (`|||`), and nested
+# block (`{- -}`) — so a file that merely *names* one of these tokens in prose
+# (as src/interface/abi/LayoutProofs.idr does in its module docstring) is not a
+# false positive. String literals are comment-marker-aware so an in-string
+# `--` cannot hide following code. Line numbers are preserved for reporting.
+#
+# Usage:   scripts/honesty-guard.sh [PATH ...]      (PATH = file or dir; default: src)
+# Exit:    0 + "Clean."                      when no smell is found
+#          1 + "N smell(s) in M file(s)"      and a file:line list otherwise
+#
+# Advisory by design: it is a diagnostic, not a substitute for the
+# totality-checked `idris2 --build` of verification/proofs/vclut-core.ipkg.
+
+set -u
+
+PATTERN='\b(believe_me|really_believe_me|assert_total|assert_smaller|idris_crash|postulate|sorry|partial)\b|\?[A-Za-z_]'
+
+# ---- Idris comment stripper (preserves one output line per input line) ------
+awkprog=$(mktemp)
+filelist=$(mktemp)
+hits=$(mktemp)
+trap 'rm -f "$awkprog" "$filelist" "$hits"' EXIT INT TERM
+
+cat > "$awkprog" <<'AWK'
+# Blank out Idris2 comments while keeping line count stable.
+#   depth : nesting depth of {- -} block comments (persists across lines)
+#   instr : inside a "..." string literal (reset per line; Idris strings
+#           do not span lines except rare triple-quoted forms)
+BEGIN { depth = 0 }
+{
+  line = $0; n = length(line); out = ""; i = 1; instr = 0
+  while (i <= n) {
+    c   = substr(line, i, 1)
+    two = substr(line, i, 2)
+    if (depth > 0) {                       # inside a block comment
+      if (two == "-}") { depth--; i += 2; continue }
+      if (two == "{-") { depth++; i += 2; continue }
+      i++; continue
+    }
+    if (instr) {                           # inside a string literal
+      out = out c
+      if (c == "\\") { i++; if (i <= n) out = out substr(line, i, 1); i++; continue }
+      if (c == "\"") { instr = 0 }
+      i++; continue
+    }
+    if (two == "{-") { depth++; i += 2; continue }   # open block comment
+    if (two == "--") { break }                       # line comment to EOL
+    if (substr(line, i, 3) == "|||") { break }       # doc comment to EOL
+    if (c == "\"") { instr = 1; out = out c; i++; continue }
+    out = out c
+    i++
+  }
+  print out
+}
+AWK
+
+# ---- collect target files ---------------------------------------------------
+[ "$#" -eq 0 ] && set -- src
+for arg in "$@"; do
+  if [ -d "$arg" ]; then
+    find "$arg" -type f -name '*.idr'
+  elif [ -f "$arg" ]; then
+    printf '%s\n' "$arg"
+  else
+    echo "honesty-guard: no such path: $arg" >&2
+  fi
+done | sort -u > "$filelist"
+
+# ---- scan -------------------------------------------------------------------
+while IFS= read -r f; do
+  [ -n "$f" ] || continue
+  awk -f "$awkprog" "$f" | grep -nE "$PATTERN" | sed "s|^|$f:|" >> "$hits"
+done < "$filelist"
+
+# ---- report -----------------------------------------------------------------
+if [ -s "$hits" ]; then
+  cat "$hits"
+  n=$(wc -l < "$hits" | tr -d ' ')
+  m=$(cut -d: -f1 "$hits" | sort -u | wc -l | tr -d ' ')
+  echo "honesty-guard: $n smell(s) in $m file(s)"
+  exit 1
+fi
+echo "honesty-guard: Clean."
+exit 0

verification/proofs/VERIFICATION-STANCE.adoc

@@ -76,6 +76,11 @@ and a fully-qualified `hasStringLit` (a bare lowercase occurrence in a
 *type* signature is silently auto-bound by Idris 2 as a fresh implicit,
 which had decoupled the predicate from its definition).
 
+That same proof-escape scan runs locally (advisory-only) via `sh
+scripts/honesty-guard.sh [PATH…]` (default `src/`); it strips Idris line/doc/block
+comments before matching, so tokens merely *named* in prose are not flagged, and
+it exits non-zero on any escape symbol found outside a comment.
+
 *New finding (Phase 1):* `src/interface/abi/Layout.idr` and
 `src/interface/abi/Foreign.idr` (`VclTotal.ABI.Layout/.Foreign`) do *not*
 compile under idris2 0.8.0 and contain *unsound* scaffolding (`paddingFor`