Skip to content

Commit 3d4e26d

Browse files
feat(check-trusted-base): add .trusted-base-ignore path-fragment exemptions (#223)
## Why Some escape-hatch markers genuinely should not require per-site documentation: - **Scanner test fixtures** (e.g. `test/soundness/fixtures/code_safety/*` in hypatia) exist *to be detected* by the scanner. They are deliberate inputs to the trusted-base discipline, not violations of it. - **Local agent-worktree shadows** (`.claude/worktrees/...`) duplicate the canonical tree while branches are checked out side-by-side; they re-trigger the scan on copies of files already counted in the main tree. - **Detector self-reference**: scanners that match banned-pattern strings to test for those patterns will trip themselves (cf. somethings-fishy#27 — the `unsafeCoerce` literal in the detector pattern table). Before this PR, the only options were inline `TRUSTED:` comments at every site or per-file enumeration in `docs/proof-debt.md`. Both are workarounds *at the call site*, not policy-level statements that "this whole directory is intentional self-scan noise." ## What Optional `.trusted-base-ignore` file in repo root, mirroring the existing `.hypatia-ignore` format: ``` # 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/ ``` When a marker's file path contains any ignore pattern, it is silently exempted. The script prints `[OK] N marker(s) exempted via .trusted-base-ignore.` for transparency. The early-exit "no proof-debt doc but markers exist" guard is relaxed to also accept a non-empty `.trusted-base-ignore` as sufficient disposition — enabling repos to be entirely exempt-driven if that fits their shape. ## Tests `scripts/tests/check-trusted-base-test.sh` — 8 cases, all green: - 3 regressions (no-docs early-exit / inline TRUSTED / proof-debt entry). - 5 new (path-fragment exemption / substring match / comments-only file / non-matching pattern / mixed exempt-plus-documented). Mirrors the existing `scripts/tests/check-ts-allowlist-test.sh` test pattern (tmpdir fixture + exit-code + substring assertion). ## Self-check on standards/ After the change, running `bash scripts/check-trusted-base.sh .` from the standards repo root still passes: ``` [INFO] Found 15 soundness-relevant escape hatch(es). [OK] proof-debt document(s) found: docs/proof-debt.md PROOF-NEEDS.md [OK] All 15 escape hatch(es) are documented (inline annotation, entry in: docs/proof-debt.md PROOF-NEEDS.md, or .trusted-base-ignore exemption). ``` ## Docs `docs/TRUSTED-BASE-REDUCTION-POLICY.adoc` updated with a new `=== .trusted-base-ignore — path-fragment exemption file` subsection under `== Enforcement`. Existing inline-annotation and proof-debt-enumeration guidance is unchanged. ## Auto-merge SQUASH (per estate policy). 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent 12d6fd6 commit 3d4e26d

3 files changed

Lines changed: 315 additions & 11 deletions

File tree

docs/TRUSTED-BASE-REDUCTION-POLICY.adoc

Lines changed: 36 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -207,14 +207,45 @@ as a `trusted-base` job. The script:
207207
`believe_me`, `really_believe_me`, `assert_total`, top-level `partial`,
208208
`assume val`, `admit_p`, `:axiom`, plus cross-language `TODO PROOF` /
209209
`OWED:` / `FIXME PROOF` markers in soundness-relevant positions).
210-
. Verifies each is either preceded within 5 lines by a `TRUSTED:`,
211-
`AXIOM:`, or `OWED:` leading comment, OR enumerated by path in
212-
`docs/proof-debt.md` (or `.adoc`).
213-
. Fails CI when a marker is naked (no annotation AND no proof-debt.md
214-
entry).
210+
. Verifies each is one of:
211+
.. preceded within 5 lines by a `TRUSTED:`, `AXIOM:`, or `OWED:` leading comment, OR
212+
.. enumerated by path in `docs/proof-debt.md` (or `.adoc`, or `PROOF-NEEDS.md`), OR
213+
.. exempted via a path-fragment substring match in `.trusted-base-ignore`.
214+
. Fails CI when a marker is naked (no annotation, no proof-debt entry, no
215+
ignore-file exemption).
215216
. No-ops cleanly on repos with zero proof-bearing files (true for most
216217
of the estate).
217218

219+
=== `.trusted-base-ignore` — path-fragment exemption file
220+
221+
For markers that should NOT need per-site documentation — typically
222+
test fixtures that exist *to be detected* by the scanner, local
223+
worktree shadows, or other intentional self-scan noise — the script
224+
consults an optional `.trusted-base-ignore` file in the repo root.
225+
Format mirrors `.hypatia-ignore`:
226+
227+
[source]
228+
----
229+
# Comments start with `#`.
230+
# Each non-comment line is a path-fragment substring match against the
231+
# repo-relative file path. Narrow the fragment to avoid hiding adjacent
232+
# findings.
233+
234+
# Scanner test fixtures: exist solely to verify the detector fires.
235+
test/soundness/fixtures/
236+
237+
# Local agent worktree shadows: not part of the canonical tree.
238+
.claude/worktrees/
239+
----
240+
241+
Prefer this over inline `TRUSTED:` comments only for *whole-path* or
242+
*whole-directory* exemptions with a documented org-policy rationale.
243+
Per-site `TRUSTED:` / `AXIOM:` comments remain the right tool for
244+
one-off documented escapes where the rationale is local to a single
245+
construct. `.trusted-base-ignore` is to `check-trusted-base.sh` what
246+
`.hypatia-ignore` is to the hypatia scanner — same shape, same
247+
discipline, separate scope.
248+
218249
A follow-up may extend it to fail CI when `docs/proof-debt.md` §(d) DEBT
219250
entries are past their stated deadline.
220251

scripts/check-trusted-base.sh

Lines changed: 60 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -180,20 +180,64 @@ for cand in docs/proof-debt.md docs/proof-debt.adoc PROOF-NEEDS.md docs/PROOF-NE
180180
fi
181181
done
182182

183-
if [ ${#debt_docs[@]} -eq 0 ]; then
183+
# ─────────────────────────────────────────────────────────────────────────────
184+
# Load `.trusted-base-ignore` if present (format mirrors `.hypatia-ignore`):
185+
# - lines starting with `#` are comments;
186+
# - each non-comment, non-blank line is a path-fragment substring that
187+
# exempts every marker whose file path contains the fragment.
188+
# Use for: test fixtures that exist to be detected by the scanner, local
189+
# worktree shadows (`.claude/worktrees/`), and other intentional self-scan
190+
# noise. Per-site `TRUSTED:`/`AXIOM:` comments remain the preferred
191+
# mechanism for one-off documented escapes; this file is for whole-path
192+
# exemptions that carry a stated rationale.
193+
# ─────────────────────────────────────────────────────────────────────────────
194+
trusted_base_ignores=()
195+
if [ -f .trusted-base-ignore ]; then
196+
while IFS= read -r line || [ -n "$line" ]; do
197+
# Strip trailing whitespace/CR for cross-platform safety.
198+
line="${line%$'\r'}"
199+
line="${line%"${line##*[![:space:]]}"}"
200+
case "$line" in
201+
''|'#'*) ;;
202+
*) trusted_base_ignores+=("$line") ;;
203+
esac
204+
done < .trusted-base-ignore
205+
if [ ${#trusted_base_ignores[@]} -gt 0 ]; then
206+
echo "[INFO] Loaded ${#trusted_base_ignores[@]} pattern(s) from .trusted-base-ignore."
207+
fi
208+
fi
209+
210+
if [ ${#debt_docs[@]} -eq 0 ] && [ ${#trusted_base_ignores[@]} -eq 0 ]; then
184211
echo "[ERROR] No docs/proof-debt.md (or equivalent) found, but $marker_count escape hatches exist."
185212
echo "[ERROR] Seed one per the schema at hyperpolymath/standards/docs/TRUSTED-BASE-REDUCTION-POLICY.adoc."
186213
exit 1
187214
fi
188215

189-
echo "[OK] proof-debt document(s) found: ${debt_docs[*]}"
216+
if [ ${#debt_docs[@]} -gt 0 ]; then
217+
echo "[OK] proof-debt document(s) found: ${debt_docs[*]}"
218+
fi
190219

191220
# For each marker, check documentation
192221
undocumented=0
222+
exempted=0
193223
while IFS=$'\t' read -r f ln kind ctx; do
194224
# Strip leading ./
195225
f_clean="${f#./}"
196226

227+
# 0. .trusted-base-ignore — substring match on the file path. Use for
228+
# test fixtures, worktree shadows, and other intentional self-scan
229+
# noise that should NOT need per-site documentation.
230+
is_exempted=false
231+
for pattern in "${trusted_base_ignores[@]}"; do
232+
case "$f_clean" in
233+
*"$pattern"*) is_exempted=true; break ;;
234+
esac
235+
done
236+
if $is_exempted; then
237+
exempted=$((exempted + 1))
238+
continue
239+
fi
240+
197241
# 1. Inline TRUSTED:/AXIOM: comment on any of the 5 lines preceding the marker
198242
local_start=$(( ln - 5 ))
199243
[ "$local_start" -lt 1 ] && local_start=1
@@ -222,18 +266,28 @@ while IFS=$'\t' read -r f ln kind ctx; do
222266
# Undocumented.
223267
echo "[ERROR] Undocumented escape hatch at $f_clean:$ln ($kind):"
224268
echo " $ctx"
225-
echo " Annotate with a 'TRUSTED:' or 'AXIOM:' leading comment, or"
226-
echo " enumerate in any of: ${debt_docs[*]}"
269+
echo " Annotate with a 'TRUSTED:' or 'AXIOM:' leading comment,"
270+
echo " enumerate in any of: ${debt_docs[*]:-<none>}, or"
271+
echo " add a path-fragment to .trusted-base-ignore if this is"
272+
echo " intentional self-scan noise (e.g. test fixture, worktree shadow)."
227273
undocumented=$((undocumented + 1))
228274
done < "$markers_tsv"
229275

276+
if [ "$exempted" -gt 0 ]; then
277+
echo "[OK] $exempted marker(s) exempted via .trusted-base-ignore."
278+
fi
279+
230280
if [ "$undocumented" -gt 0 ]; then
231281
echo ""
232282
echo "[ERROR] $undocumented/$marker_count escape hatch(es) are undocumented."
233-
echo "[ERROR] Each must be annotated inline OR enumerated in one of: ${debt_docs[*]}"
283+
echo "[ERROR] Each must be annotated inline, enumerated in one of: ${debt_docs[*]:-<none>}, or exempted via .trusted-base-ignore."
234284
echo "[ERROR] See https://github.com/hyperpolymath/standards/blob/main/docs/TRUSTED-BASE-REDUCTION-POLICY.adoc"
235285
exit 1
236286
fi
237287

238-
echo "[OK] All $marker_count escape hatch(es) are documented (inline annotation or entry in: ${debt_docs[*]})."
288+
if [ "$exempted" -eq "$marker_count" ]; then
289+
echo "[OK] All $marker_count escape hatch(es) handled (entirely via .trusted-base-ignore exemption)."
290+
else
291+
echo "[OK] All $marker_count escape hatch(es) are documented (inline annotation, entry in: ${debt_docs[*]:-<none>}, or .trusted-base-ignore exemption)."
292+
fi
239293
exit 0
Lines changed: 219 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,219 @@
1+
#!/usr/bin/env bash
2+
# SPDX-License-Identifier: PMPL-1.0-or-later
3+
# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
4+
#
5+
# Regression test for scripts/check-trusted-base.sh — exercises the
6+
# `.trusted-base-ignore` path-fragment exemption mechanism plus the
7+
# existing inline-annotation and proof-debt enumeration paths.
8+
9+
set -uo pipefail
10+
11+
SCRIPT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
12+
SCRIPT="$SCRIPT_DIR/../check-trusted-base.sh"
13+
14+
if [[ ! -x "$SCRIPT" ]]; then
15+
echo "FATAL: cannot locate $SCRIPT" >&2
16+
exit 2
17+
fi
18+
19+
PASS=0
20+
FAIL=0
21+
22+
run_case() {
23+
local name="$1"; shift
24+
local expected_exit="$1"; shift
25+
local expected_substr="$1"; shift
26+
local setup_fn="$1"; shift
27+
28+
local tmp
29+
tmp="$(mktemp -d)"
30+
(
31+
cd "$tmp"
32+
"$setup_fn"
33+
)
34+
set +e
35+
local out
36+
out="$(cd "$tmp" && bash "$SCRIPT" . 2>&1)"
37+
local actual_exit=$?
38+
set -e
39+
40+
local ok=true
41+
if [[ "$actual_exit" -ne "$expected_exit" ]]; then ok=false; fi
42+
if [[ -n "$expected_substr" && "$out" != *"$expected_substr"* ]]; then ok=false; fi
43+
44+
if $ok; then
45+
echo "ok $name"
46+
PASS=$((PASS+1))
47+
else
48+
echo "FAIL $name (exit=$actual_exit, expected=$expected_exit)"
49+
echo "---- output ----"
50+
echo "$out"
51+
echo "----------------"
52+
FAIL=$((FAIL+1))
53+
fi
54+
rm -rf "$tmp"
55+
}
56+
57+
# Each setup creates a fresh fixture tree at $PWD (the tmpdir).
58+
59+
setup_marker_no_docs() {
60+
mkdir -p src
61+
cat > src/Foo.idr <<'EOF'
62+
module Foo
63+
%default total
64+
partial
65+
foo : Int -> Int
66+
foo x = x
67+
EOF
68+
}
69+
70+
setup_marker_with_inline_trusted() {
71+
mkdir -p src docs
72+
cat > src/Foo.idr <<'EOF'
73+
module Foo
74+
%default total
75+
-- TRUSTED: documented exception per local policy.
76+
partial
77+
foo : Int -> Int
78+
foo x = x
79+
EOF
80+
# Inline annotations still require a proof-debt index per the original
81+
# script's contract; the empty doc satisfies that.
82+
cat > docs/proof-debt.md <<'EOF'
83+
# Proof Debt
84+
(Inline annotations only.)
85+
EOF
86+
}
87+
88+
setup_marker_with_proof_debt() {
89+
mkdir -p src docs
90+
cat > src/Foo.idr <<'EOF'
91+
module Foo
92+
%default total
93+
partial
94+
foo : Int -> Int
95+
foo x = x
96+
EOF
97+
cat > docs/proof-debt.md <<'EOF'
98+
# Proof Debt
99+
See src/Foo.idr:3 — documented partial marker.
100+
EOF
101+
}
102+
103+
setup_marker_with_ignore_exact() {
104+
mkdir -p test/fixtures
105+
cat > test/fixtures/admitted.v <<'EOF'
106+
Theorem foo : True.
107+
Admitted.
108+
EOF
109+
cat > .trusted-base-ignore <<'EOF'
110+
# Test fixtures: deliberately contain the patterns under test.
111+
test/fixtures/
112+
EOF
113+
}
114+
115+
setup_marker_with_ignore_substring() {
116+
mkdir -p test/soundness/fixtures/code_safety
117+
cat > test/soundness/fixtures/code_safety/admitted.v <<'EOF'
118+
Theorem foo : True.
119+
Admitted.
120+
EOF
121+
cat > .trusted-base-ignore <<'EOF'
122+
# Scanner fixtures - intentional.
123+
fixtures/code_safety
124+
EOF
125+
}
126+
127+
setup_ignore_comments_only_still_fails() {
128+
mkdir -p src docs
129+
cat > src/Foo.idr <<'EOF'
130+
module Foo
131+
%default total
132+
partial
133+
foo : Int -> Int
134+
foo x = x
135+
EOF
136+
cat > docs/proof-debt.md <<'EOF'
137+
# Proof Debt
138+
(Empty.)
139+
EOF
140+
cat > .trusted-base-ignore <<'EOF'
141+
# only comments here
142+
# nothing real
143+
EOF
144+
}
145+
146+
setup_ignore_does_not_match() {
147+
mkdir -p src docs
148+
cat > src/Foo.idr <<'EOF'
149+
module Foo
150+
%default total
151+
partial
152+
foo : Int -> Int
153+
foo x = x
154+
EOF
155+
cat > docs/proof-debt.md <<'EOF'
156+
# Proof Debt
157+
(Empty.)
158+
EOF
159+
cat > .trusted-base-ignore <<'EOF'
160+
# Pattern that does not match.
161+
test/fixtures/
162+
EOF
163+
}
164+
165+
setup_mixed_exempt_and_documented() {
166+
mkdir -p src test/fixtures docs
167+
cat > src/Foo.idr <<'EOF'
168+
module Foo
169+
%default total
170+
partial
171+
foo : Int -> Int
172+
foo x = x
173+
EOF
174+
cat > test/fixtures/bar.v <<'EOF'
175+
Theorem bar : True.
176+
Admitted.
177+
EOF
178+
cat > docs/proof-debt.md <<'EOF'
179+
# Proof Debt
180+
src/Foo.idr:3 — documented.
181+
EOF
182+
cat > .trusted-base-ignore <<'EOF'
183+
# Exempt fixtures.
184+
test/fixtures/
185+
EOF
186+
}
187+
188+
# Existing behaviour must still work.
189+
run_case "marker with no docs and no ignore fails (early exit)" \
190+
1 "No docs/proof-debt.md (or equivalent) found" setup_marker_no_docs
191+
192+
run_case "inline TRUSTED comment passes (regression)" \
193+
0 "All 1 escape hatch(es) are documented" setup_marker_with_inline_trusted
194+
195+
run_case "entry in proof-debt.md passes (regression)" \
196+
0 "All 1 escape hatch(es) are documented" setup_marker_with_proof_debt
197+
198+
# New .trusted-base-ignore behaviour.
199+
run_case "single path-fragment exempts marker (no proof-debt doc)" \
200+
0 "1 marker(s) exempted via .trusted-base-ignore" setup_marker_with_ignore_exact
201+
202+
run_case "substring-match exemption picks up deeper paths" \
203+
0 "1 marker(s) exempted via .trusted-base-ignore" setup_marker_with_ignore_substring
204+
205+
run_case "ignore file with only comments behaves as no exemptions" \
206+
1 "1/1 escape hatch(es) are undocumented" setup_ignore_comments_only_still_fails
207+
208+
run_case "ignore pattern that does not match still fails" \
209+
1 "1/1 escape hatch(es) are undocumented" setup_ignore_does_not_match
210+
211+
run_case "mixed: one marker exempted, one documented in proof-debt" \
212+
0 "1 marker(s) exempted via .trusted-base-ignore" setup_mixed_exempt_and_documented
213+
214+
echo
215+
echo "PASS=$PASS FAIL=$FAIL"
216+
if [[ "$FAIL" -gt 0 ]]; then
217+
exit 1
218+
fi
219+
exit 0

0 commit comments

Comments
 (0)