Add module_name method for method name processing (#865)

Addresses runtimeverification/kontrol#337. 

This PR adds property `module_name` to `APRProof`, which transforms the
`proof.id` into a valid module name by escaping illegal characters. It
also adds substitution of `[` and `]` with `bkp`.

~This PR adds static method `make_module_name` to `KFlatModule`, which
transforms the `proof.id` into a valid module name by escaping illegal
characters. It also adds substitution of `[` and `]` with `-bkp-`. It
also adds a unit test for `make_module_name`.~

---------

Co-authored-by: devops <[email protected]>

Author: palinatolmach

docs/conf.py

@@ -9,8 +9,8 @@
 project = 'pyk'
 author = 'Runtime Verification, Inc'
 copyright = '2024, Runtime Verification, Inc'
-version = '0.1.617'
-release = '0.1.617'
+version = '0.1.618'
+release = '0.1.618'
 
 # -- General configuration ---------------------------------------------------
 # https://www.sphinx-doc.org/en/master/usage/configuration.html#general-configuration

package/version

@@ -1 +1 @@
-0.1.617
+0.1.618

pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "pyk"
-version = "0.1.617"
+version = "0.1.618"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

src/pyk/proof/reachability.py

@@ -92,6 +92,10 @@ def __init__(
                 assert type(subproof) is RefutationProof
                 self.node_refutations[node_id] = subproof
 
+    @property
+    def module_name(self) -> str:
+        return self._make_module_name(self.id)
+
     @property
     def pending(self) -> list[KCFG.Node]:
         return [node for node in self.explorable if self.is_pending(node.id)]
@@ -130,6 +134,12 @@ def prune(self, node_id: NodeIdLike, keep_nodes: Iterable[NodeIdLike] = ()) -> l
         pruned_nodes = super().prune(node_id, keep_nodes=list(keep_nodes) + [self.init, self.target])
         return pruned_nodes
 
+    @staticmethod
+    def _make_module_name(proof_id: str) -> str:
+        return 'M-' + re.sub(
+            r'[\[\]]|[_%().:,]+', lambda match: 'bkt' if match.group(0) in ['[', ']'] else '-', proof_id.upper()
+        )
+
     @staticmethod
     def read_proof(id: str, proof_dir: Path) -> APRProof:
         proof_path = proof_dir / f'{hash_str(id)}.json'
@@ -731,7 +741,7 @@ def _inject_module(module_name: str, import_name: str, sentences: list[KRuleLike
                 dependencies_as_rules.append(apr_subproof.as_rule(priority=20))
         circularity_rule = proof.as_rule(priority=20)
 
-        module_name = 'M-' + re.sub(r'[_%().:,]+', '-', self.proof.id.upper())
+        module_name = self.proof.module_name
         self.dependencies_module_name = module_name + '-DEPENDS-MODULE'
         self.circularities_module_name = module_name + '-CIRCULARITIES-MODULE'
         _inject_module(self.dependencies_module_name, self.main_module_name, dependencies_as_rules)

src/tests/unit/test_proof.py

@@ -15,6 +15,7 @@
 
 if TYPE_CHECKING:
     from pathlib import Path
+    from typing import Final
 
     from pytest import TempPathFactory
 
@@ -219,6 +220,25 @@ def test_apr_proof_from_dict_heterogeneous_subproofs(proof_dir: Path) -> None:
     assert proof.dict == proof_from_disk.dict
 
 
+MODULE_NAME_TEST_DATA: Final = (
+    ('sq-bracket', 'TEST-KONTROL-TEST-UINT256-BYTES[]-0', 'M-TEST-KONTROL-TEST-UINT256-BYTESbktbkt-0'),
+    ('underscore', 'TEST_KONTROL_%)_UINT256-1', 'M-TEST-KONTROL-UINT256-1'),
+)
+
+
+@pytest.mark.parametrize(
+    'test_id,proof_id,expected',
+    MODULE_NAME_TEST_DATA,
+    ids=[test_id for test_id, *_ in MODULE_NAME_TEST_DATA],
+)
+def test_proof_module_name(test_id: str, proof_id: str, expected: str) -> None:
+    # Given
+    output = APRProof._make_module_name(proof_id)
+
+    # Then
+    assert output == expected
+
+
 #### APRBMCProof