test APRProver: what if a dependency fails (#631)

Adds an untrue RL claim which depends on an untrue dependency, and two
tests: (1) if the dependency is admitted, the main claim passes (even
though untrue), and (2) if the dependency is not admitted, then the main
claim will not be proved (will have status 'pending').

---------

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

Author: 3 people

package/version

@@ -1 +1 @@
-0.1.432
+0.1.433

pyproject.toml

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

src/tests/integration/k-files/imp-simple-spec.k

@@ -164,4 +164,12 @@ module IMP-SIMPLE-SPEC
                         </state>
                       requires 0 <=Int N
 
+    claim [simple-untrue]:
+      <state>... $s |-> (1 => 2) ...</state>
+
+    claim [dep-fail-1]:
+      <k> $s = $s + 1; => . ...</k>
+      <state> $s |-> (0 => 2) </state>
+      [depends(simple-untrue)]
+
 endmodule

src/tests/integration/kcfg/test_imp.py

@@ -343,7 +343,9 @@ def same_loop(self, c1: CTerm, c2: CTerm) -> bool:
     ),
 )
 
-APR_PROVE_TEST_DATA: Iterable[tuple[str, Path, str, str, int | None, int | None, Iterable[str], ProofStatus, int]] = (
+APR_PROVE_TEST_DATA: Iterable[
+    tuple[str, Path, str, str, int | None, int | None, Iterable[str], bool, ProofStatus, int]
+] = (
     (
         'imp-simple-addition-1',
         K_FILES / 'imp-simple-spec.k',
@@ -352,6 +354,7 @@ def same_loop(self, c1: CTerm, c2: CTerm) -> bool:
         2,
         1,
         [],
+        True,
         ProofStatus.PASSED,
         1,
     ),
@@ -363,6 +366,7 @@ def same_loop(self, c1: CTerm, c2: CTerm) -> bool:
         2,
         7,
         [],
+        True,
         ProofStatus.PASSED,
         1,
     ),
@@ -374,6 +378,7 @@ def same_loop(self, c1: CTerm, c2: CTerm) -> bool:
         2,
         1,
         [],
+        True,
         ProofStatus.PASSED,
         1,
     ),
@@ -385,6 +390,7 @@ def same_loop(self, c1: CTerm, c2: CTerm) -> bool:
         2,
         100,
         [],
+        True,
         ProofStatus.PASSED,
         1,
     ),
@@ -396,6 +402,7 @@ def same_loop(self, c1: CTerm, c2: CTerm) -> bool:
         2,
         1,
         ['IMP.while'],
+        True,
         ProofStatus.PASSED,
         1,
     ),
@@ -407,6 +414,7 @@ def same_loop(self, c1: CTerm, c2: CTerm) -> bool:
         4,
         100,
         ['IMP.while'],
+        True,
         ProofStatus.PASSED,
         1,
     ),
@@ -418,6 +426,7 @@ def same_loop(self, c1: CTerm, c2: CTerm) -> bool:
         10,
         1,
         [],
+        True,
         ProofStatus.FAILED,
         2,
     ),
@@ -429,6 +438,7 @@ def same_loop(self, c1: CTerm, c2: CTerm) -> bool:
         None,
         None,
         [],
+        True,
         ProofStatus.PASSED,
         1,
     ),
@@ -440,6 +450,7 @@ def same_loop(self, c1: CTerm, c2: CTerm) -> bool:
         None,
         None,
         [],
+        True,
         ProofStatus.PASSED,
         1,
     ),
@@ -451,6 +462,7 @@ def same_loop(self, c1: CTerm, c2: CTerm) -> bool:
         None,
         None,
         [],
+        True,
         ProofStatus.PASSED,
         1,
     ),
@@ -462,6 +474,7 @@ def same_loop(self, c1: CTerm, c2: CTerm) -> bool:
         None,
         None,
         [],
+        True,
         ProofStatus.PASSED,
         2,
     ),
@@ -473,6 +486,7 @@ def same_loop(self, c1: CTerm, c2: CTerm) -> bool:
         None,
         None,
         [],
+        True,
         ProofStatus.PASSED,
         2,
     ),
@@ -484,6 +498,7 @@ def same_loop(self, c1: CTerm, c2: CTerm) -> bool:
         None,
         None,
         [],
+        True,
         ProofStatus.PASSED,
         1,  # We can reuse subproofs.
     ),
@@ -495,6 +510,7 @@ def same_loop(self, c1: CTerm, c2: CTerm) -> bool:
         None,
         None,
         [],
+        True,
         ProofStatus.PASSED,
         1,  # We can reuse subproofs.
     ),
@@ -506,6 +522,7 @@ def same_loop(self, c1: CTerm, c2: CTerm) -> bool:
         None,
         None,
         ['IMP.while'],  # If we do not include `IMP.while` in this list, we get 4 branches instead of 2
+        True,
         ProofStatus.PASSED,
         2,
     ),
@@ -517,6 +534,7 @@ def same_loop(self, c1: CTerm, c2: CTerm) -> bool:
         None,
         None,
         [],
+        True,
         ProofStatus.PASSED,
         1,
     ),
@@ -528,9 +546,34 @@ def same_loop(self, c1: CTerm, c2: CTerm) -> bool:
         None,
         None,
         [],
+        False,
         ProofStatus.FAILED,
         1,
     ),
+    (
+        'imp-dep-untrue-fail',
+        K_FILES / 'imp-simple-spec.k',
+        'IMP-SIMPLE-SPEC',
+        'dep-fail-1',
+        None,
+        None,
+        [],
+        False,
+        ProofStatus.PENDING,  # because we do NOT admit the dependency
+        1,
+    ),
+    (
+        'imp-dep-untrue-admitted',
+        K_FILES / 'imp-simple-spec.k',
+        'IMP-SIMPLE-SPEC',
+        'dep-fail-1',
+        None,
+        None,
+        [],
+        True,
+        ProofStatus.PASSED,  # because we DO admit the dependency, even though it is untrue
+        1,
+    ),
 )
 
 PATH_CONSTRAINTS_TEST_DATA: Iterable[
@@ -824,7 +867,7 @@ def test_assume_defined(
         assert actual == expected
 
     @pytest.mark.parametrize(
-        'test_id,spec_file,spec_module,claim_id,max_iterations,max_depth,cut_rules,proof_status,expected_leaf_number',
+        'test_id,spec_file,spec_module,claim_id,max_iterations,max_depth,cut_rules,admit_deps,proof_status,expected_leaf_number',
         APR_PROVE_TEST_DATA,
         ids=[test_id for test_id, *_ in APR_PROVE_TEST_DATA],
     )
@@ -839,6 +882,7 @@ def test_all_path_reachability_prove(
         max_iterations: int | None,
         max_depth: int | None,
         cut_rules: Iterable[str],
+        admit_deps: bool,
         proof_status: ProofStatus,
         expected_leaf_number: int,
         tmp_path_factory: TempPathFactory,
@@ -871,7 +915,8 @@ def qualify(module: str, label: str) -> str:
                 for c in deps_claims
             ]
             for dp in deps_proofs:
-                dp.admit()
+                if admit_deps:
+                    dp.admit()
                 dp.write_proof_data()
             # </Admit all the dependencies >