pyk: booster-only recover mode for the APR prover, isolating and recording Kore handoffs#4931

Draft

ehildenb wants to merge 26 commits into

developfrom

proxy-prover

Commits on Jun 8, 2026

cterm/symbolic, kcfg/explore, tests/unit/cterm/test_symbolic: surface execute abort on CTermExecute, add raise_on_aborted

ehildenb
and
claude
committed
kore/rpc, cterm/symbolic, tests/unit/{kore/test_client,cterm/test_symbolic}: add indeterminate to ImpliesResult and CTermImplies

ehildenb
and
claude
committed
cterm/symbolic, tests/unit/cterm/test_symbolic: thread haskell_logging through execute, simplify, kast_simplify, implies

ehildenb
and
claude
committed
kcfg/explore, tests/unit/cterm/test_symbolic: thread booster_only_simplify/raise_on_aborted through extend_cterm

ehildenb
and
claude
committed
kcfg/{kcfg,explore}, proof/reachability, tests/unit/{test_proof,kcfg/test_explore}: move the stuck judgment from extend_cterm into commit

ehildenb
and
claude
committed
proof/reachability, tests/unit/test_proof: _check_subsume returns a tagged outcome, thread booster_only

ehildenb
and
claude
committed
kcfg/{kcfg,store}, tests/unit/test_kcfg: add Node.variants (Producer, NodeVariant) and public add_variant

ehildenb
and
claude
committed
kcfg/kcfg, tests/unit/test_kcfg: add recover-mode node attrs and KoreHandoff / kore_handoffs

ehildenb
and
claude
committed
kcfg/kcfg, tests/unit/kcfg/test_store: persist new attrs and variants through KCFGStore

ehildenb
and
claude
committed
kore/rpc, cterm/symbolic, kcfg/explore, tests/unit/kcfg/test_explore: variant-appending simplify helper with request_id + log-entry capture

ehildenb
and
claude
committed
proof/reachability, tests/unit/test_proof: recover_mode flag, recover_task on APRProofStep, task selection in get_steps

ehildenb
and
claude
committed
proof/reachability, tests/unit/test_proof: step_proof dispatch + recover-mode outcome types

ehildenb
and
claude
committed
proof/reachability, tests/unit/test_proof: commit transitions for recover-mode

ehildenb
and
claude
committed
proof/reachability, tests/unit/test_proof: write recover-logs/{request_id}.jsonl from outcomes

ehildenb
and
claude
committed
cli/pyk, proof/prove_rpc, tests/unit/test_toml_args: --booster-recover-mode through ProveOptions to APRProver

ehildenb
and
claude
committed
tests/integration/proof/test_imp: recover-mode prove of known IMP claims

ehildenb
and
claude
committed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

pyk: booster-only recover mode for the APR prover, isolating and recording Kore handoffs#4931

pyk: booster-only recover mode for the APR prover, isolating and recording Kore handoffs#4931
ehildenb wants to merge 26 commits into
developfrom
proxy-prover

Commits on Jun 8, 2026

cterm/symbolic, kcfg/explore, tests/unit/cterm/test_symbolic: surface execute abort on CTermExecute, add raise_on_aborted

kore/rpc, cterm/symbolic, tests/unit/{kore/test_client,cterm/test_symbolic}: add indeterminate to ImpliesResult and CTermImplies

cterm/symbolic, tests/unit/cterm/test_symbolic: thread haskell_logging through execute, simplify, kast_simplify, implies

kcfg/explore, tests/unit/cterm/test_symbolic: thread booster_only_simplify/raise_on_aborted through extend_cterm

kcfg/{kcfg,explore}, proof/reachability, tests/unit/{test_proof,kcfg/test_explore}: move the stuck judgment from extend_cterm into commit

proof/reachability, tests/unit/test_proof: _check_subsume returns a tagged outcome, thread booster_only

kcfg/{kcfg,store}, tests/unit/test_kcfg: add Node.variants (Producer, NodeVariant) and public add_variant

kcfg/kcfg, tests/unit/test_kcfg: add recover-mode node attrs and KoreHandoff / kore_handoffs

kcfg/kcfg, tests/unit/kcfg/test_store: persist new attrs and variants through KCFGStore

kore/rpc, cterm/symbolic, kcfg/explore, tests/unit/kcfg/test_explore: variant-appending simplify helper with request_id + log-entry capture

proof/reachability, tests/unit/test_proof: recover_mode flag, recover_task on APRProofStep, task selection in get_steps

proof/reachability, tests/unit/test_proof: step_proof dispatch + recover-mode outcome types

proof/reachability, tests/unit/test_proof: commit transitions for recover-mode

proof/reachability, tests/unit/test_proof: write recover-logs/{request_id}.jsonl from outcomes

cli/pyk, proof/prove_rpc, tests/unit/test_toml_args: --booster-recover-mode through ProveOptions to APRProver

tests/integration/proof/test_imp: recover-mode prove of known IMP claims

Commits on Jun 10, 2026

kore/rpc, cterm/symbolic, tests/unit/{cterm/test_symbolic,kore/test_client}: map kore Aborted (code 6) to AbortedError, treat aborted implies as indeterminate

tests/unit/{cterm/test_symbolic,kcfg/test_explore,test_proof}: trim #4928-logging scope-creep and in-flux recover-mode orchestration tests

kore/rpc, cterm/symbolic, kcfg/explore, proof/reachability: drop recover-mode per-request log capture, rely on #4928 haskell_log_dir

kcfg/kcfg, proof/reachability, kcfg/explore: enum-ize handoff flavour and recover backend, exhaustive task/backend matches, drop dangling design-doc refs

tests/unit/{test_proof,kcfg/test_explore,cterm/test_symbolic,test_kcfg}: drop in-flux orchestration tests, parameterize and consolidate the rest

proof/reachability, tests/unit/test_proof: short-circuit #Bottom cterms to Vacuous before recover-mode semantics callbacks

cterm/symbolic: drop unused CTermExecute.aborted flag

kore/rpc: drop drive-by MultipleStatesError (code 7) mapping

kcfg/store: drop stale design-doc reference from OptimizedNodeStore comment

kore/rpc, cterm/symbolic, proof/reachability: drop speculative ImpliesResult.indeterminate wire field