Add progressive depth-halving policy to Prover.advance_proof

.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

deps/haskell-backend_release

@@ -1 +1 @@
-v0.1.147
+v0.1.150

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";
     };

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."

package/debian/kframework/changelog

@@ -1,4 +1,4 @@
-kframework (7.1.329) unstable; urgency=medium
+kframework (7.1.333) unstable; urgency=medium
 
   * Initial Release.
 

package/version

@@ -1 +1 @@
-7.1.329
+7.1.333

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

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"

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)
 

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,13 +517,35 @@ 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',
         type=str,
         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"
+            ' <save-directory>/haskell-logs/<request_id>.jsonl (one JSON value per line).'
+            ' Requires --save-directory.'
+        ),
+    )
 
     show_args = pyk_args_command.add_parser(
         'show',