Refactor: split `CompilationModel.lean` (5,404 lines) into separate modules

[Th0rgal]

Why

CompilationModel.lean is the single largest file in the codebase at 5,404 lines. It contains:

• Type definitions (Expr, Stmt, CompilationModel, etc.)
• The entire compiler logic (compileExpr, compileStmt, compile)
• Validation walkers
• ABI encoding
• 201 error messages

This is the #1 obstacle for:

• LLM comprehension: models struggle with 5k+ line files and lose context
• Build times: changes to any part of the file trigger full recompilation of everything downstream
• Code review: PRs touching this file are hard to review

Solution

Split into separate modules:

Compiler/
  CompilationModel/
    Types.lean          -- Expr, Stmt, CompilationModel, Field, StorageSlot, etc.
    ExprCompiler.lean   -- compileExpr and expression-level compilation
    StmtCompiler.lean   -- compileStmt and statement-level compilation
    Compile.lean        -- top-level compile function, contract assembly
    Validation.lean     -- validation walkers, field checks
    AbiEncoding.lean    -- ABI JSON generation, selector computation
    Errors.lean         -- error message constants and formatting (optional)
  CompilationModel.lean -- re-exports all submodules for backwards compatibility

Effort

1 week

Acceptance

• All content from the monolith distributed across well-named submodules
• A single CompilationModel.lean re-export file for backwards compatibility
• No regressions in build or proofs
• Incremental build time improvement measurable on the compiler target

[Th0rgal]

Merged incremental refactor step in #1212 (March 5, 2026): extracted , , and into as a low-risk split toward the full decomposition.

[Th0rgal]

Correction to previous comment (formatting glitch):

Merged incremental refactor step in #1212 (March 5, 2026): extracted internalFunctionPrefix, internalFunctionYulName, and pickFreshName into Compiler/CompilationModel/InternalNaming.lean as a low-risk split toward the full CompilationModel.lean decomposition.

[Th0rgal]

Landed an incremental split in PR #1212 (merged): extracted internal naming helpers from into as a low-risk first step toward broader modularization.

[Th0rgal]

Landed an incremental split in PR #1212 (merged): extracted internal naming helpers from Compiler/CompilationModel.lean into Compiler/CompilationModel/InternalNaming.lean as a low-risk first step toward broader modularization.

[Th0rgal]

Landed another incremental split in #1215 (merged, March 5, 2026): extracted dynamic-data helpers from into new module as a low-risk step toward full decomposition.

[Th0rgal]

Correction to previous comment (formatting glitch):

Merged incremental refactor step in #1215 (March 5, 2026): extracted dynamic-data helpers from Compiler/CompilationModel.lean into Compiler/CompilationModel/DynamicData.lean.

Also merged #1214 (March 5, 2026), which splits declaration-heavy DSL/type definitions into Compiler/CompilationModel/Types.lean.

[Th0rgal]

Merged incremental split step: #1216.

This extracts packed-bit validation/masking helpers and name-collection traversals from CompilationModel.lean into Compiler/CompilationModel/ValidationHelpers.lean, reducing top-level file complexity while preserving behavior.

[Th0rgal]

Merged incremental split in #1217: extracted bind-name + array-element usage analysis helpers into Compiler/CompilationModel/UsageAnalysis.lean and reduced CompilationModel.lean accordingly.

Local validation run:

• lake build Compiler.CompilationModel.UsageAnalysis Compiler.CompilationModel
• lake build Compiler.Selector Compiler.ABI Compiler.MacroTranslateInvariantTest