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

package/version

@@ -1 +1 @@
-0.1.431
+0.1.432

pyproject.toml

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

src/pyk/__main__.py

@@ -1,6 +1,5 @@
 from __future__ import annotations
 
-import json
 import logging
 import sys
 from argparse import ArgumentParser, FileType
@@ -100,7 +99,7 @@ def exec_prove(args: Namespace) -> None:
     kompiled_dir: Path = args.definition_dir
     kprover = KProve(kompiled_dir, args.main_file)
     final_state = kprover.prove(Path(args.spec_file), spec_module_name=args.spec_module, args=args.kArgs)
-    args.output_file.write(json.dumps(mlOr([state.kast for state in final_state]).to_dict()))
+    args.output_file.write(final_state.kast.to_json())
     _LOGGER.info(f'Wrote file: {args.output_file.name}')
 
 

src/pyk/cterm.py

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

src/pyk/ktool/kprove.py

@@ -197,7 +197,7 @@ def prove(
         depth: int | None = None,
         haskell_log_format: KoreExecLogFormat = KoreExecLogFormat.ONELINE,
         haskell_log_debug_transition: bool = True,
-    ) -> list[CTerm]:
+    ) -> CTerm:
         log_file = spec_file.with_suffix('.debug-log') if log_axioms_file is None else log_axioms_file
         if log_file.exists():
             log_file.unlink()
@@ -245,13 +245,13 @@ def prove(
             raise RuntimeError('kprove failed!')
 
         if dry_run:
-            return [CTerm.bottom()]
+            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:
+        final_state = CTerm.from_kast(kast_term(json.loads(proc_result.stdout), KInner))  # type: ignore # https://github.com/python/mypy/issues/4717
+        if final_state.is_top 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_state
 
     def prove_claim(
         self,
@@ -265,7 +265,7 @@ def prove_claim(
         allow_zero_step: bool = False,
         dry_run: bool = False,
         depth: int | None = None,
-    ) -> list[CTerm]:
+    ) -> CTerm:
         with self._tmp_claim_definition(claim, claim_id, lemmas=lemmas) as (claim_path, claim_module_name):
             return self.prove(
                 claim_path,
@@ -305,12 +305,12 @@ 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)))
         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,7 @@ 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 result.is_top
 
     def test_prove(self, kprove: KProve, spec_module: KFlatModule) -> None:
         # Given
@@ -64,4 +62,4 @@ 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 result.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,4 @@ 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 result.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,5 @@ 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 not result1.is_top
+        assert result2.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())