mirror of
https://github.com/allaunthefox/SilverSight.git
synced 2026-07-31 01:25:21 +00:00
allaun
3504bca392
Implements the YaFF-inspired separation of schema, layout, and access pattern
in Core/SilverSight/Semantics/:
- Schema.lean: fixed-size Schema typeclass with byteSize and wellFormed.
- Layout.lean: Layout enum, AccessProfile cost model, and cost-based selector
with an ε-suboptimality theorem.
- WireFormat.lean: certified encode/decode/roundTrip/encode_size structure.
- View.lean: zero-copy View with address-arithmetic invariant.
- LayoutBridge.lean: certified layout-conversion structure and identity bridges.
- CanalLayout.lean: CanalRegime enum and regime-aware layout selection.
Also updates:
- lakefile.lean: adds SilverSight.Semantics.* roots to SilverSightCore.
- docs/ARCHITECTURE.md, RRC_REFACTOR_READINESS.md, PROJECT_MAP.{md,json},
build_logs/2026-06-21_session_build_baseline.md, and GLOSSARY.md.
- AGENTS.md: build baseline, blessed surfaces, and pending proof work.
Build: 2987 jobs, 0 errors (lake build)
Tests: Python 21/21, Lean/C 35/35
83 lines
2.6 KiB
Text
83 lines
2.6 KiB
Text
import Lake
|
|
open Lake DSL
|
|
open System
|
|
|
|
package «SilverSight» where
|
|
-- Settings applied to both builds and interactive editing
|
|
leanOptions := #[
|
|
⟨`pp.unicode.fun, true⟩ -- pretty-prints `fun a ↦ b`
|
|
]
|
|
-- Add any additional package configuration options here
|
|
|
|
@[default_target]
|
|
lean_lib «SilverSightCore» where
|
|
-- Add any library configuration options here
|
|
srcDir := "Core"
|
|
roots := #[`SilverSightCore, `SilverSight.FixedPoint, `SilverSight.Semantics.Schema, `SilverSight.Semantics.Layout, `SilverSight.Semantics.WireFormat, `SilverSight.Semantics.View, `SilverSight.Semantics.LayoutBridge, `SilverSight.Semantics.CanalLayout]
|
|
|
|
lean_lib «SilverSightFormal» where
|
|
srcDir := "formal"
|
|
roots := #[
|
|
`CoreFormalism.FixedPoint,
|
|
`CoreFormalism.Tactics,
|
|
`CoreFormalism.Q16_16Numerics,
|
|
`CoreFormalism.DynamicCanal,
|
|
`CoreFormalism.Bind,
|
|
`CoreFormalism.BraidBracket,
|
|
`CoreFormalism.BraidStrand,
|
|
`CoreFormalism.BraidCross,
|
|
`CoreFormalism.BraidField,
|
|
`CoreFormalism.SidonSets,
|
|
`CoreFormalism.SieveLemmas,
|
|
`CoreFormalism.InteractionGraphSidon,
|
|
`CoreFormalism.BraidEigensolid,
|
|
`CoreFormalism.BraidSpherionBridge
|
|
]
|
|
|
|
lean_lib «SilverSightRRC» where
|
|
srcDir := "formal"
|
|
roots := #[
|
|
`SilverSight.PIST.Spectral,
|
|
`SilverSight.PIST.Classify,
|
|
`SilverSight.PIST.Matrices250,
|
|
`SilverSight.RRCLogogramProjection,
|
|
`SilverSight.ReceiptCore,
|
|
`SilverSight.RRC.Emit,
|
|
`SilverSight.RRC.ReceiptDensity,
|
|
`SilverSight.RRC.PolyFactorIdentity,
|
|
`SilverSight.RRC.EntropyCandidates,
|
|
`SilverSight.RRC.Corpus250,
|
|
`SilverSight.AVMIsa.Types,
|
|
`SilverSight.AVMIsa.Value,
|
|
`SilverSight.AVMIsa.Instr,
|
|
`SilverSight.AVMIsa.State,
|
|
`SilverSight.AVMIsa.Step,
|
|
`SilverSight.AVMIsa.Run,
|
|
`SilverSight.AVMIsa.Emit
|
|
]
|
|
|
|
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"
|