trusted-base: walk back through comment blocks for TRUSTED:/AXIOM: magic (closes #296) (#300)

## Summary

Replaces the fixed 5-line preceding-comment window in
`scripts/check-trusted-base.sh` with a walk-back through the consecutive
comment block (lines that start with `--` / `//` / `|||` / `#` / `*` /
`(*`). Adds a 15-line hard floor as a sanity bound.

## Why

Real Agda / Lean / Idris postulates commonly carry 7-15 line prose
justifications labelled `-- AXIOM:` / `-- TRUSTED:` on the *opening*
line of the block. The marker (the `postulate` keyword) lands at the
*end* of the block — past the 5-line window — and the script reported
the escape hatch as undocumented even though the documentation was
plainly there.

Echidna PR #128 had to insert a redundant `-- AXIOM:` line immediately
before each postulate as a workaround. This PR fixes the underlying
script behaviour so the natural prose-block placement is recognised
estate-wide.

## Behaviour matrix

| Block shape | Old (5-line window) | New (walk-back, 15-line floor) |
|---|---|---|
| Magic word on line N-2, marker on line N | ✅ | ✅ |
| Magic word on line N-10, with 10 lines of prose comment, marker on
line N | ❌ | ✅ |
| Magic word on line N-20, marker on line N (with intervening blank or
code line) | ❌ | ❌ (block-aware) |
| No magic word in the preceding block | ❌ | ❌ (correctly fails closed)
|

## Test plan

- [x] Local synthetic test (Agda postulate with 7-line prose block +
opening AXIOM: line) now passes the script.
- [ ] CI on standards' own .v / .agda / .idr / .rs files.

Closes #296.
EOF
)

Author: hyperpolymath

scripts/check-trusted-base.sh

@@ -238,10 +238,41 @@ while IFS=$'\t' read -r f ln kind ctx; do
     continue
   fi
 
-  # 1. Inline TRUSTED:/AXIOM: comment on any of the 5 lines preceding the marker
-  local_start=$(( ln - 5 ))
-  [ "$local_start" -lt 1 ] && local_start=1
-  if sed -n "${local_start},${ln}p" "$f" 2>/dev/null | grep -qE 'TRUSTED:|AXIOM:'; then
+  # 1. Inline TRUSTED:/AXIOM: comment in the preceding comment block. We walk
+  #    backwards from the marker through consecutive comment lines (-- / // /
+  #    ||| / # / * / (*) until we hit a non-comment line, then check the
+  #    whole block for the magic word. A 5-line ceiling (the historical
+  #    window) was too narrow for real Agda postulates with a 7-15 line
+  #    prose justification labelled `-- AXIOM:` on its opening line. See
+  #    standards#296.
+  walk_start="$ln"
+  while [ "$walk_start" -gt 1 ]; do
+    prev_ln=$(( walk_start - 1 ))
+    prev_line="$(sed -n "${prev_ln}p" "$f" 2>/dev/null)"
+    case "$prev_line" in
+      *[!\ \	]*) ;;  # non-blank — fall through to comment test
+      *)
+        # blank line breaks the comment block.
+        break
+        ;;
+    esac
+    trimmed="$(echo "$prev_line" | sed -E 's/^[[:space:]]+//')"
+    case "$trimmed" in
+      --*|"|||"*|"|||"|"//"*|"/*"*|"*"*|"(*"*|"#"*)
+        walk_start="$prev_ln"
+        ;;
+      *)
+        break
+        ;;
+    esac
+  done
+  # Also bound by ln-15 as a sanity check — a 15-line "comment block"
+  # without a magic word is almost certainly something other than a
+  # documented escape hatch.
+  hard_floor=$(( ln - 15 ))
+  [ "$hard_floor" -gt "$walk_start" ] && walk_start="$hard_floor"
+  [ "$walk_start" -lt 1 ] && walk_start=1
+  if sed -n "${walk_start},${ln}p" "$f" 2>/dev/null | grep -qE 'TRUSTED:|AXIOM:'; then
     continue
   fi