mirror of
https://github.com/allaunthefox/Research-Stack.git
synced 2026-07-31 03:05:21 +00:00
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.
This commit is contained in:
parent
5bea52a09a
commit
7098ee0d64
1 changed files with 390 additions and 0 deletions
390
6-Documentation/docs/specs/SilverSight_Spec.md
Normal file
390
6-Documentation/docs/specs/SilverSight_Spec.md
Normal file
|
|
@ -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_<type>_<source_hash>_<name_hash>
|
||||
```
|
||||
|
||||
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.
|
||||
Loading…
Add table
Reference in a new issue