allaun/Research-Stack
1
0
Fork 0
mirror of https://github.com/allaunthefox/Research-Stack.git synced 2026-07-30 18:56:16 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

audit: full codebase inspection — 6 auditors, 9,606 objects, 2,068 lines of findings

Browse source 
CRITICAL (7):
- C1: Hardcoded Wolfram Alpha API key (revoke immediately)
- C2: Q16_16 rounding diverges Lean↔Python↔C (data corruption)
- C3: Receipts describe non-existent files (fabrication)
- C4: '3,500+ proofs' = compilation units, not theorems
- C5: NaN sentinel collision Lean↔C (silent corruption)
- C6: eigensolid_convergence theorem is a tautology
- C7: 74% CI failure rate

HIGH (12): duplicate definitions, SQL injection, command injection,
  1,029 duplicate files, 66 large files in git, AGENTS.md drift

MEDIUM (23): stale docs, broken cross-refs, unhandled errors
LOW (31): naming violations, misplaced files, cleanup

Master synthesis: audit/MASTER_AUDIT_SYNTHESIS.md
Per-dimension reports: audit/*_audit.md
This commit is contained in:
Allaun Silverfox 2026-06-21 02:07:35 -05:00
parent b37d705065
commit 8e51acad08
7 changed files with 2267 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

199
audit/MASTER_AUDIT_SYNTHESIS.md Normal file
View file

@ -0,0 +1,199 @@
# Master Audit Synthesis
## Research-Stack Full Codebase Audit — June 21, 2026
### 6 parallel auditors, 2,068 lines of findings, 9,606 objects inspected
---
## The Honest Picture After 10+ Iterations
This repository has been through more than 10 development iterations. Each iteration added value. Each iteration also left debris. The debris has accumulated to the point where **the documentation describes a project that doesn't exist**, the **CI fails 74% of the time**, and **441 files are duplicates** of other files in the same repo.
This is not unusual for a solo researcher using AI agents. It's the expected state. What matters is seeing it clearly.
---
## Summary by Severity
| Severity | Count | Meaning |
|----------|-------|---------|
| **CRITICAL** | 7 | Security risk, data corruption, or fundamental dishonesty |
| **HIGH** | 12 | Broken functionality that affects correctness |
| **MEDIUM** | 23 | Quality issues that impede development |
| **LOW** | 31 | Cleanup, consistency, polish |
---
## The 7 Critical Issues
### C1: Hardcoded API Key (Security — revoke today)
**File:** `wolfram_verify.py`
**Finding:** Hardcoded Wolfram Alpha API key `APPID = "HYJE3R3R63"`
**Impact:** Anyone with git access can use this key. If repo is public (it is: 0 stars but public), key is exposed.
**Fix:** Revoke key immediately. Move to env var. Scrub from git history.
### C2: Q16_16 Conversion Divergence (Data Corruption)
**Files:** `FixedPoint.lean`, `lib/q16.py`, `manifold_binary.h`
**Finding:** Lean uses `floor()`, Python uses `round()`, C uses truncation. Values at half-LSB boundaries diverge silently across the entire pipeline.
**Impact:** The same Q16_16 value means different things in different languages. This corrupts every cross-language data flow.
**Fix:** Define canonical rounding mode in one file. All languages must implement identical conversion.
### C3: Receipts Describe Non-Existent Files (Fundamental Dishonesty)
**Files:** `e2e/E2E_MASTER_RECEIPT.md`, `library/CONCEPTUAL_UPGRADE_RECEIPT.md`
**Finding:** Both receipts claim detailed test results from files (`E2EMasterTrace.lean`, `hachimoji_codec_v2.py`, `ClosedTrace.lean`, etc.) that **do not exist** in the `e2e/` or `library/` directories.
**Impact:** The receipts are fabrications. This is the most dangerous kind of technical debt — the kind that makes you believe things are proven when they aren't.
**Fix:** Generate the actual files, or remove the receipts until the files exist.
### C4: "3,500+ Proofs" Claim Is Inflated (Marketing vs. Reality)
**Files:** `README.md`, `GETTING_STARTED.md`, `EXPLANATION_FOR_HUMANS.md`
**Finding:** The "3,500+ proofs" number matches the **compilation unit count**, not actual proved theorems. Many `.lean` files contain only definitions (e.g., `CarnotEfficiency.lean` = 377 bytes, one definition + `#eval`). The 26 `sorry` markers in core theorems are not counted.
**Impact:** Visitors and potential collaborators are misled about the project's maturity.
**Fix:** Replace with accurate count (e.g., "883 lines of Chentsov proof, 0 sorry; 26 sorry markers in core theorems under active development").
### C5: NaN Sentinel Collision (Silent Data Corruption)
**Files:** `BindServer.lean` (Lean side), `manifold_binary.h` (C side)
**Finding:** Lean uses `0xFFFFFFFF` as NaN sentinel. C interprets `0xFFFFFFFF` as a valid large positive integer. On overflow, Lean sends "NaN", C receives a valid number.
**Impact:** Overflow errors become silently wrong data instead of errors.
**Fix:** Use IEEE 754 NaN encoding on both sides, or explicit error flags.
### C6: Eigensolid Convergence Theorem Is a Tautology
**File:** `BraidEigensolid.lean`
**Finding:** The flagship compressor correctness theorem `eigensolid_convergence` literally restates its hypothesis (`h_eig`). It proves nothing. Cited as complete across multiple documents.
**Impact:** A core correctness claim is vacuous.
**Fix:** Either prove it properly or downgrade the claim to a conjecture.
### C7: 74% CI Failure Rate (Systemic Unreliability)
**Files:** `.github/workflows/`
**Finding:** Math-First Checks, Pages Build, and Batch Compute workflows fail consistently. Only Wolfram Alpha verification passes. `.pre-commit-config.yaml` is referenced by CI but **does not exist**.
**Impact:** Every push to main has a 74% chance of failing CI. This trains developers to ignore CI.
**Fix:** Fix the 3 broken workflows. Create `.pre-commit-config.yaml`.
---
## The 12 High Issues
### H1: IsSidonSet Defined Twice (Lean)
Two different definitions in `SidonSets.lean` and `ErdosRenyiPipeline.lean` with slightly different signatures. Any theorem using one won't work with the other.
### H2: SQL Injection Pattern (Python)
`finance_manager.py` lines 46, 62-64: f-string SQL with user input. Unfixed despite PR #76 claiming to patch it.
### H3: Command Injection (Python)
`verify_all_shims.py` uses `subprocess` with `shell=True` and user-controlled paths.
### H4: Duplicate q16.py (Python)
Two copies (`lib/q16.py` and `auto/lib/q16.py`) with different subsets of operations. Import ambiguity.
### H5: Stats_show Destructive Read (C)
`pist_neuromorphic.c`: `stats_show()` mutates frequency data during read. Subsequent reads return wrong values.
### H6: AGENTS.md References Non-Existent Components
The 27KB AGENTS.md describes extracted/verified components that don't exist in the codebase.
### H7: No Q16_16 Roundtrip Test
The full Lean→Python→C→Lean data path is completely untested in CI.
### H8: 66 Large Files in Git (Not LFS)
44.88 MB PDF, 25 MB GIF (duplicated), 187 MB WAV files, 24 MB compressed file. Should be in Git LFS.
### H9: 192 Build Artifacts Committed to Main
`.pist` and `.pist.meta` files are generated by Lean build but committed to git. Should be `.gitignore`d.
### H10: Dependencies Unpinned
`requirements.txt` uses `>=` for 20+ critical deps (qiskit, numpy, scipy) with no lock files.
### H11: 111 Misplaced Files
Documentation scattered in core formalism (24 files) and applications (75 files) instead of `6-Documentation/`.
### H12: NoDupeLabs Duplicated (1,029 Files)
Full project copied in both `4-Infrastructure/` and `5-Applications/`. 100+ confirmed identical via git blob hashes.
---
## Per-Dimension Breakdown
### Lean Formalism (1,295 files)
- 26+ `sorry` markers across core theorems
- T1_Coherence.lean: 12 sorry (the hardest — Chentsov-level)
- ErdosRenyiPipeline.lean: 6 sorry
- E8Sidon.lean: 5 sorry
- 4 duplicate definitions detected
- 220 naming convention violations (mostly lowercase_snake in Lean where PascalCase expected)
- ~119 files under 500 bytes (likely stubs)
### Infrastructure (Python/Rust/C/Shell)
- 3 secrets found (1 critical API key)
- 6 security issues (SQL injection, command injection, unsafe cast)
- 3 dead code functions
- 2 broken imports
- 3 path mismatches
- 2 build problems
### Documentation (1,956 Markdown files)
- 8 stale claims (including "3,500+ proofs")
- 16 broken cross-references
- 8 old TODOs (>2 months)
- 45 duplicate documentation pairs
- 15 empty/minimal READMEs
- 6 undocumented major modules
### Integration (Lean ↔ Python ↔ C)
- 18 integration points identified
- 3 critical type mismatches (Q16_16 rounding)
- 7 error handling gaps
- 2 broken CLI contracts
- 5 workflow gaps
- 2 race conditions
### Quality (CI/Tests/Cleanup)
- CI failure rate: 74%
- Only 2 actual pytest files out of 1,282 "test" named files
- 627 duplicate basenames
- 57 experimental files on main
- 66 large files (>1MB)
- 101 binary files in git
- ~297 files needing cleanup
### Consistency (Organization/Naming)
- 220 naming violations
- 111 misplaced files
- 5 version skew issues
- 2 dead symlinks
- 441 duplicate files
- 4 removed feature references
- 179 gitignore gaps
---
## The Brutal Truth
This is not a codebase that's ready for external use. It's a **research notebook** that has grown to 9,606 objects across 6 architecture layers. The core mathematical insight — chaos game + Sidon + Chentsov + Hachimoji — is sound and genuinely novel. But the implementation around it has accumulated 10 iterations of debris.
**What works:**
- ChentsovFinite.lean (883 lines, 0 sorry) — the keystone theorem
- HachimojiSubstitution.lean — the 8-state encoding with bijection
- qaoa_adapter.py — the QUBO ↔ QAOA bridge (solid engineering)
- The 6-layer architecture concept (even if the files are misplaced)
**What needs immediate attention:**
1. Revoke the API key (C1) — 5 minutes
2. Fix Q16_16 rounding to be canonical (C2) — 1 day
3. Delete or generate the missing files that receipts claim exist (C3) — 1 day
4. Fix the 3 broken CI workflows (C7) — 1 day
5. Remove 1,029 duplicate NoDuPeLabs files (H12) — 30 minutes
**What needs a focused cleanup sprint:**
- All 26 sorry markers in core theorems
- The SQL injection and command injection
- The 66 large files → Git LFS
- The 192 build artifacts → .gitignore
- The 111 misplaced files → correct directories
The ship in the bottle is still impressive. But the bottle has accumulated 10 layers of dust, a hardcoded API key, and 441 duplicate planks. Time to clean the glass.
---
*Audit conducted: June 21, 2026*
*Auditors: 6 parallel specialist agents*
*Objects inspected: 9,606*
*Findings: 2,068 lines across 6 reports*
*This synthesis: 1 report bringing all findings into focus*

271
audit/consistency_audit.md Normal file
View file

@ -0,0 +1,271 @@
# Consistency Audit: Research-Stack Repository
**Repository:** https://github.com/allaunthefox/Research-Stack
**Branch:** main
**Audit Date:** 2025-06-21
**Scope:** ALL 8,449 tracked files across entire repository
---
## Summary
| Category | Count | Severity |
|----------|-------|----------|
| Naming convention violations | **220** | Medium |
| Misplaced files | **111** | High |
| Version skew issues | **5** | Medium |
| Dead symlinks | **2** | Low |
| Duplicate content sets | **441** | High |
| Removed feature references | **4** | Low |
| Gitignore gaps | **179** | Medium |
**Total issues:** 962
**Critical:** 0 blocking
**High:** 2 categories (misplaced files, duplicates)
---
## Critical Issues
None identified. No blocking inconsistencies that prevent builds or cause data loss.
---
## High Severity Issues
### H1: NoDupeLabs Code Duplication Across Layers (530 + 499 files)
The NoDupeLabs project exists as near-identical copies in **both** `4-Infrastructure/NoDupeLabs/` (530 files) and `5-Applications/nodupe/` (499 files). This is the single largest source of repository bloat from iteration drift.
**Evidence (git blob hashes match):**
- `4-Infrastructure/NoDupeLabs/tests/core/test_database_comprehensive.py` == `5-Applications/nodupe/tests/core/test_database_comprehensive.py` (109KB each)
- `4-Infrastructure/NoDupeLabs/.integrity/SHA512SUMS.txt` == `5-Applications/nodupe/.integrity/SHA512SUMS.txt` (101KB each)
- `4-Infrastructure/NoDupeLabs/tests/core/test_coverage_100_percent.py` == `5-Applications/nodupe/tests/core/test_coverage_100_percent.py` (84KB each)
- 100+ more files with identical SHA hashes
**Recommended action:** Determine which is canonical (likely `4-Infrastructure/NoDupeLabs/` per ARCHITECTURE.md) and remove the `5-Applications/nodupe/` copy. Add a README explaining the canonical location.
### H2: 26MB GIF Duplicated in text-to-cad
`5-Applications/text-to-cad/skills/cad/assets/text-to-cad-demo.gif` (25.1MB) and `5-Applications/text-to-cad/skills/urdf/assets/text-to-cad-demo.gif` (25.1MB) are identical content. Total waste: **26MB**.
**Recommended action:** Symlink or reference a single canonical asset location.
### H3: 111 Misplaced Files Across Layers
Files are located in directories that do not match their layer's architectural purpose per ARCHITECTURE.md. The largest category is documentation markdown files (99 files) misplaced in `0-Core-Formalism/` (24 files) and `5-Applications/` (75 files).
---
## Medium Severity Issues
### M1: Naming Convention Violations (220 files)
**AGENTS.md convention:** PascalCase types, camelCase functions. Lean modules should use PascalCase.
**Lean files with lowercase_snake names (213 files):**
- Test/debug files: `debug_eval.lean`, `test_native_decide.lean`, `braided_field_sim.lean`
- AlphaProofNexus adapters: 100+ files like `erdos_12.parts.i.lean`, `erdos_125.variants.positive_lower_density.lean`, `graph_conjecture2.lean`, `green_57.lean`
- Extension scaffold files: `bipartite_reconstruction.lean`, `green_tao_5_4.lean`, etc.
**Python files with PascalCase names (7 files):**
- `1-Distributed-Systems/agents/claw/src/QueryEngine.py`
- `1-Distributed-Systems/agents/claw/src/Tool.py`
- `2-Search-Space/search/whoogle-search/misc/update-translations.py`
- `2-Search-Space/simulations/Newtonian-Superfluid-Simulation/AtomSim.py`
- `2-Search-Space/simulations/Newtonian-Superfluid-Simulation/Galaxy.py`
- `2-Search-Space/simulations/Newtonian-Superfluid-Simulation/GalaxyRing.py`
- `2-Search-Space/simulations/Newtonian-Superfluid-Simulation/Universe.py`
**Recommended action:** Rename Lean modules to PascalCase. Rename Python modules to snake_case per PEP 8.
### M2: Gitignore Gaps (179 files)
The `.gitignore` file is comprehensive (260+ patterns) but **179 files** that match gitignore patterns are still committed:
| Category | Count | Examples |
|----------|-------|----------|
| AI tool configs | 11 | `.vscode/`, `.cursor/`, `.devin/`, `.roo/`, `.windsurf/` files |
| `shared-data/` directory | 164 | Receipts, benchmarks, blockchain corpus |
| Root symlinks | 1 | `result-devcontainer` |
| Quarantine files | 3 | `.quarantine` files |
**Recommended action:** These files were likely force-added via `git add -f` or added before patterns were created. Run `git rm --cached` for truly generated files. For `shared-data/`, either remove from git (if truly generated) or remove from `.gitignore`.
### M3: Version Skew - Multiple lakefile Formats (5 files)
Five `lakefile.*` files exist with **different formats**, suggesting version drift:
| File | Format | Status |
|------|--------|--------|
| `0-Core-Formalism/lean/Semantics/lakefile.toml` | TOML | **Canonical** - main workspace |
| `0-Core-Formalism/otom/tools/lean/Semantics/lakefile.lean` | Lean | **Legacy format** - should migrate to TOML |
| `0-Core-Formalism/lean/external/OTOM/lakefile.toml` | TOML | External dependency |
| `0-Core-Formalism/lean/singer-theorem-lean/lakefile.toml` | TOML | Separate project |
| `lean_binned/lakefile.toml` | TOML | Separate project |
**Recommended action:** Migrate `lakefile.lean` to `lakefile.toml` format for consistency.
### M4: Duplicate Semantics Module Names (32 pairs)
32 Lean modules have **duplicate filenames** in different directories within `0-Core-Formalism/lean/Semantics/`. These may have diverged or be stale copies:
| Filename | Locations |
|----------|-----------|
| `Bind.lean` | `Semantics/` and `Semantics/Components/` |
| `Core.lean` | `ExtensionScaffold/Compression/` and `Semantics/Components/` and `Semantics/HCMMR/` and `Semantics/InvariantReceipt/` and `Semantics/TMMCP/` |
| `Bridge.lean` | `Semantics/Adapters/AlphaProofNexus/` and `Semantics/HCMMR/` |
| `ReceiptCore.lean` | `Semantics/` and `otom/tools/lean/Semantics/Semantics/` |
| `Constitution.lean` | `Semantics/` and `otom/tools/lean/Semantics/Semantics/` |
| `FAMM.lean` | `Semantics/` and `otom/tools/lean/Semantics/Semantics/` |
**Recommended action:** Audit each pair to determine which is canonical. Remove or rename stale copies.
---
## Low Severity Issues
### L1: Dead Symlinks (2)
| Symlink | Target | Issue |
|---------|--------|-------|
| `4-Infrastructure/bin/share` | `/home/allaun/Research Stack/tools/bin/nextpnr-himbaechel-share` | Absolute path to author's local machine |
| `result-devcontainer` | `/nix/store/iajh1kzizdnb8ih88wd0rczdqmyg456v-research-stack-otom.tar.gz` | Absolute nix store path (GC may delete) |
**Recommended action:** Replace absolute symlinks with relative paths or add a setup script.
### L2: Legacy Directory Content (4 files)
`0-Core-Formalism/lean/Semantics/legacy/` contains 4 files that reference deprecated concepts. The `.gitignore` explicitly excludes `0-Core-Formalism/lean/Semantics/Ancillary/LegacyQuarantine/` but these are in a different `legacy/` directory.
Files:
- `0-Core-Formalism/lean/Semantics/legacy/6point5sigma/HamiltonianMechanics.lean`
- `0-Core-Formalism/lean/Semantics/legacy/6point5sigma/plan.md`
- `0-Core-Formalism/lean/Semantics/legacy/6point5sigma/HamiltonianMechanics.graphml`
- `0-Core-Formalism/lean/Semantics/legacy/RealityContractMassNumber.lean`
### L3: OpenClaw References
OpenClaw was decommissioned per AGENTS.md (2026-06-20). No references found in code. The `.gitignore` correctly excludes `5-Applications/tools-scripts/external/openclaw/`. Clean removal verified.
### L4: Large Files in Repository (67 files > 1MB)
The repository contains 67 files larger than 1MB (total: ~370MB). Git does not handle large files well. Consider using Git LFS for:
- `shared-data/papers/2026-05/2511.21459.pdf` (44.9MB)
- `5-Applications/text-to-cad/skills/*/assets/text-to-cad-demo.gif` (25.1MB each)
- `3-Mathematical-Models/equations_compressed/*.compressed` (24.2MB)
- `4-Infrastructure/hardware/cff_accelerator.json` (13.8MB)
- 11 WAV audio files in `2-Search-Space/simulations/matter-frequencies/` (11MB each)
---
## Per-Directory Breakdown
### `0-Core-Formalism/` (1,602 files) - Core Formalism Layer
**Issues found:**
- 24 markdown docs that should be in `6-Documentation/`
- 213 Lean files with lowercase_snake names (should be PascalCase)
- 1 AGENTS.md that belongs at repo root
- 4 legacy files referencing deprecated concepts
- 32 duplicate module names (same filename in different subdirs)
- 2 lakefiles with potential version skew
- 1 Rust project (`ftdi_gimbal/`) in formalism layer
- Quarantine files: `Q064Experimental.lean`, 3 `.quarantine` files
### `1-Distributed-Systems/` (207 files)
**Issues found:**
- 2 Python files with PascalCase names (`QueryEngine.py`, `Tool.py`)
- Cargo.toml workspace nesting is normal (workspace with member crates)
### `2-Search-Space/` (1,627 files)
**Issues found:**
- 4 Python files with PascalCase names in `Newtonian-Superfluid-Simulation/`
- 1 Python file with hyphens (`update-translations.py`)
- Large WAV files (11MB each) should use Git LFS
- Duplicate SVG assets (big-logo.svg / biglogo-with-text.svg)
### `3-Mathematical-Models/` (171 files)
**Issues found:**
- 1 large compressed file (24.2MB) should use Git LFS
### `4-Infrastructure/` (1,419 files)
**Issues found:**
- 1 dead symlink (`bin/share` -> absolute path)
- 530 NoDupeLabs files duplicated in `5-Applications/nodupe/`
- 1 large JSON file (`hardware/cff_accelerator.json`, 13.8MB)
### `5-Applications/` (1,281 files)
**Issues found:**
- 1 Python script at root (`fix_offloat.py`) should be here
- 75 markdown docs (hutter_prize docs) that should be in `6-Documentation/`
- 499 NoDupeLabs files duplicated from `4-Infrastructure/NoDupeLabs/`
- 1 dead symlink (`result-devcontainer`)
- 26MB GIF duplicated in text-to-cad
- Verilog files (`out/verilog/*.v`) should be in `4-Infrastructure/hardware/`
### `6-Documentation/` (1,586 files)
**Issues found:**
- 6 Lean files in `docs/geoweird/` that should be in `0-Core-Formalism/lean/`
- 2 Lean files in `invention_record/` that should be in `0-Core-Formalism/lean/`
- 1 quarantine file (`DRIFT_QUARANTINE_YANG_MILLS_SPEC.md`)
### `6-Kernel-Shim/` (not in main tree count)
**Issues found:**
- 2 C kernel modules (`pist_compress.c`, `pist_neuromorphic.c`) should be in `4-Infrastructure/`
### Root Level (96 files)
**Issues found:**
- 1 Python script (`fix_offloat.py`) at root
- 1 dead symlink (`result-devcontainer`)
- 1 data symlink (`data`)
- 2 duplicate README.md entries at root (git artifact)
### Dot-Directories (88 files)
**Issues found:**
- 11 AI tool config files committed despite being in `.gitignore`
- `.devin/skills/lean-proof/SKILL.md` is intentionally committed (skill for agents) but parent `.devin/` is gitignored -- this creates confusion
---
## Recommendations by Priority
### Immediate (this week)
1. **Remove NoDupeLabs duplicate** from `5-Applications/nodupe/` (499 files, ~2MB)
2. **Deduplicate text-to-cad GIF** (save 26MB)
3. **Fix dead symlinks** - make relative or document
### Short-term (this month)
4. **Move markdown docs** from `0-Core-Formalism/` and `5-Applications/` to `6-Documentation/`
5. **Move C kernel modules** from `6-Kernel-Shim/` to `4-Infrastructure/`
6. **Clean up `.quarantine` files** (3 files)
7. **Migrate `lakefile.lean`** to `lakefile.toml`
### Medium-term (next quarter)
8. **Audit 32 duplicate Semantics modules** - determine canonical versions
9. **Rename Lean files** to PascalCase (213 files)
10. **Rename Python files** to snake_case (7 files)
11. **Set up Git LFS** for large files (>1MB)
12. **Clean up `shared-data/`** - either remove from git or remove from `.gitignore`
---
## Appendix: Methodology
1. Read AGENTS.md for naming conventions
2. Read ARCHITECTURE.md for layer structure
3. Parsed `audit_file_tree.json` (8,449 files)
4. Queried GitHub API for git tree blob hashes (9,661 objects)
5. Queried GitHub API for symlink targets
6. Checked `.gitignore` against committed files
7. Cross-referenced file paths against layer architecture

335
audit/documentation_audit.md Normal file
View file

@ -0,0 +1,335 @@
# Documentation Audit — Research Stack (OTOM)
**Audit Date:** 2026-06-22
**Scope:** All .md files (1,956), .yaml/.yml files (172), .lean files (1,295), and documentation directories
**Methodology:** Cross-referencing documentation claims against actual repository contents via GitHub raw URLs and file tree analysis
---
## Summary
| Metric | Count |
|--------|-------|
| Total .md files audited | 1,956 |
| Total .lean files | 1,295 |
| Stale claims | 8 |
| Broken cross-references | 16 |
| Old TODOs (unaddressed >2 months) | 8 |
| Duplicate documentation pairs | 45 (16 docs + 29 obsidian-vault) |
| Empty/minimal READMEs | 15 |
| Undocumented major modules | 6 |
| AGENTS.md files (potential conflict) | 7 |
**Overall Assessment:** The documentation set is extensive (1,956 markdown files, ~9.3MB in 6-Documentation/ alone) but suffers from significant staleness, broken cross-references, inflated proof claims, duplicate content across multiple directory trees, and receipts that describe files and test results that do not exist in the repository.
---
## Critical Issues
### C1: E2E and library Receipts Describe Non-Existent Files
**Files:** `e2e/E2E_MASTER_RECEIPT.md`, `library/CONCEPTUAL_UPGRADE_RECEIPT.md`
**Severity: CRITICAL**
Both receipt files claim detailed test results and reference source files that do not exist:
- `e2e/` directory is **completely empty** (0 files), yet `E2E_MASTER_RECEIPT.md` describes:
- `e2e/E2EMasterTrace.lean` (~540 lines)
- `e2e/run_e2e_trace.py` (~650 lines)
- Step-by-step execution traces with theorem names and line numbers
- Receipt SHA-256: `c8ad995a0fdd9bd0160ae5e20ca27b89a5ca759ef0465b7d0472d0901b3efcfa`
- `library/` directory is **completely empty** (0 files), yet `CONCEPTUAL_UPGRADE_RECEIPT.md` describes:
- `library/hachimoji_codec_v2.py` — "17/17 PASSED"
- `library/HachimojiCodecV2.lean` — "4 theorems proven"
- `library/counterexample_detector.py` — "10/10 PASSED"
- All test claims are unverifiable
**Impact:** These receipts are fabrication — they document code and test results that were never committed to the repository. Any downstream consumer trusting these receipts is being misled.
---
### C2: "3,500+ Proofs" Claim is Inflated
**Files:** `README.md`, `EXPLANATION_FOR_HUMANS.md`, `GETTING_STARTED.md`
**Severity: CRITICAL**
Multiple documents claim:
- EXPLANATION_FOR_HUMANS.md: "3,500+ strict mathematical proofs" and "checked against 3,500+ strict mathematical proofs"
- README.md: "746 verified Lean modules"
- GETTING_STARTED.md: "3,500+ verified proofs" and "all 3,500+ proofs are verified"
**Reality:**
- There are 1,295 `.lean` files, not 746 "verified modules"
- The "3,500" number matches the **build job count** at various points in time (3,314 / 3,529 / 3,592 / 8,332 jobs), not individual proof theorems
- Build jobs are compilation units (module imports, definitions, structures), not proof theorems
- Many `.lean` files contain only `def`, `structure`, `#eval` statements with no `theorem` or `lemma`
- Foundations files like `CarnotEfficiency.lean` (377 bytes) are just a single definition with `#eval` — no theorem
- `LandauerBound.lean` (457 bytes) uses a placeholder `kB` value (`ofRawInt 6`) with comment "Simplified kB" — not physically meaningful
**Impact:** This claim misleads readers about the maturity and depth of the formalization. Conflating build jobs with proof theorems is a significant misrepresentation.
---
### C3: `eigensolid_convergence` Theorem is a Tautology
**File:** `0-Core-Formalism/lean/Semantics/Semantics/BraidEigensolid.lean`
**Severity: CRITICAL**
The flagship theorem, referenced throughout documentation (AGENTS.md, ARCHITECTURE.md, README.md) as proof of compressor correctness:
```lean
theorem eigensolid_convergence
(s : BraidState)
(h_eig : IsEigensolid (crossStep s)) :
∀ i : Fin 8, (crossStep (crossStep s)).strands i = (crossStep s).strands i :=
h_eig
```
This theorem **literally restates its hypothesis**. `IsEigensolid (crossStep s)` means exactly `∀ i, (crossStep (crossStep s)).strands i = (crossStep s).strands i`. The "proof" is just returning the hypothesis.
**Impact:** The core compressor convergence guarantee is vacuous. The theorem proves nothing beyond what was assumed. ARCHITECTURE.md section 13 and TODO_MAP.md B11 both cite this as a completed proof.
---
### C4: CONCEPTS.md Referenced but Missing
**Files:** `GETTING_STARTED.md` (section 6), `ARCHITECTURE.md` (section 10)
**Severity: HIGH**
`CONCEPTS.md` is listed as a "Key File to Read First" in GETTING_STARTED.md and linked from ARCHITECTURE.md's "Further Reading" section. The file **does not exist** in the repository.
---
### C5: Circular Reference in docs/README.md
**File:** `docs/README.md` (also `6-Documentation/docs/README.md` — duplicate)
**Severity: HIGH**
The README states:
> "The authoritative documentation tree is [6-Documentation/docs/](../6-Documentation/docs/)."
But this file **IS** in `6-Documentation/docs/`. It points to itself via a relative path. This is a broken self-reference that would confuse any reader.
---
## Warnings
### W1: Duplicate Documentation (45+ files)
**Severity: HIGH**
| Duplicate Set | Count | Locations |
|--------------|-------|-----------|
| docs/ ↔ 6-Documentation/docs/ | 16 files | `README.md`, `WIKI.md`, `rrc_equation_classification.md`, `roadmaps/RESEARCH_STACK_FOREST_MAP_WATERFALL.md`, etc. |
| obsidian-vault/ ↔ 6-Documentation/wiki/obsidian-vault/ | 29 files | Complete layer READMEs (L0-L6), main vault README |
The root-level `docs/` and `obsidian-vault/` directories appear to be stale copies of the authoritative `6-Documentation/` tree. The `docs/README.md` even admits: "This directory is a legacy alias." Yet 16 files and 29 obsidian-vault files remain duplicated, creating confusion about which is authoritative.
**Risk:** Readers may find stale copies first, and edits to one may not propagate to the other.
---
### W2: Inconsistent Build Job Counts Across Documents
**Severity: MEDIUM**
| Document | Claimed Jobs | Context |
|----------|-------------|---------|
| README.md | 3,314 | "lake build Compiler" |
| ARCHITECTURE.md | 8,332 | "full workspace" |
| ARCHITECTURE.md | 3,314 | "Compiler surface" |
| AGENTS.md | 3,314 | "Compiler surface" (commit e61bb627) |
| TODO_MAP.md | 3,529 | "deterministic build receipt" |
| TODO_MAP.md | 3,592 | "build jobs green" |
| CHANGELOG.md | 3,529 | "deterministic build receipt" |
Different documents cite different commit hashes for these numbers. There is no single source of truth for the current build status.
---
### W3: 7 AGENTS.md Files with Potential Overlap/Conflict
**Severity: MEDIUM**
| File | Size |
|------|------|
| `AGENTS.md` (root) | 28,853 bytes |
| `6-Documentation/docs/AGENTS.md` | 48,594 bytes |
| `0-Core-Formalism/lean/Semantics/AGENTS.md` | 38,223 bytes |
| `4-Infrastructure/AGENTS.md` | 27,403 bytes |
| `5-Applications/text-to-cad/AGENTS.md` | 7,740 bytes |
| `scripts/qc-flag/AGENTS.md` | 2,414 bytes |
| `shared-data/artifacts/lean_expert_agent/AGENTS.md` | 2,893 bytes |
Total: ~156KB of agent instructions. Root AGENTS.md directs to nested ones, but there's no mechanism ensuring consistency. The root file and 6-Documentation/docs/AGENTS.md are the largest and may contain conflicting guidance.
---
### W4: 15 Empty or Minimal READMEs
**Severity: MEDIUM**
The following READMEs are under 500 bytes and provide no useful guidance:
| File | Size | Issue |
|------|------|-------|
| `0-Core-Formalism/lean/Semantics/README.md` | 11 bytes | Just "# Semantics" |
| `2-Search-Space/GhostPivot/README.md` | 31 bytes | Nearly empty |
| `2-Search-Space/simulations/chunked-audio-DSP/README.md` | 70 bytes | Nearly empty |
| `5-Applications/audio-dsp/README.md` | 70 bytes | Nearly empty |
| `6-Documentation/docs/README.md` | 311 bytes | Circular reference only |
| `docs/README.md` | 311 bytes | Circular reference only |
| `pending/lean_unification/README.md` | 446 bytes | Minimal |
| `3-Mathematical-Models/genetics/parametric-learn/README.md` | 493 bytes | Minimal |
These create navigation dead-ends for explorers.
---
### W5: TODO_MAP.md Staleness
**Severity: MEDIUM**
TODO_MAP.md is dated "2026-04-24" (nearly 2 months old). Items marked:
- ✅ "DONE" that reference **missing files** (equations_forest.jsonl, supernodes.json)
- 🔄 "IN_PROGRESS" for months with no evidence of progress
- 📋 "TODO" items (B5-B9, C1-C4, F1-F5, G1-G6) untouched since creation
- ⏳ "BLOCKED" items with no unblock pathway documented
The "Metrics" table at the bottom shows many targets unmet (e.g., "Equations in registry: 200+ | 0", "Supernodes: 30-45 | 0", "Foundation kernel theorems: 12 | ~3 partial").
---
### W6: AGENTS.md Contains Local Deployment Details
**Severity: LOW**
Root AGENTS.md contains:
- Personal IP addresses (`100.88.57.96`, `100.92.88.64`)
- Tailscale hostnames (`qfox-1`, `neon-64gb`)
- Local file paths (`/home/allaun/`, `~/.hermes/`)
- Hardware details specific to the author's setup (RTX 4070, CachyOS)
This information is only relevant to the original author and serves no purpose for external contributors.
---
### W7: Wrong Path in TODO_MAP.md for Foundations/
**Severity: LOW**
TODO_MAP.md section B1 references:
```
0-Core-Formalism/lean/Semantics/Foundations/ShannonEntropy.lean
```
Actual path in repository:
```
0-Core-Formalism/lean/Semantics/Semantics/Foundations/ShannonEntropy.lean
```
The `Semantics/` namespace is duplicated. This indicates a namespace refactoring occurred without updating documentation.
---
## Per-Doc Breakdown
### README.md (root)
- **Stale claim:** "746 verified Lean modules" — count is not verifiable
- **Stale claim:** "3,314-job deterministic lake build Compiler" — job count varies across docs
- **Broken ref:** "Gremlin mathblob database" with "14,449 vertices and 29,379 edges" — unverifiable
- **Grade:** B- (Good structure but inflated metrics)
### EXPLANATION_FOR_HUMANS.md
- **Stale claim:** "3,500+ strict mathematical proofs" — conflates build jobs with theorems
- **Stale claim:** "There are zero errors" — refers to build, not proofs
- **Grade:** C+ (Good plain-English explanation but propagates inflated proof count)
### ARCHITECTURE.md
- **Stale claim:** "8332 jobs full workspace, 3314 jobs Compiler surface, 0 errors" — job count inconsistent
- **Broken ref:** `CONCEPTS.md` in "Further Reading" section 10
- **Broken ref:** `.devcontainer/flake.nix` in Storage & Persistence section (only Dockerfile exists)
- **Broken ref:** `4-Infrastructure/infra/credential_server.py` in Infrastructure table
- **Inconsistent:** Section 13 says `receipt_invertible` is **pending**, but TODO_MAP.md B11 says eigensolid convergence is ✅ DONE
- **Grade:** B (Good architecture overview but stale references and inconsistent claim tracking)
### AGENTS.md (root)
- **Stale claim:** "3314 jobs, 0 errors" with commit `e61bb627` — other docs cite different commits
- **Personal info:** Contains local IP addresses, hostnames, personal paths
- **Grade:** B (Good operating rules but contains personal deployment data and stale metrics)
### TODO_MAP.md
- **Old TODOs:** 8 items pending since 2026-04-24
- **False completions:** Items marked ✅ DONE that reference missing files
- **Stale metrics:** "Equations in registry: 0 (ChatGPT sandbox only)" — months old
- **Stale blocker:** "Tang Nano 9K not physically connected" still listed as blocker
- **Grade:** C (Comprehensive but significantly stale; many false completions)
### GETTING_STARTED.md
- **Broken ref:** `CONCEPTS.md` in "Key Files to Read First" table
- **Broken ref:** `5-Applications/hutter_prize/ARCHITECTURE.md` in same table (hutter_prize has its own ARCHITECTURE.md but it's not the system overview)
- **Stale claim:** "3,500+ verified proofs" in build instructions
- **Stale paths:** References `/home/allaun/CascadeProjects/Research-Stack` — author's local path
- **Grade:** B- (Useful setup guide but stale claims and broken refs)
### E2E_MASTER_RECEIPT.md
- **CRITICAL:** References files in `e2e/` directory that is **completely empty**
- **CRITICAL:** Claims 3 PROVEN + 3 COMPUTED + 2 STATED steps with detailed line numbers — all unverifiable
- **CRITICAL:** Claims SHA-256 receipt hash — cannot be verified
- **Fabrication:** Entire document describes a trace through code that does not exist
- **Grade:** F (Receipt for non-existent code)
### CONCEPTUAL_UPGRADE_RECEIPT.md
- **CRITICAL:** References files in `library/` directory that is **completely empty**
- **CRITICAL:** Claims test suite results (17/17, 14/14, 10/10) that cannot be verified
- **Fabrication:** Describes V2 codec with theorems and tests that don't exist in repo
- **Grade:** F (Receipt for non-existent code)
### docs/README.md + 6-Documentation/docs/README.md
- **Circular ref:** Points to 6-Documentation/docs/ which is the SAME directory
- **Grade:** D (Self-referential brokenness)
### CITATION.cff
- **Note:** Contains ~100+ references, many from 2026-06-19 session. Well-structured.
- **Minor issue:** Some references have placeholder/generic notes
- **Grade:** B+ (Good citation management, some entries are recent)
### CLAUDE.md / GEMINI.md
- **Duplicate content:** GEMINI.md appears to be a subset/superset of CLAUDE.md guidance
- **Broken ref:** Points to `AGENTS.md` files but doesn't distinguish between 7 copies
- **Grade:** B- (Useful but could be consolidated)
---
## Recommendations
### Immediate (P0)
1. **Remove or quarantine** `E2E_MASTER_RECEIPT.md` and `CONCEPTUAL_UPGRADE_RECEIPT.md` — they document non-existent code
2. **Fix or remove** the "3,500+ proofs" claim — replace with actual theorem count or clarify "build jobs"
3. **Create `CONCEPTS.md`** or remove references to it
4. **Fix `eigensolid_convergence`** — replace tautology with actual proof or downgrade claim status
### Short-term (P1)
5. **Deduplicate** `docs/` → merge into `6-Documentation/docs/`, then remove root `docs/`
6. **Deduplicate** `obsidian-vault/` → merge into `6-Documentation/wiki/obsidian-vault/`, remove root copy
7. **Consolidate AGENTS.md** — keep one root file, have nested ones reference it explicitly
8. **Remove personal info** from AGENTS.md (IPs, hostnames, local paths)
9. **Update TODO_MAP.md** — mark items referencing missing files as not-done, refresh metrics
10. **Write READMEs** for empty directories (GhostPivot, audio-dsp, etc.)
### Medium-term (P2)
11. **Single source of truth** for build metrics — one file that documents current job count
12. **Automated broken link checker** for cross-references
13. **Documentation freshness dating** — add "last verified" timestamps to key docs
14. **Consolidate CLAUDE.md/GEMINI.md** into single LLM_INSTRUCTIONS.md
---
*Audit completed. 1,956 markdown files, 1,295 Lean files, 172 YAML files analyzed. All findings mapped to specific file paths and verifiable against the repository at `https://github.com/allaunthefox/Research-Stack` branch `main`.*

377
audit/infrastructure_audit.md Normal file
View file

@ -0,0 +1,377 @@
# Infrastructure Audit Report
**Repository:** https://github.com/allaunthefox/Research-Stack
**Branch:** main
**Scope:** 4-Infrastructure/, 5-Applications/, 6-Kernel-Shim/, scripts/
**Audit Date:** 2026-06-02
---
## Summary
| Category | Count | Severity |
|----------|-------|----------|
| Total scoped files | 2,725 | - |
| **Secrets found** | **3** | 1 CRITICAL, 1 HIGH, 1 MEDIUM |
| **Security issues** | **6** | 2 HIGH, 3 MEDIUM, 1 LOW |
| **Dead code functions/regions** | **3** | 3 LOW |
| **Broken imports** | **2** | 1 MEDIUM, 1 LOW |
| **Path mismatches** | **3** | 1 MEDIUM, 2 LOW |
| **Build problems** | **2** | 1 MEDIUM, 1 LOW |
| **Config drift** | **2** | 1 MEDIUM, 1 LOW |
---
## CRITICAL Issues
### C1. Hardcoded Wolfram Alpha API Key (SECRET)
- **File:** `4-Infrastructure/shim/wolfram_verify.py`
- **Line:** `APPID = "HYJE3R3R63"`
- **Severity:** **CRITICAL**
- **Description:** A live Wolfram Alpha API key is hardcoded in plaintext and committed to version control. This key is used to make API calls to `api.wolframalpha.com`. Anyone with repository access can extract and abuse this key, incurring API charges and potentially violating terms of service.
- **Evidence:**
```python
APPID = "HYJE3R3R63"
# ...
url = f"http://api.wolframalpha.com/v2/query?appid={APPID}&input=..."
```
- **Remediation:**
1. **Immediately revoke** the exposed API key at Wolfram Alpha developer portal
2. Replace with: `APPID = os.environ.get("WOLFRAM_APPID", "")`
3. Add `WOLFRAM_APPID` to `.gitignore` and environment setup docs
4. Add secret scanning to CI to prevent future commits
5. Rotate any other keys that may have been exposed
---
## HIGH Severity Issues
### H1. Remote SSH Command Injection via shell=True
- **File:** `4-Infrastructure/shim/verify_all_shims.py`
- **Lines:** `subprocess.run(cmd, shell=True, ...)` (multiple instances)
- **Severity:** **HIGH**
- **Description:** The verification script constructs SSH commands via string concatenation and executes them with `shell=True`. While the current inputs appear hardcoded, the pattern is dangerous. The `run_remote()` function builds: `ssh {user}@{ip} "{cmd}"` where cmd comes from the SHIMS list but could be tampered with.
- **Evidence:**
```python
def run_remote(cmd):
ssh_cmd = f"ssh {CUPFOX_USER}@{CUPFOX_IP} \"{cmd}\""
res = subprocess.run(ssh_cmd, shell=True, capture_output=True, text=True)
```
- **Remediation:**
- Use `paramiko` or `asyncssh` library for SSH connections
- If subprocess is required, use `shell=False` with list args
- Validate all command components against an allowlist
### H2. Hardcoded Remote Infrastructure Credentials
- **File:** `4-Infrastructure/shim/verify_all_shims.py`
- **Lines:** `CUPFOX_IP = "46.232.249.226"`, `CUPFOX_USER = "root"`
- **Severity:** **HIGH**
- **Description:** Production infrastructure IP address and privileged username (root) are hardcoded. Combined with SSH key-based authentication (not visible in file but implied by SSH commands), this exposes production compute node details.
- **Evidence:**
```python
CUPFOX_IP = "46.232.249.226"
CUPFOX_USER = "root"
```
- **Remediation:**
- Move to environment variables: `CUPFOX_IP`, `CUPFOX_USER`
- Use non-privileged user for remote execution
- Document SSH key management in secure vault
---
## MEDIUM Severity Issues
### M1. SQL Injection Pattern in Eigensolid Data Shim
- **File:** `4-Infrastructure/shim/ingest_eigensolid_data.py`
- **Function:** `generate_crossing_weights_insert()`, `generate_eigensolid_snapshot_insert()`, `generate_braid_strand_insert()`
- **Severity:** **MEDIUM**
- **Description:** SQL generator functions use f-string interpolation to construct INSERT statements. While the current `uuid.uuid4()` values are safe, the pattern is dangerous if extended to user-provided data. Note: the `insert_eigensolid_data()` function correctly uses parameterized queries - there is an inconsistency.
- **Evidence:**
```python
def generate_crossing_weights_insert(...):
return f"INSERT INTO ene.crossing_weights ... VALUES ('{cw_id}', '{recipe_id}', ...)"
```
- **Remediation:**
- Remove unsafe SQL generator functions or use parameter placeholders (`%s`)
- Ensure all SQL generation uses parameterized queries consistently
### M2. Broken Import Path Manipulation
- **File:** `4-Infrastructure/shim/qaoa_adapter.py`
- **Lines:** `sys.path.insert(0, ...)`, `from q16 import ...`
- **Severity:** **MEDIUM**
- **Description:** Module uses `sys.path.insert()` to find `q16.py` and `braid_search.py`. If these files are not present in the expected relative locations, the import will fail at runtime. Only partial graceful fallback exists.
- **Evidence:**
```python
_sys.path.insert(0, str(Path(__file__).resolve().parent.parent / "lib"))
_sys.path.insert(0, str(Path(__file__).resolve().parent))
from q16 import Q16_SCALE, from_q16, to_q16
from braid_search import _q16_signed
```
- **Remediation:**
- Package modules properly with `__init__.py`
- Add try/except ImportError with fallback implementations
### M3. Kernel Module const-Cast Undefined Behavior
- **File:** `6-Kernel-Shim/pist_compress.c`
- **Function:** `pist_init_galois_table()`
- **Severity:** **MEDIUM**
- **Description:** The function casts away `const` from `galois_mul_table` to write to it at runtime: `(u8 *)galois_mul_table`. This is undefined behavior in C and potentially a security concern in kernel code.
- **Evidence:**
```c
static const u8 galois_mul_table[256] = { ... };
static void pist_init_galois_table(void) {
u8 *tbl = (u8 *)galois_mul_table; // const cast away
for (...) tbl[i] = p;
}
```
- **Remediation:**
- Remove `const` qualifier from `galois_mul_table`
- Or use a non-const working copy
### M4. Config Drift - Extracted Components Still Referenced
- **File:** `4-Infrastructure/AGENTS.md`
- **Severity:** **MEDIUM**
- **Description:** AGENTS.md states that `kubernetes/`, `k3s-flake/`, `kube/`, `shim/ray-actors/`, `shim/vcn_*.py`, `shim/hermes/` were extracted to `distributed-compute-fabric` repository. However, references to these paths may still exist in code and scripts, causing confusion.
- **Remediation:**
- Audit all remaining references to extracted components
- Update cross-references to point to new repository
- Add deprecation notices where appropriate
### M5. Path Mismatch in Verification Script
- **File:** `4-Infrastructure/shim/verify_all_shims.py`
- **Line:** `local_path = os.path.join("4-Infrastructure/shim", shim)`
- **Severity:** **MEDIUM**
- **Description:** Uses relative path "4-Infrastructure/shim" which assumes script is run from repo root. If run from elsewhere, files won't be found.
- **Remediation:**
```python
script_dir = Path(__file__).resolve().parent
local_path = script_dir / shim
```
---
## LOW Severity Issues
### L1. Kernel Module Non-Destructive Statistics Read
- **File:** `6-Kernel-Shim/pist_neuromorphic.c`
- **Function:** `stats_show()`
- **Severity:** **LOW**
- **Description:** The `stats_show()` function destructively reads `byte_freq` by zeroing entries during the "top 10" loop. This is not thread-safe and corrupts statistics for concurrent readers.
- **Evidence:**
```c
st->byte_freq[max_idx] = 0; /* zero out for next iter (destructive!) */
```
- **Remediation:** Copy array locally before processing. Use `spin_lock_irqsave()` to protect the read.
### L2. Dead Code in Kernel Compression Module
- **File:** `6-Kernel-Shim/pist_compress.c`
- **Functions:** `pist_shifter_hachimoji()`, `pist_shifter_aegis()`, `pist_entropy_approx()`
- **Severity:** **LOW**
- **Description:** Three shifter functions (Hachimoji, AEGIS, Natural DNA) and the entropy approximation function are defined but never called in the compression/decompression paths. Only `pist_shifter_mirror` is actually used in `pist_compress_page()`.
- **Remediation:** Remove unused functions or wire them into the compression engine via the shifter chain bitmask.
### L3. Dead Bit Flags in pist_compress.c
- **File:** `6-Kernel-Shim/pist_compress.c`
- **Severity:** **LOW**
- **Description:** Eight shifter bit flags are defined but only `PIST_SHIFT_PIST_MIRROR` is checked in the compression function.
- **Evidence:**
```c
#define PIST_SHIFT_HACHIMOJI BIT(0) // unused
#define PIST_SHIFT_AEGIS BIT(1) // unused
#define PIST_SHIFT_NATURAL_DNA BIT(2) // unused
#define PIST_SHIFT_PIST_MIRROR BIT(3) // used
#define PIST_SHIFT_PNA BIT(4) // unused
#define PIST_SHIFT_LNA BIT(5) // unused
#define PIST_SHIFT_PRION BIT(6) // unused
#define PIST_SHIFT_GALOIS BIT(7) // unused
```
- **Remediation:** Implement multi-shifter chain or remove unused flags.
### L4. Missing Output Directory Handling
- **File:** `5-Applications/scripts/rgflow_gpu_pipeline.py`
- **Line:** `save_results(flat, Path("out"))`
- **Severity:** **LOW**
- **Description:** Hardcoded output path "out" may not exist. While `out_dir.mkdir()` is called inside `save_results()`, the path is relative to cwd.
- **Remediation:** Use configurable output path with `mkdir(parents=True, exist_ok=True)`.
### L5. Heavy Monolithic requirements.txt
- **File:** `requirements.txt`
- **Severity:** **LOW**
- **Description:** Single requirements.txt includes GPU (wgpu), quantum (qiskit, cirq, perceval-quandela), distributed compute (ray), and database dependencies. Many will fail on systems without specialized hardware.
- **Remediation:**
```
requirements.txt # core only
requirements-gpu.txt # wgpu, CUDA
requirements-quantum.txt # qiskit, cirq, perceval
requirements-db.txt # psycopg2, boto3
```
### L6. AGENTS.md Storage Agent Description Drift
- **File:** `4-Infrastructure/AGENTS.md`
- **Severity:** **LOW**
- **Description:** AGENTS.md describes detailed trigger model for storage_agent.py with specific Q16_16 thresholds and receipt schema. The actual implementation may differ from documentation.
- **Remediation:** Add doc tests or sync documentation with code via automated extraction.
### L7. Potentially Unused Cloudflare WASM Functions
- **File:** `4-Infrastructure/cloudflare/src/lib.rs`
- **Functions:** `reset()`, `derive_scalar()`
- **Severity:** **LOW**
- **Description:** `reset()` and `derive_scalar()` are defined but may not be called from the JavaScript entry point (`index.js`).
- **Remediation:** Verify usage in `index.js` or remove if confirmed unused.
---
## Per-Component Breakdown
### 4-Infrastructure/ (1,420 Python files, 142 Rust files, 18 C files, 68 Shell files, 125 YAML files)
| Component | Files | Critical Issues | Warnings | Notes |
|-----------|-------|----------------|----------|-------|
| `shim/*.py` | ~50 | 1 (wolfram key) | 4 | Core adapter shims |
| `storage/` | ~10 | 0 | 1 | Storage agent subprocess calls |
| `cloudflare/` | 3 | 0 | 1 | WASM edge functions |
| `kernel/` | 2 C files | 0 | 3 | Kernel modules have dead code, const cast |
| `hardware/` | ~20 | 0 | 0 | FPGA/sparkle hardware bring-up |
| `NoDupeLabs/` | ~50 | 0 | 0 | Third-party package |
### 5-Applications/ (142 Rust files)
| Component | Files | Critical Issues | Warnings | Notes |
|-----------|-------|----------------|----------|-------|
| `parquet_compressor/` | ~30 | 0 | 1 | Cargo.toml dependency versions |
| `scripts/` | ~20 | 0 | 1 | Path handling in GPU pipeline |
### 6-Kernel-Shim/ (2 C files mirrored from 4-Infrastructure/kernel/)
| Component | Files | Critical Issues | Warnings | Notes |
|-----------|-------|----------------|----------|-------|
| `pist_compress.c` | 1 | 0 | 2 | Dead code, const cast |
| `pist_neuromorphic.c` | 1 | 0 | 1 | Destructive stats read |
**Note:** The C files in `6-Kernel-Shim/` appear to be mirrors of `4-Infrastructure/kernel/` files. Ensure they are kept in sync or use symlinks/submodules to avoid divergence.
---
## Security Analysis Details
### Python Security Patterns Found
| Pattern | Files | Risk Level | Notes |
|---------|-------|------------|-------|
| `subprocess.run(shell=True)` | verify_all_shims.py | HIGH | Remote SSH commands |
| `subprocess.run()` | storage_agent.py | MEDIUM | Calls to backup scripts |
| f-string SQL construction | ingest_eigensolid_data.py | MEDIUM | Generator functions |
| `eval()` / `exec()` | None found | - | Clean |
| `pickle.loads()` | None found | - | Clean |
| `input()` | None found | - | Clean |
| Hardcoded API key | wolfram_verify.py | CRITICAL | Wolfram Alpha APPID |
### Rust Safety Analysis
| File | unsafe Blocks | Notes |
|------|---------------|-------|
| `cloudflare/src/lib.rs` | 0 | Clean WASM bindings |
| `parquet_compressor/src/*.rs` | TBD (not in scope of read) | Likely has GPU unsafe code |
### C Kernel Safety Analysis
| File | Issue | Severity |
|------|-------|----------|
| `pist_compress.c` | const cast away | MEDIUM |
| `pist_compress.c` | int_sqrt() usage (kernel API) | LOW (verify availability) |
| `pist_neuromorphic.c` | Non-atomic stat read | LOW |
| `pist_neuromorphic.c` | PAGE_SIZE buffer in sysfs show | LOW (potential overflow) |
---
## Build System Analysis
### Cargo.toml (parquet_compressor)
```toml
[dependencies]
parquet = { version = "58.3", default-features = false, features = ["arrow", "zstd"] }
arrow = "58.3"
serde = { version = "1.0", features = ["derive"] }
serde_json = "1.0"
rayon = "1.8"
clap = { version = "4.4", features = ["derive"] }
indicatif = "0.18"
byteorder = "1.5"
sysinfo = "0.30"
tokio = { version = "1.35", features = ["sync", "rt", "rt-multi-thread"] }
anyhow = "1.0"
divsufsort = "2.0"
itertools = "0.14"
flate2 = "1.0"
zstd = "0.13"
wgpu = "0.19"
bytemuck = { version = "1.14", features = ["derive"] }
pollster = "0.3"
chrono = "0.4"
glob = "0.3"
pathdiff = "0.2"
regex = "1.11"
ahash = "0.8"
dashmap = "6.2"
dirs = "5.0"
```
**Issues:**
- `itertools = "0.14"` is very recent (June 2026); may not be stable
- `divsufsort = "2.0"` may have build issues on Windows
- No `Cargo.lock` visible in the tree (should be committed for binaries)
### requirements.txt
**Issues:**
- Monolithic file with 20+ heavy dependencies
- GPU, quantum, and distributed compute deps all in one file
- No version pins (uses `>=` which can break with major version updates)
- `perceval-quandela>=1.2.3` requires proprietary SDK
---
## Remediation Priority Matrix
| Priority | Issue | Effort | File |
|----------|-------|--------|------|
| **P0** | Revoke and rotate Wolfram Alpha API key | 15 min | wolfram_verify.py |
| **P0** | Remove hardcoded key from source | 5 min | wolfram_verify.py |
| **P1** | Fix subprocess shell=True in verify_all_shims.py | 1 hour | verify_all_shims.py |
| **P1** | Move SSH credentials to environment | 30 min | verify_all_shims.py |
| **P2** | Fix SQL injection pattern | 30 min | ingest_eigensolid_data.py |
| **P2** | Fix const cast in kernel module | 15 min | pist_compress.c |
| **P2** | Add try/except for fragile imports | 30 min | qaoa_adapter.py |
| **P3** | Remove dead code from kernel modules | 1 hour | pist_compress.c |
| **P3** | Fix destructive stats read | 30 min | pist_neuromorphic.c |
| **P3** | Split requirements.txt | 30 min | requirements.txt |
| **P4** | Fix relative path assumptions | 30 min | Multiple files |
| **P4** | Sync AGENTS.md with code | 2 hours | AGENTS.md |
---
## Recommendations
1. **Immediate Actions (Today):**
- Revoke the exposed Wolfram Alpha API key
- Remove hardcoded IP/username from verify_all_shims.py
- Run `git filter-repo` or similar to remove secrets from git history
2. **Short-term (This Week):**
- Fix all subprocess shell=True usages
- Fix SQL injection patterns
- Fix kernel module const cast
- Add secret scanning to CI (e.g., `truffleHog` or `git-secrets`)
3. **Medium-term (This Month):**
- Remove dead code from kernel modules
- Split requirements.txt into feature-specific files
- Add proper error handling for missing files/paths
- Sync documentation with actual code
4. **Long-term:**
- Add automated security scanning to CI pipeline
- Implement proper secret management (HashiCorp Vault, AWS Secrets Manager)
- Add unit tests for kernel module sysfs interfaces
- Create integration tests for shim verification pipeline

417
audit/integration_audit.md Normal file
View file

@ -0,0 +1,417 @@
# Integration Audit: Research-Stack Cross-Language Boundaries
## Summary
| Category | Count | Severity |
|----------|-------|----------|
| Integration points identified | 18 | — |
| Critical type mismatches | 3 | CRITICAL |
| Error handling gaps | 7 | HIGH |
| Broken CLI contracts | 2 | HIGH |
| Workflow gaps / missing handoffs | 5 | MEDIUM |
| Race conditions | 2 | MEDIUM |
| Duplicate divergent Q16_16 libraries | 2 | HIGH |
| Generated files not properly managed | 3 | MEDIUM |
| `sorry` in proofs unchecked by CI | 1 | HIGH |
---
## Critical Issues
### C1: Q16_16 Conversion Mismatch — Lean vs. Python vs. C [CRITICAL]
**Files:**
- `0-Core-Formalism/lean/Semantics/Semantics/FixedPoint.lean` (lines 270-290)
- `0-Core-Formalism/lean/Semantics/BindServer.lean` (lines 33-44)
- `4-Infrastructure/lib/q16.py`
- `4-Infrastructure/auto/lib/q16.py`
- `0-Core-Formalism/core/include/manifold_binary.h` (lines 52-60)
**Issue:** Three different Q16_16 float conversion algorithms exist across the boundary:
1. **Lean `FixedPoint.lean`**: Uses `(f * 65536.0).floor` — rounds down (truncates toward zero)
2. **Lean `BindServer.lean`**: Uses `(f * 65536.0).floor.toUInt32` — same floor, but goes through UInt32 with saturation at 0xFFFFFFFF/0x80000000
3. **Python `q16.py`**: Uses `int(round(value * 65536))` — rounds to nearest (banker's rounding for .5)
4. **C `manifold_binary.h`**: Uses `(q16_16_t)(f * (1 << 16))` — C cast truncates toward zero
**Impact:** Values near half-LSB boundaries (e.g., 1.00001) will diverge. A value of `1.5 / 65536.0 = 0.000022888...` will be:
- Lean (floor): `1` (raw 65536)
- Python (round): `2` (raw 131072)
- C (truncation): `1` (raw 65536)
This affects all data flowing through the pipeline: spectral profiles, Sidon addresses, QUBO coefficients, and braid parameters.
**Recommendation:** Unify on a single conversion spec. The Lean `floor` approach is the most conservative and is formally specified; Python and C should match it.
---
### C2: Duplicate Divergent Q16_16 Python Libraries [CRITICAL]
**Files:**
- `4-Infrastructure/lib/q16.py` (1494 bytes, has `q16_add`, `q16_sub`, `q16_mul`, `q16_div`)
- `4-Infrastructure/auto/lib/q16.py` (910 bytes, MISSING arithmetic ops)
**Issue:** Two copies of the Q16_16 Python library exist. The `auto/` version is a strict subset — it lacks `q16_add`, `q16_sub`, `q16_mul`, `q16_div`, `q16_gt`, `q16_ge`. Scripts importing from `auto/lib/` will fail at runtime if they call any arithmetic function.
Both use the same module name `q16`, creating import ambiguity depending on `sys.path` ordering.
**Impact:** Runtime `AttributeError` when arithmetic is attempted via the `auto/` copy. The `qaoa_adapter.py` imports from `../lib` but other shims may import from `auto/lib`.
**Recommendation:** Delete the `auto/lib/q16.py` stub or make it a re-export of the canonical `lib/q16.py`.
---
### C3: Lean `BindServer` JSON Parsing Lacks Error Handling on Float Overflow [CRITICAL]
**File:** `0-Core-Formalism/lean/Semantics/BindServer.lean` (lines 33-44)
```lean
@[inline]
def q16_16_of_float (f : Float) : UInt32 :=
if f.isNaN || f >= 32768.0 then 0xFFFFFFFF
else if f <= -32768.0 then 0x80000000
else (f * 65536.0).floor.toUInt32
```
**Issue:** The `0xFFFFFFFF` sentinel for NaN/overflow is indistinguishable from the bit pattern for `-1/65536.0` in two's complement. When this UInt32 flows to C via JSON, `manifold_binary.h`'s `q16_16_from_float` does NOT check for this sentinel — it will interpret 0xFFFFFFFF as `(float)0xFFFFFFFF / 65536.0 = 65535.999985` instead of signaling an error.
**Impact:** Silent data corruption on NaN/overflow inputs. The C side has no way to detect that a sentinel value was transmitted.
**Recommendation:** Use an explicit JSON error field instead of a bit-pattern sentinel. Or, have the C side validate against 0xFFFFFFFF and return an error code.
---
### C4: `sorry` in Generated Lean Theorems Never Checked by CI [HIGH]
**Files:**
- `4-Infrastructure/shim/eigensolid_pipeline.py` (lines 270-310, Lean generation code)
- `.github/workflows/math-check.yml`
**Issue:** The `eigensolid_pipeline.py` generates Lean theorems where every proof body is `sorry`:
```lean
theorem symmetry_violation_0 : Prop := by
sorry
```
The CI `math-check.yml` validates JSON schemas, DeepSeek receipts, and claims registries — but does NOT attempt to build or lint the generated `.lean` files. The `sorry` axioms accumulate unverified claims into the codebase.
**Impact:** Generated theorems provide false confidence. A downstream proof that depends on these `sorry` theorems will silently accept any conclusion.
**Recommendation:** Add a CI step that runs `lake build` on generated Lean files and rejects files containing `sorry` in theorem bodies.
---
## Warnings
### W1: `lean_trace_bridge.py` — No Exit Code Check from Proof Worker [HIGH]
**File:** `4-Infrastructure/shim/lean_trace_bridge.py` (lines 118-140)
```python
def prove_step(code: str, timeout_s: int = 120) -> dict:
result = subprocess.run(
["curl", "-s", "--connect-timeout", "10", "-X", "POST", ...],
capture_output=True, text=True, timeout=timeout_s,
)
if result.returncode != 0:
return {"ok": False, "error": f"curl: {result.stderr[:200]}", ...}
```
**Issue:** Only checks curl's exit code, NOT the HTTP status code from the proof worker. A 500/404 from the worker would produce `returncode == 0` from curl but with non-JSON body, leading to a `JSONDecodeError` that IS caught — but an HTTP 200 with `{"ok": false, ...}` is silently recorded as a failed step without raising any alarm.
**Impact:** Network errors and worker failures are silently logged as "failure" steps with no alerting mechanism.
**Recommendation:** Check the HTTP response status code explicitly and surface non-2xx responses as distinct error categories.
---
### W2: `eigensolid_pipeline.py` — No Schema Version Validation on Input JSON [HIGH]
**File:** `4-Infrastructure/shim/eigensolid_pipeline.py` (lines 456-460)
```python
extraction = json.loads(extraction_path.read_text())
```
**Issue:** The extraction JSON is loaded without any schema validation. If the upstream CERN data format changes (e.g., renames `conservation_laws` to `conservationLaws`), the pipeline will silently produce empty outputs rather than fail.
**Impact:** Silent data loss on upstream format changes.
**Recommendation:** Add a JSON schema validation step and version check before processing.
---
### W3: `load_dependency_graph.py` — Hardcoded Gremlin Credentials from `.env` [HIGH]
**File:** `scripts/load_dependency_graph.py` (lines 43-48)
```python
ENV_FILE = ROOT / ".env.gremlin"
load_dotenv(ENV_FILE)
ENDPOINT = os.environ["GREMLIN_ENDPOINT"]
USERNAME = os.environ["GREMLIN_USERNAME"]
PASSWORD = os.environ["GREMLIN_PASSWORD"]
```
**Issue:** Requires `.env.gremlin` to exist with plaintext credentials. If the file is missing, the script crashes with `KeyError`. The credentials file is gitignored in most setups but may be accidentally committed.
**Impact:** Deployment fragility + potential credential leak.
**Recommendation:** Add graceful fallback when env vars are missing, and warn about the credential file in `.gitignore`.
---
### W4: `build_static.sh` — Executable List May Be Stale [MEDIUM]
**File:** `0-Core-Formalism/lean/Semantics/build-static/build_static.sh` (lines 26-28)
```bash
EXECUTABLES=(bindserver searchserver SemanticsCli openworm_benchmark \
ExtremeParameterTestEval NominalParameterTestEval moim_benchmark \
generate_sparkle_phi_s3c tangnano9k_emitter)
```
**Issue:** The list of executables is hardcoded. If the Lean `lakefile.lean` changes and adds/removes executables, this list will silently fail to build the new targets or crash trying to build removed ones.
**Impact:** Build inconsistency between `lake build` and the static compilation script.
**Recommendation:** Parse the executable list from `lakefile.lean` or use `lake exe --list` if available.
---
### W5: `pist_neuromorphic.c` — Stats Export Destructively Modifies Frequency Data [MEDIUM]
**File:** `6-Kernel-Shim/pist_neuromorphic.c` (lines 433-445)
```c
for (i = 0; i < 10 && pos < PAGE_SIZE - 64; i++) {
int max_idx = 0;
// ...find max...
pos += sprintf(buf + pos, " %02x=%llu", max_idx, st->byte_freq[max_idx]);
st->byte_freq[max_idx] = 0; /* zero out for next iter (destructive!) */
}
```
**Issue:** The `stats_show` sysfs handler zeroes out byte frequencies while formatting the output. A concurrent read will see corrupted (partially zeroed) data. This is a race condition within a single show call, not even requiring concurrent readers.
**Impact:** Frequency data is corrupted after the first read. Subsequent reads show only zeros for the top-10 frequencies.
**Recommendation:** Copy the frequency array before formatting, or use a non-destructive selection algorithm (e.g., min-heap for top-k).
---
### W6: `qaoa_adapter.py` — Optional Backend Imports Fail Silently [MEDIUM]
**File:** `4-Infrastructure/shim/qaoa_adapter.py` (lines 40-52)
```python
try:
import cirq
_HAS_CIRQ = True
except ImportError:
_HAS_CIRQ = False
```
**Issue:** All three quantum backends (cirq, qiskit, numpy) are optional. If none are installed, many functions will fail at call time rather than import time. The `qaoa_solve_qubo` function references `_HAS_CIRQ` and `_HAS_QISKIT` but may still proceed to use numpy-dependent code that expects `np` to exist.
**Impact:** Late failure with confusing error messages when quantum backends are missing.
**Recommendation:** Add a runtime check at module load that at least `numpy` is available, and raise a clear `ImportError` if not.
---
### W7: `batch_compute.yml` — Uses `actions/checkout@v4` (Outdated) [LOW]
**File:** `.github/workflows/batch_compute.yml` (line 31)
```yaml
uses: actions/checkout@v4
```
**Issue:** Other workflows in the same repo use `actions/checkout@v6` (e.g., `math-check.yml`). Version mismatch may lead to different behavior around LFS handling, fetch-depth, etc.
**Impact:** Inconsistent CI behavior between workflows.
**Recommendation:** Standardize on `actions/checkout@v6` across all workflows.
---
### W8: `manifold_binary.c` — Deserialization Does Not Validate Array Bounds [MEDIUM]
**File:** `0-Core-Formalism/core/src/manifold_binary.c` (lines 71-130)
**Issue:** `manifold_binary_deserialize` validates the header magic and version, but does NOT validate that `num_shells * sizeof(PistShell)` etc. won't overflow a `size_t`. On a maliciously crafted input with very large `num_shells`, the `malloc()` call may succeed (returning NULL or a wrapped size) and the subsequent `memcpy` will write out of bounds.
**Impact:** Potential buffer overflow on untrusted binary input.
**Recommendation:** Add bounds checks: `if (num_shells > MAX_SHELLS) return -5;` before allocation.
---
### W9: `eigensolid_pipeline.py` Generated Lean File Missing `end` Namespace Check [MEDIUM]
**File:** `4-Infrastructure/shim/eigensolid_pipeline.py` (lines 265-275)
```python
lines.append("end Semantics.CERNEigensolidData")
return "\n".join(lines)
```
**Issue:** The generated Lean code is always wrapped in `namespace Semantics.CERNEigensolidData` / `end Semantics.CERNEigensolidData`. However, the generated content may contain syntax errors (e.g., malformed identifiers from `lean_ident`) that cause `lake build` to fail on the entire file, blocking all other modules.
**Impact:** A single malformed theorem name can break the entire Lean build.
**Recommendation:** Run `lake build` on generated files before they are checked in, and isolate generated files into a separate lake package.
---
### W10: `load_dependency_graph.py` — Theorem Body Parsing Is Fragile [MEDIUM]
**File:** `scripts/load_dependency_graph.py` (lines 108-140)
**Issue:** The theorem body extraction uses a heuristic that walks lines until the next `theorem `, `lemma `, or `def `. This will fail for:
- Nested `def` inside a `where` clause
- `theorem` mentioned in a comment string inside a proof
- Tactics that output these keywords in error messages
**Impact:** Incorrect theorem body extraction leads to wrong dependency edges in the Gremlin graph.
**Recommendation:** Use Lean's server protocol (`lean --server`) for accurate AST-based parsing, or at minimum add a TODO acknowledging the heuristic nature.
---
## Per-Pipeline Breakdown
### Pipeline A: Equation → Eigensolid → Lean Theorems
**Files:** `eigensolid_pipeline.py` → `CERNEigensolidData.lean` → `lake build`
| Step | Output | Handoff Risk |
|------|--------|-------------|
| CERN parquet → DataFrame | `pd.DataFrame` | Medium — column names hardcoded |
| Extraction JSON → dict | `dict` | **High** — no schema validation |
| Spectral profile → Sidon address | `SidonAddress` | Medium — threshold hardcoded |
| Sidon address → Lean code | `str` (Lean text) | **High** — `sorry` in every proof |
| Lean text → file | `.lean` file | Medium — no build verification |
**Gap:** The generated Lean file is written to disk but never compiled or checked by CI. The `sorry` placeholder means no mathematical validation occurs.
**Race Condition:** If the pipeline is run concurrently with different `--alpha` values, the output `.lean` file will be overwritten without version tracking.
---
### Pipeline B: Lean Proof → Trace Capture → Gremlin Graph
**Files:** `lean_trace_bridge.py` → `trace.json` → `load_dependency_graph.py` → Gremlin
| Step | Output | Handoff Risk |
|------|--------|-------------|
| Lean code → proof worker | HTTP POST | **High** — no HTTP status check |
| Proof worker → JSON response | `dict` | Medium — malformed responses ignored |
| Trace → JSON file | `trace.json` | Low |
| All files → Gremlin | Gremlin vertices/edges | **High** — credential file dependency |
**Gap:** Phase 7 verification queries run after loading but do NOT check that theorem bodies contain valid Lean syntax — only that the graph structure is connected.
---
### Pipeline C: Q16_16 ↔ QUBO ↔ QAOA Circuit ↔ Receipt
**Files:** `qaoa_adapter.py` → `qubo_highs.py` → receipt JSON
| Step | Languages | Handoff Risk |
|------|-----------|-------------|
| Lean QUBOFormulation → Python QUBO | Lean ↔ Python | **Critical** — Q16_16 conversion mismatch |
| Python QUBO → HiGHS MIP | Python ↔ C++ | Medium — optional dependency |
| HiGHS solution → receipt | Python → JSON | Low |
**Gap:** The `qaoa_adapter.py` imports from `braid_search` which may not be available, and the fallback `_fallback_bracket_qubo` uses different coefficients than the original. This means QUBO results depend on which modules are importable, not just the input data.
---
### Pipeline D: C Kernel → Sysfs → Userspace Daemon
**Files:** `pist_compress.c` / `pist_neuromorphic.c` → `/sys/kernel/pist*/` → (daemon implied)
| Step | Output | Handoff Risk |
|------|--------|-------------|
| Kernel module → sysfs | text/binary | **Medium** — stats_show is destructive |
| sysfs → userspace | (not implemented) | **High** — no daemon in repo |
**Gap:** There is NO userspace daemon in the repository that reads from `/sys/kernel/pist_neuromorphic/dag_dump`. The `dag_generation` counter increments but nothing consumes it. The DAG export functionality is incomplete.
---
### Pipeline E: Lean Static Build → FPGA Bitstream
**Files:** `build_static.sh` → `lake exe tangnano9k_emitter` → Verilog → FPGA
| Step | Output | Handoff Risk |
|------|--------|-------------|
| Lean → C → static binary | ELF | Medium — hardcoded executable list |
| Static binary → Verilog | `.v` files | Medium — `lake exe` may fail silently |
| Verilog → FPGA bitstream | `.bit` | **High** — no CI for this path |
**Gap:** The `build_static.sh` script references `5-Applications/out/verilog/build_tangnano9k.sh` which may not exist in all environments. The FPGA synthesis path has no CI coverage.
---
## Type Mismatch Matrix
| Type | Lean Definition | Python Implementation | C Implementation | Consistent? |
|------|----------------|----------------------|------------------|-------------|
| Q16_16 scale | `65536` (`q16Scale`) | `65536` (`Q16_SCALE`) | `1 << 16` = 65536 | YES |
| Q16_16 float→raw | `(f * 65536.0).floor` | `int(round(v * 65536))` | `(int32_t)(f * 65536)` | **NO** |
| Q16_16 raw→float | `Float.ofInt q.toInt / 65536.0` | `value / 65536` | `(float)q / 65536` | YES |
| Q16_16 NaN sentinel | `infinity` = `q16MaxRaw` | None | None | **NO** |
| Q16_16 overflow | Saturates to `maxVal`/`minVal` | No saturation check | No saturation check | **NO** |
| Sidon set | `[1, 2, 4, 8, 16, 32, 64, 128]` | Same (Python) | Not in C | N/A |
| JSON Q16_16 | `{"val": <int>}` | Raw int | Not used | **NO** |
---
## Generated Files Status
| File | Generated By | Checked In? | Should Be? |
|------|-------------|-------------|------------|
| `CERNEigensolidData.lean` | `eigensolid_pipeline.py` | Likely NO | NO (regenerate in CI) |
| `eigensolid_analysis.json` | `eigensolid_pipeline.py` | Likely NO | NO (CI artifact) |
| `shared-data/data/stack_solidification/*.json` | Various shims | Partially YES | YES (receipts) |
| `4-Infrastructure/shim/burgers_chaos_game_receipt.json` | `burgers_chaos_game.py` | YES | YES (example receipt) |
| `4-Infrastructure/shim/eigensolid_analysis/` | `eigensolid_pipeline.py` | Unknown | NO (CI output) |
| `.lake/build/bin/*` | `lake build` | NO (gitignored) | NO (build output) |
**Note:** The repository contains some checked-in receipts (`shared-data/data/stack_solidification/*.json`) but the generation pipeline for these is not documented in CI. This creates a risk that checked-in receipts are stale relative to the generating code.
---
## CI Workflow Gaps
| Workflow | Tests Lean Build? | Tests Q16_16 Roundtrip? | Tests Kernel Module? | Tests Receipt Integrity? |
|----------|------------------|------------------------|---------------------|------------------------|
| `math-check.yml` | NO | NO | NO | YES (SHA-256) |
| `wolfram-verification.yml` | NO (only comments) | NO | NO | NO |
| `batch_compute.yml` | NO | NO | NO | NO |
| `lean_action_ci.yml` | YES (OTOM subproject) | NO | NO | NO |
**Gap:** No CI workflow tests the full roundtrip: Lean Q16_16 → JSON → Python → C → back to Lean. A dedicated integration test should:
1. Generate Q16_16 values in Lean
2. Export via `BindServer` JSON
3. Parse in Python with `q16.py`
4. Serialize via `manifold_binary.h` format
5. Deserialize in C
6. Roundtrip back to Lean
7. Verify bit-exact equality
---
## Recommendations (Priority Order)
1. **Unify Q16_16 conversion**: Standardize on `floor` semantics across all three languages. Add a conformance test.
2. **Deduplicate q16.py**: Remove the `auto/lib/` copy or make it re-export from `lib/`.
3. **Add NaN/error propagation**: Use JSON `{"error": "overflow"}` instead of 0xFFFFFFFF sentinel.
4. **Build generated Lean in CI**: Add `lake build` step for all generated `.lean` files. Reject `sorry`.
5. **Fix destructive stats_show**: Copy frequency array before formatting in `pist_neuromorphic.c`.
6. **Add schema validation**: Validate extraction JSON against a schema before processing.
7. **Complete the kernel userspace bridge**: Implement or document the DAG consumer daemon.
8. **Add roundtrip integration test**: Test the full Lean→Python→C→Lean data flow in CI.

259
audit/lean_formalism_audit.md Normal file
View file

@ -0,0 +1,259 @@
# Lean Formalism Audit Report
**Repository**: allaunthefox/Research-Stack
**Branch**: main
**Date**: 2025-01-18
**Scope**: All 1,295 Lean files
---
## Executive Summary
| Metric | Count |
|--------|-------|
| Total Lean files | 1,295 |
| Files scanned (largest + smallest) | ~159 |
| Files with `sorry` | ~14+ (estimated 30-60 across all 1,295) |
| Total `sorry` count (scanned) | 14+ confirmed |
| Files with `admit` | 0 confirmed |
| Files with `proof_wanted` | 0 confirmed |
| Broken/inaccessible files | ~70 (fetch timeout) |
| Placeholder files (imports only, no content) | ~3 confirmed |
| Import cycles detected | None confirmed |
| Naming convention violations | Minimal |
---
## 1. SORRY INVENTORY (CRITICAL)
### Confirmed Files with `sorry`
| File | Sorry Count | Severity | Notes |
|------|-------------|----------|-------|
| `0-Core-Formalism/lean/Semantics/Core/T1_Coherence.lean` | 12 | **CRITICAL** | Core coherence theorems - measure theory integration gaps |
| `0-Core-Formalism/lean/Semantics/Semantics/ErdosRenyiPipeline.lean` | 6 | **HIGH** | Sidon iff collision backward, energy zero iff, Erdos-Renyi density bounds, CRT sieve backward, structure bonus log bound |
| `0-Core-Formalism/lean/Semantics/Semantics/E8Sidon.lean` | 5 | **HIGH** | Householder involution algebra (2), chaos game Sidon preservation (1), trajectory sum translation |
| `0-Core-Formalism/lean/external/OTOM/SSMS.lean` | 2 | **MEDIUM** | MLGRU delta bound (Q16.16 arithmetic theory), ACI preservation (truncation error lemmas) |
| `0-Core-Formalism/lean/Semantics/ExtensionScaffold/Physics/NBody.lean` | 1 | **LOW** | Single sorry in simFlowPhi field |
### Sorry Classification
**Hard sorry (real mathematics needed)**:
- T1_Coherence: Measure theory integration proofs (12)
- E8Sidon: Householder reflection algebra, chaos game trajectory proofs (5)
- ErdosRenyiPipeline: Sidon characterization completeness, analytic number theory bounds (6)
**Medium sorry ( Lean machinery needed)**:
- SSMS: Q16.16 fixed-point algebra lemmas (2)
- NBody: Minor field assignment (1)
**Estimated total sorry across all 1,295 files**: ~30-60
(based on density in scanned files extrapolated)
### Sorry by Module
| Module | Estimated Sorry Count |
|--------|----------------------|
| Semantics/Core (BindAxioms, InformationManifold, T1_Coherence) | 12+ |
| Semantics/Semantics/E8Sidon | 5 |
| Semantics/Semantics/ErdosRenyiPipeline | 6 |
| Semantics/Semantics/Other (~500 files) | 5-10 estimated |
| ExtensionScaffold/Physics | 1 |
| ExtensionScaffold/ENE | 0 (import-only files) |
| External/OTOM | 2 |
| Singer-theorem-lean (~73 files) | Unknown (many timed out) |
| Lean_binned (~93 files) | Unknown (many timed out) |
---
## 2. BROKEN FILES (CRITICAL)
### Files That Failed to Fetch (likely too large or network issues)
**Large theorem files (> 80KB)**:
- `singer-theorem-lean/Erdos30/BoundaryD1SurvivorCounts.lean`
- `singer-theorem-lean/Erdos30/BoundaryD1TheoremRangeFrontier.lean`
- `singer-theorem-lean/Erdos30/BoundarySecantRigidLeafProfileBridge.lean`
- `singer-theorem-lean/Erdos30/BoundarySecantTheoremRangeFrontier.lean`
- `singer-theorem-lean/Erdos30/BoundarySecantTheoremRangeLocalClassification.lean`
- `singer-theorem-lean/Erdos30/BoundarySecantTheoremRangeLocalRealization.lean`
**Other broken files**:
- `Semantics/Semantics/ASICTopology.lean`
- `Semantics/Semantics/Adapters/AlphaProofNexus/erdos_12.parts.i.lean`
- `Semantics/Semantics/Adapters/AlphaProofNexus/erdos_741.parts.i.lean`
- `Semantics/Semantics/Adapters/AlphaProofNexus/erdos_846.lean`
- `Semantics/Semantics/Adapters/AlphaProofNexus/graph_conjecture2.lean`
- `Semantics/Semantics/Benchmarks/HadwigerNelson.lean`
- `Semantics/Semantics/CooperativeLUT.lean`
- `Semantics/Semantics/DeltaGCLCompression.lean`
- `Semantics/Semantics/EntropyMeasures.lean`
- `Semantics/Semantics/ExtendedManifoldEncoding.lean`
- `Semantics/Semantics/Foundations/CarnotEfficiency.lean`
- `Semantics/Semantics/InvariantReceipt/Receipt.lean`
- `Semantics/Semantics/N3L_Energy.lean`
- `Semantics/Semantics/PIST/Classify.lean`
- `Semantics/Semantics/Physics/NBody.lean`
- `Semantics/Semantics/Q16InverseProof.lean`
- `Semantics/Semantics/RRC/Corpus250.lean`
- `Semantics/Semantics/RRC/EntropyCandidates/Candidates.lean`
- `Semantics/Semantics/SidonSets.lean`
- `Semantics/Semantics/Testing/ArrayTest.lean`
- `Semantics/Semantics/Testing/LemmaTest2.lean`
- `Semantics/TestFintype.lean`
- `external/OTOM/Atoms.lean`
- `external/OTOM/Basic.lean`
- `external/OTOM/ComputationProfile.lean`
- `external/OTOM/MetricCore.lean`
- `external/OTOM/Physics.lean`
- `3-Mathematical-Models/manifold_compression/src/AutoAdaptiveMetatypeSystem.lean`
- ~40 lean_binned files
**Root cause**: Most failures are likely due to network timeout (files > 60KB or path length issues). Not necessarily syntactically broken.
---
## 3. PLACEHOLDER FILES (INFO)
Files with only imports and no actual definitions:
| File | Lines | Size | Content |
|------|-------|------|---------|
| `0-Core-Formalism/lean/Semantics/Biology.lean` | 3 | 134B | Imports only, no definitions |
| `0-Core-Formalism/lean/Semantics/GenerateLUTMain.lean` | 5 | 248B | Single import + minimal code |
| `0-Core-Formalism/lean/Semantics/PurifyMain.lean` | 9 | 264B | Minimal stub |
| `2-Search-Space/SearchSpace.lean` | 7 | 129B | Empty placeholder |
Additional small stub files (< 500 bytes) that may need attention: ~119 files total.
---
## 4. IMPORT ANALYSIS
### Import Cycles
**None detected** in the scanned files. The module structure follows a DAG pattern:
- `Core/` → `Semantics/` → `ExtensionScaffold/`
- `external/` is self-contained
- `singer-theorem-lean/` imports from `Semantics/SidonSets` but not vice versa
### Heavy Import Chains
- `E8Sidon.lean` imports `Semantics.SidonSets` (mathematical dependency)
- `NBody.lean` imports 8 modules: Bind, DynamicCanal, LocalDerivative, HyperFlow, FixedPoint, BraidStrand, BraidBracket, CMYKFrequencyCore, ThroatPhysics, Wormhole, QuantumEraserCache
- `ErdosRenyiPipeline.lean` imports 7 Mathlib modules
### Missing Imports
None detected in scanned files. All referenced definitions appear properly imported.
---
## 5. NAMING CONVENTION ANALYSIS
### AGENTS.md §2 Compliance
**Generally excellent compliance** across the codebase:
| Convention | Status | Examples |
|------------|--------|----------|
| PascalCase for types/structures | **Good** | `Q1616`, `NBodyState`, `Particle`, `BitLinearParams`, `MlgruState`, `ScalarNode`, `GossipPacket`, `DirSimplicialComplex`, `BettiSwooshH`, `SwooshEvent`, `SubleqCore`, `NUVMap`, `ChainPattern`, `RatchetLUT`, `SolveEntry`, `H264Macroblock`, `NUVMapCacheState`, `Slug3State`, `Slug3Node` |
| camelCase for functions | **Good** | `velocityVerletStep`, `computeHamiltonian`, `gravitationalForce`, `totalForceOnParticle`, `energyGradientToNUVMap`, `verletStepWithNUVMap`, `ratchetLUTUpdate`, `batchNUVMapCache`, `nuvMapCacheHitRate`, `cmykToYuv`, `classifyYUV`, `hardwareDecompressPipeline` |
| ALL_CAPS for constants | **Good** | `GRADIENT_THRESHOLD`, `Y_LOW`, `Y_MID`, `Y_HIGH`, `UV_LOW`, `UV_MID`, `UV_HIGH` |
### Minor Issues
- Some Lean-generated files in `singer-theorem-lean/` use snake_case (e.g., `bipartite_reconstruction.lean`, `erdos_12.parts.i.lean`) but these are generated artifacts
- `lean_binned/` files use hex hashes in names (by design)
---
## 6. DUPLICATION ANALYSIS
### Potential Duplications Found
1. **`IsSidonSet` defined in multiple files**:
- `Semantics/Semantics/SidonSets.lean` (canonical)
- `Semantics/Semantics/ErdosRenyiPipeline.lean` (local copy with slightly different signature)
- Risk: Divergence between definitions
2. **`CoverageSystem` / `IsGap` / `IsLosslessMap`**:
- May overlap with coverage concepts in other pipeline files
3. **N-body physics duplicated**:
- `ExtensionScaffold/Physics/NBody.lean` (the canonical one)
- `Semantics/Semantics/Physics/NBody.lean` (potentially a copy)
4. **Q16.16 fixed-point type**:
- `Semantics/Q16_16.lean` (canonical)
- `external/OTOM/SSMS.lean` has its own `Q1616` structure
- Risk: Two fixed-point implementations may diverge
---
## 7. CODE QUALITY OBSERVATIONS
### Strengths
- **Extensive documentation**: Header comments explain architecture, status, and design decisions
- **Computational verification**: Many files use `native_decide` and `#eval` for testing
- **Axiom discipline**: Axioms clearly marked (e.g., `axiom E4_sq_eq_E8_coeff`) with justification
- **Well-structured namespaces**: Hierarchical `namespace` usage (e.g., `Semantics.E8Sidon`, `ExtensionScaffold.Physics.NBody`)
- **Section organization**: Clear section markers (§1, §2, etc.)
### Weaknesses
- **sorry accumulation**: Core files (T1_Coherence, E8Sidon) have significant mathematical gaps
- **Large files**: Several files exceed 50KB (EntropyMeasures ~265KB, AutoImported ~99KB) making review difficult
- **Generated code**: `singer-theorem-lean/` files appear largely auto-generated with limited human review
- **lean_binned files**: ~93 files that are equation stubs with minimal content
---
## 8. CRITICAL ISSUES (Must Fix)
1. **T1_Coherence.lean: 12 sorry markers** - Core coherence theorems need measure theory proofs
2. **E8Sidon.lean: 5 sorry markers** - Householder reflection algebra incomplete
3. **ErdosRenyiPipeline.lean: 6 sorry markers** - Key iff characterizations incomplete
4. **SSMS.lean: 2 sorry markers** - ACI preservation theorem blocked on Q16.16 algebra
5. **Large file fetch failures** - 70+ files could not be accessed; need to verify they build
6. **`IsSidonSet` duplication** - Two different definitions in SidonSets.lean vs ErdosRenyiPipeline.lean
## 9. WARNINGS (Should Fix)
1. **~119 small files (< 500 bytes)** - May be stubs that need content or removal
2. **Placeholder imports-only files** - Biology.lean, SearchSpace.lean have no definitions
3. **Duplicate Q1616 implementation** - SSMS.lean reimplements the fixed-point type
4. **Singer-theorem-lean generated files** - No clear provenance/verification for large auto-generated proofs
5. **Lean_binned files** - 93 equation stubs, most with minimal content
## 10. INFO (Nice to Have)
1. Add `proof_wanted` markers for theorems that should be prioritized
2. Document the dependency graph between modules
3. Consider splitting files > 50KB into smaller modules
4. Add CI build verification for all files
5. Standardize `native_decide` usage (some files over-rely on it)
---
## Per-Module Breakdown
| Module | Files | Scanned | Sorry | Broken | Placeholders | Status |
|--------|-------|---------|-------|--------|-------------|--------|
| Semantics/Core | 3 | 3 | 12+ | 0 | 0 | Needs proofs |
| Semantics/Semantics | ~500 | ~40 | 11+ | ~15 | ~2 | Mixed quality |
| Semantics/ExtensionScaffold | ~50 | ~15 | 1 | ~8 | ~1 | Generally good |
| singer-theorem-lean | 73 | 6 | ? | 6 | 0 | Large generated files |
| external/OTOM | 13 | 5 | 2 | 5 | 0 | Good structure |
| lean_binned | 93 | ~50 | ? | ~40 | ~93 | Stubs by design |
| 2-Search-Space | 10 | 0 | ? | 0 | ~1 | Not scanned |
| 6-Documentation | 9 | 0 | 0 | 0 | 0 | Docs only |
---
## Top 10 Files by Sorry Count (Confirmed)
1. `T1_Coherence.lean` — 12 sorry (CRITICAL)
2. `ErdosRenyiPipeline.lean` — 6 sorry (HIGH)
3. `E8Sidon.lean` — 5 sorry (HIGH)
4. `SSMS.lean` — 2 sorry (MEDIUM)
5. `NBody.lean` — 1 sorry (LOW)
---
*Report generated by automated analysis of 159 representative files + detailed manual review of key modules.*

409
audit/quality_audit.md Normal file
View file

@ -0,0 +1,409 @@
# Quality Audit: Research-Stack
**Repository:** https://github.com/allaunthefox/Research-Stack
**Branch:** main
**Audit Date:** 2026-06-21
**Auditor:** Automated CI/CD & Code Quality Audit
---
## Summary
| Metric | Count |
|---|---|
| CI workflows (user-defined) | 4 |
| CI workflows (dynamic/dependabot/pages) | 3 |
| CI workflows passing (latest run) | 1/4 (Wolfram Alpha) |
| CI workflows failing (latest run) | 3/4 |
| Overall CI failure rate (last 100 runs) | 74% |
| Test files (name matches) | 1,282 |
| Actual unit test files (pytest/unittest) | 2 |
| Lean proof test files | 61 |
| Rust test files | 35 |
| Code duplications (duplicate basenames) | 627 |
| Experimental files on main | 57 |
| Large files (>1MB) | 66 |
| Binary files in git | 101 |
| .pist / .pist.meta generated artifacts | 192 |
| Receipt files | 104 |
| Pre-commit config | NOT FOUND |
| .gitattributes | Present (has contradictory LFS config) |
| Version pinning (Python) | Partially pinned (mixed == and >=) |
| Version pinning (Rust) | Locked (Cargo.lock present) |
| Version pinning (JS) | Locked (package-lock.json present) |
| Files needing cleanup | ~297+ |
---
## Critical Issues
### 1. CI/CD: 74% Failure Rate Across All Workflows (SEVERITY: CRITICAL)
The last 100 GitHub Actions runs show a **74% failure rate** (74 failures, 26 successes). This is a systemic CI reliability problem.
**Workflow-by-workflow status (latest run):**
| Workflow | Path | Status |
|---|---|---|
| Math-First Checks | `.github/workflows/math-check.yml` | **FAILING** |
| Batch Compute Runner | `.github/workflows/batch_compute.yml` | **FAILING** |
| Copilot Setup Steps | `.github/workflows/copilot-setup-steps.yml` | Unknown (path-triggered) |
| Wolfram Alpha Verification | `.github/workflows/wolfram-verification.yml` | **PASSING** |
| Pages Build & Deploy | `dynamic/pages/pages-build-deployment` | **FAILING** |
| Dependabot (cargo) | `dynamic/dependabot/dependabot-updates` | **FAILING** |
| Dependabot (npm) | `dynamic/dependabot/dependabot-updates` | Mixed (some pass, some fail) |
**Evidence:** API query `https://api.github.com/repos/allaunthefox/Research-Stack/actions/runs?per_page=100` returns `74 failure` vs `26 success` conclusions.
**Root causes likely include:**
- `math-check.yml` runs schema validation, receipt validation, self-tests, and pre-commit hooks on PR/push. Multiple steps can fail independently.
- `batch_compute.yml` runs daily compute jobs with external WASM dependencies.
- `pages-build-deployment` is a GitHub-managed Pages workflow that may fail due to build output issues.
- Dependabot updates fail on individual ecosystem updates (cargo, uv, npm) indicating dependency resolution issues.
**Impact:** Contributors cannot trust CI signals. Failures are so common they likely get ignored, masking real regressions.
**Remediation:**
1. Fix Math-First Checks first (core quality gate) — inspect job logs to identify failing steps.
2. Fix Pages build — likely a Jekyll/build output issue.
3. Remove or fix the daily Batch Compute workflow (harvests runner minutes, likely wasteful).
4. Stabilize Dependabot by pinning dependency versions and resolving ecosystem conflicts.
---
### 2. Missing Pre-commit Configuration File (SEVERITY: CRITICAL)
`math-check.yml` references `.pre-commit-config.yaml` in its `on.push.paths` trigger and runs `pre-commit run --from-ref "$base" --to-ref "$head"` in the `pre-commit` job.
However, **`.pre-commit-config.yaml` does NOT exist** at the repository root.
**Evidence:**
- The file tree API traversal finds no `.pre-commit-config.yaml`.
- Direct file content API returns 404.
- The CI job installs `pre-commit>=3.7` but has no hooks file to read.
**Impact:** The pre-commit CI job will fail every time it runs (no config file found). This explains one of the failure modes in Math-First Checks.
**Remediation:** Create a `.pre-commit-config.yaml` at the repo root, or remove the pre-commit job from CI.
---
### 3. 66 Large Files (>1MB) Committed to Git (SEVERITY: HIGH)
Multiple files over 1MB are stored in the repository, significantly impacting clone times and repository size. These should be tracked via Git LFS or stored externally.
**Largest offenders:**
| File | Size |
|---|---|
| `shared-data/papers/2026-05/2511.21459.pdf` | **44.88 MB** |
| `5-Applications/text-to-cad/skills/cad/assets/text-to-cad-demo.gif` | **25.07 MB** |
| `5-Applications/text-to-cad/skills/urdf/assets/text-to-cad-demo.gif` | **25.07 MB** |
| `3-Mathematical-Models/equations_compressed/unknown_equations_20260504_134248.compressed` | **24.23 MB** |
| `4-Infrastructure/hardware/cff_accelerator.json` | **13.84 MB** |
| `2-Search-Space/simulations/matter-frequencies/wav-files/*.wav` (17 files x ~11MB) | **~187 MB combined** |
| `2-Search-Space/simulations/Newtonian-Superfluid-Simulation/YouCut_20260426_155638157.gif` | **9.50 MB** |
| `2-Search-Space/simulations/Newtonian-Superfluid-Simulation/demo-simulation.mp4` | **9.44 MB** |
| `.github/assets/rainbow_raccoon_compiler.png` | **6.97 MB** |
**Impact:** Repository bloat. Fresh clones take significantly longer. CI jobs spend time downloading these files even when not needed.
**Remediation:**
1. Move all media files (`.wav`, `.gif`, `.mp4`, `.png`, `.pdf`) to Git LFS or external storage.
2. The `.gitattributes` file already has LFS filters configured but many of these large files are NOT tracked by LFS (the LFS config appears to be present but the files themselves may have been committed before `.gitattributes` was added).
3. Use `git lfs migrate` to move existing large files to LFS.
---
### 4. 192 Generated Artifacts (`.pist` / `.pist.meta`) Committed to Main (SEVERITY: HIGH)
The `0-Core-Formalism/lean/Semantics/` directory contains **96 `.lean.pist` files and 96 `.lean.pist.meta` files**. These are clearly build artifacts / generated files from the Lean compiler.
**Evidence:** Files like:
- `AdaptivePrecision.lean.pist`
- `AdaptivePrecision.lean.pist.meta`
- `FPGAExtraction.lean.pist`
- `MinimumNeuralCompression.lean.pist`
**Impact:** Generated files create merge conflicts, bloat diffs, and become stale. They should be `.gitignore`d and generated at build time.
**Remediation:** Add `*.pist` and `*.pist.meta` to `.gitignore` and remove all committed instances.
---
### 5. 104 Receipt Files (Generated Artifacts) in Repository (SEVERITY: MEDIUM)
The `shared-data/artifacts/deepseek_review/` directory contains receipt files (`.receipt.json`). These are CI-generated artifacts tracking automated review outputs.
**Impact:** Generated receipts create noise in the git history. The CI validates them against SHA-256 (which is good) but storing them in the repo is an anti-pattern for generated artifacts.
**Remediation:** Store receipts as CI artifacts (using `actions/upload-artifact`) rather than committing them to the repository.
---
## Warnings
### W1. Contradictory `.gitattributes` LFS Configuration
The `.gitattributes` file has contradictory rules for the same extensions:
```gitattributes
*.bin filter=lfs diff=lfs merge=lfs -text
*.bin !text !filter !merge !diff
```
Each file type has TWO rules — one enabling LFS and one disabling it. This is clearly a merge artifact or misconfiguration. The second rule overrides the first for many extensions, meaning LFS may not actually be applied.
**Files affected:** `.bin`, `.tar.gz`, `.npz`, `.db`, `.zip`, `.zst`, `.gguf`, `.parquet`, `.iso`, `.so`, `.tar.zst`, `.gz`, `.xz`, `.png`, `.jpg`, `.jpeg`, `.gif`, `.json`, `.step`, `.stp`, `.stl`
**Remediation:** Fix `.gitattributes` to have a single consistent rule per extension. Remove the `!filter !merge !diff` override lines.
---
### W2. Python Dependencies Partially Unpinned
Multiple `requirements.txt` files use `>=` (minimum version) instead of `==` (pinned):
**Unpinned (dangerous):**
- `4-Infrastructure/shim/requirements.txt`: Uses `>=` for ALL 20+ dependencies (`reedsolo>=1.7.0`, `cryptography>=41.0.0`, `qiskit>=1.0.0`, etc.)
- `5-Applications/requirements_swarm_api.txt`: Likely unpinned
**Pinned (good):**
- `2-Search-Space/manifold/requirements.txt`: Uses `==` (`fastapi==0.104.1`, `numpy==1.24.3`)
**No Python lock files** (no `poetry.lock`, no `requirements.lock`, no `Pipfile.lock`) at the root or in most subprojects.
**Impact:** A future release of any dependency (e.g., `qiskit>=1.0.0`, `numpy>=1.24.0`) can break builds without any code changes.
**Remediation:** Pin all Python dependencies with `==` and generate lock files. Use `pip-tools` or `poetry` to manage dependencies deterministically.
---
### W3. Duplicate Basenames Suggest Copy-Paste Code (627 instances)
**Most duplicated filenames:**
| Filename | Count | Likely Issue |
|---|---|---|
| `mod.rs` | 126 | Many separate Rust crates (expected for workspace) |
| `__init__.py` | 123 | Many Python packages (normal) |
| `lib.rs` | 44 | Rust library roots (normal for workspace) |
| `+server.ts` | 28 | SvelteKit API routes (Svelte pattern) |
| `main.rs` | 20 | Multiple entrypoints |
| `test_cli.py` | 6 | **Same test file name in 6 locations** |
| `test_coverage_gaps.py` | 6 | **Same test file name in 6 locations** |
The `test_cli.py` and `test_coverage_gaps.py` appearing in 6 locations each is suspicious — these may be copied between projects without modification, indicating the same test logic duplicated.
**Remediation:** Audit the `test_cli.py` and `test_coverage_gaps.py` files for actual duplication. Extract shared test utilities to a common module.
---
### W4. Lean Files with "Test" in Name That Are Not Tests (61 files)
Many Lean files in `0-Core-Formalism/lean/Semantics/**/Testing/` contain proof attempts and benchmarks, not automated unit tests. They won't be discovered or executed by any test runner.
**Examples:**
- `BitcoinRGFlowTest.lean` — a proof benchmark, not a runnable test
- `VirtualGPUBenchmark.lean` — a benchmark script
- `ReceiptReproducibilityTest.lean` — manual verification steps
**Impact:** These create false confidence. They look like tests but aren't executed by CI.
---
### W5. Workflow Trigger Paths Too Narrow
Several workflows only run on specific path changes, meaning they rarely trigger and failures may go undetected for long periods:
- `math-check.yml`: Only triggers on `0-Core-Formalism/lean/Semantics/**`, `shared-data/**`, etc.
- `wolfram-verification.yml`: Only triggers on `.lean` file changes.
- `batch_compute.yml`: Only runs on schedule (daily) or manual dispatch.
**Impact:** CI failures can persist undetected because the workflows don't run on most changes.
---
### W6. Dependabot Workflow Failures
Dependabot has been consistently failing on:
- `cargo in /4-Infrastructure/servo-fetch for time` — cargo ecosystem updates failing
- `uv in /. for h11` — Python dependency resolution failures
- `npm_and_yarn in /3-Mathematical-Models/bezier-kit for js-yaml` — JS dependency issues
**Impact:** Security patches and bug fixes are not being applied automatically.
---
## Per-Component Breakdown
### 0-Core-Formalism/ (Lean + Rust)
| Metric | Value |
|---|---|
| `.lean` files | 1,305 |
| `.rs` files | 942 |
| Lean test files (name match) | 61 |
| Rust test files (name match) | 35 |
| `.pist` generated artifacts | 96 |
| `.pist.meta` generated artifacts | 96 |
| `_output.txt` artifacts | 1 |
| CI workflows touching this | `math-check.yml`, `wolfram-verification.yml` |
**Issues:**
- 192 generated `.pist` files committed to git (CRITICAL)
- `Quarantine/Q064Experimental.lean` — clearly experimental file on main
- `ExperimentTracker.lean` — experimental tracking file
- `test.lean` at root of semantics directory — temporary test file
- `ExtremeParameterTestEval_output.txt` — generated output committed
---
### 1-Distributed-Systems/
| Metric | Value |
|---|---|
| Rust crates with tests | 3+ (claw: `api/tests/`, `runtime/tests/`, `rusty-claude-cli/tests/`) |
| CI coverage | None specific |
**Issues:**
- No dedicated CI workflow for the distributed systems code
- Tests exist but aren't run in CI
---
### 2-Search-Space/
| Metric | Value |
|---|---|
| Large media files | 17 WAV files (~187 MB), 2 GIFs (~12 MB), 1 MP4 (~9 MB) |
| `test_cli.py` duplicates | 6+ locations |
| Binary test data | 3 large HTML entity files (animal.html, aristotle.html, lion.html) |
**Issues:**
- Simulation media files (WAV, GIF, MP4) should be in LFS or external storage (HIGH)
- `testcases/entity/*.html` files (1-1.5 MB each) are test fixtures — acceptable but large
---
### 3-Mathematical-Models/
| Metric | Value |
|---|---|
| Large compressed file | `equations_compressed/unknown_equations_20260504_134248.compressed` (24.23 MB) |
| CI coverage | None specific |
**Issues:**
- Large opaque `.compressed` file — no indication of what's inside or how to regenerate it
- No tests for mathematical models
---
### 4-Infrastructure/
| Metric | Value |
|---|---|
| Rust crates | Multiple (servo-fetch, waveprobe, ene) |
| Python shims | Multiple |
| `requirements.txt` with unpinned deps | `4-Infrastructure/shim/requirements.txt` |
| Large JSON files | `cff_accelerator.json` (13.84 MB), `cern_pde_extraction.json` (6.44 MB) |
| `flake.nix` / `flake.lock` | Present at root, pinned to `nixos-24.11` |
**Issues:**
- `shim/requirements.txt` has 20+ unpinned `>=` dependencies (WARNING)
- Large JSON data files committed directly (should be LFS)
- `k3s-flake/tests/package.json` — no lock file validation in CI
---
### 5-Applications/
| Metric | Value |
|---|---|
| Large GIF duplicates | `text-to-cad-demo.gif` appears in 2 locations (25.07 MB each) |
| Python backend | `cluster-dashboard/backend/requirements.txt` |
| CI coverage | None specific |
**Issues:**
- 50+ MB of duplicate GIF files (same file in two skill directories)
- No application-level CI testing
---
### .github/workflows/
| Workflow | Size | Purpose | Status |
|---|---|---|---|
| `batch_compute.yml` | 2,074 B | Daily compute job | FAILING |
| `copilot-setup-steps.yml` | 432 B | Lean setup helper | Unknown |
| `math-check.yml` | 6,221 B | Schema + receipt validation | FAILING |
| `wolfram-verification.yml` | 5,577 B | Math formula verification | PASSING |
**Issues:**
- `math-check.yml` references `.pre-commit-config.yaml` that doesn't exist
- `actions/checkout@v6` used in some workflows but `actions/checkout@v4` in others — version inconsistency
- `setup-python@v5` vs `setup-python@v6` — version inconsistency
- `upload-artifact@v4` — good, latest version
- `batch_compute.yml` installs `ffmpeg`, `numpy`, `requests`, `cryptography`, `reedsolo`, `highspy` without version pinning
- No `workflow_call` or reusable workflow patterns — everything is duplicated
---
## File Inventory
### Files Needing Cleanup (delete or .gitignore)
| Category | Count | Pattern |
|---|---|---|
| `.lean.pist` files | 96 | `*.lean.pist` — Lean build artifacts |
| `.lean.pist.meta` files | 96 | `*.lean.pist.meta` — Lean build metadata |
| `_output.txt` files | 1 | `*_output.txt` — generated test output |
| `.consolidation-manifests/` | 2 | Large SHA256 manifest files (1-1.5 MB) |
| Receipt JSON files | 104 | `shared-data/artifacts/deepseek_review/*.receipt.json` |
| Test output / temp | Various | `test-results/`, `.pist`, `.meta` |
### Experimental/Temporary Files on Main
| File | Reason |
|---|---|
| `Q064Experimental.lean` | Contains "Experimental" in name |
| `ExperimentTracker.lean` | Experimental tracking |
| `RydbergExperimentalTest.lean` | Experimental physics test |
| `experiment-001.html` | HTML experiment prototype |
| `test.lean` | Root-level temp test file |
| `Experiment.svelte`, `ExperimentProgress.svelte` | Svelte experiment UI |
| `ranking-diff/src/routes/api/experiments/` | Entire experiment API directory |
### Large Files Requiring LFS or External Storage
| File | Size |
|---|---|
| `shared-data/papers/2026-05/2511.21459.pdf` | 44.88 MB |
| `text-to-cad-demo.gif` (x2) | 50.14 MB total |
| `unknown_equations_*.compressed` | 24.23 MB |
| `cff_accelerator.json` | 13.84 MB |
| `*.wav` files (x17) | ~187 MB total |
| `YouCut_*.gif` | 9.50 MB |
| `demo-simulation.mp4` | 9.44 MB |
| `lean_dependency_dag_parallel.svg` | 8.38 MB |
| `rainbow_raccoon_compiler.png` | 6.97 MB |
| `cern_pde_extraction.json` | 6.44 MB |
---
## Recommendations (Priority Order)
1. **Create `.pre-commit-config.yaml`** or remove the pre-commit job from `math-check.yml` (CRITICAL)
2. **Fix Math-First Checks CI** — inspect logs, fix failing steps (CRITICAL)
3. **Remove `.pist` / `.pist.meta` files** from git and add to `.gitignore` (HIGH)
4. **Move large files to Git LFS** using `git lfs migrate` (HIGH)
5. **Pin Python dependencies** — convert all `>=` to `==`, add lock files (HIGH)
6. **Fix `.gitattributes`** — remove contradictory LFS rules (MEDIUM)
7. **Move receipt files** to CI artifacts instead of committed files (MEDIUM)
8. **Add CI workflows** for Rust and Python test suites (MEDIUM)
9. **Consolidate duplicate test files** (`test_cli.py`, `test_coverage_gaps.py`) (MEDIUM)
10. **Stabilize Dependabot** by resolving ecosystem conflicts (LOW)
---
*End of Audit Report*