mirror of
https://github.com/allaunthefox/SilverSight.git
synced 2026-07-31 01:25:21 +00:00
ba8ee11159
Three fixes per code review:
1. CARTAN/HOLOMONY := True → CONJECTURE sorry
The two predicates were def := True + theorem := trivial. This is the
exact YB tautology pattern in def-clothing: a named predicate that's
definitionally True, so the conjecture is vacuously proven, and it
passes the scanner clean. Fixed: predicates are now Nonempty (M → M)
(placeholder, not True), and theorems are sorry with CONJECTURE tags.
The sorry is loud (sorryAx shows in #print axioms).
2. SCANNER PATCH: catch vacuous-predicate proofs
Extended anti_smuggle_check.py to detect or
or multi-line where the predicate is defined as True
in the same file. This closes the blind spot exposed by the := True
conversion: the scanner now catches the YB pattern in def-clothing.
Verified: catches the test case, passes on the fixed UnifiedCovariant.
3. AXIOM WITNESS upgraded to whitelist
#print axioms comment now specifies the full whitelist:
{propext, Classical.choice, Quot.sound, sorryAx}
Any axiom outside this set is a smuggle. The sorryAx entries are
expected (from the 3 CONJECTURE/CITED sorries) and documented.
228 lines
9.4 KiB
Python
228 lines
9.4 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*$')
|
|
|
|
# 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|AXIOM)',
|
|
re.IGNORECASE
|
|
)
|
|
|
|
|
|
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) and ci_mode:
|
|
# Check if the sorry is justified (has CITED/CONJECTURE/JUSTIFICATION tag nearby)
|
|
surrounding = '\n'.join(lines[max(0, i - 5):min(len(lines), i + 2)])
|
|
if not AXIOM_JUSTIFIED.search(surrounding):
|
|
findings += 1
|
|
print(f" [WARN] {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)")
|
|
|
|
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())
|