mirror of
https://github.com/allaunthefox/SilverSight.git
synced 2026-07-30 17:16:16 +00:00
allaun
fec200205e
Ports three Research Stack RRC gates into formal/SilverSight/RRC/ using the existing CoreFormalism braid and Q16_16 surfaces. Adds a Lean ↔ C ↔ Python Q16_16 roundtrip test: - c/q16_canonical.c: canonical saturating Q16_16 C library - exe/Q16_16Roundtrip.lean: Lake extern_lib linked executable - tests/test_q16_roundtrip.py: Python ↔ C harness (revived from quarantine) Updates lakefile.lean with q16-roundtrip executable and extern_lib q16_canonical. Build: lake build SilverSightRRC 3006 jobs, 0 errors; q16-roundtrip 5949 jobs, 0 errors
426 lines
14 KiB
Python
426 lines
14 KiB
Python
"""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())
|