Move module prove_rpc from ktool to proof

Author: tothtamas28

pyk/src/pyk/__main__.py

@@ -41,7 +41,7 @@
 from .ktool.kprint import KPrint
 from .ktool.kprove import KProve
 from .ktool.krun import KRun
-from .ktool.prove_rpc import ProveRpc
+from .proof.prove_rpc import ProveRpc
 from .proof.reachability import APRFailureInfo, APRProof
 from .proof.show import APRProofNodePrinter, APRProofShow
 from .utils import check_file_path, ensure_dir_path, exit_with_process_error

pyk/src/pyk/ktool/prove_rpc.py renamed to pyk/src/pyk/proof/prove_rpc.py

@@ -5,7 +5,7 @@
 
 from ..kast.manip import extract_lhs
 from ..kast.outer import KApply
-from ..proof import APRProof, APRProver, EqualityProof, ImpliesProver
+from . import APRProof, APRProver, EqualityProof, ImpliesProver
 
 if TYPE_CHECKING:
     from collections.abc import Callable
@@ -15,8 +15,8 @@
     from ..cli.pyk import ProveOptions
     from ..kast.outer import KClaim
     from ..kcfg import KCFGExplore
-    from ..proof import Proof, Prover
-    from .kprove import KProve
+    from ..ktool.kprove import KProve
+    from . import Proof, Prover
 
 _LOGGER: Final = logging.getLogger(__name__)
 

pyk/src/tests/integration/ktool/test_imp.py renamed to pyk/src/tests/integration/proof/test_prove_rpc.py

@@ -10,8 +10,8 @@
 from pyk.cli.pyk import ProveOptions
 from pyk.kast.inner import KApply, KSequence, KVariable
 from pyk.kcfg.semantics import DefaultSemantics
-from pyk.ktool.prove_rpc import ProveRpc
 from pyk.proof import ProofStatus
+from pyk.proof.prove_rpc import ProveRpc
 from pyk.testing import KCFGExploreTest, KProveTest
 from pyk.utils import single
 
@@ -170,7 +170,7 @@ def custom_step(self, c: CTerm, cs: CTermSymbolic) -> KCFGExtendResult | None:
 )
 
 
-class TestImpProve(KCFGExploreTest, KProveTest):
+class TestProveRpc(KCFGExploreTest, KProveTest):
     KOMPILE_MAIN_FILE = K_FILES / 'imp-verification.k'
 
     def semantics(self, definition: KDefinition) -> KCFGSemantics: