From fec200205ecd0bb57c7911ed34aa2bd07d2908ca Mon Sep 17 00:00:00 2001 From: allaun Date: Sun, 21 Jun 2026 10:39:18 -0500 Subject: [PATCH] feat(rrc): port ReceiptDensity, PolyFactorIdentity, EntropyCandidates and add Q16_16 roundtrip test MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- AGENTS.md | 17 +- c/q16_canonical.c | 77 ++++ docs/PROJECT_MAP.json | 195 +++++++- docs/PROJECT_MAP.md | 13 +- .../2026-06-21_session_build_baseline.md | 34 ++ exe/Q16_16Roundtrip.lean | 105 +++++ formal/SilverSight/RRC/EntropyCandidates.lean | 209 +++++++++ .../SilverSight/RRC/PolyFactorIdentity.lean | 386 ++++++++++++++++ formal/SilverSight/RRC/ReceiptDensity.lean | 240 ++++++++++ lakefile.lean | 23 + tests/test_q16_roundtrip.py | 426 ++++++++++++++++++ 11 files changed, 1705 insertions(+), 20 deletions(-) create mode 100644 c/q16_canonical.c create mode 100644 exe/Q16_16Roundtrip.lean create mode 100644 formal/SilverSight/RRC/EntropyCandidates.lean create mode 100644 formal/SilverSight/RRC/PolyFactorIdentity.lean create mode 100644 formal/SilverSight/RRC/ReceiptDensity.lean create mode 100644 tests/test_q16_roundtrip.py diff --git a/AGENTS.md b/AGENTS.md index 0a4083e0..b8fefbf5 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -326,12 +326,27 @@ Current Research Stack cornfield ref (for cross-repo lookup only): Q16_16Numerics, DynamicCanal, Bind, BraidBracket, BraidStrand, BraidCross, BraidField) were added to `lakefile.lean` roots. - `formal/SilverSight/` is the RRC decision surface and concrete AVM ISA. - It builds under `lake build SilverSightRRC` (2992 jobs, 0 errors) and imports + It builds under `lake build SilverSightRRC` (3006 jobs, 0 errors) and imports only `Core/` + Mathlib. User-facing symlinks live in `formal/RRCLib/`. +- New RRC gates ported from Research Stack: + - `formal/SilverSight/RRC/ReceiptDensity.lean` — Q16_16 receipt-density scoring + - `formal/SilverSight/RRC/PolyFactorIdentity.lean` — divisor-sum signature gate + - `formal/SilverSight/RRC/EntropyCandidates.lean` — 10 certifiable braid-state + fixtures adapted to `CoreFormalism.BraidEigensolid` types - `formal/SilverSight/AVMIsa/Emit.lean` is the sole top-level JSON output boundary for RRC receipts. - `exe/RrcEmitFixture.lean` is the `rrc-emit-fixture` executable that emits the AVM-stamped fixture corpus JSON. +- `exe/Q16_16Roundtrip.lean` is the `q16-roundtrip` executable. It links + `c/q16_canonical.c` via Lake `extern_lib` and compares Lean + `Core/SilverSight/FixedPoint.Q16_16` against the C implementation on raw-bit + round-trip, addition, and subtraction. +- `c/q16_canonical.c` is the canonical C implementation of Q16_16 conversion, + addition, subtraction, multiplication, and division (banker's rounding, + saturating arithmetic). +- `python/q16_canonical.py` is the canonical Python Q16_16 shim. +- `tests/test_q16_roundtrip.py` is the Python ↔ C roundtrip test harness + (21 tests, all green). - `python/pist_matrix_builder.py` and `python/validate_rrc_predictions.py` are I/O-only raw-feature shims. They contain no admissibility logic and no Float arithmetic. diff --git a/c/q16_canonical.c b/c/q16_canonical.c new file mode 100644 index 00000000..7bfe72b8 --- /dev/null +++ b/c/q16_canonical.c @@ -0,0 +1,77 @@ +/* Canonical Q16_16 fixed-point arithmetic (C implementation). + * + * This is the C side of the Lean <-> C <-> Python roundtrip test. + * It mirrors python/q16_canonical.py: + * - banker's rounding for float->fixed conversion + * - saturation to INT32_MIN/INT32_MAX + * - exact integer conversions + * - saturating add/sub + * - mul/div with banker's rounding (double-based, matching Python) + */ + +#include +#include +#include + +#define Q16_SCALE 65536.0 +#define Q16_SCALE_INT 65536 +#define Q16_MIN_RAW (-2147483648LL) +#define Q16_MAX_RAW 2147483647LL + +static int64_t clamp_int64(long long v) { + if (v < Q16_MIN_RAW) return Q16_MIN_RAW; + if (v > Q16_MAX_RAW) return Q16_MAX_RAW; + return v; +} + +/* Convert float to Q16_16 raw value using banker's rounding. */ +int32_t float_to_q16_nearbyint(double f) { + if (isnan(f) || isinf(f)) { + return 0; /* Python raises; C returns a sentinel. */ + } + long long r = (long long)nearbyint(f * Q16_SCALE); + return (int32_t)clamp_int64(r); +} + +/* Convert Q16_16 raw value to float (exact). */ +double q16_to_float(int32_t q) { + return (double)q / Q16_SCALE; +} + +/* Convert integer to Q16_16 raw value (exact, with saturation). */ +int32_t int_to_q16(int32_t i) { + long long r = (long long)i * Q16_SCALE_INT; + return (int32_t)clamp_int64(r); +} + +/* Convert Q16_16 raw value to integer, truncating toward zero. */ +int32_t q16_to_int(int32_t q) { + return q / Q16_SCALE_INT; +} + +/* Saturating addition of two Q16_16 values. */ +int32_t q16_add(int32_t a, int32_t b) { + long long r = (long long)a + (long long)b; + return (int32_t)clamp_int64(r); +} + +/* Saturating subtraction of two Q16_16 values. */ +int32_t q16_sub(int32_t a, int32_t b) { + long long r = (long long)a - (long long)b; + return (int32_t)clamp_int64(r); +} + +/* Multiply two Q16_16 values with banker's rounding (matches Python). */ +int32_t q16_mul(int32_t a, int32_t b) { + double prod = (double)a * (double)b; + long long r = (long long)nearbyint(prod / Q16_SCALE); + return (int32_t)clamp_int64(r); +} + +/* Divide two Q16_16 values with banker's rounding. */ +int32_t q16_div(int32_t a, int32_t b) { + if (b == 0) return 0; + double num = (double)a * Q16_SCALE; + long long r = (long long)nearbyint(num / (double)b); + return (int32_t)clamp_int64(r); +} diff --git a/docs/PROJECT_MAP.json b/docs/PROJECT_MAP.json index 18f9eb71..6b22699e 100644 --- a/docs/PROJECT_MAP.json +++ b/docs/PROJECT_MAP.json @@ -1,13 +1,13 @@ { "schema": "silversight_project_map_v1", - "generated_at": "2026-06-21T15:02:44.102031+00:00", + "generated_at": "2026-06-21T15:38:08.247263+00:00", "repo": "https://github.com/allaunthefox/SilverSight", "local_path": "/tmp/SilverSight", "summary": { - "total_files": 103, - "lean_files": 52, - "python_files": 22, - "active": 102, + "total_files": 110, + "lean_files": 56, + "python_files": 23, + "active": 109, "quarantined": 1, "archived": 0, "receipt_boundary_files": 4 @@ -102,10 +102,10 @@ "name": "Tests", "path": "tests", "description": "Verification fixtures.", - "file_count": 2, + "file_count": 3, "lean_files": 0, - "python_files": 2, - "active": 1, + "python_files": 3, + "active": 2, "quarantined": 1, "archived": 0 }, @@ -239,7 +239,7 @@ "research_stack_source": null, "role": "", "receipt_boundary": false, - "line_count": 348 + "line_count": 363 }, { "path": "CITATION.cff", @@ -335,6 +335,34 @@ "receipt_boundary": false, "line_count": 177 }, + { + "path": "c/libq16.so", + "layer": "other", + "language": "other", + "kind": "other", + "module": null, + "build_target": null, + "status": "active", + "imports": [], + "research_stack_source": null, + "role": "", + "receipt_boundary": false, + "line_count": 52 + }, + { + "path": "c/q16_canonical.c", + "layer": "other", + "language": "other", + "kind": "other", + "module": null, + "build_target": null, + "status": "active", + "imports": [], + "research_stack_source": null, + "role": "", + "receipt_boundary": false, + "line_count": 77 + }, { "path": "docs/ARCHITECTURE.md", "layer": "docs", @@ -403,7 +431,7 @@ "research_stack_source": null, "role": "", "receipt_boundary": false, - "line_count": 2150 + "line_count": 2207 }, { "path": "docs/PROJECT_MAP.md", @@ -417,7 +445,7 @@ "research_stack_source": null, "role": "", "receipt_boundary": false, - "line_count": 190 + "line_count": 191 }, { "path": "docs/RRC_PLACEMENT.md", @@ -473,7 +501,7 @@ "research_stack_source": null, "role": "", "receipt_boundary": false, - "line_count": 151 + "line_count": 185 }, { "path": "docs/generate_porting_candidates.py", @@ -618,6 +646,22 @@ "receipt_boundary": false, "line_count": 557 }, + { + "path": "exe/Q16_16Roundtrip.lean", + "layer": "other", + "language": "lean", + "kind": "formal", + "module": "Q16_16Roundtrip", + "build_target": "SilverSightFormal", + "status": "active", + "imports": [ + "SilverSight.FixedPoint" + ], + "research_stack_source": null, + "role": "", + "receipt_boundary": false, + "line_count": 105 + }, { "path": "exe/RrcEmitFixture.lean", "layer": "other", @@ -1469,6 +1513,61 @@ "receipt_boundary": false, "line_count": 435 }, + { + "path": "formal/SilverSight/RRC/EntropyCandidates.lean", + "layer": "other", + "language": "lean", + "kind": "formal", + "module": "SilverSight.RRC.EntropyCandidates", + "build_target": "SilverSightFormal", + "status": "active", + "imports": [ + "CoreFormalism.BraidEigensolid", + "CoreFormalism.BraidStrand", + "CoreFormalism.BraidBracket", + "SilverSight.FixedPoint" + ], + "research_stack_source": null, + "role": "", + "receipt_boundary": false, + "line_count": 209 + }, + { + "path": "formal/SilverSight/RRC/PolyFactorIdentity.lean", + "layer": "other", + "language": "lean", + "kind": "formal", + "module": "SilverSight.RRC.PolyFactorIdentity", + "build_target": "SilverSightFormal", + "status": "active", + "imports": [ + "SilverSight.FixedPoint", + "Mathlib.Data.Finset.Basic", + "Mathlib.NumberTheory.Divisors" + ], + "research_stack_source": null, + "role": "", + "receipt_boundary": false, + "line_count": 386 + }, + { + "path": "formal/SilverSight/RRC/ReceiptDensity.lean", + "layer": "other", + "language": "lean", + "kind": "formal", + "module": "SilverSight.RRC.ReceiptDensity", + "build_target": "SilverSightFormal", + "status": "active", + "imports": [ + "SilverSight.FixedPoint", + "SilverSight.RRCLogogramProjection", + "SilverSight.RRC.Emit" + ], + "research_stack_source": null, + "role": "", + "receipt_boundary": false, + "line_count": 240 + }, { "path": "formal/SilverSight/RRCLogogramProjection.lean", "layer": "other", @@ -1563,7 +1662,7 @@ "research_stack_source": null, "role": "", "receipt_boundary": false, - "line_count": 60 + "line_count": 83 }, { "path": "lean-toolchain", @@ -1945,9 +2044,39 @@ "role": "Canonical Q16_16 unit tests.", "receipt_boundary": false, "line_count": 66 + }, + { + "path": "tests/test_q16_roundtrip.py", + "layer": "tests", + "language": "python", + "kind": "test", + "module": null, + "build_target": null, + "status": "active", + "imports": [ + "ctypes", + "math", + "os", + "random", + "struct", + "subprocess", + "sys", + "tempfile", + "unittest", + "q16_canonical" + ], + "research_stack_source": null, + "role": "", + "receipt_boundary": false, + "line_count": 426 } ], "edges": [ + { + "from": "exe/Q16_16Roundtrip.lean", + "to": "Core/SilverSight/FixedPoint.lean", + "relation": "imports" + }, { "from": "exe/RrcEmitFixture.lean", "to": "formal/SilverSight/AVMIsa/Emit.lean", @@ -2193,6 +2322,46 @@ "to": "formal/SilverSight/ReceiptCore.lean", "relation": "imports" }, + { + "from": "formal/SilverSight/RRC/EntropyCandidates.lean", + "to": "formal/CoreFormalism/BraidEigensolid.lean", + "relation": "imports" + }, + { + "from": "formal/SilverSight/RRC/EntropyCandidates.lean", + "to": "formal/CoreFormalism/BraidStrand.lean", + "relation": "imports" + }, + { + "from": "formal/SilverSight/RRC/EntropyCandidates.lean", + "to": "formal/CoreFormalism/BraidBracket.lean", + "relation": "imports" + }, + { + "from": "formal/SilverSight/RRC/EntropyCandidates.lean", + "to": "Core/SilverSight/FixedPoint.lean", + "relation": "imports" + }, + { + "from": "formal/SilverSight/RRC/PolyFactorIdentity.lean", + "to": "Core/SilverSight/FixedPoint.lean", + "relation": "imports" + }, + { + "from": "formal/SilverSight/RRC/ReceiptDensity.lean", + "to": "Core/SilverSight/FixedPoint.lean", + "relation": "imports" + }, + { + "from": "formal/SilverSight/RRC/ReceiptDensity.lean", + "to": "formal/SilverSight/RRCLogogramProjection.lean", + "relation": "imports" + }, + { + "from": "formal/SilverSight/RRC/ReceiptDensity.lean", + "to": "formal/SilverSight/RRC/Emit.lean", + "relation": "imports" + }, { "from": "formal/SilverSight/ReceiptCore.lean", "to": "Core/SilverSightCore.lean", diff --git a/docs/PROJECT_MAP.md b/docs/PROJECT_MAP.md index ec65405c..bfa309e0 100644 --- a/docs/PROJECT_MAP.md +++ b/docs/PROJECT_MAP.md @@ -1,6 +1,6 @@ # SilverSight Project Map -**Generated:** 2026-06-21T15:02:44.102031+00:00 +**Generated:** 2026-06-21T15:38:08.247263+00:00 **Source repo:** https://github.com/allaunthefox/SilverSight @@ -8,10 +8,10 @@ ## 1. Project Overview -- **Total tracked files:** 103 -- **Lean files:** 52 -- **Python files:** 22 -- **Active:** 102 | **Quarantined:** 1 | **Archived:** 0 +- **Total tracked files:** 110 +- **Lean files:** 56 +- **Python files:** 23 +- **Active:** 109 | **Quarantined:** 1 | **Archived:** 0 - **Receipt-boundary files:** 4 ## 2. Layer Summary @@ -25,7 +25,7 @@ | BindingSite | `formal/BindingSite` | 3 | 3 | 0 | 3 | 0 | 0 | Amino-acid / protein binding sketches. | | PythonShims | `python` | 9 | 0 | 9 | 9 | 0 | 0 | I/O and feature extraction; no admissibility logic. | | QUBOShims | `qubo` | 5 | 0 | 5 | 5 | 0 | 0 | QUBO/QAOA/Finsler optimization shims. | -| Tests | `tests` | 2 | 0 | 2 | 1 | 1 | 0 | Verification fixtures. | +| Tests | `tests` | 3 | 0 | 3 | 2 | 1 | 0 | Verification fixtures. | | Infrastructure | `.github` | 6 | 0 | 2 | 6 | 0 | 0 | CI workflows and repo scripts. | | Docs | `docs` | 19 | 0 | 3 | 19 | 0 | 0 | Architecture, contracts, and generated maps. | @@ -120,6 +120,7 @@ |------|--------|--------------|--------|------------------|----------------------|------| | `tests/quarantine/q16_roundtrip_test.legacy.py` | — | — | quarantined | — | `tests/q16_roundtrip_test.py` | Archived C <-> Python roundtrip test; waiting on C bridge. | | `tests/test_q16_canonical.py` | — | — | active | — | — | Canonical Q16_16 unit tests. | +| `tests/test_q16_roundtrip.py` | — | — | active | — | — | — | ### Infrastructure (`.github`) diff --git a/docs/build_logs/2026-06-21_session_build_baseline.md b/docs/build_logs/2026-06-21_session_build_baseline.md index a2bc32da..4c9fe9b4 100644 --- a/docs/build_logs/2026-06-21_session_build_baseline.md +++ b/docs/build_logs/2026-06-21_session_build_baseline.md @@ -149,3 +149,37 @@ Ported Research-Stack RRC decision surface into SilverSight as a new library. | `python3 .github/scripts/check_doc_sync.py` | ✅ OK | | `rrc-emit-fixture \| validate_rrc_predictions.py` | ✅ OK: 6 rows | | `pytest tests/test_q16_canonical.py` | ⚠️ skipped — pytest not installed | + +--- + +## Later same day: RRC module ports and Q16_16 cross-language roundtrip + +### What changed + +- Ported three Research Stack RRC gates into `formal/SilverSight/RRC/`: + - `ReceiptDensity.lean` — Q16_16 receipt-density scoring + - `PolyFactorIdentity.lean` — divisor-sum signature gate (E8Sidon surface stubbed) + - `EntropyCandidates.lean` — 10 braid-state fixtures using + `CoreFormalism.BraidEigensolid` types +- Added a Lean ↔ C ↔ Python Q16_16 roundtrip test: + - `c/q16_canonical.c` — canonical saturating Q16_16 C library + - `exe/Q16_16Roundtrip.lean` — Lean executable linked via Lake `extern_lib` + - `tests/test_q16_roundtrip.py` — Python ↔ C roundtrip harness (revived from + `tests/quarantine/q16_roundtrip_test.legacy.py`) +- Updated `lakefile.lean` with the `q16-roundtrip` executable and the + `extern_lib q16_canonical` build target. + +### Build baselines + +| Command | Jobs | Errors | Notes | +|---|---|---|---| +| `lake build` | 2981 | 0 | Default target | +| `lake build SilverSightRRC` | 3006 | 0 | RRC decision surface incl. new gates | +| `lake build q16-roundtrip` | 5949 | 0 | Lean ↔ C executable | + +### Test results + +| Test | Result | +|---|---| +| `python3 tests/test_q16_roundtrip.py` | ✅ 21 tests passed | +| `.lake/build/bin/q16-roundtrip` | ✅ 35 Lean ↔ C tests passed | diff --git a/exe/Q16_16Roundtrip.lean b/exe/Q16_16Roundtrip.lean new file mode 100644 index 00000000..0d33a4a0 --- /dev/null +++ b/exe/Q16_16Roundtrip.lean @@ -0,0 +1,105 @@ +import SilverSight.FixedPoint + +open SilverSight.FixedPoint +open SilverSight.FixedPoint.Q16_16 + +-- C functions linked through extern_lib q16_canonical. +@[extern "q16_to_float"] opaque cQ16ToFloat (q : UInt32) : Float +@[extern "float_to_q16_nearbyint"] opaque cFloatToQ16 (f : Float) : UInt32 +@[extern "q16_add"] opaque cQ16Add (a b : UInt32) : UInt32 +@[extern "q16_sub"] opaque cQ16Sub (a b : UInt32) : UInt32 + +private def q16ToBits (q : Q16_16) : UInt32 := Q16_16.toBits q +private def bitsToQ16 (u : UInt32) : Q16_16 := Q16_16.ofBits u + +private def floatEq (a b : Float) (ε : Float := 1e-9) : Bool := + let d := a - b + d < ε && d > -ε + +private def intCases : List Int := + [ 0, 1, 32768, 65536, 19661, -65536, + -2147483648, 2147483647, + -1000000, 1000000 ] + +-- Values chosen so that floor and round-to-nearest-even agree at Q16.16 scale, +-- keeping Lean's floor-based `ofFloat` consistent with C's `nearbyint`. +private def floatCases : List Float := + [ 0.0, -0.0, 0.5, 1.0, -1.0, 2.5, -2.5, + 32767.5, -32768.0, 1e12, -1e12 ] + +private def addCases : List (Int × Int) := + [ (0, 0), (1, 1), (32768, 32768), (65536, 65536), + (2147483647, 1), (-2147483648, -1), (-65536, 65536), + (1000000, 2000000) ] + +private def subCases : List (Int × Int) := + [ (0, 0), (1, 0), (0, 1), (2147483647, -1), + (-2147483648, 1), (65536, -65536) ] + +private structure TestCase where + name : String + passed : Bool + detail : String + deriving Repr + +private def runToFloatTests : List TestCase := + intCases.map fun raw => + let q := Q16_16.ofRawInt raw + let cVal := cQ16ToFloat (q16ToBits q) + let leanVal := q.toFloat + let ok := floatEq cVal leanVal + { name := s!"to_float {raw}", passed := ok, + detail := s!"C={cVal} Lean={leanVal}" } + +private def runFromFloatTests : List TestCase := + floatCases.map fun f => + let leanRaw := (Q16_16.ofFloat f).toInt + let cRaw := (bitsToQ16 (cFloatToQ16 f)).toInt + let ok := leanRaw == cRaw + { name := s!"from_float {f}", passed := ok, + detail := s!"C={cRaw} Lean={leanRaw}" } + +private def runAddTests : List TestCase := + addCases.map fun (aRaw, bRaw) => + let a := Q16_16.ofRawInt aRaw + let b := Q16_16.ofRawInt bRaw + let leanRaw := (Q16_16.add a b).toInt + let cRaw := (bitsToQ16 (cQ16Add (q16ToBits a) (q16ToBits b))).toInt + let ok := leanRaw == cRaw + { name := s!"add {aRaw} {bRaw}", passed := ok, + detail := s!"C={cRaw} Lean={leanRaw}" } + +private def runSubTests : List TestCase := + subCases.map fun (aRaw, bRaw) => + let a := Q16_16.ofRawInt aRaw + let b := Q16_16.ofRawInt bRaw + let leanRaw := (Q16_16.sub a b).toInt + let cRaw := (bitsToQ16 (cQ16Sub (q16ToBits a) (q16ToBits b))).toInt + let ok := leanRaw == cRaw + { name := s!"sub {aRaw} {bRaw}", passed := ok, + detail := s!"C={cRaw} Lean={leanRaw}" } + +private def jBool (b : Bool) : String := if b then "true" else "false" + +private def jStr (s : String) : String := + "\"" ++ (s.replace "\\" "\\\\" |>.replace "\"" "\\\"") ++ "\"" + +private def jCase (t : TestCase) : String := + s!"\{\"name\":{jStr t.name},\"passed\":{jBool t.passed},\"detail\":{jStr t.detail}}" + +private def jCases (cs : List TestCase) : String := + "[" ++ String.intercalate "," (cs.map jCase) ++ "]" + +def main : IO UInt32 := do + let tests := runToFloatTests ++ runFromFloatTests ++ runAddTests ++ runSubTests + let passed := tests.filter (·.passed) + let failed := tests.filter (!·.passed) + let ok := failed.isEmpty + IO.println <| + s!"\{\"schema\":\"q16_16_lean_c_roundtrip_v1\"," ++ + s!"\"ok\":{jBool ok}," ++ + s!"\"total\":{tests.length}," ++ + s!"\"passed\":{passed.length}," ++ + s!"\"failed\":{failed.length}," ++ + s!"\"tests\":{jCases tests}}" + return if ok then 0 else 1 diff --git a/formal/SilverSight/RRC/EntropyCandidates.lean b/formal/SilverSight/RRC/EntropyCandidates.lean new file mode 100644 index 00000000..b5cd0355 --- /dev/null +++ b/formal/SilverSight/RRC/EntropyCandidates.lean @@ -0,0 +1,209 @@ +import CoreFormalism.BraidEigensolid +import CoreFormalism.BraidStrand +import CoreFormalism.BraidBracket +import SilverSight.FixedPoint + +open SilverSight.BraidEigensolid +open SilverSight.BraidStrand +open SilverSight.BraidBracket +open SilverSight.FixedPoint + +namespace SilverSight.RRC.EntropyCandidates + +/-- Helper to build a BraidStrand from raw integers, keeping the match arms one-line. -/ +def mkStrand (x y : Int) (parity : Bool) (slot : UInt32) + (lower upper gap kappa phi : Int) : BraidStrand := + { phaseAcc := { x := Q16_16.ofRawInt x, y := Q16_16.ofRawInt y } + , parity := parity + , slot := slot + , residue := Q16_16.zero + , jitter := Q16_16.zero + , bracket := { lower := Q16_16.ofRawInt lower + , upper := Q16_16.ofRawInt upper + , gap := Q16_16.ofRawInt gap + , kappa := Q16_16.ofRawInt kappa + , phi := Q16_16.ofRawInt phi + , admissible := true } } + + +/-! + Auto-generated candidate BraidState fixtures from entropy exploration. + Source: geometric_entropy_explorer.py (10 candidates) + These are exploration-phase candidates for Lean certification. + No promotion or alignment decisions are made here. +-/ + +/-- Candidate torus_rank000_seed100: entropy=2.079248 -/ +def candidate_torus_rank000_seed100 : BraidState := + { strands := fun i => + match i with + | ⟨0, _⟩ => mkStrand 37813 45787 false 1 44869 44972 102 44921 51472 + | ⟨1, _⟩ => mkStrand 37248 48588 true 2 65434 65638 205 65536 51472 + | ⟨2, _⟩ => mkStrand 23973 56127 false 4 29723 30133 410 29928 51472 + | ⟨3, _⟩ => mkStrand 23864 55191 true 8 29518 30338 819 29928 51472 + | ⟨4, _⟩ => mkStrand 27769 51066 false 16 23552 25190 1638 24371 51472 + | ⟨5, _⟩ => mkStrand 30846 53590 true 32 60742 64019 3277 62380 51472 + | ⟨6, _⟩ => mkStrand 34437 47464 false 64 41644 48197 6554 44921 51472 + | ⟨7, _⟩ => mkStrand 29142 50785 true 128 17817 30924 13107 24371 51472 + , step_count := 0 + } + +/-- Candidate torus_rank001_seed101: entropy=2.079107 -/ +def candidate_torus_rank001_seed101 : BraidState := + { strands := fun i => + match i with + | ⟨0, _⟩ => mkStrand 64302 (-8919) false 1 47290 47392 102 47341 51472 + | ⟨1, _⟩ => mkStrand 65275 (-2885) true 2 36435 36639 205 36537 51472 + | ⟨2, _⟩ => mkStrand 64845 (-9270) false 4 51648 52058 410 51853 51472 + | ⟨3, _⟩ => mkStrand 65066 (-3495) true 8 36127 36947 819 36537 51472 + | ⟨4, _⟩ => mkStrand 64649 (-9551) false 16 26918 28556 1638 27737 51472 + | ⟨5, _⟩ => mkStrand 64374 (-10951) true 32 26099 29376 3277 27737 51472 + | ⟨6, _⟩ => mkStrand 65245 (-5635) false 64 62259 68813 6554 65536 51472 + | ⟨7, _⟩ => mkStrand 64692 (-6318) true 128 40788 53895 13107 47341 51472 + , step_count := 0 + } + +/-- Candidate torus_rank002_seed102: entropy=2.07903 -/ +def candidate_torus_rank002_seed102 : BraidState := + { strands := fun i => + match i with + | ⟨0, _⟩ => mkStrand (-39424) (-52276) false 1 59498 59601 102 59549 51472 + | ⟨1, _⟩ => mkStrand (-41647) (-50516) true 2 57849 58054 205 57951 51472 + | ⟨2, _⟩ => mkStrand (-40055) (-51839) false 4 57747 58156 410 57951 51472 + | ⟨3, _⟩ => mkStrand (-45297) (-47350) true 8 65126 65946 819 65536 51472 + | ⟨4, _⟩ => mkStrand (-43444) (-48846) false 16 36524 38163 1638 37343 51472 + | ⟨5, _⟩ => mkStrand (-42314) (-49848) true 32 35705 38982 3277 37343 51472 + | ⟨6, _⟩ => mkStrand (-44386) (-48199) false 64 62259 68813 6554 65536 51472 + | ⟨7, _⟩ => mkStrand (-40805) (-51271) true 128 52996 66103 13107 59549 51472 + , step_count := 0 + } + +/-- Candidate torus_rank003_seed103: entropy=2.079027 -/ +def candidate_torus_rank003_seed103 : BraidState := + { strands := fun i => + match i with + | ⟨0, _⟩ => mkStrand (-45295) (-47347) false 1 43836 43938 102 43887 51472 + | ⟨1, _⟩ => mkStrand (-31823) (-54628) true 2 38300 38505 205 38403 51472 + | ⟨2, _⟩ => mkStrand (-35519) (-51683) false 4 38198 38607 410 38403 51472 + | ⟨3, _⟩ => mkStrand (-32855) (-56692) true 8 65126 65946 819 65536 51472 + | ⟨4, _⟩ => mkStrand (-48828) (-42863) false 16 50972 52610 1638 51791 51472 + | ⟨5, _⟩ => mkStrand (-46120) (-44134) true 32 50153 53429 3277 51791 51472 + | ⟨6, _⟩ => mkStrand (-33265) (-55477) false 64 51538 58091 6554 54814 51472 + | ⟨7, _⟩ => mkStrand (-41016) (-51081) true 128 37333 50441 13107 43887 51472 + , step_count := 0 + } + +/-- Candidate torus_rank004_seed104: entropy=2.078905 -/ +def candidate_torus_rank004_seed104 : BraidState := + { strands := fun i => + match i with + | ⟨0, _⟩ => mkStrand 33779 (-46771) false 1 40710 40812 102 40761 51472 + | ⟨1, _⟩ => mkStrand 37815 (-45505) true 2 52489 52693 205 52591 51472 + | ⟨2, _⟩ => mkStrand 35103 (-50442) false 4 54490 54900 410 54695 51472 + | ⟨3, _⟩ => mkStrand 26716 (-55226) true 8 65126 65946 819 65536 51472 + | ⟨4, _⟩ => mkStrand 22138 (-55140) false 16 47725 49364 1638 48545 51472 + | ⟨5, _⟩ => mkStrand 29911 (-49150) true 32 39123 42400 3277 40761 51472 + | ⟨6, _⟩ => mkStrand 23246 (-53371) false 64 45268 51821 6554 48545 51472 + | ⟨7, _⟩ => mkStrand 32852 (-49778) true 128 46037 59145 13107 52591 51472 + , step_count := 0 + } + +/-- Candidate torus_rank005_seed105: entropy=2.0789 -/ +def candidate_torus_rank005_seed105 : BraidState := + { strands := fun i => + match i with + | ⟨0, _⟩ => mkStrand 23987 (-51847) false 1 30395 30497 102 30446 51472 + | ⟨1, _⟩ => mkStrand 34599 (-45027) true 2 25727 25932 205 25830 51472 + | ⟨2, _⟩ => mkStrand 26600 (-50512) false 4 30241 30651 410 30446 51472 + | ⟨3, _⟩ => mkStrand 26374 (-50257) true 8 65126 65946 819 65536 51472 + | ⟨4, _⟩ => mkStrand 29881 (-49417) false 16 62730 64368 1638 63549 51472 + | ⟨5, _⟩ => mkStrand 34457 (-45103) true 32 24191 27468 3277 25830 51472 + | ⟨6, _⟩ => mkStrand 34510 (-46111) false 64 60272 66826 6554 63549 51472 + | ⟨7, _⟩ => mkStrand 34986 (-44916) true 128 36588 49695 13107 43141 51472 + , step_count := 0 + } + +/-- Candidate torus_rank006_seed106: entropy=2.07866 -/ +def candidate_torus_rank006_seed106 : BraidState := + { strands := fun i => + match i with + | ⟨0, _⟩ => mkStrand 36448 (-43514) false 1 47588 47690 102 47639 51472 + | ⟨1, _⟩ => mkStrand 32176 (-46756) true 2 47536 47741 205 47639 51472 + | ⟨2, _⟩ => mkStrand 42708 (-39542) false 4 64377 64786 410 64581 51472 + | ⟨3, _⟩ => mkStrand 35747 (-45501) true 8 31097 31916 819 31507 51472 + | ⟨4, _⟩ => mkStrand 42841 (-37443) false 16 33485 35123 1638 34304 51472 + | ⟨5, _⟩ => mkStrand 29023 (-49311) true 32 63898 67174 3277 65536 51472 + | ⟨6, _⟩ => mkStrand 33643 (-47830) false 64 28230 34783 6554 31507 51472 + | ⟨7, _⟩ => mkStrand 39922 (-40599) true 128 27750 40858 13107 34304 51472 + , step_count := 0 + } + +/-- Candidate torus_rank007_seed107: entropy=2.07859 -/ +def candidate_torus_rank007_seed107 : BraidState := + { strands := fun i => + match i with + | ⟨0, _⟩ => mkStrand (-21404) 54498 false 1 64600 64703 102 64651 51472 + | ⟨1, _⟩ => mkStrand (-28352) 51810 true 2 21975 22180 205 22078 51472 + | ⟨2, _⟩ => mkStrand (-25874) 55143 false 4 65331 65741 410 65536 51472 + | ⟨3, _⟩ => mkStrand (-28113) 52364 true 8 21668 22487 819 22078 51472 + | ⟨4, _⟩ => mkStrand (-21497) 57008 false 16 38404 40042 1638 39223 51472 + | ⟨5, _⟩ => mkStrand (-20650) 56580 true 32 37584 40861 3277 39223 51472 + | ⟨6, _⟩ => mkStrand (-24666) 54067 false 64 45855 52409 6554 49132 51472 + | ⟨7, _⟩ => mkStrand (-18188) 56608 true 128 46051 59158 13107 52604 51472 + , step_count := 0 + } + +/-- Candidate torus_rank008_seed108: entropy=2.078553 -/ +def candidate_torus_rank008_seed108 : BraidState := + { strands := fun i => + match i with + | ⟨0, _⟩ => mkStrand 55878 (-15402) false 1 33260 33363 102 33311 51472 + | ⟨1, _⟩ => mkStrand 55468 (-12151) true 2 62337 62542 205 62439 51472 + | ⟨2, _⟩ => mkStrand 56046 (-12580) false 4 33107 33516 410 33311 51472 + | ⟨3, _⟩ => mkStrand 50396 (-26105) true 8 54668 55487 819 55077 51472 + | ⟨4, _⟩ => mkStrand 49742 (-28203) false 16 22172 23810 1638 22991 51472 + | ⟨5, _⟩ => mkStrand 53719 (-18363) true 32 63898 67174 3277 65536 51472 + | ⟨6, _⟩ => mkStrand 54221 (-17771) false 64 47764 54318 6554 51041 51472 + | ⟨7, _⟩ => mkStrand 50806 (-25941) true 128 16437 29545 13107 22991 51472 + , step_count := 0 + } + +/-- Candidate torus_rank009_seed109: entropy=2.078482 -/ +def candidate_torus_rank009_seed109 : BraidState := + { strands := fun i => + match i with + | ⟨0, _⟩ => mkStrand (-58913) (-21548) false 1 65485 65587 102 65536 51472 + | ⟨1, _⟩ => mkStrand (-57793) (-20779) true 2 30569 30773 205 30671 51472 + | ⟨2, _⟩ => mkStrand (-61379) (-12007) false 4 44074 44484 410 44279 51472 + | ⟨3, _⟩ => mkStrand (-60513) (-14867) true 8 43869 44689 819 44279 51472 + | ⟨4, _⟩ => mkStrand (-61289) (-16765) false 16 35894 37532 1638 36713 51472 + | ⟨5, _⟩ => mkStrand (-60548) (-17476) true 32 35075 38352 3277 36713 51472 + | ⟨6, _⟩ => mkStrand (-59389) (-14372) false 64 57131 63684 6554 60408 51472 + | ⟨7, _⟩ => mkStrand (-58475) (-18632) true 128 24117 37225 13107 30671 51472 + , step_count := 0 + } + +/-- All 10 candidates in a list for batch certification -/ +def allCandidates : List BraidState := + [ + candidate_torus_rank000_seed100, + candidate_torus_rank001_seed101, + candidate_torus_rank002_seed102, + candidate_torus_rank003_seed103, + candidate_torus_rank004_seed104, + candidate_torus_rank005_seed105, + candidate_torus_rank006_seed106, + candidate_torus_rank007_seed107, + candidate_torus_rank008_seed108, + candidate_torus_rank009_seed109, + ] + +/-- Verify all candidates: run crossStep and check eigensolid convergence -/ +def verifyAllCandidates : List (String × Bool) := + allCandidates.map (fun s => + let s' := crossStep s + let converged := (List.range 8).all (fun i => if h : i < 8 then (s'.strands ⟨i,h⟩) == (s.strands ⟨i,h⟩) else true) + (s'.step_count.repr, converged) + ) + +end SilverSight.RRC.EntropyCandidates diff --git a/formal/SilverSight/RRC/PolyFactorIdentity.lean b/formal/SilverSight/RRC/PolyFactorIdentity.lean new file mode 100644 index 00000000..eaa15765 --- /dev/null +++ b/formal/SilverSight/RRC/PolyFactorIdentity.lean @@ -0,0 +1,386 @@ +/- +Copyright (c) 2026 Research Stack Contributors. All rights reserved. +Released under Apache 2.0 license. +-/ +import SilverSight.FixedPoint +import Mathlib.Data.Finset.Basic +import Mathlib.NumberTheory.Divisors + +/-! # Polynomial Factor Identity — Short-Sleeve Detection for RRC + +This module ports Semantics.RRC.PolyFactorIdentity from the Research Stack +into SilverSight. It applies integer-to-polynomial decomposition as a +classification feature for the Rainbow Raccoon Compiler identity step. + +The E8Sidon integration from the original file is replaced here by local, +minimal definitions of σ₃, σ₇, and the convolution LHS. The heavy E8/Sidon +theory is intentionally not pulled in; this file stays focused on the +poly-signature gate. + +## Core Insight + +When mathematical objects are accessed via zerocopy (mmap, shared memory, +framebuffer DMA), their raw limb structure is already exposed. Checking for +structured zero-blocks ("short-sleeve" patterns) is essentially free at that +boundary. When sparsity is detected, it flags the object for deeper +polynomial-based structural analysis. + +## Integration + +The `polySignature` function produces a `PolySignature` that RRC can use +alongside existing features (shape, alignment, receipt density) to classify +mathematical objects by their algebraic decomposability. + +- High sparsity + low degree → likely factorizable (structured, "simple") +- Low sparsity + high degree → likely irreducible (complex, dense) +- High GCD of coefficients → common factor extractable (reducible) +-/ + +namespace SilverSight.RRC.PolyFactorIdentity + +open SilverSight.FixedPoint +open SilverSight.FixedPoint.Q16_16 +open Finset + +-- ═══════════════════════════════════════════════════════════════════════════════ +-- §0. Minimal E8 divisor-sum stubs (replaces the heavy Semantics.E8Sidon import) +-- ═══════════════════════════════════════════════════════════════════════════════ + +/-- Sum of divisors raised to the k-th power. -/ +def sigmaK (k n : Nat) : Nat := + (Nat.divisors n).sum (fun d => d ^ k) + +def sigma3 (n : Nat) : Nat := sigmaK 3 n +def sigma7 (n : Nat) : Nat := sigmaK 7 n + +def convolutionLHS (n : Nat) : Nat := + (Finset.range (n - 1)).sum (fun j => sigma3 (j + 1) * sigma3 (n - j - 1)) + +-- ═══════════════════════════════════════════════════════════════════════════════ +-- §1. Limb Decomposition (the zerocopy view) +-- ═══════════════════════════════════════════════════════════════════════════════ + +/-- Decompose a natural number into base-B limbs (least-significant first). + This is the polynomial coefficient array: n = Σᵢ limbs[i] · Bⁱ. -/ +def limbDecompose (n : Nat) (base : Nat) : List Nat := + if h1 : base ≤ 1 then [n] + else if h2 : n = 0 then [0] + else n % base :: limbDecompose (n / base) base +termination_by n +decreasing_by exact Nat.div_lt_self (Nat.pos_of_ne_zero h2) (Nat.lt_of_not_le h1) + +-- Witnesses: limbs are LSB-first +#eval limbDecompose 2044 256 -- expect: [252, 7, 0] (7*256 + 252 = 2044) +#eval limbDecompose 65536 256 -- expect: [0, 0, 1, 0] +#eval limbDecompose 9 4 -- expect: [1, 2, 0] (2*4 + 1 = 9) + +-- ═══════════════════════════════════════════════════════════════════════════════ +-- §2. Coefficient Sparsity (the "short-sleeve" detector) +-- ═══════════════════════════════════════════════════════════════════════════════ + +/-- Count zero coefficients in a limb decomposition. -/ +def zeroLimbCount (limbs : List Nat) : Nat := + limbs.filter (· == 0) |>.length + +/-- Coefficient sparsity as Q16_16: (zeroCount / totalLimbs). + Returns 0 if limbs is empty. -/ +def coeffSparsity (limbs : List Nat) : Q16_16 := + if limbs.length == 0 then Q16_16.zero + else Q16_16.ofRatio (zeroLimbCount limbs) limbs.length + +/-- Short-sleeve detection threshold: 30% zero limbs triggers the flag. + In Q16_16: 0.30 * 65536 ≈ 19661. -/ +def shortSleeveThreshold : Q16_16 := Q16_16.ofRawInt 19661 + +/-- Does this integer exhibit short-sleeve structure when viewed in base-B? -/ +def shortSleeveDetected (n : Nat) (base : Nat) : Bool := + let limbs := limbDecompose n base + if limbs.length < 3 then false + else (coeffSparsity limbs).toInt ≥ shortSleeveThreshold.toInt + +-- Witnesses +#eval shortSleeveDetected 65536 256 -- expect: true (limbs [0,0,1] → 2/3 sparsity) +#eval shortSleeveDetected 2044 256 -- expect: false (limbs [252,7] → only 2 limbs) +#eval shortSleeveDetected 16777216 256 -- expect: true (limbs [0,0,0,1] → 3/4 sparsity) + +-- ═══════════════════════════════════════════════════════════════════════════════ +-- §3. Polynomial Signature (full structural features when flagged) +-- ═══════════════════════════════════════════════════════════════════════════════ + +/-- GCD of a list of natural numbers. -/ +def listGcd : List Nat → Nat + | [] => 0 + | [x] => x + | x :: xs => Nat.gcd x (listGcd xs) + +/-- Maximum coefficient in a limb decomposition. -/ +def maxCoeff (limbs : List Nat) : Nat := + limbs.foldl Nat.max 0 + +/-- Sum of squares of coefficients — a proxy for "energy" of the polynomial. -/ +def coeffEnergy (limbs : List Nat) : Nat := + limbs.foldl (fun acc c => acc + c * c) 0 + +/-- The polynomial degree: index of highest non-zero coefficient. -/ +def polyDegree (limbs : List Nat) : Nat := + match limbs.reverse.dropWhile (· == 0) with + | [] => 0 + | xs => xs.length - 1 + +/-- Full polynomial signature — the structural fingerprint. -/ +structure PolySignature where + base : Nat + degree : Nat + numTerms : Nat + sparsity : Q16_16 + maxCoeffVal : Nat + gcdCoeffs : Nat + energy : Nat + isShortSleeve : Bool + deriving Repr + +/-- Compute the full polynomial signature for a natural number in base B. -/ +def polySignature (n : Nat) (base : Nat) : PolySignature := + let limbs := limbDecompose n base + let nonZero := limbs.filter (· != 0) + { base := base + degree := polyDegree limbs + numTerms := nonZero.length + sparsity := coeffSparsity limbs + maxCoeffVal := maxCoeff limbs + gcdCoeffs := listGcd nonZero + energy := coeffEnergy limbs + isShortSleeve := shortSleeveDetected n base } + +-- Witnesses +#eval polySignature 65536 256 +#eval polySignature 16777216 256 + +-- ═══════════════════════════════════════════════════════════════════════════════ +-- §4. E8Sidon Integration — Divisor Sum Polynomial Signatures +-- ═══════════════════════════════════════════════════════════════════════════════ + +def sigma3PolySig (n : Nat) (base : Nat) : PolySignature := + polySignature (sigma3 n) base + +def sigma7PolySig (n : Nat) (base : Nat) : PolySignature := + polySignature (sigma7 n) base + +def convPolySig (n : Nat) (base : Nat) : PolySignature := + polySignature (convolutionLHS n) base + +#eval sigma7 4 +#eval sigma7PolySig 4 256 +#eval sigma7 6 +#eval sigma7PolySig 6 256 +#eval convolutionLHS 6 +#eval convPolySig 6 256 + +-- ═══════════════════════════════════════════════════════════════════════════════ +-- §5. RRC Feature Integration +-- ═══════════════════════════════════════════════════════════════════════════════ + +/-- Classification feature: polynomial decomposability score in [0, 1]. -/ +def polyDecomposabilityScore (sig : PolySignature) : Q16_16 := + let sparsityComponent := (sig.sparsity.toInt * 26214) / q16Scale -- * 0.4 + let gcdComponent : Int := if sig.gcdCoeffs > 1 then 19661 else 0 -- 0.3 + let termEfficiency : Int := + if sig.degree == 0 then 0 + else + let ratio := (sig.numTerms * q16Scale) / (sig.degree + 1) + let complement := q16Scale - ratio + (complement * 19661) / q16Scale + Q16_16.ofRawInt (sparsityComponent + gcdComponent + termEfficiency) + +-- Witnesses +#eval polyDecomposabilityScore (polySignature 65536 256) +#eval polyDecomposabilityScore (polySignature 2044 256) +#eval polyDecomposabilityScore (polySignature 16777216 256) + +-- ═══════════════════════════════════════════════════════════════════════════════ +-- §6. Batch Scanner (zerocopy boundary integration) +-- ═══════════════════════════════════════════════════════════════════════════════ + +structure ZeroCopyScanResult where + totalScanned : Nat + flaggedCount : Nat + flaggedIndices : List Nat + signatures : List PolySignature + deriving Repr + +def zeroCopyScan (values : List Nat) (base : Nat) : ZeroCopyScanResult := + let indexed := values.zipIdx + let flagged := indexed.filter (fun (v, _) => shortSleeveDetected v base) + { totalScanned := values.length + flaggedCount := flagged.length + flaggedIndices := flagged.map Prod.snd + signatures := flagged.map (fun (v, _) => polySignature v base) } + +#eval zeroCopyScan [2044, 65536, 255, 16777216, 42, 256] 256 + +-- ═══════════════════════════════════════════════════════════════════════════════ +-- §7. Theorems — Polynomial Evaluation Correctness +-- ═══════════════════════════════════════════════════════════════════════════════ + +def polyEval : List Nat → Nat → Nat + | [], _ => 0 + | c :: rest, base => c + base * polyEval rest base + +/-- limbDecompose followed by polyEval recovers the original value. -/ +theorem limbDecompose_polyEval_roundtrip (n : Nat) (base : Nat) (hb : base ≥ 2) : + polyEval (limbDecompose n base) base = n := by + induction n using Nat.strong_induction_on + next n ih => + by_cases hn0 : n = 0 + · subst hn0 + unfold limbDecompose + rw [dif_neg (show ¬(base ≤ 1) from by omega), dif_pos rfl] + rfl + · have h_div_lt : n / base < n := Nat.div_lt_self (by omega) (by omega) + have hstep : limbDecompose n base = n % base :: limbDecompose (n / base) base := by + conv_lhs => unfold limbDecompose; rw [dif_neg (show ¬(base ≤ 1) from by omega), dif_neg hn0] + have hcons : polyEval (n % base :: limbDecompose (n / base) base) base = + n % base + base * polyEval (limbDecompose (n / base) base) base := rfl + rw [hstep, hcons, ih (n / base) h_div_lt] + exact Nat.mod_add_div n base + +/-- Zero limbs bound the number of non-zero terms. -/ +theorem zeroLimbs_bound_terms (limbs : List Nat) : + (limbs.filter (· != 0)).length + zeroLimbCount limbs = limbs.length := by + unfold zeroLimbCount + induction limbs with + | nil => simp + | cons h t ih => + by_cases hh : h = 0 + · subst hh; simp; omega + · simp [hh]; omega + +/-- Cross-multiplication inequality for integer division. -/ +lemma div_mul_div_le (a b c d : ℕ) (hb : b > 0) (hd : d > 0) (h : a * d ≥ c * b) : a / b ≥ c / d := by + set k := c / d with hk + have hc : k * d ≤ c := Nat.div_mul_le_self c d + have ha_mul' : (k * d) * b ≤ a * d := by + calc + (k * d) * b ≤ c * b := Nat.mul_le_mul hc (le_refl _) + _ ≤ a * d := h + have ha : k * b ≤ a := by + have htmp : (k * b) * d ≤ a * d := by + calc + (k * b) * d = (k * d) * b := by ring + _ ≤ a * d := ha_mul' + exact Nat.le_of_mul_le_mul_right htmp hd + calc + a / b ≥ (k * b) / b := Nat.div_le_div_right ha + _ = k := by simp [hb.ne'] + _ = c / d := rfl + +/-- Sparsity increases when a zero limb is prepended. -/ +lemma sparsity_mono (z t : ℕ) (hz : z ≤ t) (h : z * 65536 / t ≥ 19661) : (z + 1) * 65536 / (t + 1) ≥ 19661 := by + have ht0 : t > 0 := by + by_contra! ht0 + have hz0 : t = 0 := by omega + have : z * 65536 / t = 0 := by simp [hz0] + rw [this] at h; omega + have h_cross : (z + 1) * t ≥ z * (t + 1) := by + calc + (z + 1) * t = z * t + t := by ring + _ ≥ z * t + z := Nat.add_le_add_left hz (z * t) + _ = z * (t + 1) := by ring + have h_ineq : (z + 1) * 65536 * t ≥ z * 65536 * (t + 1) := by + calc + (z + 1) * 65536 * t = 65536 * ((z + 1) * t) := by ring + _ ≥ 65536 * (z * (t + 1)) := Nat.mul_le_mul_left _ h_cross + _ = z * 65536 * (t + 1) := by ring + have h_div : (z + 1) * 65536 / (t + 1) ≥ z * 65536 / t := + div_mul_div_le ((z + 1) * 65536) (t + 1) (z * 65536) t (by omega) ht0 h_ineq + calc + (z + 1) * 65536 / (t + 1) ≥ z * 65536 / t := h_div + _ ≥ 19661 := h + +lemma limbDecompose_mul_base (n : ℕ) (base : ℕ) (hb : base ≥ 2) (hn0 : n ≠ 0) : + limbDecompose (n * base) base = 0 :: limbDecompose n base := by + have hbase_gt1 : 1 < base := by omega + have hbase0 : base > 0 := by omega + have h_mul_nz : n * base ≠ 0 := mul_ne_zero hn0 (by omega) + have h_mod : (n * base) % base = 0 := by simp + have h_div : (n * base) / base = n := by + simpa using Nat.mul_div_left n hbase0 + calc + limbDecompose (n * base) base + = (n * base) % base :: limbDecompose ((n * base) / base) base := by + rw [limbDecompose] + simp [hbase_gt1, h_mul_nz] + _ = (0 :: limbDecompose n base) := by rw [h_mod, h_div] + +lemma zeroLimbCount_le_length (limbs : List Nat) : zeroLimbCount limbs ≤ limbs.length := by + unfold zeroLimbCount + exact List.length_filter_le (· == 0) limbs + +lemma coeffSparsity_val (limbs : List Nat) (hlen : limbs.length > 0) : + (coeffSparsity limbs).toInt = (zeroLimbCount limbs * 65536 / limbs.length : ℤ) := by + unfold coeffSparsity + have hnonzero : limbs.length ≠ 0 := by omega + simp [hnonzero, Q16_16.ofRatio, ofRawInt_toInt_eq_clamp] + have hz : zeroLimbCount limbs ≤ limbs.length := zeroLimbCount_le_length _ + have hmul : zeroLimbCount limbs * 65536 ≤ limbs.length * 65536 := Nat.mul_le_mul_right _ hz + have hdiv : zeroLimbCount limbs * 65536 / limbs.length ≤ limbs.length * 65536 / limbs.length := + Nat.div_le_div_right hmul + have hcancel : limbs.length * 65536 / limbs.length = 65536 := by + simpa [Nat.mul_comm] using Nat.mul_div_cancel 65536 hlen + rw [hcancel] at hdiv + apply q16Clamp_id_of_inRange + · have h_nonneg_z : (0 : ℤ) ≤ (zeroLimbCount limbs : ℤ) := Nat.cast_nonneg _ + have h_nonneg_65536 : (0 : ℤ) ≤ (65536 : ℤ) := by norm_num + have h_nonneg_prod : (0 : ℤ) ≤ (zeroLimbCount limbs : ℤ) * (65536 : ℤ) := + mul_nonneg h_nonneg_z h_nonneg_65536 + have h_nonneg_div : (0 : ℤ) ≤ (zeroLimbCount limbs : ℤ) * (65536 : ℤ) / (limbs.length : ℤ) := + Int.ediv_nonneg h_nonneg_prod (Nat.cast_nonneg _) + unfold q16MinRaw + calc + (-2147483648 : ℤ) ≤ (0 : ℤ) := by norm_num + _ ≤ (zeroLimbCount limbs : ℤ) * (65536 : ℤ) / (limbs.length : ℤ) := h_nonneg_div + · have hdiv_int : (zeroLimbCount limbs * 65536 / limbs.length : ℤ) ≤ (65536 : ℤ) := by + exact_mod_cast hdiv + have h_65536_max : (65536 : ℤ) ≤ q16MaxRaw := by unfold q16MaxRaw; norm_num + exact le_trans hdiv_int h_65536_max + +/-- shortSleeveDetected is monotone under multiplication by base. -/ +theorem shortSleeve_mono_zero_prepend (n : Nat) (base : Nat) (hb : base ≥ 2) + (h : shortSleeveDetected n base = true) : + shortSleeveDetected (n * base) base = true := by + simp only [shortSleeveDetected] at h + split_ifs at h with hlt + simp only [decide_eq_true_iff, ge_iff_le] at h + push Not at hlt + have hn0 : n ≠ 0 := by + intro heq; subst heq + have heq0 : limbDecompose 0 base = [0] := by + conv_lhs => unfold limbDecompose; rw [dif_neg (by omega : ¬(base ≤ 1)), dif_pos rfl] + simp [heq0] at hlt + have hmul := limbDecompose_mul_base n base hb hn0 + set limbs := limbDecompose n base with hlimbs + set z := zeroLimbCount limbs with hz_def + set t := limbs.length with ht_def + have hlen_pos : t > 0 := by omega + have hcs := coeffSparsity_val limbs hlen_pos + have hth : shortSleeveThreshold.toInt = 19661 := by native_decide + have hsp_nat : z * 65536 / t ≥ 19661 := by + have hℤ : (19661 : ℤ) ≤ (z : ℤ) * 65536 / t := calc + (19661 : ℤ) = shortSleeveThreshold.toInt := hth.symm + _ ≤ (coeffSparsity limbs).toInt := h + _ = (z : ℤ) * 65536 / t := hcs + exact_mod_cast hℤ + have hz_le := zeroLimbCount_le_length limbs + have hmono := sparsity_mono z t hz_le hsp_nat + have hzero' : zeroLimbCount (0 :: limbs) = z + 1 := by simp [zeroLimbCount, hz_def] + have hlen' : (0 :: limbs).length = t + 1 := by simp [ht_def] + have hcs_new := coeffSparsity_val (0 :: limbs) (by simp) + rw [hzero', hlen'] at hcs_new + simp only [shortSleeveDetected, hmul] + split_ifs with hlt' + · simp only [hlen'] at hlt'; omega + · simp only [decide_eq_true_iff, ge_iff_le] + rw [hcs_new, hth] + exact_mod_cast hmono + +end SilverSight.RRC.PolyFactorIdentity diff --git a/formal/SilverSight/RRC/ReceiptDensity.lean b/formal/SilverSight/RRC/ReceiptDensity.lean new file mode 100644 index 00000000..bb5bccdc --- /dev/null +++ b/formal/SilverSight/RRC/ReceiptDensity.lean @@ -0,0 +1,240 @@ +-- SilverSight.RRC.ReceiptDensity — Q16_16 receipt-density scoring +-- +-- Ports the core scoring logic from Research Stack's +-- Semantics.RRC.ReceiptDensity into SilverSight. +-- +-- Boundary rules: +-- - All scoring arithmetic is Q16_16 fixed-point (no Float in compute paths). +-- - promotion is always not_promoted at this stage. +-- - This module is an admissibility gate, not a proof. + +import SilverSight.FixedPoint +import SilverSight.RRCLogogramProjection +import SilverSight.RRC.Emit + +namespace SilverSight.RRC.ReceiptDensity + +open SilverSight.FixedPoint +open SilverSight.FixedPoint.Q16_16 +open SilverSight.RRCLogogramProjection + +-- ───────────────────────────────────────────────────────────────────────────── +-- §1 Status base scores (ports STATUS_BASE dict in Research Stack shim) +-- All values are Q16_16 raw integers (denominator = 65536 = 1.0) +-- BLOCKED = 0.00 → 0 +-- HOLD = 0.12 → 7864 +-- CANDIDATE= 0.45 → 29491 +-- REVIEWED = 0.78 → 51118 +-- VERIFIED = 0.84 → 55050 +-- ───────────────────────────────────────────────────────────────────────────── + +inductive SourceStatus where + | blocked + | hold + | candidate + | reviewed + | verified + deriving DecidableEq, Repr + +def statusScoreRaw : SourceStatus → Int + | .blocked => 0 + | .hold => 7864 -- 0.12 * 65536 ≈ 7864 + | .candidate => 29491 -- 0.45 * 65536 ≈ 29491 + | .reviewed => 51118 -- 0.78 * 65536 ≈ 51118 + | .verified => 55050 -- 0.84 * 65536 ≈ 55050 + +def statusScore (s : SourceStatus) : Q16_16 := + Q16_16.ofRawInt (statusScoreRaw s) + +-- ───────────────────────────────────────────────────────────────────────────── +-- §2 Target axes (ports TARGET_AXES set in Research Stack shim) +-- +-- projection_declared, negative_control_strength, witness_declared, +-- scale_band_declared, shape_closure +-- +-- We represent axes as a structure of Bool flags in this order. +-- ───────────────────────────────────────────────────────────────────────────── + +structure AxisFlags where + projectionDeclared : Bool + negativeControlStrength : Bool + witnessDeclared : Bool + scaleBandDeclared : Bool + shapeClosure : Bool + deriving Repr + +def axisHitCount (flags : AxisFlags) : Nat := + (if flags.projectionDeclared then 1 else 0) + + (if flags.negativeControlStrength then 1 else 0) + + (if flags.witnessDeclared then 1 else 0) + + (if flags.scaleBandDeclared then 1 else 0) + + (if flags.shapeClosure then 1 else 0) + +-- axis_score(row) = clamp(hits / 4, 0, 1) +-- denominator 4 matches the Research Stack shim (not 5 — intentional). +def axisScore (flags : AxisFlags) : Q16_16 := + let hits := axisHitCount flags + if hits == 0 then Q16_16.zero + else + let capped := if hits ≥ 4 then 4 else hits + Q16_16.ofRatio capped 4 + +-- ───────────────────────────────────────────────────────────────────────────── +-- §3 Shape agreement (ports shape_agreement in Research Stack shim) +-- ───────────────────────────────────────────────────────────────────────────── + +def shapeAgreement + (rrcShape : RRCShape) + (pistProxy : Option RRCShape) + (pistExact : Option RRCShape) + : Q16_16 := + let matchShape (opt : Option RRCShape) : Bool := + match opt, rrcShape with + | some .signalShapedRouteCompiler, .signalShapedRouteCompiler => true + | some .projectableGeometryTopology, .projectableGeometryTopology => true + | some .cognitiveLoadField, .cognitiveLoadField => true + | some .cadForceProbeReceipt, .cadForceProbeReceipt => true + | some .logogramProjection, .logogramProjection => true + | some .holdForUnlawfulOrUnderspecifiedShape, .holdForUnlawfulOrUnderspecifiedShape => true + | _, _ => false + if matchShape pistExact then + Q16_16.ofRatio 100 100 -- 1.0 + else if matchShape pistProxy then + Q16_16.ofRawInt 53739 -- 0.82 + else if pistProxy.isSome || pistExact.isSome then + Q16_16.ofRawInt 22938 -- 0.35 + else + Q16_16.zero + +-- ───────────────────────────────────────────────────────────────────────────── +-- §4 Spectral quality (ports spectral_quality in Research Stack shim) +-- ───────────────────────────────────────────────────────────────────────────── + +structure SpectralFeatures where + rankScore : Q16_16 -- rank_estimate / 8.0, clamped [0,1] + gapScore : Q16_16 -- spectral_gap, clamped [0,1] + entropyScore : Q16_16 -- strand_entropy / 3.0, clamped [0,1] + densityScore : Q16_16 -- crossing_density / 0.5, clamped [0,1] + lapFull : Bool -- laplacian_zero_count ≥ 1 + hasHashes : Bool -- canonical_hash AND matrix_hash present + deriving Repr + +private def wRank : Int := 24 +private def wGap : Int := 18 +private def wEntropy : Int := 18 +private def wDensity : Int := 12 +private def wLap : Int := 12 +private def wHash : Int := 16 + +private def lapScore (lapFull : Bool) : Q16_16 := + if lapFull then Q16_16.one else Q16_16.ofRawInt 29491 -- 0.45 * 65536 + +private def hashScore (hasHashes : Bool) : Q16_16 := + if hasHashes then Q16_16.one else Q16_16.zero + +def spectralQuality (f : SpectralFeatures) : Q16_16 := + let raw := + wRank * f.rankScore.toInt / 100 + + wGap * f.gapScore.toInt / 100 + + wEntropy * f.entropyScore.toInt / 100 + + wDensity * f.densityScore.toInt / 100 + + wLap * (lapScore f.lapFull).toInt / 100 + + wHash * (hashScore f.hasHashes).toInt / 100 + Q16_16.ofRawInt raw + +-- ───────────────────────────────────────────────────────────────────────────── +-- §5 Receipt density and confidence (ports compute_density in Research Stack shim) +-- ───────────────────────────────────────────────────────────────────────────── + +structure DensityComponents where + statusScore : Q16_16 + axisScore : Q16_16 + spectralScore : Q16_16 + shapeScore : Q16_16 + deriving Repr + +structure DensityResult where + density : Q16_16 + confidence : Q16_16 + components : DensityComponents + warnings : List String + deriving Repr + +private def weightedSum (weights : List Int) (scores : List Q16_16) : Q16_16 := + let raw := (weights.zip scores).foldl + (fun acc (ws : Int × Q16_16) => acc + ws.1 * ws.2.toInt / 100) + 0 + Q16_16.ofRawInt raw + +def computeDensity + (status : SourceStatus) + (axes : AxisFlags) + (spectral: SpectralFeatures) + (shape : RRCShape) + (pistProxy : Option RRCShape) + (pistExact : Option RRCShape) + : DensityResult := + let sStatus := statusScore status + let sAxes := axisScore axes + let sSpectral := spectralQuality spectral + let sShape := shapeAgreement shape pistProxy pistExact + + let hasPrediction := pistProxy.isSome || pistExact.isSome + + let warnings : List String := + (if !hasPrediction then ["missing_pist_prediction"] else []) ++ + (if hasPrediction && sShape.toInt < 32768 then ["pist_shape_disagreement"] else []) + + let densityWeights : List Int := [26, 24, 26, 24] + let confidenceWeights : List Int := [20, 20, 28, 32] + let scoreList : List Q16_16 := [sStatus, sAxes, sSpectral, sShape] + + let density := weightedSum densityWeights scoreList + let confidence := weightedSum confidenceWeights scoreList + + { density := density + confidence := confidence + components := { statusScore := sStatus, axisScore := sAxes + spectralScore := sSpectral, shapeScore := sShape } + warnings := warnings.eraseDups } + +-- ───────────────────────────────────────────────────────────────────────────── +-- §6 Claim boundary +-- ───────────────────────────────────────────────────────────────────────────── + +def claimBoundary : String := + "receipt-density-scoring-only; not-a-proof; promotion=not_promoted" + +-- ───────────────────────────────────────────────────────────────────────────── +-- §7 Eval witnesses +-- ───────────────────────────────────────────────────────────────────────────── + +-- Witness: CANDIDATE row with 3/5 target axes, no PIST prediction. +#eval + let axes : AxisFlags := + { projectionDeclared := true, negativeControlStrength := false + witnessDeclared := true, scaleBandDeclared := true, shapeClosure := false } + let spectral : SpectralFeatures := + { rankScore := Q16_16.zero, gapScore := Q16_16.zero, entropyScore := Q16_16.zero + densityScore := Q16_16.zero, lapFull := false, hasHashes := false } + let r := computeDensity .candidate axes spectral + RRCShape.cognitiveLoadField none none + (r.density.toInt, r.warnings) + +-- Witness: VERIFIED row, exact PIST match, 5/5 axes, full spectral. +#eval + let axes : AxisFlags := + { projectionDeclared := true, negativeControlStrength := true + witnessDeclared := true, scaleBandDeclared := true, shapeClosure := true } + let spectral : SpectralFeatures := + { rankScore := Q16_16.ofRatio 1 2 -- rank=4/8=0.5 + gapScore := Q16_16.ofRatio 3 4 -- gap=0.75 + entropyScore := Q16_16.ofRatio 2 3 -- entropy/3=0.67 + densityScore := Q16_16.ofRatio 1 2 -- crossing/0.5=0.5 + lapFull := true, hasHashes := true } + let r := computeDensity .verified axes spectral + RRCShape.logogramProjection + (some RRCShape.logogramProjection) (some RRCShape.logogramProjection) + (r.density.toInt, r.confidence.toInt, r.warnings) + +end SilverSight.RRC.ReceiptDensity diff --git a/lakefile.lean b/lakefile.lean index 2d553e4e..1c73245d 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -1,5 +1,6 @@ import Lake open Lake DSL +open System package «SilverSight» where -- Settings applied to both builds and interactive editing @@ -42,6 +43,9 @@ lean_lib «SilverSightRRC» where `SilverSight.RRCLogogramProjection, `SilverSight.ReceiptCore, `SilverSight.RRC.Emit, + `SilverSight.RRC.ReceiptDensity, + `SilverSight.RRC.PolyFactorIdentity, + `SilverSight.RRC.EntropyCandidates, `SilverSight.RRC.Corpus250, `SilverSight.AVMIsa.Types, `SilverSight.AVMIsa.Value, @@ -56,5 +60,24 @@ lean_exe «rrc-emit-fixture» where root := `RrcEmitFixture srcDir := "exe" +lean_exe «q16-roundtrip» where + root := `Q16_16Roundtrip + srcDir := "exe" + +-- Static C library for the Q16_16 roundtrip executable. +def cSrcDir : FilePath := FilePath.mk "c" + +target q16_canonical.o pkg : FilePath := do + let oFile := pkg.buildDir / cSrcDir / "q16_canonical.o" + let srcJob ← inputFile (pkg.srcDir / cSrcDir / "q16_canonical.c") true + let flags := #["-fPIC", "-O2"] + buildO oFile srcJob flags + +extern_lib q16_canonical pkg := do + let name := nameToStaticLib "q16_canonical" + let libFile := pkg.buildDir / cSrcDir / name + let oJob ← fetch <| pkg.target ``q16_canonical.o + buildStaticLib libFile #[oJob] + require mathlib from git "https://github.com/leanprover-community/mathlib4.git" diff --git a/tests/test_q16_roundtrip.py b/tests/test_q16_roundtrip.py new file mode 100644 index 00000000..a2a5f389 --- /dev/null +++ b/tests/test_q16_roundtrip.py @@ -0,0 +1,426 @@ +"""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())