security/framework/checks/axiom-budget.sh

#!/usr/bin/env bash
# axiom-budget.sh -- count unproven-assertion primitives in a proof tree and
# fail if they drift above the declared budget.
#
# The framework's honest-disclosure rule: every `sorry`, `admit`/`abort`,
# `axiom`, `declare axiom`, and vacuous `:= True`/`trivial` is an UNPROVEN
# assertion. Their count is the proof's real surface of trust. It must be
# DECLARED (in `<repo>/.assurance/budget.txt`, one `KEY=MAX` per line) and may
# never silently grow. Magnetar shipped 69 such assertions while PROOF-CLAIMS
# read "proven".
#
# COMMENT-AWARE: word-grep is too dumb -- it counts prose like
# "DISCHARGED (no admit)" or "axiom would be discharged..." as a real
# assertion (this over-counted pulsar at 87 and magnetar admits at 4, all from
# `(* ... *)` / `--` comment lines). We strip comments FIRST, then count only
# real declarations/tactics. A separate prose linter runs as a WARNING only.
#
# budget.txt keys: SORRY, ADMIT, AXIOM, VACUOUS (omitted key => max 0).
# No budget.txt => report-only the first time (prints the counts to seed one).
#
# Usage: axiom-budget.sh <repo-root>
set -uo pipefail
ROOT="${1:?usage: axiom-budget.sh <repo-root>}"
PD=""
for d in "$ROOT/proofs" "$ROOT/spec" "$ROOT"; do [ -d "$d" ] && PD="$d" && break; done
[ -z "$PD" ] && { echo "    [skip] no proof tree"; exit 0; }

# Strip comments from a single proof file, preserving line structure.
#   .ec    -> nestable (* ... *) blocks
#   .lean  -> nestable /- ... -/ blocks + `--` line comments
# (EC has no line comment; Lean line comment runs to EOL.)
strip_comments() {
  case "$1" in
    *.ec)
      awk '
        BEGIN { depth = 0 }
        {
          out = ""; i = 1; n = length($0)
          while (i <= n) {
            c2 = substr($0, i, 2)
            if (depth > 0) {
              if (c2 == "*)") { depth--; i += 2; continue }
              if (c2 == "(*") { depth++; i += 2; continue }
              i++; continue
            } else {
              if (c2 == "(*") { depth++; i += 2; continue }
              out = out substr($0, i, 1); i++
            }
          }
          print out
        }' "$1" ;;
    *.lean)
      awk '
        BEGIN { depth = 0 }
        {
          out = ""; i = 1; n = length($0)
          while (i <= n) {
            c2 = substr($0, i, 2)
            if (depth > 0) {
              if (c2 == "-/") { depth--; i += 2; continue }
              if (c2 == "/-") { depth++; i += 2; continue }
              i++; continue
            } else {
              if (c2 == "/-") { depth++; i += 2; continue }
              if (c2 == "--") { break }          # line comment to EOL
              out = out substr($0, i, 1); i++
            }
          }
          print out
        }' "$1" ;;
    *) cat "$1" ;;
  esac
}

# count <ext-glob...> <ERE> : count ERE matches over comment-stripped sources.
count_stripped() {
  local ere="$1"; shift
  local total=0 f
  for f in "$@"; do
    [ -f "$f" ] || continue
    c=$(strip_comments "$f" | grep -hoE "$ere" 2>/dev/null | wc -l | tr -d ' ')
    total=$((total + c))
  done
  echo "$total"
}

mapfile -t EC_FILES   < <(find "$PD" -name '*.ec'   2>/dev/null)
mapfile -t LEAN_FILES < <(find "$PD" -name '*.lean' 2>/dev/null)
ALL=( "${EC_FILES[@]}" "${LEAN_FILES[@]}" )

# Real Lean unproven terms: `sorry`/`admit` as tokens (post-strip).
SORRY=$(count_stripped '(^|[^A-Za-z0-9_])sorry([^A-Za-z0-9_]|$)' "${LEAN_FILES[@]}")
# Real proof-closing-without-proof tactics: Lean `admit`, EC `admit`/`abort`.
ADMIT=$(count_stripped '(^|[^A-Za-z0-9_])(admit|abort)([^A-Za-z0-9_]|$)' "${ALL[@]}")
# Real axiom declarations (line-anchored, post-strip).
AXIOM=$(count_stripped '^[[:space:]]*(declare[[:space:]]+)?axiom[[:space:]]' "${ALL[@]}")
# Vacuous Lean bodies.
VACUOUS=$(count_stripped ':=[[:space:]]*(True|trivial)([[:space:]]|$)' "${LEAN_FILES[@]}")

echo "    counts (comment-stripped): SORRY=$SORRY ADMIT=$ADMIT AXIOM=$AXIOM VACUOUS=$VACUOUS"

# Prose linter -- WARNING ONLY. Mentions of these words inside comments are
# often legitimate ("DISCHARGED (no admit)"); surfaced so a reviewer can spot a
# claim that should be code, never gating.
PROSE=0
for f in "${ALL[@]}"; do
  [ -f "$f" ] || continue
  raw=$(grep -cE '(^|[^A-Za-z0-9_])(sorry|admit|abort)([^A-Za-z0-9_]|$)' "$f" 2>/dev/null); raw=${raw:-0}
  strp=$(strip_comments "$f" | grep -cE '(^|[^A-Za-z0-9_])(sorry|admit|abort)([^A-Za-z0-9_]|$)' 2>/dev/null); strp=${strp:-0}
  PROSE=$((PROSE + raw - strp))
done
[ "$PROSE" -gt 0 ] && echo "    [warn] $PROSE comment-only mention(s) of sorry/admit/abort (prose, not counted)"

BUD="$ROOT/.assurance/budget.txt"
if [ ! -f "$BUD" ]; then
  echo "    [warn] no $BUD -- declare a budget to enforce drift. Seed it with the counts above."
  exit 0
fi
get() { grep -E "^$1=" "$BUD" 2>/dev/null | tail -1 | cut -d= -f2 | tr -dc '0-9'; }
fail=0
for k in SORRY ADMIT AXIOM VACUOUS; do
  cur=$(eval echo \$$k); max=$(get "$k"); max=${max:-0}
  if [ "$cur" -gt "$max" ]; then
    echo "    [FAIL] $k=$cur exceeds declared budget $max -- new unproven assertions added without updating .assurance/budget.txt + PROOF-CLAIMS"
    fail=1
  fi
done
[ "$fail" -eq 0 ] && { echo "    [ok]   unproven-assertion counts within declared budget"; exit 0; }
exit 2