BioSight/python/phi/test_verified_units.py
allaun e0d0f2f7fd feat(test): implement verified test units matching Lean oracle witnesses
Added fixtures.json and test_verified_units.py. Verifies character classification
classes, consistency rule maps under syntax errors, and Q16_16 parabola conjugate
slopes exact outputs (large: 158217, small: -27147) and tolerance bounds matching
Lean witnesses.

Build: 0 failures (python3 equation_dna_encoder.py --verify)
2026-06-27 23:20:23 -05:00

118 lines
4.1 KiB
Python

import os
import json
import sys
# Add package directory to path so we can import from phi
sys.path.insert(0, os.path.dirname(os.path.dirname(os.path.abspath(__file__))))
from phi.charclass import classify_char
from phi.consistency import check_consistency
# Helper functions for Q16_16 math in Python matching Lean's FixedPoint behavior
def q16_mul(a, b):
return (a * b) // 65536
def q16_div(a, b):
return (a * 65536) // b
def int_sqrt(n):
if n < 0:
raise ValueError("Square root of negative number")
if n == 0:
return 0
x = n
y = (x + 1) // 2
while y < x:
x = y
y = (x + n // x) // 2
return x
def q16_sqrt(q_raw):
if q_raw <= 0:
return 0
return int_sqrt(q_raw * 65536)
def parabola_conjugate_pair(m_raw):
m_sq = q16_mul(m_raw, m_raw)
sqrt_term = q16_sqrt(m_sq + 65536)
s1 = m_raw + sqrt_term
s2 = q16_div(-65536, s1)
return s1, s2
def run_verified_tests():
fixtures_path = os.path.join(os.path.dirname(__file__), "fixtures.json")
with open(fixtures_path, "r", encoding="utf-8") as f:
fixtures = json.load(f)
failures = 0
print("=== Running Verified Test Units ===")
# 1. Character Classification Verification
print("Running Character Classification Tests...")
for item in fixtures["character_classification"]:
char = item["char"]
expected = item["class"]
actual = classify_char(char)
if actual == expected:
print(f" ✓ Character '{char}': expected class {expected}, got {actual}")
else:
print(f" ✗ Character '{char}': expected class {expected}, got {actual}")
failures += 1
# 2. Consistency Checks Verification
print("Running Consistency Checks Tests...")
for item in fixtures["consistency_checks"]:
expr = item["expr"]
expected_dna = item["expected_dna"]
fail_rule = item["fail_rule"]
# Runs the rules in consistency.py and encodes as bases
from phi.consistency import check_consistency, CONSISTENCY_RULES
results_dict = check_consistency(expr)
actual_dna = "".join(["G" if results_dict[rule] else "T" for rule in CONSISTENCY_RULES])
if actual_dna == expected_dna:
print(f" ✓ Expr '{expr}': expected DNA '{expected_dna}' (fail rule: {fail_rule}), got '{actual_dna}'")
else:
print(f" ✗ Expr '{expr}': expected DNA '{expected_dna}', got '{actual_dna}'")
failures += 1
# 3. Fixed-Point Arithmetic & Slopes Verification
print("Running Fixed-Point Slope Tests...")
for name, item in fixtures["fixed_point_slopes"].items():
input_scale = item["input_scale"]
expected_large = item["expected_slope_large"]
expected_small = item["expected_slope_small"]
tolerance_lsb = item["tolerance_lsb"]
actual_large, actual_small = parabola_conjugate_pair(input_scale)
# Verify large slope match
large_match = (actual_large == expected_large)
# Verify small slope match
small_match = (actual_small == expected_small)
# Verify orthogonality within tolerance
prod = q16_mul(actual_large, actual_small)
target = -65536
diff = abs(prod - target)
tol_match = (diff <= tolerance_lsb)
if large_match and small_match and tol_match:
print(f" ✓ slopes for {name}: expected ({expected_large}, {expected_small}), got ({actual_large}, {actual_small}) within {tolerance_lsb} LSB tolerance")
else:
print(f" ✗ slopes for {name}: expected ({expected_large}, {expected_small}) with tol {tolerance_lsb}, got ({actual_large}, {actual_small}) diff {diff}")
failures += 1
print("===================================")
if failures == 0:
print("ALL VERIFIED TEST UNITS PASSED")
return True
else:
print(f"{failures} VERIFIED TEST UNIT(S) FAILED")
return False
if __name__ == "__main__":
success = run_verified_tests()
sys.exit(0 if success else 1)