return list[CTerm]

Author: iFrostizz

src/pyk/__main__.py

@@ -1,5 +1,6 @@
 from __future__ import annotations
 
+import json
 import logging
 import sys
 from argparse import ArgumentParser, FileType
@@ -99,7 +100,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(final_state.kast.to_json())
+    args.output_file.write(json.dumps(mlOr([state.kast for state in final_state]).to_dict()))
     _LOGGER.info(f'Wrote file: {args.output_file.name}')
 
 

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
 
@@ -197,7 +197,7 @@ def prove(
         depth: int | None = None,
         haskell_log_format: KoreExecLogFormat = KoreExecLogFormat.ONELINE,
         haskell_log_debug_transition: bool = True,
-    ) -> CTerm:
+    ) -> list[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,14 @@ def prove(
             raise RuntimeError('kprove failed!')
 
         if dry_run:
-            return CTerm.bottom()
+            return [CTerm.bottom()]
 
         debug_log = _get_rule_log(log_file)
-        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:
+        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 final_state
+        return final_states
 
     def prove_claim(
         self,
@@ -265,7 +266,7 @@ def prove_claim(
         allow_zero_step: bool = False,
         dry_run: bool = False,
         depth: int | None = None,
-    ) -> CTerm:
+    ) -> list[CTerm]:
         with self._tmp_claim_definition(claim, claim_id, lemmas=lemmas) as (claim_path, claim_module_name):
             return self.prove(
                 claim_path,
@@ -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,7 +306,8 @@ def prove_cterm(
             allow_zero_step=allow_zero_step,
             depth=depth,
         )
-        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) 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 = [
             CTerm.from_kast(mlAnd([constraint_subst.unapply(ns), constraint_subst.ml_pred])) for ns in next_states

src/tests/integration/kprove/test_emit_json_spec.py

@@ -5,10 +5,12 @@
 
 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
@@ -41,7 +43,7 @@ def test_prove_claim(self, kprove: KProve, spec_module: KFlatModule) -> None:
         result = kprove.prove_claim(spec_module.claims[0], 'looping-1')
 
         # Then
-        assert result.is_top
+        assert CTerm._is_top(mlOr([res.kast for res in result]))
 
     def test_prove(self, kprove: KProve, spec_module: KFlatModule) -> None:
         # Given
@@ -62,4 +64,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 result.is_top
+        assert CTerm._is_top(mlOr([res.kast for res in result]))

src/tests/integration/kprove/test_print_prove_rewrite.py

@@ -2,9 +2,11 @@
 
 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
@@ -45,4 +47,4 @@ def test_print_prove_rewrite(self, kprove: KProve) -> None:
 
         # Then
         assert actual == expected
-        assert result.is_top
+        assert CTerm._is_top(mlOr([res.kast for res in result]))

src/tests/integration/kprove/test_prove_claim_with_lemmas.py

@@ -2,10 +2,12 @@
 
 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
@@ -34,5 +36,5 @@ def test_prove_claim_with_lemmas(self, kprove: KProve) -> None:
         result2 = kprove.prove_claim(claim, 'claim-with-lemma', lemmas=[lemma])
 
         # Then
-        assert not result1.is_top
-        assert result2.is_top
+        assert not CTerm._is_top(mlOr([res.kast for res in result1]))
+        assert CTerm._is_top(mlOr([res.kast for res in result2]))