diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index 7eae5bcee0..25d65fa3c7 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -45,7 +45,7 @@ jobs: gh release upload --repo runtimeverification/k --clobber "v${version}" "${tarball}" cachix-release: - name: 'k-framework-binary cachix release' + name: 'Cachix release (binary cache `k-framework-binary` + dependency cache `k-framework`)' strategy: matrix: include: @@ -79,7 +79,14 @@ jobs: with: name: k-framework-binary - - name: 'Publish K to k-framework-binary cache' + # Both publishes build the same three derivations, so they run as sequential + # steps on one runner: the first populates the local Nix store and the second is + # a store hit. They run independently (continue-on-error) so a flaky upload to + # one cache neither blocks nor masks the other, and a final guard fails the job + # if either push failed. + - name: 'Publish K to k-framework-binary cache (private)' + id: binary + continue-on-error: true uses: workflow/nix-shell-action@v3.3.2 env: CACHIX_AUTH_TOKEN: '${{ secrets.CACHIX_PRIVATE_KFB_TOKEN }}' @@ -91,7 +98,7 @@ jobs: script: | # Install kup export PATH="$(nix build github:runtimeverification/kup --no-link --json | jq -r '.[].outputs | to_entries[].value')/bin:$PATH" - + # Publish all three package variants using kup publish # Using public macOS runner has proven reliable for large file uploads kup publish --verbose k-framework-binary .#k --keep-days 180 || true @@ -101,38 +108,9 @@ jobs: # kup/cachix pin visibility can be flaky; verify pins and narinfo via public API bash .github/scripts/check-cachix-pin.sh - cachix-release-dependencies: - name: 'k-framework cachix release' - strategy: - matrix: - include: - - runner: ubuntu-24.04 - os: ubuntu-24.04 - - runner: macos-latest - os: macos-15 - runs-on: ${{ matrix.runner }} - timeout-minutes: 120 - steps: - - name: 'Check out code' - uses: actions/checkout@v4 - - - name: 'Install Nix' - if: ${{ !startsWith(matrix.os, 'self') }} - uses: cachix/install-nix-action@v31.5.1 - with: - install_url: https://releases.nixos.org/nix/nix-2.30.1/install - extra_nix_config: | - access-tokens = github.com=${{ secrets.GITHUB_TOKEN }} - substituters = http://cache.nixos.org - trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= - - - name: 'Install Cachix' - if: ${{ !startsWith(matrix.os, 'self') }} - uses: cachix/cachix-action@v14 - with: - name: k-framework-binary - - - name: 'Build and cache K and K dependencies' + - name: 'Build and cache K and K dependencies (public)' + id: dependencies + continue-on-error: true uses: workflow/nix-shell-action@v3 env: GC_DONT_GC: 1 @@ -152,6 +130,14 @@ jobs: DRV_K_OPENSSL_PROCPS_SECP256K1=$(nix-store --query --deriver ${K_OPENSSL_PROCPS_SECP256K1}) nix-store --query --requisites --include-outputs ${DRV_K_OPENSSL_PROCPS_SECP256K1} | cachix push k-framework + - name: 'Fail if either cachix publish failed' + run: | + binary='${{ steps.binary.outcome }}' + dependencies='${{ steps.dependencies.outcome }}' + echo "binary publish: ${binary}" + echo "dependencies publish: ${dependencies}" + [ "${binary}" = 'success' ] && [ "${dependencies}" = 'success' ] + pyk-build-wheel: name: 'Pyk: Build Python wheel' runs-on: ubuntu-24.04 @@ -313,7 +299,7 @@ jobs: name: 'Publish Release' runs-on: [self-hosted, linux, normal] environment: production - needs: [cachix-release, cachix-release-dependencies, source-tarball, ubuntu-jammy, ubuntu-noble, set-release-id] + needs: [cachix-release, source-tarball, ubuntu-jammy, ubuntu-noble, set-release-id] steps: - name: 'Check out code' uses: actions/checkout@v4 diff --git a/deps/haskell-backend_release b/deps/haskell-backend_release index 8fe50701c1..a402c50ee2 100644 --- a/deps/haskell-backend_release +++ b/deps/haskell-backend_release @@ -1 +1 @@ -v0.1.147 +v0.1.150 diff --git a/flake.lock b/flake.lock index ab9f9a8cc4..9dc83c895c 100644 --- a/flake.lock +++ b/flake.lock @@ -64,16 +64,16 @@ "z3": "z3" }, "locked": { - "lastModified": 1779860189, - "narHash": "sha256-hCyz2V6ZDAqenUhZD7yPLk+EyiMauJghxMuOO1HHhWc=", + "lastModified": 1780590347, + "narHash": "sha256-iYTKRQzsC56EfHNuDO/O9MbMFmNV9c2CM4NwOXSeSc4=", "owner": "runtimeverification", "repo": "haskell-backend", - "rev": "786db62a39ac444e04481719339a60ae240e85cd", + "rev": "515eccf4a8ebbb0fe8ff807d15a96ce096ce2670", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v0.1.147", + "ref": "v0.1.150", "repo": "haskell-backend", "type": "github" } @@ -141,11 +141,11 @@ }, "nixpkgs-unstable": { "locked": { - "lastModified": 1779560665, - "narHash": "sha256-tpyBcxPpcQb8ukyNF7DoCwfSY3VPsxHoYwj00Cayv5o=", + "lastModified": 1780243769, + "narHash": "sha256-x5UQuRsH3MqI0U9afaXSNqzTPSeZlRLvFAav2Ux1pNw=", "owner": "NixOS", "repo": "nixpkgs", - "rev": "64c08a7ca051951c8eae34e3e3cb1e202fe36786", + "rev": "331800de5053fcebacf6813adb5db9c9dca22a0c", "type": "github" }, "original": { diff --git a/flake.nix b/flake.nix index 16d6ecf92c..5fd8648e61 100644 --- a/flake.nix +++ b/flake.nix @@ -8,7 +8,7 @@ llvm-backend.inputs.nixpkgs.follows = "nixpkgs"; haskell-backend = { - url = "github:runtimeverification/haskell-backend/v0.1.147"; + url = "github:runtimeverification/haskell-backend/v0.1.150"; inputs.rv-nix-tools.follows = "rv-nix-tools"; inputs.nixpkgs.follows = "nixpkgs"; }; diff --git a/haskell-backend/src/main/native/haskell-backend b/haskell-backend/src/main/native/haskell-backend index 786db62a39..515eccf4a8 160000 --- a/haskell-backend/src/main/native/haskell-backend +++ b/haskell-backend/src/main/native/haskell-backend @@ -1 +1 @@ -Subproject commit 786db62a39ac444e04481719339a60ae240e85cd +Subproject commit 515eccf4a8ebbb0fe8ff807d15a96ce096ce2670 diff --git a/install-k b/install-k index 6914b47e17..84c2e9b92b 100755 --- a/install-k +++ b/install-k @@ -1,6 +1,6 @@ #!/bin/sh -e -K_VERSION=7.1.329 +K_VERSION=7.1.333 if [ `id -u` -ne 0 ]; then echo "$0: error: This script must be run as root." diff --git a/package/debian/kframework/changelog b/package/debian/kframework/changelog index 32ccd32806..f55add2a85 100644 --- a/package/debian/kframework/changelog +++ b/package/debian/kframework/changelog @@ -1,4 +1,4 @@ -kframework (7.1.329) unstable; urgency=medium +kframework (7.1.333) unstable; urgency=medium * Initial Release. diff --git a/package/version b/package/version index 093b104b6f..6da8e9a46b 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -7.1.329 +7.1.333 diff --git a/pyk/docs/conf.py b/pyk/docs/conf.py index 88e64d2fd9..0c9d42bf9c 100644 --- a/pyk/docs/conf.py +++ b/pyk/docs/conf.py @@ -9,8 +9,8 @@ project = 'pyk' author = 'Runtime Verification, Inc' copyright = '2024, Runtime Verification, Inc' -version = '7.1.329' -release = '7.1.329' +version = '7.1.333' +release = '7.1.333' # -- General configuration --------------------------------------------------- # https://www.sphinx-doc.org/en/master/usage/configuration.html#general-configuration diff --git a/pyk/pyproject.toml b/pyk/pyproject.toml index 45227c7e3b..841ade38c6 100644 --- a/pyk/pyproject.toml +++ b/pyk/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "hatchling.build" [project] name = "kframework" -version = "7.1.329" +version = "7.1.333" description = "" readme = "README.md" requires-python = ">=3.10" diff --git a/pyk/src/pyk/__main__.py b/pyk/src/pyk/__main__.py index f958936569..9b6c974642 100644 --- a/pyk/src/pyk/__main__.py +++ b/pyk/src/pyk/__main__.py @@ -255,11 +255,18 @@ def exec_prove(options: ProveOptions) -> None: kprove = KProve(kompiled_directory, use_directory=options.temp_directory) + haskell_log_dir: Path | None = None + if options.haskell_logging: + if options.save_directory is None: + raise ValueError('--haskell-logging requires --save-directory to write the per-request log bundles') + haskell_log_dir = options.save_directory / 'haskell-logs' + @contextmanager def explore_context() -> Iterator[KCFGExplore]: with cterm_symbolic( definition=kprove.definition, definition_dir=kprove.definition_dir, + haskell_log_dir=haskell_log_dir, ) as cts: yield KCFGExplore(cts) diff --git a/pyk/src/pyk/cli/pyk.py b/pyk/src/pyk/cli/pyk.py index 432eaf7194..75a9ecc1ed 100644 --- a/pyk/src/pyk/cli/pyk.py +++ b/pyk/src/pyk/cli/pyk.py @@ -316,8 +316,10 @@ class ProveOptions(LoggingOptions, SpecOptions, SaveDirOptions): kore_rpc_command: str | Iterable[str] | None max_depth: int | None max_iterations: int | None + step_timeout: int | None assume_defined: bool show_kcfg: bool + haskell_logging: bool @staticmethod def default() -> dict[str, Any]: @@ -328,8 +330,10 @@ def default() -> dict[str, Any]: 'kore_rpc_command': None, 'max_depth': None, 'max_iterations': None, + 'step_timeout': None, 'assume_defined': False, 'show_kcfg': False, + 'haskell_logging': False, } @staticmethod @@ -513,6 +517,17 @@ def create_argument_parser() -> ArgumentParser: type=int, help='Maximum number of KCFG explorations to take in attempting to discharge proof.', ) + prove_args.add_argument( + '--step-timeout', + dest='step_timeout', + type=int, + default=None, + help=( + 'Per-step wall-clock budget in whole seconds (floored at 1). When a symbolic-execution step' + ' exceeds it, the step is interrupted, its execution depth is halved, and it is retried;' + ' proving stops once the depth cannot be reduced further. Omit to disable the timeout.' + ), + ) prove_args.add_argument( '--kore-rpc-command', dest='kore_rpc_command', @@ -520,6 +535,17 @@ def create_argument_parser() -> ArgumentParser: default=None, help='Custom command to start RPC server.', ) + prove_args.add_argument( + '--haskell-logging', + dest='haskell_logging', + default=None, + action='store_true', + help=( + "Request the haskell-backend's per-request log bundle on every RPC and write it to" + ' /haskell-logs/.jsonl (one JSON value per line).' + ' Requires --save-directory.' + ), + ) show_args = pyk_args_command.add_parser( 'show', diff --git a/pyk/src/pyk/cterm/symbolic.py b/pyk/src/pyk/cterm/symbolic.py index f7c20cca79..66d178dcb3 100644 --- a/pyk/src/pyk/cterm/symbolic.py +++ b/pyk/src/pyk/cterm/symbolic.py @@ -1,5 +1,6 @@ from __future__ import annotations +import json import logging from contextlib import contextmanager from dataclasses import dataclass @@ -28,7 +29,7 @@ if TYPE_CHECKING: from collections.abc import Iterable, Iterator from pathlib import Path - from typing import Final + from typing import Any, Final from ..kast import KInner from ..kast.outer import KDefinition, KFlatModule @@ -40,6 +41,25 @@ _LOGGER: Final = logging.getLogger(__name__) +#: Canonical default set of haskell-backend log entries to capture per request for fallback +#: diagnosis. Spans both engines: kore entry types (resolved by the backend against its log +#: registry) and booster context tags. Sent verbatim on the ``haskell-logging`` request field; +#: the backend skips any name it does not recognise, so this can evolve without a lockstep backend +#: release. Override per ``CTermSymbolic`` (e.g. downstream semantics needing a different set). +HASKELL_LOGGING_ENTRIES: Final = ( + # Kore engine: equation attempt/application plus the term index that resolves their hashes. + 'DebugAttemptEquation', + 'DebugApplyEquation', + 'DebugTerm', + # Booster: proxy/fallback decisions, detail, aborts, simplification, and rewrite steps. + 'Proxy', + 'Detail', + 'Abort', + 'Simplify', + 'Rewrite', +) + + class NextState(NamedTuple): state: CTerm condition: KInner | None @@ -74,6 +94,8 @@ class CTermSymbolic: _log_succ_rewrites: bool _log_fail_rewrites: bool _booster_only_simplify: bool + _haskell_log_entries: tuple[str, ...] + _haskell_log_dir: Path | None def __init__( self, @@ -83,12 +105,21 @@ def __init__( log_succ_rewrites: bool = True, log_fail_rewrites: bool = False, booster_only_simplify: bool = False, + haskell_log_entries: Iterable[str] = HASKELL_LOGGING_ENTRIES, + haskell_log_dir: Path | None = None, ): self._kore_client = kore_client self._definition = definition self._log_succ_rewrites = log_succ_rewrites self._log_fail_rewrites = log_fail_rewrites self._booster_only_simplify = booster_only_simplify + # *Which* entries to request when logging is on; this populated default is not itself a + # switch — logging stays off until `haskell_log_dir` is set (or a per-call flag enables it). + # Overridable so downstream callers can tailor the set. + self._haskell_log_entries = tuple(haskell_log_entries) + # The switch: when set, every RPC requests the per-request `haskell-logging` bundle and the + # captured entries are written to `/.jsonl` (one JSON value per line). + self._haskell_log_dir = haskell_log_dir def kast_to_kore(self, kinner: KInner) -> Pattern: return kast_to_kore(self._definition, kinner, sort=GENERATED_TOP_CELL) @@ -96,6 +127,36 @@ def kast_to_kore(self, kinner: KInner) -> Pattern: def kore_to_kast(self, pattern: Pattern) -> KInner: return kore_to_kast(self._definition, pattern) + def interrupt(self) -> None: + """Abort a backend request currently in flight on another thread; see `KoreClient.interrupt`.""" + self._kore_client.interrupt() + + def _haskell_logging_request(self, haskell_logging: bool | None) -> tuple[str, ...] | None: + """Resolve the per-call on/off flag to the list of log entries to request. + + An explicit per-call value wins; otherwise logging is on exactly when a ``haskell_log_dir`` + is configured (so the captured bundle has somewhere to land). When on, the configured entry + set is requested; when off — or the set is empty — the wire field is omitted (``None``). + """ + enabled = haskell_logging if haskell_logging is not None else self._haskell_log_dir is not None + return self._haskell_log_entries if enabled and self._haskell_log_entries else None + + def _capture_haskell_log(self, entries: tuple[Any, ...] | None) -> None: + """Write a response's ``haskell-log-entries`` bundle to its own file. + + No-op unless a ``haskell_log_dir`` is configured and ``entries`` is non-empty. Each entry + is one JSON value per line (jsonl), in a file named for the request id (taken from the + backing client) so concurrent proof workers never collide. + """ + if self._haskell_log_dir is None or not entries: + return + request_id = self._kore_client.last_request_id + if request_id is None: + return + self._haskell_log_dir.mkdir(parents=True, exist_ok=True) + log_file = self._haskell_log_dir / f'{request_id}.jsonl' + log_file.write_text('\n'.join(json.dumps(entry) for entry in entries) + '\n') + def execute( self, cterm: CTerm, @@ -104,6 +165,7 @@ def execute( terminal_rules: Iterable[str] | None = None, module_name: str | None = None, booster_only_simplify: bool | None = None, + haskell_logging: bool | None = None, ) -> CTermExecute: _LOGGER.debug(f'Executing: {cterm}') @@ -120,9 +182,11 @@ def execute( booster_only_simplify=( booster_only_simplify if booster_only_simplify is not None else self._booster_only_simplify ), + haskell_logging=self._haskell_logging_request(haskell_logging), ) except SmtSolverError as err: raise self._smt_solver_error(err) from err + self._capture_haskell_log(response.haskell_log_entries) if isinstance(response, AbortedResult): unknown_predicate = response.unknown_predicate.text if response.unknown_predicate else None @@ -151,29 +215,42 @@ def execute( ) def simplify( - self, cterm: CTerm, module_name: str | None = None, booster_only_simplify: bool | None = None + self, + cterm: CTerm, + module_name: str | None = None, + booster_only_simplify: bool | None = None, + haskell_logging: bool | None = None, ) -> tuple[CTerm, tuple[LogEntry, ...]]: _LOGGER.debug(f'Simplifying: {cterm}') kast_simplified, logs = self.kast_simplify( - cterm.kast, module_name=module_name, booster_only_simplify=booster_only_simplify + cterm.kast, + module_name=module_name, + booster_only_simplify=booster_only_simplify, + haskell_logging=haskell_logging, ) return CTerm.from_kast(kast_simplified), logs def kast_simplify( - self, kast: KInner, module_name: str | None = None, booster_only_simplify: bool | None = None + self, + kast: KInner, + module_name: str | None = None, + booster_only_simplify: bool | None = None, + haskell_logging: bool | None = None, ) -> tuple[KInner, tuple[LogEntry, ...]]: _LOGGER.debug(f'Simplifying: {kast}') kore = self.kast_to_kore(kast) try: - kore_simplified, logs = self._kore_client.simplify( + kore_simplified, logs, entries = self._kore_client.simplify( kore, module_name=module_name, booster_only_simplify=( booster_only_simplify if booster_only_simplify is not None else self._booster_only_simplify ), + haskell_logging=self._haskell_logging_request(haskell_logging), ) except SmtSolverError as err: raise self._smt_solver_error(err) from err + self._capture_haskell_log(entries) kast_simplified = self.kore_to_kast(kore_simplified) return kast_simplified, logs @@ -214,6 +291,7 @@ def implies( module_name: str | None = None, assume_defined: bool = False, booster_only_simplify: bool | None = None, + haskell_logging: bool | None = None, ) -> CTermImplies: _LOGGER.debug(f'Checking implication: {antecedent} #Implies {consequent}') _consequent = consequent.kast @@ -238,9 +316,11 @@ def implies( booster_only_simplify=( booster_only_simplify if booster_only_simplify is not None else self._booster_only_simplify ), + haskell_logging=self._haskell_logging_request(haskell_logging), ) except SmtSolverError as err: raise self._smt_solver_error(err) from err + self._capture_haskell_log(result.haskell_log_entries) if not result.valid: if result.substitution is not None: @@ -258,6 +338,7 @@ def implies( module_name=module_name, assume_defined=assume_defined, booster_only_simplify=booster_only_simplify, + haskell_logging=haskell_logging, ) config_match = _config_match.csubst if config_match is None: @@ -339,12 +420,18 @@ def cterm_symbolic( log_succ_rewrites: bool = True, log_fail_rewrites: bool = False, booster_only_simplify: bool = False, + haskell_log_dir: Path | None = None, start_server: bool = True, fallback_on: Iterable[FallbackReason] | None = None, interim_simplification: int | None = None, simplify_each: int | None = None, no_post_exec_simplify: bool = False, ) -> Iterator[CTermSymbolic]: + # `haskell_log_entries` feeds both the legacy server-side `-l` file logging and the new + # per-request capture set. For the latter, fall back to the canonical default when the caller + # leaves it unset, so the per-request bundle works out of the box while still letting clients + # override which entries to request here. + request_log_entries = tuple(haskell_log_entries) or HASKELL_LOGGING_ENTRIES if start_server: # Old way of handling KoreServer, to be removed with kore_server( @@ -372,11 +459,18 @@ def cterm_symbolic( log_succ_rewrites=log_succ_rewrites, log_fail_rewrites=log_fail_rewrites, booster_only_simplify=booster_only_simplify, + haskell_log_entries=request_log_entries, + haskell_log_dir=haskell_log_dir, ) else: if port is None: raise ValueError('Missing port with start_server=False') with KoreClient('localhost', port, bug_report=bug_report, bug_report_id=id) as client: yield CTermSymbolic( - client, definition, log_succ_rewrites=log_succ_rewrites, log_fail_rewrites=log_fail_rewrites + client, + definition, + log_succ_rewrites=log_succ_rewrites, + log_fail_rewrites=log_fail_rewrites, + haskell_log_entries=request_log_entries, + haskell_log_dir=haskell_log_dir, ) diff --git a/pyk/src/pyk/kcfg/explore.py b/pyk/src/pyk/kcfg/explore.py index 5562132e3e..81716fdd4b 100644 --- a/pyk/src/pyk/kcfg/explore.py +++ b/pyk/src/pyk/kcfg/explore.py @@ -59,6 +59,10 @@ def _pretty_printer(self) -> PrettyPrinter: def pretty_print(self, kinner: KInner) -> str: return self._pretty_printer.print(kinner) + def interrupt(self) -> None: + """Abort a backend request currently in flight on another thread; see `KoreClient.interrupt`.""" + self.cterm_symbolic.interrupt() + def _extract_rule_labels(self, _logs: tuple[LogEntry, ...]) -> list[str]: _rule_lines = [] for node_log in _logs: @@ -218,6 +222,7 @@ def extend_cterm( cut_point_rules: Iterable[str] = (), terminal_rules: Iterable[str] = (), module_name: str | None = None, + haskell_logging: bool | None = None, ) -> list[KCFGExtendResult]: custom_step_result = self.kcfg_semantics.custom_step(_cterm, self.cterm_symbolic, node_id) @@ -234,6 +239,7 @@ def extend_cterm( cut_point_rules=cut_point_rules, terminal_rules=terminal_rules, module_name=module_name, + haskell_logging=haskell_logging, ) extend_results: list[KCFGExtendResult] = [] diff --git a/pyk/src/pyk/kore/rpc.py b/pyk/src/pyk/kore/rpc.py index ed101b7ec4..94de640144 100644 --- a/pyk/src/pyk/kore/rpc.py +++ b/pyk/src/pyk/kore/rpc.py @@ -85,6 +85,15 @@ def __exit__(self, *args: Any) -> None: @abstractmethod def close(self) -> None: ... + def interrupt(self) -> None: + """Abort a request that is currently in flight on another thread. + + After `interrupt()` returns, a thread blocked in `request()` must raise promptly and + the transport must remain usable for subsequent requests. The default implementation + does nothing; transports backed by an interruptible connection should override it. + """ + ... + @abstractmethod def _request(self, req: str) -> str: ... @@ -101,6 +110,7 @@ class TransportType(Enum): class SingleSocketTransport(Transport): _host: str _port: int + _timeout: int | None _sock: socket.socket _file: IO[str] @@ -113,6 +123,7 @@ def __init__( ): self._host = host self._port = port + self._timeout = timeout self._sock = self._create_connection(host, port, timeout) self._file = self._sock.makefile('r') @@ -141,6 +152,23 @@ def close(self) -> None: self._file.close() self._sock.close() + def interrupt(self) -> None: + # Shutting down the socket unblocks a thread currently blocked in `readline`, causing + # its read to raise. We then reconnect so the transport stays usable for later requests. + # The old socket is closed; the old file object is left to be reclaimed by the garbage + # collector to avoid racing a `close()` against the unwinding reader thread. + old_sock = self._sock + try: + old_sock.shutdown(socket.SHUT_RDWR) + except OSError: + pass + self._sock = self._create_connection(self._host, self._port, self._timeout) + self._file = self._sock.makefile('r') + try: + old_sock.close() + except OSError: + pass + def _request(self, req: str) -> str: self._sock.sendall(req.encode()) server_addr = self._description() @@ -190,6 +218,7 @@ class JsonRpcClientFacade(ContextManager['JsonRpcClientFacade']): _clients: dict[str, list[JsonRpcClient]] _default_client: JsonRpcClient + _last_request_id: str | None def __init__( self, @@ -204,6 +233,7 @@ def __init__( ): client_cache = {} self._clients = {} + self._last_request_id = None self._default_client = JsonRpcClient( default_host, default_port, @@ -245,15 +275,29 @@ def close(self) -> None: for client in clients: client.close() + @property + def last_request_id(self) -> str | None: + """The JSON-RPC id of the most recent request issued through this facade (``None`` if none yet).""" + return self._last_request_id + + def interrupt(self) -> None: + self._default_client.interrupt() + for clients in self._clients.values(): + for client in clients: + client.interrupt() + def request(self, method: str, **params: Any) -> dict[str, Any]: if method in self._clients: for client in self._clients[method]: response = client.request(method, **params) + self._last_request_id = client.last_request_id if 'error' in response: return response return response else: - return self._default_client.request(method, **params) + response = self._default_client.request(method, **params) + self._last_request_id = self._default_client.last_request_id + return response class JsonRpcClient(ContextManager['JsonRpcClient']): @@ -261,6 +305,7 @@ class JsonRpcClient(ContextManager['JsonRpcClient']): _transport: Transport _req_id: int + _last_request_id: str | None _bug_report: BugReport | None _bug_report_id: str | None @@ -277,9 +322,15 @@ def __init__( ): self._transport = self._create_transport(transport, host=host, port=port, timeout=timeout) self._req_id = 1 + self._last_request_id = None self._bug_report_id = bug_report_id self._bug_report = bug_report + @property + def last_request_id(self) -> str | None: + """The JSON-RPC id of the most recent request issued by this client (``None`` if none yet).""" + return self._last_request_id + @staticmethod def _create_transport(transport: TransportType, *, host: str, port: int, timeout: int | None) -> Transport: match transport: @@ -299,11 +350,15 @@ def __exit__(self, *args: Any) -> None: def close(self) -> None: self._transport.close() + def interrupt(self) -> None: + self._transport.interrupt() + def request(self, method: str, **params: Any) -> dict[str, Any]: label = client_label.get() prefix = label if label is not None else str(id(self)) req_id = f'{prefix}-{self._req_id:03}' self._req_id += 1 + self._last_request_id = req_id payload = { 'jsonrpc': self._JSON_RPC_VERSION, @@ -626,6 +681,16 @@ def to_dict(self) -> dict[str, Any]: return {'tag': 'failure', 'rule-id': self.rule_id, 'reason': self.reason} +def _parse_haskell_log_entries(dct: Mapping[str, Any]) -> tuple[Any, ...] | None: + """Parse the optional per-request ``haskell-log-entries`` bundle (arbitrary JSON values). + + Present only when the request set a non-empty ``haskell-logging`` entry list; absent ⇒ ``None``. + Entries are kept as raw JSON in ``--log-format json`` shape so they feed straight into ``parse_kore_log``. + """ + entries = dct.get('haskell-log-entries') + return tuple(entries) if entries is not None else None + + class ExecuteResult(ABC): _TYPES: Mapping[StopReason, str] = { StopReason.STUCK: 'StuckResult', @@ -645,6 +710,7 @@ class ExecuteResult(ABC): next_states: tuple[State, ...] | None rule: str | None logs: tuple[LogEntry, ...] + haskell_log_entries: tuple[Any, ...] | None @classmethod def from_dict(cls: type[ER], dct: Mapping[str, Any]) -> ER: @@ -669,6 +735,7 @@ class StuckResult(ExecuteResult): state: State depth: int logs: tuple[LogEntry, ...] + haskell_log_entries: tuple[Any, ...] | None = None @classmethod def from_dict(cls: type[StuckResult], dct: Mapping[str, Any]) -> StuckResult: @@ -678,6 +745,7 @@ def from_dict(cls: type[StuckResult], dct: Mapping[str, Any]) -> StuckResult: state=State.from_dict(dct['state']), depth=dct['depth'], logs=logs, + haskell_log_entries=_parse_haskell_log_entries(dct), ) @@ -691,6 +759,7 @@ class DepthBoundResult(ExecuteResult): state: State depth: int logs: tuple[LogEntry, ...] + haskell_log_entries: tuple[Any, ...] | None = None @classmethod def from_dict(cls: type[DepthBoundResult], dct: Mapping[str, Any]) -> DepthBoundResult: @@ -700,6 +769,7 @@ def from_dict(cls: type[DepthBoundResult], dct: Mapping[str, Any]) -> DepthBound state=State.from_dict(dct['state']), depth=dct['depth'], logs=logs, + haskell_log_entries=_parse_haskell_log_entries(dct), ) @@ -713,6 +783,7 @@ class TimeoutResult(ExecuteResult): state: State depth: int logs: tuple[LogEntry, ...] + haskell_log_entries: tuple[Any, ...] | None = None @classmethod def from_dict(cls: type[TimeoutResult], dct: Mapping[str, Any]) -> TimeoutResult: @@ -722,6 +793,7 @@ def from_dict(cls: type[TimeoutResult], dct: Mapping[str, Any]) -> TimeoutResult state=State.from_dict(dct['state']), depth=dct['depth'], logs=logs, + haskell_log_entries=_parse_haskell_log_entries(dct), ) @@ -735,6 +807,7 @@ class BranchingResult(ExecuteResult): depth: int next_states: tuple[State, ...] logs: tuple[LogEntry, ...] + haskell_log_entries: tuple[Any, ...] | None = None @classmethod def from_dict(cls: type[BranchingResult], dct: Mapping[str, Any]) -> BranchingResult: @@ -745,6 +818,7 @@ def from_dict(cls: type[BranchingResult], dct: Mapping[str, Any]) -> BranchingRe depth=dct['depth'], next_states=tuple(State.from_dict(next_state) for next_state in dct['next-states']), logs=logs, + haskell_log_entries=_parse_haskell_log_entries(dct), ) @@ -758,6 +832,7 @@ class CutPointResult(ExecuteResult): next_states: tuple[State, ...] rule: str logs: tuple[LogEntry, ...] + haskell_log_entries: tuple[Any, ...] | None = None @classmethod def from_dict(cls: type[CutPointResult], dct: Mapping[str, Any]) -> CutPointResult: @@ -769,6 +844,7 @@ def from_dict(cls: type[CutPointResult], dct: Mapping[str, Any]) -> CutPointResu next_states=tuple(State.from_dict(next_state) for next_state in dct['next-states']), rule=dct['rule'], logs=logs, + haskell_log_entries=_parse_haskell_log_entries(dct), ) @@ -782,12 +858,19 @@ class TerminalResult(ExecuteResult): depth: int rule: str logs: tuple[LogEntry, ...] + haskell_log_entries: tuple[Any, ...] | None = None @classmethod def from_dict(cls: type[TerminalResult], dct: Mapping[str, Any]) -> TerminalResult: cls._check_reason(dct) logs = tuple(LogEntry.from_dict(l) for l in dct['logs']) if 'logs' in dct else () - return TerminalResult(state=State.from_dict(dct['state']), depth=dct['depth'], rule=dct['rule'], logs=logs) + return TerminalResult( + state=State.from_dict(dct['state']), + depth=dct['depth'], + rule=dct['rule'], + logs=logs, + haskell_log_entries=_parse_haskell_log_entries(dct), + ) @final @@ -800,6 +883,7 @@ class VacuousResult(ExecuteResult): state: State depth: int logs: tuple[LogEntry, ...] + haskell_log_entries: tuple[Any, ...] | None = None @classmethod def from_dict(cls: type[VacuousResult], dct: Mapping[str, Any]) -> VacuousResult: @@ -809,6 +893,7 @@ def from_dict(cls: type[VacuousResult], dct: Mapping[str, Any]) -> VacuousResult state=State.from_dict(dct['state']), depth=dct['depth'], logs=logs, + haskell_log_entries=_parse_haskell_log_entries(dct), ) @@ -823,6 +908,7 @@ class AbortedResult(ExecuteResult): depth: int unknown_predicate: Pattern | None logs: tuple[LogEntry, ...] + haskell_log_entries: tuple[Any, ...] | None = None @classmethod def from_dict(cls: type[AbortedResult], dct: Mapping[str, Any]) -> AbortedResult: @@ -833,6 +919,7 @@ def from_dict(cls: type[AbortedResult], dct: Mapping[str, Any]) -> AbortedResult depth=dct['depth'], unknown_predicate=kore_term(dct['unknown-predicate']) if dct.get('unknown-predicate') else None, logs=logs, + haskell_log_entries=_parse_haskell_log_entries(dct), ) @@ -844,6 +931,7 @@ class ImpliesResult: substitution: Pattern | None predicate: Pattern | None logs: tuple[LogEntry, ...] + haskell_log_entries: tuple[Any, ...] | None = None @staticmethod def from_dict(dct: Mapping[str, Any]) -> ImpliesResult: @@ -856,39 +944,61 @@ def from_dict(dct: Mapping[str, Any]) -> ImpliesResult: substitution=kore_term(substitution) if substitution is not None else None, predicate=kore_term(predicate) if predicate is not None else None, logs=logs, + haskell_log_entries=_parse_haskell_log_entries(dct), ) +class SimplifyResult(NamedTuple): + """Result of a ``simplify`` call. + + A ``NamedTuple`` (not a bare tuple) so the optional ``haskell_log_entries`` bundle can be + carried alongside the simplified ``state`` and ``logs`` without losing positional ergonomics. + """ + + state: Pattern + logs: tuple[LogEntry, ...] + haskell_log_entries: tuple[Any, ...] | None + + class GetModelResult(ABC): # noqa: B024 + haskell_log_entries: tuple[Any, ...] | None + @staticmethod def from_dict(dct: Mapping[str, Any]) -> GetModelResult: status = dct['satisfiable'] + entries = _parse_haskell_log_entries(dct) match status: case 'Unknown': - return UnknownResult() + return UnknownResult(haskell_log_entries=entries) case 'Unsat': - return UnsatResult() + return UnsatResult(haskell_log_entries=entries) case 'Sat': substitution = dct.get('substitution') - return SatResult(model=kore_term(substitution) if substitution else None) + return SatResult( + model=kore_term(substitution) if substitution else None, + haskell_log_entries=entries, + ) case _: raise ValueError(f'Unknown status: {status}') @final @dataclass(frozen=True) -class UnknownResult(GetModelResult): ... +class UnknownResult(GetModelResult): + haskell_log_entries: tuple[Any, ...] | None = None @final @dataclass(frozen=True) -class UnsatResult(GetModelResult): ... +class UnsatResult(GetModelResult): + haskell_log_entries: tuple[Any, ...] | None = None @final @dataclass(frozen=True) class SatResult(GetModelResult): model: Pattern | None + haskell_log_entries: tuple[Any, ...] | None = None class KoreClient(ContextManager['KoreClient']): @@ -930,6 +1040,26 @@ def __exit__(self, *args: Any) -> None: def close(self) -> None: self._client.close() + @property + def last_request_id(self) -> str | None: + """The JSON-RPC id of the most recent request issued by this client. + + ``None`` before any request has been made. Snapshot it immediately after a call + (e.g. ``execute``/``implies``/``simplify``) to key per-request data (logs, handoff + metadata) to that exact request. Each proof worker drives its own ``KoreClient`` + (see ``_ProverPool``), so this needs no cross-thread synchronization. + """ + return self._client.last_request_id + + def interrupt(self) -> None: + """Abort an `execute`/`simplify`/… request currently in flight on another thread. + + After this returns the interrupted call raises and the client stays usable. Only + effective for the single-socket transport; a no-op for transports that cannot abort + an in-flight request. + """ + self._client.interrupt() + def _request(self, method: str, **params: Any) -> dict[str, Any]: try: return self._client.request(method, **params) @@ -978,6 +1108,7 @@ def execute( log_successful_rewrites: bool | None = None, log_failed_rewrites: bool | None = None, booster_only_simplify: bool | None = None, + haskell_logging: Iterable[str] | None = None, ) -> ExecuteResult: params = filter_none( { @@ -992,6 +1123,7 @@ def execute( 'log-successful-rewrites': log_successful_rewrites, 'log-failed-rewrites': log_failed_rewrites, 'booster-only': booster_only_simplify, + 'haskell-logging': list(haskell_logging) if haskell_logging is not None else None, } ) @@ -1006,6 +1138,7 @@ def implies( module_name: str | None = None, assume_defined: bool = False, booster_only_simplify: bool | None = None, + haskell_logging: Iterable[str] | None = None, ) -> ImpliesResult: params = filter_none( { @@ -1014,6 +1147,7 @@ def implies( 'module': module_name, 'assume-defined': assume_defined, 'booster-only': booster_only_simplify, + 'haskell-logging': list(haskell_logging) if haskell_logging is not None else None, } ) @@ -1026,35 +1160,50 @@ def simplify( *, module_name: str | None = None, booster_only_simplify: bool | None = None, - ) -> tuple[Pattern, tuple[LogEntry, ...]]: + haskell_logging: Iterable[str] | None = None, + ) -> SimplifyResult: params = filter_none( { 'state': self._state(pattern), 'module': module_name, 'booster-only': booster_only_simplify, + 'haskell-logging': list(haskell_logging) if haskell_logging is not None else None, } ) result = self._request('simplify', **params) logs = tuple(LogEntry.from_dict(l) for l in result['logs']) if 'logs' in result else () - return kore_term(result['state']), logs + return SimplifyResult(kore_term(result['state']), logs, _parse_haskell_log_entries(result)) - def get_model(self, pattern: Pattern, module_name: str | None = None) -> GetModelResult: + def get_model( + self, + pattern: Pattern, + module_name: str | None = None, + haskell_logging: Iterable[str] | None = None, + ) -> GetModelResult: params = filter_none( { 'state': self._state(pattern), 'module': module_name, + 'haskell-logging': list(haskell_logging) if haskell_logging is not None else None, } ) result = self._request('get-model', **params) return GetModelResult.from_dict(result) - def add_module(self, module: Module, *, name_as_id: bool | None = None) -> str: + def add_module( + self, + module: Module, + *, + name_as_id: bool | None = None, + haskell_logging: Iterable[str] | None = None, + ) -> str: params = filter_none( { 'module': module.text, 'name-as-id': name_as_id, + 'haskell-logging': list(haskell_logging) if haskell_logging is not None else None, } ) result = self._request('add-module', **params) @@ -1245,19 +1394,20 @@ def _extra_args(self) -> list[str]: if self._smt_tactic is not None: smt_server_args += ['--smt-tactic', self._smt_tactic] - if self._log_axioms_file is not None: - haskell_log_args = [ - '--log', - str(self._log_axioms_file), - '--log-format', - self._haskell_log_format.value, - '--log-entries', - ','.join(self._haskell_log_entries), - ] - else: - haskell_log_args = [] - - return smt_server_args + haskell_log_args + return smt_server_args + self._haskell_log_cli_args() + + def _haskell_log_cli_args(self) -> list[str]: + # kore-rpc form: `--log FILE`, `--log-entries A,B,C`. Booster overrides for `--log-file FILE` and repeated `-l`. + if self._log_axioms_file is None: + return [] + return [ + '--log', + str(self._log_axioms_file), + '--log-format', + self._haskell_log_format.value, + '--log-entries', + ','.join(self._haskell_log_entries), + ] def _populate_bug_report(self, bug_report: BugReport) -> None: prog_name = self._command[0] @@ -1375,6 +1525,21 @@ def _extra_args(self) -> list[str]: res += [arg for glob in self._not_log_context for arg in ['--not-log-context', glob]] return res + def _haskell_log_cli_args(self) -> list[str]: + # kore-rpc-booster diverged from kore-rpc: `--log-file FILE` (not `--log FILE`), + # and repeated `-l ENTRY` (not `--log-entries A,B,C`). + if self._log_axioms_file is None: + return [] + args = [ + '--log-file', + str(self._log_axioms_file), + '--log-format', + self._haskell_log_format.value, + ] + for entry in self._haskell_log_entries: + args += ['-l', entry] + return args + def _populate_bug_report(self, bug_report: BugReport) -> None: super()._populate_bug_report(bug_report) bug_report.add_file(self._llvm_definition, Path('llvm_definition/definition.kore')) diff --git a/pyk/src/pyk/proof/proof.py b/pyk/src/pyk/proof/proof.py index 0d1eef04d2..3edc8d45d3 100644 --- a/pyk/src/pyk/proof/proof.py +++ b/pyk/src/pyk/proof/proof.py @@ -3,7 +3,9 @@ import json import logging from abc import ABC, abstractmethod -from concurrent.futures import ThreadPoolExecutor, wait +from concurrent.futures import ThreadPoolExecutor +from concurrent.futures import TimeoutError as FuturesTimeoutError +from concurrent.futures import wait from dataclasses import dataclass from enum import Enum from itertools import chain @@ -499,6 +501,33 @@ def init_proof(self, proof: P) -> None: """ ... + #: Per-step wall-clock budget in whole seconds (minimum 1). When set, `advance_proof` runs each + #: step under this budget and, on timeout, interrupts it, calls `shrink_step`, and retries. + #: `None` (the default) disables the policy, so steps run synchronously with no time limit. A + #: prover that can do less work per step (e.g. `APRProver`, by lowering its execution depth) + #: should pair this with `shrink_step`. + step_timeout: int | None = None + + def shrink_step(self) -> bool: + """Reduce the amount of work a single `step_proof` does, after a step timed out. + + Return `True` if the step was made smaller (so it is worth retrying), or `False` if the + step is already at its minimum size (so `advance_proof` should stop). The default is a + no-op that returns `False`; see `step_timeout`. + """ + return False + + def interrupt(self) -> None: + """Abort a `step_proof` call currently running on another thread, as quickly as possible. + + Used by the timeout-and-shrink policy in `advance_proof` to abandon a step that has + exhausted its `step_timeout` budget. After this returns, a thread blocked in `step_proof` + must raise promptly and the prover must remain usable for subsequent steps. The default + implementation does nothing; provers backed by an interruptible resource (e.g. a Kore RPC + connection) should override it. + """ + ... + def advance_proof( self, proof: P, @@ -509,7 +538,8 @@ def advance_proof( ) -> None: """Advance a proof. - Performs loop `Proof.get_steps()` -> `Prover.step_proof()` -> `Proof.commit()`. + Performs loop `Proof.get_steps()` -> `Prover.step_proof()` (within `step_timeout`, else + `interrupt` + `shrink_step` and retry, or stop if it cannot shrink) -> `Proof.commit()`. Args: proof: proof to advance. @@ -522,25 +552,59 @@ def advance_proof( iterations = 0 _LOGGER.info(f'Initializing proof: {proof.id}') self.init_proof(proof) - while True: - steps = list(proof.get_steps()) - _LOGGER.info(f'Found {len(steps)} next steps for proof: {proof.id}') - if len(steps) == 0: - break - for step in steps: - if fail_fast and proof.failed: - _LOGGER.warning(f'Terminating proof early because fail_fast is set: {proof.id}') - proof.failure_info = self.failure_info(proof) - return - if max_iterations is not None and max_iterations <= iterations: - return - iterations += 1 - results = self.step_proof(step) - for result in results: - proof.commit(result) - if iterations % maintenance_rate == 0: - proof.write_proof_data() - callback(proof) + + timed = self.step_timeout is not None + executor = ThreadPoolExecutor(max_workers=1) if timed else None + try: + while True: + steps = list(proof.get_steps()) + _LOGGER.info(f'Found {len(steps)} next steps for proof: {proof.id}') + if len(steps) == 0: + break + shrank_step = False + for step in steps: + if fail_fast and proof.failed: + _LOGGER.warning(f'Terminating proof early because fail_fast is set: {proof.id}') + proof.failure_info = self.failure_info(proof) + return + if max_iterations is not None and max_iterations <= iterations: + return + if timed: + assert executor is not None + budget = self.step_timeout + assert budget is not None + future = executor.submit(self.step_proof, step) + try: + results = future.result(timeout=budget) + except FuturesTimeoutError: + # The step exhausted its budget: interrupt it, ask the prover to do less + # work per step, and re-fetch steps so the same node is retried smaller. + self.interrupt() + wait([future]) + if not self.shrink_step(): + _LOGGER.warning( + f'Proof {proof.id}: step exhausted {budget}s budget and cannot be ' + f'shrunk further; stopping.' + ) + return + _LOGGER.warning( + f'Proof {proof.id}: step exhausted {budget}s budget; shrinking and retrying.' + ) + shrank_step = True + break + else: + results = self.step_proof(step) + iterations += 1 + for result in results: + proof.commit(result) + if iterations % maintenance_rate == 0: + proof.write_proof_data() + callback(proof) + if shrank_step: + continue + finally: + if executor is not None: + executor.shutdown(wait=False) if proof.failed: proof.failure_info = self.failure_info(proof) diff --git a/pyk/src/pyk/proof/prove_rpc.py b/pyk/src/pyk/proof/prove_rpc.py index df01ad30b4..9b852daaa6 100644 --- a/pyk/src/pyk/proof/prove_rpc.py +++ b/pyk/src/pyk/proof/prove_rpc.py @@ -52,6 +52,7 @@ def prove_rpc(self, options: ProveOptions) -> list[Proof]: max_depth=options.max_depth, save_directory=options.save_directory, max_iterations=options.max_iterations, + step_timeout=options.step_timeout, ) for claim in all_claims ] @@ -63,6 +64,7 @@ def _prove_claim_rpc( max_depth: int | None = None, save_directory: Path | None = None, max_iterations: int | None = None, + step_timeout: int | None = None, ) -> Proof: definition = self._kprove.definition @@ -90,7 +92,12 @@ def _prove_claim_rpc( prover = ImpliesProver(proof, kcfg_explore, assume_defined=assume_defined) else: assert type(proof) is APRProof - prover = APRProver(kcfg_explore, execute_depth=max_depth, assume_defined=assume_defined) + prover = APRProver( + kcfg_explore, + execute_depth=max_depth, + assume_defined=assume_defined, + step_timeout=step_timeout, + ) prover.advance_proof(proof, max_iterations=max_iterations) # type: ignore [arg-type] if proof.passed: diff --git a/pyk/src/pyk/proof/reachability.py b/pyk/src/pyk/proof/reachability.py index 0b4a66d2b3..b7c01d913d 100644 --- a/pyk/src/pyk/proof/reachability.py +++ b/pyk/src/pyk/proof/reachability.py @@ -725,6 +725,7 @@ class APRProver(Prover[APRProof, APRProofStep, APRProofResult]): kcfg_explore: KCFGExplore extra_module: KFlatModule | None optimize_kcfg: bool + step_timeout: int | None def __init__( self, @@ -738,6 +739,7 @@ def __init__( assume_defined: bool = False, extra_module: KFlatModule | None = None, optimize_kcfg: bool = False, + step_timeout: int | None = None, ) -> None: self.kcfg_explore = kcfg_explore @@ -751,10 +753,23 @@ def __init__( self.assume_defined = assume_defined self.extra_module = extra_module self.optimize_kcfg = optimize_kcfg + # Whole seconds, floored at 1; None disables the per-step timeout/shrink policy entirely. + self.step_timeout = max(1, step_timeout) if step_timeout is not None else None def close(self) -> None: self.kcfg_explore.cterm_symbolic._kore_client.close() + def shrink_step(self) -> bool: + # On step timeout, halve the execution depth (floor 1) so the next attempt does less work + # per `extend_cterm`. Returns False once `execute_depth` is unset or already at the minimum. + if self.execute_depth is None or self.execute_depth <= 1: + return False + self.execute_depth = max(1, self.execute_depth // 2) + return True + + def interrupt(self) -> None: + self.kcfg_explore.interrupt() + def init_proof(self, proof: APRProof) -> None: # Stamp proof.id on every subsequent kore-RPC request from this thread so # booster's `{request: ...}` log lines self-identify the originating diff --git a/pyk/src/tests/integration/kore/test_kore_client.py b/pyk/src/tests/integration/kore/test_kore_client.py index 528bc4cd79..547f875606 100644 --- a/pyk/src/tests/integration/kore/test_kore_client.py +++ b/pyk/src/tests/integration/kore/test_kore_client.py @@ -391,7 +391,7 @@ def test_simplify( expected: Pattern, ) -> None: # When - actual, _logs = kore_client.simplify(pattern) + actual, _logs, _entries = kore_client.simplify(pattern) # Then assert actual == expected diff --git a/pyk/src/tests/integration/test_division_hooks.py b/pyk/src/tests/integration/test_division_hooks.py index d64f494298..6a28036b55 100644 --- a/pyk/src/tests/integration/test_division_hooks.py +++ b/pyk/src/tests/integration/test_division_hooks.py @@ -137,7 +137,7 @@ def test_simplify(self, kore_client: KoreClient, op: str, a: int, b: int, c: int # Given pattern = div_pattern(op, a, b) - expected = (int_dv(c), ()) + expected = (int_dv(c), (), None) # When actual = kore_client.simplify(pattern) diff --git a/pyk/src/tests/unit/kore/test_client.py b/pyk/src/tests/unit/kore/test_client.py index 8842da2550..e93e4558c2 100644 --- a/pyk/src/tests/unit/kore/test_client.py +++ b/pyk/src/tests/unit/kore/test_client.py @@ -228,7 +228,7 @@ def test_simplify( rpc_client.assume_response(response) # When - actual, _logs = kore_client.simplify(pattern) + actual, _logs, _entries = kore_client.simplify(pattern) # Then rpc_client.assert_request('simplify', **params) diff --git a/pyk/src/tests/unit/test_advance_proof.py b/pyk/src/tests/unit/test_advance_proof.py new file mode 100644 index 0000000000..fe955f78e9 --- /dev/null +++ b/pyk/src/tests/unit/test_advance_proof.py @@ -0,0 +1,160 @@ +from __future__ import annotations + +from threading import Event +from typing import TYPE_CHECKING + +from pyk.proof.proof import Proof, ProofStatus, Prover + +if TYPE_CHECKING: + from collections.abc import Mapping + from pathlib import Path + from typing import Any + + +class _StepInterrupted(Exception): + """Raised inside `step_proof` when the prover is interrupted, mimicking a backend abort.""" + + +class CountingProof(Proof[int, int]): + """Minimal proof that needs `target` committed steps to pass.""" + + target: int + committed: int + + def __init__(self, id: str, target: int) -> None: + super().__init__(id) + self.target = target + self.committed = 0 + + def commit(self, result: int) -> None: + self.committed += result + + @property + def own_status(self) -> ProofStatus: + return ProofStatus.PASSED if self.committed >= self.target else ProofStatus.PENDING + + @property + def can_progress(self) -> bool: + return self.committed < self.target + + @classmethod + def from_dict(cls: type[CountingProof], dct: Mapping[str, Any], proof_dir: Path | None = None) -> CountingProof: + raise NotImplementedError + + def write_proof_data(self) -> None: ... + + def get_steps(self) -> list[int]: + return [self.committed] if self.can_progress else [] + + +class CountingProver(Prover[CountingProof, int, int]): + """Prover whose `step_proof` is "slow" (blocks for up to `slow_step_secs`) while `depth` exceeds `quick_at_depth`. + + Mirrors `APRProver`: a fixed `step_timeout` budgets each step, and `shrink_step` halves the depth. + A slow step that is interrupted before its budget elapses raises (mimicking a backend abort); a slow + step that is never interrupted finishes its work on its own. Tracks the number of interruptions so + tests can assert how many times a step was shrunk. + """ + + depth: int + quick_at_depth: int + step_timeout: int | None + slow_step_secs: float + interrupt_count: int + _interrupt_event: Event + + def __init__( + self, depth: int, quick_at_depth: int, step_timeout: int | None = 1, slow_step_secs: float = 10.0 + ) -> None: + self.depth = depth + self.quick_at_depth = quick_at_depth + self.step_timeout = step_timeout + self.slow_step_secs = slow_step_secs + self.interrupt_count = 0 + self._interrupt_event = Event() + + def close(self) -> None: ... + + def failure_info(self, proof: CountingProof) -> Any: + return None + + def init_proof(self, proof: CountingProof) -> None: ... + + def shrink_step(self) -> bool: + if self.depth <= 1: + return False + self.depth = max(1, self.depth // 2) + return True + + def interrupt(self) -> None: + self.interrupt_count += 1 + self._interrupt_event.set() + + def step_proof(self, step: int) -> list[int]: + self._interrupt_event.clear() + if self.depth > self.quick_at_depth: + # A "slow" step: block for up to `slow_step_secs`. If `advance_proof` interrupts us first + # (because the step budget elapsed) abort like a real backend; otherwise the step finishes + # its work on its own and commits normally. + if self._interrupt_event.wait(timeout=self.slow_step_secs): + raise _StepInterrupted() + return [1] + + +def test_advance_proof_shrinks_until_progress() -> None: + # Given: depth 4 stalls, but a step completes once depth drops to <= 2. + proof = CountingProof('counting', target=1) + prover = CountingProver(depth=4, quick_at_depth=2) + + # When + prover.advance_proof(proof) + + # Then: one timeout shrinks 4 -> 2, then a step commits and the proof passes. + assert proof.status == ProofStatus.PASSED + assert prover.depth == 2 + assert prover.interrupt_count == 1 + + +def test_advance_proof_stops_when_cannot_shrink_further() -> None: + # Given: every step stalls regardless of depth. + proof = CountingProof('counting', target=1) + prover = CountingProver(depth=2, quick_at_depth=0) + + # When + prover.advance_proof(proof) + + # Then: depth shrinks 2 -> 1, then stops at the floor; the proof stays pending. + assert proof.status == ProofStatus.PENDING + assert proof.committed == 0 + assert prover.depth == 1 + assert prover.interrupt_count == 2 + + +def test_advance_proof_no_shrink_when_steps_are_fast() -> None: + # Given: step_timeout set but steps always complete in time. + proof = CountingProof('counting', target=3) + prover = CountingProver(depth=2, quick_at_depth=2) + + # When + prover.advance_proof(proof) + + # Then: no interruptions, depth untouched, proof passes. + assert proof.status == ProofStatus.PASSED + assert prover.depth == 2 + assert prover.interrupt_count == 0 + + +def test_advance_proof_without_step_timeout_is_unaffected() -> None: + # Given: step_timeout is None -> classic in-loop behavior, no watchdog thread. Each step is "slow" + # (depth 8 > quick_at_depth 4), but without a budget nothing interrupts it, so the step runs to + # completion synchronously instead of being aborted and shrunk. + proof = CountingProof('counting', target=2) + prover = CountingProver(depth=8, quick_at_depth=4, step_timeout=None, slow_step_secs=0.05) + + # When + prover.advance_proof(proof) + + # Then: both slow steps complete on their own; nothing is interrupted or shrunk. + assert proof.status == ProofStatus.PASSED + assert prover.depth == 8 + assert prover.interrupt_count == 0