|
| 1 | +#!/usr/bin/env bash |
| 2 | +# SPDX-License-Identifier: MPL-2.0 |
| 3 | +# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) |
| 4 | +# |
| 5 | +# check-trusted-base.sh |
| 6 | +# |
| 7 | +# Implements the enforcement leg of the estate Trusted-Base Reduction Policy |
| 8 | +# (docs/TRUSTED-BASE-REDUCTION-POLICY.adoc — standards#203). |
| 9 | +# |
| 10 | +# For every soundness-relevant escape hatch in a proof-bearing repo, verifies |
| 11 | +# the hatch is one of: |
| 12 | +# (a) discharged — entry in `docs/proof-debt.md` §(a) |
| 13 | +# (b) budgeted — entry in §(b) AND preceded by a `TRUSTED:` leading comment |
| 14 | +# (c) necessary — entry in §(c) AND preceded by an `AXIOM:` leading comment |
| 15 | +# (d) debt — entry in §(d) with deadline + owner (still counts as |
| 16 | +# documented; CI passes but the entry is enumerated in the |
| 17 | +# CI summary) |
| 18 | +# |
| 19 | +# Markers searched: |
| 20 | +# Coq *.v — `^Axiom`, `^Admitted`, `admit\.` |
| 21 | +# Lean *.lean — `\bsorry\b`, `^axiom\b` |
| 22 | +# Agda *.agda — `^postulate`, `^\s*postulate` |
| 23 | +# Idris2 *.idr* — `believe_me`, `really_believe_me`, `assert_total`, |
| 24 | +# top-level `^partial$`, `^%default partial` |
| 25 | +# F\* *.fst — `assume val`, `admit_p` |
| 26 | +# Rust/Hs *.rs|*.hs — `unsafePerformIO`, `unsafeCoerce` (soundness-relevant) |
| 27 | +# |
| 28 | +# Exit codes: |
| 29 | +# 0 — repo has no proof-bearing files, OR every marker is documented. |
| 30 | +# 1 — at least one marker is undocumented (neither annotated inline nor |
| 31 | +# enumerated in docs/proof-debt.md). |
| 32 | +# 2 — invocation/environment error. |
| 33 | +# |
| 34 | +# Wired into governance-reusable.yml as the `trusted-base` job. |
| 35 | + |
| 36 | +set -u |
| 37 | + |
| 38 | +repo_root="${1:-.}" |
| 39 | +cd "$repo_root" || { echo "ERROR: cannot cd to $repo_root" >&2; exit 2; } |
| 40 | + |
| 41 | +# ───────────────────────────────────────────────────────────────────────────── |
| 42 | +# Find all proof-bearing files (excluding vendored / build artefacts). |
| 43 | +# ───────────────────────────────────────────────────────────────────────────── |
| 44 | +PRUNE_PATHS=(-path '*/.git' -prune -o |
| 45 | + -path '*/.lake' -prune -o |
| 46 | + -path '*/_build' -prune -o |
| 47 | + -path '*/build' -prune -o |
| 48 | + -path '*/target' -prune -o |
| 49 | + -path '*/node_modules' -prune -o |
| 50 | + -path '*/dist' -prune -o |
| 51 | + -path '*/.venv' -prune -o |
| 52 | + -path '*/vendored' -prune -o) |
| 53 | + |
| 54 | +proof_files=$(find . "${PRUNE_PATHS[@]}" -type f \( \ |
| 55 | + -name '*.v' -o -name '*.lean' -o -name '*.agda' -o \ |
| 56 | + -name '*.idr' -o -name '*.idr2' -o -name '*.fst' -o \ |
| 57 | + -name '*.dfy' -o -name '*.tla' -o -name '*.ads' -o -name '*.adb' \) -print) |
| 58 | + |
| 59 | +unsafe_files=$(find . "${PRUNE_PATHS[@]}" -type f \( \ |
| 60 | + -name '*.rs' -o -name '*.hs' \) -print) |
| 61 | + |
| 62 | +if [ -z "$proof_files" ]; then |
| 63 | + echo "[OK] No proof-bearing files in this repo; check-trusted-base.sh is a no-op." |
| 64 | + exit 0 |
| 65 | +fi |
| 66 | + |
| 67 | +# ───────────────────────────────────────────────────────────────────────────── |
| 68 | +# Gather every marker — one row per (file, line, kind, identifier). |
| 69 | +# ───────────────────────────────────────────────────────────────────────────── |
| 70 | +markers_tsv=$(mktemp) |
| 71 | +trap 'rm -f "$markers_tsv"' EXIT |
| 72 | + |
| 73 | +is_comment_line() { |
| 74 | + # Heuristic: line whose first non-whitespace chars are a comment marker. |
| 75 | + # Returns 0 (true) when the line is a comment. |
| 76 | + local trimmed |
| 77 | + trimmed="$(echo "$1" | sed -E 's/^[[:space:]]+//')" |
| 78 | + case "$trimmed" in |
| 79 | + --*|"||| "*|"|||"*|//*|/\**|"* "*|"(*"*|"#"*) return 0 ;; |
| 80 | + esac |
| 81 | + return 1 |
| 82 | +} |
| 83 | + |
| 84 | +emit_marker() { |
| 85 | + # 1=file, 2=line, 3=kind, 4=identifier-or-context |
| 86 | + # Skip if the line itself is a comment line (false positives — talking *about* |
| 87 | + # the construct rather than using it). |
| 88 | + if is_comment_line "$4"; then |
| 89 | + return 0 |
| 90 | + fi |
| 91 | + printf '%s\t%s\t%s\t%s\n' "$1" "$2" "$3" "$4" >> "$markers_tsv" |
| 92 | +} |
| 93 | + |
| 94 | +# Coq Axiom / Admitted |
| 95 | +echo "$proof_files" | grep -E '\.v$' | while read -r f; do |
| 96 | + [ -z "$f" ] && continue |
| 97 | + grep -nE '^[[:space:]]*(Axiom|Admitted|admit\.)' "$f" 2>/dev/null | while IFS=: read -r ln rest; do |
| 98 | + emit_marker "$f" "$ln" "coq-axiom-or-admit" "$(echo "$rest" | head -c 80)" |
| 99 | + done |
| 100 | +done |
| 101 | + |
| 102 | +# Lean sorry / axiom |
| 103 | +echo "$proof_files" | grep -E '\.lean$' | while read -r f; do |
| 104 | + [ -z "$f" ] && continue |
| 105 | + grep -nE '\bsorry\b|^[[:space:]]*axiom[[:space:]]' "$f" 2>/dev/null | while IFS=: read -r ln rest; do |
| 106 | + emit_marker "$f" "$ln" "lean-sorry-or-axiom" "$(echo "$rest" | head -c 80)" |
| 107 | + done |
| 108 | +done |
| 109 | + |
| 110 | +# Agda postulate (top-level only) |
| 111 | +echo "$proof_files" | grep -E '\.agda$' | while read -r f; do |
| 112 | + [ -z "$f" ] && continue |
| 113 | + grep -nE '^[[:space:]]*postulate' "$f" 2>/dev/null | while IFS=: read -r ln rest; do |
| 114 | + emit_marker "$f" "$ln" "agda-postulate" "$(echo "$rest" | head -c 80)" |
| 115 | + done |
| 116 | +done |
| 117 | + |
| 118 | +# Idris2 believe_me / assert_total / really_believe_me |
| 119 | +echo "$proof_files" | grep -E '\.(idr|idr2)$' | while read -r f; do |
| 120 | + [ -z "$f" ] && continue |
| 121 | + grep -nE 'believe_me|really_believe_me|assert_total' "$f" 2>/dev/null | while IFS=: read -r ln rest; do |
| 122 | + # Skip comment-only mentions (the entire line is a comment) |
| 123 | + case "$rest" in |
| 124 | + *"||| "*|*"-- "*"believe_me"*) [ -n "$(echo "$rest" | grep -E '^[[:space:]]*\|\|\||^[[:space:]]*--')" ] && continue ;; |
| 125 | + esac |
| 126 | + emit_marker "$f" "$ln" "idris-believe-or-assert" "$(echo "$rest" | head -c 80)" |
| 127 | + done |
| 128 | +done |
| 129 | + |
| 130 | +# Idris2 top-level partial |
| 131 | +echo "$proof_files" | grep -E '\.(idr|idr2)$' | while read -r f; do |
| 132 | + [ -z "$f" ] && continue |
| 133 | + grep -nE '^partial$|^%default[[:space:]]+partial' "$f" 2>/dev/null | while IFS=: read -r ln rest; do |
| 134 | + emit_marker "$f" "$ln" "idris-partial" "$(echo "$rest" | head -c 80)" |
| 135 | + done |
| 136 | +done |
| 137 | + |
| 138 | +# F* assume val / admit_p |
| 139 | +echo "$proof_files" | grep -E '\.fst$' | while read -r f; do |
| 140 | + [ -z "$f" ] && continue |
| 141 | + grep -nE 'assume[[:space:]]+val|admit_p' "$f" 2>/dev/null | while IFS=: read -r ln rest; do |
| 142 | + emit_marker "$f" "$ln" "fstar-assume-or-admit" "$(echo "$rest" | head -c 80)" |
| 143 | + done |
| 144 | +done |
| 145 | + |
| 146 | +# Rust/Haskell soundness-relevant escapes (only inside src/) |
| 147 | +if [ -n "$unsafe_files" ]; then |
| 148 | + echo "$unsafe_files" | head -2000 | while read -r f; do |
| 149 | + [ -z "$f" ] && continue |
| 150 | + grep -nE 'unsafePerformIO|unsafeCoerce' "$f" 2>/dev/null | while IFS=: read -r ln rest; do |
| 151 | + # Skip if this is a comment line |
| 152 | + case "$rest" in |
| 153 | + *"//"*"unsafePerformIO"*|*"--"*"unsafePerformIO"*) |
| 154 | + [ -n "$(echo "$rest" | grep -E '^[[:space:]]*//|^[[:space:]]*--')" ] && continue ;; |
| 155 | + esac |
| 156 | + emit_marker "$f" "$ln" "rust-or-hs-unsafe" "$(echo "$rest" | head -c 80)" |
| 157 | + done |
| 158 | + done |
| 159 | +fi |
| 160 | + |
| 161 | +marker_count=$(wc -l < "$markers_tsv") |
| 162 | + |
| 163 | +if [ "$marker_count" -eq 0 ]; then |
| 164 | + echo "[OK] No soundness-relevant escape hatches detected." |
| 165 | + exit 0 |
| 166 | +fi |
| 167 | + |
| 168 | +echo "[INFO] Found $marker_count soundness-relevant escape hatch(es)." |
| 169 | + |
| 170 | +# ───────────────────────────────────────────────────────────────────────────── |
| 171 | +# Verify each marker is documented: |
| 172 | +# - inline `TRUSTED:` or `AXIOM:` comment within 5 lines preceding, OR |
| 173 | +# - enumerated in docs/proof-debt.md (substring match on file:line OR on the |
| 174 | +# identifier captured) |
| 175 | +# ───────────────────────────────────────────────────────────────────────────── |
| 176 | +debt_docs=() |
| 177 | +for cand in docs/proof-debt.md docs/proof-debt.adoc PROOF-NEEDS.md docs/PROOF-NEEDS.md; do |
| 178 | + if [ -f "$cand" ]; then |
| 179 | + debt_docs+=("$cand") |
| 180 | + fi |
| 181 | +done |
| 182 | + |
| 183 | +if [ ${#debt_docs[@]} -eq 0 ]; then |
| 184 | + echo "[ERROR] No docs/proof-debt.md (or equivalent) found, but $marker_count escape hatches exist." |
| 185 | + echo "[ERROR] Seed one per the schema at hyperpolymath/standards/docs/TRUSTED-BASE-REDUCTION-POLICY.adoc." |
| 186 | + exit 1 |
| 187 | +fi |
| 188 | + |
| 189 | +echo "[OK] proof-debt document(s) found: ${debt_docs[*]}" |
| 190 | + |
| 191 | +# For each marker, check documentation |
| 192 | +undocumented=0 |
| 193 | +while IFS=$'\t' read -r f ln kind ctx; do |
| 194 | + # Strip leading ./ |
| 195 | + f_clean="${f#./}" |
| 196 | + |
| 197 | + # 1. Inline TRUSTED:/AXIOM: comment on any of the 5 lines preceding the marker |
| 198 | + local_start=$(( ln - 5 )) |
| 199 | + [ "$local_start" -lt 1 ] && local_start=1 |
| 200 | + if sed -n "${local_start},${ln}p" "$f" 2>/dev/null | grep -qE 'TRUSTED:|AXIOM:'; then |
| 201 | + continue |
| 202 | + fi |
| 203 | + |
| 204 | + # 2. Mention in ANY of the proof-debt documents — match on `<file>:<line>` |
| 205 | + # substring, or on the file path alone (in which case we accept any |
| 206 | + # reference). |
| 207 | + documented_in="" |
| 208 | + for doc in "${debt_docs[@]}"; do |
| 209 | + if grep -qF "$f_clean:$ln" "$doc" 2>/dev/null; then |
| 210 | + documented_in="$doc" |
| 211 | + break |
| 212 | + fi |
| 213 | + if grep -qF "$f_clean" "$doc" 2>/dev/null; then |
| 214 | + documented_in="$doc" |
| 215 | + break |
| 216 | + fi |
| 217 | + done |
| 218 | + if [ -n "$documented_in" ]; then |
| 219 | + continue |
| 220 | + fi |
| 221 | + |
| 222 | + # Undocumented. |
| 223 | + echo "[ERROR] Undocumented escape hatch at $f_clean:$ln ($kind):" |
| 224 | + echo " $ctx" |
| 225 | + echo " Annotate with a 'TRUSTED:' or 'AXIOM:' leading comment, or" |
| 226 | + echo " enumerate in any of: ${debt_docs[*]}" |
| 227 | + undocumented=$((undocumented + 1)) |
| 228 | +done < "$markers_tsv" |
| 229 | + |
| 230 | +if [ "$undocumented" -gt 0 ]; then |
| 231 | + echo "" |
| 232 | + 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[*]}" |
| 234 | + echo "[ERROR] See https://github.com/hyperpolymath/standards/blob/main/docs/TRUSTED-BASE-REDUCTION-POLICY.adoc" |
| 235 | + exit 1 |
| 236 | +fi |
| 237 | + |
| 238 | +echo "[OK] All $marker_count escape hatch(es) are documented (inline annotation or entry in: ${debt_docs[*]})." |
| 239 | +exit 0 |
0 commit comments