From 7098ee0d640ce436a1e45832999d4c10ed8096a1 Mon Sep 17 00:00:00 2001 From: allaun Date: Sun, 21 Jun 2026 14:01:42 -0500 Subject: [PATCH] docs(specs): add SilverSight specification draft with Core Semantics sections Adds 6-Documentation/docs/specs/SilverSight_Spec.md, documenting the YaFF-inspired separation of schema, layout, access pattern, wire format, view, layout bridge, and canal-aware layout selection for the SilverSight clean-slate architecture. --- .../docs/specs/SilverSight_Spec.md | 390 ++++++++++++++++++ 1 file changed, 390 insertions(+) create mode 100644 6-Documentation/docs/specs/SilverSight_Spec.md diff --git a/6-Documentation/docs/specs/SilverSight_Spec.md b/6-Documentation/docs/specs/SilverSight_Spec.md new file mode 100644 index 00000000..12f7f352 --- /dev/null +++ b/6-Documentation/docs/specs/SilverSight_Spec.md @@ -0,0 +1,390 @@ +# SilverSight Specification + +**Status:** Draft — architecture target for the Research Stack clean rebase + +**Version:** 0.1 + +**Date:** 2026-06-21 + +**Ground truth:** Lean 4 (`0-Core-Formalism/lean/SilverSight/`) + +--- + +## 1. Purpose + +**SilverSight** is the clean-slate successor to the Research Stack. It keeps every formally verified concept, discards the accumulated duplication and unproven scaffolding, and re-expresses the system as a single, searchable, substrate-agnostic compute fabric. + +Goals: + +- Every concept has a **stable ID**, a **Lean definition**, and a **receipt**. +- All admissibility, routing, alignment, and gating decisions live in Lean. +- Python, Rust, and Verilog are **extraction targets only**; they contain no logic. +- The same formal object can be serialized to **1-Wire**, **PCIe**, **DRAM**, or **JSON** without changing its meaning. +- Claims advance through the claim-state ladder: `BEAUTIFUL_PROVISIONAL` → `CALIBRATED_ENGINEERING_DELTA` → `REVIEWED` → `VERIFIED`. + +Non-goals: + +- Preserving the legacy directory tree. +- Carrying forward duplicate `Q16_16` definitions, unproven Python shims, demo scripts, or SaaS integrations. +- Supporting floating-point arithmetic in compute paths. + +--- + +## 2. Axioms + +1. **Lean is the source of truth.** Every other representation is a shim or extraction target. +2. **Fixed-point only.** `Q0_16` is the default for dimensionless scalars. `Q16_16` is allowed only with a documented, theorem-backed reason. `Float` is banned in core compute paths. +3. **No `sorry` in the main build.** Proof holes may exist only in quarantined modules with a `TODO(lean-port)` ticket and human sign-off. +4. **All composition is `bind`.** If a domain cannot be expressed as a `bind` instance with a lawful check, a cost function, and an invariant extractor, the domain is ill-posed. +5. **Every substrate is equivalent.** A 1-Wire bus, a PCIe lane, and a DRAM trace are different physical instantiations of the same `DynamicCanal` geometry. +6. **Receipts are the compressed state.** A receipt is not metadata; it is the encoding. Invertibility of the receipt is the definition of lossless transformation. +7. **Claims need evidence.** LLM agreement, elegance, or coherence do not promote a claim. + +--- + +## 3. Concepts Borrowed from YaFF + +YaFF (Yet another Flat Format) provides a useful conceptual separation: **schema is not layout**. SilverSight formalizes this in Lean. + +### 3.1 Schema / Layout / WireFormat + +These three concepts live in separate Core modules so that schema and layout can never be confused. + +```lean +-- Core/SilverSight/Semantics/Schema.lean +class Schema (α : Type) where + byteSize : Nat + wellFormed : α → Bool + +-- Core/SilverSight/Semantics/Layout.lean +inductive Layout where + | rowMajor + | columnar + | compact + | mmapView + +-- Core/SilverSight/Semantics/WireFormat.lean +structure WireFormat (α : Type) [Schema α] (layout : Layout) where + encode : α → ByteArray + decode : ByteArray → Option α + encode_size : ∀ a, (encode a).size = byteSize α + roundTrip : ∀ a, decode (encode a) = some a + +-- Core examples (row-major encodings for Bool and UInt8) +def boolRowMajor : WireFormat Bool rowMajor +def uint8RowMajor : WireFormat UInt8 rowMajor +``` + +- `Schema α` (`Core/SilverSight/Semantics/Schema.lean`) is the source of truth. It gives the canonical wire size and a well-formedness predicate. Core schemas are fixed-size; variable-length containers are library extensions that point into separately-scoped buffers. +- `Layout` (`Core/SilverSight/Semantics/Layout.lean`) is a physical encoding choice, not a logical shape. +- `WireFormat α layout` (`Core/SilverSight/Semantics/WireFormat.lean`) is a certified encoder/decoder pair whose `roundTrip` field is a Lean proof. + +### 3.2 Zero-Copy Views + +A `View` is a theorem that a structured value can be read from a byte range without copying the underlying buffer. + +```lean +-- Core/SilverSight/Semantics/View.lean +structure View (α : Type) [Schema α] where + base : ByteArray + offset : Nat + valid : offset + byteSize α ≤ base.size + +def View.readUInt8 (v : View UInt8) : UInt8 +``` + +The `valid` invariant is address arithmetic, not a runtime check. For a `UInt8` view it reduces to `offset < base.size`; `readUInt8` returns the byte at `offset` without copying the buffer. Multi-byte accessors are a library extension that must preserve the same `offset + byteSize α ≤ base.size` invariant. + +### 3.3 Layout Bridges + +For any two layouts of the same schema, a `LayoutBridge` converts between them and preserves meaning: + +```lean +-- Core/SilverSight/Semantics/LayoutBridge.lean +structure LayoutBridge (α : Type) [Schema α] (L1 L2 : Layout) where + wf1 : WireFormat α L1 + wf2 : WireFormat α L2 + convert : ByteArray → ByteArray + correct : ∀ a, convert (wf1.encode a) = wf2.encode a +``` + +The bridge carries the source and target `WireFormat` values so that `correct` is a concrete equality between certified encodings. This has the same shape as `BraidState` / `crossStep` convergence: a transformation that preserves an invariant. The Core supplies identity bridges; row-major ↔ columnar and compact-expansion bridges are library extensions. + +### 3.4 Adaptive Layout Selection + +The Core provides a pure cost-based layout selector in `Core/SilverSight/Semantics/Layout.lean`: + +```lean +def Layout.cost (layout : Layout) (profile : AccessProfile) : Q0_16 + +def chooseLayoutByCost (profile : AccessProfile) : Layout + +theorem chooseLayoutByCost_le (profile : AccessProfile) (l : Layout) : + Layout.cost (chooseLayoutByCost profile) profile ≤ Layout.cost l profile +``` + +`chooseLayoutByCost` folds over `allLayouts` and picks the cheapest; the theorem proves it is ε-suboptimal (no Core layout is cheaper for the given profile). + +Regime-aware selection is added in `Core/SilverSight/Semantics/CanalLayout.lean`: + +```lean +-- Core/SilverSight/Semantics/CanalLayout.lean +inductive CanalRegime where + | coherent + | stressed + | throat + +def chooseLayout (profile : AccessProfile) (regime : CanalRegime) : Layout +``` + +A `CanalRegime` can override the cost-based choice when the substrate is in a known pressure state. The Core keeps the cost model and the regime override separate so that layout choice remains a decision, not a built-in physical constant. + +### 3.5 Where YaFF Concepts Are Used + +| YaFF idea | SilverSight location | Use | +|-----------|----------------------|-----| +| Schema / layout separation | `Semantics.Schema` / `Semantics.Layout` / `Semantics.WireFormat` | Certified encodings for receipts and braid states | +| Zero-copy views | `Semantics.View` | Formal address arithmetic for DMA/mmap surfaces | +| Layout bridges | `Semantics.LayoutBridge` | Proven conversions between row/columnar/compact formats | +| Adaptive layouts | `Semantics.CanalLayout` (decision) + `CoreFormalism.DynamicCanal` (physics) | Layout choice as a function of pressure regime | +| Columnar layout | `Semantics.Layout.columnar` (future `RRC.Corpus250`) | Efficient matrix storage for PIST/RRC data | + +YaFF itself is **not a dependency**. Only the concepts are borrowed and re-proved in Lean. + +--- + +## 4. The 1-Wire Substrate Model + +The 1-Wire concept from `PCIE_IDLE_CYCLE_SUBSTRATE_SPEC.md` becomes the hardware extraction floor. + +### 4.1 DynamicCanal as Universal Substrate + +- The Core abstracts substrate pressure into `Semantics.CanalRegime` (`coherent`, `stressed`, `throat`), used by `chooseLayout`. +- The library `CoreFormalism.DynamicCanal` provides the full physics: `Lane`, `Timing`, `pressure`, `lambdaEff`, and `classifyRegime`. +- The canal widens under pressure: `λ_eff(P)` decreases, allowing more flow. +- `Timing.lean` derives physical timing parameters from the canal state. + +### 4.2 1-Wire Mapping + +A 1-Wire transaction is a sequence of timed pulses: + +| Pulse | DynamicCanal meaning | Trit | +|-------|----------------------|------| +| Reset pulse | Descriptor ring head advance | — | +| Presence pulse | Controller ACK / device alive | — | +| Write-1 slot (long) | Canal wide, high pressure | +1 | +| Write-0 slot (short) | Canal narrow, low pressure | -1 | +| Read slot (sampled) | Canal coherent, steady state | 0 | + +The trit stream feeds the trinary VM (`DynamicCanal.LanePayload`). The VM state is folded into a `Q0_16` scalar receipt. + +### 4.3 Substrate Independence + +The same scalar receipt is derived whether the physical path is: + +- a $1 DS18B20 on a 1-Wire bus, +- a PCIe Gen 5 lane, +- a DRAM fly-by trace, +- a JSON boundary shim. + +The substrate determines throughput; the invariant is unchanged. + +--- + +## 5. Architecture + +SilverSight collapses the old seven-layer tree into five layers. Each layer exports only data structures and `bind` instances to the next layer. + +```text +0-Core-Formalism/ + lean/SilverSight/ + Semantics/ -- Schema, Layout, WireFormat, DynamicCanal, Bind, Receipt + RRC/ -- Receipt routing and classification + FixedPoint/ -- Q0_16, Q16_16, deterministic arithmetic + AVM/ -- ON HOLD until Phase 2 ISA rebuild +1-Search-Space/ + corpus/ -- Token-strand matrices, PIST predictions, concept index + probes/ -- Hutter Prize, FAMM scars, entropy explorers +2-Mathematical-Models/ + physics/ -- Manifolds, PIST, BraidStorm, TSM + compression/ -- Eigensolid convergence, receipt invertibility +3-Infrastructure/ + shims/ -- Pure I/O: JSON read/write, DB calls, subprocess spawn + hardware/ -- FPGA, Verilog, UART, DMA bring-up docs and receipts + databases/ -- Postgres and Gremlin schema manifests +4-Applications/ + cad/ -- Text-to-CAD harness + llm-review/ -- Ollama/DeepSeek review emitter + dashboards/ -- Hermes, monitoring, telemetry +5-Documentation/ + specs/ -- Architecture and interface specs + claims/ -- Claim-state ladder manifests + wiki/ -- Human-readable concept reference +``` + +### 5.1 Layer Contracts + +| Layer | Owns | Must Not Own | +|-------|------|--------------| +| Core Formalism | Definitions, theorems, schemas, layouts, costs | I/O, secrets, float | +| Search Space | Raw features, matrices, candidate manifests | Admissibility logic | +| Mathematical Models | Physics equations, compression theorems | Hardware pinouts | +| Infrastructure | I/O scripts, DB schemas, deployment manifests | Cost functions | +| Applications | User interfaces, review emitters, CAD hooks | Core invariants | +| Documentation | Specs, claim manifests, evidence DAGs | Executable logic | + +--- + +## 6. Stable IDs and Concept Map + +Every concept receives a stable ID: + +```text +silversight___ +``` + +Examples: + +- `silversight_math_0a1b2c_eigensolidConvergence` +- `silversight_doc_3d4e5f_wireFrameLayout` +- `silversight_py_6g7h8i_extractAllConcepts` + +IDs are stored in: + +- `extraction/data_inventory.json` — database + repo file summary +- `extraction/all_concepts_merged.json` — unified concept list +- PostgreSQL `arxiv.math_objects` — structured math objects +- Gremlin `concepts` graph — vertices and edges + +The inventory script `scripts/inventory_everything.py` regenerates the map from all sources. + +--- + +## 7. Porting Criteria from Research Stack + +### 7.1 Keep + +- Lean modules that compile under `lake build` with zero errors. +- Curated `extraction/math.json` and `extraction/ideas.json`. +- Hardware receipts with instrument provenance (SRAM load, UART beacon, bitstream hash). +- Verified compression receipts with corpus provenance and SI compression ratios. +- The `bind` primitive and existing `bind` instances. + +### 7.2 Delete + +- Duplicate `Q16_16` type definitions (unify to `Semantics.FixedPoint`). +- Python files containing cost computation, invariant checks, or branching decisions. +- Demo scripts, benchmark scraps, and `demo_*.py` files. +- Integrations with external SaaS (OpenWebUI tools, scrapers, cloud APIs). +- Legacy branches and cornfielded code unless explicitly recovered. +- Files that cannot be typed without `unsafe` or `sorry`. + +### 7.3 Transform + +- Python shims → pure I/O wrappers (read JSON, write JSONL, spawn subprocess). +- Markdown specs → structured spec sections under `5-Documentation/specs/`. +- Rust modules → extraction targets generated from Lean specs. +- Verilog → combinational logic derived from Lean theorems. + +--- + +## 8. Verification Requirements + +Before any module is promoted to `VERIFIED`: + +1. `lake build` passes with zero errors in `0-Core-Formalism/lean/SilverSight/`. +2. Every `def` that computes a cost or invariant has either: + - an `#eval` example with expected output in a comment, or + - a theorem proving a property. +3. No `sorry` in the main import path. +4. No `Float` in core compute paths. +5. All fixed-point operations are deterministic across x86, ARM, and RISC-V. +6. Statistical claims meet the 5σ minimum (6.5σ preferred). +7. Compression claims use SI ratio `original / compressed` and baseline against zlib/gzip/brotli/zstd. +8. Physical claims use SI units and include uncertainty quantification. +9. Hardware claims include continuous state verification (not just exit codes). +10. Staged files pass `git diff --cached --check` and a secret scan. + +--- + +## 9. Migration Phases + +### Phase 0 — Inventory and Spec (current) + +- Complete concept inventory: Postgres, Gremlin, local repo. +- Finalize this spec and the target directory structure. +- Identify all duplicate `Q16_16` definitions and quarantine unproven modules. + +### Phase 1 — Core Lean Modules + +Create the SilverSight core in Lean: + +- `Semantics.Schema` +- `Semantics.Layout` +- `Semantics.WireFormat` +- `Semantics.View` +- `Semantics.LayoutBridge` +- `Semantics.DynamicCanal` +- `Semantics.Receipt` +- `Semantics.Bind` +- `FixedPoint.Q0_16` / `Q16_16` + +### Phase 2 — Port Verified Theorems + +- Move theorems from `0-Core-Formalism/lean/Semantics/` that compile cleanly. +- Delete duplicates. +- Quarantine modules with `sorry` outside the main import path. + +### Phase 3 — Rewrite Shims + +- Convert Python scripts to pure I/O. +- Update `distribute_extraction.py` to use only certified concepts. +- Keep `inventory_everything.py` as the canonical map generator. + +### Phase 4 — Hardware Extraction + +- Generate Verilog from Lean specs. +- Produce FPGA receipts with bitstream hashes and UART beacons. +- Prove `fpga_extraction_correctness` for each burned DAG-LUT. + +### Phase 5 — Documentation and Promotion + +- Write specs under `5-Documentation/specs/`. +- Maintain claim-state manifests. +- Promote claims only with reviewer provenance and reproducible evidence. + +--- + +## 10. Cost and Compute Notes + +For the conversion grunt work (restructure/rename modules across ~26.6M tokens of Lean): + +- **MiMo v2.5 Pro API** input-only: ~$11.56 +- **MiMo v2.5 Pro API** plan + apply pass: ~$23–$35 +- **Local H200 rental** with a 27B 2-bit MTP model: borderline; likely $40–$90 depending on actual tok/s +- **API is cheaper** for a one-shot refactor; local GPU only wins for multi-pass or privacy-sensitive workloads. + +--- + +## 11. Open Questions + +1. What is the exact module granularity for the SilverSight core? One namespace per file is required. +2. Does AVM stay on hold, or is it rebuilt as part of Phase 2? +3. How are Mathlib and other `.lake` dependencies vendored in the new repo? +4. Which legacy Python scripts are essential I/O shims vs. deletable decision logic? +5. What is the canonical claim-state manifest format? + +--- + +## 12. Summary + +SilverSight is not a refactor. It is a **rebase**: + +- Same formal truths. +- Fewer files. +- Cleaner boundaries. +- Searchable concept map. +- Hardware-extractable receipts. +- Lean as the single source of truth. + +The immediate next step is Phase 1: write the core Lean modules that formalize the YaFF-inspired schema/layout separation and the 1-Wire substrate model.