Minimize imports via lake shake and add import lint/stats

[joehendrix]

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.

[MikaelMayer]

🤖🔍 Overall this is a solid mechanical import-minimization PR with clear metrics. A few concerns:

1. Internal Std imports: Several files now import Std.Data.DTreeMap.Internal.Operations, Std.Tactic.BVDecide.Normalize.Prop, Std.Tactic.BVDecide.Normalize.BitVec, Std.Tactic.BVDecide.Normalize.Bool, and Std.Do.Triple.SpecLemmas. These look like internal implementation modules that may not be part of Std's stable API. If they get reorganized upstream, this will break. Consider whether these are truly the minimal necessary imports or if there's a more stable public entry point.

2. Emptied aggregator modules: Imperative.lean, SMT.lean, and LExprType.lean are now empty module files with no imports. If they're truly dead, they should be deleted rather than left as empty shells. If they're kept for the -- shake: keep aggregator pattern, they need the annotation.

3. MetaVerifier.lean workaround: The comment "For some reason shake wants to meta import the following while lake itself only requires imports" suggests shake may be producing incorrect suggestions here. The pattern of duplicating imports as both meta import and import -- shake: keep is unusual and warrants investigation.

4. Deletion candidates list: The 23 -- noimport: modules in Strata.lean is a significant number of orphaned modules. Is there a plan to either delete them or re-integrate them?

[MikaelMayer]

🤖🔍 All previous comments appear addressed — reviewer sign-off still needed.

• Internal Std imports (Std.Data.DTreeMap.Internal.Operations, Std.Do.Triple.SpecLemmas, Std.Tactic.BVDecide.Normalize.Prop) replaced with stable public entry points (Std.Data.DTreeMap, Std.Do, Std.Tactic.BVDecide)
• Empty aggregator shells deleted and replaced with proper -- shake: keep-all aggregator modules at the parent level
• Orphaned -- noimport: modules now properly imported in Strata.lean
• MetaVerifier pattern acknowledged as a shake bug to file (acceptable)
• public section in Boole/Grammar.lean confirmed intentional by author

[MikaelMayer]

🤖🔍 All previous comments appear addressed — reviewer sign-off still needed.

New commit 046c7bf adds Strata.Languages.Laurel.Grammar import and fixes ReflectTests.lean imports — both look correct.

Minor note: Std.Tactic.BVDecide.Normalize.Prop remains in MetaVerifier.lean (an internal module), but given the acknowledged shake bugs in that file, this is acceptable for now.

[MikaelMayer]

🤖🔍 All previous inline comments appear addressed:

• Internal Std imports in LTy.lean and Tactics.lean replaced with stable entry points ✅
• Empty aggregator modules (Imperative, SMT, LExprType) properly fixed or deleted ✅
• Orphaned modules now properly imported in Strata.lean ✅
• MetaVerifier shake bug acknowledged ✅
• public section in Boole/Grammar confirmed intentional ✅

One new concern: DDMAxiomsExtraction.lean had a #guard_msgs in #eval examplePgm.commands test removed (commit f381871). This test exists and passes on main. Was this removal intentional, or did the import change break the .commands output? If the output changed due to import minimization, the expected output should be updated rather than the test deleted.

Also minor: Std.Tactic.BVDecide.Normalize.BitVec remains in Verifier.lean (an internal module), while the same pattern was fixed to Std.Tactic.BVDecide in LTy.lean. Not blocking but worth noting for consistency.

Reviewer sign-off still needed.

[shigoel]

LGTM!