Add RPC based prover to KProve interface (#948)

This PR aims to expose a very basic RPC prover in the `KProve` class. In
particular:

- The command `pyk prove ...` is renamed to `pyk prove-legacy ...` (and
single test adjusted). This functionality is not really used anywhere.
- The functionality `legacy_explore` from KEVM is upstreamd to
`cterm_symbolic` helper in `cterm.symbolic`. It has the same option to
start or not an RPC server, and also implements the context-manager
functionality.
- The functionality to do proving with RPC server is added to `KProve`.
We have:
- `KProve.prove_claim_rpc`: starts up a `kore-rpc` server using
`cterm_symbolic`, and runs the proof as an `APRProof`. Nothing fancy is
done with interpreting claim dependencies, circularities, or
parallelism.
- `KProve.prove_rpc`: mimics the `KProve.prove` interface where a spec
file with a potential list of claims is passed in, collects the claims
and discharges them with `KProve.prove_claim_rpc`.
- A lot of defunct functionality is removed from `KProve`:
- Early prototype of RPC based prover `KProve.prove_cterm` is removed,
and associated tests.
- Various arguments to `KProve.prove` which were not being used
anywhere, or only used in specific ways, are eliminated to simplify the
function (for eventual removal of that function, as it's the
`prove-legacy` hookup).
- The function `KProve.get_claim_modules` no longer uses
`KProve.prove(...)` functionality, instead directly invokes
`_kprove(...)` helper to further allow `KProve.prove(...)` to be
simplified.
- A test-suite is added for `KProve.prove_rpc` which re-uses all the
tests from `proof/test_imp.py` which are passing using the new interface
directly, to make sure the functionality doesn't break.

---------

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

Author: ehildenb

docs/conf.py

@@ -9,8 +9,8 @@
 project = 'pyk'
 author = 'Runtime Verification, Inc'
 copyright = '2024, Runtime Verification, Inc'
-version = '0.1.691'
-release = '0.1.691'
+version = '0.1.692'
+release = '0.1.692'
 
 # -- General configuration ---------------------------------------------------
 # https://www.sphinx-doc.org/en/master/usage/configuration.html#general-configuration

package/version

@@ -1 +1 @@
-0.1.691
+0.1.692

pyproject.toml

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

src/pyk/__main__.py

@@ -210,7 +210,7 @@ def exec_rpc_kast(args: Namespace) -> None:
     args.output_file.write(json.dumps(request))
 
 
-def exec_prove(args: Namespace) -> None:
+def exec_prove_legacy(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)
@@ -310,16 +310,16 @@ def create_argument_parser() -> ArgumentParser:
     )
     rpc_kast_args.add_argument('--output-file', type=FileType('w'), default='-')
 
-    prove_args = pyk_args_command.add_parser(
-        'prove',
+    prove_legacy_args = pyk_args_command.add_parser(
+        'prove-legacy',
         help='Prove an input specification (using kprovex).',
         parents=[k_cli_args.logging_args, definition_args],
     )
-    prove_args.add_argument('main_file', type=str, help='Main file used for kompilation.')
-    prove_args.add_argument('spec_file', type=str, help='File with the specification module.')
-    prove_args.add_argument('spec_module', type=str, help='Module with claims to be proven.')
-    prove_args.add_argument('--output-file', type=FileType('w'), default='-')
-    prove_args.add_argument('kArgs', nargs='*', help='Arguments to pass through to K invocation.')
+    prove_legacy_args.add_argument('main_file', type=str, help='Main file used for kompilation.')
+    prove_legacy_args.add_argument('spec_file', type=str, help='File with the specification module.')
+    prove_legacy_args.add_argument('spec_module', type=str, help='Module with claims to be proven.')
+    prove_legacy_args.add_argument('--output-file', type=FileType('w'), default='-')
+    prove_legacy_args.add_argument('kArgs', nargs='*', help='Arguments to pass through to K invocation.')
 
     pyk_args_command.add_parser(
         'graph-imports',

src/pyk/cterm/__init__.py

@@ -1,2 +1,2 @@
 from .cterm import CSubst, CTerm, build_claim, build_rule, cterm_build_claim, cterm_build_rule
-from .symbolic import CTermSymbolic
+from .symbolic import CTermSymbolic, cterm_symbolic

src/pyk/cterm/symbolic.py

@@ -1,25 +1,38 @@
 from __future__ import annotations
 
 import logging
+from contextlib import contextmanager
 from typing import TYPE_CHECKING, NamedTuple
 
 from ..cterm import CSubst, CTerm
 from ..kast.inner import KApply, KLabel, KRewrite, KVariable, Subst
 from ..kast.manip import flatten_label, free_vars
 from ..konvert import kast_to_kore, kore_to_kast
-from ..kore.rpc import AbortedResult, SatResult, StopReason, UnknownResult, UnsatResult
+from ..kore.rpc import (
+    AbortedResult,
+    KoreClient,
+    KoreExecLogFormat,
+    SatResult,
+    StopReason,
+    TransportType,
+    UnknownResult,
+    UnsatResult,
+    kore_server,
+)
 from ..prelude.k import GENERATED_TOP_CELL
 from ..prelude.ml import is_top, mlEquals, mlTop
 
 if TYPE_CHECKING:
-    from collections.abc import Iterable
+    from collections.abc import Iterable, Iterator
+    from pathlib import Path
     from typing import Final
 
     from ..kast import KInner
     from ..kast.outer import KDefinition
     from ..kore.kompiled import KompiledKore
-    from ..kore.rpc import KoreClient, LogEntry
+    from ..kore.rpc import FallbackReason, LogEntry
     from ..kore.syntax import Pattern
+    from ..utils import BugReport
 
 
 _LOGGER: Final = logging.getLogger(__name__)
@@ -228,3 +241,66 @@ def assume_defined(self, cterm: CTerm, module_name: str | None = None) -> CTerm:
         kast_simplified, logs = self.kast_simplify(kast, module_name=module_name)
         _LOGGER.debug(f'Definedness condition computed: {kast_simplified}')
         return cterm.add_constraint(kast_simplified)
+
+
+@contextmanager
+def cterm_symbolic(
+    definition: KDefinition,
+    kompiled_kore: KompiledKore,
+    definition_dir: Path,
+    *,
+    id: str | None = None,
+    port: int | None = None,
+    kore_rpc_command: str | Iterable[str] | None = None,
+    llvm_definition_dir: Path | None = None,
+    smt_timeout: int | None = None,
+    smt_retry_limit: int | None = None,
+    smt_tactic: str | None = None,
+    bug_report: BugReport | None = None,
+    haskell_log_format: KoreExecLogFormat = KoreExecLogFormat.ONELINE,
+    haskell_log_entries: Iterable[str] = (),
+    log_axioms_file: Path | None = None,
+    trace_rewrites: bool = False,
+    start_server: bool = True,
+    maude_port: int | None = None,
+    fallback_on: Iterable[FallbackReason] | None = None,
+    interim_simplification: int | None = None,
+    no_post_exec_simplify: bool = False,
+) -> Iterator[CTermSymbolic]:
+    if start_server:
+        # Old way of handling KoreServer, to be removed
+        with kore_server(
+            definition_dir=definition_dir,
+            llvm_definition_dir=llvm_definition_dir,
+            module_name=definition.main_module_name,
+            port=port,
+            command=kore_rpc_command,
+            bug_report=bug_report,
+            smt_timeout=smt_timeout,
+            smt_retry_limit=smt_retry_limit,
+            smt_tactic=smt_tactic,
+            haskell_log_format=haskell_log_format,
+            haskell_log_entries=haskell_log_entries,
+            log_axioms_file=log_axioms_file,
+            fallback_on=fallback_on,
+            interim_simplification=interim_simplification,
+            no_post_exec_simplify=no_post_exec_simplify,
+        ) as server:
+            with KoreClient('localhost', server.port, bug_report=bug_report, bug_report_id=id) as client:
+                yield CTermSymbolic(client, definition, kompiled_kore, trace_rewrites=trace_rewrites)
+    else:
+        if port is None:
+            raise ValueError('Missing port with start_server=False')
+        if maude_port is None:
+            dispatch = None
+        else:
+            dispatch = {
+                'execute': [('localhost', maude_port, TransportType.HTTP)],
+                'simplify': [('localhost', maude_port, TransportType.HTTP)],
+                'add-module': [
+                    ('localhost', maude_port, TransportType.HTTP),
+                    ('localhost', port, TransportType.SINGLE_SOCKET),
+                ],
+            }
+        with KoreClient('localhost', port, bug_report=bug_report, bug_report_id=id, dispatch=dispatch) as client:
+            yield CTermSymbolic(client, definition, kompiled_kore, trace_rewrites=trace_rewrites)