pyk: booster-only recover mode for the APR prover, isolating and recording Kore handoffs#4931
Draft
ehildenb wants to merge 26 commits into
Draft
pyk: booster-only recover mode for the APR prover, isolating and recording Kore handoffs#4931ehildenb wants to merge 26 commits into
ehildenb wants to merge 26 commits into
Conversation
… execute abort on CTermExecute, add raise_on_aborted Add `aborted: bool` to the CTermExecute NamedTuple and a `raise_on_aborted: bool = True` parameter to CTermSymbolic.execute. The default preserves today's raise-on-abort; passing False surfaces the AbortedResult as `aborted=True` instead of raising, which is the signal booster-only recover-mode needs. Fixes the one positional unpack of the tuple at explore.py (the only consumer that destructured it). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> (cherry picked from commit d4e9cb3966d821f3a422cfd1eb09e5c6769915a6)
…bolic}: add indeterminate to ImpliesResult and CTermImplies Surface the backend's additive `indeterminate :: Maybe Bool` (booster commit f911be4e0) — set only on MatchIndeterminate-no-progress, absent on every decisive verdict and error. Parsed onto ImpliesResult via `dct.get` and threaded onto CTermImplies, letting recover-mode tell a decisive invalid (trust) from a couldn't-determine (escalate to kore). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> (cherry picked from commit 0c7c26b83ae9218557b7017c412cf96bd08bed5f)
…g through execute, simplify, kast_simplify, implies
Add an optional haskell_logging per-call parameter to
CTermSymbolic.{execute,simplify,kast_simplify,implies} (including the recursive
failure-reason implies). Additive and default-preserving: omitting it reproduces
today's calls exactly (None leaves backend logging untouched).
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
(cherry picked from commit 4a3b142c80cd552a5df4961f1470d873fa83a84d)
…plify/raise_on_aborted through extend_cterm Forward the recover-mode per-call params booster_only_simplify and raise_on_aborted through KCFGExplore.extend_cterm to CTermSymbolic.execute (which already accepts them), and exercise raise_on_aborted in the extend-forwarding test. Additive and default-preserving. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> (cherry picked from commit 111113b034d9baaa68d21b09383076fffaa3d005)
…test_explore}: move the stuck judgment from extend_cterm into commit `extend_cterm` no longer decides `Stuck` for the depth-0 no-progress case; it emits the neutral `NoProgress` result instead. `step_proof` maps that to a new `APRProofStuckResult`, and `commit` is now the sole site that calls `add_stuck` — the coordinator owns the terminal judgment, which is the seam recover-mode needs. `Vacuous` stays in `extend_cterm` (a context-free semantic verdict) and `KCFG.extend`'s `Stuck` case is retained for other proof types. Behaviour is identical in normal mode: no-progress always becomes stuck. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> (cherry picked from commit 80b0a4aecd3eb0d47eace790c666e610958a898b)
…agged outcome, thread booster_only Replace `_check_subsume`'s `CSubst | None` return with a tagged `Subsumed(csubst) | DecisiveInvalid | Indeterminate`, built from the implies result's `csubst` + `indeterminate`, and thread a `booster_only` param into the implies call (default None reproduces today's instance-default behaviour). The single caller maps `Subsumed`→cover and the rest→execute, identical to the old `csubst is None`; the three-way classification is unit-tested directly. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> (cherry picked from commit b28db83e528d8d90d09e890e5791e156b9c97f40)
… NodeVariant) and public add_variant Add an additive simplification-provenance chain to KCFG.Node: a `Producer` enum, a `NodeVariant` record, and a `variants` tuple field (excluded from node equality/ordering/hash so identity is unchanged, omitted from `to_dict` when empty for byte-identical legacy serialisation). Public `KCFG.add_variant` appends a variant and makes its term canonical, seeding an INIT entry on the first call so the chain is self-contained — exposed for downstream init/target pre-simplification. `OptimizedNodeStore` now carries the chain through (it previously rebuilt nodes and dropped extra fields). Inert until wired in by the recover-mode commits that follow. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> (cherry picked from commit ed95720fd8ac1f6f766c9a72ac243c82758f755b)
…Handoff / kore_handoffs Add the inert recover-mode KCFGNodeAttrs (BOOSTER_TRIED, KORE_TRIED, SUBSUME_INDETERMINATE, BOTH_BACKENDS_FAILED) and a KoreHandoff record with a `kore_handoffs` list on KCFG (add/iter accessors), serialised additively in to_dict / to_dict_no_nodes (omitted when empty) and read back in from_dict. Inert until wired in by the recover-mode commits that follow. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> (cherry picked from commit d0e4b68045260256906e5d95d81a24ef9292c407)
… through KCFGStore Teach KCFGStore to round-trip the recover-mode state: the four new node attrs are persisted as top-level side-lists (alongside vacuous/stuck, driven by a single `_ATTR_SIDE_LISTS` map), `variants` is carried through from the per-node file instead of being dropped on read, and `kore_handoffs` rides the kcfg-level dict (via to_dict_no_nodes / from_dict). Reads use `dct.get` so legacy stores without the new keys still load. Round-trip + back-compat unit tests added. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> (cherry picked from commit 4454551e39791caba3eed9e514e3fcf10e9f29df)
… variant-appending simplify helper with request_id + log-entry capture Mirror the `last_request_id` thread-local with a `last_haskell_log_entries` one (captured generically in KoreClient._request), exposed via CTermSymbolic passthrough accessors. Add KCFGExplore.simplify_variant: re-simplifies a cterm with one backend (haskell_logging on) and returns a SimplifyVariant carrying the producer, simplified cterm, request_id, and captured log bundle — for the coordinator to land via KCFG.add_variant and store. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> (cherry picked from commit 3eaa3e3cd05d513e29766dbf8305b1a3ab195f96)
…_task on APRProofStep, task selection in get_steps Add a RecoverTask enum, `recovery_rung`/`recover_task_for` helpers implementing the recover-mode task-choice rules (rung + attrs → task), a `recover_task` field on APRProofStep, and a `recover_mode` flag on APRProver (propagated onto APRProof in init_proof so the coordinator's get_steps/commit can use it). get_steps stamps the per-node task and disables extend-and-cache in recover-mode. Inert when recover_mode is off; task-selection table unit-tested incl. the no-op case. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> (cherry picked from commit e3bb6627cc508a2afd4b482bfd6b46ca4704dec9)
…ver-mode outcome types Add recover-mode worker outcomes (AddVariant, RecoverNoProgress, RecoverAdvance, RecoverClose) carrying per-call LoggedCalls and, for kore steps, the decisive request id for commit to build a KoreHandoff. step_proof dispatches to a self-contained _recover_step (simplify, or a backend-parameterized subsume-then-execute try) when recover_task is set; the normal path is untouched. TRY_KORE executes depth=1 and runs a kore implies only when the node carries SUBSUME_INDETERMINATE; the recover-mode logging policy gates which calls are captured. _check_subsume also threads haskell_logging. commit wiring lands in a following commit. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> (cherry picked from commit 49ba6c0ca1b95fc529b65d5648a2452069d0a7d7)
…over-mode commit now lands the recover-mode outcomes: AddVariant appends the variant and clears BOOSTER_TRIED/SUBSUME_INDETERMINATE iff the term changed (the no-op short-circuit); no-progress sets the per-backend attr (+ SUBSUME_INDETERMINATE) and, at rung-2 exhaustion of both backends, tags BOTH_BACKENDS_FAILED and marks the node stuck; kore advance/close apply the extension/cover and record the execute/implies KoreHandoff (execute target resolved to the new successor). Tests cover the full ladder walk to BOTH_BACKENDS_FAILED, the no-op short-circuit, and handoff attribution. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> (cherry picked from commit 7f4f82b39c883d593fdf39f7aa5bb4365ae1136a)
…t_id}.jsonl from outcomes
commit now writes one `{proof_subdir}/recover-logs/{request_id}.jsonl` per
logged kore call carried on a recover outcome (one entry per line, --log-format
json shape, so it feeds parse_kore_log). Disk writes stay on the coordinator
(main) thread; no-ops for in-memory proofs or calls that captured nothing.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
(cherry picked from commit f1fe0a567f7fd88744070ee69d65480cb153b37f)
…r-mode through ProveOptions to APRProver Add the `--booster-recover-mode` CLI flag and `booster_recover_mode` ProveOptions field, threaded through prove_rpc → _prove_claim_rpc → APRProver(recover_mode=…). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> (cherry picked from commit 3075366ae1167fcc137e1170bfbeb8f5ed1bc8c6)
Add an integration test that proves addition-1/addition-2/pre-branch-proved with APRProver(recover_mode=True) and asserts they still PASS — recover-mode works as well as the normal prover — while checking the diagnostic state stays well-formed (every kore_handoff names a backend + request id; each node's canonical term matches its variant chain's tail). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> (cherry picked from commit 80e56273c4388ff6811685edbda53ec6ef144849)
ehildenb
changed the title
…lient}: map kore Aborted (code 6) to AbortedError, treat aborted implies as indeterminate Recover-mode's TRY_KORE rung calls kore-implies directly (booster_only=False), so a kore-rpc `Aborted` response (`code: 6`, e.g. data "unknown constraints") surfaced as an unhandled `DefaultError` and crashed the proof. The two-engine proxy absorbs this error for normal implies traffic, so normal-mode never saw it. Map the backend's `Aborted` (code 6) and `MultipleStates` (code 7) — the two `JsonRpcBackendError` constructors that were missing from `KoreClient._error` — to named `KoreClientError` subclasses. Catch `AbortedError` in `CTermSymbolic.implies`, alongside the existing `SmtSolverError` handler, and surface it as an indeterminate, not-subsumed `CTermImplies` (indeterminate=True) — uniform with how booster-implies reports a MatchIndeterminate, which `_check_subsume` already turns into `Indeterminate`. An aborted implication is "couldn't decide," never a claimed subsumption, so this is sound: the proof continues/finalizes as not-subsumed instead of crashing. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> (cherry picked from commit ec5541b363cce4babc6da0729f04bca18d0b5834)
…4928-logging scope-creep and in-flux recover-mode orchestration tests Drop the per-request-logging tests that belong to the already-merged #4928 feature (entry-set requests, haskell_log_dir bundle writing, cterm_symbolic factory wiring) and the brittle Mock-dispatch recover-mode tests that pin in-flux orchestration. Keep the stable contracts: abort/indeterminate handling, recover task-selection decision tables, KCFG commit transitions, and the simplify_variant producer/request_id mapping. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…ver-mode per-request log capture, rely on #4928 haskell_log_dir The per-request haskell-log bundle is already captured and written by the merged #4928 feature (CTermSymbolic.haskell_log_dir -> <dir>/<request_id>.jsonl, entries returned in-band on every result). Remove recover-mode's parallel path: the thread-local last_haskell_log_entries capture in KoreClient, the CTermSymbolic passthrough property, the SimplifyVariant/outcome log_entries fields, and the dedicated recover-logs writer. Recover-mode keeps only the request_id, recorded on KoreHandoff as the join key into the #4928 log file for the same request. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
… and recover backend, exhaustive task/backend matches, drop dangling design-doc refs Promote the two stringly-typed recover-mode flags to enums per the structured-data convention: KoreHandoff.flavour -> HandoffFlavour (kcfg/kcfg) and the recover no-progress backend -> RecoverBackend (proof/reachability). Replace the corresponding catch-all branches with exhaustive matches (RecoverTask in _recover_step, RecoverBackend in _commit_recover_no_progress) so an added variant is a type error, not a silent fall-through. Drop the bare "(see CN)"/"§N" markers that referenced an out-of-tree design doc; the surrounding prose stands on its own. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…g}: drop in-flux orchestration tests, parameterize and consolidate the rest
Apply the testing policy to the recover-mode unit tests: don't pin a feature still in
flux, and prefer parameterized harnesses (extensible) over one-off bespoke ones.
Drop:
- the commit-transition block in test_proof (6 tests + _recover_proof/_no_progress/_add_variant
helpers) — it built a bespoke harness for one-off tests pinning the in-flux APRProof.commit
state machine, which the end-to-end test_imp recover-mode test already exercises behaviourally;
- test_recover_task_noop_shortcircuit — fully redundant with the rung1-tried row already in the
parametrized _TASK_DATA;
- the two simplify_variant tests — glue around a one-line producer conditional.
Consolidate one-off clusters that shared a harness into parameterized tables:
- test_recovery_rung -> parametrized over node rung configs;
- test_extend_cterm_{no_progress,step} -> one parametrized classify test;
- the two non-raising execute-abort tests -> one parametrized surface test (the default-raises
property stays separate);
- the three Node serialisation round-trips -> one parametrized round-trip plus a single
omitted-when-empty back-compat test.
Keep the genuine property tests (add_variant chain semantics, equality-ignores-variants,
store round-trip/back-compat, idempotence, fast-skip short-circuit) and the parametrized
decision-table and wire-parsing tests.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…ms to Vacuous before recover-mode semantics callbacks A recover-mode booster-only re-simplify can collapse a vacuous node's configuration to bare #Bottom, which add_variant installs as the node's canonical cterm. Semantics callbacks that destructure cells (e.g. KEVM's is_terminal reading the K cell) then crash on the next ladder step. Guard step_proof: a recover-task step on a bottom cterm returns the same Vacuous extend result the normal path produces, so commit marks the node vacuous before any semantics callback runs. Reported by Kontrol's recover-mode experiment (k-pr-change-request.md). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Nothing consumes it: extend_cterm ignores the field and the recover ladder sees a no-progress abort as a depth-0 NoProgress result. The load-bearing surface is raise_on_aborted=False (do not crash on AbortedResult), which stays. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Only the Aborted (code 6) mapping is load-bearing for recover-mode; code 7 keeps falling through to DefaultError as before this branch. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…omment Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…sResult.indeterminate wire field No released backend sends it (pinned v0.1.150 reports an indeterminate booster implies as a plain valid:false), and the backend's indeterminate reporting is being reworked separately -- baking in this wire shape now is premature. The recover ladder's live indeterminate signal is the abort-shaped implies (code 6 -> AbortedError), carried on the internal CTermImplies.indeterminate, which becomes a plain bool fed only by that catch. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
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
1 participant
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.
No description provided.