security(adversarial-review): ADVERSARIAL_REVIEW_MASTER.md

docs/adversarial_review/ADVERSARIAL_REVIEW_MASTER.md

@@ -0,0 +1,217 @@
+# ADVERSARIAL REVIEW — SilverSight Full Project Audit
+
+**Date**: 2026-06-23
+**Doctrine**: Guilty Until Proven Innocent
+**Reviewers**: 5 specialized adversarial agents
+**Scope**: ~130 source files across Lean 4, Python, WGSL, HTML5/JS
+
+---
+
+## EXECUTIVE SUMMARY
+
+The adversarial review found **156 issues** across 5 domains:
+
+| Domain | Critical | High | Medium | Low | Total |
+|--------|----------|------|--------|-----|-------|
+| Formal Verification | 5 | 8 | 10 | 5 | 28 |
+| Code Implementation | 11 | 18 | 27 | 15 | 71 |
+| Mathematical Foundation | 5 | 7 | 7 | 5 | 24 |
+| Systems Integration | 4 | 9 | 7 | 2 | 22 |
+| Cryptographic Security | 5 | 8 | 10 | 5 | 28 |
+| **UNIQUE (deduplicated)** | **18** | **28** | **42** | **25** | **113** |
+
+**Verdict**: The project is a promising research prototype with genuine insights
+(particularly in Sidon sets, codec consistency, AVM core, and the eigensolid
+conditional theorem) but is **NOT production-ready**. The flagship claims
+(Chentsov's theorem, NP-hard solving, Finsler metric) are not substantiated.
+
+---
+
+## TOP 10 CRITICAL ISSUES (Project-Threatening)
+
+### CR-1: Chentsov's Theorem is NOT Proven
+**Files**: `ChentsovFinite.lean`
+**Finding**: The flagship claim proves only that a functional equation H(t)=c/t
+has unique solution, and that Fisher metric is invariant under splittings. It
+**never connects** Chentsov invariance to the metric structure. The final steps
+use `rfl` (reflexivity) where genuine mathematical arguments are required.
+**Impact**: The project's unique selling point is unproven.
+**Fix**: Write the connecting argument from Chentsov invariance to the
+functional equation, or restate the theorem with its actual scope.
+
+### CR-2: 7 Axioms Assert Deep Unproven Number Theory
+**Files**: `PVGS_DQ_Bridge/` section files
+**Finding**: Baker's theorem, BMS bounds, Goormaghtigh conjecture are stated
+as axioms. If any axiom is inconsistent or misstated, the entire bridge collapses.
+**Impact**: Potential inconsistency in the formal system.
+**Fix**: Replace axioms with proven bounds or clearly mark as conjectures.
+
+### CR-3: SQL Injection in Citation Module
+**File**: `python/hachimoji_citation.py`
+**Finding**: User-provided equation strings are concatenated directly into SQL
+queries via naive `replace("'", "''")`. PoC: `"1=1'; DROP TABLE arxiv_papers; --"`
+**Impact**: Arbitrary SQL execution on the citation database.
+**Fix**: Use parameterized queries (psycopg2 `%s` placeholders).
+
+### CR-4: Receipt System Trivially Forgeable
+**File**: `formal/RRCLib/ReceiptCore.lean`, `python/integration_sprint.py`
+**Finding**: Receipt `valid: Bool` field has NO cryptographic validation. An
+adversary sets `valid := true` and all checks pass. SHA256 truncated to 24 hex
+chars has birthday bound of ~2^48, not 2^128.
+**Impact**: Entire trust system is forgeable.
+**Fix**: Add HMAC-SHA256 signature with secret key, use full 64-char SHA256.
+
+### CR-5: Memory Exhaustion via Unbounded Enumeration
+**Files**: `python/dna_gpu.py`, `dna_lut.py`, `dna_qubo_sort.py`
+**Finding**: All enumerate `2**n_vars` without bounds checking. At n=30, allocates
+256 GB.
+**Impact**: Denial of service / OOM kill.
+**Fix**: Add max_n_vars guard (e.g., 20), streaming computation for large n.
+
+### CR-6: Q16_16 Arithmetic Precision Loss
+**File**: `python/pist_braid_bridge.py`, `python/q16_canonical.py`
+**Finding**: `q16_mul()` in bridge uses `//` (floor division), canonical uses
+`round()`. Lean uses `floor`. Three variants produce different results by ±1 LSB.
+At boundary values, `float_to_q16(32767.5)` differs by 32,767 LSBs.
+**Impact**: Cross-module numerical drift.
+**Fix**: Single canonical Q16_16 library, exact integer arithmetic throughout.
+
+### CR-7: Finsler Metric Fails Finsler Axioms
+**File**: `qubo/finsler_metric.py`
+**Finding**: Claimed Randers metric F = α + β fails homogeneity (depends on
+endpoints, not tangent vectors), requires post-hoc `max(F, 1e-10)` for positivity,
+and does not enforce |β| < α.
+**Impact**: Mathematical foundation of QUBO solver is invalid.
+**Fix**: Implement proper Randers metric with tangent vector arguments and
+enforce |β| < α.
+
+### CR-8: Spectral Profile Has Trivial Collisions
+**File**: `python/spectral_profile.py`
+**Finding**: Profiles computed from byte-level statistics only. Confirmed
+collisions: `"a+b=c"`, `"x+y=z"`, `"x*y=z"`, `"p/q=r"` all produce identical
+8D profiles.
+**Impact**: Classifier can be poisoned by adversarial input crafting.
+**Fix**: Add semantic features or cryptographic hash to break collisions.
+
+### CR-9: Eigensolid Convergence is Enumeration, Not Proof
+**File**: `formal/CoreFormalism/BraidEigensolid.lean`
+**Finding**: The convergence theorem checks 8 cases via `native_decide`, not a
+mathematical proof. The `receipt_invertible` theorem is a tautology:
+`(A==B) ↔ (valid A ↔ valid B)` proves nothing about bijection.
+**Impact**: The compressor correctness claim is unsubstantiated.
+**Fix**: Prove convergence by induction, or clearly mark as verified-by-computation.
+
+### CR-10: DNA Encoding Fully Reversible (No Encryption)
+**Files**: `python/dna_codec.py`, `formal/CoreFormalism/HachimojiCodec.lean`
+**Finding**: Perfect bijection with no key, no salt, no encryption. Any
+intercepted DNA sequence leaks its entire payload via simple lookup table.
+**Impact**: Zero confidentiality for encoded data.
+**Fix**: Add keyed permutation layer or encrypt-then-encode for sensitive data.
+
+---
+
+## DOMAIN-SPECIFIC SUMMARIES
+
+### Formal Verification (28 findings)
+- **23 sorries** across the project (proof gaps)
+- **7 axioms** (potential inconsistency risks)
+- **30+ native_decide** (computation, not proof)
+- **293 theorem declarations** but many are tautologies
+- **What IS proven well**: SidonSets (Lindstrom bound), HachimojiCodec
+  consistency, SilverSightCore AVM theorems, InteractionGraphSidon CRT theorems,
+  BraidEigensolid.eigensolid_trivial (conditional)
+- **What's NOT proven**: Chentsov uniqueness, eigensolid convergence,
+  receipt bijection, PVGS bridge theorems
+
+### Code Implementation (71 findings)
+- **8% test coverage** overall, 23% of tested Python
+- **19 modules with ZERO tests** (integration pipeline, chaos game, all WGSL,
+  all HTML5/JS, citation layer)
+- **SQL injection** in citation module
+- **Command injection** via subprocess
+- **WGSL race conditions** in all shaders
+- **WebGPU O(n²) dispatches** for large datasets
+- **Q16_16 precision loss** in Python→float conversion
+- **Massive code duplication** (qubo_energy 5x, BASES 6x, int_to_dna 3x)
+
+### Mathematical Foundation (24 findings)
+- **Chentsov theorem is vacuous** — rfl where proof needed
+- **Finsler metric fails axioms** — not actually a Finsler metric
+- **NP-hard claims unsubstantiated** — total work exceeds brute force
+- **Eigensolid_trivial is genuinely correct** — a real conditional theorem
+- **Phi-corkscrew bijection is valid** — ψ/2π irrational gives injectivity
+- **Fisher-Rao distance formula is correct** — arccos(Σ√(pᵢqᵢ)) is standard
+
+### Systems Integration (22 findings)
+- **Lean↔Python Q16_16 divergence**: `//` vs `round()` vs `floor`
+- **"Spectral profile" means 3 different things** across 2 languages
+- **Python receipts and Lean ReceiptCore have ZERO common fields**
+- **No end-to-end integration test exists**
+- **DNA alphabet ordering is actually CONSISTENT** (ABCGPSTZ everywhere) —
+  the "known bug" was previously fixed
+- **GPU buffer formats differ** between JS and Python paths
+
+### Cryptographic Security (28 findings)
+- **Receipt forgery**: trivial (valid: Bool with no crypto)
+- **DNA encoding**: fully reversible with public LUT
+- **Spectral collisions**: confirmed with 4 distinct equations
+- **Chaos game LCG**: fully predictable from hash
+- **Q16_16 div-by-zero**: returns MAX_RAW silently
+- **WGSL buffer overflow**: unbounded `sequences[seq_idx]`
+- **Cross-mode agreement bypass**: 50% difference still "agrees"
+
+---
+
+## WHAT IS GENUINELY GOOD
+
+Despite the issues, several components are solid:
+
+1. **SidonSets.lean** — Genuine formal mathematics (Lindstrom bound, Johnson
+   bound, Singer theorem infrastructure)
+2. **HachimojiCodec.lean** — Honestly proven consistency theorems
+3. **SilverSightCore.lean** — All TIC/AVM theorems correctly proven by induction
+4. **BraidEigensolid.eigensolid_trivial** — Real conditional theorem with
+   complete proof
+5. **Integration sprint** — All 4 modes agree (CV=0.0), all checks pass
+6. **Φ-corkscrew bijection** — Mathematically valid (irrational rotation)
+7. **Golden spiral recovery** — Bijective encoding with exact roundtrip
+8. **BraidSpherionBridge** — The braidCross ↔ Mountain.merge correspondence
+   lemma is well-structured
+
+---
+
+## RECOMMENDATIONS
+
+### Immediate (Block Production)
+1. Fix SQL injection in `hachimoji_citation.py`
+2. Add bounds checking to all `2**n` enumerations
+3. Unify Q16_16 arithmetic to single canonical implementation
+4. Add HMAC to receipt system
+
+### Short-Term (Before Public Release)
+5. Write the missing Chentsov connecting argument or restate theorem
+6. Replace 7 axioms with proven bounds or conjecture markers
+7. Add keyed encryption layer to DNA encoding for sensitive data
+8. Write end-to-end integration test
+9. Achieve 80%+ test coverage for critical paths
+10. Fix Finsler metric to satisfy axioms
+
+### Long-Term (Research Direction)
+11. Replace `native_decide` proofs with actual proofs
+12. Prove eigensolid convergence by induction
+13. Close the 23 sorries
+14. Add semantic features to spectral profile to break collisions
+15. Formalize the Φ-corkscrew bijection in Lean
+
+---
+
+## REVIEWER FILES
+
+| Reviewer | File | Lines |
+|----------|------|-------|
+| Formal Verification | `ADVERSARIAL_REVIEW_FORMAL.md` | 696 |
+| Code Implementation | `ADVERSARIAL_REVIEW_CODE.md` | 1,003 |
+| Mathematical Foundation | `ADVERSARIAL_REVIEW_MATH.md` | 723 |
+| Systems Integration | `ADVERSARIAL_REVIEW_SYSTEMS.md` | ~800 |
+| Cryptographic Security | `ADVERSARIAL_REVIEW_CRYPTO.md` | 785 |
+| **Master Synthesis** | **ADVERSARIAL_REVIEW_MASTER.md** | **This file** |