import Lake
open Lake DSL
open System

package «SilverSight» where
  leanOptions := #[
    ⟨`pp.unicode.fun, true⟩
  ]

-- ─── Layer 0: Core Foundation ────────────────────────────────────────────────
@[default_target]
lean_lib «SilverSightCore» where
  srcDir := "Core"
  roots := #[`SilverSightCore, `SilverSight.FixedPoint, `SilverSight.Semantics.Schema, `SilverSight.Semantics.Layout, `SilverSight.Semantics.WireFormat, `SilverSight.Semantics.View, `SilverSight.Semantics.LayoutBridge, `SilverSight.Semantics.CanalLayout]

-- ─── Layer 1: Numerics & Fixed-Point ─────────────────────────────────────────
lean_lib «SilverSightNumerics» where
  srcDir := "formal"
  roots := #[
    `CoreFormalism.FixedPoint,
    `CoreFormalism.Tactics,
    `CoreFormalism.Q16_16Numerics,
    `SilverSight.PrimeLut,
    `SilverSight.FixedPointBridge
  ]

-- ─── Layer 2: Canal / Dynamic Infrastructure ─────────────────────────────────
lean_lib «SilverSightCanal» where
  srcDir := "formal"
  roots := #[
    `CoreFormalism.DynamicCanal,
    `CoreFormalism.Bind
  ]

-- ─── Layer 3a: Braid Theory ──────────────────────────────────────────────────
lean_lib «SilverSightBraid» where
  srcDir := "formal"
  roots := #[
    `CoreFormalism.BraidBracket,
    `CoreFormalism.BraidStrand,
    `CoreFormalism.BraidCross,
    `CoreFormalism.BraidField,
    `CoreFormalism.BraidStateN,
    `CoreFormalism.BraidEigensolid,
    `CoreFormalism.BraidSpherionBridge,
    `CoreFormalism.ContractedCrossStep
  ]

-- ─── Layer 3b: Sidon / Number Theory ─────────────────────────────────────────
lean_lib «SilverSightSidon» where
  srcDir := "formal"
  roots := #[
    `CoreFormalism.SidonSets,
    `CoreFormalism.SieveLemmas,
    `CoreFormalism.InteractionGraphSidon,
    `CoreFormalism.CRTSidon,
    `CoreFormalism.CRTSidonN,
    `CoreFormalism.E8Sidon,
    `CoreFormalism.EisensteinSeries,
    `CoreFormalism.GoormaghtighEnumeration,
    `CoreFormalism.StrandCapacityBound
  ]

-- ─── Layer 3c: Hachimoji DNA Encoding ────────────────────────────────────────
lean_lib «SilverSightHachimoji» where
  srcDir := "formal"
  roots := #[
    `CoreFormalism.HachimojiBase,
    `CoreFormalism.HachimojiCodec,
    `CoreFormalism.HachimojiLUT,
    `CoreFormalism.HachimojiBridging,
    `CoreFormalism.HachimojiManifoldAxiom,
    `SilverSight.HachimojiN8,
    `SilverSight.HachimojiN8Bridge,
    `SilverSight.HachimojiCharClass,
    `SilverSight.PhiDNALayout,
    `SilverSight.PhiConsistency,
    `SilverSight.PhiPipelineReceipt
  ]

-- ─── Layer 4: PIST / Spectral Classification ─────────────────────────────────
lean_lib «SilverSightPIST» where
  srcDir := "formal"
  roots := #[
    `SilverSight.PIST.Spectral,
    `SilverSight.PIST.SpectralN,
    `SilverSight.PIST.MatrixN,
    `SilverSight.PIST.CharPoly,
    `SilverSight.PIST.FisherRigidity,
    `SilverSight.PIST.FisherRigidityN,
    `SilverSight.PIST.Classify,
    `SilverSight.PIST.ClassifyN,
    `SilverSight.PIST.Matrices250,
    `SilverSight.PIST.UnifiedCovariant,
    `SilverSight.PIST.CartanConnection,
    `SilverSight.PIST.YangBaxter,
    `SilverSight.PIST.SidonMirrorNotch,
    `SilverSight.PIST.Tdoku16D,
    `SilverSight.PIST.CrossDomainSynthesis,
    `SilverSight.PIST.MultiSurfacePacker,
    `SilverSight.PIST.ManifoldShortcut,
    `SilverSight.PIST.SidonAdapter,
    `SilverSight.PIST.WeightCandidateGen,
    `SilverSight.PIST.UnitDistCandidateGen,
    `SilverSight.PIST.CMYKColoringCore
  ]

-- ─── Layer 5: AVM Instruction Set Architecture ───────────────────────────────
lean_lib «SilverSightAVM» where
  srcDir := "formal"
  roots := #[
    `SilverSight.AVMIsa.Types,
    `SilverSight.AVMIsa.Value,
    `SilverSight.AVMIsa.Instr,
    `SilverSight.AVMIsa.State,
    `SilverSight.AVMIsa.Step,
    `SilverSight.AVMIsa.TypeCheck,
    `SilverSight.AVMIsa.TypeSafety,
    `SilverSight.AVMIsa.Run,
    `SilverSight.AVMIsa.Emit
  ]

-- ─── Layer 6: RRC Receipt Pipeline ───────────────────────────────────────────
lean_lib «SilverSightRRC» where
  srcDir := "formal"
  roots := #[
    `SilverSight.RRCLogogramProjection,
    `SilverSight.ReceiptCore,
    `SilverSight.RRC.Emit,
    `SilverSight.RRC.ReceiptDensity,
    `SilverSight.RRC.PolyFactorIdentity,
    `SilverSight.RRC.EntropyCandidates,
    `SilverSight.RRC.Q16_16Manifold,
    `RRCLib.RRCEmit
  ]

-- ─── Layer 7: Binding Site Codec ─────────────────────────────────────────────
lean_lib «SilverSightBindingSite» where
  srcDir := "formal"
  roots := #[
    `BindingSite.BindingSiteTypes,
    `BindingSite.BindingSiteHachimoji,
    `BindingSite.BindingSiteEntropy,
    `BindingSite.BindingSiteCodec
  ]

-- ─── Layer 8: Optimisation / Feasible Set ────────────────────────────────────
lean_lib «SilverSightFeasible» where
  srcDir := "formal"
  roots := #[
    `SilverSight.FeasibleSet.Theorem,
    `SilverSight.FeasibleSet.QUBORelaxation
  ]

-- ─── Standalone / Miscellaneous ──────────────────────────────────────────────
lean_lib «SilverSightMisc» where
  srcDir := "formal"
  roots := #[
    `SilverSight.AngrySphinx,
    `SilverSight.BlockCoprimeDensity,
    `SilverSight.CollatzBraid,
    `SilverSight.GoldenSpiral,
    `SilverSight.GCCL,
    `SilverSight.WireFormat,
    `SilverSight.ProductSchema,
    `SilverSight.ProductWireFormat,
    `SilverSight.Receipt,
    `SilverSight.AdjugateMatrix,
    `SilverSight.ChiralClockModel,
    `SilverSight.ColdReviewer,
    `SilverSight.HCMR,
    `SilverSight.CacheSieve,
    `SilverSight.Blitter6502OISC,
    `SilverSight.YangMillsPerformance,
    `SilverSight.WorkloadTestbench,
    `SilverSight.Rollup,
    `SilverSight.CollectiveIntelligence.CostTransparency
  ]

-- ─── Geometry (standalone) ───────────────────────────────────────────────────
lean_lib «SilverSightGeometry» where
  srcDir := "formal"
  roots := #[
    `CoreFormalism.ComplexProjectiveSpace,
    `CoreFormalism.ChentsovFinite,
    `CoreFormalism.HopfFibration,
    `CoreFormalism.AutoProof
  ]

/-! Dead code archived 2026-07-03. See archive/dead_code_2026-07-03/README.md
    - CoreFormalism/CharacterTransform.lean
    - PVGS_DQ_Bridge/ (8 .lean + 1 .py)
    - UniversalEncoding/ (2 .lean)
    - SilverSight/PIST/SpectralWitness.lean
    - SilverSight/Bind.lean
    - SilverSight/FeasibleSet/TestChain.lean
-/

-- ─── Executables ─────────────────────────────────────────────────────────────

lean_exe «rrc-emit-fixture» where
  root := `RrcEmitFixture
  srcDir := "exe"

lean_exe «q16-roundtrip» where
  root := `Q16_16Roundtrip
  srcDir := "exe"

-- Static C library for the Q16_16 roundtrip executable.
def cSrcDir : FilePath := FilePath.mk "c"

target q16_canonical.o pkg : FilePath := do
  let oFile := pkg.buildDir / cSrcDir / "q16_canonical.o"
  let srcJob ← inputFile (pkg.srcDir / cSrcDir / "q16_canonical.c") true
  let flags := #["-fPIC", "-O2"]
  buildO oFile srcJob flags

extern_lib q16_canonical pkg := do
  let name := nameToStaticLib "q16_canonical"
  let libFile := pkg.buildDir / cSrcDir / name
  let oJob ← fetch <| pkg.target ``q16_canonical.o
  buildStaticLib libFile #[oJob]

require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git" @ "v4.30.0-rc2"