#!/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 := ` where 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 := `. # 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())