allaun/Research-Stack
1
0
Fork 0
mirror of https://github.com/allaunthefox/Research-Stack.git synced 2026-07-31 03:05:21 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions
Research-Stack/0-Core-Formalism/lean/SilverSight/AGENTS.md
allaun a7c7e3a51c docs: fix SilverSight local clone path 
Local clone is at /home/allaun/SilverSight, not /tmp/SilverSight.
2026-06-22 22:18:19 -05:00

2.1 KiB
Raw Permalink Blame History

AGENTS.md — SilverSight

SilverSight is the clean-slate rebase of the Research Stack.

Repository

GitHub: https://github.com/allaunthefox/SilverSight Local clone: /home/allaun/SilverSight Formal modules: formal/SilverSight/

Location (in Research Stack — for lake build integration)

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 to the SilverSight repository.

  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