From 5cbb488a96fcf8f4d91c2369903664a73f815805 Mon Sep 17 00:00:00 2001 From: rv-jenkins Date: Wed, 3 Jun 2026 09:38:52 -0600 Subject: [PATCH 01/10] Update dependency: deps/haskell-backend_release (#4926) Co-authored-by: devops --- deps/haskell-backend_release | 2 +- flake.lock | 14 +++++++------- flake.nix | 2 +- haskell-backend/src/main/native/haskell-backend | 2 +- 4 files changed, 10 insertions(+), 10 deletions(-) diff --git a/deps/haskell-backend_release b/deps/haskell-backend_release index 8fe50701c1..07102b5515 100644 --- a/deps/haskell-backend_release +++ b/deps/haskell-backend_release @@ -1 +1 @@ -v0.1.147 +v0.1.149 diff --git a/flake.lock b/flake.lock index ab9f9a8cc4..46c22bc8b5 100644 --- a/flake.lock +++ b/flake.lock @@ -64,16 +64,16 @@ "z3": "z3" }, "locked": { - "lastModified": 1779860189, - "narHash": "sha256-hCyz2V6ZDAqenUhZD7yPLk+EyiMauJghxMuOO1HHhWc=", + "lastModified": 1780406844, + "narHash": "sha256-6T8TAiAAjI2wHzvPWmTdRZW4hR8lf3C4ChqIJQZgL00=", "owner": "runtimeverification", "repo": "haskell-backend", - "rev": "786db62a39ac444e04481719339a60ae240e85cd", + "rev": "ce904db16331b0cd07e1a9f06d34224aa461d02d", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v0.1.147", + "ref": "v0.1.149", "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..869b4b368c 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.149"; 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..ce904db163 160000 --- a/haskell-backend/src/main/native/haskell-backend +++ b/haskell-backend/src/main/native/haskell-backend @@ -1 +1 @@ -Subproject commit 786db62a39ac444e04481719339a60ae240e85cd +Subproject commit ce904db16331b0cd07e1a9f06d34224aa461d02d From 6e87368a81672bc5fb7b3f2fbafc68426f6d5346 Mon Sep 17 00:00:00 2001 From: devops Date: Wed, 3 Jun 2026 15:39:17 +0000 Subject: [PATCH 02/10] Set Version: 7.1.330 --- install-k | 2 +- package/debian/kframework/changelog | 2 +- package/version | 2 +- pyk/docs/conf.py | 4 ++-- pyk/pyproject.toml | 2 +- 5 files changed, 6 insertions(+), 6 deletions(-) diff --git a/install-k b/install-k index 6914b47e17..8a008eeece 100755 --- a/install-k +++ b/install-k @@ -1,6 +1,6 @@ #!/bin/sh -e -K_VERSION=7.1.329 +K_VERSION=7.1.330 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..ef65973a0d 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.330) unstable; urgency=medium * Initial Release. diff --git a/package/version b/package/version index 093b104b6f..30c25a124a 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -7.1.329 +7.1.330 diff --git a/pyk/docs/conf.py b/pyk/docs/conf.py index 88e64d2fd9..dc2fffb703 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.330' +release = '7.1.330' # -- 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..0d6fd30900 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.330" description = "" readme = "README.md" requires-python = ">=3.10" From 195ce2de5f98de708dcdbcd3192d8bc268810333 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Thu, 4 Jun 2026 09:01:44 -0600 Subject: [PATCH 03/10] Optimize Nix release workflow (#4927) The k-framework-binary (private, via kup) and k-framework (public, via cachix) publishes built the same three derivations on separate runners, recompiling K four times (2 jobs x 2 OS) for work that needs two builds. Fold them into one matrix job: the first publish populates the local Nix store so the second's nix build is an instant store hit. The two publishes stay independent (continue-on-error + if: always()) so a flaky upload to one cache neither blocks nor masks the other, and a final guard re-fails the job if either push failed, preserving the release gate the two separate jobs provided. Drop the removed cachix-release-dependencies from the release job's needs. --------- Co-authored-by: Claude Opus 4.8 --- .github/workflows/release.yml | 58 +++++++++++++---------------------- 1 file changed, 22 insertions(+), 36 deletions(-) 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 From 5d786ca3578881344001874d04bd4957756a32b0 Mon Sep 17 00:00:00 2001 From: devops Date: Thu, 4 Jun 2026 15:02:05 +0000 Subject: [PATCH 04/10] Set Version: 7.1.331 --- install-k | 2 +- package/debian/kframework/changelog | 2 +- package/version | 2 +- pyk/docs/conf.py | 4 ++-- pyk/pyproject.toml | 2 +- 5 files changed, 6 insertions(+), 6 deletions(-) diff --git a/install-k b/install-k index 8a008eeece..1a7fb52ad8 100755 --- a/install-k +++ b/install-k @@ -1,6 +1,6 @@ #!/bin/sh -e -K_VERSION=7.1.330 +K_VERSION=7.1.331 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 ef65973a0d..9256d37ba9 100644 --- a/package/debian/kframework/changelog +++ b/package/debian/kframework/changelog @@ -1,4 +1,4 @@ -kframework (7.1.330) unstable; urgency=medium +kframework (7.1.331) unstable; urgency=medium * Initial Release. diff --git a/package/version b/package/version index 30c25a124a..66e58fce07 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -7.1.330 +7.1.331 diff --git a/pyk/docs/conf.py b/pyk/docs/conf.py index dc2fffb703..b92e0ca13f 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.330' -release = '7.1.330' +version = '7.1.331' +release = '7.1.331' # -- 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 0d6fd30900..9603cc9020 100644 --- a/pyk/pyproject.toml +++ b/pyk/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "hatchling.build" [project] name = "kframework" -version = "7.1.330" +version = "7.1.331" description = "" readme = "README.md" requires-python = ">=3.10" From fb2fde270681dd129f180019295a6dbec4bd3195 Mon Sep 17 00:00:00 2001 From: rv-jenkins Date: Thu, 4 Jun 2026 13:29:11 -0600 Subject: [PATCH 05/10] Update dependency: deps/haskell-backend_release (#4929) Co-authored-by: devops --- deps/haskell-backend_release | 2 +- flake.lock | 8 ++++---- flake.nix | 2 +- haskell-backend/src/main/native/haskell-backend | 2 +- 4 files changed, 7 insertions(+), 7 deletions(-) diff --git a/deps/haskell-backend_release b/deps/haskell-backend_release index 07102b5515..a402c50ee2 100644 --- a/deps/haskell-backend_release +++ b/deps/haskell-backend_release @@ -1 +1 @@ -v0.1.149 +v0.1.150 diff --git a/flake.lock b/flake.lock index 46c22bc8b5..9dc83c895c 100644 --- a/flake.lock +++ b/flake.lock @@ -64,16 +64,16 @@ "z3": "z3" }, "locked": { - "lastModified": 1780406844, - "narHash": "sha256-6T8TAiAAjI2wHzvPWmTdRZW4hR8lf3C4ChqIJQZgL00=", + "lastModified": 1780590347, + "narHash": "sha256-iYTKRQzsC56EfHNuDO/O9MbMFmNV9c2CM4NwOXSeSc4=", "owner": "runtimeverification", "repo": "haskell-backend", - "rev": "ce904db16331b0cd07e1a9f06d34224aa461d02d", + "rev": "515eccf4a8ebbb0fe8ff807d15a96ce096ce2670", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v0.1.149", + "ref": "v0.1.150", "repo": "haskell-backend", "type": "github" } diff --git a/flake.nix b/flake.nix index 869b4b368c..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.149"; + 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 ce904db163..515eccf4a8 160000 --- a/haskell-backend/src/main/native/haskell-backend +++ b/haskell-backend/src/main/native/haskell-backend @@ -1 +1 @@ -Subproject commit ce904db16331b0cd07e1a9f06d34224aa461d02d +Subproject commit 515eccf4a8ebbb0fe8ff807d15a96ce096ce2670 From 8d42b843403199a317cc157421d8da5df9c7bdc6 Mon Sep 17 00:00:00 2001 From: devops Date: Thu, 4 Jun 2026 19:29:36 +0000 Subject: [PATCH 06/10] Set Version: 7.1.332 --- install-k | 2 +- package/debian/kframework/changelog | 2 +- package/version | 2 +- pyk/docs/conf.py | 4 ++-- pyk/pyproject.toml | 2 +- 5 files changed, 6 insertions(+), 6 deletions(-) diff --git a/install-k b/install-k index 1a7fb52ad8..9190e82709 100755 --- a/install-k +++ b/install-k @@ -1,6 +1,6 @@ #!/bin/sh -e -K_VERSION=7.1.331 +K_VERSION=7.1.332 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 9256d37ba9..0a822916bd 100644 --- a/package/debian/kframework/changelog +++ b/package/debian/kframework/changelog @@ -1,4 +1,4 @@ -kframework (7.1.331) unstable; urgency=medium +kframework (7.1.332) unstable; urgency=medium * Initial Release. diff --git a/package/version b/package/version index 66e58fce07..5dcfc81c62 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -7.1.331 +7.1.332 diff --git a/pyk/docs/conf.py b/pyk/docs/conf.py index b92e0ca13f..f1f758faf0 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.331' -release = '7.1.331' +version = '7.1.332' +release = '7.1.332' # -- 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 9603cc9020..885135d916 100644 --- a/pyk/pyproject.toml +++ b/pyk/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "hatchling.build" [project] name = "kframework" -version = "7.1.331" +version = "7.1.332" description = "" readme = "README.md" requires-python = ">=3.10" From 32499b648706aee42fbb715a458394e5d452821b Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Fri, 5 Jun 2026 10:13:14 -0600 Subject: [PATCH 07/10] pyk: per-request haskell-backend RPC logging (#4928) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit ~Blocked on: https://github.com/runtimeverification/haskell-backend/pull/4151~ ~Blocked on: https://github.com/runtimeverification/k/pull/4929~ Lets pyk request the haskell-backend's per-request log bundle and write it to disk, so downstream can diagnose fallback behaviour per RPC. The request carries the list of log entries to capture and the response returns them in-band; pyk owns the default set and writes each request's bundle to its own file. This pairs with the haskell-backend per-request-rpc branch, which adds the haskell-logging request field ([String]) and the haskell-log-entries response field to the five JSON-RPC endpoints and captures the named entries independently of the server's -l/--log-file configuration. Changes: - BoosterServer now emits the booster-form haskell-log CLI (--log-file FILE, repeated -l ENTRY) via a new overridable _haskell_log_cli_args hook; it previously sent the kore-rpc form (--log, --log-entries A,B), which made kore-rpc-booster exit on a usage error before opening its RPC port. - KoreClient.{execute,implies,simplify,get_model,add_module} take haskell_logging: Iterable[str] | None — the entries to capture for that request — and send it as the haskell-logging wire field (omitted when None); the optional haskell-log-entries bundle is parsed onto every result type, and simplify returns a SimplifyResult (state, logs, haskell_log_entries). - KoreClient.last_request_id exposes the JSON-RPC id of the most recent request issued by the client, used to name each per-request log file. - CTermSymbolic owns the canonical default entry set (HASKELL_LOGGING_ENTRIES), overridable per instance (and through the cterm_symbolic factory) so downstream can tailor it; the on/off flag is threaded through execute/simplify/kast_simplify/implies and KCFGExplore.extend_cterm. - CTermSymbolic takes a haskell_log_dir: when set, every RPC requests the bundle and the entries returned on the response are written to /.jsonl (one JSON value per line, named by request id so concurrent proof workers never collide). - pyk prove --haskell-logging points that sink at /haskell-logs/ (requires --save-directory). Validation: - make -C pyk check clean. - Confirmed against the per-request-rpc backend implementation: it accepts haskell-logging: [String], routes the flat list to both engines (skipping names each does not recognise), tag-matches id-carrying contexts like Rewrite, and returns the captured entries in-band — pyk's default set is fully recognised, no skips. - Integration and regression-new not run locally (the machine's K install is pinned for a benchmark) — relying on CI. --------- Co-authored-by: Claude Opus 4.7 --- pyk/src/pyk/__main__.py | 7 + pyk/src/pyk/cli/pyk.py | 13 ++ pyk/src/pyk/cterm/symbolic.py | 102 ++++++++++- pyk/src/pyk/kcfg/explore.py | 2 + pyk/src/pyk/kore/rpc.py | 167 +++++++++++++++--- .../integration/kore/test_kore_client.py | 2 +- .../tests/integration/test_division_hooks.py | 2 +- pyk/src/tests/unit/kore/test_client.py | 2 +- 8 files changed, 264 insertions(+), 33 deletions(-) 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..8a23469ed8 100644 --- a/pyk/src/pyk/cli/pyk.py +++ b/pyk/src/pyk/cli/pyk.py @@ -318,6 +318,7 @@ class ProveOptions(LoggingOptions, SpecOptions, SaveDirOptions): max_iterations: int | None assume_defined: bool show_kcfg: bool + haskell_logging: bool @staticmethod def default() -> dict[str, Any]: @@ -330,6 +331,7 @@ def default() -> dict[str, Any]: 'max_iterations': None, 'assume_defined': False, 'show_kcfg': False, + 'haskell_logging': False, } @staticmethod @@ -520,6 +522,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..af8f9a4e36 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,32 @@ def kast_to_kore(self, kinner: KInner) -> Pattern: def kore_to_kast(self, pattern: Pattern) -> KInner: return kore_to_kast(self._definition, pattern) + 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 +161,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 +178,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 +211,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 +287,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 +312,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 +334,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 +416,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 +455,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..1eef51588a 100644 --- a/pyk/src/pyk/kcfg/explore.py +++ b/pyk/src/pyk/kcfg/explore.py @@ -218,6 +218,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 +235,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..e4e0355883 100644 --- a/pyk/src/pyk/kore/rpc.py +++ b/pyk/src/pyk/kore/rpc.py @@ -190,6 +190,7 @@ class JsonRpcClientFacade(ContextManager['JsonRpcClientFacade']): _clients: dict[str, list[JsonRpcClient]] _default_client: JsonRpcClient + _last_request_id: str | None def __init__( self, @@ -204,6 +205,7 @@ def __init__( ): client_cache = {} self._clients = {} + self._last_request_id = None self._default_client = JsonRpcClient( default_host, default_port, @@ -245,15 +247,23 @@ 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 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 +271,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 +288,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: @@ -304,6 +321,7 @@ def request(self, method: str, **params: Any) -> dict[str, Any]: 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 +644,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 +673,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 +698,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 +708,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 +722,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 +732,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 +746,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 +756,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 +770,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 +781,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 +795,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 +807,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 +821,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 +846,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 +856,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 +871,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 +882,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 +894,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 +907,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 +1003,17 @@ 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 _request(self, method: str, **params: Any) -> dict[str, Any]: try: return self._client.request(method, **params) @@ -978,6 +1062,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 +1077,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 +1092,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 +1101,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 +1114,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 +1348,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 +1479,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/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) From 69f2b84533fd66be2013ab4a2bea9c3f59f01fca Mon Sep 17 00:00:00 2001 From: devops Date: Fri, 5 Jun 2026 16:13:35 +0000 Subject: [PATCH 08/10] Set Version: 7.1.333 --- install-k | 2 +- package/debian/kframework/changelog | 2 +- package/version | 2 +- pyk/docs/conf.py | 4 ++-- pyk/pyproject.toml | 2 +- 5 files changed, 6 insertions(+), 6 deletions(-) diff --git a/install-k b/install-k index 9190e82709..84c2e9b92b 100755 --- a/install-k +++ b/install-k @@ -1,6 +1,6 @@ #!/bin/sh -e -K_VERSION=7.1.332 +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 0a822916bd..f55add2a85 100644 --- a/package/debian/kframework/changelog +++ b/package/debian/kframework/changelog @@ -1,4 +1,4 @@ -kframework (7.1.332) unstable; urgency=medium +kframework (7.1.333) unstable; urgency=medium * Initial Release. diff --git a/package/version b/package/version index 5dcfc81c62..6da8e9a46b 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -7.1.332 +7.1.333 diff --git a/pyk/docs/conf.py b/pyk/docs/conf.py index f1f758faf0..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.332' -release = '7.1.332' +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 885135d916..841ade38c6 100644 --- a/pyk/pyproject.toml +++ b/pyk/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "hatchling.build" [project] name = "kframework" -version = "7.1.332" +version = "7.1.333" description = "" readme = "README.md" requires-python = ">=3.10" From 25b62013fbe6f7d8b859e17f016f4d67e678337d Mon Sep 17 00:00:00 2001 From: Stevengre Date: Mon, 8 Jun 2026 16:55:43 +0800 Subject: [PATCH 09/10] Add step-timeout/shrink policy to Prover.advance_proof Implements runtimeverification/k#4924: factor kontrol's `--per-depth-timeout` mechanism out of tool-specific code and into a generic policy in `Prover.advance_proof`. `advance_proof` now runs each step under the prover's `step_timeout` (a per-step wall-clock budget). A step that exceeds its budget is interrupted, the prover is asked to `shrink_step` (do less work per step), and the step is retried (the timed-out node was never committed, so it reappears from `get_steps`). If the prover cannot shrink further, advancement stops. Provers without a `step_timeout` run synchronously as before, so `advance_proof` stays generic and gains no new parameter. - Prover: `step_timeout` attribute (whole seconds, None disables) plus no-op `shrink_step()` / `interrupt()` hooks - APRProver: `step_timeout` ctor arg (floored at 1s); `shrink_step` halves `execute_depth`; `interrupt` aborts the in-flight Kore request - KCFGExplore/CTermSymbolic/KoreClient/JsonRpc*/Transport: `interrupt()` that force-unblocks an in-flight single-socket request and reconnects - Unit tests: shrink-until-progress, stop-at-floor, fast-path, disabled --- pyk/src/pyk/cterm/symbolic.py | 4 + pyk/src/pyk/kcfg/explore.py | 4 + pyk/src/pyk/kore/rpc.py | 46 +++++++ pyk/src/pyk/proof/proof.py | 106 ++++++++++++--- pyk/src/pyk/proof/reachability.py | 15 +++ pyk/src/tests/unit/test_advance_proof.py | 160 +++++++++++++++++++++++ 6 files changed, 314 insertions(+), 21 deletions(-) create mode 100644 pyk/src/tests/unit/test_advance_proof.py diff --git a/pyk/src/pyk/cterm/symbolic.py b/pyk/src/pyk/cterm/symbolic.py index af8f9a4e36..66d178dcb3 100644 --- a/pyk/src/pyk/cterm/symbolic.py +++ b/pyk/src/pyk/cterm/symbolic.py @@ -127,6 +127,10 @@ 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. diff --git a/pyk/src/pyk/kcfg/explore.py b/pyk/src/pyk/kcfg/explore.py index 1eef51588a..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: diff --git a/pyk/src/pyk/kore/rpc.py b/pyk/src/pyk/kore/rpc.py index e4e0355883..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() @@ -252,6 +280,12 @@ 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]: @@ -316,6 +350,9 @@ 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)) @@ -1014,6 +1051,15 @@ def last_request_id(self) -> str | None: """ 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) 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/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/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 From fa4c4faf5ae3d1310715c13f3f11a59c0b9d3c34 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Mon, 8 Jun 2026 17:49:47 +0800 Subject: [PATCH 10/10] Expose --step-timeout as a prove CLI option The step-timeout/shrink policy added to Prover.advance_proof was reachable only programmatically. Wire it through the pyk prove command: add a step_timeout field to ProveOptions, a --step-timeout argument (whole seconds, floored at 1 by APRProver), and thread the value from ProveRpc into APRProver. Omitting the flag leaves step_timeout=None, preserving the prior synchronous behavior. --- pyk/src/pyk/cli/pyk.py | 13 +++++++++++++ pyk/src/pyk/proof/prove_rpc.py | 9 ++++++++- 2 files changed, 21 insertions(+), 1 deletion(-) diff --git a/pyk/src/pyk/cli/pyk.py b/pyk/src/pyk/cli/pyk.py index 8a23469ed8..75a9ecc1ed 100644 --- a/pyk/src/pyk/cli/pyk.py +++ b/pyk/src/pyk/cli/pyk.py @@ -316,6 +316,7 @@ 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 @@ -329,6 +330,7 @@ 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, @@ -515,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', 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: