Allow compilation of a <file>:<module> via --add-module.

[mariaKt]

This PR extends the --add-module option to accept K source files (.k/.md) in addition to JSON, using the format file.k:MODULE_NAME or file.md:MODULE_NAME.

• Parses K source modules via kprove --dry-run (pyk's parse_modules), matching how kontrol's --lemmas flag works
• JSON format (file.json from --to-module) remains supported for backward compatibility
• Type of add_module changed from Path | None to str | None across the pipeline

The intend of this was to be used for conditional compilation of the lemmas added for the validate owner function. However, while working on it, I found that currently there are limitations to what rules can be loaded dynamically, making static compilation of the lemmas for validate owner a better short term option. We could comment out the imports, so that by default the lemmas are not used, or try adding a new build target.

Identified limitations

• syntax declarations (generally, other than tokens for existing sorts)
• KAs
• subsort injections

[Stevengre]

This looks like it currently lacks sufficient test coverage, especially for the newly introduced file.k/md/json:MODULE paths.

I’m also not fully convinced about the necessity of this feature. From my understanding, the “one file → one module” workflow already covers most use cases, so the added value here isn’t entirely clear to me yet.

That said, extending functionality is generally a good direction. However, before merging, I think we should at least have:

• Proper tests covering the new code paths (not just the existing JSON case)
• Documentation updates clarifying the intended use cases and expected behavior

Otherwise, this risks introducing an under-specified and under-tested feature into the codebase.

[mariaKt]

This looks like it currently lacks sufficient test coverage, especially for the newly introduced file.k/md/json:MODULE paths.

I’m also not fully convinced about the necessity of this feature. From my understanding, the “one file → one module” workflow already covers most use cases, so the added value here isn’t entirely clear to me yet.

That said, extending functionality is generally a good direction. However, before merging, I think we should at least have:

* Proper tests covering the new code paths (not just the existing JSON case)

* Documentation updates clarifying the intended use cases and expected behavior

Otherwise, this risks introducing an under-specified and under-tested feature into the codebase.

You are correct. Here is the context. When I first started this, there were multiple modules in a file and I meant to import only some, so the extension Path -> str made sense. Then, as I worked around the limitations, I ended up with only one module to be imported in the new file, so this extension alone (without the necessary pyk functionality extensions) would not help much. The feature I believe can be useful that is added here is the ability to read from .k/.md in addition to .json would be useful. However, there are restrictions in how the rules can be written when loading a .k/.md module, that are not present when using the .json path.

In any case, this cannot be used for the current lemmas, so as you point out I will need to add a couple of small unit tests for these.