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
-- 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
# 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 |
allaun
5e0f8b72f1