From 1ce4093041725f58c20fd85a7a302ce88733e3f7 Mon Sep 17 00:00:00 2001 From: allaun Date: Sun, 21 Jun 2026 06:05:58 -0500 Subject: [PATCH] =?UTF-8?q?docs:=20add=20PORTING=5FMAP.md=20for=20Research?= =?UTF-8?q?-Stack=20=E2=86=92=20SilverSight=20migration?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Maps every proven Research-Stack component to its SilverSight library, with status: PORTED / PORT / ADAPT / DROP. Also lists gaps, conflicts, and recommended porting order. --- PORTING_MAP.md | 256 +++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 256 insertions(+) create mode 100644 PORTING_MAP.md diff --git a/PORTING_MAP.md b/PORTING_MAP.md new file mode 100644 index 00000000..7620e471 --- /dev/null +++ b/PORTING_MAP.md @@ -0,0 +1,256 @@ +# SilverSight Porting Map + +**Source:** Research-Stack (`/home/allaun/Research Stack`) +**Target:** SilverSight (`https://github.com/allaunthefox/SilverSight`) +**Goal:** Move only what is proven, active, and compatible with the library-method architecture. + +--- + +## 1. Current SilverSight State + +SilverSight already has a clean skeleton built around the 5-layer conceptual map: + +``` +Core/ + SilverSightCore.lean ← 200-line invariant core +formal/ + CoreFormalism/ ← Chentsov, Hachimoji, Q16_16 + PVGS_DQ_Bridge/ ← 7 sections + master bridge + UniversalEncoding/ ← 50-token math address space + BindingSite/ ← amino-acid / protein binding sketches +python/ + chaos_game.py + sidon_address.py + spectral_profile.py + q16_canonical.py +qubo/ + finsler_metric.py + qubo_builder.py + qaoa_circuit.py + classical_solver.py +tests/ + q16_roundtrip_test.py +docs/ + ARCHITECTURE.md + LIBRARY_MANIFEST.md + RRC_PLACEMENT.md +REBASE_RULES.md ← seed ruleset from Research-Stack +``` + +--- + +## 2. Research-Stack Source Inventory + +The source tree is large (~9,600 objects, ~1,300 Lean files). Most of it is exploratory or extracted to other repos. The durable, proven subset lives in: + +| Area | What matters | +|------|--------------| +| `0-Core-Formalism/lean/Semantics/Semantics/` | Proven Lean modules: FixedPoint, SidonSets, SieveLemmas, InteractionGraphSidon, BraidEigensolid, BraidSpherionBridge, AVMIsa.*, RRC.Emit/Corpus250, TransportQUBOBridge, ChentsovBridge. | +| `4-Infrastructure/shim/` | Python shims: qaoa_adapter.py, qubo_highs.py, benchmark_finsler_qap.py, chaos_game_16d.py, sidon_generation_kernel.py, geometric_entropy_explorer.py, candidate_certification_bridge.py, stack_solidification_audit.py. | +| `6-Documentation/docs/` | AGENTS.md strict rules, architecture specs, distilled notes, specs (DP-RRC, Virtio-Net compute, etc.). | +| `5-Applications/text-to-cad/` | CAD/URDF harness and skills. | +| `scripts/qc-flag/` | Lean QC flagger protocol. | +| `.devin/skills/lean-proof/SKILL.md` | Mandatory proof-quality skill. | +| `.github/skills/contextstream-workflow/SKILL.md` | Persistent memory workflow. | +| `.github/skills/research-stack-workflow/SKILL.md` | Token-efficient proof workflow. | +| `.cursorrules`, `.devin/`, `.claude/`, `.roo/`, `.kilo/`, `.windsurf/` | Editor/agent hook configs that enforce ContextStream-first rules. | + +--- + +## 3. Porting Matrix + +### Legend + +| Status | Meaning | +|--------|---------| +| ✅ **PORTED** | Already exists in SilverSight in compatible form. | +| 🟡 **PORT** | Proven/active in Research-Stack; should move to SilverSight as-is or with minimal renaming. | +| 🟠 **ADAPT** | Concept survives, but implementation must be refactored for the library-method architecture. | +| 🔴 **DROP** | Quarantined, hairy, extracted to other repos, or superseded by SilverSight design. | + +--- + +### Core Layer + +| Research-Stack | SilverSight Target | Status | Notes | +|----------------|-------------------|--------|-------| +| `Semantics.FixedPoint.lean` | `Core/SilverSightCore.lean` / `formal/CoreFormalism/Q16_16_Spec.lean` | 🟡 PORT | The full FixedPoint module with Q0_16/Q16_16 inverse trig, clamping, and determinism theorems should replace the current thin spec. | +| `Semantics.SidonSets.lean` | `Core/` or `SearchLib/` | 🟡 PORT | Proven Sidon set construction, Singer theorem, Bertrand residue injectivity. Core to addressing. | +| `Semantics.InteractionGraphSidon.lean` | `SearchLib/` | 🟡 PORT | RRC weak-axis reconstruction via CRT; part of search/addressing. | +| `Semantics.SieveLemmas.lean` | `SearchLib/` or `Core/` | 🟡 PORT | Coprime-sieve reconstruction, CRT recovery theorem, executable witnesses. | +| `Semantics.ChentsovBridge.lean` | `formal/CoreFormalism/ChentsovFinite.lean` | ✅ PORTED | Already present; keep the finite n=8 proof as the core theorem. | +| `Semantics.TransportQUBOBridge.lean` | `QUBOLib/` or `MetricLib/` | 🟡 PORT | Finsler → QUBO bridge; 0 sorries, 2 axioms with TODO(lean-port). Clean fit. | + +--- + +### LexLib / MathLib Layer + +| Research-Stack | SilverSight Target | Status | Notes | +|----------------|-------------------|--------|-------| +| `UniversalMathEncoding.lean` | `formal/UniversalEncoding/UniversalMathEncoding.lean` | ✅ PORTED | Already exists. Needs LaTeX parser (`expressionToReceipt`) completed. | +| `ChiralitySpace.lean` | `formal/UniversalEncoding/ChiralitySpace.lean` | ✅ PORTED | Already exists. | +| `math_symbols.py`, `build_math_symbols_db.py` | `python/` | 🟡 PORT | Token vocabulary builder for the 50-token address space. | +| `equation_shape_parser.py` | `python/` | 🟡 PORT | Parses equation strings into structural features. | + +--- + +### SearchLib Layer + +| Research-Stack | SilverSight Target | Status | Notes | +|----------------|-------------------|--------|-------| +| `python/chaos_game_16d.py` | `python/chaos_game.py` | 🟠 ADAPT | 16D chaos game engine. Port logic but strip Research-Stack hair (VCN refs, etc.). | +| `python/sidon_generation_kernel.py` | `python/sidon_address.py` | 🟠 ADAPT | Sidon label generation. Merge into existing `sidon_address.py`. | +| `python/geometric_entropy_explorer.py` | `python/spectral_profile.py` | 🟠 ADAPT | Entropy-exploration candidate generator. Use as basis for `SearchLib` basin exploration. | +| `python/candidate_certification_bridge.py` | `python/` | 🟠 ADAPT | Generates `Candidates.lean` from entropy exploration. Refactor to produce SilverSight receipts. | +| `Semantics.BraidEigensolid.lean` | `SearchLib/` | 🟡 PORT | Proven `eigensolid_convergence` + `receipt_invertible`. Canonical compressor target. | +| `Semantics.AntiBraidStorm.lean` | `SearchLib/` | 🟡 PORT | Adversarial verification for receipt aliasing. | + +--- + +### StructureLib Layer + +| Research-Stack | SilverSight Target | Status | Notes | +|----------------|-------------------|--------|-------| +| `formal/UniversalEncoding/ChiralitySpace.lean` | `StructureLib/` | ✅ PORTED | Already present. | +| `formal/BindingSite/*.lean` | `StructureLib/` or `Library/BindingSite/` | 🟠 ADAPT | Move from standalone directory into a library that imports only Core. | + +--- + +### MetricLib Layer + +| Research-Stack | SilverSight Target | Status | Notes | +|----------------|-------------------|--------|-------| +| `4-Infrastructure/shim/qaoa_adapter.py` | `qubo/finsler_metric.py` / `qubo/qubo_builder.py` | 🟠 ADAPT | 2,421-line QUBO ↔ Ising ↔ Pauli bridge. Split into MetricLib + QUBOLib pieces. | +| `4-Infrastructure/shim/benchmark_finsler_qap.py` | `qubo/test_optimize.py` | 🟠 ADAPT | Finsler-Randers QAP benchmark. Use as validation suite. | +| `4-Infrastructure/shim/benchmark_finsler_qaoa.py` | `qubo/test_optimize.py` | 🟠 ADAPT | Finsler-QAOA benchmark. Use as validation suite. | +| `Semantics.TransportTheory` / `Semantics.ChentsovBridge` | `MetricLib/` | 🟡 PORT | Finsler metric + Chentsov theorem formalisms. | + +--- + +### QUBOLib Layer + +| Research-Stack | SilverSight Target | Status | Notes | +|----------------|-------------------|--------|-------| +| `4-Infrastructure/shim/qaoa_adapter.py` | `qubo/qaoa_circuit.py` / `qubo/qubo_builder.py` | 🟠 ADAPT | Split: QUBO builder stays in QUBOLib; Finsler metric moves to MetricLib. | +| `4-Infrastructure/shim/qubo_highs.py` | `qubo/classical_solver.py` | 🟠 ADAPT | HiGHS MIP bridge and TSP assignment relaxation. Merge into `classical_solver.py`. | +| `4-Infrastructure/shim/pist_matrix_builder.py` | `python/` | 🟡 PORT | 250-equation PIST matrix builder; produces deterministic 8×8 strand adjacency. | +| `4-Infrastructure/shim/build_corpus250.py` | `python/` | 🟠 ADAPT | Generates RRC corpus rows. Refactor to emit SilverSight `LexLib` inputs. | + +--- + +### PVGSLib Layer + +| Research-Stack | SilverSight Target | Status | Notes | +|----------------|-------------------|--------|-------| +| `formal/PVGS_DQ_Bridge/PVGS_DQ_Bridge_fixed.lean` + sections | `formal/PVGS_DQ_Bridge/` | ✅ PORTED | Already present. Still has `sorry`s to close. | +| `Semantics.EffectiveBoundDQ.lean` | `PVGSLib/` | 🟡 PORT | DualQuaternion effective bounds; dependency for bridge. | +| `Semantics.DualQuaternion.lean` (if exists) | `PVGSLib/` | 🟡 PORT | Required by EffectiveBoundDQ. | + +--- + +### EventLib Layer + +| Research-Stack | SilverSight Target | Status | Notes | +|----------------|-------------------|--------|-------| +| `SilverSightCore.lean` TIC axiom | `Core/SilverSightCore.lean` | ✅ PORTED | Already present conceptually. | +| `python/chaos_game.py` iteration counter | `python/chaos_game.py` | 🟠 ADAPT | Make TIC derivation explicit: each chaos-game step emits an event receipt. | +| `4-Infrastructure/shim/run_trace_v2_canary.py` | `EventLib/` | 🔴 DROP | Trace-canary runner tied to Research-Stack ENE schema. Reimplement against SilverSight core. | + +--- + +### AuditLib Layer + +| Research-Stack | SilverSight Target | Status | Notes | +|----------------|-------------------|--------|-------| +| `5-Applications/tools-scripts/llm/ollama_deepseek_review_emitter.py` | `AuditLib/` | 🟠 ADAPT | Receipt verification + SHA256 answer check. Refactor to verify SilverSight receipts. | +| `4-Infrastructure/shim/pvgs_receipt_hash.py` | `formal/PVGS_DQ_Bridge/` / `AuditLib/` | ✅ PORTED | Already present in SilverSight. | +| `shared-data/data/stack_solidification/` receipts | `AuditLib/` | 🔴 DROP | Research-Stack runtime receipts; archive only. Regenerate in SilverSight. | + +--- + +### RRCLib Layer + +| Research-Stack | SilverSight Target | Status | Notes | +|----------------|-------------------|--------|-------| +| `Semantics.RRC.Emit.lean` | `RRCLib/` | 🟡 PORT | Alignment classifier; emits RRC verdicts. | +| `Semantics.RRC.Corpus250.lean` | `RRCLib/` | 🟡 PORT | 250-equation raw-feature corpus. | +| `Semantics.AVMIsa.Emit.lean` | `RRCLib/` | 🟡 PORT | **Sole output boundary** for top-level receipt JSON. | +| `Semantics.RRC.ReceiptDensity.lean` | `RRCLib/` | 🟡 PORT | Receipt density scoring. | +| `Semantics.RRCLogogramProjection.lean` | `RRCLib/` | 🟡 PORT | Logogram receipt types + admission gates. | +| `4-Infrastructure/shim/validate_rrc_predictions.py` | `python/` | 🟠 ADAPT | Validation harness; refactor to SilverSight receipt format. | + +--- + +### Infrastructure Layer + +| Research-Stack | SilverSight Target | Status | Notes | +|----------------|-------------------|--------|-------| +| `AGENTS.md` hierarchy | `docs/` + root `AGENTS.md` | 🟡 PORT | Bring root + core subtree AGENTS.md rules. Drop stale project-state blocks. | +| `REBASE_RULES.md` | root `REBASE_RULES.md` | ✅ PORTED | Already pushed. | +| `.github/workflows/lean-check.yml` | `.github/workflows/` | 🟠 ADAPT | Adapt CI to SilverSight `lake build` paths. | +| `.github/workflows/python-check.yml` | `.github/workflows/` | 🟠 ADAPT | Adapt Python test paths. | +| `.github/workflows/q16-roundtrip.yml` | `.github/workflows/` | ✅ PORTED | Already present. | +| `.devin/skills/lean-proof/SKILL.md` | `.devin/skills/` | 🟡 PORT | Mandatory for all Lean work. | +| `.github/skills/contextstream-workflow/SKILL.md` | `.github/skills/` | 🟡 PORT | Persistent memory workflow. | +| `.github/skills/research-stack-workflow/SKILL.md` | `.github/skills/` | 🟠 ADAPT | Rename to `silversight-workflow`; update paths. | +| `.cursorrules`, `.devin/config.json`, `.claude/settings.json` | root / `.devin/` | 🟡 PORT | Editor hook configs enforcing ContextStream-first rules. | +| `scripts/qc-flag/` | `scripts/qc-flag/` | 🟡 PORT | 7-check Lean QC protocol. | + +--- + +## 4. Gaps + +Things SilverSight's architecture calls for but Research-Stack does not cleanly provide: + +| Gap | Where it belongs | What to build | +|-----|------------------|---------------| +| `SilverSightCore.lean` completeness | `Core/` | Finish HachimojiState, Receipt, Instruction, δ, TIC axiom, loop invariant. Current file is a sketch. | +| LexLib / MathLib | `Library/LexLib.lean` | No complete LaTeX/ASCII tokenizer exists in Research-Stack. Build from `equation_shape_parser.py` + `math_symbols.py`. | +| EventLib | `Library/EventLib.lean` | TIC counter is conceptual only. Implement event receipts from chaos-game steps. | +| RRCLib | `Library/RRCLib/` | RRC is in `PVGS_DQ_Bridge_fixed.lean` §4. Extract into standalone library per `docs/RRC_PLACEMENT.md`. | +| Orchestrator | `Orchestrator/SilverSight.lean` | No equivalent in Research-Stack. Build new composition layer. | +| CBridge / PythonBridge | `CBridge/`, `PythonBridge/` | Mentioned in `docs/ARCHITECTURE.md` but not present. Build Q16_16 C lib + ctypes bindings. | +| Doc-sync CI | `.github/workflows/doc-sync.yml` | Exists but needs to verify porting map + architecture docs stay consistent. | + +--- + +## 5. Conflicts + +| Conflict | Resolution | +|----------|------------| +| Research-Stack `Q16_16.lean` vs SilverSight `Q16_16_Spec.lean` | SilverSight spec is thin. Replace with Research-Stack `FixedPoint.lean` (canonical, proven, includes Q0_16 + inverse trig). | +| Research-Stack `qaoa_adapter.py` (2,421 lines) vs SilverSight split `qubo/*.py` | Split adapter: Finsler/QUBO builder → MetricLib/QUBOLib; circuit generation → QUBOLib; bitstring bridge → PVGSLib. | +| Research-Stack `AGENTS.md` references many dead paths | Port rules, not state. Update path references to SilverSight equivalents. | +| SilverSight `ARCHITECTURE.md` uses 6 layers; conceptual map uses 5 | Reconcile: 5-layer conceptual map is authoritative; 6-layer doc is an older draft. Update `ARCHITECTURE.md` to match 5-layer model + library method. | + +--- + +## 6. Recommended Porting Order + +1. **Core first** — Replace `Q16_16_Spec.lean` with full `FixedPoint.lean`. Lock down `SilverSightCore.lean`. +2. **SearchLib** — Port `SidonSets.lean`, `SieveLemmas.lean`, `InteractionGraphSidon.lean`. +3. **RRCLib** — Extract RRC gates from `PVGS_DQ_Bridge_fixed.lean` §4 into standalone library. +4. **QUBOLib + MetricLib** — Split `qaoa_adapter.py` and `qubo_highs.py` cleanly. +5. **LexLib** — Build tokenizer from `math_symbols.py` + `equation_shape_parser.py`. +6. **AuditLib + EventLib** — Implement receipt validation and TIC counting. +7. **Orchestrator** — Compose all libraries through Core. +8. **Skills + editor configs** — Port agent rules last, once directory structure is stable. + +--- + +## 7. Drop List + +Do **not** port these Research-Stack artifacts: + +- `legacy/` and `ExtensionScaffold/` modules with pre-existing errors. +- Quarantined `PIST.HybridTSMPISTTorus`. +- VCN/LUPINE infrastructure (extracted to `distributed-compute-fabric`). +- Kubernetes/k3s manifests, Ray actors, Garage/restic storage scripts (extracted to `distributed-compute-fabric`). +- Stale assignment boards (`windsurf/ASSIGNMENTS.md`) and old sorry audits (`windsurf/SORRY_AUDIT.md`). +- Runtime DBs, consolidation manifests, and generated receipts under `shared-data/` and `.headroom/`. +- `.agents/plugins/marketplace.json` and dormant substack-connector. +- Biological/genetics extensions unless the BindingSite direction is pursued. + +--- + +*This map is a living document. Update it as components are ported or reclassified.*