Set Version: 1.0.255

feat: add `--step-timeout` option for kontrol prove (#1160)

Exposes pyk's per-step timeout through `kontrol prove`. When
`--step-timeout S` is set, each rewrite step is given a wall-clock budget
of `S` whole seconds; on timeout the backend request is interrupted, the
execution depth is halved, and the step is retried (enforced by
`APRProver`, threaded via `run_prover`).

Default `None` disables the timeout, leaving prior behavior unchanged.

Set Version: 1.0.253

Update dependency: deps/kevm_release (#1159)

* deps/kevm_release: Set Version 1.0.920

* Sync uv files: kevm-pyk version 1.0.920

* flake.{nix,lock}: update Nix derivations

* deps/kevm_release: Set Version 1.0.921

* Sync uv files: kevm-pyk version 1.0.921

* flake.{nix,lock}: update Nix derivations

---------

Co-authored-by: devops <devops@runtimeverification.com>

avoid raising the FileNotFoundError while reading the proofs (#1156)

Co-authored-by: Palina <palina.tolmach@runtimeverification.com>

Update dependency: deps/kevm_release (#1158)

* deps/kevm_release: Set Version 1.0.919

* Sync uv files: kevm-pyk version 1.0.919

* deps/k_release: sync release file version 7.1.337

* flake.{nix,lock}: update Nix derivations

---------

Co-authored-by: devops <devops@runtimeverification.com>

Update dependency: deps/kevm_release (#1157)

* deps/kevm_release: Set Version 1.0.918

* Sync uv files: kevm-pyk version 1.0.918

* deps/k_release: sync release file version 7.1.336

* flake.{nix,lock}: update Nix derivations

---------

Co-authored-by: devops <devops@runtimeverification.com>

Set Version: 1.0.250

Update dependency: deps/kevm_release (#1155)

* deps/kevm_release: Set Version 1.0.917

* Sync uv files: kevm-pyk version 1.0.917

* deps/k_release: sync release file version 7.1.335

* flake.{nix,lock}: update Nix derivations

---------

Co-authored-by: devops <devops@runtimeverification.com>

Thread Haskell-backend logging and booster-only-simplify flags (#1149)

* cli,options,prove,foundry,display: thread Haskell-backend logging + booster-only-simplify flags; CLAUDE.md: document

Propagate the opt-in Haskell-backend RPC logging from KEVM PR
runtimeverification/evm-semantics#2857 into kontrol.

Adds `--haskell-log-dir`, `--haskell-log-entries`, and
`--booster-only-simplify` to the shared `RpcOptions`, threaded through
the direct `CTermSymbolic` construction in `prove.py` and through every
`kevm_pyk.utils.legacy_explore` call site (`simplify-node`, `step-node`,
`section-edge`, `get-model`, `show --failure-info`). When omitted, the
log entry set defaults to pyk's curated `HASKELL_LOGGING_ENTRIES`.

CLAUDE.md documents the debugging workflow the flags enable.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

* options,prove,tests/test_toml_args: default --haskell-log-entries to curated set for all RPC commands

The curated HASKELL_LOGGING_ENTRIES fallback was applied only at the
prove call site, so show/simplify-node/step-node/section-edge/get-model
passed an empty entries list and captured nothing when --haskell-log-dir
was set without --haskell-log-entries. Resolve the default once in
RpcOptions so every consumer gets the curated set, and drop the now-redundant
`or HASKELL_LOGGING_ENTRIES` special-case in prove.py.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

* CLAUDE.md: document architecture, dev/build workflow, commands, tests, deps, and kup overrides

Expand the project conventions doc beyond the Haskell-logging debug section
with durable orientation that should not need rediscovery: the src/kontrol
module layout and Options pattern, the make-based check/format/test workflow,
kdist targets, the kontrol command set and proof loop, the three test suites
and their custom pytest options, dependency/release/Nix packaging, and kup
--version/--override syntax for pinning the K toolchain.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

* tests/{conftest,test_foundry_prove}: forward --haskell-log-dir pytest option into ProveOptions

Mirror KEVM's test harness: add a --haskell-log-dir pytest option (and a
session fixture that creates the directory) and thread it into the main
foundry-prove test's ProveOptions. Defaults to None, so the suite is
unchanged unless the flag is passed; when set, the existing CTermSymbolic
logging path captures one <request-id>.jsonl bundle per RPC, and
--haskell-log-entries defaults to the curated set so logs are non-empty.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

---------

Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>