Minimize imports via lake shake and add import lint/stats (#1020)

## Summary

Run `lake shake` to minimize the import graph across all 293 Strata
modules,
reducing average transitive Strata imports by 32% (56 → 38) and total
transitive
imports (including Lean/Std) by 40% (1379 → 831). Add CI linting to
ensure
`Strata.lean` transitively imports every module, and add an import
statistics
script for ongoing measurement.

## Changes

- **Import lint driver (`Scripts/CheckImports.lean`)**: Verifies that
all `.lean`
files under `Strata/` are transitively imported by `Strata.lean`.
Registered as
`lintDriver` in `lakefile.toml` so `lake lint` runs it automatically.
Supports
`-- noimport: Strata.Foo` comments in `Strata.lean` to allowlist
intentionally
  excluded modules.

- **Import statistics script (`Scripts/ImportStats.lean`)**: Computes
per-module
transitive import counts (both total and Strata-only), reporting
average,
median, min, max, top/bottom lists, and histograms. Run via `lake exe
ImportStats`.

- **`lake shake Strata --fix`**: Applied shake's suggestions to remove
unnecessary
imports across 225 files (net -185 lines). This is the bulk of the
change.

- **Aggregator modules use `-- shake: keep`**: Pure aggregator modules
  (`CBMC.lean`, `GOTO.lean`, `B3.lean`, `Dyn.lean`, `Python.lean`,
  `Imperative.lean`, `Lambda.lean`, `DDM.lean`, `LExprType.lean`,
`B3/Verifier.lean`) intentionally re-export their submodules and are
annotated
  with `-- shake: keep` so `lake shake --fix` won't strip them.

- **DDM elaboration imports use `-- shake: keep`**: Files using
`#dialect`,
`#strata`, `#strata_gen`, and related macros have elaboration-time
import
  dependencies that shake cannot detect. These are annotated with
  `-- shake: keep` to prevent breakage.

- **Renamed aggregator files**: `Dyn/Dyn.lean` → `Dyn.lean`,
  `Python/Python.lean` → `Python.lean`, `Imperative/Imperative.lean` →
`Imperative.lean` — the `Foo/Foo.lean` pattern is unnecessary now that
these
  are proper `module` files.

- **Orphaned modules added to `Strata.lean`**: When shake stripped
re-exports
from real code files (e.g. `ProgramWF.lean` no longer re-exports
`StatementWF`),
the orphaned modules were added directly to `Strata.lean` to maintain
full
  coverage.

## Results

| Metric | Before | After | Change |
|---|---|---|---|
| Avg transitive imports (Strata-only) | 56.2 | 38.2 | -32% |
| Median transitive imports (Strata-only) | 38 | 22 | -42% |
| Avg transitive imports (all) | 1379 | 831 | -40% |
| Total import edges (Strata-only) | 16,455 | 11,194 | -32% |
| Clean build time | 3m 02s | 2m 58s | -2% |

By submitting this pull request, I confirm that you can use, modify,
copy, and
redistribute this contribution, under the terms of your choice.

Author: joehendrix

Strata.lean

@@ -12,9 +12,9 @@ import Strata.DDM.Integration.Lean
 import Strata.DDM.Ion
 
 /- Dialect Library -/
-import Strata.DL.SMT.SMT
+import Strata.DL.SMT
 import Strata.DL.Lambda.Lambda
-import Strata.DL.Imperative.Imperative
+import Strata.DL.Imperative
 
 /- Utilities -/
 import Strata.Util.NameProofs
@@ -25,6 +25,8 @@ import Strata.Languages.Core.FactoryWF
 import Strata.Languages.Core.SeqModel
 import Strata.Languages.Core.StatementSemantics
 import Strata.Languages.Core.SarifOutput
+
+import Strata.Languages.Laurel.Grammar
 import Strata.Languages.Laurel.LaurelCompilationPipeline
 
 /- Code Transforms -/
@@ -71,4 +73,28 @@ import Strata.SimpleAPI
 /- Pipeline -/
 import Strata.Pipeline.PyAnalyzeLaurel
 
--- noimport: Strata.Util.Random -- deletion candidate: nothing imports this module
+ -- deletion candidates: nothing imports these modules:
+
+-- noimport:
+import Strata.DL.Imperative.CFGSemantics
+import Strata.DL.Imperative.SemanticsProps
+import Strata.DL.Lambda.Denote.Assumptions
+import Strata.DL.Lambda.Denote.CallOfLFuncDenote
+import Strata.DL.Lambda.Denote.LExprDenote
+import Strata.DL.Lambda.Denote.LExprDenoteConstrs
+import Strata.DL.Lambda.Denote.LExprDenoteEq
+import Strata.DL.Lambda.Denote.LExprDenoteProps
+import Strata.DL.Lambda.Denote.LExprDenoteSubst
+import Strata.DL.Lambda.Denote.LExprDenoteTySubst
+import Strata.DL.Lambda.Denote.LExprSemanticsConsistent
+import Strata.DL.Lambda.LExprTypeSpec
+import Strata.DL.Lambda.MetaData
+import Strata.DL.Lambda.Reflect
+import Strata.DL.Lambda.Semantics
+import Strata.DL.Lambda.TypeFactoryWF
+import Strata.DL.Util.HList
+import Strata.Languages.Core.ProgramWF
+import Strata.Languages.Core.StatementWF
+import Strata.Languages.Dyn.DDMTransform.Parse
+import Strata.Languages.Dyn.DDMTransform.Translate
+import Strata.Util.Random

Strata/Backends/CBMC/CProver.lean

@@ -7,5 +7,3 @@ module
 
 -------------------------------------------------------------------------------
 
-public import Strata.Backends.CBMC.GOTO.Program
-public import Strata.Backends.CBMC.GOTO.InstToJson

Strata/Backends/CBMC/CollectSymbols.lean

@@ -6,10 +6,8 @@
 module
 
 public import Strata.Backends.CBMC.GOTO.InstToJson
-public import Strata.Backends.CBMC.GOTO.LambdaToCProverGOTO
-import Strata.DL.Lambda.TypeConstructor
-import Strata.DL.Lambda.TypeFactory
 public import Strata.Languages.Core.Program
+import Strata.Backends.CBMC.GOTO.LambdaToCProverGOTO
 
 namespace Strata
 

Strata/Backends/CBMC/Common.lean

@@ -5,8 +5,8 @@
 -/
 module
 
-public import Lean.Data.Json
 public import Strata.DL.Util.Map
+public import Lean.Data.Json.FromToJson.Basic
 
 public section
 

Strata/Backends/CBMC/CoreToCBMC.lean

@@ -8,15 +8,9 @@ module
 public import Strata.Backends.CBMC.Common
 public import Strata.Languages.Core.Procedure
 
-import Lean.Data.Json
-import Lean.Parser.Types
-import Strata.DDM.Integration.Lean.HashCommands
-import Strata.Languages.Core.Env
-import Strata.Languages.Core.DDMTransform.Grammar
+public import Strata.DDM.AST
+import Strata.DDM.Integration.Lean.HashCommands -- shake: keep
 import Strata.Languages.Core.DDMTransform.Translate
-import Strata.DL.Util.Map
-import Strata.Languages.Core.Core
-import Strata.Util.Tactics
 
 public section
 

Strata/Backends/CBMC/GOTO/Code.lean

@@ -6,7 +6,6 @@
 module
 
 public import Strata.Backends.CBMC.GOTO.Expr
-public import Strata.Backends.CBMC.GOTO.SourceLocation
 import Strata.Util.Tactics
 
 namespace CProverGOTO

Strata/Backends/CBMC/GOTO/CoreToCProverGOTO.lean

@@ -5,12 +5,14 @@
 -/
 module
 
-public import Strata.Backends.CBMC.GOTO.InstToJson
-public import Strata.Backends.CBMC.GOTO.DefaultSymbols
 public import Strata.Backends.CBMC.GOTO.LambdaToCProverGOTO
 public import Strata.DL.Imperative.ToCProverGOTO
-public import Strata.Languages.Core.Verifier
-import Lean.Parser.Types
+public import Strata.Backends.CBMC.GOTO.Program
+public import Strata.Languages.Core.Program
+import Strata.Backends.CBMC.GOTO.DefaultSymbols
+import Strata.Languages.Core.DDMTransform.Translate
+import Strata.Languages.Core.ProgramType
+import Strata.Util.Json
 
 public section
 

Strata/Backends/CBMC/GOTO/CoreToGOTOPipeline.lean

@@ -5,9 +5,13 @@
 -/
 module
 
-public import Strata.Backends.CBMC.CollectSymbols
 public import Strata.Backends.CBMC.GOTO.CoreToCProverGOTO
 import Strata.Transform.ProcedureInlining
+public import Strata.Languages.Core.Factory
+import Strata.Backends.CBMC.CollectSymbols
+import Strata.Backends.CBMC.GOTO.DefaultSymbols
+import Strata.Languages.Core.ProgramType
+import Strata.Util.Json
 
 /-! ## Core-to-GOTO translation pipeline
 

Strata/Backends/CBMC/GOTO/Expr.lean

@@ -6,7 +6,6 @@
 module
 
 public import Strata.Backends.CBMC.GOTO.Type
-public import Strata.Backends.CBMC.GOTO.SourceLocation
 import Strata.Util.Tactics
 
 namespace CProverGOTO

Strata/Backends/CBMC/GOTO/InstToJson.lean

@@ -5,11 +5,12 @@
 -/
 module
 
-public import Strata.Backends.CBMC.Common
-public import Strata.Util.Json
 public import Strata.Backends.CBMC.GOTO.Program
 
 import Strata.Util.Tactics
+public import Strata.DL.Util.Map
+import Strata.Backends.CBMC.Common
+import Strata.Util.Json
 
 public section