# 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.