Fully qualify claim labels/dependencies, include dependencies in output (#842)

We were having trouble in
runtimeverification/evm-semantics#2272 selecting
the correct claims because they can be unqualified by the user. This PR:

- Fully qualifies all claim labels and dependency labels returned by
`KProve.get_claim_modules`.
- Makes sure that we return not only the user-selected claims, but their
dependencies (unless the user turns that off), from `KProve.get_claims`.
- Adds a test-suite for the claim selection functionality.

There is a bug in this code, and a test added (and skipped using
`pytest.skip()`) which demonstrates a (probably minor) issue where we
are not checking that claim dependencies are in a module imported by the
current module.

---------

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

Author: ehildenb

docs/conf.py

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

package/version

@@ -1 +1 @@
-0.1.605
+0.1.606

pyproject.toml

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

src/pyk/ktool/kprove.py

@@ -347,6 +347,7 @@ def get_claims(
         md_selector: str | None = None,
         claim_labels: Iterable[str] | None = None,
         exclude_claim_labels: Iterable[str] | None = None,
+        include_dependencies: bool = True,
     ) -> list[KClaim]:
         flat_module_list = self.get_claim_modules(
             spec_file=spec_file,
@@ -355,16 +356,51 @@ def get_claims(
             md_selector=md_selector,
         )
 
-        all_claims = {c.label: c for m in flat_module_list.modules for c in m.claims}
-        unfound_labels = []
-        claim_labels = list(all_claims.keys()) if claim_labels is None else claim_labels
-        exclude_claim_labels = [] if exclude_claim_labels is None else exclude_claim_labels
-        unfound_labels.extend([cl for cl in claim_labels if cl not in all_claims])
-        unfound_labels.extend([cl for cl in exclude_claim_labels if cl not in all_claims])
+        _module_names = [module.name for module in flat_module_list.modules]
+
+        def _get_claim_module(_label: str) -> str | None:
+            if _label.find('.') > 0 and _label.split('.')[0] in _module_names:
+                return _label.split('.')[0]
+            return None
+
+        all_claims = {
+            claim.label: (claim, _get_claim_module(claim.label))
+            for module in flat_module_list.modules
+            for claim in module.claims
+            if _get_claim_module(claim.label) is not None
+        }
+
+        claim_labels = list(all_claims.keys()) if claim_labels is None else list(claim_labels)
+        exclude_claim_labels = [] if exclude_claim_labels is None else list(exclude_claim_labels)
+
+        final_claims: dict[str, KClaim] = {}
+        unfound_labels: list[str] = []
+        while len(claim_labels) > 0:
+            claim_label = claim_labels.pop(0)
+            if claim_label in final_claims or claim_label in exclude_claim_labels:
+                continue
+            if claim_label not in all_claims:
+                claim_label = f'{flat_module_list.main_module}.{claim_label}'
+            if claim_label not in all_claims:
+                unfound_labels.append(claim_label)
+                continue
+
+            _claim, _module_name = all_claims[claim_label]
+            _updated_dependencies: list[str] = []
+            for _dependency_label in _claim.dependencies:
+                if _get_claim_module(_dependency_label) is None:
+                    _dependency_label = f'{_module_name}.{_dependency_label}'
+                _updated_dependencies.append(_dependency_label)
+            if len(_updated_dependencies) > 0:
+                claim_labels.extend(_updated_dependencies)
+                _claim = _claim.let(att=_claim.att.update({'depends': ','.join(_updated_dependencies)}))
+
+            final_claims[claim_label] = _claim
+
         if len(unfound_labels) > 0:
             raise ValueError(f'Claim labels not found: {unfound_labels}')
 
-        return [all_claims[cl] for cl in all_claims if cl in claim_labels and cl not in exclude_claim_labels]
+        return list(final_claims.values())
 
     @contextmanager
     def _tmp_claim_definition(

src/tests/integration/k-files/multi-claim-spec.k

@@ -0,0 +1,40 @@
+module MULTI-CLAIM
+    configuration <k> $PGM:Pgm </k>
+
+    syntax Pgm ::= "a" | "b" | "c"
+endmodule
+
+module MULTI-CLAIM-SPEC-DEPENDENCY-1
+    imports MULTI-CLAIM
+
+    claim [dep-1.1]: <k> a => b </k>
+endmodule
+
+module MULTI-CLAIM-SPEC-DEPENDENCY-2
+    imports MULTI-CLAIM
+
+    claim [dep-2.1]: <k> b => c </k>
+
+    claim [dep-2.2]: <k> b => c </k> [depends(MULTI-CLAIM-SPEC-DEPENDENCY-1.dep-1.1)]
+
+    claim [rep-dep]: <k> c => b </k>
+endmodule
+
+module MULTI-CLAIM-SPEC
+    imports MULTI-CLAIM-SPEC-DEPENDENCY-1
+    imports MULTI-CLAIM-SPEC-DEPENDENCY-2
+
+    claim <k> a => b </k>
+
+    claim [dep]: <k> c => a </k>
+
+    claim [main.1]: <k> a => c </k> [depends(dep,MULTI-CLAIM-SPEC-DEPENDENCY-1.dep-1.1)]
+
+    claim [main.2]: <k> a => c </k> [depends(dep,MULTI-CLAIM-SPEC-DEPENDENCY-1.dep-1.2)]
+
+    claim [main.3]: <k> a => c </k> [depends(MULTI-CLAIM-SPEC.dep)]
+
+    claim [main.4]: <k> a => c </k> [depends(dep-1.2)]
+
+    claim [rep-dep]: <k> c => b </k>
+endmodule

src/tests/integration/kprove/test_get_claims.py

@@ -0,0 +1,97 @@
+from __future__ import annotations
+
+from typing import TYPE_CHECKING
+
+import pytest
+
+from pyk.testing import KProveTest
+
+from ..utils import K_FILES
+
+if TYPE_CHECKING:
+    from collections.abc import Iterable
+
+    from pyk.ktool.kprove import KProve
+
+
+GET_CLAIMS_SPEC_DATA_SKIP: Iterable[str] = ('simple-dep-in-submodule-2',)
+
+
+GET_CLAIMS_SPEC_DATA: Iterable[tuple[str, list[str], dict[str, list[str]] | None]] = (
+    (
+        'simple-dep-in-submodule-fail',
+        ['dep-1.1'],
+        None,
+    ),
+    (
+        'simple-dep-in-submodule-pass',
+        ['MULTI-CLAIM-SPEC-DEPENDENCY-1.dep-1.1'],
+        {'MULTI-CLAIM-SPEC-DEPENDENCY-1.dep-1.1': []},
+    ),
+    (
+        'simple-dep-in-submodule-2',
+        ['MULTI-CLAIM-SPEC-DEPENDENCY-2.dep-2.2'],
+        None,
+    ),
+    (
+        'no-dep-name-unqualified',
+        ['dep'],
+        {'MULTI-CLAIM-SPEC.dep': []},
+    ),
+    (
+        'no-dep-name-qualified',
+        ['MULTI-CLAIM-SPEC.dep'],
+        {'MULTI-CLAIM-SPEC.dep': []},
+    ),
+    (
+        'two-deps-one-nested',
+        ['MULTI-CLAIM-SPEC.main.1'],
+        {
+            'MULTI-CLAIM-SPEC.main.1': ['MULTI-CLAIM-SPEC.dep', 'MULTI-CLAIM-SPEC-DEPENDENCY-1.dep-1.1'],
+            'MULTI-CLAIM-SPEC.dep': [],
+            'MULTI-CLAIM-SPEC-DEPENDENCY-1.dep-1.1': [],
+        },
+    ),
+    (
+        'bad-unqualified-main-dep',
+        ['MULTI-CLAIM-SPEC.main.4'],
+        None,
+    ),
+    (
+        'rep-dep-in-submodule',
+        ['rep-dep'],
+        {'MULTI-CLAIM-SPEC.rep-dep': []},
+    ),
+)
+
+
+class TestGetClaims(KProveTest):
+    KOMPILE_MAIN_FILE = K_FILES / 'multi-claim-spec.k'
+    KOMPILE_ARGS = {'main_module': 'MULTI-CLAIM'}
+    SPEC_MODULE_NAME = 'MULTI-CLAIM-SPEC'
+
+    @pytest.mark.parametrize(
+        'test_id,include_labels,expected_graph',
+        GET_CLAIMS_SPEC_DATA,
+        ids=[test_id for test_id, *_ in GET_CLAIMS_SPEC_DATA],
+    )
+    def test_get_claims(
+        self, kprove: KProve, test_id: str, include_labels: list[str], expected_graph: dict[str, list[str]] | None
+    ) -> None:
+        if test_id in GET_CLAIMS_SPEC_DATA_SKIP:
+            pytest.skip()
+        if expected_graph is None:
+            with pytest.raises(ValueError):
+                actual_claims = kprove.get_claims(
+                    self.KOMPILE_MAIN_FILE, self.SPEC_MODULE_NAME, claim_labels=include_labels
+                )
+
+        else:
+            actual_claims = kprove.get_claims(
+                self.KOMPILE_MAIN_FILE, self.SPEC_MODULE_NAME, claim_labels=include_labels
+            )
+            actual_graph: dict[str, list[str]] = {claim.label: claim.dependencies for claim in actual_claims}
+
+            assert set(expected_graph.keys()) == set(actual_graph.keys())
+            for claim_label, deps in expected_graph.items():
+                assert set(deps) == set(actual_graph[claim_label])