mirror of
https://github.com/allaunthefox/SilverSight.git
synced 2026-07-31 01:25:21 +00:00
feat(rrc): port ReceiptDensity, PolyFactorIdentity, EntropyCandidates and add Q16_16 roundtrip test
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
This commit is contained in:
parent
fbb71cffc9
commit
fec200205e
11 changed files with 1705 additions and 20 deletions
17
AGENTS.md
17
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.
|
||||
|
|
|
|||
77
c/q16_canonical.c
Normal file
77
c/q16_canonical.c
Normal file
|
|
@ -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 <math.h>
|
||||
#include <stdint.h>
|
||||
#include <float.h>
|
||||
|
||||
#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);
|
||||
}
|
||||
|
|
@ -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",
|
||||
|
|
|
|||
|
|
@ -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`)
|
||||
|
||||
|
|
|
|||
|
|
@ -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 |
|
||||
|
|
|
|||
105
exe/Q16_16Roundtrip.lean
Normal file
105
exe/Q16_16Roundtrip.lean
Normal file
|
|
@ -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
|
||||
209
formal/SilverSight/RRC/EntropyCandidates.lean
Normal file
209
formal/SilverSight/RRC/EntropyCandidates.lean
Normal file
|
|
@ -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
|
||||
386
formal/SilverSight/RRC/PolyFactorIdentity.lean
Normal file
386
formal/SilverSight/RRC/PolyFactorIdentity.lean
Normal file
|
|
@ -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
|
||||
240
formal/SilverSight/RRC/ReceiptDensity.lean
Normal file
240
formal/SilverSight/RRC/ReceiptDensity.lean
Normal file
|
|
@ -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
|
||||
|
|
@ -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"
|
||||
|
|
|
|||
426
tests/test_q16_roundtrip.py
Normal file
426
tests/test_q16_roundtrip.py
Normal file
|
|
@ -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())
|
||||
Loading…
Add table
Reference in a new issue