diff --git a/python/equation_dna_encoder.py b/python/equation_dna_encoder.py index 53732c1..2b5aec9 100644 --- a/python/equation_dna_encoder.py +++ b/python/equation_dna_encoder.py @@ -82,6 +82,15 @@ if __name__ == "__main__": print(f"FAIL: SilverSight verification failed: {e}") fail += 1 + # 1c. Verified Test Units + try: + from phi.test_verified_units import run_verified_tests + if not run_verified_tests(): + fail += 1 + except Exception as e: + print(f"FAIL: Verified Test Units failed to run: {e}") + fail += 1 + # 2. encode_phi result = encode_phi("E(x) = x^2") if result is None: diff --git a/python/phi/fixtures.json b/python/phi/fixtures.json new file mode 100644 index 0000000..df7bb77 --- /dev/null +++ b/python/phi/fixtures.json @@ -0,0 +1,60 @@ +{ + "character_classification": [ + {"char": "θ", "class": 9}, + {"char": "π", "class": 9}, + {"char": "λ", "class": 9}, + {"char": "Δ", "class": 10}, + {"char": "→", "class": 10}, + {"char": "+", "class": 3}, + {"char": "*", "class": 3}, + {"char": "/", "class": 3}, + {"char": "x", "class": 1}, + {"char": "1", "class": 0} + ], + "consistency_checks": [ + { + "expr": "(x + 1", + "expected_dna": "TGGGTG", + "fail_rule": "balanced_parens" + }, + { + "expr": "x ++ 1", + "expected_dna": "GTGGGG", + "fail_rule": "valid_operator_order" + }, + { + "expr": "1x + 1", + "expected_dna": "GGGGTG", + "fail_rule": "valid_variable_name" + }, + { + "expr": " ", + "expected_dna": "GGGTTG", + "fail_rule": "no_empty_expression" + }, + { + "expr": "x = 1; y = 2", + "expected_dna": "GGGGTG", + "fail_rule": "single_expression" + }, + { + "expr": "longvarname + 1", + "expected_dna": "GGGGGT", + "fail_rule": "defined_reference" + } + ], + "fixed_point_slopes": { + "m_1_0": { + "input_scale": 65536, + "expected_slope_large": 158217, + "expected_slope_small": -27147, + "tolerance_lsb": 4 + }, + "m_0_0": { + "input_scale": 0, + "expected_slope_large": 65536, + "expected_slope_small": -65536, + "tolerance_lsb": 0 + } + } +} diff --git a/python/phi/test_verified_units.py b/python/phi/test_verified_units.py new file mode 100644 index 0000000..9d3c847 --- /dev/null +++ b/python/phi/test_verified_units.py @@ -0,0 +1,118 @@ +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)