mirror of
https://github.com/allaunthefox/SilverSight.git
synced 2026-07-31 01:25:21 +00:00
allaun
3b1e590b09
Scanner (scripts/anti_smuggle_check.py): - detect trivially-inhabited Prop defs — Nonempty (M→M), True, Nonempty Unit — the stealth-True pattern that evaded the `:= True`-only check; leaves real predicates like Nonempty (KählerManifold V) untouched. - flag standalone `sorry` (the `by\n sorry` shape) that evaded the `:=`/`=>`-prefixed EMPTY_SORRY regex; routed through the same justification-tag window so tagged research sorries stay clean. Archive: - preserve + log formal/CoreFormalism/SidonWrapping.lean, a rotted orphan (never registered, imported nowhere, crtLift arity mismatch, 2 unjustified sorries). File was untracked, so removed from disk directly; full source + rationale kept under archive/2026-07-03/ with DELETION_LOG.md. Effect: strict `anti_smuggle_check.py --ci formal` was a false green (missed the two gaps above); now an honest green after the orphan removal. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
276 lines
12 KiB
Python
276 lines
12 KiB
Python
#!/usr/bin/env python3
|
|
"""
|
|
Anti-smuggle CI gate: detect vacuous theorems and unjustified axioms.
|
|
|
|
Catches patterns like:
|
|
- theorem body is `:= rfl` with no prior computation
|
|
- equality where both sides are syntactically identical (bound var rename)
|
|
- `:=` followed by a reference to a trivially-true definition
|
|
- `by` block with only `rfl` or `simp` that does no work
|
|
- `axiom` declarations without a justification tag (CITED/CONJECTURE/JUSTIFICATION)
|
|
- bare `sorry` without a justification tag
|
|
|
|
The axiom scanner is the key anti-smuggle layer: a `sorry` screams
|
|
(sorryAx warning), but a custom `axiom` named like a citation slips
|
|
past both lean_verify and the rfl/renamed-sum checks. Every custom
|
|
axiom must carry a justification tag in its docstring or it fails CI.
|
|
|
|
Usage:
|
|
python3 scripts/anti_smuggle_check.py # scan formal/
|
|
python3 scripts/anti_smuggle_check.py --ci # strict mode (exit 1 on any finding)
|
|
python3 scripts/anti_smuggle_check.py --file foo.lean # single file
|
|
"""
|
|
|
|
import argparse
|
|
import os
|
|
import re
|
|
import sys
|
|
from pathlib import Path
|
|
|
|
SUSPICIOUS_RFL = re.compile(
|
|
r'(theorem|lemma)\s+(\w+)\s*[^:]*:\s*([^=]+)=\s*([^=]+)\s*:=\s*rfl\b'
|
|
)
|
|
SUSPICIOUS_BY_RFL = re.compile(
|
|
r'(theorem|lemma)\s+(\w+)\s*[^:]*:\s*([^=]+)=\s*([^=]+)\s*:=\s*by\s+rfl\b'
|
|
)
|
|
SUSPICIOUS_RENAME = re.compile(
|
|
r'(theorem|lemma)\s+(\w+)\s*[^:]*:\s*'
|
|
r'∀[^,]+,([^,]+),([^,]+),([^,]+),([^,]+),([^,]+),([^,]+)\.\s*'
|
|
r'\(∑[^:]+\s*=\s*∑[^:]+\)'
|
|
)
|
|
|
|
BARE_RFL_LINE = re.compile(r'^\s*(:=|=>)\s*rfl\s*$')
|
|
LAMBDA_RFL = re.compile(
|
|
r'^\s*:=\s*(fun\s+(\w+\s+)+\w+\s*=>\s*rfl|λ\s+(\w+\s+)+\w+\s*=>\s*rfl)\s*$'
|
|
)
|
|
EMPTY_SORRY = re.compile(r'^\s*(:=|=>)\s*(by\s+)?sorry\s*$')
|
|
# Standalone `sorry` / `by sorry` at the start of a line (the `by\n sorry`
|
|
# shape) — evades EMPTY_SORRY, which needs a `:=`/`=>` prefix. Trailing comment
|
|
# allowed (`\b`, not `$`), so `sorry -- CONJECTURE: …` still matches and is
|
|
# then cleared by the justification-window check.
|
|
STANDALONE_SORRY = re.compile(r'^\s*(by\s+)?sorry\b')
|
|
|
|
# Axiom declarations — any custom axiom must carry a justification tag
|
|
AXIOM_DECL = re.compile(r'^\s*axiom\s+(\w+)\b')
|
|
AXIOM_JUSTIFIED = re.compile(
|
|
r'(?:CITED|CONJECTURE|JUSTIFICATION|HONESTY CLASS)',
|
|
re.IGNORECASE
|
|
)
|
|
|
|
# Predicate defs whose body is TRIVIALLY INHABITED — "stealth True".
|
|
# A `def NAME ... : Prop := <body>` where <body> is closable with no real
|
|
# content lets a companion `theorem NAME ... := ⟨id⟩ / trivial` vacuously
|
|
# "prove" a named conjecture while dodging the `:= True` scanner (the body is
|
|
# not literally True). The canonical trap is `Nonempty (M → M)` — inhabited by
|
|
# `⟨id⟩`. Detect the concrete, defensible set; a real predicate like
|
|
# `Nonempty (KählerManifold V)` (structure argument, no self-arrow) is NOT hit.
|
|
DEF_PROP = re.compile(
|
|
r'def\s+(\w+)\b.*?:\s*Prop\s*:=\s*(.+?)\s*$', re.MULTILINE
|
|
)
|
|
# Nonempty (X → X): identity inhabits it. Domain must equal codomain.
|
|
NONEMPTY_ENDO = re.compile(r'^Nonempty\s*\(\s*([\w.]+)\s*(?:→|->)\s*([\w.]+)\s*\)$')
|
|
# Directly trivially-inhabited bodies (Prop-level units / reflexive True).
|
|
TRIVIAL_BODY = re.compile(
|
|
r'^(True'
|
|
r'|Nonempty\s+(?:PUnit|Unit|True)\b.*'
|
|
r'|Nonempty\s*\(\s*(?:PUnit|Unit|True)\b.*\)'
|
|
r'|PUnit|Unit)$'
|
|
)
|
|
|
|
|
|
def is_trivially_inhabited_body(body: str) -> bool:
|
|
"""True if a `: Prop :=` body is closable with no mathematical content."""
|
|
b = body.strip().rstrip('-').strip() # drop trailing `-- comment` start
|
|
# strip a trailing inline comment if present
|
|
b = re.split(r'\s--', b, maxsplit=1)[0].strip()
|
|
if TRIVIAL_BODY.match(b):
|
|
return True
|
|
m = NONEMPTY_ENDO.match(b)
|
|
if m and m.group(1) == m.group(2):
|
|
return True
|
|
return False
|
|
|
|
|
|
def check_file(path: str, ci_mode: bool) -> int:
|
|
"""Check a single .lean file for smuggle patterns. Returns finding count."""
|
|
findings = 0
|
|
try:
|
|
with open(path, 'r') as f:
|
|
content = f.read()
|
|
except Exception as e:
|
|
print(f" ERROR reading {path}: {e}")
|
|
return 0
|
|
|
|
rel = os.path.relpath(path)
|
|
|
|
# 1. Check for `:= rfl` after an equality
|
|
for m in SUSPICIOUS_RFL.finditer(content):
|
|
lhs = m.group(3).strip()
|
|
rhs = m.group(4).strip()
|
|
if lhs == rhs:
|
|
findings += 1
|
|
print(f" [SMUGGLE] {rel}:{line_of(content, m.start())} "
|
|
f"theorem '{m.group(2)}' is `:= rfl` with identical LHS/RHS '{lhs}'")
|
|
|
|
# 2. Check for `:= by rfl`
|
|
for m in SUSPICIOUS_BY_RFL.finditer(content):
|
|
lhs = m.group(3).strip()
|
|
rhs = m.group(4).strip()
|
|
if lhs == rhs:
|
|
findings += 1
|
|
print(f" [SMUGGLE] {rel}:{line_of(content, m.start())} "
|
|
f"theorem '{m.group(2)}' is `:= by rfl` with identical LHS/RHS")
|
|
|
|
# 3. Check for the YB pattern: sums with bound variable rename
|
|
for m in SUSPICIOUS_RENAME.finditer(content):
|
|
# This is a specific pattern: ∀ ... (sum ... r ... = sum ... s ...)
|
|
# It might still be non-trivial if the body does work; flag for review
|
|
findings += 1
|
|
print(f" [SMUGGLE] {rel}:{line_of(content, m.start())} "
|
|
f"theorem '{m.group(2)}' has ∀-quantified equation with sums "
|
|
f"(possible bound-variable rename)")
|
|
|
|
# 4. Check for trivial theorem bodies: `:= rfl`, `:= fun ... => rfl`, `:= by rfl`
|
|
lines = content.split('\n')
|
|
for i, line in enumerate(lines):
|
|
stripped = line.strip()
|
|
|
|
# Check single-line `:= rfl`
|
|
if re.match(r'^\s*:=\s*rfl\s*$', stripped):
|
|
surrounding = '\n'.join(lines[max(0, i - 3):i + 1])
|
|
if re.search(r'(theorem|lemma)\s+\w+', surrounding):
|
|
findings += 1
|
|
print(f" [SMUGGLE] {rel}:{i + 1} bare `:= rfl` as theorem body")
|
|
|
|
# Check `:= fun ... => rfl` (possibly multi-line: `:=` on prev line, `fun ... => rfl` on this line)
|
|
if re.match(r'^\s*fun\s+(\w+\s+)+\w+\s*=>\s*rfl\s*$', stripped) or \
|
|
re.match(r'^\s*λ\s+(\w+\s+)+\w+\s*=>\s*rfl\s*$', stripped):
|
|
surrounding = '\n'.join(lines[max(0, i - 2):i + 1])
|
|
if re.search(r'(theorem|lemma)\s+\w+|:=\s*$', surrounding, re.MULTILINE):
|
|
findings += 1
|
|
print(f" [SMUGGLE] {rel}:{i + 1} `fun ... => rfl` lambda as theorem body")
|
|
|
|
if (EMPTY_SORRY.match(stripped) or STANDALONE_SORRY.match(stripped)) and ci_mode:
|
|
# Check if the sorry is justified (has CITED/CONJECTURE/JUSTIFICATION tag nearby)
|
|
surrounding = '\n'.join(lines[max(0, i - 8):min(len(lines), i + 2)])
|
|
if not AXIOM_JUSTIFIED.search(surrounding):
|
|
findings += 1
|
|
print(f" [SMUGGLE] {rel}:{i + 1} bare sorry without justification tag "
|
|
f"(expected CITED/CONJECTURE/JUSTIFICATION)")
|
|
|
|
# Check for vacuous-predicate proofs: `:= trivial` or `:= by trivial`
|
|
# or multi-line `:= by\n trivial`
|
|
# where the predicate is defined as `True` or unfolds to `True`.
|
|
# This is the YB pattern in def-clothing: a named geometric predicate
|
|
# that's definitionally True, so the conjecture is vacuously proven.
|
|
if re.match(r'^\s*:=\s*(by\s+)?trivial\s*$', stripped) or \
|
|
re.match(r'^\s*trivial\s*$', stripped):
|
|
surrounding = '\n'.join(lines[max(0, i - 10):i + 1])
|
|
if re.search(r'(theorem|lemma)\s+\w+', surrounding):
|
|
# Check if the predicate in the theorem statement is defined as True
|
|
theorem_match = re.search(r'(theorem|lemma)\s+(\w+)\s*:\s*(\w+)', surrounding)
|
|
if theorem_match:
|
|
pred_name = theorem_match.group(3)
|
|
# Check if this predicate is defined as True anywhere in the file
|
|
true_def = re.compile(
|
|
rf'def\s+{re.escape(pred_name)}\b.*?:=\s*True\b',
|
|
re.DOTALL
|
|
)
|
|
if true_def.search(content):
|
|
findings += 1
|
|
print(f" [SMUGGLE] {rel}:{i + 1} `trivial` on predicate "
|
|
f"'{pred_name}' defined as True "
|
|
f"(vacuous proof of conjecture)")
|
|
else:
|
|
print(f" [INFO] {rel}:{i + 1} `trivial` on '{pred_name}' "
|
|
f"(predicate not True — may be legitimate)")
|
|
|
|
# 5. Inventory custom axiom declarations
|
|
# Every `axiom` must have a justification tag in the preceding docstring/comment.
|
|
# Unjustified axioms are the quiet smuggle: they look like citations but
|
|
# slip past lean_verify and the compiler's sorry warning.
|
|
for i, line in enumerate(lines):
|
|
m = AXIOM_DECL.match(line)
|
|
if m:
|
|
axiom_name = m.group(1)
|
|
# Skip standard library axioms (propext, Classical, etc.)
|
|
if axiom_name in ('propext', 'Classical', 'ofNonempty', 'Quot',
|
|
'funext', 'choice', 'Exists'):
|
|
continue
|
|
# Check preceding 10 lines for justification tag
|
|
preceding = '\n'.join(lines[max(0, i - 10):i])
|
|
if AXIOM_JUSTIFIED.search(preceding):
|
|
# Justified axiom — OK but inventory it
|
|
print(f" [AXIOM] {rel}:{i + 1} axiom '{axiom_name}' (justified)")
|
|
else:
|
|
findings += 1
|
|
print(f" [SMUGGLE] {rel}:{i + 1} axiom '{axiom_name}' "
|
|
f"WITHOUT justification tag "
|
|
f"(expected CITED/CONJECTURE/JUSTIFICATION in docstring)")
|
|
|
|
# 6. Stealth-True predicate defs: `def NAME ... : Prop := <trivially inhabited>`.
|
|
# Catches the `Nonempty (M → M)` blind spot that the `:= True` scanner misses.
|
|
for m in DEF_PROP.finditer(content):
|
|
name, body = m.group(1), m.group(2)
|
|
if is_trivially_inhabited_body(body):
|
|
findings += 1
|
|
print(f" [SMUGGLE] {rel}:{line_of(content, m.start())} def '{name}' "
|
|
f"is a stealth-True predicate (body '{body.strip()}' is trivially "
|
|
f"inhabited — use an opaque `axiom` signature instead)")
|
|
|
|
return findings
|
|
|
|
|
|
def line_of(content: str, pos: int) -> int:
|
|
"""Return 1-indexed line number for a character position."""
|
|
return content[:pos].count('\n') + 1
|
|
|
|
|
|
def check_dir(root: str, ci_mode: bool) -> int:
|
|
"""Recursively check all .lean files under root."""
|
|
total = 0
|
|
for dirpath, _, filenames in os.walk(root):
|
|
for fn in filenames:
|
|
if fn.endswith('.lean'):
|
|
total += check_file(os.path.join(dirpath, fn), ci_mode)
|
|
return total
|
|
|
|
|
|
def main():
|
|
parser = argparse.ArgumentParser(
|
|
description="Anti-smuggle CI gate for Lean theorem vacuity"
|
|
)
|
|
parser.add_argument('paths', nargs='*', default=['formal'],
|
|
help='Files or directories to check')
|
|
parser.add_argument('--ci', action='store_true',
|
|
help='Strict mode: exit 1 on any finding')
|
|
parser.add_argument('--file', type=str,
|
|
help='Check a single file')
|
|
args = parser.parse_args()
|
|
|
|
total = 0
|
|
if args.file:
|
|
total += check_file(args.file, args.ci)
|
|
for path in args.paths:
|
|
if os.path.isfile(path):
|
|
total += check_file(path, args.ci)
|
|
elif os.path.isdir(path):
|
|
total += check_dir(path, args.ci)
|
|
elif path != 'formal':
|
|
print(f"WARNING: {path} not found", file=sys.stderr)
|
|
|
|
if total == 0:
|
|
print("Anti-smuggle check: PASSED (no vacuities detected)")
|
|
return 0
|
|
else:
|
|
msg = f"Anti-smuggle check: {total} potential vacuit{'y' if total == 1 else 'ies'} found"
|
|
if args.ci:
|
|
print(f"FAIL: {msg}", file=sys.stderr)
|
|
return 1
|
|
else:
|
|
print(f"WARNING: {msg}")
|
|
return 0
|
|
|
|
|
|
if __name__ == '__main__':
|
|
sys.exit(main())
|