From 470c2be637ff6e91e547601a14a00ea56a0d04ed Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 27 May 2026 09:55:18 +0100 Subject: [PATCH] feat(check-trusted-base): add .trusted-base-ignore exemptions [See PR body for details.] Co-Authored-By: Claude Opus 4.7 (1M context) --- docs/TRUSTED-BASE-REDUCTION-POLICY.adoc | 41 ++++- scripts/check-trusted-base.sh | 66 ++++++- scripts/tests/check-trusted-base-test.sh | 219 +++++++++++++++++++++++ 3 files changed, 315 insertions(+), 11 deletions(-) create mode 100755 scripts/tests/check-trusted-base-test.sh diff --git a/docs/TRUSTED-BASE-REDUCTION-POLICY.adoc b/docs/TRUSTED-BASE-REDUCTION-POLICY.adoc index cabef27c..f9f57800 100644 --- a/docs/TRUSTED-BASE-REDUCTION-POLICY.adoc +++ b/docs/TRUSTED-BASE-REDUCTION-POLICY.adoc @@ -207,14 +207,45 @@ as a `trusted-base` job. The script: `believe_me`, `really_believe_me`, `assert_total`, top-level `partial`, `assume val`, `admit_p`, `:axiom`, plus cross-language `TODO PROOF` / `OWED:` / `FIXME PROOF` markers in soundness-relevant positions). -. Verifies each is either preceded within 5 lines by a `TRUSTED:`, - `AXIOM:`, or `OWED:` leading comment, OR enumerated by path in - `docs/proof-debt.md` (or `.adoc`). -. Fails CI when a marker is naked (no annotation AND no proof-debt.md - entry). +. Verifies each is one of: +.. preceded within 5 lines by a `TRUSTED:`, `AXIOM:`, or `OWED:` leading comment, OR +.. enumerated by path in `docs/proof-debt.md` (or `.adoc`, or `PROOF-NEEDS.md`), OR +.. exempted via a path-fragment substring match in `.trusted-base-ignore`. +. Fails CI when a marker is naked (no annotation, no proof-debt entry, no + ignore-file exemption). . No-ops cleanly on repos with zero proof-bearing files (true for most of the estate). +=== `.trusted-base-ignore` — path-fragment exemption file + +For markers that should NOT need per-site documentation — typically +test fixtures that exist *to be detected* by the scanner, local +worktree shadows, or other intentional self-scan noise — the script +consults an optional `.trusted-base-ignore` file in the repo root. +Format mirrors `.hypatia-ignore`: + +[source] +---- +# Comments start with `#`. +# Each non-comment line is a path-fragment substring match against the +# repo-relative file path. Narrow the fragment to avoid hiding adjacent +# findings. + +# Scanner test fixtures: exist solely to verify the detector fires. +test/soundness/fixtures/ + +# Local agent worktree shadows: not part of the canonical tree. +.claude/worktrees/ +---- + +Prefer this over inline `TRUSTED:` comments only for *whole-path* or +*whole-directory* exemptions with a documented org-policy rationale. +Per-site `TRUSTED:` / `AXIOM:` comments remain the right tool for +one-off documented escapes where the rationale is local to a single +construct. `.trusted-base-ignore` is to `check-trusted-base.sh` what +`.hypatia-ignore` is to the hypatia scanner — same shape, same +discipline, separate scope. + A follow-up may extend it to fail CI when `docs/proof-debt.md` §(d) DEBT entries are past their stated deadline. diff --git a/scripts/check-trusted-base.sh b/scripts/check-trusted-base.sh index 82014e73..8ce18e19 100755 --- a/scripts/check-trusted-base.sh +++ b/scripts/check-trusted-base.sh @@ -180,20 +180,64 @@ for cand in docs/proof-debt.md docs/proof-debt.adoc PROOF-NEEDS.md docs/PROOF-NE fi done -if [ ${#debt_docs[@]} -eq 0 ]; then +# ───────────────────────────────────────────────────────────────────────────── +# Load `.trusted-base-ignore` if present (format mirrors `.hypatia-ignore`): +# - lines starting with `#` are comments; +# - each non-comment, non-blank line is a path-fragment substring that +# exempts every marker whose file path contains the fragment. +# Use for: test fixtures that exist to be detected by the scanner, local +# worktree shadows (`.claude/worktrees/`), and other intentional self-scan +# noise. Per-site `TRUSTED:`/`AXIOM:` comments remain the preferred +# mechanism for one-off documented escapes; this file is for whole-path +# exemptions that carry a stated rationale. +# ───────────────────────────────────────────────────────────────────────────── +trusted_base_ignores=() +if [ -f .trusted-base-ignore ]; then + while IFS= read -r line || [ -n "$line" ]; do + # Strip trailing whitespace/CR for cross-platform safety. + line="${line%$'\r'}" + line="${line%"${line##*[![:space:]]}"}" + case "$line" in + ''|'#'*) ;; + *) trusted_base_ignores+=("$line") ;; + esac + done < .trusted-base-ignore + if [ ${#trusted_base_ignores[@]} -gt 0 ]; then + echo "[INFO] Loaded ${#trusted_base_ignores[@]} pattern(s) from .trusted-base-ignore." + fi +fi + +if [ ${#debt_docs[@]} -eq 0 ] && [ ${#trusted_base_ignores[@]} -eq 0 ]; then echo "[ERROR] No docs/proof-debt.md (or equivalent) found, but $marker_count escape hatches exist." echo "[ERROR] Seed one per the schema at hyperpolymath/standards/docs/TRUSTED-BASE-REDUCTION-POLICY.adoc." exit 1 fi -echo "[OK] proof-debt document(s) found: ${debt_docs[*]}" +if [ ${#debt_docs[@]} -gt 0 ]; then + echo "[OK] proof-debt document(s) found: ${debt_docs[*]}" +fi # For each marker, check documentation undocumented=0 +exempted=0 while IFS=$'\t' read -r f ln kind ctx; do # Strip leading ./ f_clean="${f#./}" + # 0. .trusted-base-ignore — substring match on the file path. Use for + # test fixtures, worktree shadows, and other intentional self-scan + # noise that should NOT need per-site documentation. + is_exempted=false + for pattern in "${trusted_base_ignores[@]}"; do + case "$f_clean" in + *"$pattern"*) is_exempted=true; break ;; + esac + done + if $is_exempted; then + exempted=$((exempted + 1)) + 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 @@ -222,18 +266,28 @@ while IFS=$'\t' read -r f ln kind ctx; do # Undocumented. echo "[ERROR] Undocumented escape hatch at $f_clean:$ln ($kind):" echo " $ctx" - echo " Annotate with a 'TRUSTED:' or 'AXIOM:' leading comment, or" - echo " enumerate in any of: ${debt_docs[*]}" + echo " Annotate with a 'TRUSTED:' or 'AXIOM:' leading comment," + echo " enumerate in any of: ${debt_docs[*]:-}, or" + echo " add a path-fragment to .trusted-base-ignore if this is" + echo " intentional self-scan noise (e.g. test fixture, worktree shadow)." undocumented=$((undocumented + 1)) done < "$markers_tsv" +if [ "$exempted" -gt 0 ]; then + echo "[OK] $exempted marker(s) exempted via .trusted-base-ignore." +fi + if [ "$undocumented" -gt 0 ]; then echo "" echo "[ERROR] $undocumented/$marker_count escape hatch(es) are undocumented." - echo "[ERROR] Each must be annotated inline OR enumerated in one of: ${debt_docs[*]}" + echo "[ERROR] Each must be annotated inline, enumerated in one of: ${debt_docs[*]:-}, or exempted via .trusted-base-ignore." echo "[ERROR] See https://github.com/hyperpolymath/standards/blob/main/docs/TRUSTED-BASE-REDUCTION-POLICY.adoc" exit 1 fi -echo "[OK] All $marker_count escape hatch(es) are documented (inline annotation or entry in: ${debt_docs[*]})." +if [ "$exempted" -eq "$marker_count" ]; then + echo "[OK] All $marker_count escape hatch(es) handled (entirely via .trusted-base-ignore exemption)." +else + echo "[OK] All $marker_count escape hatch(es) are documented (inline annotation, entry in: ${debt_docs[*]:-}, or .trusted-base-ignore exemption)." +fi exit 0 diff --git a/scripts/tests/check-trusted-base-test.sh b/scripts/tests/check-trusted-base-test.sh new file mode 100755 index 00000000..f7a446f2 --- /dev/null +++ b/scripts/tests/check-trusted-base-test.sh @@ -0,0 +1,219 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: PMPL-1.0-or-later +# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +# +# Regression test for scripts/check-trusted-base.sh — exercises the +# `.trusted-base-ignore` path-fragment exemption mechanism plus the +# existing inline-annotation and proof-debt enumeration paths. + +set -uo pipefail + +SCRIPT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)" +SCRIPT="$SCRIPT_DIR/../check-trusted-base.sh" + +if [[ ! -x "$SCRIPT" ]]; then + echo "FATAL: cannot locate $SCRIPT" >&2 + exit 2 +fi + +PASS=0 +FAIL=0 + +run_case() { + local name="$1"; shift + local expected_exit="$1"; shift + local expected_substr="$1"; shift + local setup_fn="$1"; shift + + local tmp + tmp="$(mktemp -d)" + ( + cd "$tmp" + "$setup_fn" + ) + set +e + local out + out="$(cd "$tmp" && bash "$SCRIPT" . 2>&1)" + local actual_exit=$? + set -e + + local ok=true + if [[ "$actual_exit" -ne "$expected_exit" ]]; then ok=false; fi + if [[ -n "$expected_substr" && "$out" != *"$expected_substr"* ]]; then ok=false; fi + + if $ok; then + echo "ok $name" + PASS=$((PASS+1)) + else + echo "FAIL $name (exit=$actual_exit, expected=$expected_exit)" + echo "---- output ----" + echo "$out" + echo "----------------" + FAIL=$((FAIL+1)) + fi + rm -rf "$tmp" +} + +# Each setup creates a fresh fixture tree at $PWD (the tmpdir). + +setup_marker_no_docs() { + mkdir -p src + cat > src/Foo.idr <<'EOF' +module Foo +%default total +partial +foo : Int -> Int +foo x = x +EOF +} + +setup_marker_with_inline_trusted() { + mkdir -p src docs + cat > src/Foo.idr <<'EOF' +module Foo +%default total +-- TRUSTED: documented exception per local policy. +partial +foo : Int -> Int +foo x = x +EOF + # Inline annotations still require a proof-debt index per the original + # script's contract; the empty doc satisfies that. + cat > docs/proof-debt.md <<'EOF' +# Proof Debt +(Inline annotations only.) +EOF +} + +setup_marker_with_proof_debt() { + mkdir -p src docs + cat > src/Foo.idr <<'EOF' +module Foo +%default total +partial +foo : Int -> Int +foo x = x +EOF + cat > docs/proof-debt.md <<'EOF' +# Proof Debt +See src/Foo.idr:3 — documented partial marker. +EOF +} + +setup_marker_with_ignore_exact() { + mkdir -p test/fixtures + cat > test/fixtures/admitted.v <<'EOF' +Theorem foo : True. +Admitted. +EOF + cat > .trusted-base-ignore <<'EOF' +# Test fixtures: deliberately contain the patterns under test. +test/fixtures/ +EOF +} + +setup_marker_with_ignore_substring() { + mkdir -p test/soundness/fixtures/code_safety + cat > test/soundness/fixtures/code_safety/admitted.v <<'EOF' +Theorem foo : True. +Admitted. +EOF + cat > .trusted-base-ignore <<'EOF' +# Scanner fixtures - intentional. +fixtures/code_safety +EOF +} + +setup_ignore_comments_only_still_fails() { + mkdir -p src docs + cat > src/Foo.idr <<'EOF' +module Foo +%default total +partial +foo : Int -> Int +foo x = x +EOF + cat > docs/proof-debt.md <<'EOF' +# Proof Debt +(Empty.) +EOF + cat > .trusted-base-ignore <<'EOF' +# only comments here +# nothing real +EOF +} + +setup_ignore_does_not_match() { + mkdir -p src docs + cat > src/Foo.idr <<'EOF' +module Foo +%default total +partial +foo : Int -> Int +foo x = x +EOF + cat > docs/proof-debt.md <<'EOF' +# Proof Debt +(Empty.) +EOF + cat > .trusted-base-ignore <<'EOF' +# Pattern that does not match. +test/fixtures/ +EOF +} + +setup_mixed_exempt_and_documented() { + mkdir -p src test/fixtures docs + cat > src/Foo.idr <<'EOF' +module Foo +%default total +partial +foo : Int -> Int +foo x = x +EOF + cat > test/fixtures/bar.v <<'EOF' +Theorem bar : True. +Admitted. +EOF + cat > docs/proof-debt.md <<'EOF' +# Proof Debt +src/Foo.idr:3 — documented. +EOF + cat > .trusted-base-ignore <<'EOF' +# Exempt fixtures. +test/fixtures/ +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 + +run_case "inline TRUSTED comment passes (regression)" \ + 0 "All 1 escape hatch(es) are documented" setup_marker_with_inline_trusted + +run_case "entry in proof-debt.md passes (regression)" \ + 0 "All 1 escape hatch(es) are documented" setup_marker_with_proof_debt + +# New .trusted-base-ignore behaviour. +run_case "single path-fragment exempts marker (no proof-debt doc)" \ + 0 "1 marker(s) exempted via .trusted-base-ignore" setup_marker_with_ignore_exact + +run_case "substring-match exemption picks up deeper paths" \ + 0 "1 marker(s) exempted via .trusted-base-ignore" setup_marker_with_ignore_substring + +run_case "ignore file with only comments behaves as no exemptions" \ + 1 "1/1 escape hatch(es) are undocumented" setup_ignore_comments_only_still_fails + +run_case "ignore pattern that does not match still fails" \ + 1 "1/1 escape hatch(es) are undocumented" setup_ignore_does_not_match + +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 + +echo +echo "PASS=$PASS FAIL=$FAIL" +if [[ "$FAIL" -gt 0 ]]; then + exit 1 +fi +exit 0