Research-Stack/6-Documentation/docs/specs/SilverSight_Spec.md

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.

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

-- 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:

-- 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:

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:

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

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:

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.