Convert Strata/DL/ files to Lean modules

[joehendrix]

Summary

Convert 65 of 66 files under Strata/DL/ (plus 10 supporting files outside
DL) to Lean modules. This is the first step toward making Strata.SimpleAPI
fully modular.

Details

• Visibility. Each converted file wraps its declarations in
  public section/end so importers see them. Imports that appear in
  public signatures become public import; internal-only imports stay
  private.
• Namespace extensions kept private. Definitions that extend Lean or
  library namespaces (e.g. BitVec.width, List.dedup) stay private by
  default so Strata does not conflict with Batteries or Mathlib.
  Consumers that need these use import all to opt in explicitly.
• Type aliases need @[expose]. Lean's module system requires
  @[expose] on abbrev definitions whose underlying type must be
  visible to importers (e.g. abbrev Map α β := List (α × β)).
  Without it, compilation fails with a "type differs" error.
• Match-pattern defs need @[expose, match_pattern]. Definitions
  used in pattern matching (e.g. LMonoTy.bool, LExpr.boolConst)
  must be both exposed and marked as match patterns.
• Proof unfolding across module boundaries. When a proof in module A
  needs to simp/unfold a private definition from module B, we add
  import all B alongside the regular import. This is used for
  Counter, StringGen, Init.Data.Repr, and several Lambda modules.
• Meta imports. Files with elab or macro definitions use
  public meta import for Lean metaprogramming libraries. Meta helper
  functions called by elab macros cannot be private because
  downstream non-module files would not see them.
• GOTO backend files converted. Imperative/ToCProverGOTO imports
  GOTO backend types, so 6 files under Backends/CBMC/GOTO/ were also
  converted. Target changed from a def with manual instances to
  @[expose] abbrev Target := Nat, which removes boilerplate and makes
  the type transparent. InstToJson drops the now-unnecessary
  .toNat call.
• TestGen excluded. Lambda/TestGen.lean depends on Plausible
  (not yet a module) and is left unconverted. Only test files import it.
• No behavioral changes. All existing tests pass.

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

[shigoel]

Thank you!

[keyboardDrummer]

Sweet!

[keyboardDrummer]

How practical is the use of public section ... end ? From a declaration signature you can't easily see whether it's located in a public section or not. It seems more explicit to me to specify on a per declaration basis whether it needs to be public or not.