Fix claim selection process for unlabeled claims (runtimeverification/pyk#866)

Here: runtimeverification/pyk#842, a mistake was
made where claims without labels were filtered out of the claims to be
processed and returned by `KProve.get_claims`. This PR addresses that
and adds tests. In particular:

- Two claims in the `multi-claim-spec.k` which were ill-formed because
of dependencies (but not tested for it) are removed.
- An ill-formed (because of dependencies) claim is added in a separate
module, and a new test added which exercises that a `ValueError` is
thrown when loading this module.
- A new test is added which asserts that the correct number of claims is
loaded from the main module. On `master`, this test is failing because
it skips claims without labels, but is fixed on this PR.
- Adjustments to how claims are filtered are made, so that it's simpler
and includes all claims, even ones without explicit module names in the
label.

---------

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

Author: 2 people

pyk/docs/conf.py

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

pyk/package/version

@@ -1 +1 @@
-0.1.615
+0.1.616

pyk/pyproject.toml

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

pyk/src/pyk/ktool/kprove.py

@@ -364,10 +364,7 @@ def _get_claim_module(_label: str) -> str | None:
             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.label: (claim, module.name) for module in flat_module_list.modules for claim in module.claims
         }
 
         claim_labels = list(all_claims.keys()) if claim_labels is None else list(claim_labels)

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

@@ -26,15 +26,19 @@ module MULTI-CLAIM-SPEC
 
     claim <k> a => b </k>
 
+    claim <k> a => c </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
+
+module MULTI-CLAIM-BROKEN-SPEC
+    imports MULTI-CLAIM-SPEC
+
+    claim [bad-dep]: <k> a => b </k> [depends(non-existent-1)]
+endmodule

pyk/src/tests/integration/kprove/test_get_claims.py

@@ -95,3 +95,11 @@ def test_get_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])
+
+    def test_get_claims_unlabeled(self, kprove: KProve) -> None:
+        claims = kprove.get_claims(self.KOMPILE_MAIN_FILE, self.SPEC_MODULE_NAME)
+        assert len(claims) == 10
+
+    def test_get_claims_broken(self, kprove: KProve) -> None:
+        with pytest.raises(ValueError):
+            kprove.get_claims(self.KOMPILE_MAIN_FILE, 'MULTI-CLAIM-BROKEN-SPEC')