diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 9654178..9c93552 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -78,6 +78,18 @@ jobs: - name: Verify witness quality (ban fake check-only witnesses) run: bash scripts/check_witness_quality.sh + # Statement-level non-vacuity: lints the .lean files CHANGED by this PR + # for near-vacuity shapes (∀var ∃const quantifier inversion, `: True` + # conclusion, `: False` hypothesis) that build/axiom/witness gates miss, + # and fails on any unsigned flag. A genuine statement that trips the lint + # carries an inline `-- fidelity:` sign-off. Self-tests its detector on a + # vacuous/genuine fixture pair. The base ref is passed so the diff is + # scoped to the PR; on push it falls back to HEAD~1, else all files. + - name: Verify statement fidelity (non-vacuity, changed files) + env: + FIDELITY_BASE_REF: ${{ github.event.pull_request.base.sha }} + run: bash scripts/check_statement_fidelity.sh + - name: Verify no custom constants run: | if grep -rnE --include="*.lean" '^[[:space:]]*constant[[:space:]]+[^:]+:' FormalSLT/ FormalSLT.lean examples/; then diff --git a/scripts/check_statement_fidelity.sh b/scripts/check_statement_fidelity.sh new file mode 100755 index 0000000..419c2a7 --- /dev/null +++ b/scripts/check_statement_fidelity.sh @@ -0,0 +1,128 @@ +#!/usr/bin/env bash +# Statement-fidelity / non-vacuity gate (BLOCKING). +# +# Why this exists: a theorem can build, be axiom-clean, and still be vacuous +# (e.g. a quantifier-inverted ∀var ∃const bound, a `: True` conclusion, or a +# `: False` hypothesis). The build/axiom/witness gates do not catch those +# shapes at the statement level. This gate lints the common near-vacuity shapes +# on the .lean files touched by a change and FAILS the build on any unsigned +# flag. A genuinely non-vacuous statement that trips the lint carries an inline +# `-- fidelity:` sign-off explaining why (e.g. why the constant is uniform); +# the checker downgrades a signed flag to `ok(signed)`. +# +# Scope: it runs on the .lean files CHANGED by the current PR/push (diff vs the +# base ref), so a clean PR is not blocked by a pre-existing statement elsewhere. +# When no base ref is resolvable (e.g. a manual run on a detached checkout) it +# falls back to scanning every tracked .lean file. +# +# It then runs a fixture pair to prove the detector discriminates: a synthetic +# vacuous theorem MUST be flagged (gate would fail), and a synthetic genuine +# theorem MUST pass. This proves the gate itself works, so a regression that +# silently neuters the checker is caught. +# +# Run from CI alongside the build, axiom, and witness-quality gates. +set -euo pipefail + +ROOT="$(git rev-parse --show-toplevel)" +cd "$ROOT" + +CHECKER="$ROOT/scripts/statement_fidelity_check.py" +if [ ! -f "$CHECKER" ]; then + echo "FAIL: $CHECKER not found" >&2 + exit 1 +fi + +# --- Resolve the set of changed .lean files. --------------------------------- +# Priority: +# 1. explicit base ref in FIDELITY_BASE_REF (lets CI pass the PR base sha) +# 2. GitHub PR base (origin/$GITHUB_BASE_REF) on pull_request events +# 3. the previous commit (HEAD~1) on a push with history +# 4. fall back: every tracked .lean file +base_ref="" +if [ -n "${FIDELITY_BASE_REF:-}" ] && git rev-parse --verify --quiet "${FIDELITY_BASE_REF}^{commit}" >/dev/null; then + base_ref="${FIDELITY_BASE_REF}" +elif [ -n "${GITHUB_BASE_REF:-}" ]; then + git fetch --quiet --depth=1 origin "${GITHUB_BASE_REF}" 2>/dev/null || true + if git rev-parse --verify --quiet "origin/${GITHUB_BASE_REF}^{commit}" >/dev/null; then + base_ref="origin/${GITHUB_BASE_REF}" + fi +elif git rev-parse --verify --quiet "HEAD~1^{commit}" >/dev/null; then + base_ref="HEAD~1" +fi + +declare -a CHANGED=() +if [ -n "$base_ref" ]; then + mb="$(git merge-base "$base_ref" HEAD 2>/dev/null || echo "$base_ref")" + echo "== statement-fidelity gate: changed .lean files vs ${base_ref} (merge-base ${mb}) ==" + while IFS= read -r f; do + [ -n "$f" ] || continue + case "$f" in *.lean) [ -f "$f" ] && CHANGED+=("$f") ;; esac + done < <(git diff --name-only --diff-filter=ACMR "$mb" HEAD) +else + echo "== statement-fidelity gate: no base ref resolvable, scanning all tracked .lean files ==" + while IFS= read -r f; do + [ -n "$f" ] && CHANGED+=("$f") + done < <(git ls-files '*.lean') +fi + +fail=0 + +if [ "${#CHANGED[@]}" -eq 0 ]; then + echo " (no .lean files in scope)" +else + for f in "${CHANGED[@]}"; do + out="$(python3 "$CHECKER" "$f" 2>&1)" && rc=0 || rc=$? + if [ "$rc" -ne 0 ]; then + echo " FLAG in $f" >&2 + echo "$out" | sed 's/^/ /' >&2 + fail=1 + elif echo "$out" | grep -q 'ok(signed)'; then + echo " ok (signed flag) $f" + echo "$out" | grep 'ok(signed)' | sed 's/^/ /' + fi + done + [ "$fail" -eq 0 ] && echo " ok: ${#CHANGED[@]} changed .lean file(s), no unsigned fidelity flags" +fi + +# --- Fixture pair: prove the detector actually discriminates. ----------------- +echo "== detector fixture pair ==" +WORK="$(mktemp -d)" +trap 'rm -rf "$WORK"' EXIT + +VACUOUS_FIX="$WORK/FixtureVacuous.lean" +cat > "$VACUOUS_FIX" <<'EOF' +-- ∀t ∃c, ‖f t‖ ≤ c * g t : the constant is chosen after the variable, so the +-- bound is trivially satisfiable. The detector MUST flag this (quantifier +-- inversion). The genuine form is ∃c, ∀t. +theorem fixture_vacuous {t : ℝ} (f g : ℝ → ℝ) : ∃ c : ℝ, ‖f t‖ ≤ c * (g t) := by + sorry +EOF + +GENUINE_FIX="$WORK/FixtureGenuine.lean" +cat > "$GENUINE_FIX" <<'EOF' +-- ∃c, ∀t : the constant is uniform over t (quantified inside the ∃). The +-- detector MUST NOT flag this; it is the genuine, non-vacuous shape. +theorem fixture_genuine (f g : ℝ → ℝ) : ∃ c : ℝ, ∀ t : ℝ, ‖f t‖ ≤ c * (g t) := by + sorry +EOF + +if python3 "$CHECKER" "$VACUOUS_FIX" >/dev/null 2>&1; then + echo " FAIL vacuous fixture was NOT flagged (detector broken)" >&2 + fail=1 +else + echo " ok vacuous fixture flagged (detector RED-flags quantifier inversion)" +fi + +if python3 "$CHECKER" "$GENUINE_FIX" >/dev/null 2>&1; then + echo " ok genuine (∃c ∀t) fixture passed" +else + echo " FAIL genuine fixture was flagged (detector over-eager)" >&2 + fail=1 +fi + +if [ "$fail" -ne 0 ]; then + echo "statement-fidelity gate FAILED" >&2 + exit 1 +fi + +echo "statement-fidelity gate passed: no unsigned fidelity flags, detector verified" diff --git a/scripts/statement_fidelity_check.py b/scripts/statement_fidelity_check.py new file mode 100755 index 0000000..1714b43 --- /dev/null +++ b/scripts/statement_fidelity_check.py @@ -0,0 +1,106 @@ +#!/usr/bin/env python3 +"""Statement-fidelity / non-vacuity gate for Lean theorems (NON-NEGOTIABLE). + +Vacuity is undecidable in general, so this does the two things that ARE mechanizable and forces the +rest to an explicit human/adversarial sign-off: + + 1. LINT the common near-vacuity shapes (static, regex over theorem statements): + - quantifier inversion: a theorem with a free variable param (e.g. {t : ℝ}) whose conclusion is + `∃ c ..., ‖f t ...‖ ≤ c * (...)` — i.e. ∀t ∃c, near-vacuous (the constant is chosen AFTER the + variable, so the bound is trivially satisfiable). The genuine form is ∃c, ∀t. (This is the + INC-2026-06-22 lemma-3 catch.) + - trivial conclusion: `: True`, `↔ True`, or a hypothesis that is literally `False`. + 2. REQUIRE a fidelity sign-off for every load-bearing theorem: a `-- fidelity:` line stating why the + statement is non-vacuous (the witness / why the constant is uniform / the adversarial-falsify result), + OR the theorem is flagged. + +It does NOT replace the adversarial-falsify reasoning pass — it forces it. Run on a Lean file; exit 1 on flags. +Usage: statement_fidelity_check.py [theorem_name ...] +""" +import re, sys + +NORM = r'(?:‖|\bnorm\b|abs |\|)' # a magnitude on the LHS of a bound + +def theorems(src): + # crude: split on top-level `theorem`/`lemma` keywords, keep name + the statement up to `:= by`/`:=`. + # The vacuity lint runs on `stmt` (the statement only). The `-- fidelity:` sign-off, however, may sit + # on the comment line(s) immediately ABOVE the keyword or anywhere inside the proof body, so we also + # yield a `signoff` window that spans from the preceding comment block through the body up to the next + # top-level decl. Without this, a legitimate `-- fidelity:` override never registers (the sign-off line + # is outside `stmt`), and the gate would block genuine ∃c-∀var theorems with no working escape hatch. + starts = [m.start() for m in re.finditer(r'(?m)^\s*(?:noncomputable\s+)?(?:theorem|lemma)\s+[A-Za-z0-9_\']+', src)] + for i, m in enumerate(re.finditer(r'(?m)^\s*(?:noncomputable\s+)?(?:theorem|lemma)\s+([A-Za-z0-9_\']+)', src)): + name = m.group(1) + start = m.start() + nxt = starts[i + 1] if i + 1 < len(starts) else len(src) + # bound the body to THIS declaration (next top-level decl, capped) so a statement that ends with + # `:= term` (no newline after `:=`) does not bleed into the following theorem and mis-attribute flags. + body = src[start:min(nxt, start + 1600)] + stmt = re.split(r':=\s*by|:=\s*$|:=\n|:=\s', body)[0] + # signoff window: preceding contiguous comment lines + the decl body up to the next top-level decl. + pre = src[:start] + lines = pre.split('\n') + j = len(lines) - 1 + if j >= 0 and lines[j].strip() == '': + j -= 1 + k = j + while k >= 0 and lines[k].lstrip().startswith('--'): + k -= 1 + comment_block = '\n'.join(lines[k + 1:j + 1]) + signoff = comment_block + '\n' + src[start:nxt] + yield name, stmt, signoff + +def flags_for(name, stmt): + out = [] + # Lean identifiers: letters, digits, _, ', unicode subscripts ₀-₉ and Greek/primes + ID = r"[A-Za-z0-9_\'₀-₉Ͱ-Ͽ]+" + # param vars declared in {..}/(..) of a numeric/complex sort + params = re.findall(r'[\{\(]\s*((?:' + ID + r'\s+)*' + ID + r')\s*:\s*(?:ℝ|ℂ|ℕ|ℤ|ℚ)', stmt) + pvars = set() + for p in params: + pvars.update(p.split()) + pvars = {v for v in pvars if not v.isdigit()} # drop numeric tokens like "1" from `(1 : ℝ)` + # quantifier inversion = BAD (∀var ∃const): a theorem-PARAM var appears in a `≤ c * ...` bound where the + # constant c is ∃-bound, and NO inner `∀` re-binds the var between the ∃ and the bound. The GOOD form + # (∃c, ∀var, bound) has an inner ∀ after the ∃ and must NOT be flagged. + concl = stmt.split(':', 1)[-1] + ex = re.search(r'∃\s*(' + ID + r')', concl) + if ex: + c = ex.group(1) + after = concl[ex.end():] + le = after.find('≤') + seg = after[:le] if le != -1 else after + inner_forall = '∀' in seg # ∃c ... ∀var ... ≤ => uniform => GOOD, skip + bound = re.search(NORM + r'[\s\S]*?≤\s*' + re.escape(c) + r'\s*\*', concl) + mentions_param = any(re.search(re.escape(v), concl) for v in pvars) + if bound and mentions_param and pvars and not inner_forall: + out.append(f"QUANTIFIER-INVERSION: '{name}' is ∀{{{','.join(sorted(pvars))}}} ∃{c} (constant after " + f"variable) — near-vacuous; the genuine form is ∃{c} ∀var. Hoist the ∃ outside the params, " + f"or add a `-- fidelity:` line proving the constant is uniform.") + if re.search(r':\s*True\b', stmt) or re.search(r'↔\s*True\b', stmt): + out.append(f"TRIVIAL-CONCLUSION: '{name}' concludes `True` — vacuous.") + if re.search(r'\(\s*[A-Za-z0-9_\' ]+\s*:\s*False\s*\)', stmt): + out.append(f"FALSE-HYPOTHESIS: '{name}' has a `: False` hypothesis — vacuously true.") + return out + +def main(): + if len(sys.argv) < 2: + print("usage: statement_fidelity_check.py [theorem ...]"); return 2 + src = open(sys.argv[1], encoding='utf-8', errors='ignore').read() + only = set(sys.argv[2:]) + flagged = 0; checked = 0 + for name, stmt, signoff in theorems(src): + if only and name not in only: continue + checked += 1 + fl = flags_for(name, stmt) + signed = bool(re.search(r'--\s*fidelity:', signoff)) + for f in fl: + if signed: + print(f" ok(signed) {f.split(':',1)[0]} on {name} — has -- fidelity: sign-off") + else: + print(f" FLAG {f}"); flagged += 1 + print(f"--- checked {checked} decl(s), {flagged} flag(s)") + return 1 if flagged else 0 + +if __name__ == "__main__": + sys.exit(main())