mirror of
https://github.com/allaunthefox/Research-Stack.git
synced 2026-07-31 03:05:21 +00:00
allaun
106ef0f271
Phase 1 core (7 new Lean files, 3307 jobs, 0 errors): - Schema.lean: Schema class with 6 type instances - WireFormat.lean: WireFormat structure + Layout enum - ProductSchema.lean: Schema (α × β) instance - ProductWireFormat.lean: Row-major pair encoders with roundTrip proofs - Receipt.lean: Receipt structure + GateType enum - Bind.lean: bindReceipt composition + 8 theorems - SilverSight.lean: root import module Claim promotions (3 claims → VERIFIED): - silversight_claim_q16_unified: FixedPoint.lean 12 theorems, 0 sorry - silversight_claim_eigensolid_convergence: BraidEigensolid.lean:175 - silversight_claim_receipt_invertible: BraidEigensolid.lean:249 Theorem triage (3,057 theorems classified): - TIER_1_CORE: 118 theorems (6 modules, direct port) - TIER_2_FOUNDATION: 1,591 theorems (121 modules) - TIER_3_EXTENSION: 1,084 theorems (291 modules) - TIER_4_QUARANTINE: 137 theorems (15 modules) - TIER_5_EXCLUDED: 127 theorems (18 modules) Build: SilverSight 3307 jobs, 0 errors, 0 sorries
116 lines
3.3 KiB
TOML
116 lines
3.3 KiB
TOML
name = "Semantics"
|
|
version = "0.1.0"
|
|
srcDir = "."
|
|
# Compiler is the narrow fast-verification target for CI: only the blessed
|
|
# RRC + AVMIsa + ReceiptCore surface. Semantics is the full workspace build.
|
|
defaultTargets = ["Compiler", "Semantics"]
|
|
|
|
[[require]]
|
|
name = "sparkle"
|
|
git = "https://github.com/Verilean/sparkle.git"
|
|
rev = "252341078dba3c2612719746e6a459dada2248ea"
|
|
|
|
[[require]]
|
|
name = "mathlib"
|
|
git = "https://github.com/leanprover-community/mathlib4"
|
|
rev = "v4.30.0-rc2"
|
|
|
|
[[lean_lib]]
|
|
name = "Semantics"
|
|
|
|
# ── Compiler: blessed RRC compiler surface ────────────────────────────────────
|
|
# Fast CI target. Only these modules form the "functional Rainbow Raccoon
|
|
# Compiler" proof-of-life:
|
|
# Semantics.RRC.Emit — fixture corpus → alignment gate → JSON (Goal A+)
|
|
# Semantics.AVMIsa.Emit — AVM canaries → RRC → JSON (Goal A); sole output boundary
|
|
# also stamps Semantics.RRC.Corpus250 (250-equation corpus)
|
|
# Semantics.RRC.Corpus250 — raw 250-equation features (Python-supplied, Lean-gated)
|
|
# Libraries (imported by roots, not roots themselves):
|
|
# Semantics.AVMIsa.* — ISA, types, step, run
|
|
# Semantics.ReceiptCore — receipt ledger, promotion gates
|
|
# Semantics.RRCLogogramProjection — projection/merge/lane theorems
|
|
# Semantics.FixedPoint — Q16_16, Q0_16 (no Float in compute paths)
|
|
[[lean_lib]]
|
|
name = "Compiler"
|
|
roots = ["Semantics.RRC.Emit", "Semantics.AVMIsa.Emit", "Semantics.RRC.Corpus250"]
|
|
|
|
[[lean_lib]]
|
|
name = "PIST"
|
|
srcDir = "../../../2-Search-Space/PIST"
|
|
# HybridTSMPISTTorus removed from roots: pre-existing sorry/#eval failures,
|
|
# no module imports it, quarantined pending Lean 4.30 port.
|
|
roots = ["PIST", "PistBridge", "PistSimulation", "TorsionalPIST", "Trace"]
|
|
|
|
[[lean_lib]]
|
|
name = "FAMM"
|
|
srcDir = "../../../2-Search-Space/FAMM"
|
|
roots = ["FAMM"]
|
|
|
|
[[lean_lib]]
|
|
name = "ExtensionScaffold"
|
|
|
|
[[lean_lib]]
|
|
name = "Biology"
|
|
|
|
# ── SilverSight: schema/layout/wireformat core ──────────────────────────────
|
|
# Phase 1 core: product-type encoders, Receipt/Bind composition primitive.
|
|
[[lean_lib]]
|
|
name = "SilverSight"
|
|
roots = ["Semantics.SilverSight"]
|
|
|
|
# OTOM external proofs — uncomment when resolving sorries.
|
|
# Build: lake build OTOMProofs
|
|
# Buildable: DiffusionSNRBias, Constitution
|
|
# Others have structural errors beyond sorries.
|
|
# [[lean_lib]]
|
|
# name = "OTOMProofs"
|
|
# srcDir = "../external/OTOM"
|
|
# roots = ["DiffusionSNRBias", "Constitution"]
|
|
|
|
[[lean_exe]]
|
|
name = "bindserver"
|
|
root = "BindServer"
|
|
|
|
[[lean_exe]]
|
|
name = "searchserver"
|
|
root = "SearchServer"
|
|
|
|
[[lean_exe]]
|
|
name = "SemanticsCli"
|
|
root = "Main"
|
|
|
|
[[lean_exe]]
|
|
name = "openworm_benchmark"
|
|
root = "OpenWormBenchmark"
|
|
|
|
[[lean_exe]]
|
|
name = "ExtremeParameterTestEval"
|
|
root = "ExtremeParameterTestEval"
|
|
|
|
[[lean_exe]]
|
|
name = "NominalParameterTestEval"
|
|
root = "NominalParameterTestEval"
|
|
|
|
[[lean_exe]]
|
|
name = "moim_benchmark"
|
|
root = "MOIMBenchmarkMain"
|
|
|
|
[[lean_exe]]
|
|
name = "generate_sparkle_phi_s3c"
|
|
root = "GenerateSparklePhiS3C"
|
|
|
|
[[lean_exe]]
|
|
name = "tangnano9k_emitter"
|
|
root = "TangNano9KEmitter"
|
|
|
|
[[lean_exe]]
|
|
name = "sabotage_prevention_cli"
|
|
root = "SabotagePreventionCli"
|
|
|
|
[[lean_exe]]
|
|
name = "rrc-watchdog"
|
|
root = "RrcWatchdog"
|
|
|
|
[[lean_exe]]
|
|
name = "pist-classify-trace"
|
|
root = "PistClassifyTrace"
|