mirror of
https://github.com/allaunthefox/BioSight.git
synced 2026-07-31 03:05:22 +00:00
allaun
295130c078
- Aligned layer naming and numbering (1 to 4) with the formal Lean specifications in SilverSight. - Implemented phi.silversight to verify rule ordering, N=8 necessity, and Lean compilation status. - Integrated SilverSight validation checks into equation_dna_encoder.py and rigour_pipeline.py. Build: 3307 jobs, 0 errors (lake build)
143 lines
4.5 KiB
Python
143 lines
4.5 KiB
Python
"""
|
|
phi.silversight — Import and integration layer for SilverSight formal verification
|
|
|
|
This module acts as the runtime bridge between the BioSight Python shims and the
|
|
formal Lean specifications in SilverSight (/home/allaun/SilverSight). It verifies
|
|
that all admissibility and layout decisions are formally backed by SilverSight.
|
|
"""
|
|
|
|
from __future__ import annotations
|
|
|
|
import os
|
|
import subprocess
|
|
import sys
|
|
from typing import Dict, List, Tuple
|
|
|
|
|
|
SILVERSIGHT_PATH = "/home/allaun/SilverSight"
|
|
|
|
|
|
def check_silversight_available() -> bool:
|
|
"""Check if the SilverSight repository is locally cloned and accessible."""
|
|
return os.path.isdir(SILVERSIGHT_PATH)
|
|
|
|
|
|
def verify_n8_necessity() -> Tuple[bool, str]:
|
|
"""Verify that the N=8 Necessity Theorem is present in SilverSight."""
|
|
lean_file = os.path.join(SILVERSIGHT_PATH, "formal/SilverSight/HachimojiN8.lean")
|
|
if not os.path.isfile(lean_file):
|
|
return False, f"HachimojiN8.lean not found at {lean_file}"
|
|
|
|
with open(lean_file, "r") as f:
|
|
content = f.read()
|
|
|
|
if "theorem n8_necessity" not in content:
|
|
return False, "HachimojiN8.lean is missing 'theorem n8_necessity'"
|
|
|
|
return True, "N=8 Necessity Theorem successfully verified in SilverSight"
|
|
|
|
|
|
def verify_consistency_rules() -> Tuple[bool, str]:
|
|
"""Verify that Python consistency rules align with SilverSight's ConsistencyRule."""
|
|
lean_file = os.path.join(SILVERSIGHT_PATH, "formal/SilverSight/PhiConsistency.lean")
|
|
if not os.path.isfile(lean_file):
|
|
return False, f"PhiConsistency.lean not found at {lean_file}"
|
|
|
|
with open(lean_file, "r") as f:
|
|
content = f.read()
|
|
|
|
# Python rule list
|
|
if not __package__:
|
|
from consistency import CONSISTENCY_RULES
|
|
else:
|
|
from .consistency import CONSISTENCY_RULES
|
|
|
|
# Lean constructor declaration snippet
|
|
# ConsistencyRule is defined with constructors in order:
|
|
# balanced_parens, valid_operator_order, valid_variable_name, no_empty_expression, single_expression, defined_reference
|
|
for rule in CONSISTENCY_RULES:
|
|
if rule not in content:
|
|
return False, f"Rule {rule!r} not found in SilverSight's ConsistencyRule definition"
|
|
|
|
return True, f"All {len(CONSISTENCY_RULES)} consistency rules successfully verified against SilverSight"
|
|
|
|
|
|
def run_lean_build() -> Tuple[bool, str]:
|
|
"""Run lake build on SilverSight to ensure formal proofs compile cleanly."""
|
|
try:
|
|
res = subprocess.run(
|
|
["lake", "build"],
|
|
cwd=SILVERSIGHT_PATH,
|
|
capture_output=True,
|
|
text=True,
|
|
timeout=15
|
|
)
|
|
if res.returncode != 0:
|
|
return False, f"lake build failed:\n{res.stderr}"
|
|
return True, "SilverSight Lean build compiles cleanly with zero errors"
|
|
except Exception as e:
|
|
return False, f"Failed to run lake build: {e}"
|
|
|
|
|
|
def verify_pipeline_receipt() -> Dict[str, bool]:
|
|
"""Perform full verification of the encoding pipeline against SilverSight specifications.
|
|
|
|
Returns a dictionary of check names and boolean results.
|
|
"""
|
|
results = {
|
|
"silversight_available": False,
|
|
"n8_necessity_theorem": False,
|
|
"consistency_rules_match": False,
|
|
"lean_compilation_passes": False,
|
|
}
|
|
|
|
if not check_silversight_available():
|
|
return results
|
|
|
|
results["silversight_available"] = True
|
|
|
|
ok, _ = verify_n8_necessity()
|
|
results["n8_necessity_theorem"] = ok
|
|
|
|
ok, _ = verify_consistency_rules()
|
|
results["consistency_rules_match"] = ok
|
|
|
|
ok, _ = run_lean_build()
|
|
results["lean_compilation_passes"] = ok
|
|
|
|
return results
|
|
|
|
|
|
if __name__ == "__main__":
|
|
print("Running SilverSight Verification Bridge...")
|
|
|
|
if not check_silversight_available():
|
|
print("FAIL: SilverSight repository not available at /home/allaun/SilverSight")
|
|
sys.exit(1)
|
|
|
|
print("✓ SilverSight repository available")
|
|
|
|
ok, msg = verify_n8_necessity()
|
|
if ok:
|
|
print(f"✓ {msg}")
|
|
else:
|
|
print(f"FAIL: {msg}")
|
|
sys.exit(1)
|
|
|
|
ok, msg = verify_consistency_rules()
|
|
if ok:
|
|
print(f"✓ {msg}")
|
|
else:
|
|
print(f"FAIL: {msg}")
|
|
sys.exit(1)
|
|
|
|
print("Building SilverSight Lean project (this may take a few seconds)...")
|
|
ok, msg = run_lean_build()
|
|
if ok:
|
|
print(f"✓ {msg}")
|
|
else:
|
|
print(f"FAIL: {msg}")
|
|
sys.exit(1)
|
|
|
|
print("\nAll SilverSight validation gates PASSED.")
|
|
sys.exit(0)
|