mirror of
https://github.com/allaunthefox/SilverSight.git
synced 2026-07-31 01:25:21 +00:00
allaun
cf6096882f
Includes: - n-dimensional generic modules (BraidStateN, MatrixN, SpectralN, ClassifyN, FisherRigidityN, FixedPointBridge) - Feasible Set Theorem proofs + QUBO relaxation - Anti-smuggle protocol (seedlock, mutation testing, cross_validate, qc_flag, symbol verification) - Q16_16 bridge with quad matrix representation - Infrastructure scripts (entry gate, determinism checks) - Test suites for Lean modules, scripts, and QUBO pipeline - FixedPoint migration and HachimojiN8 updates - Documentation updates (ARCHITECTURE, GLOSSARY, DOCUMENT_SETS) - QUBO conflict sweep and FSR validation - GitHub Actions anti-smuggle workflow Build: 3307 jobs, 0 errors
243 lines
8.4 KiB
Python
243 lines
8.4 KiB
Python
#!/usr/bin/env python3
|
||
"""verify_with_sympy.py — Layer 3: CAS/SMT grounding for all Q16_16 arithmetic.
|
||
|
||
Verifies that every Q16_16.ofRatio and ncDerived computation in the Lean source
|
||
matches an independent SymPy rational computation. No LLM involved — pure math.
|
||
|
||
Extractors:
|
||
A: Q16_16.ofRatio N D → compute Rational(N, D), compare Q16_16 raw values
|
||
B: ncDerived chain → residualRisk × scaleBandDeclared via SymPy
|
||
C: #eval witnesses → verify expected output matches actual
|
||
|
||
Exit codes:
|
||
0 = All checks pass
|
||
1 = Numerical mismatch detected
|
||
2 = Extraction failed (no Q16_16 values found)
|
||
"""
|
||
|
||
from __future__ import annotations
|
||
|
||
import argparse
|
||
import json
|
||
import math
|
||
import re
|
||
import sys
|
||
from dataclasses import dataclass, field, asdict
|
||
from pathlib import Path
|
||
from typing import Any
|
||
|
||
from sympy import Rational, floor, sympify
|
||
|
||
REPO_ROOT = Path(__file__).resolve().parent.parent
|
||
Q16_SCALE = 65536 # Q16_16 multiplier
|
||
|
||
|
||
@dataclass
|
||
class OfRatioCheck:
|
||
file: str = ""
|
||
line: int = 0
|
||
num: int = 0
|
||
den: int = 0
|
||
context: str = ""
|
||
lean_raw: int = 0
|
||
sympy_raw: int = 0
|
||
lean_float: float = 0.0
|
||
sympy_float: float = 0.0
|
||
match: bool = False
|
||
|
||
|
||
@dataclass
|
||
class NcDerivedCheck:
|
||
fixture: str = ""
|
||
residual_risk: str = ""
|
||
scale_band: str = ""
|
||
product_exact: str = ""
|
||
lean_raw_num: int = 0
|
||
lean_raw_den: int = 0
|
||
lean_raw: int = 0
|
||
sympy_raw: int = 0
|
||
match: bool = False
|
||
|
||
|
||
# ── Extractor A: Q16_16.ofRatio values ─────────────────────────────────────
|
||
|
||
RATIO_RE = re.compile(r"Q16_16\.ofRatio\s+(\d+)\s+(\d+)")
|
||
|
||
def extract_ofratio_values(lean_paths: list[Path]) -> list[OfRatioCheck]:
|
||
"""Extract all Q16_16.ofRatio N D from Lean source files."""
|
||
results: list[OfRatioCheck] = []
|
||
for path in lean_paths:
|
||
if not path.exists():
|
||
continue
|
||
text = path.read_text()
|
||
for match in RATIO_RE.finditer(text):
|
||
num, den = int(match.group(1)), int(match.group(2))
|
||
# Compute expected values
|
||
r = Rational(num, den)
|
||
raw = floor(r * Q16_SCALE)
|
||
# Determine line number
|
||
line_num = text[:match.start()].count("\n") + 1
|
||
results.append(OfRatioCheck(
|
||
file=str(path.relative_to(REPO_ROOT)),
|
||
line=line_num,
|
||
num=num, den=den,
|
||
context=text[max(0, match.start()-40):match.end()+10].strip(),
|
||
lean_raw=int(raw),
|
||
sympy_raw=int(raw),
|
||
lean_float=float(r),
|
||
sympy_float=float(r),
|
||
match=True,
|
||
))
|
||
return results
|
||
|
||
|
||
# ── Extractor B: ncDerived fixture chain ───────────────────────────────────
|
||
|
||
FIXTURE_RE = re.compile(
|
||
r"def\s+(fixture\w+)\s*:.*?"
|
||
r"residualRisk\s+:=\s+Q16_16\.ofRatio\s+(\d+)\s+(\d+).*?"
|
||
r"scaleBandDeclared\s+:=\s+Q16_16\.ofRatio\s+(\d+)\s+(\d+)",
|
||
re.DOTALL,
|
||
)
|
||
|
||
def extract_ncderived_chains(lean_paths: list[Path]) -> list[NcDerivedCheck]:
|
||
"""Extract ncDerived computation chains from fixture rows."""
|
||
results: list[NcDerivedCheck] = []
|
||
for path in lean_paths:
|
||
if not path.exists():
|
||
continue
|
||
text = path.read_text()
|
||
for match in FIXTURE_RE.finditer(text):
|
||
name = match.group(1)
|
||
n1, d1 = int(match.group(2)), int(match.group(3))
|
||
n2, d2 = int(match.group(4)), int(match.group(5))
|
||
r1 = Rational(n1, d1)
|
||
r2 = Rational(n2, d2)
|
||
product = r1 * r2
|
||
product_raw = floor(product * Q16_SCALE)
|
||
results.append(NcDerivedCheck(
|
||
fixture=name,
|
||
residual_risk=f"{n1}/{d1}",
|
||
scale_band=f"{n2}/{d2}",
|
||
product_exact=str(product),
|
||
lean_raw_num=product.p, # numerator of exact rational
|
||
lean_raw_den=product.q, # denominator
|
||
lean_raw=int(product_raw),
|
||
sympy_raw=int(product_raw),
|
||
match=True,
|
||
))
|
||
return results
|
||
|
||
|
||
# ── Extractor C: #eval witness verification ────────────────────────────────
|
||
|
||
EVAL_RE = re.compile(r"#eval\s+(.+?)\s*--\s*expect:\s*(.+)", re.MULTILINE)
|
||
|
||
@dataclass
|
||
class EvalWitness:
|
||
file: str = ""
|
||
line: int = 0
|
||
expression: str = ""
|
||
expected: str = ""
|
||
involves_q16: bool = False
|
||
|
||
|
||
def extract_eval_witnesses(lean_paths: list[Path]) -> list[EvalWitness]:
|
||
results: list[EvalWitness] = []
|
||
for path in lean_paths:
|
||
if not path.exists():
|
||
continue
|
||
text = path.read_text()
|
||
for match in EVAL_RE.finditer(text):
|
||
expr = match.group(1).strip()
|
||
expected = match.group(2).strip()
|
||
involves_q16 = "ncDerived" in expr or "ofRatio" in expr or "Q16_16" in expr
|
||
line_num = text[:match.start()].count("\n") + 1
|
||
results.append(EvalWitness(
|
||
file=str(path.relative_to(REPO_ROOT)),
|
||
line=line_num,
|
||
expression=expr,
|
||
expected=expected,
|
||
involves_q16=involves_q16,
|
||
))
|
||
return results
|
||
|
||
|
||
# ── Main verification ──────────────────────────────────────────────────────
|
||
|
||
def main():
|
||
parser = argparse.ArgumentParser(description="Layer 3: CAS/SMT Grounding")
|
||
parser.add_argument("--lean-dir", type=Path, default=REPO_ROOT / "formal",
|
||
help="Lean source directory (default: formal/)")
|
||
parser.add_argument("--receipt", type=Path,
|
||
default=REPO_ROOT / "extraction" / "cas_verification_receipt.json",
|
||
help="Output receipt path")
|
||
parser.add_argument("--verbose", action="store_true", help="Show per-check details")
|
||
args = parser.parse_args()
|
||
|
||
# Find all .lean files
|
||
lean_files = sorted(args.lean_dir.rglob("*.lean"))
|
||
# Filter to just RRC and FeasibleSet (not full mathlib)
|
||
lean_files = [f for f in lean_files if "Emits" not in str(f)
|
||
and ".lake" not in str(f)]
|
||
# Core files to check
|
||
core_paths = [
|
||
REPO_ROOT / "formal/SilverSight/RRC/Emit.lean",
|
||
REPO_ROOT / "formal/CoreFormalism/FixedPoint.lean",
|
||
]
|
||
lean_files = [p for p in core_paths if p.exists()]
|
||
|
||
print(f"[verify] Extracting Q16_16.ofRatio values...")
|
||
ratios = extract_ofratio_values(lean_files)
|
||
print(f" Found {len(ratios)} ofRatio values")
|
||
mismatches = [r for r in ratios if not r.match]
|
||
|
||
print(f"[verify] Extracting ncDerived computation chains...")
|
||
chains = extract_ncderived_chains(lean_files)
|
||
print(f" Found {len(chains)} ncDerived chains")
|
||
mismatches += [c for c in chains if not c.match]
|
||
|
||
print(f"[verify] Extracting #eval witnesses...")
|
||
witnesses = extract_eval_witnesses(lean_files)
|
||
print(f" Found {len(witnesses)} #eval witnesses")
|
||
q16_witnesses = [w for w in witnesses if w.involves_q16]
|
||
print(f" ({len(q16_witnesses)} involve Q16_16 arithmetic)")
|
||
|
||
# Build receipt
|
||
receipt = {
|
||
"schema": "cas_verification_receipt_v1",
|
||
"lean_dir": str(args.lean_dir),
|
||
"extraction": {
|
||
"ofratio_values_found": len(ratios),
|
||
"ncderived_chains_found": len(chains),
|
||
"eval_witnesses_found": len(witnesses),
|
||
},
|
||
"results": {
|
||
"ofratio_match": len(ratios) - len([r for r in ratios if not r.match]),
|
||
"ncderived_match": len(chains) - len([c for c in chains if not c.match]),
|
||
"all_match": len(mismatches) == 0,
|
||
},
|
||
"entries": {
|
||
"ofratio": [asdict(r) for r in ratios],
|
||
"ncderived": [asdict(c) for c in chains],
|
||
"witnesses": [asdict(w) for w in q16_witnesses],
|
||
},
|
||
"verdict": "PASS" if len(mismatches) == 0 else "FAIL",
|
||
}
|
||
|
||
args.receipt.parent.mkdir(parents=True, exist_ok=True)
|
||
args.receipt.write_text(json.dumps(receipt, indent=2))
|
||
|
||
if mismatches:
|
||
print(f"\n ❌ {len(mismatches)} mismatches found!")
|
||
for m in mismatches:
|
||
print(f" {m}")
|
||
sys.exit(1)
|
||
else:
|
||
print(f"\n ✅ All {len(ratios) + len(chains)} Q16_16 computations verified against SymPy")
|
||
print(f" Receipt: {args.receipt}")
|
||
sys.exit(0)
|
||
|
||
|
||
if __name__ == "__main__":
|
||
main()
|