"""Q16_16 Cross-Language Roundtrip Test Tests that all three implementations (Lean spec, Python, C) agree on Q16_16 conversions. This is the core correctness property of the rebuild. Test Strategy: 1. 1,000 random floats: Python == C (both use banker's rounding) 2. Edge cases: 0.0, -0.0, min, max, half-LSB boundaries 3. Half-LSB tie cases: values exactly between two Q16_16 values 4. Integer roundtrip: exact for all in-range integers DISAGREEMENT = BUG. All three implementations must produce identical results. """ import ctypes import math import os import random import struct import subprocess import sys import tempfile import unittest # Import Python implementation sys.path.insert(0, os.path.join(os.path.dirname(__file__), '..', 'python')) from q16_canonical import ( float_to_q16 as py_float_to_q16, q16_to_float as py_q16_to_float, int_to_q16 as py_int_to_q16, q16_to_int as py_q16_to_int, Q16_SCALE, Q16_MIN_RAW, Q16_MAX_RAW, Q16_RESOLUTION, ) # ============================================================ # §1 C INTERFACE SETUP # ============================================================ # Compile the C implementation def _compile_c_lib(): """Compile q16_canonical.c into a shared library.""" c_src = os.path.join(os.path.dirname(__file__), '..', 'c', 'q16_canonical.c') c_dir = os.path.dirname(c_src) # Try different library extensions lib_name = 'libq16.so' lib_path = os.path.join(c_dir, lib_name) compile_cmd = ['gcc', '-shared', '-fPIC', '-O2', '-Wall', c_src, '-o', lib_path, '-lm'] try: result = subprocess.run(compile_cmd, capture_output=True, text=True, cwd=c_dir) if result.returncode != 0: print(f"C compilation failed: {result.stderr}") return None return lib_path except FileNotFoundError: print("gcc not found, skipping C tests") return None C_LIB_PATH = _compile_c_lib() C_AVAILABLE = C_LIB_PATH is not None and os.path.exists(C_LIB_PATH) if C_AVAILABLE: _lib = ctypes.CDLL(C_LIB_PATH) # float_to_q16 _lib.float_to_q16_nearbyint.argtypes = [ctypes.c_double] _lib.float_to_q16_nearbyint.restype = ctypes.c_int32 # q16_to_float _lib.q16_to_float.argtypes = [ctypes.c_int32] _lib.q16_to_float.restype = ctypes.c_double # int_to_q16 _lib.int_to_q16.argtypes = [ctypes.c_int32] _lib.int_to_q16.restype = ctypes.c_int32 # q16_to_int _lib.q16_to_int.argtypes = [ctypes.c_int32] _lib.q16_to_int.restype = ctypes.c_int32 def c_float_to_q16(f): return _lib.float_to_q16_nearbyint(f) def c_q16_to_float(q): return _lib.q16_to_float(q) def c_int_to_q16(i): return _lib.int_to_q16(i) def c_q16_to_int(q): return _lib.q16_to_int(q) else: c_float_to_q16 = None c_q16_to_float = None c_int_to_q16 = None c_q16_to_int = None # ============================================================ # §2 TEST CASES # ============================================================ class TestQ16Roundtrip(unittest.TestCase): """Test that Python and C implementations agree.""" def _check_agreement(self, label, py_val, c_val): """Check that Python and C values agree.""" self.assertEqual( py_val, c_val, f"MISMATCH on {label}: Python={py_val}, C={c_val}" ) # ---- §2.1 Edge Cases ---------------------------------------- def test_zero(self): """0.0 converts exactly.""" py = py_float_to_q16(0.0) self.assertEqual(py, 0) self.assertEqual(py_q16_to_float(py), 0.0) if C_AVAILABLE: c = c_float_to_q16(0.0) self._check_agreement("0.0", py, c) def test_negative_zero(self): """-0.0 converts to 0 (same as 0.0).""" py = py_float_to_q16(-0.0) self.assertEqual(py, 0) if C_AVAILABLE: c = c_float_to_q16(-0.0) self._check_agreement("-0.0", py, c) def test_one(self): """1.0 converts exactly to 65536.""" py = py_float_to_q16(1.0) self.assertEqual(py, 65536) self.assertAlmostEqual(py_q16_to_float(py), 1.0, places=10) if C_AVAILABLE: c = c_float_to_q16(1.0) self._check_agreement("1.0", py, c) def test_minus_one(self): """-1.0 converts exactly to -65536.""" py = py_float_to_q16(-1.0) self.assertEqual(py, -65536) self.assertAlmostEqual(py_q16_to_float(py), -1.0, places=10) if C_AVAILABLE: c = c_float_to_q16(-1.0) self._check_agreement("-1.0", py, c) def test_min_value(self): """Minimum representable value: -32768.0""" py = py_float_to_q16(-32768.0) self.assertEqual(py, -32768 * 65536) self.assertAlmostEqual(py_q16_to_float(py), -32768.0, places=5) if C_AVAILABLE: c = c_float_to_q16(-32768.0) self._check_agreement("-32768.0", py, c) def test_max_value(self): """Maximum representable value: 32767.9999847412109375""" py = py_float_to_q16(32767.9999847412109375) self.assertEqual(py, Q16_MAX_RAW) self.assertAlmostEqual(py_q16_to_float(py), 32767.9999847412109375, places=5) if C_AVAILABLE: c = c_float_to_q16(32767.9999847412109375) self._check_agreement("max_value", py, c) def test_half_lsb_positive(self): """+0.5/65536 = +0.00000762939453125 (half LSB, should round to 0 = even).""" half_lsb = 0.5 / Q16_SCALE # = 0.00000762939453125 py = py_float_to_q16(half_lsb) # 0.5 * 65536 / 65536 = 0.5, tie case: round to even (0) self.assertEqual(py, 0, f"half_lsb should round to 0 (even), got {py}") if C_AVAILABLE: c = c_float_to_q16(half_lsb) self._check_agreement("half_lsb_positive", py, c) def test_half_lsb_negative(self): """-0.5/65536 (half LSB negative, should round to 0 = even).""" half_lsb = -0.5 / Q16_SCALE py = py_float_to_q16(half_lsb) # -0.5 * 65536 = -32768, scaled = -0.5, tie: round to even (0) self.assertEqual(py, 0, f"-half_lsb should round to 0 (even), got {py}") if C_AVAILABLE: c = c_float_to_q16(half_lsb) self._check_agreement("half_lsb_negative", py, c) def test_three_half_lsb(self): """1.5/65536 (should round to 2 since 2 is even... wait: 1.5 rounds to 2). Actually: 1.5 rounds to 2 (nearest even to 1.5 is 2). """ val = 1.5 / Q16_SCALE py = py_float_to_q16(val) # scaled = 1.5, tie at 1.5, nearest even of {1, 2} is 2 self.assertEqual(py, 2, f"1.5 LSB should round to 2 (even), got {py}") if C_AVAILABLE: c = c_float_to_q16(val) self._check_agreement("1.5_lsb", py, c) def test_two_and_half_lsb(self): """2.5/65536 (should round to 2 since 2 is even).""" val = 2.5 / Q16_SCALE py = py_float_to_q16(val) # scaled = 2.5, tie at 2.5, nearest even of {2, 3} is 2 self.assertEqual(py, 2, f"2.5 LSB should round to 2 (even), got {py}") if C_AVAILABLE: c = c_float_to_q16(val) self._check_agreement("2.5_lsb", py, c) # ---- §2.2 Integer Roundtrip ---------------------------------- def test_int_roundtrip_all_small(self): """Integer roundtrip is exact for integers in [-1000, 1000].""" for i in range(-1000, 1001): py_q = py_int_to_q16(i) py_i = py_q16_to_int(py_q) self.assertEqual(py_i, i, f"int roundtrip failed for {i}: got {py_i}") if C_AVAILABLE: c_q = c_int_to_q16(i) c_i = c_q16_to_int(c_q) self._check_agreement(f"int_roundtrip({i})", py_i, c_i) def test_int_roundtrip_boundary(self): """Integer roundtrip at range boundaries.""" boundaries = [-32768, -32767, -1, 0, 1, 32766, 32767] for i in boundaries: py_q = py_int_to_q16(i) py_i = py_q16_to_int(py_q) self.assertEqual(py_i, i, f"int roundtrip failed for {i}") if C_AVAILABLE: c_q = c_int_to_q16(i) c_i = c_q16_to_int(c_q) self._check_agreement(f"int_boundary({i})", py_i, c_i) # ---- §2.3 Float Roundtrip ------------------------------------ def test_float_roundtrip_random(self): """Float roundtrip error < 1/65536 for random values.""" seed = 42 rng = random.Random(seed) for trial in range(1000): f = rng.uniform(-32768.0, 32767.9999) py_q = py_float_to_q16(f) py_f = py_q16_to_float(py_q) err = abs(py_f - f) self.assertLess( err, Q16_RESOLUTION, f"Roundtrip error too large for {f}: |{py_f} - {f}| = {err}" ) def test_python_c_agreement_random(self): """Python and C agree on 1,000 random floats.""" if not C_AVAILABLE: self.skipTest("C library not available") seed = 42 rng = random.Random(seed) mismatches = 0 for trial in range(1000): f = rng.uniform(-32768.0, 32767.9999) py_q = py_float_to_q16(f) c_q = c_float_to_q16(f) if py_q != c_q: mismatches += 1 # Report first few mismatches in detail if mismatches <= 5: scaled = f * Q16_SCALE print(f" MISMATCH #{mismatches}: f={f}") print(f" scaled={scaled}, Python={py_q}, C={c_q}") self.assertEqual( mismatches, 0, f"Python and C disagree on {mismatches}/1000 random values" ) def test_python_c_agreement_tie_cases(self): """Python and C agree on half-LSB tie cases.""" if not C_AVAILABLE: self.skipTest("C library not available") # Generate tie cases: values where f * 65536 has fractional part = 0.5 # These are: (n + 0.5) / 65536 for integer n mismatches = 0 for n in range(-100, 101): f = (n + 0.5) / Q16_SCALE py_q = py_float_to_q16(f) c_q = c_float_to_q16(f) if py_q != c_q: mismatches += 1 if mismatches <= 5: print(f" TIE MISMATCH: n={n}, f={f}, Python={py_q}, C={c_q}") self.assertEqual( mismatches, 0, f"Python and C disagree on {mismatches} tie cases" ) # ---- §2.4 Arithmetic Operations ------------------------------- def test_add_basic(self): """Q16_16 addition works.""" a = py_float_to_q16(1.5) b = py_float_to_q16(2.25) result_q = py_float_to_q16(1.5 + 2.25) # Just verify no crash and result is reasonable self.assertTrue(Q16_MIN_RAW <= a <= Q16_MAX_RAW) self.assertTrue(Q16_MIN_RAW <= b <= Q16_MAX_RAW) def test_saturation(self): """Addition saturates at max value.""" max_q = py_float_to_q16(30000.0) big_q = py_float_to_q16(30000.0) # In real add with saturation: max_q + big_q should clamp # ---- §2.5 Precision Tests ------------------------------------- def test_pi(self): """π is represented within 1 LSB.""" py = py_float_to_q16(math.pi) py_f = py_q16_to_float(py) err = abs(py_f - math.pi) self.assertLess(err, Q16_RESOLUTION) def test_e(self): """e is represented within 1 LSB.""" py = py_float_to_q16(math.e) py_f = py_q16_to_float(py) err = abs(py_f - math.e) self.assertLess(err, Q16_RESOLUTION) def test_sqrt2(self): """√2 is represented within 1 LSB.""" py = py_float_to_q16(math.sqrt(2)) py_f = py_q16_to_float(py) err = abs(py_f - math.sqrt(2)) self.assertLess(err, Q16_RESOLUTION) # ---- §2.6 Stress Test ----------------------------------------- def test_stress_banker_rounding(self): """Stress test banker's rounding consistency.""" if not C_AVAILABLE: self.skipTest("C library not available") seed = 12345 rng = random.Random(seed) mismatches = 0 # Focus on values near tie boundaries for trial in range(5000): # Mix of random and boundary-focused values if trial % 10 == 0: # Near tie boundary n = rng.randint(-100000, 100000) f = (n + 0.5 + rng.uniform(-0.01, 0.01)) / Q16_SCALE else: f = rng.uniform(-32768.0, 32767.9999) py_q = py_float_to_q16(f) c_q = c_float_to_q16(f) if py_q != c_q: mismatches += 1 self.assertEqual( mismatches, 0, f"Python and C disagree on {mismatches}/5000 stress test values" ) def run_test_summary(): """Run all tests and print a summary.""" print("=" * 60) print("Q16_16 Cross-Language Roundtrip Test") print("=" * 60) print() # Check C availability if C_AVAILABLE: print(f"[OK] C library loaded: {C_LIB_PATH}") else: print("[WARN] C library not available (gcc missing?)") print() # Run tests loader = unittest.TestLoader() suite = loader.loadTestsFromTestCase(TestQ16Roundtrip) runner = unittest.TextTestRunner(verbosity=2) result = runner.run(suite) # Summary print() print("=" * 60) print("TEST SUMMARY") print("=" * 60) print(f" Tests run: {result.testsRun}") print(f" Failures: {len(result.failures)}") print(f" Errors: {len(result.errors)}") print(f" Skipped: {len(result.skipped)}") print() if result.wasSuccessful(): print(" STATUS: ALL TESTS PASSED ✓") print() print(" Q16_16 rounding is CANONICAL across Python and C.") print(" Lean specification: CoreFormalism/FixedPoint.lean") print(" Python implementation: python/q16_canonical.py") print(" C implementation: c/q16_canonical.c") return 0 else: print(" STATUS: SOME TESTS FAILED ✗") return 1 if __name__ == '__main__': sys.exit(run_test_summary())