Hotfix for the handling of bottom and top for the CTerm class

package/version

@@ -1 +1 @@
-0.1.448
+0.1.449

pyproject.toml

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

src/pyk/cterm.py

@@ -98,6 +98,10 @@ def _is_spurious_constraint(term: KInner) -> bool:
             return True
         return False
 
+    @cached_property
+    def is_top(self) -> bool:
+        return CTerm._is_top(self.kast)
+
     @staticmethod
     def _is_top(kast: KInner) -> bool:
         flat = flatten_label('#And', kast)

src/pyk/ktool/kprove.py

@@ -17,7 +17,7 @@
 from ..kast.inner import KInner
 from ..kast.manip import extract_subst, flatten_label, free_vars
 from ..kast.outer import KDefinition, KFlatModule, KFlatModuleList, KImport, KRequire
-from ..prelude.ml import is_top, mlAnd
+from ..prelude.ml import mlAnd
 from ..utils import gen_file_timestamp, run_process, unique
 from .kprint import KPrint
 
@@ -248,10 +248,11 @@ def prove(
             return [CTerm.bottom()]
 
         debug_log = _get_rule_log(log_file)
-        final_state = kast_term(json.loads(proc_result.stdout), KInner)  # type: ignore # https://github.com/python/mypy/issues/4717
-        if is_top(final_state) and len(debug_log) == 0 and not allow_zero_step:
+        as_kast = kast_term(json.loads(proc_result.stdout), KInner)  # type: ignore # https://github.com/python/mypy/issues/4717
+        final_states = [CTerm.from_kast(disjunct) for disjunct in flatten_label('#Or', as_kast)]
+        if next(state.is_top for state in final_states) and len(debug_log) == 0 and not allow_zero_step:
             raise ValueError(f'Proof took zero steps, likely the LHS is invalid: {spec_file}')
-        return [CTerm.from_kast(disjunct) for disjunct in flatten_label('#Or', final_state)]
+        return final_states
 
     def prove_claim(
         self,
@@ -295,7 +296,7 @@ def prove_cterm(
         depth: int | None = None,
     ) -> list[CTerm]:
         claim, var_map = build_claim(claim_id, init_cterm, target_cterm, keep_vars=free_vars(init_cterm.kast))
-        next_state = self.prove_claim(
+        next_states_cterm = self.prove_claim(
             claim,
             claim_id,
             lemmas=lemmas,
@@ -305,12 +306,13 @@ def prove_cterm(
             allow_zero_step=allow_zero_step,
             depth=depth,
         )
-        next_states = list(unique(CTerm.from_kast(var_map(ns.kast)) for ns in next_state if not CTerm._is_top(ns.kast)))
+        # next_states = list(unique(var_map(ns) for ns in flatten_label('#Or', next_state.kast) if not is_top(ns)))
+        next_states = list(unique(var_map(ns.kast) for ns in next_states_cterm if not ns.is_top))
         constraint_subst, _ = extract_subst(init_cterm.kast)
-        next_states = [
-            CTerm.from_kast(mlAnd([constraint_subst.unapply(ns.kast), constraint_subst.ml_pred])) for ns in next_states
+        next_states_cterm = [
+            CTerm.from_kast(mlAnd([constraint_subst.unapply(ns), constraint_subst.ml_pred])) for ns in next_states
         ]
-        return next_states if len(next_states) > 0 else [CTerm.top()]
+        return next_states_cterm if len(next_states_cterm) > 0 else [CTerm.top()]
 
     def get_claim_modules(
         self,

src/tests/integration/kprove/test_emit_json_spec.py

@@ -5,12 +5,10 @@
 
 import pytest
 
-from pyk.cterm import CTerm
 from pyk.kast.kast import EMPTY_ATT
 from pyk.kast.manip import remove_generated_cells
 from pyk.kast.outer import KDefinition, KRequire
 from pyk.kast.pretty import paren
-from pyk.prelude.ml import mlOr
 from pyk.testing import KProveTest
 
 from ..utils import K_FILES
@@ -43,7 +41,8 @@ def test_prove_claim(self, kprove: KProve, spec_module: KFlatModule) -> None:
         result = kprove.prove_claim(spec_module.claims[0], 'looping-1')
 
         # Then
-        assert CTerm._is_top(mlOr([res.kast for res in result]))
+        assert len(result) == 1
+        assert result[0].is_top
 
     def test_prove(self, kprove: KProve, spec_module: KFlatModule) -> None:
         # Given
@@ -64,4 +63,5 @@ def test_prove(self, kprove: KProve, spec_module: KFlatModule) -> None:
         result = kprove.prove(spec_file, spec_module_name=spec_module_name, args=['-I', str(include_dir)])
 
         # Then
-        assert CTerm._is_top(mlOr([res.kast for res in result]))
+        assert len(result) == 1
+        assert result[0].is_top

src/tests/integration/kprove/test_print_prove_rewrite.py

@@ -2,11 +2,9 @@
 
 from typing import TYPE_CHECKING
 
-from pyk.cterm import CTerm
 from pyk.kast.inner import KApply, KRewrite, KVariable
 from pyk.kast.manip import push_down_rewrites
 from pyk.kast.outer import KClaim
-from pyk.prelude.ml import mlOr
 from pyk.testing import KProveTest
 
 from ..utils import K_FILES
@@ -47,4 +45,5 @@ def test_print_prove_rewrite(self, kprove: KProve) -> None:
 
         # Then
         assert actual == expected
-        assert CTerm._is_top(mlOr([res.kast for res in result]))
+        assert len(result) == 1
+        assert result[0].is_top

src/tests/integration/kprove/test_prove_claim_with_lemmas.py

@@ -2,12 +2,10 @@
 
 from typing import TYPE_CHECKING
 
-from pyk.cterm import CTerm
 from pyk.kast import KAtt
 from pyk.kast.inner import KToken
 from pyk.kast.outer import KClaim, KRule
 from pyk.prelude.kbool import BOOL
-from pyk.prelude.ml import mlOr
 from pyk.testing import KProveTest
 
 from ..utils import K_FILES
@@ -36,5 +34,7 @@ def test_prove_claim_with_lemmas(self, kprove: KProve) -> None:
         result2 = kprove.prove_claim(claim, 'claim-with-lemma', lemmas=[lemma])
 
         # Then
-        assert not CTerm._is_top(mlOr([res.kast for res in result1]))
-        assert CTerm._is_top(mlOr([res.kast for res in result2]))
+        assert len(result1) == 1
+        assert len(result2) == 1
+        assert not result1[0].is_top
+        assert result2[0].is_top

src/tests/integration/test_pyk.py

@@ -93,5 +93,5 @@ def test_minimize_term(self, assume_argv: AssumeArgv, tmp_path: Path, definition
         main()
         assume_argv(['pyk', 'print', str(definition_dir), str(prove_res_file), '--output-file', str(actual_file)])
         main()
-        # assert expected_file.read_text() == actual_file.read_text()
+        assert expected_file.read_text() == actual_file.read_text()
         expected_file.write_text(actual_file.read_text())