Migrate StrataTest files to be Lean modules

[joehendrix]

Migrate 241 of 282 non-Boole StrataTest files to be Lean modules, completing the module migration started in #982.

• Added module keyword to 241 test files. The Boole test files are excluded because gen_smt_vcs produces proof terms that fail kernel type-checking when the file is a module.

• Added meta import for Strata/StrataTest dependencies where #eval, #guard_msgs, or #guard need native implementations from the imported module.

• Added meta import all where proofs use simp, rfl, or native_decide on definitions whose bodies must be visible across the module boundary.

• Added import all where non-meta definitions (types, instances) need access to definition bodies from other StrataTest modules.

• Added meta section wrappers around test code that exercises native implementations, since #eval/#guard_msgs/#guard require meta context to call into compiled code from another module.

• Added import Strata.DDM.Integration.Lean.HashCommands (non-meta) in files using #strata/#dialect syntax, since the syntax extension must be available at parse time regardless of meta context.

• Updated byte offsets in #guard_msgs docstrings where expected output includes position-dependent labels (e.g., invariant names derived from source positions shifted by added import lines).

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

[MikaelMayer]

🤖🔍 This PR systematically migrates 241 StrataTest files to Lean modules by adding module, converting imports to meta import/import all as needed, wrapping test code in meta section/end, and updating byte offsets in #guard_msgs output.

The mechanical changes are consistent and well-motivated. A few observations:

DenoteTests.lean: The ~60-line helper block (denoteQuery_rfl, denoteQuery_sorts_rfl, and supporting lemmas) is well-documented and addresses a real limitation of the module system. The maxHeartbeats 80000000 settings are high but appear necessary for the polymorphic sort examples.

ReflectTests.lean: The refactoring from elab macros to #eval do blocks is a clean adaptation to the module boundary constraints.

Loops.lean: Uses public section (rather than meta section) and public import, which makes sense since other test files import definitions from it.

EncoderTests.lean: The split into two sections (meta for #guard checks, non-meta for proofs) is a reasonable approach to the module boundary.

Overall this is a well-executed mechanical migration with thoughtful handling of the edge cases.

[atomb]

This looks good to me. I think the one test failure is due to a file in StrataTestExtra (rather than StrataTest) that needs a #guard_msgs update.

[MikaelMayer]

🤖🔍 The force-push updated ReflectTests.lean — switching from meta import/meta section to public import with meta def + elab macros. This is a cleaner approach than the previous #eval do ... MetaM.run' pattern.

One observation: the elaborate_lexpr test output changed from (5 == 5) = true to true — this is because #eval now reduces the expression rather than pretty-printing the elaborated form. The test still exercises LExpr.toExpr but verifies a different property (evaluation result vs. pretty-printed structure). This seems intentional given the module constraints but worth the PR author confirming.

All previous observations remain addressed — reviewer sign-off still needed.

[MikaelMayer]

🤖🔍 New commit "Fix extra tests" looks good. The shift from meta import all/meta section to explicit public import/public def in TestExamples.lean and TestDiagnostics.lean is cleaner — it makes cross-module visibility explicit rather than relying on meta sections. The added imports in Issue1000Test and VerifyPythonTest correctly account for the loss of transitive meta import all. All previous comments appear addressed — reviewer sign-off still needed.