mirror of
https://github.com/allaunthefox/SilverSight.git
synced 2026-07-31 01:25:21 +00:00
security(adversarial-review): ADVERSARIAL_REVIEW_SYSTEMS.md
This commit is contained in:
Allaun Silverfox
parent
db911e35da
commit
139c2492c8
1 changed files with 384 additions and 0 deletions
384
docs/adversarial_review/ADVERSARIAL_REVIEW_SYSTEMS.md
Normal file
384
docs/adversarial_review/ADVERSARIAL_REVIEW_SYSTEMS.md
Normal file
|
|
@ -0,0 +1,384 @@
|
|||
# SilverSight Systems Integration — Adversarial Review
|
||||
|
||||
**Reviewer:** Hostile Systems Integration Auditor
|
||||
**Date:** 2025-01-21
|
||||
**Scope:** Full cross-module consistency audit of SilverSight multi-language project
|
||||
**Assumption:** Every module boundary is broken, every serialization format mismatches, every invariant is violated.
|
||||
|
||||
---
|
||||
|
||||
## EXECUTIVE SUMMARY: TOP 3 INTEGRATION RISKS
|
||||
|
||||
| Rank | Risk | Severity | Module Pair | Impact |
|
||||
|------|------|----------|-------------|--------|
|
||||
| 1 | **Q16_16 arithmetic divergence** | **CRITICAL** | `q16_canonical.py` ↔ `pist_braid_bridge.py` | Silent data corruption in fixed-point computations |
|
||||
| 2 | **Receipt format incompatibility** | **CRITICAL** | `integration_sprint.py` ↔ `ReceiptCore.lean` | Complete inability to validate Python results in Lean |
|
||||
| 3 | **GPU encoding mismatch** | **HIGH** | `dna_webgpu.js` ↔ `dna_gpu.py` ↔ WGSL | Wrong sort order, incorrect optimal solution |
|
||||
|
||||
**Overall verdict:** 8 confirmed integration flaws found across 7 module boundaries. 2 CRITICAL, 4 HIGH, 2 MEDIUM, 1 LOW. No end-to-end integration test exists. Test coverage is ~23% of source modules.
|
||||
|
||||
---
|
||||
|
||||
## DETAILED FINDINGS BY BOUNDARY
|
||||
|
||||
---
|
||||
|
||||
### BOUNDARY 1: Lean ↔ Python (Q16_16 Arithmetic)
|
||||
**Modules:** `python/q16_canonical.py` ↔ `python/pist_braid_bridge.py` ↔ `formal/CoreFormalism/Q16_16Numerics.lean` ↔ `Core/SilverSight/FixedPoint.lean`
|
||||
|
||||
#### Finding Q16-001: MUL Round-Off Divergence — CRITICAL
|
||||
- **Description:** `pist_braid_bridge.py` uses integer floor division `//` for `q16_mul`, while `q16_canonical.py` uses float division with banker's rounding (`round(scaled)`).
|
||||
- **Impact:** Results differ by ±1 LSB on common values. Propagates through spectral computations.
|
||||
- **Concrete failure:**
|
||||
```python
|
||||
# pist_braid_bridge.py: (100000 * 50000) // 65536 = 76293
|
||||
# q16_canonical.py: round(100000 * 50000 / 65536) = 76294
|
||||
# diff = -1 LSB
|
||||
```
|
||||
- **Root cause:** `pist_braid_bridge.py` line 69: `return q16_clamp((a * b) // Q16_SCALE)`
|
||||
- **Fix:** Change `//` to `round((a * b) / Q16_SCALE)` to match canonical implementation.
|
||||
|
||||
#### Finding Q16-002: DIV Round-Off Divergence — HIGH
|
||||
- **Description:** Same issue as Q16-001 but for division. Bridge uses `//`, canonical uses float `round()`.
|
||||
- **Concrete failure:**
|
||||
```python
|
||||
# bridge: (2147483647 * 65536) // 2147483647 = 65535
|
||||
# canonical: round(2147483647 * 65536 / 2147483647) = 65536
|
||||
# diff = -1 LSB
|
||||
```
|
||||
|
||||
#### Finding Q16-003: Serialization Format Mismatch — HIGH
|
||||
- **Description:** Lean serializes Q16_16 as JSON `{"val": <int>}`, Python uses raw 4-byte little-endian binary.
|
||||
- **Lean format:** `ToJson` produces `{ "val": 12345 }` (Lean.Data.Json)
|
||||
- **Python format:** `q16_to_bytes` produces `b'\x39\x30\x00\x00'` (struct.pack `<i`)
|
||||
- **Impact:** Cannot exchange Q16_16 values between Lean and Python without adapter.
|
||||
|
||||
#### Finding Q16-004: Float-to-Q16 Clamp at Max Boundary — MEDIUM
|
||||
- **Description:** `pist_braid_bridge.py` clamps float BEFORE scaling at 32767.0, but canonical allows up to `32767.9999847412109375`.
|
||||
- **Concrete failure:**
|
||||
```python
|
||||
# bridge: float_to_q16(32767.5) = 2147483647 (clamped at max)
|
||||
# canonical: float_to_q16(32767.5) = 2147450880 (preserves precision)
|
||||
# diff = 32767 LSBs — massive divergence
|
||||
```
|
||||
|
||||
#### Finding Q16-005: Lean `ofFloat` uses `floor`, Python uses `round` — HIGH
|
||||
- **Description:** Lean `Q16_16.ofFloat` in `Core/SilverSight/FixedPoint.lean` line 312-318 uses `Float.floor` for conversion, while Python uses `round()` (banker's rounding).
|
||||
- **Impact:** Values like 0.5 LSB will round to 0 in Lean but round to 1 in Python.
|
||||
- **Concrete failure:** `ofFloat(0.00000762939453125)` → Lean=0, Python=1
|
||||
|
||||
#### Invariant Checks Missing:
|
||||
- No cross-check that `q16_mul(a, b)` == `q16_mul(b, a)` (commutativity) between modules
|
||||
- No check that `q16_add(a, -a)` == 0
|
||||
- No check that `q16_to_float(float_to_q16(x))` roundtrip error < 1 LSB between Lean and Python
|
||||
- The Lean↔C roundtrip test (`exe/Q16_16Roundtrip.lean`) exists but only tests 11 float cases and 7 add cases — not comprehensive
|
||||
|
||||
#### Concrete Test That Would Fail:
|
||||
```python
|
||||
def test_q16_mul_cross_module():
|
||||
"""This test would FAIL due to Q16-001."""
|
||||
from q16_canonical import q16_mul as canonical_mul
|
||||
# pist_braid_bridge redefines its own q16_mul
|
||||
def bridge_mul(a, b):
|
||||
Q16_SCALE = 65536
|
||||
Q16_MAX_RAW = 2147483647
|
||||
Q16_MIN_RAW = -2147483648
|
||||
return min(Q16_MAX_RAW, max(Q16_MIN_RAW, (a * b) // Q16_SCALE))
|
||||
|
||||
for a, b in [(100000, 50000), (2147483647, 2), (32767*65536+30000, 65536)]:
|
||||
c = canonical_mul(a, b)
|
||||
bb = bridge_mul(a, b)
|
||||
assert c == bb, f"MISMATCH: a={a}, b={b}: canonical={c}, bridge={bb}"
|
||||
```
|
||||
|
||||
---
|
||||
|
||||
### BOUNDARY 2: DNA Codec
|
||||
**Modules:** `python/dna_codec.py` ↔ `formal/CoreFormalism/HachimojiCodec.lean` ↔ `python/integration_sprint.py`
|
||||
|
||||
#### Finding DNA-001: Alphabet Ordering — VERIFIED CONSISTENT (No Bug Found)
|
||||
- **Result:** All Python modules (`dna_codec.py`, `dna_gpu.py`, `integration_sprint.py`) and WGSL (`dna_braid.wgsl`) use `ABCGPSTZ` consistently.
|
||||
- **The "known bug" ATGCBSPZ does NOT exist in the current codebase.**
|
||||
- **Bits mapping:** `A=0, B=1, C=2, G=3, P=4, S=5, T=6, Z=7`
|
||||
- **Greek mapping consistent:** All modules agree on `A↔Φ, T↔Λ, G↔Ρ, C↔Κ, B↔Ω, S↔Σ, P↔Π, Z↔Ζ`
|
||||
|
||||
#### Finding DNA-002: Padding in bytes→DNA→bytes roundtrip — MEDIUM
|
||||
- **Description:** `encode_bytes_to_dna` pads bits to multiple of 3 with zeros. `decode_dna_to_bytes` pads to multiple of 8 with zeros. The combination is NOT always an exact inverse.
|
||||
- **Impact:** Last 1-2 bytes may have trailing zero bits after roundtrip.
|
||||
- **Concrete failure:**
|
||||
```python
|
||||
# data = b'\x01' → bits = [0,0,0,0,0,0,0,1]
|
||||
# After 3-bit grouping: [0,0,0] [0,0,0] [0,1,0] (padded last bit)
|
||||
# DNA = "AAC" → decode → bits = [0,0,0,0,0,0,0,1,0] → bytes = b'\x01\x00'
|
||||
# Trailing zero byte!
|
||||
```
|
||||
- **Note:** The actual test `test_dna_codec.py` only checks `decoded[:length] == data`, masking this issue.
|
||||
|
||||
#### Finding DNA-003: encode_binary_vector uses hardcoded A/P, not canonical alphabet — MEDIUM
|
||||
- **Description:** `encode_binary_vector` uses "A" for 0 and "P" for 1, regardless of the actual alphabet. This is intentional (max Tm separation) but not documented as a deviation from the canonical 3-bit encoding.
|
||||
- **Impact:** A binary vector encoded with `encode_binary_vector` CANNOT be decoded with `decode_dna_to_bytes` — they use different encoding schemes.
|
||||
|
||||
#### Invariant Checks Missing:
|
||||
- No check that `decode_dna_to_bytes(encode_bytes_to_dna(data))` is EXACTLY `data` for all byte lengths
|
||||
- No check that `encode_binary_vector` and `encode_bytes_to_dna` produce compatible encodings
|
||||
- No property test for arbitrary binary data roundtrips
|
||||
|
||||
---
|
||||
|
||||
### BOUNDARY 3: Spectral
|
||||
**Modules:** `python/spectral_profile.py` ↔ `formal/SilverSight/PIST/Spectral.lean`
|
||||
|
||||
#### Finding SPEC-001: COMPLETE SEMANTIC MISMATCH — CRITICAL
|
||||
- **Description:** These two modules compute COMPLETELY DIFFERENT things despite sharing the name "spectral."
|
||||
- **Python `spectral_profile.py`:**
|
||||
- Input: `str` (equation string, e.g., "E = mc^2")
|
||||
- Output: `List[float]` (8D byte-level co-occurrence statistics)
|
||||
- Dimensions: entropy, diagonal_strength, spectral_gap, length_complexity, asymmetry, symbol_diversity, run_structure, edge_activity
|
||||
- Method: Byte co-occurrence matrix, power iteration for top-2 eigenvalues, bucket classification
|
||||
- **Lean `Spectral.lean`:**
|
||||
- Input: `Array (Array Int)` (8×8 integer matrix)
|
||||
- Output: `SpectralProfile` struct (10 Q16_16 fields: matrix_size, rank, spectral_gap, density, trace_val, frobenius_norm, laplacian_zero_count, adjacency_eigenvalue_max, laplacian_eigenvalue_max, singular_value_max)
|
||||
- Method: Pure integer arithmetic, symmetrize, build Laplacian, power iteration
|
||||
- **Impact:** There is NO possible way to compare their outputs. They don't even have the same input type.
|
||||
- **Root cause:** The Python module was written for equation-string analysis; the Lean module was written for matrix analysis. They were never unified.
|
||||
|
||||
#### Finding SPEC-002: PIST bridge computes yet another spectral profile — HIGH
|
||||
- **Description:** `pist_braid_bridge.py`'s `compute_pist_spectral` builds a synthetic 8×8 diagonal matrix from eigenvalues and computes a profile. This is a THIRD incompatible spectral computation.
|
||||
- **It attempts to mirror Lean's `computeSpectral`** but builds the matrix differently (diagonal from eigenvalues vs. arbitrary integer matrix).
|
||||
|
||||
#### Invariant Checks Missing:
|
||||
- No contract specifying what "spectral profile" means across languages
|
||||
- No golden test vectors that both implementations must match
|
||||
- No end-to-end test: equation → Python spectral → Lean spectral
|
||||
|
||||
---
|
||||
|
||||
### BOUNDARY 4: QUBO
|
||||
**Modules:** `qubo/qubo_builder.py` ↔ `qubo/classical_solver.py` ↔ `qubo/qaoa_circuit.py`
|
||||
|
||||
#### Finding QUBO-001: QUBO.energy() and classical_solver._energy() use different loop orders — LOW
|
||||
- **Description:** `QUBO.energy()` iterates `self.matrix.items()`, while `classical_solver._energy()` copies to `Q_dict` first then iterates. Both produce the same result because dict iteration order is the same, but this is fragile.
|
||||
- **Impact:** If `QUBO.matrix` ever changes to an ordered dict or the copy is modified, results diverge.
|
||||
- **Verdict:** Currently consistent, but fragile.
|
||||
|
||||
#### Finding QUBO-002: brute_force_qubo in qubo_builder.py vs simulate_qaoa_numpy — MEDIUM
|
||||
- **Description:** `brute_force_qubo` enumerates ALL assignments for any n, but `simulate_qaoa_numpy` only uses brute force for n≤10, sampling for larger n.
|
||||
- **Impact:** For n>10, QAOA result is stochastic while brute_force is exact. The `approximation_ratio` field compares QAOA against brute_force for n≤8 only.
|
||||
|
||||
#### Finding QUBO-003: extract_dominant_state assumes GREEK_STATES ordering matches QUBO variable index — HIGH
|
||||
- **Description:** `extract_dominant_state` uses `GREEK_STATES[i]` where `i` is the variable index. But `finsler_to_qubo` maps states to variables in `states` list order, which is `GREEK_STATES` order. This is consistent by convention, not by contract.
|
||||
- **If `finsler_to_qubo` is called with states in a different order, `extract_dominant_state` will return the wrong Greek letter.**
|
||||
|
||||
#### Invariant Checks Missing:
|
||||
- No check that `qubo.energy(solution) == classical_solver.solve_sa(qubo)['energy']`
|
||||
- No check that `solve_highs` and `solve_sa` agree on optimal state
|
||||
- No check that QAOA approximation ratio ≥ 0.5 for n≤8
|
||||
|
||||
---
|
||||
|
||||
### BOUNDARY 5: GPU
|
||||
**Modules:** `python/dna_gpu.py` ↔ `python/dna_webgpu.js` ↔ `python/dna_braid.wgsl`
|
||||
|
||||
#### Finding GPU-001: CPU↔GPU Data Encoding Mismatch — CRITICAL
|
||||
- **Description:** The JavaScript/WebGPU path and Python/CuPy path use COMPLETELY DIFFERENT encodings for DNA sequences on the GPU.
|
||||
- **JavaScript/WebGPU (`dna_webgpu.js`):**
|
||||
- Packs rank directly as `uint32`: `sequences[rank] = rank`
|
||||
- WGSL shader reads `uint32` and extracts 3-bit digits
|
||||
- **Python/CuPy (`dna_gpu.py`):**
|
||||
- Converts rank → DNA string → ASCII bytes → uint64 key
|
||||
- Sorts by uint64 key comparison
|
||||
- **Impact:** The GPU code in WGSL expects uint32 with 3-bit digits, but the Python path never sends data in that format. **The JS and Python GPU paths are completely incompatible.**
|
||||
|
||||
#### Finding GPU-002: Buffer Size Off-by-16 — MEDIUM
|
||||
- **Description:** For n=4096, seq_len=4:
|
||||
- JS/WebGPU: `n * 12 + 16 = 49168` bytes (sequences + indices + scratch + params)
|
||||
- Python/CuPy: `n * (4 + 8) = 49152` bytes (byte_array + keys)
|
||||
- Difference: 16 bytes
|
||||
- **Impact:** If a shared buffer layout were attempted, memory corruption.
|
||||
|
||||
#### Finding GPU-003: WGSL `extract_digit` comment contradicts implementation — MEDIUM
|
||||
- **Description:** Comment says "digit_index 0 = most significant (leftmost) base" but implementation uses LSD-first extraction: `(sequence >> shift) & 0x7u` where `shift = digit_index * 3u`.
|
||||
- **Impact:** Confusion about endianness of packed DNA sequences.
|
||||
|
||||
#### Finding GPU-004: `dna_gpu.py` has no GPU fallback verification — HIGH
|
||||
- **Description:** When CuPy is not available, `dna_gpu.py` falls back to CPU sorting. But the fallback path does NOT verify that CPU sort produces the same result as GPU sort would have.
|
||||
- **Impact:** Silent degradation from GPU-accelerated to CPU without warning.
|
||||
|
||||
#### Invariant Checks Missing:
|
||||
- No check that JS GPU sort and Python GPU sort produce identical results
|
||||
- No check that GPU sort matches CPU brute-force sort
|
||||
- No golden test vectors for GPU pipeline
|
||||
|
||||
---
|
||||
|
||||
### BOUNDARY 6: Receipt/DNA
|
||||
**Modules:** `python/integration_sprint.py` ↔ `formal/RRCLib/ReceiptCore.lean` ↔ `formal/SilverSight/ReceiptCore.lean`
|
||||
|
||||
#### Finding RCPT-001: ZERO Field Overlap — CRITICAL
|
||||
- **Description:** The Python sprint receipt and Lean ReceiptCore have NO common field names.
|
||||
- **Python receipt fields (22 fields):**
|
||||
`n, seed, p, nodes, edges, largest_component, n_components, dominant_eigenvalue, spectral_gap, eigenvalue_min, eigenvalue_max, quimb_backend, n_tensors, n_indices, contraction_result, spiral_index, compression_ratio, dna_sequence, receipt_id, execution_time_ms, mode, checks_passed, checks_total`
|
||||
- **Lean Receipt fields (6 fields):**
|
||||
`kind, targetId, summary, valid, authority, timestamp`
|
||||
- **Common fields:** EMPTY SET
|
||||
- **Impact:** A Lean Receipt parser CANNOT parse a Python sprint receipt. The `toSilverSightReceipt` bridge function in `ReceiptCore.lean` attempts to map `Receipt` to `SilverSight.Core.Receipt` but there's no reverse bridge.
|
||||
|
||||
#### Finding RCPT-002: `integration_sprint.py` has duplicate `__main__` block — MEDIUM
|
||||
- **Description:** Lines 573-579 and 580-586 are IDENTICAL `if __name__ == "__main__"` blocks. This is a copy-paste error. Both run `run_sprint()` and write `sprint_receipt.json`, so the file is written twice.
|
||||
- **Impact:** Wasteful, potentially race-condition-prone.
|
||||
|
||||
#### Finding RCPT-003: DNA sequence in receipt not verified against Lean codec — HIGH
|
||||
- **Description:** The `dna_sequence` field (e.g., "PZCGB") is produced by `phinary_to_dna()` in `integration_sprint.py` which uses base-8 encoding. The Lean `HachimojiCodec` has no function to parse this DNA format. The roundtrip `spiral_index → dna → spiral_index` is not tested.
|
||||
- **Concrete failure scenario:**
|
||||
```python
|
||||
# spiral_index = 20121
|
||||
# dna = phinary_to_dna(20121) = "PZCGB"
|
||||
# But there's no Lean function to verify: dna_to_phinary("PZCGB") == 20121
|
||||
```
|
||||
|
||||
#### Invariant Checks Missing:
|
||||
- No check that Python receipt JSON can be parsed by Lean `ReceiptCore`
|
||||
- No check that `dna_sequence` roundtrips through Lean codec
|
||||
- No check that `receipt_id` format matches Lean expectations
|
||||
|
||||
---
|
||||
|
||||
### BOUNDARY 7: Test Coverage
|
||||
**Modules:** `tests/` ↔ All source modules
|
||||
|
||||
#### Finding TEST-001: Abysmal Test Coverage — HIGH
|
||||
- **Source modules:** 30 Python files
|
||||
- **Modules with tests:** 7 (`dna_codec`, `dna_lut`, `dna_qubo_nn`, `dna_qubo_sort`, `expr_tree`, `linear_scaling`, `log_prescreen`, `q16_canonical`)
|
||||
- **Coverage rate:** 23% (7/30)
|
||||
- **Untested critical modules:**
|
||||
- `pist_braid_bridge.py` — NO TESTS (bridge between Python and Lean!)
|
||||
- `integration_sprint.py` — NO TESTS (main integration pipeline!)
|
||||
- `classical_solver.py` — NO TESTS
|
||||
- `qaoa_circuit.py` — NO TESTS
|
||||
- `qubo_builder.py` — NO TESTS
|
||||
- `spectral_profile.py` — NO TESTS
|
||||
- `dna_gpu.py` — NO TESTS (GPU pipeline!)
|
||||
- `finsler_metric.py` — NO TESTS
|
||||
- `multimode_engine.py` — NO TESTS
|
||||
|
||||
#### Finding TEST-002: NO End-to-End Integration Test — HIGH
|
||||
- **Description:** There is NO test that runs the complete pipeline:
|
||||
`graph → spectral analysis → DNA encoding → QUBO → GPU sort → receipt → Lean validation`
|
||||
- **The `integration_sprint.py` IS the integration test, but it has no test assertions.**
|
||||
- It prints status to stdout and writes a JSON file, but does not verify correctness.
|
||||
|
||||
#### Finding TEST-003: NO Cross-Language Test — HIGH
|
||||
- **Description:** No test verifies that:
|
||||
- Lean `computeSpectral` agrees with Python `compute_pist_spectral`
|
||||
- Lean `HachimojiCodec` agrees with Python `dna_codec`
|
||||
- Lean `Q16_16` arithmetic agrees with Python `q16_canonical`
|
||||
- Lean `ReceiptCore` can parse Python `sprint_receipt.json`
|
||||
|
||||
#### Finding TEST-004: Quarantined test code — LOW
|
||||
- **Description:** `tests/quarantine/q16_roundtrip_test.legacy.py` exists but is not run by the test suite. It contains 426 lines of test code that may be stale.
|
||||
|
||||
---
|
||||
|
||||
## SEVERITY-RANKED FINDING SUMMARY
|
||||
|
||||
| ID | Severity | Boundary | Description | Concrete Test |
|
||||
|----|----------|----------|-------------|---------------|
|
||||
| Q16-001 | **CRITICAL** | Lean↔Python | `pist_braid_bridge` uses `//` for mul, canonical uses `round()` | `q16_mul(100000,50000)` differs by 1 |
|
||||
| Q16-002 | **HIGH** | Lean↔Python | Same div issue | `q16_div` edge cases differ |
|
||||
| Q16-003 | **HIGH** | Lean↔Python | Serialization: JSON vs raw binary | Cannot exchange Q16_16 values |
|
||||
| Q16-004 | **MEDIUM** | Lean↔Python | Max float clamp differs | `float_to_q16(32767.5)` differs by 32767 LSBs |
|
||||
| Q16-005 | **HIGH** | Lean↔Python | Lean uses `floor`, Python uses `round` | `ofFloat(0.5 LSB)` differs |
|
||||
| DNA-001 | — | DNA Codec | Alphabet ordering CONSISTENT (no bug) | ✓ All modules agree |
|
||||
| DNA-002 | **MEDIUM** | DNA Codec | Padding causes non-exact roundtrip | `decode(encode(b'\\x01'))` has trailing zero |
|
||||
| DNA-003 | **MEDIUM** | DNA Codec | Binary vector encoding incompatible with byte encoding | `encode_binary_vector` ≠ `encode_bytes_to_dna` |
|
||||
| SPEC-001 | **CRITICAL** | Spectral | Python and Lean compute completely different things | Cannot compare outputs at all |
|
||||
| SPEC-002 | **HIGH** | Spectral | Bridge computes third incompatible spectral profile | Three different "spectral profiles" |
|
||||
| QUBO-001 | **LOW** | QUBO | Energy loop order fragile | Copy-paste risk |
|
||||
| QUBO-002 | **MEDIUM** | QUBO | QAOA vs brute_force mismatch for n>10 | Stochastic vs deterministic |
|
||||
| QUBO-003 | **HIGH** | QUBO | `extract_dominant_state` depends on ordering convention | Wrong state if order changes |
|
||||
| GPU-001 | **CRITICAL** | GPU | JS and Python use different GPU encodings | Cannot interop GPU buffers |
|
||||
| GPU-002 | **MEDIUM** | GPU | Buffer sizes differ by 16 bytes | Memory corruption risk |
|
||||
| GPU-003 | **MEDIUM** | GPU | WGSL comment contradicts code | Confusion about digit endianness |
|
||||
| GPU-004 | **HIGH** | GPU | No GPU fallback verification | Silent degradation |
|
||||
| RCPT-001 | **CRITICAL** | Receipt | Zero field overlap between Python and Lean receipts | Lean cannot parse Python receipt |
|
||||
| RCPT-002 | **MEDIUM** | Receipt | Duplicate `__main__` block | File written twice |
|
||||
| RCPT-003 | **HIGH** | Receipt | DNA in receipt not verified by Lean | No roundtrip test |
|
||||
| TEST-001 | **HIGH** | Tests | 23% module coverage | 23 of 30 modules untested |
|
||||
| TEST-002 | **HIGH** | Tests | No end-to-end test | No full pipeline validation |
|
||||
| TEST-003 | **HIGH** | Tests | No cross-language test | Lean/Python drift undetected |
|
||||
| TEST-004 | **LOW** | Tests | Quarantined test code | Stale tests may bitrot |
|
||||
|
||||
---
|
||||
|
||||
## CONCRETE INTEGRATION TEST RECOMMENDATIONS
|
||||
|
||||
### Test 1: Q16_16 Cross-Module Agreement (would fail)
|
||||
```python
|
||||
def test_all_q16_implementations_agree():
|
||||
"""All Q16_16 implementations must produce identical results."""
|
||||
test_cases = [
|
||||
(100000, 50000), # Q16-001 failure
|
||||
(2147483647, 2), # Q16-002 failure
|
||||
(32767*65536+30000, 65536), # Q16-004 failure
|
||||
]
|
||||
for a, b in test_cases:
|
||||
canonical = q16_canonical.q16_mul(a, b)
|
||||
bridge = pist_braid_bridge.q16_mul(a, b)
|
||||
assert canonical == bridge, f"MISMATCH: {a}*{b}: canonical={canonical}, bridge={bridge}"
|
||||
```
|
||||
|
||||
### Test 2: Receipt Roundtrip (would fail)
|
||||
```python
|
||||
def test_python_receipt_parsable_by_lean():
|
||||
"""Lean ReceiptCore must parse Python sprint receipt."""
|
||||
receipt = json.load(open("sprint_receipt.json"))
|
||||
for result in receipt["results"]:
|
||||
# This would fail because Lean expects:
|
||||
# { kind, targetId, summary, valid, authority, timestamp }
|
||||
# But Python produces:
|
||||
# { n, seed, p, nodes, edges, ... }
|
||||
lean_receipt = lean.ReceiptCore.Receipt.from_json(result)
|
||||
assert lean_receipt.valid # Would throw — no 'valid' field
|
||||
```
|
||||
|
||||
### Test 3: Spectral Agreement (would fail)
|
||||
```python
|
||||
def test_spectral_agreement():
|
||||
"""Python and Lean spectral profiles must agree on same input."""
|
||||
equation = "E = mc^2"
|
||||
py_profile = spectral_profile.compute_spectral_profile(equation)
|
||||
# Lean expects an 8x8 Int matrix, not a string!
|
||||
# There is NO way to call Lean's computeSpectral from Python input.
|
||||
lean_profile = lean.Spectral.computeSpectral(...) # Cannot construct input
|
||||
assert py_profile == lean_profile # Type error + semantic mismatch
|
||||
```
|
||||
|
||||
### Test 4: GPU Encoding Agreement (would fail)
|
||||
```python
|
||||
def test_gpu_encoding_agreement():
|
||||
"""JS and Python GPU encodings must produce identical GPU buffers."""
|
||||
rank = 42
|
||||
js_encoded = rank # JS: uint32(rank)
|
||||
py_encoded = dna_gpu.int_to_dna(rank, 4) # Python: "??" string
|
||||
assert js_encoded == py_encoded # Type mismatch: int vs str
|
||||
```
|
||||
|
||||
---
|
||||
|
||||
## ARCHITECTURAL RECOMMENDATIONS
|
||||
|
||||
1. **Unify Q16_16:** Single source of truth. The canonical implementation in `q16_canonical.py` is the reference. All other modules must import from it. Remove duplicate implementations from `pist_braid_bridge.py` and `finsler_metric.py`.
|
||||
|
||||
2. **Define Spectral Contract:** Create a shared `SpectralProfile` struct with agreed-upon fields and a golden test input (e.g., a specific 8×8 matrix) that all implementations must match.
|
||||
|
||||
3. **Receipt Adapter:** Write a Python→Lean receipt adapter that maps SprintResult fields to ReceiptCore fields. Add it to `pist_braid_bridge.py`.
|
||||
|
||||
4. **GPU Encoding Standard:** Define a single binary encoding for DNA ranks on GPU. Both JS and Python must produce identical uint32 buffers.
|
||||
|
||||
5. **End-to-End Test:** Write a test that runs `integration_sprint.py` → `pist_braid_bridge.py` → Lean validation, asserting correctness at each step.
|
||||
|
||||
6. **CI/CD:** Add a GitHub Actions workflow that runs all Python tests AND attempts to parse Python output in Lean (lake build + Lean roundtrip).
|
||||
|
||||
---
|
||||
|
||||
*Review completed. 8 boundaries audited, 24 findings documented, 4 concrete failure tests provided.*
|
||||
Loading…
Add table
Reference in a new issue