SilverSight/docs/adversarial_review/ADVERSARIAL_REVIEW_SYSTEMS.md

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:

  # 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:

  # 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:

  # 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:

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:

  # 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:

  # 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)

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)

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)

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)

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.