From b6ab3e5f22d7bb236404e5489e19566b7c19e595 Mon Sep 17 00:00:00 2001 From: allaun Date: Mon, 22 Jun 2026 15:05:14 -0500 Subject: [PATCH] refactor(silversight): move to correct location + set no-write on Research Stack MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit SilverSight modules moved from Semantics/Semantics/SilverSight/ to SilverSight/SilverSight/ (separate directory, same lake project). Changes: - SilverSight Lean modules: Schema, WireFormat, ProductSchema, ProductWireFormat, Receipt, Bind → 0-Core-Formalism/lean/SilverSight/ - Imports updated: Semantics.SilverSight.* → SilverSight.* - Namespace updated: Semantics.SilverSight → SilverSight - Cross-project imports preserved: Semantics.FixedPoint, open Semantics.FixedPoint - lakefile.toml: SilverSight lean_lib now uses srcDir = ../SilverSight - AGENTS.md: READ-ONLY notice added — Research Stack is archived, all new formal work goes to SilverSight - SilverSight/AGENTS.md: clean-slate operating contract Build: SilverSight 3307 jobs, 0 errors Build: Compiler 3314 jobs, 0 errors --- .../lean/Semantics/Semantics/SilverSight.lean | 8 --- 0-Core-Formalism/lean/Semantics/lakefile.toml | 8 ++- 0-Core-Formalism/lean/SilverSight/AGENTS.md | 63 +++++++++++++++++++ .../lean/SilverSight/SilverSight.lean | 8 +++ .../SilverSight/Bind.lean | 6 +- .../SilverSight/ProductSchema.lean | 6 +- .../SilverSight/ProductWireFormat.lean | 8 +-- .../SilverSight/Receipt.lean | 4 +- .../SilverSight/Schema.lean | 4 +- .../SilverSight/WireFormat.lean | 6 +- AGENTS.md | 22 +++++++ 11 files changed, 115 insertions(+), 28 deletions(-) delete mode 100644 0-Core-Formalism/lean/Semantics/Semantics/SilverSight.lean create mode 100644 0-Core-Formalism/lean/SilverSight/AGENTS.md create mode 100644 0-Core-Formalism/lean/SilverSight/SilverSight.lean rename 0-Core-Formalism/lean/{Semantics/Semantics => SilverSight}/SilverSight/Bind.lean (98%) rename 0-Core-Formalism/lean/{Semantics/Semantics => SilverSight}/SilverSight/ProductSchema.lean (96%) rename 0-Core-Formalism/lean/{Semantics/Semantics => SilverSight}/SilverSight/ProductWireFormat.lean (95%) rename 0-Core-Formalism/lean/{Semantics/Semantics => SilverSight}/SilverSight/Receipt.lean (98%) rename 0-Core-Formalism/lean/{Semantics/Semantics => SilverSight}/SilverSight/Schema.lean (97%) rename 0-Core-Formalism/lean/{Semantics/Semantics => SilverSight}/SilverSight/WireFormat.lean (97%) diff --git a/0-Core-Formalism/lean/Semantics/Semantics/SilverSight.lean b/0-Core-Formalism/lean/Semantics/Semantics/SilverSight.lean deleted file mode 100644 index a05034b2..00000000 --- a/0-Core-Formalism/lean/Semantics/Semantics/SilverSight.lean +++ /dev/null @@ -1,8 +0,0 @@ -import Semantics.SilverSight.Schema -import Semantics.SilverSight.WireFormat -import Semantics.SilverSight.ProductSchema -import Semantics.SilverSight.ProductWireFormat -import Semantics.SilverSight.Receipt -import Semantics.SilverSight.Bind - -namespace Semantics.SilverSight diff --git a/0-Core-Formalism/lean/Semantics/lakefile.toml b/0-Core-Formalism/lean/Semantics/lakefile.toml index e6263f9b..90c76731 100644 --- a/0-Core-Formalism/lean/Semantics/lakefile.toml +++ b/0-Core-Formalism/lean/Semantics/lakefile.toml @@ -52,11 +52,13 @@ name = "ExtensionScaffold" [[lean_lib]] name = "Biology" -# ── SilverSight: schema/layout/wireformat core ────────────────────────────── -# Phase 1 core: product-type encoders, Receipt/Bind composition primitive. +# ── SilverSight: clean-slate rebase ───────────────────────────────────────── +# Lives at 0-Core-Formalism/lean/SilverSight/ (separate from Semantics tree). +# Imports Semantics.FixedPoint cross-project. Build: lake build SilverSight [[lean_lib]] name = "SilverSight" -roots = ["Semantics.SilverSight"] +srcDir = "../SilverSight" +roots = ["SilverSight"] # OTOM external proofs — uncomment when resolving sorries. # Build: lake build OTOMProofs diff --git a/0-Core-Formalism/lean/SilverSight/AGENTS.md b/0-Core-Formalism/lean/SilverSight/AGENTS.md new file mode 100644 index 00000000..cd4f8c68 --- /dev/null +++ b/0-Core-Formalism/lean/SilverSight/AGENTS.md @@ -0,0 +1,63 @@ +# AGENTS.md — SilverSight + +**SilverSight is the clean-slate rebase of the Research Stack.** + +## Location + +``` +0-Core-Formalism/lean/SilverSight/ + SilverSight/ + Schema.lean + WireFormat.lean + ProductSchema.lean + ProductWireFormat.lean + Receipt.lean + Bind.lean + SilverSight.lean ← root import +``` + +## Rules + +1. **SilverSight is the ONLY target for new formal work.** Do NOT add new modules to `0-Core-Formalism/lean/Semantics/Semantics/`. All new Lean code goes here. + +2. **Imports from Semantics are allowed** (cross-project): `import Semantics.FixedPoint`, `import Semantics.Spectrum`, etc. + +3. **No `sorry` in committed code.** Same rule as the Research Stack. + +4. **No `Float` in compute paths.** Use `Q0_16` or `Q16_16`. + +5. **Build gate:** `lake build SilverSight` must pass (3307 jobs, 0 errors as of 2026-06-22). + +6. **Every new module needs:** + - `@[simp]` theorems for key computations + - `#eval` witnesses with expected output in comments + - A docstring explaining the module's purpose + +7. **The claim manifest** lives at `6-Documentation/docs/claims/manifest_v1.json` (shared with Research Stack docs). + +## What Belongs Here + +- Schema/Layout/WireFormat core (YaFF-inspired) +- Product-type encoders +- Receipt/Bind composition primitive +- DynamicCanal physics (when ported) +- RRC corpus and PIST pipeline (when ported) +- Compression theorems (when ported) + +## What Does NOT Belong Here + +- Research Stack legacy modules (stay in `Semantics/Semantics/`) +- Python shims (stay in `4-Infrastructure/shim/`) +- Documentation (stay in `6-Documentation/`) +- Extraction JSONs (stay in `extraction/`) + +## Current Status + +| Module | Status | Sorry | +|--------|--------|-------| +| Schema.lean | Complete | 0 | +| WireFormat.lean | Complete | 0 | +| ProductSchema.lean | Complete | 0 | +| ProductWireFormat.lean | Complete | 0 | +| Receipt.lean | Complete | 0 | +| Bind.lean | Complete | 0 | diff --git a/0-Core-Formalism/lean/SilverSight/SilverSight.lean b/0-Core-Formalism/lean/SilverSight/SilverSight.lean new file mode 100644 index 00000000..9066c4c2 --- /dev/null +++ b/0-Core-Formalism/lean/SilverSight/SilverSight.lean @@ -0,0 +1,8 @@ +import SilverSight.Schema +import SilverSight.WireFormat +import SilverSight.ProductSchema +import SilverSight.ProductWireFormat +import SilverSight.Receipt +import SilverSight.Bind + +namespace Semantics.SilverSight diff --git a/0-Core-Formalism/lean/Semantics/Semantics/SilverSight/Bind.lean b/0-Core-Formalism/lean/SilverSight/SilverSight/Bind.lean similarity index 98% rename from 0-Core-Formalism/lean/Semantics/Semantics/SilverSight/Bind.lean rename to 0-Core-Formalism/lean/SilverSight/SilverSight/Bind.lean index 5411b14b..8e89a30e 100644 --- a/0-Core-Formalism/lean/Semantics/Semantics/SilverSight/Bind.lean +++ b/0-Core-Formalism/lean/SilverSight/SilverSight/Bind.lean @@ -1,6 +1,6 @@ -import Semantics.SilverSight.Receipt +import SilverSight.Receipt -namespace Semantics.SilverSight +namespace SilverSight open Semantics.FixedPoint open Semantics.FixedPoint.Q16_16 @@ -111,4 +111,4 @@ def r3 := mkReceipt .validate (Q16_16.ofInt 20) "wellformed" 3 #eval (bindReceipt r1 r2).cost -- expected: 5242880 (Q16_16 of 80) #eval (bindReceipt r1 r2).wellFormed -- expected: true -end Semantics.SilverSight +end SilverSight diff --git a/0-Core-Formalism/lean/Semantics/Semantics/SilverSight/ProductSchema.lean b/0-Core-Formalism/lean/SilverSight/SilverSight/ProductSchema.lean similarity index 96% rename from 0-Core-Formalism/lean/Semantics/Semantics/SilverSight/ProductSchema.lean rename to 0-Core-Formalism/lean/SilverSight/SilverSight/ProductSchema.lean index dc99df31..8382c32c 100644 --- a/0-Core-Formalism/lean/Semantics/Semantics/SilverSight/ProductSchema.lean +++ b/0-Core-Formalism/lean/SilverSight/SilverSight/ProductSchema.lean @@ -1,6 +1,6 @@ -import Semantics.SilverSight.Schema +import SilverSight.Schema -namespace Semantics.SilverSight +namespace SilverSight open Semantics.FixedPoint @@ -45,4 +45,4 @@ theorem prod_wellFormed [Schema α] [Schema β] (a : α) (b : β) : #eval Schema.byteSize ((UInt8 × UInt8) × UInt32) -- expected: 6 #eval Schema.byteSize (UInt8 × UInt8 × UInt32) -- expected: 6 -end Semantics.SilverSight +end SilverSight diff --git a/0-Core-Formalism/lean/Semantics/Semantics/SilverSight/ProductWireFormat.lean b/0-Core-Formalism/lean/SilverSight/SilverSight/ProductWireFormat.lean similarity index 95% rename from 0-Core-Formalism/lean/Semantics/Semantics/SilverSight/ProductWireFormat.lean rename to 0-Core-Formalism/lean/SilverSight/SilverSight/ProductWireFormat.lean index eb8bddf7..cc8bcf43 100644 --- a/0-Core-Formalism/lean/Semantics/Semantics/SilverSight/ProductWireFormat.lean +++ b/0-Core-Formalism/lean/SilverSight/SilverSight/ProductWireFormat.lean @@ -1,7 +1,7 @@ -import Semantics.SilverSight.WireFormat -import Semantics.SilverSight.ProductSchema +import SilverSight.WireFormat +import SilverSight.ProductSchema -namespace Semantics.SilverSight +namespace SilverSight open Semantics.FixedPoint @@ -64,4 +64,4 @@ def boolPairRowMajor : WireFormat (Bool × Bool) Layout.rowMajor where #eval uint8BoolRowMajor.decode (ByteArray.mk #[42, 1]) -- expected: some (42, true) #eval Schema.byteSize (UInt8 × Bool) -- expected: 2 -end Semantics.SilverSight +end SilverSight diff --git a/0-Core-Formalism/lean/Semantics/Semantics/SilverSight/Receipt.lean b/0-Core-Formalism/lean/SilverSight/SilverSight/Receipt.lean similarity index 98% rename from 0-Core-Formalism/lean/Semantics/Semantics/SilverSight/Receipt.lean rename to 0-Core-Formalism/lean/SilverSight/SilverSight/Receipt.lean index 6be29fb1..f5a07e8d 100644 --- a/0-Core-Formalism/lean/Semantics/Semantics/SilverSight/Receipt.lean +++ b/0-Core-Formalism/lean/SilverSight/SilverSight/Receipt.lean @@ -1,6 +1,6 @@ import Semantics.FixedPoint -namespace Semantics.SilverSight +namespace SilverSight open Semantics.FixedPoint open Semantics.FixedPoint.Q16_16 @@ -74,4 +74,4 @@ def Receipt.sharesInvariant (r1 r2 : Receipt) : Bool := r1.invariant == r2.invar #eval (mkReceipt .encode Q16_16.zero "A" 1).sharesInvariant (mkReceipt .decode Q16_16.zero "A" 2) -- expected: true #eval (mkReceipt .encode Q16_16.zero "A" 1).sharesInvariant (mkReceipt .decode Q16_16.zero "B" 2) -- expected: false -end Semantics.SilverSight +end SilverSight diff --git a/0-Core-Formalism/lean/Semantics/Semantics/SilverSight/Schema.lean b/0-Core-Formalism/lean/SilverSight/SilverSight/Schema.lean similarity index 97% rename from 0-Core-Formalism/lean/Semantics/Semantics/SilverSight/Schema.lean rename to 0-Core-Formalism/lean/SilverSight/SilverSight/Schema.lean index 6270077b..c9594db3 100644 --- a/0-Core-Formalism/lean/Semantics/Semantics/SilverSight/Schema.lean +++ b/0-Core-Formalism/lean/SilverSight/SilverSight/Schema.lean @@ -1,6 +1,6 @@ import Semantics.FixedPoint -namespace Semantics.SilverSight +namespace SilverSight open Semantics.FixedPoint @@ -65,4 +65,4 @@ instance : Schema Q0_16 where #eval Schema.byteSize Q16_16 -- expected: 4 #eval Schema.byteSize Q0_16 -- expected: 2 -end Semantics.SilverSight +end SilverSight diff --git a/0-Core-Formalism/lean/Semantics/Semantics/SilverSight/WireFormat.lean b/0-Core-Formalism/lean/SilverSight/SilverSight/WireFormat.lean similarity index 97% rename from 0-Core-Formalism/lean/Semantics/Semantics/SilverSight/WireFormat.lean rename to 0-Core-Formalism/lean/SilverSight/SilverSight/WireFormat.lean index 00d1bedb..b79ab3c0 100644 --- a/0-Core-Formalism/lean/Semantics/Semantics/SilverSight/WireFormat.lean +++ b/0-Core-Formalism/lean/SilverSight/SilverSight/WireFormat.lean @@ -1,6 +1,6 @@ -import Semantics.SilverSight.Schema +import SilverSight.Schema -namespace Semantics.SilverSight +namespace SilverSight open Semantics.FixedPoint @@ -71,4 +71,4 @@ def boolRowMajor : WireFormat Bool Layout.rowMajor where #eval boolRowMajor.decode (boolRowMajor.encode true) -- expected: some true #eval boolRowMajor.decode (boolRowMajor.encode false) -- expected: some false -end Semantics.SilverSight +end SilverSight diff --git a/AGENTS.md b/AGENTS.md index 76085eeb..eb4b5f8c 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -2,6 +2,28 @@ This file is the first stop for coding agents working in this repository. +## ⛔ READ-ONLY NOTICE — SilverSight Has Replaced This Repo + +**The Research Stack is a READ-ONLY archive.** SilverSight is the clean-slate +successor. All new formal work MUST go to `0-Core-Formalism/lean/SilverSight/`. + +| Action | Allowed? | +|--------|----------| +| Add new Lean modules to `Semantics/Semantics/` | **NO** → use `SilverSight/` | +| Add new Python shims to `4-Infrastructure/shim/` | **NO** → use SilverSight shim dir | +| Edit existing Research Stack files (bug fixes, doc updates) | **YES** | +| Run `lake build` on existing modules | **YES** | +| Run DB sync scripts | **YES** | +| Add new AGENTS.md rules to Research Stack | **NO** → add to SilverSight | + +**Enforcement:** Any agent that adds new files to the Research Stack Lean tree +(`0-Core-Formalism/lean/Semantics/Semantics/`) instead of SilverSight +(`0-Core-Formalism/lean/SilverSight/`) is violating this contract. + +**SilverSight location:** `0-Core-Formalism/lean/SilverSight/` +**SilverSight AGENTS.md:** `0-Core-Formalism/lean/SilverSight/AGENTS.md` +**SilverSight build:** `lake build SilverSight` (from `0-Core-Formalism/lean/Semantics/`) + ## Local Hermes Deployment (2026-06-20) Hermes Agent v0.14.0 is the primary chat/dashboard gateway, serving the