Add progressive depth-halving policy to Prover.advance_proof#2
Closed
Stevengre wants to merge 14 commits into
Closed
Add progressive depth-halving policy to Prover.advance_proof#2Stevengre wants to merge 14 commits into
Stevengre wants to merge 14 commits into
Conversation
Stevengre
force-pushed
the
feat/per-depth-timeout-advance-proof
branch
2 times, most recently
from
afffa34 to
a3cda8c
Compare
…4926) Co-authored-by: devops <devops@runtimeverification.com>
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 <noreply@anthropic.com>
…4929) Co-authored-by: devops <devops@runtimeverification.com>
~Blocked on: runtimeverification/haskell-backend#4151 ~Blocked on: runtimeverification#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 <haskell_log_dir>/<request_id>.jsonl (one JSON value per line, named by request id so concurrent proof workers never collide). - pyk prove --haskell-logging points that sink at <save-directory>/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 <noreply@anthropic.com>
Stevengre
force-pushed
the
feat/per-depth-timeout-advance-proof
branch
from
a3cda8c to
a05123d
Compare
Implements runtimeverification#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
Stevengre
force-pushed
the
feat/per-depth-timeout-advance-proof
branch
from
a05123d to
25b6201
Compare
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.
Stevengre
force-pushed
the
feat/per-depth-timeout-advance-proof
branch
from
b7bd030 to
fa4c4fa
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
4 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Implements runtimeverification#4924.
Factors kontrol's
--per-depth-timeoutmechanism out of tool-specific code and into a generic policy inProver.advance_proof, as suggested by @ehildenb in this review comment.What it does
advance_proofnow runs each step under the prover'sstep_timeout— a per-step wall-clock budget (whole seconds, minimum 1;Nonedisables the policy). When astep_proofexceeds its budget:shrink_step(do less work per step), andget_steps.If the prover cannot shrink any further, advancement stops (the proof stays pending). Provers that don't set a
step_timeoutrun steps synchronously, exactly as on master.How it stays generic
The policy lives entirely in the base
Proverand is driven by:step_timeout: int | None— attribute; per-step budget in whole seconds,Noneopts out.shrink_step() -> bool— reduce per-step work; returnFalsewhen already minimal (no-op default).interrupt()— abort an in-flightstep_proofon another thread (no-op default).advance_proofnever mentions "depth" — it only knows about a per-step budget and an opaque "shrink" operation. The depth knob stays a prover concern:APRProvertakes astep_timeoutctor arg (floored at 1s);shrink_stephalvesexecute_depth;interruptcallskcfg_explore.interrupt().To actually abort an in-flight Kore RPC call,
interrupt()is threaded throughKCFGExplore→CTermSymbolic→KoreClient→JsonRpcClientFacade/JsonRpcClient→Transport.SingleSocketTransport.interrupt()shuts down the blocked socket (unblocking the reader thread) and reconnects so the prover stays usable;HttpTransport.interrupt()is a documented no-op.Testing
pyk/src/tests/unit/test_advance_proof.py(in-memory fake prover, no backend): covers shrink-until-progress, stop-when-cannot-shrink, no-shrink-when-fast, and the disabled (nostep_timeout) path.make -C pyk checkpasses (flake8, mypy, autoflake, isort, pydocstyle, black).Notes / follow-up
Client-side
interrupt()reconnects to the sameKoreServer(preserving added modules), but an abandoned computation may keep running server-side until it notices the dropped connection — unlike kontrol's full process-group kill. The shallower retry still proceeds correctly; a fully faithful server-restart variant would require the prover to own the server handle and is left as a follow-up.CLI flag plumbing remains on the tool side (e.g. kontrol sets
APRProver(step_timeout=...)); this PR only provides the generic capability.