mirror of
https://github.com/allaunthefox/Research-Stack.git
synced 2026-07-31 03:05:21 +00:00
docs: SilverSight directory structure specification
Formalizes: - Naming conventions (PascalCase dirs, PascalCase.lean files) - Repository root structure (formal/, python/, qubo/, tests/, docs/) - Module naming (Schema, WireFormat, ProductSchema, etc.) - Import conventions (cross-project from Semantics) - Build targets (lake build SilverSight) - File size limits (500 lines max per Lean module) - What goes where (formal → formal/, shims → python/, etc.)
This commit is contained in:
parent
22782776a9
commit
5e0f8b72f1
1 changed files with 140 additions and 0 deletions
140
0-Core-Formalism/lean/SilverSight/DIRECTORY_SPEC.md
Normal file
140
0-Core-Formalism/lean/SilverSight/DIRECTORY_SPEC.md
Normal file
|
|
@ -0,0 +1,140 @@
|
|||
# SilverSight Directory Structure Specification
|
||||
|
||||
## Naming Conventions
|
||||
|
||||
| Item | Convention | Example |
|
||||
|------|-----------|---------|
|
||||
| Directory | `PascalCase` | `SilverSight/`, `CoreFormalism/` |
|
||||
| Lean file | `PascalCase.lean` | `Schema.lean`, `WireFormat.lean` |
|
||||
| Python file | `snake_case.py` | `chaos_game.py`, `q16_16_roundtrip.py` |
|
||||
| Config file | `lowercase.ext` | `lakefile.toml`, `lean-toolchain` |
|
||||
| Documentation | `UPPER_CASE.md` or `PascalCase.md` | `AGENTS.md`, `README.md` |
|
||||
|
||||
## Repository Root
|
||||
|
||||
```
|
||||
SilverSight/
|
||||
├── AGENTS.md ← operating contract
|
||||
├── README.md ← public-facing docs
|
||||
├── CITATION.cff ← citation metadata
|
||||
├── REBASE_RULES.md ← migration rules
|
||||
├── PORTING_MAP.md ← Research Stack → SilverSight mapping
|
||||
├── lakefile.toml ← Lean build config
|
||||
├── lean-toolchain ← Lean version pin
|
||||
├── lake-manifest.json ← dependency lockfile
|
||||
├── pytest.ini ← Python test config
|
||||
├── requirements.txt ← Python dependencies
|
||||
│
|
||||
├── formal/ ← Lean 4 formal modules
|
||||
│ ├── SilverSight/ ← core SilverSight modules
|
||||
│ │ ├── Schema.lean
|
||||
│ │ ├── WireFormat.lean
|
||||
│ │ ├── ProductSchema.lean
|
||||
│ │ ├── ProductWireFormat.lean
|
||||
│ │ ├── Receipt.lean
|
||||
│ │ ├── Bind.lean
|
||||
│ │ ├── AVMIsa/ ← AVM ISA surface
|
||||
│ │ ├── RRC/ ← Rainbow Raccoon Compiler
|
||||
│ │ └── PIST/ ← PIST classification
|
||||
│ │
|
||||
│ ├── CoreFormalism/ ← foundational theorems
|
||||
│ │ ├── FixedPoint.lean
|
||||
│ │ ├── SidonSets.lean
|
||||
│ │ └── ...
|
||||
│ │
|
||||
│ ├── PVGS_DQ_Bridge/ ← photon-varied Gaussian state bridge
|
||||
│ ├── UniversalEncoding/ ← 50-token math address space
|
||||
│ ├── BindingSite/ ← amino acid vocabulary
|
||||
│ └── RRCLib/ ← RRC library modules
|
||||
│
|
||||
├── Core/ ← core runtime modules
|
||||
│
|
||||
├── python/ ← Python shims (I/O only)
|
||||
│ ├── chaos_game.py
|
||||
│ ├── sidon_addressing.py
|
||||
│ ├── spectral_profile.py
|
||||
│ └── q16_16_canonical.py
|
||||
│
|
||||
├── qubo/ ← QUBO/QAOA optimization
|
||||
│ ├── finsler_metric.py
|
||||
│ ├── qubo_builder.py
|
||||
│ ├── qaoa_circuit.py
|
||||
│ └── classical_solver.py
|
||||
│
|
||||
├── tests/ ← test suite
|
||||
│ ├── test_q16_roundtrip.py
|
||||
│ ├── test_schema.py
|
||||
│ └── test_bind.py
|
||||
│
|
||||
├── docs/ ← documentation
|
||||
│ ├── architecture.md
|
||||
│ ├── glossary.md
|
||||
│ └── testing.md
|
||||
│
|
||||
├── experiments/ ← experimental code (not production)
|
||||
│
|
||||
├── extraction/ ← generated JSON artifacts
|
||||
│
|
||||
└── .github/workflows/ ← CI/CD
|
||||
├── lean-check.yml
|
||||
├── python-check.yml
|
||||
└── q16-roundtrip.yml
|
||||
```
|
||||
|
||||
## Module Naming (Lean)
|
||||
|
||||
| Type | Pattern | Example |
|
||||
|------|---------|---------|
|
||||
| Schema class | `Schema` | `class Schema (α : Type)` |
|
||||
| Wire format | `WireFormat` | `structure WireFormat` |
|
||||
| Product type | `ProductSchema` | `instance : Schema (α × β)` |
|
||||
| Receipt | `Receipt` | `structure Receipt` |
|
||||
| Bind | `Bind` | `def bindReceipt` |
|
||||
| Theorem | `camelCase` | `byteSize_nonneg` |
|
||||
| Lemma | `camelCase` | `roundTrip_correct` |
|
||||
| Instance | `PascalCase` | `uint8Schema` |
|
||||
|
||||
## Import Conventions
|
||||
|
||||
```lean
|
||||
-- SilverSight modules import from Semantics cross-project
|
||||
import Semantics.FixedPoint
|
||||
import Semantics.Spectrum
|
||||
|
||||
-- Internal SilverSight imports use relative paths
|
||||
import SilverSight.Schema
|
||||
import SilverSight.WireFormat
|
||||
```
|
||||
|
||||
## Build Targets
|
||||
|
||||
```bash
|
||||
# Full SilverSight build
|
||||
lake build SilverSight
|
||||
|
||||
# Narrow target
|
||||
lake build SilverSight.Schema
|
||||
|
||||
# Compiler surface (blessed API)
|
||||
lake build Compiler
|
||||
```
|
||||
|
||||
## File Size Limits
|
||||
|
||||
| File | Max Lines | Notes |
|
||||
|------|-----------|-------|
|
||||
| Lean module | 500 | One namespace per file |
|
||||
| Python shim | 300 | Pure I/O only |
|
||||
| Documentation | No limit | But prefer modular docs |
|
||||
|
||||
## What Goes Where
|
||||
|
||||
| Content | Location | Why |
|
||||
|---------|----------|-----|
|
||||
| Lean formal modules | `formal/SilverSight/` | Core formalization |
|
||||
| Python shims | `python/` | I/O only, no logic |
|
||||
| QUBO/QAOA | `qubo/` | Optimization domain |
|
||||
| Tests | `tests/` | Verification |
|
||||
| Docs | `docs/` | Human-readable |
|
||||
| Experiments | `experiments/` | Not production |
|
||||
| Generated JSON | `extraction/` | Artifacts |
|
||||
Loading…
Add table
Reference in a new issue